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

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

Term_sub'(Case'(m, xi, n), s) → Frozen'(m, Sum_sub'(xi, s), n, s)
Frozen'(m, Sum_constant'(Left'), n, s) → Term_sub'(m, s)
Frozen'(m, Sum_constant'(Right'), n, s) → Term_sub'(n, s)
Frozen'(m, Sum_term_var'(xi), n, s) → Case'(Term_sub'(m, s), xi, Term_sub'(n, s))
Term_sub'(Term_app'(m, n), s) → Term_app'(Term_sub'(m, s), Term_sub'(n, s))
Term_sub'(Term_pair'(m, n), s) → Term_pair'(Term_sub'(m, s), Term_sub'(n, s))
Term_sub'(Term_inl'(m), s) → Term_inl'(Term_sub'(m, s))
Term_sub'(Term_inr'(m), s) → Term_inr'(Term_sub'(m, s))
Term_sub'(Term_var'(x), Id') → Term_var'(x)
Term_sub'(Term_var'(x), Cons_usual'(y, m, s)) → m
Term_sub'(Term_var'(x), Cons_usual'(y, m, s)) → Term_sub'(Term_var'(x), s)
Term_sub'(Term_var'(x), Cons_sum'(xi, k, s)) → Term_sub'(Term_var'(x), s)
Term_sub'(Term_sub'(m, s), t) → Term_sub'(m, Concat'(s, t))
Sum_sub'(xi, Id') → Sum_term_var'(xi)
Sum_sub'(xi, Cons_sum'(psi, k, s)) → Sum_constant'(k)
Sum_sub'(xi, Cons_sum'(psi, k, s)) → Sum_sub'(xi, s)
Sum_sub'(xi, Cons_usual'(y, m, s)) → Sum_sub'(xi, s)
Concat'(Concat'(s, t), u) → Concat'(s, Concat'(t, u))
Concat'(Cons_usual'(x, m, s), t) → Cons_usual'(x, Term_sub'(m, t), Concat'(s, t))
Concat'(Cons_sum'(xi, k, s), t) → Cons_sum'(xi, k, Concat'(s, t))
Concat'(Id', s) → s

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Case'/1
Sum_sub'/0
Sum_term_var'/0
Term_var'/0
Cons_usual'/0
Cons_sum'/0

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

Term_sub'(Case'(m, n), s) → Frozen'(m, Sum_sub'(s), n, s)
Frozen'(m, Sum_constant'(Left'), n, s) → Term_sub'(m, s)
Frozen'(m, Sum_constant'(Right'), n, s) → Term_sub'(n, s)
Frozen'(m, Sum_term_var', n, s) → Case'(Term_sub'(m, s), Term_sub'(n, s))
Term_sub'(Term_app'(m, n), s) → Term_app'(Term_sub'(m, s), Term_sub'(n, s))
Term_sub'(Term_pair'(m, n), s) → Term_pair'(Term_sub'(m, s), Term_sub'(n, s))
Term_sub'(Term_inl'(m), s) → Term_inl'(Term_sub'(m, s))
Term_sub'(Term_inr'(m), s) → Term_inr'(Term_sub'(m, s))
Term_sub'(Term_var', Id') → Term_var'
Term_sub'(Term_var', Cons_usual'(m, s)) → m
Term_sub'(Term_var', Cons_usual'(m, s)) → Term_sub'(Term_var', s)
Term_sub'(Term_var', Cons_sum'(k, s)) → Term_sub'(Term_var', s)
Term_sub'(Term_sub'(m, s), t) → Term_sub'(m, Concat'(s, t))
Sum_sub'(Id') → Sum_term_var'
Sum_sub'(Cons_sum'(k, s)) → Sum_constant'(k)
Sum_sub'(Cons_sum'(k, s)) → Sum_sub'(s)
Sum_sub'(Cons_usual'(m, s)) → Sum_sub'(s)
Concat'(Concat'(s, t), u) → Concat'(s, Concat'(t, u))
Concat'(Cons_usual'(m, s), t) → Cons_usual'(Term_sub'(m, t), Concat'(s, t))
Concat'(Cons_sum'(k, s), t) → Cons_sum'(k, Concat'(s, t))
Concat'(Id', s) → s

Rewrite Strategy: INNERMOST

Infered types.

Rules:
Term_sub'(Case'(m, n), s) → Frozen'(m, Sum_sub'(s), n, s)
Frozen'(m, Sum_constant'(Left'), n, s) → Term_sub'(m, s)
Frozen'(m, Sum_constant'(Right'), n, s) → Term_sub'(n, s)
Frozen'(m, Sum_term_var', n, s) → Case'(Term_sub'(m, s), Term_sub'(n, s))
Term_sub'(Term_app'(m, n), s) → Term_app'(Term_sub'(m, s), Term_sub'(n, s))
Term_sub'(Term_pair'(m, n), s) → Term_pair'(Term_sub'(m, s), Term_sub'(n, s))
Term_sub'(Term_inl'(m), s) → Term_inl'(Term_sub'(m, s))
Term_sub'(Term_inr'(m), s) → Term_inr'(Term_sub'(m, s))
Term_sub'(Term_var', Id') → Term_var'
Term_sub'(Term_var', Cons_usual'(m, s)) → m
Term_sub'(Term_var', Cons_usual'(m, s)) → Term_sub'(Term_var', s)
Term_sub'(Term_var', Cons_sum'(k, s)) → Term_sub'(Term_var', s)
Term_sub'(Term_sub'(m, s), t) → Term_sub'(m, Concat'(s, t))
Sum_sub'(Id') → Sum_term_var'
Sum_sub'(Cons_sum'(k, s)) → Sum_constant'(k)
Sum_sub'(Cons_sum'(k, s)) → Sum_sub'(s)
Sum_sub'(Cons_usual'(m, s)) → Sum_sub'(s)
Concat'(Concat'(s, t), u) → Concat'(s, Concat'(t, u))
Concat'(Cons_usual'(m, s), t) → Cons_usual'(Term_sub'(m, t), Concat'(s, t))
Concat'(Cons_sum'(k, s), t) → Cons_sum'(k, Concat'(s, t))
Concat'(Id', s) → s

Types:
Term_sub' :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Id':Cons_usual':Cons_sum' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
Case' :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
Frozen' :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Sum_constant':Sum_term_var' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Id':Cons_usual':Cons_sum' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
Sum_sub' :: Id':Cons_usual':Cons_sum' → Sum_constant':Sum_term_var'
Sum_constant' :: Left':Right' → Sum_constant':Sum_term_var'
Left' :: Left':Right'
Right' :: Left':Right'
Sum_term_var' :: Sum_constant':Sum_term_var'
Term_app' :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
Term_pair' :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
Term_inl' :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
Term_inr' :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
Term_var' :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
Id' :: Id':Cons_usual':Cons_sum'
Cons_usual' :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var' → Id':Cons_usual':Cons_sum' → Id':Cons_usual':Cons_sum'
Cons_sum' :: Left':Right' → Id':Cons_usual':Cons_sum' → Id':Cons_usual':Cons_sum'
Concat' :: Id':Cons_usual':Cons_sum' → Id':Cons_usual':Cons_sum' → Id':Cons_usual':Cons_sum'
_hole_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'1 :: Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
_hole_Id':Cons_usual':Cons_sum'2 :: Id':Cons_usual':Cons_sum'
_hole_Sum_constant':Sum_term_var'3 :: Sum_constant':Sum_term_var'
_hole_Left':Right'4 :: Left':Right'
_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5 :: Nat → Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'
_gen_Id':Cons_usual':Cons_sum'6 :: Nat → Id':Cons_usual':Cons_sum'

Heuristically decided to analyse the following defined symbols:
Term_sub', Sum_sub', Concat'

They will be analysed ascendingly in the following order:
Sum_sub' < Term_sub'
Term_sub' = Concat'

Generator Equations:
_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0) ⇔ Term_var'
_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(+(x, 1)) ⇔ Case'(Term_var', _gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(x))
_gen_Id':Cons_usual':Cons_sum'6(0) ⇔ Id'
_gen_Id':Cons_usual':Cons_sum'6(+(x, 1)) ⇔ Cons_usual'(Term_var', _gen_Id':Cons_usual':Cons_sum'6(x))

The following defined symbols remain to be analysed:
Sum_sub', Term_sub', Concat'

They will be analysed ascendingly in the following order:
Sum_sub' < Term_sub'
Term_sub' = Concat'

Proved the following rewrite lemma:
Sum_sub'(_gen_Id':Cons_usual':Cons_sum'6(_n8)) → Sum_term_var', rt ∈ Ω(1 + _n8)

Induction Base:
Sum_sub'(_gen_Id':Cons_usual':Cons_sum'6(0)) →_R^Ω(1)
Sum_term_var'

Induction Step:
Sum_sub'(_gen_Id':Cons_usual':Cons_sum'6(+(_$n9, 1))) →_R^Ω(1)
Sum_sub'(_gen_Id':Cons_usual':Cons_sum'6(_$n9)) →_IH
Sum_term_var'

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

Lemmas:
Sum_sub'(_gen_Id':Cons_usual':Cons_sum'6(_n8)) → Sum_term_var', rt ∈ Ω(1 + _n8)

The following defined symbols remain to be analysed:
Concat', Term_sub'

They will be analysed ascendingly in the following order:
Term_sub' = Concat'

Proved the following rewrite lemma:
Concat'(_gen_Id':Cons_usual':Cons_sum'6(_n838), _gen_Id':Cons_usual':Cons_sum'6(0)) → _gen_Id':Cons_usual':Cons_sum'6(_n838), rt ∈ Ω(1 + _n838)

Induction Base:
Concat'(_gen_Id':Cons_usual':Cons_sum'6(0), _gen_Id':Cons_usual':Cons_sum'6(0)) →_R^Ω(1)
_gen_Id':Cons_usual':Cons_sum'6(0)

