YES(O(1), O(n^2)) 34.87/9.44 YES(O(1), O(n^2)) 34.87/9.48 34.87/9.48 34.87/9.48 34.87/9.48 34.87/9.48 34.87/9.48 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 34.87/9.48 34.87/9.48 34.87/9.48
34.87/9.48 34.87/9.48 34.87/9.48
34.87/9.48
34.87/9.48

(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) 34.87/9.48
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s) 34.87/9.48
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s) 34.87/9.48
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s)) 34.87/9.48
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s)) 34.87/9.48
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s)) 34.87/9.48
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s)) 34.87/9.48
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s)) 34.87/9.48
Term_sub(Term_var(x), Id) → Term_var(x) 34.87/9.48
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m 34.87/9.48
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s) 34.87/9.48
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s) 34.87/9.48
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t)) 34.87/9.48
Sum_sub(xi, Id) → Sum_term_var(xi) 34.87/9.48
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k) 34.87/9.48
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s) 34.87/9.48
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s) 34.87/9.48
Concat(Concat(s, t), u) → Concat(s, Concat(t, u)) 34.87/9.48
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t)) 34.87/9.48
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t)) 34.87/9.48
Concat(Id, s) → s

Rewrite Strategy: INNERMOST
34.87/9.48
34.87/9.48

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

Converted CpxTRS to CDT
34.87/9.48
34.87/9.48

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 34.87/9.48
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.48
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.48
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 34.87/9.48
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 34.87/9.48
Term_sub(Term_var(z0), Id) → Term_var(z0) 34.87/9.48
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 34.87/9.48
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.48
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.48
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 34.87/9.48
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 34.87/9.48
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 34.87/9.48
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 34.87/9.48
Sum_sub(z0, Id) → Sum_term_var(z0) 34.87/9.48
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 34.87/9.48
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.48
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.48
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 34.87/9.48
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 34.87/9.48
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 34.87/9.48
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)) 34.87/9.48
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.48
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.48
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 34.87/9.48
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 34.87/9.48
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 34.87/9.48
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 34.87/9.48
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.48
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 34.87/9.48
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 34.87/9.48
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 34.87/9.48
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 34.87/9.48
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 34.87/9.48
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.48
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 34.87/9.48
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)) 34.87/9.48
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.48
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.48
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 34.87/9.48
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 34.87/9.48
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 34.87/9.48
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 34.87/9.48
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.48
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 34.87/9.48
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 34.87/9.48
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 34.87/9.48
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 34.87/9.48
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 34.87/9.48
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.48
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 34.87/9.48
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

34.87/9.48
34.87/9.48

(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(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)) 34.87/9.48
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 34.87/9.48
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 34.87/9.48
Concat(Id, z0) → z0 34.87/9.48
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.48
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.48
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 34.87/9.48
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 34.87/9.48
Term_sub(Term_var(z0), Id) → Term_var(z0) 34.87/9.48
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 34.87/9.48
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.48
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.48
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 34.87/9.48
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 34.87/9.48
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 34.87/9.48
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 34.87/9.48
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 34.87/9.48
Sum_sub(z0, Id) → Sum_term_var(z0) 34.87/9.48
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 34.87/9.49
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.49
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)) 34.87/9.49
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.49
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.49
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 34.87/9.49
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 34.87/9.49
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 34.87/9.49
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 34.87/9.49
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.49
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 34.87/9.49
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 34.87/9.49
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 34.87/9.49
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 34.87/9.49
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 34.87/9.49
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.49
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 34.87/9.49
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 34.87/9.49

