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 FAP = AP:FindAugPath 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₁[ Element of 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₂[ Element of 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

let k be Element of 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 57; :: thesis: verum

end;

A3: S₂[ 0 ] ;
A4: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A3, A2);

now

let k be Element of 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 = choose (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

per cases ( AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k)) = {} or ( AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k)) <> {} & not (the_Source_of G) . (choose (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) . (choose (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) . (choose (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) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k))))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k))))) by A6, Def10;

now

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) . (choose (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) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k)))) in dom ((AP:CompSeq EL,source) . (n + k)) ) ; :: thesis: S₁[k + 1]

then A12: ( choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k))) is_forward_edge_wrt (AP:CompSeq EL,source) . (n + k) or choose (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) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k))))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k))))) by A6, A11, Def10;

now

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) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k)))) by A11, A12, A14, Def6, Def7;
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 Element of NAT st S₁[k] holds
S₁[k + 1] ;
A17: S₁[ 0 ] ;
A18: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(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

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 13;
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 13;
((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