:: by Gilbert Lee

::

:: Received February 22, 2005

:: Copyright (c) 2005-2019 Association of Mizar Users

definition

let G be _Graph;

end;
attr G is connected means :Def1: :: GLIB_002:def 1

for u, v being Vertex of G ex W being Walk of G st W is_Walk_from u,v;

for u, v being Vertex of G ex W being Walk of G st W is_Walk_from u,v;

:: 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 );

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 );

for G being _Graph holds

( G is acyclic iff for W being Walk of G holds not W is Cycle-like );

definition
end;

:: deftheorem defines Tree-like GLIB_002:def 3 :

for G being _Graph holds

( G is Tree-like iff ( G is acyclic & G is connected ) );

for G being _Graph holds

( G is Tree-like iff ( G is acyclic & G is connected ) );

registration

for b_{1} being _Graph st b_{1} is trivial holds

b_{1} is connected
end;

cluster Relation-like omega -defined Function-like V34() [Graph-like] trivial -> connected for set ;

coherence for b

b

proof end;

registration

for b_{1} being _Graph st b_{1} is trivial & b_{1} is loopless holds

b_{1} is Tree-like
end;

cluster Relation-like omega -defined Function-like V34() [Graph-like] loopless trivial -> Tree-like for set ;

coherence for b

b

proof end;

registration
end;

registration

for b_{1} being _Graph st b_{1} is Tree-like holds

( b_{1} is acyclic & b_{1} is connected )
;

end;

cluster Relation-like omega -defined Function-like V34() [Graph-like] Tree-like -> connected acyclic for set ;

coherence for b

( b

registration

for b_{1} being _Graph st b_{1} is acyclic & b_{1} is connected holds

b_{1} is Tree-like
;

end;

cluster Relation-like omega -defined Function-like V34() [Graph-like] connected acyclic -> Tree-like for set ;

coherence for b

b

registration

let G be _Graph;

let v be Vertex of G;

coherence

for b_{1} being inducedSubgraph of G,{v}, {} holds b_{1} is Tree-like
;

end;
let v be Vertex of G;

coherence

for b

definition

let G be _Graph;

let v be set ;

end;
let v be set ;

pred G is_DTree_rooted_at v means :: GLIB_002:def 4

( G is Tree-like & ( for x being Vertex of G ex W being DWalk of G st W is_Walk_from v,x ) );

( G is Tree-like & ( for x being Vertex of G ex W being DWalk of G st W is_Walk_from v,x ) );

:: deftheorem 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 ) ) );

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 ) ) );

registration

ex b_{1} being _Graph st

( b_{1} is trivial & b_{1} is finite & b_{1} is Tree-like )

ex b_{1} being _Graph st

( not b_{1} is trivial & b_{1} is finite & b_{1} is Tree-like )
end;

cluster Relation-like omega -defined Function-like V34() [Graph-like] finite trivial Tree-like for set ;

existence ex b

