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

f(s(X)) → f(X)
g(cons(0, Y)) → g(Y)
g(cons(s(X), Y)) → s(X)
h(cons(X, Y)) → h(g(cons(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'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))

Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'

Heuristically decided to analyse the following defined symbols:
f', g', h'

They will be analysed ascendingly in the following order:
g' < h'

Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))

Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'

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

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

They will be analysed ascendingly in the following order:
g' < h'

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

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

Induction Step:
f'(_gen_s':0':cons'4(+(1, +(_\$n7, 1)))) →RΩ(1)
f'(_gen_s':0':cons'4(+(1, _\$n7))) →IH
_*5

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

Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))

Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'

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

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

The following defined symbols remain to be analysed:
g', h'

They will be analysed ascendingly in the following order:
g' < h'

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

Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))

Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'

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

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

The following defined symbols remain to be analysed:
h'

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

Rules:
f'(s'(X)) → f'(X)
g'(cons'(0', Y)) → g'(Y)
g'(cons'(s'(X), Y)) → s'(X)
h'(cons'(X, Y)) → h'(g'(cons'(X, Y)))

Types:
f' :: s':0':cons' → f'
s' :: s':0':cons' → s':0':cons'
g' :: s':0':cons' → s':0':cons'
cons' :: s':0':cons' → s':0':cons' → s':0':cons'
0' :: s':0':cons'
h' :: s':0':cons' → h'
_hole_f'1 :: f'
_hole_s':0':cons'2 :: s':0':cons'
_hole_h'3 :: h'
_gen_s':0':cons'4 :: Nat → s':0':cons'

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

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

No more defined symbols left to analyse.

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