Runtime Complexity TRS:
The TRS R consists of the following 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)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following 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')
Log1(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')))

Rewrite Strategy: INNERMOST

Infered types.

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')
Log1(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')))

Types:
O' :: 0':I':1':true':false' → 0':I':1':true':false'
0' :: 0':I':1':true':false'
+' :: 0':I':1':true':false' → 0':I':1':true':false' → 0':I':1':true':false'
I' :: 0':I':1':true':false' → 0':I':1':true':false'
-' :: 0':I':1':true':false' → 0':I':1':true':false' → 0':I':1':true':false'
1' :: 0':I':1':true':false'
not' :: 0':I':1':true':false' → 0':I':1':true':false'
true' :: 0':I':1':true':false'
false' :: 0':I':1':true':false'
and' :: 0':I':1':true':false' → 0':I':1':true':false' → 0':I':1':true':false'
if' :: 0':I':1':true':false' → 0':I':1':true':false' → 0':I':1':true':false' → 0':I':1':true':false'
ge' :: 0':I':1':true':false' → 0':I':1':true':false' → 0':I':1':true':false'
Log'' :: 0':I':1':true':false' → 0':I':1':true':false'
Log1 :: 0':I':1':true':false' → 0':I':1':true':false'
Val' :: L':l':r':N' → 0':I':1':true':false'
L' :: 0':I':1':true':false' → L':l':r':N'
N' :: 0':I':1':true':false' → L':l':r':N' → L':l':r':N' → L':l':r':N'
l' :: L':l':r':N'
r' :: L':l':r':N'
Min' :: L':l':r':N' → 0':I':1':true':false'
Max' :: L':l':r':N' → 0':I':1':true':false'
BS' :: L':l':r':N' → 0':I':1':true':false'
Size' :: L':l':r':N' → 0':I':1':true':false'
WB' :: L':l':r':N' → 0':I':1':true':false'
_hole_0':I':1':true':false'1 :: 0':I':1':true':false'
_hole_L':l':r':N'2 :: L':l':r':N'
_gen_0':I':1':true':false'3 :: Nat → 0':I':1':true':false'
_gen_L':l':r':N'4 :: Nat → L':l':r':N'

Heuristically decided to analyse the following defined symbols:
+', -', ge', Log'', Min', Max', BS', Size', WB'

They will be analysed ascendingly in the following order:
+' < Log''
+' < Size'
-' < WB'
ge' < Log''
ge' < BS'
ge' < WB'
Min' < BS'
Max' < BS'
Size' < WB'

Generator Equations:
_gen_0':I':1':true':false'3(0) ⇔ 0'
_gen_0':I':1':true':false'3(+(x, 1)) ⇔ I'(_gen_0':I':1':true':false'3(x))
_gen_L':l':r':N'4(0) ⇔ L'(0')
_gen_L':l':r':N'4(+(x, 1)) ⇔ N'(0', L'(0'), _gen_L':l':r':N'4(x))

The following defined symbols remain to be analysed:
+', -', ge', Log'', Min', Max', BS', Size', WB'

They will be analysed ascendingly in the following order:
+' < Log''
+' < Size'
-' < WB'
ge' < Log''
ge' < BS'
ge' < WB'
Min' < BS'
Max' < BS'
Size' < WB'

Proved the following rewrite lemma:
+'(_gen_0':I':1':true':false'3(+(1, _n6)), _gen_0':I':1':true':false'3(+(1, _n6))) → _*5, rt ∈ Ω(_n6)

Induction Base:
+'(_gen_0':I':1':true':false'3(+(1, 0)), _gen_0':I':1':true':false'3(+(1, 0)))

Induction Step:
+'(_gen_0':I':1':true':false'3(+(1, +(_$n7, 1))), _gen_0':I':1':true':false'3(+(1, +(_$n7, 1)))) →_R^Ω(1)
O'(+'(+'(_gen_0':I':1':true':false'3(+(1, _$n7)), _gen_0':I':1':true':false'3(+(1, _$n7))), I'(0'))) →_IH
O'(+'(_*5, I'(0')))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
+'(_gen_0':I':1':true':false'3(+(1, _n6)), _gen_0':I':1':true':false'3(+(1, _n6))) → _*5, rt ∈ Ω(_n6)

The following defined symbols remain to be analysed:
-', ge', Log'', Min', Max', BS', Size', WB'

