fmod FIB is
  protecting NAT .

  op a : -> Nat [ctor].

  var M : Nat .
  
  op fib : Nat -> Nat .
  eq fib(0) = 0 .
  eq fib(s 0) = s 0 .
  eq fib(s s M) = fib(M) + fib(s M) .
  
  op fibm : Nat -> Nat [memo].
  eq fibm(0) = 0 .
  eq fibm(s 0) = s 0 .
  eq fibm(s s M) = fibm(M) + fibm(s M) .
endfm