let G1 be finite real-weighted WGraph; 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);
now let n be
Nat;
( S1[n] implies 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));
set G3 = the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 ;
A1:
(PRIM:CompSeq G1) . (n + 1) = PRIM:Step ((PRIM:CompSeq G1) . n)
by Def17;
A2:
((PRIM:CompSeq G1) . n) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . n) `1)
by Th30;
((PRIM:CompSeq G1) . n) `1 is non
empty Subset of
(the_Vertices_of G1)
by Th30;
then A3:
(
the_Vertices_of the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 = ((PRIM:CompSeq G1) . n) `1 &
the_Edges_of the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 = ((PRIM:CompSeq G1) . n) `2 )
by A2, GLIB_000:def 37;
assume A4:
S1[
n]
;
S1[n + 1]then A5:
the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 is
Tree-like
;
now A6:
the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 .order() = ( the inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 .size()) + 1
by A5, GLIB_002:46;
let G2 be
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . (n + 1)) `1 ,
((PRIM:CompSeq G1) . (n + 1)) `2 ;
G2 is Tree-like A7:
((PRIM:CompSeq G1) . (n + 1)) `2 c= G1 .edgesBetween (((PRIM:CompSeq G1) . (n + 1)) `1)
by Th30;
((PRIM:CompSeq G1) . (n + 1)) `1 is non
empty Subset of
(the_Vertices_of G1)
by Th30;
then A8:
the_Vertices_of G2 = ((PRIM:CompSeq G1) . (n + 1)) `1
by A7, GLIB_000:def 37;
now per cases
( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) = {} or PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} )
;
suppose A9:
PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {}
;
G2 is Tree-like set GnV =
((PRIM:CompSeq G1) . n) `1 ;
set GnVg =
(the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1);
A10:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) SJoins ((PRIM:CompSeq G1) . n) `1 ,
(the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1),
G1
by A9, Def13;
consider v being
Vertex of
G1 such that A14:
not
v in ((PRIM:CompSeq G1) . n) `1
and A15:
(PRIM:CompSeq G1) . (n + 1) = [((((PRIM:CompSeq G1) . n) `1) \/ {v}),((((PRIM:CompSeq G1) . n) `2) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))})]
by A1, A9, Th28;
A16:
card (((PRIM:CompSeq G1) . (n + 1)) `1) =
card ((((PRIM:CompSeq G1) . n) `1) \/ {v})
by A15, MCART_1:7
.=
(card (((PRIM:CompSeq G1) . n) `1)) + 1
by A14, CARD_2:41
;
card (((PRIM:CompSeq G1) . (n + 1)) `2) =
card ((((PRIM:CompSeq G1) . n) `2) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))})
by A15, MCART_1:7
.=
(card (((PRIM:CompSeq G1) . n) `2)) + 1
by A11, CARD_2:41
;
then
G2 .order() = (G2 .size()) + 1
by A3, A7, A8, A6, A16, GLIB_000:def 37;
hence
G2 is
Tree-like
by GLIB_002:47;
verum end; hence
G2 is
Tree-like
;
verum end; hence
S1[
n + 1]
;
verum end;
then A17:
for n being Nat st S1[n] holds
S1[n + 1]
;
(PRIM:CompSeq G1) . 0 = PRIM:Init G1
by Def17;
then
( ((PRIM:CompSeq G1) . 0) `1 = {(choose (the_Vertices_of G1))} & ((PRIM:CompSeq G1) . 0) `2 = {} )
by MCART_1:7;
then A18:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A18, 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
; verum