:: About Supergraphs, {P}art {III}
:: by Sebastian Koch
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


Lm12: for p being non empty FinSequence
for x being object
for n being Element of dom (p ^ <*x*>) holds
( not n <= (len (p ^ <*x*>)) - 1 or n = (len (p ^ <*x*>)) - 1 or n <= (len p) - 1 )

proof end;

Lm13: for p being non empty FinSequence
for x being object
for n being Element of dom (<*x*> ^ p) holds
( not n <= (len (<*x*> ^ p)) - 1 or n = 1 or ( n - 1 in dom p & n - 1 <= (len p) - 1 ) )

proof end;

::: START into GLIB_000 ?
registration
let G be _Graph;
let v be Vertex of G;
cluster -> _trivial for inducedSubgraph of G,{v},G .edgesBetween {v};
coherence
for b1 being inducedSubgraph of G,{v} holds b1 is _trivial
proof end;
end;

theorem Th1: :: GLIB_008:1
for G being _Graph
for X being set
for v being Vertex of G holds G .edgesBetween (X \ {v}) = (G .edgesBetween X) \ (v .edgesInOut())
proof end;

theorem Th2: :: GLIB_008:2
for G being _Graph
for X being set
for v being Vertex of G st v is isolated holds
G .edgesBetween (X \ {v}) = G .edgesBetween X
proof end;

theorem Th3: :: GLIB_008:3
for G being non-Dmulti _Graph
for v being Vertex of G holds v .inDegree() = card (v .inNeighbors())
proof end;

theorem Th4: :: GLIB_008:4
for G being non-Dmulti _Graph
for v being Vertex of G holds v .outDegree() = card (v .outNeighbors())
proof end;

theorem Th5: :: GLIB_008:5
for G being simple _Graph
for v being Vertex of G holds v .degree() = card (v .allNeighbors())
proof end;

theorem Th6: :: GLIB_008:6
for G being _Graph holds
( G is loopless iff for v being Vertex of G holds not v in v .allNeighbors() )
proof end;

theorem Th7: :: GLIB_008:7
for G being _Graph
for v being Vertex of G holds
( v is isolated iff v .allNeighbors() = {} )
proof end;

Lm2: for G1 being _Graph
for v being set
for G2 being removeVertex of G1,v st not v in the_Vertices_of G1 holds
G1 == G2

proof end;

theorem Th8: :: GLIB_008:8
for G1 being _Graph
for v being set
for G2 being removeVertex of G1,v st ( G1 is _trivial or not v in the_Vertices_of G1 ) holds
G1 == G2
proof end;

Lm3: for G1, G2 being _Graph
for v being set st G1 == G2 & not v in the_Vertices_of G1 holds
G2 is removeVertex of G1,v

proof end;

theorem Th9: :: GLIB_008:9
for G1, G2 being _Graph
for v being set st G1 == G2 & ( G1 is _trivial or not v in the_Vertices_of G1 ) holds
G2 is removeVertex of G1,v
proof end;

:: converse of GLIB_000:21
theorem Th10: :: GLIB_008:10
for G being _Graph st ex v1, v2 being Vertex of G st v1 <> v2 holds
not G is _trivial
proof end;

registration
let G be non _trivial _Graph;
let X be set ;
cluster -> non _trivial for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ X;
coherence
for b1 being removeEdges of G,X holds not b1 is _trivial
proof end;
end;

theorem Th11: :: GLIB_008:11
for G1 being _finite _Graph
for G2 being Subgraph of G1 holds
( G2 is spanning iff G1 .order() = G2 .order() )
proof end;

theorem Th12: :: GLIB_008:12
for G1 being _Graph
for G2 being spanning Subgraph of G1 st the_Edges_of G1 = the_Edges_of G2 holds
G1 == G2
proof end;

theorem Th13: :: GLIB_008:13
for G1 being _finite _Graph
for G2 being spanning Subgraph of G1 st G1 .size() = G2 .size() holds
G1 == G2
proof end;

theorem Th14: :: GLIB_008:14
for G1 being _Graph
for V being set
for G2 being inducedSubgraph of G1,V st G2 is spanning holds
G1 == G2
proof end;

theorem Th15: :: GLIB_008:15
for G being _Graph holds
( not G is _trivial iff ex H being Subgraph of G st not H is spanning )
proof end;

theorem Th16: :: GLIB_008:16
for G being _Graph st ex v being Vertex of G st v is endvertex holds
not G is _trivial
proof end;

Lm4: for G1, G2 being _Graph
for e being set
for G3 being removeEdge of G1,e
for G4 being removeEdge of G2,e st G1 == G2 holds
G3 == G4

proof end;

:: removeEdge and removeVertex commute, Part I
theorem :: GLIB_008:17
for G1 being _Graph
for v, e being set
for G2 being removeVertex of G1,v
for G3 being removeEdge of G1,e
for G4 being removeEdge of G2,e holds G4 is removeVertex of G3,v
proof end;

Lm5: for G1, G3, G4 being _Graph
for e being set
for G2 being removeEdge of G1,e st G1 == G3 & G2 == G4 holds
G4 is removeEdge of G3,e

proof end;

:: removeEdge and removeVertex commute, Part II
theorem Th18: :: GLIB_008:18
for G1 being _Graph
for v, e being set
for G2 being removeEdge of G1,e
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeEdge of G3,e
proof end;

Lm6: for G being _finite connected _Graph ex H being Subgraph of G st
( H is spanning & H is Tree-like & H is connected & H is acyclic )

proof end;

registration
let G be _finite connected _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite spanning connected acyclic Tree-like for Subgraph of G;
existence
ex b1 being Subgraph of G st
( b1 is spanning & b1 is Tree-like & b1 is connected & b1 is acyclic )
by Lm6;
end;

theorem Th19: :: GLIB_008:19
for G1 being connected _Graph
for G2 being Subgraph of G1 st the_Edges_of G1 c= the_Edges_of G2 holds
G1 == G2
proof end;

theorem :: GLIB_008:20
for G1 being _finite connected _Graph
for G2 being Subgraph of G1 st G1 .size() = G2 .size() holds
G1 == G2
proof end;

theorem Th21: :: GLIB_008:21
for G1 being _finite Tree-like _Graph
for G2 being spanning Tree-like Subgraph of G1 holds G1 == G2
proof end;

registration
let G be non _trivial _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] _trivial non spanning connected for Subgraph of G;
existence
ex b1 being Subgraph of G st
( not b1 is spanning & b1 is _trivial & b1 is connected )
proof end;
end;

:: counterpart of GLIB_002:12
theorem Th22: :: GLIB_008:22
for G being _Graph
for v1, v2 being Vertex of G st not v1 in G .reachableFrom v2 holds
G .reachableFrom v1 misses G .reachableFrom v2
proof end;

theorem Th23: :: GLIB_008:23
for G being _Graph holds G .componentSet() is a_partition of the_Vertices_of G
proof end;

