(VAR x y ) (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) )