let k, n be Nat; :: thesis:
let f, g, 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 IN = OuterVx (g,n);
set Ug = UsedVx (g,n);
assume that
A1: f is_Input_of_Dijkstra_Alg G,n,W and
A2: v1 = 1 and
A3: n >= 1 and
A4: g = ((repeat ((Relax n) * (findmin n))) . k) . f and
A5: h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f and
A6: OuterVx (g,n) <> {} and
A7: 1 in UsedVx (g,n) ; :: thesis:
assume A8: for v3 being Vertex of G
for j being Nat st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ; :: thesis:
assume that
A9: for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 and
A10: for m being Nat st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ; :: thesis:
set mi = ((n * n) + (3 * n)) + 1;
set Ak = Argmin ((OuterVx (g,n)),g,n);
A11: 1 <= ((n * n) + (3 * n)) + 1 by NAT_1:12;
A12: len f = ((n * n) + (3 * n)) + 1 by A1;
A13: (findmin n) . g = (g,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (g,n)),g,n)),(- jj)) by Def11;
A14: dom ((findmin n) . g) = dom g by Th33;
h = (Relax n) . ((findmin n) . g) by A4, A5, Th22;
then A15: h = Relax (((findmin n) . g),n) by Def15;
A16: Seg n = the carrier of G by A1;
then reconsider VG = the carrier of G as non empty Subset of NAT by A3;
A17: W is_weight>=0of G by GRAPH_5:def 13;
A18: (2 * n) + n = (2 + 1) * n ;
A19: dom f = dom g by A4, Th41;
A20: 1 <= Argmin ((OuterVx (g,n)),g,n) by A6, Th29;
A21: Argmin ((OuterVx (g,n)),g,n) <= n by A6, Th29;
A22: g . (n + (Argmin ((OuterVx (g,n)),g,n))) <> - 1 by A6, Th29;
set Uh = UsedVx (h,n);
A23: ( UsedVx (h,n) = (UsedVx (g,n)) \/ {(Argmin ((OuterVx (g,n)),g,n))} & not Argmin ((OuterVx (g,n)),g,n) in UsedVx (g,n) ) by A4, A5, A6, Th39;
then A24: UsedVx (g,n) c= UsedVx (h,n) by XBOOLE_1:7;
A25: n < ((n * n) + (3 * n)) + 1 by Lm7;
A26: dom f = dom h by A5, Th41;
reconsider vk = Argmin ((OuterVx (g,n)),g,n) as Vertex of G by A16, A20, A21, FINSEQ_1:1;
consider pk being FinSequence of NAT , PK being oriented Chain of G such that
A27: pk is_simple_vertex_seq_at g, Argmin ((OuterVx (g,n)),g,n),n and
A28: for i being Nat st 1 <= i & i < len pk holds
pk . i in UsedVx (g,n) and
A29: PK is_oriented_edge_seq_of pk and
A30: PK is_shortestpath_of v1,vk, UsedVx (g,n),W and
A31: cost (PK,W) = g . ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) and
A32: ( not vk in UsedVx (g,n) implies PK islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A22, A23;
A33: ex kk being Nat st
( kk = Argmin ((OuterVx (g,n)),g,n) & kk in OuterVx (g,n) & ( for i being Nat st i in OuterVx (g,n) holds
g /. ((2 * n) + kk) <= g /. ((2 * n) + i) ) & ( for i being Nat st i in OuterVx (g,n) & g /. ((2 * n) + kk) = g /. ((2 * n) + i) holds
kk <= i ) ) by A6, Def10;
set nAk = (2 * n) + (Argmin ((OuterVx (g,n)),g,n));
A34: 1 < (2 * n) + (Argmin ((OuterVx (g,n)),g,n)) by A20, A21, Lm11;
A35: (2 * n) + (Argmin ((OuterVx (g,n)),g,n)) < ((n * n) + (3 * n)) + 1 by A20, A21, Lm11;
A36: Argmin ((OuterVx (g,n)),g,n) < (2 * n) + (Argmin ((OuterVx (g,n)),g,n)) by A20, A21, Lm11;
A37: (2 * n) + (Argmin ((OuterVx (g,n)),g,n)) in dom g by A12, A19, A34, A35, FINSEQ_3:25;
A38: f,g equal_at (3 * n) + 1,(n * n) + (3 * n) by A4, Th46;
PK is_orientedpath_of v1,vk, UsedVx (g,n) by A30, GRAPH_5:def 18;
then A39: PK is_orientedpath_of v1,vk by GRAPH_5:def 4;
then PK <> {} by GRAPH_5:def 3;
then A40: len PK >= 1 by FINSEQ_1:20;
A41: ((n * n) + (3 * n)) + 1 in dom g by A11, A12, A19, FINSEQ_3:25;
then A42: ((findmin n) . g) /. (((n * n) + (3 * n)) + 1) = ((findmin n) . g) . (((n * n) + (3 * n)) + 1) by A14, PARTFUN1:def 6
.= Argmin ((OuterVx (g,n)),g,n) by A13, A21, A25, A41, Th17 ;
A43: ((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) = ((findmin n) . g) . ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) by A14, A37, PARTFUN1:def 6
.= cost (PK,W) by A13, A31, A35, A36, Th18 ;
set nk = n + (Argmin ((OuterVx (g,n)),g,n));
A44: 1 < n + (Argmin ((OuterVx (g,n)),g,n)) by A20, A21, Lm12;
A45: n + (Argmin ((OuterVx (g,n)),g,n)) <= 2 * n by A20, A21, Lm12;
A46: n + (Argmin ((OuterVx (g,n)),g,n)) < ((n * n) + (3 * n)) + 1 by A20, A21, Lm12;
n + 1 <= n + (Argmin ((OuterVx (g,n)),g,n)) by A20, XREAL_1:7;
then A47: n < n + (Argmin ((OuterVx (g,n)),g,n)) by NAT_1:13;
A48: n + (Argmin ((OuterVx (g,n)),g,n)) in dom g by A12, A19, A44, A46, FINSEQ_3:25;
A49: ((findmin n) . g) . (n + (Argmin ((OuterVx (g,n)),g,n))) = g . (n + (Argmin ((OuterVx (g,n)),g,n))) by A46, A47, Th31;

set Wke = ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin ((OuterVx (g,n)),g,n)));
assume A50: (findmin n) . g hasBetterPathAt n, Argmin ((OuterVx (g,n)),g,n) ; :: thesis:
then A51: ( ((findmin n) . g) . (n + (Argmin ((OuterVx (g,n)),g,n))) = - 1 or ((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) > newpathcost (((findmin n) . g),n,(Argmin ((OuterVx (g,n)),g,n))) ) ;
((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin ((OuterVx (g,n)),g,n))) >= 0 by A50;
then (((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n)))) + (((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin ((OuterVx (g,n)),g,n)))) >= (((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n)))) + 0 by XREAL_1:7;
hence contradiction by A6, A42, A49, A51, Th29; :: thesis:

