:: Miscellaneous Graph Preliminaries
::  by Sebastian Koch
:: 
:: Received December 30, 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, TARSKI, ARYTM_3,
      CARD_1, XBOOLE_0, GLIB_000, PARTFUN1, FINSET_1, ZFMISC_1, RELAT_2,
      FUNCT_2, GLIB_009, MOD_4, WAYBEL_0, GLIB_006, GLIB_007, FUNCT_4,
      ORDINAL2, CARD_2, SCMYCIEL, SGRAPH1, GLIB_010, MATRIX11, BSPACE,
      SETFAM_1, ORDINAL1, FUNCT_7, YELLOW_1, WELLORD2, CHORD, NAT_1, GLIB_002,
      XXREAL_0, CARD_3, FUNCOP_1, PBOOLE, EQREL_1, RFINSEQ, FINSEQ_8, GRAPH_2,
      ORDINAL4, RING_3, GLIB_011, ARYTM_1, GLIB_001;
 notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
      ENUMSET1, FUNCT_1, RELAT_2, ORDINAL1, RELSET_1, PARTFUN1, WELLORD2,
      FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CHORD,
      PARTFUN2, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, VALUED_0, NAT_D,
      CARD_2, FINSEQ_1, EQREL_1, FINSEQ_2, FINSEQ_4, NEWTON, FUNCT_7, RFINSEQ,
      FINSEQ_6, FINSEQ_8, ORDERS_1, CARD_3, ABIAN, GLIB_000, GLIB_001,
      STRUCT_0, ORDERS_2, GROUP_1, GROUP_2, GROUP_6, YELLOW_1, SGRAPH1,
      MATRIX11, GLIB_002, GLIB_003, BSPACE, ORDERS_5, GLIB_006, GLIB_007,
      GLIB_008, GLIB_009, GLIB_010, GLIB_011;
 constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
      FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000,
      STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, ALGSTR_0, GROUP_1, GLIB_001, ABIAN,
      CARD_3, FINSEQ_1, GLIB_002, GLIB_003, SETFAM_1, EQREL_1, GROUP_2,
      GROUP_6, GLIB_006, GLIB_007, PARTFUN2, BSPACE, SETWISEO, CHORD, RAT_1,
      MATRIX11, GLIB_008, FUNCT_7, GLIB_009, GLIB_010, SQUARE_1, NEWTON,
      VALUED_0, CLASSES1, FINSEQ_2, SGRAPH1, ORDERS_2, YELLOW_1, RFINSEQ,
      GRAPH_2, FINSEQ_8, GLIB_011, FINSEQ_6, ENUMSET1, ORDERS_5;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
      XREAL_0, NAT_1, FINSEQ_1, GLIB_000, CARD_1, FUNCT_2, RELSET_1, XTUPLE_0,
      CARD_3, GLIB_006, GLIB_008, GLIB_009, GLIB_010, MSAFREE5, GRFUNC_1,
      RELAT_2, SUBSET_1, GLIB_011;
 requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;


begin :: Preliminaries not directly related to graphs

:: generalization of XBOOLE_1:45
:: into XBOOLE_1 ?
theorem :: GLIBPRE0:1
  for X,Y,Z being set st Z c= X holds X \/ (Y \ Z) = X \/ Y;

:: generalization of XBOOLE_1:89
:: into XBOOLE_1 ?
theorem :: GLIBPRE0:2
  for X, Y, Z being set holds X /\ Z misses Y \ Z;

:: into ZFMISC_1 ?
theorem :: GLIBPRE0:3
  for x,y being object holds {x,y}\{the Element of {x,y}} = {} iff x = y;

:: into ZFMISC_1 ?
theorem :: GLIBPRE0:4
  for a,b,x,y being object st a <> b & x = the Element of {a,b} &
    y = the Element of ({a,b}\{the Element of {a,b}})
  holds x = a & y = b or x = b & y = a;

:: into ZFMISC_1 ?
theorem :: GLIBPRE0:5
  for a,b,x,y being object holds {a,b} = {x,y} iff
    x = a & y = b or x = b & y = a;

:: into SUBSET_1 ?
theorem :: GLIBPRE0:6
  for X being set, Y being non empty set
  holds X c< Y iff X is proper Subset of Y;

