(COMMENT from Gluck and Kawabe's paper)
(COMMENT
The function double duplicates each element in the given list. It
makes use of the primitive operator du for the duplication. For
example, double([A,B,C]) = [A,A,B,B,C,C].
)
(COMMENT
fun double [] = []
| double (x::xs) = x :: x :: double xs;
)
(VAR x y xs x1 x2)
(RULES
double(nil) -> nil
double(cons(x,xs)) -> cons(x,cons(x,double(xs)))
)