let G be _finite real-weighted WGraph; :: thesis: for src being Vertex of G
for n being Nat holds
( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} iff dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src )
let src be Vertex of G; :: thesis: for n being Nat holds
( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} iff dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src )
let n be Nat; :: thesis: ( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} iff dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src )
set DCS = DIJK:CompSeq src;
set RFS = G .reachableDFrom src;
set Gn = (DIJK:CompSeq src) . n;
set Gn1a = (DIJK:CompSeq src) . (n + 1);
set BestEdges = DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set SGn = the_Source_of G;
set TGn = the_Target_of G;

hereby :: thesis: ( dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src implies DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} )

assume A1: DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} ; :: thesis: dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src

now :: thesis: not dom (((DIJK:CompSeq src) . n) `1) <> G .reachableDFrom src

defpred S₁[ set ] means ( (the_Source_of G) . $1 in dom (((DIJK:CompSeq src) . n) `1) & not (the_Target_of G) . $1 in dom (((DIJK:CompSeq src) . n) `1) );
assume A2: dom (((DIJK:CompSeq src) . n) `1) <> G .reachableDFrom src ; :: thesis: contradiction
consider BE1 being Subset of (the_Edges_of G) such that
A3: for x being set holds
( x in BE1 iff ( x in the_Edges_of G & S<sub>1</sub>[x] ) ) from SUBSET_1:sch 1();
dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src by Th19;
then A4: dom (((DIJK:CompSeq src) . n) `1) c< G .reachableDFrom src by A2, XBOOLE_0:def 8;

now :: thesis: not BE1 = {}

(DIJK:CompSeq src) . 0 = DIJK:Init src by Def11;
then dom (((DIJK:CompSeq src) . 0) `1) = {src} ;
then A5: src in dom (((DIJK:CompSeq src) . 0) `1) by TARSKI:def 1;
assume A6: BE1 = {} ; :: thesis: contradiction
consider v being object such that
A7: v in G .reachableDFrom src and
A8: not v in dom (((DIJK:CompSeq src) . n) `1) by A4, XBOOLE_0:6;
reconsider v = v as Vertex of G by A7;
consider W being directed Walk of G such that
A9: W is_Walk_from src,v by A7, GLIB_002:def 6;
defpred S<sub>2</sub>[ Nat] means ( $1 is odd & $1 <= len W & not W . $1 in dom (((DIJK:CompSeq src) . n) `1) );
W . (len W) = W .last() by GLIB_001:def 7
.= v by A9, GLIB_001:def 23 ;
then A10: ex k being Nat st S₂[k] by A8;
consider k being Nat such that
A11: ( S₂[k] & ( for m being Nat st S₂[m] holds
k <= m ) ) from NAT_1:sch 5(A10);
A12: dom (((DIJK:CompSeq src) . 0) `1) c= dom (((DIJK:CompSeq src) . n) `1) by Th18;

now :: thesis: contradiction

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: contradiction

then W . k = W .first() by GLIB_001:def 6
.= src by A9, GLIB_001:def 23 ;
hence contradiction by A5, A12, A11; :: thesis: verum

end;

suppose A13: k <> 1 ; :: thesis: contradiction

reconsider k9 = k as odd Element of NAT by A11, ORDINAL1:def 12;
1 <= k by A11, ABIAN:12;
then 1 < k by A13, XXREAL_0:1;
then 1 + 1 < k + 1 by XREAL_1:8;
then 2 * 1 <= k by NAT_1:13;
then reconsider k2a = k9 - (2 * 1) as odd Element of NAT by INT_1:5;
set e = W . (k2a + 1);
A14: k - 2 < (len W) - 0 by A11, XREAL_1:15;
then A15: W . (k2a + 1) DJoins W . k2a,W . (k2a + 2),G by GLIB_001:122;
then A16: (the_Target_of G) . (W . (k2a + 1)) = W . (k2a + 2) ;
k2a < k - 0 by XREAL_1:15;
then A17: W . k2a in dom (((DIJK:CompSeq src) . n) `1) by A11, A14;
( W . (k2a + 1) in the_Edges_of G & (the_Source_of G) . (W . (k2a + 1)) = W . k2a ) by A15;
hence contradiction by A3, A6, A11, A17, A16; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then reconsider BE1 = BE1 as non empty finite set ;
deffunc H₁( Element of BE1) -> set = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . $1)) + ((the_Weight_of G) . $1);
consider e1 being Element of BE1 such that
A18: for e2 being Element of BE1 holds H<sub>1</sub>(e1) <= H<sub>1</sub>(e2) from PRE_CIRC:sch 5();
A19: not (the_Target_of G) . e1 in dom (((DIJK:CompSeq src) . n) `1) by A3;
A20: e1 in the_Edges_of G by A3;
then (the_Target_of G) . e1 in the_Vertices_of G by FUNCT_2:5;
then A21: (the_Target_of G) . e1 in (the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)) by A19, XBOOLE_0:def 5;

A22: now :: thesis: for y being set st y DSJoins dom (((DIJK:CompSeq src) . n) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),G holds
((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . y)) + ((the_Weight_of G) . y)

let y be set ; :: thesis: ( y DSJoins dom (((DIJK:CompSeq src) . n) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),G implies ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . y)) + ((the_Weight_of G) . y) )
assume A23: y DSJoins dom (((DIJK:CompSeq src) . n) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),G ; :: thesis: ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . y)) + ((the_Weight_of G) . y)
then (the_Target_of G) . y in (the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)) ;
then A24: not (the_Target_of G) . y in dom (((DIJK:CompSeq src) . n) `1) by XBOOLE_0:def 5;
( y in the_Edges_of G & (the_Source_of G) . y in dom (((DIJK:CompSeq src) . n) `1) ) by A23;
then y in BE1 by A3, A24;
hence ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . y)) + ((the_Weight_of G) . y) by A18; :: thesis: verum

end;

(the_Source_of G) . e1 in dom (((DIJK:CompSeq src) . n) `1) by A3;
then e1 DSJoins dom (((DIJK:CompSeq src) . n) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),G by A20, A21;
hence contradiction by A1, A22, Def7; :: thesis: verum

end;

hence dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src ; :: thesis: verum

end;

assume A25: dom (((DIJK:CompSeq src) . n) `1) = G .reachableDFrom src ; :: thesis: DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {}
A26: (DIJK:CompSeq src) . (n + 1) = DIJK:Step ((DIJK:CompSeq src) . n) by Def11;

now :: thesis: not DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {}

assume DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {} ; :: thesis: contradiction
then A27: card (dom (((DIJK:CompSeq src) . (n + 1)) `1)) = (card (G .reachableDFrom src)) + 1 by A26, A25, Th15;
Segm (card (dom (((DIJK:CompSeq src) . (n + 1)) `1))) c= Segm (card (G .reachableDFrom src)) by Th19, CARD_1:11;
then (card (G .reachableDFrom src)) + 1 <= (card (G .reachableDFrom src)) + 0 by A27, NAT_1:39;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

hence DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} ; :: thesis: verum