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)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
log(x, 0) → baseError
log(x, s(0)) → baseError
log(0, s(s(b))) → logZeroError
log(s(x), s(s(b))) → loop(s(x), s(s(b)), s(0), 0)
loop(x, s(s(b)), s(y), z) → if(le(x, s(y)), x, s(s(b)), s(y), z)
if(true, x, b, y, z) → z
if(false, x, b, y, z) → loop(x, b, times(b, 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)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(0', y) → 0'
times'(s'(x), y) → plus'(y, times'(x, y))
log'(x, 0') → baseError'
log'(x, s'(0')) → baseError'
log'(0', s'(s'(b))) → logZeroError'
log'(s'(x), s'(s'(b))) → loop'(s'(x), s'(s'(b)), s'(0'), 0')
loop'(x, s'(s'(b)), s'(y), z) → if'(le'(x, s'(y)), x, s'(s'(b)), s'(y), z)
if'(true', x, b, y, z) → z
if'(false', x, b, y, z) → loop'(x, b, times'(b, 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)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(0', y) → 0'
times'(s'(x), y) → plus'(y, times'(x, y))
log'(x, 0') → baseError'
log'(x, s'(0')) → baseError'
log'(0', s'(s'(b))) → logZeroError'
log'(s'(x), s'(s'(b))) → loop'(s'(x), s'(s'(b)), s'(0'), 0')
loop'(x, s'(s'(b)), s'(y), z) → if'(le'(x, s'(y)), x, s'(s'(b)), s'(y), z)
if'(true', x, b, y, z) → z
if'(false', x, b, y, z) → loop'(x, b, times'(b, y), s'(z))

Types:
le' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → false':true'
s' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
0' :: s':0':baseError':logZeroError'
false' :: false':true'
true' :: false':true'
plus' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
times' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
log' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
baseError' :: s':0':baseError':logZeroError'
logZeroError' :: s':0':baseError':logZeroError'
loop' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
if' :: false':true' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
_hole_false':true'1 :: false':true'
_hole_s':0':baseError':logZeroError'2 :: s':0':baseError':logZeroError'
_gen_s':0':baseError':logZeroError'3 :: Nat → s':0':baseError':logZeroError'

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

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(0', y) → 0'
times'(s'(x), y) → plus'(y, times'(x, y))
log'(x, 0') → baseError'
log'(x, s'(0')) → baseError'
log'(0', s'(s'(b))) → logZeroError'
log'(s'(x), s'(s'(b))) → loop'(s'(x), s'(s'(b)), s'(0'), 0')
loop'(x, s'(s'(b)), s'(y), z) → if'(le'(x, s'(y)), x, s'(s'(b)), s'(y), z)
if'(true', x, b, y, z) → z
if'(false', x, b, y, z) → loop'(x, b, times'(b, y), s'(z))

Types:
le' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → false':true'
s' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
0' :: s':0':baseError':logZeroError'
false' :: false':true'
true' :: false':true'
plus' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
times' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
log' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
baseError' :: s':0':baseError':logZeroError'
logZeroError' :: s':0':baseError':logZeroError'
loop' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
if' :: false':true' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
_hole_false':true'1 :: false':true'
_hole_s':0':baseError':logZeroError'2 :: s':0':baseError':logZeroError'
_gen_s':0':baseError':logZeroError'3 :: Nat → s':0':baseError':logZeroError'

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

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

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

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

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

Induction Step:
le'(_gen_s':0':baseError':logZeroError'3(+(1, +(_$n6, 1))), _gen_s':0':baseError':logZeroError'3(+(_$n6, 1))) →RΩ(1)
le'(_gen_s':0':baseError':logZeroError'3(+(1, _$n6)), _gen_s':0':baseError':logZeroError'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)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(0', y) → 0'
times'(s'(x), y) → plus'(y, times'(x, y))
log'(x, 0') → baseError'
log'(x, s'(0')) → baseError'
log'(0', s'(s'(b))) → logZeroError'
log'(s'(x), s'(s'(b))) → loop'(s'(x), s'(s'(b)), s'(0'), 0')
loop'(x, s'(s'(b)), s'(y), z) → if'(le'(x, s'(y)), x, s'(s'(b)), s'(y), z)
if'(true', x, b, y, z) → z
if'(false', x, b, y, z) → loop'(x, b, times'(b, y), s'(z))

