(GOAL COMPLEXITY) (STARTTERM CONSTRUCTORBASED) (VAR x y z ) (STRATEGY INNERMOST) (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))) )