:: Weighted and Labeled Graphs
:: by Gilbert Lee
::
:: Received February 22, 2005
:: Copyright (c) 2005-2026 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, NUMBER09;
notations TARSKI, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, XCMPLX_0,
XXREAL_0, XREAL_0, DOMAIN_1, RELAT_1, PARTFUN1, FUNCT_1, PBOOLE,
RELSET_1, FUNCT_2, VALUED_0, GRAPH_5, RVSUM_1, FINSEQ_5, FINSEQ_1,
FINSET_1, NAT_1, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001, GLIB_002,
RECDEF_1;
constructors DOMAIN_1, BINOP_2, FINSOP_1, RVSUM_1, FINSEQ_5, GRAPH_5,
GLIB_001, GLIB_002, RECDEF_1, RELSET_1, FINSEQ_6;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, GLIB_000, GLIB_002, INT_1,
VALUED_0, CARD_1, FUNCT_2, PARTFUN1, RELSET_1, FINSEQ_6;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
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; :: redefines Seq (FINSEQ_1, definition)
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 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 FINSEQ_1:def 14;
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 A23,A24,FINSEQ_1:def 14;
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 15;
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;
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 FINSEQ_1:def 14;
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 15;
then
A78: q.n = fss.x1 by A73,A77,FUNCT_1:12;
A79: Seq fssq = fssq * Sgm(dom fssq) by FINSEQ_1:def 15;
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 {x} is included_in_Seg by FINSEQ_1:def 13;
then Sgm(dom fss) = Sgm(dom fssq) ^ Sgm({x}) by 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;
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; :: redefines .weightSeq() (GLIB_003, definition)
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
.= <* (the_Weight_of G).e *>.n by A6;
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
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;
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 FINSEQ_1:def 14;
let n be Nat;
A17: Seq ws = ws * Sgm(dom es) by A2,FINSEQ_1:def 15;
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 15
,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;