Types:
le' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → false':true'
s' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
0' :: s':0':baseError':logZeroError'
false' :: false':true'
true' :: false':true'
plus' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
times' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
log' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
baseError' :: s':0':baseError':logZeroError'
logZeroError' :: s':0':baseError':logZeroError'
loop' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
if' :: false':true' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
_hole_false':true'1 :: false':true'
_hole_s':0':baseError':logZeroError'2 :: s':0':baseError':logZeroError'
_gen_s':0':baseError':logZeroError'3 :: Nat → s':0':baseError':logZeroError'

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

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

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

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

Proved the following rewrite lemma:
plus'(_gen_s':0':baseError':logZeroError'3(_n995), _gen_s':0':baseError':logZeroError'3(b)) → _gen_s':0':baseError':logZeroError'3(+(_n995, b)), rt ∈ Ω(1 + n995)

Induction Base:
plus'(_gen_s':0':baseError':logZeroError'3(0), _gen_s':0':baseError':logZeroError'3(b)) →RΩ(1)
_gen_s':0':baseError':logZeroError'3(b)

Induction Step:
plus'(_gen_s':0':baseError':logZeroError'3(+(_$n996, 1)), _gen_s':0':baseError':logZeroError'3(_b1128)) →RΩ(1)
s'(plus'(_gen_s':0':baseError':logZeroError'3(_$n996), _gen_s':0':baseError':logZeroError'3(_b1128))) →IH
s'(_gen_s':0':baseError':logZeroError'3(+(_$n996, _b1128)))

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)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(0', y) → 0'
times'(s'(x), y) → plus'(y, times'(x, y))
log'(x, 0') → baseError'
log'(x, s'(0')) → baseError'
log'(0', s'(s'(b))) → logZeroError'
log'(s'(x), s'(s'(b))) → loop'(s'(x), s'(s'(b)), s'(0'), 0')
loop'(x, s'(s'(b)), s'(y), z) → if'(le'(x, s'(y)), x, s'(s'(b)), s'(y), z)
if'(true', x, b, y, z) → z
if'(false', x, b, y, z) → loop'(x, b, times'(b, y), s'(z))

Types:
le' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → false':true'
s' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
0' :: s':0':baseError':logZeroError'
false' :: false':true'
true' :: false':true'
plus' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
times' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
log' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
baseError' :: s':0':baseError':logZeroError'
logZeroError' :: s':0':baseError':logZeroError'
loop' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
if' :: false':true' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
_hole_false':true'1 :: false':true'
_hole_s':0':baseError':logZeroError'2 :: s':0':baseError':logZeroError'
_gen_s':0':baseError':logZeroError'3 :: Nat → s':0':baseError':logZeroError'

Lemmas:
le'(_gen_s':0':baseError':logZeroError'3(+(1, _n5)), _gen_s':0':baseError':logZeroError'3(_n5)) → false', rt ∈ Ω(1 + n5)
plus'(_gen_s':0':baseError':logZeroError'3(_n995), _gen_s':0':baseError':logZeroError'3(b)) → _gen_s':0':baseError':logZeroError'3(+(_n995, b)), rt ∈ Ω(1 + n995)

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

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

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

Proved the following rewrite lemma:
times'(_gen_s':0':baseError':logZeroError'3(_n2031), _gen_s':0':baseError':logZeroError'3(b)) → _gen_s':0':baseError':logZeroError'3(*(_n2031, b)), rt ∈ Ω(1 + b2291·n2031 + n2031)

Induction Base:
times'(_gen_s':0':baseError':logZeroError'3(0), _gen_s':0':baseError':logZeroError'3(b)) →RΩ(1)
0'

Induction Step:
times'(_gen_s':0':baseError':logZeroError'3(+(_$n2032, 1)), _gen_s':0':baseError':logZeroError'3(_b2291)) →RΩ(1)
plus'(_gen_s':0':baseError':logZeroError'3(_b2291), times'(_gen_s':0':baseError':logZeroError'3(_$n2032), _gen_s':0':baseError':logZeroError'3(_b2291))) →IH
plus'(_gen_s':0':baseError':logZeroError'3(_b2291), _gen_s':0':baseError':logZeroError'3(*(_$n2032, _b2291))) →LΩ(1 + b2291)
_gen_s':0':baseError':logZeroError'3(+(_b2291, *(_$n2032, _b2291)))

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

