/home/nowonder/forschung/aprove/TPDB05/TRS/HM/t011.trs

The program

(VAR x y)
(RULES
g(f(x),y) -> f(h(x,y))
h(x,y) -> g(x, f(y))
)

(COMMENT
Example 6 in \cite{G96}.
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend