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