:: Dijkstra's Shortest Path Algorithm
:: by Jing-Chao Chen
::
:: Received March 17, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem Th1: :: GRAPHSP:1
for p being FinSequence
for x being set holds
( ( not x in rng p &amp; p is one-to-one ) iff p ^ <*x*> is one-to-one )
proofend;

theorem Th2: :: GRAPHSP:2
for X being set
for p being FinSequence of X
for ii being Integer st 1 <= ii &amp; ii <= len p holds
p . ii in X
proofend;

theorem Th3: :: GRAPHSP:3
for X being set
for p being FinSequence of X
for ii being Integer st 1 <= ii &amp; ii <= len p holds
p /. ii = p . ii
proofend;

theorem Th4: :: GRAPHSP:4
for G being Graph
for pe being FinSequence of the carrier' of G
for W being Function st W is_weight_of G &amp; len pe = 1 holds
cost (pe,W) = W . (pe . 1)
proofend;

theorem Th5: :: GRAPHSP:5
for G being Graph
for e being set st e in the carrier' of G holds
<*e*> is oriented Simple Chain of G
proofend;

Lm1:  for n being Nat
for p, q being FinSequence st 1 <= n &amp; n <= len p holds
p . n = (p ^ q) . n
proofend;

Lm2:  for n being Element of NAT
for p, q being FinSequence st 1 <= n &amp; n <= len q holds
q . n = (p ^ q) . ((len p) + n)
proofend;

theorem Th6: :: GRAPHSP:6
for G being Graph
for pe, qe being FinSequence of the carrier' of G
for p being oriented Simple Chain of G st p = pe ^ qe &amp; len pe >= 1 &amp; len qe >= 1 holds
( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) &amp; the Source of G . (p . 1) <> the Source of G . (qe . 1) )
proofend;

begin

theorem Th7: :: GRAPHSP:7
for G being Graph
for p being oriented Chain of G
for V being set
for v1, v2 being Vertex of G holds
( p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2} )
proofend;

theorem Th8: :: GRAPHSP:8
for G being Graph
for p being oriented Chain of G
for W being Function
for V being set
for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
proofend;

theorem Th9: :: GRAPHSP:9
for G being Graph
for p, q being oriented Chain of G
for W being Function
for V being set
for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W &amp; q is_shortestpath_of v1,v2,V,W holds
cost (p,W) = cost (q,W)
proofend;

theorem Th10: :: GRAPHSP:10
for G being oriented Graph
for v1, v2 being Vertex of G
for e1, e2 being set st e1 in the carrier' of G &amp; e2 in the carrier' of G &amp; e1 orientedly_joins v1,v2 &amp; e2 orientedly_joins v1,v2 holds
e1 = e2
proofend;

Lm3:  for i being Element of NAT
for G being Graph
for pe being FinSequence of the carrier' of G st 1 <= i &amp; i <= len pe holds
( the Source of G . (pe . i) in the carrier of G &amp; the Target of G . (pe . i) in the carrier of G )
proofend;

theorem Th11: :: GRAPHSP:11
for G being Graph
for U, V being set
for v1, v2 being Vertex of G st the carrier of G = U \/ V &amp; v1 in U &amp; v2 in V &amp; ( for v3, v4 being Vertex of G st v3 in U &amp; v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds
for p being oriented Chain of G holds not p is_orientedpath_of v1,v2
proofend;

Lm4:  for i being Element of NAT
for G being Graph
for pe being FinSequence of the carrier' of G
for v1 being Vertex of G st 1 <= i &amp; i <= len pe &amp; ( v1 = the Source of G . (pe . i) or v1 = the Target of G . (pe . i) ) holds
v1 in vertices pe
proofend;

theorem Th12: :: GRAPHSP:12
for G being Graph
for p being oriented Chain of G
for U, V being set
for v1, v2 being Vertex of G st the carrier of G = U \/ V &amp; v1 in U &amp; ( for v3, v4 being Vertex of G st v3 in U &amp; v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) &amp; p is_orientedpath_of v1,v2 holds
p is_orientedpath_of v1,v2,U
proofend;

begin

theorem Th13: :: GRAPHSP:13
for W being Function
for V being set
for G being finite Graph
for P, Q being oriented Chain of G
for v1, v2, v3 being Vertex of G st W is_weight>=0of G &amp; P is_shortestpath_of v1,v2,V,W &amp; v1 <> v2 &amp; v1 <> v3 &amp; Q is_shortestpath_of v1,v3,V,W &amp; ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) &amp; P islongestInShortestpath V,v1,W holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
proofend;

theorem Th14: :: GRAPHSP:14
for e being set
for G being oriented finite Graph
for P being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v1, v2 being Vertex of G st e in the carrier' of G &amp; P = <*e*> &amp; e orientedly_joins v1,v2 holds
P is_shortestpath_of v1,v2,{v1},W
proofend;