end;

then not (findmin n) . g hasBetterPathAt n,(n + (Argmin ((OuterVx (g,n)),g,n))) -' n by NAT_D:34;
then A52: h . (n + (Argmin ((OuterVx (g,n)),g,n))) = g . (n + (Argmin ((OuterVx (g,n)),g,n))) by A14, A15, A45, A47, A48, A49, Def14;

hereby :: thesis:

let v3 be Vertex of G; :: thesis:
let j be Nat; :: thesis:
assume that
A53: v3 <> v1 and
A54: v3 = j and
A55: h . (n + j) <> - 1 ; :: thesis:
set nj = n + j;
A56: j in VG by A54;
then A57: 1 <= j by A16, FINSEQ_1:1;
A58: j <= n by A16, A56, FINSEQ_1:1;
then A59: 1 < n + j by A57, Lm12;
A60: n + j <= 2 * n by A57, A58, Lm12;
A61: n + j < ((n * n) + (3 * n)) + 1 by A57, A58, Lm12;
then A62: n + j in dom g by A12, A19, A59, FINSEQ_3:25;
A63: (n + j) -' n = j by NAT_D:34;
n + 1 <= n + j by A57, XREAL_1:7;
then A64: n < n + j by NAT_1:13;
set m2 = (2 * n) + j;
A65: (2 * n) + j <= 3 * n by A18, A58, XREAL_1:7;
(2 * n) + 1 <= (2 * n) + j by A57, XREAL_1:7;
then A66: 2 * n < (2 * n) + j by NAT_1:13;
A67: ((2 * n) + j) -' (2 * n) = j by NAT_D:34;
A68: 1 < (2 * n) + j by A57, A58, Lm11;
A69: (2 * n) + j < ((n * n) + (3 * n)) + 1 by A57, A58, Lm11;
then A70: (2 * n) + j in dom g by A12, A19, A68, FINSEQ_3:25;
A71: (2 * n) + j in dom ((findmin n) . g) by A12, A14, A19, A68, A69, FINSEQ_3:25;
A72: ((findmin n) . g) . (n + j) = g . (n + j) by A13, A21, A61, A64, Th18;
n <= 2 * n by Lm6;
then n < (2 * n) + j by A66, XXREAL_0:2;
then A73: ((findmin n) . g) . ((2 * n) + j) = g . ((2 * n) + j) by A13, A21, A69, Th18;
A74: j < ((n * n) + (3 * n)) + 1 by A25, A58, XXREAL_0:2;
then A75: j in dom g by A12, A19, A57, FINSEQ_3:25;
A76: j in dom h by A12, A26, A57, A74, FINSEQ_3:25;
set Akj = ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j;
A77: 1 < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A58, Lm13;
A78: Argmin ((OuterVx (g,n)),g,n) < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A58, Lm13;
A79: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j < ((n * n) + (3 * n)) + 1 by A20, A21, A58, Lm13;
then A80: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j in dom g by A12, A19, A77, FINSEQ_3:25;
A81: (3 * n) + 1 <= ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A57, A58, Lm14;
A82: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j <= (n * n) + (3 * n) by A20, A21, A57, A58, Lm14;
A83: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) = ((findmin n) . g) . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A14, A42, A80, PARTFUN1:def 6
.= g . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A13, A78, A79, Th18
.= f . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A38, A80, A81, A82
.= Weight (vk,v3,W) by A1, A54 ;
A84: ((findmin n) . g) /. ((2 * n) + j) = g . ((2 * n) + j) by A14, A70, A73, PARTFUN1:def 6;

