(VAR x)

(DATATYPES
  Nat = µX.< 0, s(X) >
)

(SIGNATURES
  d :: Nat -> Nat
  exp :: Nat -> Nat
)


(RULES
  d(0) -> 0
  d(s(x)) -> s(s(d(x)))
  exp(0) -> s(0)
  exp(s(x)) -> d(exp(x))
)