theorem Th24: :: GLIB_008:24
for G being _Graph
for C being a_partition of the_Vertices_of G
for v being Vertex of G st C = G .componentSet() holds
EqClass (v,C) = G .reachableFrom v
proof end;

:: holds more generally when G is non trivial and v0 is non cut-vertex;
:: however, this theorem is used to show that endvertex implies non cut-vertex
theorem Th25: :: GLIB_008:25
for G1 being _Graph
for v0, v1 being Vertex of G1
for G2 being removeVertex of G1,v0
for v2 being Vertex of G2 st v0 is endvertex & v1 = v2 & v1 in G1 .reachableFrom v0 holds
G2 .reachableFrom v2 = (G1 .reachableFrom v1) \ {v0}
proof end;

theorem Th26: :: GLIB_008:26
for G1 being non _trivial _Graph
for v0, v1 being Vertex of G1
for G2 being removeVertex of G1,v0
for v2 being Vertex of G2 st v1 = v2 & not v1 in G1 .reachableFrom v0 holds
G2 .reachableFrom v2 = G1 .reachableFrom v1
proof end;

theorem Th27: :: GLIB_008:27
for G being _finite non _trivial Tree-like _Graph
for v being Vertex of G st G .order() = 2 holds
v is endvertex
proof end;

registration
let G be non _trivial connected _Graph;
let v be Vertex of G;
cluster v .allNeighbors() -> non empty ;
coherence
not v .allNeighbors() is empty
by Th7, GLIB_002:2;
end;

:: END into GLIB_002 ?
:: into HELLY ?
theorem :: GLIB_008:28
for T being _Tree
for a being Vertex of T holds T .pathBetween (a,a) = T .walkOf a
proof end;

:: into HELLY ?
theorem Th29: :: GLIB_008:29
for T being _Tree
for a, b being Vertex of T
for e being object st e Joins a,b,T holds
T .pathBetween (a,b) = T .walkOf (a,e,b) by GLIB_001:15, HELLY:def 2;

:: into HELLY ?
theorem Th30: :: GLIB_008:30
for T being _finite non _trivial _Tree
for v being Vertex of T ex v1, v2 being Vertex of T st
( v1 <> v2 & v1 is endvertex & v2 is endvertex & v in (T .pathBetween (v1,v2)) .vertices() )
proof end;

:: into HELLY ?
theorem Th31: :: GLIB_008:31
for G1 being _finite non _trivial Tree-like _Graph
for G2 being non spanning connected Subgraph of G1 ex v being Vertex of G1 st
( v is endvertex & not v in the_Vertices_of G2 )
proof end;

:: START into GLIB_006 ?
theorem Th32: :: GLIB_008:32
for G2, G3 being _Graph
for V being set
for G1 being addVertices of G2,V st G2 == G3 holds
G1 is addVertices of G3,V
proof end;

theorem Th33: :: GLIB_008:33
for G2 being _Graph
for G1 being Supergraph of G2 st the_Edges_of G1 = the_Edges_of G2 holds
G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)
proof end;

theorem Th34: :: GLIB_008:34
for G1 being _finite _Graph
for G2 being Subgraph of G1 st G1 .size() = G2 .size() holds
G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)
proof end;

theorem :: GLIB_008:35
for G1 being non _trivial _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is isolated holds
G1 is addVertex of G2,v
proof end;

theorem Th36: :: GLIB_008:36
for G2, G3 being _Graph
for v1, e, v2 being object
for G1 being addEdge of G2,v1,e,v2 st G2 == G3 holds
G1 is addEdge of G3,v1,e,v2
proof end;

theorem Th37: :: GLIB_008:37
for G1 being _Graph
for e being set
for G2 being removeEdge of G1,e st e in the_Edges_of G1 holds
G1 is addEdge of G2,(the_Source_of G1) . e,e,(the_Target_of G1) . e
proof end;

theorem Th38: :: GLIB_008:38
for G1 being non _trivial _Graph
for v being Vertex of G1
for e being object
for G2 being removeVertex of G1,v st {e} = v .edgesInOut() & not e Joins v,v,G1 & G1 is not addAdjVertex of G2,v .adj e,e,v holds
G1 is addAdjVertex of G2,v,e,v .adj e
proof end;

theorem Th39: :: GLIB_008:39
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for w being Vertex of G1
for v being Vertex of G2 st v2 in G2 .reachableFrom v1 & v = w holds
G1 .reachableFrom w = G2 .reachableFrom v
proof end;

theorem Th40: :: GLIB_008:40
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st v2 in G2 .reachableFrom v1 holds
G1 .componentSet() = G2 .componentSet()
proof end;

:: v1 and v2 are connected in supergraph
theorem Th41: :: GLIB_008:41
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for w1, w2 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 & w2 = v2 holds
w2 in G1 .reachableFrom w1
proof end;

:: their components are connected as well
theorem Th42: :: GLIB_008:42
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for w1 being Vertex of G1 st not e in the_Edges_of G2 & w1 = v1 holds
G1 .reachableFrom w1 = (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2)
proof end;

:: the other components stay unaffected
theorem Th43: :: GLIB_008:43
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2
for w being Vertex of G1
for v being Vertex of G2 st not e in the_Edges_of G2 & v = w & not v in G2 .reachableFrom v1 & not v in G2 .reachableFrom v2 holds
G1 .reachableFrom w = G2 .reachableFrom v
proof end;

:: composition of component set in graph with added edge
theorem Th44: :: GLIB_008:44
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v1),(G2 .reachableFrom v2)}) \/ {((G2 .reachableFrom v1) \/ (G2 .reachableFrom v2))}
proof end;

Lm7: for G2 being _Graph
for v1, v2 being Vertex of G2 st not v2 in G2 .reachableFrom v1 holds
not (G2 .reachableFrom v1) \/ (G2 .reachableFrom v2) in G2 .componentSet()

proof end;

Lm8: for G1 being _finite _Graph
for e being set
for G2 being removeEdge of G1,e holds G1 .numComponents() c= G2 .numComponents()

proof end;

:: removing an endvertex doesn't change number of components
theorem Th45: :: GLIB_008:45
for G1 being _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v is endvertex holds
G1 .numComponents() = G2 .numComponents()
proof end;

registration
let G be _Graph;
cluster endvertex -> non cut-vertex for Element of the_Vertices_of G;
coherence
for b1 being Vertex of G st b1 is endvertex holds
not b1 is cut-vertex
proof end;
end;

theorem :: GLIB_008:46
for G1 being _finite non _trivial connected _Graph
for G2 being non spanning connected Subgraph of G1 ex v being Vertex of G1 st
( not v is cut-vertex & not v in the_Vertices_of G2 )
proof end;

Lm9: for G3 being _Graph
for v being object
for V being set
for v1 being Vertex of G3
for G1 being addAdjVertexAll of G3,v,V \/ {v1} st V c= the_Vertices_of G3 & not v in the_Vertices_of G3 & not v1 in V holds
ex G2 being addAdjVertexAll of G3,v,V ex e being object st
( not e in the_Edges_of G2 & ( G1 is addEdge of G2,v,e,v1 or G1 is addEdge of G2,v1,e,v ) )

