theorem
for
i,
n being
Nat for
f,
g being
Element of
REAL * for
G being
oriented finite Graph for
W being
Function of the
carrier' of
G,
Real>=0 for
v1,
v2 being
Vertex of
G st
f is_Input_of_Dijkstra_Alg G,
n,
W &
v1 = 1 & 1
<> v2 &
v2 = i &
n >= 1 &
g = (DijkstraAlgorithm n) . f holds
( the
carrier of
G = (UsedVx (g,n)) \/ (UnusedVx (g,n)) & (
v2 in UsedVx (
g,
n) implies ex
p being
FinSequence of
NAT ex
P being
oriented Chain of
G st
(
p is_simple_vertex_seq_at g,
i,
n &
P is_oriented_edge_seq_of p &
P is_shortestpath_of v1,
v2,
W &
cost (
P,
W)
= g . ((2 * n) + i) ) ) & (
v2 in UnusedVx (
g,
n) implies for
Q being
oriented Chain of
G holds not
Q is_orientedpath_of v1,
v2 ) )