:: Miscellaneous Graph Preliminaries, {I}
::  by Sebastian Koch
:: 
:: Received March 30, 2021
:: Copyright (c) 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, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1, FINSEQ_1,
      NAT_1, FUNCT_4, FUNCOP_1, ZFMISC_1, CARD_1, ARYTM_3, CARD_2, ORDINAL2,
      XXREAL_0, PBOOLE, GLIB_000, RING_3, GLIB_002, PARTFUN1, FUNCT_2, CHORD,
      SCMYCIEL, REWRITE1, ARYTM_1, GLIB_006, GLIB_007, GLIB_009, GLIB_010,
      GLIB_012, WAYBEL_0, MOD_4, RELAT_2, GRAPH_1, GLIB_001, ABIAN, SGRAPH1,
      TREES_1, MSUALG_6, EQREL_1, GLIB_013, GLIB_014, RCOMP_1, MSAFREE2,
      FUNCT_7, HELLY, INT_1, TAXONOM2, CARD_3, AOFA_I00;
 notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1,
      RELAT_1, FUNCT_1, RELAT_2, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2,
      BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, CARD_1, PBOOLE, ORDERS_1,
      CARD_3, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, NAT_1, INT_1, VALUED_0,
      NAT_D, CARD_2, FINSEQ_1, EQREL_1, NEWTON, ABIAN, FINSEQ_6, GLIB_000,
      FINSEQ_8, GRAPH_2, TAXONOM2, COMPUT_1, GLIB_001, GLIB_002, CHORD, HELLY,
      AOFA_I00, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIB_011,
      GLIBPRE0, GLIB_012, GLIB_013, GLIB_014, GLUNIR00;
 constructors DOMAIN_1, FUNCT_4, NAT_1, NAT_D, BINOP_2, CARD_2, FINSEQ_4,
      PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, SQUARE_1, GLIB_000,
      NEWTON, XTUPLE_0, CHORD, GLIB_002, GLIB_006, GLIB_007, GLIB_008,
      GLIB_009, GLIB_010, GLIB_011, GLIB_001, ABIAN, BINOP_1, FINSOP_1,
      RVSUM_1, FINSEQ_5, GRAPH_5, FUNCT_2, FIB_NUM2, FINSEQ_8, HELLY, FUNCT_3,
      GRAPH_2, FINSEQ_6, FUNCT_7, FINSEQ_1, SUBSET_1, RELAT_1, ENUMSET1,
      ORDINAL1, INT_1, XXREAL_0, XREAL_0, XCMPLX_0, GLIB_012, PARTFUN2,
      ORDERS_1, TOLER_1, TAXONOM2, SETFAM_1, COMPUT_1, EQREL_1, GLIBPRE0,
      GLIB_013, GLIB_014, GLUNIR00, WELLORD1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      FINSET_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, FINSEQ_4, FUNCT_2, PARTFUN1,
      RELSET_1, GLIB_000, CHORD, GLIB_002, GLIB_006, GLIB_007, GLIB_009,
      GLIB_008, GLIB_010, GLIB_011, SQUARE_1, NEWTON, XTUPLE_0, ABIAN,
      GLIB_001, NUMBERS, MEMBERED, INT_1, CARD_3, RFINSEQ, GRAPH_2, GLIB_012,
      SETFAM_1, COMPUT_1, ZFMISC_1, OPOSET_1, RELAT_2, GLIBPRE0, GLIB_013,
      GLIB_014, ORDERS_1, ORDINAL5, EQREL_1, MSAFREE5, PRE_POLY;
 requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;


begin :: Preliminaries not directly related to graphs

:: Proof mostly copied from XREGULAR:10
:: into XREGULAR ?
theorem :: GLIBPRE1:1
  for X1, X2, X3, X4, X5, X6, X7 being set
  holds not (X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X7 &
    X7 in X1);

:: Proof mostly copied from XREGULAR:10
:: into XREGULAR ?
theorem :: GLIBPRE1:2
  for X1, X2, X3, X4, X5, X6, X7, X8 being set
  holds not (X1 in X2 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X7 &
    X7 in X8 & X8 in X1);

:: into FUNCT_1 ?
registration
  cluster one-to-one constant -> trivial for Function;
end;

:: into FUNCT_1 ?
theorem :: GLIBPRE1:3
  for f being Function
  holds f is non empty constant iff ex y being object st rng f = {y};

:: into PBOOLE ?
registration
  let X be set;
  cluster one-to-one for ManySortedSet of X;
end;

:: into PBOOLE ?
registration
  let X be set;
  cluster total one-to-one for X-defined Function;
end;

:: into PBOOLE ?
registration
  let X be non empty set;
  cluster total one-to-one non empty for X-defined Function;
end;

:: this is a variant of FUNCT_2:sch 4 which can be used a little bit easier
:: into FUNCT_2 ?
scheme :: GLIBPRE1:sch 1
  LambdaDf {C, D() -> non empty set, F(Element of C()) -> object} :
    ex f being Function of C(),D() st
      for x being Element of C() holds f.x=F(x)
provided
   for x being Element of C() holds F(x) in D();

:: into FUNCOP_1 ?
theorem :: GLIBPRE1:4
  for f being one-to-one Function, y being object st rng f = {y}
  ex x being object st f = x .--> y;

:: into FUNCOP_1 ?
registration
  let f be one-to-one Function;
  cluster f~ -> one-to-one;
end;

:: into FUNCT_3 or FUNCOP_1 ?
registration
  let f be Function, g be one-to-one Function;
  cluster <: f,g :> -> one-to-one;
  cluster <: g,f :> -> one-to-one;
end;

:: into FUNCT_3 or FUNCOP_1 ?
theorem :: GLIBPRE1:5
  for f being empty Function holds .:f = {} .--> {};

:: into FUNCT_3 ?
registration
  let f be one-to-one Function;
  cluster .:f -> one-to-one;
end;

:: into FUNCT_3 ?
theorem :: GLIBPRE1:6
  for f being non empty one-to-one Function
  for X being non empty Subset of bool dom f
  holds rng((.:f)|X) = the set of all f.:x where x is Element of X;

:: into FUNCT_4 ?
theorem :: GLIBPRE1:7
  for f being Function, g, h being one-to-one Function
  st h = f +* g holds h"|rng g = g";

:: special case of FUNCT_7:10, compare FUNCT_7:9, FUNCT_7:11
:: into FUNCT_4 ?
theorem :: GLIBPRE1:8
  for f, g, h being Function st rng f c= dom h holds (g +* h)*f = h*f;

:: into FUNCT_4 ?
theorem :: GLIBPRE1:9
  for f being Function, g being one-to-one Function
  holds (f +* g)*(g") = id rng g;

:: into RELAT_2 or ORDERS_1 ?
registration
  cluster reflexive connected -> strongly_connected for Relation;
end;

:: into RELSET_1 or ORDERS_1 ?
theorem :: GLIBPRE1:10
  for X being set, R being Relation of X
  holds R is antisymmetric iff R \ id X is asymmetric;

:: into EQREL_1 or TAXONOM2 ?
theorem :: GLIBPRE1:11
  for X being set st X is mutually-disjoint
  holds X \ {{}} is a_partition of union X;

:: into EQREL_1 or TAXONOM2 ?
registration
  let X be set;
  cluster -> mutually-disjoint for a_partition of X;
end;

:: compare CARD_2:86, Proof mostly copied from there
:: into CARD_2 ?
theorem :: GLIBPRE1:12
  for M,N being Cardinal, f being Function holds
    (M c= card dom f & for x being object st x in dom f
      holds N c= card (f.x)) implies M*`N c= Sum Card f;

:: into CARD_3 ?
theorem :: GLIBPRE1:13
  for X, x being set st x in X holds (disjoin Card id X).x = [: card x, {x} :];

:: into CARD_3 or TAXONOM2 ?
theorem :: GLIBPRE1:14
  for X being set st X is mutually-disjoint holds Sum Card id X = card union X;

:: compare CARD_2:87, Proof mostly copied from there
:: into CARD_2 ?
theorem :: GLIBPRE1:15
  for X being set, M, N being Cardinal st X is mutually-disjoint &
    M c= card X & for Y being set st Y in X holds N c= card Y
  holds M*`N c= card union X;

:: into COMPUT_1 ?
theorem :: GLIBPRE1:16
  for F being compatible functional set
  st (for f1 being Function st f1 in F holds f1 is one-to-one &
    for f2 being Function st f2 in F & f1 <> f2 holds rng f1 misses rng f2)
  holds union F is one-to-one;

begin :: into GLIB_000

registration
  let G be non _trivial _Graph;
  cluster non empty proper for Subset of the_Vertices_of G;
end;

theorem :: GLIBPRE1:17
  for G being _Graph, X being set holds G.edgesBetween(X,X) = G.edgesBetween(X)
;

theorem :: GLIBPRE1:18
  for G being _Graph holds G is _trivial iff the_Vertices_of G is trivial;

theorem :: GLIBPRE1:19
  for G1 being _Graph, G2 being Subgraph of G1
  holds G2 is inducedSubgraph of G1, the_Vertices_of G2, the_Edges_of G2;

theorem :: GLIBPRE1:20
  for G1, G2 being _Graph, G3 being spanning Subgraph of G1
  st G2 == G3 holds G2 is spanning Subgraph of G1;

theorem :: GLIBPRE1:21
  for G being _Graph, e being object st e in the_Edges_of G
  holds e in G.edgesBetween({(the_Source_of G).e,(the_Target_of G).e});

theorem :: GLIBPRE1:22
  for G being _Graph holds G == createGraph(the_Vertices_of G, the_Edges_of G,
    the_Source_of G, the_Target_of G);

:: generalization of GLIB_000:def 52
theorem :: GLIBPRE1:23
  for G being _Graph, v being Vertex of G
  holds v is endvertex iff v.degree() = 1;

theorem :: GLIBPRE1:24
  for G being loopless _Graph, v being Vertex of G holds
    v.inNeighbors() c= the_Vertices_of G \ {v} &
    v.outNeighbors() c= the_Vertices_of G \ {v} &
    v.allNeighbors() c= the_Vertices_of G \ {v};

theorem :: GLIBPRE1:25
  for G being _Graph st (for v being Vertex of G holds
    v.inNeighbors() c= the_Vertices_of G \ {v} or
    v.outNeighbors() c= the_Vertices_of G \ {v} or
    v.allNeighbors() c= the_Vertices_of G \ {v})
  holds G is loopless;

:: basic Proof copied from NAT --> G -> Graph-yielding
registration
  let X be set, G be _Graph;
  cluster X --> G -> Graph-yielding;
end;

registration
  let x be object, G be _Graph;
  cluster x .--> G -> Graph-yielding;
end;

registration
  let X be set;
  cluster Graph-yielding for ManySortedSet of X;
end;

registration
  let X be non empty set;
  cluster non empty Graph-yielding for ManySortedSet of X;
end;

definition
  let X be non empty set, f be Graph-yielding ManySortedSet of X;
  let x be Element of X;
  redefine func f.x -> _Graph;
end;

begin

registration
  let G being _Graph, P being Path of G;
  cluster P.vertexSeq() | P.length() -> one-to-one;
end;

:: compare GLIB_001:154
theorem :: GLIBPRE1:26
  for G being _Graph, P being Path of G holds P.length() c= G.order();

:: compare GLIB_001:144
theorem :: GLIBPRE1:27
  for G being _Graph, T being Trail of G holds T.length() c= G.size();

theorem :: GLIBPRE1:28
  for G being _Graph, W being Walk of G st len W = 3 or W.length() = 1
  ex e being object st e Joins W.first(),W.last(),G &
    W = G.walkOf(W.first(),e,W.last());

theorem :: GLIBPRE1:29
  for G being _Graph, W being Walk of G, e being object
  st e in W.edges() & not e in G.loops() & W is Circuit-like
  ex e0 being object st e0 in W.edges() & e0 <> e;

:: compare GLIB_001:149 and CHORD:93
theorem :: GLIBPRE1:30
  for G being _Graph, P being Path of G, n, m being odd Element of NAT
  st n < m & m <= len P & (n <> 1 or m <> len P) holds P.cut(n,m) is open;

:: cutting a closed walk at an edge
theorem :: GLIBPRE1:31
  for G being _Graph, W being closed Walk of G, n being odd Element of NAT
  st n < len W holds
    W.cut(n+2,len W).append(W.cut(1,n)) is_Walk_from W.(n+2),W.n &
    (W is Trail-like implies
      W.cut(n+2,len W).edges() misses W.cut(1,n).edges() &
      W.cut(n+2,len W).append(W.cut(1,n)).edges() = W.edges() \ {W.(n+1)}) &
    (W is Path-like implies
      W.cut(n+2,len W).vertices() /\ W.cut(1,n).vertices() = {W.first()} &
      (not W.(n+1) in G.loops()
        implies W.cut(n+2,len W).append(W.cut(1,n)) is open) &
      W.cut(n+2,len W).append(W.cut(1,n)) is Path-like);

:: extension of GLIB_001:157
theorem :: GLIBPRE1:32
  for G being _Graph, W1 being Walk of G, e,x,y being object
  st e Joins x,y,G & e in W1.edges() & W1 is Cycle-like
  ex W2 being Path of G st W2 is_Walk_from x,y &
    W2.edges() = W1.edges() \ {e} & (not e in G.loops() implies W2 is open);

theorem :: GLIBPRE1:33
  for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
  holds len W1 <= len W2 iff W1.length() <= W2.length();

theorem :: GLIBPRE1:34
  for G being _Graph, W being Walk of G
  holds W.length() = W.reverse().length();

theorem :: GLIBPRE1:35
  for G being _Graph, W being Walk of G, e being object
  st not e in W.last().edgesInOut() holds W.addEdge(e) = W;

theorem :: GLIBPRE1:36
  for G being _Graph, W being Walk of G, e,x being object
  st e Joins W.last(),x,G holds W.addEdge(e).length() = W.length() + 1;

theorem :: GLIBPRE1:37
  for G1 being _Graph, E being set, G2 being removeEdges of G1, E
  for W1 being Walk of G1 st W1.edges() misses E holds W1 is Walk of G2;

begin :: into GLIB_002

theorem :: GLIBPRE1:38
  for G1, G2 being _Graph, G3 being Component of G1 st G2 == G3
  holds G2 is Component of G1;

theorem :: GLIBPRE1:39
  for G1, G2 being _Graph, G3 being Component of G1 st G1 == G2
  holds G3 is Component of G2;

:: or into HELLY
theorem :: GLIBPRE1:40
  for G being Tree-like _Graph, H being spanning Subgraph of G
  st H is connected holds G == H;

registration
  let G be _Graph;
  cluster -> non empty for Element of G.componentSet();
end;

registration
  let G be _Graph;
  cluster G.componentSet() -> mutually-disjoint;
end;

begin :: into CHORD

theorem :: GLIBPRE1:41
  for G being _Graph, v,w being Vertex of G
  holds v,w are_adjacent iff w in v.allNeighbors();

:: the necessary existence clustering is from _008, but should be in _002
theorem :: GLIBPRE1:42
  for G being _Graph, S being set, v being Vertex of G
  st not v in S & S meets G.reachableFrom(v) holds G.AdjacentSet(S) <> {};

:: the necessary existence clustering is from _008, but should be in _002
registration
  let G be non _trivial connected _Graph;
  let S be non empty proper Subset of the_Vertices_of G;
  cluster G.AdjacentSet(S) -> non empty;
end;

theorem :: GLIBPRE1:43
  for G being complete _Graph, v being Vertex of G
  holds the_Vertices_of G \ {v} c= v.allNeighbors();

theorem :: GLIBPRE1:44
  for G being loopless complete _Graph, v being Vertex of G
  holds v.allNeighbors() = the_Vertices_of G \ {v};

theorem :: GLIBPRE1:45
  for G being simple complete _Graph, v being Vertex of G
  holds v.degree()+`1 = G.order();

registration
  let G be _Graph;
  cluster trivial -> minlength for Walk of G;
  cluster minlength Path-like for Walk of G;
end;

registration
  let G be _Graph, W be minlength Walk of G;
  cluster W.reverse() -> minlength;
end;

theorem :: GLIBPRE1:46
  for G1 being _Graph, G2 being Subgraph of G1
  for W1 being Walk of G1, W2 being Walk of G2
  st W1 = W2 & W1 is minlength holds W2 is minlength;

theorem :: GLIBPRE1:47
  for G being _Graph, v being Vertex of G, W being Walk of G
  st W is_Walk_from v,v holds W is minlength iff W = G.walkOf(v);

theorem :: GLIBPRE1:48
  for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
  st G1 == G2 & W1 = W2 & W1 is minlength holds W2 is minlength;

begin :: into GLIB_006

:: other direction of first part of GLIB_000:72 and GLIB_006:70
theorem :: GLIBPRE1:49
  for G1, G2 being _Graph
  st the_Vertices_of G2 c= the_Vertices_of G1 &
    (for e,x,y being object st e DJoins x,y,G2 holds e DJoins x,y,G1)
  holds G2 is Subgraph of G1 & G1 is Supergraph of G2;

theorem :: GLIBPRE1:50
  for G1 being _Graph, G3 being Subgraph of G1, v,e,w being object
  for G2 being addEdge of G3,v,e,w st e DJoins v,w,G1
  holds G2 is Subgraph of G1;

:: adding an edge to a tree makes it unicyclic
theorem :: GLIBPRE1:51
  for G being Tree-like _Graph, v1,v2 being Vertex of G, e being object
  for H being addEdge of G,v1,e,v2 st not e in the_Edges_of G holds
    H is non acyclic & for W1, W2 being Walk of H
      st W1 is Cycle-like & W2 is Cycle-like holds W1.edges() = W2.edges();

:: if adding an edge to a graph makes it unicyclic, it has been a tree before
theorem :: GLIBPRE1:52
  for G being connected _Graph
  st ex v1,v2 being Vertex of G, e being object, H being addEdge of G,v1,e,v2
    st not e in the_Edges_of G & for W1, W2 being Walk of H
      st W1 is Cycle-like & W2 is Cycle-like holds W1.edges() = W2.edges()
  holds G is Tree-like;

theorem :: GLIBPRE1:53
  for G2 being _Graph, v,e,w being object, G1 being addAdjVertex of G2,v,e,w
  holds the_Vertices_of G1 c= the_Vertices_of G2 \/ {v,w} &
    the_Edges_of G1 c= the_Edges_of G2 \/ {e};

theorem :: GLIBPRE1:54
  for G2 being _Graph, v,v2 being Vertex of G2, e,w being object
  for G1 being addAdjVertex of G2,v,e,w, v1 being Vertex of G1
  st v1 = v2 & not v in G2.reachableFrom(v2) &
    not e in the_Edges_of G2 & not w in the_Vertices_of G2
  holds G1.reachableFrom(v1) = G2.reachableFrom(v2);

theorem :: GLIBPRE1:55
  for G2 being _Graph, w,v2 being Vertex of G2, v,e being object
  for G1 being addAdjVertex of G2,v,e,w, v1 being Vertex of G1
  st v1 = v2 & not w in G2.reachableFrom(v2) &
    not e in the_Edges_of G2 & not v in the_Vertices_of G2
  holds G1.reachableFrom(v1) = G2.reachableFrom(v2);

theorem :: GLIBPRE1:56
  for G2 being _Graph, v being Vertex of G2, e,w being object
  for G1 being addAdjVertex of G2,v,e,w, v1 being Vertex of G1
  st v1 = v & not e in the_Edges_of G2 & not w in the_Vertices_of G2
  holds G1.reachableFrom(v1) = G2.reachableFrom(v) \/ {w};

theorem :: GLIBPRE1:57
  for G2 being _Graph, v,e being object, w being Vertex of G2
  for G1 being addAdjVertex of G2,v,e,w, v1 being Vertex of G1
  st v1 = w & not e in the_Edges_of G2 & not v in the_Vertices_of G2
  holds G1.reachableFrom(v1) = G2.reachableFrom(w) \/ {v};

theorem :: GLIBPRE1:58
  for G2 being _Graph, v being Vertex of G2, e,w being object
  for G1 being addAdjVertex of G2,v,e,w
  st not e in the_Edges_of G2 & not w in the_Vertices_of G2
  holds G1.componentSet() =
    G2.componentSet() \ {G2.reachableFrom(v)} \/ {G2.reachableFrom(v) \/ {w}};

theorem :: GLIBPRE1:59
  for G2 being _Graph, v,e being object, w being Vertex of G2
  for G1 being addAdjVertex of G2,v,e,w
  st not e in the_Edges_of G2 & not v in the_Vertices_of G2
  holds G1.componentSet() =
    G2.componentSet() \ {G2.reachableFrom(w)} \/ {G2.reachableFrom(w) \/ {v}};

theorem :: GLIBPRE1:60
  for G2 being _Graph, v,e,w being object, G1 being addAdjVertex of G2,v,e,w
  for W1 being Walk of G1, W2 being Walk of G2
  st W1 = W2 & W2 is minlength holds W1 is minlength;

:: the necessary existence clustering is from _008, but should be in _002
theorem :: GLIBPRE1:61
  for G1 being non _trivial connected _Graph
  for G2 being non spanning Subgraph of G1
  ex v,e,w being object
  st v <> w & e DJoins v,w,G1 & not e in the_Edges_of G2 &
    (for G3 being addAdjVertex of G2,v,e,w holds G3 is Subgraph of G1) &
    ((v in the_Vertices_of G2 & not w in the_Vertices_of G2) or
      (not v in the_Vertices_of G2 & w in the_Vertices_of G2));

theorem :: GLIBPRE1:62
  for G2 being _Graph, v being Vertex of G2, e,w,x being object
  for G1 being addAdjVertex of G2,v,e,w
  for W1 being Walk of G1, W2 being Walk of G2
  st W1 = W2 & W2 is minlength & W2 is_Walk_from x,v & not e in the_Edges_of G2
  holds W1.addEdge(e) is minlength;

theorem :: GLIBPRE1:63
  for G2 being _Graph, v,e,x being object, w being Vertex of G2
  for G1 being addAdjVertex of G2,v,e,w
  for W1 being Walk of G1, W2 being Walk of G2
  st W1 = W2 & W2 is minlength & W2 is_Walk_from x,w & not e in the_Edges_of G2
  holds W1.addEdge(e) is minlength;

registration
  cluster non empty non non-Dmulti non non-multi for Graph-yielding Function;
end;

registration
  cluster non empty non acyclic non connected for Graph-yielding Function;
end;

registration
  cluster non empty non edgeless for Graph-yielding Function;
end;

registration
  cluster non empty non loopfull for Graph-yielding Function;
end;

begin :: into GLIB_007

theorem :: GLIBPRE1:64
  for G2,G3 being _Graph, V, E being set, G1 being addVertices of G3, V
  for G4 being reverseEdgeDirections of G3, E
  holds G2 is reverseEdgeDirections of G1, E iff G2 is addVertices of G4, V;

theorem :: GLIBPRE1:65  :: ThD3
  for G2,G3 being _Graph, v,e,w being object
  for G1 being addEdge of G3,v,e,w st not e in the_Edges_of G3
  holds G2 is reverseEdgeDirections of G1, {e} iff G2 is addEdge of G3,w,e,v;

theorem :: GLIBPRE1:66
  for G2, G3 being _Graph, v,e,w being object
  for G1 being addAdjVertex of G3,v,e,w st not e in the_Edges_of G3 holds
    G2 is reverseEdgeDirections of G1, {e} iff G2 is addAdjVertex of G3,w,e,v;

theorem :: GLIBPRE1:67
  for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
  for W1 being Walk of G1, W2 being Walk of G2
  st W1 = W2 holds W1 is minlength iff W2 is minlength;

begin :: into GLIB_008

theorem :: GLIBPRE1:68
  for G1 being edgeless _Graph, G2 being _Graph
  holds G1 is Subgraph of G2 iff the_Vertices_of G1 c= the_Vertices_of G2;

registration
  cluster loopless non edgeless for _Graph;
end;

begin :: into GLIB_009

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

theorem :: GLIBPRE1:69
  for G being plain _Graph holds G = createGraph(the_Vertices_of G,
    the_Edges_of G, the_Source_of G, the_Target_of G);

theorem :: GLIBPRE1:70
  for G being _Graph, H being removeLoops of G
  holds the_Edges_of G = G.loops() iff H is edgeless;

theorem :: GLIBPRE1:71
  for G being _Graph, H being removeLoops of G, H9 being loopless Subgraph of G
  holds H9 is Subgraph of H;

theorem :: GLIBPRE1:72
  for G1 being _Graph, G2 being removeLoops of G1
  for W1 being minlength Walk of G1 holds W1 is Walk of G2;

theorem :: GLIBPRE1:73
  for G1 being _Graph, G2 being removeLoops of G1
  for W1 being Walk of G1, W2 being Walk of G2
  st W1 = W2 holds W1 is minlength iff W2 is minlength;

theorem :: GLIBPRE1:74
  for G1 being _Graph, G2 being removeLoops of G1
  for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
  st v1 = v2 & w1 = w2 & v1 <> w1
  holds v1,w1 are_adjacent iff v2,w2 are_adjacent;

theorem :: GLIBPRE1:75
  for G1 being _Graph, G2 being removeParallelEdges of G1
  for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
  st v1 = v2 & w1 = w2 holds v1,w1 are_adjacent iff v2,w2 are_adjacent;

theorem :: GLIBPRE1:76
  for G1 being _Graph, G2 being removeDParallelEdges of G1
  for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
  st v1 = v2 & w1 = w2 holds v1,w1 are_adjacent iff v2,w2 are_adjacent;

theorem :: GLIBPRE1:77
  for G1 being _Graph, G2 being SimpleGraph of G1
  for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
  st v1 = v2 & w1 = w2 & v1 <> w1
  holds v1,w1 are_adjacent iff v2,w2 are_adjacent;

theorem :: GLIBPRE1:78
  for G1 being _Graph, G2 being DSimpleGraph of G1
  for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
  st v1 = v2 & w1 = w2 & v1 <> w1
  holds v1,w1 are_adjacent iff v2,w2 are_adjacent;

begin :: into GLIB_010

theorem :: GLIBPRE1:79
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v2 = F_V.v1 & F is total
  holds F_V.:G1.reachableFrom(v1) c= G2.reachableFrom(v2);

:: onto would be enough, but there are no theorems for that
:: (there could be multiple walks of G1 mapping to a specific one of G2)
theorem :: GLIBPRE1:80
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v1 in dom F_V & v2 = F_V.v1 & F is one-to-one onto
  holds G2.reachableFrom(v2) c= F_V.:G1.reachableFrom(v1);

theorem :: GLIBPRE1:81
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v2 = F_V.v1 & F is isomorphism
  holds F_V.:G1.reachableFrom(v1) = G2.reachableFrom(v2);

theorem :: GLIBPRE1:82
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  st F is isomorphism holds G2.componentSet() =
    the set of all F_V.:C where C is Element of G1.componentSet();

theorem :: GLIBPRE1:83
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  st F is isomorphism holds G1.numComponents() = G2.numComponents();

registration
  let G be loopless _Graph;
  cluster G-isomorphic -> loopless for _Graph;
end;

theorem :: GLIBPRE1:84
  for G1, G2, G3, G4 being _Graph, F1 being empty PGraphMapping of G1, G2
  for F2 being empty PGraphMapping of G3, G4 holds F1 = F2;

theorem :: GLIBPRE1:85
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  holds F | dom F = F & (rng F) |` F = F;

theorem :: GLIBPRE1:86
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  st F is total holds (rng F) |` F is total;

theorem :: GLIBPRE1:87
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  st F is onto holds F | dom F is onto;

theorem :: GLIBPRE1:88
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  holds F is PGraphMapping of G1, rng F;

theorem :: GLIBPRE1:89
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  holds F is PGraphMapping of dom F, G2;

:: Proof mostly taken from GLIB_010:46, generalization of the same
theorem :: GLIBPRE1:90
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for X,Y being Subset of the_Vertices_of G1 st F is total
  holds F_E.:G1.edgesBetween(X,Y) c= G2.edgesBetween(F_V.:X,F_V.:Y);

:: generalization of GLIB_010:7 and GLIB_010:46
theorem :: GLIBPRE1:91
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2, V being set
  holds F_E.:G1.edgesBetween(V) c= G2.edgesBetween(F_V.:V);

:: generalization of GLIB_010:86
theorem :: GLIBPRE1:92
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for X,Y being Subset of the_Vertices_of G1 st F is weak_SG-embedding onto
  holds F_E.:G1.edgesBetween(X,Y) = G2.edgesBetween(F_V.:X,F_V.:Y);

:: generalization of GLIB_010:87
theorem :: GLIBPRE1:93
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2, V being set
  st F is continuous holds F_E.:G1.edgesBetween(V) = G2.edgesBetween(F_V.:V);

theorem :: GLIBPRE1:94
  for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
  for W2 being F-valued Walk of G2
  holds (F"W2).vertices() = F_V"W2.vertices();

theorem :: GLIBPRE1:95
  for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
  for W2 being F-valued Walk of G2
  holds (F"W2).edges() = F_E"W2.edges();

theorem :: GLIBPRE1:96
  for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
  for W2 being F-valued Walk of G2, v,w being object
  holds W2 is_Walk_from v,w implies F"W2 is_Walk_from F"_V.v, F"_V.w;

theorem :: GLIBPRE1:97
  for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v2 = F_V.v1 & F is isomorphism
  holds F_V"G2.reachableFrom(v2) = G1.reachableFrom(v1);

theorem :: GLIBPRE1:98
  for G1, G2 being _Graph
  for F being PGraphMapping of G1, G2, H being Subgraph of G2
  holds F_E"the_Edges_of H c= G1.edgesBetween(F_V"the_Vertices_of H);

theorem :: GLIBPRE1:99
  for G1, G2 being _Graph
  for F being non empty PGraphMapping of G1, G2, H2 being Subgraph of rng F
  for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
  holds rng(F | H1) == H2;

theorem :: GLIBPRE1:100
  for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
  for V2 being non empty Subset of the_Vertices_of rng F
  for H being inducedSubgraph of rng F, V2
  st G1.edgesBetween(F_V"the_Vertices_of H) c= dom F_E
  holds F_E"the_Edges_of H = G1.edgesBetween(F_V"the_Vertices_of H);

theorem :: GLIBPRE1:101
  for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
  for V2 being non empty Subset of the_Vertices_of rng F
  for H2 being inducedSubgraph of rng F, V2
  for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2
  st G1.edgesBetween(F_V"the_Vertices_of H2) c= dom F_E holds rng(F | H1) == H2
;

theorem :: GLIBPRE1:102
  for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
  for V being non empty Subset of the_Vertices_of dom F
  for H being inducedSubgraph of G1, V st F is continuous
  holds rng(F | H) is inducedSubgraph of G2, F_V.:V;

theorem :: GLIBPRE1:103
  for G1, G2 being _Graph
  for F being non empty PGraphMapping of G1, G2, H2 being Subgraph of rng F
  for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
  for W1 being Walk of H1 holds W1 is F-defined Walk of G1;

theorem :: GLIBPRE1:104
  for G1, G2 being _Graph
  for F being non empty PGraphMapping of G1, G2, H2 being Subgraph of rng F
  for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
  for W1 being F-defined Walk of G1 st W1 is Walk of H1
  holds F.:W1 is Walk of H2;

theorem :: GLIBPRE1:105
  for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
  for H being Subgraph of rng F, W being Walk of H
  holds W is F-valued Walk of G2;

theorem :: GLIBPRE1:106
  for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1,G2
  for H2 being Subgraph of rng F
  for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
  for W2 being F-valued Walk of G2 st W2 is Walk of H2
  holds F"W2 is Walk of H1;

theorem :: GLIBPRE1:107
  for G1, G2 being _Graph
  for F being non empty one-to-one PGraphMapping of G1, G2
  for H2 being acyclic Subgraph of rng F
  for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
  holds H1 is acyclic;

theorem :: GLIBPRE1:108
  for G1, G2 being _Graph
  for F being non empty one-to-one PGraphMapping of G1, G2
  for H2 being connected Subgraph of rng F
  for H1 being inducedSubgraph of G1,F_V"the_Vertices_of H2,F_E"the_Edges_of H2
  holds H1 is connected;

:: To see why F_E being one-to-one is necessary for (D)continuity
:: consider the surjective mapping from K_4 to K_2. It is (D)continuous,
:: but if you take H = 2K_2, then the induced map isn't (D)continuous anymore
:: (but it still is semi-(D)continuous).
theorem :: GLIBPRE1:109
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for H being Subgraph of G1
  for F9 being PGraphMapping of H, rng(F | H) st F9 = F | H holds
    (F9 is non empty implies F9 is onto) &
    (F is total implies F9 is total) &
    (F is one-to-one implies F9 is one-to-one) &
    (F is directed implies F9 is directed) &
    (F is semi-continuous implies F9 is semi-continuous) &
    (F is continuous & F_E is one-to-one implies F9 is continuous) &
    (F is semi-Dcontinuous implies F9 is semi-Dcontinuous) &
    (F is Dcontinuous & F_E is one-to-one implies F9 is Dcontinuous);

theorem :: GLIBPRE1:110
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for H being Subgraph of G1
  for F9 being PGraphMapping of H, rng(F | H) st F9 = F | H holds
    (F is weak_SG-embedding implies F9 is weak_SG-embedding) &
    (F is strong_SG-embedding implies F9 is isomorphism) &
    (F is directed strong_SG-embedding implies F9 is Disomorphism);

begin :: into GLIB_013

:: or into GLIB_012 (vertex-finite can be replaced by _finite)
theorem :: GLIBPRE1:111
  for G1 being vertex-finite Dsimple _Graph, G2 being DGraphComplement of G1
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds
    v2.inDegree() = G1.order() - (v1.inDegree()+1) &
    v2.outDegree() = G1.order() - (v1.outDegree()+1) &
    v2.degree() = 2*G1.order() - (v1.degree()+2);

:: or into GLIB_012 (vertex-finite can be replaced by _finite)
theorem :: GLIBPRE1:112
  for G1 being vertex-finite simple _Graph, G2 being GraphComplement of G1
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
  holds v2.degree() = G1.order() - (v1.degree()+1);

theorem :: GLIBPRE1:113
  for G being vertex-finite Dsimple _Graph, v being Vertex of G
  holds v.inDegree() < G.order() & v.outDegree() < G.order();

theorem :: GLIBPRE1:114
  for G being vertex-finite simple _Graph, v being Vertex of G
  holds v.degree() < G.order();

registration
  cluster 1-edge -> non-multi for _Graph;
end;

begin :: into GLIB_014

registration
  let S be \/-tolerating Graph-membered set;
  cluster -> \/-tolerating for Subset of S;
end;

theorem :: GLIBPRE1:115
  for S1, S2 being Graph-membered set st S1 c= S2 holds
    the_Vertices_of S1 c= the_Vertices_of S2 &
    the_Edges_of S1 c= the_Edges_of S2 &
    the_Source_of S1 c= the_Source_of S2 &
    the_Target_of S1 c= the_Target_of S2;

theorem :: GLIBPRE1:116
  for S being GraphUnionSet, G being GraphUnion of S
  for e,v,w being object st e DJoins v,w,G
  ex H being Element of S st e DJoins v,w,H;

theorem :: GLIBPRE1:117
  for S being GraphUnionSet, G being GraphUnion of S
  for e,v,w being object st e Joins v,w,G
  ex H being Element of S st e Joins v,w,H;

theorem :: GLIBPRE1:118
  for S1, S2 being GraphUnionSet
  for G1 being (GraphUnion of S1), G2 being GraphUnion of S2
  st (for H2 being Element of S2 ex H1 being Element of S1
    st H2 is Subgraph of H1)
  holds G2 is Subgraph of G1;

theorem :: GLIBPRE1:119
  for S1, S2 being GraphUnionSet
  for G1 being (GraphUnion of S1), G2 being GraphUnion of S2
  st S2 c= S1 holds G2 is Subgraph of G1;

theorem :: GLIBPRE1:120
  for G1, G2 being _Graph, G being GraphUnion of G1, G2
  st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
  holds G.order() = G1.order() +` G2.order();

theorem :: GLIBPRE1:121
  for G1, G2 being _Graph, G being GraphUnion of G1, G2
  st G1 tolerates G2 & the_Edges_of G1 misses the_Edges_of G2
  holds G.size() = G1.size() +` G2.size();

theorem :: GLIBPRE1:122
  for G1, G2 being connected _Graph, G being GraphUnion of G1, G2
  st the_Vertices_of G1 meets the_Vertices_of G2 holds G is connected;

theorem :: GLIBPRE1:123
  for G1, G2 being _Graph, G being GraphUnion of G1, G2, W being Walk of G
  st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
  holds W is Walk of G1 or W is Walk of G2;

theorem :: GLIBPRE1:124
  for G1, G2 being _Graph, G being GraphUnion of G1, G2
  for v1 being Vertex of G1, v being Vertex of G
  st the_Vertices_of G1 misses the_Vertices_of G2
  holds v = v1 implies G.reachableFrom(v) = G1.reachableFrom(v1);

theorem :: GLIBPRE1:125
  for G1, G2 being _Graph, G being GraphUnion of G1, G2
  for v2 being Vertex of G2, v being Vertex of G
  st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
  holds v = v2 implies G.reachableFrom(v) = G2.reachableFrom(v2);

theorem :: GLIBPRE1:126
  for G1, G2 being _Graph, G being GraphUnion of G1, G2
  st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
  holds G.componentSet() = G1.componentSet() \/ G2.componentSet() &
    G.numComponents() = G1.numComponents() +` G2.numComponents();

begin :: into GLUNIR00

theorem :: GLIBPRE1:127
  for V being non empty set, E being Relation of V
  holds createGraph(V,E).loops() = E /\ id V;

theorem :: GLIBPRE1:128
  for V being non empty set, E being Relation of V
  holds createGraph(V, E \ id V) is removeLoops of createGraph(V,E);