MAYBE 0.18/0.21 MAYBE 0.18/0.21 0.18/0.21 Problem: 0.18/0.21 0(#()) -> #() 0.18/0.21 +(x,#()) -> x 0.18/0.21 +(#(),x) -> x 0.18/0.21 +(0(x),0(y)) -> 0(+(x,y)) 0.18/0.21 +(0(x),1(y)) -> 1(+(x,y)) 0.18/0.21 +(1(x),0(y)) -> 1(+(x,y)) 0.18/0.21 +(1(x),1(y)) -> 0(+(+(x,y),1(#()))) 0.18/0.21 +(x,+(y,z)) -> +(+(x,y),z) 0.18/0.21 -(x,#()) -> x 0.18/0.21 -(#(),x) -> #() 0.18/0.21 -(0(x),0(y)) -> 0(-(x,y)) 0.18/0.21 -(0(x),1(y)) -> 1(-(-(x,y),1(#()))) 0.18/0.21 -(1(x),0(y)) -> 1(-(x,y)) 0.18/0.21 -(1(x),1(y)) -> 0(-(x,y)) 0.18/0.21 not(false()) -> true() 0.18/0.21 not(true()) -> false() 0.18/0.21 and(x,true()) -> x 0.18/0.21 and(x,false()) -> false() 0.18/0.21 if(true(),x,y) -> x 0.18/0.21 if(false(),x,y) -> y 0.18/0.21 ge(0(x),0(y)) -> ge(x,y) 0.18/0.21 ge(0(x),1(y)) -> not(ge(y,x)) 0.18/0.21 ge(1(x),0(y)) -> ge(x,y) 0.18/0.21 ge(1(x),1(y)) -> ge(x,y) 0.18/0.21 ge(x,#()) -> true() 0.18/0.21 ge(#(),1(x)) -> false() 0.18/0.21 ge(#(),0(x)) -> ge(#(),x) 0.18/0.21 val(l(x)) -> x 0.18/0.21 val(n(x,y,z)) -> x 0.18/0.21 min(l(x)) -> x 0.18/0.21 min(n(x,y,z)) -> min(y) 0.18/0.21 max(l(x)) -> x 0.18/0.21 max(n(x,y,z)) -> max(z) 0.18/0.21 bs(l(x)) -> true() 0.18/0.21 bs(n(x,y,z)) -> and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) 0.18/0.21 size(l(x)) -> 1(#()) 0.18/0.21 size(n(x,y,z)) -> +(+(size(x),size(y)),1(#())) 0.18/0.21 wb(l(x)) -> true() 0.18/0.21 wb(n(x,y,z)) -> 0.18/0.21 and(if(ge(size(y),size(z)),ge(1(#()),-(size(y),size(z))),ge(1(#()),-(size(z),size(y)))), 0.18/0.21 and(wb(y),wb(z))) 0.18/0.21 0.18/0.21 Proof: 0.18/0.21 Open 0.18/0.21 EOF