:: 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 b₁ being inducedSubgraph of G,{v} holds b₁ 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 b₁ being removeEdges of G,X holds not b₁ 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 b₁ being Subgraph of G st
( b₁ is spanning & b₁ is Tree-like & b₁ is connected & b₁ 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 b₁ being Subgraph of G st
( not b₁ is spanning & b₁ is _trivial & b₁ 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 b₁ being Vertex of G st b₁ is endvertex holds
not b₁ 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 b₁ being removeEdges of G,(the_Edges_of G) holds b₁ is edgeless

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like finite [Graph-like] edgeless for set ;

existence
ex b₁ being _Graph st b₁ 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 b₁ being Subgraph of G st
( b₁ is edgeless & b₁ is spanning )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] _trivial edgeless for Subgraph of G;

existence
ex b₁ being Subgraph of G st
( b₁ is edgeless & b₁ 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 b₁ being _Graph st b₁ is edgeless holds
( b₁ is non-multi & b₁ is non-Dmulti & b₁ is loopless & b₁ is simple & b₁ is Dsimple )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] loopless _trivial -> edgeless for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is loopless holds
b₁ 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 b₁ being Walk of G holds b₁ is V5()

proof end;

cluster -> edgeless for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ 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 b₁ being addVertices of G,X holds b₁ is edgeless

proof end;

cluster -> edgeless for reverseEdgeDirections of G,X;

coherence
for b₁ being reverseEdgeDirections of G,X holds b₁ 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 b₁ being _Graph st b₁ is edgeless holds
( b₁ is acyclic & b₁ is chordal )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] _trivial edgeless -> Tree-like for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is edgeless holds
b₁ 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 b₁ being _Graph st not b₁ is _trivial & b₁ is edgeless holds
( not b₁ is connected & not b₁ is Tree-like & not b₁ is complete )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] connected edgeless -> _trivial for set ;

coherence
for b₁ being _Graph st b₁ is connected & b₁ is edgeless holds
b₁ 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 b₁ being addAdjVertexToAll of G, the_Vertices_of G holds not b₁ is edgeless

proof end;

cluster -> non edgeless for addAdjVertexFromAll of G, the_Vertices_of G, the_Vertices_of G;

coherence
for b₁ being addAdjVertexFromAll of G, the_Vertices_of G holds not b₁ is edgeless

proof end;

cluster -> non edgeless for addAdjVertexAll of G, the_Vertices_of G, the_Vertices_of G;

coherence
for b₁ being addAdjVertexAll of G, the_Vertices_of G holds not b₁ 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 b₁ being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b₁ is edgeless

proof end;

cluster -> non edgeless for addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v;

coherence
for b₁ being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds not b₁ 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 b₁ being addEdge of G,v, the_Edges_of G,w holds not b₁ is edgeless

proof end;

end;

registration

let G be edgeless _Graph;

cluster Component-like -> _trivial for Subgraph of G;

coherence
for b₁ being Component of G holds b₁ 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 b₁ being Vertex of G holds
( b₁ is isolated & not b₁ is cut-vertex & not b₁ 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 b₁ being _Graph st
( b₁ is _trivial & b₁ is _finite & b₁ is edgeless )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite non _trivial edgeless for set ;

existence
ex b₁ being _Graph st
( not b₁ is _trivial & b₁ is _finite & b₁ is edgeless )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite _trivial non edgeless for set ;

existence
ex b₁ being _Graph st
( b₁ is _trivial & b₁ is _finite & not b₁ is edgeless )

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] _finite non _trivial non edgeless for set ;

existence
ex b₁ being _Graph st
( not b₁ is _trivial & b₁ is _finite & not b₁ 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 b₁ being Supergraph of G holds not b₁ is edgeless

proof end;

let X be set ;

cluster -> non edgeless for reverseEdgeDirections of G,X;

coherence
for b₁ being reverseEdgeDirections of G,X holds not b₁ 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 b₁ being Graph-yielding Function st b₁ is _trivial & b₁ is loopless holds
b₁ 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 b₁ being Graph-yielding Function st b₁ is edgeless holds
( b₁ is non-multi & b₁ is non-Dmulti & b₁ is loopless & b₁ is simple & b₁ is Dsimple & b₁ 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 b₁ being FinSequence st
( b₁ is empty & b₁ 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 b₁ being FinSequence st
( not b₁ is empty & b₁ 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 b₁ being Graph-yielding FinSequence st
( not b₁ is empty & b₁ is _finite & b₁ is loopless & b₁ is _trivial & b₁ is non-multi & b₁ is non-Dmulti & b₁ is simple & b₁ is Dsimple & b₁ is connected & b₁ is acyclic & b₁ is Tree-like & b₁ 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 b₁ being Graph-yielding FinSequence st
( not b₁ is empty & b₁ is _finite & b₁ is loopless & b₁ is non-trivial & b₁ is non-multi & b₁ is non-Dmulti & b₁ is simple & b₁ is Dsimple & b₁ is connected & b₁ is acyclic & b₁ 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{ P₁[ _finite _Graph] } :

for G being _finite edgeless _Graph holds P₁[G]

provided

A1: for G being _trivial edgeless _Graph holds P₁[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 & P₁[G2] holds
P₁[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{ P₁[ _finite _Graph] } :

for G being _finite _Graph holds P₁[G]

provided

A1: for G being _trivial edgeless _Graph holds P₁[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 & P₁[G2] holds
P₁[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 & P₁[G2] holds
P₁[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{ P₁[ _finite _Graph] } :

for G being _finite Tree-like _Graph holds P₁[G]

provided

A1: for G being _trivial edgeless _Graph holds P₁[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 & P₁[G2] holds
( ( for G1 being addAdjVertex of G2,v,e,w holds P₁[G1] ) & ( for G1 being addAdjVertex of G2,w,e,v holds P₁[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{ P₁[ _finite _Graph] } :

for G being _finite connected _Graph holds P₁[G]

provided

A1: for G being _trivial edgeless _Graph holds P₁[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 & P₁[G2] holds
( ( for G1 being addAdjVertex of G2,v,e,w holds P₁[G1] ) & ( for G1 being addAdjVertex of G2,w,e,v holds P₁[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 & P₁[G2] holds
P₁[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{ P₁[ _finite _Graph] } :

for G being _finite simple _Graph holds P₁[G]

provided

A1: for G being _trivial edgeless _Graph holds P₁[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 & P₁[G2] holds
P₁[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{ P₁[ _finite _Graph] } :

for G being _finite simple connected _Graph holds P₁[G]

provided

A1: for G being _trivial edgeless _Graph holds P₁[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 & P₁[G2] holds
P₁[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;