MAYBE 0.08/0.18 MAYBE 0.08/0.18 0.08/0.18 Problem: 0.08/0.18 0(#()) -> #() 0.08/0.18 +(x,#()) -> x 0.08/0.18 +(#(),x) -> x 0.08/0.18 +(0(x),0(y)) -> 0(+(x,y)) 0.08/0.18 +(0(x),1(y)) -> 1(+(x,y)) 0.08/0.18 +(1(x),0(y)) -> 1(+(x,y)) 0.08/0.18 +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0.08/0.18 *(#(),x) -> #() 0.08/0.18 *(0(x),y) -> 0(*(x,y)) 0.08/0.18 *(1(x),y) -> +(0(*(x,y)),y) 0.08/0.18 sum(nil()) -> 0(#()) 0.08/0.18 sum(cons(x,l)) -> +(x,sum(l)) 0.08/0.18 prod(nil()) -> 1(#()) 0.08/0.18 prod(cons(x,l)) -> *(x,prod(l)) 0.08/0.18 0.08/0.18 Proof: 0.08/0.18 Open 0.08/0.19 EOF