(VAR x xs ys)

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

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

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