/home/nowonder/forschung/aprove/TPDB05/TRS/various/11.trs

The program

(VAR x y z)
(RULES
f(0,1,x) -> f(h(x),h(x),x)
h(0) -> 0
h(g(x,y)) -> y
)
(COMMENT Example 4.5 (TRS $\RR_2$) in \cite{O02})