fmod NAT-TEST is
  sorts Nat Int .
  subsort Nat < Int .

  op 0 : -> Nat [ctor].
  op s_ : Nat -> Nat [ctor iter prec 35].

  var M N : Nat .

  op _+_ : Nat Nat -> Nat [prec 50].
  eq M + s N = s (M + N) .
  eq M + 0 = M .

  op _*_ : Nat Nat -> Nat [prec 45].
  eq M * s N = (M * N) + M .
  eq M * 0 = 0 .
endfm