(VAR x y)
(RULES
f(0) -> 1
f(s(x)) -> g(x,s(x))
g(0,y) -> y
g(s(x),y) -> g(x,+(y,s(x)))
+(x,0) -> x
+(x,s(y)) -> s(+(x,y))
g(s(x),y) -> g(x,s(+(y,x)))
)
(COMMENT Example 2.16 in \cite{SK90})