by GLIB_007:61;

:: into GLIB_007 ?
theorem Th47: :: GLIB_008:47
for G1 being non _trivial simple _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v holds G1 is addAdjVertexAll of G2,v,v .allNeighbors()
proof end;

definition
let G be _Graph;
attr G is edgeless means :Def1: :: GLIB_008:def 1
the_Edges_of G = {} ;
end;

:: deftheorem Def1 defines edgeless GLIB_008:def 1 :
for G being _Graph holds
( G is edgeless iff the_Edges_of G = {} );

theorem :: GLIB_008:48
for G being _Graph holds
( G is edgeless iff card (the_Edges_of G) = 0 ) ;

theorem Th49: :: GLIB_008:49
for G being _Graph holds
( G is edgeless iff G .size() = 0 )
proof end;

registration
let G be _Graph;
cluster -> edgeless for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (the_Edges_of G);
coherence
for b1 being removeEdges of G,(the_Edges_of G) holds b1 is edgeless
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] edgeless for set ;
existence
ex b1 being _Graph st b1 is edgeless
proof end;
let G be _Graph;
cluster Relation-like NAT -defined Function-like finite [Graph-like] spanning edgeless for Subgraph of G;
existence
ex b1 being Subgraph of G st
( b1 is edgeless & b1 is spanning )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] _trivial edgeless for Subgraph of G;
existence
ex b1 being Subgraph of G st
( b1 is edgeless & b1 is _trivial )
proof end;
end;

registration
let G be edgeless _Graph;
cluster the_Edges_of G -> empty ;
coherence
the_Edges_of G is empty
by Def1;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] edgeless -> loopless non-multi non-Dmulti simple Dsimple for set ;
coherence
for b1 being _Graph st b1 is edgeless holds
( b1 is non-multi & b1 is non-Dmulti & b1 is loopless & b1 is simple & b1 is Dsimple )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless _trivial -> edgeless for set ;
coherence
for b1 being _Graph st b1 is _trivial & b1 is loopless holds
b1 is edgeless
by GLIB_000:23;
let V be non empty set ;
let S, T be Function of {},V;
cluster createGraph (V,{},S,T) -> edgeless ;
coherence
createGraph (V,{},S,T) is edgeless
;
end;

theorem :: GLIB_008:50
for G being edgeless _Graph
for e, v1, v2 being object holds
( not e Joins v1,v2,G & not e DJoins v1,v2,G )
proof end;

theorem :: GLIB_008:51
for G being edgeless _Graph
for e being object
for X, Y being set holds
( not e SJoins X,Y,G & not e DSJoins X,Y,G )
proof end;

theorem Th52: :: GLIB_008:52
for G1, G2 being _Graph st G1 == G2 & G1 is edgeless holds
G2 is edgeless by GLIB_000:def 34;

registration
let G be edgeless _Graph;
cluster -> V5() for Walk of G;
coherence
for b1 being Walk of G holds b1 is V5()
proof end;
cluster -> edgeless for Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is edgeless
proof end;
let X be set ;
cluster G .edgesInto X -> empty ;
coherence
G .edgesInto X is empty
;
cluster G .edgesOutOf X -> empty ;
coherence
G .edgesOutOf X is empty
;
cluster G .edgesInOut X -> empty ;
coherence
G .edgesInOut X is empty
;
cluster G .edgesBetween X -> empty ;
coherence
G .edgesBetween X is empty
;
cluster G .set (WeightSelector,X) -> edgeless ;
coherence
G .set (WeightSelector,X) is edgeless
by GLIB_003:7, Th52;
cluster G .set (ELabelSelector,X) -> edgeless ;
coherence
G .set (ELabelSelector,X) is edgeless
by GLIB_003:7, Th52;
cluster G .set (VLabelSelector,X) -> edgeless ;
coherence
G .set (VLabelSelector,X) is edgeless
by GLIB_003:7, Th52;
cluster -> edgeless for addVertices of G,X;
coherence
for b1 being addVertices of G,X holds b1 is edgeless
proof end;
cluster -> edgeless for reverseEdgeDirections of G,X;
coherence
for b1 being reverseEdgeDirections of G,X holds b1 is edgeless
proof end;
let Y be set ;
cluster G .edgesBetween (X,Y) -> empty ;
coherence
G .edgesBetween (X,Y) is empty
;
cluster G .edgesDBetween (X,Y) -> empty ;
coherence
G .edgesDBetween (X,Y) is empty
;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] edgeless -> acyclic chordal for set ;
coherence
for b1 being _Graph st b1 is edgeless holds
( b1 is acyclic & b1 is chordal )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] _trivial edgeless -> Tree-like for set ;
coherence
for b1 being _Graph st b1 is _trivial & b1 is edgeless holds
b1 is Tree-like
;
cluster Relation-like NAT -defined Function-like finite [Graph-like] non _trivial edgeless -> non connected non Tree-like non complete for set ;
coherence
for b1 being _Graph st not b1 is _trivial & b1 is edgeless holds
( not b1 is connected & not b1 is Tree-like & not b1 is complete )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] connected edgeless -> _trivial for set ;
coherence
for b1 being _Graph st b1 is connected & b1 is edgeless holds
b1 is _trivial
;
end;

theorem :: GLIB_008:53
for G1 being edgeless _Graph
for G2 being Subgraph of G1 holds G1 is addVertices of G2,(the_Vertices_of G1) \ (the_Vertices_of G2)
proof end;

theorem Th54: :: GLIB_008:54
for G2 being _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 holds
not G1 is edgeless
proof end;

theorem Th55: :: GLIB_008:55
for G2 being _Graph
for v1 being Vertex of G2
for e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st not v2 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is edgeless
proof end;

theorem Th56: :: GLIB_008:56
for G2 being _Graph
for v1, e being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v1,e,v2 st not v1 in the_Vertices_of G2 & not e in the_Edges_of G2 holds
not G1 is edgeless
proof end;

theorem Th57: :: GLIB_008:57
for G2 being _Graph
for v being object
for V being non empty Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds
not G1 is edgeless by GLIB_007:47;

registration
let G be _Graph;
cluster -> non edgeless for addAdjVertexToAll of G, the_Vertices_of G, the_Vertices_of G;
coherence
for b1 being addAdjVertexToAll of G, the_Vertices_of G holds not b1 is edgeless
proof end;
cluster -> non edgeless for addAdjVertexFromAll of G, the_Vertices_of G, the_Vertices_of G;
coherence
for b1 being addAdjVertexFromAll of G, the_Vertices_of G holds not b1 is edgeless
proof end;
cluster -> non edgeless for addAdjVertexAll of G, the_Vertices_of G, the_Vertices_of G;
coherence
for b1 being addAdjVertexAll of G, the_Vertices_of G holds not b1 is edgeless
proof end;
let v be Vertex of G;
cluster -> non edgeless for addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G;
coherence
for b1 being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b1 is edgeless
proof end;
cluster -> non edgeless for addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v;
coherence
for b1 being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds not b1 is edgeless
proof end;
let w be Vertex of G;
cluster -> non edgeless for addEdge of G,v, the_Edges_of G,w;
coherence
for b1 being addEdge of G,v, the_Edges_of G,w holds not b1 is edgeless
proof end;
end;

registration
let G be edgeless _Graph;
cluster Component-like -> _trivial for Subgraph of G;
coherence
for b1 being Component of G holds b1 is _trivial
;
let v be Vertex of G;
cluster v .edgesIn() -> empty ;
coherence
v .edgesIn() is empty
;
cluster v .edgesOut() -> empty ;
coherence
v .edgesOut() is empty
;
cluster v .edgesInOut() -> empty ;
coherence
v .edgesInOut() is empty
;
end;

registration
let G be edgeless _Graph;
cluster -> isolated non endvertex non cut-vertex for Element of the_Vertices_of G;
coherence
for b1 being Vertex of G holds
( b1 is isolated & not b1 is cut-vertex & not b1 is endvertex )
proof end;
let v be Vertex of G;
cluster v .inDegree() -> empty ;
coherence
v .inDegree() is empty
proof end;
cluster v .outDegree() -> empty ;
coherence
v .outDegree() is empty
proof end;
cluster v .inNeighbors() -> empty ;
coherence
v .inNeighbors() is empty
proof end;
cluster v .outNeighbors() -> empty ;
coherence
v .outNeighbors() is empty
proof end;
end;

registration
let G be edgeless _Graph;
let v be Vertex of G;
cluster v .degree() -> empty ;
coherence
v .degree() is empty
proof end;
cluster v .allNeighbors() -> empty ;
coherence
v .allNeighbors() is empty
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite _trivial edgeless for set ;
existence
ex b1 being _Graph st
( b1 is _trivial & b1 is _finite & b1 is edgeless )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite non _trivial edgeless for set ;
existence
ex b1 being _Graph st
( not b1 is _trivial & b1 is _finite & b1 is edgeless )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite _trivial non edgeless for set ;
existence
ex b1 being _Graph st
( b1 is _trivial & b1 is _finite & not b1 is edgeless )
proof end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite non _trivial non edgeless for set ;
existence
ex b1 being _Graph st
( not b1 is _trivial & b1 is _finite & not b1 is edgeless )
proof end;
end;

registration
let G be non edgeless _Graph;
cluster the_Edges_of G -> non empty ;
coherence
not the_Edges_of G is empty
by Def1;
cluster -> non edgeless for Supergraph of G;
coherence
for b1 being Supergraph of G holds not b1 is edgeless
proof end;
let X be set ;
cluster -> non edgeless for reverseEdgeDirections of G,X;
coherence
for b1 being reverseEdgeDirections of G,X holds not b1 is edgeless
proof end;
cluster G .set (WeightSelector,X) -> non edgeless ;
coherence
not G .set (WeightSelector,X) is edgeless
proof end;
cluster G .set (ELabelSelector,X) -> non edgeless ;
coherence
not G .set (ELabelSelector,X) is edgeless
proof end;
cluster G .set (VLabelSelector,X) -> non edgeless ;
coherence
not G .set (VLabelSelector,X) is edgeless
proof end;
end;

definition
let G be non edgeless _Graph;
mode Edge of G is Element of the_Edges_of G;
end;

theorem :: GLIB_008:58
for G1 being _finite edgeless _Graph
for G2 being Subgraph of G1 st G1 .order() = G2 .order() holds
G1 == G2
proof end;

definition
let GF be Graph-yielding Function;
attr GF is edgeless means :Def2: :: GLIB_008:def 2
for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is edgeless );
end;

:: deftheorem Def2 defines edgeless GLIB_008:def 2 :
for GF being Graph-yielding Function holds
( GF is edgeless iff for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is edgeless ) );

definition
let GF be non empty Graph-yielding Function;
redefine attr GF is edgeless means :Def3: :: GLIB_008:def 3
for x being Element of dom GF holds GF . x is edgeless ;
compatibility
( GF is edgeless iff for x being Element of dom GF holds GF . x is edgeless )
proof end;
end;

:: deftheorem Def3 defines edgeless GLIB_008:def 3 :
for GF being non empty Graph-yielding Function holds
( GF is edgeless iff for x being Element of dom GF holds GF . x is edgeless );

Lm10: 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;
redefine attr GSq is edgeless means :Def4: :: GLIB_008:def 4
for n being Nat holds GSq . n is edgeless ;
compatibility
( GSq is edgeless iff for n being Nat holds GSq . n is edgeless )
proof end;
end;

:: deftheorem Def4 defines edgeless GLIB_008:def 4 :
for GSq being GraphSeq holds
( GSq is edgeless iff for n being Nat holds GSq . n is edgeless );

registration
cluster Relation-like Function-like Graph-yielding loopless _trivial -> Graph-yielding edgeless for set ;
coherence
for b1 being Graph-yielding Function st b1 is _trivial & b1 is loopless holds
b1 is edgeless
proof end;
cluster Relation-like Function-like Graph-yielding edgeless -> Graph-yielding loopless non-multi non-Dmulti simple Dsimple acyclic for set ;
coherence
for b1 being Graph-yielding Function st b1 is edgeless holds
( b1 is non-multi & b1 is non-Dmulti & b1 is loopless & b1 is simple & b1 is Dsimple & b1 is acyclic )
proof end;
end;

registration
let GF be non empty Graph-yielding edgeless Function;
let x be Element of dom GF;
cluster GF . x -> edgeless ;
coherence
GF . x is edgeless
by Def3;
end;

registration
let GSq be edgeless GraphSeq;
let x be Nat;
cluster GSq . x -> edgeless ;
coherence
GSq . x is edgeless
by Def4;
end;

registration
let G be _Graph;
cluster <*G*> -> Graph-yielding ;
coherence
<*G*> is Graph-yielding
proof end;
end;

registration
let G be _finite _Graph;
cluster <*G*> -> _finite ;
coherence
<*G*> is _finite
proof end;
end;

registration
let G be loopless _Graph;
cluster <*G*> -> loopless ;
coherence
<*G*> is loopless
proof end;
end;

registration
let G be _trivial _Graph;
cluster <*G*> -> _trivial ;
coherence
<*G*> is _trivial
proof end;
end;

registration
let G be non _trivial _Graph;
cluster <*G*> -> non-trivial ;
coherence
<*G*> is non-trivial
proof end;
end;

registration
let G be non-multi _Graph;
cluster <*G*> -> non-multi ;
coherence
<*G*> is non-multi
proof end;
end;

registration
let G be non-Dmulti _Graph;
cluster <*G*> -> non-Dmulti ;
coherence
<*G*> is non-Dmulti
proof end;
end;

registration
let G be simple _Graph;
cluster <*G*> -> simple ;
coherence
<*G*> is simple
;
end;

registration
let G be Dsimple _Graph;
cluster <*G*> -> Dsimple ;
coherence
<*G*> is Dsimple
;
end;

registration
let G be connected _Graph;
cluster <*G*> -> connected ;
coherence
<*G*> is connected
proof end;
end;

registration
let G be acyclic _Graph;
cluster <*G*> -> acyclic ;
coherence
<*G*> is acyclic
proof end;
end;

registration
let G be Tree-like _Graph;
cluster <*G*> -> Tree-like ;
coherence
<*G*> is Tree-like
;
end;

registration
let G be edgeless _Graph;
cluster <*G*> -> edgeless ;
coherence
<*G*> is edgeless
proof end;
end;

registration
cluster empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding for set ;
existence
ex b1 being FinSequence st
( b1 is empty & b1 is Graph-yielding )
proof end;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding for set ;
existence
ex b1 being FinSequence st
( not b1 is empty & b1 is Graph-yielding )
proof end;
end;

registration
let p be non empty Graph-yielding FinSequence;
cluster p . 1 -> Relation-like Function-like ;
coherence
( p . 1 is Function-like & p . 1 is Relation-like )
proof end;
cluster p . (len p) -> Relation-like Function-like ;
coherence
( p . (len p) is Function-like & p . (len p) is Relation-like )
proof end;
end;

registration
let p be non empty Graph-yielding FinSequence;
cluster p . 1 -> NAT -defined finite ;
coherence
( p . 1 is finite & p . 1 is NAT -defined )
proof end;
cluster p . (len p) -> NAT -defined finite ;
coherence
( p . (len p) is finite & p . (len p) is NAT -defined )
proof end;
end;

registration
let p be non empty Graph-yielding FinSequence;
cluster p . 1 -> [Graph-like] ;
coherence
p . 1 is [Graph-like]
proof end;
cluster p . (len p) -> [Graph-like] ;
coherence
p . (len p) is [Graph-like]
proof end;
end;

registration
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding _finite loopless _trivial non-multi non-Dmulti simple Dsimple connected acyclic Tree-like edgeless for set ;
existence
ex b1 being Graph-yielding FinSequence st
( not b1 is empty & b1 is _finite & b1 is loopless & b1 is _trivial & b1 is non-multi & b1 is non-Dmulti & b1 is simple & b1 is Dsimple & b1 is connected & b1 is acyclic & b1 is Tree-like & b1 is edgeless )
proof end;
cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding _finite loopless non-trivial non-multi non-Dmulti simple Dsimple connected acyclic Tree-like for set ;
existence
ex b1 being Graph-yielding FinSequence st
( not b1 is empty & b1 is _finite & b1 is loopless & b1 is non-trivial & b1 is non-multi & b1 is non-Dmulti & b1 is simple & b1 is Dsimple & b1 is connected & b1 is acyclic & b1 is Tree-like )
proof end;
end;

registration
let p be Graph-yielding FinSequence;
let n be Nat;
cluster p | n -> Graph-yielding ;
coherence
p | n is Graph-yielding
proof end;
cluster p /^ n -> Graph-yielding ;
coherence
p /^ n is Graph-yielding
proof end;
let m be Nat;
cluster smid (p,m,n) -> Graph-yielding ;
coherence
smid (p,m,n) is Graph-yielding
proof end;
cluster (m,n) -cut p -> Graph-yielding ;
coherence
(m,n) -cut p is Graph-yielding
proof end;
end;

registration
let p be Graph-yielding _finite FinSequence;
let n be Nat;
cluster p | n -> _finite ;
coherence
p | n is _finite
proof end;
cluster p /^ n -> _finite ;
coherence
p /^ n is _finite
proof end;
let m be Nat;
cluster smid (p,m,n) -> _finite ;
coherence
smid (p,m,n) is _finite
proof end;
cluster (m,n) -cut p -> _finite ;
coherence
(m,n) -cut p is _finite
proof end;
end;

registration
let p be Graph-yielding loopless FinSequence;
let n be Nat;
cluster p | n -> loopless ;
coherence
p | n is loopless
proof end;
cluster p /^ n -> loopless ;
coherence
p /^ n is loopless
proof end;
let m be Nat;
cluster smid (p,m,n) -> loopless ;
coherence
smid (p,m,n) is loopless
proof end;
cluster (m,n) -cut p -> loopless ;
coherence
(m,n) -cut p is loopless
proof end;
end;

registration
let p be Graph-yielding _trivial FinSequence;
let n be Nat;
cluster p | n -> _trivial ;
coherence
p | n is _trivial
proof end;
cluster p /^ n -> _trivial ;
coherence
p /^ n is _trivial
proof end;
let m be Nat;
cluster smid (p,m,n) -> _trivial ;
coherence
smid (p,m,n) is _trivial
proof end;
cluster (m,n) -cut p -> _trivial ;
coherence
(m,n) -cut p is _trivial
proof end;
end;

registration
let p be Graph-yielding non-trivial FinSequence;
let n be Nat;
cluster p | n -> non-trivial ;
coherence
p | n is non-trivial
proof end;
cluster p /^ n -> non-trivial ;
coherence
p /^ n is non-trivial
proof end;
let m be Nat;
cluster smid (p,m,n) -> non-trivial ;
coherence
smid (p,m,n) is non-trivial
proof end;
cluster (m,n) -cut p -> non-trivial ;
coherence
(m,n) -cut p is non-trivial
proof end;
end;

registration
let p be Graph-yielding non-multi FinSequence;
let n be Nat;
cluster p | n -> non-multi ;
coherence
p | n is non-multi
proof end;
cluster p /^ n -> non-multi ;
coherence
p /^ n is non-multi
proof end;
let m be Nat;
cluster smid (p,m,n) -> non-multi ;
coherence
smid (p,m,n) is non-multi
proof end;
cluster (m,n) -cut p -> non-multi ;
coherence
(m,n) -cut p is non-multi
proof end;
end;

registration
let p be Graph-yielding non-Dmulti FinSequence;
let n be Nat;
cluster p | n -> non-Dmulti ;
coherence
p | n is non-Dmulti
proof end;
cluster p /^ n -> non-Dmulti ;
coherence
p /^ n is non-Dmulti
proof end;
let m be Nat;
cluster smid (p,m,n) -> non-Dmulti ;
coherence
smid (p,m,n) is non-Dmulti
proof end;
cluster (m,n) -cut p -> non-Dmulti ;
coherence
(m,n) -cut p is non-Dmulti
proof end;
end;

registration
let p be Graph-yielding simple FinSequence;
let n be Nat;
cluster p | n -> simple ;
coherence
p | n is simple
;
cluster p /^ n -> simple ;
coherence
p /^ n is simple
;
let m be Nat;
cluster smid (p,m,n) -> simple ;
coherence
smid (p,m,n) is simple
;
cluster (m,n) -cut p -> simple ;
coherence
(m,n) -cut p is simple
;
end;

registration
let p be Graph-yielding Dsimple FinSequence;
let n be Nat;
cluster p | n -> Dsimple ;
coherence
p | n is Dsimple
;
cluster p /^ n -> Dsimple ;
coherence
p /^ n is Dsimple
;
let m be Nat;
cluster smid (p,m,n) -> Dsimple ;
coherence
smid (p,m,n) is Dsimple
;
cluster (m,n) -cut p -> Dsimple ;
coherence
(m,n) -cut p is Dsimple
;
end;

registration
let p be Graph-yielding connected FinSequence;
let n be Nat;
cluster p | n -> connected ;
coherence
p | n is connected
proof end;
cluster p /^ n -> connected ;
coherence
p /^ n is connected
proof end;
let m be Nat;
cluster smid (p,m,n) -> connected ;
coherence
smid (p,m,n) is connected
proof end;
cluster (m,n) -cut p -> connected ;
coherence
(m,n) -cut p is connected
proof end;
end;

registration
let p be Graph-yielding acyclic FinSequence;
let n be Nat;
cluster p | n -> acyclic ;
coherence
p | n is acyclic
proof end;
cluster p /^ n -> acyclic ;
coherence
p /^ n is acyclic
proof end;
let m be Nat;
cluster smid (p,m,n) -> acyclic ;
coherence
smid (p,m,n) is acyclic
proof end;
cluster (m,n) -cut p -> acyclic ;
coherence
(m,n) -cut p is acyclic
proof end;
end;

registration
let p be Graph-yielding Tree-like FinSequence;
let n be Nat;
cluster p | n -> Tree-like ;
coherence
p | n is Tree-like
;
cluster p /^ n -> Tree-like ;
coherence
p /^ n is Tree-like
;
let m be Nat;
cluster smid (p,m,n) -> Tree-like ;
coherence
smid (p,m,n) is Tree-like
;
cluster (m,n) -cut p -> Tree-like ;
coherence
(m,n) -cut p is Tree-like
;
end;

registration
let p be Graph-yielding edgeless FinSequence;
let n be Nat;
cluster p | n -> edgeless ;
coherence
p | n is edgeless
proof end;
cluster p /^ n -> edgeless ;
coherence
p /^ n is edgeless
proof end;
let m be Nat;
cluster smid (p,m,n) -> edgeless ;
coherence
smid (p,m,n) is edgeless
proof end;
cluster (m,n) -cut p -> edgeless ;
coherence
(m,n) -cut p is edgeless
proof end;
end;

registration
let p, q be Graph-yielding FinSequence;
cluster p ^ q -> Graph-yielding ;
coherence
p ^ q is Graph-yielding
proof end;
cluster p ^' q -> Graph-yielding ;
coherence
p ^' q is Graph-yielding
proof end;
end;

registration
let p, q be Graph-yielding _finite FinSequence;
cluster p ^ q -> _finite ;
coherence
p ^ q is _finite
proof end;
cluster p ^' q -> _finite ;
coherence
p ^' q is _finite
proof end;
end;

registration
let p, q be Graph-yielding loopless FinSequence;
cluster p ^ q -> loopless ;
coherence
p ^ q is loopless
proof end;
cluster p ^' q -> loopless ;
coherence
p ^' q is loopless
proof end;
end;

registration
let p, q be Graph-yielding _trivial FinSequence;
cluster p ^ q -> _trivial ;
coherence
p ^ q is _trivial
proof end;
cluster p ^' q -> _trivial ;
coherence
p ^' q is _trivial
proof end;
end;

registration
let p, q be Graph-yielding non-trivial FinSequence;
cluster p ^ q -> non-trivial ;
coherence
p ^ q is non-trivial
proof end;
cluster p ^' q -> non-trivial ;
coherence
p ^' q is non-trivial
proof end;
end;

registration
let p, q be Graph-yielding non-multi FinSequence;
cluster p ^ q -> non-multi ;
coherence
p ^ q is non-multi
proof end;
cluster p ^' q -> non-multi ;
coherence
p ^' q is non-multi
proof end;
end;

registration
let p, q be Graph-yielding non-Dmulti FinSequence;
cluster p ^ q -> non-Dmulti ;
coherence
p ^ q is non-Dmulti
proof end;
cluster p ^' q -> non-Dmulti ;
coherence
p ^' q is non-Dmulti
proof end;
end;

registration
let p, q be Graph-yielding simple FinSequence;
cluster p ^ q -> simple ;
coherence
p ^ q is simple
;
cluster p ^' q -> simple ;
coherence
p ^' q is simple
;
end;

registration
let p, q be Graph-yielding Dsimple FinSequence;
cluster p ^ q -> Dsimple ;
coherence
p ^ q is Dsimple
;
cluster p ^' q -> Dsimple ;
coherence
p ^' q is Dsimple
;
end;

registration
let p, q be Graph-yielding connected FinSequence;
cluster p ^ q -> connected ;
coherence
p ^ q is connected
proof end;
cluster p ^' q -> connected ;
coherence
p ^' q is connected
proof end;
end;

registration
let p, q be Graph-yielding acyclic FinSequence;
cluster p ^ q -> acyclic ;
coherence
p ^ q is acyclic
proof end;
cluster p ^' q -> acyclic ;
coherence
p ^' q is acyclic
proof end;
end;

registration
let p, q be Graph-yielding Tree-like FinSequence;
cluster p ^ q -> Tree-like ;
coherence
p ^ q is Tree-like
;
cluster p ^' q -> Tree-like ;
coherence
p ^' q is Tree-like
;
end;

registration
let p, q be Graph-yielding edgeless FinSequence;
cluster p ^ q -> edgeless ;
coherence
p ^ q is edgeless
proof end;
cluster p ^' q -> edgeless ;
coherence
p ^' q is edgeless
proof end;
end;

registration
let G1, G2 be _Graph;
cluster <*G1,G2*> -> Graph-yielding ;
coherence
<*G1,G2*> is Graph-yielding
proof end;
let G3 be _Graph;
cluster <*G1,G2,G3*> -> Graph-yielding ;
coherence
<*G1,G2,G3*> is Graph-yielding
proof end;
end;

registration
let G1, G2 be _finite _Graph;
cluster <*G1,G2*> -> _finite ;
coherence
<*G1,G2*> is _finite
proof end;
let G3 be _finite _Graph;
cluster <*G1,G2,G3*> -> _finite ;
coherence
<*G1,G2,G3*> is _finite
proof end;
end;

registration
let G1, G2 be loopless _Graph;
cluster <*G1,G2*> -> loopless ;
coherence
<*G1,G2*> is loopless
proof end;
let G3 be loopless _Graph;
cluster <*G1,G2,G3*> -> loopless ;
coherence
<*G1,G2,G3*> is loopless
proof end;
end;

registration
let G1, G2 be _trivial _Graph;
cluster <*G1,G2*> -> _trivial ;
coherence
<*G1,G2*> is _trivial
proof end;
let G3 be _trivial _Graph;
cluster <*G1,G2,G3*> -> _trivial ;
coherence
<*G1,G2,G3*> is _trivial
proof end;
end;

registration
let G1, G2 be non _trivial _Graph;
cluster <*G1,G2*> -> non-trivial ;
coherence
<*G1,G2*> is non-trivial
proof end;
let G3 be non _trivial _Graph;
cluster <*G1,G2,G3*> -> non-trivial ;
coherence
<*G1,G2,G3*> is non-trivial
proof end;
end;

registration
let G1, G2 be non-multi _Graph;
cluster <*G1,G2*> -> non-multi ;
coherence
<*G1,G2*> is non-multi
proof end;
let G3 be non-multi _Graph;
cluster <*G1,G2,G3*> -> non-multi ;
coherence
<*G1,G2,G3*> is non-multi
proof end;
end;

registration
let G1, G2 be non-Dmulti _Graph;
cluster <*G1,G2*> -> non-Dmulti ;
coherence
<*G1,G2*> is non-Dmulti
proof end;
let G3 be non-Dmulti _Graph;
cluster <*G1,G2,G3*> -> non-Dmulti ;
coherence
<*G1,G2,G3*> is non-Dmulti
proof end;
end;

registration
let G1, G2 be simple _Graph;
cluster <*G1,G2*> -> simple ;
coherence
<*G1,G2*> is simple
;
let G3 be simple _Graph;
cluster <*G1,G2,G3*> -> simple ;
coherence
<*G1,G2,G3*> is simple
;
end;

registration
let G1, G2 be Dsimple _Graph;
cluster <*G1,G2*> -> Dsimple ;
coherence
<*G1,G2*> is Dsimple
;
let G3 be Dsimple _Graph;
cluster <*G1,G2,G3*> -> Dsimple ;
coherence
<*G1,G2,G3*> is Dsimple
;
end;

registration
let G1, G2 be connected _Graph;
cluster <*G1,G2*> -> connected ;
coherence
<*G1,G2*> is connected
proof end;
let G3 be connected _Graph;
cluster <*G1,G2,G3*> -> connected ;
coherence
<*G1,G2,G3*> is connected
proof end;
end;

registration
let G1, G2 be acyclic _Graph;
cluster <*G1,G2*> -> acyclic ;
coherence
<*G1,G2*> is acyclic
proof end;
let G3 be acyclic _Graph;
cluster <*G1,G2,G3*> -> acyclic ;
coherence
<*G1,G2,G3*> is acyclic
proof end;
end;

registration
let G1, G2 be Tree-like _Graph;
cluster <*G1,G2*> -> Tree-like ;
coherence
<*G1,G2*> is Tree-like
;
let G3 be Tree-like _Graph;
cluster <*G1,G2,G3*> -> Tree-like ;
coherence
<*G1,G2,G3*> is Tree-like
;
end;

registration
let G1, G2 be edgeless _Graph;
cluster <*G1,G2*> -> edgeless ;
coherence
<*G1,G2*> is edgeless
proof end;
let G3 be edgeless _Graph;
cluster <*G1,G2,G3*> -> edgeless ;
coherence
<*G1,G2,G3*> is edgeless
proof end;
end;

:: finite addition of vertices can be finitely constructed with addVertex only
theorem Th59: :: GLIB_008:59
for G2 being _Graph
for V being finite set
for G1 being addVertices of G2,V ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
proof end;

theorem Th60: :: GLIB_008:60
for G being _finite _Graph
for H being Subgraph of G st G .size() = H .size() holds
ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
proof end;

theorem Th61: :: GLIB_008:61
for G being _finite edgeless _Graph
for H being Subgraph of G ex p being non empty Graph-yielding _finite edgeless FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
proof end;

:: finite edgeless graphs can be finitely constructed with addVertex only
theorem Th62: :: GLIB_008:62
for G being _finite edgeless _Graph ex p being non empty Graph-yielding _finite edgeless FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
proof end;

scheme :: GLIB_008:sch 1
FinEdgelessGraphs{ P1[ _finite _Graph] } :
for G being _finite edgeless _Graph holds P1[G]
provided
A1: for G being _trivial edgeless _Graph holds P1[G] and
A2: for G2 being _finite edgeless _Graph
for v being object
for G1 being addVertex of G2,v st not v in the_Vertices_of G2 & P1[G2] holds
P1[G1]
proof end;

theorem :: GLIB_008:63
for p being non empty Graph-yielding FinSequence st p . 1 is edgeless & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ) holds
p . (len p) is edgeless
proof end;

theorem Th64: :: GLIB_008:64
for G being _finite _Graph
for H being spanning Subgraph of G ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
proof end;

theorem :: GLIB_008:65
for G being _finite _Graph ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 is edgeless & p . (len p) = G & len p = (G .size()) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
proof end;

theorem Th66: :: GLIB_008:66
for G being _finite connected _Graph
for H being spanning connected Subgraph of G ex p being non empty Graph-yielding _finite connected FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .size()) - (H .size())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) )
proof end;

theorem Th67: :: GLIB_008:67
for G1 being _finite _Graph
for H being Subgraph of G1 ex G2 being spanning Subgraph of G1 ex p being non empty Graph-yielding _finite FinSequence st
( H .size() = G2 .size() & p . 1 == H & p . (len p) = G2 & len p = ((G1 .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
proof end;

theorem Th68: :: GLIB_008:68
for G being _finite _Graph
for H being Subgraph of G ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 == H & p . (len p) = G & len p = (((G .order()) + (G .size())) - ((H .order()) + (H .size()))) + 1 & ( for n being Element of dom p holds
( not n <= (len p) - 1 or ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) or ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) ) )
proof end;

:: finite graphs can be finitely constructed with addVertex and addEdge only
theorem Th69: :: GLIB_008:69
for G being _finite _Graph ex p being non empty Graph-yielding _finite FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = (G .order()) + (G .size()) & ( for n being Element of dom p holds
( not n <= (len p) - 1 or ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) or ex v being Vertex of G st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) ) )
proof end;

scheme :: GLIB_008:sch 2
FinGraphs{ P1[ _finite _Graph] } :
for G being _finite _Graph holds P1[G]
provided
A1: for G being _trivial edgeless _Graph holds P1[G] and
A2: for G2 being _finite _Graph
for v being object
for G1 being addVertex of G2,v st not v in the_Vertices_of G2 & P1[G2] holds
P1[G1] and
A3: for G2 being _finite _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & P1[G2] holds
P1[G1]
proof end;

theorem :: GLIB_008:70
for p being non empty Graph-yielding FinSequence st p . 1 is _finite & ( for n being Element of dom p holds
( not n <= (len p) - 1 or ex v being object st p . (n + 1) is addVertex of p . n,v or ex v1, e, v2 being object st p . (n + 1) is addEdge of p . n,v1,e,v2 ) ) holds
p . (len p) is _finite
proof end;

