obj DATA is pr BOOL .
    sort Medium .
    ops land water : -> Medium .
  endo

  th BASE is sorts Object Person .  pr DATA .
    op object : -> Object .
    op person : -> Person .
    op medium : -> Medium .
    op use : Person Object -> Bool .
    op on  : Object Medium -> Bool .
    eq use(person, object) = true .
    eq on(object, medium)  = true .
  endth

  th HOUSE is sorts Object Person .  pr DATA .
    op house    : -> Object .
    op resident : -> Person .
    op live-in  : Person Object -> Bool .
    op on       : Object Medium -> Bool .
    eq live-in(resident, house) = true .
    eq on(house, land) = true .
  endth

  th BOAT is sorts Object Person .  pr DATA .
    op boat  : -> Object .
    op psngr : -> Person .
    op ride  : Person Object -> Bool .
    op on    : Object Medium -> Bool .
    eq ride(psngr, boat) = true .
    eq on(boat, water)   = true .
  endth

  view M1 from BASE to HOUSE is
    op object to house .
    op person to resident .
    op use to live-in .
    op medium to land .
  endv

  view M2 from BASE to BOAT is
    op object to boat .
    op person to psngr .
    op use to ride .
    op medium to water .
  endv

  th BASE is sorts Object Person .  pr DATA .
    op object : -> Object .
    op person : -> Person .
    op use    : Person Object -> Bool .
    op on     : Object Medium -> Bool .
    eq use(person, object) = true .
  endth

  view M1 from BASE to HOUSE is
    op object to house .
    op person to resident .
    op use to live-in .
  endv

  view M2 from BASE to BOAT is
    op object to boat .
    op person to psngr .
    op use to ride .
  endv

  th HOUSEBOAT is sorts Object Person .  pr DATA .
    op houseboat : -> Object .
    op resident  : -> Person .
    op live&ride : Person Object -> Bool .
    op on        : Object Medium -> Bool .
    eq live&ride(resident, houseboat) = true .
    eq on(houseboat, water) = true .
  endth

  view M3 from HOUSE to HOUSEBOAT is
    op house to houseboat .
    op live-in to live&ride .
  endv

  view M4 from BOAT to HOUSEBOAT is
    op boat to houseboat .
    op psngr to resident .
    op ride to live&ride .
  endv

  view C from BASE to HOUSEBOAT is
    op object to houseboat .
    op person to resident .
    op use to live&ride .
  endv

  th BOATHOUSE is sorts Object Person .  pr DATA .
    op boathouse : -> Object .
    op boat      : -> Object .
    op live-in   : Person Object -> Bool .
    op on        : Object Medium -> Bool .
    eq live-in(r:Universal>Person(boat), boathouse) = true .
    eq on(boathouse, land) = true .
    eq on(boat, water)     = true .
    op psngr : -> Person .
    op ride : Person Object -> Bool .
    eq ride(psngr, boat) = true .
  endth

  red boat . 
  red r:Universal>Person(boat).
  red ~setsort~(Person, boat). 
  red live-in(boat, boathouse).
  red live-in(r:Universal>Person(boat), boathouse).
  red live-in(~setsort~(Person, boat), boathouse).

  view M3 from HOUSE to BOATHOUSE is
    op house to boathouse .
    op resident to r:Universal>Person(boat) .
  endv

  view M4 from BOAT to BOATHOUSE is
  endv

  view C from BASE to BOATHOUSE is
    op object to boathouse .
    op person to boat .
    op use to live-in .
  endv

  obj DATA is pr BOOL .
    sort Medium .
    ops land water land-or-water : -> Medium .
  endo

  th BOATHOUSE is sorts Object Person .  pr DATA .
    op boathouse : -> Object .
    op boat      : -> Object .
    op live-in   : Person Object -> Bool .
    op on        : Object Medium -> Bool .
    eq live-in(~setsort~(Person, boat), boathouse) = true .
    eq on(boathouse, land) = true .
    eq on(boat, water)     = true .
    op psngr : -> Person .
    op ride : Person Object -> Bool .
    eq ride(psngr, boat) = true .
  endth

  red boat . 
  red r:Universal>Person(boat).
  red ~setsort~(Person, boat). 
  red live-in(boat, boathouse).
  red live-in(r:Universal>Person(boat), boathouse).
  red live-in(~setsort~(Person, boat), boathouse).

  th BOATHOUSE is sorts Object Person .  pr DATA .
     subsort Object < Person .
    op boathouse : -> Object .
    op boat      : -> Object .
    op live-in   : Person Object -> Bool .
    op on        : Object Medium -> Bool .
    eq on(boathouse, land) = true .
    eq on(boat, water)     = true .
    op psngr : -> Person .
    op ride : Person Object -> Bool .
    eq ride(psngr, boat) = true .
  endth

  red boat . 
  red r:Universal>Person(boat).
  red ~setsort~(Person, boat). 
  red live-in(boat, boathouse).
  red live-in(r:Universal>Person(boat), boathouse).
  red live-in(~setsort~(Person, boat), boathouse).