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