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