Induction Step:
Concat'(_gen_Id':Cons_usual':Cons_sum'6(+(_$n839, 1)), _gen_Id':Cons_usual':Cons_sum'6(0)) →_R^Ω(1)
Cons_usual'(Term_sub'(Term_var', _gen_Id':Cons_usual':Cons_sum'6(0)), Concat'(_gen_Id':Cons_usual':Cons_sum'6(_$n839), _gen_Id':Cons_usual':Cons_sum'6(0))) →_R^Ω(1)
Cons_usual'(Term_var', Concat'(_gen_Id':Cons_usual':Cons_sum'6(_$n839), _gen_Id':Cons_usual':Cons_sum'6(0))) →_IH
Cons_usual'(Term_var', _gen_Id':Cons_usual':Cons_sum'6(_$n839))

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

The following defined symbols remain to be analysed:
Term_sub'

They will be analysed ascendingly in the following order:
Term_sub' = Concat'

Proved the following rewrite lemma:
Term_sub'(_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), _gen_Id':Cons_usual':Cons_sum'6(_n109609)) → _gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), rt ∈ Ω(1 + _n109609)

Induction Base:
Term_sub'(_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), _gen_Id':Cons_usual':Cons_sum'6(0)) →_R^Ω(1)
Term_var'

Induction Step:
Term_sub'(_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), _gen_Id':Cons_usual':Cons_sum'6(+(_$n109610, 1))) →_R^Ω(1)
Term_sub'(Term_var', _gen_Id':Cons_usual':Cons_sum'6(_$n109610)) →_IH
_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0)

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

Lemmas:
Sum_sub'(_gen_Id':Cons_usual':Cons_sum'6(_n8)) → Sum_term_var', rt ∈ Ω(1 + _n8)
Concat'(_gen_Id':Cons_usual':Cons_sum'6(_n838), _gen_Id':Cons_usual':Cons_sum'6(0)) → _gen_Id':Cons_usual':Cons_sum'6(_n838), rt ∈ Ω(1 + _n838)
Term_sub'(_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), _gen_Id':Cons_usual':Cons_sum'6(_n109609)) → _gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), rt ∈ Ω(1 + _n109609)

The following defined symbols remain to be analysed:
Concat'

They will be analysed ascendingly in the following order:
Term_sub' = Concat'

Proved the following rewrite lemma:
Concat'(_gen_Id':Cons_usual':Cons_sum'6(_n164633), _gen_Id':Cons_usual':Cons_sum'6(b)) → _gen_Id':Cons_usual':Cons_sum'6(+(_n164633, b)), rt ∈ Ω(1 + _b165038·_n164633 + _n164633)

Induction Base:
Concat'(_gen_Id':Cons_usual':Cons_sum'6(0), _gen_Id':Cons_usual':Cons_sum'6(b)) →_R^Ω(1)
_gen_Id':Cons_usual':Cons_sum'6(b)

Induction Step:
Concat'(_gen_Id':Cons_usual':Cons_sum'6(+(_$n164634, 1)), _gen_Id':Cons_usual':Cons_sum'6(_b165038)) →_R^Ω(1)
Cons_usual'(Term_sub'(Term_var', _gen_Id':Cons_usual':Cons_sum'6(_b165038)), Concat'(_gen_Id':Cons_usual':Cons_sum'6(_$n164634), _gen_Id':Cons_usual':Cons_sum'6(_b165038))) →_L^{Ω(1 + _b165038)}
Cons_usual'(_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), Concat'(_gen_Id':Cons_usual':Cons_sum'6(_$n164634), _gen_Id':Cons_usual':Cons_sum'6(_b165038))) →_IH
Cons_usual'(_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), _gen_Id':Cons_usual':Cons_sum'6(+(_$n164634, _b165038)))

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

Lemmas:
Sum_sub'(_gen_Id':Cons_usual':Cons_sum'6(_n8)) → Sum_term_var', rt ∈ Ω(1 + _n8)
Concat'(_gen_Id':Cons_usual':Cons_sum'6(_n164633), _gen_Id':Cons_usual':Cons_sum'6(b)) → _gen_Id':Cons_usual':Cons_sum'6(+(_n164633, b)), rt ∈ Ω(1 + _b165038·_n164633 + _n164633)
Term_sub'(_gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), _gen_Id':Cons_usual':Cons_sum'6(_n109609)) → _gen_Case':Term_app':Term_pair':Term_inl':Term_inr':Term_var'5(0), rt ∈ Ω(1 + _n109609)

No more defined symbols left to analyse.

The lowerbound Ω(n²) was proven with the following lemma:
Concat'(_gen_Id':Cons_usual':Cons_sum'6(_n164633), _gen_Id':Cons_usual':Cons_sum'6(b)) → _gen_Id':Cons_usual':Cons_sum'6(+(_n164633, b)), rt ∈ Ω(1 + _b165038·_n164633 + _n164633)