:: GLIB_002 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let X be finite set ;
cluster bool X -> finite ;
coherence
bool X is finite
by FINSET_1:24;
end;

theorem Th1: :: GLIB_002:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being finite set st 1 < card X holds
ex x1, x2 being set st
( x1 in X & x2 in X & x1 <> x2 )
proof end;

definition
let G be _Graph;
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;
end;

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

definition
let G be _Graph;
attr G is acyclic means :Def2: :: GLIB_002:def 2
for W being Walk of G holds not W is Cycle-like;
end;

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

definition
let G be _Graph;
attr G is Tree-like means :Def3: :: GLIB_002:def 3
( G is acyclic & G is connected );
end;

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

registration
cluster trivial -> connected GraphStruct ;
coherence
for b1 being _Graph st b1 is trivial holds
b1 is connected
proof end;
end;

registration
cluster loopless trivial -> Tree-like GraphStruct ;
coherence
for b1 being _Graph st b1 is trivial & b1 is loopless holds
b1 is Tree-like
proof end;
end;

registration
cluster acyclic -> simple GraphStruct ;
coherence
for b1 being _Graph st b1 is acyclic holds
b1 is simple
proof end;
end;

registration
cluster Tree-like -> simple connected acyclic GraphStruct ;
coherence
for b1 being _Graph st b1 is Tree-like holds
( b1 is acyclic & b1 is connected )
by Def3;
end;

registration
cluster connected acyclic -> simple connected acyclic Tree-like GraphStruct ;
coherence
for b1 being _Graph st b1 is acyclic & b1 is connected holds
b1 is Tree-like
by Def3;
end;

registration
let G be _Graph;
let v be Vertex of G;
cluster -> Tree-like inducedSubgraph of G,{v}, {} ;
coherence
for b1 being inducedSubgraph of G,{v}, {} holds b1 is Tree-like
;
end;

definition
let G be _Graph;
let v be set ;
pred G is_DTree_rooted_at v means :Def4: :: 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 ) );
end;

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

registration
cluster finite trivial simple connected acyclic Tree-like GraphStruct ;
existence
ex b1 being _Graph st
( b1 is trivial & b1 is finite & b1 is Tree-like )
proof end;
cluster finite non trivial simple connected acyclic Tree-like GraphStruct ;
existence
ex b1 being _Graph st
( not b1 is trivial & b1 is finite & b1 is Tree-like )
proof end;
end;

registration
let G be _Graph;
cluster finite trivial simple connected acyclic Tree-like Subgraph of G;
existence
ex b1 being Subgraph of G st
( b1 is trivial & b1 is finite & b1 is Tree-like )
proof end;
end;

registration
let G be acyclic _Graph;
cluster -> acyclic Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is acyclic
proof end;
end;

definition
let G be _Graph;
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 set holds
( x in it iff ex W being Walk of G st W is_Walk_from v,x );
existence
ex b1 being non empty Subset of (the_Vertices_of G) st
for x being set holds
( x in b1 iff ex W being Walk of G st W is_Walk_from v,x )
proof end;
uniqueness
for b1, b2 being non empty Subset of (the_Vertices_of G) st ( for x being set holds
( x in b1 iff ex W being Walk of G st W is_Walk_from v,x ) ) & ( for x being set holds
( x in b2 iff ex W being Walk of G st W is_Walk_from v,x ) ) holds
b1 = b2
proof end;
end;

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

definition
let G be _Graph;
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 set holds
( x in it iff ex W being DWalk of G st W is_Walk_from v,x );
existence
ex b1 being non empty Subset of (the_Vertices_of G) st
for x being set holds
( x in b1 iff ex W being DWalk of G st W is_Walk_from v,x )
proof end;
uniqueness
for b1, b2 being non empty Subset of (the_Vertices_of G) st ( for x being set holds
( x in b1 iff ex W being DWalk of G st W is_Walk_from v,x ) ) & ( for x being set holds
( x in b2 iff ex W being DWalk of G st W is_Walk_from v,x ) ) holds
b1 = b2
proof end;
end;

:: 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
proof end;

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

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

registration
let G be _Graph;
cluster Component-like -> connected Subgraph of G;
coherence
for b1 being Subgraph of G st b1 is Component-like holds
b1 is connected
by Def7;
end;

registration
let G be _Graph;
let v be Vertex of G;
cluster -> connected Component-like inducedSubgraph of G,G .reachableFrom v,G .edgesBetween (G .reachableFrom v);
coherence
for b1 being inducedSubgraph of G,(G .reachableFrom v) holds b1 is Component-like
proof end;
end;

