YES(O(1), O(n^1)) 84.34/33.71 YES(O(1), O(n^1)) 84.34/33.74 84.34/33.74 84.34/33.74 84.34/33.74 84.34/33.74 84.34/33.74 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 84.34/33.74 84.34/33.74 84.34/33.74
84.34/33.74
84.34/33.74
84.34/33.74
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxRelTRS
84.34/33.74 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
84.34/33.74 
↳2 CdtProblem
84.34/33.74 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳4 CdtProblem
84.34/33.74 
↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳6 CdtProblem
84.34/33.74 
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)
84.34/33.74 
↳8 CdtProblem
84.34/33.74 
↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳10 CdtProblem
84.34/33.74 
↳11 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳12 CdtProblem
84.34/33.74 
↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳14 CdtProblem
84.34/33.74 
↳15 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳16 CdtProblem
84.34/33.74 
↳17 CdtLeafRemovalProof (ComplexityIfPolyImplication)
84.34/33.74 
↳18 CdtProblem
84.34/33.74 
↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳20 CdtProblem
84.34/33.74 
↳21 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳22 CdtProblem
84.34/33.74 
↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
84.34/33.74 
↳24 CdtProblem
84.34/33.74 
↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
84.34/33.74 
↳26 CdtProblem
84.34/33.74 
↳27 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
84.34/33.74 
↳28 CdtProblem
84.34/33.74 
↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
84.34/33.74 
↳30 CdtProblem
84.34/33.74 
↳31 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳32 CdtProblem
84.34/33.74 
↳33 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
84.34/33.74 
↳34 CdtProblem
84.34/33.74 
↳35 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳36 CdtProblem
84.34/33.74 
↳37 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳38 CdtProblem
84.34/33.74 
↳39 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
84.34/33.74 
↳40 CdtProblem
84.34/33.74 
↳41 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
84.34/33.74 
↳42 CdtProblem
84.34/33.74 
↳43 SIsEmptyProof (BOTH BOUNDS(ID, ID))
84.34/33.74 
↳44 BOUNDS(O(1), O(1))
84.34/33.74
84.34/33.74 84.34/33.74
84.34/33.74
84.34/33.74

(0) Obligation:

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

getNodeFromEdge(S(S(x')), E(x, y)) → y 84.34/33.74
via(u, v, Cons(E(x, y), xs), edges) → via[Ite][False][Ite](!EQ(u, x), u, v, Cons(E(x, y), xs), edges) 84.34/33.74
getNodeFromEdge(S(0), E(x, y)) → x 84.34/33.74
member(x', Cons(x, xs)) → member[Ite][False][Ite](eqEdge(x', x), x', Cons(x, xs)) 84.34/33.74
getNodeFromEdge(0, E(x, y)) → x 84.34/33.74
eqEdge(E(e11, e12), E(e21, e22)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(e11, e21), !EQ(e12, e22)), e21, e22, e11, e12) 84.34/33.74
via(u, v, Nil, edges) → Nil 84.34/33.74
notEmpty(Cons(x, xs)) → True 84.34/33.74
notEmpty(Nil) → False 84.34/33.74
member(x, Nil) → False 84.34/33.74
reach(u, v, edges) → reach[Ite](member(E(u, v), edges), u, v, edges) 84.34/33.74
goal(u, v, edges) → reach(u, v, edges)

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

!EQ(S(x), S(y)) → !EQ(x, y) 84.34/33.74
!EQ(0, S(y)) → False 84.34/33.74
!EQ(S(x), 0) → False 84.34/33.74
!EQ(0, 0) → True 84.34/33.74
and(False, False) → False 84.34/33.74
and(True, False) → False 84.34/33.74
and(False, True) → False 84.34/33.74
and(True, True) → True 84.34/33.74
via[Ite][False][Ite](True, u, v, Cons(E(x, y), xs), edges) → via[Ite][False][Ite][True][Let](u, v, Cons(E(x, y), xs), edges, reach(y, v, edges)) 84.34/33.74
via[Ite][False][Ite](False, u, v, Cons(x, xs), edges) → via(u, v, xs, edges) 84.34/33.74
member[Ite][False][Ite](False, x', Cons(x, xs)) → member(x', xs) 84.34/33.74
reach[Ite](False, u, v, edges) → via(u, v, edges, edges) 84.34/33.74
reach[Ite](True, u, v, edges) → Cons(E(u, v), Nil) 84.34/33.74
member[Ite][False][Ite](True, x, xs) → True

Rewrite Strategy: INNERMOST
84.34/33.74
84.34/33.74

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

Relative innermost TRS to CDT Problem.
84.34/33.74
84.34/33.74

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 84.34/33.74
!EQ(0, S(z0)) → False 84.34/33.74
!EQ(S(z0), 0) → False 84.34/33.74
!EQ(0, 0) → True 84.34/33.74
and(False, False) → False 84.34/33.74
and(True, False) → False 84.34/33.74
and(False, True) → False 84.34/33.74
and(True, True) → True 84.34/33.74
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 84.34/33.79
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 84.34/33.79
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 84.34/33.79
member[Ite][False][Ite](True, z0, z1) → True 84.34/33.79
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 84.34/33.79
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 84.34/33.79
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 84.34/33.79
getNodeFromEdge(S(0), E(z0, z1)) → z0 84.34/33.79
getNodeFromEdge(0, E(z0, z1)) → z0 84.34/33.79
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 84.34/33.79
via(z0, z1, Nil, z2) → Nil 84.34/33.79
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 84.34/33.79
member(z0, Nil) → False 84.34/33.79
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 84.34/33.79
notEmpty(Cons(z0, z1)) → True 84.34/33.79
notEmpty(Nil) → False 84.34/33.79
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 84.34/33.79
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 84.34/33.79
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 84.34/33.79
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 84.34/33.79
MEMBER[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c10(MEMBER(z0, z2)) 84.34/33.79
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 84.34/33.79
VIA(z0, z1, Cons(E(z2, z3), z4), z5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2)) 84.34/33.79
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 84.34/33.79
EQEDGE(E(z0, z1), E(z2, z3)) → c21(AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2), !EQ'(z1, z3)) 84.34/33.79
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 84.34/33.79
GOAL(z0, z1, z2) → c25(REACH(z0, z1, z2))
S tuples:

VIA(z0, z1, Cons(E(z2, z3), z4), z5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2)) 84.34/33.79
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 84.34/33.79
EQEDGE(E(z0, z1), E(z2, z3)) → c21(AND(!EQ(z0, z2), !EQ(z1, z3)), !EQ'(z0, z2), !EQ'(z1, z3)) 84.34/33.79
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 84.34/33.79
GOAL(z0, z1, z2) → c25(REACH(z0, z1, z2))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], MEMBER[ITE][FALSE][ITE], REACH[ITE], VIA, MEMBER, EQEDGE, REACH, GOAL

