Runtime Complexity (innermost) proof of /tmp/tmpK2uMfL/lse.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CdtProblem

↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CdtProblem

↳5 CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))), 750 ms)

↳6 CdtProblem

↳7 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CdtProblem

↳9 CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))), 455 ms)

↳10 CdtProblem

↳11 CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))), 675 ms)

↳12 CdtProblem

↳13 CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))), 716 ms)

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))), 1619 ms)

↳16 CdtProblem

↳17 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳18 BOUNDS(O(1), O(1))

(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: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Id) → c5
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c6
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Id) → c13
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c14
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
CONCAT(Id, z0) → c20

S tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Id) → c5
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c6
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Id) → c13
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c14
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
CONCAT(Id, z0) → c20

K tuples:none
Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing nodes:

SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c14
TERM_SUB(Term_var(z0), Id) → c5
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c6
SUM_SUB(z0, Id) → c13
CONCAT(Id, z0) → c20

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

K tuples:none
Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(5) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

We considered the (Usable) Rules:none
And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = x₁
POL(Case(x₁, x₂, x₃)) = [1] + x₁ + x₃
POL(Concat(x₁, x₂)) = [5] + x₁ + [2]x₂
POL(Cons_sum(x₁, x₂, x₃)) = [1] + x₃
POL(Cons_usual(x₁, x₂, x₃)) = x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₃
POL(Frozen(x₁, x₂, x₃, x₄)) = [3] + [2]x₁ + [3]x₃ + [3]x₄
POL(Id) = [4]
POL(Left) = [3]
POL(Right) = [2]
POL(SUM_SUB(x₁, x₂)) = 0
POL(Sum_constant(x₁)) = 0
POL(Sum_sub(x₁, x₂)) = [5]x₁
POL(Sum_term_var(x₁)) = [3]
POL(TERM_SUB(x₁, x₂)) = x₁
POL(Term_app(x₁, x₂)) = x₁ + x₂
POL(Term_inl(x₁)) = [1] + x₁
POL(Term_inr(x₁)) = [1] + x₁
POL(Term_pair(x₁, x₂)) = [4] + x₁ + x₂
POL(Term_sub(x₁, x₂)) = [2]x₁ + [4]x₂
POL(Term_var(x₁)) = 0
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(7) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(9) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

We considered the (Usable) Rules:none
And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [4]x₁
POL(Case(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(Concat(x₁, x₂)) = [2] + x₁ + [2]x₂
POL(Cons_sum(x₁, x₂, x₃)) = [5] + x₂ + x₃
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = [4]x₁ + [4]x₃
POL(Frozen(x₁, x₂, x₃, x₄)) = [3] + [4]x₁ + [2]x₂ + [2]x₃ + [3]x₄
POL(Id) = [3]
POL(Left) = [3]
POL(Right) = [3]
POL(SUM_SUB(x₁, x₂)) = 0
POL(Sum_constant(x₁)) = [5]
POL(Sum_sub(x₁, x₂)) = [3] + [2]x₁ + x₂
POL(Sum_term_var(x₁)) = [3] + x₁
POL(TERM_SUB(x₁, x₂)) = [4]x₁
POL(Term_app(x₁, x₂)) = x₁ + x₂
POL(Term_inl(x₁)) = [2] + x₁
POL(Term_inr(x₁)) = [3] + x₁
POL(Term_pair(x₁, x₂)) = x₁ + x₂
POL(Term_sub(x₁, x₂)) = x₁ + x₂
POL(Term_var(x₁)) = [3]
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(11) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))

We considered the (Usable) Rules:none
And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [4]x₁
POL(Case(x₁, x₂, x₃)) = [3] + x₁ + x₃
POL(Concat(x₁, x₂)) = x₁ + [4]x₂
POL(Cons_sum(x₁, x₂, x₃)) = [4] + x₃
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = [4] + [4]x₁ + [4]x₃
POL(Frozen(x₁, x₂, x₃, x₄)) = [2] + [3]x₁ + [4]x₂ + [2]x₃ + [2]x₄
POL(Id) = [3]
POL(Left) = [5]
POL(Right) = [2]
POL(SUM_SUB(x₁, x₂)) = [1]
POL(Sum_constant(x₁)) = 0
POL(Sum_sub(x₁, x₂)) = [3]x₁
POL(Sum_term_var(x₁)) = 0
POL(TERM_SUB(x₁, x₂)) = [2] + [4]x₁
POL(Term_app(x₁, x₂)) = [2] + x₁ + x₂
POL(Term_inl(x₁)) = [3] + x₁
POL(Term_inr(x₁)) = [3] + x₁
POL(Term_pair(x₁, x₂)) = [1] + x₁ + x₂
POL(Term_sub(x₁, x₂)) = [4]x₁ + [2]x₂
POL(Term_var(x₁)) = [3]
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(13) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))

