obj NAT is
  sort Nat .
  op  0 : -> Nat .
  op s_ : Nat -> Nat [prec 1].
  op _+_ : Nat Nat -> Nat [assoc comm]
  var M N : Nat .
  eq M + 0 = M .
  eq M + s N = s(M + N) .
  op _*_ : Nat Nat -> Nat .
  eq M * 0 = 0 .
  eq M * s N = (M * N) + M .
endo