let n, k be Element of NAT ; :: thesis: for f, g, h being Element of REAL *
for G being oriented finite Graph
for W being Function of the carrier' of G,Real>=0
for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & 1 in UsedVx (g,n) & ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) )
let f, g, h be Element of REAL * ; :: thesis: for G being oriented finite Graph
for W being Function of the carrier' of G,Real>=0
for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & 1 in UsedVx (g,n) & ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) )
let G be oriented finite Graph; :: thesis: for W being Function of the carrier' of G,Real>=0
for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & 1 in UsedVx (g,n) & ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) )
let W be Function of the carrier' of G,Real>=0; :: thesis: for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & 1 in UsedVx (g,n) & ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) )
let v1 be Vertex of G; :: thesis: ( f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & 1 in UsedVx (g,n) & ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) & ( for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ) implies ( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) ) )
set R = Relax n;
set M = findmin n;
set IN = OuterVx (g,n);
set Ug = UsedVx (g,n);
assume that
A1: f is_Input_of_Dijkstra_Alg G,n,W and
A2: v1 = 1 and
A3: n >= 1 and
A4: g = ((repeat ((Relax n) * (findmin n))) . k) . f and
A5: h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f and
A6: OuterVx (g,n) <> {} and
A7: 1 in UsedVx (g,n) ; :: thesis: ( ex v3 being Vertex of G ex j being Element of NAT st
( v3 <> v1 & v3 = j & g . (n + j) <> - 1 & ( for p being FinSequence of NAT
for P being oriented Chain of G holds
( not p is_simple_vertex_seq_at g,j,n or ex i being Element of NAT st
( 1 <= i & i < len p & not p . i in UsedVx (g,n) ) or not P is_oriented_edge_seq_of p or not P is_shortestpath_of v1,v3, UsedVx (g,n),W or not cost (P,W) = g . ((2 * n) + j) or ( not v3 in UsedVx (g,n) & not P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) ) or ex m, j being Element of NAT st
( g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) & not f . (((2 * n) + (n * m)) + j) = - 1 ) or ex m being Element of NAT st
( m in UsedVx (g,n) & not g . (n + m) <> - 1 ) or ( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) ) )
assume A8: for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ; :: thesis: ( ex m, j being Element of NAT st
( g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) & not f . (((2 * n) + (n * m)) + j) = - 1 ) or ex m being Element of NAT st
( m in UsedVx (g,n) & not g . (n + m) <> - 1 ) or ( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) ) )
assume that
A9: for m, j being Element of NAT st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 and
A10: for m being Element of NAT st m in UsedVx (g,n) holds
g . (n + m) <> - 1 ; :: thesis: ( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) & ( for m, j being Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) )
set mi = ((n * n) + (3 * n)) + 1;
set Ak = Argmin ((OuterVx (g,n)),g,n);
A11: 1 <= ((n * n) + (3 * n)) + 1 by NAT_1:12;
A12: len f = ((n * n) + (3 * n)) + 1 by A1, Def20;
A13: (findmin n) . g = (g,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (g,n)),g,n)),(- 1)) by Def11;
A14: dom ((findmin n) . g) = dom g by Th34;
h = (Relax n) . ((findmin n) . g) by A4, A5, Th23;
then A15: h = Relax (((findmin n) . g),n) by Def15;
A16: Seg n = the carrier of G by A1, Def20;
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, Th42;
A20: 1 <= Argmin ((OuterVx (g,n)),g,n) by A6, Th30;
A21: Argmin ((OuterVx (g,n)),g,n) <= n by A6, Th30;
A22: g . (n + (Argmin ((OuterVx (g,n)),g,n))) <> - 1 by A6, Th30;
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, Th40;
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, Th42;
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 Element of 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 Element of NAT st
( kk = Argmin ((OuterVx (g,n)),g,n) & kk in OuterVx (g,n) & ( for i being Element of NAT st i in OuterVx (g,n) holds
g /. ((2 * n) + kk) <= g /. ((2 * n) + i) ) & ( for i being Element of NAT st i in OuterVx (g,n) & g /. ((2 * n) + kk) = g /. ((2 * n) + i) holds
kk <= i ) ) by A6, Def10;
set nAk = (2 * n) + (Argmin ((OuterVx (g,n)),g,n));
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, Th47;
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, Th18 ;
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, Th19 ;
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, 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 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))) ) by Def13;
((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + (Argmin ((OuterVx (g,n)),g,n))) >= 0 by A50, 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:7;
hence contradiction by A6, A42, A49, A51, Th30; :: 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 Element of NAT st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) )
let v3 be Vertex of G; :: thesis: for j being Element of NAT st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( b4 is_simple_vertex_seq_at h,P,n & ( for i being Element of NAT st 1 <= b6 & b6 < len i holds
i . b6 in UsedVx (h,n) ) & b5 is_oriented_edge_seq_of b4 & b5 is_shortestpath_of v1,p, UsedVx (h,n),W & cost (b5,W) = h . ((2 * n) + P) & ( not p in UsedVx (h,n) implies b5 islongestInShortestpath UsedVx (h,n),v1,W ) )
let j be Element of NAT ; :: thesis: ( v3 <> v1 & v3 = j & h . (n + j) <> - 1 implies ex p being FinSequence of NAT ex P being oriented Chain of G st
( b3 is_simple_vertex_seq_at h,P,n & ( for i being Element of NAT st 1 <= b5 & b5 < len i holds
i . b5 in UsedVx (h,n) ) & b4 is_oriented_edge_seq_of b3 & b4 is_shortestpath_of v1,p, UsedVx (h,n),W & cost (b4,W) = h . ((2 * n) + P) & ( not p in UsedVx (h,n) implies b4 islongestInShortestpath UsedVx (h,n),v1,W ) ) )
assume that
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 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;
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, Th19;
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, Th19;
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, Th19
.= f . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A19, A38, A80, A81, A82, Def16
.= Weight (vk,v3,W) by A1, A54, Def20 ;
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 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 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 Element of 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 Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) )
take P = P; :: thesis: ( p is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) )
thus p is_simple_vertex_seq_at h,j,n by A4, A5, A6, A12, A86, A87, A88, Lm17; :: thesis: ( ( for i being Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (h,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) )
hereby :: thesis: ( P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (P,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) )
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len p implies p . i in UsedVx (h,n) )
assume that
A93: 1 <= i and
A94: i < len p ; :: thesis: p . i in UsedVx (h,n)
p . i in UsedVx (g,n) by A88, A93, A94;
hence p . i in UsedVx (h,n) by A24; :: thesis: verum
end;
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 Element of NAT : ( i in dom h & 1 <= i & i <= n & h . i = - 1 ) } by A15, A57, A58, A76;
then A95: ( j in UsedVx (g,n) or j in {(Argmin ((OuterVx (g,n)),g,n))} ) by A23, 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 that
A96: not v4 in UsedVx (g,n) and
A97: Q is_shortestpath_of v1,v4, UsedVx (g,n),W ; :: thesis: cost (P,W) <= cost (b1,W)
A98: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A99: 1 <= j4 by A16, A98, FINSEQ_1:1;
A100: j4 <= n by A16, A98, FINSEQ_1:1;
then A101: g . (n + j4) <> - 1 by A1, A2, A7, A9, A17, A96, A97, A99, 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 Element of NAT st 1 <= i & i < len q holds
q . i in UsedVx (g,n) and
R is_oriented_edge_seq_of q and
A102: R is_shortestpath_of v1,v4, UsedVx (g,n),W and
A103: cost (R,W) = g . ((2 * n) + j4) and
A104: ( not v4 in UsedVx (g,n) implies R islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A96;
A105: cost (R,W) = cost (Q,W) by A97, A102, Th9;
per cases ( j in UsedVx (g,n) or j = Argmin ((OuterVx (g,n)),g,n) ) by A95, 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, A96, A104, GRAPH_5:def 19;
hence cost (P,W) <= cost (Q,W) by A90, A105, Th9; :: thesis: verum
end;
suppose A106: j = Argmin ((OuterVx (g,n)),g,n) ; :: thesis: cost (P,W) <= cost (b1,W)
j4 <= ((n * n) + (3 * n)) + 1 by A25, A100, XXREAL_0:2;
then A107: j4 in dom g by A12, A19, A99, FINSEQ_3:25;
then g . j4 <> - 1 by A96, A99, A100;
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 A99, A100, A101, A107;
then A108: g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) <= g /. ((2 * n) + j4) by A33;
A109: g /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) = g . ((2 * n) + (Argmin ((OuterVx (g,n)),g,n))) by A37, PARTFUN1:def 6;
A110: 1 < (2 * n) + j4 by A99, A100, Lm11;
(2 * n) + j4 < ((n * n) + (3 * n)) + 1 by A99, A100, Lm11;
then (2 * n) + j4 in dom g by A12, A19, A110, FINSEQ_3:25;
hence cost (P,W) <= cost (Q,W) by A91, A103, A105, A106, A108, A109, 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 A111: ((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 A112: ((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 A113: ((findmin n) . g) /. ((2 * n) + j) <= newpathcost (((findmin n) . g),n,j) by A63, A85, A111, Def13;
A114: ((findmin n) . g) /. ((2 * n) + j) = cost (P,W) by A71, A73, A91, PARTFUN1:def 6;
consider e being set such that
A115: e in the carrier' of G and
A116: e orientedly_joins vk,v3 by A83, A112, Th24;
reconsider pe = <*e*> as oriented Chain of G by A115, Th5;
A117: len pe = 1 by FINSEQ_1:40;
A118: pe . 1 = e by FINSEQ_1:40;
then consider Q being oriented Chain of G such that
A119: Q = PK ^ pe and
Q is_orientedpath_of v1,v3 by A39, A40, A116, A117, GRAPH_5:33;
cost (pe,W) = W . (pe . 1) by A17, A117, Th4, GRAPH_5:46
.= Weight (vk,v3,W) by A115, A116, A118, Th26 ;
then cost (Q,W) = newpathcost (((findmin n) . g),n,j) by A17, A42, A43, A83, A119, 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, A113, A114, A115, A116, A119, 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, Th24;
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 A120: not v3 in UsedVx (h,n) ; :: thesis: P islongestInShortestpath UsedVx (h,n),v1,W
then A121: not v3 in UsedVx (g,n) by A23, 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 that
A122: v2 in UsedVx (h,n) and
A123: 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, A122, 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 A124: 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, A124, Th8; :: thesis: cost (PK,W) <= cost (P,W)
g . j <> - 1 by A54, A57, A58, A75, A121;
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 A55, A57, A58, A75, A86;
then A125: 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, A125, PARTFUN1:def 6; :: thesis: verum
end;
suppose A126: 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
A127: Q is_shortestpath_of v1,v2, UsedVx (g,n),W and
A128: cost (Q,W) <= cost (P,W) by A23, A92, A120, A123, GRAPH_5:def 19, XBOOLE_0:def 3;
A129: now
let R be oriented Chain of G; :: thesis: for v4 being Vertex of G st not v4 in UsedVx (g,n) & R is_shortestpath_of v1,v4, UsedVx (g,n),W holds
cost (Q,W) <= cost (R,W)
let v4 be Vertex of G; :: thesis: ( not v4 in UsedVx (g,n) & R is_shortestpath_of v1,v4, UsedVx (g,n),W implies cost (Q,W) <= cost (R,W) )
assume that
A130: not v4 in UsedVx (g,n) and
A131: R is_shortestpath_of v1,v4, UsedVx (g,n),W ; :: thesis: cost (Q,W) <= cost (R,W)
A132: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A133: 1 <= j4 by A16, A132, FINSEQ_1:1;
j4 <= n by A16, A132, FINSEQ_1:1;
then g . (n + j4) <> - 1 by A1, A2, A7, A9, A17, A130, A131, A133, 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 Element of NAT st 1 <= i & i < len rn holds
rn . i in UsedVx (g,n) and
RR is_oriented_edge_seq_of rn and
A134: RR is_shortestpath_of v1,v4, UsedVx (g,n),W and
cost (RR,W) = g . ((2 * n) + j4) and
A135: ( not v4 in UsedVx (g,n) implies RR islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A130;
consider QQ being oriented Chain of G such that
A136: QQ is_shortestpath_of v1,v2, UsedVx (g,n),W and
A137: cost (QQ,W) <= cost (RR,W) by A123, A126, A130, A135, GRAPH_5:def 19;
cost (QQ,W) = cost (Q,W) by A127, A136, Th9;
hence cost (Q,W) <= cost (R,W) by A131, A134, A137, 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, A123, A127, A129, GRAPH_5:64; :: thesis: cost (Q,W) <= cost (P,W)
thus cost (Q,W) <= cost (P,W) by A128; :: thesis: verum
end;
end;
end;
hence P islongestInShortestpath UsedVx (h,n),v1,W by GRAPH_5:def 19; :: thesis: verum
end;
end;
suppose A138: (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 A139: (Relax (((findmin n) . g),n)) . (n + j) = Argmin ((OuterVx (g,n)),g,n) by A14, A42, A60, A62, A64, Def14;
A140: ( ((findmin n) . g) . (n + j) = - 1 or ((findmin n) . g) /. ((2 * n) + j) > newpathcost (((findmin n) . g),n,j) ) by A63, A138, Def13;
A141: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) >= 0 by A63, A138, Def13;
A142: ((findmin n) . g) . j <> - 1 by A63, A138, Def13;
A143: newpathcost (((findmin n) . g),n,j) = (((findmin n) . g) /. ((2 * n) + (Argmin ((OuterVx (g,n)),g,n)))) + (Weight (vk,v3,W)) by A42, A83;
A144: now
assume A145: Argmin ((OuterVx (g,n)),g,n) = j ; :: thesis: contradiction
then A146: ((findmin n) . g) . (n + j) <> - 1 by A13, A21, A22, A61, A64, Th19;
(((findmin n) . g) /. ((2 * n) + j)) + (Weight (vk,v3,W)) >= (((findmin n) . g) /. ((2 * n) + j)) + 0 by A83, A141, XREAL_1:7;
hence contradiction by A63, A138, A143, A145, A146, Def13; :: thesis: verum
end;
A147: now
assume j in UsedVx (g,n) ; :: thesis: contradiction
then ex i being Element of NAT st
( j = i & i in dom g & 1 <= i & i <= n & g . i = - 1 ) ;
hence contradiction by A25, A142, Th33; :: thesis: verum
end;
consider e being set such that
A148: ( e in the carrier' of G & e orientedly_joins vk,v3 ) by A83, A141, Th24;
reconsider pe = <*e*> as oriented Chain of G by A148, Th5;
A149: len pe = 1 by FINSEQ_1:40;
A150: pe . 1 = e by FINSEQ_1:40;
then consider Q being oriented Chain of G such that
A151: Q = PK ^ pe and
Q is_orientedpath_of v1,v3 by A39, A40, A148, A149, GRAPH_5:33;
take q = pk ^ <*j*>; :: thesis: ex Q being oriented Chain of G st
( q is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len q holds
q . i in UsedVx (h,n) ) & Q is_oriented_edge_seq_of q & Q is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (Q,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies Q islongestInShortestpath UsedVx (h,n),v1,W ) )
take Q = Q; :: thesis: ( q is_simple_vertex_seq_at h,j,n & ( for i being Element of NAT st 1 <= i & i < len q holds
q . i in UsedVx (h,n) ) & Q is_oriented_edge_seq_of q & Q is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (Q,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies Q islongestInShortestpath UsedVx (h,n),v1,W ) )
thus q is_simple_vertex_seq_at h,j,n by A4, A5, A6, A12, A15, A27, A28, A52, A139, A144, A147, 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 ) )
A152: len pk > 1 by A27, Def18;
A153: pk is_vertex_seq_at g, Argmin ((OuterVx (g,n)),g,n),n by A27, Def18;
A154: q . (len pk) = pk . (len pk) by A152, Lm1
.= Argmin ((OuterVx (g,n)),g,n) by A153, Def17 ;
hereby :: thesis: ( Q is_oriented_edge_seq_of q & Q is_shortestpath_of v1,v3, UsedVx (h,n),W & cost (Q,W) = h . ((2 * n) + j) & ( not v3 in UsedVx (h,n) implies Q islongestInShortestpath UsedVx (h,n),v1,W ) )
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len q implies q . i in UsedVx (h,n) )
assume that
A155: 1 <= i and
A156: i < len q ; :: thesis: q . i in UsedVx (h,n)
i < (len pk) + 1 by A156, FINSEQ_2:16;
then A157: 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 A154, 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 A158: i < len pk by A157, XXREAL_0:1;
q . i = pk . i by A155, A157, Lm1;
hence ( q . i in {(Argmin ((OuterVx (g,n)),g,n))} or q . i in UsedVx (g,n) ) by A28, A155, A158; :: thesis: verum
end;
end;
end;
hence q . i in UsedVx (h,n) by A23, XBOOLE_0:def 3; :: thesis: verum
end;
A159: len Q = (len PK) + 1 by A149, A151, FINSEQ_1:22;
A160: len pk = (len PK) + 1 by A29, Def19;
then A161: len q = (len Q) + 1 by A159, FINSEQ_2:16;
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 that
A162: 1 <= i and
A163: 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 A164: i = len Q ; :: thesis: ( the Source of G . (Q . b1) = q . b1 & the Target of G . (Q . b1) = q . (b1 + 1) )
then A165: Q . i = e by A149, A150, A151, A159, Lm2;
then A166: the Target of G . (Q . i) = v3 by A148, GRAPH_4:def 1;
thus the Source of G . (Q . i) = q . i by A148, A154, A159, A160, A164, A165, 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, A159, A160, A164, A166, 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 A167: i < len Q by A163, XXREAL_0:1;
then A168: i <= len PK by A159, NAT_1:13;
then A169: the Source of G . (PK . i) = pk . i by A29, A162, Def19;
A170: the Target of G . (PK . i) = pk . (i + 1) by A29, A162, A168, Def19;
A171: Q . i = PK . i by A151, A162, A168, Lm1;
A172: i + 1 <= len pk by A159, A160, A167, NAT_1:13;
thus the Source of G . (Q . i) = q . i by A159, A160, A162, A163, A169, A171, Lm1; :: thesis: the Target of G . (Q . i) = q . (i + 1)
thus the Target of G . (Q . i) = q . (i + 1) by A170, A171, A172, Lm1, NAT_1:12; :: thesis: verum
end;
end;
end;
hence Q is_oriented_edge_seq_of q by A161, 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 ) )
A173: (cost (PK,W)) + (cost (pe,W)) = cost (Q,W) by A17, A151, GRAPH_5:46, GRAPH_5:54;
A174: cost (pe,W) = W . (pe . 1) by A17, A149, Th4, GRAPH_5:46
.= Weight (vk,v3,W) by A148, A150, Th26 ;
then A175: newpathcost (((findmin n) . g),n,j) = cost (Q,W) by A17, A42, A43, A83, A151, 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 A176: 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 A177: 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, A176, A177
.= Weight (v2,v3,W) by A1, A54, 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 A2, A7, A23, A30, A53, A148, A151, Th15; :: thesis: verum
end;
suppose A178: 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 Element of NAT st 1 <= i & i < len p holds
p . i in UsedVx (g,n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx (g,n),W & cost (P,W) = g . ((2 * n) + j) & ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) by A8, 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, A140, A148, A151, A173, A174, A178, Th19, GRAPH_5:65; :: thesis: verum
end;
end;
end;
thus cost (Q,W) = h . ((2 * n) + j) by A15, A63, A65, A66, A67, A71, A138, A175, 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 A179: (cost (PK,W)) + 0 <= cost (Q,W) by A173, XREAL_1:7;
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 that
A180: v2 in UsedVx (h,n) and
A181: 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, A180, 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 A182: 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, A182, Th8; :: thesis: cost (PK,W) <= cost (Q,W)
thus cost (PK,W) <= cost (Q,W) by A179; :: thesis: verum
end;
suppose A183: 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
A184: P is_shortestpath_of v1,v2, UsedVx (g,n),W and
A185: cost (P,W) <= cost (PK,W) by A4, A5, A6, A32, A181, Th40, GRAPH_5:def 19;
A186: now
let R be oriented Chain of G; :: thesis: for v4 being Vertex of G st not v4 in UsedVx (g,n) & R is_shortestpath_of v1,v4, UsedVx (g,n),W holds
cost (P,W) <= cost (R,W)
let v4 be Vertex of G; :: thesis: ( not v4 in UsedVx (g,n) & R is_shortestpath_of v1,v4, UsedVx (g,n),W implies cost (P,W) <= cost (R,W) )
assume that
A187: not v4 in UsedVx (g,n) and
A188: R is_shortestpath_of v1,v4, UsedVx (g,n),W ; :: thesis: cost (P,W) <= cost (R,W)
A189: v4 in VG ;
then reconsider j4 = v4 as Element of NAT ;
A190: 1 <= j4 by A16, A189, FINSEQ_1:1;
j4 <= n by A16, A189, FINSEQ_1:1;
then g . (n + j4) <> - 1 by A1, A2, A7, A9, A17, A187, A188, A190, 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 Element of NAT st 1 <= i & i < len rn holds
rn . i in UsedVx (g,n) and
RR is_oriented_edge_seq_of rn and
A191: RR is_shortestpath_of v1,v4, UsedVx (g,n),W and
cost (RR,W) = g . ((2 * n) + j4) and
A192: ( not v4 in UsedVx (g,n) implies RR islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A7, A8, A187;
consider PP being oriented Chain of G such that
A193: PP is_shortestpath_of v1,v2, UsedVx (g,n),W and
A194: cost (PP,W) <= cost (RR,W) by A181, A183, A187, A192, GRAPH_5:def 19;
cost (PP,W) = cost (P,W) by A184, A193, Th9;
hence cost (P,W) <= cost (R,W) by A188, A191, A194, 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, A181, A184, A186, GRAPH_5:64; :: thesis: cost (P,W) <= cost (Q,W)
thus cost (P,W) <= cost (Q,W) by A179, A185, 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 that
A195: h . (n + j) = - 1 and
A196: 1 <= j and
A197: j <= n and
A198: m in UsedVx (h,n) ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
set nj = n + j;
A199: 1 < n + j by A196, A197, Lm12;
A200: n + j <= 2 * n by A196, A197, Lm12;
A201: n + j < ((n * n) + (3 * n)) + 1 by A196, A197, Lm12;
then A202: n + j in dom g by A12, A19, A199, FINSEQ_3:25;
n + 1 <= n + j by A196, XREAL_1:7;
then A203: n < n + j by NAT_1:13;
A204: now
assume (findmin n) . g hasBetterPathAt n,(n + j) -' n ; :: thesis: contradiction
then h . (n + j) = Argmin ((OuterVx (g,n)),g,n) by A14, A15, A42, A200, A202, A203, Def14;
hence contradiction by A195, NAT_1:2; :: thesis: verum
end;
A205: ((findmin n) . g) . (n + j) = g . (n + j) by A13, A21, A201, A203, Th19;
then A206: g . (n + j) = - 1 by A14, A15, A195, A200, A202, A203, A204, Def14;
then A207: not j in UsedVx (g,n) by A10;
j < ((n * n) + (3 * n)) + 1 by A25, A197, XXREAL_0:2;
then j in dom g by A12, A19, A196, FINSEQ_3:25;
then g . j <> - 1 by A196, A197, A207;
then A208: ((findmin n) . g) . j <> - 1 by A13, A22, A25, A197, A206, Th19;
not (findmin n) . g hasBetterPathAt n,j by A204, NAT_D:34;
then A209: ((findmin n) . g) /. (((2 * n) + (n * (((findmin n) . g) /. (((n * n) + (3 * n)) + 1)))) + j) < 0 by A205, A206, A208, Def13;
reconsider v3 = j as Vertex of G by A16, A196, A197, FINSEQ_1:1;
set Akj = ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j;
A210: 1 < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A197, Lm13;
A211: Argmin ((OuterVx (g,n)),g,n) < ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A197, Lm13;
A212: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j < ((n * n) + (3 * n)) + 1 by A20, A21, A197, Lm13;
then A213: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j in dom g by A12, A19, A210, FINSEQ_3:25;
A214: (3 * n) + 1 <= ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j by A20, A21, A196, A197, Lm14;
A215: ((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j <= (n * n) + (3 * n) by A20, A21, A196, A197, Lm14;
A216: f . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) = Weight (vk,v3,W) by A1, Def20;
A217: ((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, A213, PARTFUN1:def 6
.= g . (((2 * n) + (n * (Argmin ((OuterVx (g,n)),g,n)))) + j) by A13, A211, A212, Th19
.= Weight (vk,v3,W) by A19, A38, A213, A214, A215, A216, Def16 ;
per cases ( m in {(Argmin ((OuterVx (g,n)),g,n))} or m in UsedVx (g,n) ) by A23, A198, XBOOLE_0:def 3;
suppose m in {(Argmin ((OuterVx (g,n)),g,n))} ; :: thesis: f . (((2 * n) + (n * b1)) + b2) = - 1
then A218: 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 A209, A217, Th24;
then Weight (vk,v3,W) = - 1 by Def7;
hence f . (((2 * n) + (n * m)) + j) = - 1 by A1, A218, 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 A9, A196, A197, A206; :: thesis: verum
end;
end;
end;
let m be Element of NAT ; :: thesis: ( m in UsedVx (h,n) implies h . (n + m) <> - 1 )
assume A219: 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, A219, XBOOLE_0:def 3;
suppose A220: 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, A220; :: 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;