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