:: Weighted and Labeled Graphs :: by Gilbert Lee :: :: Received February 22, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin definition let D be set ; let fs be FinSequence of D; let fss be Subset of fs; :: original:Seq redefine func Seq fss -> FinSequence of D; correctness coherence Seq fss is FinSequence of D; proofend; end; theorem :: GLIB_003:1 for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being set for 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 ) proofend; theorem Th2: :: GLIB_003:2 for fs being FinSequence of REAL for fss being Subset of fs st ( for i being Element of NAT st i in dom fs holds 0 <= fs . i ) holds Sum (Seq fss) <= Sum fs proofend; begin definition func WeightSelector -> Element of NAT equals :: GLIB_003:def 1 5; coherence 5 is Element of NAT ; func ELabelSelector -> Element of NAT equals :: GLIB_003:def 2 6; coherence 6 is Element of NAT ; func VLabelSelector -> Element of NAT equals :: GLIB_003:def 3 7; coherence 7 is Element of NAT ; end; :: deftheorem defines WeightSelector GLIB_003:def_1_:_ WeightSelector = 5; :: deftheorem defines ELabelSelector GLIB_003:def_2_:_ ELabelSelector = 6; :: deftheorem defines VLabelSelector GLIB_003:def_3_:_ VLabelSelector = 7; definition let G be GraphStruct; attrG is [Weighted] means :Def4: :: GLIB_003:def 4 ( WeightSelector in dom G & G . WeightSelector is ManySortedSet of the_Edges_of G ); attrG is [ELabeled] means :Def5: :: GLIB_003:def 5 ( ELabelSelector in dom G & ex f being Function st ( G . ELabelSelector = f & dom f c= the_Edges_of G ) ); attrG is [VLabeled] means :Def6: :: GLIB_003:def 6 ( VLabelSelector in dom G & ex f being Function st ( G . VLabelSelector = f & dom f c= the_Vertices_of G ) ); end; :: deftheorem Def4 defines [Weighted] GLIB_003:def_4_:_ for G being GraphStruct holds ( G is [Weighted] iff ( WeightSelector in dom G & G . WeightSelector is ManySortedSet of the_Edges_of G ) ); :: deftheorem Def5 defines [ELabeled] GLIB_003:def_5_:_ for G being GraphStruct holds ( G is [ELabeled] iff ( ELabelSelector in dom G & ex f being Function st ( G . ELabelSelector = f & dom f c= the_Edges_of G ) ) ); :: deftheorem Def6 defines [VLabeled] GLIB_003:def_6_:_ for G being GraphStruct holds ( G is [VLabeled] iff ( VLabelSelector in dom G & ex f being Function st ( G . VLabelSelector = f & dom f c= the_Vertices_of G ) ) ); registration cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] for set ; existence ex b1 being GraphStruct st ( b1 is [Graph-like] & b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) proofend; 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; coherence G . WeightSelector is ManySortedSet of the_Edges_of G by Def4; end; :: deftheorem defines the_Weight_of GLIB_003:def_7_:_ for G being WGraph holds the_Weight_of G = G . WeightSelector; definition let G be EGraph; func the_ELabel_of G -> Function equals :: GLIB_003:def 8 G . ELabelSelector; coherence G . ELabelSelector is Function proofend; end; :: deftheorem defines the_ELabel_of GLIB_003:def_8_:_ for G being EGraph holds the_ELabel_of G = G . ELabelSelector; definition let G be VGraph; func the_VLabel_of G -> Function equals :: GLIB_003:def 9 G . VLabelSelector; coherence G . VLabelSelector is Function proofend; end; :: deftheorem defines the_VLabel_of GLIB_003:def_9_:_ for G being VGraph holds the_VLabel_of G = G . VLabelSelector; Lm1: for G being EGraph holds dom (the_ELabel_of G) c= the_Edges_of G proofend; Lm2: for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G proofend; registration let G be _Graph; let X be set ; clusterG .set (WeightSelector,X) -> [Graph-like] ; coherence G .set (WeightSelector,X) is [Graph-like] proofend; clusterG .set (ELabelSelector,X) -> [Graph-like] ; coherence G .set (ELabelSelector,X) is [Graph-like] proofend; clusterG .set (VLabelSelector,X) -> [Graph-like] ; coherence G .set (VLabelSelector,X) is [Graph-like] proofend; end; Lm3: for G being _Graph for X being set holds ( G .set (WeightSelector,X) == G & G .set (ELabelSelector,X) == G & G .set (VLabelSelector,X) == G ) proofend; registration let G be finite _Graph; let X be set ; clusterG .set (WeightSelector,X) -> finite ; coherence G .set (WeightSelector,X) is finite proofend; clusterG .set (ELabelSelector,X) -> finite ; coherence G .set (ELabelSelector,X) is finite proofend; clusterG .set (VLabelSelector,X) -> finite ; coherence G .set (VLabelSelector,X) is finite proofend; end; registration let G be loopless _Graph; let X be set ; clusterG .set (WeightSelector,X) -> loopless ; coherence G .set (WeightSelector,X) is loopless proofend; clusterG .set (ELabelSelector,X) -> loopless ; coherence G .set (ELabelSelector,X) is loopless proofend; clusterG .set (VLabelSelector,X) -> loopless ; coherence G .set (VLabelSelector,X) is loopless proofend; end; registration let G be trivial _Graph; let X be set ; clusterG .set (WeightSelector,X) -> trivial ; coherence G .set (WeightSelector,X) is trivial proofend; clusterG .set (ELabelSelector,X) -> trivial ; coherence G .set (ELabelSelector,X) is trivial proofend; clusterG .set (VLabelSelector,X) -> trivial ; coherence G .set (VLabelSelector,X) is trivial proofend; end; registration let G be non trivial _Graph; let X be set ; clusterG .set (WeightSelector,X) -> non trivial ; coherence not G .set (WeightSelector,X) is trivial proofend; clusterG .set (ELabelSelector,X) -> non trivial ; coherence not G .set (ELabelSelector,X) is trivial proofend; clusterG .set (VLabelSelector,X) -> non trivial ; coherence not G .set (VLabelSelector,X) is trivial proofend; end; registration let G be non-multi _Graph; let X be set ; clusterG .set (WeightSelector,X) -> non-multi ; coherence G .set (WeightSelector,X) is non-multi proofend; clusterG .set (ELabelSelector,X) -> non-multi ; coherence G .set (ELabelSelector,X) is non-multi proofend; clusterG .set (VLabelSelector,X) -> non-multi ; coherence G .set (VLabelSelector,X) is non-multi proofend; end; registration let G be non-Dmulti _Graph; let X be set ; clusterG .set (WeightSelector,X) -> non-Dmulti ; coherence G .set (WeightSelector,X) is non-Dmulti proofend; clusterG .set (ELabelSelector,X) -> non-Dmulti ; coherence G .set (ELabelSelector,X) is non-Dmulti proofend; clusterG .set (VLabelSelector,X) -> non-Dmulti ; coherence G .set (VLabelSelector,X) is non-Dmulti proofend; end; registration let G be connected _Graph; let X be set ; clusterG .set (WeightSelector,X) -> connected ; coherence G .set (WeightSelector,X) is connected proofend; clusterG .set (ELabelSelector,X) -> connected ; coherence G .set (ELabelSelector,X) is connected proofend; clusterG .set (VLabelSelector,X) -> connected ; coherence G .set (VLabelSelector,X) is connected proofend; end; registration let G be acyclic _Graph; let X be set ; clusterG .set (WeightSelector,X) -> acyclic ; coherence G .set (WeightSelector,X) is acyclic proofend; clusterG .set (ELabelSelector,X) -> acyclic ; coherence G .set (ELabelSelector,X) is acyclic proofend; clusterG .set (VLabelSelector,X) -> acyclic ; coherence G .set (VLabelSelector,X) is acyclic proofend; end; registration let G be WGraph; let X be set ; clusterG .set (ELabelSelector,X) -> [Weighted] ; coherence G .set (ELabelSelector,X) is [Weighted] proofend; clusterG .set (VLabelSelector,X) -> [Weighted] ; coherence G .set (VLabelSelector,X) is [Weighted] proofend; end; registration let G be _Graph; let X be ManySortedSet of the_Edges_of G; clusterG .set (WeightSelector,X) -> [Weighted] ; coherence G .set (WeightSelector,X) is [Weighted] proofend; end; registration let G be _Graph; let WL be non empty set ; let W be Function of (the_Edges_of G),WL; clusterG .set (WeightSelector,W) -> [Weighted] ; coherence G .set (WeightSelector,W) is [Weighted] ; end; registration let G be EGraph; let X be set ; clusterG .set (WeightSelector,X) -> [ELabeled] ; coherence G .set (WeightSelector,X) is [ELabeled] proofend; clusterG .set (VLabelSelector,X) -> [ELabeled] ; coherence G .set (VLabelSelector,X) is [ELabeled] proofend; end; registration let G be _Graph; let Y be set ; let X be PartFunc of (the_Edges_of G),Y; clusterG .set (ELabelSelector,X) -> [ELabeled] ; coherence G .set (ELabelSelector,X) is [ELabeled] proofend; end; registration let G be _Graph; let X be ManySortedSet of the_Edges_of G; clusterG .set (ELabelSelector,X) -> [ELabeled] ; coherence G .set (ELabelSelector,X) is [ELabeled] proofend; end; registration let G be VGraph; let X be set ; clusterG .set (WeightSelector,X) -> [VLabeled] ; coherence G .set (WeightSelector,X) is [VLabeled] proofend; clusterG .set (ELabelSelector,X) -> [VLabeled] ; coherence G .set (ELabelSelector,X) is [VLabeled] proofend; end; registration let G be _Graph; let Y be set ; let X be PartFunc of (the_Vertices_of G),Y; clusterG .set (VLabelSelector,X) -> [VLabeled] ; coherence G .set (VLabelSelector,X) is [VLabeled] proofend; end; registration let G be _Graph; let X be ManySortedSet of the_Vertices_of G; clusterG .set (VLabelSelector,X) -> [VLabeled] ; coherence G .set (VLabelSelector,X) is [VLabeled] proofend; end; registration let G be _Graph; clusterG .set (ELabelSelector,{}) -> [ELabeled] ; coherence G .set (ELabelSelector,{}) is [ELabeled] proofend; clusterG .set (VLabelSelector,{}) -> [VLabeled] ; coherence G .set (VLabelSelector,{}) is [VLabeled] proofend; end; registration let G be _Graph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] for Subgraph of G; existence ex b1 being Subgraph of G st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) proofend; end; definition let G be WGraph; let G2 be [Weighted] Subgraph of G; attrG2 is weight-inheriting means :Def10: :: GLIB_003:def 10 the_Weight_of G2 = (the_Weight_of G) | (the_Edges_of G2); end; :: deftheorem Def10 defines weight-inheriting GLIB_003:def_10_:_ for G being WGraph for G2 being [Weighted] Subgraph of G holds ( G2 is weight-inheriting iff the_Weight_of G2 = (the_Weight_of G) | (the_Edges_of G2) ); definition let G be EGraph; let G2 be [ELabeled] Subgraph of G; attrG2 is elabel-inheriting means :Def11: :: GLIB_003:def 11 the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of G2); end; :: deftheorem Def11 defines elabel-inheriting GLIB_003:def_11_:_ for G being EGraph for G2 being [ELabeled] Subgraph of G holds ( G2 is elabel-inheriting iff the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of G2) ); definition let G be VGraph; let G2 be [VLabeled] Subgraph of G; attrG2 is vlabel-inheriting means :Def12: :: GLIB_003:def 12 the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of G2); end; :: deftheorem Def12 defines vlabel-inheriting GLIB_003:def_12_:_ for G being VGraph for G2 being [VLabeled] Subgraph of G holds ( G2 is vlabel-inheriting iff the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of G2) ); registration let G be WGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] weight-inheriting for Subgraph of G; existence ex b1 being [Weighted] Subgraph of G st b1 is weight-inheriting proofend; end; registration let G be EGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] elabel-inheriting for Subgraph of G; existence ex b1 being [ELabeled] Subgraph of G st b1 is elabel-inheriting proofend; end; registration let G be VGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [VLabeled] vlabel-inheriting for Subgraph of G; existence ex b1 being [VLabeled] Subgraph of G st b1 is vlabel-inheriting proofend; end; registration let G be WEGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] weight-inheriting elabel-inheriting for Subgraph of G; existence ex b1 being [Weighted] [ELabeled] Subgraph of G st ( b1 is weight-inheriting & b1 is elabel-inheriting ) proofend; end; registration let G be WVGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [VLabeled] weight-inheriting vlabel-inheriting for Subgraph of G; existence ex b1 being [Weighted] [VLabeled] Subgraph of G st ( b1 is weight-inheriting & b1 is vlabel-inheriting ) proofend; end; registration let G be EVGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting for Subgraph of G; existence ex b1 being [ELabeled] [VLabeled] Subgraph of G st ( b1 is elabel-inheriting & b1 is vlabel-inheriting ) proofend; end; registration let G be WEVGraph; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting for Subgraph of G; existence ex b1 being [Weighted] [ELabeled] [VLabeled] Subgraph of G st ( b1 is weight-inheriting & b1 is elabel-inheriting & b1 is vlabel-inheriting ) proofend; end; definition let G be WGraph; mode WSubgraph of G is [Weighted] weight-inheriting Subgraph of G; end; definition let G be EGraph; mode ESubgraph of G is [ELabeled] elabel-inheriting Subgraph of G; end; definition let G be VGraph; mode VSubgraph of G is [VLabeled] vlabel-inheriting Subgraph of G; end; definition let G be WEGraph; mode WESubgraph of G is [Weighted] [ELabeled] weight-inheriting elabel-inheriting Subgraph of G; end; definition let G be WVGraph; mode WVSubgraph of G is [Weighted] [VLabeled] weight-inheriting vlabel-inheriting Subgraph of G; end; definition let G be EVGraph; mode EVSubgraph of G is [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting Subgraph of G; end; definition let G be WEVGraph; mode WEVSubgraph of G is [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting Subgraph of G; end; registration let G be _Graph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] for inducedSubgraph of G,V,E; existence ex b1 being inducedSubgraph of G,V,E st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) proofend; end; registration let G be WGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] weight-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [Weighted] inducedSubgraph of G,V,E st b1 is weight-inheriting proofend; end; registration let G be EGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] elabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [ELabeled] inducedSubgraph of G,V,E st b1 is elabel-inheriting proofend; end; registration let G be VGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [VLabeled] vlabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [VLabeled] inducedSubgraph of G,V,E st b1 is vlabel-inheriting proofend; end; registration let G be WEGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] weight-inheriting elabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [Weighted] [ELabeled] inducedSubgraph of G,V,E st ( b1 is weight-inheriting & b1 is elabel-inheriting ) proofend; end; registration let G be WVGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [VLabeled] weight-inheriting vlabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [Weighted] [VLabeled] inducedSubgraph of G,V,E st ( b1 is weight-inheriting & b1 is vlabel-inheriting ) proofend; end; registration let G be EVGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( b1 is elabel-inheriting & b1 is vlabel-inheriting ) proofend; end; registration let G be WEVGraph; let V, E be set ; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting for inducedSubgraph of G,V,E; existence ex b1 being [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G,V,E st ( b1 is weight-inheriting & b1 is elabel-inheriting & b1 is vlabel-inheriting ) proofend; end; definition let G be WGraph; let V, E be set ; mode inducedWSubgraph of G,V,E is [Weighted] weight-inheriting inducedSubgraph of G,V,E; end; definition let G be EGraph; let V, E be set ; mode inducedESubgraph of G,V,E is [ELabeled] elabel-inheriting inducedSubgraph of G,V,E; end; definition let G be VGraph; let V, E be set ; mode inducedVSubgraph of G,V,E is [VLabeled] vlabel-inheriting inducedSubgraph of G,V,E; end; definition let G be WEGraph; let V, E be set ; mode inducedWESubgraph of G,V,E is [Weighted] [ELabeled] weight-inheriting elabel-inheriting inducedSubgraph of G,V,E; end; definition let G be WVGraph; let V, E be set ; mode inducedWVSubgraph of G,V,E is [Weighted] [VLabeled] weight-inheriting vlabel-inheriting inducedSubgraph of G,V,E; end; definition let G be EVGraph; let V, E be set ; mode inducedEVSubgraph of G,V,E is [ELabeled] [VLabeled] elabel-inheriting vlabel-inheriting inducedSubgraph of G,V,E; end; definition let G be WEVGraph; let V, E be set ; mode inducedWEVSubgraph of G,V,E is [Weighted] [ELabeled] [VLabeled] weight-inheriting elabel-inheriting vlabel-inheriting inducedSubgraph of G,V,E; end; definition let G be WGraph; let V be set ; mode inducedWSubgraph of G,V is inducedWSubgraph of G,V,G .edgesBetween V; end; definition let G be EGraph; let V be set ; mode inducedESubgraph of G,V is inducedESubgraph of G,V,G .edgesBetween V; end; definition let G be VGraph; let V be set ; mode inducedVSubgraph of G,V is inducedVSubgraph of G,V,G .edgesBetween V; end; definition let G be WEGraph; let V be set ; mode inducedWESubgraph of G,V is inducedWESubgraph of G,V,G .edgesBetween V; end; definition let G be WVGraph; let V be set ; mode inducedWVSubgraph of G,V is inducedWVSubgraph of G,V,G .edgesBetween V; end; definition let G be EVGraph; let V be set ; mode inducedEVSubgraph of G,V is inducedEVSubgraph of G,V,G .edgesBetween V; end; definition let G be WEVGraph; let V be set ; mode inducedWEVSubgraph of G,V is inducedWEVSubgraph of G,V,G .edgesBetween V; end; definition let G be WGraph; attrG is real-weighted means :Def13: :: GLIB_003:def 13 the_Weight_of G is real-valued ; end; :: deftheorem Def13 defines real-weighted GLIB_003:def_13_:_ for G being WGraph holds ( G is real-weighted iff the_Weight_of G is real-valued ); definition let G be WGraph; attrG is nonnegative-weighted means :Def14: :: GLIB_003:def 14 rng (the_Weight_of G) c= Real>=0 ; end; :: deftheorem Def14 defines nonnegative-weighted GLIB_003:def_14_:_ for G being WGraph holds ( G is nonnegative-weighted iff rng (the_Weight_of G) c= Real>=0 ); registration cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] nonnegative-weighted -> real-weighted for set ; coherence for b1 being WGraph st b1 is nonnegative-weighted holds b1 is real-weighted proofend; end; definition let G be EGraph; attrG is real-elabeled means :Def15: :: GLIB_003:def 15 the_ELabel_of G is real-valued ; end; :: deftheorem Def15 defines real-elabeled GLIB_003:def_15_:_ for G being EGraph holds ( G is real-elabeled iff the_ELabel_of G is real-valued ); definition let G be VGraph; attrG is real-vlabeled means :Def16: :: GLIB_003:def 16 the_VLabel_of G is real-valued ; end; :: deftheorem Def16 defines real-vlabeled GLIB_003:def_16_:_ for G being VGraph holds ( G is real-vlabeled iff the_VLabel_of G is real-valued ); definition let G be WEVGraph; attrG is real-WEV means :Def17: :: GLIB_003:def 17 ( G is real-weighted & G is real-elabeled & G is real-vlabeled ); end; :: deftheorem Def17 defines real-WEV GLIB_003:def_17_:_ for G being WEVGraph holds ( G is real-WEV iff ( G is real-weighted & G is real-elabeled & G is real-vlabeled ) ); registration cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] real-WEV -> real-weighted real-elabeled real-vlabeled for set ; coherence for b1 being WEVGraph st b1 is real-WEV holds ( b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled ) by Def17; cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] real-weighted real-elabeled real-vlabeled -> real-WEV for set ; coherence for b1 being WEVGraph st b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled holds b1 is real-WEV by Def17; end; registration let G be _Graph; let X be Function of (the_Edges_of G),REAL; clusterG .set (WeightSelector,X) -> real-weighted ; coherence G .set (WeightSelector,X) is real-weighted proofend; end; registration let G be _Graph; let X be PartFunc of (the_Edges_of G),REAL; clusterG .set (ELabelSelector,X) -> real-elabeled ; coherence G .set (ELabelSelector,X) is real-elabeled proofend; end; registration let G be _Graph; let X be real-valued ManySortedSet of the_Edges_of G; clusterG .set (ELabelSelector,X) -> real-elabeled ; coherence G .set (ELabelSelector,X) is real-elabeled proofend; end; registration let G be _Graph; let X be PartFunc of (the_Vertices_of G),REAL; clusterG .set (VLabelSelector,X) -> real-vlabeled ; coherence G .set (VLabelSelector,X) is real-vlabeled proofend; end; registration let G be _Graph; let X be real-valued ManySortedSet of the_Vertices_of G; clusterG .set (VLabelSelector,X) -> real-vlabeled ; coherence G .set (VLabelSelector,X) is real-vlabeled proofend; end; registration let G be _Graph; clusterG .set (ELabelSelector,{}) -> real-elabeled ; coherence G .set (ELabelSelector,{}) is real-elabeled proofend; clusterG .set (VLabelSelector,{}) -> real-vlabeled ; coherence G .set (VLabelSelector,{}) is real-vlabeled proofend; end; registration let G be _Graph; let v be Vertex of G; let val be real number ; clusterG .set (VLabelSelector,(v .--> val)) -> [VLabeled] ; coherence G .set (VLabelSelector,(v .--> val)) is [VLabeled] proofend; end; registration let G be _Graph; let v be Vertex of G; let val be real number ; clusterG .set (VLabelSelector,(v .--> val)) -> real-vlabeled ; coherence G .set (VLabelSelector,(v .--> val)) is real-vlabeled proofend; end; registration cluster Relation-like NAT -defined Function-like finite [Graph-like] finite trivial Tree-like [Weighted] [ELabeled] [VLabeled] nonnegative-weighted real-WEV for set ; existence ex b1 being WEVGraph st ( b1 is finite & b1 is trivial & b1 is Tree-like & b1 is nonnegative-weighted & b1 is real-WEV ) proofend; cluster Relation-like NAT -defined Function-like finite [Graph-like] finite non trivial Tree-like [Weighted] [ELabeled] [VLabeled] nonnegative-weighted real-WEV for set ; existence ex b1 being WEVGraph st ( b1 is finite & not b1 is trivial & b1 is Tree-like & b1 is nonnegative-weighted & b1 is real-WEV ) proofend; end; registration let G be finite WGraph; cluster the_Weight_of G -> finite ; coherence the_Weight_of G is finite proofend; end; registration let G be finite EGraph; cluster the_ELabel_of G -> finite ; coherence the_ELabel_of G is finite proofend; end; registration let G be finite VGraph; cluster the_VLabel_of G -> finite ; coherence the_VLabel_of G is finite proofend; end; registration let G be real-weighted WGraph; cluster the_Weight_of G -> real-valued ; coherence the_Weight_of G is real-valued by Def13; end; registration let G be real-elabeled EGraph; cluster the_ELabel_of G -> real-valued ; coherence the_ELabel_of G is real-valued by Def15; end; registration let G be real-vlabeled VGraph; cluster the_VLabel_of G -> real-valued ; coherence the_VLabel_of G is real-valued by Def16; end; registration let G be real-weighted WGraph; let X be set ; clusterG .set (ELabelSelector,X) -> real-weighted ; coherence G .set (ELabelSelector,X) is real-weighted proofend; clusterG .set (VLabelSelector,X) -> real-weighted ; coherence G .set (VLabelSelector,X) is real-weighted proofend; end; registration let G be nonnegative-weighted WGraph; let X be set ; clusterG .set (ELabelSelector,X) -> nonnegative-weighted ; coherence G .set (ELabelSelector,X) is nonnegative-weighted proofend; clusterG .set (VLabelSelector,X) -> nonnegative-weighted ; coherence G .set (VLabelSelector,X) is nonnegative-weighted proofend; end; registration let G be real-elabeled EGraph; let X be set ; clusterG .set (WeightSelector,X) -> real-elabeled ; coherence G .set (WeightSelector,X) is real-elabeled proofend; clusterG .set (VLabelSelector,X) -> real-elabeled ; coherence G .set (VLabelSelector,X) is real-elabeled proofend; end; registration let G be real-vlabeled VGraph; let X be set ; clusterG .set (WeightSelector,X) -> real-vlabeled ; coherence G .set (WeightSelector,X) is real-vlabeled proofend; clusterG .set (ELabelSelector,X) -> real-vlabeled ; coherence G .set (ELabelSelector,X) is real-vlabeled proofend; end; definition let G be WGraph; let W be Walk of G; funcW .weightSeq() -> FinSequence means :Def18: :: 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) ) ); existence ex b1 being FinSequence st ( len b1 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b1 holds b1 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) ) proofend; uniqueness for b1, b2 being FinSequence st len b1 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b1 holds b1 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) & len b2 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b2 holds b2 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) holds b1 = b2 proofend; end; :: deftheorem Def18 defines .weightSeq() GLIB_003:def_18_:_ for G being WGraph for W being Walk of G for b3 being FinSequence holds ( b3 = W .weightSeq() iff ( len b3 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b3 holds b3 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) ) ); definition let G be real-weighted WGraph; let W be Walk of G; :: original:.weightSeq() redefine funcW .weightSeq() -> FinSequence of REAL ; coherence W .weightSeq() is FinSequence of REAL proofend; end; definition let G be real-weighted WGraph; let W be Walk of G; funcW .cost() -> Real equals :: GLIB_003:def 19 Sum (W .weightSeq()); coherence Sum (W .weightSeq()) is Real ; end; :: deftheorem defines .cost() GLIB_003:def_19_:_ for G being real-weighted WGraph for W being Walk of G holds W .cost() = Sum (W .weightSeq()); Lm4: for x, y, X, Y being set for f being PartFunc of X,Y st x in X & y in Y holds f +* (x .--> y) is PartFunc of X,Y proofend; definition let G be EGraph; funcG .labeledE() -> Subset of (the_Edges_of G) equals :: GLIB_003:def 20 dom (the_ELabel_of G); coherence dom (the_ELabel_of G) is Subset of (the_Edges_of G) by Lm1; end; :: deftheorem defines .labeledE() GLIB_003:def_20_:_ for G being EGraph holds G .labeledE() = dom (the_ELabel_of G); definition let G be EGraph; let e, x be set ; funcG .labelEdge (e,x) -> EGraph equals :Def21: :: GLIB_003:def 21 G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) if e in the_Edges_of G otherwise G; coherence ( ( e in the_Edges_of G implies G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) is EGraph ) & ( not e in the_Edges_of G implies G is EGraph ) ) proofend; consistency for b1 being EGraph holds verum ; end; :: deftheorem Def21 defines .labelEdge GLIB_003:def_21_:_ for G being EGraph for e, x being set holds ( ( e in the_Edges_of G implies G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) ) & ( not e in the_Edges_of G implies G .labelEdge (e,x) = G ) ); registration let G be finite EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> finite ; coherence G .labelEdge (e,x) is finite proofend; end; registration let G be loopless EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> loopless ; coherence G .labelEdge (e,x) is loopless proofend; end; registration let G be trivial EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> trivial ; coherence G .labelEdge (e,x) is trivial proofend; end; registration let G be non trivial EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> non trivial ; coherence not G .labelEdge (e,x) is trivial proofend; end; registration let G be non-multi EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> non-multi ; coherence G .labelEdge (e,x) is non-multi proofend; end; registration let G be non-Dmulti EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> non-Dmulti ; coherence G .labelEdge (e,x) is non-Dmulti proofend; end; registration let G be connected EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> connected ; coherence G .labelEdge (e,x) is connected proofend; end; registration let G be acyclic EGraph; let e, x be set ; clusterG .labelEdge (e,x) -> acyclic ; coherence G .labelEdge (e,x) is acyclic proofend; end; registration let G be WEGraph; let e, x be set ; clusterG .labelEdge (e,x) -> [Weighted] ; coherence G .labelEdge (e,x) is [Weighted] proofend; end; registration let G be EVGraph; let e, x be set ; clusterG .labelEdge (e,x) -> [VLabeled] ; coherence G .labelEdge (e,x) is [VLabeled] proofend; end; registration let G be real-weighted WEGraph; let e, x be set ; clusterG .labelEdge (e,x) -> real-weighted ; coherence G .labelEdge (e,x) is real-weighted proofend; end; registration let G be nonnegative-weighted WEGraph; let e, x be set ; clusterG .labelEdge (e,x) -> nonnegative-weighted ; coherence G .labelEdge (e,x) is nonnegative-weighted proofend; end; registration let G be real-elabeled EGraph; let e be set ; let x be Real; clusterG .labelEdge (e,x) -> real-elabeled ; coherence G .labelEdge (e,x) is real-elabeled proofend; end; registration let G be real-vlabeled EVGraph; let e, x be set ; clusterG .labelEdge (e,x) -> real-vlabeled ; coherence G .labelEdge (e,x) is real-vlabeled proofend; end; definition let G be VGraph; let v, x be set ; funcG .labelVertex (v,x) -> VGraph equals :Def22: :: GLIB_003:def 22 G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) if v in the_Vertices_of G otherwise G; coherence ( ( v in the_Vertices_of G implies G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) is VGraph ) & ( not v in the_Vertices_of G implies G is VGraph ) ) proofend; consistency for b1 being VGraph holds verum ; end; :: deftheorem Def22 defines .labelVertex GLIB_003:def_22_:_ for G being VGraph for v, x being set holds ( ( v in the_Vertices_of G implies G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) ) & ( not v in the_Vertices_of G implies G .labelVertex (v,x) = G ) ); definition let G be VGraph; funcG .labeledV() -> Subset of (the_Vertices_of G) equals :: GLIB_003:def 23 dom (the_VLabel_of G); coherence dom (the_VLabel_of G) is Subset of (the_Vertices_of G) by Lm2; end; :: deftheorem defines .labeledV() GLIB_003:def_23_:_ for G being VGraph holds G .labeledV() = dom (the_VLabel_of G); registration let G be finite VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> finite ; coherence G .labelVertex (v,x) is finite proofend; end; registration let G be loopless VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> loopless ; coherence G .labelVertex (v,x) is loopless proofend; end; registration let G be trivial VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> trivial ; coherence G .labelVertex (v,x) is trivial proofend; end; registration let G be non trivial VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> non trivial ; coherence not G .labelVertex (v,x) is trivial proofend; end; registration let G be non-multi VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> non-multi ; coherence G .labelVertex (v,x) is non-multi proofend; end; registration let G be non-Dmulti VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> non-Dmulti ; coherence G .labelVertex (v,x) is non-Dmulti proofend; end; registration let G be connected VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> connected ; coherence G .labelVertex (v,x) is connected proofend; end; registration let G be acyclic VGraph; let v, x be set ; clusterG .labelVertex (v,x) -> acyclic ; coherence G .labelVertex (v,x) is acyclic proofend; end; registration let G be WVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> [Weighted] ; coherence G .labelVertex (v,x) is [Weighted] proofend; end; registration let G be EVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> [ELabeled] ; coherence G .labelVertex (v,x) is [ELabeled] proofend; end; registration let G be real-weighted WVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> real-weighted ; coherence G .labelVertex (v,x) is real-weighted proofend; end; registration let G be nonnegative-weighted WVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> nonnegative-weighted ; coherence G .labelVertex (v,x) is nonnegative-weighted proofend; end; registration let G be real-elabeled EVGraph; let v, x be set ; clusterG .labelVertex (v,x) -> real-elabeled ; coherence G .labelVertex (v,x) is real-elabeled proofend; end; registration let G be real-vlabeled VGraph; let v be set ; let x be Real; clusterG .labelVertex (v,x) -> real-vlabeled ; coherence G .labelVertex (v,x) is real-vlabeled proofend; end; registration let G be real-weighted WGraph; cluster [Weighted] weight-inheriting -> real-weighted for Subgraph of G; coherence for b1 being WSubgraph of G holds b1 is real-weighted proofend; end; registration let G be nonnegative-weighted WGraph; cluster [Weighted] weight-inheriting -> nonnegative-weighted for Subgraph of G; coherence for b1 being WSubgraph of G holds b1 is nonnegative-weighted proofend; end; registration let G be real-elabeled EGraph; cluster [ELabeled] elabel-inheriting -> real-elabeled for Subgraph of G; coherence for b1 being ESubgraph of G holds b1 is real-elabeled proofend; end; registration let G be real-vlabeled VGraph; cluster [VLabeled] vlabel-inheriting -> real-vlabeled for Subgraph of G; coherence for b1 being VSubgraph of G holds b1 is real-vlabeled proofend; end; definition let GSq be GraphSeq; attrGSq is [Weighted] means :Def24: :: GLIB_003:def 24 for x being Nat holds GSq . x is [Weighted] ; attrGSq is [ELabeled] means :Def25: :: GLIB_003:def 25 for x being Nat holds GSq . x is [ELabeled] ; attrGSq is [VLabeled] means :Def26: :: GLIB_003:def 26 for x being Nat holds GSq . x is [VLabeled] ; end; :: deftheorem Def24 defines [Weighted] GLIB_003:def_24_:_ for GSq being GraphSeq holds ( GSq is [Weighted] iff for x being Nat holds GSq . x is [Weighted] ); :: deftheorem Def25 defines [ELabeled] GLIB_003:def_25_:_ for GSq being GraphSeq holds ( GSq is [ELabeled] iff for x being Nat holds GSq . x is [ELabeled] ); :: deftheorem Def26 defines [VLabeled] GLIB_003:def_26_:_ for GSq being GraphSeq holds ( GSq is [VLabeled] iff for x being Nat holds GSq . x is [VLabeled] ); registration cluster Relation-like NAT -defined Function-like total Graph-yielding [Weighted] [ELabeled] [VLabeled] for set ; existence ex b1 being GraphSeq st ( b1 is [Weighted] & b1 is [ELabeled] & b1 is [VLabeled] ) proofend; 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; let x be Nat; clusterGSq . x -> [Weighted] for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is [Weighted] by Def24; end; registration let GSq be EGraphSeq; let x be Nat; clusterGSq . x -> [ELabeled] for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is [ELabeled] by Def25; end; registration let GSq be VGraphSeq; let x be Nat; clusterGSq . x -> [VLabeled] for _Graph; coherence for b1 being _Graph st b1 = GSq . x holds b1 is [VLabeled] by Def26; end; definition let GSq be WGraphSeq; attrGSq is real-weighted means :Def27: :: GLIB_003:def 27 for x being Nat holds GSq . x is real-weighted ; attrGSq is nonnegative-weighted means :Def28: :: GLIB_003:def 28 for x being Nat holds GSq . x is nonnegative-weighted ; end; :: deftheorem Def27 defines real-weighted GLIB_003:def_27_:_ for GSq being WGraphSeq holds ( GSq is real-weighted iff for x being Nat holds GSq . x is real-weighted ); :: deftheorem Def28 defines nonnegative-weighted GLIB_003:def_28_:_ for GSq being WGraphSeq holds ( GSq is nonnegative-weighted iff for x being Nat holds GSq . x is nonnegative-weighted ); definition let GSq be EGraphSeq; attrGSq is real-elabeled means :Def29: :: GLIB_003:def 29 for x being Nat holds GSq . x is real-elabeled ; end; :: deftheorem Def29 defines real-elabeled GLIB_003:def_29_:_ for GSq being EGraphSeq holds ( GSq is real-elabeled iff for x being Nat holds GSq . x is real-elabeled ); definition let GSq be VGraphSeq; attrGSq is real-vlabeled means :Def30: :: GLIB_003:def 30 for x being Nat holds GSq . x is real-vlabeled ; end; :: deftheorem Def30 defines real-vlabeled GLIB_003:def_30_:_ for GSq being VGraphSeq holds ( GSq is real-vlabeled iff for x being Nat holds GSq . x is real-vlabeled ); definition let GSq be WEVGraphSeq; attrGSq is real-WEV means :Def31: :: GLIB_003:def 31 for x being Nat holds GSq . x is real-WEV ; end; :: deftheorem Def31 defines real-WEV GLIB_003:def_31_:_ for GSq being WEVGraphSeq holds ( GSq is real-WEV iff for x being Nat holds GSq . x is real-WEV ); registration cluster Relation-like NAT -defined Function-like total Graph-yielding [Weighted] [ELabeled] [VLabeled] real-WEV -> real-weighted real-elabeled real-vlabeled for set ; coherence for b1 being WEVGraphSeq st b1 is real-WEV holds ( b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled ) proofend; cluster Relation-like NAT -defined Function-like total Graph-yielding [Weighted] [ELabeled] [VLabeled] real-weighted real-elabeled real-vlabeled -> real-WEV for set ; coherence for b1 being WEVGraphSeq st b1 is real-weighted & b1 is real-elabeled & b1 is real-vlabeled holds b1 is real-WEV proofend; end; registration cluster Relation-like NAT -defined Function-like total Graph-yielding halting finite loopless trivial non-multi simple Tree-like [Weighted] [ELabeled] [VLabeled] nonnegative-weighted real-WEV for set ; existence ex b1 being WEVGraphSeq st ( b1 is halting & b1 is finite & b1 is loopless & b1 is trivial & b1 is non-multi & b1 is simple & b1 is real-WEV & b1 is nonnegative-weighted & b1 is Tree-like ) proofend; end; registration let GSq be real-weighted WGraphSeq; let x be Nat; clusterGSq . x -> real-weighted for WGraph; coherence for b1 being WGraph st b1 = GSq . x holds b1 is real-weighted by Def27; end; registration let GSq be nonnegative-weighted WGraphSeq; let x be Nat; clusterGSq . x -> nonnegative-weighted for WGraph; coherence for b1 being WGraph st b1 = GSq . x holds b1 is nonnegative-weighted by Def28; end; registration let GSq be real-elabeled EGraphSeq; let x be Nat; clusterGSq . x -> real-elabeled for EGraph; coherence for b1 being EGraph st b1 = GSq . x holds b1 is real-elabeled by Def29; end; registration let GSq be real-vlabeled VGraphSeq; let x be Nat; clusterGSq . x -> real-vlabeled for VGraph; coherence for b1 being VGraph st b1 = GSq . x holds b1 is real-vlabeled by Def30; end; begin 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 by Lm1; theorem :: GLIB_003:6 for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G by Lm2; :: Theorems regarding G.set() theorem :: GLIB_003:7 for G being _Graph for X being set holds ( G == G .set (WeightSelector,X) & G == G .set (ELabelSelector,X) & G == G .set (VLabelSelector,X) ) by Lm3; :: Theorems regarding WSubgraphs theorem :: GLIB_003:8 for G1, G2, 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 proofend; theorem :: GLIB_003:9 for G1 being WGraph for G2 being WSubgraph of G1 for G3 being WSubgraph of G2 holds G3 is WSubgraph of G1 proofend; theorem :: GLIB_003:10 for G1, G2 being WGraph for G3 being WSubgraph of G1 st G1 == G2 & the_Weight_of G1 = the_Weight_of G2 holds G3 is WSubgraph of G2 proofend; theorem :: GLIB_003:11 for G1 being WGraph for G2 being WSubgraph of G1 for x being set st x in the_Edges_of G2 holds (the_Weight_of G2) . x = (the_Weight_of G1) . x proofend; :: Theorems regarding W.weightSeq() theorem Th12: :: GLIB_003:12 for G being WGraph for W being Walk of G st W is trivial holds W .weightSeq() = {} proofend; theorem :: GLIB_003:13 for G being WGraph for W being Walk of G holds len (W .weightSeq()) = W .length() proofend; theorem Th14: :: GLIB_003:14 for G being WGraph for x, y, e being set st e Joins x,y,G holds (G .walkOf (x,e,y)) .weightSeq() = <*((the_Weight_of G) . e)*> proofend; theorem Th15: :: GLIB_003:15 for G being WGraph for W being Walk of G holds (W .reverse()) .weightSeq() = Rev (W .weightSeq()) proofend; theorem Th16: :: GLIB_003:16 for G being WGraph for W1, W2 being Walk of G st W1 .last() = W2 .first() holds (W1 .append W2) .weightSeq() = (W1 .weightSeq()) ^ (W2 .weightSeq()) proofend; theorem Th17: :: GLIB_003:17 for G being WGraph for W being Walk of G for e being set st e in (W .last()) .edgesInOut() holds (W .addEdge e) .weightSeq() = (W .weightSeq()) ^ <*((the_Weight_of G) . e)*> proofend; theorem Th18: :: GLIB_003:18 for G being real-weighted WGraph for W1 being Walk of G for W2 being Subwalk of W1 ex ws being Subset of (W1 .weightSeq()) st W2 .weightSeq() = Seq ws proofend; theorem Th19: :: GLIB_003:19 for G1, G2 being WGraph for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds W1 .weightSeq() = W2 .weightSeq() proofend; theorem Th20: :: GLIB_003:20 for G1 being WGraph for G2 being WSubgraph of G1 for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 holds W1 .weightSeq() = W2 .weightSeq() proofend; :: Theorems regarding W.cost() theorem :: GLIB_003:21 for G being real-weighted WGraph for W being Walk of G st W is trivial holds W .cost() = 0 by Th12, RVSUM_1:72; theorem :: GLIB_003:22 for G being real-weighted WGraph for v1, v2 being Vertex of G for e being set st e Joins v1,v2,G holds (G .walkOf (v1,e,v2)) .cost() = (the_Weight_of G) . e proofend; theorem :: GLIB_003:23 for G being real-weighted WGraph for W being Walk of G holds W .cost() = (W .reverse()) .cost() proofend; theorem :: GLIB_003:24 for G being real-weighted WGraph for W1, W2 being Walk of G st W1 .last() = W2 .first() holds (W1 .append W2) .cost() = (W1 .cost()) + (W2 .cost()) proofend; theorem :: GLIB_003:25 for G being real-weighted WGraph for W being Walk of G for e being set st e in (W .last()) .edgesInOut() holds (W .addEdge e) .cost() = (W .cost()) + ((the_Weight_of G) . e) proofend; theorem :: GLIB_003:26 for G1, G2 being real-weighted WGraph for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 & the_Weight_of G1 = the_Weight_of G2 holds W1 .cost() = W2 .cost() by Th19; theorem :: GLIB_003:27 for G1 being real-weighted WGraph for G2 being WSubgraph of G1 for W1 being Walk of G1 for W2 being Walk of G2 st W1 = W2 holds W1 .cost() = W2 .cost() by Th20; :: Theorems regarding nonnegative-weighted WGraphs theorem Th28: :: GLIB_003:28 for G being nonnegative-weighted WGraph for W being Walk of G for n being Element of NAT st n in dom (W .weightSeq()) holds 0 <= (W .weightSeq()) . n proofend; theorem :: GLIB_003:29 for G being nonnegative-weighted WGraph for W being Walk of G holds 0 <= W .cost() proofend; theorem :: GLIB_003:30 for G being nonnegative-weighted WGraph for W1 being Walk of G for W2 being Subwalk of W1 holds W2 .cost() <= W1 .cost() proofend; theorem :: GLIB_003:31 for G being nonnegative-weighted WGraph for e being set st e in the_Edges_of G holds 0 <= (the_Weight_of G) . e proofend; :: Theorems involving G.labelEdge theorem Th32: :: GLIB_003:32 for G being EGraph for 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) proofend; theorem :: GLIB_003:33 for G being EGraph for e, x being set st e in the_Edges_of G holds (the_ELabel_of (G .labelEdge (e,x))) . e = x proofend; theorem :: GLIB_003:34 for G being EGraph for e, x being set holds G == G .labelEdge (e,x) proofend; theorem :: GLIB_003:35 for G being WEGraph for e, x being set holds the_Weight_of G = the_Weight_of (G .labelEdge (e,x)) proofend; theorem Th36: :: GLIB_003:36 for G being EVGraph for e, x being set holds the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) proofend; theorem :: GLIB_003:37 for G being EGraph for e1, e2, x being set st e1 <> e2 holds (the_ELabel_of (G .labelEdge (e1,x))) . e2 = (the_ELabel_of G) . e2 proofend; :: Theorems involving G.labelVertex theorem Th38: :: GLIB_003:38 for G being VGraph for 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) proofend; theorem :: GLIB_003:39 for G being VGraph for v, x being set st v in the_Vertices_of G holds (the_VLabel_of (G .labelVertex (v,x))) . v = x proofend; theorem :: GLIB_003:40 for G being VGraph for v, x being set holds G == G .labelVertex (v,x) proofend; theorem :: GLIB_003:41 for G being WVGraph for v, x being set holds the_Weight_of G = the_Weight_of (G .labelVertex (v,x)) proofend; theorem Th42: :: GLIB_003:42 for G being EVGraph for v, x being set holds the_ELabel_of G = the_ELabel_of (G .labelVertex (v,x)) proofend; theorem :: GLIB_003:43 for G being VGraph for v1, v2, x being set st v1 <> v2 holds (the_VLabel_of (G .labelVertex (v1,x))) . v2 = (the_VLabel_of G) . v2 proofend; :: 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 Th45: :: GLIB_003:45 for G being EGraph for e, x being set st e in the_Edges_of G holds (G .labelEdge (e,x)) .labeledE() = (G .labeledE()) \/ {e} proofend; theorem :: GLIB_003:46 for G being EGraph for e, x being set st e in the_Edges_of G holds G .labeledE() c= (G .labelEdge (e,x)) .labeledE() proofend; theorem :: GLIB_003:47 for G being finite EGraph for 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 proofend; theorem :: GLIB_003:48 for G being EGraph for 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 ) proofend; theorem :: GLIB_003:49 for G being EVGraph for v, x being set holds G .labeledE() = (G .labelVertex (v,x)) .labeledE() by Th42; theorem :: GLIB_003:50 for G being EGraph for e, x being set st e in the_Edges_of G holds e in (G .labelEdge (e,x)) .labeledE() proofend; :: 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 Th52: :: GLIB_003:52 for G being VGraph for v, x being set st v in the_Vertices_of G holds (G .labelVertex (v,x)) .labeledV() = (G .labeledV()) \/ {v} proofend; theorem :: GLIB_003:53 for G being VGraph for v, x being set st v in the_Vertices_of G holds G .labeledV() c= (G .labelVertex (v,x)) .labeledV() proofend; theorem :: GLIB_003:54 for G being finite VGraph for 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 proofend; theorem :: GLIB_003:55 for G being VGraph for 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 ) proofend; theorem :: GLIB_003:56 for G being EVGraph for e, x being set holds G .labeledV() = (G .labelEdge (e,x)) .labeledV() by Th36; theorem :: GLIB_003:57 for G being VGraph for v being Vertex of G for x being set holds v in (G .labelVertex (v,x)) .labeledV() proofend;