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.760 CpxRelTRS9.08/2.76
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))9.08/2.76
↳2 CdtProblem9.08/2.76
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))9.08/2.76
↳4 CdtProblem9.08/2.76
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)9.08/2.76
↳6 CdtProblem9.08/2.76
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))9.08/2.76
↳8 CdtProblem9.08/2.76
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))9.08/2.76
↳10 CdtProblem9.08/2.76
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))9.08/2.76
↳12 BOUNDS(O(1), O(1))9.08/2.76
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)
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))))
Tuples:
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)
S 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))
K tuples:none
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))
prefix, domatch, eqNatList, notEmpty, strmatch, and, !EQ, domatch[Ite][True][Ite]
!EQ', DOMATCH[ITE][TRUE][ITE], PREFIX, DOMATCH, EQNATLIST, STRMATCH
c4, c8, c9, c10, c15, c16, c22
Tuples:
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)
S 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))
K tuples:none
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))
prefix, domatch, eqNatList, notEmpty, strmatch, and, !EQ, domatch[Ite][True][Ite]
!EQ', DOMATCH[ITE][TRUE][ITE], DOMATCH, EQNATLIST, STRMATCH, PREFIX
c4, c8, c9, c15, c16, c22, c10
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c16(!EQ'(z0, z2)) 9.08/2.77
STRMATCH(z0, z1) → c22(DOMATCH(z0, z1, Nil))
Tuples:
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)
S 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))
K tuples:none
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))
prefix, domatch, eqNatList, notEmpty, strmatch, and, !EQ, domatch[Ite][True][Ite]
!EQ', DOMATCH[ITE][TRUE][ITE], DOMATCH, PREFIX
c4, c8, c9, c15, c10
We considered the (Usable) Rules:
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)))
And the Tuples:
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
The order we found is given by the following interpretation:
!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))
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
Tuples:
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)
S 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))
K tuples:
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
Defined Rule Symbols:
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)))
prefix, domatch, eqNatList, notEmpty, strmatch, and, !EQ, domatch[Ite][True][Ite]
!EQ', DOMATCH[ITE][TRUE][ITE], DOMATCH, PREFIX
c4, c8, c9, c15, c10
We considered the (Usable) Rules:
PREFIX(Cons(z0, z1), Cons(z2, z3)) → c10(!EQ'(z0, z2), PREFIX(z1, z3))
And the Tuples:
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
The order we found is given by the following interpretation:
!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))
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
Tuples:
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)
S tuples:none
!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))
Defined Rule Symbols:
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))
prefix, domatch, eqNatList, notEmpty, strmatch, and, !EQ, domatch[Ite][True][Ite]
!EQ', DOMATCH[ITE][TRUE][ITE], DOMATCH, PREFIX
c4, c8, c9, c15, c10