(VAR x y z) (RULES minus(0) -> 0 +(x,0) -> x +(0,y) -> y +(minus(1),1) -> 0 minus(minus(x)) -> x +(x,minus(y)) -> minus(+(minus(x),y)) +(x,+(y,z)) -> +(+(x,y),z) +(minus(+(x,1)),1) -> minus(x) ) (COMMENT Example 2.10 (Unary Integer Addition) in \cite{SK90})