:: About Graph Complements :: by Sebastian Koch :: :: Received December 30, 2019 :: Copyright (c) 2019-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, 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, RING_3, PARTFUN1, FUNCT_2, CHORD, SCMYCIEL, REWRITE1, ARYTM_1, GLIB_006, GLIB_007, GLIB_009, GLIB_010, GLIB_011, GLIB_012, MCART_1, WAYBEL_0, MOD_4, RELAT_2, GRAPH_1, GLIB_001, ORDINAL4, ABIAN, SGRAPH1, RFINSEQ, FINSEQ_8, GRAPH_2; notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, ENUMSET1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, VALUED_0, NAT_D, CARD_2, FINSEQ_1, NEWTON, ABIAN, RFINSEQ, FINSEQ_6, FINSEQ_8, GRAPH_2, GLIB_000, GLIB_001, GLIB_002, CHORD, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIB_011; constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2, FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000, NEWTON, XTUPLE_0, CHORD, GLIB_002, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIB_011, GLIB_001, ABIAN, BINOP_1, FINSOP_1, RVSUM_1, FINSEQ_5, GRAPH_5, FUNCT_2, FIB_NUM2, FINSEQ_8, HELLY, FUNCT_3, GRAPH_2, RFINSEQ, FINSEQ_6, FUNCT_7, FINSEQ_1, SUBSET_1, RELAT_1, ENUMSET1, ORDINAL1, INT_1, XREAL_0, XCMPLX_0, FINSET_1, CARD_3, FUNCT_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, RELSET_1, GLIB_000, CHORD, GLIB_006, GLIB_007, GLIB_009, GLIB_008, GLIB_010, GLIB_011, XTUPLE_0, ABIAN, GLIB_001, MEMBERED, INT_1, MSAFREE5; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin :: Loopfull Graphs definition let G be _Graph; attr G is loopfull means :: GLIB_012:def 1 :: or reflexive for v being Vertex of G ex e being object st e Joins v,v,G; end; theorem :: GLIB_012:1 for G being _Graph holds G is loopfull iff for v being Vertex of G ex e being object st e DJoins v,v,G; theorem :: GLIB_012:2 for G being _Graph holds G is loopfull iff for v being Vertex of G holds v,v are_adjacent; registration cluster loopfull -> non loopless for _Graph; cluster _trivial non loopless -> loopfull for _Graph; cluster loopfull complete for _Graph; cluster non loopfull for _Graph; end; theorem :: GLIB_012:3 for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E holds G1 is loopfull iff G2 is loopfull; registration let G be loopfull _Graph, E be set; cluster -> loopfull for reverseEdgeDirections of G, E; end; registration let G be non loopfull _Graph, E be set; cluster -> non loopfull for reverseEdgeDirections of G, E; end; theorem :: GLIB_012:4 for G1, G2 being _Graph st G1 == G2 holds G1 is loopfull implies G2 is loopfull; theorem :: GLIB_012:5 for G2 being loopfull _Graph, G1 being Supergraph of G2 st the_Vertices_of G1 = the_Vertices_of G2 holds G1 is loopfull; theorem :: GLIB_012:6 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st rng F_V = the_Vertices_of G2 & G1.loops() c= dom F_E holds G1 is loopfull implies G2 is loopfull; theorem :: GLIB_012:7 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is total onto holds G1 is loopfull implies G2 is loopfull; theorem :: GLIB_012:8 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is semi-continuous & dom F_V=the_Vertices_of G1 & G2.loops() c= rng F_E holds G2 is loopfull implies G1 is loopfull; theorem :: GLIB_012:9 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is total onto semi-continuous holds G2 is loopfull implies G1 is loopfull; theorem :: GLIB_012:10 for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is isomorphism holds G1 is loopfull iff G2 is loopfull; registration let G be loopfull _Graph, V be set; cluster -> loopfull for inducedSubgraph of G, V; cluster -> loopfull for removeVertices of G, V; cluster -> loopfull for removeVertex of G, V; end; registration let G be non loopfull _Graph; cluster -> non loopfull for spanning Subgraph of G; let E be set; cluster -> non loopfull for inducedSubgraph of G, the_Vertices_of G, E; cluster -> non loopfull for removeEdges of G, E; cluster -> non loopfull for removeEdge of G, E; end; theorem :: GLIB_012:11 for G2 being _Graph, V being set, G1 being addVertices of G2, V st V \ the_Vertices_of G2 <> {} holds G1 is non loopfull; registration let G be non loopfull _Graph, V be set; cluster -> non loopfull for addVertices of G, V; end; registration let G be loopfull _Graph, v,e,w be object; cluster -> loopfull for addEdge of G,v,e,w; end; theorem :: GLIB_012:12 for G2 being _Graph, v being Vertex of G2, e,w being object for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds G1 is non loopfull; theorem :: GLIB_012:13 for G2 being _Graph, v,e being object, w being Vertex of G2 for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds G1 is non loopfull; registration let G be non loopfull _Graph, v,e,w be object; cluster -> non loopfull for addAdjVertex of G,v,e,w; end; theorem :: GLIB_012:14 for G2 being _Graph, v being object, V being Subset of the_Vertices_of G2 for G1 being addAdjVertexAll of G2,v,V st not v in the_Vertices_of G2 holds G1 is non loopfull; registration let G be non loopfull _Graph, v be object, V be set; cluster -> non loopfull for addAdjVertexAll of G,v,V; end; registration let G be loopfull _Graph; cluster -> loopfull for removeParallelEdges of G; cluster -> loopfull for removeDParallelEdges of G; end; :: removeLoops is loopless, hence non loopfull registration let G be non loopfull _Graph; cluster -> non loopfull for removeParallelEdges of G; cluster -> non loopfull for removeDParallelEdges of G; end; definition let GF be Graph-yielding Function; attr GF is loopfull means :: GLIB_012:def 2 for x being object st x in dom GF ex G being _Graph st GF.x = G & G is loopfull; end; registration let G be loopfull _Graph; cluster <* G *> -> loopfull; cluster NAT --> G -> loopfull; end; definition let GF be non empty Graph-yielding Function; redefine attr GF is loopfull means :: GLIB_012:def 3 for x being Element of dom GF holds GF.x is loopfull; end; definition let GSq be GraphSeq; redefine attr GSq is loopfull means :: GLIB_012:def 4 for n being Nat holds GSq.n is loopfull; end; registration cluster empty -> loopfull for Graph-yielding Function; cluster non empty loopfull -> non loopless for Graph-yielding Function; end; registration cluster loopfull for GraphSeq; cluster non empty loopfull for Graph-yielding FinSequence; end; registration let GF be loopfull non empty Graph-yielding Function, x be Element of dom GF; cluster GF.x -> loopfull; end; registration let GSq be loopfull GraphSeq, x be Nat; cluster GSq.x -> loopfull; end; registration let p be loopfull Graph-yielding FinSequence, n be Nat; cluster p | n -> loopfull; cluster p /^ n -> loopfull; let m be Nat; cluster smid(p,m,n) -> loopfull; cluster (m,n)-cut p -> loopfull; end; registration let p, q be loopfull Graph-yielding FinSequence; cluster p ^ q -> loopfull; cluster p ^' q -> loopfull; end; registration let G1, G2 be loopfull _Graph; cluster <* G1, G2 *> -> loopfull; let G3 be loopfull _Graph; cluster <* G1, G2, G3 *> -> loopfull; end; begin :: Adding Loops to a Graph :: a loop is added to each vertex in V, regardless if that :: vertex has a loop already or not definition let G be _Graph, V be set; mode addLoops of G, V -> Supergraph of G means :: GLIB_012:def 5 the_Vertices_of it = the_Vertices_of G & ex E being set, f being one-to-one Function st E misses the_Edges_of G & the_Edges_of it = the_Edges_of G \/ E & dom f = E & rng f = V & the_Source_of it = the_Source_of G +* f & the_Target_of it = the_Target_of G +* f if V c= the_Vertices_of G otherwise it == G; end; definition let G be _Graph; mode addLoops of G is addLoops of G, the_Vertices_of G; end; theorem :: GLIB_012:15 for G2 being _Graph, V being set, G1 being addLoops of G2, V holds the_Vertices_of G1 = the_Vertices_of G2; theorem :: GLIB_012:16 for G2 being _Graph, V being set, G1 being addLoops of G2, V for e,v,w being object st v <> w holds e DJoins v,w,G1 iff e DJoins v,w,G2; theorem :: GLIB_012:17 for G2 being _Graph, V being set, G1 being addLoops of G2, V for e,v,w being object st v <> w holds e Joins v,w,G1 iff e Joins v,w,G2; theorem :: GLIB_012:18 for G2 being _Graph, V being Subset of the_Vertices_of G2 for G1 being addLoops of G2, V for v being Vertex of G1 st v in V holds v,v are_adjacent; theorem :: GLIB_012:19 for G2 being _Graph, V being set for G1 being addLoops of G2, V holds G1.order() = G2.order(); theorem :: GLIB_012:20 for G2 being _Graph, V being Subset of the_Vertices_of G2 for G1 being addLoops of G2, V holds G1.size() = G2.size() +` card V; theorem :: GLIB_012:21 for G1, G2 being _Graph holds G1 is addLoops of G2, {} iff G1 == G2; theorem :: GLIB_012:22 for G being _Graph holds G is addLoops of G, {}; theorem :: GLIB_012:23 for G being _Graph, V1, V2 being Subset of the_Vertices_of G for G1 being addLoops of G, V1, G2 being addLoops of G1, V2 st V1 misses V2 holds G2 is addLoops of G, V1 \/ V2; theorem :: GLIB_012:24 for G3 being _Graph, V1, V2 being Subset of the_Vertices_of G3 for G1 being addLoops of G3, V1 \/ V2 st V1 misses V2 ex G2 being addLoops of G3, V1 st G1 is addLoops of G2, V2; theorem :: GLIB_012:25 for G2 being loopless _Graph, V being Subset of the_Vertices_of G2 for G1 being addLoops of G2, V holds the_Edges_of G2 misses G1.loops() & the_Edges_of G1 = the_Edges_of G2 \/ G1.loops(); theorem :: GLIB_012:26 for G1 being loopless _Graph, V being set for G2 being addLoops of G1, V, G3 being removeLoops of G2 holds G1 == G3; theorem :: GLIB_012:27 for G1, G2 being _Graph, v being Vertex of G2 holds G1 is addLoops of G2, {v} iff ex e being object st not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v; :: finite addition of loops can be finitely constructed with one loop at a time theorem :: GLIB_012:28 for G2 being _Graph, V being finite Subset of the_Vertices_of G2 for G1 being addLoops of G2, V ex p being non empty Graph-yielding FinSequence st p.1 == G2 & p.len p = G1 & len p = card V + 1 & for n being Element of dom p st n <= len p - 1 holds ex v being Vertex of G2, e being object st p.(n+1) is addEdge of p.n, v,e,v & v in V & not e in the_Edges_of p.n; theorem :: GLIB_012:29 for G3, G4 being _Graph, V1, V2 being set for G1 being addLoops of G3, V1, G2 being addLoops of G4, V2 for F0 being PGraphMapping of G3, G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & F0_V | V1 is one-to-one & dom(F0_V | V1) = V1 & rng(F0_V | V1) = V2 ex F being PGraphMapping of G1, G2 st F_V = F0_V & F_E | dom F0_E = F0_E & (F0 is non empty implies F is non empty) & (F0 is total implies F is total) & (F0 is onto implies F is onto) & (F0 is one-to-one implies F is one-to-one) & (F0 is directed implies F is directed) & (F0 is weak_SG-embedding implies F is weak_SG-embedding) & (F0 is isomorphism implies F is isomorphism) & (F0 is Disomorphism implies F is Disomorphism); theorem :: GLIB_012:30 for G3 being _Graph, G4 being G3-isomorphic _Graph for G1 being addLoops of G3 for G2 being addLoops of G4 holds G2 is G1-isomorphic; theorem :: GLIB_012:31 for G3 being _Graph, G4 being G3-Disomorphic _Graph for G1 being addLoops of G3 for G2 being addLoops of G4 holds G2 is G1-Disomorphic; theorem :: GLIB_012:32 for G3, G4 being _Graph, V being set for G1 being addLoops of G3, V, G2 being addLoops of G4, V st G3 == G4 holds G2 is G1-Disomorphic; theorem :: GLIB_012:33 for G3 being _Graph, V, E being set, G4 being reverseEdgeDirections of G3, E for G1 being addLoops of G3, V, G2 being addLoops of G4, V holds G2 is G1-isomorphic; theorem :: GLIB_012:34 for G3 being _Graph, E, V being set, G4 being reverseEdgeDirections of G3, E for G1 being addLoops of G3, V, G2 being reverseEdgeDirections of G1, E st E c= the_Edges_of G3 holds G2 is addLoops of G4, V; theorem :: GLIB_012:35 for G3 being _Graph, V1 being Subset of the_Vertices_of G3 for V2 being non empty Subset of the_Vertices_of G3 for G4 being inducedSubgraph of G3, V2 for G1 being addLoops of G3, V1, G2 being inducedSubgraph of G1, V2 holds G2 is addLoops of G4, V1 /\ V2; theorem :: GLIB_012:36 for G2 being _Graph, V being set, G1 being addLoops of G2, V for v1 being Vertex of G1, v2 being Vertex of G2 st not v1 in V & v1 = v2 holds (v1 is isolated iff v2 is isolated) & (v1 is endvertex iff v2 is endvertex); theorem :: GLIB_012:37 for G2 being _Graph, V being set, G1 being addLoops of G2, V for P being Path of G1 holds P is Path of G2 or ex v,e being object st e Joins v,v,G1 & P = G1.walkOf(v,e,v); theorem :: GLIB_012:38 for G2 being _Graph, V being set, G1 being addLoops of G2, V for W being Walk of G1 st W.edges() misses G1.loops() \ G2.loops() holds W is Walk of G2; registration let G be _Graph; cluster -> loopfull for addLoops of G; let V be non empty Subset of the_Vertices_of G; cluster -> non loopless for addLoops of G, V; end; theorem :: GLIB_012:39 for G2 being _Graph, V being set, G1 being addLoops of G2, V holds G1 is _finite iff G2 is _finite; registration let G be _finite _Graph, V be set; cluster -> _finite for addLoops of G, V; end; registration let G be non _finite _Graph, V be set; cluster -> non _finite for addLoops of G, V; end; theorem :: GLIB_012:40 for G2 being _Graph, V being set, G1 being addLoops of G2, V holds G1 is connected iff G2 is connected; registration let G be connected _Graph, V be set; cluster -> connected for addLoops of G, V; end; registration let G be non connected _Graph, V be set; cluster -> non connected for addLoops of G, V; end; theorem :: GLIB_012:41 for G2 being _Graph, V being set, G1 being addLoops of G2, V holds G1 is chordal iff G2 is chordal; registration let G be chordal _Graph, V be set; cluster -> chordal for addLoops of G, V; end; :: non chordal clustering will be done later registration let G be non edgeless _Graph, V be set; cluster -> non edgeless for addLoops of G, V; end; registration let G be loopfull _Graph, V be set; cluster -> loopfull for addLoops of G, V; end; registration let G be simple _Graph, V be set; cluster -> non-multi for addLoops of G, V; end; registration let G be Dsimple _Graph, V be set; cluster -> non-Dmulti for addLoops of G, V; end; theorem :: GLIB_012:42 for G2 being _Graph, V being Subset of the_Vertices_of G2 for G1 being addLoops of G2, V, v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & v1 in V ex e being object st e DJoins v1,v1,G1 & not e in the_Edges_of G2 & v1.edgesIn() = v2.edgesIn()\/{e} & v1.edgesOut() = v2.edgesOut()\/{e} & v1.edgesInOut() = v2.edgesInOut() \/ {e}; theorem :: GLIB_012:43 for G2 being _Graph, V being Subset of the_Vertices_of G2 for G1 being addLoops of G2, V, v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & v1 in V holds v1.inDegree() = v2.inDegree() +` 1 & v1.outDegree() = v2.outDegree() +` 1 & v1.degree() = v2.degree() +` 2; theorem :: GLIB_012:44 for G2 being _Graph, V being Subset of the_Vertices_of G2 for G1 being addLoops of G2, V, v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & not v1 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(); begin :: Directed Graph Complement with Loops definition let G be _Graph; mode DLGraphComplement of G -> non-Dmulti _Graph means :: GLIB_012:def 6 the_Vertices_of it = the_Vertices_of G & the_Edges_of it misses the_Edges_of G & for v,w being Vertex of G holds (ex e1 being object st e1 DJoins v,w,G) iff (not ex e2 being object st e2 DJoins v,w,it); end; theorem :: GLIB_012:45 for G1, G2, G3 being _Graph, G4 being DLGraphComplement of G1 st G1 == G2 & G3 == G4 holds G3 is DLGraphComplement of G2; registration let G be _Graph; cluster plain for DLGraphComplement of G; end; theorem :: GLIB_012:46 for G1 being _Graph, G2 being DLGraphComplement of G1, e1,e2,v,w being object holds e1 DJoins v,w,G1 implies not e2 DJoins v,w,G2; theorem :: GLIB_012:47 for G1 being _Graph, G2 being removeDParallelEdges of G1 for G3 being DLGraphComplement of G1 holds G3 is DLGraphComplement of G2; theorem :: GLIB_012:48 for G1, G2 being _Graph for G3 being removeDParallelEdges of G1, G4 being removeDParallelEdges of G2 for G5 being DLGraphComplement of G1, G6 being DLGraphComplement of G2 st G4 is G3-Disomorphic holds G6 is G5-Disomorphic; theorem :: GLIB_012:49 for G1 being _Graph, G2 being G1-Disomorphic _Graph for G3 being DLGraphComplement of G1, G4 being DLGraphComplement of G2 holds G4 is G3-Disomorphic; theorem :: GLIB_012:50 for G1 being _Graph, G2, G3 being DLGraphComplement of G1 holds G3 is G2-Disomorphic; theorem :: GLIB_012:51 for G1 being _Graph, G2 being reverseEdgeDirections of G1 for G3 being DLGraphComplement of G1, G4 being reverseEdgeDirections of G3 holds G4 is DLGraphComplement of G2; theorem :: GLIB_012:52 for G1 being _Graph, V being non empty Subset of the_Vertices_of G1 for G2 being inducedSubgraph of G1, V for G3 being DLGraphComplement of G1, G4 being inducedSubgraph of G3, V holds G4 is DLGraphComplement of G2; theorem :: GLIB_012:53 for G1 being _Graph, V being proper Subset of the_Vertices_of G1 for G2 being removeVertices of G1, V for G3 being DLGraphComplement of G1, G4 being removeVertices of G3, V holds G4 is DLGraphComplement of G2; :: involutiveness of graph complement (DLC case) theorem :: GLIB_012:54 for G1 being non-Dmulti _Graph, G2 being DLGraphComplement of G1 holds G1 is DLGraphComplement of G2; theorem :: GLIB_012:55 for G1 being _Graph, G2 being DLGraphComplement of G1 holds G1.order() = G2.order(); theorem :: GLIB_012:56 for G1 being _Graph, G2 being DLGraphComplement of G1 holds (G1 is _trivial iff G2 is _trivial) & (G1 is loopfull iff G2 is loopless) & (G1 is loopless iff G2 is loopfull); registration let G be _trivial _Graph; cluster -> _trivial for DLGraphComplement of G; end; registration let G be non _trivial _Graph; cluster -> non _trivial for DLGraphComplement of G; end; registration let G be loopfull _Graph; cluster -> loopless for DLGraphComplement of G; end; registration let G be non loopfull _Graph; cluster -> non loopless for DLGraphComplement of G; end; registration let G be loopless _Graph; cluster -> loopfull for DLGraphComplement of G; end; registration let G be non loopless _Graph; cluster -> non loopfull for DLGraphComplement of G; end; theorem :: GLIB_012:57 for G1 being _Graph, G2 being DLGraphComplement of G1 st the_Edges_of G1 = G1.loops() holds G2 is complete; registration let G be edgeless _Graph; cluster -> complete for DLGraphComplement of G; end; registration let G be non connected _Graph; cluster -> connected for DLGraphComplement of G; end; theorem :: GLIB_012:58 for G1 being _Graph, G2 being DLGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds (v1 is isolated implies v2 is non isolated) & (v1 is endvertex implies v2 is non endvertex); theorem :: GLIB_012:59 for G1 being _Graph, G2 being DLGraphComplement of G1 for v,w being Vertex of G1 holds (not ex e being object st e Joins v,w,G1) implies (ex e being object st e Joins v,w,G2); theorem :: GLIB_012:60 for G1 being _Graph, G2 being DLGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds v2.inNeighbors() = the_Vertices_of G2 \ v1.inNeighbors() & v2.outNeighbors() = the_Vertices_of G2 \ v1.outNeighbors(); theorem :: GLIB_012:61 for G1 being _Graph, G2 being DLGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2.inNeighbors() = the_Vertices_of G2 & v2.outNeighbors() = the_Vertices_of G2 & v2.allNeighbors() = the_Vertices_of G2; begin :: Undirected Graph Complement with Loops definition let G be _Graph; mode LGraphComplement of G -> non-multi _Graph means :: GLIB_012:def 7 the_Vertices_of it = the_Vertices_of G & the_Edges_of it misses the_Edges_of G & for v,w being Vertex of G holds (ex e1 being object st e1 Joins v,w,G) iff (not ex e2 being object st e2 Joins v,w,it); end; theorem :: GLIB_012:62 for G1, G2, G3 being _Graph, G4 being LGraphComplement of G1 st G1 == G2 & G3 == G4 holds G3 is LGraphComplement of G2; registration let G be _Graph; cluster plain for LGraphComplement of G; end; theorem :: GLIB_012:63 for G1 being _Graph, G2 being non-multi _Graph holds G2 is LGraphComplement of G1 iff the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2 st v1 = v2 & w1 = w2 holds v1,w1 are_adjacent iff not v2,w2 are_adjacent; theorem :: GLIB_012:64 for G1 being _Graph, G2 being LGraphComplement of G1, e1,e2,v,w being object holds e1 Joins v,w,G1 implies not e2 Joins v,w,G2; theorem :: GLIB_012:65 for G1 being _Graph, G2 being removeParallelEdges of G1 for G3 being LGraphComplement of G1 holds G3 is LGraphComplement of G2; theorem :: GLIB_012:66 for G1, G2 being _Graph for G3 being removeParallelEdges of G1, G4 being removeParallelEdges of G2 for G5 being LGraphComplement of G1, G6 being LGraphComplement of G2 st G4 is G3-isomorphic holds G6 is G5-isomorphic; theorem :: GLIB_012:67 for G1 being _Graph, G2 being G1-isomorphic _Graph for G3 being LGraphComplement of G1, G4 being LGraphComplement of G2 holds G4 is G3-isomorphic; theorem :: GLIB_012:68 for G1 being _Graph, G2, G3 being LGraphComplement of G1 holds G3 is G2-isomorphic; theorem :: GLIB_012:69 for G1 being _Graph, V being non empty Subset of the_Vertices_of G1 for G2 being inducedSubgraph of G1, V for G3 being LGraphComplement of G1, G4 being inducedSubgraph of G3, V holds G4 is LGraphComplement of G2; theorem :: GLIB_012:70 for G1 being _Graph, V being proper Subset of the_Vertices_of G1 for G2 being removeVertices of G1, V for G3 being LGraphComplement of G1, G4 being removeVertices of G3, V holds G4 is LGraphComplement of G2; :: involutiveness of graph complement (LC case) theorem :: GLIB_012:71 for G1 being non-multi _Graph, G2 being LGraphComplement of G1 holds G1 is LGraphComplement of G2; theorem :: GLIB_012:72 for G1 being _Graph, G2 being LGraphComplement of G1 holds G1.order() = G2.order(); theorem :: GLIB_012:73 for G1 being _Graph, G2 being LGraphComplement of G1 holds (G1 is _trivial iff G2 is _trivial) & (G1 is loopfull iff G2 is loopless) & (G1 is loopless iff G2 is loopfull); registration let G be _trivial _Graph; cluster -> _trivial for LGraphComplement of G; end; registration let G be non _trivial _Graph; cluster -> non _trivial for LGraphComplement of G; end; registration let G be loopfull _Graph; cluster -> loopless for LGraphComplement of G; end; registration let G be non loopfull _Graph; cluster -> non loopless for LGraphComplement of G; end; registration let G be loopless _Graph; cluster -> loopfull for LGraphComplement of G; end; registration let G be non loopless _Graph; cluster -> non loopfull for LGraphComplement of G; end; theorem :: GLIB_012:74 for G1 being _Graph, G2 being LGraphComplement of G1 st the_Edges_of G1 = G1.loops() holds G2 is complete; registration let G be edgeless _Graph; cluster -> complete for LGraphComplement of G; end; theorem :: GLIB_012:75 for G1 being complete _Graph, G2 being LGraphComplement of G1 holds the_Edges_of G2 = G2.loops(); registration let G be complete loopfull _Graph; cluster -> edgeless for LGraphComplement of G; end; registration let G be non connected _Graph; cluster -> connected for LGraphComplement of G; end; theorem :: GLIB_012:76 for G1 being _Graph, G2 being LGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds (v1 is isolated implies v2 is non isolated) & (v1 is endvertex implies v2 is non endvertex); theorem :: GLIB_012:77 for G1 being _Graph, G2 being LGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds v2.allNeighbors() = the_Vertices_of G2 \ v1.allNeighbors(); theorem :: GLIB_012:78 for G1 being _Graph, G2 being LGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2.allNeighbors() = the_Vertices_of G2; begin :: Directed Graph Complement without Loops definition let G be _Graph; mode DGraphComplement of G -> Dsimple _Graph means :: GLIB_012:def 8 ex G9 being DLGraphComplement of G st it is removeLoops of G9; end; theorem :: GLIB_012:79 for G1, G2, G3 being _Graph, G4 being DGraphComplement of G1 st G1 == G2 & G3 == G4 holds G3 is DGraphComplement of G2; registration let G be _Graph; cluster plain for DGraphComplement of G; end; theorem :: GLIB_012:80 for G1 being _Graph, G2 being Dsimple _Graph holds G2 is DGraphComplement of G1 iff the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & for v,w being Vertex of G1 st v <> w holds (ex e1 being object st e1 DJoins v,w,G1) iff (not ex e2 being object st e2 DJoins v,w,G2); theorem :: GLIB_012:81 for G1 being _Graph, G2 being DGraphComplement of G1, e1,e2,v,w being object holds e1 DJoins v,w,G1 implies not e2 DJoins v,w,G2; theorem :: GLIB_012:82 for G1 being _Graph, G2 being DSimpleGraph of G1 for G3 being DGraphComplement of G1 holds G3 is DGraphComplement of G2; theorem :: GLIB_012:83 for G1, G2 being _Graph for G3 being DSimpleGraph of G1, G4 being DSimpleGraph of G2 for G5 being DGraphComplement of G1, G6 being DGraphComplement of G2 st G4 is G3-Disomorphic holds G6 is G5-Disomorphic; theorem :: GLIB_012:84 for G1 being _Graph, G2 being G1-Disomorphic _Graph for G3 being DGraphComplement of G1, G4 being DGraphComplement of G2 holds G4 is G3-Disomorphic; theorem :: GLIB_012:85 for G1 being _Graph, G2, G3 being DGraphComplement of G1 holds G3 is G2-Disomorphic; theorem :: GLIB_012:86 for G1 being _Graph, G2 being reverseEdgeDirections of G1 for G3 being DGraphComplement of G1, G4 being reverseEdgeDirections of G3 holds G4 is DGraphComplement of G2; theorem :: GLIB_012:87 for G1 being _Graph, V being non empty Subset of the_Vertices_of G1 for G2 being inducedSubgraph of G1, V for G3 being DGraphComplement of G1, G4 being inducedSubgraph of G3, V holds G4 is DGraphComplement of G2; theorem :: GLIB_012:88 for G1 being _Graph, V being proper Subset of the_Vertices_of G1 for G2 being removeVertices of G1, V for G3 being DGraphComplement of G1, G4 being removeVertices of G3, V holds G4 is DGraphComplement of G2; :: involutiveness of graph complement (DC case) theorem :: GLIB_012:89 for G1 being Dsimple _Graph, G2 being DGraphComplement of G1 holds G1 is DGraphComplement of G2; theorem :: GLIB_012:90 for G1 being _Graph, G2 being DGraphComplement of G1 holds G1.order() = G2.order(); theorem :: GLIB_012:91 for G1 being _Graph, G2 being DGraphComplement of G1 holds G1 is _trivial iff G2 is _trivial; registration let G be _trivial _Graph; cluster -> _trivial for DGraphComplement of G; end; registration let G be non _trivial _Graph; cluster -> non _trivial for DGraphComplement of G; end; theorem :: GLIB_012:92 for G1 being _Graph, G2 being DGraphComplement of G1 st the_Edges_of G1 = G1.loops() holds G2 is complete; registration let G be edgeless _Graph; cluster -> complete for DGraphComplement of G; end; registration let G be _trivial edgeless _Graph; cluster -> edgeless for DGraphComplement of G; end; registration let G be non connected _Graph; cluster -> connected for DGraphComplement of G; end; theorem :: GLIB_012:93 for G1 being non _trivial _Graph, G2 being DGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds v1 is isolated implies v2 is non isolated; theorem :: GLIB_012:94 for G1 being _Graph, G2 being DGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & 3 c= G1.order() holds v1 is endvertex implies v2 is non endvertex; theorem :: GLIB_012:95 for G1 being _Graph, G2 being DGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds v2.inNeighbors() = the_Vertices_of G2 \ (v1.inNeighbors() \/ {v2}) & v2.outNeighbors() = the_Vertices_of G2 \ (v1.outNeighbors() \/ {v2}); theorem :: GLIB_012:96 for G1 being _Graph, G2 being DGraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2.inNeighbors() = the_Vertices_of G2 \ {v2} & v2.outNeighbors() = the_Vertices_of G2 \ {v2} & v2.allNeighbors() = the_Vertices_of G2 \ {v2}; begin :: Undirected Graph Complement without Loops definition let G be _Graph; mode GraphComplement of G -> simple _Graph means :: GLIB_012:def 9 ex G9 being LGraphComplement of G st it is removeLoops of G9; end; theorem :: GLIB_012:97 for G1, G2, G3 being _Graph, G4 being GraphComplement of G1 st G1 == G2 & G3 == G4 holds G3 is GraphComplement of G2; registration let G be _Graph; cluster plain for GraphComplement of G; end; theorem :: GLIB_012:98 for G1 being _Graph, G2 being simple _Graph holds G2 is GraphComplement of G1 iff the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & for v,w being Vertex of G1 st v <> w holds (ex e1 being object st e1 Joins v,w,G1) iff (not ex e2 being object st e2 Joins v,w,G2); theorem :: GLIB_012:99 for G1 being _Graph, G2 being simple _Graph holds G2 is GraphComplement of G1 iff the_Vertices_of G2 = the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G1 & for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds v1,w1 are_adjacent iff not v2,w2 are_adjacent; theorem :: GLIB_012:100 for G1 being _Graph, G2 being GraphComplement of G1, e1,e2,v,w being object holds e1 Joins v,w,G1 implies not e2 Joins v,w,G2; theorem :: GLIB_012:101 for G1 being _Graph, G2 being SimpleGraph of G1 for G3 being GraphComplement of G1 holds G3 is GraphComplement of G2; theorem :: GLIB_012:102 for G1, G2 being _Graph for G3 being SimpleGraph of G1, G4 being SimpleGraph of G2 for G5 being GraphComplement of G1, G6 being GraphComplement of G2 st G4 is G3-isomorphic holds G6 is G5-isomorphic; theorem :: GLIB_012:103 for G1 being _Graph, G2 being G1-isomorphic _Graph for G3 being GraphComplement of G1, G4 being GraphComplement of G2 holds G4 is G3-isomorphic; theorem :: GLIB_012:104 for G1 being _Graph, G2, G3 being GraphComplement of G1 holds G3 is G2-isomorphic; theorem :: GLIB_012:105 for G1 being _Graph, v being object, V being Subset of the_Vertices_of G1 for G2 being addAdjVertexAll of G1,v,V for G3 being GraphComplement of G1 st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 ex G4 being addAdjVertexAll of G3,v,the_Vertices_of G1 \ V st G4 is GraphComplement of G2; theorem :: GLIB_012:106 for G1 being _Graph, v being object, G2 being addVertex of G1,v for G3 being GraphComplement of G1 st not v in the_Vertices_of G1 ex G4 being addAdjVertexAll of G3,v st G4 is GraphComplement of G2; theorem :: GLIB_012:107 for G1 being _Graph, v being object, G2 being addAdjVertexAll of G1,v for G3 being GraphComplement of G1, G4 being addVertex of G3,v st not v in the_Vertices_of G1 & the_Edges_of G2 misses the_Edges_of G3 holds G4 is GraphComplement of G2; theorem :: GLIB_012:108 for G1 being _Graph, V being non empty Subset of the_Vertices_of G1 for G2 being inducedSubgraph of G1, V for G3 being GraphComplement of G1, G4 being inducedSubgraph of G3, V holds G4 is GraphComplement of G2; theorem :: GLIB_012:109 for G1 being _Graph, V being proper Subset of the_Vertices_of G1 for G2 being removeVertices of G1, V for G3 being GraphComplement of G1, G4 being removeVertices of G3, V holds G4 is GraphComplement of G2; :: involutiveness of graph complement (C case) theorem :: GLIB_012:110 for G1 being simple _Graph, G2 being GraphComplement of G1 holds G1 is GraphComplement of G2; theorem :: GLIB_012:111 for G1 being _Graph, G2 being GraphComplement of G1 holds G1.order() = G2.order(); theorem :: GLIB_012:112 for G1 being _Graph, G2 being GraphComplement of G1 holds (G1 is _trivial iff G2 is _trivial); registration let G be _trivial _Graph; cluster -> _trivial for GraphComplement of G; end; registration let G be non _trivial _Graph; cluster -> non _trivial for GraphComplement of G; end; theorem :: GLIB_012:113 for G1 being _Graph, G2 being GraphComplement of G1 holds (G1 is complete iff G2 is edgeless) & (the_Edges_of G1 = G1.loops() iff G2 is complete); registration let G be complete _Graph; cluster -> edgeless for GraphComplement of G; end; registration let G be non complete _Graph; cluster -> non edgeless for GraphComplement of G; end; registration let G be edgeless _Graph; cluster -> complete for GraphComplement of G; end; registration let G be non connected _Graph; cluster -> connected for GraphComplement of G; end; theorem :: GLIB_012:114 for G1 being non _trivial _Graph, G2 being GraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds v1 is isolated implies v2 is non isolated; theorem :: GLIB_012:115 for G1 being _Graph, G2 being GraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & G1.order() = 2 holds (v1 is endvertex implies v2 is isolated) & (v1 is isolated implies v2 is endvertex); theorem :: GLIB_012:116 for G1 being simple _Graph, G2 being GraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & G1.order() = 2 holds (v1 is endvertex iff v2 is isolated) & (v1 is isolated iff v2 is endvertex); :: in case G.order() = 3 we have the endvertices of P3 with complement K2+K1 theorem :: GLIB_012:117 for G1 being _Graph, G2 being GraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & 4 c= G1.order() holds v1 is endvertex implies v2 is non endvertex; theorem :: GLIB_012:118 for G1 being _Graph, G2 being GraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds v2.allNeighbors() = the_Vertices_of G2 \ (v1.allNeighbors() \/ {v2}); theorem :: GLIB_012:119 for G1 being _Graph, G2 being GraphComplement of G1 for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds v2.allNeighbors() = the_Vertices_of G2 \ {v2}; begin :: Self-complementary Graphs definition let G be _Graph; attr G is self-DLcomplementary means :: GLIB_012:def 10 for H being DLGraphComplement of G holds H is G-Disomorphic; attr G is self-Lcomplementary means :: GLIB_012:def 11 for H being LGraphComplement of G holds H is G-isomorphic; attr G is self-Dcomplementary means :: GLIB_012:def 12 for H being DGraphComplement of G holds H is G-Disomorphic; attr G is self-complementary means :: GLIB_012:def 13 for H being GraphComplement of G holds H is G-isomorphic; end; theorem :: GLIB_012:120 for G being _Graph holds G is self-DLcomplementary iff ex H being DLGraphComplement of G st H is G-Disomorphic; theorem :: GLIB_012:121 for G being _Graph holds G is self-Lcomplementary iff ex H being LGraphComplement of G st H is G-isomorphic; theorem :: GLIB_012:122 for G being _Graph holds G is self-Dcomplementary iff ex H being DGraphComplement of G st H is G-Disomorphic; theorem :: GLIB_012:123 for G being _Graph holds G is self-complementary iff ex H being GraphComplement of G st H is G-isomorphic; registration cluster self-DLcomplementary -> non loopless non loopfull non-Dmulti connected for _Graph; cluster self-Lcomplementary -> non loopless non loopfull non-multi connected for _Graph; cluster self-Dcomplementary -> Dsimple connected for _Graph; cluster self-complementary -> simple connected for _Graph; end; :: K2 with an added loop is self-DLcomplementary and :: P4 with loops at the endvertices or the other two vertices :: is self-Lcomplementary, but both won't be clustered here :: hence no existence cluster for the attributes here registration cluster _trivial edgeless -> self-Dcomplementary self-complementary for _Graph; cluster self-Dcomplementary self-complementary -> _trivial edgeless for _Graph; cluster self-DLcomplementary -> non _trivial non self-Lcomplementary non self-Dcomplementary non self-complementary for _Graph; cluster self-Lcomplementary -> non _trivial non self-DLcomplementary non self-Dcomplementary non self-complementary for _Graph; end; registration cluster self-Dcomplementary self-complementary for _Graph; end;