( b

proof end;

cluster Relation-like omega -defined Function-like V34() [Graph-like] finite non trivial Tree-like for set ;

existence ex b

( not b

proof end;

registration

let G be _Graph;

ex b_{1} being Subgraph of G st

( b_{1} is trivial & b_{1} is finite & b_{1} is Tree-like )

end;
cluster Relation-like omega -defined Function-like V34() [Graph-like] finite trivial Tree-like for Subgraph of G;

existence ex b

( b

proof end;

registration
end;

definition

let G be _Graph;

let v be Vertex of G;

ex b_{1} being non empty Subset of (the_Vertices_of G) st

for x being object holds

( x in b_{1} iff ex W being Walk of G st W is_Walk_from v,x )

for b_{1}, b_{2} being non empty Subset of (the_Vertices_of G) st ( for x being object holds

( x in b_{1} iff ex W being Walk of G st W is_Walk_from v,x ) ) & ( for x being object holds

( x in b_{2} iff ex W being Walk of G st W is_Walk_from v,x ) ) holds

b_{1} = b_{2}

end;
let v be Vertex of G;

func G .reachableFrom v -> non empty Subset of (the_Vertices_of G) means :Def5: :: GLIB_002:def 5

for x being object holds

( x in it iff ex W being Walk of G st W is_Walk_from v,x );

existence for x being object holds

( x in it iff ex W being Walk of G st W is_Walk_from v,x );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def5 defines .reachableFrom GLIB_002:def 5 :

for G being _Graph

for v being Vertex of G

for b_{3} being non empty Subset of (the_Vertices_of G) holds

( b_{3} = G .reachableFrom v iff for x being object holds

( x in b_{3} iff ex W being Walk of G st W is_Walk_from v,x ) );

for G being _Graph

for v being Vertex of G

for b

( b

( x in b

definition

let G be _Graph;

let v be Vertex of G;

ex b_{1} being non empty Subset of (the_Vertices_of G) st

for x being object holds

( x in b_{1} iff ex W being DWalk of G st W is_Walk_from v,x )

for b_{1}, b_{2} being non empty Subset of (the_Vertices_of G) st ( for x being object holds

( x in b_{1} iff ex W being DWalk of G st W is_Walk_from v,x ) ) & ( for x being object holds

( x in b_{2} iff ex W being DWalk of G st W is_Walk_from v,x ) ) holds

b_{1} = b_{2}

end;
let v be Vertex of G;

func G .reachableDFrom v -> non empty Subset of (the_Vertices_of G) means :Def6: :: GLIB_002:def 6

for x being object holds

( x in it iff ex W being DWalk of G st W is_Walk_from v,x );

existence for x being object holds

( x in it iff ex W being DWalk of G st W is_Walk_from v,x );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def6 defines .reachableDFrom GLIB_002:def 6 :

for G being _Graph

for v being Vertex of G

for b_{3} being non empty Subset of (the_Vertices_of G) holds

( b_{3} = G .reachableDFrom v iff for x being object holds

( x in b_{3} iff ex W being DWalk of G st W is_Walk_from v,x ) );

for G being _Graph

for v being Vertex of G

for b

( b

( x in b

Lm1: for G being _Graph

for v being Vertex of G holds v in G .reachableFrom v

proof end;

Lm2: for G being _Graph

for v1 being Vertex of G

for e, x, y being object st x in G .reachableFrom v1 & e Joins x,y,G holds

y in G .reachableFrom v1

proof end;

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

proof end;

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

proof end;

definition

let G1 be _Graph;

let G2 be Subgraph of G1;

end;
let G2 be Subgraph of G1;

attr G2 is Component-like means :Def7: :: GLIB_002:def 7

( G2 is connected & ( for G3 being connected Subgraph of G1 holds not G2 c< G3 ) );

( G2 is connected & ( for G3 being connected Subgraph of G1 holds not G2 c< G3 ) );

:: 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 ) ) );

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 ) ) );

registration

let G be _Graph;

coherence

for b_{1} being Subgraph of G st b_{1} is Component-like holds

b_{1} is connected
;

end;
coherence

for b

b

registration

let G be _Graph;

let v be Vertex of G;

for b_{1} being inducedSubgraph of G,(G .reachableFrom v) holds b_{1} is Component-like

end;
let v be Vertex of G;

cluster -> Component-like for inducedSubgraph of G,G .reachableFrom v,G .edgesBetween (G .reachableFrom v);

coherence for b

proof end;

registration

let G be _Graph;

ex b_{1} being Subgraph of G st b_{1} is Component-like

end;
cluster Relation-like omega -defined Function-like V34() [Graph-like] Component-like for Subgraph of G;

existence ex b

proof end;

definition

let G be _Graph;

ex b_{1} being non empty Subset-Family of (the_Vertices_of G) st

for x being set holds

( x in b_{1} iff ex v being Vertex of G st x = G .reachableFrom v )

for b_{1}, b_{2} being non empty Subset-Family of (the_Vertices_of G) st ( for x being set holds

( x in b_{1} iff ex v being Vertex of G st x = G .reachableFrom v ) ) & ( for x being set holds

( x in b_{2} iff ex v being Vertex of G st x = G .reachableFrom v ) ) holds

b_{1} = b_{2}

end;
func G .componentSet() -> non empty Subset-Family of (the_Vertices_of G) means :Def8: :: GLIB_002:def 8

for x being set holds

( x in it iff ex v being Vertex of G st x = G .reachableFrom v );

existence for x being set holds

( x in it iff ex v being Vertex of G st x = G .reachableFrom v );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def8 defines .componentSet() GLIB_002:def 8 :

for G being _Graph

for b_{2} being non empty Subset-Family of (the_Vertices_of G) holds

( b_{2} = G .componentSet() iff for x being set holds

( x in b_{2} iff ex v being Vertex of G st x = G .reachableFrom v ) );

for G being _Graph

for b

( b

( x in b

registration

let G be _Graph;

let X be Element of G .componentSet() ;

coherence

for b_{1} being inducedSubgraph of G,X holds b_{1} is Component-like

end;
let X be Element of G .componentSet() ;

coherence

for b

proof end;

:: deftheorem defines .numComponents() GLIB_002:def 9 :

for G being _Graph holds G .numComponents() = card (G .componentSet());

for G being _Graph holds G .numComponents() = card (G .componentSet());

definition

let G be finite _Graph;

:: original: .numComponents()

redefine func G .numComponents() -> non zero Element of NAT ;

coherence

G .numComponents() is non zero Element of NAT

end;
:: original: .numComponents()

redefine func G .numComponents() -> non zero Element of NAT ;

coherence

G .numComponents() is non zero Element of NAT

proof end;

definition

let G be _Graph;

let v be Vertex of G;

end;
let v be Vertex of G;

attr v is cut-vertex means :: GLIB_002:def 10

for G2 being removeVertex of G,v holds G .numComponents() in G2 .numComponents() ;

for G2 being removeVertex of G,v holds G .numComponents() in G2 .numComponents() ;

:: deftheorem 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() );

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() );

definition

let G be finite _Graph;

let v be Vertex of G;

( v is cut-vertex iff for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() )

end;
let v be Vertex of G;

redefine attr v is cut-vertex means :: GLIB_002:def 11

for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() ;

compatibility for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() ;

( v is cut-vertex iff for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() )

proof end;

:: deftheorem 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() );

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

proof end;

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

proof end;

Lm7: for G being _Graph st ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G holds

G is connected

proof end;

Lm8: for G being _Graph st G is connected holds

for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G

proof end;

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

proof end;

Lm10: for G1 being _Graph

for G2 being connected Subgraph of G1 st G2 is spanning holds

G1 is connected

proof end;

Lm11: for G being _Graph holds

( G is connected iff G .componentSet() = {(the_Vertices_of G)} )

proof end;

Lm12: for G1, G2 being _Graph st G1 == G2 holds

G1 .componentSet() = G2 .componentSet()

proof end;

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)

proof end;

Lm14: for G being _Graph

for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C)

proof end;

Lm15: for G being _Graph

for C1, C2 being Component of G holds

( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 )

proof end;

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 )

proof end;

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

proof end;

Lm18: for G being _Graph holds

( G is connected iff G .numComponents() = 1 )

proof end;

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() )

proof end;

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

proof end;

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 )

proof end;

registration

let G be finite non trivial connected _Graph;

existence

not for b_{1} being Vertex of G holds b_{1} is cut-vertex

end;
existence

not for b

proof end;

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

proof end;

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 )

proof end;

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 )

proof end;

registration

let G be finite non trivial Tree-like _Graph;

existence

ex b_{1} being Vertex of G st b_{1} is endvertex

end;
existence

ex b

proof end;

registration

let G be finite non trivial Tree-like _Graph;

let v be endvertex Vertex of G;

for b_{1} being removeVertex of G,v holds b_{1} is Tree-like
by Lm5;

end;
let v be endvertex Vertex of G;

cluster -> Tree-like for inducedSubgraph of G,(the_Vertices_of G) \ {v},G .edgesBetween ((the_Vertices_of G) \ {v});

coherence for b

definition

let GF be Graph-yielding Function;

end;
attr GF is connected means :: GLIB_002:def 12

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is connected );

for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is connected );

:: deftheorem defines connected GLIB_002:def 12 :

for GF being Graph-yielding Function holds

( GF is connected iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is connected ) );

for GF being Graph-yielding Function holds

( GF is connected iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is connected ) );

:: deftheorem defines acyclic GLIB_002:def 13 :

for GF being Graph-yielding Function holds

( GF is acyclic iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is acyclic ) );

for GF being Graph-yielding Function holds

( GF is acyclic iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is acyclic ) );

:: deftheorem defines Tree-like GLIB_002:def 14 :

for GF being Graph-yielding Function holds

( GF is Tree-like iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is Tree-like ) );

for GF being Graph-yielding Function holds

( GF is Tree-like iff for x being object st x in dom GF holds

ex G being _Graph st

( GF . x = G & G is Tree-like ) );

definition

let GF be non empty Graph-yielding Function;

( GF is connected iff for x being Element of dom GF holds GF . x is connected )

( GF is acyclic iff for x being Element of dom GF holds GF . x is acyclic )

