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

0 CpxRelTRS
↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 14 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳6 CdtProblem
↳7 CdtUsableRulesProof (⇔, 0 ms)
↳8 CdtProblem
↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 192 ms)
↳10 CdtProblem
↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
↳12 CdtProblem
↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 594 ms)
↳14 CdtProblem
↳15 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 BOUNDS(1, 1)

(0) Obligation:

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


The TRS R consists of the following rules:

nolexicord(Nil, b1, a2, b2, a3, b3) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) → nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1), Cons(x, xs), b1, a2, b2, a3, b3)
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
goal(a1, b1, a2, b2, a3, b3) → nolexicord(a1, b1, a2, b2, a3, b3)

The (relative) TRS S consists of the following rules:

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
nolexicord[Ite][False][Ite](False, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs)) → nolexicord(xs', xs', xs', xs', xs', xs)
nolexicord[Ite][False][Ite](True, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs), Cons(x', xs')) → nolexicord(xs', xs', xs', xs', xs', xs)

Rewrite Strategy: INNERMOST

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

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

nolexicord(Nil, b1, a2, b2, a3, b3) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
nolexicord(Cons(x, xs), b1, a2, b2, a3, b3) → nolexicord[Ite][False][Ite](eqNatList(Cons(x, xs), b1), Cons(x, xs), b1, a2, b2, a3, b3)
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
goal(a1, b1, a2, b2, a3, b3) → nolexicord(a1, b1, a2, b2, a3, b3)
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
nolexicord[Ite][False][Ite](False, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs)) → nolexicord(xs', xs', xs', xs', xs', xs)
nolexicord[Ite][False][Ite](True, Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x', xs'), Cons(x, xs), Cons(x', xs')) → nolexicord(xs', xs', xs', xs', xs', xs)

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

nolexicord(Nil, z0, z1, z2, z3, z4) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
nolexicord(Cons(z0, z1), z2, z3, z4, z5, z6) → nolexicord[Ite][False][Ite](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6)
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
eqNatList(Nil, Cons(z0, z1)) → False
eqNatList(Nil, Nil) → True
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
goal(z0, z1, z2, z3, z4, z5) → nolexicord(z0, z1, z2, z3, z4, z5)
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
nolexicord[Ite][False][Ite](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → nolexicord(z1, z1, z1, z1, z1, z3)
nolexicord[Ite][False][Ite](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → nolexicord(z1, z1, z1, z1, z1, z3)
Tuples:

NOLEXICORD(Nil, z0, z1, z2, z3, z4) → c
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
EQNATLIST(Cons(z0, z1), Nil) → c3
EQNATLIST(Nil, Cons(z0, z1)) → c4
EQNATLIST(Nil, Nil) → c5
NUMBER42 → c6
GOAL(z0, z1, z2, z3, z4, z5) → c7(NOLEXICORD(z0, z1, z2, z3, z4, z5))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
!EQ'(0, S(z0)) → c9
!EQ'(S(z0), 0) → c10
!EQ'(0, 0) → c11
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
S tuples:

NOLEXICORD(Nil, z0, z1, z2, z3, z4) → c
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
EQNATLIST(Cons(z0, z1), Nil) → c3
EQNATLIST(Nil, Cons(z0, z1)) → c4
EQNATLIST(Nil, Nil) → c5
NUMBER42 → c6
GOAL(z0, z1, z2, z3, z4, z5) → c7(NOLEXICORD(z0, z1, z2, z3, z4, z5))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
!EQ'(0, S(z0)) → c9
!EQ'(S(z0), 0) → c10
!EQ'(0, 0) → c11
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
K tuples:none
Defined Rule Symbols:

nolexicord, eqNatList, number42, goal, !EQ, nolexicord[Ite][False][Ite]

Defined Pair Symbols:

NOLEXICORD, EQNATLIST, NUMBER42, GOAL, !EQ', NOLEXICORD[ITE][FALSE][ITE]

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1, z2, z3, z4, z5) → c7(NOLEXICORD(z0, z1, z2, z3, z4, z5))
Removed 8 trailing nodes:

NOLEXICORD(Nil, z0, z1, z2, z3, z4) → c
EQNATLIST(Nil, Nil) → c5
!EQ'(S(z0), 0) → c10
!EQ'(0, S(z0)) → c9
EQNATLIST(Nil, Cons(z0, z1)) → c4
NUMBER42 → c6
EQNATLIST(Cons(z0, z1), Nil) → c3
!EQ'(0, 0) → c11

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

nolexicord(Nil, z0, z1, z2, z3, z4) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
nolexicord(Cons(z0, z1), z2, z3, z4, z5, z6) → nolexicord[Ite][False][Ite](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6)
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
eqNatList(Nil, Cons(z0, z1)) → False
eqNatList(Nil, Nil) → True
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
goal(z0, z1, z2, z3, z4, z5) → nolexicord(z0, z1, z2, z3, z4, z5)
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
nolexicord[Ite][False][Ite](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → nolexicord(z1, z1, z1, z1, z1, z3)
nolexicord[Ite][False][Ite](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → nolexicord(z1, z1, z1, z1, z1, z3)
Tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
S tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
K tuples:none
Defined Rule Symbols:

nolexicord, eqNatList, number42, goal, !EQ, nolexicord[Ite][False][Ite]

Defined Pair Symbols:

NOLEXICORD, EQNATLIST, !EQ', NOLEXICORD[ITE][FALSE][ITE]

Compound Symbols:

c1, c2, c8, c12, c13

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

nolexicord(Nil, z0, z1, z2, z3, z4) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
nolexicord(Cons(z0, z1), z2, z3, z4, z5, z6) → nolexicord[Ite][False][Ite](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6)
eqNatList(Nil, Cons(z0, z1)) → False
eqNatList(Nil, Nil) → True
number42 → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
goal(z0, z1, z2, z3, z4, z5) → nolexicord(z0, z1, z2, z3, z4, z5)
nolexicord[Ite][False][Ite](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → nolexicord(z1, z1, z1, z1, z1, z3)
nolexicord[Ite][False][Ite](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → nolexicord(z1, z1, z1, z1, z1, z3)

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
S tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
K tuples:none
Defined Rule Symbols:

eqNatList, !EQ

Defined Pair Symbols:

NOLEXICORD, EQNATLIST, !EQ', NOLEXICORD[ITE][FALSE][ITE]

Compound Symbols:

c1, c2, c8, c12, c13

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

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

NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
We considered the (Usable) Rules:none
And the Tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = [1] + x1   
POL(!EQ'(x1, x2)) = 0   
POL(0) = [1]   
POL(Cons(x1, x2)) = [1] + x2   
POL(EQNATLIST(x1, x2)) = 0   
POL(False) = [1]   
POL(NOLEXICORD(x1, x2, x3, x4, x5, x6)) = x3   
POL(NOLEXICORD[ITE][FALSE][ITE](x1, x2, x3, x4, x5, x6, x7)) = x4   
POL(Nil) = 0   
POL(S(x1)) = [1] + x1   
POL(True) = [1]   
POL(c1(x1, x2)) = x1 + x2   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c2(x1)) = x1   
POL(c8(x1)) = x1   
POL(eqNatList(x1, x2)) = [1] + x1   
POL(eqNatList[Match][Cons][Match][Cons][Ite](x1, x2, x3, x4, x5)) = [1]   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
S tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
K tuples:

NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
Defined Rule Symbols:

eqNatList, !EQ

Defined Pair Symbols:

NOLEXICORD, EQNATLIST, !EQ', NOLEXICORD[ITE][FALSE][ITE]

Compound Symbols:

c1, c2, c8, c12, c13

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

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

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
S tuples:

!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
K tuples:

NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
Defined Rule Symbols:

eqNatList, !EQ

Defined Pair Symbols:

NOLEXICORD, EQNATLIST, !EQ', NOLEXICORD[ITE][FALSE][ITE]

Compound Symbols:

c1, c2, c8, c12, c13

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

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

!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = [2]x1 + x2 + [2]x22 + x1·x2   
POL(!EQ'(x1, x2)) = x2   
POL(0) = 0   
POL(Cons(x1, x2)) = [1] + x1 + x2   
POL(EQNATLIST(x1, x2)) = x2   
POL(False) = 0   
POL(NOLEXICORD(x1, x2, x3, x4, x5, x6)) = x2 + x5 + [2]x6 + x5·x6   
POL(NOLEXICORD[ITE][FALSE][ITE](x1, x2, x3, x4, x5, x6, x7)) = x6 + [2]x7 + x6·x7   
POL(Nil) = 0   
POL(S(x1)) = [1] + x1   
POL(True) = 0   
POL(c1(x1, x2)) = x1 + x2   
POL(c12(x1)) = x1   
POL(c13(x1)) = x1   
POL(c2(x1)) = x1   
POL(c8(x1)) = x1   
POL(eqNatList(x1, x2)) = 0   
POL(eqNatList[Match][Cons][Match][Cons][Ite](x1, x2, x3, x4, x5)) = 0   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
S tuples:none
K tuples:

NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c12(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c13(NOLEXICORD(z1, z1, z1, z1, z1, z3))
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c1(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c2(!EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c8(!EQ'(z0, z1))
Defined Rule Symbols:

eqNatList, !EQ

Defined Pair Symbols:

NOLEXICORD, EQNATLIST, !EQ', NOLEXICORD[ITE][FALSE][ITE]

Compound Symbols:

c1, c2, c8, c12, c13

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

The set S is empty

(16) BOUNDS(1, 1)