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 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);
now let n be
Nat;
( S1[n] implies S1[n + 1] )assume A1:
S1[
n]
;
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)));
A2:
(PRIM:CompSeq G1) . (n + 1) = PRIM:Step ((PRIM:CompSeq G1) . n)
by Def17;
now let Gn1s be
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . (n + 1)) `1 ,
((PRIM:CompSeq G1) . (n + 1)) `2 ;
Gn1s is connected A3:
(
((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 Th30;
then A4:
the_Vertices_of Gn1s = ((PRIM:CompSeq G1) . (n + 1)) `1
by GLIB_000:def 37;
A5:
the_Edges_of Gn1s = ((PRIM:CompSeq G1) . (n + 1)) `2
by A3, GLIB_000:def 37;
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 A6:
(
PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} &
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 )
;
Gn1s is connected then A7:
(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 A2, Def15;
then A8:
((PRIM:CompSeq G1) . (n + 1)) `2 = (((PRIM:CompSeq G1) . n) `2) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))}
by MCART_1:7;
A9:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)
by A6;
then reconsider v1 =
(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as
Vertex of
G1 by FUNCT_2:5;
A10:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),
v1,
G1
by A9, GLIB_000:def 13;
set Gns = the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 ;
A11:
the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 is
connected
by A1;
A12:
(
((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 Th30;
then A13:
the_Vertices_of the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 = ((PRIM:CompSeq G1) . n) `1
by GLIB_000:def 37;
A14:
((PRIM:CompSeq G1) . (n + 1)) `1 = (((PRIM:CompSeq G1) . n) `1) \/ {v1}
by A7, MCART_1:7;
then A15:
the_Vertices_of the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 c= the_Vertices_of Gn1s
by A4, A13, XBOOLE_1:7;
the_Edges_of the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 = ((PRIM:CompSeq G1) . n) `2
by A12, GLIB_000:def 37;
then reconsider Gns = the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 as
Subgraph of
Gn1s by A5, A8, A15, GLIB_000:44, XBOOLE_1:7;
set src = the
Vertex of
Gns;
reconsider src9 = the
Vertex of
Gns as
Vertex of
Gn1s by GLIB_000:42;
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 A5, A8, XBOOLE_0:def 3;
then A16:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),
v1,
Gn1s
by A10, GLIB_000:73;
now let x be
Vertex of
Gn1s;
ex W being Walk of Gn1s st W is_Walk_from src9,xnow per cases
( x = v1 or x <> v1 )
;
suppose A17:
x = v1
;
ex W being Walk of Gn1s st W is_Walk_from src9,xreconsider v29 =
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as
Vertex of
Gns by A6, A12, GLIB_000:def 37;
consider W being
Walk of
Gns such that A18:
W is_Walk_from the
Vertex of
Gns,
v29
by A11, GLIB_002:def 1;
reconsider W =
W as
Walk of
Gn1s by GLIB_001:167;
W is_Walk_from src9,
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))
by A18, GLIB_001:19;
then
W .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) is_Walk_from src9,
x
by A16, A17, GLIB_001:66;
hence
ex
W being
Walk of
Gn1s st
W is_Walk_from src9,
x
;
verum end; hence
ex
W being
Walk of
Gn1s st
W is_Walk_from src9,
x
;
verum end; hence
Gn1s is
connected
by GLIB_002:6;
verum end; suppose A20:
(
PRIM:NextBestEdges ((PRIM:CompSeq G1) . n) <> {} & not
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1 )
;
Gn1s is connected then A21:
(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 A2, Def15;
then A22:
((PRIM:CompSeq G1) . (n + 1)) `2 = (((PRIM:CompSeq G1) . n) `2) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))}
by MCART_1:7;
A23:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) SJoins ((PRIM:CompSeq G1) . n) `1 ,
(the_Vertices_of G1) \ (((PRIM:CompSeq G1) . n) `1),
G1
by A20, Def13;
then A24:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) in the_Edges_of G1
by GLIB_000:def 15;
then reconsider v2 =
(the_Source_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as
Vertex of
G1 by FUNCT_2:5;
A25:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),
v2,
G1
by A24, GLIB_000:def 13;
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 A5, A22, XBOOLE_0:def 3;
then A26:
choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)) Joins (the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))),
v2,
Gn1s
by A25, GLIB_000:73;
set Gns = the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 ;
A27:
the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 is
connected
by A1;
A28:
(
((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 Th30;
then A29:
the_Vertices_of the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 = ((PRIM:CompSeq G1) . n) `1
by GLIB_000:def 37;
A30:
((PRIM:CompSeq G1) . (n + 1)) `1 = (((PRIM:CompSeq G1) . n) `1) \/ {v2}
by A21, MCART_1:7;
then A31:
the_Vertices_of the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 c= the_Vertices_of Gn1s
by A4, A29, XBOOLE_1:7;
the_Edges_of the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 = ((PRIM:CompSeq G1) . n) `2
by A28, GLIB_000:def 37;
then reconsider Gns = the
inducedSubgraph of
G1,
((PRIM:CompSeq G1) . n) `1 ,
((PRIM:CompSeq G1) . n) `2 as
Subgraph of
Gn1s by A5, A22, A31, GLIB_000:44, XBOOLE_1:7;
set src = the
Vertex of
Gns;
reconsider src9 = the
Vertex of
Gns as
Vertex of
Gn1s by GLIB_000:42;
A32:
(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) in ((PRIM:CompSeq G1) . n) `1
by A20, A23, GLIB_000:def 15;
now let x be
Vertex of
Gn1s;
ex W being Walk of Gn1s st W is_Walk_from src9,xnow per cases
( x = v2 or x <> v2 )
;
suppose A33:
x = v2
;
ex W being Walk of Gn1s st W is_Walk_from src9,xreconsider v19 =
(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) as
Vertex of
Gns by A32, A28, GLIB_000:def 37;
consider W being
Walk of
Gns such that A34:
W is_Walk_from the
Vertex of
Gns,
v19
by A27, GLIB_002:def 1;
reconsider W =
W as
Walk of
Gn1s by GLIB_001:167;
W is_Walk_from src9,
(the_Target_of G1) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n)))
by A34, GLIB_001:19;
then
W .addEdge (choose (PRIM:NextBestEdges ((PRIM:CompSeq G1) . n))) is_Walk_from src9,
x
by A26, A33, GLIB_001:66;
hence
ex
W being
Walk of
Gn1s st
W is_Walk_from src9,
x
;
verum end; hence
ex
W being
Walk of
Gn1s st
W is_Walk_from src9,
x
;
verum end; hence
Gn1s is
connected
by GLIB_002:6;
verum end; hence
Gn1s is
connected
;
verum end; hence
S1[
n + 1]
;
verum end;
then A36:
for n being Nat st S1[n] holds
S1[n + 1]
;
then A38:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A38, A36);
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
; verum