let n be Element of NAT ; :: thesis:
let f, h be Element of REAL * ; :: thesis:
let G be oriented finite Graph; :: thesis:
let W be Function of the carrier' of G,Real>=0 ; :: thesis:
let v1 be Vertex of G; :: thesis:
set R = Relax n;
set M = findmin n;
set f0 = ((repeat ((Relax n) * (findmin n))) . 0 ) . f;
set mi = ((n * n) + (3 * n)) + 1;
assume that
A1: f is_Input_of_Dijkstra_Alg G,n,W and
A2: v1 = 1 and
A3: n >= 1 and
A4: h = ((repeat ((Relax n) * (findmin n))) . 1) . f ; :: thesis:
A5: len f = ((n * n) + (3 * n)) + 1 by A1, Def20;
set nk = n + 1;
A6: (2 * n) + n = (2 + 1) * n ;
A7: f . (n + 1) = 0 by A1, Def20;
A8: 1 <= ((n * n) + (3 * n)) + 1 by NAT_1:12;
then A9: 1 in dom f by A5, FINSEQ_3:27;
A10: ( ( for j being Element of NAT st 1 <= j & j <= n holds
f . j = 1 ) & ( for j being Element of NAT st 2 <= j & j <= n holds
f . (n + j) = - 1 ) ) by A1, Def20;
then A11: {1} = UsedVx h,n by A3, A4, A7, A9, Th48;
h = ((repeat ((Relax n) * (findmin n))) . (0 + 1)) . f by A4;
then h = (Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) by Th23;
then A12: h = Relax ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)),n by Def15;
A13: Seg n = the carrier of G by A1, Def20;
then reconsider VG = the carrier of G as non empty Subset of NAT by A3;
set Ak = Argmin (OuterVx f,n),f,n;
A14: dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) = dom (((repeat ((Relax n) * (findmin n))) . 0 ) . f) by Th34
.= dom f by Th22 ;
A15: 1 = Argmin (OuterVx f,n),f,n by A3, A7, A10, A9, Th48;
A16: (findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f) = (findmin n) . f by Th22
.= f,(((n * n) + (3 * n)) + 1) := 1,(- 1) by A15, Def11 ;
then ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . 1 = - 1 by A9, Th20;
then not (findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f) hasBetterPathAt n,1 by Def13;
then A17: not (findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f) hasBetterPathAt n,(n + 1) -' n by NAT_D:34;
A18: n + 1 < ((n * n) + (3 * n)) + 1 by A3, Lm12;
A19: W is_weight>=0of G by GRAPH_5:def 13;

hereby :: thesis:

