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