(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< 0, I(X), 1, true, false, L(X), N(X, X, X), l, r >)
(SIGNATURES
    O :: [A] -> A
    + :: [A x A] -> A
    - :: [A x A] -> A
    not :: [A] -> A
    and :: [A x A] -> A
    if :: [A x A x A] -> A
    ge :: [A x A] -> A
    Log' :: [A] -> A
    Log :: [A] -> A
    Val :: [A] -> A
    Min :: [A] -> A
    Max :: [A] -> A
    BS :: [A] -> A
    Size :: [A] -> A
    WB :: [A] -> A)
(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()))))