let W be Function; 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 ; 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; 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; 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; ( 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 that
A1:
W is_weight>=0of G
and
A2:
P is_shortestpath_of v1,v2,V,W
and
A3:
v1 <> v2
and
A4:
v1 <> v3
and
A5:
Q is_shortestpath_of v1,v3,V,W
and
A6:
for e being set holds
( not e in the carrier' of G or not e orientedly_joins v2,v3 )
and
A7:
P islongestInShortestpath V,v1,W
; Q is_shortestpath_of v1,v3,V \/ {v2},W
set V9 = V \/ {v2};
set FS = the Source of G;
set FT = the Target of G;
A8:
now for S being oriented Chain of G st S is_orientedpath_of v1,v3,V \/ {v2} holds
cost (Q,W) <= cost (S,W)let S be
oriented Chain of
G;
( S is_orientedpath_of v1,v3,V \/ {v2} implies cost (Q,W) <= cost (b1,W) )assume A9:
S is_orientedpath_of v1,
v3,
V \/ {v2}
;
cost (Q,W) <= cost (b1,W)then consider s being
oriented Simple Chain of
G such that A10:
s is_shortestpath_of v1,
v3,
V \/ {v2},
W
by A1, GRAPH_5:62;
A11:
cost (
s,
W)
<= cost (
S,
W)
by A9, A10, GRAPH_5:def 18;
A12:
s is_orientedpath_of v1,
v3,
V \/ {v2}
by A10, GRAPH_5:def 18;
then A13:
s is_orientedpath_of v1,
v3
by GRAPH_5:def 4;
then A14:
the
Source of
G . (s . 1) = v1
by GRAPH_5:def 3;
s <> {}
by A13, GRAPH_5:def 3;
then
len s >= 1
by FINSEQ_1:20;
then consider i being
Nat such that A15:
len s = 1
+ i
by NAT_1:10;
A16:
(vertices s) \ {v3} c= V \/ {v2}
by A12, GRAPH_5:def 4;
A17:
the
Target of
G . (s . (len s)) = v3
by A13, GRAPH_5:def 3;
consider s1,
s2 being
FinSequence such that A18:
len s1 = i
and A19:
len s2 = 1
and A20:
s = s1 ^ s2
by A15, FINSEQ_2:22;
reconsider s1 =
s1,
s2 =
s2 as
oriented Simple Chain of
G by A20, GRAPH_5:14;
reconsider vx = the
Source of
G . (s2 . 1) as
Vertex of
G by A19, Lm3;
A21:
s2 . 1
= s . (len s)
by A15, A18, A19, A20, Lm2;
per cases
( not v2 in vertices s or v2 = v3 or ( v2 in vertices s & v2 <> v3 ) )
;
suppose A24:
( not
v2 in vertices s or
v2 = v3 )
;
cost (Q,W) <= cost (b1,W)set Vs =
vertices s;
((vertices s) \ {v3}) \ {v2} c= V
by A16, XBOOLE_1:43;
then A25:
(vertices s) \ ({v3} \/ {v2}) c= V
by XBOOLE_1:41;
then
s is_orientedpath_of v1,
v3,
V
by A13, GRAPH_5:def 4;
then
cost (
Q,
W)
<= cost (
s,
W)
by A5, GRAPH_5:def 18;
hence
cost (
Q,
W)
<= cost (
S,
W)
by A11, XXREAL_0:2;
verum end; suppose A27:
(
v2 in vertices s &
v2 <> v3 )
;
cost (Q,W) <= cost (b1,W)A28:
len s1 < len s
by A15, A18, NAT_1:13;
consider j being
Nat such that A29:
1
<= j
and A30:
j <= len s
and A31:
v2 = the
Target of
G . (s . j)
by A3, A14, A27, GRAPH_5:28;
len s1 <> 0
by A15, A18, A17, A27, A29, A30, A31, XXREAL_0:1;
then A32:
len s1 >= 0 + 1
by INT_1:7;
vx =
the
Source of
G . (s . ((len s1) + 1))
by A19, A20, Lm2
.=
the
Target of
G . (s . (len s1))
by A32, A28, GRAPH_1:def 15
;
then
vx = the
Target of
G . (s1 . (len s1))
by A20, A32, Lm1;
then A33:
vx in vertices s1
by A32, Lm4;
not
vx in {v2}
by A22, TARSKI:def 1;
then A34:
vx in (vertices s1) \ {v2}
by A33, XBOOLE_0:def 5;
then consider k being
Nat such that A36:
len s1 = j + k
by NAT_1:10;
consider t1,
t2 being
FinSequence such that A37:
len t1 = j
and
len t2 = k
and A38:
s1 = t1 ^ t2
by A36, FINSEQ_2:22;
reconsider t1 =
t1,
t2 =
t2 as
oriented Simple Chain of
G by A38, GRAPH_5:14;
A39:
t1 <> {}
by A29, A37;
set Vt =
vertices t1;
(vertices (s1 ^ s2)) \ {v3} c= V \/ {v2}
by A12, A20, GRAPH_5:def 4;
then A40:
(vertices (t1 ^ t2)) \ {v3} c= V \/ {v2}
by A38, GRAPH_5:23;
then A41:
(vertices t1) \ {v3} c= V \/ {v2}
by GRAPH_5:23;
A42:
len s2 >= 1
by A19;
then
not
v3 in vertices s1
by A4, A20, A14, A17, A32, GRAPH_5:18;
then
vertices s1 c= V \/ {v2}
by A38, A40, ZFMISC_1:57;
then A43:
(vertices s1) \ {v2} c= V
by XBOOLE_1:43;
not
v1 in vertices s2
by A4, A19, A20, A14, A17, A32, GRAPH_5:18;
then
vx <> v1
by A19, Lm4;
then consider q being
oriented Chain of
G such that A44:
q is_shortestpath_of v1,
vx,
V,
W
and A45:
cost (
q,
W)
<= cost (
P,
W)
by A7, A34, A43, GRAPH_5:def 19;
A46:
0 <= cost (
t2,
W)
by A1, GRAPH_5:50;
vertices t1 c= vertices (t1 ^ t2)
by GRAPH_5:26;
then
not
v3 in vertices t1
by A4, A20, A14, A17, A32, A38, A42, GRAPH_5:18;
then
vertices t1 c= V \/ {v2}
by A41, ZFMISC_1:57;
then A47:
(vertices t1) \ {v2} c= V
by XBOOLE_1:43;
A48: the
Source of
G . (t1 . 1) =
the
Source of
G . (s1 . 1)
by A29, A37, A38, Lm1
.=
v1
by A20, A14, A32, Lm1
;
cost (
s1,
W)
= (cost (t1,W)) + (cost (t2,W))
by A1, A38, GRAPH_5:46, GRAPH_5:54;
then A49:
0 + (cost (t1,W)) <= cost (
s1,
W)
by A46, XREAL_1:7;
the
Target of
G . (t1 . (len t1)) =
the
Target of
G . (s1 . j)
by A29, A37, A38, Lm1
.=
v2
by A20, A29, A31, A35, Lm1
;
then
t1 is_orientedpath_of v1,
v2
by A48, A39, GRAPH_5:def 3;
then
t1 is_orientedpath_of v1,
v2,
V
by A47, GRAPH_5:def 4;
then
cost (
P,
W)
<= cost (
t1,
W)
by A2, GRAPH_5:def 18;
then
cost (
q,
W)
<= cost (
t1,
W)
by A45, XXREAL_0:2;
then A50:
cost (
q,
W)
<= cost (
s1,
W)
by A49, XXREAL_0:2;
A51:
s2 . 1
orientedly_joins vx,
v3
by A21, A17, GRAPH_4:def 1;
A52:
q is_orientedpath_of v1,
vx,
V
by A44, GRAPH_5:def 18;
then A53:
q is_orientedpath_of v1,
vx
by GRAPH_5:def 4;
then
q <> {}
by GRAPH_5:def 3;
then A54:
len q >= 1
by FINSEQ_1:20;
then consider p being
oriented Chain of
G such that A55:
p = q ^ s2
and
p is_orientedpath_of v1,
v3
by A19, A51, A53, GRAPH_5:33;
p is_orientedpath_of v1,
v3,
V \/ {vx}
by A19, A52, A51, A54, A55, GRAPH_5:34;
then
p is_orientedpath_of v1,
v3,
V
by A34, A43, ZFMISC_1:40;
then
cost (
Q,
W)
<= cost (
p,
W)
by A5, GRAPH_5:def 18;
then A56:
cost (
Q,
W)
<= (cost (q,W)) + (cost (s2,W))
by A1, A55, GRAPH_5:46, GRAPH_5:54;
cost (
s,
W)
= (cost (s1,W)) + (cost (s2,W))
by A1, A20, GRAPH_5:46, GRAPH_5:54;
then
(cost (q,W)) + (cost (s2,W)) <= cost (
s,
W)
by A50, XREAL_1:7;
then
cost (
Q,
W)
<= cost (
s,
W)
by A56, XXREAL_0:2;
hence
cost (
Q,
W)
<= cost (
S,
W)
by A11, XXREAL_0:2;
verum end; end;
Q is_orientedpath_of v1,v3,V
by A5, GRAPH_5:def 18;
then
Q is_orientedpath_of v1,v3,V \/ {v2}
by GRAPH_5:32, XBOOLE_1:7;
hence
Q is_shortestpath_of v1,v3,V \/ {v2},W
by A8, GRAPH_5:def 18; verum