/home/nowonder/forschung/aprove/TPDB05/TRS/D33/27.trs

The program

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

(COMMENT Example 27 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend