The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^3).

0 CpxRelTRS
↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 13 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳6 CdtProblem
↳7 CdtUsableRulesProof (⇔, 0 ms)
↳8 CdtProblem
↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 195 ms)
↳10 CdtProblem
↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
↳12 CdtProblem
↳13 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 327 ms)
↳14 CdtProblem
↳15 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CdtProblem
↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)), 1447 ms)
↳18 CdtProblem
↳19 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳20 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

overlap(Cons(x, xs), ys) → overlap[Ite][True][Ite](member(x, ys), Cons(x, xs), ys)
overlap(Nil, ys) → False
member(x', Cons(x, xs)) → member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
member(x, Nil) → False
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
goal(xs, ys) → overlap(xs, ys)

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

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
overlap[Ite][True][Ite](False, Cons(x, xs), ys) → overlap(xs, ys)
member[Ite][True][Ite](False, x', Cons(x, xs)) → member(x', xs)
overlap[Ite][True][Ite](True, xs, ys) → True
member[Ite][True][Ite](True, x, xs) → True

Rewrite Strategy: INNERMOST

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

overlap(Cons(x, xs), ys) → overlap[Ite][True][Ite](member(x, ys), Cons(x, xs), ys)
overlap(Nil, ys) → False
member(x', Cons(x, xs)) → member[Ite][True][Ite](!EQ(x, x'), x', Cons(x, xs))
member(x, Nil) → False
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
goal(xs, ys) → overlap(xs, ys)
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
overlap[Ite][True][Ite](False, Cons(x, xs), ys) → overlap(xs, ys)
member[Ite][True][Ite](False, x', Cons(x, xs)) → member(x', xs)
overlap[Ite][True][Ite](True, xs, ys) → True
member[Ite][True][Ite](True, x, xs) → True

Rewrite Strategy: INNERMOST

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
OVERLAP(Nil, z0) → c1
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
MEMBER(z0, Nil) → c3
NOTEMPTY(Cons(z0, z1)) → c4
NOTEMPTY(Nil) → c5
GOAL(z0, z1) → c6(OVERLAP(z0, z1))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
!EQ'(0, S(z0)) → c8
!EQ'(S(z0), 0) → c9
!EQ'(0, 0) → c10
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
OVERLAP[ITE][TRUE][ITE](True, z0, z1) → c12
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
MEMBER[ITE][TRUE][ITE](True, z0, z1) → c14
S tuples:

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
OVERLAP(Nil, z0) → c1
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
MEMBER(z0, Nil) → c3
NOTEMPTY(Cons(z0, z1)) → c4
NOTEMPTY(Nil) → c5
GOAL(z0, z1) → c6(OVERLAP(z0, z1))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
!EQ'(0, S(z0)) → c8
!EQ'(S(z0), 0) → c9
!EQ'(0, 0) → c10
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
OVERLAP[ITE][TRUE][ITE](True, z0, z1) → c12
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
MEMBER[ITE][TRUE][ITE](True, z0, z1) → c14
K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1) → c6(OVERLAP(z0, z1))
Removed 9 trailing nodes:

NOTEMPTY(Nil) → c5
MEMBER(z0, Nil) → c3
NOTEMPTY(Cons(z0, z1)) → c4
OVERLAP(Nil, z0) → c1
OVERLAP[ITE][TRUE][ITE](True, z0, z1) → c12
MEMBER[ITE][TRUE][ITE](True, z0, z1) → c14
!EQ'(0, 0) → c10
!EQ'(0, S(z0)) → c8
!EQ'(S(z0), 0) → c9

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
S tuples:

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c7, c11, c13

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

