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

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