:: The Underlying Principle of {D}ijkstra's Shortest Path Algorithm
:: by Jingchao Chen and Yatsuka Nakamura
::
:: Received January 7, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem Th1: :: GRAPH_5:1
for x being set
for f, g being Function st rng f c= rng g & x in dom f holds
ex y being set st
( y in dom g & f . x = g . y )
proofend;

scheme :: GRAPH_5:sch 1
LambdaAB{ F1() ->  set , F2() ->  set , F3( Element of F2()) ->  set } :
 ex f being Function st
( dom f = F1() & ( for x being Element of F2() st x in F1() holds
f . x = F3(x) ) )
proofend;

theorem Th2: :: GRAPH_5:2
for D being finite set
for n being Element of NAT
for X being set st X =  {  x where x is Element of D * : ( 1 <= len x &amp; len x <= n )  }  holds
X is finite
proofend;

theorem Th3: :: GRAPH_5:3
for D being finite set
for n being Element of NAT
for X being set st X =  {  x where x is Element of D * : len x <= n  }  holds
X is finite
proofend;

theorem Th4: :: GRAPH_5:4
for D being finite set
for k being Element of NAT st card D = k + 1 holds
ex x being Element of D ex C being Subset of D st
( D = C \/ {x} &amp; card C = k )
proofend;

theorem Th5: :: GRAPH_5:5
for D being finite set st card D = 1 holds
ex x being Element of D st D = {x}
proofend;

scheme :: GRAPH_5:sch 2
MinValue{ F1() ->  non empty finite set , F2( Element of F1()) ->  real number } :
 ex x being Element of F1() st
for y being Element of F1() holds F2(x) <= F2(y)
proofend;

definition
let D be set ;
let X be non empty Subset of (D *);
:: original:Element
redefine mode Element of X ->  FinSequence of D;
coherence
 for b1 being Element of X holds b1 is FinSequence of D
proofend;
end;

begin

Lm1:  for n being Element of 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 q, p being FinSequence st 1 <= n &amp; n <= len q holds
q . n = (p ^ q) . ((len p) + n)
proofend;

theorem Th6: :: GRAPH_5:6
for p being FinSequence holds
( ( for n, m being Element of NAT st 1 <= n &amp; n < m &amp; m <= len p holds
p . n <> p . m ) iff p is one-to-one )
proofend;

theorem Th7: :: GRAPH_5:7
for p being FinSequence holds
( ( for n, m being Element of NAT st 1 <= n &amp; n < m &amp; m <= len p holds
p . n <> p . m ) iff card (rng p) = len p )
proofend;

theorem :: GRAPH_5:8
for i being Element of NAT
for G being Graph
for pe being FinSequence of the carrier' of G st i in dom 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 ) by FINSEQ_2:11, FUNCT_2:5;

theorem Th9: :: GRAPH_5:9
for x being set
for q, p being FinSequence st q ^ <*x*> is one-to-one &amp; rng (q ^ <*x*>) c= rng p holds
ex p1, p2 being FinSequence st
( p = (p1 ^ <*x*>) ^ p2 &amp; rng q c= rng (p1 ^ p2) )
proofend;

begin

theorem Th10: :: GRAPH_5:10
for p, q being FinSequence
for G being Graph st p ^ q is Chain of G holds
( p is Chain of G &amp; q is Chain of G )
proofend;

theorem Th11: :: GRAPH_5:11
for p, q being FinSequence
for G being Graph st p ^ q is oriented Chain of G holds
( p is oriented Chain of G &amp; q is oriented Chain of G )
proofend;

theorem Th12: :: GRAPH_5:12
for G being Graph
for p, q being oriented Chain of G st the Target of G . (p . (len p)) = the Source of G . (q . 1) holds
p ^ q is oriented Chain of G
proofend;

begin

theorem Th13: :: GRAPH_5:13
for G being Graph holds {} is oriented Simple Chain of G
proofend;

theorem Th14: :: GRAPH_5:14
for p, q being FinSequence
for G being Graph st p ^ q is oriented Simple Chain of G holds
( p is oriented Simple Chain of G &amp; q is oriented Simple Chain of G )
proofend;

theorem Th15: :: GRAPH_5:15
for G being Graph
for pe being FinSequence of the carrier' of G st len pe = 1 holds
pe is oriented Simple Chain of G
proofend;

theorem Th16: :: GRAPH_5:16
for G being Graph
for p being oriented Simple Chain of G
for q being FinSequence of the carrier' of G st len p >= 1 &amp; len q = 1 &amp; the Source of G . (q . 1) = the Target of G . (p . (len p)) &amp; the Source of G . (p . 1) <> the Target of G . (p . (len p)) &amp; ( for k being Element of NAT holds
( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) holds
p ^ q is oriented Simple Chain of G
proofend;

theorem Th17: :: GRAPH_5:17
for G being Graph
for p being oriented Simple Chain of G holds p is V14()
proofend;

begin

definition
let G be Graph;
let e be Element of the carrier' of G;
func vertices e ->  set  equals :: GRAPH_5:def 1
{( the Source of G . e),( the Target of G . e)};
coherence
 {( the Source of G . e),( the Target of G . e)} is set ;
end;

:: deftheorem  defines vertices GRAPH_5:def_1_:_
 for G being Graph
for e being Element of the carrier' of G holds vertices e = {( the Source of G . e),( the Target of G . e)};

definition
let G be Graph;
let pe be FinSequence of the carrier' of G;
func vertices pe ->  Subset of the carrier of G equals :: GRAPH_5:def 2
 {  v where v is Vertex of G : ex i being Element of NAT st
( i in dom pe &amp; v in vertices (pe /. i) )  }  ;
coherence
  {  v where v is Vertex of G : ex i being Element of NAT st
( i in dom pe &amp; v in vertices (pe /. i) )  }  is Subset of the carrier of G
proofend;
end;

:: deftheorem  defines vertices GRAPH_5:def_2_:_
 for G being Graph
for pe being FinSequence of the carrier' of G holds vertices pe =  {  v where v is Vertex of G : ex i being Element of NAT st
( i in dom pe &amp; v in vertices (pe /. i) )  }  ;

theorem Th18: :: GRAPH_5:18
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 &amp; the Source of G . (p . 1) <> the Target of G . (p . (len p)) holds
( not the Source of G . (p . 1) in vertices qe &amp; not the Target of G . (p . (len p)) in vertices pe )
proofend;

theorem Th19: :: GRAPH_5:19
for V being set
for G being Graph
for pe being FinSequence of the carrier' of G holds
( vertices pe c= V iff for i being Nat st i in dom pe holds
vertices (pe /. i) c= V )
proofend;

theorem Th20: :: GRAPH_5:20
for V being set
for G being Graph
for pe being FinSequence of the carrier' of G st not vertices pe c= V holds
ex i being Element of NAT ex q, r being FinSequence of the carrier' of G st
( i + 1 <= len pe &amp; not vertices (pe /. (i + 1)) c= V &amp; len q = i &amp; pe = q ^ r &amp; vertices q c= V )
proofend;

theorem Th21: :: GRAPH_5:21
for G being Graph
for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe holds
vertices qe c= vertices pe
proofend;

theorem Th22: :: GRAPH_5:22
for X, V being set
for G being Graph
for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe &amp; (vertices pe) \ X c= V holds
(vertices qe) \ X c= V
proofend;

theorem Th23: :: GRAPH_5:23
for X, V being set
for G being Graph
for pe, qe being FinSequence of the carrier' of G st (vertices (pe ^ qe)) \ X c= V holds
( (vertices pe) \ X c= V &amp; (vertices qe) \ X c= V )
proofend;

theorem Th24: :: GRAPH_5:24
for i being Element of NAT
for G being Graph
for pe being FinSequence of the carrier' of G
for v being Element of G st i in dom pe &amp; ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds
v in vertices pe
proofend;

theorem Th25: :: GRAPH_5:25
for G being Graph
for pe being FinSequence of the carrier' of G st len pe = 1 holds
vertices pe = vertices (pe /. 1)
proofend;

theorem Th26: :: GRAPH_5:26
for G being Graph
for pe, qe being FinSequence of the carrier' of G holds
( vertices pe c= vertices (pe ^ qe) &amp; vertices qe c= vertices (pe ^ qe) )
proofend;

theorem Th27: :: GRAPH_5:27
for G being Graph
for pe being FinSequence of the carrier' of G
for p, q being oriented Chain of G st p = q ^ pe &amp; len q >= 1 &amp; len pe = 1 holds
vertices p = (vertices q) \/ {( the Target of G . (pe . 1))}
proofend;

theorem Th28: :: GRAPH_5:28
for G being Graph
for v being Element of G
for p being oriented Chain of G st v <> the Source of G . (p . 1) &amp; v in vertices p holds
ex i being Element of NAT st
( 1 <= i &amp; i <= len p &amp; v = the Target of G . (p . i) )
proofend;

begin

definition
let G be Graph;
let p be oriented Chain of G;
let v1, v2 be Element of G;
predp is_orientedpath_of v1,v2 means :Def3: :: GRAPH_5:def 3
( p <> {} &amp; the Source of G . (p . 1) = v1 &amp; the Target of G . (p . (len p)) = v2 );
end;

:: deftheorem Def3 defines is_orientedpath_of GRAPH_5:def_3_:_
 for G being Graph
for p being oriented Chain of G
for v1, v2 being Element of G holds
( p is_orientedpath_of v1,v2 iff ( p <> {} &amp; the Source of G . (p . 1) = v1 &amp; the Target of G . (p . (len p)) = v2 ) );

definition
let G be Graph;
let v1, v2 be Element of G;
let p be oriented Chain of G;
let V be set ;
predp is_orientedpath_of v1,v2,V means :Def4: :: GRAPH_5:def 4
( p is_orientedpath_of v1,v2 &amp; (vertices p) \ {v2} c= V );
end;

:: deftheorem Def4 defines is_orientedpath_of GRAPH_5:def_4_:_
 for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G
for V being set holds
( p is_orientedpath_of v1,v2,V iff ( p is_orientedpath_of v1,v2 &amp; (vertices p) \ {v2} c= V ) );

