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