/home/nowonder/forschung/aprove/TPDB05/TRS/AG01/#3.33.trs

The program

(from AG01 3.33)
(VAR x)
(RULES
p(f(f(x))) -> q(f(g(x)))
p(g(g(x))) -> q(g(f(x)))
q(f(f(x))) -> p(f(g(x)))
q(g(g(x))) -> p(g(f(x)))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend