let e, V be 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 ) )
let W be 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 ) )
let G be 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 ) )
let P, Q, R be 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 ) )
let v1, v2, v3 be Element of G; ( 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 implies ( ( 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 ) ) )
assume that
A1:
e in the carrier' of G
and
A2:
W is_weight>=0of G
and
A3:
len P >= 1
and
A4:
P is_shortestpath_of v1,v2,V,W
and
A5:
v1 <> v2
and
A6:
v1 <> v3
and
A7:
R = P ^ <*e*>
and
A8:
Q is_shortestpath_of v1,v3,V,W
and
A9:
e orientedly_joins v2,v3
and
A10:
P islongestInShortestpath V,v1,W
; ( ( 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 ) )
A11:
P is_orientedpath_of v1,v2,V
by A4;
then A12:
v1 in V
by A5, Th29;
set Eg = the carrier' of G;
reconsider pe = <*e*> as FinSequence of the carrier' of G by A1, FINSEQ_1:74;
set V9 = V \/ {v2};
Q is_orientedpath_of v1,v3,V
by A8;
then A13:
Q is_orientedpath_of v1,v3,V \/ {v2}
by Th30, XBOOLE_1:7;
A14:
( len pe = 1 & pe . 1 = e )
by FINSEQ_1:40;
then consider s being oriented Simple Chain of G such that
A15:
s is_shortestpath_of v1,v3,V \/ {v2},W
by A2, A3, A7, A9, A11, Th32, Th60;
A16:
R is_orientedpath_of v1,v3,V \/ {v2}
by A3, A7, A9, A11, A14, Th32;
A17:
now ( cost (Q,W) <= cost (s,W) implies ( ( 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 ) ) )assume A18:
cost (
Q,
W)
<= cost (
s,
W)
;
( ( 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 ) )hereby ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W )
assume
cost (
Q,
W)
<= cost (
R,
W)
;
Q is_shortestpath_of v1,v3,V \/ {v2},Wnow for u being oriented Chain of G st u is_orientedpath_of v1,v3,V \/ {v2} holds
cost (Q,W) <= cost (u,W)let u be
oriented Chain of
G;
( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (Q,W) <= cost (u,W) )assume
u is_orientedpath_of v1,
v3,
V \/ {v2}
;
cost (Q,W) <= cost (u,W)then
cost (
s,
W)
<= cost (
u,
W)
by A15;
hence
cost (
Q,
W)
<= cost (
u,
W)
by A18, XXREAL_0:2;
verum end; hence
Q is_shortestpath_of v1,
v3,
V \/ {v2},
W
by A13;
verum
end; hereby verum
assume A19:
cost (
Q,
W)
>= cost (
R,
W)
;
R is_shortestpath_of v1,v3,V \/ {v2},Wnow for u being oriented Chain of G st u is_orientedpath_of v1,v3,V \/ {v2} holds
cost (R,W) <= cost (u,W)let u be
oriented Chain of
G;
( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (R,W) <= cost (u,W) )assume
u is_orientedpath_of v1,
v3,
V \/ {v2}
;
cost (R,W) <= cost (u,W)then
cost (
s,
W)
<= cost (
u,
W)
by A15;
then
cost (
Q,
W)
<= cost (
u,
W)
by A18, XXREAL_0:2;
hence
cost (
R,
W)
<= cost (
u,
W)
by A19, XXREAL_0:2;
verum end; hence
R is_shortestpath_of v1,
v3,
V \/ {v2},
W
by A16;
verum
end; end;
set FT = the Target of G;
set FS = the Source of G;
A20:
( the Source of G . e = v2 & the Target of G . e = v3 )
by A9, GRAPH_4:def 1;
A21:
s is_orientedpath_of v1,v3,V \/ {v2}
by A15;
then A22:
s is_orientedpath_of v1,v3
;
then A23:
the Target of G . (s . (len s)) = v3
;
s <> {}
by A22;
then A24:
len s >= 1
by FINSEQ_1:20;
per cases
( len s >= 2 or len s < 1 + 1 )
;
suppose
len s >= 2
;
( ( 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 ) )then consider k being
Nat such that A25:
len s = (1 + 1) + k
by NAT_1:10;
A26:
(V \/ {v2}) \ {v2} = V \ {v2}
by XBOOLE_1:40;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
A27:
len s = 1
+ (1 + k)
by A25;
then consider s1,
s2 being
FinSequence such that A28:
len s1 = 1
+ k
and A29:
len s2 = 1
and A30:
s = s1 ^ s2
by FINSEQ_2:22;
reconsider s1 =
s1,
s2 =
s2 as
oriented Simple Chain of
G by A30, Th12;
A31:
len s1 >= 1
by A28, NAT_1:12;
A32:
the
Source of
G . (s . 1) = v1
by A22;
then A33:
the
Source of
G . (s1 . 1) = v1
by A30, A31, Lm1;
len s2 = 1
by A29;
then A34:
not
v3 in vertices s1
by A6, A23, A30, A31, A32, Th16;
A35:
s2 . 1
= s . (len s)
by A27, A28, A29, A30, Lm2;
then A36:
(vertices s) \ {v3} =
((vertices s1) \/ {v3}) \ {v3}
by A23, A28, A29, A30, Th25, NAT_1:12
.=
(vertices s1) \ {v3}
by XBOOLE_1:40
.=
vertices s1
by A34, ZFMISC_1:57
;
then
vertices s1 c= V \/ {v2}
by A21;
then
(vertices s1) \ {v2} c= (V \/ {v2}) \ {v2}
by XBOOLE_1:33;
then A37:
(vertices s1) \ {v2} c= V
by A26, XBOOLE_1:1;
A38:
len s1 < len s
by A27, A28, NAT_1:13;
then A39:
the
Source of
G . (s . ((len s1) + 1)) = the
Target of
G . (s . (len s1))
by A31, GRAPH_1:def 15;
A40:
s1 . (len s1) = s . (len s1)
by A30, A31, Lm1;
then A41:
the
Source of
G . (s2 . 1) = the
Target of
G . (s1 . (len s1))
by A27, A28, A35, A31, A38, GRAPH_1:def 15;
A42:
cost (
s,
W)
= (cost (s1,W)) + (cost (s2,W))
by A2, A30, Th44, Th52;
A43:
not
v1 in vertices s2
by A6, A23, A29, A30, A31, A32, Th16;
hereby verum
per cases
( v2 in vertices s1 or not v2 in vertices s1 )
;
suppose
v2 in vertices s1
;
( ( 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 ) )then consider i being
Nat such that A44:
1
<= i
and A45:
i <= len s1
and A46:
v2 = the
Target of
G . (s1 . i)
by A5, A33, Th26;
s2 /. 1
in the
carrier' of
G
by A1;
then A47:
s2 . 1
in the
carrier' of
G
by A29, FINSEQ_4:15;
hereby verum
per cases
( the Source of G . (s2 . 1) = v2 or the Source of G . (s2 . 1) <> v2 )
;
suppose A48:
the
Source of
G . (s2 . 1) = v2
;
( ( 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 ) )
s1 <> {}
by A28;
then
s1 is_orientedpath_of v1,
v2
by A33, A41, A48;
then
s1 is_orientedpath_of v1,
v2,
V
by A37;
then A49:
cost (
P,
W)
<= cost (
s1,
W)
by A4;
s2 . 1
= e
by A1, A23, A20, A35, A47, A48, GRAPH_1:def 7;
then
s2 = pe
by A29, FINSEQ_1:40;
then
cost (
R,
W)
= (cost (P,W)) + (cost (s2,W))
by A2, A7, Th44, Th52;
then A50:
cost (
R,
W)
<= cost (
s,
W)
by A42, A49, XREAL_1:7;
hereby ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W )
assume
cost (
Q,
W)
<= cost (
R,
W)
;
Q is_shortestpath_of v1,v3,V \/ {v2},Wthen A51:
cost (
Q,
W)
<= cost (
s,
W)
by A50, XXREAL_0:2;
now for u being oriented Chain of G st u is_orientedpath_of v1,v3,V \/ {v2} holds
cost (Q,W) <= cost (u,W)let u be
oriented Chain of
G;
( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (Q,W) <= cost (u,W) )assume
u is_orientedpath_of v1,
v3,
V \/ {v2}
;
cost (Q,W) <= cost (u,W)then
cost (
s,
W)
<= cost (
u,
W)
by A15;
hence
cost (
Q,
W)
<= cost (
u,
W)
by A51, XXREAL_0:2;
verum end; hence
Q is_shortestpath_of v1,
v3,
V \/ {v2},
W
by A13;
verum
end; hereby verum
assume
cost (
Q,
W)
>= cost (
R,
W)
;
R is_shortestpath_of v1,v3,V \/ {v2},Wnow for u being oriented Chain of G st u is_orientedpath_of v1,v3,V \/ {v2} holds
cost (R,W) <= cost (u,W)let u be
oriented Chain of
G;
( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (R,W) <= cost (u,W) )assume
u is_orientedpath_of v1,
v3,
V \/ {v2}
;
cost (R,W) <= cost (u,W)then
cost (
s,
W)
<= cost (
u,
W)
by A15;
hence
cost (
R,
W)
<= cost (
u,
W)
by A50, XXREAL_0:2;
verum end; hence
R is_shortestpath_of v1,
v3,
V \/ {v2},
W
by A16;
verum
end; end; suppose A52:
the
Source of
G . (s2 . 1) <> v2
;
( ( 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 ) )
len s1 in dom s1
by A31, FINSEQ_3:25;
then reconsider vx = the
Target of
G . (s1 . (len s1)) as
Vertex of
G by FINSEQ_2:11, FUNCT_2:5;
A53:
not
vx in {v2}
by A41, A52, TARSKI:def 1;
len s1 in dom s1
by A31, FINSEQ_3:25;
then A54:
vx in vertices s1
by Th22;
vertices s1 c= V \/ {v2}
by A21, A36;
then A55:
vx in V
by A54, A53, XBOOLE_0:def 3;
{vx} c= V
by A55, TARSKI:def 1;
then A56:
V \/ {vx} c= V
by XBOOLE_1:8;
1
in dom s2
by A29, FINSEQ_3:25;
then
vx <> v1
by A25, A28, A35, A40, A43, A39, Th22;
then consider q9 being
oriented Chain of
G such that A57:
q9 is_shortestpath_of v1,
vx,
V,
W
and A58:
cost (
q9,
W)
<= cost (
P,
W)
by A10, A55;
consider j being
Nat such that A59:
len s1 = i + j
by A45, NAT_1:10;
A60:
q9 is_orientedpath_of v1,
vx,
V
by A57;
then A61:
q9 is_orientedpath_of v1,
vx
;
then
q9 <> {}
;
then A62:
len q9 >= 1
by FINSEQ_1:20;
the
Target of
G . (q9 . (len q9)) = vx
by A61;
then reconsider qx =
q9 ^ s2 as
oriented Chain of
G by A25, A28, A35, A40, A39, Th10;
len qx = (len q9) + 1
by A29, FINSEQ_1:22;
then A63:
(
qx <> {} & the
Target of
G . (qx . (len qx)) = v3 )
by A23, A29, A35, Lm2;
the
Source of
G . (q9 . 1) = v1
by A61;
then
the
Source of
G . (qx . 1) = v1
by A62, Lm1;
then A64:
qx is_orientedpath_of v1,
v3
by A63;
(vertices q9) \ {vx} c= V
by A60;
then
vertices q9 c= V \/ {vx}
by XBOOLE_1:44;
then
vertices q9 c= V
by A56;
then A65:
(vertices q9) \ {v3} c= V \ {v3}
by XBOOLE_1:33;
vertices qx = (vertices q9) \/ {v3}
by A23, A29, A35, A62, Th25;
then
(vertices qx) \ {v3} = (vertices q9) \ {v3}
by XBOOLE_1:40;
then
(vertices qx) \ {v3} c= V
by A65, XBOOLE_1:1;
then
qx is_orientedpath_of v1,
v3,
V
by A64;
then A66:
cost (
Q,
W)
<= cost (
qx,
W)
by A8;
reconsider j =
j as
Element of
NAT by ORDINAL1:def 12;
consider t1,
t2 being
FinSequence such that A67:
len t1 = i
and
len t2 = j
and A68:
s1 = t1 ^ t2
by A59, FINSEQ_2:22;
reconsider t1 =
t1,
t2 =
t2 as
oriented Simple Chain of
G by A68, Th12;
A69:
the
Target of
G . (t1 . (len t1)) = v2
by A44, A46, A67, A68, Lm1;
vertices t1 c= vertices (t1 ^ t2)
by Th24;
then
(vertices t1) \ {v2} c= (vertices s1) \ {v2}
by A68, XBOOLE_1:33;
then A70:
(vertices t1) \ {v2} c= V
by A37;
(
t1 <> {} & the
Source of
G . (t1 . 1) = v1 )
by A33, A44, A67, A68, Lm1;
then
t1 is_orientedpath_of v1,
v2
by A69;
then
t1 is_orientedpath_of v1,
v2,
V
by A70;
then A71:
cost (
P,
W)
<= cost (
t1,
W)
by A4;
A72:
cost (
t2,
W)
>= 0
by A2, Th48;
cost (
s1,
W)
= (cost (t1,W)) + (cost (t2,W))
by A2, A68, Th44, Th52;
then
(cost (t1,W)) + 0 <= cost (
s1,
W)
by A72, XREAL_1:7;
then
cost (
P,
W)
<= cost (
s1,
W)
by A71, XXREAL_0:2;
then A73:
cost (
q9,
W)
<= cost (
s1,
W)
by A58, XXREAL_0:2;
cost (
qx,
W)
= (cost (q9,W)) + (cost (s2,W))
by A2, Th44, Th52;
then
cost (
qx,
W)
<= cost (
s,
W)
by A42, A73, XREAL_1:7;
then A74:
cost (
Q,
W)
<= cost (
s,
W)
by A66, XXREAL_0:2;
hereby ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W )
assume
cost (
Q,
W)
<= cost (
R,
W)
;
Q is_shortestpath_of v1,v3,V \/ {v2},Wnow for u being oriented Chain of G st u is_orientedpath_of v1,v3,V \/ {v2} holds
cost (Q,W) <= cost (u,W)let u be
oriented Chain of
G;
( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (Q,W) <= cost (u,W) )assume
u is_orientedpath_of v1,
v3,
V \/ {v2}
;
cost (Q,W) <= cost (u,W)then
cost (
s,
W)
<= cost (
u,
W)
by A15;
hence
cost (
Q,
W)
<= cost (
u,
W)
by A74, XXREAL_0:2;
verum end; hence
Q is_shortestpath_of v1,
v3,
V \/ {v2},
W
by A13;
verum
end; hereby verum
assume
cost (
Q,
W)
>= cost (
R,
W)
;
R is_shortestpath_of v1,v3,V \/ {v2},Wthen A75:
cost (
R,
W)
<= cost (
s,
W)
by A74, XXREAL_0:2;
now for u being oriented Chain of G st u is_orientedpath_of v1,v3,V \/ {v2} holds
cost (R,W) <= cost (u,W)let u be
oriented Chain of
G;
( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (R,W) <= cost (u,W) )assume
u is_orientedpath_of v1,
v3,
V \/ {v2}
;
cost (R,W) <= cost (u,W)then
cost (
s,
W)
<= cost (
u,
W)
by A15;
hence
cost (
R,
W)
<= cost (
u,
W)
by A75, XXREAL_0:2;
verum end; hence
R is_shortestpath_of v1,
v3,
V \/ {v2},
W
by A16;
verum
end; end; end; suppose
not
v2 in vertices s1
;
( ( 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 ) )then A76:
(vertices s1) \ {v2} = vertices s1
by ZFMISC_1:57;
then
(vertices s1) \ {v2} c= V \/ {v2}
by A21, A36;
then
(vertices s) \ {v3} c= V
by A36, A76, XBOOLE_1:43;
then
s is_orientedpath_of v1,
v3,
V
by A22;
hence
( (
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 ) )
by A8, A17;
verum end; end; suppose
len s < 1
+ 1
;
( ( 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 ) )then A77:
len s <= 1
by NAT_1:13;
then A78:
len s = 1
by A24, XXREAL_0:1;
A79:
vertices s = vertices (s /. 1)
by A24, A77, Th23, XXREAL_0:1;
(vertices s) \ {v3} c= V
then
s is_orientedpath_of v1,
v3,
V
by A22;
hence
( (
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 ) )
by A8, A17;
verum end;