---- typing desugaring: complete
---- termination criterion: minimal
---- polynomial interpretation: linear (2), simple-mized (6)
---- CS-TRS transf.: no transformation

(fmod MYNAT is
  sort Nat .
  op 0 : -> Nat .
  op s : Nat -> Nat .
  op plus : Nat Nat -> Nat .
  vars N M : Nat .
  eq plus(N, 0) = N .
  eq plus(N, s(M)) = s(plus(N, M)) .
 endfm)