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