(VAR x y z)
(RULES
+(0,y) -> y
+(s(x),0) -> s(x)
+(s(x),s(y)) -> s(+(s(x),+(y,0)))
)
(COMMENT Example 4.12 (Addition) in \cite{SK90})