let W be Function; :: thesis: for V being set
for G being finite Graph
for P, Q being oriented Chain of G
for v1, v2, v3 being Vertex of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
let V be set ; :: thesis: for G being finite Graph
for P, Q being oriented Chain of G
for v1, v2, v3 being Vertex of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
let G be finite Graph; :: thesis: for P, Q being oriented Chain of G
for v1, v2, v3 being Vertex of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
let P, Q be oriented Chain of G; :: thesis: for v1, v2, v3 being Vertex of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
let v1, v2, v3 be Vertex of G; :: thesis: ( W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W implies Q is_shortestpath_of v1,v3,V \/ {v2},W )
assume A1:
( W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & ( for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W )
; :: thesis: Q is_shortestpath_of v1,v3,V \/ {v2},W
set V' = V \/ {v2};
set FS = the Source of G;
set FT = the Target of G;
A2:
W is_weight_of G
by A1, GRAPH_5:50;
A3:
now let S be
oriented Chain of
G;
:: thesis: ( S is_orientedpath_of v1,v3,V \/ {v2} implies cost Q,W <= cost b1,W )assume A4:
S is_orientedpath_of v1,
v3,
V \/ {v2}
;
:: thesis: cost Q,W <= cost b1,Wthen consider s being
oriented Simple Chain of
G such that A5:
s is_shortestpath_of v1,
v3,
V \/ {v2},
W
by A1, GRAPH_5:66;
A6:
s is_orientedpath_of v1,
v3,
V \/ {v2}
by A5, GRAPH_5:def 18;
then A7:
s is_orientedpath_of v1,
v3
by GRAPH_5:def 4;
then
s <> {}
by GRAPH_5:def 3;
then
len s >= 1
by FINSEQ_1:28;
then consider i being
Nat such that A8:
len s = 1
+ i
by NAT_1:10;
consider s1,
s2 being
FinSequence such that A9:
(
len s1 = i &
len s2 = 1 &
s = s1 ^ s2 )
by A8, FINSEQ_2:25;
reconsider s1 =
s1,
s2 =
s2 as
oriented Simple Chain of
G by A9, GRAPH_5:17;
A10:
s2 . 1
= s . (len s)
by A8, A9, Lm2;
A11:
( the
Source of
G . (s . 1) = v1 & the
Target of
G . (s . (len s)) = v3 )
by A7, GRAPH_5:def 3;
reconsider vx = the
Source of
G . (s2 . 1) as
Vertex of
G by A9, Lm3;
A14:
(vertices s) \ {v3} c= V \/ {v2}
by A6, GRAPH_5:def 4;
A15:
cost s,
W <= cost S,
W
by A4, A5, GRAPH_5:def 18;
per cases
( not v2 in vertices s or v2 = v3 or ( v2 in vertices s & v2 <> v3 ) )
;
suppose A16:
( not
v2 in vertices s or
v2 = v3 )
;
:: thesis: cost Q,W <= cost b1,Wset Vs =
vertices s;
((vertices s) \ {v3}) \ {v2} c= V
by A14, XBOOLE_1:43;
then A17:
(vertices s) \ ({v3} \/ {v2}) c= V
by XBOOLE_1:41;
then
s is_orientedpath_of v1,
v3,
V
by A7, GRAPH_5:def 4;
then
cost Q,
W <= cost s,
W
by A1, GRAPH_5:def 18;
hence
cost Q,
W <= cost S,
W
by A15, XXREAL_0:2;
:: thesis: verum end; suppose A19:
(
v2 in vertices s &
v2 <> v3 )
;
:: thesis: cost Q,W <= cost b1,Wthen consider j being
Element of
NAT such that A20:
( 1
<= j &
j <= len s &
v2 = the
Target of
G . (s . j) )
by A1, A11, GRAPH_5:32;
len s1 <> 0
by A8, A9, A11, A19, A20, XXREAL_0:1;
then
len s1 > 0
;
then A21:
len s1 >= 0 + 1
by INT_1:20;
A22:
len s1 < len s
by A8, A9, NAT_1:13;
A23:
vx =
the
Source of
G . (s . ((len s1) + 1))
by A9, Lm2
.=
the
Target of
G . (s . (len s1))
by A21, A22, GRAPH_1:def 13
;
then consider k being
Nat such that A25:
len s1 = j + k
by NAT_1:10;
consider t1,
t2 being
FinSequence such that A26:
(
len t1 = j &
len t2 = k &
s1 = t1 ^ t2 )
by A25, FINSEQ_2:25;
reconsider t1 =
t1,
t2 =
t2 as
oriented Simple Chain of
G by A26, GRAPH_5:17;
A27: the
Source of
G . (t1 . 1) =
the
Source of
G . (s1 . 1)
by A20, A26, Lm1
.=
v1
by A9, A11, A21, Lm1
;
A28:
t1 <> {}
by A20, A26;
the
Target of
G . (t1 . (len t1)) =
the
Target of
G . (s1 . j)
by A20, A26, Lm1
.=
v2
by A9, A20, A24, Lm1
;
then A29:
t1 is_orientedpath_of v1,
v2
by A27, A28, GRAPH_5:def 3;
A30:
len s2 >= 1
by A9;
then A31:
not
v3 in vertices s1
by A1, A9, A11, A21, GRAPH_5:21;
set Vt =
vertices t1;
vertices t1 c= vertices (t1 ^ t2)
by GRAPH_5:30;
then A32:
not
v3 in vertices t1
by A1, A9, A11, A21, A26, A30, GRAPH_5:21;
(vertices (s1 ^ s2)) \ {v3} c= V \/ {v2}
by A6, A9, GRAPH_5:def 4;
then A33:
(vertices (t1 ^ t2)) \ {v3} c= V \/ {v2}
by A26, GRAPH_5:26;
then
(vertices t1) \ {v3} c= V \/ {v2}
by GRAPH_5:26;
then
vertices t1 c= V \/ {v2}
by A32, ZFMISC_1:65;
then
(vertices t1) \ {v2} c= V
by XBOOLE_1:43;
then
t1 is_orientedpath_of v1,
v2,
V
by A29, GRAPH_5:def 4;
then A34:
cost P,
W <= cost t1,
W
by A1, GRAPH_5:def 18;
vx = the
Target of
G . (s1 . (len s1))
by A9, A21, A23, Lm1;
then A35:
vx in vertices s1
by A21, Lm4;
not
vx in {v2}
by A12, TARSKI:def 1;
then A36:
vx in (vertices s1) \ {v2}
by A35, XBOOLE_0:def 5;
vertices s1 c= V \/ {v2}
by A26, A31, A33, ZFMISC_1:65;
then A37:
(vertices s1) \ {v2} c= V
by XBOOLE_1:43;
not
v1 in vertices s2
by A1, A9, A11, A21, GRAPH_5:21;
then
vx <> v1
by A9, Lm4;
then consider q being
oriented Chain of
G such that A38:
(
q is_shortestpath_of v1,
vx,
V,
W &
cost q,
W <= cost P,
W )
by A1, A36, A37, GRAPH_5:def 19;
A39:
q is_orientedpath_of v1,
vx,
V
by A38, GRAPH_5:def 18;
A40:
s2 . 1
orientedly_joins vx,
v3
by A10, A11, GRAPH_4:def 1;
A41:
q is_orientedpath_of v1,
vx
by A39, GRAPH_5:def 4;
then
q <> {}
by GRAPH_5:def 3;
then A42:
len q >= 1
by FINSEQ_1:28;
then consider p being
oriented Chain of
G such that A43:
(
p = q ^ s2 &
p is_orientedpath_of v1,
v3 )
by A9, A40, A41, GRAPH_5:37;
p is_orientedpath_of v1,
v3,
V \/ {vx}
by A9, A39, A40, A42, A43, GRAPH_5:38;
then
p is_orientedpath_of v1,
v3,
V
by A36, A37, ZFMISC_1:46;
then
cost Q,
W <= cost p,
W
by A1, GRAPH_5:def 18;
then A44:
cost Q,
W <= (cost q,W) + (cost s2,W)
by A2, A43, GRAPH_5:58;
A45:
cost q,
W <= cost t1,
W
by A34, A38, XXREAL_0:2;
A46:
cost s1,
W = (cost t1,W) + (cost t2,W)
by A2, A26, GRAPH_5:58;
0 <= cost t2,
W
by A1, GRAPH_5:54;
then
0 + (cost t1,W) <= cost s1,
W
by A46, XREAL_1:9;
then A47:
cost q,
W <= cost s1,
W
by A45, XXREAL_0:2;
cost s,
W = (cost s1,W) + (cost s2,W)
by A2, A9, GRAPH_5:58;
then
(cost q,W) + (cost s2,W) <= cost s,
W
by A47, XREAL_1:9;
then
cost Q,
W <= cost s,
W
by A44, XXREAL_0:2;
hence
cost Q,
W <= cost S,
W
by A15, XXREAL_0:2;
:: thesis: verum end; end;
Q is_orientedpath_of v1,v3,V
by A1, GRAPH_5:def 18;
then
Q is_orientedpath_of v1,v3,V \/ {v2}
by GRAPH_5:36, XBOOLE_1:7;
hence
Q is_shortestpath_of v1,v3,V \/ {v2},W
by A3, GRAPH_5:def 18; :: thesis: verum