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

active(f(x)) → mark(x)
top(active(c)) → top(mark(c))
top(mark(x)) → top(check(x))
check(f(x)) → f(check(x))
check(x) → start(match(f(X), x))
match(f(x), f(y)) → f(match(x, y))
match(X, x) → proper(x)
proper(c) → ok(c)
proper(f(x)) → f(proper(x))
f(ok(x)) → ok(f(x))
start(ok(x)) → found(x)
f(found(x)) → found(f(x))
top(found(x)) → top(active(x))
active(f(x)) → f(active(x))
f(mark(x)) → mark(f(x))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

active'(f'(x)) → mark'(x)
top'(active'(c')) → top'(mark'(c'))
top'(mark'(x)) → top'(check'(x))
check'(f'(x)) → f'(check'(x))
check'(x) → start'(match'(f'(X'), x))
match'(f'(x), f'(y)) → f'(match'(x, y))
match'(X', x) → proper'(x)
proper'(c') → ok'(c')
proper'(f'(x)) → f'(proper'(x))
f'(ok'(x)) → ok'(f'(x))
start'(ok'(x)) → found'(x)
f'(found'(x)) → found'(f'(x))
top'(found'(x)) → top'(active'(x))
active'(f'(x)) → f'(active'(x))
f'(mark'(x)) → mark'(f'(x))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
active'(f'(x)) → mark'(x)
top'(active'(c')) → top'(mark'(c'))
top'(mark'(x)) → top'(check'(x))
check'(f'(x)) → f'(check'(x))
check'(x) → start'(match'(f'(X'), x))
match'(f'(x), f'(y)) → f'(match'(x, y))
match'(X', x) → proper'(x)
proper'(c') → ok'(c')
proper'(f'(x)) → f'(proper'(x))
f'(ok'(x)) → ok'(f'(x))
start'(ok'(x)) → found'(x)
f'(found'(x)) → found'(f'(x))
top'(found'(x)) → top'(active'(x))
active'(f'(x)) → f'(active'(x))
f'(mark'(x)) → mark'(f'(x))

Types:
active' :: mark':c':X':ok':found' → mark':c':X':ok':found'
f' :: mark':c':X':ok':found' → mark':c':X':ok':found'
mark' :: mark':c':X':ok':found' → mark':c':X':ok':found'
top' :: mark':c':X':ok':found' → top'
c' :: mark':c':X':ok':found'
check' :: mark':c':X':ok':found' → mark':c':X':ok':found'
start' :: mark':c':X':ok':found' → mark':c':X':ok':found'
match' :: mark':c':X':ok':found' → mark':c':X':ok':found' → mark':c':X':ok':found'
X' :: mark':c':X':ok':found'
proper' :: mark':c':X':ok':found' → mark':c':X':ok':found'
ok' :: mark':c':X':ok':found' → mark':c':X':ok':found'
found' :: mark':c':X':ok':found' → mark':c':X':ok':found'
_hole_mark':c':X':ok':found'1 :: mark':c':X':ok':found'
_hole_top'2 :: top'
_gen_mark':c':X':ok':found'3 :: Nat → mark':c':X':ok':found'

Heuristically decided to analyse the following defined symbols:
top', check', f', match', proper', active'

They will be analysed ascendingly in the following order:
check' < top'
active' < top'
f' < check'
match' < check'
f' < match'
f' < proper'
f' < active'
proper' < match'

Generator Equations:
_gen_mark':c':X':ok':found'3(0) ⇔ c'
_gen_mark':c':X':ok':found'3(+(x, 1)) ⇔ mark'(_gen_mark':c':X':ok':found'3(x))

The following defined symbols remain to be analysed:
f', top', check', match', proper', active'

They will be analysed ascendingly in the following order:
check' < top'
active' < top'
f' < check'
match' < check'
f' < match'
f' < proper'
f' < active'
proper' < match'

Proved the following rewrite lemma:
f'(_gen_mark':c':X':ok':found'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Induction Base:
f'(_gen_mark':c':X':ok':found'3(+(1, 0)))

Induction Step:
f'(_gen_mark':c':X':ok':found'3(+(1, +(_$n6, 1)))) →_R^Ω(1)
mark'(f'(_gen_mark':c':X':ok':found'3(+(1, _$n6)))) →_IH
mark'(_*4)

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

Lemmas:
f'(_gen_mark':c':X':ok':found'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_mark':c':X':ok':found'3(0) ⇔ c'
_gen_mark':c':X':ok':found'3(+(x, 1)) ⇔ mark'(_gen_mark':c':X':ok':found'3(x))

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

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

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

Lemmas:
f'(_gen_mark':c':X':ok':found'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_mark':c':X':ok':found'3(0) ⇔ c'
_gen_mark':c':X':ok':found'3(+(x, 1)) ⇔ mark'(_gen_mark':c':X':ok':found'3(x))

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

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

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

Lemmas:
f'(_gen_mark':c':X':ok':found'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_mark':c':X':ok':found'3(0) ⇔ c'
_gen_mark':c':X':ok':found'3(+(x, 1)) ⇔ mark'(_gen_mark':c':X':ok':found'3(x))

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

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

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

Lemmas:
f'(_gen_mark':c':X':ok':found'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_mark':c':X':ok':found'3(0) ⇔ c'
_gen_mark':c':X':ok':found'3(+(x, 1)) ⇔ mark'(_gen_mark':c':X':ok':found'3(x))

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

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

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

Lemmas:
f'(_gen_mark':c':X':ok':found'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_mark':c':X':ok':found'3(0) ⇔ c'
_gen_mark':c':X':ok':found'3(+(x, 1)) ⇔ mark'(_gen_mark':c':X':ok':found'3(x))

The following defined symbols remain to be analysed:
top'

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

Lemmas:
f'(_gen_mark':c':X':ok':found'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_mark':c':X':ok':found'3(0) ⇔ c'
_gen_mark':c':X':ok':found'3(+(x, 1)) ⇔ mark'(_gen_mark':c':X':ok':found'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
f'(_gen_mark':c':X':ok':found'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)