Compound Symbols:

c, c8, c9, c10, c12, c17, c19, c21, c24, c25

84.34/33.79
84.34/33.79

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

Removed 1 trailing tuple parts
84.34/33.79
84.34/33.79

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 84.34/33.79
!EQ(0, S(z0)) → False 84.34/33.79
!EQ(S(z0), 0) → False 84.34/33.79
!EQ(0, 0) → True 84.34/33.79
and(False, False) → False 84.34/33.79
and(True, False) → False 84.34/33.79
and(False, True) → False 84.34/33.79
and(True, True) → True 84.34/33.79
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 84.34/33.79
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 84.34/33.79
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 84.34/33.79
member[Ite][False][Ite](True, z0, z1) → True 84.34/33.79
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 84.34/33.79
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 84.34/33.79
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 84.34/33.79
getNodeFromEdge(S(0), E(z0, z1)) → z0 84.34/33.79
getNodeFromEdge(0, E(z0, z1)) → z0 84.34/33.79
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 84.34/33.79
via(z0, z1, Nil, z2) → Nil 84.34/33.79
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 84.34/33.79
member(z0, Nil) → False 84.34/33.79
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 84.34/33.79
notEmpty(Cons(z0, z1)) → True 84.34/33.79
notEmpty(Nil) → False 84.34/33.79
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 84.34/33.79
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 84.34/33.79
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.91
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.91
MEMBER[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c10(MEMBER(z0, z2)) 85.12/33.91
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.91
VIA(z0, z1, Cons(E(z2, z3), z4), z5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2)) 85.12/33.91
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
GOAL(z0, z1, z2) → c25(REACH(z0, z1, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c21(!EQ'(z0, z2), !EQ'(z1, z3))
S tuples:

VIA(z0, z1, Cons(E(z2, z3), z4), z5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2)) 85.12/33.91
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
GOAL(z0, z1, z2) → c25(REACH(z0, z1, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c21(!EQ'(z0, z2), !EQ'(z1, z3))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], MEMBER[ITE][FALSE][ITE], REACH[ITE], VIA, MEMBER, REACH, GOAL, EQEDGE

Compound Symbols:

c, c8, c9, c10, c12, c17, c19, c24, c25, c21

85.12/33.91
85.12/33.91

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC
85.12/33.91
85.12/33.91

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.91
!EQ(0, S(z0)) → False 85.12/33.91
!EQ(S(z0), 0) → False 85.12/33.91
!EQ(0, 0) → True 85.12/33.91
and(False, False) → False 85.12/33.91
and(True, False) → False 85.12/33.91
and(False, True) → False 85.12/33.91
and(True, True) → True 85.12/33.91
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.91
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.91
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.91
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.91
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.91
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.91
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.91
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.91
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.91
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.91
via(z0, z1, Nil, z2) → Nil 85.12/33.91
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.91
member(z0, Nil) → False 85.12/33.91
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.91
notEmpty(Cons(z0, z1)) → True 85.12/33.91
notEmpty(Nil) → False 85.12/33.91
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.91
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.91
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.91
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.91
MEMBER[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c10(MEMBER(z0, z2)) 85.12/33.91
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.91
VIA(z0, z1, Cons(E(z2, z3), z4), z5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2)) 85.12/33.91
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
GOAL(z0, z1, z2) → c25(REACH(z0, z1, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3))
S tuples:

VIA(z0, z1, Cons(E(z2, z3), z4), z5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2)) 85.12/33.91
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
GOAL(z0, z1, z2) → c25(REACH(z0, z1, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], MEMBER[ITE][FALSE][ITE], REACH[ITE], VIA, MEMBER, REACH, GOAL, EQEDGE

Compound Symbols:

c, c8, c9, c10, c12, c17, c19, c24, c25, c1

85.12/33.91
85.12/33.91

(7) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1, z2) → c25(REACH(z0, z1, z2))
85.12/33.91
85.12/33.91

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.91
!EQ(0, S(z0)) → False 85.12/33.91
!EQ(S(z0), 0) → False 85.12/33.91
!EQ(0, 0) → True 85.12/33.91
and(False, False) → False 85.12/33.91
and(True, False) → False 85.12/33.91
and(False, True) → False 85.12/33.91
and(True, True) → True 85.12/33.91
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.91
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.91
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.91
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.91
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.91
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.91
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.91
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.91
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.91
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.91
via(z0, z1, Nil, z2) → Nil 85.12/33.91
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.91
member(z0, Nil) → False 85.12/33.91
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.91
notEmpty(Cons(z0, z1)) → True 85.12/33.91
notEmpty(Nil) → False 85.12/33.91
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.91
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.91
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.91
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.91
MEMBER[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c10(MEMBER(z0, z2)) 85.12/33.91
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.91
VIA(z0, z1, Cons(E(z2, z3), z4), z5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2)) 85.12/33.91
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3))
S tuples:

VIA(z0, z1, Cons(E(z2, z3), z4), z5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2)) 85.12/33.91
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], MEMBER[ITE][FALSE][ITE], REACH[ITE], VIA, MEMBER, REACH, EQEDGE

Compound Symbols:

c, c8, c9, c10, c12, c17, c19, c24, c1

85.12/33.91
85.12/33.91

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

Use narrowing to replace VIA(z0, z1, Cons(E(z2, z3), z4), z5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5), !EQ'(z0, z2)) by

VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5), !EQ'(0, S(z0))) 85.12/33.91
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5), !EQ'(S(z0), 0)) 85.12/33.91
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5), !EQ'(0, 0))
85.12/33.91
85.12/33.91

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.91
!EQ(0, S(z0)) → False 85.12/33.91
!EQ(S(z0), 0) → False 85.12/33.91
!EQ(0, 0) → True 85.12/33.91
and(False, False) → False 85.12/33.91
and(True, False) → False 85.12/33.91
and(False, True) → False 85.12/33.91
and(True, True) → True 85.12/33.91
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.91
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.91
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.91
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.91
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.91
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.91
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.91
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.91
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.91
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.91
via(z0, z1, Nil, z2) → Nil 85.12/33.91
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.91
member(z0, Nil) → False 85.12/33.91
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.91
notEmpty(Cons(z0, z1)) → True 85.12/33.91
notEmpty(Nil) → False 85.12/33.91
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.91
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.91
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.91
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.91
MEMBER[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c10(MEMBER(z0, z2)) 85.12/33.91
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.91
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.91
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5), !EQ'(0, S(z0))) 85.12/33.91
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5), !EQ'(S(z0), 0)) 85.12/33.91
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5), !EQ'(0, 0))
S tuples:

MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.91
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5), !EQ'(0, S(z0))) 85.12/33.91
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5), !EQ'(S(z0), 0)) 85.12/33.91
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5), !EQ'(0, 0))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], MEMBER[ITE][FALSE][ITE], REACH[ITE], MEMBER, REACH, EQEDGE, VIA

Compound Symbols:

c, c8, c9, c10, c12, c19, c24, c1, c17

85.12/33.91
85.12/33.91

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

Removed 3 trailing tuple parts
85.12/33.91
85.12/33.91

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.91
!EQ(0, S(z0)) → False 85.12/33.91
!EQ(S(z0), 0) → False 85.12/33.91
!EQ(0, 0) → True 85.12/33.91
and(False, False) → False 85.12/33.91
and(True, False) → False 85.12/33.91
and(False, True) → False 85.12/33.91
and(True, True) → True 85.12/33.91
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.91
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.91
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.91
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.91
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.91
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.91
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.91
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.91
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.91
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.91
via(z0, z1, Nil, z2) → Nil 85.12/33.91
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.91
member(z0, Nil) → False 85.12/33.91
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.91
notEmpty(Cons(z0, z1)) → True 85.12/33.91
notEmpty(Nil) → False 85.12/33.91
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.91
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.91
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.91
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.91
MEMBER[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c10(MEMBER(z0, z2)) 85.12/33.91
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.91
MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.91
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.91
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5))
S tuples:

MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.91
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.91
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], MEMBER[ITE][FALSE][ITE], REACH[ITE], MEMBER, REACH, EQEDGE, VIA

Compound Symbols:

c, c8, c9, c10, c12, c19, c24, c1, c17, c17

85.12/33.91
85.12/33.91

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MEMBER(z0, Cons(z1, z2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge(z0, z1), z0, Cons(z1, z2)), EQEDGE(z0, z1)) by

MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), E(z0, z1), Cons(E(z2, z3), x2)), EQEDGE(E(z0, z1), E(z2, z3)))
85.12/33.91
85.12/33.91

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.91
!EQ(0, S(z0)) → False 85.12/33.91
!EQ(S(z0), 0) → False 85.12/33.91
!EQ(0, 0) → True 85.12/33.91
and(False, False) → False 85.12/33.91
and(True, False) → False 85.12/33.91
and(False, True) → False 85.12/33.91
and(True, True) → True 85.12/33.91
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.91
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.91
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.91
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.91
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.91
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.91
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.91
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.91
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.91
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.91
via(z0, z1, Nil, z2) → Nil 85.12/33.91
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.91
member(z0, Nil) → False 85.12/33.91
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.91
notEmpty(Cons(z0, z1)) → True 85.12/33.91
notEmpty(Nil) → False 85.12/33.91
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.91
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.91
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.91
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.91
MEMBER[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c10(MEMBER(z0, z2)) 85.12/33.91
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.91
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.91
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), E(z0, z1), Cons(E(z2, z3), x2)), EQEDGE(E(z0, z1), E(z2, z3)))
S tuples:

REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.91
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.91
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(MEMBER[ITE][FALSE][ITE](eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), E(z0, z1), Cons(E(z2, z3), x2)), EQEDGE(E(z0, z1), E(z2, z3)))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], MEMBER[ITE][FALSE][ITE], REACH[ITE], REACH, EQEDGE, VIA, MEMBER

Compound Symbols:

c, c8, c9, c10, c12, c24, c1, c17, c17, c19

85.12/33.91
85.12/33.91

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

Removed 1 trailing tuple parts
85.12/33.91
85.12/33.91

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.91
!EQ(0, S(z0)) → False 85.12/33.91
!EQ(S(z0), 0) → False 85.12/33.91
!EQ(0, 0) → True 85.12/33.91
and(False, False) → False 85.12/33.91
and(True, False) → False 85.12/33.91
and(False, True) → False 85.12/33.91
and(True, True) → True 85.12/33.91
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.91
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.91
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.91
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.91
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.91
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.91
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.91
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.91
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.91
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.91
via(z0, z1, Nil, z2) → Nil 85.12/33.91
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.91
member(z0, Nil) → False 85.12/33.91
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.91
notEmpty(Cons(z0, z1)) → True 85.12/33.91
notEmpty(Nil) → False 85.12/33.91
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.91
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.91
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.91
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.91
MEMBER[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c10(MEMBER(z0, z2)) 85.12/33.91
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.91
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.91
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3)))
S tuples:

REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.91
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.91
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.91
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3)))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], MEMBER[ITE][FALSE][ITE], REACH[ITE], REACH, EQEDGE, VIA, MEMBER

Compound Symbols:

c, c8, c9, c10, c12, c24, c1, c17, c17, c19

85.12/33.91
85.12/33.91

(17) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

MEMBER[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c10(MEMBER(z0, z2))
85.12/33.91
85.12/33.91

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.91
!EQ(0, S(z0)) → False 85.12/33.91
!EQ(S(z0), 0) → False 85.12/33.91
!EQ(0, 0) → True 85.12/33.91
and(False, False) → False 85.12/33.91
and(True, False) → False 85.12/33.91
and(False, True) → False 85.12/33.91
and(True, True) → True 85.12/33.91
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.91
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.91
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.91
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.91
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.91
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.91
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.91
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.91
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.91
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.91
via(z0, z1, Nil, z2) → Nil 85.12/33.91
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.91
member(z0, Nil) → False 85.12/33.91
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.91
notEmpty(Cons(z0, z1)) → True 85.12/33.91
notEmpty(Nil) → False 85.12/33.91
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.91
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.91
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.91
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.91
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.91
REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.91
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.91
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.91
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.93
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.93
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.93
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3)))
S tuples:

REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) 85.12/33.93
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.93
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.93
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.93
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.93
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.93
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.93
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3)))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], REACH, EQEDGE, VIA, MEMBER

Compound Symbols:

c, c8, c9, c12, c24, c1, c17, c17, c19

85.12/33.93
85.12/33.93

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

Use narrowing to replace REACH(z0, z1, z2) → c24(REACH[ITE](member(E(z0, z1), z2), z0, z1, z2), MEMBER(E(z0, z1), z2)) by

REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.93
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil), MEMBER(E(x0, x1), Nil)) 85.12/33.93
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2))
85.12/33.93
85.12/33.93

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.93
!EQ(0, S(z0)) → False 85.12/33.93
!EQ(S(z0), 0) → False 85.12/33.93
!EQ(0, 0) → True 85.12/33.93
and(False, False) → False 85.12/33.93
and(True, False) → False 85.12/33.93
and(False, True) → False 85.12/33.93
and(True, True) → True 85.12/33.93
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.93
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.93
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.93
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.93
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.93
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.93
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.93
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.93
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.93
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.93
via(z0, z1, Nil, z2) → Nil 85.12/33.93
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.93
member(z0, Nil) → False 85.12/33.93
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.93
notEmpty(Cons(z0, z1)) → True 85.12/33.93
notEmpty(Nil) → False 85.12/33.93
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.93
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.93
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.93
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.93
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.93
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.93
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.93
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.93
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.93
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.93
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.93
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.93
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.93
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil), MEMBER(E(x0, x1), Nil)) 85.12/33.93
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2))
S tuples:

EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.93
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.93
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.93
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.93
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.93
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.93
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.93
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.93
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil), MEMBER(E(x0, x1), Nil)) 85.12/33.93
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c17, c19, c24, c24

85.12/33.93
85.12/33.93

(21) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
85.12/33.93
85.12/33.93

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.93
!EQ(0, S(z0)) → False 85.12/33.93
!EQ(S(z0), 0) → False 85.12/33.93
!EQ(0, 0) → True 85.12/33.93
and(False, False) → False 85.12/33.93
and(True, False) → False 85.12/33.93
and(False, True) → False 85.12/33.93
and(True, True) → True 85.12/33.93
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.93
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.93
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.93
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.93
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.93
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.93
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.93
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.93
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.93
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.93
via(z0, z1, Nil, z2) → Nil 85.12/33.93
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.93
member(z0, Nil) → False 85.12/33.93
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.93
notEmpty(Cons(z0, z1)) → True 85.12/33.93
notEmpty(Nil) → False 85.12/33.93
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.93
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.93
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.93
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.93
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.93
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.93
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.93
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.93
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.93
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.93
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
S tuples:

EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
K tuples:none
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c17, c19, c24, c24

85.12/33.94
85.12/33.94

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

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2))
We considered the (Usable) Rules:

eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True
And the Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
The order we found is given by the following interpretation:
Polynomial interpretation : 85.12/33.94

