(from AG01 3.27) (VAR x) (RULES f(f(x)) -> g(f(x)) g(g(x)) -> f(x) )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend