(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