Runtime Complexity (full) proof of /tmp/tmpIrKhZt/lse.xml

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

0 CpxTRS

↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 14 ms)

↳2 CpxTRS

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

↳4 CpxTRS

↳5 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 26 ms)

↳6 CdtProblem

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

↳8 CdtProblem

↳9 CdtUsableRulesProof (⇔, 0 ms)

↳10 CdtProblem

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

↳12 CdtProblem

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

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 46 ms)

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 130 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 95 ms)

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 82 ms)

↳22 CdtProblem

↳23 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 75 ms)

↳24 CdtProblem

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

↳26 BOUNDS(1, 1)

(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(x₁, x₂)) = x₁
POL(Case(x₁, x₂, x₃)) = [1] + x₁ + x₃
POL(Cons_sum(x₁, x₂, x₃)) = [1] + x₃
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₁ + x₃
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(SUM_SUB(x₁, x₂)) = 0
POL(Sum_constant(x₁)) = 0
POL(Sum_sub(x₁, x₂)) = 0
POL(Sum_term_var(x₁)) = 0
POL(TERM_SUB(x₁, x₂)) = x₁
POL(Term_app(x₁, x₂)) = [1] + x₁ + x₂
POL(Term_inl(x₁)) = [1] + x₁
POL(Term_inr(x₁)) = [1] + x₁
POL(Term_pair(x₁, x₂)) = x₁ + x₂
POL(Term_var(x₁)) = 0
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁

(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(x₁, x₂)) = x₁
POL(Case(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃
POL(Cons_sum(x₁, x₂, x₃)) = [1] + x₂ + x₃
POL(Cons_usual(x₁, x₂, x₃)) = x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = [1] + x₁ + x₃
POL(Id) = [1]
POL(Left) = 0
POL(Right) = 0
POL(SUM_SUB(x₁, x₂)) = 0
POL(Sum_constant(x₁)) = [1]
POL(Sum_sub(x₁, x₂)) = [1] + x₁ + x₂
POL(Sum_term_var(x₁)) = [1]
POL(TERM_SUB(x₁, x₂)) = x₁
POL(Term_app(x₁, x₂)) = x₁ + x₂
POL(Term_inl(x₁)) = x₁
POL(Term_inr(x₁)) = x₁
POL(Term_pair(x₁, x₂)) = [1] + x₁ + x₂
POL(Term_var(x₁)) = 0
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁

(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(x₁, x₂)) = [2]x₁·x₂ + [2]x₁²
POL(Case(x₁, x₂, x₃)) = x₁ + x₃
POL(Cons_sum(x₁, x₂, x₃)) = x₃
POL(Cons_usual(x₁, x₂, x₃)) = [2] + x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₃·x₄ + x₁·x₄
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(SUM_SUB(x₁, x₂)) = 0
POL(Sum_constant(x₁)) = 0
POL(Sum_sub(x₁, x₂)) = [2] + x₁ + [2]x₁·x₂ + [2]x₁²
POL(Sum_term_var(x₁)) = 0
POL(TERM_SUB(x₁, x₂)) = x₁·x₂
POL(Term_app(x₁, x₂)) = [2] + x₁ + x₂
POL(Term_inl(x₁)) = [2] + x₁
POL(Term_inr(x₁)) = [2] + x₁
POL(Term_pair(x₁, x₂)) = [2] + x₁ + x₂
POL(Term_var(x₁)) = [2]
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁

(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(x₁, x₂)) = [2]x₁·x₂
POL(Case(x₁, x₂, x₃)) = [2] + x₁ + x₂ + x₃
POL(Cons_sum(x₁, x₂, x₃)) = x₃
POL(Cons_usual(x₁, x₂, x₃)) = [1] + x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₄ + [2]x₃·x₄ + [2]x₁·x₄
POL(Id) = [1]
POL(Left) = [2]
POL(Right) = 0
POL(SUM_SUB(x₁, x₂)) = x₂ + [2]x₁·x₂
POL(Sum_constant(x₁)) = [2]
POL(Sum_sub(x₁, x₂)) = [2] + [2]x₂ + x₂² + [2]x₁·x₂ + [2]x₁²
POL(Sum_term_var(x₁)) = 0
POL(TERM_SUB(x₁, x₂)) = [2]x₁·x₂
POL(Term_app(x₁, x₂)) = [2] + x₁ + x₂
POL(Term_inl(x₁)) = x₁
POL(Term_inr(x₁)) = [2] + x₁
POL(Term_pair(x₁, x₂)) = [1] + x₁ + x₂
POL(Term_var(x₁)) = 0
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁

(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(x₁, x₂)) = [2]x₁ + [2]x₁·x₂ + [2]x₁²
POL(Case(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃
POL(Cons_sum(x₁, x₂, x₃)) = [2] + x₃
POL(Cons_usual(x₁, x₂, x₃)) = [2] + x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = [2]x₁ + [2]x₃ + x₃·x₄ + x₁·x₄ + [2]x₁² + x₁·x₃ + [2]x₃²
POL(Id) = [1]
POL(Left) = 0
POL(Right) = [1]
POL(SUM_SUB(x₁, x₂)) = x₁ + x₁·x₂ + x₁²
POL(Sum_constant(x₁)) = [1]
POL(Sum_sub(x₁, x₂)) = [2]x₂² + x₁·x₂ + [2]x₁²
POL(Sum_term_var(x₁)) = 0
POL(TERM_SUB(x₁, x₂)) = [2]x₁ + x₁·x₂ + [2]x₁²
POL(Term_app(x₁, x₂)) = x₁ + x₂
POL(Term_inl(x₁)) = x₁
POL(Term_inr(x₁)) = [2] + x₁
POL(Term_pair(x₁, x₂)) = [1] + x₁ + x₂
POL(Term_var(x₁)) = [1]
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁

(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(x₁, x₂)) = x₁·x₂ + [2]x₁²
POL(Case(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃
POL(Cons_sum(x₁, x₂, x₃)) = [1] + x₃
POL(Cons_usual(x₁, x₂, x₃)) = x₂ + x₃
POL(FROZEN(x₁, x₂, x₃, x₄)) = x₃·x₄ + x₁·x₄
POL(Id) = 0
POL(Left) = [1]
POL(Right) = [1]
POL(SUM_SUB(x₁, x₂)) = x₂
POL(Sum_constant(x₁)) = 0
POL(Sum_sub(x₁, x₂)) = [2]x₁·x₂
POL(Sum_term_var(x₁)) = 0
POL(TERM_SUB(x₁, x₂)) = x₁·x₂
POL(Term_app(x₁, x₂)) = x₁ + x₂
POL(Term_inl(x₁)) = x₁
POL(Term_inr(x₁)) = [1] + x₁
POL(Term_pair(x₁, x₂)) = x₁ + x₂
POL(Term_var(x₁)) = 0
POL(c(x₁, x₂)) = x₁ + x₂
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c18(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c5(x₁, x₂)) = x₁ + x₂
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁

(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

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) CdtUsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) BOUNDS(1, 1)