:: Miscellaneous Graph Preliminaries
:: by Sebastian Koch
::
:: Copyright (c) 2019-2021 Association of Mizar Users

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

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

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

:: 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}} & not ( x = a & y = b ) holds
( x = b & y = a )
proof end;

:: 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 ) ) ) by ZFMISC_1:22;

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

registration
let X be non empty set ;
cluster id X -> non irreflexive ;
coherence
not id X is irreflexive
proof end;
cluster [:X,X:] -> non irreflexive non asymmetric ;
coherence
( not [:X,X:] is irreflexive & not [:X,X:] is asymmetric )
proof end;
existence
ex b1 being Relation of X st
( not b1 is irreflexive & not b1 is asymmetric )
proof end;
existence
ex b1 being Relation of X st
( b1 is symmetric & b1 is irreflexive & not b1 is total )
proof end;
existence
ex b1 being Relation of X st
( b1 is symmetric & not b1 is irreflexive & not b1 is empty )
proof end;
end;

registration
let X be non trivial set ;
cluster id X -> non connected ;
coherence
not id X is connected
proof end;
existence
ex b1 being Relation of X st
( b1 is symmetric & not b1 is connected )
proof end;
cluster [:X,X:] -> non antisymmetric ;
coherence
not [:X,X:] is antisymmetric
proof end;
existence
not for b1 being Relation of X holds b1 is antisymmetric
proof end;
end;

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

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

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

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

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

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

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

:: into CARD_1 ?
registration
let a, b be Cardinal;
cluster a /\ b -> cardinal ;
coherence
a /\ b is cardinal
by ORDINAL3:13;
cluster a \/ b -> cardinal ;
coherence
a \/ b is cardinal
by ORDINAL3:12;
end;

:: into ORDINAL1 or WELLORD2 ?
registration
let X be c=-linear set ;
coherence
proof end;
end;

:: into YELLOW_1 or ORDERS_5 ?
registration
let X be c=-linear set ;
coherence
proof end;
end;

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

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

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

Th19: for X being functional set holds meet X is Function
proof end;

registration
let X be functional set ;
coherence
( meet X is Function-like & meet X is Relation-like )
by Th19;
end;

:: into PENCIL_1 ?
:: mostly copied from there
theorem Th20: :: 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 ) )
proof end;

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

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

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

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

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

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

:: into GLIB_000 ?
theorem :: GLIBPRE0:23
for G being _Graph
for v being Vertex of G holds
( v is isolated iff not v in (rng ()) \/ (rng ()) )
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: GLIBPRE0:46
for G being _Graph
for C being Component of G
for v1 being Vertex of G
for 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() )
proof end;

theorem :: GLIBPRE0:47
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for v1 being Vertex of G1
for 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() )
proof end;

theorem :: GLIBPRE0:48
for G2 being _Graph
for v, w, e being object
for G1 being addEdge of G2,v,e,w
for v1 being Vertex of G1
for 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() )
proof end;

theorem :: GLIBPRE0:49
for G2 being _Graph
for v, w being Vertex of G2
for 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() = () \/ {e} & v1 .outDegree() = () + 1 & v1 .edgesInOut() = () \/ {e} & v1 .degree() = () + 1 )
proof end;

theorem :: GLIBPRE0:50
for G2 being _Graph
for v, w being Vertex of G2
for 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() = () \/ {e} & w1 .inDegree() = () + 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = () \/ {e} & w1 .degree() = () + 1 )
proof end;

theorem :: GLIBPRE0:51
for G2 being _Graph
for v being Vertex of G2
for 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() = () \/ {e} & v1 .inDegree() = () + 1 & v1 .edgesOut() = () \/ {e} & v1 .outDegree() = () + 1 & v1 .edgesInOut() = () \/ {e} & v1 .degree() = () + 2 )
proof end;

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

:: counterpart of GLIB_007:55
theorem :: GLIBPRE0:53
for G2 being _Graph
for v being object
proof end;

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

