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