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