theorem :: GLIBPRE0:55
for G1 being _Graph
for G2 being reverseEdgeDirections of G1
for v1 being Vertex of G1
for 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() )
proof end;

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

theorem :: GLIBPRE0:57
for G2 being _Graph
for v being object
for V being set
for 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 )
proof end;

theorem Th62: :: GLIBPRE0:58
for G2 being _Graph
for v being object
for V being set
for v1 being Vertex of G1
for 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() )
proof end;

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

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

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

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

theorem Th67: :: GLIBPRE0:63
for G being _Graph holds G .loops() = dom (() /\ ())
proof end;

Lm1: for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds G2 is reverseEdgeDirections of G1,E \ (G1 .loops())

proof end;

Lm2: for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E \ (G1 .loops()) holds G2 is reverseEdgeDirections of G1,E

proof end;

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

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

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

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

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

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

registration
let G be non loopless _Graph;
cluster -> non loopless for removeParallelEdges of G;
coherence
for b1 being removeParallelEdges of G holds not b1 is loopless
proof end;
cluster -> non loopless for removeDParallelEdges of G;
coherence
for b1 being removeDParallelEdges of G holds not b1 is loopless
proof end;
end;

registration
let G be non edgeless _Graph;
cluster -> non edgeless for removeParallelEdges of G;
coherence
for b1 being removeParallelEdges of G holds not b1 is edgeless
proof end;
cluster -> non edgeless for removeDParallelEdges of G;
coherence
for b1 being removeDParallelEdges of G holds not b1 is edgeless
proof end;
end;

theorem :: GLIBPRE0:70
for G being _Graph
for E being RepEdgeSelection of G holds card E = card ()
proof end;

theorem :: GLIBPRE0:71
for G being _Graph
for E being RepDEdgeSelection of G holds card E = card ()
proof end;

Lm3: for G being _Graph
for X being set
for E being Subset of ()
for H being reverseEdgeDirections of G,X st E is RepEdgeSelection of G holds
E is RepEdgeSelection of H

proof end;

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

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

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

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

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

registration
existence
ex b1 being _Graph st
( not b1 is non-multi & b1 is non-Dmulti )
proof end;
end;

definition
let GF be Graph-yielding Function;
attr GF is plain means :Def1: :: GLIBPRE0:def 1
for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is plain );
end;

:: deftheorem Def1 defines plain GLIBPRE0:def 1 :
for GF being Graph-yielding Function holds
( GF is plain iff for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is plain ) );

registration
let G be plain _Graph;
cluster <*G*> -> plain ;
coherence
<*G*> is plain
proof end;
coherence
NAT --> G is plain
by FUNCOP_1:7;
end;

definition
let GF be non empty Graph-yielding Function;
redefine attr GF is plain means :Def2: :: GLIBPRE0:def 2
for x being Element of dom GF holds GF . x is plain ;
compatibility
( GF is plain iff for x being Element of dom GF holds GF . x is plain )
proof end;
end;

:: deftheorem Def2 defines plain GLIBPRE0:def 2 :
for GF being non empty Graph-yielding Function holds
( GF is plain iff for x being Element of dom GF holds GF . x is plain );

Lm4: for F being ManySortedSet of NAT
for n being object holds
( n is Nat iff n in dom F )

proof end;

definition
let GSq be GraphSeq;
redefine attr GSq is plain means :Def3: :: GLIBPRE0:def 3
for n being Nat holds GSq . n is plain ;
compatibility
( GSq is plain iff for n being Nat holds GSq . n is plain )
proof end;
end;

:: deftheorem Def3 defines plain GLIBPRE0:def 3 :
for GSq being GraphSeq holds
( GSq is plain iff for n being Nat holds GSq . n is plain );

registration
coherence
for b1 being Graph-yielding Function st b1 is empty holds
b1 is plain
;
end;

registration
existence
ex b1 being GraphSeq st b1 is plain
proof end;
existence
ex b1 being Graph-yielding FinSequence st
( not b1 is empty & b1 is plain )
proof end;
end;

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

