(VAR a b c k l x )

(DATATYPES a = µX. < empty, cons(X,X) >
 )

(SIGNATURES
   f :: a x a -> a
   g :: a x a x a -> a
 )


(RULES
   f(empty,l) -> l
   f(cons(x,k),l) -> g(k,l,cons(x,k))
   g(a,b,c) -> f(a,cons(b,c))
)