The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^2, INF).

(0) Obligation:

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: FULL

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative 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

S is empty.
Rewrite Strategy: FULL

(3) SlicingProof (LOWER BOUND(ID) transformation)

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

(4) Obligation:

Runtime Complexity Relative 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

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

(7) OrderProof (LOWER BOUND(ID) transformation)

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

(8) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(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

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

Induction Base:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(0)) →_R^Ω(1)
Sum_term_var

Induction Step:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(+(n8_0, 1))) →_R^Ω(1)
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) →_IH
Sum_term_var

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

(10) Complex Obligation (BEST)

(11) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

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

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

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)

Induction Base:
Concat(gen_Id:Cons_usual:Cons_sum6_0(0), gen_Id:Cons_usual:Cons_sum6_0(0)) →_R^Ω(1)
gen_Id:Cons_usual:Cons_sum6_0(0)

Induction Step:
Concat(gen_Id:Cons_usual:Cons_sum6_0(+(n370_0, 1)), gen_Id:Cons_usual:Cons_sum6_0(0)) →_R^Ω(1)
Cons_usual(Term_sub(Term_var, gen_Id:Cons_usual:Cons_sum6_0(0)), Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0))) →_R^Ω(1)
Cons_usual(Term_var, Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0))) →_IH
Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(c371_0))

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

(13) Complex Obligation (BEST)

(14) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

The following defined symbols remain to be analysed:
Term_sub

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

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Induction Base:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(0)) →_R^Ω(1)
Term_var

Induction Step:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(+(n183948_0, 1))) →_R^Ω(1)
Term_sub(Term_var, gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) →_IH
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0)

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

(16) Complex Obligation (BEST)

(17) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

The following defined symbols remain to be analysed:
Concat

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

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)

Induction Base:
Concat(gen_Id:Cons_usual:Cons_sum6_0(0), gen_Id:Cons_usual:Cons_sum6_0(b)) →_R^Ω(1)
gen_Id:Cons_usual:Cons_sum6_0(b)

Induction Step:
Concat(gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, 1)), gen_Id:Cons_usual:Cons_sum6_0(b)) →_R^Ω(1)
Cons_usual(Term_sub(Term_var, gen_Id:Cons_usual:Cons_sum6_0(b)), Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b))) →_L^{Ω(1 + b)}
Cons_usual(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b))) →_IH
Cons_usual(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(+(b, c390071_0)))

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

(19) Complex Obligation (BEST)

(20) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(21) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)

(22) BOUNDS(n^2, INF)

(23) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(24) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
Concat(gen_Id:Cons_usual:Cons_sum6_0(n390070_0), gen_Id:Cons_usual:Cons_sum6_0(b)) → gen_Id:Cons_usual:Cons_sum6_0(+(n390070_0, b)), rt ∈ Ω(1 + b·n390070₀ + n390070₀)

(25) BOUNDS(n^2, INF)

(26) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), gen_Id:Cons_usual:Cons_sum6_0(n183948_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0), rt ∈ Ω(1 + n183948₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

(28) BOUNDS(n^1, INF)

(29) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)
Concat(gen_Id:Cons_usual:Cons_sum6_0(n370_0), gen_Id:Cons_usual:Cons_sum6_0(0)) → gen_Id:Cons_usual:Cons_sum6_0(n370_0), rt ∈ Ω(1 + n370₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

(31) BOUNDS(n^1, INF)

(32) Obligation:

TRS:
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_var1_0 :: Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
hole_Id:Cons_usual:Cons_sum2_0 :: Id:Cons_usual:Cons_sum
hole_Sum_constant:Sum_term_var3_0 :: Sum_constant:Sum_term_var
hole_Left:Right4_0 :: Left:Right
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum6_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(0) ⇔ Term_var
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(+(x, 1)) ⇔ Case(Term_var, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var5_0(x))
gen_Id:Cons_usual:Cons_sum6_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum6_0(+(x, 1)) ⇔ Cons_usual(Term_var, gen_Id:Cons_usual:Cons_sum6_0(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(gen_Id:Cons_usual:Cons_sum6_0(n8_0)) → Sum_term_var, rt ∈ Ω(1 + n8₀)

(34) BOUNDS(n^1, INF)