let G be _finite real-weighted WGraph; for n being Nat holds card (((PRIM:CompSeq G) . n) `1) = min ((n + 1),(card (G .reachableFrom the Element of the_Vertices_of G)))
set CS = PRIM:CompSeq G;
set src = the Element of the_Vertices_of G;
defpred S1[ Nat] means card (((PRIM:CompSeq G) . $1) `1) = min (($1 + 1),(card (G .reachableFrom the Element of the_Vertices_of G)));
set G0 = (PRIM:CompSeq G) . 0;
the Element of the_Vertices_of G in G .reachableFrom the Element of the_Vertices_of G
by GLIB_002:9;
then
{ the Element of the_Vertices_of G} c= G .reachableFrom the Element of the_Vertices_of G
by ZFMISC_1:31;
then
card { the Element of the_Vertices_of G} <= card (G .reachableFrom the Element of the_Vertices_of G)
by NAT_1:43;
then A1:
0 + 1 <= card (G .reachableFrom the Element of the_Vertices_of G)
by CARD_1:30;
A2:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A3:
S1[
n]
;
S1[n + 1]set Gn =
(PRIM:CompSeq G) . n;
set Gn1 =
(PRIM:CompSeq G) . (n + 1);
set e = the
Element of
PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
A4:
(PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n)
by Def17;
now S1[n + 1]per cases
( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} or PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} )
;
suppose A8:
PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {}
;
S1[n + 1]A9:
((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the
Element of
the_Vertices_of G
by Th33;
A10:
((PRIM:CompSeq G) . n) `1 <> G .reachableFrom the
Element of
the_Vertices_of G
by A8, Th35;
then A13:
card (((PRIM:CompSeq G) . n) `1) = n + 1
by A3, XXREAL_0:15;
consider v being
Vertex of
G such that A14:
not
v in ((PRIM:CompSeq G) . n) `1
and A15:
(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 A4, A8, Th28;
A16:
card (((PRIM:CompSeq G) . (n + 1)) `1) =
card ((((PRIM:CompSeq G) . n) `1) \/ {v})
by A15
.=
(card (((PRIM:CompSeq G) . n) `1)) + 1
by A14, CARD_2:41
;
card (((PRIM:CompSeq G) . n) `1) <= card (G .reachableFrom the Element of the_Vertices_of G)
by Th33, NAT_1:43;
then
n + 1
< card (G .reachableFrom the Element of the_Vertices_of G)
by A11, A13, XXREAL_0:1;
then
(n + 1) + 1
<= card (G .reachableFrom the Element of the_Vertices_of G)
by NAT_1:13;
hence
S1[
n + 1]
by A16, A13, XXREAL_0:def 9;
verum end; end; end; hence
S1[
n + 1]
;
verum end;
(PRIM:CompSeq G) . 0 = PRIM:Init G
by Def17;
then
{ the Element of the_Vertices_of G} = ((PRIM:CompSeq G) . 0) `1
;
then
card (((PRIM:CompSeq G) . 0) `1) = 1
by CARD_1:30;
then A17:
S1[ 0 ]
by A1, XXREAL_0:def 9;
for n being Nat holds S1[n]
from NAT_1:sch 2(A17, A2);
hence
for n being Nat holds card (((PRIM:CompSeq G) . n) `1) = min ((n + 1),(card (G .reachableFrom the Element of the_Vertices_of G)))
; verum