(VAR x y )
(RULES 
        +(0, y) -> y
        +(s(x), y) -> s(+(x, y))
        -(0, y) -> 0
        -(x, 0) -> x
        -(s(x), s(y)) -> -(x, y)
        
)