set include BOOL off .

fmod NAT+OPS is
   *** copy of BOOLEAN
   sort Bool .
   op true : -> Bool .
   op false : -> Bool .
   op not_ : Bool -> Bool .
   op _and_ : Bool Bool -> Bool .
   op _or_ : Bool Bool -> Bool .
   var A : Bool .
   eq not true = false .
   eq not false = true .
   eq true and A = A .
   eq false and A = false .
   eq true or A = true .
   eq false or A = A .

   *** copy of BASIC-NAT
   sort Nat .
   op 0 : -> Nat .
   op s : Nat -> Nat .
   op _+_ : Nat Nat -> Nat .
   vars N M : Nat .
   eq 0 + N = N .
   eq s(M) + N = s(M + N) .

   op _*_ : Nat Nat -> Nat .
   op _-_ : Nat Nat -> Nat .
   op _<=_  : Nat Nat -> Bool .
   op _>_ : Nat Nat -> Bool .

   eq 0 * N = 0 .
   eq s(M) * N = (M * N) + N .
   eq 0 - N = 0 .
   eq s(M) - 0 = s(M) .
   eq s(M) - s(N) = M - N .
   eq 0 <= N = true .
   eq s(M) <= 0 = false .
   eq s(M) <= s(N) = M <= N .
   eq M > N = not (M <= N) .
endfm

red s(s(s(0))) * s(s(0)) > s(s(s(0)) - s(0)) .
***(
reduce in NAT+OPS : (s(s(s(0))) * s(s(0))) > s(s(s(0)) - s(0)) .
rewrites: 20 in -10ms cpu (0ms real) (~ rewrites/second)
result Bool: true
)

set include BOOL on .