let G be finite real-weighted WGraph; :: thesis: for src being Vertex of G
for n being Nat holds ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1))
let src be Vertex of G; :: thesis: for n being Nat holds ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1))
set DCS = DIJK:CompSeq src;
set D0 = (DIJK:CompSeq src) . 0;
defpred S₁[ Nat] means ((DIJK:CompSeq src) . $1) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . $1) `1));

now

let n be Nat; :: thesis: ( ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1)) implies ((DIJK:CompSeq src) . (n + 1)) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) )
set Dn = (DIJK:CompSeq src) . n;
set Dn1 = (DIJK:CompSeq src) . (n + 1);
set BE = DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set e = choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n));
set target = (the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)));
set val = ((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))));
set DnE = (((DIJK:CompSeq src) . n) `2) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))};
assume A1: ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1)) ; :: thesis: ((DIJK:CompSeq src) . (n + 1)) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1))
A2: (DIJK:CompSeq src) . (n + 1) = DIJK:Step ((DIJK:CompSeq src) . n) by Def11;

now

let x be set ; :: thesis: ( x in ((DIJK:CompSeq src) . (n + 1)) `2 implies x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) )
n <= n + 1 by NAT_1:12;
then A3: dom (((DIJK:CompSeq src) . n) `1) c= dom (((DIJK:CompSeq src) . (n + 1)) `1) by Th18;
assume A4: x in ((DIJK:CompSeq src) . (n + 1)) `2 ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1))

now

per cases ( DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} or DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {} ) ;

suppose DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1))

then (DIJK:CompSeq src) . (n + 1) = (DIJK:CompSeq src) . n by A2, Def8;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) by A1, A4; :: thesis: verum

end;

suppose A5: DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {} ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1))

then A6: (DIJK:CompSeq src) . (n + 1) = [((((DIJK:CompSeq src) . n) `1) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))))),((((DIJK:CompSeq src) . n) `2) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))})] by A2, Def8;
then A7: ((DIJK:CompSeq src) . (n + 1)) `2 = (((DIJK:CompSeq src) . n) `2) \/ {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} by MCART_1:7;
((DIJK:CompSeq src) . (n + 1)) `1 = (((DIJK:CompSeq src) . n) `1) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))) .--> (((((DIJK:CompSeq src) . n) `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))))) by A6, MCART_1:7;
then A8: dom (((DIJK:CompSeq src) . (n + 1)) `1) = (dom (((DIJK:CompSeq src) . n) `1)) \/ {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} by Lm1;
A9: choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) in DIJK:NextBestEdges ((DIJK:CompSeq src) . n) by A5;

now

per cases ( x in ((DIJK:CompSeq src) . n) `2 or x in {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} ) by A4, A7, XBOOLE_0:def 3;

suppose A10: x in ((DIJK:CompSeq src) . n) `2 ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1))

A11: ((DIJK:CompSeq src) . n) `2 in bool (the_Edges_of G) by MCART_1:10;
( (the_Source_of G) . x in dom (((DIJK:CompSeq src) . n) `1) & (the_Target_of G) . x in dom (((DIJK:CompSeq src) . n) `1) ) by A1, A10, GLIB_000:31;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) by A3, A10, A11, GLIB_000:31; :: thesis: verum

end;

suppose x in {(choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)))} ; :: thesis: x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1))

then A12: x = choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) by TARSKI:def 1;
then (the_Target_of G) . x in {((the_Target_of G) . (choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n))))} by TARSKI:def 1;
then A13: (the_Target_of G) . x in dom (((DIJK:CompSeq src) . (n + 1)) `1) by A8, XBOOLE_0:def 3;
choose (DIJK:NextBestEdges ((DIJK:CompSeq src) . n)) DSJoins dom (((DIJK:CompSeq src) . n) `1),(the_Vertices_of G) \ (dom (((DIJK:CompSeq src) . n) `1)),G by A5, Def7;
then (the_Source_of G) . x in dom (((DIJK:CompSeq src) . n) `1) by A12, GLIB_000:def 16;
hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) by A3, A9, A12, A13, GLIB_000:31; :: thesis: verum

end;

end;

end;

hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) ; :: thesis: verum

end;

end;

end;

hence x in G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) ; :: thesis: verum

end;

hence ((DIJK:CompSeq src) . (n + 1)) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . (n + 1)) `1)) by TARSKI:def 3; :: thesis: verum

end;

then A14: for k being Nat st S₁[k] holds
S₁[k + 1] ;
(DIJK:CompSeq src) . 0 = DIJK:Init src by Def11;
then for x being set st x in ((DIJK:CompSeq src) . 0) `2 holds
x in G .edgesBetween (dom (((DIJK:CompSeq src) . 0) `1)) by MCART_1:7;
then A15: S₁[ 0 ] by TARSKI:def 3;
for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A14);
hence for n being Nat holds ((DIJK:CompSeq src) . n) `2 c= G .edgesBetween (dom (((DIJK:CompSeq src) . n) `1)) ; :: thesis: verum