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

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

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 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 ; :: thesis: 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 :: thesis: for S being oriented Chain of G st S is_orientedpath_of v1,v3,V \/ {v2} holds

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

Q is_orientedpath_of v1,v3,V
by A5, GRAPH_5:def 18;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 (b_{1},W) )

assume A9: S is_orientedpath_of v1,v3,V \/ {v2} ; :: thesis: cost (Q,W) <= cost (b_{1},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;

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

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;

A22: now :: thesis: not vx = v2

assume
vx = v2
; :: thesis: contradiction

then A23: s2 . 1 orientedly_joins v2,v3 by A21, A17, GRAPH_4:def 1;

1 in dom s2 by A19, FINSEQ_3:25;

hence contradiction by A6, A23, FINSEQ_2:11; :: thesis: verum

end;then A23: s2 . 1 orientedly_joins v2,v3 by A21, A17, GRAPH_4:def 1;

1 in dom s2 by A19, FINSEQ_3:25;

hence contradiction by A6, A23, FINSEQ_2:11; :: thesis: verum

per cases
( not v2 in vertices s or v2 = v3 or ( v2 in vertices s & v2 <> v3 ) )
;

end;

suppose A24:
( not v2 in vertices s or v2 = v3 )
; :: thesis: cost (Q,W) <= cost (b_{1},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 cost (Q,W) <= cost (s,W) by A5, GRAPH_5:def 18;

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

end;((vertices s) \ {v3}) \ {v2} c= V by A16, XBOOLE_1:43;

then A25: (vertices s) \ ({v3} \/ {v2}) c= V by XBOOLE_1:41;

now :: thesis: (vertices s) \ {v3} c= V

then
s is_orientedpath_of v1,v3,V
by A13, GRAPH_5:def 4;end;

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

suppose A27:
( v2 in vertices s & v2 <> v3 )
; :: thesis: cost (Q,W) <= cost (b_{1},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;

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

end;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;

A35: now :: thesis: not j > len s1

then consider k being Nat such that assume
j > len s1
; :: thesis: contradiction

then j >= (len s1) + 1 by INT_1:7;

hence contradiction by A15, A18, A17, A27, A30, A31, XXREAL_0:1; :: thesis: verum

end;then j >= (len s1) + 1 by INT_1:7;

hence contradiction by A15, A18, A17, A27, A30, A31, XXREAL_0:1; :: thesis: verum

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

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