registration
let G be _Graph;
cluster connected Component-like Subgraph of G;
existence
ex b1 being Subgraph of G st b1 is Component-like
proof end;
end;

definition
let G be _Graph;
mode Component of G is Component-like Subgraph of G;
end;

definition
let G be _Graph;
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
ex b1 being non empty Subset-Family of (the_Vertices_of G) st
for x being set holds
( x in b1 iff ex v being Vertex of G st x = G .reachableFrom v )
proof end;
uniqueness
for b1, b2 being non empty Subset-Family of (the_Vertices_of G) st ( for x being set holds
( x in b1 iff ex v being Vertex of G st x = G .reachableFrom v ) ) & ( for x being set holds
( x in b2 iff ex v being Vertex of G st x = G .reachableFrom v ) ) holds
b1 = b2
proof end;
end;

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

registration
let G be _Graph;
let X be Element of G .componentSet() ;
cluster -> connected Component-like inducedSubgraph of G,X,G .edgesBetween X;
coherence
for b1 being inducedSubgraph of G,X holds b1 is Component-like
proof end;
end;

definition
let G be _Graph;
func G .numComponents() -> Cardinal equals :: GLIB_002:def 9
Card (G .componentSet() );
coherence
Card (G .componentSet() ) is Cardinal
;
end;

:: deftheorem defines .numComponents() GLIB_002:def 9 :
for G being _Graph holds G .numComponents() = Card (G .componentSet() );

definition
let G be finite _Graph;
:: original: .numComponents()
redefine func G .numComponents() -> non empty Nat;
coherence
G .numComponents() is non empty Nat
proof end;
end;

definition
let G be _Graph;
let v be Vertex of G;
attr v is cut-vertex means :Def10: :: GLIB_002:def 10
for G2 being removeVertex of G,v holds G .numComponents() <` G2 .numComponents() ;
end;

:: 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() <` G2 .numComponents() );

definition
let G be finite _Graph;
let v be Vertex of G;
redefine attr v is cut-vertex means :Def11: :: GLIB_002:def 11
for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() ;
compatibility
( v is cut-vertex iff for G2 being removeVertex of G,v holds G .numComponents() < G2 .numComponents() )
proof end;
end;

:: 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
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 G1, G2 being _Graph st G1 == G2 holds
G1 .numComponents() = G2 .numComponents()
by Lm12;

