(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(s(0)) -> k(0)
        k(0) -> 0
        s(s(s(0))) -> k(s(0))
        k(s(0)) -> s(0)
        s(s(s(s(s(s(s(s(s(s(0)))))))))) -> k(s(s(0)))
        k(s(s(0))) -> s(s(s(s(s(s(s(s(0))))))))
        h(k(x), g(x)) -> k(s(x))
        
)