==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm) .
rewrites: 1
result Bool: true
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm) .
rewrites: 1
result Bool: false
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  subsort 'Foo < 'Bar .
  op 'a : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm) .
Warning: the connected component in the sort graph that contains sort Bar has
    no maximal sorts due to a cycle.
rewrites: 1
result Bool: false
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm, 'a.Foo) .
rewrites: 1
result Bool: true
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm, 'b.Foo) .
rewrites: 1
result Bool: false
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm, 
  'X:Foo <- 'a.Foo) .
rewrites: 2
result Bool: true
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm, 
  'X:Foo <- 'a.Foo ; 
  'Y:Foo <- 'a.Foo) .
rewrites: 3
result Bool: true
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm, 
  'X:Foo <- 'a.Foo ; 
  'Y:Foo <- 'b.Foo) .
rewrites: 1
result Bool: false
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm, (none).Substitution) .
rewrites: 1
result Bool: true
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  op 'b : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm, 
  'X:Foo <- 'a.Foo ; 
  'X:Foo <- 'b.Foo) .
rewrites: 1
result Bool: false
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'FLOAT .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  op 'b : nil -> 'Foo [none] .
  none
  none
endfm, 
  'X:Bar <- 'a.Foo) .
rewrites: 1
result Bool: false
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'BOOL .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  op 'b : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm, 
  'X:Bar <- 'true.Bool) .
rewrites: 1
result Bool: false
==========================================
reduce in META-LEVEL : wellFormed(fmod 'FOO is
  protecting 'BOOL .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  op 'b : nil -> 'Foo [none] .
  mb 'a.Foo : 'Bar [none] .
  none
endfm, 
  'X:Bool <- 'true.Bool) .
rewrites: 1
result Bool: true
==========================================
reduce in META-LEVEL : wellFormed(mod 'FOO is
  protecting 'BOOL .
  sorts 'Bar ; 'Foo .
  subsort 'Bar < 'Foo .
  op 'a : nil -> 'Foo [none] .
  op 'b : nil -> 'Foo [none] .
  none
  none
  rl 'a.Foo => 'b.Foo [label('k)] .
endm, 
  'X:Bar <- 'true.Bool) .
rewrites: 1
result Bool: false
Bye.