(VAR x y z)
(RULES
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)))
)
(COMMENT Example in \cite[Section~6.1]{U03})