:: GLIB_004 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem Th1: :: GLIB_004:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th2: :: GLIB_004:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th3: :: GLIB_004:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th4: :: GLIB_004:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th5: :: GLIB_004:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
:: 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 :
definition
let G be
real-WEV WEVGraph;
func DIJK:NextBestEdges G -> Subset of
(the_Edges_of G) means :
Def4:
:: GLIB_004:def 4
for
e1 being
set holds
(
e1 in it iff (
e1 DSJoins G .labeledV() ,
(the_Vertices_of G) \ (G .labeledV() ),
G & ( for
e2 being
set st
e2 DSJoins G .labeledV() ,
(the_Vertices_of G) \ (G .labeledV() ),
G holds
((the_VLabel_of G) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((the_VLabel_of G) . ((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 G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G & ( for e2 being set st e2 DSJoins G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G holds
((the_VLabel_of G) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((the_VLabel_of G) . ((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 G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G & ( for e2 being set st e2 DSJoins G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G holds
((the_VLabel_of G) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((the_VLabel_of G) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) & ( for e1 being set holds
( e1 in b2 iff ( e1 DSJoins G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G & ( for e2 being set st e2 DSJoins G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G holds
((the_VLabel_of G) . ((the_Source_of G) . e1)) + ((the_Weight_of G) . e1) <= ((the_VLabel_of G) . ((the_Source_of G) . e2)) + ((the_Weight_of G) . e2) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines DIJK:NextBestEdges GLIB_004:def 4 :
:: deftheorem Def5 defines DIJK:Step GLIB_004:def 5 :
:: deftheorem defines DIJK:Init GLIB_004:def 6 :
:: deftheorem Def7 defines DIJK:CompSeq GLIB_004:def 7 :
:: deftheorem defines DIJK:SSSP GLIB_004:def 8 :
theorem Th10: :: GLIB_004:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th11: :: GLIB_004:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th12: :: GLIB_004:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th13: :: GLIB_004:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th14: :: GLIB_004:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th15: :: GLIB_004:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th16: :: GLIB_004:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th17: :: GLIB_004:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th18: :: GLIB_004:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th19: :: GLIB_004:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th20: :: GLIB_004:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th21: :: GLIB_004:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th22: :: GLIB_004:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th23: :: GLIB_004:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th24: :: GLIB_004:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th25: :: GLIB_004:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
:: deftheorem defines WGraphSelectors GLIB_004:def 9 :
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 10 :
:: deftheorem defines .cost() GLIB_004:def 11 :
theorem :: GLIB_004:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th33: :: GLIB_004:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th34: :: GLIB_004:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
definition
let G be
real-weighted WVGraph;
func PRIM:NextBestEdges G -> Subset of
(the_Edges_of G) means :
Def12:
:: GLIB_004:def 12
for
e1 being
set holds
(
e1 in it iff (
e1 SJoins G .labeledV() ,
(the_Vertices_of G) \ (G .labeledV() ),
G & ( for
e2 being
set st
e2 SJoins G .labeledV() ,
(the_Vertices_of G) \ (G .labeledV() ),
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 G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G & ( for e2 being set st e2 SJoins G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),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 G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G & ( for e2 being set st e2 SJoins G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) & ( for e1 being set holds
( e1 in b2 iff ( e1 SJoins G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G & ( for e2 being set st e2 SJoins G .labeledV() ,(the_Vertices_of G) \ (G .labeledV() ),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def12 defines PRIM:NextBestEdges GLIB_004:def 12 :
:: deftheorem defines PRIM:Init GLIB_004:def 13 :
definition
let G be
real-WEV WEVGraph;
set e =
choose (PRIM:NextBestEdges G);
func PRIM:Step G -> real-WEV WEVGraph equals :
Def14:
:: GLIB_004:def 14
G if PRIM:NextBestEdges G = {} (G .labelEdge (choose (PRIM:NextBestEdges G)),1) .labelVertex ((the_Target_of G) . (choose (PRIM:NextBestEdges G))),1
if (
PRIM:NextBestEdges G <> {} &
(the_Source_of G) . (choose (PRIM:NextBestEdges G)) in G .labeledV() )
otherwise (G .labelEdge (choose (PRIM:NextBestEdges G)),1) .labelVertex ((the_Source_of G) . (choose (PRIM:NextBestEdges G))),1;
coherence
( ( PRIM:NextBestEdges G = {} implies G is real-WEV WEVGraph ) & ( PRIM:NextBestEdges G <> {} & (the_Source_of G) . (choose (PRIM:NextBestEdges G)) in G .labeledV() implies (G .labelEdge (choose (PRIM:NextBestEdges G)),1) .labelVertex ((the_Target_of G) . (choose (PRIM:NextBestEdges G))),1 is real-WEV WEVGraph ) & ( not PRIM:NextBestEdges G = {} & ( not PRIM:NextBestEdges G <> {} or not (the_Source_of G) . (choose (PRIM:NextBestEdges G)) in G .labeledV() ) implies (G .labelEdge (choose (PRIM:NextBestEdges G)),1) .labelVertex ((the_Source_of G) . (choose (PRIM:NextBestEdges G))),1 is real-WEV WEVGraph ) )
;
consistency
for b1 being real-WEV WEVGraph st PRIM:NextBestEdges G = {} & PRIM:NextBestEdges G <> {} & (the_Source_of G) . (choose (PRIM:NextBestEdges G)) in G .labeledV() holds
( b1 = G iff b1 = (G .labelEdge (choose (PRIM:NextBestEdges G)),1) .labelVertex ((the_Target_of G) . (choose (PRIM:NextBestEdges G))),1 )
;
end;
:: deftheorem Def14 defines PRIM:Step GLIB_004:def 14 :
:: deftheorem Def15 defines PRIM:CompSeq GLIB_004:def 15 :
:: deftheorem defines PRIM:MST GLIB_004:def 16 :
Lm4:
for G being real-weighted WGraph holds
( G == PRIM:Init G & the_Weight_of G = the_Weight_of (PRIM:Init G) & the_ELabel_of (PRIM:Init G) = {} & the_VLabel_of (PRIM:Init G) = (choose (the_Vertices_of G)) .--> 1 )
Lm5:
for G being real-weighted WGraph holds
( (PRIM:Init G) .labeledV() = {(choose (the_Vertices_of G))} & (PRIM:Init G) .labeledE() = {} )
Lm6:
for G being real-WEV WEVGraph st PRIM:NextBestEdges G <> {} holds
ex v being Vertex of G st
( not v in G .labeledV() & PRIM:Step G = (G .labelEdge (choose (PRIM:NextBestEdges G)),1) .labelVertex v,1 )
Lm7:
for G being real-WEV WEVGraph holds
( G == PRIM:Step G & the_Weight_of G = the_Weight_of (PRIM:Step G) & G .labeledE() c= (PRIM:Step G) .labeledE() & G .labeledV() c= (PRIM:Step G) .labeledV() )
Lm8:
for G being finite real-weighted WGraph
for n being Nat holds
( G == (PRIM:CompSeq G) .-> n & the_Weight_of ((PRIM:CompSeq G) .-> n) = the_Weight_of G )
Lm9:
for G being finite real-weighted WGraph
for n being Nat holds
( ((PRIM:CompSeq G) .-> n) .labeledV() is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) .-> n) .labeledE() c= G .edgesBetween (((PRIM:CompSeq G) .-> n) .labeledV() ) )
Lm10:
for G1 being finite real-weighted WGraph
for n being Nat
for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) .-> n) .labeledV() ,((PRIM:CompSeq G1) .-> n) .labeledE() holds G2 is connected
Lm11:
for G1 being finite real-weighted WGraph
for n being Nat
for G2 being inducedSubgraph of G1,(((PRIM:CompSeq G1) .-> n) .labeledV() ) holds G2 is connected
Lm12:
for G being finite real-weighted WGraph
for n being Nat holds ((PRIM:CompSeq G) .-> n) .labeledV() c= G .reachableFrom (choose (the_Vertices_of G))
Lm13:
for G being finite real-weighted WGraph
for i, j being Nat st i <= j holds
( ((PRIM:CompSeq G) .-> i) .labeledV() c= ((PRIM:CompSeq G) .-> j) .labeledV() & ((PRIM:CompSeq G) .-> i) .labeledE() c= ((PRIM:CompSeq G) .-> j) .labeledE() )
Lm14:
for G being finite real-weighted WGraph
for n being Nat holds
( PRIM:NextBestEdges ((PRIM:CompSeq G) .-> n) = {} iff ((PRIM:CompSeq G) .-> n) .labeledV() = G .reachableFrom (choose (the_Vertices_of G)) )
Lm15:
for G being finite real-weighted WGraph
for n being Nat holds card (((PRIM:CompSeq G) .-> n) .labeledV() ) = min (n + 1),(card (G .reachableFrom (choose (the_Vertices_of G))))
Lm16:
for G being finite real-weighted WGraph holds
( PRIM:CompSeq G is halting & ((PRIM:CompSeq G) .Lifespan() ) + 1 = card (G .reachableFrom (choose (the_Vertices_of G))) )
Lm17:
for G1 being finite real-weighted WGraph
for n being Nat
for G2 being inducedSubgraph of G1,((PRIM:CompSeq G1) .-> n) .labeledV() ,((PRIM:CompSeq G1) .-> n) .labeledE() holds G2 is Tree-like
Lm18:
for G being finite connected real-weighted WGraph holds (PRIM:MST G) .labeledV() = the_Vertices_of G
:: deftheorem Def17 defines min-cost GLIB_004:def 17 :
theorem :: GLIB_004:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th36: :: GLIB_004:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:48
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:49
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:50
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:51
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem Th52: :: GLIB_004:52
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)
theorem :: GLIB_004:53
:: Showing IDV graph ... (Click the Palm Tree again to close it) ![Show TPTP problem Show TPTP problem](../TPTP.gif)