POL(!EQ(x1, x2)) = 0    85.12/33.94
POL(!EQ'(x1, x2)) = 0    85.12/33.94
POL(0) = 0    85.12/33.94
POL(Cons(x1, x2)) = [1]    85.12/33.94
POL(E(x1, x2)) = 0    85.12/33.94
POL(EQEDGE(x1, x2)) = 0    85.12/33.94
POL(False) = 0    85.12/33.94
POL(MEMBER(x1, x2)) = 0    85.12/33.94
POL(Nil) = 0    85.12/33.94
POL(REACH(x1, x2, x3)) = [1]    85.12/33.94
POL(REACH[ITE](x1, x2, x3, x4)) = [1]    85.12/33.94
POL(S(x1)) = 0    85.12/33.94
POL(True) = 0    85.12/33.94
POL(VIA(x1, x2, x3, x4)) = [1]    85.12/33.94
POL(VIA[ITE][FALSE][ITE](x1, x2, x3, x4, x5)) = x4    85.12/33.94
POL(and(x1, x2)) = [3]    85.12/33.94
POL(c(x1)) = x1    85.12/33.94
POL(c1(x1)) = x1    85.12/33.94
POL(c12(x1)) = x1    85.12/33.94
POL(c17(x1)) = x1    85.12/33.94
POL(c17(x1, x2)) = x1 + x2    85.12/33.94
POL(c19(x1)) = x1    85.12/33.94
POL(c24(x1)) = x1    85.12/33.94
POL(c24(x1, x2)) = x1 + x2    85.12/33.94
POL(c8(x1)) = x1    85.12/33.94
POL(c9(x1)) = x1    85.12/33.94
POL(eqEdge(x1, x2)) = 0    85.12/33.94
POL(eqEdge[Match][E][Match][E][Ite](x1, x2, x3, x4, x5)) = [3] + x2 + x3 + x4 + x5    85.12/33.94
POL(member(x1, x2)) = [3] + [3]x1 + [3]x2    85.12/33.94
POL(member[Ite][False][Ite](x1, x2, x3)) = 0   
85.12/33.94
85.12/33.94

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
S tuples:

EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c17, c19, c24, c24

85.12/33.94
85.12/33.94

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

EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3))
We considered the (Usable) Rules:

eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True
And the Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
The order we found is given by the following interpretation:
Polynomial interpretation : 85.12/33.94

POL(!EQ(x1, x2)) = [1]    85.12/33.94
POL(!EQ'(x1, x2)) = 0    85.12/33.94
POL(0) = 0    85.12/33.94
POL(Cons(x1, x2)) = 0    85.12/33.94
POL(E(x1, x2)) = [1]    85.12/33.94
POL(EQEDGE(x1, x2)) = [1]    85.12/33.94
POL(False) = [1]    85.12/33.94
POL(MEMBER(x1, x2)) = x1    85.12/33.94
POL(Nil) = 0    85.12/33.94
POL(REACH(x1, x2, x3)) = [1]    85.12/33.94
POL(REACH[ITE](x1, x2, x3, x4)) = x1    85.12/33.94
POL(S(x1)) = 0    85.12/33.94
POL(True) = [1]    85.12/33.94
POL(VIA(x1, x2, x3, x4)) = [1]    85.12/33.94
POL(VIA[ITE][FALSE][ITE](x1, x2, x3, x4, x5)) = x1    85.12/33.94
POL(and(x1, x2)) = [5]    85.12/33.94
POL(c(x1)) = x1    85.12/33.94
POL(c1(x1)) = x1    85.12/33.94
POL(c12(x1)) = x1    85.12/33.94
POL(c17(x1)) = x1    85.12/33.94
POL(c17(x1, x2)) = x1 + x2    85.12/33.94
POL(c19(x1)) = x1    85.12/33.94
POL(c24(x1)) = x1    85.12/33.94
POL(c24(x1, x2)) = x1 + x2    85.12/33.94
POL(c8(x1)) = x1    85.12/33.94
POL(c9(x1)) = x1    85.12/33.94
POL(eqEdge(x1, x2)) = 0    85.12/33.94
POL(eqEdge[Match][E][Match][E][Ite](x1, x2, x3, x4, x5)) = 0    85.12/33.94
POL(member(x1, x2)) = [2]    85.12/33.94
POL(member[Ite][False][Ite](x1, x2, x3)) = [4]x1   
85.12/33.94
85.12/33.94

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
S tuples:

VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c17, c19, c24, c24

85.12/33.94
85.12/33.94

(27) 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(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3)))
We considered the (Usable) Rules:

eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True
And the Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
The order we found is given by the following interpretation:
Polynomial interpretation : 85.12/33.94

POL(!EQ(x1, x2)) = 0    85.12/33.94
POL(!EQ'(x1, x2)) = 0    85.12/33.94
POL(0) = 0    85.12/33.94
POL(Cons(x1, x2)) = 0    85.12/33.94
POL(E(x1, x2)) = [1]    85.12/33.94
POL(EQEDGE(x1, x2)) = 0    85.12/33.94
POL(False) = [1]    85.12/33.94
POL(MEMBER(x1, x2)) = x1    85.12/33.94
POL(Nil) = 0    85.12/33.94
POL(REACH(x1, x2, x3)) = [1]    85.12/33.94
POL(REACH[ITE](x1, x2, x3, x4)) = x1    85.12/33.94
POL(S(x1)) = 0    85.12/33.94
POL(True) = [4]    85.12/33.94
POL(VIA(x1, x2, x3, x4)) = [1]    85.12/33.94
POL(VIA[ITE][FALSE][ITE](x1, x2, x3, x4, x5)) = [1]    85.12/33.94
POL(and(x1, x2)) = [3]    85.12/33.94
POL(c(x1)) = x1    85.12/33.94
POL(c1(x1)) = x1    85.12/33.94
POL(c12(x1)) = x1    85.12/33.94
POL(c17(x1)) = x1    85.12/33.94
POL(c17(x1, x2)) = x1 + x2    85.12/33.94
POL(c19(x1)) = x1    85.12/33.94
POL(c24(x1)) = x1    85.12/33.94
POL(c24(x1, x2)) = x1 + x2    85.12/33.94
POL(c8(x1)) = x1    85.12/33.94
POL(c9(x1)) = x1    85.12/33.94
POL(eqEdge(x1, x2)) = 0    85.12/33.94
POL(eqEdge[Match][E][Match][E][Ite](x1, x2, x3, x4, x5)) = 0    85.12/33.94
POL(member(x1, x2)) = [4]    85.12/33.94
POL(member[Ite][False][Ite](x1, x2, x3)) = [4]x1   
85.12/33.94
85.12/33.94

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
S tuples:

VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3)))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c17, c19, c24, c24

85.12/33.94
85.12/33.94

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

REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2)))
We considered the (Usable) Rules:

eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True
And the Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
The order we found is given by the following interpretation:
Polynomial interpretation : 85.12/33.94

POL(!EQ(x1, x2)) = 0    85.12/33.94
POL(!EQ'(x1, x2)) = 0    85.12/33.94
POL(0) = 0    85.12/33.94
POL(Cons(x1, x2)) = 0    85.12/33.94
POL(E(x1, x2)) = 0    85.12/33.94
POL(EQEDGE(x1, x2)) = 0    85.12/33.94
POL(False) = [1]    85.12/33.94
POL(MEMBER(x1, x2)) = 0    85.12/33.94
POL(Nil) = 0    85.12/33.94
POL(REACH(x1, x2, x3)) = [1]    85.12/33.94
POL(REACH[ITE](x1, x2, x3, x4)) = x1    85.12/33.94
POL(S(x1)) = 0    85.12/33.94
POL(True) = 0    85.12/33.94
POL(VIA(x1, x2, x3, x4)) = [1]    85.12/33.94
POL(VIA[ITE][FALSE][ITE](x1, x2, x3, x4, x5)) = [1]    85.12/33.94
POL(and(x1, x2)) = [3]    85.12/33.94
POL(c(x1)) = x1    85.12/33.94
POL(c1(x1)) = x1    85.12/33.94
POL(c12(x1)) = x1    85.12/33.94
POL(c17(x1)) = x1    85.12/33.94
POL(c17(x1, x2)) = x1 + x2    85.12/33.94
POL(c19(x1)) = x1    85.12/33.94
POL(c24(x1)) = x1    85.12/33.94
POL(c24(x1, x2)) = x1 + x2    85.12/33.94
POL(c8(x1)) = x1    85.12/33.94
POL(c9(x1)) = x1    85.12/33.94
POL(eqEdge(x1, x2)) = 0    85.12/33.94
POL(eqEdge[Match][E][Match][E][Ite](x1, x2, x3, x4, x5)) = 0    85.12/33.94
POL(member(x1, x2)) = [1]    85.12/33.94
POL(member[Ite][False][Ite](x1, x2, x3)) = [2]x1   
85.12/33.94
85.12/33.94

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
S tuples:

VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2)))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c17, c19, c24, c24

85.12/33.94
85.12/33.94

(31) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace VIA(S(z0), x1, Cons(E(S(z1), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(z0), x1, Cons(E(S(z1), x3), x4), x5), !EQ'(S(z0), S(z1))) by

VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2)))
85.12/33.94
85.12/33.94

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2)))
S tuples:

VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2)))
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2)))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c19, c24, c24, c17

85.12/33.94
85.12/33.94

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

VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2)))
We considered the (Usable) Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True
And the Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2)))
The order we found is given by the following interpretation:
Polynomial interpretation : 85.12/33.94

POL(!EQ(x1, x2)) = 0    85.12/33.94
POL(!EQ'(x1, x2)) = 0    85.12/33.94
POL(0) = 0    85.12/33.94
POL(Cons(x1, x2)) = 0    85.12/33.94
POL(E(x1, x2)) = 0    85.12/33.94
POL(EQEDGE(x1, x2)) = 0    85.12/33.94
POL(False) = 0    85.12/33.94
POL(MEMBER(x1, x2)) = 0    85.12/33.94
POL(Nil) = 0    85.12/33.94
POL(REACH(x1, x2, x3)) = [1]    85.12/33.94
POL(REACH[ITE](x1, x2, x3, x4)) = [1]    85.12/33.94
POL(S(x1)) = 0    85.12/33.94
POL(True) = 0    85.12/33.94
POL(VIA(x1, x2, x3, x4)) = [1]    85.12/33.94
POL(VIA[ITE][FALSE][ITE](x1, x2, x3, x4, x5)) = [1]    85.12/33.94
POL(and(x1, x2)) = [2]    85.12/33.94
POL(c(x1)) = x1    85.12/33.94
POL(c1(x1)) = x1    85.12/33.94
POL(c12(x1)) = x1    85.12/33.94
POL(c17(x1)) = x1    85.12/33.94
POL(c17(x1, x2)) = x1 + x2    85.12/33.94
POL(c19(x1)) = x1    85.12/33.94
POL(c24(x1)) = x1    85.12/33.94
POL(c24(x1, x2)) = x1 + x2    85.12/33.94
POL(c8(x1)) = x1    85.12/33.94
POL(c9(x1)) = x1    85.12/33.94
POL(eqEdge(x1, x2)) = [4]    85.12/33.94
POL(eqEdge[Match][E][Match][E][Ite](x1, x2, x3, x4, x5)) = x1    85.12/33.94
POL(member(x1, x2)) = [3] + [3]x1 + [3]x2    85.12/33.94
POL(member[Ite][False][Ite](x1, x2, x3)) = 0   
85.12/33.94
85.12/33.94

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2)))
S tuples:

VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0)))
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2)))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c19, c24, c24, c17

85.12/33.94
85.12/33.94

(35) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) by

REACH(z0, z1, Cons(E(z2, z3), x3)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), E(z0, z1), Cons(E(z2, z3), x3)), z0, z1, Cons(E(z2, z3), x3)), MEMBER(E(z0, z1), Cons(E(z2, z3), x3)))
85.12/33.94
85.12/33.94

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2))) 85.12/33.94
REACH(z0, z1, Cons(E(z2, z3), x3)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1), E(z0, z1), Cons(E(z2, z3), x3)), z0, z1, Cons(E(z2, z3), x3)), MEMBER(E(z0, z1), Cons(E(z2, z3), x3)))
S tuples:

VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0)))
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2)))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c19, c24, c17, c24

85.12/33.94
85.12/33.94

(37) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
85.12/33.94
85.12/33.94

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2))) 85.12/33.94
REACH(z0, z1, Cons(E(z2, z3), x3)) → c24(MEMBER(E(z0, z1), Cons(E(z2, z3), x3)))
S tuples:

VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0)))
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2)))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c19, c24, c17

85.12/33.94
85.12/33.94

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

VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0)))
We considered the (Usable) Rules:

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

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2))) 85.12/33.94
REACH(z0, z1, Cons(E(z2, z3), x3)) → c24(MEMBER(E(z0, z1), Cons(E(z2, z3), x3)))
The order we found is given by the following interpretation:
Polynomial interpretation : 85.12/33.94

POL(!EQ(x1, x2)) = 0    85.12/33.94
POL(!EQ'(x1, x2)) = 0    85.12/33.94
POL(0) = 0    85.12/33.94
POL(Cons(x1, x2)) = [4] + x2    85.12/33.94
POL(E(x1, x2)) = 0    85.12/33.94
POL(EQEDGE(x1, x2)) = 0    85.12/33.94
POL(False) = 0    85.12/33.94
POL(MEMBER(x1, x2)) = 0    85.12/33.94
POL(Nil) = 0    85.12/33.94
POL(REACH(x1, x2, x3)) = [1] + [3]x2    85.12/33.94
POL(REACH[ITE](x1, x2, x3, x4)) = [1] + x1 + [3]x3 + x4    85.12/33.94
POL(S(x1)) = 0    85.12/33.94
POL(True) = 0    85.12/33.94
POL(VIA(x1, x2, x3, x4)) = [1] + [3]x2 + x3    85.12/33.94
POL(VIA[ITE][FALSE][ITE](x1, x2, x3, x4, x5)) = [3]x3 + x4    85.12/33.94
POL(c(x1)) = x1    85.12/33.94
POL(c1(x1)) = x1    85.12/33.94
POL(c12(x1)) = x1    85.12/33.94
POL(c17(x1)) = x1    85.12/33.94
POL(c17(x1, x2)) = x1 + x2    85.12/33.94
POL(c19(x1)) = x1    85.12/33.94
POL(c24(x1)) = x1    85.12/33.94
POL(c8(x1)) = x1    85.12/33.94
POL(c9(x1)) = x1   
85.12/33.94
85.12/33.94

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2))) 85.12/33.94
REACH(z0, z1, Cons(E(z2, z3), x3)) → c24(MEMBER(E(z0, z1), Cons(E(z2, z3), x3)))
S tuples:

REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0)))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c19, c24, c17

85.12/33.94
85.12/33.94

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

REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
We considered the (Usable) Rules:

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

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2))) 85.12/33.94
REACH(z0, z1, Cons(E(z2, z3), x3)) → c24(MEMBER(E(z0, z1), Cons(E(z2, z3), x3)))
The order we found is given by the following interpretation:
Polynomial interpretation : 85.12/33.94

