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.88 5.49/1.88 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 5.49/1.88 5.49/1.88 5.49/1.88
5.49/1.88 5.49/1.88 5.49/1.88
5.49/1.88
5.49/1.88

(0) Obligation:

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

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)

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

!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

Rewrite Strategy: INNERMOST
5.49/1.88
5.49/1.88

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

Relative innermost TRS to CDT Problem.
5.49/1.88
5.49/1.88

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

!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)
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))
S tuples:

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
Defined Rule Symbols:

overlap, member, notEmpty, goal, !EQ, overlap[Ite][True][Ite], member[Ite][True][Ite]

Defined Pair Symbols:

!EQ', OVERLAP[ITE][TRUE][ITE], MEMBER[ITE][TRUE][ITE], OVERLAP, MEMBER, GOAL

Compound Symbols:

c, c4, c6, c8, c10, c14

5.49/1.89
5.49/1.89

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1) → c14(OVERLAP(z0, z1))
5.49/1.89
5.49/1.89

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

!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)
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))
S tuples:

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
Defined Rule Symbols:

overlap, member, notEmpty, goal, !EQ, overlap[Ite][True][Ite], member[Ite][True][Ite]

Defined Pair Symbols:

!EQ', OVERLAP[ITE][TRUE][ITE], MEMBER[ITE][TRUE][ITE], OVERLAP, MEMBER

Compound Symbols:

c, c4, c6, c8, c10

5.49/1.90
5.49/1.90

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

OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
We considered the (Usable) Rules:

!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
And the 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))
The order we found is given by the following interpretation:
Polynomial interpretation : 5.49/1.90

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   
5.49/1.90
5.49/1.90

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

!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)
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))
S tuples:

MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
K tuples:

OVERLAP(Cons(z0, z1), z2) → c8(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
Defined Rule Symbols:

overlap, member, notEmpty, goal, !EQ, overlap[Ite][True][Ite], member[Ite][True][Ite]

Defined Pair Symbols:

!EQ', OVERLAP[ITE][TRUE][ITE], MEMBER[ITE][TRUE][ITE], OVERLAP, MEMBER

Compound Symbols:

c, c4, c6, c8, c10

5.99/1.90
5.99/1.90

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

MEMBER(z0, Cons(z1, z2)) → c10(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
We considered the (Usable) Rules:

!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
And the 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))
The order we found is given by the following interpretation:
Polynomial interpretation : 5.99/1.90

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   
5.99/1.90
5.99/1.90

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

!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)
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))
S tuples:none
K tuples:

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, member, notEmpty, goal, !EQ, overlap[Ite][True][Ite], member[Ite][True][Ite]

Defined Pair Symbols:

!EQ', OVERLAP[ITE][TRUE][ITE], MEMBER[ITE][TRUE][ITE], OVERLAP, MEMBER

Compound Symbols:

c, c4, c6, c8, c10

5.99/1.90
5.99/1.90

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

The set S is empty
5.99/1.90
5.99/1.90

(10) BOUNDS(O(1), O(1))

5.99/1.90
5.99/1.90
5.99/1.96 EOF