POL(CONCAT(x1, x2)) = [2]x1    34.87/9.49
POL(Case(x1, x2, x3)) = x1 + x3    34.87/9.49
POL(Concat(x1, x2)) = x1 + [2]x2    34.87/9.49
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3    34.87/9.49
POL(Cons_usual(x1, x2, x3)) = x1 + x2 + x3    34.87/9.49
POL(FROZEN(x1, x2, x3, x4)) = [2]x1 + [2]x3    34.87/9.49
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4    34.87/9.49
POL(Id) = 0    34.87/9.49
POL(Left) = 0    34.87/9.49
POL(Right) = 0    34.87/9.49
POL(SUM_SUB(x1, x2)) = 0    34.87/9.49
POL(Sum_constant(x1)) = 0    34.87/9.49
POL(Sum_sub(x1, x2)) = 0    34.87/9.49
POL(Sum_term_var(x1)) = x1    34.87/9.49
POL(TERM_SUB(x1, x2)) = [2]x1    34.87/9.49
POL(Term_app(x1, x2)) = [1] + x1 + x2    34.87/9.49
POL(Term_inl(x1)) = x1    34.87/9.49
POL(Term_inr(x1)) = x1    34.87/9.49
POL(Term_pair(x1, x2)) = x1 + x2    34.87/9.49
POL(Term_sub(x1, x2)) = [4]x1 + [2]x2    34.87/9.49
POL(Term_var(x1)) = x1    34.87/9.49
POL(c(x1, x2)) = x1 + x2    34.87/9.49
POL(c1(x1, x2)) = x1 + x2    34.87/9.49
POL(c10(x1)) = x1    34.87/9.49
POL(c11(x1)) = x1    34.87/9.49
POL(c12(x1, x2)) = x1 + x2    34.87/9.49
POL(c15(x1)) = x1    34.87/9.49
POL(c16(x1)) = x1    34.87/9.49
POL(c17(x1, x2)) = x1 + x2    34.87/9.49
POL(c18(x1, x2)) = x1 + x2    34.87/9.49
POL(c19(x1)) = x1    34.87/9.49
POL(c2(x1, x2)) = x1 + x2    34.87/9.49
POL(c3(x1)) = x1    34.87/9.49
POL(c4(x1)) = x1    34.87/9.49
POL(c7(x1)) = x1    34.87/9.49
POL(c8(x1)) = x1    34.87/9.49
POL(c9(x1, x2)) = x1 + x2   
34.87/9.49
34.87/9.49

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 34.87/9.49
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.49
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 34.87/9.49
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 34.87/9.49
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 34.87/9.49
Term_sub(Term_var(z0), Id) → Term_var(z0) 34.87/9.49
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 34.87/9.49
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.49
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 34.87/9.49
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 34.87/9.49
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 34.87/9.49
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 34.87/9.49
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 34.87/9.49
Sum_sub(z0, Id) → Sum_term_var(z0) 34.87/9.49
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 34.87/9.49
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.49
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 34.87/9.49
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 34.87/9.49
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 34.87/9.49
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 34.87/9.49
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)) 34.87/9.49
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.49
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 34.87/9.49
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 34.87/9.49
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 34.87/9.49
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 34.87/9.49
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 34.87/9.49
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 34.87/9.49
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 34.87/9.49
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 34.87/9.49
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 34.87/9.49
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.51
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)) 35.35/9.51
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.51
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:

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

35.35/9.51
35.35/9.51

(5) 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)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
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)) 35.35/9.51
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.51
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.51
Concat(Id, z0) → z0 35.35/9.51
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.51
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.51
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.51
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.51
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.51
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.51
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.51
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
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)) 35.35/9.51
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.51
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 35.35/9.51

POL(CONCAT(x1, x2)) = [2]x1    35.35/9.51
POL(Case(x1, x2, x3)) = [4] + x1 + x3    35.35/9.51
POL(Concat(x1, x2)) = [4]x1 + [2]x2    35.35/9.51
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3    35.35/9.51
POL(Cons_usual(x1, x2, x3)) = [4] + x1 + x2 + x3    35.35/9.51
POL(FROZEN(x1, x2, x3, x4)) = [4] + [2]x1 + [2]x3    35.35/9.51
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4    35.35/9.51
POL(Id) = 0    35.35/9.51
POL(Left) = 0    35.35/9.51
POL(Right) = 0    35.35/9.51
POL(SUM_SUB(x1, x2)) = 0    35.35/9.51
POL(Sum_constant(x1)) = 0    35.35/9.51
POL(Sum_sub(x1, x2)) = 0    35.35/9.51
POL(Sum_term_var(x1)) = x1    35.35/9.51
POL(TERM_SUB(x1, x2)) = [2] + [2]x1    35.35/9.51
POL(Term_app(x1, x2)) = [4] + x1 + x2    35.35/9.51
POL(Term_inl(x1)) = x1    35.35/9.51
POL(Term_inr(x1)) = x1    35.35/9.51
POL(Term_pair(x1, x2)) = [1] + x1 + x2    35.35/9.51
POL(Term_sub(x1, x2)) = [2]x1 + [2]x2    35.35/9.51
POL(Term_var(x1)) = x1    35.35/9.51
POL(c(x1, x2)) = x1 + x2    35.35/9.51
POL(c1(x1, x2)) = x1 + x2    35.35/9.51
POL(c10(x1)) = x1    35.35/9.51
POL(c11(x1)) = x1    35.35/9.51
POL(c12(x1, x2)) = x1 + x2    35.35/9.51
POL(c15(x1)) = x1    35.35/9.51
POL(c16(x1)) = x1    35.35/9.51
POL(c17(x1, x2)) = x1 + x2    35.35/9.51
POL(c18(x1, x2)) = x1 + x2    35.35/9.51
POL(c19(x1)) = x1    35.35/9.51
POL(c2(x1, x2)) = x1 + x2    35.35/9.51
POL(c3(x1)) = x1    35.35/9.51
POL(c4(x1)) = x1    35.35/9.51
POL(c7(x1)) = x1    35.35/9.51
POL(c8(x1)) = x1    35.35/9.51
POL(c9(x1, x2)) = x1 + x2   
35.35/9.51
35.35/9.51

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.51
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.51
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.51
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.51
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.51
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.51
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.51
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.51
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)) 35.35/9.51
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.51
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
S tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.51
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.51
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.51
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

