(VAR x y z )
(RULES 
        i(0) -> 0
        +(0, y) -> y
        +(x, 0) -> x
        i(i(x)) -> x
        +(i(x), x) -> 0
        +(x, i(x)) -> 0
        i(+(x, y)) -> +(i(x), i(y))
        +(x, +(y, z)) -> +(+(x, y), z)
        +(+(x, i(y)), y) -> x
        +(+(x, y), i(y)) -> x
        
)