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

f_0(x) → a
f_1(x) → g_1(x, x)
g_1(s(x), y) → b(f_0(y), g_1(x, y))
f_2(x) → g_2(x, x)
g_2(s(x), y) → b(f_1(y), g_2(x, y))
f_3(x) → g_3(x, x)
g_3(s(x), y) → b(f_2(y), g_3(x, y))
f_4(x) → g_4(x, x)
g_4(s(x), y) → b(f_3(y), g_4(x, y))
f_5(x) → g_5(x, x)
g_5(s(x), y) → b(f_4(y), g_5(x, y))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

f_0'(x) → a'
f_1'(x) → g_1'(x, x)
g_1'(s'(x), y) → b'(f_0'(y), g_1'(x, y))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
f_0'/0
g_1'/1

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

f_0'a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f_0'a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))

Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'

Heuristically decided to analyse the following defined symbols:
g_1', g_2', g_3', g_4', g_5'

Rules:
f_0'a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))

Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'

Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))

The following defined symbols remain to be analysed:
g_1', g_2', g_3', g_4', g_5'

Proved the following rewrite lemma:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)

Induction Base:
g_1'(_gen_s'4(+(1, 0)))

Induction Step:
g_1'(_gen_s'4(+(1, +(_\$n7, 1)))) →RΩ(1)
b'(f_0', g_1'(_gen_s'4(+(1, _\$n7)))) →RΩ(1)
b'(a', g_1'(_gen_s'4(+(1, _\$n7)))) →IH
b'(a', _*5)

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

Rules:
f_0'a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))

Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'

Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)

Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))

The following defined symbols remain to be analysed:
g_2', g_3', g_4', g_5'

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

Rules:
f_0'a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))

Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'

Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)

Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))

The following defined symbols remain to be analysed:
g_3', g_4', g_5'

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

Rules:
f_0'a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))

Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'

Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)

Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))

The following defined symbols remain to be analysed:
g_4', g_5'

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

Rules:
f_0'a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))

Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'

Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)

Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))

The following defined symbols remain to be analysed:
g_5'

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

Rules:
f_0'a'
f_1'(x) → g_1'(x)
g_1'(s'(x)) → b'(f_0', g_1'(x))
f_2'(x) → g_2'(x, x)
g_2'(s'(x), y) → b'(f_1'(y), g_2'(x, y))
f_3'(x) → g_3'(x, x)
g_3'(s'(x), y) → b'(f_2'(y), g_3'(x, y))
f_4'(x) → g_4'(x, x)
g_4'(s'(x), y) → b'(f_3'(y), g_4'(x, y))
f_5'(x) → g_5'(x, x)
g_5'(s'(x), y) → b'(f_4'(y), g_5'(x, y))

Types:
f_0' :: a':b'
a' :: a':b'
f_1' :: s' → a':b'
g_1' :: s' → a':b'
s' :: s' → s'
b' :: a':b' → a':b' → a':b'
f_2' :: s' → a':b'
g_2' :: s' → s' → a':b'
f_3' :: s' → a':b'
g_3' :: s' → s' → a':b'
f_4' :: s' → a':b'
g_4' :: s' → s' → a':b'
f_5' :: s' → a':b'
g_5' :: s' → s' → a':b'
_hole_a':b'1 :: a':b'
_hole_s'2 :: s'
_gen_a':b'3 :: Nat → a':b'
_gen_s'4 :: Nat → s'

Lemmas:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)

Generator Equations:
_gen_a':b'3(0) ⇔ a'
_gen_a':b'3(+(x, 1)) ⇔ b'(a', _gen_a':b'3(x))
_gen_s'4(0) ⇔ _hole_s'2
_gen_s'4(+(x, 1)) ⇔ s'(_gen_s'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
g_1'(_gen_s'4(+(1, _n6))) → _*5, rt ∈ Ω(n6)