let G1 be finite real-weighted WGraph; :: thesis: for n being Nat
for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is Tree-like
set PCS = PRIM:CompSeq G1;
defpred S1[ Nat] means for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . $1) `1 ,((PRIM:CompSeq G1) . $1) `2 holds G2 is Tree-like ;
set G0 = (PRIM:CompSeq G1) . 0 ;
set src = choose (the_Vertices_of G1);
(PRIM:CompSeq G1) . 0 = PRIM:Init G1
by Def15;
then A1:
( ((PRIM:CompSeq G1) . 0 ) `1 = {(choose (the_Vertices_of G1))} & ((PRIM:CompSeq G1) . 0 ) `2 = {} )
by MCART_1:7;
A2:
S1[ 0 ]
by A1;
now let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )assume A3:
S1[
n]
;
:: thesis: S1[n + 1]set Gn =
(PRIM:CompSeq G1) . n;
set Gn1 =
(PRIM:CompSeq G1) . (n + 1);
set Next =
PRIM:NextBestEdges ((PRIM:CompSeq G1) . n);
set e =
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n));
A4:
(PRIM:CompSeq G1) . (n + 1) = PRIM:Step ((PRIM:CompSeq G1) . n)
by Def15;
consider G3 being
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 ;
A5:
G3 is
Tree-like
by A3;
A6:
(
((PRIM:CompSeq G1) . n) `1 is non
empty Subset of
(the_Vertices_of G1) &
((PRIM:CompSeq G1) . n) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . n) `1 ) )
by Lm9;
then A7:
(
the_Vertices_of G3 = ((PRIM:CompSeq G1) . n) `1 &
the_Edges_of G3 = ((PRIM:CompSeq G1) . n) `2 )
by GLIB_000:def 39;
now let G2 be
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . (n + 1)) `1 ,
((PRIM:CompSeq G1) . (n + 1)) `2 ;
:: thesis: G2 is Tree-like
(
((PRIM:CompSeq G1) . (n + 1)) `1 is non
empty Subset of
(the_Vertices_of G1) &
((PRIM:CompSeq G1) . (n + 1)) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . (n + 1)) `1 ) )
by Lm9;
then A9:
(
the_Vertices_of G2 = ((PRIM:CompSeq G1) . (n + 1)) `1 &
the_Edges_of G2 = ((PRIM:CompSeq G1) . (n + 1)) `2 )
by GLIB_000:def 39;
A10:
G3 .order() = (G3 .size() ) + 1
by A5, GLIB_002:46;
now per cases
( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) = {} or PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} )
;
suppose A11:
PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {}
;
:: thesis: G2 is Tree-like then consider v being
Vertex of
G1 such that A12:
( not
v in ((PRIM:CompSeq G1) . n) `1 &
(PRIM:CompSeq G1) . (n + 1) = [((((PRIM:CompSeq G1) . n) `1 ) \/ {v}),((((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))})] )
by A4, Lm6;
set GnV =
((PRIM:CompSeq G1) . n) `1 ;
set GnVg =
(the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1 );
A13:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) SJoins ((PRIM:CompSeq G1) . n) `1 ,
(the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1 ),
G1
by A11, Def12;
A15:
card (((PRIM:CompSeq G1) . (n + 1)) `2 ) =
card ((((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))})
by A12, MCART_1:7
.=
(card (((PRIM:CompSeq G1) . n) `2 )) + 1
by A14a, CARD_2:54
;
card (((PRIM:CompSeq G1) . (n + 1)) `1 ) =
card ((((PRIM:CompSeq G1) . n) `1 ) \/ {v})
by A12, MCART_1:7
.=
(card (((PRIM:CompSeq G1) . n) `1 )) + 1
by A12, CARD_2:54
;
then
G2 .order() = (G2 .size() ) + 1
by A7, A9, A10, A15;
hence
G2 is
Tree-like
by GLIB_002:47;
:: thesis: verum end; hence
G2 is
Tree-like
;
:: thesis: verum end; hence
S1[
n + 1]
;
:: thesis: verum end;
then A17:
for n being Nat st S1[n] holds
S1[n + 1]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A2, A17);
hence
for n being Nat
for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is Tree-like
; :: thesis: verum