/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/4.25.trs

The program

(VAR x y z)
(RULES
rev(a) -> a
rev(b) -> b
rev(++(x,y)) -> ++(rev(y),rev(x))
rev(++(x,x)) -> rev(x)
)
(COMMENT Example 4.25 (Reverse) in \cite{SK90})