35.35/9.51
35.35/9.51

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

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

FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.51
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.51
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
35.35/9.51
35.35/9.51

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.51
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.51
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.51
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.51
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.51
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.51
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.51
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.51
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.51
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.51
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.51
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.51
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.51
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.51
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)) 35.35/9.51
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.51
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.51
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.51
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.57
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.57
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.57
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.57
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.57
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.57
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
S tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.57
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.57
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.57
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.57
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.57
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.57
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

35.35/9.57
35.35/9.57

(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_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)) 35.35/9.57
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.57
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.57
Concat(Id, z0) → z0 35.35/9.57
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.57
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.57
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.57
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.57
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.57
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.57
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.57
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.57
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.57
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.57
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.57
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.57
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.57
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.57
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.57
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.57
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)) 35.35/9.57
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.57
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.57
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.57
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.57
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.57
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.57
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.57
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 35.35/9.57

POL(CONCAT(x1, x2)) = [4]x1    35.35/9.57
POL(Case(x1, x2, x3)) = [1] + x1 + x3    35.35/9.57
POL(Concat(x1, x2)) = [4]x1 + [4]x2    35.35/9.57
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3    35.35/9.57
POL(Cons_usual(x1, x2, x3)) = [1] + x1 + x2 + x3    35.35/9.57
POL(FROZEN(x1, x2, x3, x4)) = [2] + [4]x1 + [4]x3    35.35/9.57
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4    35.35/9.57
POL(Id) = 0    35.35/9.57
POL(Left) = 0    35.35/9.57
POL(Right) = 0    35.35/9.57
POL(SUM_SUB(x1, x2)) = 0    35.35/9.57
POL(Sum_constant(x1)) = 0    35.35/9.57
POL(Sum_sub(x1, x2)) = 0    35.35/9.57
POL(Sum_term_var(x1)) = x1    35.35/9.57
POL(TERM_SUB(x1, x2)) = [4]x1    35.35/9.57
POL(Term_app(x1, x2)) = x1 + x2    35.35/9.57
POL(Term_inl(x1)) = x1    35.35/9.57
POL(Term_inr(x1)) = x1    35.35/9.57
POL(Term_pair(x1, x2)) = x1 + x2    35.35/9.57
POL(Term_sub(x1, x2)) = [4] + [4]x1 + [4]x2    35.35/9.57
POL(Term_var(x1)) = x1    35.35/9.57
POL(c(x1, x2)) = x1 + x2    35.35/9.57
POL(c1(x1, x2)) = x1 + x2    35.35/9.57
POL(c10(x1)) = x1    35.35/9.57
POL(c11(x1)) = x1    35.35/9.57
POL(c12(x1, x2)) = x1 + x2    35.35/9.57
POL(c15(x1)) = x1    35.35/9.57
POL(c16(x1)) = x1    35.35/9.57
POL(c17(x1, x2)) = x1 + x2    35.35/9.57
POL(c18(x1, x2)) = x1 + x2    35.35/9.57
POL(c19(x1)) = x1    35.35/9.57
POL(c2(x1, x2)) = x1 + x2    35.35/9.57
POL(c3(x1)) = x1    35.35/9.57
POL(c4(x1)) = x1    35.35/9.57
POL(c7(x1)) = x1    35.35/9.57
POL(c8(x1)) = x1    35.35/9.57
POL(c9(x1, x2)) = x1 + x2   
35.35/9.57
35.35/9.57

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.57
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.57
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.57
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.57
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.57
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.57
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.57
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.57
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.57
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.57
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.57
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.57
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.57
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.57
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.57
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.57
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.57
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.57
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.57
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.57
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)) 35.35/9.57
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.57
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.57
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
S tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
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

35.35/9.58
35.35/9.58

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

CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2))
We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 35.35/9.58