per cases ) . g hasBetterPathAt n,(n + j) -' n or (findmin n) . g hasBetterPathAt n,(n + j) -' n ) ;

suppose A85: not (findmin n) . g hasBetterPathAt n,(n + j) -' n ; :: thesis:

then A86: h . (n + j) = g . (n + j) by A14, A15, A60, A62, A64, A72, Def14;
then consider p being FinSequence of NAT , P being oriented Chain of G such that
A87: p is_simple_vertex_seq_at g,j,n and
A88: for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) and
A89: P is_oriented_edge_seq_of p and
A90: P is_shortestpath_of v1,v3, UsedVx (g,n),W and
A91: cost (P,W) = g . ((2 * n) + j) and
A92: ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) by A8, A53, A54, A55;
take p = p; :: thesis:
take P = P; :: thesis:
thus p is_simple_vertex_seq_at h,j,n by A4, A5, A6, A12, A86, A87, A88, Lm17; :: thesis:
thus for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (h,n) by A24, A88; :: thesis:
thus P is_oriented_edge_seq_of p by A89; :: thesis:

hereby :: thesis:

per cases ) . g) . j = - 1 or ((findmin n) . g) . j <> - 1 ) ;

suppose ((findmin n) . g) . j = - 1 ; :: thesis:

then (Relax (((findmin n) . g),n)) . j = - 1 by A14, A58, A75, Def14;
then j in { i where i is Nat : ( i in dom h & 1 <= i & i <= n & h . i = - 1 ) } by A15, A57, A58, A76;
then A93: ( j in UsedVx (g,n) or j in {(Argmin ((OuterVx (g,n)),g,n))} ) by A23, XBOOLE_0:def 3;

now :: thesis:

let Q be oriented Chain of G; :: thesis:
let v4 be Vertex of G; :: thesis:
assume that
A94: not v4 in UsedVx (g,n) and
A95: Q is_shortestpath_of v1,v4, UsedVx (g,n),W ; :: thesis:
A96: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A97: 1 <= j4 by A16, A96, FINSEQ_1:1;
A98: j4 <= n by A16, A96, FINSEQ_1:1;
then A99: g . (n + j4) <> - 1 by A1, A2, A7, A9, A17, A94, A95, A97, Lm19;
then consider q being FinSequence of NAT , R being oriented Chain of G such that
q is_simple_vertex_seq_at g,j4,n and
for i being Nat st 1 <= i & i < len q holds
q . i in UsedVx (g,n) and
R is_oriented_edge_seq_of q and
A100: R is_shortestpath_of v1,v4, UsedVx (g,n),W and
A101: cost (R,W) = g . ((2 * n) + j4) and
A102: ( not v4 in UsedVx (g,n) implies R islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A94;
A103: cost (R,W) = cost (Q,W) by A95, A100, Th9;

per cases by A93, TARSKI:def 1;

suppose j in UsedVx (g,n) ; :: thesis:

then ex PP being oriented Chain of G st
( PP is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (PP,W) <= cost (R,W) ) by A53, A54, A94, A102, GRAPH_5:def 19;
hence cost (P,W) <= cost (Q,W) by A90, A103, Th9; :: thesis:

end;

suppose A104: j = Argmin ((OuterVx (g,n)),g,n) ; :: thesis:

j4 <= ((n * n) + (3 * n)) + 1 by A25, A98, XXREAL_0:2;
then A105: j4 in dom g by A12, A19, A97, FINSEQ_3:25;
then g . j4 <> - 1 by A94, A97, A98;
then j4 in { i where i is Nat : ( i in dom g & 1 <= i & i <= n & g . i <> - 1 & g . (n + i) <> - 1 ) } by A97, A98, A99, A105;
then A106: g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) <= g /. ((2 * n) + j4) by A33;
A107: g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) = g . ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) by A37, PARTFUN1:def 6;
A108: 1 < (2 * n) + j4 by A97, A98, Lm11;
(2 * n) + j4 < ((n * n) + (3 * n)) + 1 by A97, A98, Lm11;
then (2 * n) + j4 in dom g by A12, A19, A108, FINSEQ_3:25;
hence cost (P,W) <= cost (Q,W) by A91, A101, A103, A104, A106, A107, PARTFUN1:def 6; :: thesis:

end;

hence P is_shortestpath_of v1,v3, UsedVx (h,n),W by A17, A24, A53, A90, GRAPH_5:64; :: thesis:

end;

suppose A109: ((findmin n) . g) . j <> - 1 ; :: thesis:

hereby :: thesis:

per cases ) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 or ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) < 0 ) ;

suppose A110: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 ; :: thesis:

then A111: ((findmin n) . g) /. ((2 * n) + j) <= newpathcost (((findmin n) . g),n,j) by A63, A85, A109;
A112: ((findmin n) . g) /. ((2 * n) + j) = cost (P,W) by A71, A73, A91, PARTFUN1:def 6;
consider e being set such that
A113: e in the carrier' of G and
A114: e orientedly_joins vk,v3 by A83, A110, Th23;
reconsider pe = <*e*> as oriented Chain of G by A113, Th5;
A115: len pe = 1 by FINSEQ_1:40;
pe . 1 = e ;
then consider Q being oriented Chain of G such that
A117: Q = PK ^ pe and
Q is_orientedpath_of v1,v3 by A39, A40, A114, A115, GRAPH_5:33;
cost (pe,W) = W . (pe . 1) by A17, A115, Th4, GRAPH_5:46
.= Weight (vk,v3,W) by A113, A114, Th25 ;
then cost (Q,W) = newpathcost (((findmin n) . g),n,j) by A17, A42, A43, A83, A117, GRAPH_5:46, GRAPH_5:54;
hence P is_shortestpath_of v1,v3, UsedVx (h,n),W by A2, A7, A17, A23, A30, A32, A40, A53, A90, A111, A112, A113, A114, A117, GRAPH_5:65; :: thesis:

end;

suppose ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) < 0 ; :: thesis:

then for e being set holds
( not e in the carrier' of G or not e orientedly_joins vk,v3 ) by A83, Th23;
hence P is_shortestpath_of v1,v3, UsedVx (h,n),W by A2, A7, A17, A23, A30, A32, A53, A90, Th13; :: thesis:

end;

thus cost (P,W) = h . ((2 * n) + j) by A15, A63, A65, A66, A67, A71, A73, A85, A91, Def14; :: thesis:

hereby :: thesis:

assume A118: not v3 in UsedVx (h,n) ; :: thesis:
then A119: not v3 in UsedVx (g,n) by A23, XBOOLE_0:def 3;

now :: thesis:

let v2 be Vertex of G; :: thesis:
assume that
A120: v2 in UsedVx (h,n) and
A121: v2 <> v1 ; :: thesis:

per cases by A23, A120, XBOOLE_0:def 3;

suppose v2 in {(Argmin ((OuterVx (g,n)),g,n))} ; :: thesis:

then A122: v2 = vk by TARSKI:def 1;
take PK = PK; :: thesis:
thus PK is_shortestpath_of v1,v2, UsedVx (h,n),W by A23, A30, A122, Th8; :: thesis:
g . j <> - 1 by A54, A57, A58, A75, A119;
then j in { i where i is Nat : ( i in dom g & 1 <= i & i <= n & g . i <> - 1 & g . (n + i) <> - 1 ) } by A55, A57, A58, A75, A86;
then A123: g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) <= g /. ((2 * n) + j) by A33;
g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) = cost (PK,W) by A31, A37, PARTFUN1:def 6;
hence cost (PK,W) <= cost (P,W) by A70, A91, A123, PARTFUN1:def 6; :: thesis:

end;

suppose A124: v2 in UsedVx (g,n) ; :: thesis:

then consider Q being oriented Chain of G such that
A125: Q is_shortestpath_of v1,v2, UsedVx (g,n),W and
A126: cost (Q,W) <= cost (P,W) by A23, A92, A118, A121, GRAPH_5:def 19, XBOOLE_0:def 3;

A127: now :: thesis:

let R be oriented Chain of G; :: thesis:
let v4 be Vertex of G; :: thesis:
assume that
A128: not v4 in UsedVx (g,n) and
A129: R is_shortestpath_of v1,v4, UsedVx (g,n),W ; :: thesis:
A130: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A131: 1 <= j4 by A16, A130, FINSEQ_1:1;
j4 <= n by A16, A130, FINSEQ_1:1;
then g . (n + j4) <> - 1 by A1, A2, A7, A9, A17, A128, A129, A131, Lm19;
then consider rn being FinSequence of NAT , RR being oriented Chain of G such that
rn is_simple_vertex_seq_at g,j4,n and
for i being Nat st 1 <= i & i < len rn holds
rn . i in UsedVx (g,n) and
RR is_oriented_edge_seq_of rn and
A132: RR is_shortestpath_of v1,v4, UsedVx (g,n),W and
cost (RR,W) = g . ((2 * n) + j4) and
A133: ( not v4 in UsedVx (g,n) implies RR islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A128;
consider QQ being oriented Chain of G such that
A134: QQ is_shortestpath_of v1,v2, UsedVx (g,n),W and
A135: cost (QQ,W) <= cost (RR,W) by A121, A124, A128, A133, GRAPH_5:def 19;
cost (QQ,W) = cost (Q,W) by A125, A134, Th9;
hence cost (Q,W) <= cost (R,W) by A129, A132, A135, Th9; :: thesis:

end;

take Q = Q; :: thesis:
thus Q is_shortestpath_of v1,v2, UsedVx (h,n),W by A17, A24, A121, A125, A127, GRAPH_5:64; :: thesis:
thus cost (Q,W) <= cost (P,W) by A126; :: thesis:

end;

hence P islongestInShortestpath UsedVx (h,n),v1,W by GRAPH_5:def 19; :: thesis:

end;

suppose A136: (findmin n) . g hasBetterPathAt n,(n + j) -' n ; :: thesis:

then A137: (Relax (((findmin n) . g),n)) . (n + j) = Argmin ((OuterVx (g,n)),g,n) by A14, A42, A60, A62, A64, Def14;
A138: ( ((findmin n) . g) . (n + j) = - 1 or ((findmin n) . g) /. ((2 * n) + j) > newpathcost (((findmin n) . g),n,j) ) by A63, A136;
A139: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 by A63, A136;
A140: ((findmin n) . g) . j <> - 1 by A63, A136;
A141: newpathcost (((findmin n) . g),n,j) = (((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n)))) + (Weight (vk,v3,W)) by A42, A83;

A142: now :: thesis:

assume A143: Argmin ((OuterVx (g,n)),g,n) = j ; :: thesis:
then A144: ((findmin n) . g) . (n + j) <> - 1 by A13, A21, A22, A61, A64, Th18;
(((findmin n) . g) /. ((2 * n) + j)) + (Weight (vk,v3,W)) >= (((findmin n) . g) /. ((2 * n) + j)) + 0 by A83, A139, XREAL_1:7;
hence contradiction by A63, A136, A141, A143, A144; :: thesis:

end;

A145: now :: thesis:

assume j in UsedVx (g,n) ; :: thesis:
then ex i being Nat st
( j = i & i in dom g & 1 <= i & i <= n & g . i = - 1 ) ;
hence contradiction by A25, A140, Th32; :: thesis:

end;

consider e being set such that
A146: ( e in the carrier' of G & e orientedly_joins vk,v3 ) by A83, A139, Th23;
reconsider pe = <*e*> as oriented Chain of G by A146, Th5;
A147: len pe = 1 by FINSEQ_1:40;
A148: pe . 1 = e ;
then consider Q being oriented Chain of G such that
A149: Q = PK ^ pe and
Q is_orientedpath_of v1,v3 by A39, A40, A146, A147, GRAPH_5:33;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
reconsider q = pk ^ <*jj*> as FinSequence of NAT ;
take q = q; :: thesis:
take Q = Q; :: thesis:
thus q is_simple_vertex_seq_at h,j,n by A4, A5, A6, A12, A15, A27, A28, A52, A137, A142, A145, Lm18; :: thesis:
A150: len pk > 1 by A27;
A151: pk is_vertex_seq_at g, Argmin ((OuterVx (g,n)),g,n),n by A27;
A152: q . (len pk) = pk . (len pk) by A150, Lm1
.= Argmin ((OuterVx (g,n)),g,n) by A151 ;

hereby :: thesis:

let i be Nat; :: thesis:
assume that
A153: 1 <= i and
A154: i < len q ; :: thesis:
i < (len pk) + 1 by A154, FINSEQ_2:16;
then A155: i <= len pk by NAT_1:13;

now :: thesis:

per cases ;

suppose i = len pk ; :: thesis:

hence ( q . i in {(Argmin ((OuterVx (g,n)),g,n))} or q . i in UsedVx (g,n) ) by A152, TARSKI:def 1; :: thesis:

end;

suppose i <> len pk ; :: thesis:

then A156: i < len pk by A155, XXREAL_0:1;
q . i = pk . i by A153, A155, Lm1;
hence ( q . i in {(Argmin ((OuterVx (g,n)),g,n))} or q . i in UsedVx (g,n) ) by A28, A153, A156; :: thesis:

end;

hence q . i in UsedVx (h,n) by A23, XBOOLE_0:def 3; :: thesis:

end;

A157: len Q = (len PK) + 1 by A147, A149, FINSEQ_1:22;
A158: len pk = (len PK) + 1 by A29;
then A159: len q = (len Q) + 1 by A157, FINSEQ_2:16;
set FS = the Source of G;
set FT = the Target of G;

now :: thesis:

let i be Nat; :: thesis:
assume that
A160: 1 <= i and
A161: i <= len Q ; :: thesis:

per cases ;

suppose A162: i = len Q ; :: thesis:

then A163: Q . i = e by A147, A148, A149, A157, Lm2;
then A164: the Target of G . (Q . i) = v3 by A146, GRAPH_4:def 1;
thus the Source of G . (Q . i) = q . i by A146, A152, A157, A158, A162, A163, GRAPH_4:def 1; :: thesis:
thus the Target of G . (Q . i) = q . (i + 1) by A54, A157, A158, A162, A164, FINSEQ_1:42; :: thesis:

end;

suppose i <> len Q ; :: thesis:

then A165: i < len Q by A161, XXREAL_0:1;
then A166: i <= len PK by A157, NAT_1:13;
then A167: the Source of G . (PK . i) = pk . i by A29, A160;
A168: the Target of G . (PK . i) = pk . (i + 1) by A29, A160, A166;
A169: Q . i = PK . i by A149, A160, A166, Lm1;
A170: i + 1 <= len pk by A157, A158, A165, NAT_1:13;
thus the Source of G . (Q . i) = q . i by A157, A158, A160, A161, A167, A169, Lm1; :: thesis:
thus the Target of G . (Q . i) = q . (i + 1) by A168, A169, A170, Lm1, NAT_1:12; :: thesis:

end;

hence Q is_oriented_edge_seq_of q by A159; :: thesis:
A171: (cost (PK,W)) + (cost (pe,W)) = cost (Q,W) by A17, A149, GRAPH_5:46, GRAPH_5:54;
A172: cost (pe,W) = W . (pe . 1) by A17, A147, Th4, GRAPH_5:46
.= Weight (vk,v3,W) by A146, Th25 ;
then A173: newpathcost (((findmin n) . g),n,j) = cost (Q,W) by A17, A42, A43, A83, A149, GRAPH_5:46, GRAPH_5:54;

hereby :: thesis:

per cases ;

suppose A174: g . (n + j) = - 1 ; :: thesis:

now :: thesis:

let v2 be Vertex of G; :: thesis:
assume A175: v2 in UsedVx (g,n) ; :: thesis:
then reconsider m = v2 as Element of NAT ;
- 1 = f . (((2 * n) + (n * m)) + j) by A9, A57, A58, A174, A175
.= Weight (v2,v3,W) by A1, A54 ;
hence for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) by Th23; :: thesis:

end;

hence Q is_shortestpath_of v1,v3, UsedVx (h,n),W by A2, A7, A23, A30, A53, A146, A149, Th15; :: thesis:

end;

suppose A176: g . (n + j) <> - 1 ; :: thesis:

then ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) by A8, A53, A54;
hence Q is_shortestpath_of v1,v3, UsedVx (h,n),W by A2, A7, A13, A17, A21, A23, A30, A32, A40, A42, A43, A53, A61, A64, A83, A84, A138, A146, A149, A171, A172, A176, Th18, GRAPH_5:65; :: thesis:

end;

thus cost (Q,W) = h . ((2 * n) + j) by A15, A63, A65, A66, A67, A71, A136, A173, Def14; :: thesis:
0 <= cost (pe,W) by A17, GRAPH_5:50;
then A177: (cost (PK,W)) + 0 <= cost (Q,W) by A171, XREAL_1:7;

hereby :: thesis:

assume not v3 in UsedVx (h,n) ; :: thesis:

now :: thesis:

let v2 be Vertex of G; :: thesis:
assume that
A178: v2 in UsedVx (h,n) and
A179: v2 <> v1 ; :: thesis:

per cases by A23, A178, XBOOLE_0:def 3;

suppose v2 in {(Argmin ((OuterVx (g,n)),g,n))} ; :: thesis:

then A180: v2 = Argmin ((OuterVx (g,n)),g,n) by TARSKI:def 1;
take PK = PK; :: thesis:
thus PK is_shortestpath_of v1,v2, UsedVx (h,n),W by A23, A30, A180, Th8; :: thesis:
thus cost (PK,W) <= cost (Q,W) by A177; :: thesis:

end;

suppose A181: v2 in UsedVx (g,n) ; :: thesis:

then consider P being oriented Chain of G such that
A182: P is_shortestpath_of v1,v2, UsedVx (g,n),W and
A183: cost (P,W) <= cost (PK,W) by A4, A5, A6, A32, A179, Th39, GRAPH_5:def 19;

A184: now :: thesis:

let R be oriented Chain of G; :: thesis:
let v4 be Vertex of G; :: thesis:
assume that
A185: not v4 in UsedVx (g,n) and
A186: R is_shortestpath_of v1,v4, UsedVx (g,n),W ; :: thesis:
A187: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A188: 1 <= j4 by A16, A187, FINSEQ_1:1;
j4 <= n by A16, A187, FINSEQ_1:1;
then g . (n + j4) <> - 1 by A1, A2, A7, A9, A17, A185, A186, A188, Lm19;
then consider rn being FinSequence of NAT , RR being oriented Chain of G such that
rn is_simple_vertex_seq_at g,j4,n and
for i being Nat st 1 <= i & i < len rn holds
rn . i in UsedVx (g,n) and
RR is_oriented_edge_seq_of rn and
A189: RR is_shortestpath_of v1,v4, UsedVx (g,n),W and
cost (RR,W) = g . ((2 * n) + j4) and
A190: ( not v4 in UsedVx (g,n) implies RR islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A185;
consider PP being oriented Chain of G such that
A191: PP is_shortestpath_of v1,v2, UsedVx (g,n),W and
A192: cost (PP,W) <= cost (RR,W) by A179, A181, A185, A190, GRAPH_5:def 19;
cost (PP,W) = cost (P,W) by A182, A191, Th9;
hence cost (P,W) <= cost (R,W) by A186, A189, A192, Th9; :: thesis:

end;

take P = P; :: thesis:
thus P is_shortestpath_of v1,v2, UsedVx (h,n),W by A17, A24, A179, A182, A184, GRAPH_5:64; :: thesis:
thus cost (P,W) <= cost (Q,W) by A177, A183, XXREAL_0:2; :: thesis:

end;

hence Q islongestInShortestpath UsedVx (h,n),v1,W by GRAPH_5:def 19; :: thesis:

end;

hereby :: thesis:

let m, j be Nat; :: thesis:
assume that
A193: h . (n + j) = - 1 and
A194: 1 <= j and
A195: j <= n and
A196: m in UsedVx (h,n) ; :: thesis:
set nj = n + j;
A197: 1 < n + j by A194, A195, Lm12;
A198: n + j <= 2 * n by A194, A195, Lm12;
A199: n + j < ((n * n) + (3 * n)) + 1 by A194, A195, Lm12;
then A200: n + j in dom g by A12, A19, A197, FINSEQ_3:25;
n + 1 <= n + j by A194, XREAL_1:7;
then A201: n < n + j by NAT_1:13;
A202: not (findmin n) . g hasBetterPathAt n,(n + j) -' n by A193, A14, A15, A42, A198, A200, A201, Def14;
A203: ((findmin n) . g) . (n + j) = g . (n + j) by A13, A21, A199, A201, Th18;
then A204: g . (n + j) = - 1 by A14, A15, A193, A198, A200, A201, A202, Def14;
then A205: not j in UsedVx (g,n) by A10;
j < ((n * n) + (3 * n)) + 1 by A25, A195, XXREAL_0:2;
then j in dom g by A12, A19, A194, FINSEQ_3:25;
then g . j <> - 1 by A194, A195, A205;
then A206: ((findmin n) . g) . j <> - 1 by A13, A22, A25, A195, A204, Th18;
not (findmin n) . g hasBetterPathAt n,j by A202, NAT_D:34;
then A207: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) < 0 by A203, A204, A206;
reconsider v3 = j as Vertex of G by A16, A194, A195, FINSEQ_1:1;
set Akj = ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j;
A208: 1 < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A195, Lm13;
A209: Argmin ((OuterVx (g,n)),g,n) < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A195, Lm13;
A210: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j < ((n * n) + (3 * n)) + 1 by A20, A21, A195, Lm13;
then A211: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j in dom g by A12, A19, A208, FINSEQ_3:25;
A212: (3 * n) + 1 <= ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A194, A195, Lm14;
A213: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j <= (n * n) + (3 * n) by A20, A21, A194, A195, Lm14;
A214: f . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) = Weight (vk,v3,W) by A1;
A215: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) = ((findmin n) . g) . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A14, A42, A211, PARTFUN1:def 6
.= g . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A13, A209, A210, Th18
.= Weight (vk,v3,W) by A38, A211, A212, A213, A214 ;

per cases by A23, A196, XBOOLE_0:def 3;

suppose m in {(Argmin ((OuterVx (g,n)),g,n))} ; :: thesis:

then A216: m = Argmin ((OuterVx (g,n)),g,n) by TARSKI:def 1;
for e being set holds
( not e in the carrier' of G or not e orientedly_joins vk,v3 ) by A207, A215, Th23;
then Weight (vk,v3,W) = - 1 by Def7;
hence f . (((2 * n) + (n * m)) + j) = - 1 by A1, A216; :: thesis:

end;

suppose m in UsedVx (g,n) ; :: thesis:

hence f . (((2 * n) + (n * m)) + j) = - 1 by A9, A194, A195, A204; :: thesis:

end;

let m be Nat; :: thesis:
assume A217: m in UsedVx (h,n) ; :: thesis:

per cases by A23, A217, XBOOLE_0:def 3;

suppose A218: m in UsedVx (g,n) ; :: thesis:

then h . (n + m) = g . (n + m) by A4, A5, A6, A12, Lm16;
hence h . (n + m) <> - 1 by A10, A218; :: thesis:

end;

suppose m in {(Argmin ((OuterVx (g,n)),g,n))} ; :: thesis:

hence h . (n + m) <> - 1 by A22, A52, TARSKI:def 1; :: thesis:

end;