(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 CpxTRS 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), 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

(3) CdtPolyRedPairProof (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:

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
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_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
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_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(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(x1, x2)) = x1   
POL(Case(x1, x2, x3)) = [1] + x1 + x3   
POL(Concat(x1, x2)) = [5] + x1 + [2]x2   
POL(Cons_sum(x1, x2, x3)) = [1] + x3   
POL(Cons_usual(x1, x2, x3)) = x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = x1 + x3   
POL(Frozen(x1, x2, x3, x4)) = [3] + [2]x1 + [3]x3 + [3]x4   
POL(Id) = [4]   
POL(Left) = [3]   
POL(Right) = [2]   
POL(SUM_SUB(x1, x2)) = 0   
POL(Sum_constant(x1)) = 0   
POL(Sum_sub(x1, x2)) = [5]x1   
POL(Sum_term_var(x1)) = [3]   
POL(TERM_SUB(x1, x2)) = x1   
POL(Term_app(x1, x2)) = x1 + x2   
POL(Term_inl(x1)) = [1] + x1   
POL(Term_inr(x1)) = [1] + x1   
POL(Term_pair(x1, x2)) = [4] + x1 + x2   
POL(Term_sub(x1, x2)) = [2]x1 + [4]x2   
POL(Term_var(x1)) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c11(x1)) = x1   
POL(c12(x1, x2)) = x1 + x2   
POL(c15(x1)) = x1   
POL(c16(x1)) = x1   
POL(c17(x1, x2)) = x1 + x2   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c2(x1, x2)) = x1 + x2   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   

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

(5) CdtKnowledgeProof (EQUIVALENT 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))

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

(7) CdtPolyRedPairProof (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:

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
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_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
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_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(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(x1, x2)) = [4]x1   
POL(Case(x1, x2, x3)) = x1 + x2 + x3   
POL(Concat(x1, x2)) = [2] + x1 + [2]x2   
POL(Cons_sum(x1, x2, x3)) = [5] + x2 + x3   
POL(Cons_usual(x1, x2, x3)) = [1] + x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = [4]x1 + [4]x3   
POL(Frozen(x1, x2, x3, x4)) = [3] + [4]x1 + [2]x2 + [2]x3 + [3]x4   
POL(Id) = [3]   
POL(Left) = [3]   
POL(Right) = [3]   
POL(SUM_SUB(x1, x2)) = 0   
POL(Sum_constant(x1)) = [5]   
POL(Sum_sub(x1, x2)) = [3] + [2]x1 + x2   
POL(Sum_term_var(x1)) = [3] + x1   
POL(TERM_SUB(x1, x2)) = [4]x1   
POL(Term_app(x1, x2)) = x1 + x2   
POL(Term_inl(x1)) = [2] + x1   
POL(Term_inr(x1)) = [3] + x1   
POL(Term_pair(x1, x2)) = x1 + x2   
POL(Term_sub(x1, x2)) = x1 + x2   
POL(Term_var(x1)) = [3]   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c11(x1)) = x1   
POL(c12(x1, x2)) = x1 + x2   
POL(c15(x1)) = x1   
POL(c16(x1)) = x1   
POL(c17(x1, x2)) = x1 + x2   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c2(x1, x2)) = x1 + x2   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   

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

(9) CdtPolyRedPairProof (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:

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
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_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
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_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(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(x1, x2)) = [4]x1   
POL(Case(x1, x2, x3)) = [3] + x1 + x3   
POL(Concat(x1, x2)) = x1 + [4]x2   
POL(Cons_sum(x1, x2, x3)) = [4] + x3   
POL(Cons_usual(x1, x2, x3)) = [1] + x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = [4] + [4]x1 + [4]x3   
POL(Frozen(x1, x2, x3, x4)) = [2] + [3]x1 + [4]x2 + [2]x3 + [2]x4   
POL(Id) = [3]   
POL(Left) = [5]   
POL(Right) = [2]   
POL(SUM_SUB(x1, x2)) = [1]   
POL(Sum_constant(x1)) = 0   
POL(Sum_sub(x1, x2)) = [3]x1   
POL(Sum_term_var(x1)) = 0   
POL(TERM_SUB(x1, x2)) = [2] + [4]x1   
POL(Term_app(x1, x2)) = [2] + x1 + x2   
POL(Term_inl(x1)) = [3] + x1   
POL(Term_inr(x1)) = [3] + x1   
POL(Term_pair(x1, x2)) = [1] + x1 + x2   
POL(Term_sub(x1, x2)) = [4]x1 + [2]x2   
POL(Term_var(x1)) = [3]   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c11(x1)) = x1   
POL(c12(x1, x2)) = x1 + x2   
POL(c15(x1)) = x1   
POL(c16(x1)) = x1   
POL(c17(x1, x2)) = x1 + x2   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c2(x1, x2)) = x1 + x2   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   

