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