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) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
Term_sub(Case(m, xi, n), Id) →⁺ Case(Term_sub(m, Id), xi, Term_sub(n, Id))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [m / Case(m, xi, n)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) 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

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

Infered types.

(6) Obligation:

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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_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, 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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_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(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

Induction Base:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(0)) →_R^Ω(1)
Sum_term_var(hole_a3_0)

Induction Step:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(+(n12_0, 1))) →_R^Ω(1)
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) →_IH
Sum_term_var(hole_a3_0)

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, 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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_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_sum10_0(n635_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n635_0), rt ∈ Ω(1 + n635₀)

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

Induction Step:
Concat(gen_Id:Cons_usual:Cons_sum10_0(+(n635_0, 1)), gen_Id:Cons_usual:Cons_sum10_0(0)) →_R^Ω(1)
Cons_usual(hole_c7_0, Term_sub(Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(0)), Concat(gen_Id:Cons_usual:Cons_sum10_0(n635_0), gen_Id:Cons_usual:Cons_sum10_0(0))) →_R^Ω(1)
Cons_usual(hole_c7_0, Term_var(hole_b6_0), Concat(gen_Id:Cons_usual:Cons_sum10_0(n635_0), gen_Id:Cons_usual:Cons_sum10_0(0))) →_IH
Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(c636_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, 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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n635_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n635_0), rt ∈ Ω(1 + n635₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_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_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250880_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250880₀)

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

Induction Step:
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(+(n250880_0, 1))) →_R^Ω(1)
Term_sub(Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(n250880_0)) →_IH
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_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, 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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n635_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n635_0), rt ∈ Ω(1 + n635₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250880_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250880₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_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_sum10_0(n531920_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n531920_0, b)), rt ∈ Ω(1 + b·n531920₀ + n531920₀)

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

Induction Step:
Concat(gen_Id:Cons_usual:Cons_sum10_0(+(n531920_0, 1)), gen_Id:Cons_usual:Cons_sum10_0(b)) →_R^Ω(1)
Cons_usual(hole_c7_0, Term_sub(Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(b)), Concat(gen_Id:Cons_usual:Cons_sum10_0(n531920_0), gen_Id:Cons_usual:Cons_sum10_0(b))) →_L^{Ω(1 + b)}
Cons_usual(hole_c7_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), Concat(gen_Id:Cons_usual:Cons_sum10_0(n531920_0), gen_Id:Cons_usual:Cons_sum10_0(b))) →_IH
Cons_usual(hole_c7_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(+(b, c531921_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, 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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n531920_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n531920_0, b)), rt ∈ Ω(1 + b·n531920₀ + n531920₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250880_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250880₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_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_sum10_0(n531920_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n531920_0, b)), rt ∈ Ω(1 + b·n531920₀ + n531920₀)

(22) BOUNDS(n^2, INF)

(23) Obligation:

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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n531920_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n531920_0, b)), rt ∈ Ω(1 + b·n531920₀ + n531920₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250880_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250880₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_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_sum10_0(n531920_0), gen_Id:Cons_usual:Cons_sum10_0(b)) → gen_Id:Cons_usual:Cons_sum10_0(+(n531920_0, b)), rt ∈ Ω(1 + b·n531920₀ + n531920₀)

(25) BOUNDS(n^2, INF)

(26) Obligation:

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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n635_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n635_0), rt ∈ Ω(1 + n635₀)
Term_sub(gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), gen_Id:Cons_usual:Cons_sum10_0(n250880_0)) → gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0), rt ∈ Ω(1 + n250880₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

(28) BOUNDS(n^1, INF)

(29) Obligation:

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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)
Concat(gen_Id:Cons_usual:Cons_sum10_0(n635_0), gen_Id:Cons_usual:Cons_sum10_0(0)) → gen_Id:Cons_usual:Cons_sum10_0(n635_0), rt ∈ Ω(1 + n635₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

(31) BOUNDS(n^1, INF)

(32) Obligation:

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

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 → a → 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 :: a → 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 :: a → 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 :: b → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
Id :: Id:Cons_usual:Cons_sum
Cons_usual :: c → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var → Id:Cons_usual:Cons_sum → Id:Cons_usual:Cons_sum
Cons_sum :: d → 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_a3_0 :: a
hole_Sum_constant:Sum_term_var4_0 :: Sum_constant:Sum_term_var
hole_Left:Right5_0 :: Left:Right
hole_b6_0 :: b
hole_c7_0 :: c
hole_d8_0 :: d
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0 :: Nat → Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var
gen_Id:Cons_usual:Cons_sum10_0 :: Nat → Id:Cons_usual:Cons_sum

Lemmas:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

Generator Equations:
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(0) ⇔ Term_var(hole_b6_0)
gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(+(x, 1)) ⇔ Case(Term_var(hole_b6_0), hole_a3_0, gen_Case:Term_app:Term_pair:Term_inl:Term_inr:Term_var9_0(x))
gen_Id:Cons_usual:Cons_sum10_0(0) ⇔ Id
gen_Id:Cons_usual:Cons_sum10_0(+(x, 1)) ⇔ Cons_usual(hole_c7_0, Term_var(hole_b6_0), gen_Id:Cons_usual:Cons_sum10_0(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
Sum_sub(hole_a3_0, gen_Id:Cons_usual:Cons_sum10_0(n12_0)) → Sum_term_var(hole_a3_0), rt ∈ Ω(1 + n12₀)

(34) BOUNDS(n^1, INF)