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 :: thesis: not for n being Nat holds (AP:CompSeq (EL,source)) . n <> (AP:CompSeq (EL,source)) . (n + 1)

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

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be 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 = the Element of 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 :: thesis: S₁[n + 1]

per cases ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & not (the_Source_of G) . the Element of 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) . the Element of 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) . the Element of 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) .--> the Element of 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) . the Element of 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) . the Element of 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) .--> the Element of 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} by Lm1;
( the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n or the Element of 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) by A6;
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 Nat holds S₁[n] from NAT_1:sch 2(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 ; :: thesis: verum