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.880 CpxRelTRS0.00/0.88
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))0.00/0.88
↳2 CdtProblem0.00/0.88
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.88
↳4 CdtProblem0.00/0.88
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.88
↳6 CdtProblem0.00/0.88
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.88
↳8 BOUNDS(O(1), O(1))0.00/0.88
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)
!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
Tuples:
!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)
S 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))
K tuples:none
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))
member, notEmpty, goal, !EQ, member[Ite][True][Ite]
!EQ', MEMBER[ITE][TRUE][ITE], MEMBER, GOAL
c, c4, c6, c10
GOAL(z0, z1) → c10(MEMBER(z0, z1))
Tuples:
!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)
S 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))
K tuples:none
MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
member, notEmpty, goal, !EQ, member[Ite][True][Ite]
!EQ', MEMBER[ITE][TRUE][ITE], MEMBER
c, c4, c6
We considered the (Usable) Rules:
MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
And the Tuples:
!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
The order we found is given by the following interpretation:
!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))
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
Tuples:
!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)
S tuples:none
!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))
Defined Rule Symbols:
MEMBER(z0, Cons(z1, z2)) → c6(MEMBER[ITE][TRUE][ITE](!EQ(z0, z1), z0, Cons(z1, z2)), !EQ'(z0, z1))
member, notEmpty, goal, !EQ, member[Ite][True][Ite]
!EQ', MEMBER[ITE][TRUE][ITE], MEMBER
c, c4, c6