:: Weighted and Labeled Graphs :: by Gilbert Lee :: :: 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, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI, ORDINAL4, ARYTM_3, CARD_1, CARD_3, REAL_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PBOOLE, PARTFUN1, FINSET_1, ZFMISC_1, RELAT_2, GLIB_002, VALUED_0, GRAPH_5, FUNCOP_1, TREES_1, GLIB_001, FUNCT_4, FINSEQ_5, GLIB_003; notations TARSKI, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, XCMPLX_0, XXREAL_0, XREAL_0, DOMAIN_1, RELAT_1, PARTFUN1, FUNCT_1, PBOOLE, RELSET_1, FUNCT_2, VALUED_0, GRAPH_5, RVSUM_1, FINSEQ_5, FINSEQ_1, FINSET_1, NAT_1, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001, GLIB_002, RECDEF_1; constructors DOMAIN_1, BINOP_2, FINSOP_1, RVSUM_1, FINSEQ_5, GRAPH_5, GLIB_001, GLIB_002, RECDEF_1, RELSET_1, FINSEQ_6; registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, GLIB_000, GLIB_002, INT_1, VALUED_0, CARD_1, FUNCT_2, PARTFUN1, RELSET_1, FINSEQ_6; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin :: Preliminaries definition let D be set, fs be FinSequence of D, fss be Subset of fs; redefine func Seq fss -> FinSequence of D; end; theorem :: GLIB_003:1 for x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 being set, p being FinSequence st p =<*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>^<*x10*> holds len p = 10 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6 & p.7 = x7 & p.8 = x8 & p.9 = x9 & p.10 = x10; theorem :: GLIB_003:2 for fs being FinSequence of REAL, fss being Subset of fs holds ( for i being Element of NAT st i in dom fs holds 0 <= fs.i ) implies Sum (Seq fss) <= Sum fs; begin :: Definitions definition func WeightSelector -> Element of NAT equals :: GLIB_003:def 1 5; func ELabelSelector -> Element of NAT equals :: GLIB_003:def 2 6; func VLabelSelector -> Element of NAT equals :: GLIB_003:def 3 7; end; definition let G be GraphStruct; attr G is [Weighted] means :: GLIB_003:def 4 WeightSelector in dom G & G.WeightSelector is ManySortedSet of the_Edges_of G; attr G is [ELabeled] means :: GLIB_003:def 5 ELabelSelector in dom G & ex f being Function st G.ELabelSelector = f & dom f c= the_Edges_of G; attr G is [VLabeled] means :: GLIB_003:def 6 VLabelSelector in dom G & ex f being Function st G.VLabelSelector = f & dom f c= the_Vertices_of G; end; registration cluster [Graph-like] [Weighted] [ELabeled] [VLabeled] for GraphStruct; end; definition mode WGraph is [Weighted] _Graph; mode EGraph is [ELabeled] _Graph; mode VGraph is [VLabeled] _Graph; mode WEGraph is [Weighted] [ELabeled] _Graph; mode WVGraph is [Weighted] [VLabeled] _Graph; mode EVGraph is [ELabeled] [VLabeled] _Graph; mode WEVGraph is [Weighted] [ELabeled] [VLabeled] _Graph; end; definition let G be WGraph; func the_Weight_of G -> ManySortedSet of the_Edges_of G equals :: GLIB_003:def 7 G. WeightSelector; end; definition let G be EGraph; func the_ELabel_of G -> Function equals :: GLIB_003:def 8 G.ELabelSelector; end; definition let G be VGraph; func the_VLabel_of G -> Function equals :: GLIB_003:def 9 G.VLabelSelector; end; registration let G be _Graph, X be set; cluster G.set(WeightSelector, X) -> [Graph-like]; cluster G.set(ELabelSelector, X) -> [Graph-like]; cluster G.set(VLabelSelector, X) -> [Graph-like]; end; registration let G be _finite _Graph, X be set; cluster G.set(WeightSelector, X) -> _finite; cluster G.set(ELabelSelector, X) -> _finite; cluster G.set(VLabelSelector, X) -> _finite; end; registration let G be loopless _Graph, X be set; cluster G.set(WeightSelector, X) -> loopless; cluster G.set(ELabelSelector, X) -> loopless; cluster G.set(VLabelSelector, X) -> loopless; end; registration let G be _trivial _Graph, X be set; cluster G.set(WeightSelector, X) -> _trivial; cluster G.set(ELabelSelector, X) -> _trivial; cluster G.set(VLabelSelector, X) -> _trivial; end; registration let G be non _trivial _Graph, X be set; cluster G.set(WeightSelector, X) -> non _trivial; cluster G.set(ELabelSelector, X) -> non _trivial; cluster G.set(VLabelSelector, X) -> non _trivial; end; registration let G be non-multi _Graph, X be set; cluster G.set(WeightSelector, X) -> non-multi; cluster G.set(ELabelSelector, X) -> non-multi; cluster G.set(VLabelSelector, X) -> non-multi; end; registration let G be non-Dmulti _Graph, X be set; cluster G.set(WeightSelector, X) -> non-Dmulti; cluster G.set(ELabelSelector, X) -> non-Dmulti; cluster G.set(VLabelSelector, X) -> non-Dmulti; end; registration let G be connected _Graph, X be set; cluster G.set(WeightSelector, X) -> connected; cluster G.set(ELabelSelector, X) -> connected; cluster G.set(VLabelSelector, X) -> connected; end; registration let G be acyclic _Graph, X be set; cluster G.set(WeightSelector, X) -> acyclic; cluster G.set(ELabelSelector, X) -> acyclic; cluster G.set(VLabelSelector, X) -> acyclic; end; registration let G be WGraph, X be set; cluster G.set(ELabelSelector, X) -> [Weighted]; cluster G.set(VLabelSelector, X) -> [Weighted]; end; registration let G be _Graph, X be ManySortedSet of the_Edges_of G; cluster G.set(WeightSelector, X) -> [Weighted]; end; registration let G be _Graph, WL be non empty set, W be Function of the_Edges_of G, WL; cluster G.set(WeightSelector, W) -> [Weighted]; end; registration let G be EGraph, X be set; cluster G.set(WeightSelector, X) -> [ELabeled]; cluster G.set(VLabelSelector, X) -> [ELabeled]; end; registration let G be _Graph, Y be set, X be PartFunc of the_Edges_of G, Y; cluster G.set(ELabelSelector, X) -> [ELabeled]; end; registration let G be _Graph, X be ManySortedSet of the_Edges_of G; cluster G.set(ELabelSelector, X) -> [ELabeled]; end; registration let G be VGraph, X be set; cluster G.set(WeightSelector, X) -> [VLabeled]; cluster G.set(ELabelSelector, X) -> [VLabeled]; end; registration let G be _Graph, Y be set, X be PartFunc of the_Vertices_of G,Y; cluster G.set(VLabelSelector, X) -> [VLabeled]; end; registration let G be _Graph, X be ManySortedSet of the_Vertices_of G; cluster G.set(VLabelSelector, X) -> [VLabeled]; end; registration let G be _Graph; cluster G.set(ELabelSelector, {}) -> [ELabeled]; cluster G.set(VLabelSelector, {}) -> [VLabeled]; end; registration let G be _Graph; cluster [Weighted] [ELabeled] [VLabeled] for Subgraph of G; end; definition let G be WGraph, G2 be [Weighted] Subgraph of G; attr G2 is weight-inheriting means :: GLIB_003:def 10 the_Weight_of G2 = (the_Weight_of G) | the_Edges_of G2; end; definition let G be EGraph, G2 be [ELabeled] Subgraph of G; attr G2 is elabel-inheriting means :: GLIB_003:def 11 the_ELabel_of G2 = (the_ELabel_of G) | the_Edges_of G2; end; definition let G be VGraph, G2 be [VLabeled] Subgraph of G; attr G2 is vlabel-inheriting means :: GLIB_003:def 12 the_VLabel_of G2 = (the_VLabel_of G) | the_Vertices_of G2; end; registration let G be WGraph; cluster weight-inheriting for [Weighted] Subgraph of G; end; registration let G be EGraph; cluster elabel-inheriting for [ELabeled] Subgraph of G; end; registration let G be VGraph; cluster vlabel-inheriting for [VLabeled] Subgraph of G; end; registration let G be WEGraph; cluster weight-inheriting elabel-inheriting for [Weighted] [ELabeled] Subgraph of G; end; registration let G be WVGraph; cluster weight-inheriting vlabel-inheriting for [Weighted] [VLabeled] Subgraph of G; end; registration let G be EVGraph; cluster elabel-inheriting vlabel-inheriting for [ELabeled] [VLabeled] Subgraph of G; end; registration let G be WEVGraph; cluster weight-inheriting elabel-inheriting vlabel-inheriting for [Weighted] [ELabeled] [VLabeled] Subgraph of G; end; definition let G be WGraph; mode WSubgraph of G is weight-inheriting [Weighted] Subgraph of G; end; definition let G be EGraph; mode ESubgraph of G is elabel-inheriting [ELabeled] Subgraph of G; end; definition let G be VGraph; mode VSubgraph of G is vlabel-inheriting [VLabeled] Subgraph of G; end; definition let G be WEGraph; mode WESubgraph of G is weight-inheriting elabel-inheriting [Weighted] [ELabeled] Subgraph of G; end; definition let G be WVGraph; mode WVSubgraph of G is weight-inheriting vlabel-inheriting [Weighted] [VLabeled] Subgraph of G; end; definition let G be EVGraph; mode EVSubgraph of G is elabel-inheriting vlabel-inheriting [ELabeled] [VLabeled] Subgraph of G; end; definition let G be WEVGraph; mode WEVSubgraph of G is weight-inheriting elabel-inheriting vlabel-inheriting [Weighted] [ELabeled] [VLabeled] Subgraph of G; end; registration let G be _Graph, V,E be set; cluster [Weighted] [ELabeled] [VLabeled] for inducedSubgraph of G,V,E; end; registration let G be WGraph, V,E be set; cluster weight-inheriting for [Weighted] inducedSubgraph of G,V,E; end; registration let G be EGraph, V,E be set; cluster elabel-inheriting for [ELabeled] inducedSubgraph of G,V,E; end; registration let G be VGraph, V,E be set; cluster vlabel-inheriting for [VLabeled] inducedSubgraph of G,V,E; end; registration let G be WEGraph, V,E be set; cluster weight-inheriting elabel-inheriting for [Weighted] [ELabeled] inducedSubgraph of G,V,E; end; registration let G be WVGraph, V,E be set; cluster weight-inheriting vlabel-inheriting for [Weighted] [VLabeled] inducedSubgraph of G,V,E; end; registration let G be EVGraph, V,E be set; cluster elabel-inheriting vlabel-inheriting for [ELabeled] [VLabeled] inducedSubgraph of G,V,E; end; registration let G be WEVGraph, V,E be set; cluster weight-inheriting elabel-inheriting vlabel-inheriting for [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E; end; definition let G be WGraph, V,E be set; mode inducedWSubgraph of G,V,E is weight-inheriting [Weighted] inducedSubgraph of G,V,E; end; definition let G be EGraph, V,E be set; mode inducedESubgraph of G,V,E is elabel-inheriting [ELabeled] inducedSubgraph of G,V,E; end; definition let G be VGraph, V,E be set; mode inducedVSubgraph of G,V,E is vlabel-inheriting [VLabeled] inducedSubgraph of G,V,E; end; definition let G be WEGraph, V,E be set; mode inducedWESubgraph of G,V,E is weight-inheriting elabel-inheriting [Weighted] [ELabeled] inducedSubgraph of G,V,E; end; definition let G be WVGraph, V,E be set; mode inducedWVSubgraph of G,V,E is weight-inheriting vlabel-inheriting [Weighted] [VLabeled] inducedSubgraph of G,V,E; end; definition let G be EVGraph, V,E be set; mode inducedEVSubgraph of G,V,E is elabel-inheriting vlabel-inheriting [ELabeled] [VLabeled] inducedSubgraph of G,V,E; end; definition let G be WEVGraph, V,E be set; mode inducedWEVSubgraph of G,V,E is weight-inheriting elabel-inheriting vlabel-inheriting [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E; end; definition let G be WGraph, V be set; mode inducedWSubgraph of G,V is inducedWSubgraph of G,V,G.edgesBetween(V); end; definition let G be EGraph, V be set; mode inducedESubgraph of G,V is inducedESubgraph of G,V,G.edgesBetween(V); end; definition let G be VGraph, V be set; mode inducedVSubgraph of G,V is inducedVSubgraph of G,V,G.edgesBetween(V); end; definition let G be WEGraph, V be set; mode inducedWESubgraph of G,V is inducedWESubgraph of G,V,G.edgesBetween(V); end; definition let G be WVGraph, V be set; mode inducedWVSubgraph of G,V is inducedWVSubgraph of G,V,G.edgesBetween(V); end; definition let G be EVGraph, V be set; mode inducedEVSubgraph of G,V is inducedEVSubgraph of G,V,G.edgesBetween(V); end; definition let G be WEVGraph, V be set; mode inducedWEVSubgraph of G,V is inducedWEVSubgraph of G,V,G.edgesBetween(V ); end; definition let G be WGraph; attr G is real-weighted means :: GLIB_003:def 13 the_Weight_of G is real-valued; end; definition let G be WGraph; attr G is nonnegative-weighted means :: GLIB_003:def 14 rng the_Weight_of G c= Real>=0; end; registration cluster nonnegative-weighted -> real-weighted for WGraph; end; definition let G be EGraph; attr G is real-elabeled means :: GLIB_003:def 15 the_ELabel_of G is real-valued; end; definition let G be VGraph; attr G is real-vlabeled means :: GLIB_003:def 16 the_VLabel_of G is real-valued; end; definition let G be WEVGraph; attr G is real-WEV means :: GLIB_003:def 17 G is real-weighted & G is real-elabeled & G is real-vlabeled; end; registration cluster real-WEV -> real-weighted real-elabeled real-vlabeled for WEVGraph; cluster real-weighted real-elabeled real-vlabeled -> real-WEV for WEVGraph; end; registration let G be _Graph, X be Function of the_Edges_of G, REAL; cluster G.set(WeightSelector,X) -> real-weighted; end; registration let G be _Graph, X be PartFunc of the_Edges_of G, REAL; cluster G.set(ELabelSelector, X) -> real-elabeled; end; registration let G be _Graph, X be real-valued ManySortedSet of the_Edges_of G; cluster G.set(ELabelSelector,X) -> real-elabeled; end; registration let G be _Graph, X be PartFunc of the_Vertices_of G, REAL; cluster G.set(VLabelSelector, X) -> real-vlabeled; end; registration let G be _Graph, X be real-valued ManySortedSet of the_Vertices_of G; cluster G.set(VLabelSelector, X) -> real-vlabeled; end; registration let G be _Graph; cluster G.set(ELabelSelector, {}) -> real-elabeled; cluster G.set(VLabelSelector, {}) -> real-vlabeled; end; registration let G be _Graph, v be Vertex of G, val be Real; cluster G.set(VLabelSelector, v.-->val) -> [VLabeled]; end; registration let G be _Graph, v be Vertex of G, val be Real; cluster G.set(VLabelSelector, v.-->val) -> real-vlabeled; end; registration cluster _finite _trivial Tree-like nonnegative-weighted real-WEV for WEVGraph; cluster _finite non _trivial Tree-like nonnegative-weighted real-WEV for WEVGraph; end; registration let G be _finite WGraph; cluster the_Weight_of G -> finite; end; registration let G be _finite EGraph; cluster the_ELabel_of G -> finite; end; registration let G be _finite VGraph; cluster the_VLabel_of G -> finite; end; registration let G be real-weighted WGraph; cluster the_Weight_of G -> real-valued; end; registration let G be real-elabeled EGraph; cluster the_ELabel_of G -> real-valued; end; registration let G be real-vlabeled VGraph; cluster the_VLabel_of G -> real-valued; end; registration let G be real-weighted WGraph, X be set; cluster G.set(ELabelSelector ,X) -> real-weighted; cluster G.set(VLabelSelector ,X) -> real-weighted; end; registration let G be nonnegative-weighted WGraph, X be set; cluster G.set(ELabelSelector ,X) -> nonnegative-weighted; cluster G.set(VLabelSelector ,X) -> nonnegative-weighted; end; registration let G be real-elabeled EGraph, X be set; cluster G.set(WeightSelector ,X) -> real-elabeled; cluster G.set(VLabelSelector ,X) -> real-elabeled; end; registration let G be real-vlabeled VGraph, X be set; cluster G.set(WeightSelector ,X) -> real-vlabeled; cluster G.set(ELabelSelector ,X) -> real-vlabeled; end; definition let G be WGraph, W be Walk of G; func W.weightSeq() -> FinSequence means :: GLIB_003:def 18 len it = len W.edgeSeq() & for n being Nat st 1 <= n & n <= len it holds it.n = (the_Weight_of G).(W .edgeSeq().n); end; definition let G be real-weighted WGraph, W be Walk of G; redefine func W.weightSeq() -> FinSequence of REAL; end; definition let G be real-weighted WGraph, W be Walk of G; func W.cost() -> Real equals :: GLIB_003:def 19 Sum (W.weightSeq()); end; definition let G be EGraph; func G.labeledE() -> Subset of the_Edges_of G equals :: GLIB_003:def 20 dom the_ELabel_of G; end; definition let G be EGraph, e,x be object; func G.labelEdge(e,x) -> EGraph equals :: GLIB_003:def 21 G.set(ELabelSelector, the_ELabel_of G +* (e.-->x)) if e in the_Edges_of G otherwise G; end; registration let G be _finite EGraph, e,x be set; cluster G.labelEdge(e,x) -> _finite; end; registration let G be loopless EGraph, e,x be set; cluster G.labelEdge(e,x) -> loopless; end; registration let G be _trivial EGraph, e,x be set; cluster G.labelEdge(e,x) -> _trivial; end; registration let G be non _trivial EGraph, e,x be set; cluster G.labelEdge(e,x) -> non _trivial; end; registration let G be non-multi EGraph, e,x be set; cluster G.labelEdge(e,x) -> non-multi; end; registration let G be non-Dmulti EGraph, e,x be set; cluster G.labelEdge(e,x) -> non-Dmulti; end; registration let G be connected EGraph, e,x be set; cluster G.labelEdge(e,x) -> connected; end; registration let G be acyclic EGraph, e,x be set; cluster G.labelEdge(e,x) -> acyclic; end; registration let G be WEGraph, e,x be set; cluster G.labelEdge(e,x) -> [Weighted]; end; registration let G be EVGraph, e,x be set; cluster G.labelEdge(e,x) -> [VLabeled]; end; registration let G be real-weighted WEGraph, e,x be set; cluster G.labelEdge(e,x) -> real-weighted; end; registration let G be nonnegative-weighted WEGraph, e,x be set; cluster G.labelEdge(e,x) -> nonnegative-weighted; end; registration let G be real-elabeled EGraph, e be set, x be Real; cluster G.labelEdge(e,x) -> real-elabeled; end; registration let G be real-vlabeled EVGraph, e,x be set; cluster G.labelEdge(e,x) -> real-vlabeled; end; definition let G be VGraph, v,x be object; func G.labelVertex(v,x) -> VGraph equals :: GLIB_003:def 22 G.set(VLabelSelector, the_VLabel_of G +* (v.-->x)) if v in the_Vertices_of G otherwise G; end; definition let G be VGraph; func G.labeledV() -> Subset of the_Vertices_of G equals :: GLIB_003:def 23 dom the_VLabel_of G; end; registration let G be _finite VGraph, v,x be set; cluster G.labelVertex(v,x) -> _finite; end; registration let G be loopless VGraph, v,x be set; cluster G.labelVertex(v,x) -> loopless; end; registration let G be _trivial VGraph, v,x be set; cluster G.labelVertex(v,x) -> _trivial; end; registration let G be non _trivial VGraph, v,x be set; cluster G.labelVertex(v,x) -> non _trivial; end; registration let G be non-multi VGraph, v,x be set; cluster G.labelVertex(v,x) -> non-multi; end; registration let G be non-Dmulti VGraph, v,x be set; cluster G.labelVertex(v,x) -> non-Dmulti; end; registration let G be connected VGraph, v,x be set; cluster G.labelVertex(v,x) -> connected; end; registration let G be acyclic VGraph, v,x be set; cluster G.labelVertex(v,x) -> acyclic; end; registration let G be WVGraph, v,x be set; cluster G.labelVertex(v,x) -> [Weighted]; end; registration let G be EVGraph, v,x be set; cluster G.labelVertex(v,x) -> [ELabeled]; end; registration let G be real-weighted WVGraph, v,x be set; cluster G.labelVertex(v,x) -> real-weighted; end; registration let G be nonnegative-weighted WVGraph, v,x be set; cluster G.labelVertex(v,x) -> nonnegative-weighted; end; registration let G be real-elabeled EVGraph, v,x be set; cluster G.labelVertex(v,x) -> real-elabeled; end; registration let G be real-vlabeled VGraph, v be set, x be Real; cluster G.labelVertex(v,x) -> real-vlabeled; end; registration let G be real-weighted WGraph; cluster -> real-weighted for WSubgraph of G; end; registration let G be nonnegative-weighted WGraph; cluster -> nonnegative-weighted for WSubgraph of G; end; registration let G be real-elabeled EGraph; cluster -> real-elabeled for ESubgraph of G; end; registration let G be real-vlabeled VGraph; cluster -> real-vlabeled for VSubgraph of G; end; definition let GSq be GraphSeq; attr GSq is [Weighted] means :: GLIB_003:def 24 for x being Nat holds GSq.x is [Weighted]; attr GSq is [ELabeled] means :: GLIB_003:def 25 for x being Nat holds GSq.x is [ELabeled]; attr GSq is [VLabeled] means :: GLIB_003:def 26 for x being Nat holds GSq.x is [VLabeled]; end; registration cluster [Weighted] [ELabeled] [VLabeled] for GraphSeq; end; definition mode WGraphSeq is [Weighted] GraphSeq; mode EGraphSeq is [ELabeled] GraphSeq; mode VGraphSeq is [VLabeled] GraphSeq; mode WEGraphSeq is [Weighted] [ELabeled] GraphSeq; mode WVGraphSeq is [Weighted] [VLabeled] GraphSeq; mode EVGraphSeq is [ELabeled] [VLabeled] GraphSeq; mode WEVGraphSeq is [Weighted] [ELabeled] [VLabeled] GraphSeq; end; registration let GSq be WGraphSeq, x be Nat; cluster GSq.x -> [Weighted]for _Graph; end; registration let GSq be EGraphSeq, x be Nat; cluster GSq.x -> [ELabeled]for _Graph; end; registration let GSq be VGraphSeq, x be Nat; cluster GSq.x -> [VLabeled]for _Graph; end; definition let GSq be WGraphSeq; attr GSq is real-weighted means :: GLIB_003:def 27 for x being Nat holds GSq.x is real-weighted; attr GSq is nonnegative-weighted means :: GLIB_003:def 28 for x being Nat holds GSq.x is nonnegative-weighted; end; definition let GSq be EGraphSeq; attr GSq is real-elabeled means :: GLIB_003:def 29 for x being Nat holds GSq.x is real-elabeled; end; definition let GSq be VGraphSeq; attr GSq is real-vlabeled means :: GLIB_003:def 30 for x being Nat holds GSq.x is real-vlabeled; end; definition let GSq be WEVGraphSeq; attr GSq is real-WEV means :: GLIB_003:def 31 for x being Nat holds GSq.x is real-WEV; end; registration cluster real-WEV -> real-weighted real-elabeled real-vlabeled for WEVGraphSeq; cluster real-weighted real-elabeled real-vlabeled -> real-WEV for WEVGraphSeq; end; registration cluster halting _finite loopless _trivial non-multi simple real-WEV nonnegative-weighted Tree-like for WEVGraphSeq; end; registration let GSq be real-weighted WGraphSeq, x be Nat; cluster GSq.x -> real-weighted for WGraph; end; registration let GSq be nonnegative-weighted WGraphSeq, x be Nat; cluster GSq.x -> nonnegative-weighted for WGraph; end; registration let GSq be real-elabeled EGraphSeq, x be Nat; cluster GSq.x -> real-elabeled for EGraph; end; registration let GSq be real-vlabeled VGraphSeq, x be Nat; cluster GSq.x -> real-vlabeled for VGraph; end; begin :: Theorems theorem :: GLIB_003:3 WeightSelector = 5 & ELabelSelector = 6 & VLabelSelector = 7; theorem :: GLIB_003:4 (for G being WGraph holds the_Weight_of G = G.WeightSelector) & (for G being EGraph holds the_ELabel_of G = G.ELabelSelector) & for G being VGraph holds the_VLabel_of G = G.VLabelSelector; theorem :: GLIB_003:5 for G being EGraph holds dom the_ELabel_of G c= the_Edges_of G; theorem :: GLIB_003:6 for G being VGraph holds dom the_VLabel_of G c= the_Vertices_of G; :: Theorems regarding G.set() theorem :: GLIB_003:7 for G being _Graph, X being set holds G == G.set(WeightSelector, X) & G == G.set(ELabelSelector, X) & G == G.set(VLabelSelector, X); :: Theorems regarding WSubgraphs theorem :: GLIB_003:8 for G1,G2 being WGraph, G3 being WGraph st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 & G1 is WSubgraph of G3 holds G2 is WSubgraph of G3; theorem :: GLIB_003:9 for G1 being WGraph, G2 being WSubgraph of G1, G3 being WSubgraph of G2 holds G3 is WSubgraph of G1; theorem :: GLIB_003:10 for G1,G2 being WGraph, G3 being WSubgraph of G1 st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds G3 is WSubgraph of G2; theorem :: GLIB_003:11 for G1 being WGraph, G2 be WSubgraph of G1 holds for x being set st x in the_Edges_of G2 holds (the_Weight_of G2).x = (the_Weight_of G1).x; :: Theorems regarding W.weightSeq() theorem :: GLIB_003:12 for G being WGraph, W being Walk of G holds W is trivial implies W.weightSeq() = {}; theorem :: GLIB_003:13 for G being WGraph, W being Walk of G holds len W.weightSeq() = W .length(); theorem :: GLIB_003:14 for G being WGraph, x,y,e being set st e Joins x,y,G holds G .walkOf(x,e,y).weightSeq() = <* (the_Weight_of G).e *>; theorem :: GLIB_003:15 for G being WGraph, W being Walk of G holds W.reverse() .weightSeq() = Rev (W.weightSeq()); theorem :: GLIB_003:16 for G being WGraph, W1,W2 being Walk of G st W1.last() = W2 .first() holds W1.append(W2).weightSeq() = W1.weightSeq() ^ W2.weightSeq(); theorem :: GLIB_003:17 for G being WGraph, W being Walk of G, e being set st e in W .last().edgesInOut() holds W.addEdge(e).weightSeq() = W.weightSeq() ^ <* ( the_Weight_of G).e *>; theorem :: GLIB_003:18 for G being real-weighted WGraph, W1 being Walk of G, W2 being Subwalk of W1 holds ex ws being Subset of W1.weightSeq() st W2.weightSeq() = Seq ws; theorem :: GLIB_003:19 for G1,G2 being WGraph, W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds W1.weightSeq() = W2 .weightSeq(); theorem :: GLIB_003:20 for G1 being WGraph, G2 being WSubgraph of G1, W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1.weightSeq() = W2.weightSeq(); :: Theorems regarding W.cost() theorem :: GLIB_003:21 for G being real-weighted WGraph, W being Walk of G holds W is trivial implies W.cost() = 0; theorem :: GLIB_003:22 for G being real-weighted WGraph, v1,v2 being Vertex of G, e being set st e Joins v1,v2,G holds (G.walkOf(v1,e,v2)).cost() = (the_Weight_of G).e; theorem :: GLIB_003:23 for G being real-weighted WGraph, W being Walk of G holds W.cost() = W .reverse().cost(); theorem :: GLIB_003:24 for G being real-weighted WGraph, W1, W2 being Walk of G st W1.last() = W2.first() holds W1.append(W2).cost() = W1.cost() + W2.cost(); theorem :: GLIB_003:25 for G being real-weighted WGraph, W be Walk of G, e be set st e in W .last().edgesInOut() holds W.addEdge(e).cost() = W.cost() + (the_Weight_of G).e ; theorem :: GLIB_003:26 for G1,G2 being real-weighted WGraph, W1 being Walk of G1,W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds W1.cost() = W2.cost(); theorem :: GLIB_003:27 for G1 being real-weighted WGraph, G2 being WSubgraph of G1, W1 being Walk of G1, W2 being Walk of G2 st W1 = W2 holds W1.cost() = W2.cost(); :: Theorems regarding nonnegative-weighted WGraphs theorem :: GLIB_003:28 for G being nonnegative-weighted WGraph, W being Walk of G, n being Element of NAT st n in dom W.weightSeq() holds 0 <= (W.weightSeq()).n; theorem :: GLIB_003:29 for G being nonnegative-weighted WGraph, W being Walk of G holds 0 <= W.cost(); theorem :: GLIB_003:30 for G being nonnegative-weighted WGraph, W1 being Walk of G, W2 being Subwalk of W1 holds W2.cost() <= W1.cost(); theorem :: GLIB_003:31 for G being nonnegative-weighted WGraph, e be set holds e in the_Edges_of G implies 0 <= (the_Weight_of G).e; :: Theorems involving G.labelEdge theorem :: GLIB_003:32 for G being EGraph, e,x being set st e in the_Edges_of G holds the_ELabel_of G.labelEdge(e,x) = the_ELabel_of G +* (e .--> x); theorem :: GLIB_003:33 for G being EGraph, e,x being set st e in the_Edges_of G holds ( the_ELabel_of G.labelEdge(e,x)).e = x; theorem :: GLIB_003:34 for G being EGraph, e,x being set holds G == G.labelEdge(e,x); theorem :: GLIB_003:35 for G being WEGraph, e,x being set holds the_Weight_of G = the_Weight_of G.labelEdge(e,x); theorem :: GLIB_003:36 for G being EVGraph, e,x being set holds the_VLabel_of G = the_VLabel_of G.labelEdge(e,x); theorem :: GLIB_003:37 for G being EGraph, e1,e2,x being set st e1 <> e2 holds (the_ELabel_of G.labelEdge(e1,x)).e2 = (the_ELabel_of G).e2; :: Theorems involving G.labelVertex theorem :: GLIB_003:38 for G being VGraph, v,x being set st v in the_Vertices_of G holds the_VLabel_of G.labelVertex(v,x) = the_VLabel_of G +* (v .--> x); theorem :: GLIB_003:39 for G being VGraph, v,x being set st v in the_Vertices_of G holds ( the_VLabel_of G.labelVertex(v,x)).v = x; theorem :: GLIB_003:40 for G being VGraph, v,x being set holds G == G.labelVertex(v,x); theorem :: GLIB_003:41 for G being WVGraph, v,x being set holds the_Weight_of G = the_Weight_of G.labelVertex(v,x); theorem :: GLIB_003:42 for G being EVGraph, v,x being set holds the_ELabel_of G = the_ELabel_of G.labelVertex(v,x); theorem :: GLIB_003:43 for G being VGraph, v1,v2,x being set st v1 <> v2 holds (the_VLabel_of G.labelVertex(v1,x)).v2 = (the_VLabel_of G).v2; :: Theorems regarding G.labeledE() theorem :: GLIB_003:44 for G1,G2 being EGraph st the_ELabel_of G1 = the_ELabel_of G2 holds G1 .labeledE() = G2.labeledE(); theorem :: GLIB_003:45 for G being EGraph, e,x being set st e in the_Edges_of G holds G .labelEdge(e,x).labeledE() = G.labeledE() \/ {e}; theorem :: GLIB_003:46 for G being EGraph, e,x being set st e in the_Edges_of G holds G .labeledE() c= G.labelEdge(e,x).labeledE(); theorem :: GLIB_003:47 for G being _finite EGraph, e, x being set st e in the_Edges_of G & not e in G.labeledE() holds card G.labelEdge(e,x).labeledE() = card G.labeledE() + 1; theorem :: GLIB_003:48 for G being EGraph, e1,e2,x being set st not e2 in G.labeledE() & e2 in G.labelEdge(e1,x).labeledE() holds e1 = e2 & e1 in the_Edges_of G; theorem :: GLIB_003:49 for G being EVGraph, v,x being set holds G.labeledE() = G.labelVertex( v,x).labeledE(); theorem :: GLIB_003:50 for G being EGraph, e,x being set st e in the_Edges_of G holds e in G .labelEdge(e,x).labeledE(); :: Theorems regarding G.labeledV() theorem :: GLIB_003:51 for G1,G2 being VGraph st the_VLabel_of G1 = the_VLabel_of G2 holds G1 .labeledV() = G2.labeledV(); theorem :: GLIB_003:52 for G being VGraph, v,x being set st v in the_Vertices_of G holds G.labelVertex(v,x).labeledV() = G.labeledV() \/ {v}; theorem :: GLIB_003:53 for G being VGraph, v,x being set st v in the_Vertices_of G holds G .labeledV() c= G.labelVertex(v,x).labeledV(); theorem :: GLIB_003:54 for G being _finite VGraph, v, x being set st v in the_Vertices_of G & not v in G.labeledV() holds card G.labelVertex(v,x).labeledV() = card G .labeledV() + 1; theorem :: GLIB_003:55 for G being VGraph, v1,v2,x being set st not v2 in G.labeledV() & v2 in G.labelVertex(v1,x).labeledV() holds v1 = v2 & v1 in the_Vertices_of G; theorem :: GLIB_003:56 for G being EVGraph, e,x being set holds G.labeledV() = G.labelEdge(e, x).labeledV(); theorem :: GLIB_003:57 for G being VGraph, v being Vertex of G, x being set holds v in G .labelVertex(v,x).labeledV();