(from AG01 3.25) (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