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