Runtime Complexity TRS:
The TRS R consists of the following 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(true) → false
not(false) → true
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(#, 0(x)) → ge(#, x)
ge(#, 1(x)) → false
log(x) → -(log'(x), 1(#))
log'(#) → #
log'(1(x)) → +(log'(x), 1(#))
log'(0(x)) → if(ge(x, 1(#)), +(log'(x), 1(#)), #)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following 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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')

Rewrite Strategy: INNERMOST

Infered types.

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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')

Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'

Heuristically decided to analyse the following defined symbols:
+', -', ge', log'''

They will be analysed ascendingly in the following order:
+' < log'''
ge' < log'''

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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')

Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'

Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))

The following defined symbols remain to be analysed:
+', -', ge', log'''

They will be analysed ascendingly in the following order:
+' < log'''
ge' < log'''

Proved the following rewrite lemma:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)

Induction Base:
+'(_gen_#':1'3(0), _gen_#':1'3(0))

Induction Step:
+'(_gen_#':1'3(+(_\$n6, 1)), _gen_#':1'3(+(_\$n6, 1))) →RΩ(1)
0'(+'(+'(_gen_#':1'3(_\$n6), _gen_#':1'3(_\$n6)), 1'(#'))) →IH
0'(+'(_*4, 1'(#')))

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

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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')

Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'

Lemmas:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)

Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))

The following defined symbols remain to be analysed:
-', ge', log'''

They will be analysed ascendingly in the following order:
ge' < log'''

Proved the following rewrite lemma:
-'(_gen_#':1'3(_n41737), _gen_#':1'3(_n41737)) → _gen_#':1'3(0), rt ∈ Ω(1 + n41737)

Induction Base:
-'(_gen_#':1'3(0), _gen_#':1'3(0)) →RΩ(1)
#'

Induction Step:
-'(_gen_#':1'3(+(_\$n41738, 1)), _gen_#':1'3(+(_\$n41738, 1))) →RΩ(1)
0'(-'(_gen_#':1'3(_\$n41738), _gen_#':1'3(_\$n41738))) →IH
0'(_gen_#':1'3(0)) →RΩ(1)
#'

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

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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')

Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'

Lemmas:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1'3(_n41737), _gen_#':1'3(_n41737)) → _gen_#':1'3(0), rt ∈ Ω(1 + n41737)

Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))

The following defined symbols remain to be analysed:
ge', log'''

They will be analysed ascendingly in the following order:
ge' < log'''

Proved the following rewrite lemma:
ge'(_gen_#':1'3(_n44649), _gen_#':1'3(_n44649)) → true', rt ∈ Ω(1 + n44649)

Induction Base:
ge'(_gen_#':1'3(0), _gen_#':1'3(0)) →RΩ(1)
true'

Induction Step:
ge'(_gen_#':1'3(+(_\$n44650, 1)), _gen_#':1'3(+(_\$n44650, 1))) →RΩ(1)
ge'(_gen_#':1'3(_\$n44650), _gen_#':1'3(_\$n44650)) →IH
true'

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

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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')

Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'

Lemmas:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1'3(_n41737), _gen_#':1'3(_n41737)) → _gen_#':1'3(0), rt ∈ Ω(1 + n41737)
ge'(_gen_#':1'3(_n44649), _gen_#':1'3(_n44649)) → true', rt ∈ Ω(1 + n44649)

Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))

The following defined symbols remain to be analysed:
log'''

Proved the following rewrite lemma:
log'''(_gen_#':1'3(+(1, _n47789))) → _*4, rt ∈ Ω(n47789)

Induction Base:
log'''(_gen_#':1'3(+(1, 0)))

Induction Step:
log'''(_gen_#':1'3(+(1, +(_\$n47790, 1)))) →RΩ(1)
+'(log'''(_gen_#':1'3(+(1, _\$n47790))), 1'(#')) →IH
+'(_*4, 1'(#'))

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

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'(true') → false'
not'(false') → true'
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'(#', 0'(x)) → ge'(#', x)
ge'(#', 1'(x)) → false'
log''(x) → -'(log'''(x), 1'(#'))
log'''(#') → #'
log'''(1'(x)) → +'(log'''(x), 1'(#'))
log'''(0'(x)) → if'(ge'(x, 1'(#')), +'(log'''(x), 1'(#')), #')

Types:
0' :: #':1' → #':1'
#' :: #':1'
+' :: #':1' → #':1' → #':1'
1' :: #':1' → #':1'
-' :: #':1' → #':1' → #':1'
not' :: true':false' → true':false'
true' :: true':false'
false' :: true':false'
if' :: true':false' → #':1' → #':1' → #':1'
ge' :: #':1' → #':1' → true':false'
log'' :: #':1' → #':1'
log''' :: #':1' → #':1'
_hole_#':1'1 :: #':1'
_hole_true':false'2 :: true':false'
_gen_#':1'3 :: Nat → #':1'

Lemmas:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)
-'(_gen_#':1'3(_n41737), _gen_#':1'3(_n41737)) → _gen_#':1'3(0), rt ∈ Ω(1 + n41737)
ge'(_gen_#':1'3(_n44649), _gen_#':1'3(_n44649)) → true', rt ∈ Ω(1 + n44649)
log'''(_gen_#':1'3(+(1, _n47789))) → _*4, rt ∈ Ω(n47789)

Generator Equations:
_gen_#':1'3(0) ⇔ #'
_gen_#':1'3(+(x, 1)) ⇔ 1'(_gen_#':1'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
+'(_gen_#':1'3(_n5), _gen_#':1'3(_n5)) → _*4, rt ∈ Ω(n5)