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