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