fmod NAT-DIV is
   sorts Nat NzNat .
   subsort NzNat < Nat .
   op 0 : -> Nat .
   op s : Nat -> NzNat .
   op _+_ : Nat Nat -> Nat .
   op _*_ : Nat Nat -> Nat .
   op _-_ : Nat Nat -> Nat .
   op _<=_ : Nat Nat -> Bool .
   op _>_ : Nat Nat -> Bool .
   op _div_ : Nat NzNat -> Nat .
   op _mod_ : Nat NzNat -> Nat .

   vars M N : Nat .
   var P : NzNat .

   eq 0 + N = N .
   eq s(M) + N = s(M + N) .
   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 N > M = not (N <= M) .
   ceq N div P = 0 if P > N .
   ceq N div P = s((N - P) div P) if P <= N .
   ceq N mod P = N if P > N .
   ceq N mod P = (N - P) mod P if P <= N .
endfm

red s(s(s(s(s(0))))) * s(s(s(s(0)))) div s(s(s(0))) . 
***(
*** 5 * 4 div 3
WARNING: <standard input>, line 605: Ambiguous term, two parses
    are:
s(s(s(s(s(0))))) * (s(s(s(s(0)))) div s(s(s(0))))
-versus-
(s(s(s(s(s(0))))) * s(s(s(s(0))))) div s(s(s(0)))

Arbitrarily taking the first as correct.
reduce in NAT-DIV : s(s(s(s(s(0))))) * (s(s(
    s(s(0)))) div s(s(s(0)))) .
rewrites: 43 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(s(s(s(s(0)))))

*** need prec values different from the ones by default,
*** or parentheses
)

red (s(s(s(s(s(0))))) * s(s(s(s(0))))) div s(s(s(0))) . 
*** -                                -
***(
*** (5 * 4) div 3
reduce in NAT-DIV : (s(s(s(s(s(0))))) * s(s(s(s(0))))) div
    s(s(s(0))) .
rewrites: 154 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(s(s(s(s(s(0))))))
)

red (s(s(s(s(s(0))))) * s(s(s(s(0))))) mod s(s(s(0))) .
***(
*** (5 * 4) mod 3
reduce in NAT-DIV : (s(s(s(s(s(0))))) * s(s(s(s(
    0))))) mod s(s(s(0))) .
rewrites: 154 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(s(0))
)