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