(0) Obligation:

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


The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Rewrite Strategy: FULL

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

The following defined symbols can occur below the 1th argument of Frozen: Sum_sub

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))

(2) Obligation:

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


The TRS R consists of the following rules:

Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Concat(Id, s) → s
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)

Rewrite Strategy: FULL

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

Converted rc-obligation to irc-obligation.

The duplicating contexts are:
Term_sub(Term_pair(m, n), [])
Concat(Cons_usual(x, m, s), [])
Term_sub(Case(m, xi, n), [])
Term_sub(Term_app(m, n), [])
Frozen(m, Sum_term_var(xi), n, [])

The defined contexts are:
Frozen(x0, [], x2, x3)

[] just represents basic- or constructor-terms in the following defined contexts:
Frozen(x0, [], x2, x3)

As the TRS is an overlay system and the defined contexts and the duplicating contexts don't overlap, we have rc = irc.

(4) Obligation:

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


The TRS R consists of the following rules:

Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Concat(Id, s) → s
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

Term_sub, Concat, Sum_sub, Frozen

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

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

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

Removed 5 trailing nodes:

TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c3
TERM_SUB(Term_var(z0), Id) → c2
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c15
SUM_SUB(z0, Id) → c14
CONCAT(Id, z0) → c9

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
S tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
K tuples:none
Defined Rule Symbols:

Term_sub, Concat, Sum_sub, Frozen

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

c, c1, c4, c5, c6, c7, c8, c10, c11, c12, c13, c16, c17, c18

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

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

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
S tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
K tuples:none
Defined Rule Symbols:

Sum_sub

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

