let G be _finite real-weighted WGraph; :: thesis: ( PRIM:CompSeq G is halting & ((PRIM:CompSeq G) .Lifespan()) + 1 = card (G .reachableFrom the Element of the_Vertices_of G) )
set PCS = PRIM:CompSeq G;
set src = the Element of the_Vertices_of G;
set RFS = G .reachableFrom the Element of the_Vertices_of G;
consider n being Nat such that
A1: n + 1 = card (G .reachableFrom the Element of the_Vertices_of G) by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
set Gn = (PRIM:CompSeq G) . n;
set Gn1 = (PRIM:CompSeq G) . (n + 1);
A2: card (G .reachableFrom the Element of the_Vertices_of G) <= (card (G .reachableFrom the Element of the_Vertices_of G)) + 1 by NAT_1:11;
A3: card (((PRIM:CompSeq G) . (n + 1)) `1) = min (((card (G .reachableFrom the Element of the_Vertices_of G)) + 1),(card (G .reachableFrom the Element of the_Vertices_of G))) by A1, Th36
.= card (G .reachableFrom the Element of the_Vertices_of G) by A2, XXREAL_0:def 9 ;
set e = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
A4: card (((PRIM:CompSeq G) . n) `1) = min ((card (G .reachableFrom the Element of the_Vertices_of G)),(card (G .reachableFrom the Element of the_Vertices_of G))) by A1, Th36
.= card (G .reachableFrom the Element of the_Vertices_of G) ;
A5: (PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n) by Def17;
then A6: ((PRIM:CompSeq G) . n) `1 c= ((PRIM:CompSeq G) . (n + 1)) `1 by Th29;
A7: now :: thesis: not ((PRIM:CompSeq G) . n) `1 <> ((PRIM:CompSeq G) . (n + 1)) `1
assume ((PRIM:CompSeq G) . n) `1 <> ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: contradiction
then ((PRIM:CompSeq G) . n) `1 c< ((PRIM:CompSeq G) . (n + 1)) `1 by A6, XBOOLE_0:def 8;
hence contradiction by A4, A3, CARD_2:48; :: thesis: verum
end;
now :: thesis: not PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {}
assume PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ; :: thesis: contradiction
then consider v being Vertex of G such that
A8: not v in ((PRIM:CompSeq G) . n) `1 and
A9: (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1) \/ {v}),((((PRIM:CompSeq G) . n) `2) \/ { the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n)})] by A5, Th28;
A10: v in {v} by TARSKI:def 1;
((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1) \/ {v} by A9;
hence contradiction by A7, A8, A10, XBOOLE_0:def 3; :: thesis: verum
end;
then A11: (PRIM:CompSeq G) . (n + 1) = (PRIM:CompSeq G) . n by A5, Def15;
hence A12: PRIM:CompSeq G is halting ; :: thesis: ((PRIM:CompSeq G) .Lifespan()) + 1 = card (G .reachableFrom the Element of the_Vertices_of G)
now :: thesis: for m being Nat st (PRIM:CompSeq G) . m = (PRIM:CompSeq G) . (m + 1) holds
n <= m
let m be Nat; :: thesis: ( (PRIM:CompSeq G) . m = (PRIM:CompSeq G) . (m + 1) implies n <= m )
set Gm = (PRIM:CompSeq G) . m;
assume A13: (PRIM:CompSeq G) . m = (PRIM:CompSeq G) . (m + 1) ; :: thesis: n <= m
now :: thesis: not m < n
assume m < n ; :: thesis: contradiction
then A14: m + 1 <= n by NAT_1:13;
n + 0 < card (G .reachableFrom the Element of the_Vertices_of G) by A1, XREAL_1:8;
then A15: m + 1 < card (G .reachableFrom the Element of the_Vertices_of G) by A14, XXREAL_0:2;
then A16: (m + 1) + 1 <= card (G .reachableFrom the Element of the_Vertices_of G) by NAT_1:13;
A17: card (((PRIM:CompSeq G) . m) `1) = min ((m + 1),(card (G .reachableFrom the Element of the_Vertices_of G))) by Th36
.= m + 1 by A15, XXREAL_0:def 9 ;
card (((PRIM:CompSeq G) . m) `1) = min (((m + 1) + 1),(card (G .reachableFrom the Element of the_Vertices_of G))) by A13, Th36
.= (m + 1) + 1 by A16, XXREAL_0:def 9 ;
hence contradiction by A17; :: thesis: verum
end;
hence n <= m ; :: thesis: verum
end;
hence ((PRIM:CompSeq G) .Lifespan()) + 1 = card (G .reachableFrom the Element of the_Vertices_of G) by A1, A11, A12, GLIB_000:def 56; :: thesis: verum