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