(VAR x ) (RULES f(0) -> s(0) f(s(x)) -> g(s(s(x))) g(0) -> s(0) g(s(0)) -> s(0) g(s(s(x))) -> f(x) )