c, c1, c4, c5, c6, c7, c8, c10, c11, c12, c13, c16, c17, c18

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(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) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
We considered the (Usable) Rules:none
And the Tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x1, x2)) = x1   
POL(Case(x1, x2, x3)) = [1] + x1 + x3   
POL(Cons_sum(x1, x2, x3)) = [1] + x3   
POL(Cons_usual(x1, x2, x3)) = [1] + x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = x1 + x3   
POL(Id) = 0   
POL(Left) = 0   
POL(Right) = 0   
POL(SUM_SUB(x1, x2)) = 0   
POL(Sum_constant(x1)) = 0   
POL(Sum_sub(x1, x2)) = 0   
POL(Sum_term_var(x1)) = 0   
POL(TERM_SUB(x1, x2)) = x1   
POL(Term_app(x1, x2)) = [1] + x1 + x2   
POL(Term_inl(x1)) = [1] + x1   
POL(Term_inr(x1)) = [1] + x1   
POL(Term_pair(x1, x2)) = x1 + x2   
POL(Term_var(x1)) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1)) = x1   
POL(c10(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c16(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c18(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
S tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
Defined Rule Symbols:

Sum_sub

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

c, c1, c4, c5, c6, c7, c8, c10, c11, c12, c13, c16, c17, c18

(13) 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) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
S tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
Defined Rule Symbols:

Sum_sub

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

c, c1, c4, c5, c6, c7, c8, c10, c11, c12, c13, c16, c17, c18

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(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) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
We considered the (Usable) Rules:none
And the Tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x1, x2)) = x1   
POL(Case(x1, x2, x3)) = [1] + x1 + x2 + x3   
POL(Cons_sum(x1, x2, x3)) = [1] + x2 + x3   
POL(Cons_usual(x1, x2, x3)) = x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = [1] + x1 + x3   
POL(Id) = [1]   
POL(Left) = 0   
POL(Right) = 0   
POL(SUM_SUB(x1, x2)) = 0   
POL(Sum_constant(x1)) = [1]   
POL(Sum_sub(x1, x2)) = [1] + x1 + x2   
POL(Sum_term_var(x1)) = [1]   
POL(TERM_SUB(x1, x2)) = x1   
POL(Term_app(x1, x2)) = x1 + x2   
POL(Term_inl(x1)) = x1   
POL(Term_inr(x1)) = x1   
POL(Term_pair(x1, x2)) = [1] + x1 + x2   
POL(Term_var(x1)) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1)) = x1   
POL(c10(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c16(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c18(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
S tuples:

TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
Defined Rule Symbols:

Sum_sub

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

c, c1, c4, c5, c6, c7, c8, c10, c11, c12, c13, c16, c17, c18

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(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)) → c8(TERM_SUB(Term_var(z0), z3))
We considered the (Usable) Rules:none
And the Tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x1, x2)) = [2]x1·x2 + [2]x12   
POL(Case(x1, x2, x3)) = x1 + x3   
POL(Cons_sum(x1, x2, x3)) = x3   
POL(Cons_usual(x1, x2, x3)) = [2] + x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = x3·x4 + x1·x4   
POL(Id) = 0   
POL(Left) = 0   
POL(Right) = 0   
POL(SUM_SUB(x1, x2)) = 0   
POL(Sum_constant(x1)) = 0   
POL(Sum_sub(x1, x2)) = [2] + x1 + [2]x1·x2 + [2]x12   
POL(Sum_term_var(x1)) = 0   
POL(TERM_SUB(x1, x2)) = x1·x2   
POL(Term_app(x1, x2)) = [2] + x1 + x2   
POL(Term_inl(x1)) = [2] + x1   
POL(Term_inr(x1)) = [2] + x1   
POL(Term_pair(x1, x2)) = [2] + x1 + x2   
POL(Term_var(x1)) = [2]   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1)) = x1   
POL(c10(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c16(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c18(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
S tuples:

TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
Defined Rule Symbols:

Sum_sub

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

c, c1, c4, c5, c6, c7, c8, c10, c11, c12, c13, c16, c17, c18

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

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

SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
We considered the (Usable) Rules:none
And the Tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x1, x2)) = [2]x1·x2   
POL(Case(x1, x2, x3)) = [2] + x1 + x2 + x3   
POL(Cons_sum(x1, x2, x3)) = x3   
POL(Cons_usual(x1, x2, x3)) = [1] + x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = x4 + [2]x3·x4 + [2]x1·x4   
POL(Id) = [1]   
POL(Left) = [2]   
POL(Right) = 0   
POL(SUM_SUB(x1, x2)) = x2 + [2]x1·x2   
POL(Sum_constant(x1)) = [2]   
POL(Sum_sub(x1, x2)) = [2] + [2]x2 + x22 + [2]x1·x2 + [2]x12   
POL(Sum_term_var(x1)) = 0   
POL(TERM_SUB(x1, x2)) = [2]x1·x2   
POL(Term_app(x1, x2)) = [2] + x1 + x2   
POL(Term_inl(x1)) = x1   
POL(Term_inr(x1)) = [2] + x1   
POL(Term_pair(x1, x2)) = [1] + x1 + x2   
POL(Term_var(x1)) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1)) = x1   
POL(c10(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c16(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c18(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
S tuples:

TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
Defined Rule Symbols:

Sum_sub

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

c, c1, c4, c5, c6, c7, c8, c10, c11, c12, c13, c16, c17, c18

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(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)) → c1(TERM_SUB(Term_var(z0), z3))
We considered the (Usable) Rules:none
And the Tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x1, x2)) = [2]x1 + [2]x1·x2 + [2]x12   
POL(Case(x1, x2, x3)) = [1] + x1 + x2 + x3   
POL(Cons_sum(x1, x2, x3)) = [2] + x3   
POL(Cons_usual(x1, x2, x3)) = [2] + x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = [2]x1 + [2]x3 + x3·x4 + x1·x4 + [2]x12 + x1·x3 + [2]x32   
POL(Id) = [1]   
POL(Left) = 0   
POL(Right) = [1]   
POL(SUM_SUB(x1, x2)) = x1 + x1·x2 + x12   
POL(Sum_constant(x1)) = [1]   
POL(Sum_sub(x1, x2)) = [2]x22 + x1·x2 + [2]x12   
POL(Sum_term_var(x1)) = 0   
POL(TERM_SUB(x1, x2)) = [2]x1 + x1·x2 + [2]x12   
POL(Term_app(x1, x2)) = x1 + x2   
POL(Term_inl(x1)) = x1   
POL(Term_inr(x1)) = [2] + x1   
POL(Term_pair(x1, x2)) = [1] + x1 + x2   
POL(Term_var(x1)) = [1]   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1)) = x1   
POL(c10(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c16(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c18(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
S tuples:

SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
Defined Rule Symbols:

Sum_sub

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

c, c1, c4, c5, c6, c7, c8, c10, c11, c12, c13, c16, c17, c18

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(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)) → c12(SUM_SUB(z0, z3))
We considered the (Usable) Rules:none
And the Tuples:

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(CONCAT(x1, x2)) = x1·x2 + [2]x12   
POL(Case(x1, x2, x3)) = [1] + x1 + x2 + x3   
POL(Cons_sum(x1, x2, x3)) = [1] + x3   
POL(Cons_usual(x1, x2, x3)) = x2 + x3   
POL(FROZEN(x1, x2, x3, x4)) = x3·x4 + x1·x4   
POL(Id) = 0   
POL(Left) = [1]   
POL(Right) = [1]   
POL(SUM_SUB(x1, x2)) = x2   
POL(Sum_constant(x1)) = 0   
POL(Sum_sub(x1, x2)) = [2]x1·x2   
POL(Sum_term_var(x1)) = 0   
POL(TERM_SUB(x1, x2)) = x1·x2   
POL(Term_app(x1, x2)) = x1 + x2   
POL(Term_inl(x1)) = x1   
POL(Term_inr(x1)) = [1] + x1   
POL(Term_pair(x1, x2)) = x1 + x2   
POL(Term_var(x1)) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c1(x1)) = x1   
POL(c10(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c16(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c18(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
S tuples:none
K tuples:

TERM_SUB(Case(z0, z1, z2), z3) → c4(FROZEN(z0, Sum_sub(z1, z3), z2, z3), SUM_SUB(z1, z3))
TERM_SUB(Term_app(z0, z1), z2) → c5(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_inl(z0), z1) → c6(TERM_SUB(z0, z1))
TERM_SUB(Term_inr(z0), z1) → c7(TERM_SUB(z0, z1))
CONCAT(Cons_usual(z0, z1, z2), z3) → c10(TERM_SUB(z1, z3), CONCAT(z2, z3))
CONCAT(Cons_sum(z0, z1, z2), z3) → c11(CONCAT(z2, z3))
FROZEN(z0, Sum_term_var(z1), z2, z3) → c16(TERM_SUB(z0, z3), TERM_SUB(z2, z3))
FROZEN(z0, Sum_constant(Left), z1, z2) → c17(TERM_SUB(z0, z2))
FROZEN(z0, Sum_constant(Right), z1, z2) → c18(TERM_SUB(z1, z2))
TERM_SUB(Term_pair(z0, z1), z2) → c(TERM_SUB(z0, z2), TERM_SUB(z1, z2))
TERM_SUB(Term_var(z0), Cons_usual(z1, z2, z3)) → c8(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_usual(z1, z2, z3)) → c13(SUM_SUB(z0, z3))
TERM_SUB(Term_var(z0), Cons_sum(z1, z2, z3)) → c1(TERM_SUB(Term_var(z0), z3))
SUM_SUB(z0, Cons_sum(z1, z2, z3)) → c12(SUM_SUB(z0, z3))
Defined Rule Symbols:

Sum_sub

Defined Pair Symbols:

TERM_SUB, CONCAT, SUM_SUB, FROZEN

Compound Symbols:

c, c1, c4, c5, c6, c7, c8, c10, c11, c12, c13, c16, c17, c18

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

The set S is empty

(26) BOUNDS(1, 1)