registration
  let X be non empty set;
  cluster id X -> non irreflexive;
  cluster [: X, X :] -> non irreflexive non asymmetric;
  cluster non irreflexive non asymmetric for Relation of X;
  cluster symmetric irreflexive non total for Relation of X;
  cluster symmetric non irreflexive non empty for Relation of X;
end;

registration
  let X be non trivial set;
  cluster id X -> non connected;
  cluster symmetric non connected for Relation of X;
  cluster [: X, X :] -> non antisymmetric;
  cluster non antisymmetric for Relation of X;
end;

:: into RELAT_1 ?
theorem :: GLIBPRE0:7
  for R,S being Relation, X being set holds (R\/S).:X = R.:X \/ S.:X;

:: into RELAT_1 ?
theorem :: GLIBPRE0:8
  for R,S being Relation, Y being set holds (R\/S)"Y = R"Y \/ S"Y;

:: into RELAT_1 ?
theorem :: GLIBPRE0:9
  for R being Relation, X,Y being set holds Y|`R|X = Y|`R /\ R|X;

:: into RELAT_2 ?
theorem :: GLIBPRE0:10
  for R being symmetric Relation, x being object holds Im(R,x) = Coim(R,x);

:: into RELSET_1 ?
theorem :: GLIBPRE0:11
  for X being set, R being Relation of X
  holds R is irreflexive iff id X misses R;

:: into ZFMISC_1 or SYSREL ? (in both cases the qua can be omitted)
theorem :: GLIBPRE0:12
  for x,y being object holds ({[x,y]} qua Relation)~ = {[y,x]};

:: generalization of EQREL_1:6 (total is unneeded assumption)
:: into EQREL_1 ?
theorem :: GLIBPRE0:13
  for X being set, x,y being object, R being symmetric Relation of X
  holds [x,y] in R implies [y,x] in R;

:: into CARD_1 ?
registration
  let a, b be Cardinal;
  cluster a /\ b -> cardinal;
  cluster a \/ b -> cardinal;
end;

:: into ORDINAL1 or WELLORD2 ?
registration
  let X be c=-linear set;
  cluster RelIncl X -> connected;
end;

:: into YELLOW_1 or ORDERS_5 ?
registration
  let X be c=-linear set;
  cluster InclPoset X -> connected;
end;

:: into CARD_1 ?
theorem :: GLIBPRE0:14
  for X being non empty set
  st for a being set st a in X holds a is cardinal number
  ex A being Cardinal st A in X & A = meet X;

:: analogous to TOPGEN_2:3
:: into CARD_1 ?
theorem :: GLIBPRE0:15
  for X being set st for a being set st a in X holds a is cardinal number
  holds meet X is cardinal number;

:: into CARD_3 ?
registration
  let f be Cardinal-yielding Function, x be object;
  cluster f.x -> cardinal;
end;

registration
  let X be functional set;
  cluster meet X -> Function-like Relation-like;
end;

:: into PENCIL_1 ?
:: mostly copied from there
theorem :: GLIBPRE0:16
  for X being set holds 4 c= card X iff
    ex w,x,y,z being object st w in X & x in X & y in X & z in X &
      w<>x & w<>y & w<>z & x<>y & x<>z & y<>z;

:: into PENCIL_1 ?
theorem :: GLIBPRE0:17
  for X being set st 4 c= card X for w,x,y being object ex z being object
  st z in X & w<>z & x<>z & y<>z;

:: into BSPACE or SGRAPH1 ?
theorem :: GLIBPRE0:18
  for X being set holds singletons X misses 2Set X;

:: into SGRAPH1 or MATRIX11 ?
theorem :: GLIBPRE0:19
  for X, Y being set st card X = card Y holds card 2Set X = card 2Set Y;

:: into MATRIX13 ?
theorem :: GLIBPRE0:20
  for X being finite set holds card 2Set X = (card X) choose 2;

begin :: into GLIB_000

theorem :: GLIBPRE0:21
  for G being _Graph, v being Vertex of G, e,w being object
  st v is isolated holds not e Joins v,w,G;

theorem :: GLIBPRE0:22
  for G being _Graph, v being Vertex of G, e,w being object
  st v is isolated holds not e DJoins v,w,G & not e DJoins w,v,G;

:: into GLIB_000 ?
theorem :: GLIBPRE0:23
  for G being _Graph, v being Vertex of G
  holds v is isolated iff not v in rng the_Source_of G \/ rng the_Target_of G;

theorem :: GLIBPRE0:24
  for G being _Graph, v being Vertex of G, e being object
  st v is endvertex holds not e Joins v,v,G;

theorem :: GLIBPRE0:25
  for G being _Graph, v being Vertex of G holds
    v.edgesIn() = (the_Target_of G)"{v} & v.edgesOut() = (the_Source_of G)"{v};

theorem :: GLIBPRE0:26
  for G being _trivial _Graph, v being Vertex of G holds
    v.edgesIn() = the_Edges_of G & v.edgesOut() = the_Edges_of G &
    v.edgesInOut() = the_Edges_of G;

theorem :: GLIBPRE0:27
  for G being _trivial _Graph, v being Vertex of G holds
    v.inDegree() = G.size() & v.outDegree() = G.size() &
    v.degree() = G.size() +` G.size();

theorem :: GLIBPRE0:28
  for G being _Graph, X, Y being set
  holds G.edgesBetween(X,Y) = G.edgesDBetween(X,Y) \/ G.edgesDBetween(Y,X);

theorem :: GLIBPRE0:29
  for G being _Graph, v being Vertex of G
  holds v.edgesInOut() = G.edgesBetween(the_Vertices_of G,{v});

theorem :: GLIBPRE0:30
  for G being _Graph, X,Y being set
  holds G.edgesDBetween(X,Y) = G.edgesOutOf(X) /\ G.edgesInto(Y);

theorem :: GLIBPRE0:31
  for G being _Graph, X, Y being set
  holds G.edgesDBetween(X,Y) c= G.edgesBetween(X,Y);

:: generalized case for GLIB_000:19
theorem :: GLIBPRE0:32
  for G being _Graph, v being Vertex of G
  st for e being object holds not e Joins v,v,G
  holds card v.edgesInOut() = v.degree();

theorem :: GLIBPRE0:33
  for G being _Graph, v being Vertex of G
  holds v is isolated iff v.edgesIn() = {} & v.edgesOut() = {};

theorem :: GLIBPRE0:34
  for G being _Graph, v being Vertex of G
  holds v is isolated iff v.inDegree() = 0 & v.outDegree() = 0;

:: generalization of GLIB_000:def 50
theorem :: GLIBPRE0:35
  for G being _Graph, v being Vertex of G
  holds v is isolated iff v.degree() = 0;

theorem :: GLIBPRE0:36
  for G being _Graph, X being set
  holds G.edgesInto(X) = union {v.edgesIn() where v is Vertex of G : v in X};

theorem :: GLIBPRE0:37
  for G being _Graph, X being set
  holds G.edgesOutOf(X) = union {v.edgesOut() where v is Vertex of G : v in X};

theorem :: GLIBPRE0:38
  for G being _Graph, X being set holds G.edgesInOut(X)
    = union {v.edgesInOut() where v is Vertex of G : v in X};

theorem :: GLIBPRE0:39
  for G being _Graph, X, Y being set holds G.edgesDBetween(X,Y)
    = union {v.edgesOut() /\ w.edgesIn()
      where v, w is Vertex of G : v in X & w in Y};

theorem :: GLIBPRE0:40
  for G being _Graph, X, Y being set holds G.edgesBetween(X,Y)
    c= union {v.edgesInOut() /\ w.edgesInOut()
      where v, w is Vertex of G : v in X & w in Y};

theorem :: GLIBPRE0:41
  for G being _Graph, X, Y being set st X misses Y holds G.edgesBetween(X,Y)
    = union {v.edgesInOut() /\ w.edgesInOut()
      where v, w is Vertex of G : v in X & w in Y};

theorem :: GLIBPRE0:42
  for G1 being _Graph, E being set, G2 being removeEdges of G1, E
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
  holds v2.edgesIn() = v1.edgesIn() \ E & v2.edgesOut() = v1.edgesOut() \ E &
    v2.edgesInOut() = v1.edgesInOut() \ E;

theorem :: GLIBPRE0:43
  for G1, G2 being _Graph, V being set
  holds G2 is removeVertices of G1, V iff
    G2 is removeVertices of G1, V /\ the_Vertices_of G1;

theorem :: GLIBPRE0:44
  for G1 being _Graph, V being set, G2 being removeVertices of G1, V
  for v1 being Vertex of G1, v2 being Vertex of G2
  st V c< the_Vertices_of G1 & v1 = v2 holds
    v2.edgesIn() = v1.edgesIn() \ G1.edgesOutOf(V) &
    v2.edgesOut() = v1.edgesOut() \ G1.edgesInto(V) &
    v2.edgesInOut() = v1.edgesInOut() \ G1.edgesInOut(V);

theorem :: GLIBPRE0:45
  for G1 being non _trivial _Graph, v being Vertex of G1
  for G2 being removeVertex of G1, v
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds
    v2.edgesIn() = v1.edgesIn() \ v.edgesOut() &
    v2.edgesOut() = v1.edgesOut() \ v.edgesIn() &
    v2.edgesInOut() = v1.edgesInOut() \ v.edgesInOut();

begin :: into GLIB_002

theorem :: GLIBPRE0:46
  for G being _Graph, C being Component of G
  for v1 being Vertex of G, v2 being Vertex of C st v1 = v2 holds
    v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
    v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
    v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree();

begin :: into GLIB_006

theorem :: GLIBPRE0:47
  for G2 being _Graph, V being set, G1 being addVertices of G2, V
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v1 = v2 holds
    v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
    v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
    v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree();

theorem :: GLIBPRE0:48
  for G2 being _Graph, v,w,e being object, G1 being addEdge of G2,v,e,w
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v1 = v2 & v2 <> v & v2 <> w holds
    v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
    v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
    v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree();

theorem :: GLIBPRE0:49
  for G2 being _Graph, v,w being Vertex of G2, e being object
  for G1 being addEdge of G2,v,e,w for v1 being Vertex of G1
  st not e in the_Edges_of G2 & v1 = v & v <> w holds
    v1.edgesIn() = v.edgesIn() & v1.inDegree() = v.inDegree() &
    v1.edgesOut() = v.edgesOut() \/ {e} & v1.outDegree() = v.outDegree() +` 1 &
    v1.edgesInOut() = v.edgesInOut() \/ {e} & v1.degree() = v.degree() +` 1;

theorem :: GLIBPRE0:50
  for G2 being _Graph, v,w being Vertex of G2, e being object
  for G1 being addEdge of G2,v,e,w for w1 being Vertex of G1
  st not e in the_Edges_of G2 & w1 = w & v <> w holds
    w1.edgesIn() = w.edgesIn() \/ {e} & w1.inDegree() = w.inDegree() +` 1 &
    w1.edgesOut() = w.edgesOut() & w1.outDegree() = w.outDegree() &
    w1.edgesInOut() = w.edgesInOut() \/ {e} & w1.degree() = w.degree() +` 1;

theorem :: GLIBPRE0:51
  for G2 being _Graph, v being Vertex of G2, e being object
  for G1 being addEdge of G2,v,e,v for v1 being Vertex of G1
  st not e in the_Edges_of G2 & v1 = v holds
    v1.edgesIn() = v.edgesIn() \/ {e} & v1.inDegree() = v.inDegree() +` 1 &
    v1.edgesOut() = v.edgesOut() \/ {e} & v1.outDegree() = v.outDegree() +` 1 &
    v1.edgesInOut() = v.edgesInOut() \/ {e} & v1.degree() = v.degree() +` 2;

begin :: into GLIB_007

theorem :: GLIBPRE0:52
  for G3 being _Graph, E being set, G4 being reverseEdgeDirections of G3, E
  for G1 being Supergraph of G3, G2 being reverseEdgeDirections of G1, E
  st E c= the_Edges_of G3 holds G2 is Supergraph of G4;

:: counterpart of GLIB_007:55
theorem :: GLIBPRE0:53
  for G2 being _Graph, v being object, G1 being addVertex of G2, v
  holds G1 is addAdjVertexAll of G2,v,{};

theorem :: GLIBPRE0:54
  for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v1 = v2 & E c= the_Edges_of G1 holds
    v2.edgesIn() = (v1.edgesIn() \ E) \/ (v1.edgesOut() /\ E) &
    v2.edgesOut() = (v1.edgesOut() \ E) \/ (v1.edgesIn() /\ E);

theorem :: GLIBPRE0:55
  for G1 being _Graph, G2 being reverseEdgeDirections of G1
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v1 = v2 holds
    v2.edgesIn() = v1.edgesOut() & v2.inDegree() = v1.outDegree() &
    v2.edgesOut() = v1.edgesIn() & v2.outDegree() = v1.inDegree();

theorem :: GLIBPRE0:56
  for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
  holds v2.edgesInOut() = v1.edgesInOut() & v2.degree() = v1.degree();