( GF is Tree-like iff for x being Element of dom GF holds GF . x is Tree-like )

end;
redefine attr GF is connected means :Def12b: :: GLIB_002:def 15

for x being Element of dom GF holds GF . x is connected ;

compatibility for x being Element of dom GF holds GF . x is connected ;

( GF is connected iff for x being Element of dom GF holds GF . x is connected )

proof end;

redefine attr GF is acyclic means :Def13b: :: GLIB_002:def 16

for x being Element of dom GF holds GF . x is acyclic ;

compatibility for x being Element of dom GF holds GF . x is acyclic ;

( GF is acyclic iff for x being Element of dom GF holds GF . x is acyclic )

proof end;

redefine attr GF is Tree-like means :: GLIB_002:def 17

for x being Element of dom GF holds GF . x is Tree-like ;

compatibility for x being Element of dom GF holds GF . x is Tree-like ;

( GF is Tree-like iff for x being Element of dom GF holds GF . x is Tree-like )

proof end;

:: deftheorem Def12b defines connected GLIB_002:def 15 :

for GF being non empty Graph-yielding Function holds

( GF is connected iff for x being Element of dom GF holds GF . x is connected );

for GF being non empty Graph-yielding Function holds

( GF is connected iff for x being Element of dom GF holds GF . x is connected );

:: deftheorem Def13b defines acyclic GLIB_002:def 16 :

for GF being non empty Graph-yielding Function holds

( GF is acyclic iff for x being Element of dom GF holds GF . x is acyclic );

for GF being non empty Graph-yielding Function holds

( GF is acyclic iff for x being Element of dom GF holds GF . x is acyclic );

:: deftheorem defines Tree-like GLIB_002:def 17 :

for GF being non empty Graph-yielding Function holds

( GF is Tree-like iff for x being Element of dom GF holds GF . x is Tree-like );

for GF being non empty Graph-yielding Function holds

( GF is Tree-like iff for x being Element of dom GF holds GF . x is Tree-like );

LmNat: for F being ManySortedSet of NAT

for n being object holds

( n is Nat iff n in dom F )

proof end;

definition

let GSq be GraphSeq;

( GSq is connected iff for n being Nat holds GSq . n is connected )

( GSq is acyclic iff for n being Nat holds GSq . n is acyclic )

( GSq is Tree-like iff for n being Nat holds GSq . n is Tree-like )

end;
redefine attr GSq is connected means :Def12: :: GLIB_002:def 18

for n being Nat holds GSq . n is connected ;

compatibility for n being Nat holds GSq . n is connected ;

( GSq is connected iff for n being Nat holds GSq . n is connected )

proof end;

redefine attr GSq is acyclic means :Def13: :: GLIB_002:def 19

for n being Nat holds GSq . n is acyclic ;

compatibility for n being Nat holds GSq . n is acyclic ;

( GSq is acyclic iff for n being Nat holds GSq . n is acyclic )

proof end;

redefine attr GSq is Tree-like means :: GLIB_002:def 20

for n being Nat holds GSq . n is Tree-like ;

compatibility for n being Nat holds GSq . n is Tree-like ;

( GSq is Tree-like iff for n being Nat holds GSq . n is Tree-like )

proof end;

:: deftheorem Def12 defines connected GLIB_002:def 18 :

for GSq being GraphSeq holds

( GSq is connected iff for n being Nat holds GSq . n is connected );

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 19 :

for GSq being GraphSeq holds

( GSq is acyclic iff for n being Nat holds GSq . n is acyclic );

for GSq being GraphSeq holds

( GSq is acyclic iff for n being Nat holds GSq . n is acyclic );

:: deftheorem defines Tree-like GLIB_002:def 20 :

for GSq being GraphSeq holds

( GSq is Tree-like iff for n being Nat holds GSq . n is Tree-like );

for GSq being GraphSeq holds

( GSq is Tree-like iff for n being Nat holds GSq . n is Tree-like );

registration

existence

ex b_{1} being Graph-yielding Function st

