(fmod ACK is
  sort Nat .
  op 0 : -> Nat [ctor] .
  op s : Nat -> Nat [ctor] .
  op ack : Nat Nat -> Nat .
  vars N M : Nat .
  eq ack(0,M) = s(M) .
  eq ack(s(N),0) = ack(N,s(0)) .
  eq ack(s(N),s(M)) = ack(N,ack(s(N),M)) .
endfm)