(VAR x y)

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

(SIGNATURES
  f :: Nat -> Nat
  g :: Nat x Nat -> Nat
  k :: Nat -> Nat
)


(RULES
   f(s(x)) -> g(x,f(x))
   g(x,y) -> x
   g(x,y) -> y
   k(s(x)) -> f(k(x))
)