/home/nowonder/forschung/aprove/TPDB05/TRS/Rubio/aoto.trs

The program

(VAR X)
(RULES

f(f(X)) -> f(g(f(g(f(X)))))
f(g(f(X))) -> f(g(X))


)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend