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 S1[ 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 S2[ 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 S2[k] holds
S2[k + 1]
let k be 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 Def12
.= (AP:CompSeq (EL,source)) . (((AP:CompSeq (EL,source)) .Lifespan()) + 1) by Def12 ;
hence S2[k + 1] by A1, GLIB_000:def 56; :: thesis: verum
end;
A3: S2[ 0 ] ;
A4: for k being Nat holds S2[k] from NAT_1:sch 2(A3, A2);
now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[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: S1[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: S1[k + 1]
then (AP:CompSeq (EL,source)) . ((n + k) + 1) = (AP:CompSeq (EL,source)) . (n + k) by A6, Def10;
hence S1[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: S1[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 S1[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: S1[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 S1[k + 1] ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
then A16: for k being Nat st S1[k] holds
S1[k + 1] ;
A17: S1[ 0 ] ;
A18: for k being Nat holds S1[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