We considered the (Usable) Rules:

Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Id) → Sum_term_var(z0)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = [2] + [4]x₁
POL(Case(x₁, x₂, x₃)) = [4] + x₁ + x₂ + x₃
POL(Concat(x₁, x₂)) = [2] + [2]x₁ + [2]x₂
POL(Cons_sum(x₁, x₂, x₃)) = [4] + x₃
POL(Cons_usual(x₁, x₂, x₃)) = [5] + x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = [4] + [4]x₁ + x₂ + [4]x₃
POL(Frozen(x₁, x₂, x₃, x₄)) = [3] + [5]x₁ + [2]x₂ + [3]x₃ + [3]x₄
POL(Id) = [3]
POL(Left) = [2]
POL(Right) = [4]
POL(SUM_SUB(x₁, x₂)) = [4]
POL(Sum_constant(x₁)) = 0
POL(Sum_sub(x₁, x₂)) = [5] + x₁
POL(Sum_term_var(x₁)) = [4]
POL(TERM_SUB(x₁, x₂)) = [4] + [4]x₁
POL(Term_app(x₁, x₂)) = [1] + x₁ + x₂
POL(Term_inl(x₁)) = [2] + x₁
POL(Term_inr(x₁)) = [2] + x₁
POL(Term_pair(x₁, x₂)) = [2] + x₁ + x₂
POL(Term_sub(x₁, x₂)) = [4] + x₁ + [2]x₂
POL(Term_var(x₁)) = [4]
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:

TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(15) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

We considered the (Usable) Rules:

Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Id, z0) → z0
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Sum_sub(z0, Id) → Sum_term_var(z0)
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)

And the Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x₁, x₂)) = x₁·x₂ + [2]x₁²
POL(Case(x₁, x₂, x₃)) = [3] + x₁ + x₃
POL(Concat(x₁, x₂)) = [2]x₁ + x₂ + x₁·x₂
POL(Cons_sum(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = [2]x₁ + [2]x₃ + x₄ + x₃·x₄ + x₁·x₄ + [2]x₁² + x₁·x₃ + [2]x₃² + x₂²
POL(Frozen(x₁, x₂, x₃, x₄)) = [3] + [2]x₁ + [2]x₃ + [3]x₄ + x₃·x₄ + x₂·x₄ + x₁·x₄
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(SUM_SUB(x₁, x₂)) = [1] + [2]x₂
POL(Sum_constant(x₁)) = 0
POL(Sum_sub(x₁, x₂)) = [1]
POL(Sum_term_var(x₁)) = 0
POL(TERM_SUB(x₁, x₂)) = x₁·x₂ + [2]x₁²
POL(Term_app(x₁, x₂)) = [1] + x₁ + x₂
POL(Term_inl(x₁)) = x₁
POL(Term_inr(x₁)) = x₁
POL(Term_pair(x₁, x₂)) = [3] + x₁ + x₂
POL(Term_sub(x₁, x₂)) = [2]x₁ + x₂ + x₁·x₂
POL(Term_var(x₁)) = [1]
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁, x₂)) = x₁ + x₂
POL(c10(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c15(x₁)) = x₁
POL(c16(x₁)) = x₁
POL(c17(x₁, x₂)) = x₁ + x₂
POL(c18(x₁, x₂)) = x₁ + x₂
POL(c19(x₁)) = x₁
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(c9(x₁, x₂)) = x₁ + x₂

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2))
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1))
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1))
Term_sub(Term_var(z0), Id) → Term_var(z0)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2)
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2)
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3))
Sum_sub(z0, Id) → Sum_term_var(z0)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2))
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3))
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3))
Concat(Id, z0) → z0

Tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))

S tuples:none
K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3))
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))

Defined Rule Symbols:

Term_sub, Frozen, Sum_sub, Concat

Defined Pair Symbols:

TERM_SUB, FROZEN, SUM_SUB, CONCAT

Compound Symbols:

c, c1, c2, c3, c4, c7, c8, c9, c10, c11, c12, c15, c16, c17, c18, c19

(17) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

(6) Obligation:

(7) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

(10) Obligation:

(11) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

(12) Obligation:

(13) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

(14) Obligation:

(15) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^2))) transformation)

(16) Obligation:

(17) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

(18) BOUNDS(O(1), O(1))