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