Tw0:
for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
Tw3:
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: :: GLIB_004:1
theorem Th2: :: GLIB_004:2
theorem Th3: :: GLIB_004:3
theorem Th4: :: GLIB_004:4
theorem Th5: :: GLIB_004:5
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 :: GLIB_004:6
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 :: GLIB_004:7
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: :: GLIB_004:8
theorem :: GLIB_004:9
:: 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:
:: GLIB_004:def 3
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 :
Lm1:
for G being WGraph holds WGraphSelectors c= dom G
Lm2:
for G being WGraph holds
( G == G .strict WGraphSelectors & the_Weight_of G = the_Weight_of (G .strict WGraphSelectors ) )
Lm3:
for G being WGraph holds dom (G .strict WGraphSelectors ) = WGraphSelectors
:: deftheorem Def10 defines .allWSubgraphs() GLIB_004:def 5 :
:: deftheorem defines .cost() GLIB_004:def 6 :
theorem Th33: :: GLIB_004:10
theorem Th34: :: GLIB_004:11
theorem Th10: :: GLIB_004:12
theorem Th11: :: GLIB_004:13
theorem Th12: :: GLIB_004:14
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 :
Def4:
:: GLIB_004:def 7
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 Def4 defines DIJK:NextBestEdges GLIB_004:def 7 :
:: deftheorem Def5 defines DIJK:Step GLIB_004:def 8 :
:: deftheorem defines DIJK:Init GLIB_004:def 9 :
:: deftheorem dDIJKSeq defines DIJK:LabelingSeq GLIB_004:def 10 :
:: deftheorem Def7 defines DIJK:CompSeq GLIB_004:def 11 :
:: deftheorem defines DIJK:SSSP GLIB_004:def 12 :
theorem Th13: :: GLIB_004:15
theorem Th14: :: GLIB_004:16
theorem Th15: :: GLIB_004:17
theorem Th16: :: GLIB_004:18
theorem Th18: :: GLIB_004:19
theorem Th19: :: GLIB_004:20
theorem Th20: :: GLIB_004:21
theorem Th21: :: GLIB_004:22
theorem Th22: :: GLIB_004:23
theorem Th23: :: GLIB_004:24
theorem Th24: :: GLIB_004:25
theorem Th25: :: GLIB_004:26
theorem :: GLIB_004:27
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 :
Def12:
:: GLIB_004:def 13
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 Def12 defines PRIM:NextBestEdges GLIB_004:def 13 :
:: deftheorem defines PRIM:Init GLIB_004:def 14 :
:: deftheorem Def14 defines PRIM:Step GLIB_004:def 15 :
:: deftheorem dPRIMSeq defines PRIM:LabelingSeq GLIB_004:def 16 :
:: deftheorem Def15 defines PRIM:CompSeq GLIB_004:def 17 :
:: deftheorem defines PRIM:MST GLIB_004:def 18 :
theorem Lm6: :: GLIB_004:28
theorem Lm7: :: GLIB_004:29
theorem Lm9: :: GLIB_004:30
theorem Lm10: :: GLIB_004:31
theorem Lm11: :: GLIB_004:32
theorem Lm12: :: GLIB_004:33
theorem Lm13: :: GLIB_004:34
theorem Lm14: :: GLIB_004:35
theorem Lm15: :: GLIB_004:36
theorem Lm16: :: GLIB_004:37
theorem Lm17: :: GLIB_004:38
theorem Lm18: :: GLIB_004:39
:: deftheorem Def17 defines min-cost GLIB_004:def 19 :
theorem :: GLIB_004:40
theorem Th36: :: GLIB_004:41
theorem Th52: :: GLIB_004:42
theorem :: GLIB_004:43