set include BOOL off .

in basic-nat.maude
in boolean.maude

set include BOOL off .

fmod NAT+OPS is
   protecting BOOLEAN .
   protecting BASIC-NAT .

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

   vars N M : Nat .
   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 .