(from AG01 3.24)
(VAR x)
(RULES
f(0) -> s(0)
f(s(0)) -> s(0)
f(s(s(x))) -> f(f(s(x))))