let G be _finite real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for source being Vertex of G
for n being Nat
for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
let EL be FF:ELabeling of G; :: thesis: for source being Vertex of G
for n being Nat
for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
let source be Vertex of G; :: thesis: for n being Nat
for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
let n be Nat; :: thesis: for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
let v be set ; :: thesis: ( v in dom ((AP:CompSeq (EL,source)) . n) implies ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v )
set SG = the_Source_of G;
set TG = the_Target_of G;
set CS = AP:CompSeq (EL,source);
set L = (AP:CompSeq (EL,source)) .Lifespan() ;
set GL = (AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan());
set GL1 = (AP:CompSeq (EL,source)) . (((AP:CompSeq (EL,source)) .Lifespan()) + 1);
defpred S₁[ Nat] means for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . (n + $1)) . v;
defpred S₂[ Nat] means (AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan()) = (AP:CompSeq (EL,source)) . (((AP:CompSeq (EL,source)) .Lifespan()) + $1);
A1: AP:CompSeq (EL,source) is halting by Th6;

A2: now :: thesis: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
set Gn1 = (AP:CompSeq (EL,source)) . ((((AP:CompSeq (EL,source)) .Lifespan()) + k) + 1);
assume S₂[k] ; :: thesis: S₂[k + 1]
then (AP:CompSeq (EL,source)) . ((((AP:CompSeq (EL,source)) .Lifespan()) + k) + 1) = AP:Step ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) by Def12
.= (AP:CompSeq (EL,source)) . (((AP:CompSeq (EL,source)) .Lifespan()) + 1) by Def12 ;
hence S₂[k + 1] by A1, GLIB_000:def 56; :: thesis: verum

end;

A3: S₂[ 0 ] ;
A4: for k being Nat holds S₂[k] from NAT_1:sch 2(A3, A2);

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

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
set Gn = (AP:CompSeq (EL,source)) . (n + k);
set Gn1 = (AP:CompSeq (EL,source)) . ((n + k) + 1);
set Next = AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k));
set e = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k));
A6: (AP:CompSeq (EL,source)) . ((n + k) + 1) = AP:Step ((AP:CompSeq (EL,source)) . (n + k)) by Def12;

now :: thesis: S₁[k + 1]

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

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

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

end;

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

then A8: (AP:CompSeq (EL,source)) . ((n + k) + 1) = ((AP:CompSeq (EL,source)) . (n + k)) +* (((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k))) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k))) by A6, Def10;

now :: thesis: for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v

let v be set ; :: thesis: ( v in dom ((AP:CompSeq (EL,source)) . n) implies ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v )
assume A9: v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis: ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v
then A10: ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . (n + k)) . v by A5;
dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + k)) by Th5, NAT_1:11;
then v <> (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) by A7, A9;
hence ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v by A8, A10, Lm4; :: thesis: verum

end;

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

end;

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

then A12: ( the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) is_forward_edge_wrt (AP:CompSeq (EL,source)) . (n + k) or the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) is_backward_edge_wrt (AP:CompSeq (EL,source)) . (n + k) ) by Def9;
A13: (AP:CompSeq (EL,source)) . ((n + k) + 1) = ((AP:CompSeq (EL,source)) . (n + k)) +* (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k))) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k))) by A6, A11, Def10;

now :: thesis: for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v

let v be set ; :: thesis: ( v in dom ((AP:CompSeq (EL,source)) . n) implies ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v )
assume A14: v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis: ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v
then A15: ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . (n + k)) . v by A5;
dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + k)) by Th5, NAT_1:11;
then v <> (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) by A11, A12, A14;
hence ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v by A13, A15, Lm4; :: thesis: verum

end;

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

end;

end;

end;

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

end;

then A16: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A17: S₁[ 0 ] ;
A18: for k being Nat holds S₁[k] from NAT_1:sch 2(A17, A16);
assume A19: v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis: ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v

now :: thesis: ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v

per cases ( n <= (AP:CompSeq (EL,source)) .Lifespan() or (AP:CompSeq (EL,source)) .Lifespan() < n ) ;

suppose n <= (AP:CompSeq (EL,source)) .Lifespan() ; :: thesis: ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v

then consider k being Nat such that
A20: n + k = (AP:CompSeq (EL,source)) .Lifespan() by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
n + k = (AP:CompSeq (EL,source)) .Lifespan() by A20;
hence ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v by A19, A18; :: thesis: verum

end;

suppose (AP:CompSeq (EL,source)) .Lifespan() < n ; :: thesis: ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v

then consider k being Nat such that
A21: ((AP:CompSeq (EL,source)) .Lifespan()) + k = n by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
((AP:CompSeq (EL,source)) .Lifespan()) + k = n by A21;
hence ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v by A4; :: thesis: verum

end;

end;

end;

hence ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v ; :: thesis: verum