They will be analysed ascendingly in the following order:
-' < WB'
ge' < Log''
ge' < BS'
ge' < WB'
Min' < BS'
Max' < BS'
Size' < WB'

Proved the following rewrite lemma:
-'(_gen_0':I':1':true':false'3(_n579089), _gen_0':I':1':true':false'3(_n579089)) → _gen_0':I':1':true':false'3(0), rt ∈ Ω(1 + _n579089)

Induction Base:
-'(_gen_0':I':1':true':false'3(0), _gen_0':I':1':true':false'3(0)) →_R^Ω(1)
_gen_0':I':1':true':false'3(0)

Induction Step:
-'(_gen_0':I':1':true':false'3(+(_$n579090, 1)), _gen_0':I':1':true':false'3(+(_$n579090, 1))) →_R^Ω(1)
O'(-'(_gen_0':I':1':true':false'3(_$n579090), _gen_0':I':1':true':false'3(_$n579090))) →_IH
O'(_gen_0':I':1':true':false'3(0)) →_R^Ω(1)
0'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
ge', Log'', Min', Max', BS', Size', WB'

They will be analysed ascendingly in the following order:
ge' < Log''
ge' < BS'
ge' < WB'
Min' < BS'
Max' < BS'
Size' < WB'

Proved the following rewrite lemma:
ge'(_gen_0':I':1':true':false'3(_n582704), _gen_0':I':1':true':false'3(_n582704)) → true', rt ∈ Ω(1 + _n582704)

Induction Base:
ge'(_gen_0':I':1':true':false'3(0), _gen_0':I':1':true':false'3(0)) →_R^Ω(1)
true'

Induction Step:
ge'(_gen_0':I':1':true':false'3(+(_$n582705, 1)), _gen_0':I':1':true':false'3(+(_$n582705, 1))) →_R^Ω(1)
ge'(_gen_0':I':1':true':false'3(_$n582705), _gen_0':I':1':true':false'3(_$n582705)) →_IH
true'

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
+'(_gen_0':I':1':true':false'3(+(1, _n6)), _gen_0':I':1':true':false'3(+(1, _n6))) → _*5, rt ∈ Ω(_n6)
-'(_gen_0':I':1':true':false'3(_n579089), _gen_0':I':1':true':false'3(_n579089)) → _gen_0':I':1':true':false'3(0), rt ∈ Ω(1 + _n579089)
ge'(_gen_0':I':1':true':false'3(_n582704), _gen_0':I':1':true':false'3(_n582704)) → true', rt ∈ Ω(1 + _n582704)

The following defined symbols remain to be analysed:
Log'', Min', Max', BS', Size', WB'

They will be analysed ascendingly in the following order:
Min' < BS'
Max' < BS'
Size' < WB'

Proved the following rewrite lemma:
Log''(_gen_0':I':1':true':false'3(+(1, _n586364))) → _*5, rt ∈ Ω(_n586364)

Induction Base:
Log''(_gen_0':I':1':true':false'3(+(1, 0)))

Induction Step:
Log''(_gen_0':I':1':true':false'3(+(1, +(_$n586365, 1)))) →_R^Ω(1)
+'(Log''(_gen_0':I':1':true':false'3(+(1, _$n586365))), I'(0')) →_IH
+'(_*5, I'(0'))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

The following defined symbols remain to be analysed:
Min', Max', BS', Size', WB'

They will be analysed ascendingly in the following order:
Min' < BS'
Max' < BS'
Size' < WB'

Could not prove a rewrite lemma for the defined symbol Min'.

The following defined symbols remain to be analysed:
Max', BS', Size', WB'

They will be analysed ascendingly in the following order:
Max' < BS'
Size' < WB'

Could not prove a rewrite lemma for the defined symbol Max'.

The following defined symbols remain to be analysed:
BS', Size', WB'

They will be analysed ascendingly in the following order:
Size' < WB'

Could not prove a rewrite lemma for the defined symbol BS'.

The following defined symbols remain to be analysed:
Size', WB'

They will be analysed ascendingly in the following order:
Size' < WB'

Could not prove a rewrite lemma for the defined symbol Size'.

The following defined symbols remain to be analysed:
WB'

Could not prove a rewrite lemma for the defined symbol WB'.

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
+'(_gen_0':I':1':true':false'3(+(1, _n6)), _gen_0':I':1':true':false'3(+(1, _n6))) → _*5, rt ∈ Ω(_n6)