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 connected
defpred S1[ Nat] means for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . $1) `1 ,((PRIM:CompSeq G1) . $1) `2 holds G2 is connected ;
set G0 = (PRIM:CompSeq G1) . 0 ;
set v = choose (the_Vertices_of G1);
then A1:
S1[ 0 ]
;
now let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )assume A2:
S1[
n]
;
:: thesis: S1[n + 1]set Gn =
(PRIM:CompSeq G1) . n;
set Gn1 =
(PRIM:CompSeq G1) . (n + 1);
set e =
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n));
set v1 =
(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)));
set v2 =
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)));
A3:
(PRIM:CompSeq G1) . (n + 1) = PRIM:Step ((PRIM:CompSeq G1) . n)
by Def15;
now let Gn1s be
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . (n + 1)) `1 ,
((PRIM:CompSeq G1) . (n + 1)) `2 ;
:: thesis: Gn1s is connected
(
((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 A4:
(
the_Vertices_of Gn1s = ((PRIM:CompSeq G1) . (n + 1)) `1 &
the_Edges_of Gn1s = ((PRIM:CompSeq G1) . (n + 1)) `2 )
by GLIB_000:def 39;
now per cases
( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) = {} or ( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} & (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 ) or ( PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} & not (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 ) )
;
suppose A5:
(
PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} &
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 )
;
:: thesis: Gn1s is connected then A6:
(PRIM:CompSeq G1) . (n + 1) = [((((PRIM:CompSeq G1) . n) `1 ) \/ {((the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))))}),((((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))})]
by A3, Def14;
A7:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)
by A5;
then reconsider v1 =
(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as
Vertex of
G1 by FUNCT_2:7;
A8:
((PRIM:CompSeq G1) . (n + 1)) `1 = (((PRIM:CompSeq G1) . n) `1 ) \/ {v1}
by A6, MCART_1:7;
A9:
((PRIM:CompSeq G1) . (n + 1)) `2 = (((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))}
by A6, MCART_1:7;
consider Gns being
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 ;
A10:
Gns is
connected
by A2;
A11:
(
((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 A12:
(
the_Vertices_of Gns = ((PRIM:CompSeq G1) . n) `1 &
the_Edges_of Gns = ((PRIM:CompSeq G1) . n) `2 )
by GLIB_000:def 39;
then
(
the_Vertices_of Gns c= the_Vertices_of Gn1s &
the_Edges_of Gns c= the_Edges_of Gn1s )
by A4, A8, A9, XBOOLE_1:7;
then reconsider Gns =
Gns as
Subgraph of
Gn1s by GLIB_000:47;
consider src being
Vertex of
Gns;
reconsider src' =
src as
Vertex of
Gn1s by GLIB_000:45;
A14:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),
v1,
G1
by A7, GLIB_000:def 15;
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))}
by TARSKI:def 1;
then
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in the_Edges_of Gn1s
by A4, A9, XBOOLE_0:def 3;
then A15:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),
v1,
Gn1s
by A14, GLIB_000:76;
now let x be
Vertex of
Gn1s;
:: thesis: ex W being Walk of Gn1s st W is_Walk_from src',xnow per cases
( x = v1 or x <> v1 )
;
suppose A16:
x = v1
;
:: thesis: ex W being Walk of Gn1s st W is_Walk_from src',xreconsider v2' =
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as
Vertex of
Gns by A5, A11, GLIB_000:def 39;
consider W being
Walk of
Gns such that A17:
W is_Walk_from src,
v2'
by A10, GLIB_002:def 1;
reconsider W =
W as
Walk of
Gn1s by GLIB_001:168;
W is_Walk_from src',
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))
by A17, GLIB_001:20;
then
W .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) is_Walk_from src',
x
by A15, A16, GLIB_001:67;
hence
ex
W being
Walk of
Gn1s st
W is_Walk_from src',
x
;
:: thesis: verum end; hence
ex
W being
Walk of
Gn1s st
W is_Walk_from src',
x
;
:: thesis: verum end; hence
Gn1s is
connected
by GLIB_002:6;
:: thesis: verum end; suppose A19:
(
PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} & not
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 )
;
:: thesis: Gn1s is connected then A20:
(PRIM:CompSeq G1) . (n + 1) = [((((PRIM:CompSeq G1) . n) `1 ) \/ {((the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))))}),((((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))})]
by A3, Def14;
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) SJoins ((PRIM:CompSeq G1) . n) `1 ,
(the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1 ),
G1
by A19, Def12;
then A21:
(
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in the_Edges_of G1 &
(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 )
by A19, GLIB_000:def 17;
then reconsider v2 =
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as
Vertex of
G1 by FUNCT_2:7;
A22:
((PRIM:CompSeq G1) . (n + 1)) `1 = (((PRIM:CompSeq G1) . n) `1 ) \/ {v2}
by A20, MCART_1:7;
A23:
((PRIM:CompSeq G1) . (n + 1)) `2 = (((PRIM:CompSeq G1) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))}
by A20, MCART_1:7;
consider Gns being
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 ;
A24:
Gns is
connected
by A2;
A25:
(
((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 A26:
(
the_Vertices_of Gns = ((PRIM:CompSeq G1) . n) `1 &
the_Edges_of Gns = ((PRIM:CompSeq G1) . n) `2 )
by GLIB_000:def 39;
then
(
the_Vertices_of Gns c= the_Vertices_of Gn1s &
the_Edges_of Gns c= the_Edges_of Gn1s )
by A4, A22, A23, XBOOLE_1:7;
then reconsider Gns =
Gns as
Subgraph of
Gn1s by GLIB_000:47;
consider src being
Vertex of
Gns;
reconsider src' =
src as
Vertex of
Gn1s by GLIB_000:45;
A28:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),
v2,
G1
by A21, GLIB_000:def 15;
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))}
by TARSKI:def 1;
then
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in the_Edges_of Gn1s
by A4, A23, XBOOLE_0:def 3;
then A29:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),
v2,
Gn1s
by A28, GLIB_000:76;
now let x be
Vertex of
Gn1s;
:: thesis: ex W being Walk of Gn1s st W is_Walk_from src',xnow per cases
( x = v2 or x <> v2 )
;
suppose A30:
x = v2
;
:: thesis: ex W being Walk of Gn1s st W is_Walk_from src',xreconsider v1' =
(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as
Vertex of
Gns by A21, A25, GLIB_000:def 39;
consider W being
Walk of
Gns such that A31:
W is_Walk_from src,
v1'
by A24, GLIB_002:def 1;
reconsider W =
W as
Walk of
Gn1s by GLIB_001:168;
W is_Walk_from src',
(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))
by A31, GLIB_001:20;
then
W .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) is_Walk_from src',
x
by A29, A30, GLIB_001:67;
hence
ex
W being
Walk of
Gn1s st
W is_Walk_from src',
x
;
:: thesis: verum end; hence
ex
W being
Walk of
Gn1s st
W is_Walk_from src',
x
;
:: thesis: verum end; hence
Gn1s is
connected
by GLIB_002:6;
:: thesis: verum end; hence
Gn1s is
connected
;
:: thesis: verum end; hence
S1[
n + 1]
;
:: thesis: verum end;
then A33:
for n being Nat st S1[n] holds
S1[n + 1]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A33);
hence
for n being Nat
for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) . n) `1 ,((PRIM:CompSeq G1) . n) `2 holds G2 is connected
; :: thesis: verum