YES(O(1), O(n^2)) 9.08/2.72 YES(O(1), O(n^2)) 9.08/2.76 9.08/2.76 9.08/2.76 9.08/2.76 9.08/2.76 9.08/2.76 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 9.08/2.76 9.08/2.76 9.08/2.76
9.08/2.76 9.08/2.76 9.08/2.76
9.08/2.76
9.08/2.76

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

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

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

and(False, False) → False 9.08/2.76
and(True, False) → False 9.08/2.76
and(False, True) → False 9.08/2.76
and(True, True) → True 9.08/2.76
!EQ(S(x), S(y)) → !EQ(x, y) 9.08/2.76
!EQ(0, S(y)) → False 9.08/2.76
!EQ(S(x), 0) → False 9.08/2.76
!EQ(0, 0) → True 9.08/2.77
domatch[Ite][True][Ite](False, patcs, Cons(x, xs), n) → domatch(patcs, xs, Cons(n, Cons(Nil, Nil))) 9.08/2.77
domatch[Ite][True][Ite](True, patcs, Cons(x, xs), n) → Cons(n, domatch(patcs, xs, Cons(n, Cons(Nil, Nil))))

Rewrite Strategy: INNERMOST
9.08/2.77
9.08/2.77

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
9.08/2.77
9.08/2.77

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 9.08/2.77
DOMATCH[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) → c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.77
DOMATCH[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) → c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.77
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3)) 9.08/2.77
DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.77
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c16(!EQ'(z0, z2)) 9.08/2.77
STRMATCH(z0, z1) → c22(DOMATCH(z0, z1, Nil))
S tuples:

PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(AND(!EQ(z0, z2), prefix(z1, z3)), !EQ'(z0, z2), PREFIX(z1, z3)) 9.08/2.77
DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.77
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c16(!EQ'(z0, z2)) 9.08/2.77
STRMATCH(z0, z1) → c22(DOMATCH(z0, z1, Nil))
K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c4, c8, c9, c10, c15, c16, c22

9.08/2.77
9.08/2.77

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

Removed 1 trailing tuple parts
9.08/2.77
9.08/2.77

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 9.08/2.77
DOMATCH[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) → c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.77
DOMATCH[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) → c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.77
DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.77
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c16(!EQ'(z0, z2)) 9.08/2.77
STRMATCH(z0, z1) → c22(DOMATCH(z0, z1, Nil)) 9.08/2.77
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.77
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c16(!EQ'(z0, z2)) 9.08/2.77
STRMATCH(z0, z1) → c22(DOMATCH(z0, z1, Nil)) 9.08/2.77
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c4, c8, c9, c15, c16, c22, c10

9.08/2.77
9.08/2.77

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c16(!EQ'(z0, z2)) 9.08/2.77
STRMATCH(z0, z1) → c22(DOMATCH(z0, z1, Nil))
9.08/2.77
9.08/2.77

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 9.08/2.78
DOMATCH[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) → c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.78
DOMATCH[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) → c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.78
DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.78
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.78
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c4, c8, c9, c15, c10

9.08/2.78
9.08/2.78

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
We considered the (Usable) Rules:

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

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 9.08/2.78
DOMATCH[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) → c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.78
DOMATCH[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) → c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.78
DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.78
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 9.08/2.78

POL(!EQ(x1, x2)) = 0    9.08/2.78
POL(!EQ'(x1, x2)) = 0    9.08/2.78
POL(0) = [3]    9.08/2.78
POL(Cons(x1, x2)) = [2] + x2    9.08/2.78
POL(DOMATCH(x1, x2, x3)) = [1] + [4]x2    9.08/2.78
POL(DOMATCH[ITE][TRUE][ITE](x1, x2, x3, x4)) = [4]x3    9.08/2.78
POL(False) = 0    9.08/2.78
POL(Nil) = 0    9.08/2.78
POL(PREFIX(x1, x2)) = 0    9.08/2.78
POL(S(x1)) = [3] + x1    9.08/2.78
POL(True) = 0    9.08/2.78
POL(and(x1, x2)) = [3]    9.08/2.78
POL(c10(x1, x2)) = x1 + x2    9.08/2.78
POL(c15(x1, x2)) = x1 + x2    9.08/2.78
POL(c4(x1)) = x1    9.08/2.78
POL(c8(x1)) = x1    9.08/2.78
POL(c9(x1)) = x1    9.08/2.78
POL(prefix(x1, x2)) = 0   
9.08/2.78
9.08/2.78

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 9.08/2.78
DOMATCH[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) → c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.78
DOMATCH[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) → c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.78
DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.78
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:

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

DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2)))
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c4, c8, c9, c15, c10

9.08/2.78
9.08/2.78

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
We considered the (Usable) Rules:

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

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 9.08/2.79
DOMATCH[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) → c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.79
DOMATCH[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) → c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.79
DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.79
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 9.08/2.79

POL(!EQ(x1, x2)) = 0    9.08/2.79
POL(!EQ'(x1, x2)) = 0    9.08/2.79
POL(0) = 0    9.08/2.79
POL(Cons(x1, x2)) = [2] + x2    9.08/2.79
POL(DOMATCH(x1, x2, x3)) = [2] + [3]x2 + x3 + [2]x22    9.08/2.79
POL(DOMATCH[ITE][TRUE][ITE](x1, x2, x3, x4)) = [1] + [2]x32    9.08/2.79
POL(False) = 0    9.08/2.79
POL(Nil) = 0    9.08/2.79
POL(PREFIX(x1, x2)) = [3] + x2    9.08/2.79
POL(S(x1)) = 0    9.08/2.79
POL(True) = 0    9.08/2.79
POL(and(x1, x2)) = [3]    9.08/2.79
POL(c10(x1, x2)) = x1 + x2    9.08/2.79
POL(c15(x1, x2)) = x1 + x2    9.08/2.79
POL(c4(x1)) = x1    9.08/2.79
POL(c8(x1)) = x1    9.08/2.79
POL(c9(x1)) = x1    9.08/2.79
POL(prefix(x1, x2)) = 0   
9.08/2.79
9.08/2.79

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 9.08/2.79
DOMATCH[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) → c8(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.79
DOMATCH[ITE][TRUE][ITE](True, z0, Cons(z1, z2), z3) → c9(DOMATCH(z0, z2, Cons(z3, Cons(Nil, Nil)))) 9.08/2.79
DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.79
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
S tuples:none
K tuples:

DOMATCH(z0, Cons(z1, z2), z3) → c15(DOMATCH[ITE][TRUE][ITE](prefix(z0, Cons(z1, z2)), z0, Cons(z1, z2), z3), PREFIX(z0, Cons(z1, z2))) 9.08/2.79
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c4, c8, c9, c15, c10

9.08/2.79
9.08/2.79

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

The set S is empty
9.08/2.79
9.08/2.79

(12) BOUNDS(O(1), O(1))

9.08/2.79
9.08/2.79
9.47/2.83 EOF