:: About Graph Unions and Intersections :: by Sebastian Koch :: :: Received May 19, 2020 :: Copyright (c) 2020-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, FUNCT_4, ZFMISC_1, CARD_1, GLIB_000, GLIB_002, PARTFUN1, CHORD, SCMYCIEL, REWRITE1, GLIB_006, GLIB_007, GLIB_009, GLIB_012, RELAT_2, GLIB_014, SETFAM_1, TREES_1, MSUALG_6; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, FUNCT_4, FINSET_1, CARD_1, NUMBERS, COMPUT_1, GLIB_000, GLIB_002, CHORD, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIBPRE0, GLIB_012; constructors FUNCT_4, RELSET_1, CHORD, GLIB_002, GLIB_007, GLIB_008, GLIB_009, GLIB_012, COMPUT_1, GLIBPRE0; registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, CARD_1, RELSET_1, GLIB_000, GLIB_002, GLIB_009, GLIB_008, GLIB_012, COMPUT_1, GLIBPRE0; requirements BOOLE, SUBSET; begin :: Sets of Graphs definition let X be set; attr X is Graph-membered means :: GLIB_014:def 1 for x being object st x in X holds x is _Graph; end; registration cluster empty -> Graph-membered for set; end; registration let F be Graph-yielding Function; cluster rng F -> Graph-membered; end; registration let G1 be _Graph; cluster {G1} -> Graph-membered; let G2 be _Graph; cluster {G1, G2} -> Graph-membered; end; :: there is no functor/mode yet :: to construct an infinite number of graphs at once registration cluster empty Graph-membered for set; cluster trivial finite non empty Graph-membered for set; end; registration let X be Graph-membered set; cluster -> Graph-membered for Subset of X; end; :: the usual set operations preserve graph membership registration let X be Graph-membered set, Y be set; cluster X /\ Y -> Graph-membered; cluster X \ Y -> Graph-membered; end; registration let X, Y be Graph-membered set; cluster X \/ Y -> Graph-membered; cluster X \+\ Y -> Graph-membered; end; theorem :: GLIB_014:1 for X being set st (for Y being object st Y in X holds Y is Graph-membered set) holds union X is Graph-membered; theorem :: GLIB_014:2 for X being set st (ex Y being Graph-membered set st Y in X) holds meet X is Graph-membered; registration let X be non empty Graph-membered set; cluster -> Function-like Relation-like for Element of X; end; registration let X be non empty Graph-membered set; cluster -> NAT-defined finite for Element of X; end; registration let X be non empty Graph-membered set; cluster -> [Graph-like] for Element of X; end; :: several graphs attributes for sets of graphs :: ("finite" and "trivial" are deliberately omitted, :: so that the set attributes are not overridden) definition let S be Graph-membered set; attr S is plain means :: GLIB_014:def 2 for G being _Graph st G in S holds G is plain; attr S is loopless means :: GLIB_014:def 3 for G being _Graph st G in S holds G is loopless; attr S is non-multi means :: GLIB_014:def 4 for G being _Graph st G in S holds G is non-multi; attr S is non-Dmulti means :: GLIB_014:def 5 for G being _Graph st G in S holds G is non-Dmulti; attr S is simple means :: GLIB_014:def 6 for G being _Graph st G in S holds G is simple; attr S is Dsimple means :: GLIB_014:def 7 for G being _Graph st G in S holds G is Dsimple; attr S is acyclic means :: GLIB_014:def 8 for G being _Graph st G in S holds G is acyclic; attr S is connected means :: GLIB_014:def 9 for G being _Graph st G in S holds G is connected; attr S is Tree-like means :: GLIB_014:def 10 for G being _Graph st G in S holds G is Tree-like; attr S is chordal means :: GLIB_014:def 11 for G being _Graph st G in S holds G is chordal; attr S is edgeless means :: GLIB_014:def 12 for G being _Graph st G in S holds G is edgeless; attr S is loopfull means :: GLIB_014:def 13 for G being _Graph st G in S holds G is loopfull; ::attr S is vertex-finite means ::for G being _Graph st G in S holds G is vertex-finite; ::attr S is edge-finite means ::for G being _Graph st G in S holds G is edge-finite; end; :: negative clustering are omitted, because :: negative attributes (e.g. "non-loopless") are not defined yet registration cluster empty -> plain loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like chordal edgeless loopfull :: vertex-finite edge-finite; for Graph-membered set; cluster non-multi -> non-Dmulti for Graph-membered set; cluster loopless non-multi -> simple for Graph-membered set; cluster loopless non-Dmulti -> Dsimple for Graph-membered set; cluster simple -> loopless non-multi for Graph-membered set; cluster Dsimple -> loopless non-Dmulti for Graph-membered set; cluster acyclic -> simple for Graph-membered set; cluster acyclic connected -> Tree-like for Graph-membered set; cluster Tree-like -> acyclic connected for Graph-membered set; end; registration let G1 be plain _Graph; cluster {G1} -> plain; let G2 be plain _Graph; cluster {G1, G2} -> plain; end; registration let G1 be loopless _Graph; cluster {G1} -> loopless; let G2 be loopless _Graph; cluster {G1, G2} -> loopless; end; registration let G1 be non-multi _Graph; cluster {G1} -> non-multi; let G2 be non-multi _Graph; cluster {G1, G2} -> non-multi; end; registration let G1 be non-Dmulti _Graph; cluster {G1} -> non-Dmulti; let G2 be non-Dmulti _Graph; cluster {G1, G2} -> non-Dmulti; end; registration let G1 be simple _Graph; cluster {G1} -> simple; let G2 be simple _Graph; cluster {G1, G2} -> simple; end; registration let G1 be Dsimple _Graph; cluster {G1} -> Dsimple; let G2 be Dsimple _Graph; cluster {G1, G2} -> Dsimple; end; registration let G1 be acyclic _Graph; cluster {G1} -> acyclic; let G2 be acyclic _Graph; cluster {G1, G2} -> acyclic; end; registration let G1 be connected _Graph; cluster {G1} -> connected; let G2 be connected _Graph; cluster {G1, G2} -> connected; end; registration let G1 be Tree-like _Graph; cluster {G1} -> Tree-like; let G2 be Tree-like _Graph; cluster {G1, G2} -> Tree-like; end; registration let G1 be chordal _Graph; cluster {G1} -> chordal; let G2 be chordal _Graph; cluster {G1, G2} -> chordal; end; registration let G1 be edgeless _Graph; cluster {G1} -> edgeless; let G2 be edgeless _Graph; cluster {G1, G2} -> edgeless; end; registration let G1 be loopfull _Graph; cluster {G1} -> loopfull; let G2 be loopfull _Graph; cluster {G1, G2} -> loopfull; end; ::registration ::let G1 be vertex-finite _Graph; ::cluster {G1} -> vertex-finite; ::coherence; ::let G2 be vertex-finite _Graph; ::cluster {G1, G2} -> vertex-finite; ::coherence; ::end; :: ::registration ::let G1 be edge-finite _Graph; ::cluster {G1} -> edge-finite; ::coherence; ::let G2 be edge-finite _Graph; ::cluster {G1, G2} -> edge-finite; ::coherence; ::end; :: attributes given through graph yielding functions theorem :: GLIB_014:3 for F being Graph-yielding Function holds (F is plain iff rng F is plain) & (F is loopless iff rng F is loopless) & (F is non-multi iff rng F is non-multi) & (F is non-Dmulti iff rng F is non-Dmulti) & (F is acyclic iff rng F is acyclic) & (F is connected iff rng F is connected) & (F is chordal iff rng F is chordal) & (F is edgeless iff rng F is edgeless) & (F is loopfull iff rng F is loopfull); theorem :: GLIB_014:4 for F being Graph-yielding Function holds (F is simple iff rng F is simple) & (F is Dsimple iff rng F is Dsimple) & (F is Tree-like iff rng F is Tree-like); registration let F be plain Graph-yielding Function; cluster rng F -> plain; end; registration let F be loopless Graph-yielding Function; cluster rng F -> loopless; end; registration let F be non-multi Graph-yielding Function; cluster rng F -> non-multi; end; registration let F be non-Dmulti Graph-yielding Function; cluster rng F -> non-Dmulti; end; registration let F be simple Graph-yielding Function; cluster rng F -> simple; end; registration let F be Dsimple Graph-yielding Function; cluster rng F -> Dsimple; end; registration let F be acyclic Graph-yielding Function; cluster rng F -> acyclic; end; registration let F be connected Graph-yielding Function; cluster rng F -> connected; end; registration let F be Tree-like Graph-yielding Function; cluster rng F -> Tree-like; end; registration let F be chordal Graph-yielding Function; cluster rng F -> chordal; end; registration let F be edgeless Graph-yielding Function; cluster rng F -> edgeless; end; registration let F be loopfull Graph-yielding Function; cluster rng F -> loopfull; end; ::registration ::let F be vertex-finite Graph-yielding Function; ::cluster rng F -> vertex-finite; ::coherence ::proof ::let G be _Graph; ::assume G in rng F; ::then consider x being object such that ::A1: x in dom F & F.x = G by FUNCT_1:def 3; ::consider G0 being _Graph such that ::A2: F.x = G0 & G0 is vertex-finite by A1, GLIB_012:def 2; ::thus G is vertex-finite by A1, A2; ::end; ::end; :: ::registration ::let F be edge-finite Graph-yielding Function; ::cluster rng F -> edge-finite; ::coherence ::proof ::let G be _Graph; ::assume G in rng F; ::then consider x being object such that ::A1: x in dom F & F.x = G by FUNCT_1:def 3; ::consider G0 being _Graph such that ::A2: F.x = G0 & G0 is edge-finite by A1, GLIB_012:def 2; ::thus G is edge-finite by A1, A2; ::end; ::end; :: attributes of graph subsets registration let X be plain Graph-membered set; cluster -> plain for Subset of X; end; registration let X be loopless Graph-membered set; cluster -> loopless for Subset of X; end; registration let X be non-multi Graph-membered set; cluster -> non-multi for Subset of X; end; registration let X be non-Dmulti Graph-membered set; cluster -> non-Dmulti for Subset of X; end; registration let X be simple Graph-membered set; cluster -> simple for Subset of X; end; registration let X be Dsimple Graph-membered set; cluster -> Dsimple for Subset of X; end; registration let X be acyclic Graph-membered set; cluster -> acyclic for Subset of X; end; registration let X be connected Graph-membered set; cluster -> connected for Subset of X; end; registration let X be Tree-like Graph-membered set; cluster -> Tree-like for Subset of X; end; registration let X be chordal Graph-membered set; cluster -> chordal for Subset of X; end; registration let X be edgeless Graph-membered set; cluster -> edgeless for Subset of X; end; registration let X be loopfull Graph-membered set; cluster -> loopfull for Subset of X; end; ::registration ::let X be vertex-finite Graph-membered set; ::cluster -> vertex-finite for Subset of X; ::coherence by Def16; ::end; :: ::registration ::let X be edge-finite Graph-membered set; ::cluster -> edge-finite for Subset of X; ::coherence by Def16; ::end; :: attributes of graph sets and set operations registration let X be plain Graph-membered set, Y be set; cluster X /\ Y -> plain; cluster X \ Y -> plain; end; registration let X, Y be plain Graph-membered set; cluster X \/ Y -> plain; cluster X \+\ Y -> plain; end; registration let X be loopless Graph-membered set, Y be set; cluster X /\ Y -> loopless; cluster X \ Y -> loopless; end; registration let X, Y be loopless Graph-membered set; cluster X \/ Y -> loopless; cluster X \+\ Y -> loopless; end; registration let X be non-multi Graph-membered set, Y be set; cluster X /\ Y -> non-multi; cluster X \ Y -> non-multi; end; registration let X, Y be non-multi Graph-membered set; cluster X \/ Y -> non-multi; cluster X \+\ Y -> non-multi; end; registration let X be non-Dmulti Graph-membered set, Y be set; cluster X /\ Y -> non-Dmulti; cluster X \ Y -> non-Dmulti; end; registration let X, Y be non-Dmulti Graph-membered set; cluster X \/ Y -> non-Dmulti; cluster X \+\ Y -> non-Dmulti; end; registration let X be simple Graph-membered set, Y be set; cluster X /\ Y -> simple; cluster X \ Y -> simple; end; registration let X, Y be simple Graph-membered set; cluster X \/ Y -> simple; cluster X \+\ Y -> simple; end; registration let X be Dsimple Graph-membered set, Y be set; cluster X /\ Y -> Dsimple; cluster X \ Y -> Dsimple; end; registration let X, Y be Dsimple Graph-membered set; cluster X \/ Y -> Dsimple; cluster X \+\ Y -> Dsimple; end; registration let X be acyclic Graph-membered set, Y be set; cluster X /\ Y -> acyclic; cluster X \ Y -> acyclic; end; registration let X, Y be acyclic Graph-membered set; cluster X \/ Y -> acyclic; cluster X \+\ Y -> acyclic; end; registration let X be connected Graph-membered set, Y be set; cluster X /\ Y -> connected; cluster X \ Y -> connected; end; registration let X, Y be connected Graph-membered set; cluster X \/ Y -> connected; cluster X \+\ Y -> connected; end; registration let X be Tree-like Graph-membered set, Y be set; cluster X /\ Y -> Tree-like; cluster X \ Y -> Tree-like; end; registration let X, Y be Tree-like Graph-membered set; cluster X \/ Y -> Tree-like; cluster X \+\ Y -> Tree-like; end; registration let X be chordal Graph-membered set, Y be set; cluster X /\ Y -> chordal; cluster X \ Y -> chordal; end; registration let X, Y be chordal Graph-membered set; cluster X \/ Y -> chordal; cluster X \+\ Y -> chordal; end; registration let X be edgeless Graph-membered set, Y be set; cluster X /\ Y -> edgeless; cluster X \ Y -> edgeless; end; registration let X, Y be edgeless Graph-membered set; cluster X \/ Y -> edgeless; cluster X \+\ Y -> edgeless; end; registration let X be loopfull Graph-membered set, Y be set; cluster X /\ Y -> loopfull; cluster X \ Y -> loopfull; end; registration let X, Y be loopfull Graph-membered set; cluster X \/ Y -> loopfull; cluster X \+\ Y -> loopfull; end; ::registration ::let X be vertex-finite Graph-membered set, Y be set; ::cluster X /\ Y -> vertex-finite; ::coherence ::proof ::X /\ Y c= X by XBOOLE_1:17; ::hence thesis; ::end; ::cluster X \ Y -> vertex-finite; ::coherence; ::end; :: ::registration ::let X, Y be vertex-finite Graph-membered set; ::cluster X \/ Y -> vertex-finite; ::coherence ::proof ::let x be _Graph; ::assume x in X \/ Y; ::then per cases by XBOOLE_0:def 3; ::suppose x in X; ::hence thesis by Def16; ::end; ::suppose x in Y; ::hence thesis by Def16; ::end; ::end; ::cluster X \+\ Y -> vertex-finite; ::coherence ::proof ::X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6; ::hence thesis; ::end; ::end; :: ::registration ::let X be edge-finite Graph-membered set, Y be set; ::cluster X /\ Y -> edge-finite; ::coherence ::proof ::X /\ Y c= X by XBOOLE_1:17; ::hence thesis; ::end; ::cluster X \ Y -> edge-finite; ::coherence; ::end; :: ::registration ::let X, Y be edge-finite Graph-membered set; ::cluster X \/ Y -> edge-finite; ::coherence ::proof ::let x be _Graph; ::assume x in X \/ Y; ::then per cases by XBOOLE_0:def 3; ::suppose x in X; ::hence thesis by Def16; ::end; ::suppose x in Y; ::hence thesis by Def16; ::end; ::end; ::cluster X \+\ Y -> edge-finite; ::coherence ::proof ::X \+\ Y = (X \ Y) \/ (Y \ X) by XBOOLE_0:def 6; ::hence thesis; ::end; ::end; :: existence clusters for all attributes registration cluster empty plain loopless non-multi non-Dmulti simple Dsimple acyclic connected Tree-like chordal edgeless loopfull for Graph-membered set; cluster non empty Tree-like acyclic connected simple Dsimple loopless non-multi non-Dmulti for Graph-membered set; cluster non empty edgeless chordal for Graph-membered set; cluster non empty loopfull for Graph-membered set; cluster non empty plain for Graph-membered set; ::cluster non empty vertex-finite edge-finite for Graph-membered set; ::existence; end; registration let S be non empty plain Graph-membered set; cluster -> plain for Element of S; end; registration let S be non empty loopless Graph-membered set; cluster -> loopless for Element of S; end; registration let S be non empty non-multi Graph-membered set; cluster -> non-multi for Element of S; end; registration let S be non empty non-Dmulti Graph-membered set; cluster -> non-Dmulti for Element of S; end; registration let S be non empty simple Graph-membered set; cluster -> simple for Element of S; end; registration let S be non empty Dsimple Graph-membered set; cluster -> Dsimple for Element of S; end; registration let S be non empty acyclic Graph-membered set; cluster -> acyclic for Element of S; end; registration let S be non empty connected Graph-membered set; cluster -> connected for Element of S; end; registration let S be non empty Tree-like Graph-membered set; cluster -> Tree-like for Element of S; end; registration let S be non empty chordal Graph-membered set; cluster -> chordal for Element of S; end; registration let S be non empty edgeless Graph-membered set; cluster -> edgeless for Element of S; end; registration let S be non empty loopfull Graph-membered set; cluster -> loopfull for Element of S; end; ::registration ::let S be non empty vertex-finite Graph-membered set; ::cluster -> vertex-finite for Element of S; ::coherence by Def16; ::end; :: ::registration ::let S be non empty edge-finite Graph-membered set; ::cluster -> edge-finite for Element of S; ::coherence by Def16; ::end; :: getting vertices/edges/sources/targets from the Graph-membered set definition let S be Graph-membered set; func the_Vertices_of S -> set means :: GLIB_014:def 14 for V being object holds V in it iff ex G being _Graph st G in S & V = the_Vertices_of G; func the_Edges_of S -> set means :: GLIB_014:def 15 for E being object holds E in it iff ex G being _Graph st G in S & E = the_Edges_of G; func the_Source_of S -> set means :: GLIB_014:def 16 for s being object holds s in it iff ex G being _Graph st G in S & s = the_Source_of G; func the_Target_of S -> set means :: GLIB_014:def 17 for t being object holds t in it iff ex G being _Graph st G in S & t = the_Target_of G; end; definition let S be non empty Graph-membered set; redefine func the_Vertices_of S equals :: GLIB_014:def 18 the set of all the_Vertices_of G where G is Element of S; redefine func the_Edges_of S equals :: GLIB_014:def 19 the set of all the_Edges_of G where G is Element of S; redefine func the_Source_of S equals :: GLIB_014:def 20 the set of all the_Source_of G where G is Element of S; redefine func the_Target_of S equals :: GLIB_014:def 21 the set of all the_Target_of G where G is Element of S; end; registration let S be non empty Graph-membered set; cluster union the_Vertices_of S -> non empty; end; registration let S be Graph-membered set; cluster the_Source_of S -> functional; cluster the_Target_of S -> functional; end; registration let S be empty Graph-membered set; cluster the_Vertices_of S -> empty; cluster the_Edges_of S -> empty; cluster the_Source_of S -> empty; cluster the_Target_of S -> empty; end; registration let S be non empty Graph-membered set; cluster the_Vertices_of S -> non empty; cluster the_Edges_of S -> non empty; cluster the_Source_of S -> non empty; cluster the_Target_of S -> non empty; end; registration let S be trivial Graph-membered set; cluster the_Vertices_of S -> trivial; cluster the_Edges_of S -> trivial; cluster the_Source_of S -> trivial; cluster the_Target_of S -> trivial; end; theorem :: GLIB_014:5 for G being _Graph holds the_Vertices_of {G} = {the_Vertices_of G} & the_Edges_of {G} = {the_Edges_of G} & the_Source_of {G} = {the_Source_of G} & the_Target_of {G} = {the_Target_of G}; theorem :: GLIB_014:6 for G, H being _Graph holds the_Vertices_of {G,H} = {the_Vertices_of G, the_Vertices_of H} & the_Edges_of {G,H} = {the_Edges_of G, the_Edges_of H} & the_Source_of {G,H} = {the_Source_of G, the_Source_of H} & the_Target_of {G,H} = {the_Target_of G, the_Target_of H}; theorem :: GLIB_014:7 for S being Graph-membered set holds card the_Vertices_of S c= card S & card the_Edges_of S c= card S & card the_Source_of S c= card S & card the_Target_of S c= card S; registration let S be finite Graph-membered set; cluster the_Vertices_of S -> finite; cluster the_Edges_of S -> finite; cluster the_Source_of S -> finite; cluster the_Target_of S -> finite; end; registration let S be edgeless Graph-membered set; cluster union the_Edges_of S -> empty; end; theorem :: GLIB_014:8 for S1, S2 being Graph-membered set holds the_Vertices_of(S1 \/ S2) = the_Vertices_of S1 \/ the_Vertices_of S2 & the_Edges_of(S1 \/ S2) = the_Edges_of S1 \/ the_Edges_of S2 & the_Source_of(S1 \/ S2) = the_Source_of S1 \/ the_Source_of S2 & the_Target_of(S1 \/ S2) = the_Target_of S1 \/ the_Target_of S2; :: no equality, for example take {G},{H} with G == H but G <> H theorem :: GLIB_014:9 for S1, S2 being Graph-membered set holds the_Vertices_of(S1 /\ S2) c= the_Vertices_of S1 /\ the_Vertices_of S2 & the_Edges_of(S1 /\ S2) c= the_Edges_of S1 /\ the_Edges_of S2 & the_Source_of(S1 /\ S2) c= the_Source_of S1 /\ the_Source_of S2 & the_Target_of(S1 /\ S2) c= the_Target_of S1 /\ the_Target_of S2; theorem :: GLIB_014:10 for S1, S2 being Graph-membered set holds the_Vertices_of S1 \ the_Vertices_of S2 c= the_Vertices_of(S1 \ S2) & the_Edges_of S1 \ the_Edges_of S2 c= the_Edges_of(S1 \ S2) & the_Source_of S1 \ the_Source_of S2 c= the_Source_of(S1 \ S2) & the_Target_of S1 \ the_Target_of S2 c= the_Target_of(S1 \ S2); theorem :: GLIB_014:11 for S1, S2 being Graph-membered set holds the_Vertices_of S1 \+\ the_Vertices_of S2 c= the_Vertices_of(S1 \+\ S2) & the_Edges_of S1 \+\ the_Edges_of S2 c= the_Edges_of(S1 \+\ S2) & the_Source_of S1 \+\ the_Source_of S2 c= the_Source_of(S1 \+\ S2) & the_Target_of S1 \+\ the_Target_of S2 c= the_Target_of(S1 \+\ S2); begin :: Union of Graphs definition let G1, G2 be _Graph; pred G1 tolerates G2 means :: GLIB_014:def 22 the_Source_of G1 tolerates the_Source_of G2 & the_Target_of G1 tolerates the_Target_of G2; reflexivity; symmetry; end; theorem :: GLIB_014:12 for G1, G2 being _Graph st the_Edges_of G1 misses the_Edges_of G2 holds G1 tolerates G2; theorem :: GLIB_014:13 for G1, G2 being _Graph st the_Source_of G1 c= the_Source_of G2 & the_Target_of G1 c= the_Target_of G2 holds G1 tolerates G2; theorem :: GLIB_014:14 for G1 being _Graph, G2, G3 being Subgraph of G1 holds G2 tolerates G3; theorem :: GLIB_014:15 for G1 being _Graph, G2 being Subgraph of G1 holds G1 tolerates G2; theorem :: GLIB_014:16 for G1, G2 being _Graph st G1 == G2 holds G1 tolerates G2; theorem :: GLIB_014:17 for G1, G2 being _Graph holds G1 tolerates G2 iff for e,v1,w1,v2,w2 being object st e DJoins v1,w1,G1 & e DJoins v2,w2,G2 holds v1 = v2 & w1 = w2; theorem :: GLIB_014:18 for G1 being _Graph, E being Subset of the_Edges_of G1 for G2 being reverseEdgeDirections of G1, E holds G1 tolerates G2 iff E c= G1.loops(); definition let S be Graph-membered set; attr S is \/-tolerating means :: GLIB_014:def 23 for G1, G2 being _Graph st G1 in S & G2 in S holds G1 tolerates G2; end; definition let S be non empty Graph-membered set; redefine attr S is \/-tolerating means :: GLIB_014:def 24 for G1, G2 being Element of S holds G1 tolerates G2; end; registration cluster empty -> \/-tolerating for Graph-membered set; let G be _Graph; cluster {G} -> \/-tolerating; end; registration cluster non empty \/-tolerating for Graph-membered set; end; definition mode GraphUnionSet is non empty \/-tolerating Graph-membered set; end; theorem :: GLIB_014:19 for G1, G2 being _Graph holds G1 tolerates G2 iff {G1,G2} is \/-tolerating; registration let S1 be \/-tolerating Graph-membered set, S2 be set; cluster S1 /\ S2 -> \/-tolerating; cluster S1 \ S2 -> \/-tolerating; end; theorem :: GLIB_014:20 for S1, S2 being Graph-membered set st S1 \/ S2 is \/-tolerating holds S1 is \/-tolerating & S2 is \/-tolerating; registration let S be \/-tolerating Graph-membered set; cluster the_Source_of S -> compatible; cluster the_Target_of S -> compatible; end; registration let S be \/-tolerating Graph-membered set; cluster union the_Source_of S -> Function-like Relation-like; cluster union the_Target_of S -> Function-like Relation-like; end; registration let S be \/-tolerating Graph-membered set; cluster union the_Source_of S -> (union the_Edges_of S)-defined (union the_Vertices_of S)-valued; cluster union the_Target_of S -> (union the_Edges_of S)-defined (union the_Vertices_of S)-valued; end; registration let S be \/-tolerating Graph-membered set; cluster union the_Source_of S -> total; cluster union the_Target_of S -> total; end; definition let S be GraphUnionSet; mode GraphUnion of S -> _Graph means :: GLIB_014:def 25 the_Vertices_of it = union the_Vertices_of S & the_Edges_of it = union the_Edges_of S & the_Source_of it = union the_Source_of S & the_Target_of it = union the_Target_of S; end; :: not really needed ::definition ::let S be GraphUnionSet; ::func union S equals the plain GraphUnion of S; ::end; :: not proven here (DOMS from VALUED_2) :: theorem :: for S being GraphUnionSet, G being GraphUnion of S :: holds DOMS(the_Source_of S) = dom the_Source_of G & :: DOMS(the_Target_of S) = dom the_Target_of G; theorem :: GLIB_014:21 for S being GraphUnionSet, G being GraphUnion of S, H being Element of S holds H is Subgraph of G; theorem :: GLIB_014:22 for S being GraphUnionSet, G being GraphUnion of S, G9 being _Graph holds G9 is GraphUnion of S iff G == G9; registration let S be GraphUnionSet; cluster plain for GraphUnion of S; end; registration cluster loopless for GraphUnionSet; cluster edgeless for GraphUnionSet; cluster loopfull for GraphUnionSet; end; theorem :: GLIB_014:23 for S being GraphUnionSet, G being GraphUnion of S holds (S is loopless iff G is loopless) & (S is edgeless iff G is edgeless) & (S is loopfull implies G is loopfull); registration let S be loopless GraphUnionSet; cluster -> loopless for GraphUnion of S; end; registration let S be edgeless GraphUnionSet; cluster -> edgeless for GraphUnion of S; end; registration let S be loopfull GraphUnionSet; cluster -> loopfull for GraphUnion of S; end; theorem :: GLIB_014:24 for G, H being _Graph holds G is GraphUnion of {H} iff G == H; definition let G1, G2 be _Graph; mode GraphUnion of G1, G2 -> Supergraph of G1 means :: GLIB_014:def 26 ex S being GraphUnionSet st S = {G1,G2} & it is GraphUnion of S if G1 tolerates G2 otherwise it == G1; end; :: not really needed ::definition ::let G1, G2 be _Graph; ::func G1 \/ G2 equals the plain GraphUnion of G1, G2; ::end; theorem :: GLIB_014:25 for G1, G2, G being _Graph st G1 tolerates G2 holds G is GraphUnion of G1, G2 iff the_Vertices_of G = the_Vertices_of G1 \/ the_Vertices_of G2 & the_Edges_of G = the_Edges_of G1 \/ the_Edges_of G2 & the_Source_of G = the_Source_of G1 +* the_Source_of G2 & the_Target_of G = the_Target_of G1 +* the_Target_of G2; theorem :: GLIB_014:26 for G1, G2 being _Graph, G being GraphUnion of G1, G2 st G1 tolerates G2 holds G is Supergraph of G2; theorem :: GLIB_014:27 for G1, G2 being _Graph, G being GraphUnion of G1, G2 st G1 tolerates G2 holds G is GraphUnion of G2, G1; theorem :: GLIB_014:28 for G1, G2, G9 being _Graph, G being GraphUnion of G1, G2 holds G9 is GraphUnion of G1, G2 iff G == G9; registration let G1, G2 be _Graph; cluster plain for GraphUnion of G1, G2; end; theorem :: GLIB_014:29 for G, G1 being _Graph, G2 being Subgraph of G1 holds G is GraphUnion of G1, G2 iff G == G1; registration let G1, G2 be loopless _Graph; cluster -> loopless for GraphUnion of G1, G2; end; registration let G1, G2 be edgeless _Graph; cluster -> edgeless for GraphUnion of G1, G2; end; registration let G1, G2 be loopfull _Graph; cluster -> loopfull for GraphUnion of G1, G2; end; theorem :: GLIB_014:30 for G1 being _Graph, G2 being DLGraphComplement of G1 for G being GraphUnion of G1, G2, v, w being Vertex of G ex e being object st e DJoins v,w,G; registration let G1 be _Graph, G2 be DLGraphComplement of G1; cluster -> loopfull complete for GraphUnion of G1, G2; end; theorem :: GLIB_014:31 for G1 being _Graph, G2 being LGraphComplement of G1 for G being GraphUnion of G1, G2, v, w being Vertex of G ex e being object st e Joins v,w,G; registration let G1 be _Graph, G2 be LGraphComplement of G1; cluster -> loopfull complete for GraphUnion of G1, G2; end; theorem :: GLIB_014:32 for G1 being _Graph, G2 being DGraphComplement of G1 for G being GraphUnion of G1, G2, v, w being Vertex of G st v <> w ex e being object st e DJoins v,w,G; registration let G1 be _Graph, G2 be DGraphComplement of G1; cluster -> complete for GraphUnion of G1, G2; end; theorem :: GLIB_014:33 for G1 being _Graph, G2 being GraphComplement of G1 for G being GraphUnion of G1, G2, v, w being Vertex of G st v <> w ex e being object st e Joins v,w,G; registration let G1 be _Graph, G2 be GraphComplement of G1; cluster -> complete for GraphUnion of G1, G2; end; registration let G1 be non-Dmulti _Graph, G2 be DLGraphComplement of G1; cluster -> non-Dmulti for GraphUnion of G1, G2; end; registration let G1 be non-multi _Graph, G2 be LGraphComplement of G1; cluster -> non-multi for GraphUnion of G1, G2; end; registration let G1 be non-Dmulti _Graph, G2 be DGraphComplement of G1; cluster -> non-Dmulti for GraphUnion of G1, G2; end; registration let G1 be non-multi _Graph, G2 be GraphComplement of G1; cluster -> non-multi for GraphUnion of G1, G2; end; begin :: Meet of Graphs definition let S be Graph-membered set; attr S is /\-tolerating means :: GLIB_014:def 27 meet the_Vertices_of S <> {} & for G1, G2 being _Graph st G1 in S & G2 in S holds G1 tolerates G2; end; definition let S be non empty Graph-membered set; redefine attr S is /\-tolerating means :: GLIB_014:def 28 meet the_Vertices_of S <> {} & for G1, G2 being Element of S holds G1 tolerates G2; end; theorem :: GLIB_014:34 for S being Graph-membered set holds S is /\-tolerating iff S is \/-tolerating & meet the_Vertices_of S <> {}; registration let G be _Graph; cluster {G} -> /\-tolerating; end; registration cluster /\-tolerating -> \/-tolerating non empty for Graph-membered set; cluster /\-tolerating for Graph-membered set; end; definition mode GraphMeetSet is /\-tolerating Graph-membered set; end; registration let S be GraphMeetSet; cluster meet the_Vertices_of S -> non empty; end; theorem :: GLIB_014:35 for G1, G2 being _Graph holds G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 iff {G1, G2} is /\-tolerating; theorem :: GLIB_014:36 for S1, S2 being non empty Graph-membered set st S1 \/ S2 is /\-tolerating holds S1 is /\-tolerating & S2 is /\-tolerating; registration let S be GraphMeetSet; cluster meet the_Source_of S -> Function-like Relation-like; cluster meet the_Target_of S -> Function-like Relation-like; end; registration let S be GraphMeetSet; cluster meet the_Source_of S -> (meet the_Edges_of S)-defined (meet the_Vertices_of S)-valued; cluster meet the_Target_of S -> (meet the_Edges_of S)-defined (meet the_Vertices_of S)-valued; end; registration let S be GraphMeetSet; cluster meet the_Source_of S -> total; cluster meet the_Target_of S -> total; end; :: a.k.a. Graph Intersection, but not to be confused with Intersection Graph definition let S be GraphMeetSet; mode GraphMeet of S -> _Graph means :: GLIB_014:def 29 the_Vertices_of it = meet the_Vertices_of S & the_Edges_of it = meet the_Edges_of S & the_Source_of it = meet the_Source_of S & the_Target_of it = meet the_Target_of S; end; :: not really needed ::definition ::let S be GraphMeetSet; ::func meet S equals the plain GraphMeet of S; ::end; :: not proven here (DOM from CARD_3) :: theorem :: for S being GraphMeetSet, G being GraphMeet of S :: holds DOM(the_Source_of S) = dom the_Source_of G & :: DOM(the_Target_of S) = dom the_Target_of G; theorem :: GLIB_014:37 for S being GraphMeetSet, G being GraphMeet of S, H being Element of S holds H is Supergraph of G; theorem :: GLIB_014:38 for S being GraphMeetSet, G being GraphMeet of S, G9 being _Graph holds G9 is GraphMeet of S iff G == G9; registration let S be GraphMeetSet; cluster plain for GraphMeet of S; end; theorem :: GLIB_014:39 for G, H being _Graph holds G is GraphMeet of {H} iff G == H; definition let G1, G2 be _Graph; mode GraphMeet of G1, G2 -> Subgraph of G1 means :: GLIB_014:def 30 ex S being GraphMeetSet st S = {G1,G2} & it is GraphMeet of S if G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 otherwise it == G1; end; :: not really needed ::definition ::let G1, G2 be _Graph; ::func G1 /\ G2 equals the plain GraphMeet of G1, G2; ::end; theorem :: GLIB_014:40 for G1, G2, G being _Graph st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds G is GraphMeet of G1, G2 iff the_Vertices_of G = the_Vertices_of G1 /\ the_Vertices_of G2 & the_Edges_of G = the_Edges_of G1 /\ the_Edges_of G2 & the_Source_of G = the_Source_of G1 /\ the_Source_of G2 & the_Target_of G = the_Target_of G1 /\ the_Target_of G2; theorem :: GLIB_014:41 for G1, G2 being _Graph, G being GraphMeet of G1, G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds G is Subgraph of G2; theorem :: GLIB_014:42 for G1, G2 being _Graph, G being GraphMeet of G1, G2 st G1 tolerates G2 & the_Vertices_of G1 meets the_Vertices_of G2 holds G is GraphMeet of G2, G1; theorem :: GLIB_014:43 for G1, G2, G9 being _Graph, G being GraphMeet of G1, G2 holds G9 is GraphMeet of G1, G2 iff G == G9; registration let G1, G2 be _Graph; cluster plain for GraphMeet of G1, G2; end; theorem :: GLIB_014:44 for G, G1 being _Graph, G2 being Subgraph of G1 holds G is GraphMeet of G1, G2 iff G == G2; theorem :: GLIB_014:45 for G1, G2 being _Graph, G being GraphMeet of G1, G2 st the_Vertices_of G1 meets the_Vertices_of G2 & the_Edges_of G1 misses the_Edges_of G2 holds G is edgeless; registration let G1 be _Graph, G2 be DLGraphComplement of G1; cluster -> edgeless for GraphMeet of G1, G2; end; registration let G1 be _Graph, G2 be LGraphComplement of G1; cluster -> edgeless for GraphMeet of G1, G2; end; registration let G1 be _Graph, G2 be DGraphComplement of G1; cluster -> edgeless for GraphMeet of G1, G2; end; registration let G1 be _Graph, G2 be GraphComplement of G1; cluster -> edgeless for GraphMeet of G1, G2; end;