(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< #, 1(X), false, true, l(X), n(X, X, X) >)
(SIGNATURES
    0 :: [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
    val :: [A] -> A
    min :: [A] -> A
    max :: [A] -> A
    bs :: [A] -> A
    size :: [A] -> A
    wb :: [A] -> A)
(RULES
    0(#()) -> #()
    +(x,#()) -> x
    +(#(),x) -> x
    +(0(x),0(y)) -> 0(+(x,y))
    +(0(x),1(y)) -> 1(+(x,y))
    +(1(x),0(y)) -> 1(+(x,y))
    +(1(x),1(y)) -> 0(+(+(x,y)
                       ,1(#())))
    +(x,+(y,z)) -> +(+(x,y),z)
    -(x,#()) -> x
    -(#(),x) -> #()
    -(0(x),0(y)) -> 0(-(x,y))
    -(0(x),1(y)) -> 1(-(-(x,y)
                       ,1(#())))
    -(1(x),0(y)) -> 1(-(x,y))
    -(1(x),1(y)) -> 0(-(x,y))
    not(false()) -> true()
    not(true()) -> false()
    and(x,true()) -> x
    and(x,false()) -> false()
    if(true(),x,y) -> x
    if(false(),x,y) -> y
    ge(0(x),0(y)) -> ge(x,y)
    ge(0(x),1(y)) -> not(ge(y,x))
    ge(1(x),0(y)) -> ge(x,y)
    ge(1(x),1(y)) -> ge(x,y)
    ge(x,#()) -> true()
    ge(#(),1(x)) -> false()
    ge(#(),0(x)) -> ge(#(),x)
    val(l(x)) -> x
    val(n(x,y,z)) -> x
    min(l(x)) -> x
    min(n(x,y,z)) -> min(y)
    max(l(x)) -> x
    max(n(x,y,z)) -> max(z)
    bs(l(x)) -> true()
    bs(n(x,y,z)) -> and(and(ge(x
                              ,max(y))
                           ,ge(min(z),x))
                       ,and(bs(y),bs(z)))
    size(l(x)) -> 1(#())
    size(n(x,y,z)) -> +(+(size(x)
                         ,size(y))
                       ,1(#()))
    wb(l(x)) -> true()
    wb(n(x,y,z)) ->
      and(if(ge(size(y),size(z))
            ,ge(1(#()),-(size(y),size(z)))
            ,ge(1(#()),-(size(z),size(y))))
         ,and(wb(y),wb(z))))