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 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CdtProblem
↳9 CdtUsableRulesProof (⇔, 0 ms)
↳10 CdtProblem
↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 219 ms)
↳12 CdtProblem
↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 49 ms)
↳14 CdtProblem
↳15 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CdtProblem
↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 479 ms)
↳18 CdtProblem
↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 257 ms)
↳20 CdtProblem
↳21 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳22 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:

prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), y, ys, x, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)

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

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, y, ys, x, xs) → False
eqNatList[Ite](True, y, ys, x, xs) → eqNatList(xs, ys)

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:

prefix(Cons(x', xs'), Cons(x, xs)) → and(!EQ(x', x), prefix(xs', xs))
domatch(Cons(x, xs), Nil, n) → Nil
domatch(Nil, Nil, n) → Cons(n, Nil)
prefix(Cons(x, xs), Nil) → False
prefix(Nil, cs) → True
domatch(patcs, Cons(x, xs), n) → domatch[Ite](prefix(patcs, Cons(x, xs)), patcs, Cons(x, xs), n)
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Ite](!EQ(x, y), y, ys, x, xs)
eqNatList(Cons(x, xs), Nil) → False
eqNatList(Nil, Cons(y, ys)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
strmatch(patstr, str) → domatch(patstr, str, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
domatch[Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil)))
domatch[Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))
eqNatList[Ite](False, y, ys, x, xs) → False
eqNatList[Ite](True, y, ys, x, xs) → eqNatList(xs, ys)

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

prefix(Cons(z0, z1), Cons(z2, z3)) → and(!EQ(z0, z2), prefix(z1, z3))
prefix(Cons(z0, z1), Nil) → False
prefix(Nil, z0) → True
domatch(Cons(z0, z1), Nil, z2) → Nil
domatch(Nil, Nil, z0) → Cons(z0, Nil)
domatch(z0, Cons(z1, z2), z3) → domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3)
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
eqNatList(Nil, Cons(z0, z1)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
strmatch(z0, z1) → domatch(z0, z1, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
domatch[Ite](False, z0, Cons(z1, z2), z3) → domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))
domatch[Ite](True, z0, Cons(z1, z2), z3) → Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil))))
eqNatList[Ite](False, z0, z1, z2, z3) → False
eqNatList[Ite](True, z0, z1, z2, z3) → eqNatList(z3, z1)
Tuples:

PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3))
PREFIX(Cons(z0, z1), Nil) → c1
PREFIX(Nil, z0) → c2
DOMATCH(Cons(z0, z1), Nil, z2) → c3
DOMATCH(Nil, Nil, z0) → c4
DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
EQNATLIST(Cons(z0, z1), Nil) → c7
EQNATLIST(Nil, Cons(z0, z1)) → c8
EQNATLIST(Nil, Nil) → c9
NOTEMPTY(Cons(z0, z1)) → c10
NOTEMPTY(Nil) → c11
STRMATCH(z0, z1) → c12(DOMATCH(z0, z1, Nil))
AND(False, False) → c13
AND(True, False) → c14
AND(False, True) → c15
AND(True, True) → c16
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
!EQ'(0, S(z0)) → c18
!EQ'(S(z0), 0) → c19
!EQ'(0, 0) → c20
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](False, z0, z1, z2, z3) → c23
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
S tuples:

PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3))
PREFIX(Cons(z0, z1), Nil) → c1
PREFIX(Nil, z0) → c2
DOMATCH(Cons(z0, z1), Nil, z2) → c3
DOMATCH(Nil, Nil, z0) → c4
DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
EQNATLIST(Cons(z0, z1), Nil) → c7
EQNATLIST(Nil, Cons(z0, z1)) → c8
EQNATLIST(Nil, Nil) → c9
NOTEMPTY(Cons(z0, z1)) → c10
NOTEMPTY(Nil) → c11
STRMATCH(z0, z1) → c12(DOMATCH(z0, z1, Nil))
AND(False, False) → c13
AND(True, False) → c14
AND(False, True) → c15
AND(True, True) → c16
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
!EQ'(0, S(z0)) → c18
!EQ'(S(z0), 0) → c19
!EQ'(0, 0) → c20
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](False, z0, z1, z2, z3) → c23
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
K tuples:none
Defined Rule Symbols:

prefix, domatch, eqNatList, notEmpty, strmatch, and, !EQ, domatch[Ite], eqNatList[Ite]