theorem :: GLIBPRE0:57
  for G2 being _Graph, v being object, V being set
  for G1 being addAdjVertexAll of G2, v, V, w being Vertex of G1
  st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v = w
  holds w.allNeighbors() = V & w.degree() = card V;

theorem :: GLIBPRE0:58
  for G2 being _Graph, v being object, V being set
  for G1 being addAdjVertexAll of G2, v, V
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v1 = v2 & not v2 in V holds
    v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
    v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
    v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree();

theorem :: GLIBPRE0:59
  for G2 being _Graph, v being object, V being Subset of the_Vertices_of G2
  for G1 being addAdjVertexAll of G2, v, V
  for v1 being Vertex of G1, v2 being Vertex of G2
  st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
    v1.allNeighbors() = v2.allNeighbors() \/ {v} &
    v1.degree() = v2.degree() +` 1;

theorem :: GLIBPRE0:60
  for G2 being _Graph, v being object, V being set
  for G1 being addAdjVertexAll of G2, v, V
  for v1 being Vertex of G1, v2 being Vertex of G2
  st v1 = v2 holds
    v1.degree() c= v2.degree() +` 1 &
    v1.inDegree() c= v2.inDegree() +` 1 &
    v1.outDegree() c= v2.outDegree() +` 1;

begin :: into GLIB_008

theorem :: GLIBPRE0:61
  for G being _Graph holds G is edgeless iff
    for v,w being Vertex of G holds not v,w are_adjacent;

theorem :: GLIBPRE0:62
  for G being loopless _Graph holds G is edgeless iff
    for v,w being Vertex of G st v <> w holds not v,w are_adjacent;

begin :: into GLIB_009

theorem :: GLIBPRE0:63
  for G being _Graph
  holds G.loops() = dom((the_Source_of G) /\ (the_Target_of G));

theorem :: GLIBPRE0:64
  for G1, G2 being _Graph, E being set
  holds G2 is reverseEdgeDirections of G1, E iff
    G2 is reverseEdgeDirections of G1, E \ G1.loops();

theorem :: GLIBPRE0:65
  for G1 being _Graph, G2 being removeLoops of G1
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
  holds
    v2.inNeighbors() = v1.inNeighbors() \ {v1} &
    v2.outNeighbors() = v1.outNeighbors() \ {v1} &
    v2.allNeighbors() = v1.allNeighbors() \ {v1};

theorem :: GLIBPRE0:66
  for G1 being _Graph, G2 being removeParallelEdges of G1
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
  holds v2.allNeighbors() = v1.allNeighbors();

theorem :: GLIBPRE0:67
  for G1 being _Graph, G2 being removeDParallelEdges of G1
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
  holds
    v2.inNeighbors() = v1.inNeighbors() &
    v2.outNeighbors() = v1.outNeighbors() &
    v2.allNeighbors() = v1.allNeighbors();

theorem :: GLIBPRE0:68
  for G1 being _Graph, G2 being SimpleGraph of G1
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
  holds v2.allNeighbors() = v1.allNeighbors() \ {v1};

theorem :: GLIBPRE0:69
  for G1 being _Graph, G2 being DSimpleGraph of G1
  for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
  holds
    v2.inNeighbors() = v1.inNeighbors() \ {v1} &
    v2.outNeighbors() = v1.outNeighbors() \ {v1} &
    v2.allNeighbors() = v1.allNeighbors() \ {v1};

registration
  let G be non loopless _Graph;
  cluster -> non loopless for removeParallelEdges of G;
  cluster -> non loopless for removeDParallelEdges of G;
end;

registration
  let G be non edgeless _Graph;
  cluster -> non edgeless for removeParallelEdges of G;
  cluster -> non edgeless for removeDParallelEdges of G;
end;

theorem :: GLIBPRE0:70
  for G being _Graph, E being RepEdgeSelection of G
  holds card E = card Class EdgeAdjEqRel(G);

theorem :: GLIBPRE0:71
  for G being _Graph, E being RepDEdgeSelection of G
  holds card E = card Class DEdgeAdjEqRel(G);

theorem :: GLIBPRE0:72
  for G being _Graph, X being set, E being Subset of the_Edges_of G
  for H being reverseEdgeDirections of G, X
  holds E is RepEdgeSelection of G iff E is RepEdgeSelection of H;

theorem :: GLIBPRE0:73
  for G being _Graph, V being non empty Subset of the_Vertices_of G
  for H being (inducedSubgraph of G, V), E being RepEdgeSelection of G
  holds E /\ G.edgesBetween(V) is RepEdgeSelection of H;

theorem :: GLIBPRE0:74
  for G being _Graph, V being non empty Subset of the_Vertices_of G
  for H being (inducedSubgraph of G, V), E being RepDEdgeSelection of G
  holds E /\ G.edgesBetween(V) is RepDEdgeSelection of H;

theorem :: GLIBPRE0:75
  for G being _Graph, V being set, H being addVertices of G, V
  for E being Subset of the_Edges_of G
  holds E is RepEdgeSelection of G iff E is RepEdgeSelection of H;

theorem :: GLIBPRE0:76
  for G being _Graph, V being set, H being addVertices of G, V
  for E being Subset of the_Edges_of G
  holds E is RepDEdgeSelection of G iff E is RepDEdgeSelection of H;

registration
  cluster non non-multi non-Dmulti for _Graph;
end;

definition
  let GF be Graph-yielding Function;
  attr GF is plain means
:: GLIBPRE0:def 1

  for x being object st x in dom GF
    ex G being _Graph st GF.x = G & G is plain;
end;

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

definition
  let GF be non empty Graph-yielding Function;
  redefine attr GF is plain means
:: GLIBPRE0:def 2

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

definition
  let GSq be GraphSeq;
  redefine attr GSq is plain means
:: GLIBPRE0:def 3

  for n being Nat holds GSq.n is plain;
end;

registration
  cluster empty -> plain for Graph-yielding Function;
end;

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

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

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

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

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

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

begin :: into GLIB_010

theorem :: GLIBPRE0:77
  for G1, G2 being _Graph st G1 == G2
  ex F being PGraphMapping of G1, G2 st F = id G1 & F is Disomorphism;

theorem :: GLIBPRE0:78
  for G1, G2 being _Graph st G1 == G2 holds G2 is G1-Disomorphic;

theorem :: GLIBPRE0:79
  for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
  ex F being PGraphMapping of G1, G2 st F = id G1 & F is isomorphism;

theorem :: GLIBPRE0:80
  for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
  holds G2 is G1-isomorphic;

:: correction of GLIB_010:90
theorem :: GLIBPRE0:81
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  st F is Dcontinuous isomorphism holds
    (G1 is non-Dmulti iff G2 is non-Dmulti) &
    (G1 is Dsimple iff G2 is Dsimple);

theorem :: GLIBPRE0:82
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st v in dom F_V
  holds F_E.:(v.edgesInOut()) c= (F_V/.v).edgesInOut();

theorem :: GLIBPRE0:83
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is directed & v in dom F_V holds
    F_E.:(v.edgesIn()) c= (F_V/.v).edgesIn() &
    F_E.:(v.edgesOut()) c= (F_V/.v).edgesOut();

theorem :: GLIBPRE0:84
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is onto semi-continuous & v in dom F_V
  holds F_E.:(v.edgesInOut()) = (F_V/.v).edgesInOut();

theorem :: GLIBPRE0:85
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is onto semi-Dcontinuous & v in dom F_V holds
    F_E.:(v.edgesIn()) = (F_V/.v).edgesIn() &
    F_E.:(v.edgesOut()) = (F_V/.v).edgesOut();

theorem :: GLIBPRE0:86
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is isomorphism
  holds F_E.:(v.edgesInOut()) = (F_V/.v).edgesInOut();

theorem :: GLIBPRE0:87
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is Disomorphism holds
    F_E.:(v.edgesIn()) = (F_V/.v).edgesIn() &
    F_E.:(v.edgesOut()) = (F_V/.v).edgesOut();

