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