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