(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< nil, ++(X, X) >)
(SIGNATURES
    rev :: [A] -> A
    rev1 :: [A x A] -> A
    rev2 :: [A x A] -> A)
(RULES
    rev(nil()) -> nil()
    rev(++(x,y)) -> ++(rev1(x,y)
                      ,rev2(x,y))
    rev1(x,nil()) -> x
    rev1(x,++(y,z)) -> rev1(y,z)
    rev2(x,nil()) -> nil()
    rev2(x,++(y,z)) -> rev(++(x
                             ,rev(rev2(y,z)))))