Lm20: 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() <=` G .numComponents() )
proof end;

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

Lm22: 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;
cluster non cut-vertex Element of the_Vertices_of G;
existence
not for b1 being Vertex of G holds b1 is cut-vertex
proof end;
end;

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

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

Lm25: 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;
cluster endvertex Element of the_Vertices_of G;
existence
ex b1 being Vertex of G st b1 is endvertex
proof end;
end;

registration
let G be finite non trivial Tree-like _Graph;
let v be endvertex Vertex of G;
cluster -> acyclic Tree-like inducedSubgraph of G,K132((the_Vertices_of G),{v}),G .edgesBetween K132((the_Vertices_of G),{v});
coherence
for b1 being removeVertex of G,v holds b1 is Tree-like
proof end;
end;

definition
let GSq be GraphSeq;
attr GSq is connected means :Def12: :: GLIB_002:def 12
for n being Nat holds GSq .-> n is connected;
attr GSq is acyclic means :Def13: :: GLIB_002:def 13
for n being Nat holds GSq .-> n is acyclic;
attr GSq is Tree-like means :Def14: :: GLIB_002:def 14
for n being Nat holds GSq .-> n is Tree-like;
end;

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

registration
cluster trivial -> connected ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is trivial holds
b1 is connected
proof end;
cluster loopless trivial -> Tree-like ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is trivial & b1 is loopless holds
b1 is Tree-like
proof end;
cluster acyclic -> simple ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is acyclic holds
b1 is simple
proof end;
cluster Tree-like -> connected acyclic ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is Tree-like holds
( b1 is acyclic & b1 is connected )
proof end;
cluster connected acyclic -> Tree-like ManySortedSet of NAT ;
coherence
for b1 being GraphSeq st b1 is acyclic & b1 is connected holds
b1 is Tree-like
proof end;
end;

registration
cluster halting finite simple connected acyclic Tree-like ManySortedSet of NAT ;
existence
ex b1 being GraphSeq st
( b1 is halting & b1 is finite & b1 is Tree-like )
proof end;
end;

registration
let GSq be connected GraphSeq;
let n be Nat;
cluster GSq .-> n -> connected ;
coherence
GSq .-> n is connected
by Def12;
end;

registration
let GSq be acyclic GraphSeq;
let n be Nat;
cluster GSq .-> n -> acyclic ;
coherence
GSq .-> n is acyclic
by Def13;
end;

registration
let GSq be Tree-like GraphSeq;
let n be Nat;
cluster GSq .-> n -> connected acyclic Tree-like ;
coherence
GSq .-> n is Tree-like
;
end;

theorem Th2: :: GLIB_002:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being non trivial connected _Graph
for v being Vertex of G holds not v is isolated
proof end;

theorem Th3: :: GLIB_002:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GLIB_002:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 by Lm5;

theorem Th5: :: GLIB_002:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GLIB_002:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 by Lm6;

theorem :: GLIB_002:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being trivial _Graph holds G is connected ;

theorem Th8: :: GLIB_002:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph st G1 == G2 & G1 is connected holds
G2 is connected
proof end;

theorem :: GLIB_002:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for v being Vertex of G holds v in G .reachableFrom v by Lm1;

theorem :: GLIB_002:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for x, e, y being set
for v1 being Vertex of G st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1 by Lm2;

theorem :: GLIB_002:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for v being Vertex of G holds G .edgesBetween (G .reachableFrom v) = G .edgesInOut (G .reachableFrom v)
proof end;

theorem :: GLIB_002:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_002:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_002:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GLIB_002:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_002:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_002:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_002:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for v being Vertex of G holds v in G .reachableDFrom v
proof end;

theorem :: GLIB_002:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for x, e, 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:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for v being Vertex of G holds G .reachableDFrom v c= G .reachableFrom v
proof end;

theorem :: GLIB_002:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GLIB_002:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GLIB_002:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being connected Subgraph of G1 st G2 is spanning holds
G1 is connected by Lm10;

theorem :: GLIB_002:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph holds union (G .componentSet() ) = the_Vertices_of G
proof end;

theorem :: GLIB_002:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph holds
( G is connected iff G .componentSet() = {(the_Vertices_of G)} ) by Lm11;

theorem :: GLIB_002:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph st G1 == G2 holds
G1 .componentSet() = G2 .componentSet() by Lm12;

theorem :: GLIB_002:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_002:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph holds
( G is connected iff G .numComponents() = 1 ) by Lm18;

theorem :: GLIB_002:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph st G1 == G2 holds
G1 .numComponents() = G2 .numComponents() by Lm19;

theorem :: GLIB_002:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph holds
( G is Component of G iff G is connected )
proof end;

theorem :: GLIB_002:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for C being Component of G holds the_Edges_of C = G .edgesBetween (the_Vertices_of C) by Lm14;

theorem :: GLIB_002:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_002:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_002:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: GLIB_002:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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() <=` G .numComponents() ) by Lm20;

theorem :: GLIB_002:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Lm21;

theorem :: GLIB_002:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Lm22;

theorem Th38: :: GLIB_002:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for v being Vertex of G st v is cut-vertex holds
not G is trivial
proof end;

theorem :: GLIB_002:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th40: :: GLIB_002:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite connected _Graph holds G .order() <= (G .size() ) + 1
proof end;

theorem :: GLIB_002:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being acyclic _Graph holds G is simple ;

theorem :: GLIB_002:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 by Lm23;

theorem :: GLIB_002:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) by Lm24;

theorem Th44: :: GLIB_002:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph st G1 == G2 & G1 is acyclic holds
G2 is acyclic
proof end;

theorem :: GLIB_002:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) by Lm25;

theorem Th46: :: GLIB_002:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite _Graph holds
( G is Tree-like iff ( G is acyclic & G .order() = (G .size() ) + 1 ) )
proof end;

theorem :: GLIB_002:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite _Graph holds
( G is Tree-like iff ( G is connected & G .order() = (G .size() ) + 1 ) )
proof end;

theorem Th48: :: GLIB_002:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph st G1 == G2 & G1 is Tree-like holds
G2 is Tree-like
proof end;

theorem :: GLIB_002:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being _Graph
for x being set st G is_DTree_rooted_at x holds
x is Vertex of G
proof end;

theorem :: GLIB_002:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;