MAYBE

Problem:
 O(0()) -> 0()
 +(0(),x) -> x
 +(x,0()) -> x
 +(O(x),O(y)) -> O(+(x,y))
 +(O(x),I(y)) -> I(+(x,y))
 +(I(x),O(y)) -> I(+(x,y))
 +(I(x),I(y)) -> O(+(+(x,y),I(0())))
 +(x,+(y,z)) -> +(+(x,y),z)
 -(x,0()) -> x
 -(0(),x) -> 0()
 -(O(x),O(y)) -> O(-(x,y))
 -(O(x),I(y)) -> I(-(-(x,y),I(1())))
 -(I(x),O(y)) -> I(-(x,y))
 -(I(x),I(y)) -> O(-(x,y))
 not(true()) -> false()
 not(false()) -> true()
 and(x,true()) -> x
 and(x,false()) -> false()
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 ge(O(x),O(y)) -> ge(x,y)
 ge(O(x),I(y)) -> not(ge(y,x))
 ge(I(x),O(y)) -> ge(x,y)
 ge(I(x),I(y)) -> ge(x,y)
 ge(x,0()) -> true()
 ge(0(),O(x)) -> ge(0(),x)
 ge(0(),I(x)) -> false()
 Log'(0()) -> 0()
 Log'(I(x)) -> +(Log'(x),I(0()))
 Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),0())
 Log(x) -> -(Log'(x),I(0()))
 Val(L(x)) -> x
 Val(N(x,l(),r())) -> x
 Min(L(x)) -> x
 Min(N(x,l(),r())) -> Min(l())
 Max(L(x)) -> x
 Max(N(x,l(),r())) -> Max(r())
 BS(L(x)) -> true()
 BS(N(x,l(),r())) -> and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r())))
 Size(L(x)) -> I(0())
 Size(N(x,l(),r())) -> +(+(Size(l()),Size(r())),I(1()))
 WB(L(x)) -> true()
 WB(N(x,l(),r())) ->
 and(if(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))),ge(I(0()),-(Size(r()),Size(l())))),
     and(WB(l()),WB(r())))

Proof:
 Open