(VAR x y z)
(RULES
g(0,f(x,x)) -> x
g(x,s(y)) -> g(f(x,y),0)
g(s(x),y) -> g(f(x,y),0)
g(f(x,y),0) -> f(g(x,0),g(y,0))
)
(COMMENT Example 4.2.30 in \cite{K00})