let G be finite real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for source being Vertex of G
for v being set holds
( v in dom (AP:FindAugPath EL,source) iff ex P being Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL ) )
let EL be FF:ELabeling of G; :: thesis: for source being Vertex of G
for v being set holds
( v in dom (AP:FindAugPath EL,source) iff ex P being Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL ) )
let source be Vertex of G; :: thesis: for v being set holds
( v in dom (AP:FindAugPath EL,source) iff ex P being Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL ) )
let v be set ; :: thesis: ( v in dom (AP:FindAugPath EL,source) iff ex P being Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL ) )
set CS = AP:CompSeq EL,source;
set V = dom (AP:FindAugPath EL,source);

hereby :: thesis: ( ex P being Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL ) implies v in dom (AP:FindAugPath EL,source) )

assume v in dom (AP:FindAugPath EL,source) ; :: thesis: ex P being Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL )
then ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom (AP:FindAugPath EL,source) ) by Th8;
hence ex P being Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL ) ; :: thesis: verum

end;

given P being Path of G such that A1: P is_Walk_from source,v and
A2: P is_augmenting_wrt EL ; :: thesis: v in dom (AP:FindAugPath EL,source)

now

P . ((2 * 0 ) + 1) = source by A1, GLIB_001:18;
then P . ((2 * 0 ) + 1) in {source} by TARSKI:def 1;
then A3: P . ((2 * 0 ) + 1) in dom ((AP:CompSeq EL,source) . 0 ) by Th4;
set Gn = (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() );
set Gn1 = (AP:CompSeq EL,source) . (((AP:CompSeq EL,source) .Lifespan() ) + 1);
defpred S₁[ Nat] means ( not $1 is even & $1 <= len P & not P . $1 in dom (AP:FindAugPath EL,source) );
assume A4: not v in dom (AP:FindAugPath EL,source) ; :: thesis: contradiction
P . (len P) = v by A1, GLIB_001:18;
then A5: ex n being Nat st S₁[n] by A4;
consider n being Nat such that
A6: ( S₁[n] & ( for k being Nat st S₁[k] holds
n <= k ) ) from NAT_1:sch 5(A5);
reconsider n9 = n as odd Element of NAT by A6, ORDINAL1:def 13;
A7: 1 <= n by A6, ABIAN:12;
dom ((AP:CompSeq EL,source) . 0 ) c= dom (AP:FindAugPath EL,source) by Th5;
then n <> 1 by A6, A3;
then 1 < n by A7, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then reconsider n2 = n9 - (2 * 1) as odd Element of NAT by INT_1:18;
A8: n2 < n - 0 by XREAL_1:17;
then A9: n2 < len P by A6, XXREAL_0:2;
then A10: P . n2 in dom (AP:FindAugPath EL,source) by A6, A8;
set Next = AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ));
set en = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )));
AP:CompSeq EL,source is halting by Th6;
then A11: (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) = (AP:CompSeq EL,source) . (((AP:CompSeq EL,source) .Lifespan() ) + 1) by GLIB_000:def 57;
set e = P . (n2 + 1);
A12: P . (n2 + 2) = P . n ;
then A13: P . (n2 + 1) Joins P . n2,P . n,G by A9, GLIB_001:def 3;

A14: now

per cases ( P . (n2 + 1) DJoins P . n2,P . n,G or not P . (n2 + 1) DJoins P . n2,P . n,G ) ;

suppose A15: P . (n2 + 1) DJoins P . n2,P . n,G ; :: thesis: AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) <> {}

then A16: (the_Source_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) by A10, GLIB_000:def 16;
A17: P . (n2 + 1) in the_Edges_of G by A15, GLIB_000:def 16;
A18: not (the_Target_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) by A6, A15, GLIB_000:def 16;
EL . (P . (n2 + 1)) < (the_Weight_of G) . (P . (n2 + 1)) by A2, A9, A12, A15, Def8;
then P . (n2 + 1) is_forward_edge_wrt (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) by A17, A16, A18, Def6;
hence AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) <> {} by Def9; :: thesis: verum

end;

suppose A19: not P . (n2 + 1) DJoins P . n2,P . n,G ; :: thesis: AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) <> {}

then A20: P . (n2 + 1) DJoins P . n,P . n2,G by A13, GLIB_000:19;
then A21: P . (n2 + 1) in the_Edges_of G by GLIB_000:def 16;
A22: (the_Target_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) by A10, A20, GLIB_000:def 16;
A23: not (the_Source_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) by A6, A20, GLIB_000:def 16;
0 < EL . (P . (n2 + 1)) by A2, A9, A12, A19, Def8;
then P . (n2 + 1) is_backward_edge_wrt (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) by A21, A23, A22, Def7;
hence AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) <> {} by Def9; :: thesis: verum

end;

end;

end;

A24: (AP:CompSeq EL,source) . (((AP:CompSeq EL,source) .Lifespan() ) + 1) = AP:Step ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) by Def12;

now

per cases ( not (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) or (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) ) ;

suppose A25: not (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) ; :: thesis: contradiction

then (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) = ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) +* (((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))))) by A24, A11, A14, Def10;
then A26: dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) = (dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))) \/ {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))} by Lm1;
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))} by TARSKI:def 1;
hence contradiction by A25, A26, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A27: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) ; :: thesis: contradiction

( choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))) is_forward_edge_wrt (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) or choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))) is_backward_edge_wrt (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) ) by A14, Def9;
then A28: not (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) by A27, Def6, Def7;
(AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) = ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) +* (((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))))) by A24, A11, A14, A27, Def10;
then A29: dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) = (dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))) \/ {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))} by Lm1;
(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))} by TARSKI:def 1;
hence contradiction by A28, A29, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence v in dom (AP:FindAugPath EL,source) ; :: thesis: verum