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