let G be finite real-weighted WGraph; :: thesis: for s being Vertex of G holds DIJK:CompSeq s is halting
let src be Vertex of G; :: thesis: DIJK:CompSeq src is halting
set DCS = DIJK:CompSeq src;

now

take n = card (G .reachableDFrom src); :: thesis: (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1)
set Gn = (DIJK:CompSeq src) . n;
set Gn1a = (DIJK:CompSeq src) . (n + 1);
set BestEdges = DIJK:NextBestEdges ((DIJK:CompSeq src) . n);
set RSize = card (G .reachableDFrom src);
A1: (DIJK:CompSeq src) . (n + 1) = DIJK:Step ((DIJK:CompSeq src) . n) by Def7;

now

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

suppose DIJK:NextBestEdges ((DIJK:CompSeq src) . n) = {} ; :: thesis: (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1)

hence (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1) by A1, Def5; :: thesis: verum

end;

suppose A2: DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {} ; :: thesis: (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1)

A3: card (dom (((DIJK:CompSeq src) . n) `1 )) = min (n + 1),(card (G .reachableDFrom src)) by Th20;
card (G .reachableDFrom src) <= (card (G .reachableDFrom src)) + 1 by NAT_1:11;
then A4: card (dom (((DIJK:CompSeq src) . n) `1 )) = card (G .reachableDFrom src) by A3, XXREAL_0:def 9;
A5: card (dom ((DIJK:Step ((DIJK:CompSeq src) . n)) `1 )) = (card (dom (((DIJK:CompSeq src) . n) `1 ))) + 1 by A2, Th13;
A6: (card (G .reachableDFrom src)) + 1 <= ((card (G .reachableDFrom src)) + 1) + 1 by NAT_1:11;
card (G .reachableDFrom src) <= (card (G .reachableDFrom src)) + 1 by NAT_1:11;
then A7: card (G .reachableDFrom src) <= (n + 1) + 1 by A6, XXREAL_0:2;
card (dom (((DIJK:CompSeq src) . (n + 1)) `1 )) = min ((n + 1) + 1),(card (G .reachableDFrom src)) by Th20
.= card (G .reachableDFrom src) by A7, XXREAL_0:def 9 ;
hence (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1) by A4, A5, Def7; :: thesis: verum

end;

end;

end;

hence (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1) ; :: thesis: verum

end;

hence DIJK:CompSeq src is halting by GLIB_000:def 56; :: thesis: verum