let G be finite real-weighted WGraph; :: thesis: for n being Nat holds (() . 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 (() . \$1) `1 c= G .reachableFrom the Element of the_Vertices_of G;
set G0 = () . 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 = () . n;
set Gn1 = () . (n + 1);
set Next = PRIM:NextBestEdges (() . n);
set e = the Element of PRIM:NextBestEdges (() . n);
set sc = () . the Element of PRIM:NextBestEdges (() . n);
set tar = () . the Element of PRIM:NextBestEdges (() . n);
A4: (PRIM:CompSeq G) . (n + 1) = PRIM:Step (() . n) by Def17;
now :: thesis: S1[n + 1]
per cases ( PRIM:NextBestEdges (() . n) = {} or ( PRIM:NextBestEdges (() . n) <> {} & () . the Element of PRIM:NextBestEdges (() . n) in (() . n) `1 ) or ( PRIM:NextBestEdges (() . n) <> {} & not () . the Element of PRIM:NextBestEdges (() . n) in (() . n) `1 ) ) ;
suppose PRIM:NextBestEdges (() . n) = {} ; :: thesis: S1[n + 1]
hence S1[n + 1] by ; :: thesis: verum
end;
suppose A5: ( PRIM:NextBestEdges (() . n) <> {} & () . the Element of PRIM:NextBestEdges (() . n) in (() . n) `1 ) ; :: thesis: S1[n + 1]
then (PRIM:CompSeq G) . (n + 1) = [(((() . n) `1) \/ {(() . the Element of PRIM:NextBestEdges (() . n))}),(((() . n) `2) \/ { the Element of PRIM:NextBestEdges (() . n)})] by ;
then A6: ((PRIM:CompSeq G) . (n + 1)) `1 = ((() . n) `1) \/ {(() . the Element of PRIM:NextBestEdges (() . n))} ;
A7: the Element of PRIM:NextBestEdges (() . n) in PRIM:NextBestEdges (() . n) by A5;
now :: thesis: for v being object st v in (() . (n + 1)) `1 holds
v in G .reachableFrom the Element of the_Vertices_of G
end;
hence S1[n + 1] by TARSKI:def 3; :: thesis: verum
end;
suppose A9: ( PRIM:NextBestEdges (() . n) <> {} & not () . the Element of PRIM:NextBestEdges (() . n) in (() . n) `1 ) ; :: thesis: S1[n + 1]
then (PRIM:CompSeq G) . (n + 1) = [(((() . n) `1) \/ {(() . the Element of PRIM:NextBestEdges (() . n))}),(((() . n) `2) \/ { the Element of PRIM:NextBestEdges (() . n)})] by ;
then A10: ((PRIM:CompSeq G) . (n + 1)) `1 = ((() . n) `1) \/ {(() . the Element of PRIM:NextBestEdges (() . n))} ;
A11: the Element of PRIM:NextBestEdges (() . n) SJoins (() . n) `1 ,() \ ((() . n) `1),G by ;
then A12: the Element of PRIM:NextBestEdges (() . n) in the_Edges_of G ;
A13: (the_Target_of G) . the Element of PRIM:NextBestEdges (() . n) in (() . n) `1 by ;
now :: thesis: for v being object st v in (() . (n + 1)) `1 holds
v in G .reachableFrom the Element of the_Vertices_of G
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 ;
for n being Nat holds S1[n] from NAT_1:sch 2(A15, A2);
hence for n being Nat holds (() . n) `1 c= G .reachableFrom the Element of the_Vertices_of G ; :: thesis: verum