POL(CONCAT(x1, x2)) = [2]x1    35.35/9.58
POL(Case(x1, x2, x3)) = x1 + x3    35.35/9.58
POL(Concat(x1, x2)) = [1] + [4]x1 + [2]x2    35.35/9.58
POL(Cons_sum(x1, x2, x3)) = x1 + x3    35.35/9.58
POL(Cons_usual(x1, x2, x3)) = x1 + x2 + x3    35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [2]x1 + [2]x3    35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4    35.35/9.58
POL(Id) = [2]    35.35/9.58
POL(Left) = 0    35.35/9.58
POL(Right) = 0    35.35/9.58
POL(SUM_SUB(x1, x2)) = 0    35.35/9.58
POL(Sum_constant(x1)) = [2]    35.35/9.58
POL(Sum_sub(x1, x2)) = [4] + [2]x2    35.35/9.58
POL(Sum_term_var(x1)) = 0    35.35/9.58
POL(TERM_SUB(x1, x2)) = [2]x1    35.35/9.58
POL(Term_app(x1, x2)) = x1 + x2    35.35/9.58
POL(Term_inl(x1)) = x1    35.35/9.58
POL(Term_inr(x1)) = x1    35.35/9.58
POL(Term_pair(x1, x2)) = x1 + x2    35.35/9.58
POL(Term_sub(x1, x2)) = [2]x1 + [2]x2    35.35/9.58
POL(Term_var(x1)) = x1    35.35/9.58
POL(c(x1, x2)) = x1 + x2    35.35/9.58
POL(c1(x1, x2)) = x1 + x2    35.35/9.58
POL(c10(x1)) = x1    35.35/9.58
POL(c11(x1)) = x1    35.35/9.58
POL(c12(x1, x2)) = x1 + x2    35.35/9.58
POL(c15(x1)) = x1    35.35/9.58
POL(c16(x1)) = x1    35.35/9.58
POL(c17(x1, x2)) = x1 + x2    35.35/9.58
POL(c18(x1, x2)) = x1 + x2    35.35/9.58
POL(c19(x1)) = x1    35.35/9.58
POL(c2(x1, x2)) = x1 + x2    35.35/9.58
POL(c3(x1)) = x1    35.35/9.58
POL(c4(x1)) = x1    35.35/9.58
POL(c7(x1)) = x1    35.35/9.58
POL(c8(x1)) = x1    35.35/9.58
POL(c9(x1, x2)) = x1 + x2   
35.35/9.58
35.35/9.58

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
S tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(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

35.35/9.58
35.35/9.58

(13) 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_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 35.35/9.58

POL(CONCAT(x1, x2)) = [4]x1    35.35/9.58
POL(Case(x1, x2, x3)) = [4] + x1 + x3    35.35/9.58
POL(Concat(x1, x2)) = [2]x1 + x2    35.35/9.58
POL(Cons_sum(x1, x2, x3)) = x1 + x3    35.35/9.58
POL(Cons_usual(x1, x2, x3)) = x1 + x2 + x3    35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [4]x1 + [4]x3    35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4    35.35/9.58
POL(Id) = [4]    35.35/9.58
POL(Left) = 0    35.35/9.58
POL(Right) = 0    35.35/9.58
POL(SUM_SUB(x1, x2)) = 0    35.35/9.58
POL(Sum_constant(x1)) = [2]    35.35/9.58
POL(Sum_sub(x1, x2)) = [4] + x2    35.35/9.58
POL(Sum_term_var(x1)) = 0    35.35/9.58
POL(TERM_SUB(x1, x2)) = [4]x1    35.35/9.58
POL(Term_app(x1, x2)) = x1 + x2    35.35/9.58
POL(Term_inl(x1)) = x1    35.35/9.58
POL(Term_inr(x1)) = [4] + x1    35.35/9.58
POL(Term_pair(x1, x2)) = [4] + x1 + x2    35.35/9.58
POL(Term_sub(x1, x2)) = [4]x1 + x2    35.35/9.58
POL(Term_var(x1)) = x1    35.35/9.58
POL(c(x1, x2)) = x1 + x2    35.35/9.58
POL(c1(x1, x2)) = x1 + x2    35.35/9.58
POL(c10(x1)) = x1    35.35/9.58
POL(c11(x1)) = x1    35.35/9.58
POL(c12(x1, x2)) = x1 + x2    35.35/9.58
POL(c15(x1)) = x1    35.35/9.58
POL(c16(x1)) = x1    35.35/9.58
POL(c17(x1, x2)) = x1 + x2    35.35/9.58
POL(c18(x1, x2)) = x1 + x2    35.35/9.58
POL(c19(x1)) = x1    35.35/9.58
POL(c2(x1, x2)) = x1 + x2    35.35/9.58
POL(c3(x1)) = x1    35.35/9.58
POL(c4(x1)) = x1    35.35/9.58
POL(c7(x1)) = x1    35.35/9.58
POL(c8(x1)) = x1    35.35/9.58
POL(c9(x1, x2)) = x1 + x2   
35.35/9.58
35.35/9.58

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
S tuples:

TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1))
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

35.35/9.58
35.35/9.58

(15) 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_inl(z0), z1) → c3(TERM_SUB(z0, z1))
We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 35.35/9.58

