let i, n be Nat; for V being set
for f, g being Element of REAL *
for G being oriented finite Graph
for P being oriented Chain of G
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 & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds
f . (((2 * n) + (n * m)) + j) = - 1 ) holds
g . (n + i) <> - 1
let V be set ; for f, g being Element of REAL *
for G being oriented finite Graph
for P being oriented Chain of G
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 & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds
f . (((2 * n) + (n * m)) + j) = - 1 ) holds
g . (n + i) <> - 1
let f, g be Element of REAL * ; for G being oriented finite Graph
for P being oriented Chain of G
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 & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds
f . (((2 * n) + (n * m)) + j) = - 1 ) holds
g . (n + i) <> - 1
let G be oriented finite Graph; for P being oriented Chain of G
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 & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds
f . (((2 * n) + (n * m)) + j) = - 1 ) holds
g . (n + i) <> - 1
let P be oriented Chain of G; 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 & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds
f . (((2 * n) + (n * m)) + j) = - 1 ) holds
g . (n + i) <> - 1
let W be 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 & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds
f . (((2 * n) + (n * m)) + j) = - 1 ) holds
g . (n + i) <> - 1
let v1, v2 be Vertex of G; ( f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds
f . (((2 * n) + (n * m)) + j) = - 1 ) implies g . (n + i) <> - 1 )
assume that
A1:
f is_Input_of_Dijkstra_Alg G,n,W
and
A2:
W is_weight>=0of G
and
A3:
v2 = i
and
A4:
v1 <> v2
and
A5:
( 1 <= i & i <= n )
and
A6:
P is_shortestpath_of v1,v2,V,W
and
A7:
for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds
f . (((2 * n) + (n * m)) + j) = - 1
; g . (n + i) <> - 1
P is_orientedpath_of v1,v2,V
by A6, GRAPH_5:def 18;
then consider q being oriented Simple Chain of G such that
A8:
q is_shortestpath_of v1,v2,V,W
by A2, GRAPH_5:62;
set FT = the Target of G;
assume A9:
g . (n + i) = - 1
; contradiction
set e = q . (len q);
consider vs being FinSequence of the carrier of G such that
A10:
vs is_oriented_vertex_seq_of q
and
A11:
for n1, m1 being Nat st 1 <= n1 & n1 < m1 & m1 <= len vs & vs . n1 = vs . m1 holds
( n1 = 1 & m1 = len vs )
by GRAPH_4:def 7;
A12:
q is_orientedpath_of v1,v2,V
by A8, GRAPH_5:def 18;
then A13:
q is_orientedpath_of v1,v2
by GRAPH_5:def 4;
then
q <> {}
by GRAPH_5:def 3;
then A14:
len q >= 1
by FINSEQ_1:20;
then A15:
q . (len q) orientedly_joins vs /. (len q),vs /. ((len q) + 1)
by A10, GRAPH_4:def 5;
len q in dom q
by A14, FINSEQ_3:25;
then A16:
q . (len q) in the carrier' of G
by FINSEQ_2:11;
A17:
len vs = (len q) + 1
by A10, GRAPH_4:def 5;
then A18:
len q < len vs
by NAT_1:13;
then A19:
len q in dom vs
by A14, FINSEQ_3:25;
A20:
vs /. (len q) = vs . (len q)
by A14, A18, FINSEQ_4:15;
then reconsider v3 = vs . (len q) as Vertex of G ;
the Target of G . (q . (len q)) = v2
by A13, GRAPH_5:def 3;
then A21:
v2 = vs /. ((len q) + 1)
by A15, GRAPH_4:def 1;
A22:
1 < (len q) + 1
by A14, NAT_1:13;
then A23:
v2 = vs . (len vs)
by A17, A21, FINSEQ_4:15;
now not v3 = v2A24:
q . 1
orientedly_joins vs /. 1,
vs /. (1 + 1)
by A10, A14, GRAPH_4:def 5;
assume A25:
v3 = v2
;
contradictionv1 =
the
Source of
G . (q . 1)
by A13, GRAPH_5:def 3
.=
vs /. 1
by A24, GRAPH_4:def 1
.=
vs . 1
by A17, A22, FINSEQ_4:15
.=
v3
by A11, A14, A18, A23, A25
;
hence
contradiction
by A4, A25;
verum end;
then A26:
not v3 in {v2}
by TARSKI:def 1;
Seg n = the carrier of G
by A1;
then
v3 in Seg n
by A19, FINSEQ_2:11;
then reconsider m = v3 as Element of NAT ;
A27:
f . (((2 * n) + (n * m)) + i) = Weight (v3,v2,W)
by A1, A3;
v3 = the Source of G . (q . (len q))
by A15, A20, GRAPH_4:def 1;
then
v3 in vertices q
by A14, Lm4;
then A28:
m in (vertices q) \ {v2}
by A26, XBOOLE_0:def 5;
(vertices q) \ {v2} c= V
by A12, GRAPH_5:def 4;
then
f . (((2 * n) + (n * m)) + i) = - 1
by A5, A7, A9, A28;
hence
contradiction
by A15, A16, A20, A21, A27, Th23; verum