let G be finite real-weighted WGraph; :: thesis: for n being Nat holds ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom (choose (the_Vertices_of G))
set src = choose (the_Vertices_of G);
defpred S<sub>1</sub>[ Nat] means ((PRIM:CompSeq G) . $1) `1 c= G .reachableFrom (choose (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 = {(choose (the_Vertices_of G))} by MCART_1:7;

A2: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[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 = choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n));
set sc = (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)));
set tar = (the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)));
A4: (PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n) by Def17;

now

per cases ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} or ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 ) or ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & not (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 ) ) ;

suppose PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} ; :: thesis: S₁[n + 1]

hence S₁[n + 1] by A3, A4, Def15; :: thesis: verum

end;

suppose A5: ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 ) ; :: thesis: S₁[n + 1]

then (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1) \/ {((the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))}),((((PRIM:CompSeq G) . n) `2) \/ {(choose (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) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} by MCART_1:7;
A7: choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)) in PRIM:NextBestEdges ((PRIM:CompSeq G) . n) by A5;

now

let v be set ; :: thesis: ( v in ((PRIM:CompSeq G) . (n + 1)) `1 implies v in G .reachableFrom (choose (the_Vertices_of G)) )
assume A8: v in ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: v in G .reachableFrom (choose (the_Vertices_of G))

now

per cases ( v in ((PRIM:CompSeq G) . n) `1 or v in {((the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} ) by A6, A8, XBOOLE_0:def 3;

suppose v in ((PRIM:CompSeq G) . n) `1 ; :: thesis: v in G .reachableFrom (choose (the_Vertices_of G))

hence v in G .reachableFrom (choose (the_Vertices_of G)) by A3; :: thesis: verum

end;

suppose v in {((the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} ; :: thesis: v in G .reachableFrom (choose (the_Vertices_of G))

then v = (the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) by TARSKI:def 1;
then choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)) Joins (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))),v,G by A7, GLIB_000:def 13;
hence v in G .reachableFrom (choose (the_Vertices_of G)) by A3, A5, GLIB_002:10; :: thesis: verum

end;

end;

end;

hence v in G .reachableFrom (choose (the_Vertices_of G)) ; :: thesis: verum

end;

hence S₁[n + 1] by TARSKI:def 3; :: thesis: verum

end;

suppose A9: ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} & not (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 ) ; :: thesis: S₁[n + 1]

then (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1) \/ {((the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))}),((((PRIM:CompSeq G) . n) `2) \/ {(choose (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) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} by MCART_1:7;
A11: choose (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: choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)) in the_Edges_of G by GLIB_000:def 15;
A13: (the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 by A9, A11, GLIB_000:def 15;

now

let v be set ; :: thesis: ( v in ((PRIM:CompSeq G) . (n + 1)) `1 implies v in G .reachableFrom (choose (the_Vertices_of G)) )
assume A14: v in ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: v in G .reachableFrom (choose (the_Vertices_of G))

now

per cases ( v in ((PRIM:CompSeq G) . n) `1 or v in {((the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} ) by A10, A14, XBOOLE_0:def 3;

suppose v in ((PRIM:CompSeq G) . n) `1 ; :: thesis: v in G .reachableFrom (choose (the_Vertices_of G))

hence v in G .reachableFrom (choose (the_Vertices_of G)) by A3; :: thesis: verum

end;

suppose v in {((the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} ; :: thesis: v in G .reachableFrom (choose (the_Vertices_of G))

then v = (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) by TARSKI:def 1;
then choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)) Joins (the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))),v,G by A12, GLIB_000:def 13;
hence v in G .reachableFrom (choose (the_Vertices_of G)) by A3, A13, GLIB_002:10; :: thesis: verum

end;

end;

end;

hence v in G .reachableFrom (choose (the_Vertices_of G)) ; :: thesis: verum

end;

hence S₁[n + 1] by TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

choose (the_Vertices_of G) in G .reachableFrom (choose (the_Vertices_of G)) by GLIB_002:9;
then A15: S₁[ 0 ] by A1, ZFMISC_1:31;
for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A2);
hence for n being Nat holds ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom (choose (the_Vertices_of G)) ; :: thesis: verum