( b_{1} is connected & b_{1} is acyclic & b_{1} is Tree-like & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

coherence

for b_{1} being Graph-yielding Function st b_{1} is trivial holds

b_{1} is connected

for b_{1} being Graph-yielding Function st b_{1} is trivial & b_{1} is loopless holds

b_{1} is Tree-like

for b_{1} being Graph-yielding Function st b_{1} is acyclic holds

b_{1} is simple

for b_{1} being Graph-yielding Function st b_{1} is Tree-like holds

( b_{1} is acyclic & b_{1} is connected )

for b_{1} being Graph-yielding Function st b_{1} is acyclic & b_{1} is connected holds

b_{1} is Tree-like

end;
for b

b

proof end;

cluster Relation-like Function-like Graph-yielding loopless trivial -> Graph-yielding Tree-like for set ;

coherence for b

b

proof end;

coherence for b

b

proof end;

cluster Relation-like Function-like Graph-yielding Tree-like -> Graph-yielding connected acyclic for set ;

coherence for b

( b

proof end;

cluster Relation-like Function-like Graph-yielding connected acyclic -> Graph-yielding Tree-like for set ;

coherence for b

b

proof end;

registration

ex b_{1} being GraphSeq st

( b_{1} is halting & b_{1} is finite & b_{1} is Tree-like )
end;

cluster non empty Relation-like omega -defined Function-like V30( omega ) Graph-yielding halting finite Tree-like for set ;

existence ex b

( b

proof end;

registration

let GF be non empty Graph-yielding connected Function;

let x be Element of dom GF;

coherence

for b_{1} being _Graph st b_{1} = GF . x holds

b_{1} is connected
by Def12b;

end;
let x be Element of dom GF;

coherence

for b

b

registration

let GF be non empty Graph-yielding acyclic Function;

let x be Element of dom GF;

coherence

for b_{1} being _Graph st b_{1} = GF . x holds

b_{1} is acyclic
by Def13b;

end;
let x be Element of dom GF;

coherence

for b

b

registration

let GF be non empty Graph-yielding Tree-like Function;

let x be Element of dom GF;

coherence

for b_{1} being _Graph st b_{1} = GF . x holds

b_{1} is Tree-like
;

end;
let x be Element of dom GF;

coherence

for b

b

registration

let GSq be connected GraphSeq;

let n be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . n holds

b_{1} is connected
by Def12;

end;
let n be Nat;

coherence

for b

b

registration

let GSq be acyclic GraphSeq;

let n be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . n holds

b_{1} is acyclic
by Def13;

end;
let n be Nat;

coherence

for b

b

registration

let GSq be Tree-like GraphSeq;

let n be Nat;

coherence

for b_{1} being _Graph st b_{1} = GSq . n holds

b_{1} is Tree-like
;

end;
let n be Nat;

coherence

for b

b

::$CT

theorem Th2: :: GLIB_002:3

for G1 being non trivial _Graph

for v being Vertex of G1

for G2 being removeVertex of G1,v st G2 is connected & ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) holds

G1 is connected

for v being Vertex of G1

for G2 being removeVertex of G1,v st G2 is connected & ex e being set st

( e in v .edgesInOut() & not e Joins v,v,G1 ) holds

G1 is connected

proof end;

theorem :: GLIB_002:4

theorem Th4: :: GLIB_002:5

for G1 being connected _Graph

for W being Walk of G1

for e being set

for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds

G2 is connected

for W being Walk of G1

for e being set

for G2 being removeEdge of G1,e st W is Cycle-like & e in W .edges() holds

G2 is connected

proof end;

theorem :: GLIB_002:6

theorem :: GLIB_002:9

theorem :: GLIB_002:10

for G being _Graph

for v1 being Vertex of G

for e, x, y being object st x in G .reachableFrom v1 & e Joins x,y,G holds

y in G .reachableFrom v1 by Lm2;

for v1 being Vertex of G

for e, x, y being object st x in G .reachableFrom v1 & e Joins x,y,G holds

y in G .reachableFrom v1 by Lm2;

theorem :: GLIB_002:11

for G being _Graph

for v being Vertex of G holds G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v)

for v being Vertex of G holds G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v)

proof end;

theorem :: GLIB_002:12

for G being _Graph

for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds

G .reachableFrom v1 = G .reachableFrom v2 by Lm3;

for v1, v2 being Vertex of G st v1 in G .reachableFrom v2 holds

G .reachableFrom v1 = G .reachableFrom v2 by Lm3;

theorem :: GLIB_002:13

for G being _Graph

for v being Vertex of G

for W being Walk of G st v in W .vertices() holds

W .vertices() c= G .reachableFrom v by Lm4;

for v being Vertex of G

for W being Walk of G st v in W .vertices() holds

W .vertices() c= G .reachableFrom v by Lm4;

theorem :: GLIB_002:14