POL(CONCAT(x1, x2)) = [2] + [4]x1    35.35/9.58
POL(Case(x1, x2, x3)) = [1] + x1 + x3    35.35/9.58
POL(Concat(x1, x2)) = [2] + [4]x1 + [2]x2    35.35/9.58
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3    35.35/9.58
POL(Cons_usual(x1, x2, x3)) = [1] + x1 + x2 + x3    35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [4] + [4]x1 + [4]x3    35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4    35.35/9.58
POL(Id) = [4]    35.35/9.58
POL(Left) = 0    35.35/9.58
POL(Right) = 0    35.35/9.58
POL(SUM_SUB(x1, x2)) = 0    35.35/9.58
POL(Sum_constant(x1)) = [2]    35.35/9.58
POL(Sum_sub(x1, x2)) = [4] + x2    35.35/9.58
POL(Sum_term_var(x1)) = 0    35.35/9.58
POL(TERM_SUB(x1, x2)) = [4]x1    35.35/9.58
POL(Term_app(x1, x2)) = [1] + x1 + x2    35.35/9.58
POL(Term_inl(x1)) = [4] + x1    35.35/9.58
POL(Term_inr(x1)) = x1    35.35/9.58
POL(Term_pair(x1, x2)) = x1 + x2    35.35/9.58
POL(Term_sub(x1, x2)) = [2] + x1 + [4]x2    35.35/9.58
POL(Term_var(x1)) = x1    35.35/9.58
POL(c(x1, x2)) = x1 + x2    35.35/9.58
POL(c1(x1, x2)) = x1 + x2    35.35/9.58
POL(c10(x1)) = x1    35.35/9.58
POL(c11(x1)) = x1    35.35/9.58
POL(c12(x1, x2)) = x1 + x2    35.35/9.58
POL(c15(x1)) = x1    35.35/9.58
POL(c16(x1)) = x1    35.35/9.58
POL(c17(x1, x2)) = x1 + x2    35.35/9.58
POL(c18(x1, x2)) = x1 + x2    35.35/9.58
POL(c19(x1)) = x1    35.35/9.58
POL(c2(x1, x2)) = x1 + x2    35.35/9.58
POL(c3(x1)) = x1    35.35/9.58
POL(c4(x1)) = x1    35.35/9.58
POL(c7(x1)) = x1    35.35/9.58
POL(c8(x1)) = x1    35.35/9.58
POL(c9(x1, x2)) = x1 + x2   
35.35/9.58
35.35/9.58

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1))
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

35.35/9.58
35.35/9.58

(17) 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_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 35.35/9.58

POL(CONCAT(x1, x2)) = [2] + [2]x1    35.35/9.58
POL(Case(x1, x2, x3)) = [4] + x1 + x3    35.35/9.58
POL(Concat(x1, x2)) = [4] + [4]x1 + [2]x2    35.35/9.58
POL(Cons_sum(x1, x2, x3)) = [4] + x1 + x2 + x3    35.35/9.58
POL(Cons_usual(x1, x2, x3)) = [2] + x1 + x2 + x3    35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [2]x1 + [2]x3    35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [3] + [3]x1 + [3]x3 + [3]x4    35.35/9.58
POL(Id) = [4]    35.35/9.58
POL(Left) = 0    35.35/9.58
POL(Right) = 0    35.35/9.58
POL(SUM_SUB(x1, x2)) = 0    35.35/9.58
POL(Sum_constant(x1)) = 0    35.35/9.58
POL(Sum_sub(x1, x2)) = [2] + x2    35.35/9.58
POL(Sum_term_var(x1)) = 0    35.35/9.58
POL(TERM_SUB(x1, x2)) = [2]x1    35.35/9.58
POL(Term_app(x1, x2)) = [3] + x1 + x2    35.35/9.58
POL(Term_inl(x1)) = x1    35.35/9.58
POL(Term_inr(x1)) = x1    35.35/9.58
POL(Term_pair(x1, x2)) = [3] + x1 + x2    35.35/9.58
POL(Term_sub(x1, x2)) = [1] + x1 + [2]x2    35.35/9.58
POL(Term_var(x1)) = x1    35.35/9.58
POL(c(x1, x2)) = x1 + x2    35.35/9.58
POL(c1(x1, x2)) = x1 + x2    35.35/9.58
POL(c10(x1)) = x1    35.35/9.58
POL(c11(x1)) = x1    35.35/9.58
POL(c12(x1, x2)) = x1 + x2    35.35/9.58
POL(c15(x1)) = x1    35.35/9.58
POL(c16(x1)) = x1    35.35/9.58
POL(c17(x1, x2)) = x1 + x2    35.35/9.58
POL(c18(x1, x2)) = x1 + x2    35.35/9.58
POL(c19(x1)) = x1    35.35/9.58
POL(c2(x1, x2)) = x1 + x2    35.35/9.58
POL(c3(x1)) = x1    35.35/9.58
POL(c4(x1)) = x1    35.35/9.58
POL(c7(x1)) = x1    35.35/9.58
POL(c8(x1)) = x1    35.35/9.58
POL(c9(x1, x2)) = x1 + x2   
35.35/9.58
35.35/9.58

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
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