Defined Pair Symbols:

PREFIX, DOMATCH, EQNATLIST, NOTEMPTY, STRMATCH, AND, !EQ', DOMATCH[ITE], EQNATLIST[ITE]

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

STRMATCH(z0, z1) → c12(DOMATCH(z0, z1, Nil))
Removed 17 trailing nodes:

EQNATLIST(Cons(z0, z1), Nil) → c7
!EQ'(0, 0) → c20
!EQ'(0, S(z0)) → c18
AND(True, False) → c14
NOTEMPTY(Nil) → c11
AND(True, True) → c16
EQNATLIST(Nil, Nil) → c9
!EQ'(S(z0), 0) → c19
AND(False, True) → c15
EQNATLIST(Nil, Cons(z0, z1)) → c8
DOMATCH(Cons(z0, z1), Nil, z2) → c3
PREFIX(Cons(z0, z1), Nil) → c1
DOMATCH(Nil, Nil, z0) → c4
PREFIX(Nil, z0) → c2
AND(False, False) → c13
EQNATLIST[ITE](False, z0, z1, z2, z3) → c23
NOTEMPTY(Cons(z0, z1)) → c10

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

prefix(Cons(z0, z1), Cons(z2, z3)) → and(!EQ(z0, z2), prefix(z1, z3))
prefix(Cons(z0, z1), Nil) → False
prefix(Nil, z0) → True
domatch(Cons(z0, z1), Nil, z2) → Nil
domatch(Nil, Nil, z0) → Cons(z0, Nil)
domatch(z0, Cons(z1, z2), z3) → domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3)
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
eqNatList(Nil, Cons(z0, z1)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
strmatch(z0, z1) → domatch(z0, z1, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
domatch[Ite](False, z0, Cons(z1, z2), z3) → domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))
domatch[Ite](True, z0, Cons(z1, z2), z3) → Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil))))
eqNatList[Ite](False, z0, z1, z2, z3) → False
eqNatList[Ite](True, z0, z1, z2, z3) → eqNatList(z3, z1)
Tuples:

PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3))
DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
S tuples:

PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3))
DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
K tuples:none
Defined Rule Symbols:

prefix, domatch, eqNatList, notEmpty, strmatch, and, !EQ, domatch[Ite], eqNatList[Ite]

Defined Pair Symbols:

PREFIX, DOMATCH, EQNATLIST, !EQ', DOMATCH[ITE], EQNATLIST[ITE]

Compound Symbols:

c, c5, c6, c17, c21, c22, c24

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

Removed 1 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

prefix(Cons(z0, z1), Cons(z2, z3)) → and(!EQ(z0, z2), prefix(z1, z3))
prefix(Cons(z0, z1), Nil) → False
prefix(Nil, z0) → True
domatch(Cons(z0, z1), Nil, z2) → Nil
domatch(Nil, Nil, z0) → Cons(z0, Nil)
domatch(z0, Cons(z1, z2), z3) → domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3)
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
eqNatList(Nil, Cons(z0, z1)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
strmatch(z0, z1) → domatch(z0, z1, Nil)
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
domatch[Ite](False, z0, Cons(z1, z2), z3) → domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))
domatch[Ite](True, z0, Cons(z1, z2), z3) → Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil))))
eqNatList[Ite](False, z0, z1, z2, z3) → False
eqNatList[Ite](True, z0, z1, z2, z3) → eqNatList(z3, z1)
Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:none
Defined Rule Symbols:

prefix, domatch, eqNatList, notEmpty, strmatch, and, !EQ, domatch[Ite], eqNatList[Ite]

Defined Pair Symbols:

DOMATCH, EQNATLIST, !EQ', DOMATCH[ITE], EQNATLIST[ITE], PREFIX

Compound Symbols:

c5, c6, c17, c21, c22, c24, c

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

