---- AND optimization on
---- CS-TRS Transf.: Zantema's
---- CiME: 
---- AProVE: 
----   Typing desugaring: Complete
----     Termination of R could not be shown. (Duration: 1:00 minutes)
----   Typing desugaring: No Sorts
----     Termination of R successfully shown.
----   Typing desugaring: No Kinds
----     Non-Termination of R could be shown.
---- MU-TERM: 

(fmod TRUTH-VALUE is
   sort Bool .
   op true : -> Bool [ctor] .
   op false : -> Bool [ctor] .
 endfm)

(fmod TRUTH is
   protecting TRUTH-VALUE .
   sort S .
   op if_then_else_fi : Bool Universal Universal -> Universal 
        [poly (2 3 0)] .

   op _==_ : Universal Universal -> Bool 
        [prec 51 poly (1 2)] .

   op _=/=_ : Universal Universal -> Bool 
        [prec 51 poly (1 2)] .

   eq (if true then U:S else U':S fi) = U:S .
   ceq (if B:Bool then U:S else U':S fi) = U':S if B:Bool =/= true .

   eq U:S == U:S = true .
   ceq U:S == U':S = false if (U:S =/= U':S) .

   eq U:S =/= U:S = false .
   eq U:S =/= U':S = if U:S == U':S then false else true fi .

   op not_ : Bool -> Bool [prec 53] .
   eq not true = false .
   eq not false = true .
 endfm)

(fmod BOOL is
   protecting TRUTH .
   op _and_ : Bool Bool -> Bool [assoc comm prec 55] .
   op _or_ : Bool Bool -> Bool [assoc comm prec 59] .
   op _xor_ : Bool Bool -> Bool [assoc comm prec 57] .
   op not_ : Bool -> Bool [prec 53] .
   op _implies_ : Bool Bool -> Bool [gather (e E) prec 61] .
   vars A B C : Bool .
   eq true and A = A .
   eq false and A = false .
   eq A and A = A .
   eq false xor A = A .
   eq A xor A = false .
   eq A and (B xor C) = A and B xor A and C .
   eq not A = A xor true .
   eq A or B = A and B xor A xor B .
   eq A implies B = not(A xor A and B) .
 endfm)

(fmod RENAMED-BOOL is
   pr BOOL * (op _==_ to _isEqualTo_, op _=/=_ to _isNotEqualTo_) .
 endfm)

---(
set trace on .
trace include FULL-MAUDE .
set trace select on .
trace select muTermPrettyPrint .
trace select ucrt2uurt .
trace select met2urt .
trace select desugarMets .

(MU-TERM complete and-optimization off .)
(MU-TERM no sorts and-optimization off .)
(MU-TERM no kinds and-optimization off .)
)