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

The program

(VAR x)
(RULES
 f(g(x)) -> g(g(f(x)))
 f(g(x)) -> g(g(g(x)))
)

(COMMENT Example 6 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend