let V be 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
let W be 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
let G be 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
let P be 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
let v1, v2 be Element of G; ( 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) ) implies P is_shortestpath_of v1,v2,W )
assume that
A1:
W is_weight>=0of G
and
A2:
P is_shortestpath_of v1,v2,V,W
and
A3:
v1 <> v2
and
A4:
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)
; P is_shortestpath_of v1,v2,W
A5:
P is_orientedpath_of v1,v2,V
by A2;
then A6:
v1 in V
by A3, Th29;
A7:
now for r being oriented Chain of G st r is_orientedpath_of v1,v2 holds
cost (P,W) <= cost (r,W)let r be
oriented Chain of
G;
( r is_orientedpath_of v1,v2 implies cost (P,W) <= cost (b1,W) )assume A8:
r is_orientedpath_of v1,
v2
;
cost (P,W) <= cost (b1,W)per cases
( not vertices r c= V or vertices r c= V )
;
suppose A9:
not
vertices r c= V
;
cost (P,W) <= cost (b1,W)set FT = the
Target of
G;
set FS = the
Source of
G;
consider i being
Element of
NAT ,
s,
t being
FinSequence of the
carrier' of
G such that A10:
i + 1
<= len r
and A11:
not
vertices (r /. (i + 1)) c= V
and A12:
len s = i
and A13:
r = s ^ t
and A14:
vertices s c= V
by A9, Th18;
i + 1
<= (len s) + (len t)
by A10, A13, FINSEQ_1:22;
then A15:
1
<= len t
by A12, XREAL_1:6;
then consider j being
Nat such that A16:
len t = 1
+ j
by NAT_1:10;
reconsider s =
s,
t =
t as
oriented Chain of
G by A13, Th9;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 12;
consider t1,
t2 being
FinSequence such that A17:
len t1 = 1
and
len t2 = j
and A18:
t = t1 ^ t2
by A16, FINSEQ_2:22;
reconsider t1 =
t1,
t2 =
t2 as
oriented Chain of
G by A18, Th9;
A19:
r . (i + 1) =
t . 1
by A12, A13, A15, Lm2
.=
t1 . 1
by A17, A18, Lm1
;
A20:
cost (
t2,
W)
>= 0
by A1, Th48;
A21:
r = (s ^ t1) ^ t2
by A13, A18, FINSEQ_1:32;
then
cost (
r,
W)
= (cost ((s ^ t1),W)) + (cost (t2,W))
by A1, Th44, Th52;
then A22:
cost (
r,
W)
>= (cost ((s ^ t1),W)) + 0
by A20, XREAL_1:7;
set e =
r /. (i + 1);
A23:
r /. (i + 1) = r . (i + 1)
by A10, FINSEQ_4:15, NAT_1:11;
consider x being
object such that A24:
x in vertices (r /. (i + 1))
and A25:
not
x in V
by A11;
A26:
(
x = the
Source of
G . (r /. (i + 1)) or
x = the
Target of
G . (r /. (i + 1)) )
by A24, TARSKI:def 2;
1
in dom t1
by A17, FINSEQ_3:25;
then reconsider v3 =
x as
Vertex of
G by A23, A19, A26, FINSEQ_2:11, FUNCT_2:5;
A27:
v1 = the
Source of
G . (r . 1)
by A8;
hereby verum
per cases
( i = 0 or i <> 0 )
;
suppose A28:
i = 0
;
cost (P,W) <= cost (r,W)then A29:
the
Source of
G . (t1 . 1) = v1
by A8, A19;
A30:
(vertices t1) \ {v3} c= V
proof
let x be
object ;
TARSKI:def 3 ( not x in (vertices t1) \ {v3} or x in V )
assume A31:
x in (vertices t1) \ {v3}
;
x in V
then A32:
not
x in {v3}
by XBOOLE_0:def 5;
x in vertices t1
by A31, XBOOLE_0:def 5;
then
x in vertices (t1 /. 1)
by A17, Th23;
then A33:
(
x = the
Source of
G . (t1 /. 1) or
x = the
Target of
G . (t1 /. 1) )
by TARSKI:def 2;
the
Target of
G . (t1 /. 1) = v3
by A3, A5, A17, A23, A19, A25, A26, A27, A28, Th29, FINSEQ_4:15;
hence
x in V
by A6, A17, A29, A32, A33, FINSEQ_4:15, TARSKI:def 1;
verum
end;
v1 = the
Source of
G . (r /. (i + 1))
by A8, A23, A28;
then
t1 is_orientedpath_of v1,
v3
by A3, A5, A17, A23, A19, A25, A26, Th29;
then A34:
t1 is_orientedpath_of v1,
v3,
V
by A30;
then consider q being
oriented Simple Chain of
G such that A35:
q is_shortestpath_of v1,
v3,
V,
W
by A1, Th60;
s = {}
by A12, A28;
then A36:
s ^ t1 = t1
by FINSEQ_1:34;
A37:
cost (
q,
W)
<= cost (
t1,
W)
by A34, A35;
cost (
P,
W)
<= cost (
q,
W)
by A4, A25, A35;
then
cost (
P,
W)
<= cost (
t1,
W)
by A37, XXREAL_0:2;
hence
cost (
P,
W)
<= cost (
r,
W)
by A22, A36, XXREAL_0:2;
verum end; suppose A38:
i <> 0
;
cost (P,W) <= cost (r,W)reconsider u =
s ^ t1 as
oriented Chain of
G by A21, Th9;
A39:
i < len r
by A10, NAT_1:13;
i + 1
> 0 + 1
by A38, XREAL_1:8;
then A40:
i >= 1
by NAT_1:13;
then A41:
i in dom s
by A12, FINSEQ_3:25;
A44:
(vertices u) \ {v3} c= V
proof
set V3 =
{( the Target of G . (t1 . 1))};
let x be
object ;
TARSKI:def 3 ( not x in (vertices u) \ {v3} or x in V )
assume A45:
x in (vertices u) \ {v3}
;
x in V
then A46:
x in vertices u
by XBOOLE_0:def 5;
vertices u = (vertices s) \/ {( the Target of G . (t1 . 1))}
by A12, A17, A40, Th25;
then A47:
(
x in vertices s or
x in {( the Target of G . (t1 . 1))} )
by A46, XBOOLE_0:def 3;
not
x in {v3}
by A45, XBOOLE_0:def 5;
hence
x in V
by A10, A14, A19, A26, A42, A47, FINSEQ_4:15, NAT_1:11;
verum
end;
len u = (len s) + (len t1)
by FINSEQ_1:22;
then A48:
(
u <> {} &
u . (len u) = t1 . 1 )
by A17, Lm2;
u . 1 =
s . 1
by A12, A40, Lm1
.=
r . 1
by A12, A13, A40, Lm1
;
then
the
Source of
G . (u . 1) = v1
by A8;
then
u is_orientedpath_of v1,
v3
by A23, A19, A26, A42, A48;
then A49:
u is_orientedpath_of v1,
v3,
V
by A44;
then consider q being
oriented Simple Chain of
G such that A50:
q is_shortestpath_of v1,
v3,
V,
W
by A1, Th60;
A51:
cost (
q,
W)
<= cost (
u,
W)
by A49, A50;
cost (
P,
W)
<= cost (
q,
W)
by A4, A25, A50;
then
cost (
P,
W)
<= cost (
u,
W)
by A51, XXREAL_0:2;
hence
cost (
P,
W)
<= cost (
r,
W)
by A22, XXREAL_0:2;
verum end; end; end;
P is_orientedpath_of v1,v2
by A5;
hence
P is_shortestpath_of v1,v2,W
by A7; verum