:: Weighted and Labeled Graphs :: by Gilbert Lee :: :: Received February 22, 2005 :: Copyright (c) 2005-2019 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, GRAPH_2, GLIB_002, INT_1, VALUED_0, CARD_1, FUNCT_2, PARTFUN1, RELSET_1, FINSEQ_6; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; equalities GLIB_000, FUNCOP_1, RVSUM_1; expansions GLIB_000; theorems CARD_1, CARD_2, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, FINSET_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, GLIB_001, GLIB_002, GRAPH_2, GRAPH_5, INT_1, NAT_1, POLYNOM3, RELAT_1, RELSET_1, RVSUM_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, XXREAL_0, ENUMSET1, ORDERS_1, ORDINAL1, FINSOP_1, VALUED_0, PARTFUN1, XTUPLE_0, FINSEQ_6; schemes NAT_1, FINSEQ_1, FUNCT_1; begin :: Preliminaries definition let D be set, fs be FinSequence of D, fss be Subset of fs; redefine func Seq fss -> FinSequence of D; correctness proof now let y be object; assume y in rng Seq fss; then consider x being object such that A1: x in dom Seq fss and A2: (Seq fss).x = y by FUNCT_1:def 3; reconsider x as Element of NAT by A1; ex n being Element of NAT st n in dom fs & x <= n & y = fs.n by A1,A2, GLIB_001:4; then y in rng fs by FUNCT_1:def 3; hence y in D; end; then rng Seq fss c= D by TARSKI:def 3; hence thesis by FINSEQ_1:def 4; end; end; theorem 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 proof let x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 be set, p be FinSequence; set pa = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>; A1: pa.1 = x1 & pa.2 = x2 by FINSEQ_1:71; A2: pa.5 = x5 & pa.6 = x6 by FINSEQ_1:71; A3: pa.7 = x7 & pa.8 = x8 by FINSEQ_1:71; A4: len pa = 9 by FINSEQ_1:71; then A5: dom pa = Seg 9 by FINSEQ_1:def 3; then A6: 3 in dom pa & 4 in dom pa by FINSEQ_1:1; A7: pa.9 = x9 & 9 in dom pa by A5,FINSEQ_1:1,71; assume A8: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>^ <*x10*>; hence len p = len pa + len <*x10*> by FINSEQ_1:22 .= 9 + 1 by A4,FINSEQ_1:40 .= 10; A9: pa.3 = x3 & pa.4 = x4 by FINSEQ_1:71; A10: 7 in dom pa & 8 in dom pa by A5,FINSEQ_1:1; A11: 5 in dom pa & 6 in dom pa by A5,FINSEQ_1:1; 1 in dom pa & 2 in dom pa by A5,FINSEQ_1:1; hence 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 by A8,A1,A9,A2,A3,A6,A11,A10,A7,FINSEQ_1:def 7; thus p.10 = p.(len pa + 1) by A4 .= x10 by A8,FINSEQ_1:42; end; theorem Th2: 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 proof let fs be FinSequence of REAL, fss be Subset of fs; defpred P[Nat] means for fs being FinSequence of REAL, fss being Subset of fs st (for i being Element of NAT st i in dom fs holds 0 <= fs.i) & len Seq fss = \$1 holds Sum (Seq fss) <= Sum fs; assume A1: for i being Element of NAT st i in dom fs holds 0 <= fs.i; A2: len Seq fss = len Seq fss; now let k be Nat; assume A3: P[k]; let fs be FinSequence of REAL, fss be Subset of fs; assume that A4: for i being Element of NAT st i in dom fs holds 0 <= fs.i and A5: len Seq fss = k+1; consider q being (FinSequence of REAL), z being Element of REAL such that A6: Seq fss = q^<*z*> by A5,FINSEQ_2:19; card fss = k + 1 by A5,GLIB_001:5; then dom fss <> {} by CARD_1:27,RELAT_1:41; then consider d being object such that A7: d in dom fss by XBOOLE_0:def 1; A8: dom fss c= dom fs by FINSEQ_6:151; then A9: d in dom fs by A7; defpred P2[Nat] means \$1 in dom fss; consider L being Nat such that A10: dom fss c= Seg L by FINSEQ_1:def 12; A11: for n being Nat st P2[n] holds n <= L by A10,FINSEQ_1:1; reconsider d as Element of NAT by A9; d in dom fss by A7; then A12: ex d being Nat st P2[d]; consider x being Nat such that A13: P2[x] & for n being Nat st P2[n] holds n <= x from NAT_1:sch 6( A11,A12); set y = fs.x; A14: len Seq fss = len q + len <*z*> by A6,FINSEQ_1:22; then A15: k + 1 = len q + 1 by A5,FINSEQ_1:39; now set g = Sgm(dom fss); 1 <= k+1 by NAT_1:12; then A16: len Seq fss in dom Seq fss by A5,FINSEQ_3:25; A17: len Seq fss = card fss by GLIB_001:5 .= card dom fss by CARD_1:62 .= len Sgm(dom fss) by A10,FINSEQ_3:39; A18: now set k2 = g.(len g); assume A19: g.(len Seq fss) <> x; 1 <= len g by A5,A17,NAT_1:12; then len g in dom g by FINSEQ_3:25; then A20: k2 in rng g by FUNCT_1:def 3; reconsider k2 as Element of NAT; A21: rng g = dom fss by A10,FINSEQ_1:def 13; then consider v being object such that A22: v in dom g and A23: g.v = x by A13,FUNCT_1:def 3; reconsider v as Element of NAT by A22; v <= len g by A22,FINSEQ_3:25; then A24: v < len g by A17,A19,A23,XXREAL_0:1; 1 <= v by A22,FINSEQ_3:25; then x < k2 by A10,A23,A24,FINSEQ_1:def 13; hence contradiction by A13,A21,A20; end; (Seq fss).(len Seq fss) = z & Seq fss = (fss * Sgm(dom fss)) by A5,A6,A15 ,FINSEQ_1:42,def 14; then fss.(Sgm(dom fss).(len Seq fss)) = z by A16,FUNCT_1:12; then [x,z] in fss by A13,A18,FUNCT_1:1; hence y = z by FUNCT_1:1; end; then A25: Sum (Seq fss) = y + Sum q by A6,RVSUM_1:74; A26: x <= len fs by A8,A13,FINSEQ_3:25; then consider j being Nat such that A27: x + j = len fs by NAT_1:10; A28: 1 <= x by A8,A13,FINSEQ_3:25; then reconsider xx1 = x-1 as Element of NAT by INT_1:5; set fssq = fss | Seg xx1; reconsider fssq as Subset of fs by FINSEQ_6:153; consider fsD, fsC being FinSequence of REAL such that A29: len fsD = x and len fsC = j and A30: fs = fsD ^ fsC by A27,FINSEQ_2:23; A31: xx1 + 1 = x; then consider fsA, fsB being FinSequence of REAL such that A32: len fsA = xx1 and A33: len fsB = 1 and A34: fsD = fsA ^ fsB by A29,FINSEQ_2:23; x in dom fsD by A28,A29,FINSEQ_3:25; then A35: y = fsD.x by A30,FINSEQ_1:def 7; now let z be object; assume A36: z in fssq; then consider a,b being object such that A37: z = [a,b] by RELAT_1:def 1; A38: a in Seg xx1 by A36,A37,RELAT_1:def 11; then reconsider a as Element of NAT; A39: a <= xx1 by A38,FINSEQ_1:1; A40: 1 <= a by A38,FINSEQ_1:1; then A41: a in dom fsA by A32,A39,FINSEQ_3:25; A42: b = fs.a by A36,A37,FUNCT_1:1; a+0 <= x by A31,A39,XREAL_1:7; then a in dom fsD by A29,A40,FINSEQ_3:25; then b = fsD.a by A30,A42,FINSEQ_1:def 7; then b = fsA.a by A34,A41,FINSEQ_1:def 7; hence z in fsA by A37,A41,FUNCT_1:1; end; then reconsider fssq as Subset of fsA by TARSKI:def 3; now A43: now let z be object; assume z in {[x,y]}; then A44: z = [x,y] by TARSKI:def 1; [x,fss.x] in fss by A13,FUNCT_1:1; hence z in fss by A44,FUNCT_1:1; end; now [x,y] in {[x,y]} by TARSKI:def 1; then A45: [x,y] in fss by A43; let z be object; hereby assume A46: z in fssq; then consider a,b being object such that A47: z = [a,b] by RELAT_1:def 1; A48: a in Seg xx1 by A46,A47,RELAT_1:def 11; then reconsider a as Element of NAT; a <= xx1 by A48,FINSEQ_1:1; then a < x by A31,NAT_1:13; then [a,b] <> [x,y] by XTUPLE_0:1; then A49: not z in {[x,y]} by A47,TARSKI:def 1; z in fss by A46,A47,RELAT_1:def 11; hence z in fss \ {[x,y]} by A49,XBOOLE_0:def 5; end; assume A50: z in fss \ {[x,y]}; then consider a,b being object such that A51: z = [a,b] by RELAT_1:def 1; A52: a in dom fs by A50,A51,FUNCT_1:1; A53: z in fss by A50,XBOOLE_0:def 5; then A54: a in dom fss by A51,FUNCT_1:1; reconsider a as Element of NAT by A52; A55: a <= x by A13,A54; not z in {[x,y]} by A50,XBOOLE_0:def 5; then a <> x or b <> y by A51,TARSKI:def 1; then a <> x by A50,A51,A45,FUNCT_1:def 1; then a < x by A55,XXREAL_0:1; then a+1 <= x by NAT_1:13; then A56: a+1-1 <= x-1 by XREAL_1:13; 1 <= a by A52,FINSEQ_3:25; then a in Seg xx1 by A56,FINSEQ_1:1; hence z in fssq by A51,A53,RELAT_1:def 11; end; then A57: fssq = fss \ {[x,y]} by TARSKI:2; now let z be object; hereby assume A58: z in dom fss; then A59: [z, fss.z] in fss by FUNCT_1:1; then A60: z in dom fs by FUNCT_1:1; then reconsider z9 = z as Element of NAT; A61: 1 <= z9 by A60,FINSEQ_3:25; A62: z9 <= x by A13,A58; now assume not z in {x}; then z <> x by TARSKI:def 1; then z9 < xx1+1 by A62,XXREAL_0:1; then z9 <= xx1 by NAT_1:13; then z9 in Seg xx1 by A61,FINSEQ_1:1; then [z,fss.z] in fssq by A59,RELAT_1:def 11; hence z in dom fssq by FUNCT_1:1; end; hence z in (dom fssq) \/ {x} by XBOOLE_0:def 3; end; assume A63: z in (dom fssq) \/ {x}; now per cases by A63,XBOOLE_0:def 3; suppose z in dom fssq; then [z, fssq.z] in fssq by FUNCT_1:1; then [z, fssq.z] in fss by RELAT_1:def 11; hence z in dom fss by FUNCT_1:1; end; suppose z in {x}; hence z in dom fss by A13,TARSKI:def 1; end; end; hence z in dom fss; end; then A64: dom fss = (dom fssq) \/ {x} by TARSKI:2; A65: card fss = k+1 by A5,GLIB_001:5; A66: now let m,n be Nat; assume that A67: m in dom fssq and A68: n in {x}; [m,fssq.m] in fssq by A67,FUNCT_1:1; then m in Seg xx1 by RELAT_1:def 11; then A69: m <= xx1 by FINSEQ_1:1; n = x by A68,TARSKI:def 1; hence m < n by A31,A69,NAT_1:13; end; {[x,y]} c= fss by A43,TARSKI:def 3; then A70: card fssq = card fss - card {[x,y]} by A57,CARD_2:44 .= k+1-1 by A65,CARD_1:30 .= k; hence len q = len Seq(fssq) by A15,GLIB_001:5; let n be Nat; set x1 = Sgm(dom fss).n, x2 = Sgm(dom fssq).n; assume that A71: 1 <= n and A72: n <= len q; n in dom q by A71,A72,FINSEQ_3:25; then A73: q.n = (Seq fss).n by A6,FINSEQ_1:def 7; A74: ex lk being Nat st dom fssq c= Seg lk by FINSEQ_1:def 12; then len Sgm (dom fssq) = card dom fssq by FINSEQ_3:39 .= k by A70,CARD_1:62; then A75: n in dom Sgm(dom fssq) by A15,A71,A72,FINSEQ_3:25; then x2 in rng Sgm(dom fssq) by FUNCT_1:def 3; then x2 in dom fssq by A74,FINSEQ_1:def 13; then [x2,fssq.x2] in fssq by FUNCT_1:1; then [x2,fssq.x2] in fss by RELAT_1:def 11; then A76: fss.x2 = fssq.x2 by FUNCT_1:1; n <= k+1 by A5,A14,A72,NAT_1:12; then A77: n in dom Seq(fss) by A5,A71,FINSEQ_3:25; Seq fss = fss * Sgm (dom fss) by FINSEQ_1:def 14; then A78: q.n = fss.x1 by A73,A77,FUNCT_1:12; A79: Seq fssq = fssq * Sgm(dom fssq) by FINSEQ_1:def 14; len Seq fssq = card fssq by GLIB_001:5; then n in dom Seq fssq by A15,A70,A71,A72,FINSEQ_3:25; then A80: (Seq fssq).n = fssq.x2 by A79,FUNCT_1:12; now let z be object; assume z in {x}; then z = x by TARSKI:def 1; hence z in Seg len fs by A28,A26,FINSEQ_1:1; end; then {x} c= Seg len fs by TARSKI:def 3; then Sgm(dom fss) = Sgm(dom fssq) ^ Sgm({x}) by A74,A64,A66,FINSEQ_3:42; hence q.n = (Seq fssq).n by A78,A80,A75,A76,FINSEQ_1:def 7; end; then A81: q = Seq fssq by FINSEQ_1:14; now A82: dom fsD c= dom fs by A30,FINSEQ_1:26; let i be Element of NAT; A83: dom fsA c= dom fsD by A34,FINSEQ_1:26; assume A84: i in dom fsA; then fsA.i = fsD.i by A34,FINSEQ_1:def 7; then A85: fsA.i = fs.i by A30,A84,A83,FINSEQ_1:def 7; i in dom fsD by A84,A83; hence 0 <= fsA.i by A4,A85,A82; end; then Sum q <= Sum fsA by A3,A15,A81; then Sum (Seq fss) + Sum q <= y + Sum q + Sum fsA by A25,XREAL_1:7; then Sum (Seq fss) + Sum q <= y + Sum fsA + Sum q; then A86: Sum (Seq fss) <= Sum fsA + y by XREAL_1:6; now let i be Nat; assume i in dom fsC; then fs.(x+i) = fsC.i & x+i in dom fs by A29,A30,FINSEQ_1:28,def 7; hence 0 <= fsC.i by A4; end; then A87: 0 <= Sum fsC by RVSUM_1:84; 1 in dom fsB by A33,FINSEQ_3:25; then y = fsB.1 by A31,A32,A34,A35,FINSEQ_1:def 7; then A88: fsB = <* y *> by A33,FINSEQ_1:40; reconsider y as Element of REAL by XREAL_0:def 1; Sum fs = Sum fsD + Sum fsC by A30,RVSUM_1:75 .= Sum fsA + Sum <*y*> + Sum fsC by A34,A88,RVSUM_1:75 .= Sum fsA + y + Sum fsC by FINSOP_1:11; then Sum fsA + y + (0 qua Nat) <= Sum fs by A87,XREAL_1:7; hence Sum (Seq fss) <= Sum fs by A86,XXREAL_0:2; end; then A89: for k being Nat st P[k] holds P[k+1]; now let fs be FinSequence of REAL, fss be Subset of fs; assume ( for i being Element of NAT st i in dom fs holds 0 <= fs.i)& len Seq fss=0; then ( for i being Nat st i in dom fs holds 0 <= fs.i)& Seq fss = <*> REAL; hence Sum (Seq fss) <= Sum fs by RVSUM_1:72,84; end; then A90: P[ 0 ]; for k being Nat holds P[k] from NAT_1:sch 2(A90,A89); hence thesis by A1,A2; end; begin :: Definitions definition func WeightSelector -> Element of NAT equals 5; coherence; func ELabelSelector -> Element of NAT equals 6; coherence; func VLabelSelector -> Element of NAT equals 7; coherence; end; definition let G be GraphStruct; attr G is [Weighted] means :Def4: WeightSelector in dom G & G.WeightSelector is ManySortedSet of the_Edges_of G; attr G is [ELabeled] means :Def5: ELabelSelector in dom G & ex f being Function st G.ELabelSelector = f & dom f c= the_Edges_of G; attr G is [VLabeled] means :Def6: 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; existence proof set V5 = {1}, E3 = {}; set S1 = the Function of E3,V5; set W1 = the ManySortedSet of E3; set EL8 = the PartFunc of E3,REAL; set VL6 = the PartFunc of V5,REAL; set G=<*V5*>^<*E3*>^<*S1*>^<*S1*>^<*W1*>^<*EL8*>^<*VL6*>; A1: dom VL6 c= V5; A2: len G = 7 by FINSEQ_1:69; reconsider G as GraphStruct; A3: dom G = Seg 7 by A2,FINSEQ_1:def 3; then A4: SourceSelector in dom G & TargetSelector in dom G by FINSEQ_1:1; A5: WeightSelector in dom G & ELabelSelector in dom G by A3,FINSEQ_1:1; A6: G.WeightSelector = W1 & G.ELabelSelector = EL8 by FINSEQ_1:69; take G; A7: the_Vertices_of G = V5 & the_Edges_of G = E3 by FINSEQ_1:69; A8: the_Source_of G = S1 & the_Target_of G = S1 by FINSEQ_1:69; A9: VLabelSelector in dom G by A3,FINSEQ_1:1; A10: G.VLabelSelector = VL6 & dom EL8 c= E3 by FINSEQ_1:69; VertexSelector in dom G & EdgeSelector in dom G by A3,FINSEQ_1:1; hence thesis by A4,A5,A9,A7,A8,A6,A10,A1; end; 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 G. WeightSelector; coherence by Def4; end; definition let G be EGraph; func the_ELabel_of G -> Function equals G.ELabelSelector; coherence proof ex f being Function st G.ELabelSelector = f & dom f c= the_Edges_of G by Def5; hence thesis; end; end; definition let G be VGraph; func the_VLabel_of G -> Function equals G.VLabelSelector; coherence proof ex f being Function st G.VLabelSelector = f & dom f c= the_Vertices_of G by Def6; hence thesis; end; end; Lm1: for G being EGraph holds dom the_ELabel_of G c= the_Edges_of G proof let G be EGraph; ex f being Function st G.ELabelSelector = f & dom f c= the_Edges_of G by Def5 ; hence thesis; end; Lm2: for G being VGraph holds dom the_VLabel_of G c= the_Vertices_of G proof let G be VGraph; ex f being Function st G.VLabelSelector = f & dom f c= the_Vertices_of G by Def6; hence thesis; end; registration let G be _Graph, X be set; cluster G.set(WeightSelector, X) -> [Graph-like]; coherence proof not WeightSelector in _GraphSelectors by ENUMSET1:def 2; hence thesis by GLIB_000:10; end; cluster G.set(ELabelSelector, X) -> [Graph-like]; coherence proof not ELabelSelector in _GraphSelectors by ENUMSET1:def 2; hence thesis by GLIB_000:10; end; cluster G.set(VLabelSelector, X) -> [Graph-like]; coherence proof not VLabelSelector in _GraphSelectors by ENUMSET1:def 2; hence thesis by GLIB_000:10; end; end; Lm3: for G being _Graph, X being set holds G.set(WeightSelector ,X) == G & G .set(ELabelSelector ,X) == G & G.set(VLabelSelector ,X) == G proof set GS = _GraphSelectors; let G be _Graph, X be set; set G2 = G.set(WeightSelector,X); A1: not WeightSelector in GS by ENUMSET1:def 2; then A2: the_Source_of G2 = the_Source_of G & the_Target_of G2 = the_Target_of G by GLIB_000:10; the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = the_Edges_of G by A1,GLIB_000:10; hence G2 == G by A2; set G2 = G.set(ELabelSelector,X); A3: not ELabelSelector in GS by ENUMSET1:def 2; then A4: the_Source_of G2 = the_Source_of G & the_Target_of G2 = the_Target_of G by GLIB_000:10; the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = the_Edges_of G by A3,GLIB_000:10; hence G2 == G by A4; set G2 = G.set(VLabelSelector,X); A5: not VLabelSelector in GS by ENUMSET1:def 2; then A6: the_Source_of G2 = the_Source_of G & the_Target_of G2 = the_Target_of G by GLIB_000:10; the_Vertices_of G2 = the_Vertices_of G & the_Edges_of G2 = the_Edges_of G by A5,GLIB_000:10; hence thesis by A6; end; registration let G be finite _Graph, X be set; cluster G.set(WeightSelector, X) -> finite; coherence proof G.set(WeightSelector,X) == G by Lm3; hence thesis; end; cluster G.set(ELabelSelector, X) -> finite; coherence proof G.set(ELabelSelector, X) == G by Lm3; hence thesis; end; cluster G.set(VLabelSelector, X) -> finite; coherence proof G.set(VLabelSelector, X) == G by Lm3; hence thesis; end; end; registration let G be loopless _Graph, X be set; cluster G.set(WeightSelector, X) -> loopless; coherence proof G.set(WeightSelector,X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(ELabelSelector, X) -> loopless; coherence proof G.set(ELabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(VLabelSelector, X) -> loopless; coherence proof G.set(VLabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; end; registration let G be trivial _Graph, X be set; cluster G.set(WeightSelector, X) -> trivial; coherence proof G.set(WeightSelector,X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(ELabelSelector, X) -> trivial; coherence proof G.set(ELabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(VLabelSelector, X) -> trivial; coherence proof G.set(VLabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; end; registration let G be non trivial _Graph, X be set; cluster G.set(WeightSelector, X) -> non trivial; coherence proof G.set(WeightSelector,X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(ELabelSelector, X) -> non trivial; coherence proof G.set(ELabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(VLabelSelector, X) -> non trivial; coherence proof G.set(VLabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; end; registration let G be non-multi _Graph, X be set; cluster G.set(WeightSelector, X) -> non-multi; coherence proof G.set(WeightSelector,X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(ELabelSelector, X) -> non-multi; coherence proof G.set(ELabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(VLabelSelector, X) -> non-multi; coherence proof G.set(VLabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; end; registration let G be non-Dmulti _Graph, X be set; cluster G.set(WeightSelector, X) -> non-Dmulti; coherence proof G.set(WeightSelector,X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(ELabelSelector, X) -> non-Dmulti; coherence proof G.set(ELabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; cluster G.set(VLabelSelector, X) -> non-Dmulti; coherence proof G.set(VLabelSelector, X) == G by Lm3; hence thesis by GLIB_000:89; end; end; registration let G be connected _Graph, X be set; cluster G.set(WeightSelector, X) -> connected; coherence proof G.set(WeightSelector,X) == G by Lm3; hence thesis by GLIB_002:8; end; cluster G.set(ELabelSelector, X) -> connected; coherence proof G.set(ELabelSelector, X) == G by Lm3; hence thesis by GLIB_002:8; end; cluster G.set(VLabelSelector, X) -> connected; coherence proof G.set(VLabelSelector, X) == G by Lm3; hence thesis by GLIB_002:8; end; end; registration let G be acyclic _Graph, X be set; cluster G.set(WeightSelector, X) -> acyclic; coherence proof G.set(WeightSelector,X) == G by Lm3; hence thesis by GLIB_002:44; end; cluster G.set(ELabelSelector, X) -> acyclic; coherence proof G.set(ELabelSelector, X) == G by Lm3; hence thesis by GLIB_002:44; end; cluster G.set(VLabelSelector, X) -> acyclic; coherence proof G.set(VLabelSelector, X) == G by Lm3; hence thesis by GLIB_002:44; end; end; registration let G be WGraph, X be set; cluster G.set(ELabelSelector, X) -> [Weighted]; coherence proof set G1 = G.set(ELabelSelector,X); dom G c= dom G1 & WeightSelector in dom G by Def4,FUNCT_4:10; hence WeightSelector in dom G1; G == G1 by Lm3; then A1: the_Edges_of G1 = the_Edges_of G; G1.WeightSelector = the_Weight_of G by GLIB_000:9; hence thesis by A1; end; cluster G.set(VLabelSelector, X) -> [Weighted]; coherence proof set G1 = G.set(VLabelSelector,X); dom G c= dom G1 & WeightSelector in dom G by Def4,FUNCT_4:10; hence WeightSelector in dom G1; G == G1 by Lm3; then A2: the_Edges_of G1 = the_Edges_of G; G1.WeightSelector = the_Weight_of G by GLIB_000:9; hence thesis by A2; end; end; registration let G be _Graph, X be ManySortedSet of the_Edges_of G; cluster G.set(WeightSelector, X) -> [Weighted]; coherence proof set G1 = G.set(WeightSelector, X); dom G1 = dom G \/ {WeightSelector} & WeightSelector in {WeightSelector } by GLIB_000:7,TARSKI:def 1; hence WeightSelector in dom G1 by XBOOLE_0:def 3; G == G1 by Lm3; then the_Edges_of G = the_Edges_of G1; hence thesis by GLIB_000:8; end; 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]; coherence; end; registration let G be EGraph, X be set; cluster G.set(WeightSelector, X) -> [ELabeled]; coherence proof set G1 = G.set(WeightSelector,X); dom G c= dom G1 & ELabelSelector in dom G by Def5,FUNCT_4:10; hence ELabelSelector in dom G1; G == G1 by Lm3; then A1: the_Edges_of G = the_Edges_of G1; G1.ELabelSelector = the_ELabel_of G & dom the_ELabel_of G c= the_Edges_of G by Lm1,GLIB_000:9; hence thesis by A1; end; cluster G.set(VLabelSelector, X) -> [ELabeled]; coherence proof set G1 = G.set(VLabelSelector,X); dom G c= dom G1 & ELabelSelector in dom G by Def5,FUNCT_4:10; hence ELabelSelector in dom G1; G == G1 by Lm3; then A2: the_Edges_of G = the_Edges_of G1; G1.ELabelSelector = the_ELabel_of G & dom the_ELabel_of G c= the_Edges_of G by Lm1,GLIB_000:9; hence thesis by A2; end; end; registration let G be _Graph, Y be set, X be PartFunc of the_Edges_of G, Y; cluster G.set(ELabelSelector, X) -> [ELabeled]; coherence proof set G1 = G.set(ELabelSelector,X); dom G1 = dom G \/ {ELabelSelector} & ELabelSelector in {ELabelSelector } by GLIB_000:7,TARSKI:def 1; hence ELabelSelector in dom G1 by XBOOLE_0:def 3; G == G1 by Lm3; then A1: the_Edges_of G = the_Edges_of G1; dom X c= the_Edges_of G; hence thesis by A1,GLIB_000:8; end; end; registration let G be _Graph, X be ManySortedSet of the_Edges_of G; cluster G.set(ELabelSelector, X) -> [ELabeled]; coherence proof set G1 = G.set(ELabelSelector,X); dom G1 = dom G \/ {ELabelSelector} & ELabelSelector in {ELabelSelector } by GLIB_000:7,TARSKI:def 1; hence ELabelSelector in dom G1 by XBOOLE_0:def 3; G == G1 by Lm3; then A1: the_Edges_of G = the_Edges_of G1; dom X = the_Edges_of G by PARTFUN1:def 2; hence thesis by A1,GLIB_000:8; end; end; registration let G be VGraph, X be set; cluster G.set(WeightSelector, X) -> [VLabeled]; coherence proof set G1 = G.set(WeightSelector,X); dom G c= dom G1 & VLabelSelector in dom G by Def6,FUNCT_4:10; hence VLabelSelector in dom G1; G == G1 by Lm3; then A1: the_Vertices_of G = the_Vertices_of G1; G1.VLabelSelector = the_VLabel_of G & dom the_VLabel_of G c= the_Vertices_of G by Lm2,GLIB_000:9; hence thesis by A1; end; cluster G.set(ELabelSelector, X) -> [VLabeled]; coherence proof set G1 = G.set(ELabelSelector,X); dom G c= dom G1 & VLabelSelector in dom G by Def6,FUNCT_4:10; hence VLabelSelector in dom G1; G == G1 by Lm3; then A2: the_Vertices_of G = the_Vertices_of G1; G1.VLabelSelector = the_VLabel_of G & dom the_VLabel_of G c= the_Vertices_of G by Lm2,GLIB_000:9; hence thesis by A2; end; end; registration let G be _Graph, Y be set, X be PartFunc of the_Vertices_of G,Y; cluster G.set(VLabelSelector, X) -> [VLabeled]; coherence proof set G1 = G.set(VLabelSelector,X); dom G1 = dom G \/ {VLabelSelector} & VLabelSelector in {VLabelSelector } by GLIB_000:7,TARSKI:def 1; hence VLabelSelector in dom G1 by XBOOLE_0:def 3; G == G1 by Lm3; then A1: the_Vertices_of G = the_Vertices_of G1; dom X c= the_Vertices_of G; hence thesis by A1,GLIB_000:8; end; end; registration let G be _Graph, X be ManySortedSet of the_Vertices_of G; cluster G.set(VLabelSelector, X) -> [VLabeled]; coherence proof set G1 = G.set(VLabelSelector,X); dom G1 = dom G \/ {VLabelSelector} & VLabelSelector in {VLabelSelector } by GLIB_000:7,TARSKI:def 1; hence VLabelSelector in dom G1 by XBOOLE_0:def 3; G == G1 by Lm3; then A1: the_Vertices_of G = the_Vertices_of G1; dom X = the_Vertices_of G by PARTFUN1:def 2; hence thesis by A1,GLIB_000:8; end; end; registration let G be _Graph; cluster G.set(ELabelSelector, {}) -> [ELabeled]; coherence proof reconsider X ={} as PartFunc of the_Edges_of G,{} by RELSET_1:12; G.set(ELabelSelector, X) is [ELabeled]; hence thesis; end; cluster G.set(VLabelSelector, {}) -> [VLabeled]; coherence proof reconsider X ={} as PartFunc of the_Vertices_of G,{} by RELSET_1:12; G.set(VLabelSelector, X) is [VLabeled]; hence thesis; end; end; registration let G be _Graph; cluster [Weighted] [ELabeled] [VLabeled] for Subgraph of G; existence proof set W = the ManySortedSet of the_Edges_of G; set G2 = G.set(WeightSelector, W); set E = the PartFunc of the_Edges_of G2, REAL; set G3 = G2.set(ELabelSelector, E); set V = the PartFunc of the_Vertices_of G3, REAL; set G4 = G3.set(VLabelSelector, V); G == G2 & G2 == G3 by Lm3; then A1: G == G3; G3 == G4 by Lm3; then G == G4 by A1; then G4 is Subgraph of G by GLIB_000:87; hence thesis; end; end; definition let G be WGraph, G2 be [Weighted] Subgraph of G; attr G2 is weight-inheriting means :Def10: 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 :Def11: 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 :Def12: 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; existence proof reconsider GG = G as [Weighted] Subgraph of G by GLIB_000:40; take GG; thus thesis; end; end; registration let G be EGraph; cluster elabel-inheriting for [ELabeled] Subgraph of G; existence proof reconsider GG = G as [ELabeled] Subgraph of G by GLIB_000:40; take GG; dom the_ELabel_of G c= the_Edges_of G by Lm1; then the_ELabel_of GG = (the_ELabel_of G) | the_Edges_of G by RELAT_1:68; hence thesis; end; end; registration let G be VGraph; cluster vlabel-inheriting for [VLabeled] Subgraph of G; existence proof reconsider GG = G as [VLabeled] Subgraph of G by GLIB_000:40; take GG; dom the_VLabel_of G c= the_Vertices_of G by Lm2; then the_VLabel_of GG = (the_VLabel_of G) | the_Vertices_of G by RELAT_1:68 ; hence thesis; end; end; registration let G be WEGraph; cluster weight-inheriting elabel-inheriting for [Weighted] [ELabeled] Subgraph of G; existence proof reconsider GG = G as [Weighted] [ELabeled] Subgraph of G by GLIB_000:40; take GG; thus GG is weight-inheriting; dom the_ELabel_of G c= the_Edges_of G by Lm1; then the_ELabel_of GG = (the_ELabel_of G) | the_Edges_of G by RELAT_1:68; hence thesis; end; end; registration let G be WVGraph; cluster weight-inheriting vlabel-inheriting for [Weighted] [VLabeled] Subgraph of G; existence proof reconsider GG = G as [Weighted] [VLabeled] Subgraph of G by GLIB_000:40; take GG; thus GG is weight-inheriting; dom the_VLabel_of G c= the_Vertices_of G by Lm2; then the_VLabel_of GG = (the_VLabel_of G) | the_Vertices_of G by RELAT_1:68 ; hence thesis; end; end; registration let G be EVGraph; cluster elabel-inheriting vlabel-inheriting for [ELabeled] [VLabeled] Subgraph of G; existence proof reconsider GG = G as [ELabeled] [VLabeled] Subgraph of G by GLIB_000:40; take GG; dom the_ELabel_of G c= the_Edges_of G by Lm1; then the_ELabel_of GG = (the_ELabel_of G) | the_Edges_of G by RELAT_1:68; hence GG is elabel-inheriting; dom the_VLabel_of G c= the_Vertices_of G by Lm2; then the_VLabel_of GG = (the_VLabel_of G) | the_Vertices_of G by RELAT_1:68 ; hence thesis; end; end; registration let G be WEVGraph; cluster weight-inheriting elabel-inheriting vlabel-inheriting for [Weighted] [ELabeled] [VLabeled] Subgraph of G; existence proof reconsider GG = G as [Weighted] [ELabeled] [VLabeled] Subgraph of G by GLIB_000:40; take GG; thus GG is weight-inheriting; dom the_ELabel_of G c= the_Edges_of G by Lm1; then the_ELabel_of GG = (the_ELabel_of G) | the_Edges_of G by RELAT_1:68; hence GG is elabel-inheriting; dom the_VLabel_of G c= the_Vertices_of G by Lm2; then the_VLabel_of GG = (the_VLabel_of G) | the_Vertices_of G by RELAT_1:68 ; hence thesis; end; 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; existence proof now per cases; suppose A1: V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V); set X = the inducedSubgraph of G,V,E; set W = the ManySortedSet of the_Edges_of X; set G2 = X.set(WeightSelector, W); set EL = the PartFunc of the_Edges_of G2, REAL; set G3 = G2.set(ELabelSelector, EL); set VL = the PartFunc of the_Vertices_of G3, REAL; set G4 = G3.set(VLabelSelector, VL); X == G2 & G2 == G3 by Lm3; then A2: X == G3; G3 == G4 by Lm3; then A3: X == G4 by A2; then G4 is Subgraph of X by GLIB_000:87; then reconsider G4 as Subgraph of G by GLIB_000:43; the_Edges_of X = E by A1,GLIB_000:def 37; then A4: the_Edges_of G4=E by A3; the_Vertices_of X = V by A1,GLIB_000:def 37; then the_Vertices_of G4 = V by A3; then G4 is inducedSubgraph of G,V,E by A1,A4,GLIB_000:def 37; hence thesis; end; suppose A5: not (V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V)); set W = the ManySortedSet of the_Edges_of G; set G2 = G.set(WeightSelector, W); set EL = the PartFunc of the_Edges_of G2, REAL; set G3 = G2.set(ELabelSelector, EL); set VL = the PartFunc of the_Vertices_of G3, REAL; set G4 = G3.set(VLabelSelector, VL); G == G2 & G2 == G3 by Lm3; then A6: G == G3; G3 == G4 by Lm3; then A7: G == G4 by A6; then reconsider G4 as Subgraph of G by GLIB_000:87; G4 is inducedSubgraph of G,V,E by A5,A7,GLIB_000:def 37; hence thesis; end; end; hence thesis; end; end; registration let G be WGraph, V,E be set; cluster weight-inheriting for [Weighted] inducedSubgraph of G,V,E; existence proof now per cases; suppose A1: V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V); set X = the [Weighted] inducedSubgraph of G,V,E; set W = (the_Weight_of G) | the_Edges_of X; dom the_Weight_of G = the_Edges_of G by PARTFUN1:def 2; then dom W = the_Edges_of X by RELAT_1:62; then reconsider W as ManySortedSet of the_Edges_of X by PARTFUN1:def 2; set GG = X.set(WeightSelector, W); A2: GG == X by Lm3; then GG is Subgraph of X by GLIB_000:87; then reconsider GG as Subgraph of G by GLIB_000:43; A3: the_Vertices_of GG = the_Vertices_of X by A2 .= V by A1,GLIB_000:def 37; the_Edges_of GG = the_Edges_of X by A2 .= E by A1,GLIB_000:def 37; then reconsider GG as [Weighted] inducedSubgraph of G,V,E by A1,A3, GLIB_000:def 37; take GG; the_Weight_of GG = W by GLIB_000:8 .= (the_Weight_of G)|the_Edges_of GG by A2; hence GG is weight-inheriting; end; suppose A4: not (V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V)); reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG as [Weighted] inducedSubgraph of G,V,E by A4, GLIB_000:def 37; take GG; thus GG is weight-inheriting; end; end; hence thesis; end; end; registration let G be EGraph, V,E be set; cluster elabel-inheriting for [ELabeled] inducedSubgraph of G,V,E; existence proof now per cases; suppose A1: V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V); set X = the [ELabeled] inducedSubgraph of G,V,E; set EL = (the_ELabel_of G) | the_Edges_of X; reconsider EL9=EL as PartFunc of dom EL, rng EL by RELSET_1:4; reconsider EL9 as PartFunc of the_Edges_of X, rng EL by RELAT_1:58 ,RELSET_1:5; set GG = X.set(ELabelSelector, EL9); A2: GG == X by Lm3; then GG is Subgraph of X by GLIB_000:87; then reconsider GG as Subgraph of G by GLIB_000:43; A3: the_Vertices_of GG = the_Vertices_of X by A2 .= V by A1,GLIB_000:def 37; the_Edges_of GG = the_Edges_of X by A2 .= E by A1,GLIB_000:def 37; then reconsider GG as [ELabeled] inducedSubgraph of G,V,E by A1,A3, GLIB_000:def 37; take GG; the_ELabel_of GG = EL by GLIB_000:8 .= (the_ELabel_of G)|the_Edges_of GG by A2; hence GG is elabel-inheriting; end; suppose A4: not (V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V)); reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG as [ELabeled] inducedSubgraph of G,V,E by A4, GLIB_000:def 37; take GG; dom the_ELabel_of G c= the_Edges_of G by Lm1; then the_ELabel_of G = (the_ELabel_of G) | the_Edges_of G by RELAT_1:68 ; hence GG is elabel-inheriting; end; end; hence thesis; end; end; registration let G be VGraph, V,E be set; cluster vlabel-inheriting for [VLabeled] inducedSubgraph of G,V,E; existence proof now per cases; suppose A1: V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V); set X = the [VLabeled] inducedSubgraph of G,V,E; set VL = (the_VLabel_of G) | the_Vertices_of X; reconsider VL9=VL as PartFunc of dom VL, rng VL by RELSET_1:4; reconsider VL9 as PartFunc of the_Vertices_of X, rng VL by RELAT_1:58 ,RELSET_1:5; set GG = X.set(VLabelSelector, VL9); A2: GG == X by Lm3; then GG is Subgraph of X by GLIB_000:87; then reconsider GG as Subgraph of G by GLIB_000:43; A3: the_Vertices_of GG = the_Vertices_of X by A2 .= V by A1,GLIB_000:def 37; the_Edges_of GG = the_Edges_of X by A2 .= E by A1,GLIB_000:def 37; then reconsider GG as [VLabeled] inducedSubgraph of G,V,E by A1,A3, GLIB_000:def 37; take GG; the_VLabel_of GG = VL by GLIB_000:8 .= (the_VLabel_of G)|the_Vertices_of GG by A2; hence GG is vlabel-inheriting; end; suppose A4: not (V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V)); reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG as [VLabeled] inducedSubgraph of G,V,E by A4, GLIB_000:def 37; take GG; dom the_VLabel_of G c= the_Vertices_of G by Lm2; then the_VLabel_of G = (the_VLabel_of G) | the_Vertices_of G by RELAT_1:68; hence GG is vlabel-inheriting; end; end; hence thesis; end; end; registration let G be WEGraph, V,E be set; cluster weight-inheriting elabel-inheriting for [Weighted] [ELabeled] inducedSubgraph of G,V,E; existence proof now per cases; suppose A1: V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V); set X = the [Weighted] [ELabeled] inducedSubgraph of G,V,E; set W = (the_Weight_of G) | the_Edges_of X; dom the_Weight_of G = the_Edges_of G by PARTFUN1:def 2; then dom W = the_Edges_of X by RELAT_1:62; then reconsider W as ManySortedSet of the_Edges_of X by PARTFUN1:def 2; set G1 = X.set(WeightSelector, W); set EL = (the_ELabel_of G) | the_Edges_of G1; reconsider EL9=EL as PartFunc of dom EL, rng EL by RELSET_1:4; reconsider EL9 as PartFunc of the_Edges_of G1, rng EL by RELAT_1:58 ,RELSET_1:5; set G2 = G1.set(ELabelSelector, EL9); A2: G2 == G1 by Lm3; X == G1 by Lm3; then A3: G2 == X by A2; then G2 is Subgraph of X by GLIB_000:87; then reconsider G2 as Subgraph of G by GLIB_000:43; A4: the_Vertices_of G2 = the_Vertices_of X by A3 .= V by A1,GLIB_000:def 37; the_Edges_of G2 = the_Edges_of X by A3 .= E by A1,GLIB_000:def 37; then reconsider G2 as [Weighted] [ELabeled] inducedSubgraph of G,V,E by A1,A4, GLIB_000:def 37; take G2; the_Weight_of G2 = G1.WeightSelector by GLIB_000:9 .= W by GLIB_000:8 .= (the_Weight_of G)|the_Edges_of G2 by A3; hence G2 is weight-inheriting; the_ELabel_of G2 = EL by GLIB_000:8 .= (the_ELabel_of G)|the_Edges_of G2 by A2; hence G2 is elabel-inheriting; end; suppose A5: not (V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V)); reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG as [Weighted] [ELabeled] inducedSubgraph of G,V,E by A5, GLIB_000:def 37; take GG; thus GG is weight-inheriting; dom the_ELabel_of G c= the_Edges_of G by Lm1; then the_ELabel_of G = (the_ELabel_of G) | the_Edges_of G by RELAT_1:68 ; hence GG is elabel-inheriting; end; end; hence thesis; end; end; registration let G be WVGraph, V,E be set; cluster weight-inheriting vlabel-inheriting for [Weighted] [VLabeled] inducedSubgraph of G,V,E; existence proof now per cases; suppose A1: V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V); set X = the [Weighted] [VLabeled] inducedSubgraph of G,V,E; set W = (the_Weight_of G) | the_Edges_of X; dom the_Weight_of G = the_Edges_of G by PARTFUN1:def 2; then dom W = the_Edges_of X by RELAT_1:62; then reconsider W as ManySortedSet of the_Edges_of X by PARTFUN1:def 2; set G1 = X.set(WeightSelector, W); set VL = (the_VLabel_of G) | the_Vertices_of G1; reconsider VL9=VL as PartFunc of dom VL, rng VL by RELSET_1:4; reconsider VL9 as PartFunc of the_Vertices_of G1, rng VL by RELAT_1:58 ,RELSET_1:5; set G2 = G1.set(VLabelSelector, VL9); A2: G2 == G1 by Lm3; X == G1 by Lm3; then A3: G2 == X by A2; then G2 is Subgraph of X by GLIB_000:87; then reconsider G2 as Subgraph of G by GLIB_000:43; A4: the_Vertices_of G2 = the_Vertices_of X by A3 .= V by A1,GLIB_000:def 37; the_Edges_of G2 = the_Edges_of X by A3 .= E by A1,GLIB_000:def 37; then reconsider G2 as [Weighted] [VLabeled] inducedSubgraph of G,V,E by A1,A4, GLIB_000:def 37; take G2; the_Weight_of G2 = G1.WeightSelector by GLIB_000:9 .= W by GLIB_000:8 .= (the_Weight_of G)|the_Edges_of G2 by A3; hence G2 is weight-inheriting; the_VLabel_of G2 = VL by GLIB_000:8 .= (the_VLabel_of G)|the_Vertices_of G2 by A2; hence G2 is vlabel-inheriting; end; suppose A5: not (V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V)); reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG as [Weighted] [VLabeled] inducedSubgraph of G,V,E by A5, GLIB_000:def 37; take GG; thus GG is weight-inheriting; dom the_VLabel_of G c= the_Vertices_of G by Lm2; then the_VLabel_of G = (the_VLabel_of G) | the_Vertices_of G by RELAT_1:68; hence GG is vlabel-inheriting; end; end; hence thesis; end; end; registration let G be EVGraph, V,E be set; cluster elabel-inheriting vlabel-inheriting for [ELabeled] [VLabeled] inducedSubgraph of G,V,E; existence proof now per cases; suppose A1: V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V); set X = the [ELabeled] [VLabeled] inducedSubgraph of G,V,E; set EL = (the_ELabel_of G) | the_Edges_of X; reconsider EL9=EL as PartFunc of dom EL, rng EL by RELSET_1:4; reconsider EL9 as PartFunc of the_Edges_of X, rng EL by RELAT_1:58 ,RELSET_1:5; set G1 = X.set(ELabelSelector, EL9); set VL = (the_VLabel_of G) | the_Vertices_of G1; reconsider VL9=VL as PartFunc of dom VL, rng VL by RELSET_1:4; reconsider VL9 as PartFunc of the_Vertices_of G1, rng VL by RELAT_1:58 ,RELSET_1:5; set G2 = G1.set(VLabelSelector, VL9); A2: G2 == G1 by Lm3; X == G1 by Lm3; then A3: G2 == X by A2; then G2 is Subgraph of X by GLIB_000:87; then reconsider G2 as Subgraph of G by GLIB_000:43; A4: the_Vertices_of G2 = the_Vertices_of X by A3 .= V by A1,GLIB_000:def 37; the_Edges_of G2 = the_Edges_of X by A3 .= E by A1,GLIB_000:def 37; then reconsider G2 as [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A1,A4, GLIB_000:def 37; take G2; the_ELabel_of G2 = G1.ELabelSelector by GLIB_000:9 .= EL9 by GLIB_000:8 .= (the_ELabel_of G)|the_Edges_of G2 by A3; hence G2 is elabel-inheriting; the_VLabel_of G2 = VL by GLIB_000:8 .= (the_VLabel_of G)|the_Vertices_of G2 by A2; hence G2 is vlabel-inheriting; end; suppose A5: not (V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V)); reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG as [ELabeled] [VLabeled] inducedSubgraph of G,V,E by A5, GLIB_000:def 37; take GG; dom the_ELabel_of G c= the_Edges_of G by Lm1; then the_ELabel_of G = (the_ELabel_of G) | the_Edges_of G by RELAT_1:68 ; hence GG is elabel-inheriting; dom the_VLabel_of G c= the_Vertices_of G by Lm2; then the_VLabel_of G = (the_VLabel_of G) | the_Vertices_of G by RELAT_1:68; hence GG is vlabel-inheriting; end; end; hence thesis; end; 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; existence proof now per cases; suppose A1: V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V); set X = the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G ,V,E; set W = (the_Weight_of G) | the_Edges_of X; dom the_Weight_of G = the_Edges_of G by PARTFUN1:def 2; then dom W = the_Edges_of X by RELAT_1:62; then reconsider W as ManySortedSet of the_Edges_of X by PARTFUN1:def 2; set G1 = X.set(WeightSelector, W); set EL = (the_ELabel_of G) | the_Edges_of G1; reconsider EL9=EL as PartFunc of dom EL, rng EL by RELSET_1:4; reconsider EL9 as PartFunc of the_Edges_of G1, rng EL by RELAT_1:58 ,RELSET_1:5; set G2 = G1.set(ELabelSelector, EL9); set VL = (the_VLabel_of G) | the_Vertices_of G2; reconsider VL9=VL as PartFunc of dom VL, rng VL by RELSET_1:4; reconsider VL9 as PartFunc of the_Vertices_of G2, rng VL by RELAT_1:58 ,RELSET_1:5; set G3 = G2.set(VLabelSelector, VL9); A2: G2 == G1 by Lm3; A3: G3 == G2 by Lm3; X == G1 by Lm3; then G2 == X by A2; then A4: G3 == X by A3; then G3 is Subgraph of X by GLIB_000:87; then reconsider G3 as Subgraph of G by GLIB_000:43; A5: the_Vertices_of G3 = the_Vertices_of X by A4 .= V by A1,GLIB_000:def 37; the_Edges_of G3 = the_Edges_of X by A4 .= E by A1,GLIB_000:def 37; then reconsider G3 as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G ,V,E by A1,A5,GLIB_000:def 37; A6: G3 == G1 by A2,A3; take G3; the_Weight_of G3 = G2.WeightSelector by GLIB_000:9 .= G1.WeightSelector by GLIB_000:9 .= W by GLIB_000:8 .= (the_Weight_of G)|the_Edges_of G3 by A4; hence G3 is weight-inheriting; the_ELabel_of G3 = G2.ELabelSelector by GLIB_000:9 .= EL by GLIB_000:8 .= (the_ELabel_of G)|the_Edges_of G3 by A6; hence G3 is elabel-inheriting; the_VLabel_of G3 = VL by GLIB_000:8 .= (the_VLabel_of G)|the_Vertices_of G3 by A3; hence G3 is vlabel-inheriting; end; suppose A7: not (V is non empty Subset of the_Vertices_of G & E c= G .edgesBetween(V)); reconsider GG = G as Subgraph of G by GLIB_000:40; reconsider GG as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G ,V,E by A7,GLIB_000:def 37; take GG; thus GG is weight-inheriting; dom the_ELabel_of G c= the_Edges_of G by Lm1; then the_ELabel_of G = (the_ELabel_of G) | the_Edges_of G by RELAT_1:68 ; hence GG is elabel-inheriting; dom the_VLabel_of G c= the_Vertices_of G by Lm2; then the_VLabel_of G = (the_VLabel_of G) | the_Vertices_of G by RELAT_1:68; hence GG is vlabel-inheriting; end; end; hence thesis; end; 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 :Def13: the_Weight_of G is real-valued; end; definition let G be WGraph; attr G is nonnegative-weighted means :Def14: rng the_Weight_of G c= Real>=0; end; registration cluster nonnegative-weighted -> real-weighted for WGraph; coherence by XBOOLE_1:1,VALUED_0:def 3; end; definition let G be EGraph; attr G is real-elabeled means :Def15: the_ELabel_of G is real-valued; end; definition let G be VGraph; attr G is real-vlabeled means :Def16: the_VLabel_of G is real-valued; end; definition let G be WEVGraph; attr G is real-WEV means 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; coherence; cluster real-weighted real-elabeled real-vlabeled -> real-WEV for WEVGraph; coherence; end; registration let G be _Graph, X be Function of the_Edges_of G, REAL; cluster G.set(WeightSelector,X) -> real-weighted; coherence by GLIB_000:8; end; registration let G be _Graph, X be PartFunc of the_Edges_of G, REAL; cluster G.set(ELabelSelector, X) -> real-elabeled; coherence by GLIB_000:8; end; registration let G be _Graph, X be real-valued ManySortedSet of the_Edges_of G; cluster G.set(ELabelSelector,X) -> real-elabeled; coherence by GLIB_000:8; end; registration let G be _Graph, X be PartFunc of the_Vertices_of G, REAL; cluster G.set(VLabelSelector, X) -> real-vlabeled; coherence by GLIB_000:8; end; registration let G be _Graph, X be real-valued ManySortedSet of the_Vertices_of G; cluster G.set(VLabelSelector, X) -> real-vlabeled; coherence by GLIB_000:8; end; registration let G be _Graph; cluster G.set(ELabelSelector, {}) -> real-elabeled; coherence proof reconsider X = {} as PartFunc of the_Edges_of G,REAL by RELSET_1:12; G.set(ELabelSelector,X) is real-elabeled; hence thesis; end; cluster G.set(VLabelSelector, {}) -> real-vlabeled; coherence proof reconsider X = {} as PartFunc of the_Vertices_of G,REAL by RELSET_1:12; G.set(VLabelSelector,X) is real-vlabeled; hence thesis; end; end; registration let G be _Graph, v be Vertex of G, val be Real; cluster G.set(VLabelSelector, v.-->val) -> [VLabeled]; coherence proof set X = v.-->val; reconsider X = (v.-->val) as PartFunc of {v},{val}; dom (v.-->val) = {v}; then reconsider X as PartFunc of the_Vertices_of G, {val} by RELSET_1:5; rng (v.-->val) = {val} by FUNCOP_1:8; then reconsider X as PartFunc of the_Vertices_of G, REAL by RELSET_1:6; G.set(VLabelSelector,X) is real-vlabeled; hence thesis; end; end; registration let G be _Graph, v be Vertex of G, val be Real; cluster G.set(VLabelSelector, v.-->val) -> real-vlabeled; coherence proof set X = v.-->val; reconsider X = (v.-->val) as PartFunc of {v},{val}; dom (v.-->val) = {v}; then reconsider X as PartFunc of the_Vertices_of G, {val} by RELSET_1:5; for x being object st x in {val} holds x in REAL by XREAL_0:def 1; then {val} c= REAL by TARSKI:def 3; then reconsider X as PartFunc of the_Vertices_of G, REAL by RELSET_1:7; G.set(VLabelSelector,X) is real-vlabeled; hence thesis; end; end; registration cluster finite trivial Tree-like nonnegative-weighted real-WEV for WEVGraph; existence proof set E = {}; set V = {1}; reconsider S = {} as Function of E,V by RELSET_1:12; set G1 = createGraph(V,E,S,S); set WL = the Function of the_Edges_of G1, REAL; set G2 = G1.set(WeightSelector, WL); set EL = the PartFunc of the_Edges_of G2, REAL; set G3 = G2.set(ELabelSelector, EL); set VL = the PartFunc of the_Vertices_of G3, REAL; set G4 = G3.set(VLabelSelector, VL); take G4; thus G4 is finite & G4 is trivial & G4 is Tree-like; A1: the_Weight_of G4 = G3.WeightSelector by GLIB_000:9 .= G2.WeightSelector by GLIB_000:9 .= WL by GLIB_000:8; the_Edges_of G1 = {} by GLIB_000:6; then rng (the_Weight_of G4) = {} by A1; then rng (the_Weight_of G4) c= Real>=0 by XBOOLE_1:2; hence G4 is nonnegative-weighted; the_ELabel_of G4 = G3.ELabelSelector by GLIB_000:9 .= EL by GLIB_000:8; then A2: G4 is real-elabeled; G4 is real-weighted by A1; hence thesis by A2; end; cluster finite non trivial Tree-like nonnegative-weighted real-WEV for WEVGraph; existence proof set G1 = the finite non trivial Tree-like _Graph; set W = the_Edges_of G1 --> 0; A3: dom W = the_Edges_of G1; A4: rng W c= {0} by FUNCOP_1:13; then reconsider W as Function of the_Edges_of G1, REAL by A3,FUNCT_2:2; set G2 = G1.set(WeightSelector, W); reconsider EL = {} as PartFunc of the_Edges_of G2, REAL by RELSET_1:12; set G3 = G2.set(ELabelSelector, EL); reconsider VL = {} as PartFunc of the_Vertices_of G3, REAL by RELSET_1:12; set G4 = G3.set(VLabelSelector, VL); take G4; thus G4 is finite & G4 is non trivial & G4 is Tree-like; A5: the_Weight_of G4 = G3.WeightSelector by GLIB_000:9 .= G2.WeightSelector by GLIB_000:9 .= W by GLIB_000:8; for x being object st x in {0} holds x in Real>=0 by GRAPH_5:def 12; then {0} c= Real>=0 by TARSKI:def 3; then rng W c= Real>=0 by A4,XBOOLE_1:1; hence G4 is nonnegative-weighted by A5; the_ELabel_of G4 = G3.ELabelSelector by GLIB_000:9 .= EL by GLIB_000:8; then A6: G4 is real-elabeled; G4 is real-weighted by A5; hence thesis by A6; end; end; registration let G be finite WGraph; cluster the_Weight_of G -> finite; coherence proof A1: dom the_Weight_of G = the_Edges_of G by PARTFUN1:def 2; then rng the_Weight_of G is finite by FINSET_1:8; hence thesis by A1,ORDERS_1:87; end; end; registration let G be finite EGraph; cluster the_ELabel_of G -> finite; coherence proof A1: dom the_ELabel_of G c= the_Edges_of G by Lm1; then rng the_ELabel_of G is finite by FINSET_1:8; hence thesis by A1,ORDERS_1:87; end; end; registration let G be finite VGraph; cluster the_VLabel_of G -> finite; coherence proof A1: dom the_VLabel_of G c= the_Vertices_of G by Lm2; then rng the_VLabel_of G is finite by FINSET_1:8; hence thesis by A1,ORDERS_1:87; end; end; registration let G be real-weighted WGraph; cluster the_Weight_of G -> real-valued; coherence by Def13; end; registration let G be real-elabeled EGraph; cluster the_ELabel_of G -> real-valued; coherence by Def15; end; registration let G be real-vlabeled VGraph; cluster the_VLabel_of G -> real-valued; coherence by Def16; end; registration let G be real-weighted WGraph, X be set; cluster G.set(ELabelSelector ,X) -> real-weighted; coherence proof set G2 = G.set(ELabelSelector,X); the_Weight_of G2 = the_Weight_of G by GLIB_000:9; hence thesis; end; cluster G.set(VLabelSelector ,X) -> real-weighted; coherence proof set G2 = G.set(VLabelSelector,X); the_Weight_of G2 = the_Weight_of G by GLIB_000:9; hence thesis; end; end; registration let G be nonnegative-weighted WGraph, X be set; cluster G.set(ELabelSelector ,X) -> nonnegative-weighted; coherence proof set G2 = G.set(ELabelSelector,X); the_Weight_of G2 = the_Weight_of G & rng (the_Weight_of G) c= Real>=0 by Def14,GLIB_000:9; hence thesis; end; cluster G.set(VLabelSelector ,X) -> nonnegative-weighted; coherence proof set G2 = G.set(VLabelSelector,X); the_Weight_of G2 = the_Weight_of G & rng (the_Weight_of G) c= Real>=0 by Def14,GLIB_000:9; hence thesis; end; end; registration let G be real-elabeled EGraph, X be set; cluster G.set(WeightSelector ,X) -> real-elabeled; coherence proof set G2 = G.set(WeightSelector,X); the_ELabel_of G2 = the_ELabel_of G by GLIB_000:9; hence thesis; end; cluster G.set(VLabelSelector ,X) -> real-elabeled; coherence proof set G2 = G.set(VLabelSelector,X); the_ELabel_of G2 = the_ELabel_of G by GLIB_000:9; hence thesis; end; end; registration let G be real-vlabeled VGraph, X be set; cluster G.set(WeightSelector ,X) -> real-vlabeled; coherence proof set G2 = G.set(WeightSelector,X); the_VLabel_of G2 = the_VLabel_of G by GLIB_000:9; hence thesis; end; cluster G.set(ELabelSelector ,X) -> real-vlabeled; coherence proof set G2 = G.set(ELabelSelector,X); the_VLabel_of G2 = the_VLabel_of G by GLIB_000:9; hence thesis; end; end; definition let G be WGraph, W be Walk of G; func W.weightSeq() -> FinSequence means :Def18: 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 proof deffunc F(Nat) = (the_Weight_of G).(W.edgeSeq().\$1); consider IT being FinSequence such that A1: len IT =len W.edgeSeq() & for k being Nat st k in dom IT holds IT. k = F(k) from FINSEQ_1:sch 2; take IT; thus len IT = len W.edgeSeq() by A1; let n be Nat; assume 1 <= n & n <= len IT; then n in dom IT by FINSEQ_3:25; hence thesis by A1; end; uniqueness proof let IT1, IT2 be FinSequence such that A2: len IT1 = len W.edgeSeq() and A3: for n being Nat st 1 <= n & n <= len IT1 holds IT1.n = ( the_Weight_of G).(W.edgeSeq().n) and A4: len IT2 = len W.edgeSeq() and A5: for n being Nat st 1 <= n & n <= len IT2 holds IT2.n = ( the_Weight_of G).(W.edgeSeq().n); now let n be Nat; assume A6: 1 <= n & n <= len IT1; hence IT1.n = (the_Weight_of G).(W.edgeSeq().n) by A3 .= IT2.n by A2,A4,A5,A6; end; hence thesis by A2,A4,FINSEQ_1:14; end; end; definition let G be real-weighted WGraph, W be Walk of G; redefine func W.weightSeq() -> FinSequence of REAL; coherence proof now let y be object; assume y in rng W.weightSeq(); then consider x being Nat such that A1: x in dom W.weightSeq() and A2: y = W.weightSeq().x by FINSEQ_2:10; 1 <= x & x <= len W.weightSeq() by A1,FINSEQ_3:25; then y = (the_Weight_of G).(W.edgeSeq().x) by A2,Def18; hence y in REAL by XREAL_0:def 1; end; then rng W.weightSeq() c= REAL by TARSKI:def 3; hence thesis by FINSEQ_1:def 4; end; end; definition let G be real-weighted WGraph, W be Walk of G; func W.cost() -> Real equals Sum (W.weightSeq()); coherence; end; Lm4: for x,y,X,Y being set, f being PartFunc of X,Y st x in X & y in Y holds f +* (x.-->y) is PartFunc of X,Y proof let x,y,X,Y be set, f be PartFunc of X,Y; assume that A1: x in X and A2: y in Y; set F = f +* (x.-->y); A3: rng F c= rng f \/ rng (x.-->y) by FUNCT_4:17; now let z be object; assume A4: z in rng F; now per cases by A3,A4,XBOOLE_0:def 3; suppose z in rng f; hence z in Y; end; suppose z in rng (x.-->y); then z in {y} by FUNCOP_1:8; hence z in Y by A2,TARSKI:def 1; end; end; hence z in Y; end; then rng F c= Y by TARSKI:def 3; then reconsider F1=F as PartFunc of dom F,Y by RELSET_1:4; now let z be object; assume z in dom F1; then A5: z in dom f \/ dom (x.-->y) by FUNCT_4:def 1; now per cases by A5,XBOOLE_0:def 3; suppose z in dom f; hence z in X; end; suppose z in dom (x.-->y); then z in {x}; hence z in X by A1,TARSKI:def 1; end; end; hence z in X; end; then dom F1 c= X by TARSKI:def 3; hence thesis by RELSET_1:7; end; definition let G be EGraph; func G.labeledE() -> Subset of the_Edges_of G equals dom the_ELabel_of G; coherence by Lm1; end; definition let G be EGraph, e,x be object; func G.labelEdge(e,x) -> EGraph equals :Def21: G.set(ELabelSelector, the_ELabel_of G +* (e.-->x)) if e in the_Edges_of G otherwise G; coherence proof set EL = the_ELabel_of G +* (e.-->x), G2 = G.set(ELabelSelector, EL); G == G2 by Lm3; then A1: the_Edges_of G = the_Edges_of G2; hereby A2: dom EL = dom the_ELabel_of G \/ dom (e.-->x) by FUNCT_4:def 1 .= dom the_ELabel_of G \/ {e}; assume A3: e in the_Edges_of G; now let z be object; assume A4: z in dom EL; now per cases by A2,A4,XBOOLE_0:def 3; suppose A5: z in dom the_ELabel_of G; dom the_ELabel_of G c= the_Edges_of G by Lm1; hence z in the_Edges_of G by A5; end; suppose z in {e}; hence z in the_Edges_of G by A3,TARSKI:def 1; end; end; hence z in the_Edges_of G; end; then A6: dom EL c= the_Edges_of G2 by A1,TARSKI:def 3; A7: G2.ELabelSelector = EL by GLIB_000:8; ELabelSelector in dom G & dom G c= dom G2 by Def5,FUNCT_4:10; hence G2 is EGraph by A6,A7,Def5; end; thus thesis; end; consistency; end; registration let G be finite EGraph, e,x be set; cluster G.labelEdge(e,x) -> finite; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be loopless EGraph, e,x be set; cluster G.labelEdge(e,x) -> loopless; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be trivial EGraph, e,x be set; cluster G.labelEdge(e,x) -> trivial; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be non trivial EGraph, e,x be set; cluster G.labelEdge(e,x) -> non trivial; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be non-multi EGraph, e,x be set; cluster G.labelEdge(e,x) -> non-multi; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be non-Dmulti EGraph, e,x be set; cluster G.labelEdge(e,x) -> non-Dmulti; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be connected EGraph, e,x be set; cluster G.labelEdge(e,x) -> connected; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be acyclic EGraph, e,x be set; cluster G.labelEdge(e,x) -> acyclic; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be WEGraph, e,x be set; cluster G.labelEdge(e,x) -> [Weighted]; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be EVGraph, e,x be set; cluster G.labelEdge(e,x) -> [VLabeled]; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be real-weighted WEGraph, e,x be set; cluster G.labelEdge(e,x) -> real-weighted; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be nonnegative-weighted WEGraph, e,x be set; cluster G.labelEdge(e,x) -> nonnegative-weighted; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be real-elabeled EGraph, e be set, x be Real; cluster G.labelEdge(e,x) -> real-elabeled; coherence proof now per cases; suppose A1: e in the_Edges_of G; reconsider x as Element of REAL by XREAL_0:def 1; set EL = the_ELabel_of G +* (e.-->x); rng the_ELabel_of G c= REAL; then the_ELabel_of G is PartFunc of dom the_ELabel_of G, REAL by RELSET_1:4; then the_ELabel_of G is PartFunc of the_Edges_of G, REAL by Lm1, RELSET_1:5; then reconsider EL as PartFunc of the_Edges_of G, REAL by A1,Lm4; G.labelEdge(e,x) = G.set(ELabelSelector, EL) by A1,Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; registration let G be real-vlabeled EVGraph, e,x be set; cluster G.labelEdge(e,x) -> real-vlabeled; coherence proof now per cases; suppose e in the_Edges_of G; then G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)) by Def21; hence thesis; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; end; definition let G be VGraph, v,x be object; func G.labelVertex(v,x) -> VGraph equals :Def22: G.set(VLabelSelector, the_VLabel_of G +* (v.-->x)) if v in the_Vertices_of G otherwise G; coherence proof set VL = the_VLabel_of G +* (v.-->x), G2 = G.set(VLabelSelector, VL); hereby A1: dom VL = dom the_VLabel_of G \/ dom (v.-->x) by FUNCT_4:def 1; assume A2: v in the_Vertices_of G; now let y be object; assume A3: y in dom VL; now per cases by A1,A3,XBOOLE_0:def 3; suppose A4: y in dom the_VLabel_of G; dom the_VLabel_of G c= the_Vertices_of G by Lm2; hence y in the_Vertices_of G by A4; end; suppose y in dom (v.-->x); then y in {v}; hence y in the_Vertices_of G by A2,TARSKI:def 1; end; end; hence y in the_Vertices_of G; end; then dom VL c= the_Vertices_of G by TARSKI:def 3; then reconsider V1=VL as PartFunc of the_Vertices_of G,rng VL by RELSET_1:4; G2 = G.set(VLabelSelector,V1); hence G2 is VGraph; end; thus thesis; end; consistency; end; definition let G be VGraph; func G.labeledV() -> Subset of the_Vertices_of G equals dom the_VLabel_of G; coherence by Lm2; end; registration let G be finite VGraph, v,x be set; cluster G.labelVertex(v,x) -> finite; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be loopless VGraph, v,x be set; cluster G.labelVertex(v,x) -> loopless; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be trivial VGraph, v,x be set; cluster G.labelVertex(v,x) -> trivial; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be non trivial VGraph, v,x be set; cluster G.labelVertex(v,x) -> non trivial; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be non-multi VGraph, v,x be set; cluster G.labelVertex(v,x) -> non-multi; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be non-Dmulti VGraph, v,x be set; cluster G.labelVertex(v,x) -> non-Dmulti; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be connected VGraph, v,x be set; cluster G.labelVertex(v,x) -> connected; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be acyclic VGraph, v,x be set; cluster G.labelVertex(v,x) -> acyclic; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be WVGraph, v,x be set; cluster G.labelVertex(v,x) -> [Weighted]; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be EVGraph, v,x be set; cluster G.labelVertex(v,x) -> [ELabeled]; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be real-weighted WVGraph, v,x be set; cluster G.labelVertex(v,x) -> real-weighted; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be nonnegative-weighted WVGraph, v,x be set; cluster G.labelVertex(v,x) -> nonnegative-weighted; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be real-elabeled EVGraph, v,x be set; cluster G.labelVertex(v,x) -> real-elabeled; coherence proof now per cases; suppose v in the_Vertices_of G; then G.labelVertex(v,x) = G.set(VLabelSelector, the_VLabel_of G +* (v .-->x)) by Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be real-vlabeled VGraph, v be set, x be Real; cluster G.labelVertex(v,x) -> real-vlabeled; coherence proof now per cases; suppose A1: v in the_Vertices_of G; reconsider x as Element of REAL by XREAL_0:def 1; set EL = the_VLabel_of G +* (v.-->x); rng the_VLabel_of G c= REAL; then the_VLabel_of G is PartFunc of dom the_VLabel_of G, REAL by RELSET_1:4; then the_VLabel_of G is PartFunc of the_Vertices_of G, REAL by Lm2, RELSET_1:5; then reconsider EL as PartFunc of the_Vertices_of G, REAL by A1,Lm4; G.labelVertex(v,x) = G.set(VLabelSelector, EL) by A1,Def22; hence thesis; end; suppose not v in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; end; registration let G be real-weighted WGraph; cluster -> real-weighted for WSubgraph of G; coherence proof let G2 be WSubgraph of G; set W2 = (the_Weight_of G) | the_Edges_of G2; the_Weight_of G2 = W2 by Def10; hence thesis; end; end; registration let G be nonnegative-weighted WGraph; cluster -> nonnegative-weighted for WSubgraph of G; coherence proof let G2 be WSubgraph of G; now let x be object; A1: rng (the_Weight_of G) c= Real>=0 by Def14; assume x in rng (the_Weight_of G2); then A2: x in rng ((the_Weight_of G) | the_Edges_of G2) by Def10; rng ((the_Weight_of G) | the_Edges_of G2) c= rng (the_Weight_of G) by RELAT_1:70; then x in rng (the_Weight_of G) by A2; hence x in Real>=0 by A1; end; hence rng (the_Weight_of G2) c= Real>=0 by TARSKI:def 3; end; end; registration let G be real-elabeled EGraph; cluster -> real-elabeled for ESubgraph of G; coherence proof let G2 be ESubgraph of G; the_ELabel_of G2 = (the_ELabel_of G)| the_Edges_of G2 by Def11; hence thesis; end; end; registration let G be real-vlabeled VGraph; cluster -> real-vlabeled for VSubgraph of G; coherence proof let G2 be VSubgraph of G; the_VLabel_of G2 = (the_VLabel_of G)| the_Vertices_of G2 by Def12; hence thesis; end; end; definition let GSq be GraphSeq; attr GSq is [Weighted] means :Def24: for x being Nat holds GSq.x is [Weighted]; attr GSq is [ELabeled] means :Def25: for x being Nat holds GSq.x is [ELabeled]; attr GSq is [VLabeled] means :Def26: for x being Nat holds GSq.x is [VLabeled]; end; registration cluster [Weighted] [ELabeled] [VLabeled] for GraphSeq; existence proof set G = the finite loopless trivial non-multi simple real-WEV nonnegative-weighted WEVGraph; set F = NAT --> G; A1: dom F = NAT; reconsider F as ManySortedSet of NAT; reconsider F as GraphSeq; take F; now let x be Nat; x in NAT by ORDINAL1:def 12; then F.x in rng F by A1,FUNCT_1:3; then F.x in {G} by FUNCOP_1:8; hence F.x is [Weighted] & F.x is [ELabeled] & F.x is [VLabeled] by TARSKI:def 1; end; hence thesis; end; 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; coherence by Def24; end; registration let GSq be EGraphSeq, x be Nat; cluster GSq.x -> [ELabeled]for _Graph; coherence by Def25; end; registration let GSq be VGraphSeq, x be Nat; cluster GSq.x -> [VLabeled]for _Graph; coherence by Def26; end; definition let GSq be WGraphSeq; attr GSq is real-weighted means :Def27: for x being Nat holds GSq.x is real-weighted; attr GSq is nonnegative-weighted means :Def28: for x being Nat holds GSq.x is nonnegative-weighted; end; definition let GSq be EGraphSeq; attr GSq is real-elabeled means :Def29: for x being Nat holds GSq.x is real-elabeled; end; definition let GSq be VGraphSeq; attr GSq is real-vlabeled means :Def30: for x being Nat holds GSq.x is real-vlabeled; end; definition let GSq be WEVGraphSeq; attr GSq is real-WEV means for x being Nat holds GSq.x is real-WEV; end; registration cluster real-WEV -> real-weighted real-elabeled real-vlabeled for WEVGraphSeq; coherence proof let GSq be [Weighted] [ELabeled] [VLabeled] GraphSeq; assume A1: for x being Nat holds GSq.x is real-WEV; now let x be Nat; reconsider G = GSq.x as real-WEV WEVGraph by A1; G is real-WEV; hence GSq.x is real-weighted; end; hence GSq is real-weighted; now let x be Nat; reconsider G = GSq.x as real-WEV WEVGraph by A1; G is real-WEV; hence GSq.x is real-elabeled; end; hence GSq is real-elabeled; now let x be Nat; reconsider G = GSq.x as real-WEV WEVGraph by A1; G is real-WEV; hence GSq.x is real-vlabeled; end; hence thesis; end; cluster real-weighted real-elabeled real-vlabeled -> real-WEV for WEVGraphSeq; coherence proof let GSq be [Weighted] [ELabeled] [VLabeled] GraphSeq; assume A2: GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled; let x be Nat; reconsider G = GSq.x as real-weighted real-elabeled real-vlabeled WEVGraph by A2; G is real-WEV; hence thesis; end; end; registration cluster halting finite loopless trivial non-multi simple real-WEV nonnegative-weighted Tree-like for WEVGraphSeq; existence proof set G = the finite loopless trivial non-multi simple real-WEV acyclic connected Tree-like nonnegative-weighted WEVGraph; set F = NAT --> G; A1: dom F = NAT; reconsider F as ManySortedSet of NAT; reconsider F as GraphSeq; now let x be Nat; x in NAT by ORDINAL1:def 12; then F.x in rng F by A1,FUNCT_1:3; then F.x in {G} by FUNCOP_1:8; hence F.x is [Weighted] & F.x is [ELabeled] & F.x is [VLabeled] by TARSKI:def 1; end; then reconsider F as [Weighted] [ELabeled] [VLabeled] GraphSeq by Def24 ,Def25,Def26; A2: F.(1+1) = G; take F; F.1 = G; hence F is halting by A2; now let x be Nat; x in NAT by ORDINAL1:def 12; then F.x in rng F by A1,FUNCT_1:3; then F.x in {G} by FUNCOP_1:8; hence F.x is finite & F.x is loopless & F.x is trivial & F.x is non-multi & F.x is simple & F.x is real-WEV & F.x is nonnegative-weighted & F.x is Tree-like by TARSKI:def 1; end; hence thesis by GLIB_002:def 20; end; end; registration let GSq be real-weighted WGraphSeq, x be Nat; cluster GSq.x -> real-weighted for WGraph; coherence by Def27; end; registration let GSq be nonnegative-weighted WGraphSeq, x be Nat; cluster GSq.x -> nonnegative-weighted for WGraph; coherence by Def28; end; registration let GSq be real-elabeled EGraphSeq, x be Nat; cluster GSq.x -> real-elabeled for EGraph; coherence by Def29; end; registration let GSq be real-vlabeled VGraphSeq, x be Nat; cluster GSq.x -> real-vlabeled for VGraph; coherence by Def30; end; begin :: Theorems theorem WeightSelector = 5 & ELabelSelector = 6 & VLabelSelector = 7; theorem (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 for G being EGraph holds dom the_ELabel_of G c= the_Edges_of G by Lm1; theorem for G being VGraph holds dom the_VLabel_of G c= the_Vertices_of G by Lm2; :: Theorems regarding G.set() theorem for G being _Graph, 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 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 proof let G1,G2 be WGraph, G3 be WGraph; assume that A1: G1 == G2 and A2: the_Weight_of G1 = the_Weight_of G2 and A3: G1 is WSubgraph of G3; reconsider G29=G2 as [Weighted] Subgraph of G3 by A1,A3,GLIB_000:92; the_Edges_of G1 = the_Edges_of G2 by A1; then the_Weight_of G2 = (the_Weight_of G3)|the_Edges_of G2 by A2,A3,Def10; then G29 is weight-inheriting; hence thesis; end; theorem for G1 being WGraph, G2 being WSubgraph of G1, G3 being WSubgraph of G2 holds G3 is WSubgraph of G1 proof let G1 be WGraph, G2 be WSubgraph of G1, G3 be WSubgraph of G2; reconsider G39=G3 as [Weighted] Subgraph of G1 by GLIB_000:43; the_Weight_of G3=(the_Weight_of G2) | the_Edges_of G3 by Def10 .=((the_Weight_of G1) | the_Edges_of G2) | the_Edges_of G3 by Def10 .=(the_Weight_of G1)|the_Edges_of G3 by RELAT_1:74; then G39 is weight-inheriting; hence thesis; end; theorem 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 proof let G1,G2 be WGraph, G3 be WSubgraph of G1; assume that A1: G1 == G2 and A2: the_Weight_of G1 = the_Weight_of G2; reconsider G39=G3 as [Weighted] Subgraph of G2 by A1,GLIB_000:91; the_Weight_of G3 = (the_Weight_of G2) | the_Edges_of G3 by A2,Def10; then G39 is WSubgraph of G2 by Def10; hence thesis; end; theorem 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 proof let G1 be WGraph, G2 be WSubgraph of G1; let x be set; assume x in the_Edges_of G2; then A1: x in dom the_Weight_of G2 by PARTFUN1:def 2; the_Weight_of G2 = (the_Weight_of G1) | the_Edges_of G2 by Def10; hence thesis by A1,FUNCT_1:47; end; :: Theorems regarding W.weightSeq() theorem Th12: for G being WGraph, W being Walk of G holds W is trivial implies W.weightSeq() = {} proof let G be WGraph, W be Walk of G; assume W is trivial; then W.length() = 0 by GLIB_001:def 26; then len W.edgeSeq() = 0 by GLIB_001:def 18; then len W.weightSeq() = 0 by Def18; hence thesis; end; theorem for G being WGraph, W being Walk of G holds len W.weightSeq() = W .length() proof let G be WGraph, W be Walk of G; thus len W.weightSeq() = len W.edgeSeq() by Def18 .= W.length() by GLIB_001:def 18; end; theorem Th14: 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 *> proof let G be WGraph, x,y,e be set; set W = G.walkOf(x,e,y); assume e Joins x,y,G; then A1: W.edgeSeq() = <*e*> by GLIB_001:83; then len W.edgeSeq() = 1 by FINSEQ_1:39; then A2: len W.weightSeq() = 1 by Def18; A3: now let n be Nat; assume that A4: 1 <= n and A5: n <= len W.weightSeq(); A6: n = 1 by A2,A4,A5,XXREAL_0:1; hence W.weightSeq().n = (the_Weight_of G).(<*e*>.1) by A1,A5,Def18 .= (the_Weight_of G).e by FINSEQ_1:40 .= <* (the_Weight_of G).e *>.n by A6,FINSEQ_1:40; end; len W.weightSeq() = len <* (the_Weight_of G).e *> by A2,FINSEQ_1:39; hence thesis by A3,FINSEQ_1:14; end; theorem Th15: for G being WGraph, W being Walk of G holds W.reverse() .weightSeq() = Rev (W.weightSeq()) proof let G be WGraph, W be Walk of G; set W1 = W.reverse().weightSeq(), W2 = Rev (W.weightSeq()); len W.reverse() = len W by GLIB_001:21; then W.reverse().length() = W.length() by GLIB_001:113; then len W.reverse().edgeSeq() = W.length() by GLIB_001:def 18 .= len W.edgeSeq() by GLIB_001:def 18; then A1: len W1 = len W.edgeSeq() by Def18; A2: len W.weightSeq() = len W.edgeSeq() by Def18; A3: now let n be Nat; assume that A4: 1 <= n and A5: n <= len W1; A6: n in dom W.edgeSeq() by A1,A4,A5,FINSEQ_3:25; set rn = len W.weightSeq() - n + 1; reconsider rn as Element of NAT by A1,A2,A5,FINSEQ_5:1; n in Seg len W.weightSeq() by A1,A2,A4,A5,FINSEQ_1:1; then rn in Seg len W.weightSeq() by FINSEQ_5:2; then A7: 1 <= rn & rn <= len W.weightSeq() by FINSEQ_1:1; W1.n = (the_Weight_of G).(W.reverse().edgeSeq().n) by A4,A5,Def18 .= (the_Weight_of G).(Rev (W.edgeSeq()).n) by GLIB_001:84; then A8: W1.n = (the_Weight_of G).(W.edgeSeq().(len W.edgeSeq()-n+1)) by A6, FINSEQ_5:58; n in dom W.weightSeq() by A1,A2,A4,A5,FINSEQ_3:25; then W2.n = W.weightSeq().rn by FINSEQ_5:58 .= (the_Weight_of G).(W.edgeSeq().rn) by A7,Def18; hence W1.n = W2.n by A8,Def18; end; len W1 = len W2 by A1,A2,FINSEQ_5:def 3; hence thesis by A3,FINSEQ_1:14; end; theorem Th16: for G being WGraph, W1,W2 being Walk of G st W1.last() = W2 .first() holds W1.append(W2).weightSeq() = W1.weightSeq() ^ W2.weightSeq() proof let G being WGraph, W1,W2 be Walk of G; set W3 = W1.append(W2), W4 = W1.weightSeq()^W2.weightSeq(); assume A1: W1.last() = W2.first(); then W3.edgeSeq() = W1.edgeSeq() ^ W2.edgeSeq() by GLIB_001:85; then len W3.edgeSeq() = len W1.edgeSeq() + len W2.edgeSeq() by FINSEQ_1:22; then A2: len W3.weightSeq() = len W1.edgeSeq() + len W2.edgeSeq() by Def18 .= len W1.weightSeq() + len W2.edgeSeq() by Def18 .= len W1.weightSeq() + len W2.weightSeq() by Def18 .= len W4 by FINSEQ_1:22; now let n be Nat; assume A3: 1 <= n & n <= len W3.weightSeq(); then A4: W3.weightSeq().n = (the_Weight_of G).(W3.edgeSeq().n) by Def18 .= (the_Weight_of G).((W1.edgeSeq()^W2.edgeSeq()).n) by A1,GLIB_001:85; A5: n in dom W4 by A2,A3,FINSEQ_3:25; now per cases by A5,FINSEQ_1:25; suppose A6: n in dom W1.weightSeq(); then A7: 1 <= n by FINSEQ_3:25; A8: n <= len W1.weightSeq() by A6,FINSEQ_3:25; then n <= len W1.edgeSeq() by Def18; then A9: n in dom W1.edgeSeq() by A7,FINSEQ_3:25; W4.n = W1.weightSeq().n by A6,FINSEQ_1:def 7 .= (the_Weight_of G).(W1.edgeSeq().n) by A7,A8,Def18; hence W3.weightSeq().n = W4.n by A4,A9,FINSEQ_1:def 7; end; suppose ex k being Nat st k in dom W2.weightSeq() & n = len W1 .weightSeq()+k; then consider k being Nat such that A10: k in dom W2.weightSeq() and A11: n = len W1.weightSeq() + k; A12: 1 <= k by A10,FINSEQ_3:25; A13: k <= len W2.weightSeq() by A10,FINSEQ_3:25; then k <= len W2.edgeSeq() by Def18; then A14: k in dom W2.edgeSeq() by A12,FINSEQ_3:25; A15: n = len W1.edgeSeq() + k by A11,Def18; W4.n = W2.weightSeq().k by A10,A11,FINSEQ_1:def 7 .= (the_Weight_of G).(W2.edgeSeq().k) by A12,A13,Def18; hence W3.weightSeq().n = W4.n by A4,A14,A15,FINSEQ_1:def 7; end; end; hence W3.weightSeq().n = W4.n; end; hence thesis by A2,FINSEQ_1:14; end; theorem Th17: 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 *> proof let G be WGraph, W be Walk of G, e be set; set W2 = W.addEdge(e), WA = G.walkOf(W.last(),e,W.last().adj(e)); assume e in W.last().edgesInOut(); then A1: e Joins W.last(), W.last().adj(e), G by GLIB_000:67; then W2 = W.append(WA) & W.last() = WA.first() by GLIB_001:15,def 13; hence W2.weightSeq() = W.weightSeq() ^ WA.weightSeq() by Th16 .= W.weightSeq() ^ <* (the_Weight_of G).e *> by A1,Th14; end; theorem Th18: 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 proof let G be real-weighted WGraph, W1 be Walk of G, W2 be Subwalk of W1; consider es being Subset of W1.edgeSeq() such that A1: W2.edgeSeq() = Seq es by GLIB_001:def 32; deffunc F(object) = (the_Weight_of G).(es.\$1); consider ws being Function such that A2: dom ws = dom es & for x being object st x in dom es holds ws.x = F(x) from FUNCT_1:sch 3; A3: ex k being Nat st dom ws c= Seg k by A2,FINSEQ_1:def 12; then reconsider ws as FinSubsequence by FINSEQ_1:def 12; now let z be object; assume A4: z in ws; then consider x,y being object such that A5: z = [x,y] by RELAT_1:def 1; A6: x in dom es by A2,A4,A5,FUNCT_1:1; then A7: [x,es.x] in es by FUNCT_1:1; then A8: x in dom W1.edgeSeq() by FUNCT_1:1; A9: ws.x = y by A4,A5,FUNCT_1:1; reconsider x as Element of NAT by A8; x <= len W1.edgeSeq() by A8,FINSEQ_3:25; then A10: x <= len W1.weightSeq() by Def18; A11: 1 <= x by A8,FINSEQ_3:25; then A12: W1.weightSeq().x = (the_Weight_of G).(W1.edgeSeq().x) by A10,Def18; x in dom W1.weightSeq() by A11,A10,FINSEQ_3:25; then A13: [x, W1.weightSeq().x] in W1.weightSeq() by FUNCT_1:1; y = (the_Weight_of G).(es.x) by A2,A6,A9; hence z in W1.weightSeq() by A5,A7,A13,A12,FUNCT_1:1; end; then reconsider ws as Subset of W1.weightSeq() by TARSKI:def 3; take ws; A14: len Seq es = card es by GLIB_001:5 .= card dom ws by A2,CARD_1:62 .= card ws by CARD_1:62 .= len Seq ws by GLIB_001:5; then A15: len W2.weightSeq() = len Seq ws by A1,Def18; now A16: rng Sgm(dom es) = dom es by A2,A3,FINSEQ_1:def 13; let n be Nat; A17: Seq ws = ws * Sgm(dom es) by A2,FINSEQ_1:def 14; assume A18: 1 <= n & n <= len W2.weightSeq(); then A19: Seq es = es * Sgm(dom es) & n in dom Seq es by A14,A15,FINSEQ_1:def 14 ,FINSEQ_3:25; A20: n in dom Seq ws by A15,A18,FINSEQ_3:25; then n in dom Sgm(dom es) by A17,FUNCT_1:11; then A21: Sgm(dom es).n in dom es by A16,FUNCT_1:def 3; (Seq ws).n = ws.((Sgm (dom es).n)) by A17,A20,FUNCT_1:12 .= (the_Weight_of G).((es.(Sgm (dom es).n))) by A2,A21 .= (the_Weight_of G).((Seq es).n) by A19,FUNCT_1:12; hence W2.weightSeq().n = (Seq ws).n by A1,A18,Def18; end; hence thesis by A15,FINSEQ_1:14; end; theorem Th19: 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() proof let G1,G2 be WGraph, W1 be Walk of G1, W2 be Walk of G2; assume that A1: W1 = W2 and A2: the_Weight_of G1 = the_Weight_of G2; set WS1 = W1.weightSeq(), WS2 = W2.weightSeq(); A3: W1.edgeSeq() = W2.edgeSeq() by A1,GLIB_001:86; now thus len WS1 = len WS1; thus A4: len WS2 = len W1.edgeSeq() by A3,Def18 .= len WS1 by Def18; let x be Nat; assume A5: x in dom WS1; then A6: 1 <= x by FINSEQ_3:25; A7: x <= len WS1 by A5,FINSEQ_3:25; x <= len WS2 by A4,A5,FINSEQ_3:25; hence WS2.x = (the_Weight_of G2).(W2.edgeSeq().x) by A6,Def18 .= (the_Weight_of G1).(W1.edgeSeq().x) by A1,A2,GLIB_001:86 .= WS1.x by A6,A7,Def18; end; hence thesis by FINSEQ_2:9; end; theorem Th20: 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() proof let G1 be WGraph, G2 be WSubgraph of G1, W1 be Walk of G1, W2 be Walk of G2; set WS1 = W1.weightSeq(), WS2 = W2.weightSeq(); assume W1 = W2; then A1: W1.edgeSeq() = W2.edgeSeq() by GLIB_001:86; now thus len WS1 = len WS1; thus A2: len WS2 = len W1.edgeSeq() by A1,Def18 .= len WS1 by Def18; let x be Nat; assume A3: x in dom WS1; then A4: 1 <= x by FINSEQ_3:25; A5: x <= len WS2 by A2,A3,FINSEQ_3:25; then x <= len W2.edgeSeq() by Def18; then A6: x in dom W2.edgeSeq() by A4,FINSEQ_3:25; A7: x <= len WS1 by A3,FINSEQ_3:25; thus WS2.x = (the_Weight_of G2).(W2.edgeSeq().x) by A4,A5,Def18 .= ((the_Weight_of G1)|(the_Edges_of G2)).(W2.edgeSeq().x) by Def10 .= (the_Weight_of G1).(W1.edgeSeq().x) by A1,A6,FUNCT_1:49,GLIB_001:79 .= WS1.x by A4,A7,Def18; end; hence thesis by FINSEQ_2:9; end; :: Theorems regarding W.cost() theorem for G being real-weighted WGraph, W being Walk of G holds W is trivial implies W.cost() = 0 by Th12,RVSUM_1:72; theorem 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 proof let G be real-weighted WGraph, v1,v2 be Vertex of G, e be set; set W = G.walkOf(v1,e,v2); reconsider We = (the_Weight_of G).e as Element of REAL by XREAL_0:def 1; assume e Joins v1,v2,G; then W.weightSeq() = <* We *> by Th14; hence thesis by FINSOP_1:11; end; theorem for G being real-weighted WGraph, W being Walk of G holds W.cost() = W .reverse().cost() proof let G be real-weighted WGraph, W be Walk of G; thus W.cost() = Sum (Rev (W.weightSeq())) by POLYNOM3:3 .= W.reverse().cost() by Th15; end; theorem 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() proof let G be real-weighted WGraph, W1, W2 be Walk of G; set W3 = W1.append(W2); assume W1.last() = W2.first(); then W3.weightSeq() = W1.weightSeq() ^ W2.weightSeq() by Th16; hence thesis by RVSUM_1:75; end; theorem 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 proof let G be real-weighted WGraph, W be Walk of G, e be set; set W2 = W.addEdge(e); reconsider We = (the_Weight_of G). e as Element of REAL by XREAL_0:def 1; assume e in W.last().edgesInOut(); then W2.weightSeq()=W.weightSeq() ^ <*(the_Weight_of G).e*> by Th17; then Sum (W2.weightSeq()) = Sum (W.weightSeq()) + Sum <*We*> by RVSUM_1:75; hence thesis by FINSOP_1:11; end; theorem 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() by Th19; theorem 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() by Th20; :: Theorems regarding nonnegative-weighted WGraphs theorem Th28: 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 proof let G be nonnegative-weighted WGraph, W be Walk of G, n be Element of NAT; set WS = W.weightSeq(); assume A1: n in dom W.weightSeq(); then A2: 1 <= n by FINSEQ_3:25; A3: n <= len WS by A1,FINSEQ_3:25; then n <= len W.edgeSeq() by Def18; then dom the_Weight_of G = the_Edges_of G & n in dom W.edgeSeq() by A2, FINSEQ_3:25,PARTFUN1:def 2; then A4: (W.edgeSeq().n) in dom the_Weight_of G by GLIB_001:79; WS.n = (the_Weight_of G).(W.edgeSeq().n) by A2,A3,Def18; then A5: WS.n in rng (the_Weight_of G) by A4,FUNCT_1:def 3; rng (the_Weight_of G) c= Real>=0 by Def14; then WS.n in Real>=0 by A5; then ex r being Real st r = WS.n & r >= 0 by GRAPH_5:def 12; hence thesis; end; theorem for G being nonnegative-weighted WGraph, W being Walk of G holds 0 <= W.cost() proof let G be nonnegative-weighted WGraph, W be Walk of G; for i being Nat st i in dom W.weightSeq() holds 0 <= (W.weightSeq()).i by Th28; hence thesis by RVSUM_1:84; end; theorem for G being nonnegative-weighted WGraph, W1 being Walk of G, W2 being Subwalk of W1 holds W2.cost() <= W1.cost() proof let G be nonnegative-weighted WGraph, W1 be Walk of G, W2 be Subwalk of W1; (ex ws being Subset of W1.weightSeq() st W2.weightSeq() = Seq ws )& for i being Element of NAT st i in dom W1.weightSeq() holds 0 <= (W1.weightSeq()).i by Th18,Th28; hence thesis by Th2; end; theorem for G being nonnegative-weighted WGraph, e be set holds e in the_Edges_of G implies 0 <= (the_Weight_of G).e proof let G be nonnegative-weighted WGraph, e be set; assume e in the_Edges_of G; then e in dom the_Weight_of G by PARTFUN1:def 2; then A1: (the_Weight_of G).e in rng (the_Weight_of G) by FUNCT_1:3; rng (the_Weight_of G) c= Real>=0 by Def14; then (the_Weight_of G).e in Real>=0 by A1; then ex r being Real st (the_Weight_of G).e = r & r >= 0 by GRAPH_5:def 12; hence thesis; end; :: Theorems involving G.labelEdge theorem Th32: 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) proof let G be EGraph, e,x be set; assume e in the_Edges_of G; then the_ELabel_of G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x)).ELabelSelector by Def21; hence thesis by GLIB_000:8; end; theorem 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 proof let G be EGraph, e,x be set; e in {e} by TARSKI:def 1; then A1: e in dom (e.-->x); assume e in the_Edges_of G; then the_ELabel_of G.labelEdge(e,x) = the_ELabel_of G +* (e.-->x) by Th32; then (the_ELabel_of G.labelEdge(e,x)).e = (e.-->x).e by A1,FUNCT_4:13 .= x by FUNCOP_1:72; hence thesis; end; theorem for G being EGraph, e,x being set holds G == G.labelEdge(e,x) proof let G be EGraph, e,x be set; now per cases; suppose A1: e in the_Edges_of G; A2: not ELabelSelector in _GraphSelectors by ENUMSET1:def 2; A3: G.labelEdge(e,x) = G.set(ELabelSelector, the_ELabel_of G +* (e .-->x )) by A1,Def21; then A4: the_Source_of G = the_Source_of G.labelEdge(e,x) & the_Target_of G = the_Target_of G.labelEdge(e,x) by A2,GLIB_000:10; the_Vertices_of G = the_Vertices_of G.labelEdge(e,x) & the_Edges_of G = the_Edges_of G.labelEdge(e,x) by A3,A2,GLIB_000:10; hence thesis by A4; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; theorem for G being WEGraph, e,x being set holds the_Weight_of G = the_Weight_of G.labelEdge(e,x) proof let G be WEGraph, e,x be set; set G2 = G.labelEdge(e,x); now per cases; suppose e in the_Edges_of G; then G2 = G.set(ELabelSelector, the_ELabel_of G +* (e.-->x)) by Def21; hence thesis by GLIB_000:9; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; theorem Th36: for G being EVGraph, e,x being set holds the_VLabel_of G = the_VLabel_of G.labelEdge(e,x) proof let G be EVGraph, e,x be set; set G2 = G.labelEdge(e,x); now per cases; suppose e in the_Edges_of G; then G2 = G.set(ELabelSelector, the_ELabel_of G +* (e.-->x)) by Def21; hence thesis by GLIB_000:9; end; suppose not e in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; theorem 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 proof let G be EGraph, e1,e2,x be set; set G2 = G.labelEdge(e1,x); assume A1: e1 <> e2; now per cases; suppose A2: e1 in the_Edges_of G; not e2 in {e1} by A1,TARSKI:def 1; then A3: not e2 in dom (e1.-->x); the_ELabel_of G2 = the_ELabel_of G +* (e1.-->x) by A2,Th32; hence thesis by A3,FUNCT_4:11; end; suppose not e1 in the_Edges_of G; hence thesis by Def21; end; end; hence thesis; end; :: Theorems involving G.labelVertex theorem Th38: 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) proof let G be VGraph, e,x be set; assume e in the_Vertices_of G; then the_VLabel_of G.labelVertex(e,x) = G.set(VLabelSelector, the_VLabel_of G +* (e .-->x)).VLabelSelector by Def22; hence thesis by GLIB_000:8; end; theorem 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 proof let G be VGraph, e,x be set; e in {e} by TARSKI:def 1; then A1: e in dom (e.-->x); assume e in the_Vertices_of G; then the_VLabel_of G.labelVertex(e,x) = the_VLabel_of G +* (e.-->x) by Th38; then (the_VLabel_of G.labelVertex(e,x)).e = (e.-->x).e by A1,FUNCT_4:13 .= x by FUNCOP_1:72; hence thesis; end; theorem for G being VGraph, v,x being set holds G == G.labelVertex(v,x) proof let G be VGraph, e,x be set; now per cases; suppose A1: e in the_Vertices_of G; A2: not VLabelSelector in _GraphSelectors by ENUMSET1:def 2; A3: G.labelVertex(e,x) = G.set(VLabelSelector, the_VLabel_of G +* (e .-->x)) by A1,Def22; then A4: the_Source_of G = the_Source_of G.labelVertex(e,x) & the_Target_of G = the_Target_of G.labelVertex(e,x) by A2,GLIB_000:10; the_Vertices_of G = the_Vertices_of G.labelVertex(e,x) & the_Edges_of G = the_Edges_of G.labelVertex(e,x) by A3,A2,GLIB_000:10; hence thesis by A4; end; suppose not e in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; theorem for G being WVGraph, v,x being set holds the_Weight_of G = the_Weight_of G.labelVertex(v,x) proof let G be WVGraph, e,x be set; set G2 = G.labelVertex(e,x); now per cases; suppose e in the_Vertices_of G; then G2 = G.set(VLabelSelector, the_VLabel_of G +* (e.-->x)) by Def22; hence thesis by GLIB_000:9; end; suppose not e in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; theorem Th42: for G being EVGraph, v,x being set holds the_ELabel_of G = the_ELabel_of G.labelVertex(v,x) proof let G be EVGraph, e,x be set; set G2 = G.labelVertex(e,x); now per cases; suppose e in the_Vertices_of G; then G2 = G.set(VLabelSelector, the_VLabel_of G +* (e.-->x)) by Def22; hence thesis by GLIB_000:9; end; suppose not e in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; theorem 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 proof let G be VGraph, v1,v2,x be set; set G2 = G.labelVertex(v1,x); assume A1: v1 <> v2; now per cases; suppose A2: v1 in the_Vertices_of G; not v2 in {v1} by A1,TARSKI:def 1; then A3: not v2 in dom (v1.-->x); the_VLabel_of G2 = the_VLabel_of G +* (v1.-->x) by A2,Th38; hence thesis by A3,FUNCT_4:11; end; suppose not v1 in the_Vertices_of G; hence thesis by Def22; end; end; hence thesis; end; :: Theorems regarding G.labeledE() theorem for G1,G2 being EGraph st the_ELabel_of G1 = the_ELabel_of G2 holds G1 .labeledE() = G2.labeledE(); theorem Th45: for G being EGraph, e,x being set st e in the_Edges_of G holds G .labelEdge(e,x).labeledE() = G.labeledE() \/ {e} proof let G be EGraph, e,val be set; set G2 = G.labelEdge(e,val), EG = the_ELabel_of G, EG2 = the_ELabel_of G2; assume e in the_Edges_of G; then EG2 = EG +* (e.--> val) by Th32; then dom EG2 = dom EG \/ dom (e.-->val) by FUNCT_4:def 1; hence thesis; end; theorem for G being EGraph, e,x being set st e in the_Edges_of G holds G .labeledE() c= G.labelEdge(e,x).labeledE() proof let G be EGraph, e,x be set; assume e in the_Edges_of G; then G.labelEdge(e,x).labeledE() = G.labeledE() \/ {e} by Th45; hence thesis by XBOOLE_1:7; end; theorem 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 proof let G be finite EGraph, e,val be set; set G2 = G.labelEdge(e,val); set ECurr = the_ELabel_of G, ENext = the_ELabel_of G2; assume e in the_Edges_of G & not e in G.labeledE(); then A1: card (dom ECurr \/ {e}) = card (dom ECurr) + 1 & ENext = ECurr +* (e .--> val) by Th32,CARD_2:41; dom (e.-->val) = {e}; hence thesis by A1,FUNCT_4:def 1; end; theorem 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 proof let G be EGraph, e1,e2,val be set; set Gn = G.labelEdge(e1,val); assume that A1: not e2 in G.labeledE() and A2: e2 in Gn.labeledE(); e1 in the_Edges_of G by A1,A2,Def21; then the_ELabel_of Gn = (the_ELabel_of G) +* (e1 .--> val) by Th32; then e2 in dom (the_ELabel_of G) or e2 in dom (e1 .--> val) by A2,FUNCT_4:12; then e2 in {e1} by A1; hence e1 = e2 by TARSKI:def 1; thus thesis by A1,A2,Def21; end; theorem for G being EVGraph, v,x being set holds G.labeledE() = G.labelVertex( v,x).labeledE() by Th42; theorem for G being EGraph, e,x being set st e in the_Edges_of G holds e in G .labelEdge(e,x).labeledE() proof let G be EGraph, e,x be set; assume e in the_Edges_of G; then A1: G.labelEdge(e,x).labeledE() = G.labeledE() \/ {e} by Th45; e in {e} by TARSKI:def 1; hence thesis by A1,XBOOLE_0:def 3; end; :: Theorems regarding G.labeledV() theorem for G1,G2 being VGraph st the_VLabel_of G1 = the_VLabel_of G2 holds G1 .labeledV() = G2.labeledV(); theorem Th52: for G being VGraph, v,x being set st v in the_Vertices_of G holds G.labelVertex(v,x).labeledV() = G.labeledV() \/ {v} proof let G be VGraph, e,val be set; set G2 = G.labelVertex(e,val),EG=the_VLabel_of G,EG2=the_VLabel_of G2; assume e in the_Vertices_of G; then EG2 = EG +* (e.--> val) by Th38; then dom EG2 = dom EG \/ dom (e.-->val) by FUNCT_4:def 1; hence thesis; end; theorem for G being VGraph, v,x being set st v in the_Vertices_of G holds G .labeledV() c= G.labelVertex(v,x).labeledV() proof let G be VGraph, e,x be set; assume e in the_Vertices_of G; then G.labelVertex(e,x).labeledV() = G.labeledV() \/ {e} by Th52; hence thesis by XBOOLE_1:7; end; theorem 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 proof let G be finite VGraph, e,val be set; set G2 = G.labelVertex(e,val); set ECurr = the_VLabel_of G, ENext = the_VLabel_of G2; assume e in the_Vertices_of G & not e in G.labeledV(); then A1: card (dom ECurr \/ {e}) = card (dom ECurr) + 1 & ENext = ECurr +* (e .--> val) by Th38,CARD_2:41; dom (e.-->val) = {e}; hence thesis by A1,FUNCT_4:def 1; end; theorem 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 proof let G be VGraph, e1,e2,val be set; set Gn = G.labelVertex(e1,val); assume that A1: not e2 in G.labeledV() and A2: e2 in Gn.labeledV(); e1 in the_Vertices_of G by A1,A2,Def22; then the_VLabel_of Gn = (the_VLabel_of G) +* (e1 .--> val) by Th38; then e2 in dom (the_VLabel_of G) or e2 in dom (e1 .--> val) by A2,FUNCT_4:12; then e2 in {e1} by A1; hence e1 = e2 by TARSKI:def 1; thus thesis by A1,A2,Def22; end; theorem for G being EVGraph, e,x being set holds G.labeledV() = G.labelEdge(e, x).labeledV() by Th36; theorem for G being VGraph, v being Vertex of G, x being set holds v in G .labelVertex(v,x).labeledV() proof let G be VGraph, v be Vertex of G, x be set; G.labelVertex(v,x).labeledV() = G.labeledV() \/ {v} & v in {v} by Th52, TARSKI:def 1; hence thesis by XBOOLE_0:def 3; end;