let G be _finite real-weighted WGraph; :: thesis: for n being Nat holds ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G
set src = the Element of the_Vertices_of G;
defpred S1[ Nat] means ((PRIM:CompSeq G) . $1) `1 c= G .reachableFrom the Element of the_Vertices_of G;
set G0 = (PRIM:CompSeq G) . 0;
(PRIM:CompSeq G) . 0 = PRIM:Init G by Def17;
then A1: ((PRIM:CompSeq G) . 0) `1 = { the Element of the_Vertices_of G} ;
A2: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
set Gn = (PRIM:CompSeq G) . n;
set Gn1 = (PRIM:CompSeq G) . (n + 1);
set Next = PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
set e = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
set sc = (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
set tar = (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
A4: (PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n) by Def17;
now :: thesis: S1[n + 1]
per cases ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} or ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) or ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & not (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ) ;
suppose A5: ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ; :: thesis: S1[n + 1]
then (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))}),((((PRIM:CompSeq G) . n) `2) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)})] by A4, Def15;
then A6: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1) \/ {((the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ;
A7: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in PRIM:NextBestEdges ((PRIM:CompSeq G) . n) by A5;
now :: thesis: for v being object st v in ((PRIM:CompSeq G) . (n + 1)) `1 holds
v in G .reachableFrom the Element of the_Vertices_of G
let v be object ; :: thesis: ( v in ((PRIM:CompSeq G) . (n + 1)) `1 implies v in G .reachableFrom the Element of the_Vertices_of G )
assume A8: v in ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: v in G .reachableFrom the Element of the_Vertices_of G
now :: thesis: v in G .reachableFrom the Element of the_Vertices_of G
per cases ( v in ((PRIM:CompSeq G) . n) `1 or v in {((the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ) by A6, A8, XBOOLE_0:def 3;
end;
end;
hence v in G .reachableFrom the Element of the_Vertices_of G ; :: thesis: verum
end;
hence S1[n + 1] by TARSKI:def 3; :: thesis: verum
end;
suppose A9: ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & not (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ; :: thesis: S1[n + 1]
then (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))}),((((PRIM:CompSeq G) . n) `2) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)})] by A4, Def15;
then A10: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1) \/ {((the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ;
A11: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G by A9, Def13;
then A12: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in the_Edges_of G ;
A13: (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 by A9, A11;
now :: thesis: for v being object st v in ((PRIM:CompSeq G) . (n + 1)) `1 holds
v in G .reachableFrom the Element of the_Vertices_of G
let v be object ; :: thesis: ( v in ((PRIM:CompSeq G) . (n + 1)) `1 implies v in G .reachableFrom the Element of the_Vertices_of G )
assume A14: v in ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: v in G .reachableFrom the Element of the_Vertices_of G
now :: thesis: v in G .reachableFrom the Element of the_Vertices_of G
per cases ( v in ((PRIM:CompSeq G) . n) `1 or v in {((the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n))} ) by A10, A14, XBOOLE_0:def 3;
end;
end;
hence v in G .reachableFrom the Element of the_Vertices_of G ; :: thesis: verum
end;
hence S1[n + 1] by TARSKI:def 3; :: thesis: verum
end;
end;
end;
hence S1[n + 1] ; :: thesis: verum
end;
the Element of the_Vertices_of G in G .reachableFrom the Element of the_Vertices_of G by GLIB_002:9;
then A15: S1[ 0 ] by A1, ZFMISC_1:31;
for n being Nat holds S1[n] from NAT_1:sch 2(A15, A2);
 hence for n being Nat holds ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G ; :: thesis: verum