for G1 being _Graph

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableFrom v2 c= G1 .reachableFrom v1

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableFrom v2 c= G1 .reachableFrom v1

proof end;

theorem :: GLIB_002:15

for G being _Graph st ex v being Vertex of G st G .reachableFrom v = the_Vertices_of G holds

G is connected by Lm7;

G is connected by Lm7;

theorem :: GLIB_002:16

for G being _Graph st G is connected holds

for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G by Lm8;

for v being Vertex of G holds G .reachableFrom v = the_Vertices_of G by Lm8;

theorem :: GLIB_002:17

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 by Lm9;

for v1 being Vertex of G1

for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds

G1 .reachableFrom v1 = G2 .reachableFrom v2 by Lm9;

theorem :: GLIB_002:19

for G being _Graph

for e, x, y being set

for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds

y in G .reachableDFrom v1

for e, x, y being set

for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds

y in G .reachableDFrom v1

proof end;

theorem :: GLIB_002:21

for G1 being _Graph

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableDFrom v2 c= G1 .reachableDFrom v1

for G2 being Subgraph of G1

for v1 being Vertex of G1

for v2 being Vertex of G2 st v1 = v2 holds

G2 .reachableDFrom v2 c= G1 .reachableDFrom v1

proof end;

theorem :: GLIB_002:22

for G1, G2 being _Graph

for v1 being Vertex of G1

for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds

G1 .reachableDFrom v1 = G2 .reachableDFrom v2

for v1 being Vertex of G1

for v2 being Vertex of G2 st G1 == G2 & v1 = v2 holds

G1 .reachableDFrom v1 = G2 .reachableDFrom v2

proof end;

theorem :: GLIB_002:23

theorem :: GLIB_002:25

theorem :: GLIB_002:26

theorem :: GLIB_002:27

for G being _Graph

for x being set st x in G .componentSet() holds

x is non empty Subset of (the_Vertices_of G) by Lm13;

for x being set st x in G .componentSet() holds

x is non empty Subset of (the_Vertices_of G) by Lm13;

theorem :: GLIB_002:28

theorem :: GLIB_002:29

theorem :: GLIB_002:31

for G being _Graph

for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C) by Lm14;

for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C) by Lm14;

theorem :: GLIB_002:32

for G being _Graph

for C1, C2 being Component of G holds

( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 ) by Lm15;

for C1, C2 being Component of G holds

( the_Vertices_of C1 = the_Vertices_of C2 iff C1 == C2 ) by Lm15;

theorem :: GLIB_002:33

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 ) by Lm16;

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 ) by Lm16;

theorem :: GLIB_002:34

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 by Lm17;

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 by Lm17;

theorem :: GLIB_002:35

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() ) by Lm19;

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() ) by Lm19;

theorem :: GLIB_002:36

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 by Lm20;

for v being Vertex of G

for G2 being removeVertex of G,v st not v is cut-vertex holds

G2 is connected by Lm20;

theorem :: GLIB_002:37

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 ) by Lm21;

( v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex ) by Lm21;

theorem :: GLIB_002:39

for G1, G2 being _Graph

for v1 being Vertex of G1

for v2 being Vertex of G2 st G1 == G2 & v1 = v2 & v1 is cut-vertex holds

v2 is cut-vertex

for v1 being Vertex of G1

for v2 being Vertex of G2 st G1 == G2 & v1 = v2 & v1 is cut-vertex holds

v2 is cut-vertex

proof end;

theorem :: GLIB_002:42

theorem :: GLIB_002:43

theorem :: GLIB_002:45

theorem Th45: :: GLIB_002:46

for G being finite _Graph holds

( G is Tree-like iff ( G is acyclic & G .order() = (G .size()) + 1 ) )

( G is Tree-like iff ( G is acyclic & G .order() = (G .size()) + 1 ) )

proof end;

theorem :: GLIB_002:47

for G being finite _Graph holds

( G is Tree-like iff ( G is connected & G .order() = (G .size()) + 1 ) )

( G is Tree-like iff ( G is connected & G .order() = (G .size()) + 1 ) )

proof end;

theorem :: GLIB_002:50

for G1, G2 being _Graph

for x being set st G1 == G2 & G1 is_DTree_rooted_at x holds

G2 is_DTree_rooted_at x

for x being set st G1 == G2 & G1 is_DTree_rooted_at x holds

G2 is_DTree_rooted_at x

proof end;