fmod NATURAL is
  sort Natural .
  op zero : -> Natural [ctor] .
  op s : Natural -> Natural [ctor] .
  ops rem2 quo2 : Natural -> Natural .
  op _+'_ : Natural Natural -> Natural .
  op _*'_ : Natural Natural -> Natural .
  vars N M : Natural .
  eq N +' zero = N .
  eq N +' s(M) = s(N +' M) .
  eq N *' zero = zero .
  eq N *' s(M) = N +' (N *' M) .
  eq rem2(s(s(N))) = rem2(N) .
  eq rem2(s(zero)) = s(zero) .
  eq rem2(zero) = zero .
  eq quo2(s(s(N))) = s(quo2(N)) .
  eq quo2(s(zero)) = zero .
  eq quo2(zero) = zero .
endfm

mod DAMS is
  protecting NATURAL .
  sorts Mode System .
  ops think eat : -> Mode [ctor] .
  op st : Mode Mode Natural -> System [ctor] .

  vars L1 L2 : Mode .
  vars M N : Natural .

  crl st(think, L2, N) => st(eat, L2, N) if rem2(N)= s(zero) .
  rl  st(eat, L2, N) => st(think, L2, (s(s(s(zero))) *' N) +' s(zero)) .
  crl st(L1, think, N) => st(L1, eat, N) if rem2(N) = zero .
  crl st(L1, eat, N) => st(L1, think, quo2(N)) if rem2(N) = zero .
endm