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