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

top(free(x)) → top(check(new(x)))
new(free(x)) → free(new(x))
old(free(x)) → free(old(x))
new(serve) → free(serve)
old(serve) → free(serve)
check(free(x)) → free(check(x))
check(new(x)) → new(check(x))
check(old(x)) → old(check(x))
check(old(x)) → old(x)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

top'(free'(x)) → top'(check'(new'(x)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
top'(free'(x)) → top'(check'(new'(x)))
new'(free'(x)) → free'(new'(x))
old'(free'(x)) → free'(old'(x))
new'(serve') → free'(serve')
old'(serve') → free'(serve')
check'(free'(x)) → free'(check'(x))
check'(new'(x)) → new'(check'(x))
check'(old'(x)) → old'(check'(x))
check'(old'(x)) → old'(x)

Types:
top' :: free':serve' → top'
free' :: free':serve' → free':serve'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top'1 :: top'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'

Heuristically decided to analyse the following defined symbols:
top', check', new', old'

They will be analysed ascendingly in the following order:
check' < top'
new' < top'
new' < check'
old' < check'

Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))

The following defined symbols remain to be analysed:
new', top', check', old'

They will be analysed ascendingly in the following order:
check' < top'
new' < top'
new' < check'
old' < check'

Proved the following rewrite lemma:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + _n5)

Induction Base:
new'(_gen_free':serve'3(0)) →_R^Ω(1)
free'(serve')

Induction Step:
new'(_gen_free':serve'3(+(_$n6, 1))) →_R^Ω(1)
free'(new'(_gen_free':serve'3(_$n6))) →_IH
free'(_gen_free':serve'3(+(1, _$n6)))

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

Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + _n5)

Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))

The following defined symbols remain to be analysed:
old', top', check'

They will be analysed ascendingly in the following order:
check' < top'
old' < check'

Proved the following rewrite lemma:
old'(_gen_free':serve'3(_n287)) → _gen_free':serve'3(+(1, _n287)), rt ∈ Ω(1 + _n287)

Induction Base:
old'(_gen_free':serve'3(0)) →_R^Ω(1)
free'(serve')

Induction Step:
old'(_gen_free':serve'3(+(_$n288, 1))) →_R^Ω(1)
free'(old'(_gen_free':serve'3(_$n288))) →_IH
free'(_gen_free':serve'3(+(1, _$n288)))

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

Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + _n5)
old'(_gen_free':serve'3(_n287)) → _gen_free':serve'3(+(1, _n287)), rt ∈ Ω(1 + _n287)

Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))

The following defined symbols remain to be analysed:
check', top'

They will be analysed ascendingly in the following order:
check' < top'

Proved the following rewrite lemma:
check'(_gen_free':serve'3(+(1, _n591))) → _*4, rt ∈ Ω(_n591)

Induction Base:
check'(_gen_free':serve'3(+(1, 0)))

Induction Step:
check'(_gen_free':serve'3(+(1, +(_$n592, 1)))) →_R^Ω(1)
free'(check'(_gen_free':serve'3(+(1, _$n592)))) →_IH
free'(_*4)

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

Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + _n5)
old'(_gen_free':serve'3(_n287)) → _gen_free':serve'3(+(1, _n287)), rt ∈ Ω(1 + _n287)
check'(_gen_free':serve'3(+(1, _n591))) → _*4, rt ∈ Ω(_n591)

Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))

The following defined symbols remain to be analysed:
top'

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

Generator Equations:
_gen_free':serve'3(0) ⇔ serve'
_gen_free':serve'3(+(x, 1)) ⇔ free'(_gen_free':serve'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + _n5)