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 :: thesis: ex n being Element of NAT st (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1)
set RSize = card (G .reachableDFrom src);
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);
A1: (DIJK:CompSeq src) . (n + 1) = DIJK:Step ((DIJK:CompSeq src) . n) by Def11;
now :: thesis: (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1)
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, Def8; :: thesis: verum
end;
suppose A2: DIJK:NextBestEdges ((DIJK:CompSeq src) . n) <> {} ; :: thesis: (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1)
( card (dom (((DIJK:CompSeq src) . n) `1)) = min ((n + 1),(card (G .reachableDFrom src))) & card (G .reachableDFrom src) <= (card (G .reachableDFrom src)) + 1 ) by Th21, NAT_1:11;
then A3: card (dom (((DIJK:CompSeq src) . n) `1)) = card (G .reachableDFrom src) by XXREAL_0:def 9;
( (card (G .reachableDFrom src)) + 1 <= ((card (G .reachableDFrom src)) + 1) + 1 & card (G .reachableDFrom src) <= (card (G .reachableDFrom src)) + 1 ) by NAT_1:11;
then A4: card (G .reachableDFrom src) <= (n + 1) + 1 by XXREAL_0:2;
A5: card (dom (((DIJK:CompSeq src) . (n + 1)) `1)) = min (((n + 1) + 1),(card (G .reachableDFrom src))) by Th21
.= card (G .reachableDFrom src) by A4, XXREAL_0:def 9 ;
card (dom ((DIJK:Step ((DIJK:CompSeq src) . n)) `1)) = (card (dom (((DIJK:CompSeq src) . n) `1))) + 1 by A2, Th15;
hence (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1) by A3, A5, Def11; :: thesis: verum
end;
end;
end;
hence (DIJK:CompSeq src) . n = (DIJK:CompSeq src) . (n + 1) ; :: thesis: verum
end;
hence DIJK:CompSeq src is halting ; :: thesis: verum