POL(!EQ(x1, x2)) = 0    85.12/33.94
POL(!EQ'(x1, x2)) = 0    85.12/33.94
POL(0) = 0    85.12/33.94
POL(Cons(x1, x2)) = [4] + x2    85.12/33.94
POL(E(x1, x2)) = x2    85.12/33.94
POL(EQEDGE(x1, x2)) = [2]x1    85.12/33.94
POL(False) = 0    85.12/33.94
POL(MEMBER(x1, x2)) = [4]x1    85.12/33.94
POL(Nil) = 0    85.12/33.94
POL(REACH(x1, x2, x3)) = [2] + [4]x2    85.12/33.94
POL(REACH[ITE](x1, x2, x3, x4)) = [1] + x1 + [4]x3 + [4]x4    85.12/33.94
POL(S(x1)) = 0    85.12/33.94
POL(True) = 0    85.12/33.94
POL(VIA(x1, x2, x3, x4)) = [1] + [4]x2 + [4]x3    85.12/33.94
POL(VIA[ITE][FALSE][ITE](x1, x2, x3, x4, x5)) = [4]x3 + [4]x4    85.12/33.94
POL(c(x1)) = x1    85.12/33.94
POL(c1(x1)) = x1    85.12/33.94
POL(c12(x1)) = x1    85.12/33.94
POL(c17(x1)) = x1    85.12/33.94
POL(c17(x1, x2)) = x1 + x2    85.12/33.94
POL(c19(x1)) = x1    85.12/33.94
POL(c24(x1)) = x1    85.12/33.94
POL(c8(x1)) = x1    85.12/33.94
POL(c9(x1)) = x1   
85.12/33.94
85.12/33.94

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 85.12/33.94
!EQ(0, S(z0)) → False 85.12/33.94
!EQ(S(z0), 0) → False 85.12/33.94
!EQ(0, 0) → True 85.12/33.94
and(False, False) → False 85.12/33.94
and(True, False) → False 85.12/33.94
and(False, True) → False 85.12/33.94
and(True, True) → True 85.12/33.94
via[Ite][False][Ite](True, z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite][True][Let](z0, z1, Cons(E(z2, z3), z4), z5, reach(z3, z1, z5)) 85.12/33.94
via[Ite][False][Ite](False, z0, z1, Cons(z2, z3), z4) → via(z0, z1, z3, z4) 85.12/33.94
member[Ite][False][Ite](False, z0, Cons(z1, z2)) → member(z0, z2) 85.12/33.94
member[Ite][False][Ite](True, z0, z1) → True 85.12/33.94
reach[Ite](False, z0, z1, z2) → via(z0, z1, z2, z2) 85.12/33.94
reach[Ite](True, z0, z1, z2) → Cons(E(z0, z1), Nil) 85.12/33.94
getNodeFromEdge(S(S(z0)), E(z1, z2)) → z2 85.12/33.94
getNodeFromEdge(S(0), E(z0, z1)) → z0 85.12/33.94
getNodeFromEdge(0, E(z0, z1)) → z0 85.12/33.94
via(z0, z1, Cons(E(z2, z3), z4), z5) → via[Ite][False][Ite](!EQ(z0, z2), z0, z1, Cons(E(z2, z3), z4), z5) 85.12/33.94
via(z0, z1, Nil, z2) → Nil 85.12/33.94
member(z0, Cons(z1, z2)) → member[Ite][False][Ite](eqEdge(z0, z1), z0, Cons(z1, z2)) 85.12/33.94
member(z0, Nil) → False 85.12/33.94
eqEdge(E(z0, z1), E(z2, z3)) → eqEdge[Match][E][Match][E][Ite](and(!EQ(z0, z2), !EQ(z1, z3)), z2, z3, z0, z1) 85.12/33.94
notEmpty(Cons(z0, z1)) → True 85.12/33.94
notEmpty(Nil) → False 85.12/33.94
reach(z0, z1, z2) → reach[Ite](member(E(z0, z1), z2), z0, z1, z2) 85.12/33.94
goal(z0, z1, z2) → reach(z0, z1, z2)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 85.12/33.94
VIA[ITE][FALSE][ITE](True, z0, z1, Cons(E(z2, z3), z4), z5) → c8(REACH(z3, z1, z5)) 85.12/33.94
VIA[ITE][FALSE][ITE](False, z0, z1, Cons(z2, z3), z4) → c9(VIA(z0, z1, z3, z4)) 85.12/33.94
REACH[ITE](False, z0, z1, z2) → c12(VIA(z0, z1, z2, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2))) 85.12/33.94
REACH(z0, z1, Cons(E(z2, z3), x3)) → c24(MEMBER(E(z0, z1), Cons(E(z2, z3), x3)))
S tuples:none
K tuples:

REACH(x0, x1, x2) → c24(MEMBER(E(x0, x1), x2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z0, z2)) 85.12/33.94
EQEDGE(E(z0, z1), E(z2, z3)) → c1(!EQ'(z1, z3)) 85.12/33.94
MEMBER(E(z0, z1), Cons(E(z2, z3), x2)) → c19(EQEDGE(E(z0, z1), E(z2, z3))) 85.12/33.94
REACH(x0, x1, Cons(z1, z2)) → c24(REACH[ITE](member[Ite][False][Ite](eqEdge(E(x0, x1), z1), E(x0, x1), Cons(z1, z2)), x0, x1, Cons(z1, z2)), MEMBER(E(x0, x1), Cons(z1, z2))) 85.12/33.94
VIA(S(x0), x1, Cons(E(S(x2), x3), x4), x5) → c17(!EQ'(S(x0), S(x2))) 85.12/33.94
VIA(0, x1, Cons(E(S(z0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, 0, x1, Cons(E(S(z0), x3), x4), x5)) 85.12/33.94
VIA(S(z0), x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(z0), x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(0, x1, Cons(E(0, x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, 0, x1, Cons(E(0, x3), x4), x5)) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](!EQ(z0, z1), S(S(z0)), x1, Cons(E(S(S(z1)), x3), x4), x5), !EQ'(S(S(z0)), S(S(z1)))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(S(z0)), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(0), x1, Cons(E(S(S(z0)), x3), x4), x5), !EQ'(S(0), S(S(z0)))) 85.12/33.94
VIA(S(S(z0)), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](False, S(S(z0)), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(S(z0)), S(0))) 85.12/33.94
VIA(S(0), x1, Cons(E(S(0), x3), x4), x5) → c17(VIA[ITE][FALSE][ITE](True, S(0), x1, Cons(E(S(0), x3), x4), x5), !EQ'(S(0), S(0))) 85.12/33.94
REACH(x0, x1, Nil) → c24(REACH[ITE](False, x0, x1, Nil))
Defined Rule Symbols:

getNodeFromEdge, via, member, eqEdge, notEmpty, reach, goal, !EQ, and, via[Ite][False][Ite], member[Ite][False][Ite], reach[Ite]

Defined Pair Symbols:

!EQ', VIA[ITE][FALSE][ITE], REACH[ITE], EQEDGE, VIA, MEMBER, REACH

Compound Symbols:

c, c8, c9, c12, c1, c17, c19, c24, c17

85.12/33.94
85.12/33.94

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

The set S is empty
85.12/33.94
85.12/33.94

(44) BOUNDS(O(1), O(1))

85.12/33.94
85.12/33.94
85.12/33.99 EOF