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

log(x, s(s(y))) → cond(le(x, s(s(y))), x, y)
cond(true, x, y) → s(0)
cond(false, x, y) → double(log(x, square(s(s(y)))))
le(0, v) → true
le(s(u), 0) → false
le(s(u), s(v)) → le(u, v)
double(0) → 0
double(s(x)) → s(s(double(x)))
square(0) → 0
square(s(x)) → s(plus(square(x), double(x)))
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

log'(x, s'(s'(y))) → cond'(le'(x, s'(s'(y))), x, y)
cond'(true', x, y) → s'(0')
cond'(false', x, y) → double'(log'(x, square'(s'(s'(y)))))
le'(0', v) → true'
le'(s'(u), 0') → false'
le'(s'(u), s'(v)) → le'(u, v)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
square'(0') → 0'
square'(s'(x)) → s'(plus'(square'(x), double'(x)))
plus'(n, 0') → n
plus'(n, s'(m)) → s'(plus'(n, m))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
log'(x, s'(s'(y))) → cond'(le'(x, s'(s'(y))), x, y)
cond'(true', x, y) → s'(0')
cond'(false', x, y) → double'(log'(x, square'(s'(s'(y)))))
le'(0', v) → true'
le'(s'(u), 0') → false'
le'(s'(u), s'(v)) → le'(u, v)
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
square'(0') → 0'
square'(s'(x)) → s'(plus'(square'(x), double'(x)))
plus'(n, 0') → n
plus'(n, s'(m)) → s'(plus'(n, m))

Types:
log' :: s':0' → s':0' → s':0'
s' :: s':0' → s':0'
cond' :: true':false' → s':0' → s':0' → s':0'
le' :: s':0' → s':0' → true':false'
true' :: true':false'
0' :: s':0'
false' :: true':false'
double' :: s':0' → s':0'
square' :: s':0' → s':0'
plus' :: s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_hole_true':false'2 :: true':false'
_gen_s':0'3 :: Nat → s':0'

Heuristically decided to analyse the following defined symbols:
log', le', double', square', plus'

They will be analysed ascendingly in the following order:
le' < log'
double' < log'
square' < log'
double' < square'
plus' < square'

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

The following defined symbols remain to be analysed:
le', log', double', square', plus'

They will be analysed ascendingly in the following order:
le' < log'
double' < log'
square' < log'
double' < square'
plus' < square'

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

Induction Base:
le'(_gen_s':0'3(0), _gen_s':0'3(0)) →_R^Ω(1)
true'

Induction Step:
le'(_gen_s':0'3(+(_$n6, 1)), _gen_s':0'3(+(_$n6, 1))) →_R^Ω(1)
le'(_gen_s':0'3(_$n6), _gen_s':0'3(_$n6)) →_IH
true'

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

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

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

The following defined symbols remain to be analysed:
double', log', square', plus'

They will be analysed ascendingly in the following order:
double' < log'
square' < log'
double' < square'
plus' < square'

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

Induction Base:
double'(_gen_s':0'3(0)) →_R^Ω(1)
0'

Induction Step:
double'(_gen_s':0'3(+(_$n558, 1))) →_R^Ω(1)
s'(s'(double'(_gen_s':0'3(_$n558)))) →_IH
s'(s'(_gen_s':0'3(*(2, _$n558))))

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

Lemmas:
le'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → true', rt ∈ Ω(1 + _n5)
double'(_gen_s':0'3(_n557)) → _gen_s':0'3(*(2, _n557)), rt ∈ Ω(1 + _n557)

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

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

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

Proved the following rewrite lemma:
plus'(_gen_s':0'3(a), _gen_s':0'3(_n1029)) → _gen_s':0'3(+(_n1029, a)), rt ∈ Ω(1 + _n1029)

Induction Base:
plus'(_gen_s':0'3(a), _gen_s':0'3(0)) →_R^Ω(1)
_gen_s':0'3(a)

Induction Step:
plus'(_gen_s':0'3(_a1162), _gen_s':0'3(+(_$n1030, 1))) →_R^Ω(1)
s'(plus'(_gen_s':0'3(_a1162), _gen_s':0'3(_$n1030))) →_IH
s'(_gen_s':0'3(+(_$n1030, _a1162)))

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

Lemmas:
le'(_gen_s':0'3(_n5), _gen_s':0'3(_n5)) → true', rt ∈ Ω(1 + _n5)
double'(_gen_s':0'3(_n557)) → _gen_s':0'3(*(2, _n557)), rt ∈ Ω(1 + _n557)
plus'(_gen_s':0'3(a), _gen_s':0'3(_n1029)) → _gen_s':0'3(+(_n1029, a)), rt ∈ Ω(1 + _n1029)

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

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

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

Proved the following rewrite lemma:
square'(_gen_s':0'3(_n1796)) → _gen_s':0'3(*(_n1796, _n1796)), rt ∈ Ω(1 + _n1796 + _n1796²)

Induction Base:
square'(_gen_s':0'3(0)) →_R^Ω(1)
0'

Induction Step:
square'(_gen_s':0'3(+(_$n1797, 1))) →_R^Ω(1)
s'(plus'(square'(_gen_s':0'3(_$n1797)), double'(_gen_s':0'3(_$n1797)))) →_IH
s'(plus'(_gen_s':0'3(*(_$n1797, _$n1797)), double'(_gen_s':0'3(_$n1797)))) →_L^{Ω(1 + _$n1797)}
s'(plus'(_gen_s':0'3(*(_$n1797, _$n1797)), _gen_s':0'3(*(2, _$n1797)))) →_L^{Ω(1 + 2·_$n1797)}
s'(_gen_s':0'3(+(*(2, _$n1797), *(_$n1797, _$n1797))))

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

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

The following defined symbols remain to be analysed:
log'

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

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

No more defined symbols left to analyse.

The lowerbound Ω(n²) was proven with the following lemma:
square'(_gen_s':0'3(_n1796)) → _gen_s':0'3(*(_n1796, _n1796)), rt ∈ Ω(1 + _n1796 + _n1796²)