:: About Supergraphs, {P}art {III}
::  by Sebastian Koch
::
:: Received May 27, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI,
      ORDINAL4, ARYTM_3, CARD_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PBOOLE,
      FINSET_1, ZFMISC_1, RELAT_2, GLIB_002, FUNCOP_1, TREES_1, GLIB_001,
      FUNCT_4, ABIAN, REWRITE1, CHORD, HELLY, FINSEQ_8, GRAPH_1, RFINSEQ,
      XCMPLX_0, CARD_2, GRAPH_2, GLIB_006, GLIB_007, SCMYCIEL, GLIB_003,
      EQREL_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, EQREL_1, FUNCT_1,
      ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3,
      FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XXREAL_0,
      XREAL_0, NAT_1, INT_1, VALUED_0, NAT_D, CARD_2, FINSEQ_1, RVSUM_1,
      RFINSEQ, FUNCT_7, ABIAN, FINSEQ_6, GLIB_000, FINSEQ_8, GRAPH_2, GRAPH_5,
      GLIB_001, GLIB_002, HELLY, GLIB_003, CHORD, GLIB_006, GLIB_007;
 constructors DOMAIN_1, BINOP_1, BINOP_2, FINSOP_1, RVSUM_1, FINSEQ_5, GRAPH_5,
      ABIAN, WELLORD2, FUNCT_2, FIB_NUM2, FINSEQ_8, GLIB_001, GLIB_002, HELLY,
      RELSET_1, FUNCT_3, CHORD, NAT_D, GRAPH_2, RFINSEQ, FINSEQ_6, CARD_2,
      FUNCT_7, FINSEQ_1, SUBSET_1, GLIB_006, GLIB_007, RELAT_1, GLIB_003,
      EQREL_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, ABIAN,
      XREAL_0, NAT_1, MEMBERED, FINSEQ_1, GLIB_000, GLIB_001, HELLY, GLIB_002,
      CARD_1, RELSET_1, SUBSET_1, GLIB_006, GLIB_007, GLIB_003, MSAFREE5,
      JORDAN1J, EQREL_1;
 requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;


begin

::: START into GLIB_000 ?

registration
  let G be _Graph, v be Vertex of G;
  cluster -> _trivial for inducedSubgraph of G, {v};
end;

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

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

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

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

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

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

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

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

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

:: converse of GLIB_000:21
theorem :: GLIB_008:10
  for G being _Graph holds (ex v1, v2 being Vertex of G st v1 <> v2)
    implies G is non _trivial;

registration
  let G be non _trivial _Graph, X be set;
  cluster -> non _trivial for removeEdges of G, X;
end;

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

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

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

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

theorem :: GLIB_008:15
  for G being _Graph holds G is non _trivial iff
    ex H being Subgraph of G st H is non spanning;

theorem :: GLIB_008:16
  for G being _Graph
  holds (ex v being Vertex of G st v is endvertex) implies G is non _trivial;

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

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

registration
  let G be _finite connected _Graph;
  cluster spanning Tree-like connected acyclic for Subgraph of G;
end;

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

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

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

registration
  let G be non _trivial _Graph;
  cluster non spanning _trivial connected for Subgraph of G;
end;

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

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

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

:: 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 :: GLIB_008:25
  for G1 being _Graph, v0, v1 being Vertex of G1
  for G2 being removeVertex of G1,v0, v2 being Vertex of G2
  st v0 is endvertex & v1 = v2 & v1 in G1.reachableFrom(v0)
  holds G2.reachableFrom(v2) = G1.reachableFrom(v1) \ {v0};

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

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

registration
  let G be non _trivial connected _Graph, v be Vertex of G;
  cluster v.allNeighbors() -> non empty;
end;

:: END into GLIB_002 ?

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

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

:: into HELLY ?
theorem :: GLIB_008:30
  for T being non _trivial _finite _Tree, 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();

:: into HELLY ?
theorem :: GLIB_008:31
  for G1 being non _trivial _finite 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;

:: START into GLIB_006 ?

theorem :: GLIB_008:32
  for G2, G3 being _Graph, V being set, G1 being addVertices of G2, V
  st G2 == G3 holds G1 is addVertices of G3, V;

theorem :: GLIB_008:33
  for G2 being _Graph, 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;

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

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

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

theorem :: GLIB_008:37
  for G1 being _Graph, e being set, 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;

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

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

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

:: v1 and v2 are connected in supergraph
theorem :: GLIB_008:41
  for G2 being _Graph, v1,v2 being Vertex of G2, 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);

:: their components are connected as well
theorem :: GLIB_008:42
  for G2 being _Graph, v1,v2 being Vertex of G2, 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);

:: the other components stay unaffected
theorem :: GLIB_008:43
  for G2 being _Graph, v1,v2 being Vertex of G2, e being object
  for G1 being addEdge of G2,v1,e,v2
  for w being Vertex of G1, 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);

:: composition of component set in graph with added edge
theorem :: GLIB_008:44
  for G2 being _Graph, v1,v2 being Vertex of G2, 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)};

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

registration
  let G be _Graph;
  cluster endvertex -> non cut-vertex for Vertex of G;
end;

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

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

begin :: Edgeless and non edgeless graphs

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

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

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

registration
  let G be _Graph;
  cluster -> edgeless for removeEdges of G, the_Edges_of G;
end;

registration
  cluster edgeless for _Graph;
  let G be _Graph;
  cluster edgeless spanning for Subgraph of G;
  cluster edgeless _trivial for Subgraph of G;
end;

registration
  let G be edgeless _Graph;
  cluster the_Edges_of G -> empty;
end;

registration
  cluster edgeless -> non-multi non-Dmulti loopless simple Dsimple for _Graph;
  cluster _trivial loopless -> edgeless for _Graph;
  let V be non empty set, S,T be Function of {},V;
  cluster createGraph(V,{},S,T) -> edgeless;
end;

theorem :: GLIB_008:50
  for G being edgeless_Graph, e,v1,v2 being object
  holds not e Joins v1,v2,G & not e DJoins v1,v2,G;

theorem :: GLIB_008:51
  for G being edgeless_Graph, e being object, X, Y being set
  holds not e SJoins X,Y,G & not e DSJoins X,Y,G;

theorem :: GLIB_008:52
  for G1, G2 being _Graph st G1 == G2
  holds G1 is edgeless implies G2 is edgeless;

registration
  let G be edgeless _Graph;
  cluster -> trivial for Walk of G;
  cluster -> edgeless for Subgraph of G;
  let X be set;
  cluster G.edgesInto(X) -> empty;
  cluster G.edgesOutOf(X) -> empty;
  cluster G.edgesInOut(X) -> empty;
  cluster G.edgesBetween(X) -> empty;
  cluster G.set(WeightSelector, X) -> edgeless;
  cluster G.set(ELabelSelector, X) -> edgeless;
  cluster G.set(VLabelSelector, X) -> edgeless;
  cluster -> edgeless for addVertices of G, X;
  cluster -> edgeless for reverseEdgeDirections of G, X;
  let Y be set;
  cluster G.edgesBetween(X,Y) -> empty;
  cluster G.edgesDBetween(X,Y) -> empty;
end;

registration
  cluster edgeless -> acyclic chordal for _Graph;
  cluster _trivial edgeless -> Tree-like for _Graph;
  cluster non _trivial edgeless -> non connected non Tree-like non complete
    for _Graph;
  cluster connected edgeless -> _trivial for _Graph;
end;

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

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

theorem :: GLIB_008:55
  for G2 being _Graph, v1 being Vertex of G2, 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 G1 is non edgeless;

theorem :: GLIB_008:56
  for G2 being _Graph, v1, e being object, 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 G1 is non edgeless;

theorem :: GLIB_008:57
  for G2 being _Graph, 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 G1 is non edgeless;

registration
  let G be _Graph;
  cluster -> non edgeless for addAdjVertexToAll of G, the_Vertices_of G;
  cluster -> non edgeless for addAdjVertexFromAll of G, the_Vertices_of G;
  cluster -> non edgeless for addAdjVertexAll of G, the_Vertices_of G;
  let v be Vertex of G;
  cluster -> non edgeless for
    addAdjVertex of G, v, the_Edges_of G, the_Vertices_of G;
  cluster -> non edgeless for
    addAdjVertex of G, the_Vertices_of G, the_Edges_of G, v;
  let w be Vertex of G;
  cluster -> non edgeless for addEdge of G, v, the_Edges_of G, w;
end;

registration
  let G be edgeless _Graph;
  cluster -> _trivial for Component of G;
  let v be Vertex of G;
  cluster v.edgesIn() -> empty;
  cluster v.edgesOut() -> empty;
  cluster v.edgesInOut() -> empty;
end;

