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 +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0.08/0.19 +(+(x,y),z) -> +(x,+(y,z)) 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 *(*(x,y),z) -> *(x,*(y,z)) 0.08/0.19 *(x,+(y,z)) -> +(*(x,y),*(x,z)) 0.08/0.19 app(nil(),l) -> l 0.08/0.19 app(cons(x,l1),l2) -> cons(x,app(l1,l2)) 0.08/0.19 sum(nil()) -> 0(#()) 0.08/0.19 sum(cons(x,l)) -> +(x,sum(l)) 0.08/0.19 sum(app(l1,l2)) -> +(sum(l1),sum(l2)) 0.08/0.19 prod(nil()) -> 1(#()) 0.08/0.19 prod(cons(x,l)) -> *(x,prod(l)) 0.08/0.19 prod(app(l1,l2)) -> *(prod(l1),prod(l2)) 0.08/0.19 0.08/0.19 Proof: 0.08/0.19 Open 0.08/0.19 EOF