theorem Th15: :: GRAPHSP:15
for e, V being set
for G being oriented finite Graph
for P, Q being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v1, v2, v3 being Vertex of G st e in the carrier' of G &amp; P is_shortestpath_of v1,v2,V,W &amp; v1 <> v3 &amp; Q = P ^ <*e*> &amp; e orientedly_joins v2,v3 &amp; v1 in V &amp; ( for v4 being Vertex of G st v4 in V holds
for ee being set holds
( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
proofend;

theorem Th16: :: GRAPHSP:16
for U, V being set
for G being oriented finite Graph
for P being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v1, v2 being Vertex of G st the carrier of G = U \/ V &amp; v1 in U &amp; ( for v3, v4 being Vertex of G st v3 in U &amp; v4 in V holds
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds
( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )
proofend;

begin

notation
let f be Function;
let i, x be set ;
synonym (f,i) := x for f +* (i,x);
end;

definition
let f be FinSequence of REAL ;
let x be set ;
let r be Real;
:: original::=
redefine func(f,x) := r ->  FinSequence of REAL ;
coherence
 (f,x) := r is FinSequence of REAL
proofend;
end;

definition
let i, k be Element of NAT ;
let f be FinSequence of REAL ;
let r be Real;
func(f,i) := (k,r) ->  FinSequence of REAL  equals :: GRAPHSP:def 1
(((f,i) := k),k) := r;
coherence
 (((f,i) := k),k) := r is FinSequence of REAL ;
end;

:: deftheorem  defines := GRAPHSP:def_1_:_
 for i, k being Element of NAT
for f being FinSequence of REAL
for r being Real holds (f,i) := (k,r) = (((f,i) := k),k) := r;

theorem Th17: :: GRAPHSP:17
for i, k being Element of NAT
for f being Element of REAL *
for r being Real st i <> k &amp; i in dom f holds
((f,i) := (k,r)) . i = k
proofend;

theorem Th18: :: GRAPHSP:18
for m, i, k being Element of NAT
for f being Element of REAL *
for r being Real st m <> i &amp; m <> k holds
((f,i) := (k,r)) . m = f . m
proofend;

theorem Th19: :: GRAPHSP:19
for k, i being Element of NAT
for f being Element of REAL *
for r being Real st k in dom f holds
((f,i) := (k,r)) . k = r
proofend;

theorem Th20: :: GRAPHSP:20
for i, k being Element of NAT
for f being Element of REAL *
for r being Real holds dom ((f,i) := (k,r)) = dom f
proofend;

begin

definition
let X be set ;
let f, g be Element of Funcs (X,X);
:: original:*
redefine funcg * f ->  Element of Funcs (X,X);
coherence
 f * g is Element of Funcs (X,X)
proofend;
end;

definition
let X be set ;
let f be Element of Funcs (X,X);
let g be Element of X;
:: original:.
redefine funcf . g ->  Element of X;
coherence
 f . g is Element of X
proofend;
end;

definition
let X be set ;
let f be Element of Funcs (X,X);
func repeat f ->  Function of NAT,(Funcs (X,X)) means :Def2: :: GRAPHSP:def 2
( it . 0 = id X &amp; ( for i being Nat holds it . (i + 1) = f * (it . i) ) );
existence
 ex b1 being Function of NAT,(Funcs (X,X)) st
( b1 . 0 = id X &amp; ( for i being Nat holds b1 . (i + 1) = f * (b1 . i) ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,(Funcs (X,X)) st b1 . 0 = id X &amp; ( for i being Nat holds b1 . (i + 1) = f * (b1 . i) ) &amp; b2 . 0 = id X &amp; ( for i being Nat holds b2 . (i + 1) = f * (b2 . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines repeat GRAPHSP:def_2_:_
 for X being set
for f being Element of Funcs (X,X)
for b3 being Function of NAT,(Funcs (X,X)) holds
( b3 = repeat f iff ( b3 . 0 = id X &amp; ( for i being Nat holds b3 . (i + 1) = f * (b3 . i) ) ) );

theorem Th21: :: GRAPHSP:21
for F being Element of Funcs ((REAL *),(REAL *))
for f being Element of REAL *
for n, i being Element of NAT holds ((repeat F) . 0) . f = f
proofend;

Lm5:  for X being set
for f being Element of Funcs (X,X) holds dom f = X
proofend;

theorem Th22: :: GRAPHSP:22
for F, G being Element of Funcs ((REAL *),(REAL *))
for f being Element of REAL *
for i being Element of NAT holds ((repeat (F * G)) . (i + 1)) . f = F . (G . (((repeat (F * G)) . i) . f))
proofend;

definition
let g be Element of Funcs ((REAL *),(REAL *));
let f be Element of REAL * ;
:: original:.
redefine funcg . f ->  Element of REAL * ;
coherence
 g . f is Element of REAL *
proofend;
end;

definition
let f be Element of REAL * ;
let n be Nat;
func OuterVx (f,n) ->  Subset of NAT equals :: GRAPHSP:def 3
 {  i where i is Element of NAT : ( i in dom f &amp; 1 <= i &amp; i <= n &amp; f . i <> - 1 &amp; f . (n + i) <> - 1 )  }  ;
coherence
  {  i where i is Element of NAT : ( i in dom f &amp; 1 <= i &amp; i <= n &amp; f . i <> - 1 &amp; f . (n + i) <> - 1 )  }  is Subset of NAT
proofend;
end;

:: deftheorem  defines OuterVx GRAPHSP:def_3_:_
 for f being Element of REAL *
for n being Nat holds OuterVx (f,n) =  {  i where i is Element of NAT : ( i in dom f &amp; 1 <= i &amp; i <= n &amp; f . i <> - 1 &amp; f . (n + i) <> - 1 )  }  ;

definition
let f be Element of Funcs ((REAL *),(REAL *));
let g be Element of REAL * ;
let n be Nat;
assume A1: ex i being Element of NAT st OuterVx ((((repeat f) . i) . g),n) = {} ;
func LifeSpan (f,g,n) ->  Element of NAT  means :Def4: :: GRAPHSP:def 4
( OuterVx ((((repeat f) . it) . g),n) = {} &amp; ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
it <= k ) );
existence
 ex b1 being Element of NAT st
( OuterVx ((((repeat f) . b1) . g),n) = {} &amp; ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
b1 <= k ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st OuterVx ((((repeat f) . b1) . g),n) = {} &amp; ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
b1 <= k ) &amp; OuterVx ((((repeat f) . b2) . g),n) = {} &amp; ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
b2 <= k ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines LifeSpan GRAPHSP:def_4_:_
 for f being Element of Funcs ((REAL *),(REAL *))
for g being Element of REAL *
for n being Nat st ex i being Element of NAT st OuterVx ((((repeat f) . i) . g),n) = {} holds
for b4 being Element of NAT holds
( b4 = LifeSpan (f,g,n) iff ( OuterVx ((((repeat f) . b4) . g),n) = {} &amp; ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds
b4 <= k ) ) );

definition
let f be Element of Funcs ((REAL *),(REAL *));
let n be Element of NAT ;
func while_do (f,n) ->  Element of Funcs ((REAL *),(REAL *)) means :Def5: :: GRAPHSP:def 5
( dom it = REAL * &amp; ( for h being Element of REAL * holds it . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) );
existence
 ex b1 being Element of Funcs ((REAL *),(REAL *)) st
( dom b1 = REAL * &amp; ( for h being Element of REAL * holds b1 . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) )
proofend;
uniqueness
 for b1, b2 being Element of Funcs ((REAL *),(REAL *)) st dom b1 = REAL * &amp; ( for h being Element of REAL * holds b1 . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) &amp; dom b2 = REAL * &amp; ( for h being Element of REAL * holds b2 . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines while_do GRAPHSP:def_5_:_
 for f being Element of Funcs ((REAL *),(REAL *))
for n being Element of NAT
for b3 being Element of Funcs ((REAL *),(REAL *)) holds
( b3 = while_do (f,n) iff ( dom b3 = REAL * &amp; ( for h being Element of REAL * holds b3 . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) ) );

begin

definition
let G be oriented Graph;
let v1, v2 be Vertex of G;
assume A1: ex e being set st
( e in the carrier' of G &amp; e orientedly_joins v1,v2 ) ;
func XEdge (v1,v2) ->  set  means :Def6: :: GRAPHSP:def 6
 ex e being set st
( it = e &amp; e in the carrier' of G &amp; e orientedly_joins v1,v2 );
existence
 ex b1 being set ex e being set st
( b1 = e &amp; e in the carrier' of G &amp; e orientedly_joins v1,v2 ) by A1;
uniqueness
 for b1, b2 being set st ex e being set st
( b1 = e &amp; e in the carrier' of G &amp; e orientedly_joins v1,v2 ) &amp; ex e being set st
( b2 = e &amp; e in the carrier' of G &amp; e orientedly_joins v1,v2 ) holds
b1 = b2 by Th10;
end;

:: deftheorem Def6 defines XEdge GRAPHSP:def_6_:_
 for G being oriented Graph
for v1, v2 being Vertex of G st ex e being set st
( e in the carrier' of G &amp; e orientedly_joins v1,v2 ) holds
for b4 being set holds
( b4 = XEdge (v1,v2) iff ex e being set st
( b4 = e &amp; e in the carrier' of G &amp; e orientedly_joins v1,v2 ) );

definition
let G be oriented Graph;
let v1, v2 be Vertex of G;
let W be Function;
func Weight (v1,v2,W) ->  set  equals :Def7: :: GRAPHSP:def 7
W . (XEdge (v1,v2)) if  ex e being set st
( e in the carrier' of G &amp; e orientedly_joins v1,v2 )
otherwise  - 1;
correctness
coherence
( ( ex e being set st
( e in the carrier' of G &amp; e orientedly_joins v1,v2 ) implies W . (XEdge (v1,v2)) is set ) &amp; ( ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) implies - 1 is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def7 defines Weight GRAPHSP:def_7_:_
 for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function holds
( ( ex e being set st
( e in the carrier' of G &amp; e orientedly_joins v1,v2 ) implies Weight (v1,v2,W) = W . (XEdge (v1,v2)) ) &amp; ( ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) implies Weight (v1,v2,W) = - 1 ) );

definition
let G be oriented Graph;
let v1, v2 be Vertex of G;
let W be Function of the carrier' of G,Real>=0;
:: original:Weight
redefine func Weight (v1,v2,W) ->  Real;
coherence
 Weight (v1,v2,W) is Real
proofend;
end;

theorem Th23: :: GRAPHSP:23
for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function of the carrier' of G,Real>=0 holds
( Weight (v1,v2,W) >= 0 iff ex e being set st
( e in the carrier' of G &amp; e orientedly_joins v1,v2 ) )
proofend;

theorem :: GRAPHSP:24
for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function of the carrier' of G,Real>=0 holds
( Weight (v1,v2,W) = - 1 iff for e being set holds
( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) by Def7, Th23;

theorem Th25: :: GRAPHSP:25
for e being set
for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function of the carrier' of G,Real>=0 st e in the carrier' of G &amp; e orientedly_joins v1,v2 holds
Weight (v1,v2,W) = W . e
proofend;

begin

definition
let f be Element of REAL * ;
let n be Element of NAT ;
func UnusedVx (f,n) ->  Subset of NAT equals :: GRAPHSP:def 8
 {  i where i is Element of NAT : ( i in dom f &amp; 1 <= i &amp; i <= n &amp; f . i <> - 1 )  }  ;
coherence
  {  i where i is Element of NAT : ( i in dom f &amp; 1 <= i &amp; i <= n &amp; f . i <> - 1 )  }  is Subset of NAT
proofend;
end;

:: deftheorem  defines UnusedVx GRAPHSP:def_8_:_
 for f being Element of REAL *
for n being Element of NAT holds UnusedVx (f,n) =  {  i where i is Element of NAT : ( i in dom f &amp; 1 <= i &amp; i <= n &amp; f . i <> - 1 )  }  ;

definition
let f be Element of REAL * ;
let n be Element of NAT ;
func UsedVx (f,n) ->  Subset of NAT equals :: GRAPHSP:def 9
 {  i where i is Element of NAT : ( i in dom f &amp; 1 <= i &amp; i <= n &amp; f . i = - 1 )  }  ;
coherence
  {  i where i is Element of NAT : ( i in dom f &amp; 1 <= i &amp; i <= n &amp; f . i = - 1 )  }  is Subset of NAT
proofend;
end;

:: deftheorem  defines UsedVx GRAPHSP:def_9_:_
 for f being Element of REAL *
for n being Element of NAT holds UsedVx (f,n) =  {  i where i is Element of NAT : ( i in dom f &amp; 1 <= i &amp; i <= n &amp; f . i = - 1 )  }  ;

theorem Th26: :: GRAPHSP:26
for n being Element of NAT
for f being Element of REAL * holds UnusedVx (f,n) c= Seg n
proofend;

registration
let f be Element of REAL * ;
let n be Element of NAT ;
cluster UnusedVx (f,n) ->  finite ;
coherence
 UnusedVx (f,n) is finite
proofend;
end;

theorem Th27: :: GRAPHSP:27
for n being Element of NAT
for f being Element of REAL * holds OuterVx (f,n) c= UnusedVx (f,n)
proofend;

theorem Th28: :: GRAPHSP:28
for n being Element of NAT
for f being Element of REAL * holds OuterVx (f,n) c= Seg n
proofend;

registration
let f be Element of REAL * ;
let n be Element of NAT ;
cluster OuterVx (f,n) ->  finite ;
coherence
 OuterVx (f,n) is finite
proofend;
end;

definition
let X be finite Subset of NAT;
let f be Element of REAL * ;
let n be Element of NAT ;
func Argmin (X,f,n) ->  Element of NAT  means :Def10: :: GRAPHSP:def 10
( ( X <> {} implies ex i being Element of NAT st
( i = it &amp; i in X &amp; ( for k being Element of NAT st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) &amp; ( for k being Element of NAT st k in X &amp; f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) &amp; ( X = {} implies it = 0 ) );
existence
 ex b1 being Element of NAT st
( ( X <> {} implies ex i being Element of NAT st
( i = b1 &amp; i in X &amp; ( for k being Element of NAT st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) &amp; ( for k being Element of NAT st k in X &amp; f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) &amp; ( X = {} implies b1 = 0 ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ( X <> {} implies ex i being Element of NAT st
( i = b1 &amp; i in X &amp; ( for k being Element of NAT st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) &amp; ( for k being Element of NAT st k in X &amp; f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) &amp; ( X = {} implies b1 = 0 ) &amp; ( X <> {} implies ex i being Element of NAT st
( i = b2 &amp; i in X &amp; ( for k being Element of NAT st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) &amp; ( for k being Element of NAT st k in X &amp; f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) &amp; ( X = {} implies b2 = 0 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines Argmin GRAPHSP:def_10_:_
 for X being finite Subset of NAT
for f being Element of REAL *
for n, b4 being Element of NAT holds
( b4 = Argmin (X,f,n) iff ( ( X <> {} implies ex i being Element of NAT st
( i = b4 &amp; i in X &amp; ( for k being Element of NAT st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) &amp; ( for k being Element of NAT st k in X &amp; f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) &amp; ( X = {} implies b4 = 0 ) ) );

theorem Th29: :: GRAPHSP:29
for n, j being Element of NAT
for f being Element of REAL * st OuterVx (f,n) <> {} &amp; j = Argmin ((OuterVx (f,n)),f,n) holds
( j in dom f &amp; 1 <= j &amp; j <= n &amp; f . j <> - 1 &amp; f . (n + j) <> - 1 )
proofend;

theorem Th30: :: GRAPHSP:30
for n being Element of NAT
for f being Element of REAL * holds Argmin ((OuterVx (f,n)),f,n) <= n
proofend;

definition
let n be Element of NAT ;
func findmin n ->  Element of Funcs ((REAL *),(REAL *)) means :Def11: :: GRAPHSP:def 11
( dom it = REAL * &amp; ( for f being Element of REAL * holds it . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) );
existence
 ex b1 being Element of Funcs ((REAL *),(REAL *)) st
( dom b1 = REAL * &amp; ( for f being Element of REAL * holds b1 . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) )
proofend;
uniqueness
 for b1, b2 being Element of Funcs ((REAL *),(REAL *)) st dom b1 = REAL * &amp; ( for f being Element of REAL * holds b1 . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) &amp; dom b2 = REAL * &amp; ( for f being Element of REAL * holds b2 . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines findmin GRAPHSP:def_11_:_
 for n being Element of NAT
for b2 being Element of Funcs ((REAL *),(REAL *)) holds
( b2 = findmin n iff ( dom b2 = REAL * &amp; ( for f being Element of REAL * holds b2 . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) ) );

theorem Th31: :: GRAPHSP:31
for i, n being Element of NAT
for f being Element of REAL * st i > n &amp; i <> ((n * n) + (3 * n)) + 1 holds
((findmin n) . f) . i = f . i
proofend;

theorem Th32: :: GRAPHSP:32
for i, n being Element of NAT
for f being Element of REAL * st i in dom f &amp; f . i = - 1 &amp; i <> ((n * n) + (3 * n)) + 1 holds
((findmin n) . f) . i = - 1
proofend;

theorem Th33: :: GRAPHSP:33
for n being Element of NAT
for f being Element of REAL * holds dom ((findmin n) . f) = dom f
proofend;

Lm6:  for k, n being Element of NAT st k >= 1 holds
n <= k * n
proofend;

Lm7:  for n being Element of NAT holds
( 3 * n < ((n * n) + (3 * n)) + 1 &amp; n < ((n * n) + (3 * n)) + 1 &amp; 2 * n < ((n * n) + (3 * n)) + 1 )
proofend;

Lm8:  for n, k being Element of NAT holds
( ( n < k &amp; k <= 2 * n implies ( ( not 2 * n < k or not k <= 3 * n ) &amp; not k <= n &amp; not k > 3 * n ) ) &amp; ( ( k <= n or k > 3 * n ) implies ( ( not 2 * n < k or not k <= 3 * n ) &amp; ( not n < k or not k <= 2 * n ) ) ) &amp; ( 2 * n < k &amp; k <= 3 * n implies ( ( not n < k or not k <= 2 * n ) &amp; not k <= n &amp; not k > 3 * n ) ) )
proofend;

theorem Th34: :: GRAPHSP:34
for n being Element of NAT
for f being Element of REAL * st OuterVx (f,n) <> {} holds
ex j being Element of NAT st
( j in OuterVx (f,n) &amp; 1 <= j &amp; j <= n &amp; ((findmin n) . f) . j = - 1 )
proofend;

definition
let f be Element of REAL * ;
let n, k be Element of NAT ;
func newpathcost (f,n,k) ->  Real equals :: GRAPHSP:def 12
(f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k));
correctness
coherence
(f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k)) is Real;
;
end;

:: deftheorem  defines newpathcost GRAPHSP:def_12_:_
 for f being Element of REAL *
for n, k being Element of NAT holds newpathcost (f,n,k) = (f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k));

definition
let n, k be Element of NAT ;
let f be Element of REAL * ;
predf hasBetterPathAt n,k means :Def13: :: GRAPHSP:def 13
( ( f . (n + k) = - 1 or f /. ((2 * n) + k) > newpathcost (f,n,k) ) &amp; f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k) >= 0 &amp; f . k <> - 1 );
end;

:: deftheorem Def13 defines hasBetterPathAt GRAPHSP:def_13_:_
 for n, k being Element of NAT
for f being Element of REAL * holds
( f hasBetterPathAt n,k iff ( ( f . (n + k) = - 1 or f /. ((2 * n) + k) > newpathcost (f,n,k) ) &amp; f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k) >= 0 &amp; f . k <> - 1 ) );

definition
let f be Element of REAL * ;
let n be Element of NAT ;
func Relax (f,n) ->  Element of REAL *  means :Def14: :: GRAPHSP:def 14
( dom it = dom f &amp; ( for k being Element of NAT st k in dom f holds
( ( n < k &amp; k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies it . k = f /. (((n * n) + (3 * n)) + 1) ) &amp; ( not f hasBetterPathAt n,k -' n implies it . k = f . k ) ) ) &amp; ( 2 * n < k &amp; k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies it . k = newpathcost (f,n,(k -' (2 * n))) ) &amp; ( not f hasBetterPathAt n,k -' (2 * n) implies it . k = f . k ) ) ) &amp; ( ( k <= n or k > 3 * n ) implies it . k = f . k ) ) ) );
existence
 ex b1 being Element of REAL * st
( dom b1 = dom f &amp; ( for k being Element of NAT st k in dom f holds
( ( n < k &amp; k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b1 . k = f /. (((n * n) + (3 * n)) + 1) ) &amp; ( not f hasBetterPathAt n,k -' n implies b1 . k = f . k ) ) ) &amp; ( 2 * n < k &amp; k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b1 . k = newpathcost (f,n,(k -' (2 * n))) ) &amp; ( not f hasBetterPathAt n,k -' (2 * n) implies b1 . k = f . k ) ) ) &amp; ( ( k <= n or k > 3 * n ) implies b1 . k = f . k ) ) ) )
proofend;
uniqueness
 for b1, b2 being Element of REAL * st dom b1 = dom f &amp; ( for k being Element of NAT st k in dom f holds
( ( n < k &amp; k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b1 . k = f /. (((n * n) + (3 * n)) + 1) ) &amp; ( not f hasBetterPathAt n,k -' n implies b1 . k = f . k ) ) ) &amp; ( 2 * n < k &amp; k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b1 . k = newpathcost (f,n,(k -' (2 * n))) ) &amp; ( not f hasBetterPathAt n,k -' (2 * n) implies b1 . k = f . k ) ) ) &amp; ( ( k <= n or k > 3 * n ) implies b1 . k = f . k ) ) ) &amp; dom b2 = dom f &amp; ( for k being Element of NAT st k in dom f holds
( ( n < k &amp; k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b2 . k = f /. (((n * n) + (3 * n)) + 1) ) &amp; ( not f hasBetterPathAt n,k -' n implies b2 . k = f . k ) ) ) &amp; ( 2 * n < k &amp; k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b2 . k = newpathcost (f,n,(k -' (2 * n))) ) &amp; ( not f hasBetterPathAt n,k -' (2 * n) implies b2 . k = f . k ) ) ) &amp; ( ( k <= n or k > 3 * n ) implies b2 . k = f . k ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines Relax GRAPHSP:def_14_:_
 for f being Element of REAL *
for n being Element of NAT
for b3 being Element of REAL * holds
( b3 = Relax (f,n) iff ( dom b3 = dom f &amp; ( for k being Element of NAT st k in dom f holds
( ( n < k &amp; k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b3 . k = f /. (((n * n) + (3 * n)) + 1) ) &amp; ( not f hasBetterPathAt n,k -' n implies b3 . k = f . k ) ) ) &amp; ( 2 * n < k &amp; k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b3 . k = newpathcost (f,n,(k -' (2 * n))) ) &amp; ( not f hasBetterPathAt n,k -' (2 * n) implies b3 . k = f . k ) ) ) &amp; ( ( k <= n or k > 3 * n ) implies b3 . k = f . k ) ) ) ) );

definition
let n be Element of NAT ;
func Relax n ->  Element of Funcs ((REAL *),(REAL *)) means :Def15: :: GRAPHSP:def 15
( dom it = REAL * &amp; ( for f being Element of REAL * holds it . f = Relax (f,n) ) );
existence
 ex b1 being Element of Funcs ((REAL *),(REAL *)) st
( dom b1 = REAL * &amp; ( for f being Element of REAL * holds b1 . f = Relax (f,n) ) )
proofend;
uniqueness
 for b1, b2 being Element of Funcs ((REAL *),(REAL *)) st dom b1 = REAL * &amp; ( for f being Element of REAL * holds b1 . f = Relax (f,n) ) &amp; dom b2 = REAL * &amp; ( for f being Element of REAL * holds b2 . f = Relax (f,n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines Relax GRAPHSP:def_15_:_
 for n being Element of NAT
for b2 being Element of Funcs ((REAL *),(REAL *)) holds
( b2 = Relax n iff ( dom b2 = REAL * &amp; ( for f being Element of REAL * holds b2 . f = Relax (f,n) ) ) );

theorem Th35: :: GRAPHSP:35
for n being Element of NAT
for f being Element of REAL * holds dom ((Relax n) . f) = dom f
proofend;

theorem Th36: :: GRAPHSP:36
for i, n being Element of NAT
for f being Element of REAL * st ( i <= n or i > 3 * n ) &amp; i in dom f holds
((Relax n) . f) . i = f . i
proofend;

theorem Th37: :: GRAPHSP:37
for n, i being Element of NAT
for f being Element of REAL * holds dom (((repeat ((Relax n) * (findmin n))) . i) . f) = dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f)
proofend;

theorem Th38: :: GRAPHSP:38
for n, i being Element of NAT
for f being Element of REAL * st OuterVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n) <> {} holds
UnusedVx ((((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n) c< UnusedVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n)
proofend;

theorem Th39: :: GRAPHSP:39
for n, i, k being Element of NAT
for g, f, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . i) . f &amp; h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f &amp; k = Argmin ((OuterVx (g,n)),g,n) &amp; OuterVx (g,n) <> {} holds
( UsedVx (h,n) = (UsedVx (g,n)) \/ {k} &amp; not k in UsedVx (g,n) )
proofend;

theorem Th40: :: GRAPHSP:40
for n being Element of NAT
for f being Element of REAL * ex i being Element of NAT st
( i <= n &amp; OuterVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n) = {} )
proofend;

Lm9:  for n, k being Element of NAT holds n - k <= n
proofend;

Lm10:  for p, q being FinSequence of NAT
for f being Element of REAL *
for i, n being Element of NAT st ( for k being Element of NAT st 1 <= k &amp; k < len p holds
p . ((len p) - k) = f . ((p /. (((len p) - k) + 1)) + n) ) &amp; ( for k being Element of NAT st 1 <= k &amp; k < len q holds
q . ((len q) - k) = f . ((q /. (((len q) - k) + 1)) + n) ) &amp; len p <= len q &amp; p . (len p) = q . (len q) holds
for k being Element of NAT st 1 <= k &amp; k < len p holds
p . ((len p) - k) = q . ((len q) - k)
proofend;

theorem Th41: :: GRAPHSP:41
for n, i being Element of NAT
for f being Element of REAL * holds dom f = dom (((repeat ((Relax n) * (findmin n))) . i) . f)
proofend;

definition
let f, g be Element of REAL * ;
let m, n be Element of NAT ;
predf,g equal_at m,n means :Def16: :: GRAPHSP:def 16
( dom f = dom g &amp; ( for k being Element of NAT st k in dom f &amp; m <= k &amp; k <= n holds
f . k = g . k ) );
end;

:: deftheorem Def16 defines equal_at GRAPHSP:def_16_:_
 for f, g being Element of REAL *
for m, n being Element of NAT holds
( f,g equal_at m,n iff ( dom f = dom g &amp; ( for k being Element of NAT st k in dom f &amp; m <= k &amp; k <= n holds
f . k = g . k ) ) );

theorem Th42: :: GRAPHSP:42
for m, n being Element of NAT
for f being Element of REAL * holds f,f equal_at m,n
proofend;

theorem Th43: :: GRAPHSP:43
for m, n being Element of NAT
for f, g, h being Element of REAL * st f,g equal_at m,n &amp; g,h equal_at m,n holds
f,h equal_at m,n
proofend;

theorem Th44: :: GRAPHSP:44
for n, i being Element of NAT
for f being Element of REAL * holds ((repeat ((Relax n) * (findmin n))) . i) . f,((repeat ((Relax n) * (findmin n))) . (i + 1)) . f equal_at (3 * n) + 1,(n * n) + (3 * n)
proofend;

theorem :: GRAPHSP:45
for F being Element of Funcs ((REAL *),(REAL *))
for f being Element of REAL *
for n, i being Element of NAT st i < LifeSpan (F,f,n) holds
OuterVx ((((repeat F) . i) . f),n) <> {} by Def4;

theorem Th46: :: GRAPHSP:46
for n, i being Element of NAT
for f being Element of REAL * holds f,((repeat ((Relax n) * (findmin n))) . i) . f equal_at (3 * n) + 1,(n * n) + (3 * n)
proofend;

theorem Th47: :: GRAPHSP:47
for n being Element of NAT
for f being Element of REAL * st 1 <= n &amp; 1 in dom f &amp; f . (n + 1) <> - 1 &amp; ( for i being Element of NAT st 1 <= i &amp; i <= n holds
f . i = 1 ) &amp; ( for i being Element of NAT st 2 <= i &amp; i <= n holds
f . (n + i) = - 1 ) holds
( 1 = Argmin ((OuterVx (f,n)),f,n) &amp; UsedVx (f,n) = {} &amp; {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) )
proofend;

theorem Th48: :: GRAPHSP:48
for n, i, m being Element of NAT
for g, f, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . 1) . f &amp; h = ((repeat ((Relax n) * (findmin n))) . i) . f &amp; 1 <= i &amp; i <= LifeSpan (((Relax n) * (findmin n)),f,n) &amp; m in UsedVx (g,n) holds
m in UsedVx (h,n)
proofend;

definition
let p be FinSequence of NAT ;
let f be Element of REAL * ;
let i, n be Element of NAT ;
predp is_vertex_seq_at f,i,n means :Def17: :: GRAPHSP:def 17
( p . (len p) = i &amp; ( for k being Element of NAT st 1 <= k &amp; k < len p holds
p . ((len p) - k) = f . (n + (p /. (((len p) - k) + 1))) ) );
end;

:: deftheorem Def17 defines is_vertex_seq_at GRAPHSP:def_17_:_
 for p being FinSequence of NAT
for f being Element of REAL *
for i, n being Element of NAT holds
( p is_vertex_seq_at f,i,n iff ( p . (len p) = i &amp; ( for k being Element of NAT st 1 <= k &amp; k < len p holds
p . ((len p) - k) = f . (n + (p /. (((len p) - k) + 1))) ) ) );

definition
let p be FinSequence of NAT ;
let f be Element of REAL * ;
let i, n be Element of NAT ;
predp is_simple_vertex_seq_at f,i,n means :Def18: :: GRAPHSP:def 18
( p . 1 = 1 &amp; len p > 1 &amp; p is_vertex_seq_at f,i,n &amp; p is one-to-one );
end;

:: deftheorem Def18 defines is_simple_vertex_seq_at GRAPHSP:def_18_:_
 for p being FinSequence of NAT
for f being Element of REAL *
for i, n being Element of NAT holds
( p is_simple_vertex_seq_at f,i,n iff ( p . 1 = 1 &amp; len p > 1 &amp; p is_vertex_seq_at f,i,n &amp; p is one-to-one ) );

theorem :: GRAPHSP:49
for p, q being FinSequence of NAT
for f being Element of REAL *
for i, n being Element of NAT st p is_simple_vertex_seq_at f,i,n &amp; q is_simple_vertex_seq_at f,i,n holds
p = q
proofend;

definition
let G be Graph;
let p be FinSequence of the carrier' of G;
let vs be FinSequence;
predp is_oriented_edge_seq_of vs means :Def19: :: GRAPHSP:def 19
( len vs = (len p) + 1 &amp; ( for n being Nat st 1 <= n &amp; n <= len p holds
( the Source of G . (p . n) = vs . n &amp; the Target of G . (p . n) = vs . (n + 1) ) ) );
end;

:: deftheorem Def19 defines is_oriented_edge_seq_of GRAPHSP:def_19_:_
 for G being Graph
for p being FinSequence of the carrier' of G
for vs being FinSequence holds
( p is_oriented_edge_seq_of vs iff ( len vs = (len p) + 1 &amp; ( for n being Nat st 1 <= n &amp; n <= len p holds
( the Source of G . (p . n) = vs . n &amp; the Target of G . (p . n) = vs . (n + 1) ) ) ) );

theorem :: GRAPHSP:50
for G being oriented Graph
for vs being FinSequence
for p, q being oriented Chain of G st p is_oriented_edge_seq_of vs &amp; q is_oriented_edge_seq_of vs holds
p = q
proofend;

theorem :: GRAPHSP:51
for G being Graph
for vs1, vs2 being FinSequence
for p being oriented Chain of G st p is_oriented_edge_seq_of vs1 &amp; p is_oriented_edge_seq_of vs2 &amp; len p >= 1 holds
vs1 = vs2
proofend;

Lm11:  for i, n being Element of NAT st 1 <= i &amp; i <= n holds
( 1 < (2 * n) + i &amp; (2 * n) + i < ((n * n) + (3 * n)) + 1 &amp; i < (2 * n) + i )
proofend;

Lm12:  for i, n being Element of NAT st 1 <= i &amp; i <= n holds
( 1 < n + i &amp; n + i <= 2 * n &amp; n + i < ((n * n) + (3 * n)) + 1 )
proofend;

Lm13:  for i, n, j being Element of NAT st 1 <= i &amp; i <= n &amp; j <= n holds
( 1 < ((2 * n) + (n * i)) + j &amp; i < ((2 * n) + (n * i)) + j &amp; ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1 )
proofend;

Lm14:  for i, n, j being Element of NAT st 1 <= i &amp; i <= n &amp; 1 <= j &amp; j <= n holds
( (3 * n) + 1 <= ((2 * n) + (n * i)) + j &amp; ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) )
proofend;

begin

:: address possible value init. value comment
:: 1 1 or -1 1 -1 if node v1 is used
:: 2 1 or -1 1 -1 if node v2 is used
:: : : : :
:: n 1 or -1 1 -1 if node vn is used
:: n+1 0 0 preceding-node of v1 toward v1
:: n+2 -1 or Node No. -1 preceding-node of v2 toward v1
:: : : : :
:: 2*n -1 or Node No. -1 preceding-node of vn toward v1
:: 2*n+1 0 0 cost from v1 to v1
:: 2*n+2 >=0 0 minimum cost from v2 to v1
:: : : : :
:: 3*n >=0 0 minimum cost from vn to v1
:: 3*n+1 weight(v1,v1) the weight of edge(v1,v1)
:: 3*n+2 weight(v1,v2) the weight of edge(v1,v2)
:: : : :
:: 4*n weight(v1,vn) the weight of edge(v1,vn)
:: : : :
:: n*n+3*n weight(vn,vn) the weight of edge(vn,vn)
:: n*n+3n+1 Node No. current node with the shortest path
definition
let f be Element of REAL * ;
let G be oriented Graph;
let n be Element of NAT ;
let W be Function of the carrier' of G,Real>=0;
predf is_Input_of_Dijkstra_Alg G,n,W means :Def20: :: GRAPHSP:def 20
( len f = ((n * n) + (3 * n)) + 1 &amp; Seg n = the carrier of G &amp; ( for i being Element of NAT st 1 <= i &amp; i <= n holds
( f . i = 1 &amp; f . ((2 * n) + i) = 0 ) ) &amp; f . (n + 1) = 0 &amp; ( for i being Element of NAT st 2 <= i &amp; i <= n holds
f . (n + i) = - 1 ) &amp; ( for i, j being Vertex of G
for k, m being Element of NAT st k = i &amp; m = j holds
f . (((2 * n) + (n * k)) + m) = Weight (i,j,W) ) );
end;

:: deftheorem Def20 defines is_Input_of_Dijkstra_Alg GRAPHSP:def_20_:_
 for f being Element of REAL *
for G being oriented Graph
for n being Element of NAT
for W being Function of the carrier' of G,Real>=0 holds
( f is_Input_of_Dijkstra_Alg G,n,W iff ( len f = ((n * n) + (3 * n)) + 1 &amp; Seg n = the carrier of G &amp; ( for i being Element of NAT st 1 <= i &amp; i <= n holds
( f . i = 1 &amp; f . ((2 * n) + i) = 0 ) ) &amp; f . (n + 1) = 0 &amp; ( for i being Element of NAT st 2 <= i &amp; i <= n holds
f . (n + i) = - 1 ) &amp; ( for i, j being Vertex of G
for k, m being Element of NAT st k = i &amp; m = j holds
f . (((2 * n) + (n * k)) + m) = Weight (i,j,W) ) ) );

begin

definition
let n be Element of NAT ;
func DijkstraAlgorithm n ->  Element of Funcs ((REAL *),(REAL *)) equals :: GRAPHSP:def 21
 while_do (((Relax n) * (findmin n)),n);
coherence
 while_do (((Relax n) * (findmin n)),n) is Element of Funcs ((REAL *),(REAL *)) ;
end;

:: deftheorem  defines DijkstraAlgorithm GRAPHSP:def_21_:_
 for n being Element of NAT holds DijkstraAlgorithm n = while_do (((Relax n) * (findmin n)),n);

begin

Lm15:  for n being Element of NAT
for f, 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 &amp; v1 = 1 &amp; n >= 1 &amp; h = ((repeat ((Relax n) * (findmin n))) . 1) . f holds
( ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 &amp; v3 = j &amp; 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 &amp; ( for i being Element of NAT st 1 <= i &amp; i < len p holds
p . i in UsedVx (h,n) ) &amp; P is_oriented_edge_seq_of p &amp; P is_shortestpath_of v1,v3, UsedVx (h,n),W &amp; cost (P,W) = h . ((2 * n) + j) &amp; ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) &amp; ( for m, j being Element of NAT st h . (n + j) = - 1 &amp; 1 <= j &amp; j <= n &amp; m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) &amp; ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) )
proofend;

Lm16:  for n, k, i being Element of NAT
for g, f, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . k) . f &amp; h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f &amp; OuterVx (g,n) <> {} &amp; i in UsedVx (g,n) &amp; len f = ((n * n) + (3 * n)) + 1 holds
h . (n + i) = g . (n + i)
proofend;

Lm17:  for n, k, j being Element of NAT
for g, f, h being Element of REAL *
for p being FinSequence of NAT st g = ((repeat ((Relax n) * (findmin n))) . k) . f &amp; h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f &amp; OuterVx (g,n) <> {} &amp; len f = ((n * n) + (3 * n)) + 1 &amp; p is_simple_vertex_seq_at g,j,n &amp; g . (n + j) = h . (n + j) &amp; ( for i being Element of NAT st 1 <= i &amp; i < len p holds
p . i in UsedVx (g,n) ) holds
p is_simple_vertex_seq_at h,j,n
proofend;

Lm18:  for n, k, m, j being Element of NAT
for g, f, h being Element of REAL *
for p being FinSequence of NAT st g = ((repeat ((Relax n) * (findmin n))) . k) . f &amp; h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f &amp; OuterVx (g,n) <> {} &amp; len f = ((n * n) + (3 * n)) + 1 &amp; p is_simple_vertex_seq_at g,m,n &amp; m = h . (n + j) &amp; g . (n + m) = h . (n + m) &amp; m <> j &amp; not j in UsedVx (g,n) &amp; ( for i being Element of NAT st 1 <= i &amp; i < len p holds
p . i in UsedVx (g,n) ) holds
p ^ <*j*> is_simple_vertex_seq_at h,j,n
proofend;

Lm19:  for n, i being Element of NAT
for V being set
for f, g being Element of REAL *
for G being oriented finite Graph
for P being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v2, v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W &amp; W is_weight>=0of G &amp; v2 = i &amp; v1 <> v2 &amp; 1 <= i &amp; i <= n &amp; P is_shortestpath_of v1,v2,V,W &amp; ( for m, j being Element of NAT st g . (n + j) = - 1 &amp; 1 <= j &amp; j <= n &amp; m in V holds
f . (((2 * n) + (n * m)) + j) = - 1 ) holds
g . (n + i) <> - 1
proofend;

Lm20:  for n, k being Element of NAT
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 &amp; v1 = 1 &amp; n >= 1 &amp; g = ((repeat ((Relax n) * (findmin n))) . k) . f &amp; h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f &amp; OuterVx (g,n) <> {} &amp; 1 in UsedVx (g,n) &amp; ( for v3 being Vertex of G
for j being Element of NAT st v3 <> v1 &amp; v3 = j &amp; 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 &amp; ( for i being Element of NAT st 1 <= i &amp; i < len p holds
p . i in UsedVx (g,n) ) &amp; P is_oriented_edge_seq_of p &amp; P is_shortestpath_of v1,v3, UsedVx (g,n),W &amp; cost (P,W) = g . ((2 * n) + j) &amp; ( not v3 in UsedVx (g,n) implies P islongestInShortestpath UsedVx (g,n),v1,W ) ) ) &amp; ( for m, j being Element of NAT st g . (n + j) = - 1 &amp; 1 <= j &amp; j <= n &amp; m in UsedVx (g,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) &amp; ( 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 &amp; v3 = j &amp; 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 &amp; ( for i being Element of NAT st 1 <= i &amp; i < len p holds
p . i in UsedVx (h,n) ) &amp; P is_oriented_edge_seq_of p &amp; P is_shortestpath_of v1,v3, UsedVx (h,n),W &amp; cost (P,W) = h . ((2 * n) + j) &amp; ( not v3 in UsedVx (h,n) implies P islongestInShortestpath UsedVx (h,n),v1,W ) ) ) &amp; ( for m, j being Element of NAT st h . (n + j) = - 1 &amp; 1 <= j &amp; j <= n &amp; m in UsedVx (h,n) holds
f . (((2 * n) + (n * m)) + j) = - 1 ) &amp; ( for m being Element of NAT st m in UsedVx (h,n) holds
h . (n + m) <> - 1 ) )
proofend;

theorem :: GRAPHSP:52
for n, i being Element of NAT
for f, g being Element of REAL *
for G being oriented finite Graph
for W being Function of the carrier' of G,Real>=0
for v1, v2 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W &amp; v1 = 1 &amp; 1 <> v2 &amp; v2 = i &amp; n >= 1 &amp; g = (DijkstraAlgorithm n) . f holds
( the carrier of G = (UsedVx (g,n)) \/ (UnusedVx (g,n)) &amp; ( v2 in UsedVx (g,n) implies ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,i,n &amp; P is_oriented_edge_seq_of p &amp; P is_shortestpath_of v1,v2,W &amp; cost (P,W) = g . ((2 * n) + i) ) ) &amp; ( v2 in UnusedVx (g,n) implies for Q being oriented Chain of G holds not Q is_orientedpath_of v1,v2 ) )
proofend;