let i, n be Nat; :: thesis:
let f, g be Element of REAL * ; :: thesis:
let G be oriented finite Graph; :: thesis:
let W be Function of the carrier' of G,Real>=0; :: thesis:
let v1, v2 be Vertex of G; :: thesis:
assume that
A1: f is_Input_of_Dijkstra_Alg G,n,W and
A2: v1 = 1 and
A3: 1 <> v2 and
A4: v2 = i and
A5: n >= 1 and
A6: g = (DijkstraAlgorithm n) . f ; :: thesis:
A7: Seg n = the carrier of G by A1;
then reconsider VG = the carrier of G as non empty Subset of NAT by A5;
A8: f . (n + 1) = 0 by A1;
set Ug = UsedVx (g,n);
set Vg = UnusedVx (g,n);
set R = Relax n;
set M = findmin n;
set RM = repeat ((Relax n) * (findmin n));
set cn = LifeSpan (((Relax n) * (findmin n)),f,n);
set mi = ((n * n) + (3 * n)) + 1;
A9: g = ((repeat ((Relax n) * (findmin n))) . (LifeSpan (((Relax n) * (findmin n)),f,n))) . f by A6, Def5;
A10: (UsedVx (g,n)) \/ (UnusedVx (g,n)) c= VG

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A11: x in (UsedVx (g,n)) \/ (UnusedVx (g,n)) ; :: thesis:

per cases by A11, XBOOLE_0:def 3;

suppose x in UsedVx (g,n) ; :: thesis:

then ex k being Nat st
( x = k & k in dom g & 1 <= k & k <= n & g . k = - 1 ) ;
hence x in VG by A7, FINSEQ_1:1; :: thesis:

end;

suppose x in UnusedVx (g,n) ; :: thesis:

then ex k being Nat st
( x = k & k in dom g & 1 <= k & k <= n & g . k <> - 1 ) ;
hence x in VG by A7, FINSEQ_1:1; :: thesis:

end;

A12: len f = ((n * n) + (3 * n)) + 1 by A1;
VG c= (UsedVx (g,n)) \/ (UnusedVx (g,n))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A13: x in VG ; :: thesis:
then reconsider j = x as Element of NAT ;
A14: 1 <= j by A7, A13, FINSEQ_1:1;
A15: j <= n by A7, A13, FINSEQ_1:1;
n < ((n * n) + (3 * n)) + 1 by Lm7;
then j < ((n * n) + (3 * n)) + 1 by A15, XXREAL_0:2;
then j in dom f by A12, A14, FINSEQ_3:25;
then A16: j in dom g by A9, Th41;

per cases ;

suppose g . j = - 1 ; :: thesis:

then j in { k where k is Nat : ( k in dom g & 1 <= k & k <= n & g . k = - 1 ) } by A14, A15, A16;
hence x in (UsedVx (g,n)) \/ (UnusedVx (g,n)) by XBOOLE_0:def 3; :: thesis:

end;

suppose g . j <> - 1 ; :: thesis:

then j in { k where k is Nat : ( k in dom g & 1 <= k & k <= n & g . k <> - 1 ) } by A14, A15, A16;
hence x in (UsedVx (g,n)) \/ (UnusedVx (g,n)) by XBOOLE_0:def 3; :: thesis:

end;

hence A17: the carrier of G = (UsedVx (g,n)) \/ (UnusedVx (g,n)) by A10, XBOOLE_0:def 10; :: thesis:
defpred S₁[ Nat] means ( $1 <= LifeSpan (((Relax n) * (findmin n)),f,n) implies ( ( for v3 being Vertex of G
for j being Nat st v3 <> v1 & v3 = j & (((repeat ((Relax n) * (findmin n))) . $1) . f) . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at ((repeat ((Relax n) * (findmin n))) . $1) . f,j,n & ( for m being Nat st 1 <= m & m < len p holds
p . m in UsedVx ((((repeat ((Relax n) * (findmin n))) . $1) . f),n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx ((((repeat ((Relax n) * (findmin n))) . $1) . f),n),W & cost (P,W) = (((repeat ((Relax n) * (findmin n))) . $1) . f) . ((2 * n) + j) & ( not v3 in UsedVx ((((repeat ((Relax n) * (findmin n))) . $1) . f),n) implies P islongestInShortestpath UsedVx ((((repeat ((Relax n) * (findmin n))) . $1) . f),n),v1,W ) ) ) & ( for m, j being Nat st (((repeat ((Relax n) * (findmin n))) . $1) . f) . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx ((((repeat ((Relax n) * (findmin n))) . $1) . f),n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx ((((repeat ((Relax n) * (findmin n))) . $1) . f),n) holds
(((repeat ((Relax n) * (findmin n))) . $1) . f) . (n + m) <> - 1 ) ) );
1 <= ((n * n) + (3 * n)) + 1 by NAT_1:12;
then A18: 1 in dom f by A12, FINSEQ_3:25;
A19: ( ( for m being Nat st 1 <= m & m <= n holds
f . m = 1 ) & ( for m being Nat st 2 <= m & m <= n holds
f . (n + m) = - 1 ) ) by A1;
then {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) by A5, A8, A18, Th47;
then A20: 1 in UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) by TARSKI:def 1;
A21: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A22: S₁[k] ; :: thesis:

now :: thesis:

set FK1 = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f;
set UV1 = UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n);
set FK = ((repeat ((Relax n) * (findmin n))) . k) . f;
assume A23: k + 1 <= LifeSpan (((Relax n) * (findmin n)),f,n) ; :: thesis:
then A24: k < LifeSpan (((Relax n) * (findmin n)),f,n) by NAT_1:13;
then A25: OuterVx ((((repeat ((Relax n) * (findmin n))) . k) . f),n) <> {} by Def4;

per cases ;

suppose k = 0 ; :: thesis:

hence ( ( for v3 being Vertex of G
for j being Nat st v3 <> v1 & v3 = j & (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f) . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f,j,n & ( for m being Nat st 1 <= m & m < len p holds
p . m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n),W & cost (P,W) = (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f) . ((2 * n) + j) & ( not v3 in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) implies P islongestInShortestpath UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n),v1,W ) ) ) & ( for m, j being Nat st (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f) . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) holds
(((repeat ((Relax n) * (findmin n))) . (k + 1)) . f) . (n + m) <> - 1 ) ) by A1, A2, A5, Lm15; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then k >= 1 + 0 by INT_1:7;
then 1 in UsedVx ((((repeat ((Relax n) * (findmin n))) . k) . f),n) by A20, A24, Th48;
hence ( ( for v3 being Vertex of G
for j being Nat st v3 <> v1 & v3 = j & (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f) . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f,j,n & ( for m being Nat st 1 <= m & m < len p holds
p . m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n),W & cost (P,W) = (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f) . ((2 * n) + j) & ( not v3 in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) implies P islongestInShortestpath UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n),v1,W ) ) ) & ( for m, j being Nat st (((repeat ((Relax n) * (findmin n))) . (k + 1)) . f) . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx ((((repeat ((Relax n) * (findmin n))) . (k + 1)) . f),n) holds
(((repeat ((Relax n) * (findmin n))) . (k + 1)) . f) . (n + m) <> - 1 ) ) by A1, A2, A5, A22, A23, A25, Lm20, NAT_1:13; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A26: ((repeat ((Relax n) * (findmin n))) . 0) . f = f by Th21;
A27: S₁[ 0 ]

proof

set UV = UsedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n);
set h = ((repeat ((Relax n) * (findmin n))) . 0) . f;
assume 0 <= LifeSpan (((Relax n) * (findmin n)),f,n) ; :: thesis:

hereby :: thesis:

let v3 be Vertex of G; :: thesis:
let j be Nat; :: thesis:
assume that
A28: v3 <> v1 and
A29: v3 = j and
A30: (((repeat ((Relax n) * (findmin n))) . 0) . f) . (n + j) <> - 1 ; :: thesis:
A31: v3 in VG ;
then 1 <= j by A7, A29, FINSEQ_1:1;
then 1 < j by A2, A28, A29, XXREAL_0:1;
then A32: 1 + 1 <= j by INT_1:7;
assume for p being FinSequence of NAT
for P being oriented Chain of G holds
( not p is_simple_vertex_seq_at ((repeat ((Relax n) * (findmin n))) . 0) . f,j,n or ex m being Nat st
( 1 <= m & m < len p & not p . m in UsedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n) ) or not P is_oriented_edge_seq_of p or not P is_shortestpath_of v1,v3, UsedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n),W or not cost (P,W) = (((repeat ((Relax n) * (findmin n))) . 0) . f) . ((2 * n) + j) or ( not v3 in UsedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n) & not P islongestInShortestpath UsedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n),v1,W ) ) ; :: thesis:
j <= n by A7, A29, A31, FINSEQ_1:1;
hence contradiction by A1, A26, A30, A32; :: thesis:

end;

thus for m, j being Nat st (((repeat ((Relax n) * (findmin n))) . 0) . f) . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n) holds
f . (((2 * n) + (n * m)) + j) = - 1 by A5, A26, A8, A19, A18, Th47; :: thesis:
let m be Nat; :: thesis:
assume A33: m in UsedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n) ; :: thesis:
assume (((repeat ((Relax n) * (findmin n))) . 0) . f) . (n + m) = - 1 ; :: thesis:
thus contradiction by A5, A26, A8, A19, A18, A33, Th47; :: thesis:

end;

A34: for k being Nat holds S₁[k] from NAT_1:sch 2(A27, A21);
ex ii being Nat st
( ii <= n & OuterVx ((((repeat ((Relax n) * (findmin n))) . ii) . f),n) = {} ) by Th40;
then A35: OuterVx (g,n) = {} by A9, Def4;

A36: now :: thesis:

let v3, v4 be Vertex of G; :: thesis:
assume that
A37: v3 in UsedVx (g,n) and
A38: v4 in UnusedVx (g,n) ; :: thesis:
v3 in VG ;
then reconsider m = v3 as Element of NAT ;
consider j being Nat such that
A39: v4 = j and
A40: j in dom g and
A41: ( 1 <= j & j <= n ) and
A42: g . j <> - 1 by A38;

now :: thesis:

assume g . (n + j) <> - 1 ; :: thesis:
then j in { k where k is Nat : ( k in dom g & 1 <= k & k <= n & g . k <> - 1 & g . (n + k) <> - 1 ) } by A40, A41, A42;
hence contradiction by A35; :: thesis:

end;

then - 1 = f . (((2 * n) + (n * m)) + j) by A9, A34, A37, A41
.= Weight (v3,v4,W) by A1, A39 ;
hence for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) by Th23; :: thesis:

end;

A43: f . 1 = 1 by A1, A5;

now :: thesis:

assume A44: LifeSpan (((Relax n) * (findmin n)),f,n) = 0 ; :: thesis:
1 in { k where k is Nat : ( k in dom f & 1 <= k & k <= n & f . k <> - 1 & f . (n + k) <> - 1 ) } by A5, A43, A8, A18;
hence contradiction by A9, A26, A35, A44; :: thesis:

end;

then LifeSpan (((Relax n) * (findmin n)),f,n) >= 1 + 0 by INT_1:7;
then A45: v1 in UsedVx (g,n) by A2, A9, A20, Th48;

hereby :: thesis:

assume v2 in UsedVx (g,n) ; :: thesis:
then g . (n + i) <> - 1 by A4, A9, A34;
then consider p being FinSequence of NAT , P being oriented Chain of G such that
A46: p is_simple_vertex_seq_at g,i,n and
for m being Nat st 1 <= m & m < len p holds
p . m in UsedVx (g,n) and
A47: P is_oriented_edge_seq_of p and
A48: P is_shortestpath_of v1,v2, UsedVx (g,n),W and
A49: cost (P,W) = g . ((2 * n) + i) and
( not v2 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) by A2, A3, A4, A9, A34;
take p = p; :: thesis:
take P = P; :: thesis:
thus p is_simple_vertex_seq_at g,i,n by A46; :: thesis:
thus P is_oriented_edge_seq_of p by A47; :: thesis:
thus P is_shortestpath_of v1,v2,W by A17, A36, A45, A48, Th16; :: thesis:
thus cost (P,W) = g . ((2 * n) + i) by A49; :: thesis:

end;

thus ( v2 in UnusedVx (g,n) implies for Q being oriented Chain of G holds not Q is_orientedpath_of v1,v2 ) by A17, A36, A45, Th11; :: thesis: