(VAR x y ) (RULES +(x,0) -> x +(x,s(y)) -> s(+(x,y)) *(x,0) -> 0 *(x,s(y)) -> +(*(x,y),x) +(x,y) -> +(y,x) +(0,x) -> x +(s(y),x) -> s(+(x,y)) )