fmod MYNAT-SIMPLE is

sort Nat .

op 0 : -> Nat .

op s_ : Nat -> Nat .

op _+_ : Nat Nat -> Nat .

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

vars N M : Nat .

eq 0 + M = M .

eq (s N) + M = s(N + M) .

eq 0 < 0 = false .
eq 0 < (s N) = true  .
eq (s M) < 0 = false .
eq (s M) < (s N) = M < N .

eq M > N = N < M .


endfm

red (s s s 0) > (s s 0) .