Rules:
le'(s'(x), 0') → false'
le'(0', y) → true'
le'(s'(x), s'(y)) → le'(x, y)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(0', y) → 0'
times'(s'(x), y) → plus'(y, times'(x, y))
log'(x, 0') → baseError'
log'(x, s'(0')) → baseError'
log'(0', s'(s'(b))) → logZeroError'
log'(s'(x), s'(s'(b))) → loop'(s'(x), s'(s'(b)), s'(0'), 0')
loop'(x, s'(s'(b)), s'(y), z) → if'(le'(x, s'(y)), x, s'(s'(b)), s'(y), z)
if'(true', x, b, y, z) → z
if'(false', x, b, y, z) → loop'(x, b, times'(b, y), s'(z))

Types:
le' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → false':true'
s' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
0' :: s':0':baseError':logZeroError'
false' :: false':true'
true' :: false':true'
plus' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
times' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
log' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
baseError' :: s':0':baseError':logZeroError'
logZeroError' :: s':0':baseError':logZeroError'
loop' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
if' :: false':true' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
_hole_false':true'1 :: false':true'
_hole_s':0':baseError':logZeroError'2 :: s':0':baseError':logZeroError'
_gen_s':0':baseError':logZeroError'3 :: Nat → s':0':baseError':logZeroError'

Lemmas:
le'(_gen_s':0':baseError':logZeroError'3(+(1, _n5)), _gen_s':0':baseError':logZeroError'3(_n5)) → false', rt ∈ Ω(1 + n5)
plus'(_gen_s':0':baseError':logZeroError'3(_n995), _gen_s':0':baseError':logZeroError'3(b)) → _gen_s':0':baseError':logZeroError'3(+(_n995, b)), rt ∈ Ω(1 + n995)
times'(_gen_s':0':baseError':logZeroError'3(_n2031), _gen_s':0':baseError':logZeroError'3(b)) → _gen_s':0':baseError':logZeroError'3(*(_n2031, b)), rt ∈ Ω(1 + b2291·n2031 + n2031)

Generator Equations:
_gen_s':0':baseError':logZeroError'3(0) ⇔ 0'
_gen_s':0':baseError':logZeroError'3(+(x, 1)) ⇔ s'(_gen_s':0':baseError':logZeroError'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)
plus'(0', y) → y
plus'(s'(x), y) → s'(plus'(x, y))
times'(0', y) → 0'
times'(s'(x), y) → plus'(y, times'(x, y))
log'(x, 0') → baseError'
log'(x, s'(0')) → baseError'
log'(0', s'(s'(b))) → logZeroError'
log'(s'(x), s'(s'(b))) → loop'(s'(x), s'(s'(b)), s'(0'), 0')
loop'(x, s'(s'(b)), s'(y), z) → if'(le'(x, s'(y)), x, s'(s'(b)), s'(y), z)
if'(true', x, b, y, z) → z
if'(false', x, b, y, z) → loop'(x, b, times'(b, y), s'(z))

Types:
le' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → false':true'
s' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
0' :: s':0':baseError':logZeroError'
false' :: false':true'
true' :: false':true'
plus' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
times' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
log' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
baseError' :: s':0':baseError':logZeroError'
logZeroError' :: s':0':baseError':logZeroError'
loop' :: s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
if' :: false':true' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError' → s':0':baseError':logZeroError'
_hole_false':true'1 :: false':true'
_hole_s':0':baseError':logZeroError'2 :: s':0':baseError':logZeroError'
_gen_s':0':baseError':logZeroError'3 :: Nat → s':0':baseError':logZeroError'

Lemmas:
le'(_gen_s':0':baseError':logZeroError'3(+(1, _n5)), _gen_s':0':baseError':logZeroError'3(_n5)) → false', rt ∈ Ω(1 + n5)
plus'(_gen_s':0':baseError':logZeroError'3(_n995), _gen_s':0':baseError':logZeroError'3(b)) → _gen_s':0':baseError':logZeroError'3(+(_n995, b)), rt ∈ Ω(1 + n995)
times'(_gen_s':0':baseError':logZeroError'3(_n2031), _gen_s':0':baseError':logZeroError'3(b)) → _gen_s':0':baseError':logZeroError'3(*(_n2031, b)), rt ∈ Ω(1 + b2291·n2031 + n2031)

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

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
times'(_gen_s':0':baseError':logZeroError'3(_n2031), _gen_s':0':baseError':logZeroError'3(b)) → _gen_s':0':baseError':logZeroError'3(*(_n2031, b)), rt ∈ Ω(1 + b2291·n2031 + n2031)