let n, k be Element of NAT ; :: thesis: for f, g, h being Element of REAL *
for G being oriented finite Graph
for W being Function of the carrier' of G,Real>=0
for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & 1 in UsedVx g,n & ( for v3 being Vertex of G
for j being Element of 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 Element of 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 ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx g,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx g,n holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1 ) )
let f, g, h be Element of REAL * ; :: thesis: for G being oriented finite Graph
for W being Function of the carrier' of G,Real>=0
for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & 1 in UsedVx g,n & ( for v3 being Vertex of G
for j being Element of 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 Element of 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 ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx g,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx g,n holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1 ) )
let G be oriented finite Graph; :: thesis: for W being Function of the carrier' of G,Real>=0
for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & 1 in UsedVx g,n & ( for v3 being Vertex of G
for j being Element of 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 Element of 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 ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx g,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx g,n holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1 ) )
let W be Function of the carrier' of G,Real>=0 ; :: thesis: for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & 1 in UsedVx g,n & ( for v3 being Vertex of G
for j being Element of 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 Element of 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 ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx g,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx g,n holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1 ) )
let v1 be Vertex of G; :: thesis: ( f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & 1 in UsedVx g,n & ( for v3 being Vertex of G
for j being Element of 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 Element of 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 ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx g,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx g,n holds
g . (n + m) <> - 1 ) implies ( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1 ) ) )
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: ( ex v3 being Vertex of G ex j being Element of NAT st
( v3 <> v1 & v3 = j & g . (n + j) <> - 1 & ( for p being FinSequence of NAT
for P being oriented Chain of G holds
( not p is_simple_vertex_seq_at g,j,n or ex i being Element of NAT st
( 1 <= i & i < len p & not p . i in UsedVx g,n ) or not P is_oriented_edge_seq_of p or not P is_shortestpath_of v1,v3, UsedVx g,n,W or not cost P,W = g . ((2 * n) + j) or ( not v3 in UsedVx g,n & not P islongestInShortestpath UsedVx g,n,v1,W ) ) ) ) or ex m, j being Element of NAT st
( g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx g,n & not f . (((2 * n) + (n * m)) + j) = - 1 ) or ex m being Element of NAT st
( m in UsedVx g,n & not g . (n + m) <> - 1 ) or ( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1 ) ) )
assume A8: for v3 being Vertex of G
for j being Element of 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 Element of 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: ( ex m, j being Element of NAT st
( g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx g,n & not f . (((2 * n) + (n * m)) + j) = - 1 ) or ex m being Element of NAT st
( m in UsedVx g,n & not g . (n + m) <> - 1 ) or ( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1 ) ) )
assume that
A9: for m, j being Element of 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 Element of NAT st m in UsedVx g,n holds
g . (n + m) <> - 1 ; :: thesis: ( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1 ) )
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, Def20;
A13: (findmin n) . g = g,(((n * n) + (3 * n)) + 1) := (Argmin (OuterVx g,n),g,n),(- 1) by Def11;
A14: dom ((findmin n) . g) = dom g by Th34;
A15: h = (Relax n) . ((findmin n) . g) by A4, A5, Th23;
A16: h = Relax ((findmin n) . g),n by A15, Def15;
A17: Seg n = the carrier of G by A1, Def20;
reconsider VG = the carrier of G as non empty Subset of NAT by A3, A17;
A18: W is_weight>=0of G by GRAPH_5:def 13;
A19: (2 * n) + n = (2 + 1) * n ;
A20: dom f = dom g by A4, Th42;
A21: 1 <= Argmin (OuterVx g,n),g,n by A6, Th30;
A22: Argmin (OuterVx g,n),g,n <= n by A6, Th30;
A23: g . (n + (Argmin (OuterVx g,n),g,n)) <> - 1 by A6, Th30;
set Uh = UsedVx h,n;
A24: ( 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, Th40;
A26: UsedVx g,n c= UsedVx h,n by A24, XBOOLE_1:7;
A27: n < ((n * n) + (3 * n)) + 1 by Lm7;
A28: dom f = dom h by A5, Th42;
reconsider vk = Argmin (OuterVx g,n),g,n as Vertex of G by A17, A21, A22, FINSEQ_1:3;
consider pk being FinSequence of NAT , PK being oriented Chain of G such that
A29: pk is_simple_vertex_seq_at g, Argmin (OuterVx g,n),g,n,n and
A30: for i being Element of NAT st 1 <= i & i < len pk holds
pk . i in UsedVx g,n and
A31: PK is_oriented_edge_seq_of pk and
A32: PK is_shortestpath_of v1,vk, UsedVx g,n,W and
A33: cost PK,W = g . ((2 * n) + (Argmin (OuterVx g,n),g,n)) and
A34: ( not vk in UsedVx g,n implies PK islongestInShortestpath UsedVx g,n,v1,W ) by A2, A7, A8, A23, A24;
A35: ex kk being Element of NAT st
( kk = Argmin (OuterVx g,n),g,n & kk in OuterVx g,n & ( for i being Element of NAT st i in OuterVx g,n holds
g /. ((2 * n) + kk) <= g /. ((2 * n) + i) ) & ( for i being Element of 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);
A36: 1 < (2 * n) + (Argmin (OuterVx g,n),g,n) by A21, A22, Lm11;
A37: (2 * n) + (Argmin (OuterVx g,n),g,n) < ((n * n) + (3 * n)) + 1 by A21, A22, Lm11;
A38: Argmin (OuterVx g,n),g,n < (2 * n) + (Argmin (OuterVx g,n),g,n) by A21, A22, Lm11;
A39: (2 * n) + (Argmin (OuterVx g,n),g,n) in dom g by A12, A20, A36, A37, FINSEQ_3:27;
A40: f,g equal_at (3 * n) + 1,(n * n) + (3 * n) by A4, Th47;
A41: PK is_orientedpath_of v1,vk, UsedVx g,n by A32, GRAPH_5:def 18;
A42: PK is_orientedpath_of v1,vk by A41, GRAPH_5:def 4;
A43: PK <> {} by A42, GRAPH_5:def 3;
A44: len PK >= 1 by A43, FINSEQ_1:28;
A45: ((n * n) + (3 * n)) + 1 in dom g by A11, A12, A20, FINSEQ_3:27;
A46: ((findmin n) . g) /. (((n * n) + (3 * n)) + 1) = ((findmin n) . g) . (((n * n) + (3 * n)) + 1) by A14, A45, PARTFUN1:def 8
.= Argmin (OuterVx g,n),g,n by A13, A22, A27, A45, Th18 ;
A47: ((findmin n) . g) /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) = ((findmin n) . g) . ((2 * n) + (Argmin (OuterVx g,n),g,n)) by A14, A39, PARTFUN1:def 8
.= cost PK,W by A13, A33, A37, A38, Th19 ;
set nk = n + (Argmin (OuterVx g,n),g,n);
A48: 1 < n + (Argmin (OuterVx g,n),g,n) by A21, A22, Lm12;
A49: n + (Argmin (OuterVx g,n),g,n) <= 2 * n by A21, A22, Lm12;
A50: n + (Argmin (OuterVx g,n),g,n) < ((n * n) + (3 * n)) + 1 by A21, A22, Lm12;
A51: n + 1 <= n + (Argmin (OuterVx g,n),g,n) by A21, XREAL_1:9;
A52: n < n + (Argmin (OuterVx g,n),g,n) by A51, NAT_1:13;
A53: n + (Argmin (OuterVx g,n),g,n) in dom g by A12, A20, A48, A50, FINSEQ_3:27;
A54: ((findmin n) . g) . (n + (Argmin (OuterVx g,n),g,n)) = g . (n + (Argmin (OuterVx g,n),g,n)) by A50, A52, Th32;
A55: now
set Wke = ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin (OuterVx g,n),g,n));
assume A56: (findmin n) . g hasBetterPathAt n, Argmin (OuterVx g,n),g,n ; :: thesis: contradiction
A57: ( ((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) ) by A56, Def13;
A58: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin (OuterVx g,n),g,n)) >= 0 by A56, Def13;
A59: (((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 A58, XREAL_1:9;
thus contradiction by A6, A46, A54, A57, A59, Th30; :: thesis: verum
end;
A60: not (findmin n) . g hasBetterPathAt n,(n + (Argmin (OuterVx g,n),g,n)) -' n by A55, NAT_D:34;
A61: h . (n + (Argmin (OuterVx g,n),g,n)) = g . (n + (Argmin (OuterVx g,n),g,n)) by A14, A16, A49, A52, A53, A54, A60, Def14;
hereby :: thesis: ( ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1 ) )
let v3 be Vertex of G; :: thesis: for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( b4 is_simple_vertex_seq_at h,P,n & ( for i being Element of NAT st 1 <= b6 & b6 < len i holds
i . b6 in UsedVx h,n ) & b5 is_oriented_edge_seq_of b4 & b5 is_shortestpath_of v1,p, UsedVx h,n,W & cost b5,W = h . ((2 * n) + P) & ( not p in UsedVx h,n implies b5 islongestInShortestpath UsedVx h,n,v1,W ) )
let j be Element of NAT ; :: thesis: ( v3 <> v1 & v3 = j & h . (n + j) <> - 1 implies ex p being FinSequence of NAT ex P being oriented Chain of G st
( b3 is_simple_vertex_seq_at h,P,n & ( for i being Element of NAT st 1 <= b5 & b5 < len i holds
i . b5 in UsedVx h,n ) & b4 is_oriented_edge_seq_of b3 & b4 is_shortestpath_of v1,p, UsedVx h,n,W & cost b4,W = h . ((2 * n) + P) & ( not p in UsedVx h,n implies b4 islongestInShortestpath UsedVx h,n,v1,W ) ) )
assume that
A62: v3 <> v1 and
A63: v3 = j and
A64: h . (n + j) <> - 1 ; :: thesis: ex p being FinSequence of NAT ex P being oriented Chain of G st
( b3 is_simple_vertex_seq_at h,P,n & ( for i being Element of NAT st 1 <= b5 & b5 < len i holds
i . b5 in UsedVx h,n ) & b4 is_oriented_edge_seq_of b3 & b4 is_shortestpath_of v1,p, UsedVx h,n,W & cost b4,W = h . ((2 * n) + P) & ( not p in UsedVx h,n implies b4 islongestInShortestpath UsedVx h,n,v1,W ) )
set nj = n + j;
A65: j in VG by A63;
A66: 1 <= j by A17, A65, FINSEQ_1:3;
A67: j <= n by A17, A65, FINSEQ_1:3;
A68: 1 < n + j by A66, A67, Lm12;
A69: n + j <= 2 * n by A66, A67, Lm12;
A70: n + j < ((n * n) + (3 * n)) + 1 by A66, A67, Lm12;
A71: n + j in dom g by A12, A20, A68, A70, FINSEQ_3:27;
A72: (n + j) -' n = j by NAT_D:34;
A73: n + 1 <= n + j by A66, XREAL_1:9;
A74: n < n + j by A73, NAT_1:13;
set m2 = (2 * n) + j;
A75: (2 * n) + j <= 3 * n by A19, A67, XREAL_1:9;
A76: (2 * n) + 1 <= (2 * n) + j by A66, XREAL_1:9;
A77: 2 * n < (2 * n) + j by A76, NAT_1:13;
A78: ((2 * n) + j) -' (2 * n) = j by NAT_D:34;
A79: 1 < (2 * n) + j by A66, A67, Lm11;
A80: (2 * n) + j < ((n * n) + (3 * n)) + 1 by A66, A67, Lm11;
A81: (2 * n) + j in dom g by A12, A20, A79, A80, FINSEQ_3:27;
A82: (2 * n) + j in dom ((findmin n) . g) by A12, A14, A20, A79, A80, FINSEQ_3:27;
A83: ((findmin n) . g) . (n + j) = g . (n + j) by A13, A22, A70, A74, Th19;
A84: n <= 2 * n by Lm6;
A85: n < (2 * n) + j by A77, A84, XXREAL_0:2;
A86: ((findmin n) . g) . ((2 * n) + j) = g . ((2 * n) + j) by A13, A22, A80, A85, Th19;
A87: j < ((n * n) + (3 * n)) + 1 by A27, A67, XXREAL_0:2;
A88: j in dom g by A12, A20, A66, A87, FINSEQ_3:27;
A89: j in dom h by A12, A28, A66, A87, FINSEQ_3:27;
set Akj = ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j;
A90: 1 < ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j by A21, A22, A67, Lm13;
A91: Argmin (OuterVx g,n),g,n < ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j by A21, A22, A67, Lm13;
A92: ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j < ((n * n) + (3 * n)) + 1 by A21, A22, A67, Lm13;
A93: ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j in dom g by A12, A20, A90, A92, FINSEQ_3:27;
A94: (3 * n) + 1 <= ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j by A21, A22, A66, A67, Lm14;
A95: ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j <= (n * n) + (3 * n) by A21, A22, A66, A67, Lm14;
A96: ((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, A46, A93, PARTFUN1:def 8
.= g . (((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j) by A13, A91, A92, Th19
.= f . (((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j) by A20, A40, A93, A94, A95, Def16
.= Weight vk,v3,W by A1, A63, Def20 ;
A97: ((findmin n) . g) /. ((2 * n) + j) = g . ((2 * n) + j) by A14, A81, A86, PARTFUN1:def 8;
per cases ( not (findmin n) . g hasBetterPathAt n,(n + j) -' n or (findmin n) . g hasBetterPathAt n,(n + j) -' n ) ;
suppose A98: not (findmin n) . g hasBetterPathAt n,(n + j) -' n ; :: thesis: ex p being FinSequence of NAT ex P being oriented Chain of G st
( b3 is_simple_vertex_seq_at h,P,n & ( for i being Element of NAT st 1 <= b5 & b5 < len i holds
i . b5 in UsedVx h,n ) & b4 is_oriented_edge_seq_of b3 & b4 is_shortestpath_of v1,p, UsedVx h,n,W & cost b4,W = h . ((2 * n) + P) & ( not p in UsedVx h,n implies b4 islongestInShortestpath UsedVx h,n,v1,W ) )
A99: h . (n + j) = g . (n + j) by A14, A16, A69, A71, A74, A83, A98, Def14;
consider p being FinSequence of NAT , P being oriented Chain of G such that
A100: p is_simple_vertex_seq_at g,j,n and
A101: for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx g,n and
A102: P is_oriented_edge_seq_of p and
A103: P is_shortestpath_of v1,v3, UsedVx g,n,W and
A104: cost P,W = g . ((2 * n) + j) and
A105: ( not v3 in UsedVx g,n implies P islongestInShortestpath UsedVx g,n,v1,W ) by A8, A62, A63, A64, A99;
take p = p; :: thesis: ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) )
take P = P; :: thesis: ( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) )
thus p is_simple_vertex_seq_at h,j,n by A4, A5, A6, A12, A99, A100, A101, Lm17; :: thesis: ( ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) )
hereby :: thesis: ( P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) )
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len p implies p . i in UsedVx h,n )
assume that
A106: 1 <= i and
A107: i < len p ; :: thesis: p . i in UsedVx h,n
A108: p . i in UsedVx g,n by A101, A106, A107;
thus p . i in UsedVx h,n by A26, A108; :: thesis: verum
end;
thus P is_oriented_edge_seq_of p by A102; :: thesis: ( P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) )
hereby :: thesis: ( cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) )
per cases ( ((findmin n) . g) . j = - 1 or ((findmin n) . g) . j <> - 1 ) ;
suppose A109: ((findmin n) . g) . j = - 1 ; :: thesis: P is_shortestpath_of v1,v3, UsedVx h,n,W
A110: (Relax ((findmin n) . g),n) . j = - 1 by A14, A67, A88, A109, Def14;
A111: j in { i where i is Element of NAT : ( i in dom h & 1 <= i & i <= n & h . i = - 1 ) } by A16, A66, A67, A89, A110;
A112: ( j in UsedVx g,n or j in {(Argmin (OuterVx g,n),g,n)} ) by A24, A111, XBOOLE_0:def 3;
A113: now
let Q be oriented Chain of G; :: thesis: for v4 being Vertex of G st not v4 in UsedVx g,n & Q is_shortestpath_of v1,v4, UsedVx g,n,W holds
cost P,W <= cost b2,W
let v4 be Vertex of G; :: thesis: ( not v4 in UsedVx g,n & Q is_shortestpath_of v1,v4, UsedVx g,n,W implies cost P,W <= cost b1,W )
assume that
A114: not v4 in UsedVx g,n and
A115: Q is_shortestpath_of v1,v4, UsedVx g,n,W ; :: thesis: cost P,W <= cost b1,W
A116: v4 in VG ;
reconsider j4 = v4 as Element of NAT by A116;
A117: 1 <= j4 by A17, A116, FINSEQ_1:3;
A118: j4 <= n by A17, A116, FINSEQ_1:3;
A119: g . (n + j4) <> - 1 by A1, A2, A7, A9, A18, A114, A115, A117, A118, Lm19;
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 Element of NAT st 1 <= i & i < len q holds
q . i in UsedVx g,n and
R is_oriented_edge_seq_of q and
A120: R is_shortestpath_of v1,v4, UsedVx g,n,W and
A121: cost R,W = g . ((2 * n) + j4) and
A122: ( not v4 in UsedVx g,n implies R islongestInShortestpath UsedVx g,n,v1,W ) by A2, A7, A8, A114, A119;
A123: cost R,W = cost Q,W by A115, A120, Th9;
per cases ( j in UsedVx g,n or j = Argmin (OuterVx g,n),g,n ) by A112, TARSKI:def 1;
suppose A126: j = Argmin (OuterVx g,n),g,n ; :: thesis: cost P,W <= cost b1,W
A127: j4 <= ((n * n) + (3 * n)) + 1 by A27, A118, XXREAL_0:2;
A128: j4 in dom g by A12, A20, A117, A127, FINSEQ_3:27;
A129: g . j4 <> - 1 by A114, A117, A118, A128;
A130: j4 in { i where i is Element of NAT : ( i in dom g & 1 <= i & i <= n & g . i <> - 1 & g . (n + i) <> - 1 ) } by A117, A118, A119, A128, A129;
A131: g /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) <= g /. ((2 * n) + j4) by A35, A130;
A132: g /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) = g . ((2 * n) + (Argmin (OuterVx g,n),g,n)) by A39, PARTFUN1:def 8;
A133: 1 < (2 * n) + j4 by A117, A118, Lm11;
A134: (2 * n) + j4 < ((n * n) + (3 * n)) + 1 by A117, A118, Lm11;
A135: (2 * n) + j4 in dom g by A12, A20, A133, A134, FINSEQ_3:27;
thus cost P,W <= cost Q,W by A104, A121, A123, A126, A131, A132, A135, PARTFUN1:def 8; :: thesis: verum
end;
end;
end;
thus P is_shortestpath_of v1,v3, UsedVx h,n,W by A18, A26, A62, A103, A113, GRAPH_5:68; :: thesis: verum
end;
suppose A136: ((findmin n) . g) . j <> - 1 ; :: thesis: P is_shortestpath_of v1,v3, UsedVx h,n,W
hereby :: thesis: verum
per cases ( ((findmin n) . 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 A137: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 ; :: thesis: P is_shortestpath_of v1,v3, UsedVx h,n,W
A138: ((findmin n) . g) /. ((2 * n) + j) <= newpathcost ((findmin n) . g),n,j by A72, A98, A136, A137, Def13;
A139: ((findmin n) . g) /. ((2 * n) + j) = cost P,W by A82, A86, A104, PARTFUN1:def 8;
consider e being set such that
A140: e in the carrier' of G and
A141: e orientedly_joins vk,v3 by A96, A137, Th24;
reconsider pe = <*e*> as oriented Chain of G by A140, Th5;
A142: len pe = 1 by FINSEQ_1:57;
A143: pe . 1 = e by FINSEQ_1:57;
consider Q being oriented Chain of G such that
A144: Q = PK ^ pe and
Q is_orientedpath_of v1,v3 by A42, A44, A141, A142, A143, GRAPH_5:37;
A145: cost pe,W = W . (pe . 1) by A18, A142, Th4, GRAPH_5:50
.= Weight vk,v3,W by A140, A141, A143, Th26 ;
A146: cost Q,W = newpathcost ((findmin n) . g),n,j by A18, A46, A47, A96, A144, A145, GRAPH_5:50, GRAPH_5:58;
thus P is_shortestpath_of v1,v3, UsedVx h,n,W by A2, A7, A18, A24, A24, A32, A34, A44, A62, A103, A138, A139, A140, A141, A144, A146, GRAPH_5:69; :: thesis: verum
end;
suppose A147: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) < 0 ; :: thesis: P is_shortestpath_of v1,v3, UsedVx h,n,W
A148: for e being set holds
( not e in the carrier' of G or not e orientedly_joins vk,v3 ) by A96, A147, Th24;
thus P is_shortestpath_of v1,v3, UsedVx h,n,W by A2, A7, A18, A24, A32, A34, A62, A103, A148, Th13; :: thesis: verum
end;
end;
end;
end;
end;
end;
thus cost P,W = h . ((2 * n) + j) by A16, A72, A75, A77, A78, A82, A86, A98, A104, Def14; :: thesis: ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W )
hereby :: thesis: verum
assume A149: not v3 in UsedVx h,n ; :: thesis: P islongestInShortestpath UsedVx h,n,v1,W
A150: not v3 in UsedVx g,n by A24, A149, XBOOLE_0:def 3;
A151: now
let v2 be Vertex of G; :: thesis: ( v2 in UsedVx h,n & v2 <> v1 implies ex PK being oriented Chain of G st
( b2 is_shortestpath_of v1,PK, UsedVx h,n,W & cost b2,W <= cost P,W ) )
assume that
A152: v2 in UsedVx h,n and
A153: v2 <> v1 ; :: thesis: ex PK being oriented Chain of G st
( b2 is_shortestpath_of v1,PK, UsedVx h,n,W & cost b2,W <= cost P,W )
per cases ( v2 in {(Argmin (OuterVx g,n),g,n)} or v2 in UsedVx g,n ) by A24, A152, XBOOLE_0:def 3;
suppose A154: v2 in {(Argmin (OuterVx g,n),g,n)} ; :: thesis: ex PK being oriented Chain of G st
( b2 is_shortestpath_of v1,PK, UsedVx h,n,W & cost b2,W <= cost P,W )
A155: v2 = vk by A154, TARSKI:def 1;
take PK = PK; :: thesis: ( PK is_shortestpath_of v1,v2, UsedVx h,n,W & cost PK,W <= cost P,W )
thus PK is_shortestpath_of v1,v2, UsedVx h,n,W by A24, A32, A155, Th8; :: thesis: cost PK,W <= cost P,W
A156: g . j <> - 1 by A63, A66, A67, A88, A150;
A157: j in { i where i is Element of NAT : ( i in dom g & 1 <= i & i <= n & g . i <> - 1 & g . (n + i) <> - 1 ) } by A64, A66, A67, A88, A99, A156;
A158: g /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) <= g /. ((2 * n) + j) by A35, A157;
A159: g /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) = cost PK,W by A33, A39, PARTFUN1:def 8;
thus cost PK,W <= cost P,W by A81, A104, A158, A159, PARTFUN1:def 8; :: thesis: verum
end;
suppose A160: v2 in UsedVx g,n ; :: thesis: ex Q being oriented Chain of G st
( b2 is_shortestpath_of v1,Q, UsedVx h,n,W & cost b2,W <= cost P,W )
consider Q being oriented Chain of G such that
A161: Q is_shortestpath_of v1,v2, UsedVx g,n,W and
A162: cost Q,W <= cost P,W by A24, A105, A149, A153, A160, GRAPH_5:def 19, XBOOLE_0:def 3;
A163: now
let R be oriented Chain of G; :: thesis: for v4 being Vertex of G st not v4 in UsedVx g,n & R is_shortestpath_of v1,v4, UsedVx g,n,W holds
cost Q,W <= cost R,W
let v4 be Vertex of G; :: thesis: ( not v4 in UsedVx g,n & R is_shortestpath_of v1,v4, UsedVx g,n,W implies cost Q,W <= cost R,W )
assume that
A164: not v4 in UsedVx g,n and
A165: R is_shortestpath_of v1,v4, UsedVx g,n,W ; :: thesis: cost Q,W <= cost R,W
A166: v4 in VG ;
reconsider j4 = v4 as Element of NAT by A166;
A167: 1 <= j4 by A17, A166, FINSEQ_1:3;
A168: j4 <= n by A17, A166, FINSEQ_1:3;
A169: g . (n + j4) <> - 1 by A1, A2, A7, A9, A18, A164, A165, A167, A168, Lm19;
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 Element of NAT st 1 <= i & i < len rn holds
rn . i in UsedVx g,n and
RR is_oriented_edge_seq_of rn and
A170: RR is_shortestpath_of v1,v4, UsedVx g,n,W and
cost RR,W = g . ((2 * n) + j4) and
A171: ( not v4 in UsedVx g,n implies RR islongestInShortestpath UsedVx g,n,v1,W ) by A2, A7, A8, A164, A169;
consider QQ being oriented Chain of G such that
A172: QQ is_shortestpath_of v1,v2, UsedVx g,n,W and
A173: cost QQ,W <= cost RR,W by A153, A160, A164, A171, GRAPH_5:def 19;
A174: cost QQ,W = cost Q,W by A161, A172, Th9;
thus cost Q,W <= cost R,W by A165, A170, A173, A174, Th9; :: thesis: verum
end;
take Q = Q; :: thesis: ( Q is_shortestpath_of v1,v2, UsedVx h,n,W & cost Q,W <= cost P,W )
thus Q is_shortestpath_of v1,v2, UsedVx h,n,W by A18, A26, A153, A161, A163, GRAPH_5:68; :: thesis: cost Q,W <= cost P,W
thus cost Q,W <= cost P,W by A162; :: thesis: verum
end;
end;
end;
thus P islongestInShortestpath UsedVx h,n,v1,W by A151, GRAPH_5:def 19; :: thesis: verum
end;
end;
suppose A175: (findmin n) . g hasBetterPathAt n,(n + j) -' n ; :: thesis: ex q being FinSequence of NAT ex Q being oriented Chain of G st
( b3 is_simple_vertex_seq_at h,Q,n & ( for i being Element of NAT st 1 <= b5 & b5 < len i holds
i . b5 in UsedVx h,n ) & b4 is_oriented_edge_seq_of b3 & b4 is_shortestpath_of v1,q, UsedVx h,n,W & cost b4,W = h . ((2 * n) + Q) & ( not q in UsedVx h,n implies b4 islongestInShortestpath UsedVx h,n,v1,W ) )
A176: (Relax ((findmin n) . g),n) . (n + j) = Argmin (OuterVx g,n),g,n by A14, A46, A69, A71, A74, A175, Def14;
A177: ( ((findmin n) . g) . (n + j) = - 1 or ((findmin n) . g) /. ((2 * n) + j) > newpathcost ((findmin n) . g),n,j ) by A72, A175, Def13;
A178: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 by A72, A175, Def13;
A179: ((findmin n) . g) . j <> - 1 by A72, A175, Def13;
A180: newpathcost ((findmin n) . g),n,j = (((findmin n) . g) /. ((2 * n) + (Argmin (OuterVx g,n),g,n))) + (Weight vk,v3,W) by A46, A96;
A181: now
assume A182: Argmin (OuterVx g,n),g,n = j ; :: thesis: contradiction
A183: ((findmin n) . g) . (n + j) <> - 1 by A13, A22, A23, A70, A74, A182, Th19;
A184: (((findmin n) . g) /. ((2 * n) + j)) + (Weight vk,v3,W) >= (((findmin n) . g) /. ((2 * n) + j)) + 0 by A96, A178, XREAL_1:9;
thus contradiction by A72, A175, A180, A182, A183, A184, Def13; :: thesis: verum
end;
A185: now
assume A186: j in UsedVx g,n ; :: thesis: contradiction
A187: ex i being Element of NAT st
( j = i & i in dom g & 1 <= i & i <= n & g . i = - 1 ) by A186;
thus contradiction by A27, A179, A187, Th33; :: thesis: verum
end;
consider e being set such that
A188: ( e in the carrier' of G & e orientedly_joins vk,v3 ) by A96, A178, Th24;
reconsider pe = <*e*> as oriented Chain of G by A188, Th5;
A190: len pe = 1 by FINSEQ_1:57;
A191: pe . 1 = e by FINSEQ_1:57;
consider Q being oriented Chain of G such that
A192: Q = PK ^ pe and
Q is_orientedpath_of v1,v3 by A42, A44, A188, A190, A191, GRAPH_5:37;
take q = pk ^ <*j*>; :: thesis: ex Q being oriented Chain of G st
( q is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len q holds
q . i in UsedVx h,n ) & Q is_oriented_edge_seq_of q & Q is_shortestpath_of v1,v3, UsedVx h,n,W & cost Q,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies Q islongestInShortestpath UsedVx h,n,v1,W ) )
take Q = Q; :: thesis: ( q is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len q holds
q . i in UsedVx h,n ) & Q is_oriented_edge_seq_of q & Q is_shortestpath_of v1,v3, UsedVx h,n,W & cost Q,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies Q islongestInShortestpath UsedVx h,n,v1,W ) )
thus q is_simple_vertex_seq_at h,j,n by A4, A5, A6, A12, A16, A29, A30, A61, A176, A181, A185, Lm18; :: thesis: ( ( for i being Element of NAT st 1 <= i & i < len q holds
q . i in UsedVx h,n ) & Q is_oriented_edge_seq_of q & Q is_shortestpath_of v1,v3, UsedVx h,n,W & cost Q,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies Q islongestInShortestpath UsedVx h,n,v1,W ) )
A193: len pk > 1 by A29, Def18;
A194: pk is_vertex_seq_at g, Argmin (OuterVx g,n),g,n,n by A29, Def18;
A195: q . (len pk) = pk . (len pk) by A193, Lm1
.= Argmin (OuterVx g,n),g,n by A194, Def17 ;
hereby :: thesis: ( Q is_oriented_edge_seq_of q & Q is_shortestpath_of v1,v3, UsedVx h,n,W & cost Q,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies Q islongestInShortestpath UsedVx h,n,v1,W ) )
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len q implies q . i in UsedVx h,n )
assume that
A196: 1 <= i and
A197: i < len q ; :: thesis: q . i in UsedVx h,n
A198: i < (len pk) + 1 by A197, FINSEQ_2:19;
A199: i <= len pk by A198, NAT_1:13;
A200: now
per cases ( i = len pk or i <> len pk ) ;
suppose A201: i = len pk ; :: thesis: ( q . i in {(Argmin (OuterVx g,n),g,n)} or q . i in UsedVx g,n )
thus ( q . i in {(Argmin (OuterVx g,n),g,n)} or q . i in UsedVx g,n ) by A195, A201, TARSKI:def 1; :: thesis: verum
end;
suppose A202: i <> len pk ; :: thesis: ( q . i in {(Argmin (OuterVx g,n),g,n)} or q . i in UsedVx g,n )
A203: i < len pk by A199, A202, XXREAL_0:1;
A204: q . i = pk . i by A196, A199, Lm1;
thus ( q . i in {(Argmin (OuterVx g,n),g,n)} or q . i in UsedVx g,n ) by A30, A196, A203, A204; :: thesis: verum
end;
end;
end;
thus q . i in UsedVx h,n by A24, A200, XBOOLE_0:def 3; :: thesis: verum
end;
A205: len Q = (len PK) + 1 by A190, A192, FINSEQ_1:35;
A206: len pk = (len PK) + 1 by A31, Def19;
A207: len q = (len Q) + 1 by A205, A206, FINSEQ_2:19;
set FS = the Source of G;
set FT = the Target of G;
A208: now
let i be Nat; :: thesis: ( 1 <= i & i <= len Q implies ( the Source of G . (Q . b1) = q . b1 & the Target of G . (Q . b1) = q . (b1 + 1) ) )
assume that
A209: 1 <= i and
A210: i <= len Q ; :: thesis: ( the Source of G . (Q . b1) = q . b1 & the Target of G . (Q . b1) = q . (b1 + 1) )
per cases ( i = len Q or i <> len Q ) ;
suppose A211: i = len Q ; :: thesis: ( the Source of G . (Q . b1) = q . b1 & the Target of G . (Q . b1) = q . (b1 + 1) )
A212: Q . i = e by A190, A191, A192, A205, A211, Lm2;
A213: the Target of G . (Q . i) = v3 by A188, A212, GRAPH_4:def 1;
thus the Source of G . (Q . i) = q . i by A188, A195, A205, A206, A211, A212, GRAPH_4:def 1; :: thesis: the Target of G . (Q . i) = q . (i + 1)
thus the Target of G . (Q . i) = q . (i + 1) by A63, A205, A206, A211, A213, FINSEQ_1:59; :: thesis: verum
end;
suppose A214: i <> len Q ; :: thesis: ( the Source of G . (Q . b1) = q . b1 & the Target of G . (Q . b1) = q . (b1 + 1) )
A215: i < len Q by A210, A214, XXREAL_0:1;
A216: i <= len PK by A205, A215, NAT_1:13;
A217: the Source of G . (PK . i) = pk . i by A31, A209, A216, Def19;
A218: the Target of G . (PK . i) = pk . (i + 1) by A31, A209, A216, Def19;
A219: Q . i = PK . i by A192, A209, A216, Lm1;
A220: i + 1 <= len pk by A205, A206, A215, NAT_1:13;
thus the Source of G . (Q . i) = q . i by A205, A206, A209, A210, A217, A219, Lm1; :: thesis: the Target of G . (Q . i) = q . (i + 1)
thus the Target of G . (Q . i) = q . (i + 1) by A218, A219, A220, Lm1, NAT_1:12; :: thesis: verum
end;
end;
end;
thus Q is_oriented_edge_seq_of q by A207, A208, Def19; :: thesis: ( Q is_shortestpath_of v1,v3, UsedVx h,n,W & cost Q,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies Q islongestInShortestpath UsedVx h,n,v1,W ) )
A221: (cost PK,W) + (cost pe,W) = cost Q,W by A18, A192, GRAPH_5:50, GRAPH_5:58;
A222: cost pe,W = W . (pe . 1) by A18, A190, Th4, GRAPH_5:50
.= Weight vk,v3,W by A188, A191, Th26 ;
A223: newpathcost ((findmin n) . g),n,j = cost Q,W by A18, A46, A47, A96, A192, A222, GRAPH_5:50, GRAPH_5:58;
hereby :: thesis: ( cost Q,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies Q islongestInShortestpath UsedVx h,n,v1,W ) )
per cases ( g . (n + j) = - 1 or g . (n + j) <> - 1 ) ;
suppose A224: g . (n + j) = - 1 ; :: thesis: Q is_shortestpath_of v1,v3, UsedVx h,n,W
A225: now
let v2 be Vertex of G; :: thesis: ( v2 in UsedVx g,n implies for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) )
assume A226: v2 in UsedVx g,n ; :: thesis: for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 )
reconsider m = v2 as Element of NAT by A226;
A227: - 1 = f . (((2 * n) + (n * m)) + j) by A9, A66, A67, A224, A226
.= Weight v2,v3,W by A1, A63, Def20 ;
thus for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) by A227, Th24; :: thesis: verum
end;
thus Q is_shortestpath_of v1,v3, UsedVx h,n,W by A2, A7, A24, A32, A62, A188, A192, A225, Th15; :: thesis: verum
end;
suppose A228: g . (n + j) <> - 1 ; :: thesis: Q is_shortestpath_of v1,v3, UsedVx h,n,W
A229: 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 Element of 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, A62, A63, A228;
thus Q is_shortestpath_of v1,v3, UsedVx h,n,W by A2, A7, A13, A18, A22, A24, A32, A34, A44, A46, A47, A62, A70, A74, A96, A97, A177, A188, A192, A221, A222, A228, A229, Th19, GRAPH_5:69; :: thesis: verum
end;
end;
end;
thus cost Q,W = h . ((2 * n) + j) by A16, A72, A75, A77, A78, A82, A175, A223, Def14; :: thesis: ( not v3 in UsedVx h,n implies Q islongestInShortestpath UsedVx h,n,v1,W )
A230: 0 <= cost pe,W by A18, GRAPH_5:54;
A231: (cost PK,W) + 0 <= cost Q,W by A221, A230, XREAL_1:9;
hereby :: thesis: verum
assume not v3 in UsedVx h,n ; :: thesis: Q islongestInShortestpath UsedVx h,n,v1,W
A232: now
let v2 be Vertex of G; :: thesis: ( v2 in UsedVx h,n & v2 <> v1 implies ex PK being oriented Chain of G st
( b2 is_shortestpath_of v1,PK, UsedVx h,n,W & cost b2,W <= cost Q,W ) )
assume that
A233: v2 in UsedVx h,n and
A234: v2 <> v1 ; :: thesis: ex PK being oriented Chain of G st
( b2 is_shortestpath_of v1,PK, UsedVx h,n,W & cost b2,W <= cost Q,W )
per cases ( v2 in {(Argmin (OuterVx g,n),g,n)} or v2 in UsedVx g,n ) by A24, A233, XBOOLE_0:def 3;
suppose A235: v2 in {(Argmin (OuterVx g,n),g,n)} ; :: thesis: ex PK being oriented Chain of G st
( b2 is_shortestpath_of v1,PK, UsedVx h,n,W & cost b2,W <= cost Q,W )
A236: v2 = Argmin (OuterVx g,n),g,n by A235, TARSKI:def 1;
take PK = PK; :: thesis: ( PK is_shortestpath_of v1,v2, UsedVx h,n,W & cost PK,W <= cost Q,W )
thus PK is_shortestpath_of v1,v2, UsedVx h,n,W by A24, A32, A236, Th8; :: thesis: cost PK,W <= cost Q,W
thus cost PK,W <= cost Q,W by A231; :: thesis: verum
end;
suppose A237: v2 in UsedVx g,n ; :: thesis: ex P being oriented Chain of G st
( b2 is_shortestpath_of v1,P, UsedVx h,n,W & cost b2,W <= cost Q,W )
consider P being oriented Chain of G such that
A238: P is_shortestpath_of v1,v2, UsedVx g,n,W and
A239: cost P,W <= cost PK,W by A4, A5, A6, A34, A234, A237, Th40, GRAPH_5:def 19;
A240: now
let R be oriented Chain of G; :: thesis: for v4 being Vertex of G st not v4 in UsedVx g,n & R is_shortestpath_of v1,v4, UsedVx g,n,W holds
cost P,W <= cost R,W
let v4 be Vertex of G; :: thesis: ( not v4 in UsedVx g,n & R is_shortestpath_of v1,v4, UsedVx g,n,W implies cost P,W <= cost R,W )
assume that
A241: not v4 in UsedVx g,n and
A242: R is_shortestpath_of v1,v4, UsedVx g,n,W ; :: thesis: cost P,W <= cost R,W
A243: v4 in VG ;
reconsider j4 = v4 as Element of NAT by A243;
A244: 1 <= j4 by A17, A243, FINSEQ_1:3;
A245: j4 <= n by A17, A243, FINSEQ_1:3;
A246: g . (n + j4) <> - 1 by A1, A2, A7, A9, A18, A241, A242, A244, A245, Lm19;
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 Element of NAT st 1 <= i & i < len rn holds
rn . i in UsedVx g,n and
RR is_oriented_edge_seq_of rn and
A247: RR is_shortestpath_of v1,v4, UsedVx g,n,W and
cost RR,W = g . ((2 * n) + j4) and
A248: ( not v4 in UsedVx g,n implies RR islongestInShortestpath UsedVx g,n,v1,W ) by A2, A7, A8, A241, A246;
consider PP being oriented Chain of G such that
A249: PP is_shortestpath_of v1,v2, UsedVx g,n,W and
A250: cost PP,W <= cost RR,W by A234, A237, A241, A248, GRAPH_5:def 19;
A251: cost PP,W = cost P,W by A238, A249, Th9;
thus cost P,W <= cost R,W by A242, A247, A250, A251, Th9; :: thesis: verum
end;
take P = P; :: thesis: ( P is_shortestpath_of v1,v2, UsedVx h,n,W & cost P,W <= cost Q,W )
thus P is_shortestpath_of v1,v2, UsedVx h,n,W by A18, A26, A234, A238, A240, GRAPH_5:68; :: thesis: cost P,W <= cost Q,W
thus cost P,W <= cost Q,W by A231, A239, XXREAL_0:2; :: thesis: verum
end;
end;
end;
thus Q islongestInShortestpath UsedVx h,n,v1,W by A232, GRAPH_5:def 19; :: thesis: verum
end;
end;
end;
end;
hereby :: thesis: for m being Element of NAT st m in UsedVx h,n holds
h . (n + m) <> - 1
let m, j be Element of NAT ; :: thesis: ( h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n implies f . (((2 * n) + (n * b1)) + b2) = - 1 )
assume that
A252: h . (n + j) = - 1 and
A253: 1 <= j and
A254: j <= n and
A255: m in UsedVx h,n ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
set nj = n + j;
A256: 1 < n + j by A253, A254, Lm12;
A257: n + j <= 2 * n by A253, A254, Lm12;
A258: n + j < ((n * n) + (3 * n)) + 1 by A253, A254, Lm12;
A259: n + j in dom g by A12, A20, A256, A258, FINSEQ_3:27;
A260: n + 1 <= n + j by A253, XREAL_1:9;
A261: n < n + j by A260, NAT_1:13;
A262: now
assume A263: (findmin n) . g hasBetterPathAt n,(n + j) -' n ; :: thesis: contradiction
A264: h . (n + j) = Argmin (OuterVx g,n),g,n by A14, A16, A46, A257, A259, A261, A263, Def14;
thus contradiction by A252, A264, NAT_1:2; :: thesis: verum
end;
A265: ((findmin n) . g) . (n + j) = g . (n + j) by A13, A22, A258, A261, Th19;
A266: g . (n + j) = - 1 by A14, A16, A252, A257, A259, A261, A262, A265, Def14;
A267: not j in UsedVx g,n by A10, A266;
A268: j < ((n * n) + (3 * n)) + 1 by A27, A254, XXREAL_0:2;
A269: j in dom g by A12, A20, A253, A268, FINSEQ_3:27;
A270: g . j <> - 1 by A253, A254, A267, A269;
A271: ((findmin n) . g) . j <> - 1 by A13, A23, A27, A254, A266, A270, Th19;
A272: not (findmin n) . g hasBetterPathAt n,j by A262, NAT_D:34;
A273: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) < 0 by A265, A266, A271, A272, Def13;
reconsider v3 = j as Vertex of G by A17, A253, A254, FINSEQ_1:3;
set Akj = ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j;
A274: 1 < ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j by A21, A22, A254, Lm13;
A275: Argmin (OuterVx g,n),g,n < ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j by A21, A22, A254, Lm13;
A276: ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j < ((n * n) + (3 * n)) + 1 by A21, A22, A254, Lm13;
A277: ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j in dom g by A12, A20, A274, A276, FINSEQ_3:27;
A278: (3 * n) + 1 <= ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j by A21, A22, A253, A254, Lm14;
A279: ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j <= (n * n) + (3 * n) by A21, A22, A253, A254, Lm14;
A280: f . (((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j) = Weight vk,v3,W by A1, Def20;
A281: ((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, A46, A277, PARTFUN1:def 8
.= g . (((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j) by A13, A275, A276, Th19
.= Weight vk,v3,W by A20, A40, A277, A278, A279, A280, Def16 ;
per cases ( m in {(Argmin (OuterVx g,n),g,n)} or m in UsedVx g,n ) by A24, A255, XBOOLE_0:def 3;
suppose A282: m in {(Argmin (OuterVx g,n),g,n)} ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
A283: m = Argmin (OuterVx g,n),g,n by A282, TARSKI:def 1;
A284: for e being set holds
( not e in the carrier' of G or not e orientedly_joins vk,v3 ) by A273, A281, Th24;
A285: Weight vk,v3,W = - 1 by A284, Def7;
thus f . (((2 * n) + (n * m)) + j) = - 1 by A1, A283, A285, Def20; :: thesis: verum
end;
suppose A286: m in UsedVx g,n ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
thus f . (((2 * n) + (n * m)) + j) = - 1 by A9, A253, A254, A266, A286; :: thesis: verum
end;
end;
end;
let m be Element of NAT ; :: thesis: ( m in UsedVx h,n implies h . (n + m) <> - 1 )
assume A287: m in UsedVx h,n ; :: thesis: h . (n + m) <> - 1
per cases ( m in UsedVx g,n or m in {(Argmin (OuterVx g,n),g,n)} ) by A24, A287, XBOOLE_0:def 3;
suppose A288: m in UsedVx g,n ; :: thesis: h . (n + m) <> - 1
A289: h . (n + m) = g . (n + m) by A4, A5, A6, A12, A288, Lm16;
thus h . (n + m) <> - 1 by A10, A288, A289; :: thesis: verum
end;
suppose A290: m in {(Argmin (OuterVx g,n),g,n)} ; :: thesis: h . (n + m) <> - 1
thus h . (n + m) <> - 1 by A23, A61, A290, TARSKI:def 1; :: thesis: verum
end;
end;