(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_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

(11) CdtPolyRedPairProof (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:

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
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_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
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_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(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(x1, x2)) = [2] + [4]x1   
POL(Case(x1, x2, x3)) = [4] + x1 + x2 + x3   
POL(Concat(x1, x2)) = [2] + [2]x1 + [2]x2   
POL(Cons_sum(x1, x2, x3)) = [4] + x3   
POL(Cons_usual(x1, x2, x3)) = [5] + x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = [4] + [4]x1 + x2 + [4]x3   
POL(Frozen(x1, x2, x3, x4)) = [3] + [5]x1 + [2]x2 + [3]x3 + [3]x4   
POL(Id) = [3]   
POL(Left) = [2]   
POL(Right) = [4]   
POL(SUM_SUB(x1, x2)) = [4]   
POL(Sum_constant(x1)) = 0   
POL(Sum_sub(x1, x2)) = [5] + x1   
POL(Sum_term_var(x1)) = [4]   
POL(TERM_SUB(x1, x2)) = [4] + [4]x1   
POL(Term_app(x1, x2)) = [1] + x1 + x2   
POL(Term_inl(x1)) = [2] + x1   
POL(Term_inr(x1)) = [2] + x1   
POL(Term_pair(x1, x2)) = [2] + x1 + x2   
POL(Term_sub(x1, x2)) = [4] + x1 + [2]x2   
POL(Term_var(x1)) = [4]   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c11(x1)) = x1   
POL(c12(x1, x2)) = x1 + x2   
POL(c15(x1)) = x1   
POL(c16(x1)) = x1   
POL(c17(x1, x2)) = x1 + x2   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c2(x1, x2)) = x1 + x2   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   

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

(13) CdtPolyRedPairProof (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:

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
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_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3)
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2))
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3)
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_usual(z1, z2, z3)) → Sum_sub(z0, z3)
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(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(x1, x2)) = x1·x2 + [2]x12   
POL(Case(x1, x2, x3)) = [3] + x1 + x3   
POL(Concat(x1, x2)) = [2]x1 + x2 + x1·x2   
POL(Cons_sum(x1, x2, x3)) = [1] + x1 + x2 + x3   
POL(Cons_usual(x1, x2, x3)) = [1] + x1 + x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = [2]x1 + [2]x3 + x4 + x3·x4 + x1·x4 + [2]x12 + x1·x3 + [2]x32 + x22   
POL(Frozen(x1, x2, x3, x4)) = [3] + [2]x1 + [2]x3 + [3]x4 + x3·x4 + x2·x4 + x1·x4   
POL(Id) = 0   
POL(Left) = 0   
POL(Right) = 0   
POL(SUM_SUB(x1, x2)) = [1] + [2]x2   
POL(Sum_constant(x1)) = 0   
POL(Sum_sub(x1, x2)) = [1]   
POL(Sum_term_var(x1)) = 0   
POL(TERM_SUB(x1, x2)) = x1·x2 + [2]x12   
POL(Term_app(x1, x2)) = [1] + x1 + x2   
POL(Term_inl(x1)) = x1   
POL(Term_inr(x1)) = x1   
POL(Term_pair(x1, x2)) = [3] + x1 + x2   
POL(Term_sub(x1, x2)) = [2]x1 + x2 + x1·x2   
POL(Term_var(x1)) = [1]   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c11(x1)) = x1   
POL(c12(x1, x2)) = x1 + x2   
POL(c15(x1)) = x1   
POL(c16(x1)) = x1   
POL(c17(x1, x2)) = x1 + x2   
POL(c18(x1, x2)) = x1 + x2   
POL(c19(x1)) = x1   
POL(c2(x1, x2)) = x1 + x2   
POL(c3(x1)) = x1   
POL(c4(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   

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

(15) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(16) BOUNDS(O(1), O(1))