overlap(Cons(z0, z1), z2) → overlap[Ite][True][Ite](member(z0, z2), Cons(z0, z1), z2)
overlap(Nil, z0) → False
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
goal(z0, z1) → overlap(z0, z1)
overlap[Ite][True][Ite](False, Cons(z0, z1), z2) → overlap(z1, z2)
overlap[Ite][True][Ite](True, z0, z1) → True

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
S tuples:

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
K tuples:none
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c7, c11, c13

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
We considered the (Usable) Rules:none
And the Tuples:

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = 0   
POL(!EQ'(x1, x2)) = 0   
POL(0) = 0   
POL(Cons(x1, x2)) = [1] + x2   
POL(False) = 0   
POL(MEMBER(x1, x2)) = 0   
POL(MEMBER[ITE][TRUE][ITE](x1, x2, x3)) = 0   
POL(Nil) = 0   
POL(OVERLAP(x1, x2)) = [1] + x1   
POL(OVERLAP[ITE][TRUE][ITE](x1, x2, x3)) = [1] + x2   
POL(S(x1)) = 0   
POL(True) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c13(x1)) = x1   
POL(c2(x1, x2)) = x1 + x2   
POL(c7(x1)) = x1   
POL(member(x1, x2)) = 0   
POL(member[Ite][True][Ite](x1, x2, x3)) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
S tuples:

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
K tuples:

OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c7, c11, c13

(11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
S tuples:

MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
K tuples:

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

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c7, c11, c13

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
We considered the (Usable) Rules:none
And the Tuples:

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = 0   
POL(!EQ'(x1, x2)) = 0   
POL(0) = 0   
POL(Cons(x1, x2)) = [2] + x2   
POL(False) = 0   
POL(MEMBER(x1, x2)) = [2]x2   
POL(MEMBER[ITE][TRUE][ITE](x1, x2, x3)) = [2]x3   
POL(Nil) = [1]   
POL(OVERLAP(x1, x2)) = [2]x2 + [2]x1·x2   
POL(OVERLAP[ITE][TRUE][ITE](x1, x2, x3)) = [2]x2·x3   
POL(S(x1)) = 0   
POL(True) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c13(x1)) = x1   
POL(c2(x1, x2)) = x1 + x2   
POL(c7(x1)) = x1   
POL(member(x1, x2)) = [2]   
POL(member[Ite][True][Ite](x1, x2, x3)) = [2] + x1 + x2 + x32 + [2]x2·x3 + [2]x1·x2 + x22   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
S tuples:

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

OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c7, c11, c13

(15) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
S tuples:

!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
K tuples:

OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c7, c11, c13

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(!EQ(x1, x2)) = 0   
POL(!EQ'(x1, x2)) = x1   
POL(0) = 0   
POL(Cons(x1, x2)) = [1] + x1 + x2   
POL(False) = 0   
POL(MEMBER(x1, x2)) = x2 + x22   
POL(MEMBER[ITE][TRUE][ITE](x1, x2, x3)) = [1] + x32   
POL(Nil) = 0   
POL(OVERLAP(x1, x2)) = x2 + x22 + x1·x2 + x12·x2 + x1·x22   
POL(OVERLAP[ITE][TRUE][ITE](x1, x2, x3)) = x22·x3 + x2·x32   
POL(S(x1)) = [1] + x1   
POL(True) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c11(x1)) = x1   
POL(c13(x1)) = x1   
POL(c2(x1, x2)) = x1 + x2   
POL(c7(x1)) = x1   
POL(member(x1, x2)) = 0   
POL(member[Ite][True][Ite](x1, x2, x3)) = 0   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
S tuples:none
K tuples:

OVERLAP[ITE][TRUE][ITE](False, Cons(z0, z1), z2) → c11(OVERLAP(z1, z2))
OVERLAP(Cons(z0, z1), z2) → c(OVERLAP[ITE][TRUE][ITE](member(z0, z2), Cons(z0, z1), z2), MEMBER(z0, z2))
MEMBER[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) → c13(MEMBER(z0, z2))
MEMBER(z0, Cons(z1, z2)) → c2(MEMBER[ITE][TRUE][ITE](!EQ(z1, z0), z0, Cons(z1, z2)), !EQ'(z1, z0))
!EQ'(S(z0), S(z1)) → c7(!EQ'(z0, z1))
Defined Rule Symbols:

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

Defined Pair Symbols:

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

Compound Symbols:

c, c2, c7, c11, c13

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

The set S is empty

(20) BOUNDS(1, 1)