let G be finite real-weighted WGraph; :: thesis: for EL being FF:ELabeling of
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 ; :: 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);
assume A1: v in dom ((AP:CompSeq EL,source) . n) ; :: thesis: ((AP:CompSeq EL,source) . n) . v = (AP:FindAugPath EL,source) . v
defpred S1[ 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;
A2: S1[ 0 ] ;
now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; :: thesis: S1[k + 1]
set Gn = (AP:CompSeq EL,source) . (n + k);
set Gn1 = (AP:CompSeq EL,source) . ((n + k) + 1);
A4: (AP:CompSeq EL,source) . ((n + k) + 1) = AP:Step ((AP:CompSeq EL,source) . (n + k)) by Def15;
set Next = AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k));
set e = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k)));
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: S1[k + 1]
then (AP:CompSeq EL,source) . ((n + k) + 1) = (AP:CompSeq EL,source) . (n + k) by A4, Def14;
hence S1[k + 1] by A3; :: thesis: verum
end;
suppose A5: ( 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: S1[k + 1]
then A6: (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 A4, Def14;
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 A7: v in dom ((AP:CompSeq EL,source) . n) ; :: thesis: ((AP:CompSeq EL,source) . n) . v = ((AP:CompSeq EL,source) . ((n + k) + 1)) . v
then A8: ((AP:CompSeq EL,source) . n) . v = ((AP:CompSeq EL,source) . (n + k)) . v by A3;
dom ((AP:CompSeq EL,source) . n) c= dom ((AP:CompSeq EL,source) . (n + k)) by Th4, NAT_1:11;
then v <> (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k)))) by A5, A7;
hence ((AP:CompSeq EL,source) . n) . v = ((AP:CompSeq EL,source) . ((n + k) + 1)) . v by A6, A8, Tw2; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
suppose A9: ( 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: S1[k + 1]
then A10: (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 A4, Def14;
A11: ( 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 A9, Def13;
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 A12: v in dom ((AP:CompSeq EL,source) . n) ; :: thesis: ((AP:CompSeq EL,source) . n) . v = ((AP:CompSeq EL,source) . ((n + k) + 1)) . v
then A13: ((AP:CompSeq EL,source) . n) . v = ((AP:CompSeq EL,source) . (n + k)) . v by A3;
dom ((AP:CompSeq EL,source) . n) c= dom ((AP:CompSeq EL,source) . (n + k)) by Th4, NAT_1:11;
then v <> (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . (n + k)))) by A9, A11, A12, Def10, Def11;
hence ((AP:CompSeq EL,source) . n) . v = ((AP:CompSeq EL,source) . ((n + k) + 1)) . v by A10, A13, Tw2; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
then A14: for k being Element of NAT st S1[k] holds
S1[k + 1] ;
A15: for k being Element of NAT holds S1[k] from NAT_1:sch 1(A2, A14);
 A16: AP:CompSeq EL,source is halting by Th6;
defpred S2[ Element of NAT ] means (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) = (AP:CompSeq EL,source) . (((AP:CompSeq EL,source) .Lifespan() ) + $1);
A17: S2[ 0 ] ;
A18: now
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
set Gn1 = (AP:CompSeq EL,source) . ((((AP:CompSeq EL,source) .Lifespan() ) + k) + 1);
assume S2[k] ; :: thesis: S2[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 Def15
.= (AP:CompSeq EL,source) . (((AP:CompSeq EL,source) .Lifespan() ) + 1) by Def15 ;
hence S2[k + 1] by A16, GLIB_000:def 57; :: thesis: verum
end;
A19: for k being Element of NAT holds S2[k] from NAT_1:sch 1(A17, A18);
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 A1, A15; :: 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 A19; :: thesis: verum
end;
end;
end;
hence ((AP:CompSeq EL,source) . n) . v = (AP:FindAugPath EL,source) . v ; :: thesis: verum