(COMMENT Evelyne Contejean, Claude Marché, Landy Rabehasaina, RTA'97 Rewrite system for addition and multiplication of integers, in ternary representation * distributes over + (currently fails with CiME) ) (VAR z y x) (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)) *(+(x,y),z) -> +(*(x,z),*(y,z)) *(x,+(y,z)) -> +(*(x,y),*(x,z)) )