(VAR l x y )
(RULES 
        rev(nil) -> nil
        rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l))
        rev1(0, nil) -> 0
        rev1(s(x), nil) -> s(x)
        rev1(x, cons(y, l)) -> rev1(y, l)
        rev2(x, nil) -> nil
        rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l)))
        
)