35.35/9.58
35.35/9.58

(19) 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))
We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 35.35/9.58

POL(CONCAT(x1, x2)) = x1 + [2]x1·x2    35.35/9.58
POL(Case(x1, x2, x3)) = [2] + x1 + x3    35.35/9.58
POL(Concat(x1, x2)) = x1 + x2 + [2]x1·x2    35.35/9.58
POL(Cons_sum(x1, x2, x3)) = x1 + x2 + x3    35.35/9.58
POL(Cons_usual(x1, x2, x3)) = [1] + x1 + x2 + x3    35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = x1 + x3 + [2]x3·x4 + [2]x1·x4    35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [2] + x1 + x3 + [2]x4 + [2]x3·x4 + [2]x1·x4    35.35/9.58
POL(Id) = 0    35.35/9.58
POL(Left) = 0    35.35/9.58
POL(Right) = 0    35.35/9.58
POL(SUM_SUB(x1, x2)) = [2]    35.35/9.58
POL(Sum_constant(x1)) = 0    35.35/9.58
POL(Sum_sub(x1, x2)) = [3]x12    35.35/9.58
POL(Sum_term_var(x1)) = 0    35.35/9.58
POL(TERM_SUB(x1, x2)) = x1 + [2]x1·x2    35.35/9.58
POL(Term_app(x1, x2)) = [2] + x1 + x2    35.35/9.58
POL(Term_inl(x1)) = x1    35.35/9.58
POL(Term_inr(x1)) = x1    35.35/9.58
POL(Term_pair(x1, x2)) = [1] + x1 + x2    35.35/9.58
POL(Term_sub(x1, x2)) = x1 + x2 + [2]x1·x2    35.35/9.58
POL(Term_var(x1)) = [1]    35.35/9.58
POL(c(x1, x2)) = x1 + x2    35.35/9.58
POL(c1(x1, x2)) = x1 + x2    35.35/9.58
POL(c10(x1)) = x1    35.35/9.58
POL(c11(x1)) = x1    35.35/9.58
POL(c12(x1, x2)) = x1 + x2    35.35/9.58
POL(c15(x1)) = x1    35.35/9.58
POL(c16(x1)) = x1    35.35/9.58
POL(c17(x1, x2)) = x1 + x2    35.35/9.58
POL(c18(x1, x2)) = x1 + x2    35.35/9.58
POL(c19(x1)) = x1    35.35/9.58
POL(c2(x1, x2)) = x1 + x2    35.35/9.58
POL(c3(x1)) = x1    35.35/9.58
POL(c4(x1)) = x1    35.35/9.58
POL(c7(x1)) = x1    35.35/9.58
POL(c8(x1)) = x1    35.35/9.58
POL(c9(x1, x2)) = x1 + x2   
35.35/9.58
35.35/9.58

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
S tuples:

TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(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

35.35/9.58
35.35/9.58

(21) 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_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
We considered the (Usable) Rules:

Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
Concat(Id, z0) → z0 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 35.35/9.58

POL(CONCAT(x1, x2)) = [2]x1·x2 + x12    35.35/9.58
POL(Case(x1, x2, x3)) = [1] + x1 + x3    35.35/9.58
POL(Concat(x1, x2)) = x1 + x2 + x1·x2    35.35/9.58
POL(Cons_sum(x1, x2, x3)) = [1] + x1 + x2 + x3    35.35/9.58
POL(Cons_usual(x1, x2, x3)) = [3] + x1 + x2 + x3    35.35/9.58
POL(FROZEN(x1, x2, x3, x4)) = [2]x3·x4 + [2]x1·x4 + x12 + [2]x1·x3 + x32    35.35/9.58
POL(Frozen(x1, x2, x3, x4)) = [1] + x1 + x3 + x3·x4 + x2·x4 + x1·x4    35.35/9.58
POL(Id) = 0    35.35/9.58
POL(Left) = 0    35.35/9.58
POL(Right) = 0    35.35/9.58
POL(SUM_SUB(x1, x2)) = 0    35.35/9.58
POL(Sum_constant(x1)) = [1]    35.35/9.58
POL(Sum_sub(x1, x2)) = [2]    35.35/9.58
POL(Sum_term_var(x1)) = [2]    35.35/9.58
POL(TERM_SUB(x1, x2)) = [2]x1·x2 + x12    35.35/9.58
POL(Term_app(x1, x2)) = [1] + x1 + x2    35.35/9.58
POL(Term_inl(x1)) = x1    35.35/9.58
POL(Term_inr(x1)) = x1    35.35/9.58
POL(Term_pair(x1, x2)) = [1] + x1 + x2    35.35/9.58
POL(Term_sub(x1, x2)) = x1 + x2 + x1·x2    35.35/9.58
POL(Term_var(x1)) = [2]    35.35/9.58
POL(c(x1, x2)) = x1 + x2    35.35/9.58
POL(c1(x1, x2)) = x1 + x2    35.35/9.58
POL(c10(x1)) = x1    35.35/9.58
POL(c11(x1)) = x1    35.35/9.58
POL(c12(x1, x2)) = x1 + x2    35.35/9.58
POL(c15(x1)) = x1    35.35/9.58
POL(c16(x1)) = x1    35.35/9.58
POL(c17(x1, x2)) = x1 + x2    35.35/9.58
POL(c18(x1, x2)) = x1 + x2    35.35/9.58
POL(c19(x1)) = x1    35.35/9.58
POL(c2(x1, x2)) = x1 + x2    35.35/9.58
POL(c3(x1)) = x1    35.35/9.58
POL(c4(x1)) = x1    35.35/9.58
POL(c7(x1)) = x1    35.35/9.58
POL(c8(x1)) = x1    35.35/9.58
POL(c9(x1, x2)) = x1 + x2   
35.35/9.58
35.35/9.58

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.58
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.58
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.58
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.58
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.58
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.58
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.58
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.58
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.58
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.58
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.58
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.58
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.58
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.58
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)) 35.35/9.58
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
S tuples:

SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.58
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3))
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.58
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.58
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.58
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.58
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.58
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.58
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.58
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.58
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.59
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(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

35.35/9.59
35.35/9.59

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

SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.59
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)) 35.35/9.59
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.59
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.59
Concat(Id, z0) → z0 35.35/9.59
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.59
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.59
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.59
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.59
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.59
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.59
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.59
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.59
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.59
Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.59
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.59
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.59
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.59
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.59
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.59
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.59
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)) 35.35/9.59
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.59
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.59
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.59
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.59
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.59
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 35.35/9.59

POL(CONCAT(x1, x2)) = [2]x1·x2 + x12    35.35/9.59
POL(Case(x1, x2, x3)) = [1] + x1 + x3    35.35/9.59
POL(Concat(x1, x2)) = x1 + x2 + [3]x1·x2 + [2]x12    35.35/9.59
POL(Cons_sum(x1, x2, x3)) = [3] + x1 + x3    35.35/9.59
POL(Cons_usual(x1, x2, x3)) = [1] + x1 + x2 + x3    35.35/9.59
POL(FROZEN(x1, x2, x3, x4)) = [1] + x2 + [2]x3·x4 + [2]x1·x4 + x12 + [2]x1·x3 + x32    35.35/9.59
POL(Frozen(x1, x2, x3, x4)) = [2] + [2]x1 + [2]x2 + [2]x3 + [2]x4 + [3]x3·x4 + [3]x1·x4 + [2]x12 + [2]x32    35.35/9.59
POL(Id) = 0    35.35/9.59
POL(Left) = 0    35.35/9.59
POL(Right) = 0    35.35/9.59
POL(SUM_SUB(x1, x2)) = x2    35.35/9.59
POL(Sum_constant(x1)) = [3]    35.35/9.59
POL(Sum_sub(x1, x2)) = x2    35.35/9.59
POL(Sum_term_var(x1)) = 0    35.35/9.59
POL(TERM_SUB(x1, x2)) = [2]x1·x2 + x12    35.35/9.59
POL(Term_app(x1, x2)) = [1] + x1 + x2    35.35/9.59
POL(Term_inl(x1)) = x1    35.35/9.59
POL(Term_inr(x1)) = x1    35.35/9.59
POL(Term_pair(x1, x2)) = [1] + x1 + x2    35.35/9.59
POL(Term_sub(x1, x2)) = x1 + x2 + [3]x1·x2 + [2]x12    35.35/9.59
POL(Term_var(x1)) = 0    35.35/9.59
POL(c(x1, x2)) = x1 + x2    35.35/9.59
POL(c1(x1, x2)) = x1 + x2    35.35/9.59
POL(c10(x1)) = x1    35.35/9.59
POL(c11(x1)) = x1    35.35/9.59
POL(c12(x1, x2)) = x1 + x2    35.35/9.59
POL(c15(x1)) = x1    35.35/9.59
POL(c16(x1)) = x1    35.35/9.59
POL(c17(x1, x2)) = x1 + x2    35.35/9.59
POL(c18(x1, x2)) = x1 + x2    35.35/9.59
POL(c19(x1)) = x1    35.35/9.59
POL(c2(x1, x2)) = x1 + x2    35.35/9.59
POL(c3(x1)) = x1    35.35/9.59
POL(c4(x1)) = x1    35.35/9.59
POL(c7(x1)) = x1    35.35/9.59
POL(c8(x1)) = x1    35.35/9.59
POL(c9(x1, x2)) = x1 + x2   
35.35/9.59
35.35/9.59

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

