Runtime Complexity TRS:
The TRS R consists of the following rules:

le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
log(0) → logError
log(s(x)) → loop(s(x), s(0), 0)
loop(x, s(y), z) → if(le(x, s(y)), x, s(y), z)
if(true, x, y, z) → z
if(false, x, y, z) → loop(x, double(y), s(z))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:


le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))

Types:
le' :: s':0':logError' → s':0':logError' → false':true'
s' :: s':0':logError' → s':0':logError'
0' :: s':0':logError'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError' → s':0':logError'
log' :: s':0':logError' → s':0':logError'
logError' :: s':0':logError'
loop' :: s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
if' :: false':true' → s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
_hole_false':true'1 :: false':true'
_hole_s':0':logError'2 :: s':0':logError'
_gen_s':0':logError'3 :: Nat → s':0':logError'

Heuristically decided to analyse the following defined symbols:
le', double', loop'

They will be analysed ascendingly in the following order:
le' < loop'
double' < loop'

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))

Types:
le' :: s':0':logError' → s':0':logError' → false':true'
s' :: s':0':logError' → s':0':logError'
0' :: s':0':logError'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError' → s':0':logError'
log' :: s':0':logError' → s':0':logError'
logError' :: s':0':logError'
loop' :: s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
if' :: false':true' → s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
_hole_false':true'1 :: false':true'
_hole_s':0':logError'2 :: s':0':logError'
_gen_s':0':logError'3 :: Nat → s':0':logError'

Generator Equations:
_gen_s':0':logError'3(0) ⇔ 0'
_gen_s':0':logError'3(+(x, 1)) ⇔ s'(_gen_s':0':logError'3(x))

The following defined symbols remain to be analysed:
le', double', loop'

They will be analysed ascendingly in the following order:
le' < loop'
double' < loop'

Proved the following rewrite lemma:
le'(_gen_s':0':logError'3(+(1, _n5)), _gen_s':0':logError'3(_n5)) → false', rt ∈ Ω(1 + n5)

Induction Base:
le'(_gen_s':0':logError'3(+(1, 0)), _gen_s':0':logError'3(0)) →RΩ(1)
false'

Induction Step:
le'(_gen_s':0':logError'3(+(1, +(_$n6, 1))), _gen_s':0':logError'3(+(_$n6, 1))) →RΩ(1)
le'(_gen_s':0':logError'3(+(1, _$n6)), _gen_s':0':logError'3(_$n6)) →IH
false'

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))

Types:
le' :: s':0':logError' → s':0':logError' → false':true'
s' :: s':0':logError' → s':0':logError'
0' :: s':0':logError'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError' → s':0':logError'
log' :: s':0':logError' → s':0':logError'
logError' :: s':0':logError'
loop' :: s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
if' :: false':true' → s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
_hole_false':true'1 :: false':true'
_hole_s':0':logError'2 :: s':0':logError'
_gen_s':0':logError'3 :: Nat → s':0':logError'

Lemmas:
le'(_gen_s':0':logError'3(+(1, _n5)), _gen_s':0':logError'3(_n5)) → false', rt ∈ Ω(1 + n5)

Generator Equations:
_gen_s':0':logError'3(0) ⇔ 0'
_gen_s':0':logError'3(+(x, 1)) ⇔ s'(_gen_s':0':logError'3(x))

The following defined symbols remain to be analysed:
double', loop'

They will be analysed ascendingly in the following order:
double' < loop'

Proved the following rewrite lemma:
double'(_gen_s':0':logError'3(_n623)) → _gen_s':0':logError'3(*(2, _n623)), rt ∈ Ω(1 + n623)

Induction Base:
double'(_gen_s':0':logError'3(0)) →RΩ(1)
0'

Induction Step:
double'(_gen_s':0':logError'3(+(_$n624, 1))) →RΩ(1)
s'(s'(double'(_gen_s':0':logError'3(_$n624)))) →IH
s'(s'(_gen_s':0':logError'3(*(2, _$n624))))

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))

Types:
le' :: s':0':logError' → s':0':logError' → false':true'
s' :: s':0':logError' → s':0':logError'
0' :: s':0':logError'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError' → s':0':logError'
log' :: s':0':logError' → s':0':logError'
logError' :: s':0':logError'
loop' :: s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
if' :: false':true' → s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
_hole_false':true'1 :: false':true'
_hole_s':0':logError'2 :: s':0':logError'
_gen_s':0':logError'3 :: Nat → s':0':logError'

Lemmas:
le'(_gen_s':0':logError'3(+(1, _n5)), _gen_s':0':logError'3(_n5)) → false', rt ∈ Ω(1 + n5)
double'(_gen_s':0':logError'3(_n623)) → _gen_s':0':logError'3(*(2, _n623)), rt ∈ Ω(1 + n623)

Generator Equations:
_gen_s':0':logError'3(0) ⇔ 0'
_gen_s':0':logError'3(+(x, 1)) ⇔ s'(_gen_s':0':logError'3(x))

The following defined symbols remain to be analysed:
loop'

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
log'(0') → logError'
log'(s'(x)) → loop'(s'(x), s'(0'), 0')
loop'(x, s'(y), z) → if'(le'(x, s'(y)), x, s'(y), z)
if'(true', x, y, z) → z
if'(false', x, y, z) → loop'(x, double'(y), s'(z))

Types:
le' :: s':0':logError' → s':0':logError' → false':true'
s' :: s':0':logError' → s':0':logError'
0' :: s':0':logError'
false' :: false':true'
true' :: false':true'
double' :: s':0':logError' → s':0':logError'
log' :: s':0':logError' → s':0':logError'
logError' :: s':0':logError'
loop' :: s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
if' :: false':true' → s':0':logError' → s':0':logError' → s':0':logError' → s':0':logError'
_hole_false':true'1 :: false':true'
_hole_s':0':logError'2 :: s':0':logError'
_gen_s':0':logError'3 :: Nat → s':0':logError'

Lemmas:
le'(_gen_s':0':logError'3(+(1, _n5)), _gen_s':0':logError'3(_n5)) → false', rt ∈ Ω(1 + n5)
double'(_gen_s':0':logError'3(_n623)) → _gen_s':0':logError'3(*(2, _n623)), rt ∈ Ω(1 + n623)

Generator Equations:
_gen_s':0':logError'3(0) ⇔ 0'
_gen_s':0':logError'3(+(x, 1)) ⇔ s'(_gen_s':0':logError'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
le'(_gen_s':0':logError'3(+(1, _n5)), _gen_s':0':logError'3(_n5)) → false', rt ∈ Ω(1 + n5)