let V, e be set ; :: thesis: for G being oriented finite Graph

for P, Q being oriented Chain of G

for W being Function of the carrier' of G,Real>=0

for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

let G be oriented finite Graph; :: thesis: for P, Q being oriented Chain of G

for W being Function of the carrier' of G,Real>=0

for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

let P, Q be oriented Chain of G; :: thesis: for W being Function of the carrier' of G,Real>=0

for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

let W be Function of the carrier' of G,Real>=0; :: thesis: for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

let v1, v2, v3 be Vertex of G; :: thesis: ( e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) implies Q is_shortestpath_of v1,v3,V \/ {v2},W )

assume that

A1: e in the carrier' of G and

A2: P is_shortestpath_of v1,v2,V,W and

A3: v1 <> v3 and

A4: Q = P ^ <*e*> and

A5: e orientedly_joins v2,v3 and

A6: v1 in V and

A7: for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ; :: thesis: Q is_shortestpath_of v1,v3,V \/ {v2},W

set Eg = the carrier' of G;

reconsider pe = <*e*> as FinSequence of the carrier' of G by A1, FINSEQ_1:74;

A8: P is_orientedpath_of v1,v2,V by A2, GRAPH_5:def 18;

then P is_orientedpath_of v1,v2 by GRAPH_5:def 4;

then P <> {} by GRAPH_5:def 3;

then A9: len P >= 1 by FINSEQ_1:20;

set V9 = V \/ {v2};

set FS = the Source of G;

set FT = the Target of G;

A10: W is_weight>=0of G by GRAPH_5:def 13;

then Q is_orientedpath_of v1,v3,V \/ {v2} by A4, A5, A8, A9, GRAPH_5:34;

hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A11, GRAPH_5:def 18; :: thesis: verum

for P, Q being oriented Chain of G

for W being Function of the carrier' of G,Real>=0

for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

let G be oriented finite Graph; :: thesis: for P, Q being oriented Chain of G

for W being Function of the carrier' of G,Real>=0

for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

let P, Q be oriented Chain of G; :: thesis: for W being Function of the carrier' of G,Real>=0

for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

let W be Function of the carrier' of G,Real>=0; :: thesis: for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

let v1, v2, v3 be Vertex of G; :: thesis: ( e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) implies Q is_shortestpath_of v1,v3,V \/ {v2},W )

assume that

A1: e in the carrier' of G and

A2: P is_shortestpath_of v1,v2,V,W and

A3: v1 <> v3 and

A4: Q = P ^ <*e*> and

A5: e orientedly_joins v2,v3 and

A6: v1 in V and

A7: for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ; :: thesis: Q is_shortestpath_of v1,v3,V \/ {v2},W

set Eg = the carrier' of G;

reconsider pe = <*e*> as FinSequence of the carrier' of G by A1, FINSEQ_1:74;

A8: P is_orientedpath_of v1,v2,V by A2, GRAPH_5:def 18;

then P is_orientedpath_of v1,v2 by GRAPH_5:def 4;

then P <> {} by GRAPH_5:def 3;

then A9: len P >= 1 by FINSEQ_1:20;

set V9 = V \/ {v2};

set FS = the Source of G;

set FT = the Target of G;

A10: W is_weight>=0of G by GRAPH_5:def 13;

A11: now :: thesis: for S being oriented Chain of G st S is_orientedpath_of v1,v3,V \/ {v2} holds

cost (Q,W) <= cost (S,W)

( len pe = 1 & pe . 1 = e )
by FINSEQ_1:40;cost (Q,W) <= cost (S,W)

let S be oriented Chain of G; :: thesis: ( S is_orientedpath_of v1,v3,V \/ {v2} implies cost (Q,W) <= cost (S,W) )

assume A12: S is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis: cost (Q,W) <= cost (S,W)

then consider s being oriented Simple Chain of G such that

A13: s is_shortestpath_of v1,v3,V \/ {v2},W by A10, GRAPH_5:62;

set Vs = vertices s;

A14: s is_orientedpath_of v1,v3,V \/ {v2} by A13, GRAPH_5:def 18;

then A15: s is_orientedpath_of v1,v3 by GRAPH_5:def 4;

then A16: the Target of G . (s . (len s)) = v3 by GRAPH_5:def 3;

A17: (vertices s) \ {v3} c= V \/ {v2} by A14, GRAPH_5:def 4;

s <> {} by A15, GRAPH_5:def 3;

then A18: len s >= 1 by FINSEQ_1:20;

then consider i being Nat such that

A19: len s = 1 + i by NAT_1:10;

consider s1, s2 being FinSequence such that

A20: len s1 = i and

A21: len s2 = 1 and

A22: s = s1 ^ s2 by A19, FINSEQ_2:22;

reconsider s1 = s1, s2 = s2 as oriented Simple Chain of G by A22, GRAPH_5:14;

reconsider vx = the Source of G . (s2 . 1) as Vertex of G by A21, Lm3;

A23: s2 . 1 = s . (len s) by A19, A20, A21, A22, Lm2;

A24: the Source of G . (s . 1) = v1 by A15, GRAPH_5:def 3;

A25: s1 <> {}

len s1 < len s by A19, A20, NAT_1:13;

then A28: the Source of G . (s . (len s)) = the Target of G . (s . (len s1)) by A19, A20, A27, GRAPH_1:def 15

.= the Target of G . (s1 . (len s1)) by A22, A27, Lm1 ;

then not the Target of G . (s . (len s)) in vertices s1 by A3, A22, A24, A16, A27, GRAPH_5:18;

then A33: (vertices s1) \ {v3} = vertices s1 by A16, ZFMISC_1:57;

vertices s1 c= vertices (s1 ^ s2) by GRAPH_5:26;

then vertices s1 c= (vertices s) \ {v3} by A22, A33, XBOOLE_1:33;

then vertices s1 c= V \/ {v2} by A17;

then (vertices s1) \ {v2} c= (V \/ {v2}) \ {v2} by XBOOLE_1:33;

then (vertices s1) \ {v2} c= V \ {v2} by XBOOLE_1:40;

then A34: (vertices s1) \ {v2} c= V by XBOOLE_1:1;

s2 /. 1 in the carrier' of G by A1;

then A35: s2 . 1 in the carrier' of G by A21, FINSEQ_4:15;

( the Source of G . e = v2 & the Target of G . e = v3 ) by A5, GRAPH_4:def 1;

then e = s2 . 1 by A1, A23, A16, A29, A35, GRAPH_1:def 7;

then s2 = <*e*> by A21, FINSEQ_1:40;

then A36: cost (Q,W) = (cost (P,W)) + (cost (s2,W)) by A4, A10, GRAPH_5:46, GRAPH_5:54;

the Source of G . (s1 . 1) = v1 by A22, A24, A27, Lm1;

then s1 is_orientedpath_of v1,v2 by A23, A25, A28, A29, GRAPH_5:def 3;

then s1 is_orientedpath_of v1,v2,V by A34, GRAPH_5:def 4;

then A37: cost (P,W) <= cost (s1,W) by A2, GRAPH_5:def 18;

A38: cost (s,W) <= cost (S,W) by A12, A13, GRAPH_5:def 18;

cost (s,W) = (cost (s1,W)) + (cost (s2,W)) by A10, A22, GRAPH_5:46, GRAPH_5:54;

then cost (Q,W) <= cost (s,W) by A37, A36, XREAL_1:7;

hence cost (Q,W) <= cost (S,W) by A38, XXREAL_0:2; :: thesis: verum

end;assume A12: S is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis: cost (Q,W) <= cost (S,W)

then consider s being oriented Simple Chain of G such that

A13: s is_shortestpath_of v1,v3,V \/ {v2},W by A10, GRAPH_5:62;

set Vs = vertices s;

A14: s is_orientedpath_of v1,v3,V \/ {v2} by A13, GRAPH_5:def 18;

then A15: s is_orientedpath_of v1,v3 by GRAPH_5:def 4;

then A16: the Target of G . (s . (len s)) = v3 by GRAPH_5:def 3;

A17: (vertices s) \ {v3} c= V \/ {v2} by A14, GRAPH_5:def 4;

s <> {} by A15, GRAPH_5:def 3;

then A18: len s >= 1 by FINSEQ_1:20;

then consider i being Nat such that

A19: len s = 1 + i by NAT_1:10;

consider s1, s2 being FinSequence such that

A20: len s1 = i and

A21: len s2 = 1 and

A22: s = s1 ^ s2 by A19, FINSEQ_2:22;

reconsider s1 = s1, s2 = s2 as oriented Simple Chain of G by A22, GRAPH_5:14;

reconsider vx = the Source of G . (s2 . 1) as Vertex of G by A21, Lm3;

A23: s2 . 1 = s . (len s) by A19, A20, A21, A22, Lm2;

A24: the Source of G . (s . 1) = v1 by A15, GRAPH_5:def 3;

A25: s1 <> {}

proof

then A27:
len s1 >= 1
by FINSEQ_1:20;
assume
s1 = {}
; :: thesis: contradiction

