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 :: thesis: v in dom (AP:FindAugPath (EL,source))

P . ((2 * 0) + 1) = source by A1, GLIB_001:17;
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 ( $1 is odd & $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:17;
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 12;
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:5;
A8: n2 < n - 0 by XREAL_1:15;
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 = the Element of 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 56;
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 :: thesis: AP:NextBestEdges ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) <> {}

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;
A17: P . (n2 + 1) in the_Edges_of G by A15;
A18: not (the_Target_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) by A6, A15;
EL . (P . (n2 + 1)) < (the_Weight_of G) . (P . (n2 + 1)) by A2, A9, A12, A15;
then P . (n2 + 1) is_forward_edge_wrt (AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan()) by A17, A16, A18;
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;
then A21: P . (n2 + 1) in the_Edges_of G ;
A22: (the_Target_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) by A10, A20;
A23: not (the_Source_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) by A6, A20;
0 < EL . (P . (n2 + 1)) by A2, A9, A12, A19;
then P . (n2 + 1) is_backward_edge_wrt (AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan()) by A21, A23, A22;
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 :: thesis: contradiction

per cases ( not (the_Source_of G) . the Element of 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) . the Element of 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) . the Element of 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan()))) .--> the Element of 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())))} by Lm1;
(the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) in {((the_Source_of G) . the Element of 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) in dom ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) ; :: thesis: contradiction

( the Element of 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 the Element of 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) in dom ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) by A27;
(AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan()) = ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) +* (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan()))) .--> the Element of 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())))} by Lm1;
(the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan())) in {((the_Target_of G) . the Element of 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