(VAR x xs ys)

(DATATYPES
   a = < >
   b = µX. < nil, dd(a,X) >
 )

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

(RULES
  @(nil, xs)         -> xs
  @(dd(x, xs), ys) -> dd(x, @(xs, ys))
  rev(nil) -> nil
  rev(dd(x, xs)) -> @(rev(xs),dd(x, nil))
)