YES(O(1), O(n^1)) 0.00/0.85 YES(O(1), O(n^1)) 0.00/0.88 0.00/0.88 0.00/0.88 0.00/0.88 0.00/0.88 0.00/0.88 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.88 0.00/0.88 0.00/0.88
0.00/0.88 0.00/0.88 0.00/0.88
0.00/0.88
0.00/0.88

(0) Obligation:

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

member(x', Cons(x, xs)) → member[Ite][True][Ite](!EQ(x', x), x', Cons(x, xs)) 0.00/0.88
member(x, Nil) → False 0.00/0.88
notEmpty(Cons(x, xs)) → True 0.00/0.88
notEmpty(Nil) → False 0.00/0.88
goal(x, xs) → member(x, xs)

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

!EQ(S(x), S(y)) → !EQ(x, y) 0.00/0.88
!EQ(0, S(y)) → False 0.00/0.88
!EQ(S(x), 0) → False 0.00/0.88
!EQ(0, 0) → True 0.00/0.88
member[Ite][True][Ite](False, x', Cons(x, xs)) → member(x', xs) 0.00/0.88
member[Ite][True][Ite](True, x, xs) → True

Rewrite Strategy: INNERMOST
0.00/0.88
0.00/0.88

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

Relative innermost TRS to CDT Problem.
0.00/0.88
0.00/0.88

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 0.00/0.88
!EQ(0, S(z0)) → False 0.00/0.88
!EQ(S(z0), 0) → False 0.00/0.88
!EQ(0, 0) → True 0.00/0.88
member[Ite][True][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 0.00/0.88
member[Ite][True][Ite](True, z0, z1) → True 0.00/0.88
member(z0, Cons(z1, z2)) → member[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2)) 0.00/0.88
member(z0, Nil) → False 0.00/0.88
notEmpty(Cons(z0, z1)) → True 0.00/0.88
notEmpty(Nil) → False 0.00/0.88
goal(z0, z1) → member(z0, z1)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 0.00/0.88
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c4(MEMBER(z0, z2)) 0.00/0.88
MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1)) 0.00/0.88
GOAL(z0, z1) → c10(MEMBER(z0, z1))
S tuples:

MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1)) 0.00/0.88
GOAL(z0, z1) → c10(MEMBER(z0, z1))
K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c4, c6, c10

0.00/0.88
0.00/0.88

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1) → c10(MEMBER(z0, z1))
0.00/0.88
0.00/0.88

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 0.00/0.88
!EQ(0, S(z0)) → False 0.00/0.88
!EQ(S(z0), 0) → False 0.00/0.88
!EQ(0, 0) → True 0.00/0.88
member[Ite][True][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 0.00/0.88
member[Ite][True][Ite](True, z0, z1) → True 0.00/0.88
member(z0, Cons(z1, z2)) → member[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2)) 0.00/0.88
member(z0, Nil) → False 0.00/0.88
notEmpty(Cons(z0, z1)) → True 0.00/0.88
notEmpty(Nil) → False 0.00/0.88
goal(z0, z1) → member(z0, z1)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 0.00/0.88
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c4(MEMBER(z0, z2)) 0.00/0.88
MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
S tuples:

MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c4, c6

0.00/0.88
0.00/0.88

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

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

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 0.00/0.88
!EQ(0, S(z0)) → False 0.00/0.88
!EQ(S(z0), 0) → False 0.00/0.88
!EQ(0, 0) → True
And the Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 0.00/0.88
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c4(MEMBER(z0, z2)) 0.00/0.88
MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 0.00/0.88

POL(!EQ(x1, x2)) = 0    0.00/0.88
POL(!EQ'(x1, x2)) = 0    0.00/0.88
POL(0) = [3]    0.00/0.88
POL(Cons(x1, x2)) = [1] + x2    0.00/0.88
POL(False) = 0    0.00/0.88
POL(MEMBER(x1, x2)) = [1] + [4]x2    0.00/0.88
POL(MEMBER[ITE][TRUE][ITE](x1, x2, x3)) = [4]x3    0.00/0.88
POL(S(x1)) = [3] + x1    0.00/0.88
POL(True) = [3]    0.00/0.88
POL(c(x1)) = x1    0.00/0.88
POL(c4(x1)) = x1    0.00/0.88
POL(c6(x1, x2)) = x1 + x2   
0.00/0.88
0.00/0.88

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 0.00/0.88
!EQ(0, S(z0)) → False 0.00/0.88
!EQ(S(z0), 0) → False 0.00/0.88
!EQ(0, 0) → True 0.00/0.88
member[Ite][True][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 0.00/0.88
member[Ite][True][Ite](True, z0, z1) → True 0.00/0.88
member(z0, Cons(z1, z2)) → member[Ite][True][Ite](!EQ(z0, z1), z0, Cons(z1, z2)) 0.00/0.88
member(z0, Nil) → False 0.00/0.88
notEmpty(Cons(z0, z1)) → True 0.00/0.88
notEmpty(Nil) → False 0.00/0.88
goal(z0, z1) → member(z0, z1)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 0.00/0.88
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c4(MEMBER(z0, z2)) 0.00/0.88
MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
S tuples:none
K tuples:

MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c4, c6

0.00/0.88
0.00/0.88

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

The set S is empty
0.00/0.88
0.00/0.88

(8) BOUNDS(O(1), O(1))

0.00/0.88
0.00/0.88
0.00/0.90 EOF