(VAR x y)
(THEORY (AC plus) (AC mult))
(RULES
zero(sharp) -> sharp
plus(x, sharp) -> x
plus(zero(x), zero(y)) -> zero(plus(x,y))
plus(zero(x), one(y)) -> one(plus(x,y))
plus(one(x), one(y)) -> j(plus(x,plus(y, one(sharp))))
plus(zero(x), j(y)) -> j(plus(x,y))
plus(j(x), one(y)) -> zero(plus(x,y))
plus(j(x), j(y)) -> one(plus(x,plus(y, j(sharp))))
minus(x,y) -> plus(x, opp(y))
opp(sharp) -> sharp
opp(zero(x)) -> zero(opp(x))
opp(one(x)) -> j(opp(x))
opp(j(x)) -> one(opp(x))
mult(x, sharp) -> sharp
mult(zero(x), y) -> zero(mult(x, y))
mult(one(x), y) -> plus(zero(mult(x, y)), y)
)