(VAR x xs l2)


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

(SIGNATURES
  f :: L -> L
  g :: L x L -> L
  h :: L -> L
)

(RULES
  f(cons(x,xs)) -> g(xs,f(xs))
  f(nil) -> nil

  g(nil,l2) -> l2
  g(cons(x,xs),l2) -> cons(x,xs)

  h(nil) -> nil
  h(cons(x,xs)) -> cons(x,f(xs))
)