fmod BASIC-NAT is
   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) .
endfm

red s(0) + s(s(s(s(s(0))) + s(s(0)))) .
***(
reduce in BASIC-NAT : s(0) + s(s(s(s(s(0))) + s(s(0)))) .
rewrites: 6 in -10ms cpu (0ms real) (~ rewrites/second)
result Nat: s(s(s(s(s(s(s(s(0))))))))
)