let G be _finite real-weighted WGraph; :: thesis: for src being Vertex of G
for n being Nat holds dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src
let src be Vertex of G; :: thesis: for n being Nat holds dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src
set DCS = DIJK:CompSeq src;
defpred S1[ Nat] means dom (((DIJK:CompSeq src) . $1) `1) c= G .reachableDFrom src;
(DIJK:CompSeq src) . 0 = DIJK:Init src by Def11;
then A1: dom (((DIJK:CompSeq src) . 0) `1) = {src} ;
now :: thesis: for k being Nat st dom (((DIJK:CompSeq src) . k) `1) c= G .reachableDFrom src holds
dom (((DIJK:CompSeq src) . (k + 1)) `1) c= G .reachableDFrom src
let k be Nat; :: thesis: ( dom (((DIJK:CompSeq src) . k) `1) c= G .reachableDFrom src implies dom (((DIJK:CompSeq src) . (k + 1)) `1) c= G .reachableDFrom src )
assume A2: dom (((DIJK:CompSeq src) . k) `1) c= G .reachableDFrom src ; :: thesis: dom (((DIJK:CompSeq src) . (k + 1)) `1) c= G .reachableDFrom src
set Gk = (DIJK:CompSeq src) . k;
set NextG = (DIJK:CompSeq src) . (k + 1);
set BestEdges = DIJK:NextBestEdges ((DIJK:CompSeq src) . k);
set e = the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k);
set NextEG = (((DIJK:CompSeq src) . k) `2) \/ { the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k)};
set v1 = (the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k);
set target = (the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k);
set pc = (((DIJK:CompSeq src) . k) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k));
set ec = (the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k);
A3: (DIJK:CompSeq src) . (k + 1) = DIJK:Step ((DIJK:CompSeq src) . k) by Def11;
now :: thesis: for x being object st x in dom (((DIJK:CompSeq src) . (k + 1)) `1) holds
x in G .reachableDFrom src
let x be object ; :: thesis: ( x in dom (((DIJK:CompSeq src) . (k + 1)) `1) implies x in G .reachableDFrom src )
assume A4: x in dom (((DIJK:CompSeq src) . (k + 1)) `1) ; :: thesis: x in G .reachableDFrom src
now :: thesis: x in G .reachableDFrom src
per cases ( DIJK:NextBestEdges ((DIJK:CompSeq src) . k) = {} or DIJK:NextBestEdges ((DIJK:CompSeq src) . k) <> {} ) ;
suppose A5: DIJK:NextBestEdges ((DIJK:CompSeq src) . k) <> {} ; :: thesis: x in G .reachableDFrom src
set xx = x;
reconsider xx = x as Vertex of G by A4;
the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k) DSJoins dom (((DIJK:CompSeq src) . k) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . k) `1)),G by A5, Def7;
then A6: (the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k) in dom (((DIJK:CompSeq src) . k) `1) ;
then reconsider v19 = (the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k) as Vertex of G ;
(DIJK:CompSeq src) . (k + 1) = [((((DIJK:CompSeq src) . k) `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k)) .--> (((((DIJK:CompSeq src) . k) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k))))),((((DIJK:CompSeq src) . k) `2) \/ { the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k)})] by A3, A5, Def8;
then A7: ((DIJK:CompSeq src) . (k + 1)) `1 = (((DIJK:CompSeq src) . k) `1) +* (((the_Target_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k)) .--> (((((DIJK:CompSeq src) . k) `1) . ((the_Source_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k))) + ((the_Weight_of G) . the Element of DIJK:NextBestEdges ((DIJK:CompSeq src) . k)))) ;
hence x in G .reachableDFrom src ; :: thesis: verum
end;
end;
end;
hence x in G .reachableDFrom src ; :: thesis: verum
end;
hence dom (((DIJK:CompSeq src) . (k + 1)) `1) c= G .reachableDFrom src ; :: thesis: verum
end;
then A10: for k being Nat st S1[k] holds
S1[k + 1] ;
src in G .reachableDFrom src by GLIB_002:18;
then A11: S1[ 0 ] by A1, ZFMISC_1:31;
for n being Nat holds S1[n] from NAT_1:sch 2(A11, A10);
 hence for n being Nat holds dom (((DIJK:CompSeq src) . n) `1) c= G .reachableDFrom src ; :: thesis: verum