begin
theorem
theorem Th2:
begin
:: deftheorem defines WeightSelector GLIB_003:def 1 :
WeightSelector = 5;
:: deftheorem defines ELabelSelector GLIB_003:def 2 :
ELabelSelector = 6;
:: deftheorem defines VLabelSelector GLIB_003:def 3 :
VLabelSelector = 7;
:: deftheorem Def4 defines [Weighted] GLIB_003:def 4 :
for G being GraphStruct holds
( G is [Weighted] iff ( WeightSelector in dom G & G . WeightSelector is ManySortedSet of the_Edges_of G ) );
:: deftheorem Def5 defines [ELabeled] GLIB_003:def 5 :
for G being GraphStruct holds
( G is [ELabeled] iff ( ELabelSelector in dom G & ex f being Function st
( G . ELabelSelector = f & dom f c= the_Edges_of G ) ) );
:: deftheorem Def6 defines [VLabeled] GLIB_003:def 6 :
for G being GraphStruct holds
( G is [VLabeled] iff ( VLabelSelector in dom G & ex f being Function st
( G . VLabelSelector = f & dom f c= the_Vertices_of G ) ) );
:: deftheorem defines the_Weight_of GLIB_003:def 7 :
for G being WGraph holds the_Weight_of G = G . WeightSelector;
:: deftheorem defines the_ELabel_of GLIB_003:def 8 :
for G being EGraph holds the_ELabel_of G = G . ELabelSelector;
:: deftheorem defines the_VLabel_of GLIB_003:def 9 :
for G being VGraph holds the_VLabel_of G = G . VLabelSelector;
Lm1:
for G being EGraph holds dom (the_ELabel_of G) c= the_Edges_of G
Lm2:
for G being VGraph holds dom (the_VLabel_of G) c= the_Vertices_of G
Lm3:
for G being _Graph
for X being set holds
( G .set (WeightSelector,X) == G & G .set (ELabelSelector,X) == G & G .set (VLabelSelector,X) == G )
:: deftheorem Def10 defines weight-inheriting GLIB_003:def 10 :
for G being WGraph
for G2 being [Weighted] Subgraph of G holds
( G2 is weight-inheriting iff the_Weight_of G2 = (the_Weight_of G) | (the_Edges_of G2) );
:: deftheorem Def11 defines elabel-inheriting GLIB_003:def 11 :
for G being EGraph
for G2 being [ELabeled] Subgraph of G holds
( G2 is elabel-inheriting iff the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of G2) );
:: deftheorem Def12 defines vlabel-inheriting GLIB_003:def 12 :
for G being VGraph
for G2 being [VLabeled] Subgraph of G holds
( G2 is vlabel-inheriting iff the_VLabel_of G2 = (the_VLabel_of G) | (the_Vertices_of G2) );
:: deftheorem Def13 defines real-weighted GLIB_003:def 13 :
for G being WGraph holds
( G is real-weighted iff the_Weight_of G is real-valued );
:: deftheorem Def14 defines nonnegative-weighted GLIB_003:def 14 :
for G being WGraph holds
( G is nonnegative-weighted iff rng (the_Weight_of G) c= Real>=0 );
:: deftheorem Def15 defines real-elabeled GLIB_003:def 15 :
for G being EGraph holds
( G is real-elabeled iff the_ELabel_of G is real-valued );
:: deftheorem Def16 defines real-vlabeled GLIB_003:def 16 :
for G being VGraph holds
( G is real-vlabeled iff the_VLabel_of G is real-valued );
:: deftheorem Def17 defines real-WEV GLIB_003:def 17 :
for G being WEVGraph holds
( G is real-WEV iff ( G is real-weighted & G is real-elabeled & G is real-vlabeled ) );
:: deftheorem Def18 defines .weightSeq() GLIB_003:def 18 :
for G being WGraph
for W being Walk of G
for b3 being FinSequence holds
( b3 = W .weightSeq() iff ( len b3 = len (W .edgeSeq()) & ( for n being Nat st 1 <= n & n <= len b3 holds
b3 . n = (the_Weight_of G) . ((W .edgeSeq()) . n) ) ) );
:: deftheorem defines .cost() GLIB_003:def 19 :
for G being real-weighted WGraph
for W being Walk of G holds W .cost() = Sum (W .weightSeq());
Lm4:
for x, y, X, Y being set
for f being PartFunc of X,Y st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y
:: deftheorem defines .labeledE() GLIB_003:def 20 :
for G being EGraph holds G .labeledE() = dom (the_ELabel_of G);
:: deftheorem Def21 defines .labelEdge GLIB_003:def 21 :
for G being EGraph
for e, x being set holds
( ( e in the_Edges_of G implies G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) ) & ( not e in the_Edges_of G implies G .labelEdge (e,x) = G ) );
:: deftheorem Def22 defines .labelVertex GLIB_003:def 22 :
for G being VGraph
for v, x being set holds
( ( v in the_Vertices_of G implies G .labelVertex (v,x) = G .set (VLabelSelector,((the_VLabel_of G) +* (v .--> x))) ) & ( not v in the_Vertices_of G implies G .labelVertex (v,x) = G ) );
:: deftheorem defines .labeledV() GLIB_003:def 23 :
for G being VGraph holds G .labeledV() = dom (the_VLabel_of G);
:: deftheorem Def24 defines [Weighted] GLIB_003:def 24 :
for GSq being GraphSeq holds
( GSq is [Weighted] iff for x being Nat holds GSq . x is [Weighted] );
:: deftheorem Def25 defines [ELabeled] GLIB_003:def 25 :
for GSq being GraphSeq holds
( GSq is [ELabeled] iff for x being Nat holds GSq . x is [ELabeled] );
:: deftheorem Def26 defines [VLabeled] GLIB_003:def 26 :
for GSq being GraphSeq holds
( GSq is [VLabeled] iff for x being Nat holds GSq . x is [VLabeled] );
:: deftheorem Def27 defines real-weighted GLIB_003:def 27 :
for GSq being WGraphSeq holds
( GSq is real-weighted iff for x being Nat holds GSq . x is real-weighted );
:: deftheorem Def28 defines nonnegative-weighted GLIB_003:def 28 :
for GSq being WGraphSeq holds
( GSq is nonnegative-weighted iff for x being Nat holds GSq . x is nonnegative-weighted );
:: deftheorem Def29 defines real-elabeled GLIB_003:def 29 :
for GSq being EGraphSeq holds
( GSq is real-elabeled iff for x being Nat holds GSq . x is real-elabeled );
:: deftheorem Def30 defines real-vlabeled GLIB_003:def 30 :
for GSq being VGraphSeq holds
( GSq is real-vlabeled iff for x being Nat holds GSq . x is real-vlabeled );
:: deftheorem Def31 defines real-WEV GLIB_003:def 31 :
for GSq being WEVGraphSeq holds
( GSq is real-WEV iff for x being Nat holds GSq . x is real-WEV );
begin
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th35:
theorem
theorem
theorem
theorem Th39:
theorem
theorem
theorem
theorem Th43:
theorem
theorem Th45:
theorem
theorem
theorem
theorem Th49:
theorem
theorem
theorem Th52:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th59:
theorem
theorem
theorem
theorem
theorem