(VAR X Y) (RULES *(X,+(Y,1)) -> +(*(X,+(Y,*(1,0))),X) *(X,1) -> X *(X,0) -> X *(X,0) -> 0 )