(VAR x y z )
(RULES 
        0(#) -> #
        +(#, x) -> x
        +(x, #) -> x
        +(0(x), 0(y)) -> 0(+(x, y))
        +(0(x), 1(y)) -> 1(+(x, y))
        +(1(x), 0(y)) -> 1(+(x, y))
        +(0(x), j(y)) -> j(+(x, y))
        +(j(x), 0(y)) -> j(+(x, y))
        +(1(x), 1(y)) -> j(+(+(x, y), 1(#)))
        +(j(x), j(y)) -> 1(+(+(x, y), j(#)))
        +(1(x), j(y)) -> 0(+(x, y))
        +(j(x), 1(y)) -> 0(+(x, y))
        +(+(x, y), z) -> +(x, +(y, z))
        opp(#) -> #
        opp(0(x)) -> 0(opp(x))
        opp(1(x)) -> j(opp(x))
        opp(j(x)) -> 1(opp(x))
        -(x, y) -> +(x, opp(y))
        *(#, x) -> #
        *(0(x), y) -> 0(*(x, y))
        *(1(x), y) -> +(0(*(x, y)), y)
        *(j(x), y) -> -(0(*(x, y)), y)
        *(*(x, y), z) -> *(x, *(y, z))
        
)