registration
  let G be edgeless _Graph;
  cluster -> isolated non cut-vertex non endvertex for Vertex of G;
  let v be Vertex of G;
  cluster v.inDegree() -> empty;
  cluster v.outDegree() -> empty;
  cluster v.inNeighbors() -> empty;
  cluster v.outNeighbors() -> empty;
end;

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

registration
  cluster _trivial _finite edgeless for _Graph;
  cluster non _trivial _finite edgeless for _Graph;
  cluster _trivial _finite non edgeless for _Graph;
  cluster non _trivial _finite non edgeless for _Graph;
end;

registration
  let G be non edgeless _Graph;
  cluster the_Edges_of G -> non empty;
  cluster -> non edgeless for Supergraph of G;
  let X be set;
  cluster -> non edgeless for reverseEdgeDirections of G, X;
  cluster G.set(WeightSelector, X) -> non edgeless;
  cluster G.set(ELabelSelector, X) -> non edgeless;
  cluster G.set(VLabelSelector, X) -> non edgeless;
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, G2 being Subgraph of G1
  st G1.order() = G2.order() holds G1 == G2;

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

definition
  let GF be non empty Graph-yielding Function;
  redefine attr GF is edgeless means
:: GLIB_008:def 3

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

definition
  let GSq be GraphSeq;
  redefine attr GSq is edgeless means
:: GLIB_008:def 4
  for n being Nat holds GSq.n is edgeless;
end;

registration
  cluster _trivial loopless -> edgeless for Graph-yielding Function;
  cluster edgeless -> non-multi non-Dmulti loopless simple Dsimple acyclic
    for Graph-yielding Function;
end;

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

registration
  let GSq be edgeless GraphSeq, x be Nat;
  cluster GSq.x -> edgeless;
end;

begin :: Finite Graph sequences

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

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

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

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

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

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

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

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

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

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

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

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

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

registration
  cluster empty Graph-yielding for FinSequence;
  cluster non empty Graph-yielding for FinSequence;
end;

registration
  let p be non empty Graph-yielding FinSequence;
  cluster p.1 -> Function-like Relation-like;
  cluster p.len p -> Function-like Relation-like;
end;

registration
  let p be non empty Graph-yielding FinSequence;
  cluster p.1 -> finite NAT-defined;
  cluster p.len p -> finite NAT-defined;
end;

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

registration
  cluster non empty _finite loopless _trivial non-multi non-Dmulti simple
    Dsimple
    connected acyclic Tree-like edgeless for Graph-yielding FinSequence;
  cluster non empty _finite loopless non-trivial non-multi non-Dmulti simple
    Dsimple connected acyclic Tree-like for Graph-yielding FinSequence;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

begin :: Construction of finite Graphs

:: finite addition of vertices can be finitely constructed with addVertex only
theorem :: GLIB_008:59
  for G2 being _Graph, V being finite set, 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;

theorem :: GLIB_008:60
  for G being _finite _Graph, H being Subgraph of G st G.size() = H.size()
  ex p being non empty _finite Graph-yielding 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;

theorem :: GLIB_008:61
  for G being _finite edgeless _Graph, H being Subgraph of G
  ex p being non empty _finite edgeless Graph-yielding 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;

:: finite edgeless graphs can be finitely constructed with addVertex only
theorem :: GLIB_008:62
  for G being _finite edgeless _Graph
  ex p being non empty _finite edgeless Graph-yielding FinSequence
  st p.1 is _trivial 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;

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

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;

theorem :: GLIB_008:64
  for G being _finite _Graph, H being spanning Subgraph of G
  ex p being non empty _finite Graph-yielding 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, 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;

theorem :: GLIB_008:65
  for G being _finite _Graph
  ex p being non empty _finite Graph-yielding 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, 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;

theorem :: GLIB_008:66
  for G being _finite connected _Graph,
      H being spanning connected Subgraph of G
  ex p being non empty _finite connected Graph-yielding 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, 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;

theorem :: GLIB_008:67
  for G1 being _finite _Graph, H being Subgraph of G1
  ex G2 being spanning Subgraph of G1,
    p being non empty _finite Graph-yielding 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;

theorem :: GLIB_008:68
  for G being _finite _Graph, H being Subgraph of G
  ex p being non empty _finite Graph-yielding 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 st n <= len p - 1 holds
    (ex v1,v2 being Vertex of G, 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);

