(VAR x y )
(RULES 
        rev(a) -> a
        rev(b) -> b
        rev(++(x, y)) -> ++(rev(y), rev(x))
        rev(++(x, x)) -> rev(x)
        
)