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 <> {} & k >= 1 & 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 <> {} & k >= 1 & 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 <> {} & k >= 1 & 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 <> {} & k >= 1 & 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 <> {} & k >= 1 & 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 A1: ( 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 <> {} & k >= 1 & 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 A2: 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 A3: ( ( 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 ) ) ; :: 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;
A4: 1 <= ((n * n) + (3 * n)) + 1 by NAT_1:12;
A5: len f = ((n * n) + (3 * n)) + 1 by A1, Def20;
A6: (findmin n) . g = g,(((n * n) + (3 * n)) + 1) := (Argmin (OuterVx g,n),g,n),(- 1) by Def11;
A7: dom ((findmin n) . g) = dom g by Th34;
h = (Relax n) . ((findmin n) . g) by A1, Th23;
then A8: h = Relax ((findmin n) . g),n by Def15;
A9: Seg n = the carrier of G by A1, Def20;
then reconsider VG = the carrier of G as non empty Subset of NAT by A1;
A10: W is_weight>=0of G by GRAPH_5:def 13;
A11: (2 * n) + n = (2 + 1) * n ;
A12: dom f = dom g by A1, Th42;
A13: ( Argmin (OuterVx g,n),g,n in dom g & 1 <= Argmin (OuterVx g,n),g,n & Argmin (OuterVx g,n),g,n <= n & g . (Argmin (OuterVx g,n),g,n) <> - 1 & g . (n + (Argmin (OuterVx g,n),g,n)) <> - 1 ) by A1, Th30;
set Uh = UsedVx h,n;
A14: ( UsedVx h,n = (UsedVx g,n) \/ {(Argmin (OuterVx g,n),g,n)} & not Argmin (OuterVx g,n),g,n in UsedVx g,n ) by A1, Th40;
then A15: UsedVx g,n c= UsedVx h,n by XBOOLE_1:7;
A16: n < ((n * n) + (3 * n)) + 1 by Lm7;
A17: dom f = dom h by A1, Th42;
reconsider vk = Argmin (OuterVx g,n),g,n as Vertex of G by A9, A13, FINSEQ_1:3;
consider pk being FinSequence of NAT , PK being oriented Chain of G such that
A18: ( pk is_simple_vertex_seq_at g, Argmin (OuterVx g,n),g,n,n & ( for i being Element of NAT st 1 <= i & i < len pk holds
pk . i in UsedVx g,n ) & PK is_oriented_edge_seq_of pk & PK is_shortestpath_of v1,vk, UsedVx g,n,W & cost PK,W = g . ((2 * n) + (Argmin (OuterVx g,n),g,n)) & ( not vk in UsedVx g,n implies PK islongestInShortestpath UsedVx g,n,v1,W ) ) by A1, A2, A13, A14;
consider kk being Element of NAT such that
A19: ( 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 A1, Def10;
set nAk = (2 * n) + (Argmin (OuterVx g,n),g,n);
A20: ( 1 < (2 * n) + (Argmin (OuterVx g,n),g,n) & (2 * n) + (Argmin (OuterVx g,n),g,n) < ((n * n) + (3 * n)) + 1 & Argmin (OuterVx g,n),g,n < (2 * n) + (Argmin (OuterVx g,n),g,n) ) by A13, Lm11;
then A21: (2 * n) + (Argmin (OuterVx g,n),g,n) in dom g by A5, A12, FINSEQ_3:27;
A22: f,g equal_at (3 * n) + 1,(n * n) + (3 * n) by A1, Th47;
PK is_orientedpath_of v1,vk, UsedVx g,n by A18, GRAPH_5:def 18;
then A23: PK is_orientedpath_of v1,vk by GRAPH_5:def 4;
then PK <> {} by GRAPH_5:def 3;
then A24: len PK >= 1 by FINSEQ_1:28;
A25: ((n * n) + (3 * n)) + 1 in dom g by A4, A5, A12, FINSEQ_3:27;
then A26: ((findmin n) . g) /. (((n * n) + (3 * n)) + 1) = ((findmin n) . g) . (((n * n) + (3 * n)) + 1) by A7, PARTFUN1:def 8
.= Argmin (OuterVx g,n),g,n by A6, A13, A16, A25, Th18 ;
A27: ((findmin n) . g) /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) = ((findmin n) . g) . ((2 * n) + (Argmin (OuterVx g,n),g,n)) by A7, A21, PARTFUN1:def 8
.= cost PK,W by A6, A18, A20, A21, Th19 ;
set nk = n + (Argmin (OuterVx g,n),g,n);
A28: ( 1 < n + (Argmin (OuterVx g,n),g,n) & n + (Argmin (OuterVx g,n),g,n) <= 2 * n & n + (Argmin (OuterVx g,n),g,n) < ((n * n) + (3 * n)) + 1 ) by A13, Lm12;
n + 1 <= n + (Argmin (OuterVx g,n),g,n) by A13, XREAL_1:9;
then A29: n < n + (Argmin (OuterVx g,n),g,n) by NAT_1:13;
A30: n + (Argmin (OuterVx g,n),g,n) in dom g by A5, A12, A28, FINSEQ_3:27;
then A31: ((findmin n) . g) . (n + (Argmin (OuterVx g,n),g,n)) = g . (n + (Argmin (OuterVx g,n),g,n)) by A28, A29, Th32;
now
set Wke = ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin (OuterVx g,n),g,n));
assume (findmin n) . g hasBetterPathAt n, Argmin (OuterVx g,n),g,n ; :: thesis: contradiction
then A32: ( ( ((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 Def13;
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:9;
hence contradiction by A1, A26, A31, A32, Th30; :: thesis: verum
end;
then not (findmin n) . g hasBetterPathAt n,(n + (Argmin (OuterVx g,n),g,n)) -' n by NAT_D:34;
then A33: h . (n + (Argmin (OuterVx g,n),g,n)) = g . (n + (Argmin (OuterVx g,n),g,n)) by A7, A8, A28, A29, A30, A31, 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 A34: ( v3 <> v1 & v3 = j & 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;
j in VG by A34;
then A35: ( 1 <= j & j <= n ) by A9, FINSEQ_1:3;
then A36: ( 1 < n + j & n + j <= 2 * n & n + j < ((n * n) + (3 * n)) + 1 ) by Lm12;
then A37: n + j in dom g by A5, A12, FINSEQ_3:27;
A38: (n + j) -' n = j by NAT_D:34;
n + 1 <= n + j by A35, XREAL_1:9;
then A39: n < n + j by NAT_1:13;
set m2 = (2 * n) + j;
A40: (2 * n) + j <= 3 * n by A11, A35, XREAL_1:9;
(2 * n) + 1 <= (2 * n) + j by A35, XREAL_1:9;
then A41: 2 * n < (2 * n) + j by NAT_1:13;
A42: ((2 * n) + j) -' (2 * n) = j by NAT_D:34;
A43: ( 1 < (2 * n) + j & (2 * n) + j < ((n * n) + (3 * n)) + 1 ) by A35, Lm11;
then A44: (2 * n) + j in dom g by A5, A12, FINSEQ_3:27;
A45: (2 * n) + j in dom ((findmin n) . g) by A5, A7, A12, A43, FINSEQ_3:27;
A46: ((findmin n) . g) . (n + j) = g . (n + j) by A6, A13, A36, A37, A39, Th19;
n <= 2 * n by Lm6;
then n < (2 * n) + j by A41, XXREAL_0:2;
then A47: ((findmin n) . g) . ((2 * n) + j) = g . ((2 * n) + j) by A6, A13, A43, A44, Th19;
A48: j < ((n * n) + (3 * n)) + 1 by A16, A35, XXREAL_0:2;
then A49: j in dom g by A5, A12, A35, FINSEQ_3:27;
A50: j in dom h by A5, A17, A35, A48, FINSEQ_3:27;
set Akj = ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j;
A51: ( 1 < ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j & Argmin (OuterVx g,n),g,n < ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j & ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j < ((n * n) + (3 * n)) + 1 ) by A13, A35, Lm13;
then A52: ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j in dom g by A5, A12, FINSEQ_3:27;
A53: ( (3 * n) + 1 <= ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j & ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j <= (n * n) + (3 * n) ) by A13, A35, Lm14;
A54: ((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 A7, A26, A52, PARTFUN1:def 8
.= g . (((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j) by A6, A51, A52, Th19
.= f . (((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j) by A12, A22, A52, A53, Def16
.= Weight vk,v3,W by A1, A34, Def20 ;
A55: ((findmin n) . g) /. ((2 * n) + j) = g . ((2 * n) + j) by A7, A44, A47, PARTFUN1:def 8;
per cases ( not (findmin n) . g hasBetterPathAt n,(n + j) -' n or (findmin n) . g hasBetterPathAt n,(n + j) -' n ) ;
suppose A56: 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 ) )
then A57: h . (n + j) = g . (n + j) by A7, A8, A36, A37, A39, A46, Def14;
then consider p being FinSequence of NAT , P being oriented Chain of G such that
A58: ( 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 A2, A34;
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 A1, A5, A57, A58, 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 ( 1 <= i & i < len p ) ; :: thesis: p . i in UsedVx h,n
then p . i in UsedVx g,n by A58;
hence p . i in UsedVx h,n by A15; :: thesis: verum
end;
thus P is_oriented_edge_seq_of p by A58; :: 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 ((findmin n) . g) . j = - 1 ; :: thesis: P is_shortestpath_of v1,v3, UsedVx h,n,W
then (Relax ((findmin n) . g),n) . j = - 1 by A7, A35, A49, Def14;
then j in { i where i is Element of NAT : ( i in dom h & 1 <= i & i <= n & h . i = - 1 ) } by A8, A35, A50;
then A59: ( j in UsedVx g,n or j in {(Argmin (OuterVx g,n),g,n)} ) by A14, XBOOLE_0:def 3;
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 A60: ( not v4 in UsedVx g,n & Q is_shortestpath_of v1,v4, UsedVx g,n,W ) ; :: thesis: cost P,W <= cost b1,W
A61: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A62: ( 1 <= j4 & j4 <= n ) by A9, A61, FINSEQ_1:3;
then A63: g . (n + j4) <> - 1 by A1, A3, A10, A60, Lm19;
then consider q being FinSequence of NAT , R being oriented Chain of G such that
A64: ( q is_simple_vertex_seq_at g,j4,n & ( for i being Element of NAT st 1 <= i & i < len q holds
q . i in UsedVx g,n ) & R is_oriented_edge_seq_of q & R is_shortestpath_of v1,v4, UsedVx g,n,W & cost R,W = g . ((2 * n) + j4) & ( not v4 in UsedVx g,n implies R islongestInShortestpath UsedVx g,n,v1,W ) ) by A1, A2, A60;
A65: cost R,W = cost Q,W by A60, A64, Th9;
per cases ( j in UsedVx g,n or j = Argmin (OuterVx g,n),g,n ) by A59, TARSKI:def 1;
suppose j in UsedVx g,n ; :: thesis: cost P,W <= cost b1,W
then consider PP being oriented Chain of G such that
A66: ( PP is_shortestpath_of v1,v3, UsedVx g,n,W & cost PP,W <= cost R,W ) by A34, A60, A64, GRAPH_5:def 19;
thus cost P,W <= cost Q,W by A58, A65, A66, Th9; :: thesis: verum
end;
suppose A67: j = Argmin (OuterVx g,n),g,n ; :: thesis: cost P,W <= cost b1,W
j4 <= ((n * n) + (3 * n)) + 1 by A16, A62, XXREAL_0:2;
then A68: j4 in dom g by A5, A12, A62, FINSEQ_3:27;
then g . j4 <> - 1 by A60, A62;
then 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 A62, A63, A68;
then A69: g /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) <= g /. ((2 * n) + j4) by A19;
A70: g /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) = g . ((2 * n) + (Argmin (OuterVx g,n),g,n)) by A21, PARTFUN1:def 8;
( 1 < (2 * n) + j4 & (2 * n) + j4 < ((n * n) + (3 * n)) + 1 ) by A62, Lm11;
then (2 * n) + j4 in dom g by A5, A12, FINSEQ_3:27;
hence cost P,W <= cost Q,W by A58, A64, A65, A67, A69, A70, PARTFUN1:def 8; :: thesis: verum
end;
end;
end;
hence P is_shortestpath_of v1,v3, UsedVx h,n,W by A10, A15, A34, A58, GRAPH_5:68; :: thesis: verum
end;
suppose A71: ((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 A72: ((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
then A73: ((findmin n) . g) /. ((2 * n) + j) <= newpathcost ((findmin n) . g),n,j by A38, A56, A71, Def13;
A74: ((findmin n) . g) /. ((2 * n) + j) = cost P,W by A45, A47, A58, PARTFUN1:def 8;
consider e being set such that
A75: ( e in the carrier' of G & e orientedly_joins vk,v3 ) by A54, A72, Th24;
reconsider pe = <*e*> as oriented Chain of G by A75, Th5;
A76: ( len pe = 1 & pe . 1 = e ) by FINSEQ_1:57;
then consider Q being oriented Chain of G such that
A77: ( Q = PK ^ pe & Q is_orientedpath_of v1,v3 ) by A23, A24, A75, GRAPH_5:37;
cost pe,W = W . (pe . 1) by A10, A76, Th4, GRAPH_5:50
.= Weight vk,v3,W by A75, A76, Th26 ;
then cost Q,W = newpathcost ((findmin n) . g),n,j by A10, A26, A27, A54, A77, GRAPH_5:50, GRAPH_5:58;
hence P is_shortestpath_of v1,v3, UsedVx h,n,W by A1, A10, A14, A18, A24, A34, A58, A73, A74, A75, A77, GRAPH_5:69; :: thesis: verum
end;
suppose ((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
then for e being set holds
( not e in the carrier' of G or not e orientedly_joins vk,v3 ) by A54, Th24;
hence P is_shortestpath_of v1,v3, UsedVx h,n,W by A1, A10, A14, A18, A34, A58, Th13; :: thesis: verum
end;
end;
end;
end;
end;
end;
thus cost P,W = h . ((2 * n) + j) by A8, A38, A40, A41, A42, A45, A47, A56, A58, Def14; :: thesis: ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W )
hereby :: thesis: verum
assume A78: not v3 in UsedVx h,n ; :: thesis: P islongestInShortestpath UsedVx h,n,v1,W
then A79: not v3 in UsedVx g,n by A14, XBOOLE_0:def 3;
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 A80: ( v2 in UsedVx h,n & 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 A14, A80, XBOOLE_0:def 3;
suppose 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 )
then A81: v2 = vk by 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 A14, A18, A81, Th8; :: thesis: cost PK,W <= cost P,W
g . j <> - 1 by A34, A35, A49, A79;
then 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 A34, A35, A49, A57;
then A82: g /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) <= g /. ((2 * n) + j) by A19;
g /. ((2 * n) + (Argmin (OuterVx g,n),g,n)) = cost PK,W by A18, A21, PARTFUN1:def 8;
hence cost PK,W <= cost P,W by A44, A58, A82, PARTFUN1:def 8; :: thesis: verum
end;
suppose A83: 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 )
then consider Q being oriented Chain of G such that
A84: ( Q is_shortestpath_of v1,v2, UsedVx g,n,W & cost Q,W <= cost P,W ) by A14, A58, A78, A80, GRAPH_5:def 19, XBOOLE_0:def 3;
A85: 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 A86: ( not v4 in UsedVx g,n & R is_shortestpath_of v1,v4, UsedVx g,n,W ) ; :: thesis: cost Q,W <= cost R,W
A87: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
( 1 <= j4 & j4 <= n ) by A9, A87, FINSEQ_1:3;
then g . (n + j4) <> - 1 by A1, A3, A10, A86, Lm19;
then consider rn being FinSequence of NAT , RR being oriented Chain of G such that
A88: ( rn is_simple_vertex_seq_at g,j4,n & ( for i being Element of NAT st 1 <= i & i < len rn holds
rn . i in UsedVx g,n ) & RR is_oriented_edge_seq_of rn & RR is_shortestpath_of v1,v4, UsedVx g,n,W & cost RR,W = g . ((2 * n) + j4) & ( not v4 in UsedVx g,n implies RR islongestInShortestpath UsedVx g,n,v1,W ) ) by A1, A2, A86;
consider QQ being oriented Chain of G such that
A89: ( QQ is_shortestpath_of v1,v2, UsedVx g,n,W & cost QQ,W <= cost RR,W ) by A80, A83, A86, A88, GRAPH_5:def 19;
cost QQ,W = cost Q,W by A84, A89, Th9;
hence cost Q,W <= cost R,W by A86, A88, A89, 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 A10, A15, A80, A84, A85, GRAPH_5:68; :: thesis: cost Q,W <= cost P,W
thus cost Q,W <= cost P,W by A84; :: thesis: verum
end;
end;
end;
hence P islongestInShortestpath UsedVx h,n,v1,W by GRAPH_5:def 19; :: thesis: verum
end;
end;
suppose A90: (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 ) )
then A91: (Relax ((findmin n) . g),n) . (n + j) = Argmin (OuterVx g,n),g,n by A7, A26, A36, A37, A39, Def14;
A92: ( ( ((findmin n) . g) . (n + j) = - 1 or ((findmin n) . g) /. ((2 * n) + j) > newpathcost ((findmin n) . g),n,j ) & ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 & ((findmin n) . g) . j <> - 1 ) by A38, A90, Def13;
A93: newpathcost ((findmin n) . g),n,j = (((findmin n) . g) /. ((2 * n) + (Argmin (OuterVx g,n),g,n))) + (Weight vk,v3,W) by A26, A54;
A94: now
assume A95: Argmin (OuterVx g,n),g,n = j ; :: thesis: contradiction
then A96: ((findmin n) . g) . (n + j) <> - 1 by A6, A13, A36, A37, A39, Th19;
(((findmin n) . g) /. ((2 * n) + j)) + (Weight vk,v3,W) >= (((findmin n) . g) /. ((2 * n) + j)) + 0 by A54, A92, XREAL_1:9;
hence contradiction by A38, A90, A93, A95, A96, Def13; :: thesis: verum
end;
A97: now
assume j in UsedVx g,n ; :: thesis: contradiction
then consider i being Element of NAT such that
A98: ( j = i & i in dom g & 1 <= i & i <= n & g . i = - 1 ) ;
thus contradiction by A16, A92, A98, Th33; :: thesis: verum
end;
consider e being set such that
A99: ( e in the carrier' of G & e orientedly_joins vk,v3 ) by A54, A92, Th24;
reconsider pe = <*e*> as oriented Chain of G by A99, Th5;
A100: ( len pe = 1 & pe . 1 = e ) by FINSEQ_1:57;
then consider Q being oriented Chain of G such that
A101: ( Q = PK ^ pe & Q is_orientedpath_of v1,v3 ) by A23, A24, A99, 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 A1, A5, A8, A18, A33, A91, A94, A97, 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 ) )
A102: ( len pk > 1 & pk is_vertex_seq_at g, Argmin (OuterVx g,n),g,n,n ) by A18, Def18;
then A103: q . (len pk) = pk . (len pk) by Lm1
.= Argmin (OuterVx g,n),g,n by A102, 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 A104: ( 1 <= i & i < len q ) ; :: thesis: q . i in UsedVx h,n
then i < (len pk) + 1 by FINSEQ_2:19;
then A105: i <= len pk by NAT_1:13;
now
per cases ( i = len pk or i <> len pk ) ;
suppose i = len pk ; :: thesis: ( q . i in {(Argmin (OuterVx g,n),g,n)} or q . i in UsedVx g,n )
hence ( q . i in {(Argmin (OuterVx g,n),g,n)} or q . i in UsedVx g,n ) by A103, TARSKI:def 1; :: thesis: verum
end;
suppose i <> len pk ; :: thesis: ( q . i in {(Argmin (OuterVx g,n),g,n)} or q . i in UsedVx g,n )
then A106: i < len pk by A105, XXREAL_0:1;
q . i = pk . i by A104, A105, Lm1;
hence ( q . i in {(Argmin (OuterVx g,n),g,n)} or q . i in UsedVx g,n ) by A18, A104, A106; :: thesis: verum
end;
end;
end;
hence q . i in UsedVx h,n by A14, XBOOLE_0:def 3; :: thesis: verum
end;
A107: len Q = (len PK) + 1 by A100, A101, FINSEQ_1:35;
A108: len pk = (len PK) + 1 by A18, Def19;
then A109: len q = (len Q) + 1 by A107, FINSEQ_2:19;
set FS = the Source of G;
set FT = the Target of G;
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 A110: ( 1 <= i & 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 A111: i = len Q ; :: thesis: ( the Source of G . (Q . b1) = q . b1 & the Target of G . (Q . b1) = q . (b1 + 1) )
then A112: Q . i = e by A100, A101, A107, Lm2;
then A113: ( the Source of G . (Q . i) = vk & the Target of G . (Q . i) = v3 ) by A99, GRAPH_4:def 1;
thus the Source of G . (Q . i) = q . i by A99, A103, A107, A108, A111, A112, 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 A34, A107, A108, A111, A113, FINSEQ_1:59; :: thesis: verum
end;
suppose i <> len Q ; :: thesis: ( the Source of G . (Q . b1) = q . b1 & the Target of G . (Q . b1) = q . (b1 + 1) )
then A114: i < len Q by A110, XXREAL_0:1;
then A115: i <= len PK by A107, NAT_1:13;
then A116: ( the Source of G . (PK . i) = pk . i & the Target of G . (PK . i) = pk . (i + 1) ) by A18, A110, Def19;
A117: Q . i = PK . i by A101, A110, A115, Lm1;
A118: i + 1 <= len pk by A107, A108, A114, NAT_1:13;
thus the Source of G . (Q . i) = q . i by A107, A108, A110, A116, A117, Lm1; :: thesis: the Target of G . (Q . i) = q . (i + 1)
thus the Target of G . (Q . i) = q . (i + 1) by A116, A117, A118, Lm1, NAT_1:12; :: thesis: verum
end;
end;
end;
hence Q is_oriented_edge_seq_of q by A109, 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 ) )
A119: (cost PK,W) + (cost pe,W) = cost Q,W by A10, A101, GRAPH_5:50, GRAPH_5:58;
A120: cost pe,W = W . (pe . 1) by A10, A100, Th4, GRAPH_5:50
.= Weight vk,v3,W by A99, A100, Th26 ;
then A121: newpathcost ((findmin n) . g),n,j = cost Q,W by A10, A26, A27, A54, A101, 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 A122: g . (n + j) = - 1 ; :: thesis: Q is_shortestpath_of v1,v3, UsedVx h,n,W
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 A123: 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 )
then reconsider m = v2 as Element of NAT ;
- 1 = f . (((2 * n) + (n * m)) + j) by A3, A35, A122, A123
.= Weight v2,v3,W by A1, A34, Def20 ;
hence for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) by Th24; :: thesis: verum
end;
hence Q is_shortestpath_of v1,v3, UsedVx h,n,W by A1, A14, A18, A34, A99, A101, Th15; :: thesis: verum
end;
suppose A124: g . (n + j) <> - 1 ; :: thesis: Q is_shortestpath_of v1,v3, UsedVx h,n,W
then consider p being FinSequence of NAT , P being oriented Chain of G such that
A125: ( 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 A2, A34;
thus Q is_shortestpath_of v1,v3, UsedVx h,n,W by A1, A6, A10, A13, A14, A18, A24, A26, A27, A34, A36, A37, A39, A54, A55, A92, A99, A101, A119, A120, A124, A125, Th19, GRAPH_5:69; :: thesis: verum
end;
end;
end;
thus cost Q,W = h . ((2 * n) + j) by A8, A38, A40, A41, A42, A45, A90, A121, Def14; :: thesis: ( not v3 in UsedVx h,n implies Q islongestInShortestpath UsedVx h,n,v1,W )
0 <= cost pe,W by A10, GRAPH_5:54;
then A126: (cost PK,W) + 0 <= cost Q,W by A119, XREAL_1:9;
hereby :: thesis: verum
assume not v3 in UsedVx h,n ; :: thesis: Q islongestInShortestpath UsedVx h,n,v1,W
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 A127: ( v2 in UsedVx h,n & 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 A14, A127, XBOOLE_0:def 3;
suppose 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 )
then A128: v2 = Argmin (OuterVx g,n),g,n by 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 A14, A18, A128, Th8; :: thesis: cost PK,W <= cost Q,W
thus cost PK,W <= cost Q,W by A126; :: thesis: verum
end;
suppose A129: 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 )
then consider P being oriented Chain of G such that
A130: ( P is_shortestpath_of v1,v2, UsedVx g,n,W & cost P,W <= cost PK,W ) by A1, A18, A127, Th40, GRAPH_5:def 19;
A131: 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 A132: ( not v4 in UsedVx g,n & R is_shortestpath_of v1,v4, UsedVx g,n,W ) ; :: thesis: cost P,W <= cost R,W
A133: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
( 1 <= j4 & j4 <= n ) by A9, A133, FINSEQ_1:3;
then g . (n + j4) <> - 1 by A1, A3, A10, A132, Lm19;
then consider rn being FinSequence of NAT , RR being oriented Chain of G such that
A134: ( rn is_simple_vertex_seq_at g,j4,n & ( for i being Element of NAT st 1 <= i & i < len rn holds
rn . i in UsedVx g,n ) & RR is_oriented_edge_seq_of rn & RR is_shortestpath_of v1,v4, UsedVx g,n,W & cost RR,W = g . ((2 * n) + j4) & ( not v4 in UsedVx g,n implies RR islongestInShortestpath UsedVx g,n,v1,W ) ) by A1, A2, A132;
consider PP being oriented Chain of G such that
A135: ( PP is_shortestpath_of v1,v2, UsedVx g,n,W & cost PP,W <= cost RR,W ) by A127, A129, A132, A134, GRAPH_5:def 19;
cost PP,W = cost P,W by A130, A135, Th9;
hence cost P,W <= cost R,W by A132, A134, A135, 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 A10, A15, A127, A130, A131, GRAPH_5:68; :: thesis: cost P,W <= cost Q,W
thus cost P,W <= cost Q,W by A126, A130, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence Q islongestInShortestpath UsedVx h,n,v1,W by 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 A136: ( h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n ) ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
set nj = n + j;
A137: ( 1 < n + j & n + j <= 2 * n & n + j < ((n * n) + (3 * n)) + 1 ) by A136, Lm12;
then A138: n + j in dom g by A5, A12, FINSEQ_3:27;
n + 1 <= n + j by A136, XREAL_1:9;
then A139: n < n + j by NAT_1:13;
A140: now
assume (findmin n) . g hasBetterPathAt n,(n + j) -' n ; :: thesis: contradiction
then h . (n + j) = Argmin (OuterVx g,n),g,n by A7, A8, A26, A137, A138, A139, Def14;
hence contradiction by A136, NAT_1:2; :: thesis: verum
end;
A141: ((findmin n) . g) . (n + j) = g . (n + j) by A6, A13, A137, A138, A139, Th19;
then A142: g . (n + j) = - 1 by A7, A8, A136, A137, A138, A139, A140, Def14;
then A143: not j in UsedVx g,n by A3;
j < ((n * n) + (3 * n)) + 1 by A16, A136, XXREAL_0:2;
then A144: j in dom g by A5, A12, A136, FINSEQ_3:27;
then g . j <> - 1 by A136, A143;
then A145: ((findmin n) . g) . j <> - 1 by A6, A13, A16, A136, A142, A144, Th19;
not (findmin n) . g hasBetterPathAt n,j by A140, NAT_D:34;
then A146: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) < 0 by A141, A142, A145, Def13;
reconsider v3 = j as Vertex of G by A9, A136, FINSEQ_1:3;
set Akj = ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j;
A147: ( 1 < ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j & Argmin (OuterVx g,n),g,n < ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j & ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j < ((n * n) + (3 * n)) + 1 ) by A13, A136, Lm13;
then A148: ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j in dom g by A5, A12, FINSEQ_3:27;
A149: ( (3 * n) + 1 <= ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j & ((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j <= (n * n) + (3 * n) ) by A13, A136, Lm14;
A150: f . (((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j) = Weight vk,v3,W by A1, Def20;
A151: ((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 A7, A26, A148, PARTFUN1:def 8
.= g . (((2 * n) + (n * (Argmin (OuterVx g,n),g,n))) + j) by A6, A147, A148, Th19
.= Weight vk,v3,W by A12, A22, A148, A149, A150, Def16 ;
per cases ( m in {(Argmin (OuterVx g,n),g,n)} or m in UsedVx g,n ) by A14, A136, XBOOLE_0:def 3;
suppose m in {(Argmin (OuterVx g,n),g,n)} ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
then A152: 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 A146, A151, Th24;
then Weight vk,v3,W = - 1 by Def7;
hence f . (((2 * n) + (n * m)) + j) = - 1 by A1, A152, Def20; :: thesis: verum
end;
suppose m in UsedVx g,n ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
hence f . (((2 * n) + (n * m)) + j) = - 1 by A3, A136, A142; :: thesis: verum
end;
end;
end;
let m be Element of NAT ; :: thesis: ( m in UsedVx h,n implies h . (n + m) <> - 1 )
assume A153: 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 A14, A153, XBOOLE_0:def 3;
suppose A154: m in UsedVx g,n ; :: thesis: h . (n + m) <> - 1
then h . (n + m) = g . (n + m) by A1, A5, Lm16;
hence h . (n + m) <> - 1 by A3, A154; :: thesis: verum
end;
suppose m in {(Argmin (OuterVx g,n),g,n)} ; :: thesis: h . (n + m) <> - 1
hence h . (n + m) <> - 1 by A13, A33, TARSKI:def 1; :: thesis: verum
end;
end;