(VAR x y z)
(RULES
O(0) -> 0

+(0,x) -> x
+(x,0) -> x
+(O(x),O(y)) -> O(+(x,y))
+(O(x),I(y)) -> I(+(x,y))
+(I(x),O(y)) -> I(+(x,y))
+(I(x),I(y)) -> O(+(+(x,y),I(0)))

*(0,x) -> 0
*(x,0) -> 0
*(O(x),y) -> O(*(x,y))
*(I(x),y) -> +(O(*(x,y)),y)

-(x,0) -> x
-(0,x) -> 0
-(O(x),O(y)) -> O(-(x,y))
-(O(x),I(y)) -> I(-(-(x,y),I(1)))
-(I(x),O(y)) -> I(-(x,y))
-(I(x),I(y)) -> O(-(x,y))
)
(COMMENT Example 3 from \cite{U03})