:: by Sebastian Koch

::

:: Received May 27, 2019

:: Copyright (c) 2019 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;

coherence

for b_{1} being inducedSubgraph of G,{v} holds b_{1} is trivial

end;
let v be Vertex of G;

coherence

for b

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

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

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 Th4: :: GLIB_008:4

for G being non-Dmulti _Graph

for v being Vertex of G holds v .outDegree() = card (v .outNeighbors())

for v being Vertex of G holds v .outDegree() = card (v .outNeighbors())

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

( G is loopless iff for v being Vertex of G holds not v in 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

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

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

registration

let G be non trivial _Graph;

let X be set ;

coherence

for b_{1} being removeEdges of G,X holds not b_{1} is trivial

end;
let X be set ;

coherence

for b

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

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

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

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

for V being set

for G2 being inducedSubgraph of G1,V st G2 is spanning holds

G1 == G2

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

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

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;

ex b_{1} being Subgraph of G st

( b_{1} is spanning & b_{1} is Tree-like & b_{1} is connected & b_{1} is acyclic )
by Lm6;

end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] finite spanning connected acyclic Tree-like for Subgraph of G;

existence ex b

( b

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

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

for G2 being Subgraph of G1 st G1 .size() = G2 .size() holds

G1 == G2

proof end;

registration

let G be non trivial _Graph;

ex b_{1} being Subgraph of G st

( not b_{1} is spanning & b_{1} is trivial & b_{1} is connected )

end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] trivial non spanning connected for Subgraph of G;

existence ex b

( not b

proof 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

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

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

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

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

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

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;

coherence

not v .allNeighbors() is empty by Th7, GLIB_002:2;

end;
let v be Vertex of G;

coherence

not v .allNeighbors() is empty by Th7, GLIB_002:2;

:: END into GLIB_002 ?

:: into HELLY ?

:: into HELLY ?

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

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

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 )

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

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)

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)

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

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

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

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

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

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

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

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)

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

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

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

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;

coherence

for b_{1} being Vertex of G st b_{1} is endvertex holds

not b_{1} is cut-vertex

end;
coherence

for b

not b

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

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

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

:: deftheorem Def1 defines edgeless GLIB_008:def 1 :

for G being _Graph holds

( G is edgeless iff the_Edges_of G = {} );

for G being _Graph holds

( G is edgeless iff the_Edges_of G = {} );

registration

let G be _Graph;

for b_{1} being removeEdges of G,(the_Edges_of G) holds b_{1} is edgeless

end;
cluster -> edgeless for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (the_Edges_of G);

coherence for b

proof end;

registration

existence

ex b_{1} being _Graph st b_{1} is edgeless

ex b_{1} being Subgraph of G st

( b_{1} is edgeless & b_{1} is spanning )

ex b_{1} being Subgraph of G st

( b_{1} is edgeless & b_{1} is trivial )

end;
ex b

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

( b

proof end;

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

existence ex b

( b

proof end;

registration

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

( b_{1} is non-multi & b_{1} is non-Dmulti & b_{1} is loopless & b_{1} is simple & b_{1} is Dsimple )

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

b_{1} is edgeless
by GLIB_000:23;

let V be non empty set ;

let S, T be Function of {},V;

coherence

createGraph (V,{},S,T) is edgeless by GLIB_000:6;

end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] edgeless -> loopless non-multi non-Dmulti simple Dsimple for set ;

coherence for b

( b

proof end;

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

coherence for b

b

let V be non empty set ;

let S, T be Function of {},V;

coherence

createGraph (V,{},S,T) is edgeless by GLIB_000:6;

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 )

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 )

for e being object

for X, Y being set holds

( not e SJoins X,Y,G & not e DSJoins X,Y,G )

proof end;

registration

let G be edgeless _Graph;

coherence

for b_{1} being Walk of G holds b_{1} is trivial

for b_{1} being Subgraph of G holds b_{1} is edgeless

coherence

G .edgesInto X is empty ;

coherence

G .edgesOutOf X is empty ;

coherence

