YES(O(1), O(n^2)) 5.49/1.86 YES(O(1), O(n^2)) 5.49/1.88 5.49/1.88 5.49/1.88
5.49/1.88 5.49/1.880 CpxRelTRS5.49/1.88
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))5.49/1.88
↳2 CdtProblem5.49/1.88
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)5.49/1.88
↳4 CdtProblem5.49/1.88
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))5.49/1.88
↳6 CdtProblem5.49/1.88
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))5.49/1.88
↳8 CdtProblem5.49/1.88
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))5.49/1.88
↳10 BOUNDS(O(1), O(1))5.49/1.88
overlap(Cons(x, xs), ys) → overlap[Ite][True][Ite](member(x, ys), Cons(x, xs), ys) 5.49/1.88
overlap(Nil, ys) → False 5.49/1.88
member(x', Cons(x, xs)) → member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs)) 5.49/1.88
member(x, Nil) → False 5.49/1.88
notEmpty(Cons(x, xs)) → True 5.49/1.88
notEmpty(Nil) → False 5.49/1.88
goal(xs, ys) → overlap(xs, ys)
!EQ(S(x), S(y)) → !EQ(x, y) 5.49/1.88
!EQ(0, S(y)) → False 5.49/1.88
!EQ(S(x), 0) → False 5.49/1.88
!EQ(0, 0) → True 5.49/1.88
overlap[Ite][True][Ite](False, Cons(x, xs), ys) → overlap(xs, ys) 5.49/1.88
member[Ite][True][Ite](False, x', Cons(x, xs)) → member(x', xs) 5.49/1.88
overlap[Ite][True][Ite](True, xs, ys) → True 5.49/1.88
member[Ite][True][Ite](True, x, xs) → True
Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 5.49/1.88
!EQ(0, S(z0)) → False 5.49/1.88
!EQ(S(z0), 0) → False 5.49/1.88
!EQ(0, 0) → True 5.49/1.88
overlap[Ite][True][Ite](False, Cons(z0, z1), z2) → overlap(z1, z2) 5.49/1.88
overlap[Ite][True][Ite](True, z0, z1) → True 5.49/1.89
member[Ite][True][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 5.49/1.89
member[Ite][True][Ite](True, z0, z1) → True 5.49/1.89
overlap(Cons(z0, z1), z2) → overlap[Ite][True][Ite](member(z0, z2), Cons(z0, z1), z2) 5.49/1.89
overlap(Nil, z0) → False 5.49/1.89
member(z0, Cons(z1, z2)) → member[Ite][True][Ite](!EQ(z1, z0), z0, Cons(z1, z2)) 5.49/1.89
member(z0, Nil) → False 5.49/1.89
notEmpty(Cons(z0, z1)) → True 5.49/1.89
notEmpty(Nil) → False 5.49/1.89
goal(z0, z1) → overlap(z0, z1)
S tuples:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 5.49/1.89
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c4(OVERLAP(z1, z2)) 5.49/1.89
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c6(MEMBER(z0, z2)) 5.49/1.89
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2)) 5.49/1.89
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0)) 5.49/1.89
GOAL(z0, z1) → c14(OVERLAP(z0, z1))
K tuples:none
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2)) 5.49/1.89
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0)) 5.49/1.89
GOAL(z0, z1) → c14(OVERLAP(z0, z1))
overlap, member, notEmpty, goal, !EQ, overlap[Ite][True][Ite], member[Ite][True][Ite]
!EQ', OVERLAP[ITE][TRUE][ITE], MEMBER[ITE][TRUE][ITE], OVERLAP, MEMBER, GOAL
c, c4, c6, c8, c10, c14
GOAL(z0, z1) → c14(OVERLAP(z0, z1))
Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 5.49/1.89
!EQ(0, S(z0)) → False 5.49/1.90
!EQ(S(z0), 0) → False 5.49/1.90
!EQ(0, 0) → True 5.49/1.90
overlap[Ite][True][Ite](False, Cons(z0, z1), z2) → overlap(z1, z2) 5.49/1.90
overlap[Ite][True][Ite](True, z0, z1) → True 5.49/1.90
member[Ite][True][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 5.49/1.90
member[Ite][True][Ite](True, z0, z1) → True 5.49/1.90
overlap(Cons(z0, z1), z2) → overlap[Ite][True][Ite](member(z0, z2), Cons(z0, z1), z2) 5.49/1.90
overlap(Nil, z0) → False 5.49/1.90
member(z0, Cons(z1, z2)) → member[Ite][True][Ite](!EQ(z1, z0), z0, Cons(z1, z2)) 5.49/1.90
member(z0, Nil) → False 5.49/1.90
notEmpty(Cons(z0, z1)) → True 5.49/1.90
notEmpty(Nil) → False 5.49/1.90
goal(z0, z1) → overlap(z0, z1)
S tuples:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 5.49/1.90
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c4(OVERLAP(z1, z2)) 5.49/1.90
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c6(MEMBER(z0, z2)) 5.49/1.90
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2)) 5.49/1.90
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
K tuples:none
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2)) 5.49/1.90
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
overlap, member, notEmpty, goal, !EQ, overlap[Ite][True][Ite], member[Ite][True][Ite]
!EQ', OVERLAP[ITE][TRUE][ITE], MEMBER[ITE][TRUE][ITE], OVERLAP, MEMBER
c, c4, c6, c8, c10
We considered the (Usable) Rules:
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
And the Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 5.49/1.90
!EQ(0, S(z0)) → False 5.49/1.90
!EQ(S(z0), 0) → False 5.49/1.90
!EQ(0, 0) → True 5.49/1.90
member(z0, Cons(z1, z2)) → member[Ite][True][Ite](!EQ(z1, z0), z0, Cons(z1, z2)) 5.49/1.90
member(z0, Nil) → False 5.49/1.90
member[Ite][True][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 5.49/1.90
member[Ite][True][Ite](True, z0, z1) → True
The order we found is given by the following interpretation:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 5.49/1.90
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c4(OVERLAP(z1, z2)) 5.49/1.90
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c6(MEMBER(z0, z2)) 5.49/1.90
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2)) 5.49/1.90
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
POL(!EQ(x1, x2)) = 0 5.49/1.90
POL(!EQ'(x1, x2)) = 0 5.49/1.90
POL(0) = [3] 5.49/1.90
POL(Cons(x1, x2)) = [4] + x2 5.49/1.90
POL(False) = [2] 5.49/1.90
POL(MEMBER(x1, x2)) = 0 5.49/1.90
POL(MEMBER[ITE][TRUE][ITE](x1, x2, x3)) = 0 5.49/1.90
POL(Nil) = 0 5.49/1.90
POL(OVERLAP(x1, x2)) = [1] + [4]x1 5.49/1.90
POL(OVERLAP[ITE][TRUE][ITE](x1, x2, x3)) = [4]x2 5.49/1.90
POL(S(x1)) = [3] + x1 5.49/1.90
POL(True) = 0 5.49/1.90
POL(c(x1)) = x1 5.49/1.90
POL(c10(x1, x2)) = x1 + x2 5.49/1.90
POL(c4(x1)) = x1 5.49/1.90
POL(c6(x1)) = x1 5.49/1.90
POL(c8(x1, x2)) = x1 + x2 5.49/1.90
POL(member(x1, x2)) = [4] + x2 5.49/1.90
POL(member[Ite][True][Ite](x1, x2, x3)) = [4] + x3
Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 5.49/1.90
!EQ(0, S(z0)) → False 5.49/1.90
!EQ(S(z0), 0) → False 5.49/1.90
!EQ(0, 0) → True 5.49/1.90
overlap[Ite][True][Ite](False, Cons(z0, z1), z2) → overlap(z1, z2) 5.99/1.90
overlap[Ite][True][Ite](True, z0, z1) → True 5.99/1.90
member[Ite][True][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 5.99/1.90
member[Ite][True][Ite](True, z0, z1) → True 5.99/1.90
overlap(Cons(z0, z1), z2) → overlap[Ite][True][Ite](member(z0, z2), Cons(z0, z1), z2) 5.99/1.90
overlap(Nil, z0) → False 5.99/1.90
member(z0, Cons(z1, z2)) → member[Ite][True][Ite](!EQ(z1, z0), z0, Cons(z1, z2)) 5.99/1.90
member(z0, Nil) → False 5.99/1.90
notEmpty(Cons(z0, z1)) → True 5.99/1.90
notEmpty(Nil) → False 5.99/1.90
goal(z0, z1) → overlap(z0, z1)
S tuples:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 5.99/1.90
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c4(OVERLAP(z1, z2)) 5.99/1.90
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c6(MEMBER(z0, z2)) 5.99/1.90
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2)) 5.99/1.90
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
K tuples:
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
Defined Rule Symbols:
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
overlap, member, notEmpty, goal, !EQ, overlap[Ite][True][Ite], member[Ite][True][Ite]
!EQ', OVERLAP[ITE][TRUE][ITE], MEMBER[ITE][TRUE][ITE], OVERLAP, MEMBER
c, c4, c6, c8, c10
We considered the (Usable) Rules:
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
And the Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 5.99/1.90
!EQ(0, S(z0)) → False 5.99/1.90
!EQ(S(z0), 0) → False 5.99/1.90
!EQ(0, 0) → True 5.99/1.90
member(z0, Cons(z1, z2)) → member[Ite][True][Ite](!EQ(z1, z0), z0, Cons(z1, z2)) 5.99/1.90
member(z0, Nil) → False 5.99/1.90
member[Ite][True][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 5.99/1.90
member[Ite][True][Ite](True, z0, z1) → True
The order we found is given by the following interpretation:
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 5.99/1.90
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c4(OVERLAP(z1, z2)) 5.99/1.90
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c6(MEMBER(z0, z2)) 5.99/1.90
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2)) 5.99/1.90
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
POL(!EQ(x1, x2)) = 0 5.99/1.90
POL(!EQ'(x1, x2)) = 0 5.99/1.90
POL(0) = 0 5.99/1.90
POL(Cons(x1, x2)) = [1] + x2 5.99/1.90
POL(False) = 0 5.99/1.90
POL(MEMBER(x1, x2)) = [2] + x2 5.99/1.90
POL(MEMBER[ITE][TRUE][ITE](x1, x2, x3)) = [1] + x3 5.99/1.90
POL(Nil) = 0 5.99/1.90
POL(OVERLAP(x1, x2)) = [1] + x1 + [2]x2 + [2]x1·x2 + x12 5.99/1.90
POL(OVERLAP[ITE][TRUE][ITE](x1, x2, x3)) = x3 + [2]x2·x3 + x22 5.99/1.90
POL(S(x1)) = 0 5.99/1.90
POL(True) = 0 5.99/1.90
POL(c(x1)) = x1 5.99/1.90
POL(c10(x1, x2)) = x1 + x2 5.99/1.90
POL(c4(x1)) = x1 5.99/1.90
POL(c6(x1)) = x1 5.99/1.90
POL(c8(x1, x2)) = x1 + x2 5.99/1.90
POL(member(x1, x2)) = 0 5.99/1.90
POL(member[Ite][True][Ite](x1, x2, x3)) = [3] + [3]x2 + [3]x3 + [3]x32 + [3]x2·x3 + [3]x22
Tuples:
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 5.99/1.90
!EQ(0, S(z0)) → False 5.99/1.90
!EQ(S(z0), 0) → False 5.99/1.90
!EQ(0, 0) → True 5.99/1.90
overlap[Ite][True][Ite](False, Cons(z0, z1), z2) → overlap(z1, z2) 5.99/1.90
overlap[Ite][True][Ite](True, z0, z1) → True 5.99/1.90
member[Ite][True][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 5.99/1.90
member[Ite][True][Ite](True, z0, z1) → True 5.99/1.90
overlap(Cons(z0, z1), z2) → overlap[Ite][True][Ite](member(z0, z2), Cons(z0, z1), z2) 5.99/1.90
overlap(Nil, z0) → False 5.99/1.90
member(z0, Cons(z1, z2)) → member[Ite][True][Ite](!EQ(z1, z0), z0, Cons(z1, z2)) 5.99/1.90
member(z0, Nil) → False 5.99/1.90
notEmpty(Cons(z0, z1)) → True 5.99/1.90
notEmpty(Nil) → False 5.99/1.90
goal(z0, z1) → overlap(z0, z1)
S tuples:none
!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 5.99/1.90
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c4(OVERLAP(z1, z2)) 5.99/1.90
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c6(MEMBER(z0, z2)) 5.99/1.90
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2)) 5.99/1.90
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
Defined Rule Symbols:
OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2)) 5.99/1.90
MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
overlap, member, notEmpty, goal, !EQ, overlap[Ite][True][Ite], member[Ite][True][Ite]
!EQ', OVERLAP[ITE][TRUE][ITE], MEMBER[ITE][TRUE][ITE], OVERLAP, MEMBER
c, c4, c6, c8, c10