let e be set ; for G being oriented finite Graph
for P being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds
P is_shortestpath_of v1,v2,{v1},W
let G be oriented finite Graph; for P being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds
P is_shortestpath_of v1,v2,{v1},W
let P be oriented Chain of G; for W being Function of the carrier' of G,Real>=0
for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds
P is_shortestpath_of v1,v2,{v1},W
let W be Function of the carrier' of G,Real>=0; for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds
P is_shortestpath_of v1,v2,{v1},W
let v1, v2 be Vertex of G; ( e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 implies P is_shortestpath_of v1,v2,{v1},W )
assume that
A1:
e in the carrier' of G
and
A2:
P = <*e*>
and
A3:
e orientedly_joins v1,v2
; P is_shortestpath_of v1,v2,{v1},W
A4:
len P = 1
by A2, FINSEQ_1:40;
then A5:
vertices P = vertices (P /. 1)
by GRAPH_5:25;
set FS = the Source of G;
set FT = the Target of G;
set Eg = the carrier' of G;
A6:
( the Source of G . e = v1 & the Target of G . e = v2 )
by A3, GRAPH_4:def 1;
A7:
now let S be
oriented Chain of
G;
( S is_orientedpath_of v1,v2,{v1} implies cost (P,W) <= cost (S,W) )assume A8:
S is_orientedpath_of v1,
v2,
{v1}
;
cost (P,W) <= cost (S,W)
W is_weight>=0of G
by GRAPH_5:def 13;
then consider s being
oriented Simple Chain of
G such that A9:
s is_shortestpath_of v1,
v2,
{v1},
W
by A8, GRAPH_5:62;
set Vs =
vertices s;
A10:
s is_orientedpath_of v1,
v2,
{v1}
by A9, GRAPH_5:def 18;
then A11:
s is_orientedpath_of v1,
v2
by GRAPH_5:def 4;
then
s <> {}
by GRAPH_5:def 3;
then A12:
len s >= 1
by FINSEQ_1:20;
then consider i being
Nat such that A13:
len s = 1
+ i
by NAT_1:10;
A14:
the
Target of
G . (s . (len s)) = v2
by A11, GRAPH_5:def 3;
then
v2 in vertices s
by A12, Lm4;
then A15:
{v2} c= vertices s
by ZFMISC_1:31;
A16:
the
Source of
G . (s . 1) = v1
by A11, GRAPH_5:def 3;
then
v1 in vertices s
by A12, Lm4;
then
{v1} c= vertices s
by ZFMISC_1:31;
then
{v1} \/ {v2} c= vertices s
by A15, XBOOLE_1:8;
then A17:
{v1,v2} c= vertices s
by ENUMSET1:1;
consider s1,
s2 being
FinSequence such that A18:
len s1 = i
and A19:
len s2 = 1
and A20:
s = s1 ^ s2
by A13, FINSEQ_2:22;
reconsider s1 =
s1,
s2 =
s2 as
oriented Simple Chain of
G by A20, GRAPH_5:14;
(vertices s) \ {v2} c= {v1}
by A10, GRAPH_5:def 4;
then
vertices s c= {v2} \/ {v1}
by XBOOLE_1:44;
then A21:
vertices s c= {v1,v2}
by ENUMSET1:1;
now reconsider vx = the
Source of
G . (s2 . 1) as
Vertex of
G by A19, Lm3;
A22:
len s1 < len s
by A13, A18, NAT_1:13;
A23:
vx in vertices s2
by A19, Lm4;
vertices s2 c= vertices (s1 ^ s2)
by GRAPH_5:26;
then A24:
vertices s2 c= {v1,v2}
by A21, A17, A20, XBOOLE_0:def 10;
assume
s1 <> {}
;
contradictionthen A25:
len s1 >= 1
by FINSEQ_1:20;
then A26:
the
Source of
G . (s . 1) <> the
Source of
G . (s2 . 1)
by A19, A20, Th6;
len s2 = 1
by A19;
then A27:
the
Target of
G . (s . (len s)) <> the
Target of
G . (s1 . (len s1))
by A20, A25, Th6;
the
Source of
G . (s2 . 1) =
the
Source of
G . (s . ((len s1) + 1))
by A19, A20, Lm2
.=
the
Target of
G . (s . (len s1))
by A25, A22, GRAPH_1:def 13
.=
the
Target of
G . (s1 . (len s1))
by A20, A25, Lm1
;
hence
contradiction
by A16, A14, A27, A26, A24, A23, TARSKI:def 2;
verum end; then A28:
len s = 0 + 1
by A13, A18;
s /. 1
in the
carrier' of
G
by A1;
then
s . 1
in the
carrier' of
G
by A28, FINSEQ_4:15;
then
e = s . 1
by A1, A6, A16, A14, A28, GRAPH_1:def 5;
then
s = P
by A2, A28, FINSEQ_1:40;
hence
cost (
P,
W)
<= cost (
S,
W)
by A8, A9, GRAPH_5:def 18;
verum end;
A29:
P . 1 = e
by A2, FINSEQ_1:40;
then
P /. 1 = e
by A4, FINSEQ_4:15;
then
vertices P = {v1,v2}
by A6, A5, GRAPH_5:def 1;
then A30: (vertices P) \ {v2} =
({v1} \/ {v2}) \ {v2}
by ENUMSET1:1
.=
{v1} \ {v2}
by XBOOLE_1:40
;
P is_orientedpath_of v1,v2
by A2, A6, A4, A29, GRAPH_5:def 3;
then
P is_orientedpath_of v1,v2,{v1}
by A30, GRAPH_5:def 4;
hence
P is_shortestpath_of v1,v2,{v1},W
by A7, GRAPH_5:def 18; verum