begin
theorem
theorem Th2:
begin
:: deftheorem defines WeightSelector GLIB_003:def 1 :
:: deftheorem defines ELabelSelector GLIB_003:def 2 :
:: deftheorem defines VLabelSelector GLIB_003:def 3 :
:: deftheorem Def4 defines [Weighted] GLIB_003:def 4 :
:: deftheorem Def5 defines [ELabeled] GLIB_003:def 5 :
:: deftheorem Def6 defines [VLabeled] GLIB_003:def 6 :
:: deftheorem defines the_Weight_of GLIB_003:def 7 :
:: deftheorem defines the_ELabel_of GLIB_003:def 8 :
:: deftheorem defines the_VLabel_of GLIB_003:def 9 :
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 :
:: deftheorem Def11 defines elabel-inheriting GLIB_003:def 11 :
:: deftheorem Def12 defines vlabel-inheriting GLIB_003:def 12 :
:: deftheorem Def13 defines real-weighted GLIB_003:def 13 :
:: deftheorem Def14 defines nonnegative-weighted GLIB_003:def 14 :
:: deftheorem Def15 defines real-elabeled GLIB_003:def 15 :
:: deftheorem Def16 defines real-vlabeled GLIB_003:def 16 :
:: deftheorem Def17 defines real-WEV GLIB_003:def 17 :
:: deftheorem Def18 defines .weightSeq() GLIB_003:def 18 :
:: deftheorem defines .cost() GLIB_003:def 19 :
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 :
:: deftheorem Def21 defines .labelEdge GLIB_003:def 21 :
:: deftheorem Def22 defines .labelVertex GLIB_003:def 22 :
:: deftheorem defines .labeledV() GLIB_003:def 23 :
:: deftheorem Def24 defines [Weighted] GLIB_003:def 24 :
:: deftheorem Def25 defines [ELabeled] GLIB_003:def 25 :
:: deftheorem Def26 defines [VLabeled] GLIB_003:def 26 :
:: deftheorem Def27 defines real-weighted GLIB_003:def 27 :
:: deftheorem Def28 defines nonnegative-weighted GLIB_003:def 28 :
:: deftheorem Def29 defines real-elabeled GLIB_003:def 29 :
:: deftheorem Def30 defines real-vlabeled GLIB_003:def 30 :
:: deftheorem Def31 defines real-WEV GLIB_003:def 31 :
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