MAYBE
0.18/0.21	MAYBE
0.18/0.21	
0.18/0.21	Problem:
0.18/0.21	 O(0()) -> 0()
0.18/0.21	 +(0(),x) -> x
0.18/0.21	 +(x,0()) -> x
0.18/0.21	 +(O(x),O(y)) -> O(+(x,y))
0.18/0.21	 +(O(x),I(y)) -> I(+(x,y))
0.18/0.21	 +(I(x),O(y)) -> I(+(x,y))
0.18/0.21	 +(I(x),I(y)) -> O(+(+(x,y),I(0())))
0.18/0.21	 +(x,+(y,z)) -> +(+(x,y),z)
0.18/0.21	 -(x,0()) -> x
0.18/0.21	 -(0(),x) -> 0()
0.18/0.21	 -(O(x),O(y)) -> O(-(x,y))
0.18/0.21	 -(O(x),I(y)) -> I(-(-(x,y),I(1())))
0.18/0.21	 -(I(x),O(y)) -> I(-(x,y))
0.18/0.21	 -(I(x),I(y)) -> O(-(x,y))
0.18/0.21	 not(true()) -> false()
0.18/0.21	 not(false()) -> true()
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(O(x),O(y)) -> ge(x,y)
0.18/0.21	 ge(O(x),I(y)) -> not(ge(y,x))
0.18/0.21	 ge(I(x),O(y)) -> ge(x,y)
0.18/0.21	 ge(I(x),I(y)) -> ge(x,y)
0.18/0.21	 ge(x,0()) -> true()
0.18/0.21	 ge(0(),O(x)) -> ge(0(),x)
0.18/0.21	 ge(0(),I(x)) -> false()
0.18/0.21	 Log'(0()) -> 0()
0.18/0.21	 Log'(I(x)) -> +(Log'(x),I(0()))
0.18/0.21	 Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),0())
0.18/0.21	 Log(x) -> -(Log'(x),I(0()))
0.18/0.21	 Val(L(x)) -> x
0.18/0.21	 Val(N(x,l(),r())) -> x
0.18/0.21	 Min(L(x)) -> x
0.18/0.21	 Min(N(x,l(),r())) -> Min(l())
0.18/0.21	 Max(L(x)) -> x
0.18/0.21	 Max(N(x,l(),r())) -> Max(r())
0.18/0.21	 BS(L(x)) -> true()
0.18/0.21	 BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
0.18/0.21	 Size(L(x)) -> I(0())
0.18/0.21	 Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(1()))
0.18/0.21	 WB(L(x)) -> true()
0.18/0.21	 WB(N(x,l(),r())) ->
0.18/0.21	 and(if(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))),ge(I(0()),-(Size(r()),Size(l())))),
0.18/0.21	     and(WB(l()),WB(r())))
0.18/0.21	
0.18/0.21	Proof:
0.18/0.21	 Open
0.18/0.21	EOF