let e, V be set ; :: thesis:
let W be Function; :: thesis:
let G be oriented finite Graph; :: thesis:
let P, Q, R be oriented Chain of G; :: thesis:
let v1, v2, v3 be Element of G; :: thesis:
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 ; :: thesis:
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 :: thesis:

assume A18: cost (Q,W) <= cost (s,W) ; :: thesis:

hereby :: thesis:

assume cost (Q,W) <= cost (R,W) ; :: thesis:

now :: thesis:

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost (s,W) <= cost (u,W) by A15;
hence cost (Q,W) <= cost (u,W) by A18, XXREAL_0:2; :: thesis:

end;

hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A13; :: thesis:

end;

hereby :: thesis:

assume A19: cost (Q,W) >= cost (R,W) ; :: thesis:

now :: thesis:

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
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; :: thesis:

end;

hence R is_shortestpath_of v1,v3,V \/ {v2},W by A16; :: thesis:

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 ;

suppose len s >= 2 ; :: thesis:

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 :: thesis:

per cases ;

suppose v2 in vertices s1 ; :: thesis:

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 :: thesis:

per cases ;

suppose A48: the Source of G . (s2 . 1) = v2 ; :: thesis:

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 :: thesis:

assume cost (Q,W) <= cost (R,W) ; :: thesis:
then A51: cost (Q,W) <= cost (s,W) by A50, XXREAL_0:2;

now :: thesis:

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost (s,W) <= cost (u,W) by A15;
hence cost (Q,W) <= cost (u,W) by A51, XXREAL_0:2; :: thesis:

end;

hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A13; :: thesis:

end;

hereby :: thesis:

assume cost (Q,W) >= cost (R,W) ; :: thesis:

now :: thesis:

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost (s,W) <= cost (u,W) by A15;
hence cost (R,W) <= cost (u,W) by A50, XXREAL_0:2; :: thesis:

end;

hence R is_shortestpath_of v1,v3,V \/ {v2},W by A16; :: thesis:

end;

suppose A52: the Source of G . (s2 . 1) <> v2 ; :: thesis:

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 :: thesis:

assume cost (Q,W) <= cost (R,W) ; :: thesis:

now :: thesis:

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost (s,W) <= cost (u,W) by A15;
hence cost (Q,W) <= cost (u,W) by A74, XXREAL_0:2; :: thesis:

end;

hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A13; :: thesis:

end;

hereby :: thesis:

assume cost (Q,W) >= cost (R,W) ; :: thesis:
then A75: cost (R,W) <= cost (s,W) by A74, XXREAL_0:2;

now :: thesis:

let u be oriented Chain of G; :: thesis:
assume u is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis:
then cost (s,W) <= cost (u,W) by A15;
hence cost (R,W) <= cost (u,W) by A75, XXREAL_0:2; :: thesis:

end;

hence R is_shortestpath_of v1,v3,V \/ {v2},W by A16; :: thesis:

end;

suppose not v2 in vertices s1 ; :: thesis:

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; :: thesis:

end;

suppose len s < 1 + 1 ; :: thesis:

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A80: x in (vertices s) \ {v3} ; :: thesis:
then A81: not x in {v3} by XBOOLE_0:def 5;
x in vertices (s /. 1) by A79, A80, XBOOLE_0:def 5;
then A82: ( x = the Source of G . (s /. 1) or x = the Target of G . (s /. 1) ) by TARSKI:def 2;
A83: s /. 1 = s . 1 by A24, FINSEQ_4:15;
v3 = the Target of G . (s . (len s)) by A22
.= the Target of G . (s /. 1) by A78, FINSEQ_4:15 ;
hence x in V by A22, A12, A81, A82, A83, TARSKI:def 1; :: thesis:

end;

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; :: thesis:

end;