set w1 = (2 * n) + 1;
let v3 be Vertex of G; :: thesis:
let j be Element of NAT ; :: thesis:
set nj = n + j;
assume that
A20: v3 <> v1 and
A21: v3 = j and
A22: h . (n + j) <> - 1 ; :: thesis:
set m2 = (2 * n) + j;
A23: j in VG by A21;
then A24: 1 <= j by A13, FINSEQ_1:3;
then n + 1 <= n + j by XREAL_1:9;
then A25: n < n + j by NAT_1:13;
A26: j <= n by A13, A23, FINSEQ_1:3;
then A27: ( 1 < (2 * n) + j & (2 * n) + j < ((n * n) + (3 * n)) + 1 ) by A24, Lm11;
j > 1 by A2, A20, A21, A24, XXREAL_0:1;
then j >= 1 + 1 by INT_1:20;
then A28: f . (n + j) = - 1 by A1, A26, Def20;
A29: n + j <= 2 * n by A24, A26, Lm12;
A30: ((n * n) + (3 * n)) + 1 in dom f by A8, A5, FINSEQ_3:27;
then A31: ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((n * n) + (3 * n)) + 1) = ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . (((n * n) + (3 * n)) + 1) by A14, PARTFUN1:def 8
.= 1 by A16, A27, A30, Th18 ;
A32: ( 1 < (2 * n) + 1 & (2 * n) + 1 < ((n * n) + (3 * n)) + 1 ) by A3, Lm11;
then (2 * n) + 1 in dom f by A5, FINSEQ_3:27;
then A33: ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. ((2 * n) + (((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((n * n) + (3 * n)) + 1))) = ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . ((2 * n) + 1) by A14, A31, PARTFUN1:def 8
.= f . ((2 * n) + 1) by A16, A32, Th19
.= 0 by A1, A3, Def20 ;
A34: (2 * n) + j <= 3 * n by A6, A26, XREAL_1:9;
A35: ( 1 < n + j & n + j < ((n * n) + (3 * n)) + 1 ) by A24, A26, Lm12;
then A36: n + j in dom f by A5, FINSEQ_3:27;
((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . (n + j) = f . (n + j) by A16, A35, Th19;
then A37: (findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f) hasBetterPathAt n,(n + j) -' n by A14, A12, A22, A29, A36, A25, A28, Def14;
(2 * n) + 1 <= (2 * n) + j by A24, XREAL_1:9;
then A38: 2 * n < (2 * n) + j by NAT_1:13;
set m3 = ((2 * n) + (n * 1)) + j;
reconsider p = <*1,j*> as FinSequence of NAT ;
A39: p . 1 = 1 by FINSEQ_1:61;
A40: ( 1 < ((2 * n) + (n * 1)) + j & ((2 * n) + (n * 1)) + j < ((n * n) + (3 * n)) + 1 ) by A3, A26, Lm13;
then ((2 * n) + (n * 1)) + j in dom f by A5, FINSEQ_3:27;
then A41: ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((2 * n) + (n * (((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((n * n) + (3 * n)) + 1)))) + j) = ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . (((2 * n) + (n * 1)) + j) by A14, A31, PARTFUN1:def 8
.= f . (((2 * n) + (n * 1)) + j) by A16, A40, Th19
.= Weight v1,v3,W by A1, A2, A21, Def20 ;
A42: (n + j) -' n = j by NAT_D:34;
then ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((2 * n) + (n * (((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 by A37, Def13;
then consider e being set such that
A43: e in the carrier' of G and
A44: e orientedly_joins v1,v3 by A41, Th24;
reconsider pe = <*e*> as oriented Chain of G by A43, Th5;
A45: len pe = 1 by FINSEQ_1:57;
A46: len p = 2 by FINSEQ_1:61;
then A47: p . (len p) = j by FINSEQ_1:61;

A48: now

let k be Nat; :: thesis:
assume ( 1 <= k & k <= len pe ) ; :: thesis:
then A49: k = 1 by A45, XXREAL_0:1;
hence the Source of G . (pe . k) = the Source of G . e by FINSEQ_1:57
.= p . k by A2, A44, A39, A49, GRAPH_4:def 1 ;
:: thesis:
thus the Target of G . (pe . k) = the Target of G . e by A49, FINSEQ_1:57
.= p . (k + 1) by A21, A44, A46, A47, A49, GRAPH_4:def 1 ; :: thesis:

end;

A50: h . (n + j) = 1 by A14, A12, A29, A36, A25, A37, A31, Def14;

now

let k be Element of NAT ; :: thesis:
assume that
A51: 1 <= k and
A52: k < len p ; :: thesis:
k < 1 + 1 by A52, FINSEQ_1:61;
then k <= 1 by NAT_1:13;
then k = 1 by A51, XXREAL_0:1;
hence p . ((len p) - k) = h . (n + (p /. (((len p) - k) + 1))) by A50, A39, A46, A47, FINSEQ_4:24; :: thesis:

end;

then A53: p is_vertex_seq_at h,j,n by A47, Def17;
( ((2 * n) + j) -' (2 * n) = j & (2 * n) + j in dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) ) by A5, A14, A27, FINSEQ_3:27, NAT_D:34;
then A54: (Relax ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)),n) . ((2 * n) + j) = newpathcost ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)),n,(((2 * n) + j) -' (2 * n)) by A42, A37, A34, A38, Def14
.= 0 + (((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((2 * n) + (n * (((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((n * n) + (3 * n)) + 1)))) + j)) by A33, NAT_D:34 ;
take p = p; :: thesis:
take pe = pe; :: thesis:
p is one-to-one by A2, A20, A21, FINSEQ_3:103;
hence p is_simple_vertex_seq_at h,j,n by A39, A46, A53, Def18; :: thesis:

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume that
A55: 1 <= i and
A56: i < len p ; :: thesis:
i + 1 <= 1 + 1 by A46, A56, INT_1:20;
then i <= 1 by XREAL_1:8;
then i = 1 by A55, XXREAL_0:1;
hence p . i in UsedVx h,n by A11, A39, TARSKI:def 1; :: thesis:

end;

len p = (len pe) + 1 by A45, FINSEQ_1:61;
hence pe is_oriented_edge_seq_of p by A48, Def19; :: thesis:
thus pe is_shortestpath_of v1,v3, UsedVx h,n,W by A2, A11, A43, A44, Th14; :: thesis:
thus cost pe,W = W . (pe . 1) by A19, A45, Th4, GRAPH_5:50
.= W . e by FINSEQ_1:57
.= h . ((2 * n) + j) by A12, A41, A54, A43, A44, Th26 ; :: thesis:
assume not v3 in UsedVx h,n ; :: thesis:
for v2 being Vertex of G st v2 in UsedVx h,n & v2 <> v1 holds
ex Q being oriented Chain of G st
( Q is_shortestpath_of v1,v2, UsedVx h,n,W & cost Q,W <= cost pe,W ) by A2, A11, TARSKI:def 1;
hence pe islongestInShortestpath UsedVx h,n,v1,W by GRAPH_5:def 19; :: thesis:

end;

A57: 2 * n < ((n * n) + (3 * n)) + 1 by Lm7;
A58: 2 * 1 <= 2 * n by A3, XREAL_1:66;
1 < n + 1 by A3, Lm12;
then A59: n + 1 in dom f by A5, A18, FINSEQ_3:27;
A60: n < n + 1 by NAT_1:13;
n + 1 <= 2 * n by A3, Lm12;
then A61: h . (n + 1) = ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . (n + 1) by A14, A12, A60, A59, A17, Def14
.= (((repeat ((Relax n) * (findmin n))) . 0 ) . f) . (n + 1) by A18, A60, Th32
.= 0 by A7, Th22 ;
A62: n * 1 <= n * n by A3, XREAL_1:66;

hereby :: thesis:

A63: n < ((n * n) + (3 * n)) + 1 by Lm7;
let m, j be Element of NAT ; :: thesis:
assume that
A64: h . (n + j) = - 1 and
A65: 1 <= j and
A66: j <= n and
A67: m in UsedVx h,n ; :: thesis:
reconsider v2 = j as Vertex of G by A13, A65, A66, FINSEQ_1:3;
A68: 3 * n < ((n * n) + (3 * n)) + 1 by Lm7;
set m2 = (2 * n) + j;
(2 * n) + j <= 3 * n by A6, A66, XREAL_1:9;
then A69: (2 * n) + j < ((n * n) + (3 * n)) + 1 by A68, XXREAL_0:2;
(2 * n) + 1 <= (2 * n) + j by A65, XREAL_1:9;
then 2 * n < (2 * n) + j by NAT_1:13;
then 2 < (2 * n) + j by A58, XXREAL_0:2;
then A70: 1 < (2 * n) + j by XXREAL_0:2;
j <> 1 by A61, A64;
then A71: ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . j = f . j by A16, A66, A63, Th19
.= 1 by A1, A65, A66, Def20 ;
A72: ((n * n) + (3 * n)) + 1 in dom f by A8, A5, FINSEQ_3:27;
then A73: ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((n * n) + (3 * n)) + 1) = ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . (((n * n) + (3 * n)) + 1) by A14, PARTFUN1:def 8
.= 1 by A16, A69, A70, A72, Th18 ;
set nj = n + j;
1 + 1 <= n + j by A3, A65, XREAL_1:9;
then A74: 1 < n + j by NAT_1:13;
A75: n + j <= n + n by A66, XREAL_1:9;
then n + j < ((n * n) + (3 * n)) + 1 by A57, XXREAL_0:2;
then A76: n + j in dom f by A5, A74, FINSEQ_3:27;
n + 1 <= n + j by A65, XREAL_1:9;
then A77: n < n + j by NAT_1:13;
A78: n + j <= 2 * n by A75;
then A79: not (findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f) hasBetterPathAt n,(n + j) -' n by A14, A12, A64, A76, A77, A73, Def14;
then ( (n + j) -' n = j & ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . (n + j) = - 1 ) by A14, A12, A64, A78, A76, A77, Def14, NAT_D:34;
then A80: not ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((2 * n) + (n * (((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 by A79, A71, Def13;
set m3 = ((2 * n) + (n * 1)) + j;
((2 * n) + (n * 1)) + j = (2 * n) + ((n * 1) + j) ;
then 2 <= ((2 * n) + (n * 1)) + j by A58, NAT_1:12;
then A81: 1 < ((2 * n) + (n * 1)) + j by XXREAL_0:2;
j <= n * n by A62, A66, XXREAL_0:2;
then ((2 * n) + (n * 1)) + j <= (3 * n) + (n * n) by XREAL_1:9;
then A82: ((2 * n) + (n * 1)) + j < ((n * n) + (3 * n)) + 1 by NAT_1:13;
then ((2 * n) + (n * 1)) + j in dom f by A5, A81, FINSEQ_3:27;
then A83: ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((2 * n) + (n * (((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) /. (((n * n) + (3 * n)) + 1)))) + j) = ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . (((2 * n) + (n * 1)) + j) by A14, A73, PARTFUN1:def 8;
((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0 ) . f)) . (((2 * n) + (n * 1)) + j) = f . (((2 * n) + (n * 1)) + j) by A16, A81, A82, Th19
.= Weight v1,v2,W by A1, A2, Def20 ;
then for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) by A80, A83, Th24;
then A84: Weight v1,v2,W = - 1 by Def7;
m = 1 by A11, A67, TARSKI:def 1;
hence f . (((2 * n) + (n * m)) + j) = - 1 by A1, A2, A84, Def20; :: thesis:

end;

let m be Element of NAT ; :: thesis:
assume m in UsedVx h,n ; :: thesis:
then m = 1 by A11, TARSKI:def 1;
hence h . (n + m) <> - 1 by A61; :: thesis: