let G be finite real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for source being Vertex of G holds AP:CompSeq (EL,source) is halting
let EL be FF:ELabeling of G; :: thesis: for source being Vertex of G holds AP:CompSeq (EL,source) is halting
let source be Vertex of G; :: thesis: AP:CompSeq (EL,source) is halting
set CS = AP:CompSeq (EL,source);

now

set x = card (the_Vertices_of G);
defpred S₁[ Element of NAT ] means card (dom ((AP:CompSeq (EL,source)) . $1)) = $1 + 1;
assume A1: for n being Element of NAT holds (AP:CompSeq (EL,source)) . n <> (AP:CompSeq (EL,source)) . (n + 1) ; :: thesis: contradiction

A2: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
set Gn = (AP:CompSeq (EL,source)) . n;
set Gn1 = (AP:CompSeq (EL,source)) . (n + 1);
set Next = AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
set e = choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n));
A3: (AP:CompSeq (EL,source)) . (n + 1) = AP:Step ((AP:CompSeq (EL,source)) . n) by Def12;
assume A4: S₁[n] ; :: thesis: S₁[n + 1]

now

per cases ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & not (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . n) ) or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . n) ) ) ;

suppose AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} ; :: thesis: S₁[n + 1]

then (AP:CompSeq (EL,source)) . n = (AP:CompSeq (EL,source)) . (n + 1) by A3, Def10;
hence S₁[n + 1] by A1; :: thesis: verum

end;

suppose A5: ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & not (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . n) ) ; :: thesis: S₁[n + 1]

then (AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))) .--> (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))) by A3, Def10;
then dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by Lm1;
hence S₁[n + 1] by A4, A5, CARD_2:41; :: thesis: verum

end;

suppose A6: ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . n) ) ; :: thesis: S₁[n + 1]

then (AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))) .--> (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))) by A3, Def10;
then A7: dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by Lm1;
( choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n or choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) is_backward_edge_wrt (AP:CompSeq (EL,source)) . n ) by A6, Def9;
then not (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . n) by A6, Def6, Def7;
hence S₁[n + 1] by A4, A7, CARD_2:41; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

dom ((AP:CompSeq (EL,source)) . 0) = {source} by Th4;
then A8: S₁[ 0 ] by CARD_1:30;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A8, A2);
then card (dom ((AP:CompSeq (EL,source)) . (card (the_Vertices_of G)))) = (card (the_Vertices_of G)) + 1 ;
then 1 + (card (the_Vertices_of G)) <= (card (the_Vertices_of G)) + 0 by NAT_1:43;
hence contradiction by XREAL_1:6; :: thesis: verum

end;

hence AP:CompSeq (EL,source) is halting by GLIB_000:def 54; :: thesis: verum