(VAR x ) (RULES g(x) -> h(k(x)) g(x) -> x h(k(x)) -> f(x) f(x) -> x k(c) -> c f(c) -> g(c) h(k(x)) -> x h(c) -> f(c) h(c) -> c )