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

top1(free(x), y) → top2(check(new(x)), y)
top1(free(x), y) → top2(new(x), check(y))
top1(free(x), y) → top2(check(x), new(y))
top1(free(x), y) → top2(x, check(new(y)))
top2(x, free(y)) → top1(check(new(x)), y)
top2(x, free(y)) → top1(new(x), check(y))
top2(x, free(y)) → top1(check(x), new(y))
top2(x, free(y)) → top1(x, check(new(y)))
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:

top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
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:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
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:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'

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

They will be analysed ascendingly in the following order:
top1' = top2'
check' < top1'
new' < top1'
check' < top2'
new' < top2'
new' < check'
old' < check'

Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
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:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'

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', top1', top2', check', old'

They will be analysed ascendingly in the following order:
top1' = top2'
check' < top1'
new' < top1'
check' < top2'
new' < top2'
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 ircR ∈ Ω(n).

Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
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:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'

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', top1', top2', check'

They will be analysed ascendingly in the following order:
top1' = top2'
check' < top1'
check' < top2'
old' < check'

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

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

Induction Step:
old'(_gen_free':serve'3(+(_\$n586, 1))) →RΩ(1)
free'(old'(_gen_free':serve'3(_\$n586))) →IH
free'(_gen_free':serve'3(+(1, _\$n586)))

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

Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
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:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'

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

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', top1', top2'

They will be analysed ascendingly in the following order:
top1' = top2'
check' < top1'
check' < top2'

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

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

Induction Step:
check'(_gen_free':serve'3(+(1, +(_\$n1188, 1)))) →RΩ(1)
free'(check'(_gen_free':serve'3(+(1, _\$n1188)))) →IH
free'(_*4)

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

Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
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:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'

Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)
old'(_gen_free':serve'3(_n585)) → _gen_free':serve'3(+(1, _n585)), rt ∈ Ω(1 + n585)
check'(_gen_free':serve'3(+(1, _n1187))) → _*4, rt ∈ Ω(n1187)

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:
top2', top1'

They will be analysed ascendingly in the following order:
top1' = top2'

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

Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
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:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'

Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)
old'(_gen_free':serve'3(_n585)) → _gen_free':serve'3(+(1, _n585)), rt ∈ Ω(1 + n585)
check'(_gen_free':serve'3(+(1, _n1187))) → _*4, rt ∈ Ω(n1187)

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:
top1'

They will be analysed ascendingly in the following order:
top1' = top2'

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

Rules:
top1'(free'(x), y) → top2'(check'(new'(x)), y)
top1'(free'(x), y) → top2'(new'(x), check'(y))
top1'(free'(x), y) → top2'(check'(x), new'(y))
top1'(free'(x), y) → top2'(x, check'(new'(y)))
top2'(x, free'(y)) → top1'(check'(new'(x)), y)
top2'(x, free'(y)) → top1'(new'(x), check'(y))
top2'(x, free'(y)) → top1'(check'(x), new'(y))
top2'(x, free'(y)) → top1'(x, check'(new'(y)))
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:
top1' :: free':serve' → free':serve' → top1':top2'
free' :: free':serve' → free':serve'
top2' :: free':serve' → free':serve' → top1':top2'
check' :: free':serve' → free':serve'
new' :: free':serve' → free':serve'
old' :: free':serve' → free':serve'
serve' :: free':serve'
_hole_top1':top2'1 :: top1':top2'
_hole_free':serve'2 :: free':serve'
_gen_free':serve'3 :: Nat → free':serve'

Lemmas:
new'(_gen_free':serve'3(_n5)) → _gen_free':serve'3(+(1, _n5)), rt ∈ Ω(1 + n5)
old'(_gen_free':serve'3(_n585)) → _gen_free':serve'3(+(1, _n585)), rt ∈ Ω(1 + n585)
check'(_gen_free':serve'3(+(1, _n1187))) → _*4, rt ∈ Ω(n1187)

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)