(VAR X) (RULES f(g(X)) -> g(f(f(X))) f(h(X)) -> h(g(X)) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend