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