YES(O(1), O(n^1)) 3.20/1.20 YES(O(1), O(n^1)) 3.20/1.29 3.20/1.29 3.20/1.29
3.20/1.29 3.20/1.290 CpxRelTRS3.20/1.29
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))3.20/1.29
↳2 CdtProblem3.20/1.29
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)3.20/1.29
↳4 CdtProblem3.20/1.29
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))3.20/1.29
↳6 CdtProblem3.20/1.29
↳7 CdtKnowledgeProof (⇔)3.20/1.29
↳8 BOUNDS(O(1), O(1))3.20/1.29
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)))))))))))))))))))))))))))))))))))))))))) 3.20/1.29
eqNatList(Cons(x, xs), Cons(y, ys)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(x, y), y, ys, x, xs) 3.20/1.29
eqNatList(Cons(x, xs), Nil) → False 3.20/1.29
eqNatList(Nil, Cons(y, ys)) → False 3.20/1.29
eqNatList(Nil, Nil) → True 3.20/1.29
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) 3.20/1.29
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)))))))))))))))))))))))))))))))))))))))))) 3.20/1.29
goal(a1, b1, a2, b2, a3, b3) → nolexicord(a1, b1, a2, b2, a3, b3)
!EQ(S(x), S(y)) → !EQ(x, y) 3.20/1.29
!EQ(0, S(y)) → False 3.20/1.29
!EQ(S(x), 0) → False 3.20/1.29
!EQ(0, 0) → True 3.20/1.29
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) 3.20/1.29
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)
Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 3.20/1.29
!EQ(0, S(z0)) → False 3.20/1.29
!EQ(S(z0), 0) → False 3.20/1.29
!EQ(0, 0) → True 3.20/1.29
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) 3.20/1.29
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) 3.20/1.29
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)))))))))))))))))))))))))))))))))))))))))) 3.20/1.29
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) 3.20/1.29
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1) 3.20/1.29
eqNatList(Cons(z0, z1), Nil) → False 3.20/1.29
eqNatList(Nil, Cons(z0, z1)) → False 3.20/1.29
eqNatList(Nil, Nil) → True 3.20/1.29
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)))))))))))))))))))))))))))))))))))))))))) 3.20/1.29
goal(z0, z1, z2, z3, z4, z5) → nolexicord(z0, z1, z2, z3, z4, z5)
S tuples:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 3.20/1.29
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c4(NOLEXICORD(z1, z1, z1, z1, z1, z3)) 3.20/1.29
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c5(NOLEXICORD(z1, z1, z1, z1, z1, z3)) 3.20/1.29
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c7(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2)) 3.20/1.29
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c8(!EQ'(z0, z2)) 3.20/1.29
GOAL(z0, z1, z2, z3, z4, z5) → c13(NOLEXICORD(z0, z1, z2, z3, z4, z5))
K tuples:none
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c7(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2)) 3.20/1.29
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c8(!EQ'(z0, z2)) 3.20/1.29
GOAL(z0, z1, z2, z3, z4, z5) → c13(NOLEXICORD(z0, z1, z2, z3, z4, z5))
nolexicord, eqNatList, number42, goal, !EQ, nolexicord[Ite][False][Ite]
!EQ', NOLEXICORD[ITE][FALSE][ITE], NOLEXICORD, EQNATLIST, GOAL
c, c4, c5, c7, c8, c13
GOAL(z0, z1, z2, z3, z4, z5) → c13(NOLEXICORD(z0, z1, z2, z3, z4, z5))
Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 3.20/1.29
!EQ(0, S(z0)) → False 3.20/1.29
!EQ(S(z0), 0) → False 3.20/1.29
!EQ(0, 0) → True 3.20/1.29
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) 3.20/1.29
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) 3.20/1.29
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)))))))))))))))))))))))))))))))))))))))))) 3.20/1.29
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) 3.20/1.29
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1) 3.20/1.29
eqNatList(Cons(z0, z1), Nil) → False 3.20/1.29
eqNatList(Nil, Cons(z0, z1)) → False 3.20/1.29
eqNatList(Nil, Nil) → True 3.20/1.29
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)))))))))))))))))))))))))))))))))))))))))) 3.20/1.29
goal(z0, z1, z2, z3, z4, z5) → nolexicord(z0, z1, z2, z3, z4, z5)
S tuples:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 3.20/1.29
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c4(NOLEXICORD(z1, z1, z1, z1, z1, z3)) 3.20/1.29
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c5(NOLEXICORD(z1, z1, z1, z1, z1, z3)) 3.20/1.29
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c7(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2)) 3.20/1.29
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c8(!EQ'(z0, z2))
K tuples:none
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c7(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2)) 3.20/1.29
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c8(!EQ'(z0, z2))
nolexicord, eqNatList, number42, goal, !EQ, nolexicord[Ite][False][Ite]
!EQ', NOLEXICORD[ITE][FALSE][ITE], NOLEXICORD, EQNATLIST
c, c4, c5, c7, c8
We considered the (Usable) Rules:
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c7(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
And the Tuples:
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1) 3.20/1.29
eqNatList(Cons(z0, z1), Nil) → False 3.20/1.29
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 3.20/1.29
!EQ(0, S(z0)) → False 3.20/1.29
!EQ(S(z0), 0) → False 3.20/1.29
!EQ(0, 0) → True
The order we found is given by the following interpretation:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 3.20/1.29
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c4(NOLEXICORD(z1, z1, z1, z1, z1, z3)) 3.20/1.29
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c5(NOLEXICORD(z1, z1, z1, z1, z1, z3)) 3.20/1.29
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c7(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2)) 3.20/1.29
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c8(!EQ'(z0, z2))
POL(!EQ(x1, x2)) = x2 3.20/1.29
POL(!EQ'(x1, x2)) = 0 3.20/1.29
POL(0) = 0 3.20/1.29
POL(Cons(x1, x2)) = [2] + x2 3.20/1.29
POL(EQNATLIST(x1, x2)) = 0 3.20/1.29
POL(False) = 0 3.20/1.29
POL(NOLEXICORD(x1, x2, x3, x4, x5, x6)) = [1] + [2]x2 3.20/1.29
POL(NOLEXICORD[ITE][FALSE][ITE](x1, x2, x3, x4, x5, x6, x7)) = [2]x3 3.20/1.29
POL(Nil) = [1] 3.20/1.29
POL(S(x1)) = [2] + x1 3.20/1.29
POL(True) = 0 3.20/1.29
POL(c(x1)) = x1 3.20/1.29
POL(c4(x1)) = x1 3.20/1.29
POL(c5(x1)) = x1 3.20/1.29
POL(c7(x1, x2)) = x1 + x2 3.20/1.29
POL(c8(x1)) = x1 3.20/1.29
POL(eqNatList(x1, x2)) = 0 3.20/1.29
POL(eqNatList[Match][Cons][Match][Cons][Ite](x1, x2, x3, x4, x5)) = [3] + x1 + x2 + x3 + x4 + x5
Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 3.20/1.29
!EQ(0, S(z0)) → False 3.20/1.29
!EQ(S(z0), 0) → False 3.20/1.29
!EQ(0, 0) → True 3.20/1.29
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) 3.20/1.29
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) 3.20/1.29
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)))))))))))))))))))))))))))))))))))))))))) 3.20/1.29
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) 3.20/1.29
eqNatList(Cons(z0, z1), Cons(z2, z3)) → eqNatList[Match][Cons][Match][Cons][Ite](!EQ(z0, z2), z2, z3, z0, z1) 3.20/1.29
eqNatList(Cons(z0, z1), Nil) → False 3.20/1.29
eqNatList(Nil, Cons(z0, z1)) → False 3.20/1.29
eqNatList(Nil, Nil) → True 3.20/1.29
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)))))))))))))))))))))))))))))))))))))))))) 3.20/1.29
goal(z0, z1, z2, z3, z4, z5) → nolexicord(z0, z1, z2, z3, z4, z5)
S tuples:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 3.20/1.29
NOLEXICORD[ITE][FALSE][ITE](False, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3)) → c4(NOLEXICORD(z1, z1, z1, z1, z1, z3)) 3.20/1.29
NOLEXICORD[ITE][FALSE][ITE](True, Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z0, z1), Cons(z2, z3), Cons(z0, z1)) → c5(NOLEXICORD(z1, z1, z1, z1, z1, z3)) 3.20/1.29
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c7(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2)) 3.20/1.29
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c8(!EQ'(z0, z2))
K tuples:
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c8(!EQ'(z0, z2))
Defined Rule Symbols:
NOLEXICORD(Cons(z0, z1), z2, z3, z4, z5, z6) → c7(NOLEXICORD[ITE][FALSE][ITE](eqNatList(Cons(z0, z1), z2), Cons(z0, z1), z2, z3, z4, z5, z6), EQNATLIST(Cons(z0, z1), z2))
nolexicord, eqNatList, number42, goal, !EQ, nolexicord[Ite][False][Ite]
!EQ', NOLEXICORD[ITE][FALSE][ITE], NOLEXICORD, EQNATLIST
c, c4, c5, c7, c8
Now S is empty
EQNATLIST(Cons(z0, z1), Cons(z2, z3)) → c8(!EQ'(z0, z2))