Term_sub(Case(z0, z1, z2), z3) → Frozen(z0, Sum_sub(z1, z3), z2, z3) 35.35/9.59
Term_sub(Term_app(z0, z1), z2) → Term_app(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.59
Term_sub(Term_pair(z0, z1), z2) → Term_pair(Term_sub(z0, z2), Term_sub(z1, z2)) 35.35/9.59
Term_sub(Term_inl(z0), z1) → Term_inl(Term_sub(z0, z1)) 35.35/9.59
Term_sub(Term_inr(z0), z1) → Term_inr(Term_sub(z0, z1)) 35.35/9.59
Term_sub(Term_var(z0), Id) → Term_var(z0) 35.35/9.59
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → z2 35.35/9.59
Term_sub(Term_var(z0), Cons_usual(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.59
Term_sub(Term_var(z0), Cons_sum(z1, z2, z3)) → Term_sub(Term_var(z0), z3) 35.35/9.59
Term_sub(Term_sub(z0, z1), z2) → Term_sub(z0, Concat(z1, z2)) 35.35/9.59
Frozen(z0, Sum_constant(Left), z1, z2) → Term_sub(z0, z2) 35.35/9.59
Frozen(z0, Sum_constant(Right), z1, z2) → Term_sub(z1, z2) 35.35/9.59
Frozen(z0, Sum_term_var(z1), z2, z3) → Case(Term_sub(z0, z3), z1, Term_sub(z2, z3)) 35.35/9.59
Sum_sub(z0, Id) → Sum_term_var(z0) 35.35/9.59
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_constant(z2) 35.35/9.59
Sum_sub(z0, Cons_sum(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.59
Sum_sub(z0, Cons_usual(z1, z2, z3)) → Sum_sub(z0, z3) 35.35/9.59
Concat(Concat(z0, z1), z2) → Concat(z0, Concat(z1, z2)) 35.35/9.59
Concat(Cons_usual(z0, z1, z2), z3) → Cons_usual(z0, Term_sub(z1, z3), Concat(z2, z3)) 35.35/9.59
Concat(Cons_sum(z0, z1, z2), z3) → Cons_sum(z0, z1, Concat(z2, z3)) 35.35/9.59
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)) 35.35/9.59
TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.59
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.59
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.59
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c16(SUM_SUB(z0, z3)) 35.35/9.59
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.59
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3))
S tuples:none
K tuples:

TERM_SUB(Term_app(z0, z1), z2) → c1(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Case(z0, z1, z2), z3) → c(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3)) 35.35/9.59
FROZEN(z0, Sum_constant(Left), z1, z2) → c10(TERM_SUB(z0, z2)) 35.35/9.59
FROZEN(z0, Sum_constant(Right), z1, z2) → c11(TERM_SUB(z1, z2)) 35.35/9.59
CONCAT(Cons_usual(z0, z1, z2), z3) → c18(TERM_SUB(z1, z3), CONCAT(z2, z3)) 35.35/9.59
FROZEN(z0, Sum_term_var(z1), z2, z3) → c12(TERM_SUB(z0, z3), TERM_SUB(z2, z3)) 35.35/9.59
TERM_SUB(Term_sub(z0, z1), z2) → c9(TERM_SUB(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
CONCAT(Concat(z0, z1), z2) → c17(CONCAT(z0, Concat(z1, z2)), CONCAT(z1, z2)) 35.35/9.59
TERM_SUB(Term_pair(z0, z1), z2) → c2(TERM_SUB(z0, z2), TERM_SUB(z1, z2)) 35.35/9.59
TERM_SUB(Term_inr(z0), z1) → c4(TERM_SUB(z0, z1)) 35.35/9.59
TERM_SUB(Term_inl(z0), z1) → c3(TERM_SUB(z0, z1)) 35.35/9.59
CONCAT(Cons_sum(z0, z1, z2), z3) → c19(CONCAT(z2, z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c7(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3)) 35.35/9.59
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15(SUM_SUB(z0, z3)) 35.35/9.59
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

35.35/9.59
35.35/9.59

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

The set S is empty
35.35/9.59
35.35/9.59

(26) BOUNDS(O(1), O(1))

35.35/9.59
35.35/9.59
35.69/9.63 EOF