(from AG01 3.21) (VAR x y) (RULES times(x,plus(y,1)) -> plus(times(x,plus(y,times(1,0))),x) times(x,1) -> x plus(x,0) -> x times(x,0) -> 0 )
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend