begin
Lm1:
for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
Lm2:
for F being Function
for x, y, z being set st z in dom (F +* (x .--> y)) & not z in dom F holds
x = z
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
for
A being
set for
b1,
b2 being
Rbag of
A st ( for
x being
set st
x in A holds
b1 . x <= b2 . x ) holds
Sum b1 <= Sum b2
theorem
for
A being
set for
b1,
b2 being
Rbag of
A st ( for
x being
set st
x in A holds
b1 . x = b2 . x ) holds
Sum b1 = Sum b2
theorem
for
A1,
A2 being
set for
b1 being
Rbag of
A1 for
b2 being
Rbag of
A2 st
b1 = b2 holds
Sum b1 = Sum b2
theorem Th8:
theorem
begin
:: deftheorem Def1 defines is_mincost_DTree_rooted_at GLIB_004:def 1 :
:: deftheorem Def2 defines is_mincost_DPath_from GLIB_004:def 2 :
definition
let G be
finite real-weighted WGraph;
let x,
y be
set ;
func G .min_DPath_cost x,
y -> Real means :
Def3:
ex
W being
DPath of
G st
(
W is_mincost_DPath_from x,
y &
it = W .cost() )
if ex
W being
DWalk of
G st
W is_Walk_from x,
y otherwise it = 0 ;
existence
( ( ex W being DWalk of G st W is_Walk_from x,y implies ex b1 being Real ex W being DPath of G st
( W is_mincost_DPath_from x,y & b1 = W .cost() ) ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) implies ex b1 being Real st b1 = 0 ) )
uniqueness
for b1, b2 being Real holds
( ( ex W being DWalk of G st W is_Walk_from x,y & ex W being DPath of G st
( W is_mincost_DPath_from x,y & b1 = W .cost() ) & ex W being DPath of G st
( W is_mincost_DPath_from x,y & b2 = W .cost() ) implies b1 = b2 ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
consistency
for b1 being Real holds verum
;
end;
:: deftheorem Def3 defines .min_DPath_cost GLIB_004:def 3 :
:: deftheorem defines WGraphSelectors GLIB_004:def 4 :
Lm3:
for G being WGraph holds WGraphSelectors c= dom G
Lm4:
for G being WGraph holds
( G == G | WGraphSelectors & the_Weight_of G = the_Weight_of (G | WGraphSelectors ) )
Lm5:
for G being WGraph holds dom (G | WGraphSelectors ) = WGraphSelectors
:: deftheorem Def5 defines .allWSubgraphs() GLIB_004:def 5 :
:: deftheorem defines .cost() GLIB_004:def 6 :
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem Th14:
begin
definition
let G be
real-weighted WGraph;
let L be
DIJK:Labeling of
G;
func DIJK:NextBestEdges L -> Subset of
(the_Edges_of G) means :
Def7:
for
e1 being
set holds
(
e1 in it iff (
e1 DSJoins dom (L `1 ),
(the_Vertices_of G) \ (dom (L `1 )),
G & ( for
e2 being
set st
e2 DSJoins dom (L `1 ),
(the_Vertices_of G) \ (dom (L `1 )),
G holds
((L `1 ) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1 ) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) );
existence
ex b1 being Subset of (the_Edges_of G) st
for e1 being set holds
( e1 in b1 iff ( e1 DSJoins dom (L `1 ),(the_Vertices_of G) \ (dom (L `1 )),G & ( for e2 being set st e2 DSJoins dom (L `1 ),(the_Vertices_of G) \ (dom (L `1 )),G holds
((L `1 ) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1 ) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e1 being set holds
( e1 in b1 iff ( e1 DSJoins dom (L `1 ),(the_Vertices_of G) \ (dom (L `1 )),G & ( for e2 being set st e2 DSJoins dom (L `1 ),(the_Vertices_of G) \ (dom (L `1 )),G holds
((L `1 ) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1 ) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) & ( for e1 being set holds
( e1 in b2 iff ( e1 DSJoins dom (L `1 ),(the_Vertices_of G) \ (dom (L `1 )),G & ( for e2 being set st e2 DSJoins dom (L `1 ),(the_Vertices_of G) \ (dom (L `1 )),G holds
((L `1 ) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((L `1 ) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines DIJK:NextBestEdges GLIB_004:def 7 :
:: deftheorem Def8 defines DIJK:Step GLIB_004:def 8 :
:: deftheorem defines DIJK:Init GLIB_004:def 9 :
:: deftheorem Def10 defines DIJK:LabelingSeq GLIB_004:def 10 :
:: deftheorem Def11 defines DIJK:CompSeq GLIB_004:def 11 :
:: deftheorem defines DIJK:SSSP GLIB_004:def 12 :
begin
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
begin
definition
let G be
real-weighted WGraph;
let L be
PRIM:Labeling of
G;
func PRIM:NextBestEdges L -> Subset of
(the_Edges_of G) means :
Def13:
for
e1 being
set holds
(
e1 in it iff (
e1 SJoins L `1 ,
(the_Vertices_of G) \ (L `1 ),
G & ( for
e2 being
set st
e2 SJoins L `1 ,
(the_Vertices_of G) \ (L `1 ),
G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) );
existence
ex b1 being Subset of (the_Edges_of G) st
for e1 being set holds
( e1 in b1 iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1 ),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1 ),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e1 being set holds
( e1 in b1 iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1 ),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1 ),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) & ( for e1 being set holds
( e1 in b2 iff ( e1 SJoins L `1 ,(the_Vertices_of G) \ (L `1 ),G & ( for e2 being set st e2 SJoins L `1 ,(the_Vertices_of G) \ (L `1 ),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def13 defines PRIM:NextBestEdges GLIB_004:def 13 :
:: deftheorem defines PRIM:Init GLIB_004:def 14 :
:: deftheorem Def15 defines PRIM:Step GLIB_004:def 15 :
:: deftheorem Def16 defines PRIM:LabelingSeq GLIB_004:def 16 :
:: deftheorem Def17 defines PRIM:CompSeq GLIB_004:def 17 :
:: deftheorem defines PRIM:MST GLIB_004:def 18 :
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
:: deftheorem Def19 defines min-cost GLIB_004:def 19 :
begin
theorem
theorem Th41:
theorem Th42:
theorem