(VAR a k ls x)

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

(SIGNATURES
   rev :: b -> b
   r1 :: b x b -> b
 )


(RULES
   rev(ls) -> r1(ls,empty)
   r1(empty,a) -> a
   r1(cons(x,k),a) -> r1(k,cons(x,a))
)