MAYBE 0.08/0.19 MAYBE 0.08/0.19 0.08/0.19 Problem: 0.08/0.19 0(#()) -> #() 0.08/0.19 +(#(),x) -> x 0.08/0.19 +(x,#()) -> x 0.08/0.19 +(0(x),0(y)) -> 0(+(x,y)) 0.08/0.19 +(0(x),1(y)) -> 1(+(x,y)) 0.08/0.19 +(1(x),0(y)) -> 1(+(x,y)) 0.08/0.19 +(0(x),j(y)) -> j(+(x,y)) 0.08/0.19 +(j(x),0(y)) -> j(+(x,y)) 0.08/0.19 +(1(x),1(y)) -> j(+(+(x,y),1(#()))) 0.08/0.19 +(j(x),j(y)) -> 1(+(+(x,y),j(#()))) 0.08/0.19 +(1(x),j(y)) -> 0(+(x,y)) 0.08/0.19 +(j(x),1(y)) -> 0(+(x,y)) 0.08/0.19 +(+(x,y),z) -> +(x,+(y,z)) 0.08/0.19 opp(#()) -> #() 0.08/0.19 opp(0(x)) -> 0(opp(x)) 0.08/0.19 opp(1(x)) -> j(opp(x)) 0.08/0.19 opp(j(x)) -> 1(opp(x)) 0.08/0.19 -(x,y) -> +(x,opp(y)) 0.08/0.19 *(#(),x) -> #() 0.08/0.19 *(0(x),y) -> 0(*(x,y)) 0.08/0.19 *(1(x),y) -> +(0(*(x,y)),y) 0.08/0.19 *(j(x),y) -> -(0(*(x,y)),y) 0.08/0.19 *(*(x,y),z) -> *(x,*(y,z)) 0.08/0.19 0.08/0.19 Proof: 0.08/0.19 Open 0.08/0.19 EOF