definition
let G be Graph;
let v1, v2 be Element of G;
func OrientedPaths (v1,v2) ->  Subset of ( the carrier' of G *) equals :: GRAPH_5:def 5
 {  p where p is oriented Chain of G : p is_orientedpath_of v1,v2  }  ;
coherence
  {  p where p is oriented Chain of G : p is_orientedpath_of v1,v2  }  is Subset of ( the carrier' of G *)
proofend;
end;

:: deftheorem  defines OrientedPaths GRAPH_5:def_5_:_
 for G being Graph
for v1, v2 being Element of G holds OrientedPaths (v1,v2) =  {  p where p is oriented Chain of G : p is_orientedpath_of v1,v2  }  ;

theorem Th29: :: GRAPH_5:29
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds
( v1 in vertices p &amp; v2 in vertices p )
proofend;

theorem :: GRAPH_5:30
for x being set
for G being Graph
for v1, v2 being Element of G holds
( x in OrientedPaths (v1,v2) iff ex p being oriented Chain of G st
( p = x &amp; p is_orientedpath_of v1,v2 ) ) ;

theorem Th31: :: GRAPH_5:31
for V being set
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V &amp; v1 <> v2 holds
v1 in V
proofend;

theorem Th32: :: GRAPH_5:32
for V, U being set
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V &amp; V c= U holds
p is_orientedpath_of v1,v2,U
proofend;

theorem Th33: :: GRAPH_5:33
for G being Graph
for pe being FinSequence of the carrier' of G
for v1, v2, v3 being Element of G
for p being oriented Chain of G st len p >= 1 &amp; p is_orientedpath_of v1,v2 &amp; pe . 1 orientedly_joins v2,v3 &amp; len pe = 1 holds
ex q being oriented Chain of G st
( q = p ^ pe &amp; q is_orientedpath_of v1,v3 )
proofend;

theorem Th34: :: GRAPH_5:34
for V being set
for G being Graph
for pe being FinSequence of the carrier' of G
for v1, v2, v3 being Element of G
for q, p being oriented Chain of G st q = p ^ pe &amp; len p >= 1 &amp; len pe = 1 &amp; p is_orientedpath_of v1,v2,V &amp; pe . 1 orientedly_joins v2,v3 holds
q is_orientedpath_of v1,v3,V \/ {v2}
proofend;

begin

definition
let G be Graph;
let p be oriented Chain of G;
let v1, v2 be Element of G;
predp is_acyclicpath_of v1,v2 means :Def6: :: GRAPH_5:def 6
( p is Simple &amp; p is_orientedpath_of v1,v2 );
end;

:: deftheorem Def6 defines is_acyclicpath_of GRAPH_5:def_6_:_
 for G being Graph
for p being oriented Chain of G
for v1, v2 being Element of G holds
( p is_acyclicpath_of v1,v2 iff ( p is Simple &amp; p is_orientedpath_of v1,v2 ) );

definition
let G be Graph;
let p be oriented Chain of G;
let v1, v2 be Element of G;
let V be set ;
predp is_acyclicpath_of v1,v2,V means :Def7: :: GRAPH_5:def 7
( p is Simple &amp; p is_orientedpath_of v1,v2,V );
end;

:: deftheorem Def7 defines is_acyclicpath_of GRAPH_5:def_7_:_
 for G being Graph
for p being oriented Chain of G
for v1, v2 being Element of G
for V being set holds
( p is_acyclicpath_of v1,v2,V iff ( p is Simple &amp; p is_orientedpath_of v1,v2,V ) );

definition
let G be Graph;
let v1, v2 be Element of G;
func AcyclicPaths (v1,v2) ->  Subset of ( the carrier' of G *) equals :: GRAPH_5:def 8
 {  p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2  }  ;
coherence
  {  p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2  }  is Subset of ( the carrier' of G *)
proofend;
end;

:: deftheorem  defines AcyclicPaths GRAPH_5:def_8_:_
 for G being Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2) =  {  p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2  }  ;

definition
let G be Graph;
let v1, v2 be Element of G;
let V be set ;
func AcyclicPaths (v1,v2,V) ->  Subset of ( the carrier' of G *) equals :: GRAPH_5:def 9
 {  p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V  }  ;
coherence
  {  p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V  }  is Subset of ( the carrier' of G *)
proofend;
end;

:: deftheorem  defines AcyclicPaths GRAPH_5:def_9_:_
 for G being Graph
for v1, v2 being Element of G
for V being set holds AcyclicPaths (v1,v2,V) =  {  p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V  }  ;

definition
let G be Graph;
let p be oriented Chain of G;
func AcyclicPaths p ->  Subset of ( the carrier' of G *) equals :: GRAPH_5:def 10
 {  q where q is oriented Simple Chain of G : ( q <> {} &amp; the Source of G . (q . 1) = the Source of G . (p . 1) &amp; the Target of G . (q . (len q)) = the Target of G . (p . (len p)) &amp; rng q c= rng p )  }  ;
coherence
  {  q where q is oriented Simple Chain of G : ( q <> {} &amp; the Source of G . (q . 1) = the Source of G . (p . 1) &amp; the Target of G . (q . (len q)) = the Target of G . (p . (len p)) &amp; rng q c= rng p )  }  is Subset of ( the carrier' of G *)
proofend;
end;

:: deftheorem  defines AcyclicPaths GRAPH_5:def_10_:_
 for G being Graph
for p being oriented Chain of G holds AcyclicPaths p =  {  q where q is oriented Simple Chain of G : ( q <> {} &amp; the Source of G . (q . 1) = the Source of G . (p . 1) &amp; the Target of G . (q . (len q)) = the Target of G . (p . (len p)) &amp; rng q c= rng p )  }  ;

definition
let G be Graph;
func AcyclicPaths G ->  Subset of ( the carrier' of G *) equals :: GRAPH_5:def 11
 {  q where q is oriented Simple Chain of G : verum  }  ;
coherence
  {  q where q is oriented Simple Chain of G : verum  }  is Subset of ( the carrier' of G *)
proofend;
end;

:: deftheorem  defines AcyclicPaths GRAPH_5:def_11_:_
 for G being Graph holds AcyclicPaths G =  {  q where q is oriented Simple Chain of G : verum  }  ;

theorem :: GRAPH_5:35
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p = {} holds
not p is_acyclicpath_of v1,v2
proofend;

theorem :: GRAPH_5:36
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_acyclicpath_of v1,v2 holds
p is_orientedpath_of v1,v2 by Def6;

theorem :: GRAPH_5:37
for G being Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2) c= OrientedPaths (v1,v2)
proofend;

theorem Th38: :: GRAPH_5:38
for G being Graph
for p being oriented Chain of G holds AcyclicPaths p c= AcyclicPaths G
proofend;

theorem Th39: :: GRAPH_5:39
for G being Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2) c= AcyclicPaths G
proofend;

theorem Th40: :: GRAPH_5:40
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds
AcyclicPaths p c= AcyclicPaths (v1,v2)
proofend;

theorem Th41: :: GRAPH_5:41
for V being set
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds
AcyclicPaths p c= AcyclicPaths (v1,v2,V)
proofend;

theorem :: GRAPH_5:42
for G being Graph
for q, p being oriented Chain of G st q in AcyclicPaths p holds
len q <= len p
proofend;

theorem Th43: :: GRAPH_5:43
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds
( AcyclicPaths p <> {} &amp; AcyclicPaths (v1,v2) <> {} )
proofend;

theorem Th44: :: GRAPH_5:44
for V being set
for G being Graph
for v1, v2 being Element of G
for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds
( AcyclicPaths p <> {} &amp; AcyclicPaths (v1,v2,V) <> {} )
proofend;

theorem Th45: :: GRAPH_5:45
for V being set
for G being Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) c= AcyclicPaths G
proofend;

begin

notation
synonym  Real>=0 for  REAL+ ;
end;

definition
:: original:Real>=0
redefine func Real>=0  ->  Subset of REAL equals :: GRAPH_5:def 12
 {  r where r is Real : r >= 0  }  ;
compatibility
 for b1 being Subset of REAL holds
( b1 = Real>=0 iff b1 =  {  r where r is Real : r >= 0  }  ) by REAL_1:1;
coherence
 Real>=0 is Subset of REAL by ARYTM_0:1;
end;

:: deftheorem  defines Real>=0 GRAPH_5:def_12_:_
 Real>=0 =  {  r where r is Real : r >= 0  }  ;

registration
cluster Real>=0  ->  non empty ;
coherence
 not Real>=0 is empty ;
end;

definition
let G be Graph;
let W be Function;
predW is_weight>=0of G means :Def13: :: GRAPH_5:def 13
W is Function of the carrier' of G,Real>=0;
end;

:: deftheorem Def13 defines is_weight>=0of GRAPH_5:def_13_:_
 for G being Graph
for W being Function holds
( W is_weight>=0of G iff W is Function of the carrier' of G,Real>=0 );

definition
let G be Graph;
let W be Function;
predW is_weight_of G means :Def14: :: GRAPH_5:def 14
W is Function of the carrier' of G,REAL;
end;

:: deftheorem Def14 defines is_weight_of GRAPH_5:def_14_:_
 for G being Graph
for W being Function holds
( W is_weight_of G iff W is Function of the carrier' of G,REAL );

definition
let G be Graph;
let p be FinSequence of the carrier' of G;
let W be Function;
assume A1: W is_weight_of G ;
func RealSequence (p,W) ->  FinSequence of REAL  means :Def15: :: GRAPH_5:def 15
( dom p = dom it &amp; ( for i being Element of NAT st i in dom p holds
it . i = W . (p . i) ) );
existence
 ex b1 being FinSequence of REAL st
( dom p = dom b1 &amp; ( for i being Element of NAT st i in dom p holds
b1 . i = W . (p . i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of REAL st dom p = dom b1 &amp; ( for i being Element of NAT st i in dom p holds
b1 . i = W . (p . i) ) &amp; dom p = dom b2 &amp; ( for i being Element of NAT st i in dom p holds
b2 . i = W . (p . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines RealSequence GRAPH_5:def_15_:_
 for G being Graph
for p being FinSequence of the carrier' of G
for W being Function st W is_weight_of G holds
for b4 being FinSequence of REAL holds
( b4 = RealSequence (p,W) iff ( dom p = dom b4 &amp; ( for i being Element of NAT st i in dom p holds
b4 . i = W . (p . i) ) ) );

definition
let G be Graph;
let p be FinSequence of the carrier' of G;
let W be Function;
func cost (p,W) ->  Real equals :: GRAPH_5:def 16
 Sum (RealSequence (p,W));
coherence
 Sum (RealSequence (p,W)) is Real ;
end;

:: deftheorem  defines cost GRAPH_5:def_16_:_
 for G being Graph
for p being FinSequence of the carrier' of G
for W being Function holds cost (p,W) = Sum (RealSequence (p,W));

theorem Th46: :: GRAPH_5:46
for W being Function
for G being Graph st W is_weight>=0of G holds
W is_weight_of G
proofend;

theorem Th47: :: GRAPH_5:47
for W being Function
for G being Graph
for pe being FinSequence of the carrier' of G
for f being FinSequence of REAL st W is_weight>=0of G &amp; f = RealSequence (pe,W) holds
for i being Element of NAT st i in dom f holds
f . i >= 0
proofend;

theorem Th48: :: GRAPH_5:48
for i being Element of NAT
for W being Function
for G being Graph
for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe &amp; W is_weight_of G &amp; i in dom qe holds
ex j being Element of NAT st
( j in dom pe &amp; (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i )
proofend;

Lm3:  for f being FinSequence of REAL holds
( ( for y being Real st y in rng f holds
y >= 0 ) iff for i being Nat st i in dom f holds
f . i >= 0 )
proofend;

Lm4:  for p, q, r being FinSequence of REAL st r = p ^ q &amp; ( for x being Real st x in rng r holds
x >= 0 ) holds
( ( for i being Element of NAT st i in dom p holds
p . i >= 0 ) &amp; ( for i being Element of NAT st i in dom q holds
q . i >= 0 ) )
proofend;

theorem :: GRAPH_5:49
for W being Function
for G being Graph
for qe, pe being FinSequence of the carrier' of G st len qe = 1 &amp; rng qe c= rng pe &amp; W is_weight>=0of G holds
cost (qe,W) <= cost (pe,W)
proofend;

theorem Th50: :: GRAPH_5:50
for W being Function
for G being Graph
for pe being FinSequence of the carrier' of G st W is_weight>=0of G holds
cost (pe,W) >= 0
proofend;

theorem Th51: :: GRAPH_5:51
for W being Function
for G being Graph
for pe being FinSequence of the carrier' of G st pe = {} &amp; W is_weight_of G holds
cost (pe,W) = 0
proofend;

theorem Th52: :: GRAPH_5:52
for W being Function
for G being Graph
for v1, v2 being Element of G
for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2) holds
ex pe being FinSequence of the carrier' of G st
( pe in D &amp; ( for qe being FinSequence of the carrier' of G st qe in D holds
cost (pe,W) <= cost (qe,W) ) )
proofend;

theorem Th53: :: GRAPH_5:53
for V being set
for W being Function
for G being Graph
for v1, v2 being Element of G
for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) holds
ex pe being FinSequence of the carrier' of G st
( pe in D &amp; ( for qe being FinSequence of the carrier' of G st qe in D holds
cost (pe,W) <= cost (qe,W) ) )
proofend;

theorem Th54: :: GRAPH_5:54
for W being Function
for G being Graph
for pe, qe being FinSequence of the carrier' of G st W is_weight_of G holds
cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W))
proofend;

theorem Th55: :: GRAPH_5:55
for W being Function
for G being Graph
for qe, pe being FinSequence of the carrier' of G st qe is one-to-one &amp; rng qe c= rng pe &amp; W is_weight>=0of G holds
cost (qe,W) <= cost (pe,W)
proofend;

theorem Th56: :: GRAPH_5:56
for W being Function
for G being Graph
for pe being FinSequence of the carrier' of G
for p being oriented Chain of G st pe in AcyclicPaths p &amp; W is_weight>=0of G holds
cost (pe,W) <= cost (p,W)
proofend;

begin

definition
let G be Graph;
let v1, v2 be Vertex of G;
let p be oriented Chain of G;
let W be Function;
predp is_shortestpath_of v1,v2,W means :Def17: :: GRAPH_5:def 17
( p is_orientedpath_of v1,v2 &amp; ( for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds
cost (p,W) <= cost (q,W) ) );
end;

:: deftheorem Def17 defines is_shortestpath_of GRAPH_5:def_17_:_
 for G being Graph
for v1, v2 being Vertex of G
for p being oriented Chain of G
for W being Function holds
( p is_shortestpath_of v1,v2,W iff ( p is_orientedpath_of v1,v2 &amp; ( for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds
cost (p,W) <= cost (q,W) ) ) );

definition
let G be Graph;
let v1, v2 be Vertex of G;
let p be oriented Chain of G;
let V be set ;
let W be Function;
predp is_shortestpath_of v1,v2,V,W means :Def18: :: GRAPH_5:def 18
( p is_orientedpath_of v1,v2,V &amp; ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds
cost (p,W) <= cost (q,W) ) );
end;

:: deftheorem Def18 defines is_shortestpath_of GRAPH_5:def_18_:_
 for G being Graph
for v1, v2 being Vertex of G
for p being oriented Chain of G
for V being set
for W being Function holds
( p is_shortestpath_of v1,v2,V,W iff ( p is_orientedpath_of v1,v2,V &amp; ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds
cost (p,W) <= cost (q,W) ) ) );

begin

theorem :: GRAPH_5:57
for G being finite Graph
for ps being oriented Simple Chain of G holds len ps <= VerticesCount G
proofend;

theorem Th58: :: GRAPH_5:58
for G being finite Graph
for ps being oriented Simple Chain of G holds len ps <= EdgesCount G
proofend;

Lm5:  for G being finite Graph holds AcyclicPaths G is finite
proofend;

registration
let G be finite Graph;
cluster AcyclicPaths G ->  finite ;
coherence
 AcyclicPaths G is finite by Lm5;
end;

Lm6:  for G being finite Graph
for P being oriented Chain of G holds AcyclicPaths P is finite
proofend;

Lm7:  for G being finite Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2) is finite
proofend;

Lm8:  for V being set
for G being finite Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) is finite
proofend;

registration
let G be finite Graph;
let P be oriented Chain of G;
cluster AcyclicPaths P ->  finite ;
coherence
 AcyclicPaths P is finite by Lm6;
end;

registration
let G be finite Graph;
let v1, v2 be Element of G;
cluster AcyclicPaths (v1,v2) ->  finite ;
coherence
 AcyclicPaths (v1,v2) is finite by Lm7;
end;

registration
let G be finite Graph;
let v1, v2 be Element of G;
let V be set ;
cluster AcyclicPaths (v1,v2,V) ->  finite ;
coherence
 AcyclicPaths (v1,v2,V) is finite by Lm8;
end;

theorem :: GRAPH_5:59
for W being Function
for G being finite Graph
for v1, v2 being Element of G st AcyclicPaths (v1,v2) <> {} holds
ex pe being FinSequence of the carrier' of G st
( pe in AcyclicPaths (v1,v2) &amp; ( for qe being FinSequence of the carrier' of G st qe in AcyclicPaths (v1,v2) holds
cost (pe,W) <= cost (qe,W) ) ) by Th52;

theorem :: GRAPH_5:60
for V being set
for W being Function
for G being finite Graph
for v1, v2 being Element of G st AcyclicPaths (v1,v2,V) <> {} holds
ex pe being FinSequence of the carrier' of G st
( pe in AcyclicPaths (v1,v2,V) &amp; ( for qe being FinSequence of the carrier' of G st qe in AcyclicPaths (v1,v2,V) holds
cost (pe,W) <= cost (qe,W) ) ) by Th53;

theorem :: GRAPH_5:61
for W being Function
for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of G st P is_orientedpath_of v1,v2 &amp; W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W
proofend;

theorem Th62: :: GRAPH_5:62
for V being set
for W being Function
for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V &amp; W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
proofend;

begin

theorem Th63: :: GRAPH_5:63
for V being set
for W being Function
for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of G st W is_weight>=0of G &amp; P is_shortestpath_of v1,v2,V,W &amp; v1 <> v2 &amp; ( for Q being oriented Chain of G
for v3 being Element of G st not v3 in V &amp; Q is_shortestpath_of v1,v3,V,W holds
cost (P,W) <= cost (Q,W) ) holds
P is_shortestpath_of v1,v2,W
proofend;

theorem :: GRAPH_5:64
for V, U being set
for W being Function
for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of G st W is_weight>=0of G &amp; P is_shortestpath_of v1,v2,V,W &amp; v1 <> v2 &amp; V c= U &amp; ( for Q being oriented Chain of G
for v3 being Element of G st not v3 in V &amp; Q is_shortestpath_of v1,v3,V,W holds
cost (P,W) <= cost (Q,W) ) holds
P is_shortestpath_of v1,v2,U,W
proofend;

definition
let G be Graph;
let pe be FinSequence of the carrier' of G;
let V be set ;
let v1 be Vertex of G;
let W be Function;
predpe islongestInShortestpath V,v1,W means :Def19: :: GRAPH_5:def 19
 for v being Vertex of G st v in V &amp; v <> v1 holds
ex q being oriented Chain of G st
( q is_shortestpath_of v1,v,V,W &amp; cost (q,W) <= cost (pe,W) );
end;

:: deftheorem Def19 defines islongestInShortestpath GRAPH_5:def_19_:_
 for G being Graph
for pe being FinSequence of the carrier' of G
for V being set
for v1 being Vertex of G
for W being Function holds
( pe islongestInShortestpath V,v1,W iff for v being Vertex of G st v in V &amp; v <> v1 holds
ex q being oriented Chain of G st
( q is_shortestpath_of v1,v,V,W &amp; cost (q,W) <= cost (pe,W) ) );

:: [WP: ] Dijkstra's_shortest_path_algorithm
theorem :: GRAPH_5:65
for e, V being set
for W being Function
for G being oriented finite Graph
for P, Q, R being oriented Chain of G
for v1, v2, v3 being Element of G st e in the carrier' of G &amp; W is_weight>=0of G &amp; len P >= 1 &amp; P is_shortestpath_of v1,v2,V,W &amp; v1 <> v2 &amp; v1 <> v3 &amp; R = P ^ <*e*> &amp; Q is_shortestpath_of v1,v3,V,W &amp; e orientedly_joins v2,v3 &amp; P islongestInShortestpath V,v1,W holds
( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) &amp; ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) )
proofend;