:: Alternative Graph Structures
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received February 22, 2005
:: Copyright (c) 2005-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, FINSET_1, 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, XCMPLX_0;
notations TARSKI, XBOOLE_0, DOMAIN_1, SUBSET_1, PBOOLE, RELAT_1, CARD_1,
CARD_2, FUNCT_1, RELSET_1, FINSEQ_1, FINSET_1, ORDINAL1, XCMPLX_0, NAT_1,
FUNCT_2, FUNCOP_1, FUNCT_4, ORDINAL2, FINSEQ_4, NUMBERS, XXREAL_0;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1;
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;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
begin :: Definitions
registration
cluster finite NAT-defined for Function;
end;
definition
mode GraphStruct is finite NAT-defined Function;
end;
definition
func VertexSelector -> Element of NAT equals
:: GLIB_000:def 1
1;
func EdgeSelector -> Element of NAT equals
:: GLIB_000:def 2
2;
func SourceSelector -> Element of NAT equals
:: GLIB_000:def 3
3;
func TargetSelector -> Element of NAT equals
:: GLIB_000:def 4
4;
end;
definition
func _GraphSelectors -> non empty Subset of NAT equals
:: GLIB_000:def 5
{VertexSelector,
EdgeSelector, SourceSelector, TargetSelector};
end;
definition
let G be GraphStruct;
func the_Vertices_of G -> set equals
:: GLIB_000:def 6
G.VertexSelector;
func the_Edges_of G -> set equals
:: GLIB_000:def 7
G.EdgeSelector;
func the_Source_of G -> set equals
:: GLIB_000:def 8
G.SourceSelector;
func the_Target_of G -> set equals
:: GLIB_000:def 9
G.TargetSelector;
end;
definition
let G be GraphStruct;
attr G is [Graph-like] means
:: GLIB_000:def 10
VertexSelector in dom G & EdgeSelector in dom G &
SourceSelector in dom G & TargetSelector in dom G &
the_Vertices_of G is non empty set &
the_Source_of G is Function of the_Edges_of G, the_Vertices_of G &
the_Target_of G is Function of the_Edges_of G, the_Vertices_of G;
end;
registration
cluster [Graph-like] for GraphStruct;
end;
definition
mode _Graph is [Graph-like] GraphStruct;
end;
registration
let G be _Graph;
cluster the_Vertices_of G -> non empty;
end;
definition
let G be _Graph;
redefine func the_Source_of G -> Function of the_Edges_of G,the_Vertices_of
G;
redefine func the_Target_of G -> Function of the_Edges_of G,the_Vertices_of
G;
end;
definition
let V be non empty set,E be set, S,T be Function of E,V;
func createGraph(V,E,S,T) -> _Graph equals
:: GLIB_000:def 11
<* V, E, S, T *>;
end;
definition
let G be GraphStruct, n be Nat, x be set;
func G.set(n,x) -> GraphStruct equals
:: GLIB_000:def 12
G +* (n .--> x);
end;
registration
let G be _Graph;
cluster G|(_GraphSelectors) -> [Graph-like];
end;
definition
let G be _Graph, x,y,e be object;
pred e Joins x,y,G means
:: GLIB_000:def 13
e in the_Edges_of G & ( (the_Source_of G).e
= x & (the_Target_of G).e = y or (the_Source_of G).e = y & (the_Target_of G).e
= x );
end;
definition
let G be _Graph, x, y, e be object;
pred e DJoins x,y,G means
:: GLIB_000:def 14
e in the_Edges_of G & (the_Source_of G).e = x & (the_Target_of G).e = y;
end;
definition
let G be _Graph, X,Y be set,e be object;
pred e SJoins X,Y,G means
:: GLIB_000:def 15
e in the_Edges_of G & ( (the_Source_of G).e in X & (the_Target_of G).e in Y
or (the_Source_of G).e in Y & (the_Target_of G).e in X);
pred e DSJoins X,Y,G means
:: GLIB_000:def 16
e in the_Edges_of G & (the_Source_of G).e in X & (the_Target_of G).e in Y;
end;
definition
let G be _Graph;
attr G is _finite means
:: GLIB_000:def 17
the_Vertices_of G is finite & the_Edges_of G is finite;
attr G is loopless means
:: GLIB_000:def 18
not ex e being object st e in the_Edges_of G &
(the_Source_of G).e = (the_Target_of G).e;
attr G is _trivial means
:: GLIB_000:def 19
card the_Vertices_of G = 1;
attr G is non-multi means
:: GLIB_000:def 20
for e1,e2,v1,v2 being object holds e1 Joins
v1,v2,G & e2 Joins v1,v2,G implies e1 = e2;
attr G is non-Dmulti means
:: GLIB_000:def 21
for e1,e2,v1,v2 being object holds e1 DJoins
v1,v2,G & e2 DJoins v1,v2,G implies e1 = e2;
end;
definition
let G be _Graph;
attr G is simple means
:: GLIB_000:def 22
G is loopless & G is non-multi;
attr G is Dsimple means
:: GLIB_000:def 23
G is loopless & G is non-Dmulti;
end;
registration
cluster non-multi -> non-Dmulti for _Graph;
cluster simple -> loopless non-multi for _Graph;
cluster loopless non-multi -> simple for _Graph;
cluster loopless non-Dmulti -> Dsimple for _Graph;
cluster Dsimple -> loopless non-Dmulti for _Graph;
cluster _trivial loopless -> _finite for _Graph;
cluster _trivial non-Dmulti -> _finite for _Graph;
end;
registration
cluster _trivial simple for _Graph;
cluster _finite non _trivial simple for _Graph;
end;
registration
let G be _finite _Graph;
cluster the_Vertices_of G -> finite;
cluster the_Edges_of G -> finite;
end;
registration
let G be _trivial _Graph;
cluster the_Vertices_of G -> finite;
end;
registration
let V be non empty finite set, E be finite set, S,T be Function of E,V;
cluster createGraph(V,E,S,T) -> _finite;
end;
registration
let V be non empty set, E be empty set,S,T be Function of E,V;
cluster createGraph(V,E,S,T) -> simple;
end;
registration
let v be set, E be set, S,T be Function of E,{v};
cluster createGraph({v},E,S,T) -> _trivial;
end;
definition
let G be _Graph;
func G.order() -> Cardinal equals
:: GLIB_000:def 24
card the_Vertices_of G;
end;
definition
let G be _finite _Graph;
redefine func G.order() -> non zero Element of NAT;
end;
definition
let G be _Graph;
func G.size() -> Cardinal equals
:: GLIB_000:def 25
card the_Edges_of G;
end;
definition
let G be _finite _Graph;
redefine func G.size() -> Element of NAT;
end;
definition
let G be _Graph, X be set;
func G.edgesInto(X) -> Subset of the_Edges_of G means
:: GLIB_000:def 26
for e being
set holds e in it iff e in the_Edges_of G & (the_Target_of G).e in X;
func G.edgesOutOf(X) -> Subset of the_Edges_of G means
:: GLIB_000:def 27
for e being
set holds e in it iff e in the_Edges_of G & (the_Source_of G).e in X;
end;
definition
let G be _Graph, X be set;
func G.edgesInOut(X) -> Subset of the_Edges_of G equals
:: GLIB_000:def 28
G.edgesInto(X) \/ G.edgesOutOf(X);
func G.edgesBetween(X) -> Subset of the_Edges_of G equals
:: GLIB_000:def 29
G.edgesInto(X) /\ G.edgesOutOf(X);
end;
definition
let G be _Graph, X,Y be set;
func G.edgesBetween(X,Y) -> Subset of the_Edges_of G means
:: GLIB_000:def 30
for e being object holds e in it iff e SJoins X,Y,G;
func G.edgesDBetween(X,Y) -> Subset of the_Edges_of G means
:: GLIB_000:def 31
for e being object holds e in it iff e DSJoins X,Y,G;
end;
scheme :: GLIB_000:sch 1
FinGraphOrderInd{P[_Graph]}: for G being _finite _Graph holds P[G]
provided
for G being _finite _Graph st G.order() = 1 holds P[G] and
for k being non zero Nat st (for Gk being _finite _Graph st Gk
.order() = k holds P[Gk]) holds
for Gk1 being _finite _Graph st Gk1.order() = k+1 holds P[Gk1];
scheme :: GLIB_000:sch 2
FinGraphSizeInd{P[_Graph]}: for G being _finite _Graph holds P[G]
provided
for G being _finite _Graph st G.size() = 0 holds P[G] and
for k being Nat st
(for Gk being _finite _Graph st Gk.size() = k holds P[Gk]) holds
for Gk1 being _finite _Graph st Gk1.size() = k+1
holds P[Gk1];
definition
let G be _Graph;
mode Subgraph of G -> _Graph means
:: GLIB_000:def 32
the_Vertices_of it c= the_Vertices_of G &
the_Edges_of it c= the_Edges_of G & for e being set st e in
the_Edges_of it holds (the_Source_of it).e = (the_Source_of G).e & (
the_Target_of it).e = (the_Target_of G).e;
end;
definition
let G1 be _Graph, G2 be Subgraph of G1;
redefine func the_Vertices_of G2 -> non empty Subset of the_Vertices_of G1;
redefine func the_Edges_of G2 -> Subset of the_Edges_of G1;
end;
registration
let G be _Graph;
cluster _trivial simple for Subgraph of G;
end;
registration
let G be _finite _Graph;
cluster -> _finite for Subgraph of G;
end;
registration
let G be loopless _Graph;
cluster -> loopless for Subgraph of G;
end;
registration
let G be _trivial _Graph;
cluster -> _trivial for Subgraph of G;
end;
registration
let G be non-multi _Graph;
cluster -> non-multi for Subgraph of G;
end;
definition
let G1 be _Graph, G2 be Subgraph of G1;
attr G2 is spanning means
:: GLIB_000:def 33
the_Vertices_of G2 = the_Vertices_of G1;
end;
registration
let G be _Graph;
cluster spanning for Subgraph of G;
end;
definition
let G1, G2 be _Graph;
pred G1 == G2 means
:: GLIB_000:def 34
the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = the_Source_of G2 &
the_Target_of G1 = the_Target_of G2;
reflexivity;
symmetry;
end;
notation
let G1,G2 be _Graph;
antonym G1 != G2 for G1 == G2;
end;
definition
let G1,G2 be _Graph;
pred G1 c= G2 means
:: GLIB_000:def 35
G1 is Subgraph of G2;
reflexivity;
end;
definition
let G1,G2 be _Graph;
pred G1 c< G2 means
:: GLIB_000:def 36
G1 c= G2 & G1 != G2;
irreflexivity;
end;
definition
let G be _Graph, V, E be set;
mode inducedSubgraph of G,V,E -> Subgraph of G means
:: GLIB_000:def 37
the_Vertices_of
it = V & the_Edges_of it = E if V is non empty Subset of the_Vertices_of G & E
c= G.edgesBetween(V) otherwise it == G;
end;
definition
let G be _Graph, V be set;
mode inducedSubgraph of G,V is inducedSubgraph of G,V,G.edgesBetween(V);
end;
registration
let G be _Graph, V be finite non empty Subset of the_Vertices_of G, E be
finite Subset of G.edgesBetween(V);
cluster -> _finite for inducedSubgraph of G,V,E;
end;
registration
let G be _Graph, v be Element of the_Vertices_of G, E be Subset of G
.edgesBetween({v});
cluster -> _trivial for inducedSubgraph of G,{v},E;
end;
registration
let G be _Graph, v be Element of the_Vertices_of G;
cluster -> _finite _trivial for inducedSubgraph of G,{v},{};
end;
registration
let G be _Graph, V be non empty Subset of the_Vertices_of G;
cluster -> simple for inducedSubgraph of G,V,{};
end;
registration
let G be _Graph, E be Subset of the_Edges_of G;
cluster -> spanning for inducedSubgraph of G,the_Vertices_of G, E;
end;
registration
let G be _Graph;
cluster -> spanning for inducedSubgraph of G,the_Vertices_of G,{};
end;
definition
let G be _Graph, v be set;
mode removeVertex of G,v is inducedSubgraph of G, the_Vertices_of G \ {v};
end;
definition
let G be _Graph, V be set;
mode removeVertices of G,V is inducedSubgraph of G, the_Vertices_of G \ V;
end;
definition
let G be _Graph, e be set;
mode removeEdge of G,e is inducedSubgraph of G, the_Vertices_of G,
the_Edges_of G \ {e};
end;
definition
let G be _Graph, E be set;
mode removeEdges of G,E is inducedSubgraph of G, the_Vertices_of G,
the_Edges_of G \ E;
end;
registration
let G be _Graph, e be set;
cluster -> spanning for removeEdge of G,e;
end;
registration
let G be _Graph, E be set;
cluster -> spanning for removeEdges of G,E;
end;
definition
let G be _Graph;
mode Vertex of G is Element of the_Vertices_of G;
end;
definition
let G be _Graph, v be Vertex of G;
func v.edgesIn() -> Subset of the_Edges_of G equals
:: GLIB_000:def 38
G.edgesInto( {v} );
func v.edgesOut() -> Subset of the_Edges_of G equals
:: GLIB_000:def 39
G.edgesOutOf( {v} );
func v.edgesInOut() -> Subset of the_Edges_of G equals
:: GLIB_000:def 40
G.edgesInOut( {v} );
end;
definition
let G be _Graph, v be Vertex of G, e be object;
func v.adj(e) -> Vertex of G equals
:: GLIB_000:def 41
(the_Source_of G).e if e in
the_Edges_of G & (the_Target_of G).e = v, (the_Target_of G).e if e in
the_Edges_of G & (the_Source_of G).e = v & not (the_Target_of G).e = v
otherwise v;
end;
definition
let G be _Graph, v be Vertex of G;
func v.inDegree() -> Cardinal equals
:: GLIB_000:def 42
card v.edgesIn();
func v.outDegree() -> Cardinal equals
:: GLIB_000:def 43
card v.edgesOut();
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine func v.inDegree() -> Element of NAT;
redefine func v.outDegree() -> Element of NAT;
end;
definition
let G be _Graph, v be Vertex of G;
func v.degree() -> Cardinal equals
:: GLIB_000:def 44
v.inDegree() +` v.outDegree();
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine func v.degree() -> Element of NAT equals
:: GLIB_000:def 45
v.inDegree() + v
.outDegree();
end;
definition
let G be _Graph, v be Vertex of G;
func v.inNeighbors() -> Subset of the_Vertices_of G equals
:: GLIB_000:def 46
(the_Source_of G)
.:v.edgesIn();
func v.outNeighbors() -> Subset of the_Vertices_of G equals
:: GLIB_000:def 47
(the_Target_of G
).:v.edgesOut();
end;
definition
let G be _Graph, v be Vertex of G;
func v.allNeighbors() -> Subset of the_Vertices_of G equals
:: GLIB_000:def 48
v.inNeighbors()
\/ v.outNeighbors();
end;
definition
let G be _Graph, v being Vertex of G;
attr v is isolated means
:: GLIB_000:def 49
v.edgesInOut() = {};
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine attr v is isolated means
:: GLIB_000:def 50
v.degree() = 0;
end;
definition
let G be _Graph, v be Vertex of G;
attr v is endvertex means
:: GLIB_000:def 51
ex e being object st v.edgesInOut() = {e} & not e Joins v,v,G;
end;
definition
let G be _finite _Graph, v be Vertex of G;
redefine attr v is endvertex means
:: GLIB_000:def 52
v.degree() = 1;
end;
definition
let F be Function;
attr F is Graph-yielding means
:: GLIB_000:def 53
for x being object st x in dom F holds F.x is _Graph;
end;
definition
let F be ManySortedSet of NAT;
redefine attr F is Graph-yielding means
:: GLIB_000:def 54
for n being Nat holds F.n is _Graph;
attr F is halting means
:: GLIB_000:def 55
ex n being Nat st F.n = F.(n+1);
end;
definition
let F be ManySortedSet of NAT;
func F.Lifespan() -> Element of NAT means
:: GLIB_000:def 56
F.it = F.(it+1) & for n being Nat
st F.n = F.(n+1) holds it <= n if F is halting otherwise it = 0;
end;
definition
let F be ManySortedSet of NAT;
func F.Result() -> set equals
:: GLIB_000:def 57
F.(F.Lifespan());
end;
registration
cluster empty -> Graph-yielding for Function;
end;
registration
let G be _Graph;
cluster NAT --> G -> Graph-yielding;
end;
registration
cluster Graph-yielding for ManySortedSet of NAT;
end;
definition
mode GraphSeq is Graph-yielding ManySortedSet of NAT;
end;
registration
cluster -> non empty for GraphSeq;
end;
registration
cluster non empty Graph-yielding for Function;
end;
registration
let GF be non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> Function-like Relation-like;
end;
registration
let GSq be GraphSeq, x be Nat;
cluster GSq.x -> Function-like Relation-like;
end;
registration
let GF be non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> NAT -defined finite;
end;
registration
let GSq be GraphSeq, x be Nat;
cluster GSq.x -> NAT -defined finite;
end;
registration
let GF be non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> [Graph-like];
end;
registration
let GSq be GraphSeq, x be Nat;
cluster GSq.x -> [Graph-like];
end;
definition
let GF be Graph-yielding Function;
attr GF is _finite means
:: GLIB_000:def 58
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is _finite;
attr GF is loopless means
:: GLIB_000:def 59
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is loopless;
attr GF is _trivial means
:: GLIB_000:def 60
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is _trivial;
attr GF is non-trivial means
:: GLIB_000:def 61
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is non _trivial;
attr GF is non-multi means
:: GLIB_000:def 62
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is non-multi;
attr GF is non-Dmulti means
:: GLIB_000:def 63
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is non-Dmulti;
attr GF is simple means
:: GLIB_000:def 64
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is simple;
attr GF is Dsimple means
:: GLIB_000:def 65
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is Dsimple;
end;
registration
cluster empty -> _finite loopless _trivial non-trivial non-multi
non-Dmulti simple Dsimple for Graph-yielding Function;
end;
definition
let GF be non empty Graph-yielding Function;
redefine attr GF is _finite means
:: GLIB_000:def 66
for x being Element of dom GF holds GF.x is _finite;
redefine attr GF is loopless means
:: GLIB_000:def 67
for x being Element of dom GF holds GF.x is loopless;
redefine attr GF is _trivial means
:: GLIB_000:def 68
for x being Element of dom GF holds GF.x is _trivial;
redefine attr GF is non-trivial means
:: GLIB_000:def 69
for x being Element of dom GF holds GF.x is non _trivial;
redefine attr GF is non-multi means
:: GLIB_000:def 70
for x being Element of dom GF holds GF.x is non-multi;
redefine attr GF is non-Dmulti means
:: GLIB_000:def 71
for x being Element of dom GF holds GF.x is non-Dmulti;
redefine attr GF is simple means
:: GLIB_000:def 72
for x being Element of dom GF holds GF.x is simple;
redefine attr GF is Dsimple means
:: GLIB_000:def 73
for x being Element of dom GF holds GF.x is Dsimple;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is _finite means
:: GLIB_000:def 74
for x being Nat holds GSq.x is _finite;
redefine attr GSq is loopless means
:: GLIB_000:def 75
for x being Nat holds GSq.x is loopless;
redefine attr GSq is _trivial means
:: GLIB_000:def 76
for x being Nat holds GSq.x is _trivial;
redefine attr GSq is non-trivial means
:: GLIB_000:def 77
for x being Nat holds GSq.x is non _trivial;
redefine attr GSq is non-multi means
:: GLIB_000:def 78
for x being Nat holds GSq.x is non-multi;
redefine attr GSq is non-Dmulti means
:: GLIB_000:def 79
for x being Nat holds GSq.x is non-Dmulti;
redefine attr GSq is simple means
:: GLIB_000:def 80
for x being Nat holds GSq.x is simple;
redefine attr GSq is Dsimple means
:: GLIB_000:def 81
for x being Nat holds GSq.x is Dsimple;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is halting means
:: GLIB_000:def 82
ex n being Nat st GSq.n = GSq.(n+1);
end;
registration
cluster halting _finite loopless _trivial non-multi non-Dmulti
simple Dsimple for GraphSeq;
cluster halting _finite loopless non-trivial non-multi non-Dmulti simple
Dsimple for GraphSeq;
end;
registration
let GF be _finite non empty Graph-yielding Function,
x be Element of dom GF;
cluster GF.x -> _finite;
end;
registration
let GSq be _finite GraphSeq, x be Nat;
cluster GSq.x -> _finite;
end;
registration
let GF be loopless non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> loopless;
end;
registration
let GSq be loopless GraphSeq, x be Nat;
cluster GSq.x -> loopless for _Graph;
end;
registration
let GF be _trivial non empty Graph-yielding Function,
x be Element of dom GF;
cluster GF.x -> _trivial;
end;
registration
let GSq be _trivial GraphSeq, x be Nat;
cluster GSq.x -> _trivial for _Graph;
end;
registration
let GF be non-trivial non empty Graph-yielding Function;
let x be Element of dom GF;
cluster GF.x -> non _trivial;
end;
registration
let GSq be non-trivial GraphSeq, x be Nat;
cluster GSq.x -> non _trivial for _Graph;
end;
registration
let GF be non-multi non empty Graph-yielding Function;
let x be Element of dom GF;
cluster GF.x -> non-multi;
end;
registration
let GSq be non-multi GraphSeq, x be Nat;
cluster GSq.x -> non-multi for _Graph;
end;
registration
let GF be non-Dmulti non empty Graph-yielding Function;
let x be Element of dom GF;
cluster GF.x -> non-Dmulti;
end;
registration
let GSq be non-Dmulti GraphSeq, x be Nat;
cluster GSq.x -> non-Dmulti for _Graph;
end;
registration
let GF be simple non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> simple;
end;
registration
let GSq be simple GraphSeq, x be Nat;
cluster GSq.x -> simple for _Graph;
end;
registration
let GF be Dsimple non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> Dsimple;
end;
registration
let GSq be Dsimple GraphSeq, x be Nat;
cluster GSq.x -> Dsimple for _Graph;
end;
registration
cluster non-multi -> non-Dmulti for Graph-yielding Function;
end;
registration
cluster simple -> loopless non-multi for Graph-yielding Function;
end;
registration
cluster loopless non-multi -> simple for Graph-yielding Function;
end;
registration
cluster loopless non-Dmulti -> Dsimple for Graph-yielding Function;
end;
registration
cluster Dsimple -> loopless non-Dmulti for Graph-yielding Function;
end;
registration
cluster _trivial loopless -> _finite for Graph-yielding Function;
end;
registration
cluster _trivial non-Dmulti -> _finite for Graph-yielding Function;
end;
begin :: Theorems
reserve GS for GraphStruct;
reserve G,G1,G2,G3 for _Graph;
reserve e,x,x1,x2,y,y1,y2,E,V,X,Y for set;
reserve n,n1,n2 for Nat;
reserve v,v1,v2 for Vertex of G;
theorem :: GLIB_000:1
VertexSelector = 1 & EdgeSelector = 2 & SourceSelector = 3 &
TargetSelector = 4;
theorem :: GLIB_000:2
_GraphSelectors c= dom G;
theorem :: GLIB_000:3
the_Vertices_of GS = GS.VertexSelector & the_Edges_of GS = GS.
EdgeSelector & the_Source_of GS = GS.SourceSelector & the_Target_of GS = GS.
TargetSelector;
theorem :: GLIB_000:4
dom (the_Source_of G) = the_Edges_of G & dom (the_Target_of G) =
the_Edges_of G & rng (the_Source_of G) c= the_Vertices_of G & rng (
the_Target_of G) c= the_Vertices_of G;
theorem :: GLIB_000:5
GS is [Graph-like] iff _GraphSelectors c= dom GS & the_Vertices_of GS
is non empty & the_Source_of GS is Function of the_Edges_of GS,the_Vertices_of
GS & the_Target_of GS is Function of the_Edges_of GS,the_Vertices_of GS;
theorem :: GLIB_000:6 ::: obsolete as reductions are added
for V being non empty set, E being set, S,T being Function of E,V holds
the_Vertices_of createGraph(V,E,S,T) = V &
the_Edges_of createGraph(V,E,S,T) = E &
the_Source_of createGraph(V,E,S,T) = S &
the_Target_of createGraph(V,E,S,T) = T;
registration
let V be non empty set, E be set, S,T be Function of E,V;
reduce the_Vertices_of createGraph(V,E,S,T) to V;
reduce the_Edges_of createGraph(V,E,S,T) to E;
reduce the_Source_of createGraph(V,E,S,T) to S;
reduce the_Target_of createGraph(V,E,S,T) to T;
end;
theorem :: GLIB_000:7
dom GS.set(n,x) = dom GS \/ {n};
theorem :: GLIB_000:8
GS.set(n,x).n = x;
theorem :: GLIB_000:9
n1 <> n2 implies GS.n2 = GS.set(n1,x).n2;
theorem :: GLIB_000:10
not n in _GraphSelectors implies the_Vertices_of G = the_Vertices_of G
.set(n,x) & the_Edges_of G = the_Edges_of G.set(n,x) & the_Source_of G =
the_Source_of G.set(n,x) & the_Target_of G = the_Target_of G.set(n,x) & G.set(n
,x) is _Graph;
theorem :: GLIB_000:11
the_Vertices_of GS.set(VertexSelector,x) = x & the_Edges_of GS.set(
EdgeSelector,x) = x & the_Source_of GS.set(SourceSelector,x) = x &
the_Target_of GS.set(TargetSelector,x) = x;
theorem :: GLIB_000:12
n1 <> n2 implies n1 in dom GS.set(n1,x).set(n2,y) & n2 in dom GS.set(
n1,x).set(n2,y) & GS.set(n1,x).set(n2,y).n1 = x & GS.set(n1,x).set(n2,y).n2 = y
;
theorem :: GLIB_000:13
for e,x,y being object holds
e Joins x,y,G implies x in the_Vertices_of G & y in the_Vertices_of G;
theorem :: GLIB_000:14
for e,x,y being object holds
e Joins x,y,G implies e Joins y,x,G;
theorem :: GLIB_000:15
for e,x1,x2,y1,y2 being object holds
e Joins x1,y1,G & e Joins x2,y2,G implies x1 = x2 & y1 = y2 or x1 = y2
& y1 = x2;
theorem :: GLIB_000:16
for e,x,y being object holds
e Joins x,y,G iff (e DJoins x,y,G or e DJoins y,x,G);
theorem :: GLIB_000:17
for e,x,y being object st
e Joins x,y,G & ( x in X & y in Y or x in Y & y in X ) holds
e SJoins X,Y,G;
theorem :: GLIB_000:18
G is loopless iff for v being object holds
not ex e being object st e Joins v,v,G;
theorem :: GLIB_000:19
for G being loopless _Graph, v being Vertex of G holds
v.degree() = card v.edgesInOut();
theorem :: GLIB_000:20
for G being non _trivial _Graph, v being Vertex of G holds
(the_Vertices_of G) \ {v} is non empty;
theorem :: GLIB_000:21
for G being non _trivial _Graph holds ex v1, v2 being Vertex of G st v1 <> v2
;
theorem :: GLIB_000:22
for G being _trivial _Graph holds ex v being Vertex of G st
the_Vertices_of G = {v};
theorem :: GLIB_000:23
for G being _trivial loopless _Graph holds the_Edges_of G = {};
theorem :: GLIB_000:24
the_Edges_of G = {} implies G is simple;
theorem :: GLIB_000:25
for G being _finite _Graph holds G.order() >= 1;
theorem :: GLIB_000:26
for G being _Graph holds G.order() = 1 iff G is _trivial;
theorem :: GLIB_000:27
for G being _Graph holds G.order() = 1 iff ex v being Vertex of
G st the_Vertices_of G = {v};
theorem :: GLIB_000:28
e in the_Edges_of G & ((the_Source_of G).e in X or
(the_Target_of G).e in X) iff e in G.edgesInOut(X);
theorem :: GLIB_000:29
G.edgesInto(X) c= G.edgesInOut(X) & G.edgesOutOf(X) c= G.edgesInOut(X);
theorem :: GLIB_000:30
the_Edges_of G = G.edgesInOut(the_Vertices_of G);
theorem :: GLIB_000:31
e in the_Edges_of G & (the_Source_of G).e in X & (the_Target_of G).e
in X iff e in G.edgesBetween(X);
theorem :: GLIB_000:32
for e,x,y being object holds
x in X & y in X & e Joins x,y,G implies e in G.edgesBetween(X);
theorem :: GLIB_000:33
G.edgesBetween(X) c= G.edgesInOut(X);
theorem :: GLIB_000:34
the_Edges_of G = G.edgesBetween(the_Vertices_of G);
theorem :: GLIB_000:35
(the_Edges_of G) \ (G.edgesInOut(X)) = G.edgesBetween( (
the_Vertices_of G) \ X);
theorem :: GLIB_000:36
X c= Y implies G.edgesBetween(X) c= G.edgesBetween(Y);
theorem :: GLIB_000:37
for G being _Graph, X1,X2,Y1,Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G.edgesBetween(X1,Y1) c= G.edgesBetween(X2,Y2);
theorem :: GLIB_000:38
for G being _Graph, X1,X2,Y1,Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G.edgesDBetween(X1,Y1) c= G.edgesDBetween(X2,Y2);
theorem :: GLIB_000:39
for G being _Graph, v being Vertex of G holds v.edgesIn() = G
.edgesDBetween(the_Vertices_of G, {v}) & v.edgesOut() = G.edgesDBetween({v},
the_Vertices_of G);
theorem :: GLIB_000:40
G is Subgraph of G;
theorem :: GLIB_000:41
G1 is Subgraph of G2 & G2 is Subgraph of G1 iff the_Vertices_of
G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1
= the_Source_of G2 & the_Target_of G1 = the_Target_of G2;
theorem :: GLIB_000:42
for G1 being _Graph, G2 being Subgraph of G1, x being set holds (x in
the_Vertices_of G2 implies x in the_Vertices_of G1) & (x in the_Edges_of G2
implies x in the_Edges_of G1);
theorem :: GLIB_000:43
for G1 being _Graph, G2 being Subgraph of G1, G3 being Subgraph
of G2 holds G3 is Subgraph of G1;
theorem :: GLIB_000:44
for G being _Graph, G1, G2 being Subgraph of G st
the_Vertices_of G1 c= the_Vertices_of G2 & the_Edges_of G1 c= the_Edges_of G2
holds G1 is Subgraph of G2;
theorem :: GLIB_000:45
for G1 being _Graph, G2 being Subgraph of G1 holds the_Source_of
G2 = (the_Source_of G1) | the_Edges_of G2 & the_Target_of G2 = (the_Target_of
G1) | the_Edges_of G2;
theorem :: GLIB_000:46
for G being _Graph, V1,V2,E1,E2 being set, G1 being inducedSubgraph of
G,V1,E1, G2 being inducedSubgraph of G,V2,E2 st V2 c= V1 & E2 c= E1 & V2 is non
empty Subset of the_Vertices_of G & E2 c= G.edgesBetween(V2) holds G2 is
Subgraph of G1;
theorem :: GLIB_000:47
for G1 being non _trivial _Graph, v being Vertex of G1, G2 being
removeVertex of G1,v holds the_Vertices_of G2 = the_Vertices_of G1 \ {v} &
the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ {v});
theorem :: GLIB_000:48
for G1 being _finite non _trivial _Graph, v being Vertex of G1, G2 being
removeVertex of G1,v holds G2.order() + 1 = G1.order() & G2.size() + card v
.edgesInOut() = G1.size();
theorem :: GLIB_000:49
for G1 being _Graph, V being set, G2 being removeVertices of G1,
V st V c< the_Vertices_of G1 holds the_Vertices_of G2 = the_Vertices_of G1 \ V
& the_Edges_of G2 = G1.edgesBetween(the_Vertices_of G1 \ V);
theorem :: GLIB_000:50
for G1 being _finite _Graph, V being Subset of the_Vertices_of G1, G2
being removeVertices of G1,V st V <> the_Vertices_of G1 holds G2.order() + card
V = G1.order() & G2.size() + card G1.edgesInOut(V) = G1.size();
theorem :: GLIB_000:51
for G1 being _Graph, e being set, G2 being removeEdge of G1,e
holds the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of
G1 \ {e};
theorem :: GLIB_000:52
for G1 being _finite _Graph, e being set, G2 being removeEdge of G1,e
holds G1.order() = G2.order() & (e in the_Edges_of G1 implies G2.size() + 1 =
G1.size());
theorem :: GLIB_000:53
for G1 being _Graph, E being set, G2 being removeEdges of G1,E
holds the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 = the_Edges_of
G1 \ E;
theorem :: GLIB_000:54
for G1 being _Graph, E being set, G2 being removeEdges of G1,E
holds G1.order() = G2.order();
theorem :: GLIB_000:55
for G1 being _finite _Graph, E being Subset of the_Edges_of G1, G2
being removeEdges of G1,E holds G2.size() + card E = G1.size();
theorem :: GLIB_000:56
e in v.edgesIn() iff e in the_Edges_of G & (the_Target_of G).e = v;
theorem :: GLIB_000:57
e in v.edgesIn() iff ex x being set st e DJoins x,v,G;
theorem :: GLIB_000:58
e in v.edgesOut() iff e in the_Edges_of G & (the_Source_of G).e = v;
theorem :: GLIB_000:59
e in v.edgesOut() iff ex x being set st e DJoins v,x,G;
theorem :: GLIB_000:60
v.edgesInOut() = v.edgesIn() \/ v.edgesOut();
theorem :: GLIB_000:61
e in v.edgesInOut() iff e in the_Edges_of G & ((the_Source_of G)
.e = v or (the_Target_of G).e = v);
theorem :: GLIB_000:62
for e,x being object holds
e Joins v1,x,G implies e in v1.edgesInOut();
theorem :: GLIB_000:63
e Joins v1,v2,G implies e in v1.edgesIn() & e in v2.edgesOut()
or e in v2.edgesIn() & e in v1.edgesOut();
theorem :: GLIB_000:64
e in v1.edgesInOut() iff ex v2 being Vertex of G st e Joins v1,v2,G;
theorem :: GLIB_000:65
for e,x,y being object holds
e in v.edgesInOut() & e Joins x,y,G implies v = x or v = y;
theorem :: GLIB_000:66
for e being object holds
e Joins v1,v2,G implies v1.adj(e) = v2 & v2.adj(e) = v1;
theorem :: GLIB_000:67
e in v.edgesInOut() iff e Joins v,v.adj(e),G;
theorem :: GLIB_000:68
for G being _finite _Graph, e being set, v1,v2 being Vertex of G holds
e Joins v1,v2,G implies 1 <= v1.degree() & 1 <= v2.degree();
theorem :: GLIB_000:69
x in v.inNeighbors() iff ex e being object st e DJoins x,v,G;
theorem :: GLIB_000:70
x in v.outNeighbors() iff ex e being object st e DJoins v,x,G;
theorem :: GLIB_000:71
x in v.allNeighbors() iff ex e being object st e Joins v,x,G;
theorem :: GLIB_000:72
for G1 being _Graph, G2 being Subgraph of G1,
x,y being set, e being object
holds (e Joins x,y,G2 implies e Joins x,y,G1) & (e DJoins x,y,G2 implies e
DJoins x,y,G1) & (e SJoins x,y,G2 implies e SJoins x,y,G1) & (e DSJoins x,y,G2
implies e DSJoins x,y,G1);
theorem :: GLIB_000:73
for G1 being _Graph, G2 being Subgraph of G1, x,y,e being set st e in
the_Edges_of G2 holds (e Joins x,y,G1 implies e Joins x,y,G2) & (e DJoins x,y,
G1 implies e DJoins x,y,G2) & (e SJoins x,y,G1 implies e SJoins x,y,G2) & (e
DSJoins x,y,G1 implies e DSJoins x,y,G2);
theorem :: GLIB_000:74
for G1 being _Graph, G2 being spanning Subgraph of G1, G3 being
spanning Subgraph of G2 holds G3 is spanning Subgraph of G1;
theorem :: GLIB_000:75
for G1 being _finite _Graph, G2 being Subgraph of G1 holds G2.order()
<= G1.order() & G2.size() <= G1.size();
theorem :: GLIB_000:76
for G1 being _Graph, G2 being Subgraph of G1, X being set holds G2
.edgesInto(X) c= G1.edgesInto(X) & G2.edgesOutOf(X) c= G1.edgesOutOf(X) & G2
.edgesInOut(X) c= G1.edgesInOut(X) & G2.edgesBetween(X) c= G1.edgesBetween(X)
;
theorem :: GLIB_000:77
for G1 being _Graph, G2 being Subgraph of G1, X,Y being set holds G2
.edgesBetween(X,Y) c= G1.edgesBetween(X,Y) & G2.edgesDBetween(X,Y) c= G1
.edgesDBetween(X,Y);
theorem :: GLIB_000:78
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of
G1, v2 being Vertex of G2 st v1 = v2 holds v2.edgesIn() c= v1.edgesIn() & v2
.edgesOut() c= v1.edgesOut() & v2.edgesInOut() c= v1.edgesInOut();
theorem :: GLIB_000:79
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of
G1, v2 being Vertex of G2 st v1 = v2 holds v2.edgesIn() = v1.edgesIn() /\ (
the_Edges_of G2) & v2.edgesOut() = v1.edgesOut() /\ (the_Edges_of G2) & v2
.edgesInOut() = v1.edgesInOut() /\ (the_Edges_of G2);
theorem :: GLIB_000:80
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2, e being set st v1 = v2 & e in the_Edges_of G2 holds v1
.adj(e) = v2.adj(e);
theorem :: GLIB_000:81
for G1 being _finite _Graph, G2 being Subgraph of G1, v1 being Vertex
of G1, v2 being Vertex of G2 st v1 = v2 holds v2.inDegree() <= v1.inDegree() &
v2.outDegree() <= v1.outDegree() & v2.degree() <= v1.degree();
theorem :: GLIB_000:82
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 holds v2.inNeighbors() c= v1.inNeighbors() &
v2.outNeighbors() c= v1.outNeighbors() & v2.allNeighbors() c= v1.allNeighbors()
;
theorem :: GLIB_000:83
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2 is isolated;
theorem :: GLIB_000:84
for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds v2 is endvertex or v2
is isolated;
theorem :: GLIB_000:85
G1 == G2 & G2 == G3 implies G1 == G3;
theorem :: GLIB_000:86
for G being _Graph, G1,G2 being Subgraph of G st the_Vertices_of
G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 holds G1 == G2;
theorem :: GLIB_000:87
G1 == G2 iff G1 is Subgraph of G2 & G2 is Subgraph of G1;
theorem :: GLIB_000:88
for e,x,y being object holds
G1 == G2 implies (e Joins x,y,G1 implies e Joins x,y,G2) & (e
DJoins x,y,G1 implies e DJoins x,y,G2) & (e SJoins X,Y,G1 implies e SJoins X,Y,
G2) & (e DSJoins X,Y,G1 implies e DSJoins X,Y,G2);
theorem :: GLIB_000:89
G1 == G2 implies (G1 is _finite implies G2 is _finite) &
(G1 is loopless implies G2 is loopless) &
(G1 is _trivial implies G2 is _trivial) &
(G1 is non-multi implies G2 is non-multi) &
(G1 is non-Dmulti implies G2 is non-Dmulti) &
(G1 is simple implies G2 is simple) &
(G1 is Dsimple implies G2 is Dsimple);
theorem :: GLIB_000:90
G1 == G2 implies G1.order() = G2.order() & G1.size() = G2.size()
& G1.edgesInto(X) = G2.edgesInto(X) & G1.edgesOutOf(X) = G2.edgesOutOf(X) & G1
.edgesInOut(X) = G2.edgesInOut(X) & G1.edgesBetween(X) = G2.edgesBetween(X) &
G1.edgesDBetween(X,Y) = G2.edgesDBetween(X,Y);
theorem :: GLIB_000:91
G1 == G2 & G3 is Subgraph of G1 implies G3 is Subgraph of G2;
theorem :: GLIB_000:92
G1 == G2 & G1 is Subgraph of G3 implies G2 is Subgraph of G3;
theorem :: GLIB_000:93
for G1,G2 being inducedSubgraph of G,V,E holds G1 == G2;
theorem :: GLIB_000:94
for G1 being _Graph, G2 being inducedSubgraph of G1,the_Vertices_of G1
holds G1 == G2;
theorem :: GLIB_000:95
for G1,G2 being _Graph, V,E being set, G3 being inducedSubgraph of G1,
V,E st G1 == G2 holds G3 is inducedSubgraph of G2,V,E;
theorem :: GLIB_000:96
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & G1
== G2 holds v1.edgesIn() = v2.edgesIn() & v1.edgesOut() = v2.edgesOut() & v1
.edgesInOut() = v2.edgesInOut() & v1.adj(e) = v2.adj(e) & v1.inDegree() = v2
.inDegree() & v1.outDegree() = v2.outDegree() & v1.degree() = v2.degree() & v1
.inNeighbors() = v2.inNeighbors() & v1.outNeighbors() = v2.outNeighbors() & v1
.allNeighbors() = v2.allNeighbors();
theorem :: GLIB_000:97
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & G1 == G2
holds (v1 is isolated implies v2 is isolated) & (v1 is endvertex implies v2 is
endvertex);
theorem :: GLIB_000:98
for G being _Graph, G1,G2 being Subgraph of G st G1 c< G2 holds
(the_Vertices_of G1 c< the_Vertices_of G2 or the_Edges_of G1 c< the_Edges_of G2
);
theorem :: GLIB_000:99
for G being _Graph, G1,G2 being Subgraph of G st G1 c< G2 holds (ex v
being object st v in the_Vertices_of G2 & not v in the_Vertices_of G1) or
ex e being object st e in the_Edges_of G2 & not e in the_Edges_of G1;