domatch(Cons(z0, z1), Nil, z2) → Nil
domatch(Nil, Nil, z0) → Cons(z0, Nil)
domatch(z0, Cons(z1, z2), z3) → domatch[Ite](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3)
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Ite](!EQ(z0, z2), z2, z3, z0, z1)
eqNatList(Cons(z0, z1), Nil) → False
eqNatList(Nil, Cons(z0, z1)) → False
eqNatList(Nil, Nil) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
strmatch(z0, z1) → domatch(z0, z1, Nil)
domatch[Ite](False, z0, Cons(z1, z2), z3) → domatch(z0, z2, Cons(z3, Cons(Nil, Nil)))
domatch[Ite](True, z0, Cons(z1, z2), z3) → Cons(z3, domatch(z0, z2, Cons(z3, Cons(Nil, Nil))))
eqNatList[Ite](False, z0, z1, z2, z3) → False
eqNatList[Ite](True, z0, z1, z2, z3) → eqNatList(z3, z1)

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

prefix(Cons(z0, z1), Cons(z2, z3)) → and(!EQ(z0, z2), prefix(z1, z3))
prefix(Nil, z0) → True
prefix(Cons(z0, z1), Nil) → False
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:none
Defined Rule Symbols:

prefix, and, !EQ

Defined Pair Symbols:

DOMATCH, EQNATLIST, !EQ', DOMATCH[ITE], EQNATLIST[ITE], PREFIX

Compound Symbols:

c5, c6, c17, c21, c22, c24, c

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

EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
We considered the (Usable) Rules:

