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

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

a__a' → a__c'
a__b' → a__c'
a__c' → e'
a__k' → l'
a__d' → m'
a__a' → a__d'
a__b' → a__d'
a__c' → l'
a__k' → m'
a__A' → a__h'(a__f'(a__a'), a__f'(a__b'))
a__h'(X, X) → a__g'(mark'(X), mark'(X), a__f'(a__k'))
a__g'(d', X, X) → a__A'
a__f'(X) → a__z'(mark'(X), X)
a__z'(e', X) → mark'(X)
mark'(A') → a__A'
mark'(a') → a__a'
mark'(b') → a__b'
mark'(c') → a__c'
mark'(d') → a__d'
mark'(k') → a__k'
mark'(z'(X1, X2)) → a__z'(mark'(X1), X2)
mark'(f'(X)) → a__f'(mark'(X))
mark'(h'(X1, X2)) → a__h'(mark'(X1), mark'(X2))
mark'(g'(X1, X2, X3)) → a__g'(mark'(X1), mark'(X2), mark'(X3))
mark'(e') → e'
mark'(l') → l'
mark'(m') → m'
a__A' → A'
a__a' → a'
a__b' → b'
a__c' → c'
a__d' → d'
a__k' → k'
a__z'(X1, X2) → z'(X1, X2)
a__f'(X) → f'(X)
a__h'(X1, X2) → h'(X1, X2)
a__g'(X1, X2, X3) → g'(X1, X2, X3)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__a' → a__c'
a__b' → a__c'
a__c' → e'
a__k' → l'
a__d' → m'
a__a' → a__d'
a__b' → a__d'
a__c' → l'
a__k' → m'
a__A' → a__h'(a__f'(a__a'), a__f'(a__b'))
a__h'(X, X) → a__g'(mark'(X), mark'(X), a__f'(a__k'))
a__g'(d', X, X) → a__A'
a__f'(X) → a__z'(mark'(X), X)
a__z'(e', X) → mark'(X)
mark'(A') → a__A'
mark'(a') → a__a'
mark'(b') → a__b'
mark'(c') → a__c'
mark'(d') → a__d'
mark'(k') → a__k'
mark'(z'(X1, X2)) → a__z'(mark'(X1), X2)
mark'(f'(X)) → a__f'(mark'(X))
mark'(h'(X1, X2)) → a__h'(mark'(X1), mark'(X2))
mark'(g'(X1, X2, X3)) → a__g'(mark'(X1), mark'(X2), mark'(X3))
mark'(e') → e'
mark'(l') → l'
mark'(m') → m'
a__A' → A'
a__a' → a'
a__b' → b'
a__c' → c'
a__d' → d'
a__k' → k'
a__z'(X1, X2) → z'(X1, X2)
a__f'(X) → f'(X)
a__h'(X1, X2) → h'(X1, X2)
a__g'(X1, X2, X3) → g'(X1, X2, X3)

Types:
a__a' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
a__c' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
a__b' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
e' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
a__k' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
l' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
a__d' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
m' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
a__A' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
a__h' :: e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g'
a__f' :: e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g'
a__g' :: e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g'
mark' :: e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g'
d' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
a__z' :: e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g'
A' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
a' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
b' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
c' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
k' :: e':l':m':d':A':a':b':c':k':z':f':h':g'
z' :: e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g'
f' :: e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g'
h' :: e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g'
g' :: e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g' → e':l':m':d':A':a':b':c':k':z':f':h':g'
_hole_e':l':m':d':A':a':b':c':k':z':f':h':g'1 :: e':l':m':d':A':a':b':c':k':z':f':h':g'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2 :: Nat → e':l':m':d':A':a':b':c':k':z':f':h':g'

Heuristically decided to analyse the following defined symbols:
a__A', a__h', a__f', a__g', mark', a__z'

They will be analysed ascendingly in the following order:
a__A' = a__h'
a__A' = a__f'
a__A' = a__g'
a__A' = mark'
a__A' = a__z'
a__h' = a__f'
a__h' = a__g'
a__h' = mark'
a__h' = a__z'
a__f' = a__g'
a__f' = mark'
a__f' = a__z'
a__g' = mark'
a__g' = a__z'
mark' = a__z'

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__h', a__A', a__f', a__g', mark', a__z'

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

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__g', a__A', a__f', mark', a__z'

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

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__A', a__f', mark', a__z'

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

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__f', mark', a__z'

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

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__z', mark'

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

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
mark'

Proved the following rewrite lemma:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(_n25888595)) → _gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0), rt ∈ Ω(1 + _n25888595)

Induction Base:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0)) →_R^Ω(1)
e'

Induction Step:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(_$n25888596, 1))) →_R^Ω(1)
a__z'(mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(_$n25888596)), e') →_IH
a__z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0), e') →_R^Ω(1)
mark'(e') →_R^Ω(1)
e'

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

Lemmas:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(_n25888595)) → _gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0), rt ∈ Ω(1 + _n25888595)

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__h', a__A', a__f', a__g', a__z'

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

Lemmas:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(_n25888595)) → _gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0), rt ∈ Ω(1 + _n25888595)

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__g', a__A', a__f', a__z'

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

Lemmas:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(_n25888595)) → _gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0), rt ∈ Ω(1 + _n25888595)

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__A', a__f', a__z'

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

Lemmas:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(_n25888595)) → _gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0), rt ∈ Ω(1 + _n25888595)

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__f', a__z'

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

Lemmas:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(_n25888595)) → _gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0), rt ∈ Ω(1 + _n25888595)

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

The following defined symbols remain to be analysed:
a__z'

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

Lemmas:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(_n25888595)) → _gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0), rt ∈ Ω(1 + _n25888595)

Generator Equations:
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0) ⇔ e'
_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(+(x, 1)) ⇔ z'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(x), e')

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
mark'(_gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(_n25888595)) → _gen_e':l':m':d':A':a':b':c':k':z':f':h':g'2(0), rt ∈ Ω(1 + _n25888595)