G .edgesInOut X is empty ;

coherence

G .edgesBetween X is empty ;

coherence

G .set (WeightSelector,X) is edgeless by GLIB_003:7, Th52;

coherence

G .set (ELabelSelector,X) is edgeless by GLIB_003:7, Th52;

coherence

G .set (VLabelSelector,X) is edgeless by GLIB_003:7, Th52;

coherence

for b_{1} being addVertices of G,X holds b_{1} is edgeless

for b_{1} being reverseEdgeDirections of G,X holds b_{1} is edgeless

coherence

G .edgesBetween (X,Y) is empty ;

coherence

G .edgesDBetween (X,Y) is empty ;

end;
coherence

for b

proof end;

coherence for b

proof end;

let X be set ;coherence

G .edgesInto X is empty ;

coherence

G .edgesOutOf X is empty ;

coherence

G .edgesInOut X is empty ;

coherence

G .edgesBetween X is empty ;

coherence

G .set (WeightSelector,X) is edgeless by GLIB_003:7, Th52;

coherence

G .set (ELabelSelector,X) is edgeless by GLIB_003:7, Th52;

coherence

G .set (VLabelSelector,X) is edgeless by GLIB_003:7, Th52;

coherence

for b

proof end;

coherence for b

proof end;

let Y be set ;coherence

G .edgesBetween (X,Y) is empty ;

coherence

G .edgesDBetween (X,Y) is empty ;

registration

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

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

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

b_{1} is Tree-like
;

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

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

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

b_{1} is trivial
;

end;

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

coherence for b