!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, 0) → True
And the Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = x1 + x2   
POL(!EQ'(x1, x2)) = 0   
POL(0) = [1]   
POL(Cons(x1, x2)) = x1 + x2   
POL(DOMATCH(x1, x2, x3)) = 0   
POL(DOMATCH[ITE](x1, x2, x3, x4)) = 0   
POL(EQNATLIST(x1, x2)) = [1] + [2]x1 + x2   
POL(EQNATLIST[ITE](x1, x2, x3, x4, x5)) = x1 + x3 + x4 + [2]x5   
POL(False) = 0   
POL(Nil) = 0   
POL(PREFIX(x1, x2)) = 0   
POL(S(x1)) = [2] + x1   
POL(True) = [2]   
POL(and(x1, x2)) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c21(x1)) = x1   
POL(c22(x1)) = x1   
POL(c24(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1, x2)) = x1 + x2   
POL(prefix(x1, x2)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

prefix(Cons(z0, z1), Cons(z2, z3)) → and(!EQ(z0, z2), prefix(z1, z3))
prefix(Nil, z0) → True
prefix(Cons(z0, z1), Nil) → False
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:

EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
Defined Rule Symbols:

prefix, and, !EQ

Defined Pair Symbols:

DOMATCH, EQNATLIST, !EQ', DOMATCH[ITE], EQNATLIST[ITE], PREFIX

Compound Symbols:

c5, c6, c17, c21, c22, c24, c

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

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

DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
We considered the (Usable) Rules:none
And the Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = 0   
POL(!EQ'(x1, x2)) = 0   
POL(0) = 0   
POL(Cons(x1, x2)) = [1] + x2   
POL(DOMATCH(x1, x2, x3)) = x2   
POL(DOMATCH[ITE](x1, x2, x3, x4)) = x3   
POL(EQNATLIST(x1, x2)) = 0   
POL(EQNATLIST[ITE](x1, x2, x3, x4, x5)) = 0   
POL(False) = 0   
POL(Nil) = 0   
POL(PREFIX(x1, x2)) = 0   
POL(S(x1)) = 0   
POL(True) = 0   
POL(and(x1, x2)) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c21(x1)) = x1   
POL(c22(x1)) = x1   
POL(c24(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1, x2)) = x1 + x2   
POL(prefix(x1, x2)) = 0   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

prefix(Cons(z0, z1), Cons(z2, z3)) → and(!EQ(z0, z2), prefix(z1, z3))
prefix(Nil, z0) → True
prefix(Cons(z0, z1), Nil) → False
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:

EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
Defined Rule Symbols:

prefix, and, !EQ

Defined Pair Symbols:

DOMATCH, EQNATLIST, !EQ', DOMATCH[ITE], EQNATLIST[ITE], PREFIX

Compound Symbols:

c5, c6, c17, c21, c22, c24, c

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

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

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

prefix(Cons(z0, z1), Cons(z2, z3)) → and(!EQ(z0, z2), prefix(z1, z3))
prefix(Nil, z0) → True
prefix(Cons(z0, z1), Nil) → False
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:

!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:

EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
Defined Rule Symbols:

prefix, and, !EQ

Defined Pair Symbols:

DOMATCH, EQNATLIST, !EQ', DOMATCH[ITE], EQNATLIST[ITE], PREFIX

Compound Symbols:

c5, c6, c17, c21, c22, c24, c

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

PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
We considered the (Usable) Rules:none
And the Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = x1 + x2   
POL(!EQ'(x1, x2)) = [1]   
POL(0) = [2]   
POL(Cons(x1, x2)) = [2] + x2   
POL(DOMATCH(x1, x2, x3)) = [1] + [2]x1 + x2 + x1·x2 + x22   
POL(DOMATCH[ITE](x1, x2, x3, x4)) = x32 + x2·x3   
POL(EQNATLIST(x1, x2)) = [2]x1 + [2]x12   
POL(EQNATLIST[ITE](x1, x2, x3, x4, x5)) = [1] + [2]x5 + [2]x52   
POL(False) = 0   
POL(Nil) = 0   
POL(PREFIX(x1, x2)) = [1] + x2   
POL(S(x1)) = [1]   
POL(True) = 0   
POL(and(x1, x2)) = [1] + [2]x12   
POL(c(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c21(x1)) = x1   
POL(c22(x1)) = x1   
POL(c24(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1, x2)) = x1 + x2   
POL(prefix(x1, x2)) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

prefix(Cons(z0, z1), Cons(z2, z3)) → and(!EQ(z0, z2), prefix(z1, z3))
prefix(Nil, z0) → True
prefix(Cons(z0, z1), Nil) → False
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:

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

EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
Defined Rule Symbols:

prefix, and, !EQ

Defined Pair Symbols:

DOMATCH, EQNATLIST, !EQ', DOMATCH[ITE], EQNATLIST[ITE], PREFIX

Compound Symbols:

c5, c6, c17, c21, c22, c24, c

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

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

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = x2 + [2]x22   
POL(!EQ'(x1, x2)) = x1   
POL(0) = 0   
POL(Cons(x1, x2)) = [1] + x1 + x2   
POL(DOMATCH(x1, x2, x3)) = [2] + x1 + x12 + [2]x1·x2   
POL(DOMATCH[ITE](x1, x2, x3, x4)) = [2] + [2]x2·x3 + x22   
POL(EQNATLIST(x1, x2)) = [1] + [2]x1 + [2]x1·x2   
POL(EQNATLIST[ITE](x1, x2, x3, x4, x5)) = [1] + x2 + [2]x4 + [2]x5 + [2]x3·x5 + x2·x5 + x3·x4 + x2·x4   
POL(False) = 0   
POL(Nil) = 0   
POL(PREFIX(x1, x2)) = x1   
POL(S(x1)) = [1] + x1   
POL(True) = 0   
POL(and(x1, x2)) = [1] + x2 + [2]x1·x2 + x12   
POL(c(x1, x2)) = x1 + x2   
POL(c17(x1)) = x1   
POL(c21(x1)) = x1   
POL(c22(x1)) = x1   
POL(c24(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1, x2)) = x1 + x2   
POL(prefix(x1, x2)) = 0   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

prefix(Cons(z0, z1), Cons(z2, z3)) → and(!EQ(z0, z2), prefix(z1, z3))
prefix(Nil, z0) → True
prefix(Cons(z0, z1), Nil) → False
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(z0), S(z1)) → !EQ(z0, z1)
!EQ(0, S(z0)) → False
!EQ(S(z0), 0) → False
!EQ(0, 0) → True
Tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:none
K tuples:

EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c6(EQNATLIST[ITE](!EQ(z0, z2), z2, z3, z0, z1), !EQ'(z0, z2))
EQNATLIST[ITE](True, z0, z1, z2, z3) → c24(EQNATLIST(z3, z1))
DOMATCH[ITE](False, z0, Cons(z1, z2), z3) → c21(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH[ITE](True, z0, Cons(z1, z2), z3) → c22(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil))))
DOMATCH(z0, Cons(z1, z2), z3) → c5(DOMATCH[ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c(!EQ'(z0, z2), PREFIX(z1, z3))
!EQ'(S(z0), S(z1)) → c17(!EQ'(z0, z1))
Defined Rule Symbols:

prefix, and, !EQ

Defined Pair Symbols:

DOMATCH, EQNATLIST, !EQ', DOMATCH[ITE], EQNATLIST[ITE], PREFIX

Compound Symbols:

c5, c6, c17, c21, c22, c24, c

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

The set S is empty

(22) BOUNDS(1, 1)