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