begin
begin
Lm1:
for n being Element of NAT
for p, q being FinSequence st 1 <= n & n <= len p holds
p . n = (p ^ q) . n
Lm2:
for n being Element of NAT
for q, p being FinSequence st 1 <= n & n <= len q holds
q . n = (p ^ q) . ((len p) + n)
begin
begin
begin
begin
begin
begin
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 )
Lm4:
for p, q, r being FinSequence of REAL st r = p ^ q & ( 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 ) & ( for i being Element of NAT st i in dom q holds
q . i >= 0 ) )
begin
::
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 & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds
cost (p,W) <= cost (q,W) ) ) );
begin
Lm5:
for G being finite Graph holds AcyclicPaths G is finite
Lm6:
for G being finite Graph
for P being oriented Chain of G holds AcyclicPaths P is finite
Lm7:
for G being finite Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2) is finite
Lm8:
for V being set
for G being finite Graph
for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) is finite
begin
theorem Th63:
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 &
P is_shortestpath_of v1,
v2,
V,
W &
v1 <> v2 & ( for
Q being
oriented Chain of
G for
v3 being
Element of
G st not
v3 in V &
Q is_shortestpath_of v1,
v3,
V,
W holds
cost (
P,
W)
<= cost (
Q,
W) ) holds
P is_shortestpath_of v1,
v2,
W
theorem
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 &
P is_shortestpath_of v1,
v2,
V,
W &
v1 <> v2 &
V c= U & ( for
Q being
oriented Chain of
G for
v3 being
Element of
G st not
v3 in V &
Q is_shortestpath_of v1,
v3,
V,
W holds
cost (
P,
W)
<= cost (
Q,
W) ) holds
P is_shortestpath_of v1,
v2,
U,
W
theorem
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 &
W is_weight>=0of G &
len P >= 1 &
P is_shortestpath_of v1,
v2,
V,
W &
v1 <> v2 &
v1 <> v3 &
R = P ^ <*e*> &
Q is_shortestpath_of v1,
v3,
V,
W &
e orientedly_joins v2,
v3 &
P islongestInShortestpath V,
v1,
W holds
( (
cost (
Q,
W)
<= cost (
R,
W) implies
Q is_shortestpath_of v1,
v3,
V \/ {v2},
W ) & (
cost (
Q,
W)
>= cost (
R,
W) implies
R is_shortestpath_of v1,
v3,
V \/ {v2},
W ) )