then A26: len s = 1 + 0 by A19, A20;

then s . 1 orientedly_joins v1,v3 by A24, A16, GRAPH_4:def 1;

hence contradiction by A6, A7, A26, Th2; :: thesis: verum

end;then A26: len s = 1 + 0 by A19, A20;

then s . 1 orientedly_joins v1,v3 by A24, A16, GRAPH_4:def 1;

hence contradiction by A6, A7, A26, Th2; :: thesis: verum

len s1 < len s by A19, A20, NAT_1:13;

then A28: the Source of G . (s . (len s)) = the Target of G . (s . (len s1)) by A19, A20, A27, GRAPH_1:def 15

.= the Target of G . (s1 . (len s1)) by A22, A27, Lm1 ;

A29: now :: thesis: not vx <> v2

len s2 = 1
by A21;
vx <> the Target of G . (s . (len s))
by A21, A22, A23, A27, A28, Th6;

then A30: not vx in {v3} by A16, TARSKI:def 1;

vx in vertices s by A18, A23, Lm4;

then vx in (vertices s) \ {v3} by A30, XBOOLE_0:def 5;

then A31: ( vx in V or vx in {v2} ) by A17, XBOOLE_0:def 3;

assume A32: vx <> v2 ; :: thesis: contradiction

( s2 . 1 orientedly_joins vx,v3 & s2 . 1 in the carrier' of G ) by A21, A23, A16, Th2, GRAPH_4:def 1;

hence contradiction by A7, A32, A31, TARSKI:def 1; :: thesis: verum

end;then A30: not vx in {v3} by A16, TARSKI:def 1;

vx in vertices s by A18, A23, Lm4;

then vx in (vertices s) \ {v3} by A30, XBOOLE_0:def 5;

then A31: ( vx in V or vx in {v2} ) by A17, XBOOLE_0:def 3;

assume A32: vx <> v2 ; :: thesis: contradiction

( s2 . 1 orientedly_joins vx,v3 & s2 . 1 in the carrier' of G ) by A21, A23, A16, Th2, GRAPH_4:def 1;

hence contradiction by A7, A32, A31, TARSKI:def 1; :: thesis: verum

then not the Target of G . (s . (len s)) in vertices s1 by A3, A22, A24, A16, A27, GRAPH_5:18;

then A33: (vertices s1) \ {v3} = vertices s1 by A16, ZFMISC_1:57;

vertices s1 c= vertices (s1 ^ s2) by GRAPH_5:26;

then vertices s1 c= (vertices s) \ {v3} by A22, A33, XBOOLE_1:33;

then vertices s1 c= V \/ {v2} by A17;

then (vertices s1) \ {v2} c= (V \/ {v2}) \ {v2} by XBOOLE_1:33;

then (vertices s1) \ {v2} c= V \ {v2} by XBOOLE_1:40;

then A34: (vertices s1) \ {v2} c= V by XBOOLE_1:1;

s2 /. 1 in the carrier' of G by A1;

then A35: s2 . 1 in the carrier' of G by A21, FINSEQ_4:15;

( the Source of G . e = v2 & the Target of G . e = v3 ) by A5, GRAPH_4:def 1;

then e = s2 . 1 by A1, A23, A16, A29, A35, GRAPH_1:def 7;

then s2 = <*e*> by A21, FINSEQ_1:40;

then A36: cost (Q,W) = (cost (P,W)) + (cost (s2,W)) by A4, A10, GRAPH_5:46, GRAPH_5:54;

the Source of G . (s1 . 1) = v1 by A22, A24, A27, Lm1;

then s1 is_orientedpath_of v1,v2 by A23, A25, A28, A29, GRAPH_5:def 3;

then s1 is_orientedpath_of v1,v2,V by A34, GRAPH_5:def 4;

then A37: cost (P,W) <= cost (s1,W) by A2, GRAPH_5:def 18;

A38: cost (s,W) <= cost (S,W) by A12, A13, GRAPH_5:def 18;

cost (s,W) = (cost (s1,W)) + (cost (s2,W)) by A10, A22, GRAPH_5:46, GRAPH_5:54;

then cost (Q,W) <= cost (s,W) by A37, A36, XREAL_1:7;

hence cost (Q,W) <= cost (S,W) by A38, XXREAL_0:2; :: thesis: verum

then Q is_orientedpath_of v1,v3,V \/ {v2} by A4, A5, A8, A9, GRAPH_5:34;

hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A11, GRAPH_5:def 18; :: thesis: verum