registration
let GSq be plain GraphSeq;
let x be Nat;
cluster GSq . x -> plain ;
coherence
GSq . x is plain
by Def3;
end;

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

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

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

theorem Th81: :: GLIBPRE0:77
for G1, G2 being _Graph st G1 == G2 holds
ex F being PGraphMapping of G1,G2 st
( F = id G1 & F is Disomorphism )
proof end;

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

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

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

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

theorem Th86: :: GLIBPRE0:82
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st v in dom (F _V) holds
(F _E) .: () c= ((F _V) /. v) .edgesInOut()
proof end;

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

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

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

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

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

registration
let G1 be _Graph;
let G2 be edgeless _Graph;
cluster -> directed for PGraphMapping of G1,G2;
coherence
for b1 being PGraphMapping of G1,G2 holds b1 is directed
proof end;
end;

theorem Th92: :: GLIBPRE0:88
for G1, G2 being _Graph
for F0 being PGraphMapping of G1,G2 st F0 _E is one-to-one holds
ex E being Subset of () st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is 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 ) )
proof end;

theorem Th93: :: GLIBPRE0:89
for G1, G2 being _Graph
for F0 being PGraphMapping of G1,G2 st F0 _E is one-to-one holds
ex E being Subset of () 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 ) )
proof end;

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

Lm5: for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v being Vertex of G1 st F is directed & F is weak_SG-embedding holds
v .degree() c= ((F _V) /. v) .degree()

proof end;

theorem :: GLIBPRE0:91
for G1, G2 being _Graph
for 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()
proof end;

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

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

theorem Th98: :: GLIBPRE0:94
for G1, G2 being _Graph
for 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() )
proof end;

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

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

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

theorem :: GLIBPRE0:98
for G being _Graph
for v being Vertex of G st 4 c= G .order() & v is endvertex holds
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 )
proof end;

definition
let GF be Graph-yielding Function;
attr GF is chordal means :Def4: :: GLIBPRE0:def 4
for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is chordal );
end;

:: deftheorem Def4 defines chordal GLIBPRE0:def 4 :
for GF being Graph-yielding Function holds
( GF is chordal iff for x being object st x in dom GF holds
ex G being _Graph st
( GF . x = G & G is chordal ) );

registration
let G be chordal _Graph;
coherence
<*G*> is chordal
proof end;
coherence by FUNCOP_1:7;
end;

definition
let GF be non empty Graph-yielding Function;
redefine attr GF is chordal means :Def5: :: GLIBPRE0:def 5
for x being Element of dom GF holds GF . x is chordal ;
compatibility
( GF is chordal iff for x being Element of dom GF holds GF . x is chordal )
proof end;
end;

:: deftheorem Def5 defines chordal GLIBPRE0:def 5 :
for GF being non empty Graph-yielding Function holds
( GF is chordal iff for x being Element of dom GF holds GF . x is chordal );

definition
let GSq be GraphSeq;
redefine attr GSq is chordal means :Def6: :: GLIBPRE0:def 6
for n being Nat holds GSq . n is chordal ;
compatibility
( GSq is chordal iff for n being Nat holds GSq . n is chordal )
proof end;
end;

:: deftheorem Def6 defines chordal GLIBPRE0:def 6 :
for GSq being GraphSeq holds
( GSq is chordal iff for n being Nat holds GSq . n is chordal );

registration
coherence
for b1 being Graph-yielding Function st b1 is empty holds
b1 is chordal
;
end;

registration
existence
ex b1 being GraphSeq st b1 is chordal
proof end;
existence
ex b1 being Graph-yielding FinSequence st
( not b1 is empty & b1 is chordal )
proof end;
end;

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

registration
let GSq be chordal GraphSeq;
let x be Nat;
cluster GSq . x -> chordal ;
coherence
GSq . x is chordal
by Def6;
end;

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

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

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

theorem :: GLIBPRE0:99
for G1, G2 being non-Dmulti _Graph
for 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() )
proof end;

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