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

active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
f(x, y, mark(z)) → mark(f(x, y, z))
active(d) → mark(c)
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(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'(b', c', x)) → mark'(f'(x, x, x))
active'(f'(x, y, z)) → f'(x, y, active'(z))
active'(d') → m'(b')
f'(x, y, mark'(z)) → mark'(f'(x, y, z))
active'(d') → mark'(c')
proper'(b') → ok'(b')
proper'(c') → ok'(c')
proper'(d') → ok'(d')
proper'(f'(x, y, z)) → f'(proper'(x), proper'(y), proper'(z))
f'(ok'(x), ok'(y), ok'(z)) → ok'(f'(x, y, z))
top'(mark'(x)) → top'(proper'(x))
top'(ok'(x)) → top'(active'(x))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
m'/0

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

active'(f'(b', c', x)) → mark'(f'(x, x, x))
active'(f'(x, y, z)) → f'(x, y, active'(z))
active'(d') → m'
f'(x, y, mark'(z)) → mark'(f'(x, y, z))
active'(d') → mark'(c')
proper'(b') → ok'(b')
proper'(c') → ok'(c')
proper'(d') → ok'(d')
proper'(f'(x, y, z)) → f'(proper'(x), proper'(y), proper'(z))
f'(ok'(x), ok'(y), ok'(z)) → ok'(f'(x, y, z))
top'(mark'(x)) → top'(proper'(x))
top'(ok'(x)) → top'(active'(x))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
active'(f'(b', c', x)) → mark'(f'(x, x, x))
active'(f'(x, y, z)) → f'(x, y, active'(z))
active'(d') → m'
f'(x, y, mark'(z)) → mark'(f'(x, y, z))
active'(d') → mark'(c')
proper'(b') → ok'(b')
proper'(c') → ok'(c')
proper'(d') → ok'(d')
proper'(f'(x, y, z)) → f'(proper'(x), proper'(y), proper'(z))
f'(ok'(x), ok'(y), ok'(z)) → ok'(f'(x, y, z))
top'(mark'(x)) → top'(proper'(x))
top'(ok'(x)) → top'(active'(x))

Types:
active' :: b':c':mark':d':m':ok' → b':c':mark':d':m':ok'
f' :: b':c':mark':d':m':ok' → b':c':mark':d':m':ok' → b':c':mark':d':m':ok' → b':c':mark':d':m':ok'
b' :: b':c':mark':d':m':ok'
c' :: b':c':mark':d':m':ok'
mark' :: b':c':mark':d':m':ok' → b':c':mark':d':m':ok'
d' :: b':c':mark':d':m':ok'
m' :: b':c':mark':d':m':ok'
proper' :: b':c':mark':d':m':ok' → b':c':mark':d':m':ok'
ok' :: b':c':mark':d':m':ok' → b':c':mark':d':m':ok'
top' :: b':c':mark':d':m':ok' → top'
_hole_b':c':mark':d':m':ok'1 :: b':c':mark':d':m':ok'
_hole_top'2 :: top'
_gen_b':c':mark':d':m':ok'3 :: Nat → b':c':mark':d':m':ok'

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

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

Generator Equations:
_gen_b':c':mark':d':m':ok'3(0) ⇔ b'
_gen_b':c':mark':d':m':ok'3(+(x, 1)) ⇔ mark'(_gen_b':c':mark':d':m':ok'3(x))

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

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

Proved the following rewrite lemma:
f'(_gen_b':c':mark':d':m':ok'3(a), _gen_b':c':mark':d':m':ok'3(b), _gen_b':c':mark':d':m':ok'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Induction Base:
f'(_gen_b':c':mark':d':m':ok'3(a), _gen_b':c':mark':d':m':ok'3(b), _gen_b':c':mark':d':m':ok'3(+(1, 0)))

Induction Step:
f'(_gen_b':c':mark':d':m':ok'3(_a1018), _gen_b':c':mark':d':m':ok'3(_b1019), _gen_b':c':mark':d':m':ok'3(+(1, +(_$n6, 1)))) →_R^Ω(1)
mark'(f'(_gen_b':c':mark':d':m':ok'3(_a1018), _gen_b':c':mark':d':m':ok'3(_b1019), _gen_b':c':mark':d':m':ok'3(+(1, _$n6)))) →_IH
mark'(_*4)

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

Lemmas:
f'(_gen_b':c':mark':d':m':ok'3(a), _gen_b':c':mark':d':m':ok'3(b), _gen_b':c':mark':d':m':ok'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_b':c':mark':d':m':ok'3(0) ⇔ b'
_gen_b':c':mark':d':m':ok'3(+(x, 1)) ⇔ mark'(_gen_b':c':mark':d':m':ok'3(x))

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

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

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

Lemmas:
f'(_gen_b':c':mark':d':m':ok'3(a), _gen_b':c':mark':d':m':ok'3(b), _gen_b':c':mark':d':m':ok'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_b':c':mark':d':m':ok'3(0) ⇔ b'
_gen_b':c':mark':d':m':ok'3(+(x, 1)) ⇔ mark'(_gen_b':c':mark':d':m':ok'3(x))

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

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

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

Lemmas:
f'(_gen_b':c':mark':d':m':ok'3(a), _gen_b':c':mark':d':m':ok'3(b), _gen_b':c':mark':d':m':ok'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_b':c':mark':d':m':ok'3(0) ⇔ b'
_gen_b':c':mark':d':m':ok'3(+(x, 1)) ⇔ mark'(_gen_b':c':mark':d':m':ok'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_b':c':mark':d':m':ok'3(a), _gen_b':c':mark':d':m':ok'3(b), _gen_b':c':mark':d':m':ok'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)

Generator Equations:
_gen_b':c':mark':d':m':ok'3(0) ⇔ b'
_gen_b':c':mark':d':m':ok'3(+(x, 1)) ⇔ mark'(_gen_b':c':mark':d':m':ok'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
f'(_gen_b':c':mark':d':m':ok'3(a), _gen_b':c':mark':d':m':ok'3(b), _gen_b':c':mark':d':m':ok'3(+(1, _n5))) → _*4, rt ∈ Ω(_n5)