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

tower(x) → f(a, x, s(0))
f(a, 0, y) → y
f(a, s(x), y) → f(b, y, s(x))
f(b, y, x) → f(a, half(x), exp(y))
exp(0) → s(0)
exp(s(x)) → double(exp(x))
double(0) → 0
double(s(x)) → s(s(double(x)))
half(0) → double(0)
half(s(0)) → half(0)
half(s(s(x))) → s(half(x))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))

Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'

Heuristically decided to analyse the following defined symbols:
f', half', exp', double'

They will be analysed ascendingly in the following order:
half' < f'
exp' < f'
double' < half'
double' < exp'

Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))

Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'

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

The following defined symbols remain to be analysed:
double', f', half', exp'

They will be analysed ascendingly in the following order:
half' < f'
exp' < f'
double' < half'
double' < exp'

Proved the following rewrite lemma:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)

Induction Base:
double'(_gen_0':s'3(0)) →RΩ(1)
0'

Induction Step:
double'(_gen_0':s'3(+(_\$n6, 1))) →RΩ(1)
s'(s'(double'(_gen_0':s'3(_\$n6)))) →IH
s'(s'(_gen_0':s'3(*(2, _\$n6))))

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

Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))

Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'

Lemmas:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)

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

The following defined symbols remain to be analysed:
half', f', exp'

They will be analysed ascendingly in the following order:
half' < f'
exp' < f'

Proved the following rewrite lemma:
half'(_gen_0':s'3(*(2, _n351))) → _gen_0':s'3(_n351), rt ∈ Ω(1 + n351)

Induction Base:
half'(_gen_0':s'3(*(2, 0))) →RΩ(1)
double'(0') →LΩ(1)
_gen_0':s'3(*(2, 0))

Induction Step:
half'(_gen_0':s'3(*(2, +(_\$n352, 1)))) →RΩ(1)
s'(half'(_gen_0':s'3(*(2, _\$n352)))) →IH
s'(_gen_0':s'3(_\$n352))

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

Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))

Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'

Lemmas:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)
half'(_gen_0':s'3(*(2, _n351))) → _gen_0':s'3(_n351), rt ∈ Ω(1 + n351)

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

The following defined symbols remain to be analysed:
exp', f'

They will be analysed ascendingly in the following order:
exp' < f'

Proved the following rewrite lemma:
exp'(_gen_0':s'3(+(1, _n984))) → _*4, rt ∈ Ω(n984)

Induction Base:
exp'(_gen_0':s'3(+(1, 0)))

Induction Step:
exp'(_gen_0':s'3(+(1, +(_\$n985, 1)))) →RΩ(1)
double'(exp'(_gen_0':s'3(+(1, _\$n985)))) →IH
double'(_*4)

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

Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))

Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'

Lemmas:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)
half'(_gen_0':s'3(*(2, _n351))) → _gen_0':s'3(_n351), rt ∈ Ω(1 + n351)
exp'(_gen_0':s'3(+(1, _n984))) → _*4, rt ∈ Ω(n984)

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

The following defined symbols remain to be analysed:
f'

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

Rules:
tower'(x) → f'(a', x, s'(0'))
f'(a', 0', y) → y
f'(a', s'(x), y) → f'(b', y, s'(x))
f'(b', y, x) → f'(a', half'(x), exp'(y))
exp'(0') → s'(0')
exp'(s'(x)) → double'(exp'(x))
double'(0') → 0'
double'(s'(x)) → s'(s'(double'(x)))
half'(0') → double'(0')
half'(s'(0')) → half'(0')
half'(s'(s'(x))) → s'(half'(x))

Types:
tower' :: 0':s' → 0':s'
f' :: a':b' → 0':s' → 0':s' → 0':s'
a' :: a':b'
s' :: 0':s' → 0':s'
0' :: 0':s'
b' :: a':b'
half' :: 0':s' → 0':s'
exp' :: 0':s' → 0':s'
double' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_a':b'2 :: a':b'
_gen_0':s'3 :: Nat → 0':s'

Lemmas:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)
half'(_gen_0':s'3(*(2, _n351))) → _gen_0':s'3(_n351), rt ∈ Ω(1 + n351)
exp'(_gen_0':s'3(+(1, _n984))) → _*4, rt ∈ Ω(n984)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
double'(_gen_0':s'3(_n5)) → _gen_0':s'3(*(2, _n5)), rt ∈ Ω(1 + n5)