:: finite graphs can be finitely constructed with addVertex and addEdge only
theorem :: GLIB_008:69
  for G being _finite _Graph
  ex p being non empty _finite Graph-yielding FinSequence
  st p.1 is _trivial edgeless & p.len p = G & len p = G.order() + G.size() &
    for n being Element of dom p st n <= len p - 1 holds
    (ex v1,v2 being Vertex of G, 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);

scheme :: GLIB_008:sch 2
  FinGraphs { P[_finite _Graph] } : for G being _finite _Graph holds P[G]
provided
   for G being _trivial edgeless _Graph holds P[G] and
   for G2 being _finite _Graph, v being object
    for G1 being addVertex of G2,v
    st not v in the_Vertices_of G2 & P[G2] holds P[G1] and
   for G2 being _finite _Graph, v1, v2 being Vertex of G2, 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];

theorem :: GLIB_008:70
  for p being non empty Graph-yielding FinSequence
  st p.1 is _finite &
    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) 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;

theorem :: GLIB_008:71
  for G being _finite Tree-like _Graph, H being connected Subgraph of G
  ex p being non empty _finite Tree-like Graph-yielding 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
    ex v1,v2 being Vertex of G, 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));

:: finite trees can be finitely constructed with addAdjVertex only
theorem :: GLIB_008:72
  for G being _finite Tree-like _Graph
  ex p being non empty _finite Tree-like Graph-yielding FinSequence
  st p.1 is _trivial edgeless & p.len p = G & len p = G.order() &
    for n being Element of dom p st n <= len p - 1
    ex v1,v2 being Vertex of G, 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));

scheme :: GLIB_008:sch 3
  FinTrees { P[_finite _Graph] } :
    for G being _finite Tree-like _Graph holds P[G]
provided
   for G being _trivial edgeless _Graph holds P[G] and
   for G2 being _finite Tree-like _Graph
    for v being Vertex of G2, 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]);

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

:: finite connected graphs can be constructed with addAdjVertex and addEdge
theorem :: GLIB_008:74
  for G being _finite connected _Graph
  ex p being non empty _finite connected Graph-yielding FinSequence
  st p.1 is _trivial 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, 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, 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);

scheme :: GLIB_008:sch 4
  FinConnectedGraphs { P[_finite _Graph] } :
    for G being _finite connected _Graph holds P[G]
provided
   for G being _trivial edgeless _Graph holds P[G] and
   for G2 being _finite connected _Graph
    for v being Vertex of G2, 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
   for G2 being _finite connected _Graph
    for v1,v2 being Vertex of G2, 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];

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

theorem :: GLIB_008:76
  for G2 being _Graph, v being object
  for V1 being set, 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
  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, 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);

theorem :: GLIB_008:77
  for G2 being _Graph, v being object
  for V being finite set, G1 being addAdjVertexAll of G2, v, V
  st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
  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, 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);

theorem :: GLIB_008:78
  for G2 being _Graph, v being object
  for V being non empty finite set, G1 being addAdjVertexAll of G2, v, V
  st V c= the_Vertices_of G2 & not v in the_Vertices_of G2
  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, 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, 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);

theorem :: GLIB_008:79
  for G being _finite simple _Graph
  for W being set, H being inducedSubgraph of G, W
  ex p being non empty _finite simple Graph-yielding 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
    ex v being object, 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;

theorem :: GLIB_008:80
  for G being _finite simple _Graph
  ex p being non empty _finite simple Graph-yielding FinSequence
  st p.1 is _trivial edgeless & p.len p = G & len p = G.order() &
    for n being Element of dom p st n <= len p - 1
    ex v being object, 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;

scheme :: GLIB_008:sch 5
  FinSimpleGraphs { P[_finite _Graph] } :
    for G being _finite simple _Graph holds P[G]
provided
   for G being _trivial edgeless _Graph holds P[G] and
   for G2 being _finite simple _Graph, v being object, 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];

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
    ex v being object, V being set st p.(n+1) is addAdjVertexAll of p.n,v,V
  holds p.len p is simple;

theorem :: GLIB_008:82
  for G being _finite simple connected _Graph
  ex p being non empty _finite simple connected Graph-yielding FinSequence
  st p.1 is _trivial edgeless & p.len p = G & len p = G.order() &
    for n being Element of dom p st n <= len p - 1
    ex v being object, 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;

scheme :: GLIB_008:sch 6
  FinSimpleConnectedGraphs { P[_finite _Graph] } :
    for G being _finite simple connected _Graph holds P[G]
provided
   for G being _trivial edgeless _Graph holds P[G] and
   for G2 being _finite simple connected _Graph
    for v being object, 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];

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