(VAR X Y )
(RULES 
        +(X, 0) -> X
        +(X, s(Y)) -> s(+(X, Y))
        f(0, s(0), X) -> f(X, +(X, X), X)
        g(X, Y) -> X
        g(X, Y) -> Y
        
)