/home/nowonder/forschung/aprove/TPDB05/TRS/nontermin/HM/n001.trs

The program

(VAR x)
(RULES

h(f(f(x))) -> h(f(g(f(x))))
f(g(f(x))) -> f(f(x))

)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend