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

active(f(x)) → mark(f(f(x)))
chk(no(f(x))) → f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
mat(f(x), f(y)) → f(mat(x, y))
chk(no(c)) → active(c)
mat(f(x), c) → no(c)
f(active(x)) → active(f(x))
f(no(x)) → no(f(x))
f(mark(x)) → mark(f(x))
tp(mark(x)) → tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), 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'(f'(f'(x)))
chk'(no'(f'(x))) → f'(chk'(mat'(f'(f'(f'(f'(f'(f'(f'(f'(f'(f'(X')))))))))), x)))
mat'(f'(x), f'(y')) → f'(mat'(x, y'))
chk'(no'(c')) → active'(c')
mat'(f'(x), c') → no'(c')
f'(active'(x)) → active'(f'(x))
f'(no'(x)) → no'(f'(x))
f'(mark'(x)) → mark'(f'(x))
tp'(mark'(x)) → tp'(chk'(mat'(f'(f'(f'(f'(f'(f'(f'(f'(f'(f'(X')))))))))), x)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
active'(f'(x)) → mark'(f'(f'(x)))
chk'(no'(f'(x))) → f'(chk'(mat'(f'(f'(f'(f'(f'(f'(f'(f'(f'(f'(X')))))))))), x)))
mat'(f'(x), f'(y')) → f'(mat'(x, y'))
chk'(no'(c')) → active'(c')
mat'(f'(x), c') → no'(c')
f'(active'(x)) → active'(f'(x))
f'(no'(x)) → no'(f'(x))
f'(mark'(x)) → mark'(f'(x))
tp'(mark'(x)) → tp'(chk'(mat'(f'(f'(f'(f'(f'(f'(f'(f'(f'(f'(X')))))))))), x)))

Types:
active' :: mark':no':X':y':c' → mark':no':X':y':c'
f' :: mark':no':X':y':c' → mark':no':X':y':c'
mark' :: mark':no':X':y':c' → mark':no':X':y':c'
chk' :: mark':no':X':y':c' → mark':no':X':y':c'
no' :: mark':no':X':y':c' → mark':no':X':y':c'
mat' :: mark':no':X':y':c' → mark':no':X':y':c' → mark':no':X':y':c'
X' :: mark':no':X':y':c'
y' :: mark':no':X':y':c'
c' :: mark':no':X':y':c'
tp' :: mark':no':X':y':c' → tp'
_hole_mark':no':X':y':c'1 :: mark':no':X':y':c'
_hole_tp'2 :: tp'
_gen_mark':no':X':y':c'3 :: Nat → mark':no':X':y':c'

Heuristically decided to analyse the following defined symbols:
active', f', chk', mat', tp'

They will be analysed ascendingly in the following order:
active' = f'
active' < chk'
f' < chk'
f' < mat'
f' < tp'
mat' < chk'
chk' < tp'
mat' < tp'

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

The following defined symbols remain to be analysed:
f', active', chk', mat', tp'

They will be analysed ascendingly in the following order:
active' = f'
active' < chk'
f' < chk'
f' < mat'
f' < tp'
mat' < chk'
chk' < tp'
mat' < tp'

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

Induction Base:
f'(_gen_mark':no':X':y':c'3(+(1, 0)))

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

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

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

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

The following defined symbols remain to be analysed:
active', chk', mat', tp'

They will be analysed ascendingly in the following order:
active' = f'
active' < chk'
f' < chk'
f' < mat'
f' < tp'
mat' < chk'
chk' < tp'
mat' < tp'

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

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

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

The following defined symbols remain to be analysed:
mat', chk', tp'

They will be analysed ascendingly in the following order:
mat' < chk'
chk' < tp'
mat' < tp'

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

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

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

The following defined symbols remain to be analysed:
chk', tp'

They will be analysed ascendingly in the following order:
chk' < tp'

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

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

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

The following defined symbols remain to be analysed:
tp'

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

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

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

No more defined symbols left to analyse.

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