(STRATEGY
    INNERMOST)

(VAR
    L X Y)
(DATATYPES
    A = µX.< 0, nil, s(X), cons(X, X) >)
(SIGNATURES
    rev1 :: [A x A] -> A
    rev :: [A] -> A
    rev2 :: [A x A] -> A)
(RULES
    rev1(0(),nil()) -> 0()
    rev1(s(X),nil()) -> s(X)
    rev1(X,cons(Y,L)) -> rev1(Y,L)
    rev(nil()) -> nil()
    rev(cons(X,L)) -> cons(rev1(X,L)
                          ,rev2(X,L))
    rev2(X,nil()) -> nil()
    rev2(X,cons(Y,L)) -> rev(cons(X
                                 ,rev(rev2(Y,L)))))