let n be 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;
set nk = n + 1;
A6: (2 * n) + n = (2 + 1) * n ;
A7: f . (n + 1) = 0 by A1;
A8: 1 <= ((n * n) + (3 * n)) + 1 by NAT_1:12;
then A9: 1 in dom f by A5, FINSEQ_3:25;
A10: ( ( for j being Nat st 1 <= j & j <= n holds
f . j = 1 ) & ( for j being Nat st 2 <= j & j <= n holds
f . (n + j) = - 1 ) ) by A1;
then A11: {1} = UsedVx (h,n) by A3, A4, A7, A9, Th47;
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 Th22;
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;
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 Th33
.= dom f by Th21 ;
A15: 1 = Argmin ((OuterVx (f,n)),f,n) by A3, A7, A10, A9, Th47;
A16: (findmin n) . (((repeat ((Relax n) * (findmin n))) . 0) . f) = (findmin n) . f by Th21
.= (f,(((n * n) + (3 * n)) + 1)) := (1,(- jj)) by A15, Def11 ;
then ((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0) . f)) . 1 = - jj by A9, Th19;
then not (findmin n) . (((repeat ((Relax n) * (findmin n))) . 0) . f) hasBetterPathAt n,1 ;
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 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:1;
then n + 1 <= n + j by XREAL_1:7;
then A25: n < n + j by NAT_1:13;
A26: j <= n by A13, A23, FINSEQ_1:1;
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:7;
then A28: f . (n + j) = - 1 by A1, A26;
A29: n + j <= 2 * n by A24, A26, Lm12;
A30: ((n * n) + (3 * n)) + 1 in dom f by A8, A5, FINSEQ_3:25;
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 6
.= jj by A16, A27, A30, Th17 ;
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:25;
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 6
.= f . ((2 * n) + 1) by A16, A32, Th18
.= 0 by A1, A3 ;
A34: (2 * n) + j <= 3 * n by A6, A26, XREAL_1:7;
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:25;
((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0) . f)) . (n + j) = f . (n + j) by A16, A35, Th18;
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:7;
then A38: 2 * n < (2 * n) + j by NAT_1:13;
set m3 = ((2 * n) + (n * 1)) + j;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
reconsider p = <*1,jj*> as FinSequence of NAT ;
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:25;
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 6
.= f . (((2 * n) + (n * 1)) + j) by A16, A40, Th18
.= Weight (v1,v3,W) by A1, A2, A21 ;
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;
then consider e being set such that
A43: e in the carrier' of G and
A44: e orientedly_joins v1,v3 by A41, Th23;
reconsider pe = <*e*> as oriented Chain of G by A43, Th5;
A45: len pe = 1 by FINSEQ_1:40;
A46: len p = 2 by FINSEQ_1:44;
then A47: p . (len p) = j ;

A48: now :: thesis:

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
.= p . k by A2, A44, A49, GRAPH_4:def 1 ;
:: thesis:
thus the Target of G . (pe . k) = the Target of G . e by A49
.= p . (k + 1) by A21, A44, A49, GRAPH_4:def 1 ; :: thesis:

end;

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

now :: thesis:

let k be Nat; :: thesis:
assume that
A51: 1 <= k and
A52: k < len p ; :: thesis:
k < 1 + 1 by A52, FINSEQ_1:44;
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, A46, A47, FINSEQ_4:15; :: thesis:

end;

then A53: p is_vertex_seq_at h,j,n by A47;
( ((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:25, 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:94;
hence p is_simple_vertex_seq_at h,j,n by A46, A53; :: thesis:

hereby :: thesis:

let i be Nat; :: thesis:
assume that
A55: 1 <= i and
A56: i < len p ; :: thesis:
i + 1 <= 1 + 1 by A46, A56, INT_1:7;
then i <= 1 by XREAL_1:6;
then i = 1 by A55, XXREAL_0:1;
hence p . i in UsedVx (h,n) by A11, TARSKI:def 1; :: thesis:

end;

len p = (len pe) + 1 by A45, FINSEQ_1:44;
hence pe is_oriented_edge_seq_of p by A48; :: 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:46
.= W . e
.= h . ((2 * n) + j) by A12, A41, A54, A43, A44, Th25 ; :: 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:64;
1 < n + 1 by A3, Lm12;
then A59: n + 1 in dom f by A5, A18, FINSEQ_3:25;
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, Th31
.= 0 by A7, Th21 ;
A62: n * 1 <= n * n by A3, XREAL_1:64;

hereby :: thesis:

A63: n < ((n * n) + (3 * n)) + 1 by Lm7;
let m, j be 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:1;
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:7;
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:7;
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, Th18
.= 1 by A1, A65, A66 ;
A72: ((n * n) + (3 * n)) + 1 in dom f by A8, A5, FINSEQ_3:25;
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 6
.= 1 by A16, A69, A70, A72, Th17 ;
set nj = n + j;
1 + 1 <= n + j by A3, A65, XREAL_1:7;
then A74: 1 < n + j by NAT_1:13;
A75: n + j <= n + n by A66, XREAL_1:7;
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:25;
n + 1 <= n + j by A65, XREAL_1:7;
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;
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:7;
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:25;
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 6;
((findmin n) . (((repeat ((Relax n) * (findmin n))) . 0) . f)) . (((2 * n) + (n * 1)) + j) = f . (((2 * n) + (n * 1)) + j) by A16, A81, A82, Th18
.= Weight (v1,v2,W) by A1, A2 ;
then for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) by A80, A83, Th23;
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; :: thesis:

end;

let m be 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: