let k, n be 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 Nat st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being 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 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 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 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 Nat st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being 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 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 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 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 Nat st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being 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 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 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 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 Nat st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being 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 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 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 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 Nat st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) implies ( ( for v3 being Vertex of G
for j being 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 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 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 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 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 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 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 Nat st
( m in UsedVx (g,n) & not g . (n + m) <> - 1 ) or ( ( for v3 being Vertex of G
for j being 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 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 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 Nat st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) ) )
assume A8: for v3 being Vertex of G
for j being Nat st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ; :: thesis: ( ex m, j being 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 Nat st
( m in UsedVx (g,n) & not g . (n + m) <> - 1 ) or ( ( for v3 being Vertex of G
for j being 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 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 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 Nat st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) ) )
assume that
A9: for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 and
A10: for m being Nat st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ; :: thesis: ( ( for v3 being Vertex of G
for j being 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 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 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 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;
A13: (findmin n) . g = (g,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (g,n)),g,n)),(- jj)) by Def11;
A14: dom ((findmin n) . g) = dom g by Th33;
h = (Relax n) . ((findmin n) . g) by A4, A5, Th22;
then A15: h = Relax (((findmin n) . g),n) by Def15;
A16: Seg n = the carrier of G by A1;
then reconsider VG = the carrier of G as non empty Subset of NAT by A3;
A17: W is_weight>=0of G by GRAPH_5:def 13;
A18: (2 * n) + n = (2 + 1) * n ;
A19: dom f = dom g by A4, Th41;
A20: 1 <= Argmin ((OuterVx (g,n)),g,n) by A6, Th29;
A21: Argmin ((OuterVx (g,n)),g,n) <= n by A6, Th29;
A22: g . (n + (Argmin ((OuterVx (g,n)),g,n))) <> - 1 by A6, Th29;
set Uh = UsedVx (h,n);
A23: ( UsedVx (h,n) = (UsedVx (g,n)) \/ {(Argmin ((OuterVx (g,n)),g,n))} & not Argmin ((OuterVx (g,n)),g,n) in UsedVx (g,n) ) by A4, A5, A6, Th39;
then A24: UsedVx (g,n) c= UsedVx (h,n) by XBOOLE_1:7;
A25: n < ((n * n) + (3 * n)) + 1 by Lm7;
A26: dom f = dom h by A5, Th41;
reconsider vk = Argmin ((OuterVx (g,n)),g,n) as Vertex of G by A16, A20, A21, FINSEQ_1:1;
consider pk being FinSequence of NAT , PK being oriented Chain of G such that
A27: pk is_simple_vertex_seq_at g, Argmin ((OuterVx (g,n)),g,n),n and
A28: for i being Nat st 1 <= i & i < len pk holds
pk . i in UsedVx (g,n) and
A29: PK is_oriented_edge_seq_of pk and
A30: PK is_shortestpath_of v1,vk, UsedVx (g,n),W and
A31: cost (PK,W) = g . ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) and
A32: ( not vk in UsedVx (g,n) implies PK islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A22, A23;
A33: ex kk being Nat st
( kk = Argmin ((OuterVx (g,n)),g,n) & kk in OuterVx (g,n) & ( for i being Nat st i in OuterVx (g,n) holds
g /. ((2 * n) + kk) <= g /. ((2 * n) + i) ) & ( for i being Nat st i in OuterVx (g,n) & g /. ((2 * n) + kk) = g /. ((2 * n) + i) holds
kk <= i ) ) by A6, Def10;
set nAk = (2 * n) + (Argmin ((OuterVx (g,n)),g,n));
A34: 1 < (2 * n) + (Argmin ((OuterVx (g,n)),g,n)) by A20, A21, Lm11;
A35: (2 * n) + (Argmin ((OuterVx (g,n)),g,n)) < ((n * n) + (3 * n)) + 1 by A20, A21, Lm11;
A36: Argmin ((OuterVx (g,n)),g,n) < (2 * n) + (Argmin ((OuterVx (g,n)),g,n)) by A20, A21, Lm11;
A37: (2 * n) + (Argmin ((OuterVx (g,n)),g,n)) in dom g by A12, A19, A34, A35, FINSEQ_3:25;
A38: f,g equal_at (3 * n) + 1,(n * n) + (3 * n) by A4, Th46;
PK is_orientedpath_of v1,vk, UsedVx (g,n) by A30, GRAPH_5:def 18;
then A39: PK is_orientedpath_of v1,vk by GRAPH_5:def 4;
then PK <> {} by GRAPH_5:def 3;
then A40: len PK >= 1 by FINSEQ_1:20;
A41: ((n * n) + (3 * n)) + 1 in dom g by A11, A12, A19, FINSEQ_3:25;
then A42: ((findmin n) . g) /. (((n * n) + (3 * n)) + 1) = ((findmin n) . g) . (((n * n) + (3 * n)) + 1) by A14, PARTFUN1:def 6
.= Argmin ((OuterVx (g,n)),g,n) by A13, A21, A25, A41, Th17 ;
A43: ((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) = ((findmin n) . g) . ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) by A14, A37, PARTFUN1:def 6
.= cost (PK,W) by A13, A31, A35, A36, Th18 ;
set nk = n + (Argmin ((OuterVx (g,n)),g,n));
A44: 1 < n + (Argmin ((OuterVx (g,n)),g,n)) by A20, A21, Lm12;
A45: n + (Argmin ((OuterVx (g,n)),g,n)) <= 2 * n by A20, A21, Lm12;
A46: n + (Argmin ((OuterVx (g,n)),g,n)) < ((n * n) + (3 * n)) + 1 by A20, A21, Lm12;
n + 1 <= n + (Argmin ((OuterVx (g,n)),g,n)) by A20, XREAL_1:7;
then A47: n < n + (Argmin ((OuterVx (g,n)),g,n)) by NAT_1:13;
A48: n + (Argmin ((OuterVx (g,n)),g,n)) in dom g by A12, A19, A44, A46, FINSEQ_3:25;
A49: ((findmin n) . g) . (n + (Argmin ((OuterVx (g,n)),g,n))) = g . (n + (Argmin ((OuterVx (g,n)),g,n))) by A46, A47, Th31;
now :: thesis: not (findmin n) . g hasBetterPathAt n, Argmin ((OuterVx (g,n)),g,n)
set Wke = ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin ((OuterVx (g,n)),g,n)));
assume A50: (findmin n) . g hasBetterPathAt n, Argmin ((OuterVx (g,n)),g,n) ; :: thesis: contradiction
then A51: ( ((findmin n) . g) . (n + (Argmin ((OuterVx (g,n)),g,n))) = - 1 or ((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) > newpathcost (((findmin n) . g),n,(Argmin ((OuterVx (g,n)),g,n))) ) ;
((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin ((OuterVx (g,n)),g,n))) >= 0 by A50;
then (((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n)))) + (((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin ((OuterVx (g,n)),g,n)))) >= (((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n)))) + 0 by XREAL_1:7;
hence contradiction by A6, A42, A49, A51, Th29; :: thesis: verum
end;
then not (findmin n) . g hasBetterPathAt n,(n + (Argmin ((OuterVx (g,n)),g,n))) -' n by NAT_D:34;
then A52: h . (n + (Argmin ((OuterVx (g,n)),g,n))) = g . (n + (Argmin ((OuterVx (g,n)),g,n))) by A14, A15, A45, A47, A48, A49, Def14;
hereby :: thesis: ( ( for m, j being 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 Nat st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) )
let v3 be Vertex of G; :: thesis: for j being 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 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 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 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
A53: v3 <> v1 and
A54: v3 = j and
A55: 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 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;
A56: j in VG by A54;
then A57: 1 <= j by A16, FINSEQ_1:1;
A58: j <= n by A16, A56, FINSEQ_1:1;
then A59: 1 < n + j by A57, Lm12;
A60: n + j <= 2 * n by A57, A58, Lm12;
A61: n + j < ((n * n) + (3 * n)) + 1 by A57, A58, Lm12;
then A62: n + j in dom g by A12, A19, A59, FINSEQ_3:25;
A63: (n + j) -' n = j by NAT_D:34;
n + 1 <= n + j by A57, XREAL_1:7;
then A64: n < n + j by NAT_1:13;
set m2 = (2 * n) + j;
A65: (2 * n) + j <= 3 * n by A18, A58, XREAL_1:7;
(2 * n) + 1 <= (2 * n) + j by A57, XREAL_1:7;
then A66: 2 * n < (2 * n) + j by NAT_1:13;
A67: ((2 * n) + j) -' (2 * n) = j by NAT_D:34;
A68: 1 < (2 * n) + j by A57, A58, Lm11;
A69: (2 * n) + j < ((n * n) + (3 * n)) + 1 by A57, A58, Lm11;
then A70: (2 * n) + j in dom g by A12, A19, A68, FINSEQ_3:25;
A71: (2 * n) + j in dom ((findmin n) . g) by A12, A14, A19, A68, A69, FINSEQ_3:25;
A72: ((findmin n) . g) . (n + j) = g . (n + j) by A13, A21, A61, A64, Th18;
n <= 2 * n by Lm6;
then n < (2 * n) + j by A66, XXREAL_0:2;
then A73: ((findmin n) . g) . ((2 * n) + j) = g . ((2 * n) + j) by A13, A21, A69, Th18;
A74: j < ((n * n) + (3 * n)) + 1 by A25, A58, XXREAL_0:2;
then A75: j in dom g by A12, A19, A57, FINSEQ_3:25;
A76: j in dom h by A12, A26, A57, A74, FINSEQ_3:25;
set Akj = ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j;
A77: 1 < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A58, Lm13;
A78: Argmin ((OuterVx (g,n)),g,n) < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A58, Lm13;
A79: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j < ((n * n) + (3 * n)) + 1 by A20, A21, A58, Lm13;
then A80: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j in dom g by A12, A19, A77, FINSEQ_3:25;
A81: (3 * n) + 1 <= ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A57, A58, Lm14;
A82: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j <= (n * n) + (3 * n) by A20, A21, A57, A58, Lm14;
A83: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) = ((findmin n) . g) . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A14, A42, A80, PARTFUN1:def 6
.= g . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A13, A78, A79, Th18
.= f . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A38, A80, A81, A82
.= Weight (vk,v3,W) by A1, A54 ;
A84: ((findmin n) . g) /. ((2 * n) + j) = g . ((2 * n) + j) by A14, A70, A73, PARTFUN1:def 6;
per cases ( not (findmin n) . g hasBetterPathAt n,(n + j) -' n or (findmin n) . g hasBetterPathAt n,(n + j) -' n ) ;
suppose A85: not (findmin n) . g hasBetterPathAt n,(n + j) -' n ; :: thesis: 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 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 A86: h . (n + j) = g . (n + j) by A14, A15, A60, A62, A64, A72, Def14;
then consider p being FinSequence of NAT , P being oriented Chain of G such that
A87: p is_simple_vertex_seq_at g,j,n and
A88: for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) and
A89: P is_oriented_edge_seq_of p and
A90: P is_shortestpath_of v1,v3, UsedVx (g,n),W and
A91: cost (P,W) = g . ((2 * n) + j) and
A92: ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) by A8, A53, A54, A55;
take p = p; :: thesis: ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being 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 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, A86, A87, A88, Lm17; :: thesis: ( ( for i being 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 for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (h,n) by A24, A88; :: 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 ) )
thus P is_oriented_edge_seq_of p by A89; :: 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 A14, A58, A75, Def14;
then j in { i where i is Nat : ( i in dom h & 1 <= i & i <= n & h . i = - 1 ) } by A15, A57, A58, A76;
then A93: ( j in UsedVx (g,n) or j in {(Argmin ((OuterVx (g,n)),g,n))} ) by A23, XBOOLE_0:def 3;
now :: thesis: for Q being oriented Chain of G
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 (Q,W)
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
A94: not v4 in UsedVx (g,n) and
A95: Q is_shortestpath_of v1,v4, UsedVx (g,n),W ; :: thesis: cost (P,W) <= cost (b1,W)
A96: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A97: 1 <= j4 by A16, A96, FINSEQ_1:1;
A98: j4 <= n by A16, A96, FINSEQ_1:1;
then A99: g . (n + j4) <> - 1 by A1, A2, A7, A9, A17, A94, A95, A97, Lm19;
then consider q being FinSequence of NAT , R being oriented Chain of G such that
q is_simple_vertex_seq_at g,j4,n and
for i being Nat st 1 <= i & i < len q holds
q . i in UsedVx (g,n) and
R is_oriented_edge_seq_of q and
A100: R is_shortestpath_of v1,v4, UsedVx (g,n),W and
A101: cost (R,W) = g . ((2 * n) + j4) and
A102: ( not v4 in UsedVx (g,n) implies R islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A94;
A103: cost (R,W) = cost (Q,W) by A95, A100, Th9;
per cases ( j in UsedVx (g,n) or j = Argmin ((OuterVx (g,n)),g,n) ) by A93, TARSKI:def 1;
suppose j in UsedVx (g,n) ; :: thesis: cost (P,W) <= cost (b1,W)
then ex PP being oriented Chain of G st
( PP is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (PP,W) <= cost (R,W) ) by A53, A54, A94, A102, GRAPH_5:def 19;
hence cost (P,W) <= cost (Q,W) by A90, A103, Th9; :: thesis: verum
end;
suppose A104: j = Argmin ((OuterVx (g,n)),g,n) ; :: thesis: cost (P,W) <= cost (b1,W)
j4 <= ((n * n) + (3 * n)) + 1 by A25, A98, XXREAL_0:2;
then A105: j4 in dom g by A12, A19, A97, FINSEQ_3:25;
then g . j4 <> - 1 by A94, A97, A98;
then j4 in { i where i is Nat : ( i in dom g & 1 <= i & i <= n & g . i <> - 1 & g . (n + i) <> - 1 ) } by A97, A98, A99, A105;
then A106: g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) <= g /. ((2 * n) + j4) by A33;
A107: g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) = g . ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) by A37, PARTFUN1:def 6;
A108: 1 < (2 * n) + j4 by A97, A98, Lm11;
(2 * n) + j4 < ((n * n) + (3 * n)) + 1 by A97, A98, Lm11;
then (2 * n) + j4 in dom g by A12, A19, A108, FINSEQ_3:25;
hence cost (P,W) <= cost (Q,W) by A91, A101, A103, A104, A106, A107, PARTFUN1:def 6; :: thesis: verum
end;
end;
end;
hence P is_shortestpath_of v1,v3, UsedVx (h,n),W by A17, A24, A53, A90, GRAPH_5:64; :: thesis: verum
end;
suppose A109: ((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 A110: ((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 A111: ((findmin n) . g) /. ((2 * n) + j) <= newpathcost (((findmin n) . g),n,j) by A63, A85, A109;
A112: ((findmin n) . g) /. ((2 * n) + j) = cost (P,W) by A71, A73, A91, PARTFUN1:def 6;
consider e being set such that
A113: e in the carrier' of G and
A114: e orientedly_joins vk,v3 by A83, A110, Th23;
reconsider pe = <*e*> as oriented Chain of G by A113, Th5;
A115: len pe = 1 by FINSEQ_1:40;
A116: pe . 1 = e by FINSEQ_1:40;
then consider Q being oriented Chain of G such that
A117: Q = PK ^ pe and
Q is_orientedpath_of v1,v3 by A39, A40, A114, A115, GRAPH_5:33;
cost (pe,W) = W . (pe . 1) by A17, A115, Th4, GRAPH_5:46
.= Weight (vk,v3,W) by A113, A114, A116, Th25 ;
then cost (Q,W) = newpathcost (((findmin n) . g),n,j) by A17, A42, A43, A83, A117, GRAPH_5:46, GRAPH_5:54;
hence P is_shortestpath_of v1,v3, UsedVx (h,n),W by A2, A7, A17, A23, A30, A32, A40, A53, A90, A111, A112, A113, A114, A117, GRAPH_5:65; :: thesis: 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 A83, Th23;
hence P is_shortestpath_of v1,v3, UsedVx (h,n),W by A2, A7, A17, A23, A30, A32, A53, A90, Th13; :: thesis: verum
end;
end;
end;
end;
end;
end;
thus cost (P,W) = h . ((2 * n) + j) by A15, A63, A65, A66, A67, A71, A73, A85, A91, Def14; :: thesis: ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W )
hereby :: thesis: verum
assume A118: not v3 in UsedVx (h,n) ; :: thesis: P islongestInShortestpath UsedVx (h,n),v1,W
then A119: not v3 in UsedVx (g,n) by A23, XBOOLE_0:def 3;
now :: thesis: for v2 being Vertex of G st v2 in UsedVx (h,n) & v2 <> v1 holds
ex PK being oriented Chain of G st
( PK is_shortestpath_of v1,v2, UsedVx (h,n),W & cost (PK,W) <= cost (P,W) )
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
A120: v2 in UsedVx (h,n) and
A121: 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 A23, A120, 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 A122: 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 A23, A30, A122, Th8; :: thesis: cost (PK,W) <= cost (P,W)
g . j <> - 1 by A54, A57, A58, A75, A119;
then j in { i where i is Nat : ( i in dom g & 1 <= i & i <= n & g . i <> - 1 & g . (n + i) <> - 1 ) } by A55, A57, A58, A75, A86;
then A123: g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) <= g /. ((2 * n) + j) by A33;
g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) = cost (PK,W) by A31, A37, PARTFUN1:def 6;
hence cost (PK,W) <= cost (P,W) by A70, A91, A123, PARTFUN1:def 6; :: thesis: verum
end;
suppose A124: 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
A125: Q is_shortestpath_of v1,v2, UsedVx (g,n),W and
A126: cost (Q,W) <= cost (P,W) by A23, A92, A118, A121, GRAPH_5:def 19, XBOOLE_0:def 3;
A127: now :: thesis: for R being oriented Chain of G
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 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
A128: not v4 in UsedVx (g,n) and
A129: R is_shortestpath_of v1,v4, UsedVx (g,n),W ; :: thesis: cost (Q,W) <= cost (R,W)
A130: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A131: 1 <= j4 by A16, A130, FINSEQ_1:1;
j4 <= n by A16, A130, FINSEQ_1:1;
then g . (n + j4) <> - 1 by A1, A2, A7, A9, A17, A128, A129, A131, Lm19;
then consider rn being FinSequence of NAT , RR being oriented Chain of G such that
rn is_simple_vertex_seq_at g,j4,n and
for i being Nat st 1 <= i & i < len rn holds
rn . i in UsedVx (g,n) and
RR is_oriented_edge_seq_of rn and
A132: RR is_shortestpath_of v1,v4, UsedVx (g,n),W and
cost (RR,W) = g . ((2 * n) + j4) and
A133: ( not v4 in UsedVx (g,n) implies RR islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A128;
consider QQ being oriented Chain of G such that
A134: QQ is_shortestpath_of v1,v2, UsedVx (g,n),W and
A135: cost (QQ,W) <= cost (RR,W) by A121, A124, A128, A133, GRAPH_5:def 19;
cost (QQ,W) = cost (Q,W) by A125, A134, Th9;
hence cost (Q,W) <= cost (R,W) by A129, A132, A135, Th9; :: thesis: 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 A17, A24, A121, A125, A127, GRAPH_5:64; :: thesis: cost (Q,W) <= cost (P,W)
thus cost (Q,W) <= cost (P,W) by A126; :: thesis: verum
end;
end;
end;
hence P islongestInShortestpath UsedVx (h,n),v1,W by GRAPH_5:def 19; :: thesis: verum
end;
end;
suppose A136: (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 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 A137: (Relax (((findmin n) . g),n)) . (n + j) = Argmin ((OuterVx (g,n)),g,n) by A14, A42, A60, A62, A64, Def14;
A138: ( ((findmin n) . g) . (n + j) = - 1 or ((findmin n) . g) /. ((2 * n) + j) > newpathcost (((findmin n) . g),n,j) ) by A63, A136;
A139: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 by A63, A136;
A140: ((findmin n) . g) . j <> - 1 by A63, A136;
A141: newpathcost (((findmin n) . g),n,j) = (((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n)))) + (Weight (vk,v3,W)) by A42, A83;
A142: now :: thesis: not Argmin ((OuterVx (g,n)),g,n) = j
assume A143: Argmin ((OuterVx (g,n)),g,n) = j ; :: thesis: contradiction
then A144: ((findmin n) . g) . (n + j) <> - 1 by A13, A21, A22, A61, A64, Th18;
(((findmin n) . g) /. ((2 * n) + j)) + (Weight (vk,v3,W)) >= (((findmin n) . g) /. ((2 * n) + j)) + 0 by A83, A139, XREAL_1:7;
hence contradiction by A63, A136, A141, A143, A144; :: thesis: verum
end;
A145: now :: thesis: not j in UsedVx (g,n)
assume j in UsedVx (g,n) ; :: thesis: contradiction
then ex i being Nat st
( j = i & i in dom g & 1 <= i & i <= n & g . i = - 1 ) ;
hence contradiction by A25, A140, Th32; :: thesis: verum
end;
consider e being set such that
A146: ( e in the carrier' of G & e orientedly_joins vk,v3 ) by A83, A139, Th23;
reconsider pe = <*e*> as oriented Chain of G by A146, Th5;
A147: len pe = 1 by FINSEQ_1:40;
A148: pe . 1 = e by FINSEQ_1:40;
then consider Q being oriented Chain of G such that
A149: Q = PK ^ pe and
Q is_orientedpath_of v1,v3 by A39, A40, A146, A147, GRAPH_5:33;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
reconsider q = pk ^ <*jj*> as FinSequence of NAT ;
take q = q; :: thesis: ex Q being oriented Chain of G st
( q is_simple_vertex_seq_at h,j,n & ( for i being 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 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, A15, A27, A28, A52, A137, A142, A145, Lm18; :: thesis: ( ( for i being 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 ) )
A150: len pk > 1 by A27;
A151: pk is_vertex_seq_at g, Argmin ((OuterVx (g,n)),g,n),n by A27;
A152: q . (len pk) = pk . (len pk) by A150, Lm1
.= Argmin ((OuterVx (g,n)),g,n) by A151 ;
hereby :: thesis: ( 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 Nat; :: thesis: ( 1 <= i & i < len q implies q . i in UsedVx (h,n) )
assume that
A153: 1 <= i and
A154: i < len q ; :: thesis: q . i in UsedVx (h,n)
i < (len pk) + 1 by A154, FINSEQ_2:16;
then A155: i <= len pk by NAT_1:13;
now :: thesis: ( q . i in {(Argmin ((OuterVx (g,n)),g,n))} or q . i in UsedVx (g,n) )
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 A152, 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 A156: i < len pk by A155, XXREAL_0:1;
q . i = pk . i by A153, A155, Lm1;
hence ( q . i in {(Argmin ((OuterVx (g,n)),g,n))} or q . i in UsedVx (g,n) ) by A28, A153, A156; :: thesis: verum
end;
end;
end;
hence q . i in UsedVx (h,n) by A23, XBOOLE_0:def 3; :: thesis: verum
end;
A157: len Q = (len PK) + 1 by A147, A149, FINSEQ_1:22;
A158: len pk = (len PK) + 1 by A29;
then A159: len q = (len Q) + 1 by A157, FINSEQ_2:16;
set FS = the Source of G;
set FT = the Target of G;
now :: thesis: for i being Nat st 1 <= i & i <= len Q holds
( the Source of G . (Q . i) = q . i & the Target of G . (Q . i) = q . (i + 1) )
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
A160: 1 <= i and
A161: 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 A162: i = len Q ; :: thesis: ( the Source of G . (Q . b1) = q . b1 & the Target of G . (Q . b1) = q . (b1 + 1) )
then A163: Q . i = e by A147, A148, A149, A157, Lm2;
then A164: the Target of G . (Q . i) = v3 by A146, GRAPH_4:def 1;
thus the Source of G . (Q . i) = q . i by A146, A152, A157, A158, A162, A163, GRAPH_4:def 1; :: thesis: the Target of G . (Q . i) = q . (i + 1)
thus the Target of G . (Q . i) = q . (i + 1) by A54, A157, A158, A162, A164, FINSEQ_1:42; :: 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 A165: i < len Q by A161, XXREAL_0:1;
then A166: i <= len PK by A157, NAT_1:13;
then A167: the Source of G . (PK . i) = pk . i by A29, A160;
A168: the Target of G . (PK . i) = pk . (i + 1) by A29, A160, A166;
A169: Q . i = PK . i by A149, A160, A166, Lm1;
A170: i + 1 <= len pk by A157, A158, A165, NAT_1:13;
thus the Source of G . (Q . i) = q . i by A157, A158, A160, A161, A167, A169, Lm1; :: thesis: the Target of G . (Q . i) = q . (i + 1)
thus the Target of G . (Q . i) = q . (i + 1) by A168, A169, A170, Lm1, NAT_1:12; :: thesis: verum
end;
end;
end;
hence Q is_oriented_edge_seq_of q by A159; :: 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 ) )
A171: (cost (PK,W)) + (cost (pe,W)) = cost (Q,W) by A17, A149, GRAPH_5:46, GRAPH_5:54;
A172: cost (pe,W) = W . (pe . 1) by A17, A147, Th4, GRAPH_5:46
.= Weight (vk,v3,W) by A146, A148, Th25 ;
then A173: newpathcost (((findmin n) . g),n,j) = cost (Q,W) by A17, A42, A43, A83, A149, GRAPH_5:46, GRAPH_5:54;
hereby :: thesis: ( 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 A174: g . (n + j) = - 1 ; :: thesis: Q is_shortestpath_of v1,v3, UsedVx (h,n),W
now :: thesis: for v2 being Vertex of G st v2 in UsedVx (g,n) holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 )
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 A175: 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 A9, A57, A58, A174, A175
.= Weight (v2,v3,W) by A1, A54 ;
hence for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) by Th23; :: thesis: verum
end;
hence Q is_shortestpath_of v1,v3, UsedVx (h,n),W by A2, A7, A23, A30, A53, A146, A149, Th15; :: thesis: verum
end;
suppose A176: g . (n + j) <> - 1 ; :: thesis: Q is_shortestpath_of v1,v3, UsedVx (h,n),W
then ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) by A8, A53, A54;
hence Q is_shortestpath_of v1,v3, UsedVx (h,n),W by A2, A7, A13, A17, A21, A23, A30, A32, A40, A42, A43, A53, A61, A64, A83, A84, A138, A146, A149, A171, A172, A176, Th18, GRAPH_5:65; :: thesis: verum
end;
end;
end;
thus cost (Q,W) = h . ((2 * n) + j) by A15, A63, A65, A66, A67, A71, A136, A173, Def14; :: thesis: ( not v3 in UsedVx (h,n) implies Q islongestInShortestpath UsedVx (h,n),v1,W )
0 <= cost (pe,W) by A17, GRAPH_5:50;
then A177: (cost (PK,W)) + 0 <= cost (Q,W) by A171, XREAL_1:7;
hereby :: thesis: verum
assume not v3 in UsedVx (h,n) ; :: thesis: Q islongestInShortestpath UsedVx (h,n),v1,W
now :: thesis: for v2 being Vertex of G st v2 in UsedVx (h,n) & v2 <> v1 holds
ex PK being oriented Chain of G st
( PK is_shortestpath_of v1,v2, UsedVx (h,n),W & cost (PK,W) <= cost (Q,W) )
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
A178: v2 in UsedVx (h,n) and
A179: 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 A23, A178, 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 A180: 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 A23, A30, A180, Th8; :: thesis: cost (PK,W) <= cost (Q,W)
thus cost (PK,W) <= cost (Q,W) by A177; :: thesis: verum
end;
suppose A181: 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
A182: P is_shortestpath_of v1,v2, UsedVx (g,n),W and
A183: cost (P,W) <= cost (PK,W) by A4, A5, A6, A32, A179, Th39, GRAPH_5:def 19;
A184: now :: thesis: for R being oriented Chain of G
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 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
A185: not v4 in UsedVx (g,n) and
A186: R is_shortestpath_of v1,v4, UsedVx (g,n),W ; :: thesis: cost (P,W) <= cost (R,W)
A187: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A188: 1 <= j4 by A16, A187, FINSEQ_1:1;
j4 <= n by A16, A187, FINSEQ_1:1;
then g . (n + j4) <> - 1 by A1, A2, A7, A9, A17, A185, A186, A188, Lm19;
then consider rn being FinSequence of NAT , RR being oriented Chain of G such that
rn is_simple_vertex_seq_at g,j4,n and
for i being Nat st 1 <= i & i < len rn holds
rn . i in UsedVx (g,n) and
RR is_oriented_edge_seq_of rn and
A189: RR is_shortestpath_of v1,v4, UsedVx (g,n),W and
cost (RR,W) = g . ((2 * n) + j4) and
A190: ( not v4 in UsedVx (g,n) implies RR islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A185;
consider PP being oriented Chain of G such that
A191: PP is_shortestpath_of v1,v2, UsedVx (g,n),W and
A192: cost (PP,W) <= cost (RR,W) by A179, A181, A185, A190, GRAPH_5:def 19;
cost (PP,W) = cost (P,W) by A182, A191, Th9;
hence cost (P,W) <= cost (R,W) by A186, A189, A192, Th9; :: thesis: 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 A17, A24, A179, A182, A184, GRAPH_5:64; :: thesis: cost (P,W) <= cost (Q,W)
thus cost (P,W) <= cost (Q,W) by A177, A183, 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 Nat st m in UsedVx (h,n) holds
h . (n + m) <> - 1
let m, j be 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
A193: h . (n + j) = - 1 and
A194: 1 <= j and
A195: j <= n and
A196: m in UsedVx (h,n) ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
set nj = n + j;
A197: 1 < n + j by A194, A195, Lm12;
A198: n + j <= 2 * n by A194, A195, Lm12;
A199: n + j < ((n * n) + (3 * n)) + 1 by A194, A195, Lm12;
then A200: n + j in dom g by A12, A19, A197, FINSEQ_3:25;
n + 1 <= n + j by A194, XREAL_1:7;
then A201: n < n + j by NAT_1:13;
A202: not (findmin n) . g hasBetterPathAt n,(n + j) -' n by A193, A14, A15, A42, A198, A200, A201, Def14;
A203: ((findmin n) . g) . (n + j) = g . (n + j) by A13, A21, A199, A201, Th18;
then A204: g . (n + j) = - 1 by A14, A15, A193, A198, A200, A201, A202, Def14;
then A205: not j in UsedVx (g,n) by A10;
j < ((n * n) + (3 * n)) + 1 by A25, A195, XXREAL_0:2;
then j in dom g by A12, A19, A194, FINSEQ_3:25;
then g . j <> - 1 by A194, A195, A205;
then A206: ((findmin n) . g) . j <> - 1 by A13, A22, A25, A195, A204, Th18;
not (findmin n) . g hasBetterPathAt n,j by A202, NAT_D:34;
then A207: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) < 0 by A203, A204, A206;
reconsider v3 = j as Vertex of G by A16, A194, A195, FINSEQ_1:1;
set Akj = ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j;
A208: 1 < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A195, Lm13;
A209: Argmin ((OuterVx (g,n)),g,n) < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A195, Lm13;
A210: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j < ((n * n) + (3 * n)) + 1 by A20, A21, A195, Lm13;
then A211: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j in dom g by A12, A19, A208, FINSEQ_3:25;
A212: (3 * n) + 1 <= ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A194, A195, Lm14;
A213: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j <= (n * n) + (3 * n) by A20, A21, A194, A195, Lm14;
A214: f . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) = Weight (vk,v3,W) by A1;
A215: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) = ((findmin n) . g) . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A14, A42, A211, PARTFUN1:def 6
.= g . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A13, A209, A210, Th18
.= Weight (vk,v3,W) by A38, A211, A212, A213, A214 ;
per cases ( m in {(Argmin ((OuterVx (g,n)),g,n))} or m in UsedVx (g,n) ) by A23, A196, XBOOLE_0:def 3;
suppose m in {(Argmin ((OuterVx (g,n)),g,n))} ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
then A216: m = Argmin ((OuterVx (g,n)),g,n) by TARSKI:def 1;
for e being set holds
( not e in the carrier' of G or not e orientedly_joins vk,v3 ) by A207, A215, Th23;
then Weight (vk,v3,W) = - 1 by Def7;
hence f . (((2 * n) + (n * m)) + j) = - 1 by A1, A216; :: thesis: 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 A9, A194, A195, A204; :: thesis: verum
end;
end;
end;
let m be Nat; :: thesis: ( m in UsedVx (h,n) implies h . (n + m) <> - 1 )
assume A217: 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 A23, A217, XBOOLE_0:def 3;
suppose A218: m in UsedVx (g,n) ; :: thesis: h . (n + m) <> - 1
then h . (n + m) = g . (n + m) by A4, A5, A6, A12, Lm16;
hence h . (n + m) <> - 1 by A10, A218; :: thesis: verum
end;
suppose m in {(Argmin ((OuterVx (g,n)),g,n))} ; :: thesis: h . (n + m) <> - 1
hence h . (n + m) <> - 1 by A22, A52, TARSKI:def 1; :: thesis: verum
end;
end;