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, Def18;
then A6:
v1 in V
by A3, Th35;
A7:
now 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,Wper cases
( not vertices r c= V or vertices r c= V )
;
suppose A9:
not
vertices r c= V
;
cost P,W <= cost b1,Wset 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, Th23;
i + 1
<= (len s) + (len t)
by A10, A13, FINSEQ_1:35;
then A15:
1
<= len t
by A12, XREAL_1:8;
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, Th14;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 13;
consider t1,
t2 being
FinSequence such that A17:
len t1 = 1
and
len t2 = j
and A18:
t = t1 ^ t2
by A16, FINSEQ_2:25;
reconsider t1 =
t1,
t2 =
t2 as
oriented Chain of
G by A18, Th14;
A19:
r . (i + 1) =
t . 1
by A12, A13, A15, Lm2
.=
t1 . 1
by A17, A18, Lm1
;
A20:
cost t2,
W >= 0
by A1, Th54;
A21:
r = (s ^ t1) ^ t2
by A13, A18, FINSEQ_1:45;
then
cost r,
W = (cost (s ^ t1),W) + (cost t2,W)
by A1, Th50, Th58;
then A22:
cost r,
W >= (cost (s ^ t1),W) + 0
by A20, XREAL_1:9;
set e =
r /. (i + 1);
A23:
r /. (i + 1) = r . (i + 1)
by A10, FINSEQ_4:24, NAT_1:11;
consider x being
set such that A24:
x in vertices (r /. (i + 1))
and A25:
not
x in V
by A11, TARSKI:def 3;
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:27;
then reconsider v3 =
x as
Vertex of
G by A23, A19, A26, FINSEQ_2:13, FUNCT_2:7;
A27:
v1 = the
Source of
G . (r . 1)
by A8, Def3;
hereby verum
per cases
( i = 0 or i <> 0 )
;
suppose A28:
i = 0
;
cost P,W <= cost r,Wthen A29:
the
Source of
G . (t1 . 1) = v1
by A8, A19, Def3;
A30:
(vertices t1) \ {v3} c= V
proof
let x be
set ;
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, Th29;
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, Th35, FINSEQ_4:24;
hence
x in V
by A6, A17, A29, A32, A33, FINSEQ_4:24, TARSKI:def 1;
verum
end; A34:
t1 <> {}
by A17;
v1 = the
Source of
G . (r /. (i + 1))
by A8, A23, A28, Def3;
then
t1 is_orientedpath_of v1,
v3
by A3, A5, A17, A23, A19, A25, A26, A34, Def3, Th35;
then A35:
t1 is_orientedpath_of v1,
v3,
V
by A30, Def4;
then consider q being
oriented Simple Chain of
G such that A36:
q is_shortestpath_of v1,
v3,
V,
W
by A1, Th66;
s = {}
by A12, A28;
then A37:
s ^ t1 = t1
by FINSEQ_1:47;
A38:
cost q,
W <= cost t1,
W
by A35, A36, Def18;
cost P,
W <= cost q,
W
by A4, A25, A36;
then
cost P,
W <= cost t1,
W
by A38, XXREAL_0:2;
hence
cost P,
W <= cost r,
W
by A22, A37, XXREAL_0:2;
verum end; suppose A39:
i <> 0
;
cost P,W <= cost r,Wreconsider u =
s ^ t1 as
oriented Chain of
G by A21, Th14;
A40:
i < len r
by A10, NAT_1:13;
i + 1
> 0 + 1
by A39, XREAL_1:10;
then A41:
i >= 1
by NAT_1:13;
then A42:
i in dom s
by A12, FINSEQ_3:27;
A45:
(vertices u) \ {v3} c= V
proof
set V3 =
{(the Target of G . (t1 . 1))};
let x be
set ;
TARSKI:def 3 ( not x in (vertices u) \ {v3} or x in V )
assume A46:
x in (vertices u) \ {v3}
;
x in V
then A47:
x in vertices u
by XBOOLE_0:def 5;
vertices u = (vertices s) \/ {(the Target of G . (t1 . 1))}
by A12, A17, A41, Th31;
then A48:
(
x in vertices s or
x in {(the Target of G . (t1 . 1))} )
by A47, XBOOLE_0:def 3;
not
x in {v3}
by A46, XBOOLE_0:def 5;
hence
x in V
by A10, A14, A19, A26, A43, A48, FINSEQ_4:24, NAT_1:11;
verum
end;
len u = (len s) + (len t1)
by FINSEQ_1:35;
then A49:
(
u <> {} &
u . (len u) = t1 . 1 )
by A17, Lm2;
u . 1 =
s . 1
by A12, A41, Lm1
.=
r . 1
by A12, A13, A41, Lm1
;
then
the
Source of
G . (u . 1) = v1
by A8, Def3;
then
u is_orientedpath_of v1,
v3
by A23, A19, A26, A43, A49, Def3;
then A50:
u is_orientedpath_of v1,
v3,
V
by A45, Def4;
then consider q being
oriented Simple Chain of
G such that A51:
q is_shortestpath_of v1,
v3,
V,
W
by A1, Th66;
A52:
cost q,
W <= cost u,
W
by A50, A51, Def18;
cost P,
W <= cost q,
W
by A4, A25, A51;
then
cost P,
W <= cost u,
W
by A52, 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, Def4;
hence
P is_shortestpath_of v1,v2,W
by A7, Def17; verum