begin
theorem Th1:
begin
:: deftheorem Def1 defines connected GLIB_002:def 1 :
for G being _Graph holds
( G is connected iff for u, v being Vertex of G ex W being Walk of G st W is_Walk_from u,v );
:: deftheorem Def2 defines acyclic GLIB_002:def 2 :
for G being _Graph holds
( G is acyclic iff for W being Walk of G holds not W is Cycle-like );
:: deftheorem Def3 defines Tree-like GLIB_002:def 3 :
for G being _Graph holds
( G is Tree-like iff ( G is acyclic & G is connected ) );
:: deftheorem Def4 defines is_DTree_rooted_at GLIB_002:def 4 :
for G being _Graph
for v being set holds
( G is_DTree_rooted_at v iff ( G is Tree-like & ( for x being Vertex of G ex W being DWalk of G st W is_Walk_from v,x ) ) );
:: deftheorem Def5 defines .reachableFrom GLIB_002:def 5 :
for G being _Graph
for v being Vertex of G
for b3 being non empty Subset of (the_Vertices_of G) holds
( b3 = G .reachableFrom v iff for x being set holds
( x in b3 iff ex W being Walk of G st W is_Walk_from v,x ) );
:: deftheorem Def6 defines .reachableDFrom GLIB_002:def 6 :
for G being _Graph
for v being Vertex of G
for b3 being non empty Subset of (the_Vertices_of G) holds
( b3 = G .reachableDFrom v iff for x being set holds
( x in b3 iff ex W being DWalk of G st W is_Walk_from v,x ) );
Lm1:
for G being _Graph
for v being Vertex of G holds v in G .reachableFrom v
Lm2:
for G being _Graph
for v1 being Vertex of G
for e, x, y being set st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1
Lm3:
for G being _Graph
for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds
G .reachableFrom v1 = G .reachableFrom v2
Lm4:
for G being _Graph
for W being Walk of G
for v being Vertex of G st v in W .vertices() holds
W .vertices() c= G .reachableFrom v
:: deftheorem Def7 defines Component-like GLIB_002:def 7 :
for G1 being _Graph
for G2 being Subgraph of G1 holds
( G2 is Component-like iff ( G2 is connected & ( for G3 being connected Subgraph of G1 holds not G2 c< G3 ) ) );
:: deftheorem Def8 defines .componentSet() GLIB_002:def 8 :
for G being _Graph
for b2 being non empty Subset-Family of (the_Vertices_of G) holds
( b2 = G .componentSet() iff for x being set holds
( x in b2 iff ex v being Vertex of G st x = G .reachableFrom v ) );
:: deftheorem defines .numComponents() GLIB_002:def 9 :
for G being _Graph holds G .numComponents() = card (G .componentSet() );
:: deftheorem Def10 defines cut-vertex GLIB_002:def 10 :
for G being _Graph
for v being Vertex of G holds
( v is cut-vertex iff for G2 being removeVertex of G,v holds G .numComponents() in G2 .numComponents() );
:: deftheorem Def11 defines cut-vertex GLIB_002:def 11 :
for G being finite _Graph
for v being Vertex of G holds
( v is cut-vertex iff for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() );
Lm5:
for G1 being non trivial connected _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is endvertex holds
G2 is connected
Lm6:
for G being _Graph st ex v1 being Vertex of G st
for v2 being Vertex of G ex W being Walk of G st W is_Walk_from v1,v2 holds
G is connected
Lm7:
for G being _Graph st ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G holds
G is connected
Lm8:
for G being _Graph st G is connected holds
for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G
Lm9:
for G1, G2 being _Graph
for v1 being Vertex of G1
for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
Lm10:
for G1 being _Graph
for G2 being connected Subgraph of G1 st G2 is spanning holds
G1 is connected
Lm11:
for G being _Graph holds
( G is connected iff G .componentSet() = {(the_Vertices_of G)} )
Lm12:
for G1, G2 being _Graph st G1 == G2 holds
G1 .componentSet() = G2 .componentSet()
Lm13:
for G being _Graph
for x being set st x in G .componentSet() holds
x is non empty Subset of (the_Vertices_of G)
Lm14:
for G being _Graph
for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C)
Lm15:
for G being _Graph
for C1, C2 being Component of G holds
( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 )
Lm16:
for G being _Graph
for C being Component of G
for v being Vertex of G holds
( v in the_Vertices_of C iff the_Vertices_of C = G .reachableFrom v )
Lm17:
for G being _Graph
for C1, C2 being Component of G
for v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds
C1 == C2
Lm18:
for G being _Graph holds
( G is connected iff G .numComponents() = 1 )
Lm19:
for G being connected _Graph
for v being Vertex of G holds
( not v is cut-vertex iff for G2 being removeVertex of G,v holds G2 .numComponents() c= G .numComponents() )
Lm20:
for G being connected _Graph
for v being Vertex of G
for G2 being removeVertex of G,v st not v is cut-vertex holds
G2 is connected
Lm21:
for G being finite non trivial connected _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex )
Lm22:
for G being acyclic _Graph
for W being Path of G
for e being set st not e in W .edges() & e in (W .last() ) .edgesInOut() holds
W .addEdge e is Path-like
Lm23:
for G being finite non trivial acyclic _Graph st the_Edges_of G <> {} holds
ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v2 in G .reachableFrom v1 )
Lm24:
for G being finite non trivial Tree-like _Graph ex v1, v2 being Vertex of G st
( v1 <> v2 & v1 is endvertex & v2 is endvertex )
:: deftheorem Def12 defines connected GLIB_002:def 12 :
for GSq being GraphSeq holds
( GSq is connected iff for n being Nat holds GSq . n is connected );
:: deftheorem Def13 defines acyclic GLIB_002:def 13 :
for GSq being GraphSeq holds
( GSq is acyclic iff for n being Nat holds GSq . n is acyclic );
:: deftheorem Def14 defines Tree-like GLIB_002:def 14 :
for GSq being GraphSeq holds
( GSq is Tree-like iff for n being Nat holds GSq . n is Tree-like );
begin
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem
theorem
theorem Th8:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th38:
theorem
theorem Th40:
theorem
theorem
theorem
theorem Th44:
theorem
theorem Th46:
theorem
theorem Th48:
theorem
theorem