registration
  let G1 be _Graph, G2 be edgeless _Graph;
  cluster -> directed for PGraphMapping of G1, G2;
end;

theorem :: GLIBPRE0:88
  for G1, G2 being _Graph, F0 being PGraphMapping of G1, G2
  st F0_E is one-to-one
  ex E being Subset of the_Edges_of G2 st
  for G3 being reverseEdgeDirections of G2, E
  ex F being PGraphMapping of G1, G3 st F = F0 & F is directed &
    (F0 is non empty  implies F is non empty) &
    (F0 is total implies F is total) &
    (F0 is one-to-one implies F is one-to-one) &
    (F0 is onto implies F is onto) &
    (F0 is semi-continuous implies F is semi-continuous) &
    (F0 is continuous implies F is continuous);

theorem :: GLIBPRE0:89
  for G1, G2 being _Graph, F0 being PGraphMapping of G1, G2
  st F0_E is one-to-one
  ex E being Subset of the_Edges_of G2 st
  for G3 being reverseEdgeDirections of G2, E
  ex F being PGraphMapping of G1, G3 st F = F0 & F is directed &
    (F0 is weak_SG-embedding implies F is weak_SG-embedding) &
    (F0 is strong_SG-embedding implies F is strong_SG-embedding) &
    (F0 is isomorphism implies F is isomorphism);

theorem :: GLIBPRE0:90
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is directed weak_SG-embedding holds
    v.inDegree() c= (F_V/.v).inDegree() &
    v.outDegree() c= (F_V/.v).outDegree();

theorem :: GLIBPRE0:91
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is weak_SG-embedding
  holds v.degree() c= (F_V/.v).degree();

theorem :: GLIBPRE0:92
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is onto semi-Dcontinuous & v in dom F_V holds
    (F_V/.v).inDegree() c= v.inDegree() &
    (F_V/.v).outDegree() c= v.outDegree();

:: Can this theorem and all using it be improved to semi-continuous?
theorem :: GLIBPRE0:93
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is onto semi-Dcontinuous & v in dom F_V
  holds (F_V/.v).degree() c= v.degree();

theorem :: GLIBPRE0:94
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is Disomorphism holds
    v.inDegree() = (F_V/.v).inDegree() & v.outDegree() = (F_V/.v).outDegree();

theorem :: GLIBPRE0:95
  for G1, G2 being _Graph, F being PGraphMapping of G1, G2
  for v being Vertex of G1 st F is isomorphism
  holds v.degree() = (F_V/.v).degree();

begin :: into CHORD

theorem :: GLIBPRE0:96
  for G being _Graph, u,v,w being Vertex of G st v is endvertex & u <> w
  holds not u,v are_adjacent or not v,w are_adjacent;

theorem :: GLIBPRE0:97
  for G being _Graph, v being Vertex of G st 3 c= G.order() & v is endvertex
  ex u,w being Vertex of G
  st u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent;

theorem :: GLIBPRE0:98
  for G being _Graph, v being Vertex of G st 4 c= G.order() & v is endvertex
  ex x,y,z being Vertex of G
  st v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent &
    not v,y are_adjacent & not v,z are_adjacent;

definition
  let GF be Graph-yielding Function;
  attr GF is chordal means
:: GLIBPRE0:def 4

  for x being object st x in dom GF
    ex G being _Graph st GF.x = G & G is chordal;
end;

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

definition
  let GF be non empty Graph-yielding Function;
  redefine attr GF is chordal means
:: GLIBPRE0:def 5

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

definition
  let GSq be GraphSeq;
  redefine attr GSq is chordal means
:: GLIBPRE0:def 6

  for n being Nat holds GSq.n is chordal;
end;

registration
  cluster empty -> chordal for Graph-yielding Function;
end;

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

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

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

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

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

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

begin :: into GLIB_011

theorem :: GLIBPRE0:99
  for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
  for v being Vertex of G1 st f is Disomorphism holds
    v.inDegree() = (f/.v).inDegree() & v.outDegree() = (f/.v).outDegree();

theorem :: GLIBPRE0:100
  for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
  for v being Vertex of G1 st f is isomorphism
  holds v.degree() = (f/.v).degree();