theorem Th71: :: GLIB_008:71
for G being _finite Tree-like _Graph
for H being connected Subgraph of G ex p being non empty Graph-yielding _finite Tree-like FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) ) )
proof end;

:: finite trees can be finitely constructed with addAdjVertex only
theorem Th72: :: GLIB_008:72
for G being _finite Tree-like _Graph ex p being non empty Graph-yielding _finite Tree-like FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) ) )
proof end;

scheme :: GLIB_008:sch 3
FinTrees{ P1[ _finite _Graph] } :
for G being _finite Tree-like _Graph holds P1[G]
provided
A1: for G being _trivial edgeless _Graph holds P1[G] and
A2: for G2 being _finite Tree-like _Graph
for v being Vertex of G2
for e, w being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & P1[G2] holds
( ( for G1 being addAdjVertex of G2,v,e,w holds P1[G1] ) & ( for G1 being addAdjVertex of G2,w,e,v holds P1[G1] ) )
proof end;

theorem :: GLIB_008:73
for p being non empty Graph-yielding FinSequence st p . 1 is Tree-like & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, e, v2 being object st p . (n + 1) is addAdjVertex of p . n,v1,e,v2 ) holds
p . (len p) is Tree-like
proof end;

:: finite connected graphs can be constructed with addAdjVertex and addEdge
theorem Th74: :: GLIB_008:74
for G being _finite connected _Graph ex p being non empty Graph-yielding _finite connected FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = (G .size()) + 1 & ( for n being Element of dom p holds
( not n <= (len p) - 1 or ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) or ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addEdge of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) ) ) ) )
proof end;

scheme :: GLIB_008:sch 4
FinConnectedGraphs{ P1[ _finite _Graph] } :
for G being _finite connected _Graph holds P1[G]
provided
A1: for G being _trivial edgeless _Graph holds P1[G] and
A2: for G2 being _finite connected _Graph
for v being Vertex of G2
for e, w being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & P1[G2] holds
( ( for G1 being addAdjVertex of G2,v,e,w holds P1[G1] ) & ( for G1 being addAdjVertex of G2,w,e,v holds P1[G1] ) ) and
A3: for G2 being _finite connected _Graph
for v1, v2 being Vertex of G2
for e being object
for G1 being addEdge of G2,v1,e,v2 st not e in the_Edges_of G2 & P1[G2] holds
P1[G1]
proof end;

theorem :: GLIB_008:75
for p being non empty Graph-yielding FinSequence st p . 1 is connected & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, e, v2 being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 or p . (n + 1) is addEdge of p . n,v1,e,v2 ) ) holds
p . (len p) is connected
proof end;

theorem Th76: :: GLIB_008:76
for G2 being _Graph
for v being object
for V1 being set
for V2 being finite set
for G1 being addAdjVertexAll of G2,v,V1 \/ V2 st V1 \/ V2 c= the_Vertices_of G2 & not v in the_Vertices_of G2 & V1 misses V2 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 = G2 & p . (len p) = G1 & len p = (card V2) + 2 & p . 2 is addAdjVertexAll of G2,v,V1 & ( for n being Element of dom p st 2 <= n & n <= (len p) - 1 holds
ex w being Vertex of G2 ex e being object st
( e in (the_Edges_of G1) \ (the_Edges_of (p . n)) & ( p . (n + 1) is addEdge of p . n,v,e,w or p . (n + 1) is addEdge of p . n,w,e,v ) ) ) )
proof end;

theorem :: GLIB_008:77
for G2 being _Graph
for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 = G2 & p . (len p) = G1 & len p = (card V) + 2 & p . 2 is addVertex of G2,v & ( for n being Element of dom p st 2 <= n & n <= (len p) - 1 holds
ex w being Vertex of G2 ex e being object st
( e in (the_Edges_of G1) \ (the_Edges_of (p . n)) & ( p . (n + 1) is addEdge of p . n,v,e,w or p . (n + 1) is addEdge of p . n,w,e,v ) ) ) )
proof end;

theorem :: GLIB_008:78
for G2 being _Graph
for v being object
for V being non empty finite set
for G1 being addAdjVertexAll of G2,v,V st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 = G2 & p . (len p) = G1 & len p = (card V) + 1 & ex w being Vertex of G2 ex e being object st
( e in (the_Edges_of G1) \ (the_Edges_of G2) & ( p . 2 is addAdjVertex of G2,v,e,w or p . 2 is addAdjVertex of G2,w,e,v ) ) & ( for n being Element of dom p st 2 <= n & n <= (len p) - 1 holds
ex w being Vertex of G2 ex e being object st
( e in (the_Edges_of G1) \ (the_Edges_of (p . n)) & ( p . (n + 1) is addEdge of p . n,v,e,w or p . (n + 1) is addEdge of p . n,w,e,v ) ) ) )
proof end;

theorem Th79: :: GLIB_008:79
for G being _finite simple _Graph
for W being set
for H being inducedSubgraph of G,W ex p being non empty Graph-yielding _finite simple FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) )
proof end;

theorem Th80: :: GLIB_008:80
for G being _finite simple _Graph ex p being non empty Graph-yielding _finite simple FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) )
proof end;

scheme :: GLIB_008:sch 5
FinSimpleGraphs{ P1[ _finite _Graph] } :
for G being _finite simple _Graph holds P1[G]
provided
A1: for G being _trivial edgeless _Graph holds P1[G] and
A2: for G2 being _finite simple _Graph
for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 & V c= the_Vertices_of G2 & P1[G2] holds
P1[G1]
proof end;

theorem :: GLIB_008:81
for p being non empty Graph-yielding FinSequence st p . 1 is simple & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being set st p . (n + 1) is addAdjVertexAll of p . n,v,V ) holds
p . (len p) is simple
proof end;

theorem Th82: :: GLIB_008:82
for G being _finite simple connected _Graph ex p being non empty Graph-yielding _finite simple connected FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty finite set st
( v in (the_Vertices_of G) \ (the_Vertices_of (p . n)) & V c= the_Vertices_of (p . n) & p . (n + 1) is addAdjVertexAll of p . n,v,V ) ) )
proof end;

scheme :: GLIB_008:sch 6
FinSimpleConnectedGraphs{ P1[ _finite _Graph] } :
for G being _finite simple connected _Graph holds P1[G]
provided
A1: for G being _trivial edgeless _Graph holds P1[G] and
A2: for G2 being _finite simple connected _Graph
for v being object
for V being non empty finite set
for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 & V c= the_Vertices_of G2 & P1[G2] holds
P1[G1]
proof end;

theorem :: GLIB_008:83
for p being non empty Graph-yielding FinSequence st p . 1 is simple & p . 1 is connected & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object ex V being non empty set st p . (n + 1) is addAdjVertexAll of p . n,v,V ) holds
( p . (len p) is simple & p . (len p) is connected )
proof end;