( b

proof end;

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

coherence for b

b

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

( not b

proof end;

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

coherence for b

b

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)

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

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

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

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;

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;

coherence

for b_{1} being addAdjVertexToAll of G, the_Vertices_of G holds not b_{1} is edgeless

for b_{1} being addAdjVertexFromAll of G, the_Vertices_of G holds not b_{1} is edgeless

for b_{1} being addAdjVertexAll of G, the_Vertices_of G holds not b_{1} is edgeless

coherence

for b_{1} being addAdjVertex of G,v, the_Edges_of G, the_Vertices_of G holds not b_{1} is edgeless

for b_{1} being addAdjVertex of G, the_Vertices_of G, the_Edges_of G,v holds not b_{1} is edgeless

coherence

for b_{1} being addEdge of G,v, the_Edges_of G,w holds not b_{1} is edgeless

end;
coherence

for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

let v be Vertex of G;coherence

for b

proof end;

coherence for b

proof end;

let w be Vertex of G;coherence

for b

proof end;

registration

let G be edgeless _Graph;

coherence

for b_{1} being Component of G holds b_{1} is trivial
;

let v be Vertex of G;

coherence

v .edgesIn() is empty ;

coherence

v .edgesOut() is empty ;

coherence

v .edgesInOut() is empty ;

end;
coherence

for b

let v be Vertex of G;

coherence

v .edgesIn() is empty ;

coherence

v .edgesOut() is empty ;

coherence

v .edgesInOut() is empty ;

registration

let G be edgeless _Graph;

coherence

for b_{1} being Vertex of G holds

( b_{1} is isolated & not b_{1} is cut-vertex & not b_{1} is endvertex )

coherence

v .inDegree() is empty

v .outDegree() is empty

v .inNeighbors() is empty

v .outNeighbors() is empty

end;
coherence

for b

( b

proof end;

let v be Vertex of G;coherence

v .inDegree() is empty

proof end;

coherence v .outDegree() is empty

proof end;

coherence v .inNeighbors() is empty

proof end;

coherence v .outNeighbors() is empty

proof end;

registration

let G be edgeless _Graph;

let v be Vertex of G;

coherence

v .degree() is empty

v .allNeighbors() is empty

end;
let v be Vertex of G;

coherence

v .degree() is empty

proof end;

coherence v .allNeighbors() is empty

proof end;

registration

ex b_{1} being _Graph st

( b_{1} is trivial & b_{1} is finite & b_{1} is edgeless )

ex b_{1} being _Graph st

( not b_{1} is trivial & b_{1} is finite & b_{1} is edgeless )

ex b_{1} being _Graph st

( b_{1} is trivial & b_{1} is finite & not b_{1} is edgeless )

ex b_{1} being _Graph st

( not b_{1} is trivial & b_{1} is finite & not b_{1} is edgeless )
end;

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

existence ex b

( b

proof end;

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

existence ex b

( not b

proof end;

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

existence ex b

( b

proof end;

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

existence ex b

( not b

proof end;

registration

let G be non edgeless _Graph;

coherence

not the_Edges_of G is empty by Def1;

coherence

for b_{1} being Supergraph of G holds not b_{1} is edgeless

coherence

for b_{1} being reverseEdgeDirections of G,X holds not b_{1} is edgeless

not G .set (WeightSelector,X) is edgeless

not G .set (ELabelSelector,X) is edgeless

not G .set (VLabelSelector,X) is edgeless

end;
coherence

not the_Edges_of G is empty by Def1;

coherence

for b

proof end;

let X be set ;coherence

for b

proof end;

coherence not G .set (WeightSelector,X) is edgeless

proof end;

coherence not G .set (ELabelSelector,X) is edgeless

proof end;

coherence not G .set (VLabelSelector,X) is edgeless

proof 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

for G2 being Subgraph of G1 st G1 .order() = G2 .order() holds

G1 == G2

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

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;

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

end;
redefine attr GF is edgeless means :Def3: :: GLIB_008:def 3

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

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

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

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

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;

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

end;
redefine attr GSq is edgeless means :Def4: :: GLIB_008:def 4

for n being Nat holds GSq . n is edgeless ;

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

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

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

for GSq being GraphSeq holds

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

registration

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

b_{1} is edgeless

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

( b_{1} is non-multi & b_{1} is non-Dmulti & b_{1} is loopless & b_{1} is simple & b_{1} is Dsimple & b_{1} is acyclic )
end;

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

coherence for b

b

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

( b

proof end;

registration

let GF be non empty Graph-yielding edgeless Function;

let x be Element of dom GF;

coherence

GF . x is edgeless by Def3;

end;
let x be Element of dom GF;

coherence

GF . x is edgeless by Def3;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

ex b_{1} being FinSequence st

( b_{1} is empty & b_{1} is Graph-yielding )

ex b_{1} being FinSequence st

( not b_{1} is empty & b_{1} is Graph-yielding )
end;

cluster empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding for set ;

existence ex b

( b

proof end;

cluster non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Graph-yielding for set ;

existence ex b

( not b

proof end;

registration

let p be non empty Graph-yielding FinSequence;

coherence

( p . 1 is Function-like & p . 1 is Relation-like )

( p . (len p) is Function-like & p . (len p) is Relation-like )

end;
coherence

( p . 1 is Function-like & p . 1 is Relation-like )

proof end;

coherence ( p . (len p) is Function-like & p . (len p) is Relation-like )

proof end;

registration

let p be non empty Graph-yielding FinSequence;

coherence

( p . 1 is finite & p . 1 is NAT -defined )

( p . (len p) is finite & p . (len p) is NAT -defined )

end;
coherence

( p . 1 is finite & p . 1 is NAT -defined )

proof end;

coherence ( p . (len p) is finite & p . (len p) is NAT -defined )

proof end;

registration

let p be non empty Graph-yielding FinSequence;

coherence

p . 1 is [Graph-like]

p . (len p) is [Graph-like]

end;
coherence

p . 1 is [Graph-like]

proof end;

coherence p . (len p) is [Graph-like]

proof end;

registration

ex b_{1} being Graph-yielding FinSequence st

( not b_{1} is empty & b_{1} is finite & b_{1} is loopless & b_{1} is trivial & b_{1} is non-multi & b_{1} is non-Dmulti & b_{1} is simple & b_{1} is Dsimple & b_{1} is connected & b_{1} is acyclic & b_{1} is Tree-like & b_{1} is edgeless )

ex b_{1} being Graph-yielding FinSequence st

( not b_{1} is empty & b_{1} is finite & b_{1} is loopless & b_{1} is non-trivial & b_{1} is non-multi & b_{1} is non-Dmulti & b_{1} is simple & b_{1} is Dsimple & b_{1} is connected & b_{1} is acyclic & b_{1} is Tree-like )
end;

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

( not b

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

( not b

proof end;

registration

let p be Graph-yielding FinSequence;

let n be Nat;

coherence

p | n is Graph-yielding

p /^ n is Graph-yielding

coherence

smid (p,m,n) is Graph-yielding

(m,n) -cut p is Graph-yielding

end;
let n be Nat;

coherence

p | n is Graph-yielding

proof end;

coherence p /^ n is Graph-yielding

proof end;

let m be Nat;coherence

smid (p,m,n) is Graph-yielding

proof end;

coherence (m,n) -cut p is Graph-yielding

proof end;

registration

let p be Graph-yielding finite FinSequence;

let n be Nat;

coherence

p | n is finite

p /^ n is finite

coherence

smid (p,m,n) is finite

(m,n) -cut p is finite

end;
let n be Nat;

coherence

p | n is finite

proof end;

coherence p /^ n is finite

proof end;

let m be Nat;coherence

smid (p,m,n) is finite

proof end;

coherence (m,n) -cut p is finite

proof end;

registration

let p be Graph-yielding loopless FinSequence;

let n be Nat;

coherence

p | n is loopless

p /^ n is loopless

coherence

smid (p,m,n) is loopless

(m,n) -cut p is loopless

end;
let n be Nat;

coherence

p | n is loopless

proof end;

coherence p /^ n is loopless

proof end;

let m be Nat;coherence

smid (p,m,n) is loopless

proof end;

coherence (m,n) -cut p is loopless

proof end;

registration

let p be Graph-yielding trivial FinSequence;

let n be Nat;

coherence

p | n is trivial

p /^ n is trivial

coherence

smid (p,m,n) is trivial

(m,n) -cut p is trivial

end;
let n be Nat;

coherence

p | n is trivial

proof end;

coherence p /^ n is trivial

proof end;

let m be Nat;coherence

smid (p,m,n) is trivial

proof end;

coherence (m,n) -cut p is trivial

proof end;

registration

let p be Graph-yielding non-trivial FinSequence;

let n be Nat;

coherence

p | n is non-trivial

p /^ n is non-trivial

coherence

smid (p,m,n) is non-trivial

(m,n) -cut p is non-trivial

end;
let n be Nat;

coherence

p | n is non-trivial

proof end;

coherence p /^ n is non-trivial

proof end;

let m be Nat;coherence

smid (p,m,n) is non-trivial

proof end;

coherence (m,n) -cut p is non-trivial

proof end;

registration

let p be Graph-yielding non-multi FinSequence;

let n be Nat;

coherence

p | n is non-multi

p /^ n is non-multi

coherence

smid (p,m,n) is non-multi

(m,n) -cut p is non-multi

end;
let n be Nat;

coherence

p | n is non-multi

proof end;

coherence p /^ n is non-multi

proof end;

let m be Nat;coherence

smid (p,m,n) is non-multi

proof end;

coherence (m,n) -cut p is non-multi

proof end;

registration

let p be Graph-yielding non-Dmulti FinSequence;

let n be Nat;

coherence

p | n is non-Dmulti

p /^ n is non-Dmulti

coherence

smid (p,m,n) is non-Dmulti

(m,n) -cut p is non-Dmulti

end;
let n be Nat;

coherence

p | n is non-Dmulti

proof end;

coherence p /^ n is non-Dmulti

proof end;

let m be Nat;coherence

smid (p,m,n) is non-Dmulti

proof end;

coherence (m,n) -cut p is non-Dmulti

proof end;

registration

let p be Graph-yielding simple FinSequence;

let n be Nat;

coherence

p | n is simple ;

coherence

p /^ n is simple ;

let m be Nat;

coherence

smid (p,m,n) is simple ;

coherence

(m,n) -cut p is simple ;

end;
let n be Nat;

coherence

p | n is simple ;

coherence

p /^ n is simple ;

let m be Nat;

coherence

smid (p,m,n) is simple ;

coherence

(m,n) -cut p is simple ;

registration

let p be Graph-yielding Dsimple FinSequence;

let n be Nat;

coherence

p | n is Dsimple ;

coherence

p /^ n is Dsimple ;

let m be Nat;

coherence

smid (p,m,n) is Dsimple ;

coherence

(m,n) -cut p is Dsimple ;

end;
let n be Nat;

coherence

p | n is Dsimple ;

coherence

p /^ n is Dsimple ;

let m be Nat;

coherence

smid (p,m,n) is Dsimple ;

coherence

(m,n) -cut p is Dsimple ;

registration

let p be Graph-yielding connected FinSequence;

let n be Nat;

coherence

p | n is connected

p /^ n is connected

coherence

smid (p,m,n) is connected

(m,n) -cut p is connected

end;
let n be Nat;

coherence

p | n is connected

proof end;

coherence p /^ n is connected

proof end;

let m be Nat;coherence

smid (p,m,n) is connected

proof end;

coherence (m,n) -cut p is connected

proof end;

registration

let p be Graph-yielding acyclic FinSequence;

let n be Nat;

coherence

p | n is acyclic

p /^ n is acyclic

coherence

smid (p,m,n) is acyclic

(m,n) -cut p is acyclic

end;
let n be Nat;

coherence

p | n is acyclic

proof end;

coherence p /^ n is acyclic

proof end;

let m be Nat;coherence

smid (p,m,n) is acyclic

proof end;

coherence (m,n) -cut p is acyclic

proof end;

registration

let p be Graph-yielding Tree-like FinSequence;

let n be Nat;

coherence

p | n is Tree-like ;

coherence

p /^ n is Tree-like ;

let m be Nat;

coherence

smid (p,m,n) is Tree-like ;

coherence

(m,n) -cut p is Tree-like ;

end;
let n be Nat;

coherence

p | n is Tree-like ;

coherence

p /^ n is Tree-like ;

let m be Nat;

coherence

smid (p,m,n) is Tree-like ;

coherence

(m,n) -cut p is Tree-like ;

registration

let p be Graph-yielding edgeless FinSequence;

let n be Nat;

coherence

p | n is edgeless

p /^ n is edgeless

coherence

smid (p,m,n) is edgeless

(m,n) -cut p is edgeless

end;
let n be Nat;

coherence

p | n is edgeless

proof end;

coherence p /^ n is edgeless

proof end;

let m be Nat;coherence

smid (p,m,n) is edgeless

proof end;

coherence (m,n) -cut p is edgeless

proof end;

registration

let p, q be Graph-yielding FinSequence;

coherence

p ^ q is Graph-yielding

p ^' q is Graph-yielding

end;
coherence

p ^ q is Graph-yielding

proof end;

coherence p ^' q is Graph-yielding

proof end;

registration

let p, q be Graph-yielding finite FinSequence;

coherence

p ^ q is finite

p ^' q is finite

end;
coherence

p ^ q is finite

proof end;

coherence p ^' q is finite

proof end;

registration

let p, q be Graph-yielding loopless FinSequence;

coherence

p ^ q is loopless

p ^' q is loopless

end;
coherence

p ^ q is loopless

proof end;

coherence p ^' q is loopless

proof end;

registration

let p, q be Graph-yielding trivial FinSequence;

coherence

p ^ q is trivial

p ^' q is trivial

end;
coherence

p ^ q is trivial

proof end;

coherence p ^' q is trivial

proof end;

registration

let p, q be Graph-yielding non-trivial FinSequence;

coherence

p ^ q is non-trivial

p ^' q is non-trivial

end;
coherence

p ^ q is non-trivial

proof end;

coherence p ^' q is non-trivial

proof end;

registration

let p, q be Graph-yielding non-multi FinSequence;

coherence

p ^ q is non-multi

p ^' q is non-multi

end;
coherence

p ^ q is non-multi

proof end;

coherence p ^' q is non-multi

proof end;

registration

let p, q be Graph-yielding non-Dmulti FinSequence;

coherence

p ^ q is non-Dmulti

p ^' q is non-Dmulti

end;
coherence

p ^ q is non-Dmulti

proof end;

coherence p ^' q is non-Dmulti

proof end;

registration

let p, q be Graph-yielding simple FinSequence;

coherence

p ^ q is simple ;

coherence

p ^' q is simple ;

end;
coherence

p ^ q is simple ;

coherence

p ^' q is simple ;

registration

let p, q be Graph-yielding Dsimple FinSequence;

coherence

p ^ q is Dsimple ;

coherence

p ^' q is Dsimple ;

end;
coherence

p ^ q is Dsimple ;

coherence

p ^' q is Dsimple ;

registration

let p, q be Graph-yielding connected FinSequence;

coherence

p ^ q is connected

p ^' q is connected

end;
coherence

p ^ q is connected

proof end;

coherence p ^' q is connected

proof end;

registration

let p, q be Graph-yielding acyclic FinSequence;

coherence

p ^ q is acyclic

p ^' q is acyclic

end;
coherence

p ^ q is acyclic

proof end;

coherence p ^' q is acyclic

proof end;

registration

let p, q be Graph-yielding Tree-like FinSequence;

coherence

p ^ q is Tree-like ;

coherence

p ^' q is Tree-like ;

end;
coherence

p ^ q is Tree-like ;

coherence

p ^' q is Tree-like ;

registration

let p, q be Graph-yielding edgeless FinSequence;

coherence

p ^ q is edgeless

p ^' q is edgeless

end;
coherence

p ^ q is edgeless

proof end;

coherence p ^' q is edgeless

proof end;

registration

let G1, G2 be _Graph;

coherence

<*G1,G2*> is Graph-yielding

coherence

<*G1,G2,G3*> is Graph-yielding

end;
coherence

<*G1,G2*> is Graph-yielding

proof end;

let G3 be _Graph;coherence

<*G1,G2,G3*> is Graph-yielding

proof end;

registration

let G1, G2 be finite _Graph;

coherence

<*G1,G2*> is finite

coherence

<*G1,G2,G3*> is finite

end;
coherence

<*G1,G2*> is finite

proof end;

let G3 be finite _Graph;coherence

<*G1,G2,G3*> is finite

proof end;

registration

let G1, G2 be loopless _Graph;

coherence

<*G1,G2*> is loopless

coherence

<*G1,G2,G3*> is loopless

end;
coherence

<*G1,G2*> is loopless

proof end;

let G3 be loopless _Graph;coherence

<*G1,G2,G3*> is loopless

proof end;

registration

let G1, G2 be trivial _Graph;

coherence

<*G1,G2*> is trivial

coherence

<*G1,G2,G3*> is trivial

end;
coherence

<*G1,G2*> is trivial

proof end;

let G3 be trivial _Graph;coherence

<*G1,G2,G3*> is trivial

proof end;

registration

let G1, G2 be non trivial _Graph;

coherence

<*G1,G2*> is non-trivial

coherence

<*G1,G2,G3*> is non-trivial

end;
coherence

<*G1,G2*> is non-trivial

proof end;

let G3 be non trivial _Graph;coherence

<*G1,G2,G3*> is non-trivial

proof end;

registration

let G1, G2 be non-multi _Graph;

coherence

<*G1,G2*> is non-multi

coherence

<*G1,G2,G3*> is non-multi

end;
coherence

<*G1,G2*> is non-multi

proof end;

let G3 be non-multi _Graph;coherence

<*G1,G2,G3*> is non-multi

proof end;

registration

let G1, G2 be non-Dmulti _Graph;

coherence

<*G1,G2*> is non-Dmulti

coherence

<*G1,G2,G3*> is non-Dmulti

end;
coherence

<*G1,G2*> is non-Dmulti

proof end;

let G3 be non-Dmulti _Graph;coherence

<*G1,G2,G3*> is non-Dmulti

proof end;

registration

let G1, G2 be simple _Graph;

coherence

<*G1,G2*> is simple ;

let G3 be simple _Graph;

coherence

<*G1,G2,G3*> is simple ;

end;
coherence

<*G1,G2*> is simple ;

let G3 be simple _Graph;

coherence

<*G1,G2,G3*> is simple ;

registration

let G1, G2 be Dsimple _Graph;

coherence

<*G1,G2*> is Dsimple ;

let G3 be Dsimple _Graph;

coherence

<*G1,G2,G3*> is Dsimple ;

end;
coherence

<*G1,G2*> is Dsimple ;

let G3 be Dsimple _Graph;

coherence

<*G1,G2,G3*> is Dsimple ;

registration

let G1, G2 be connected _Graph;

coherence

<*G1,G2*> is connected

coherence

<*G1,G2,G3*> is connected

end;
coherence

<*G1,G2*> is connected

proof end;

let G3 be connected _Graph;coherence

<*G1,G2,G3*> is connected

proof end;

registration

let G1, G2 be acyclic _Graph;

coherence

<*G1,G2*> is acyclic

coherence

<*G1,G2,G3*> is acyclic

end;
coherence

<*G1,G2*> is acyclic

proof end;

let G3 be acyclic _Graph;coherence

<*G1,G2,G3*> is acyclic

proof end;

registration

let G1, G2 be Tree-like _Graph;

coherence

<*G1,G2*> is Tree-like ;

let G3 be Tree-like _Graph;

coherence

<*G1,G2,G3*> is Tree-like ;

end;
coherence

<*G1,G2*> is Tree-like ;

let G3 be Tree-like _Graph;

coherence

<*G1,G2,G3*> is Tree-like ;

registration

let G1, G2 be edgeless _Graph;

coherence

<*G1,G2*> is edgeless

coherence

<*G1,G2,G3*> is edgeless

end;
coherence

<*G1,G2*> is edgeless

proof end;

let G3 be edgeless _Graph;coherence

<*G1,G2,G3*> is edgeless

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

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

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

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

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

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

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

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

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

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

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

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

( 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_{1}[ finite _Graph] } :

provided

FinGraphs{ P

provided

A1:
for G being trivial edgeless _Graph holds P_{1}[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_{1}[G2] holds

P_{1}[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_{1}[G2] holds

P_{1}[G1]

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

P

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

P

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

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

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

( 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_{1}[ finite _Graph] } :

provided

FinTrees{ P

provided

A1:
for G being trivial edgeless _Graph holds P_{1}[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_{1}[G2] holds

( ( for G1 being addAdjVertex of G2,v,e,w holds P_{1}[G1] ) & ( for G1 being addAdjVertex of G2,w,e,v holds P_{1}[G1] ) )

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

( ( for G1 being addAdjVertex of G2,v,e,w holds P

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

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

( 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_{1}[ finite _Graph] } :

provided

FinConnectedGraphs{ P

provided

A1:
for G being trivial edgeless _Graph holds P_{1}[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_{1}[G2] holds

( ( for G1 being addAdjVertex of G2,v,e,w holds P_{1}[G1] ) & ( for G1 being addAdjVertex of G2,w,e,v holds P_{1}[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_{1}[G2] holds

P_{1}[G1]

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

( ( for G1 being addAdjVertex of G2,v,e,w holds P

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

P

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

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

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

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

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

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

( 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_{1}[ finite _Graph] } :

provided

FinSimpleGraphs{ P

provided

A1:
for G being trivial edgeless _Graph holds P_{1}[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_{1}[G2] holds

P_{1}[G1]

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

P

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

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

( 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_{1}[ finite _Graph] } :

provided

FinSimpleConnectedGraphs{ P

provided

A1:
for G being trivial edgeless _Graph holds P_{1}[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_{1}[G2] holds

P_{1}[G1]

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

P

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 )

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;