let G be 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
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) )
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
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) )
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
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) )
set CS = AP:CompSeq (EL,source);
set G0 = (AP:CompSeq (EL,source)) . 0;
defpred S₁[ Nat] means for v being set st v in dom ((AP:CompSeq (EL,source)) . $1) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . $1) );

A1: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set Gn = (AP:CompSeq (EL,source)) . n;
set Gn1 = (AP:CompSeq (EL,source)) . (n + 1);
set Next = AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
set e = choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n));
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
A3: (AP:CompSeq (EL,source)) . (n + 1) = AP:Step ((AP:CompSeq (EL,source)) . n) by Def12;

now

per cases ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} or AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} ) ;

suppose AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} ; :: thesis: S₁[n + 1]

then (AP:CompSeq (EL,source)) . (n + 1) = (AP:CompSeq (EL,source)) . n by A3, Def10;
hence S₁[n + 1] by A2; :: thesis: verum

end;

suppose A4: AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} ; :: thesis: S₁[n + 1]

set se = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)));
set te = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)));

now

per cases ( choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n or choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) is_backward_edge_wrt (AP:CompSeq (EL,source)) . n ) by A4, Def9;

suppose A5: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n ; :: thesis: for v being set st v in dom ((AP:CompSeq (EL,source)) . (n + 1)) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

then A6: EL . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) < (the_Weight_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) by Def6;
let v be set ; :: thesis: ( v in dom ((AP:CompSeq (EL,source)) . (n + 1)) implies ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ) )
assume A7: v in dom ((AP:CompSeq (EL,source)) . (n + 1)) ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
A8: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) in the_Edges_of G by A5, Def6;
then A9: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) DJoins (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),G by GLIB_000:def 14;
A10: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . n) by A5, Def6;
then (AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))) .--> (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))) by A3, A4, Def10;
then A11: dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by Lm1;
(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by TARSKI:def 1;
then A12: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A11, XBOOLE_0:def 3;
A13: dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by A11, XBOOLE_1:7;
then A14: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A10;

now

per cases ( v in dom ((AP:CompSeq (EL,source)) . n) or v in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} ) by A11, A7, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

then consider P being Path of G such that
A15: P is_augmenting_wrt EL and
A16: P is_Walk_from source,v and
A17: P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) by A2;
take P = P; :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
thus ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ) by A13, A15, A16, A17, XBOOLE_1:1; :: thesis: verum

end;

suppose v in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

then A18: v = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) by TARSKI:def 1;

now

per cases ( (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) = source or (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) <> source ) ;

suppose A19: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) = source ; :: thesis: ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

set P = G .walkOf (((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))));
take P = G .walkOf (((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))); :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
A20: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) Joins (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),G by A8, GLIB_000:def 13;

now

let n be odd Nat; :: thesis: ( n < len P implies ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) ) )
assume n < len P ; :: thesis: ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) )
then n < 2 + 1 by A20, GLIB_001:14;
then n <= 2 * 1 by NAT_1:13;
then n < 1 + 1 by XXREAL_0:1;
then A21: n <= 1 by NAT_1:13;
1 <= n by ABIAN:12;
then A22: n = 1 by A21, XXREAL_0:1;
A23: P = <*((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))*> by A20, GLIB_001:def 5;
then A24: P . n = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) by A22, FINSEQ_1:45;
A25: P . (n + 2) = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) by A22, A23, FINSEQ_1:45;
A26: P . (n + 1) = choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) by A22, A23, FINSEQ_1:45;
hence ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) by A5, Def6; :: thesis: ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) )
assume not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: 0 < EL . (P . (n + 1))
hence 0 < EL . (P . (n + 1)) by A8, A24, A26, A25, GLIB_000:def 14; :: thesis: verum

end;

hence P is_augmenting_wrt EL by Def8; :: thesis: ( P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
thus P is_Walk_from source,v by A18, A19, A20, GLIB_001:15; :: thesis: P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))

now

let x be set ; :: thesis: ( x in P .vertices() implies x in dom ((AP:CompSeq (EL,source)) . (n + 1)) )
assume x in P .vertices() ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))
then x in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by A20, GLIB_001:91;
hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A12, A14, TARSKI:def 2; :: thesis: verum

end;

hence P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by TARSKI:def 3; :: thesis: verum

end;

suppose A27: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) <> source ; :: thesis: ex P2 being Path of G st
( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

A28: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) Joins (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),v,G by A8, A18, GLIB_000:def 13;
consider P being Path of G such that
A29: P is_augmenting_wrt EL and
A30: P is_Walk_from source,(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) and
A31: P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) by A2, A10;
set P2 = P .addEdge (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)));
A32: not v in P .vertices() by A5, A18, A31, Def6;
A33: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) = P .last() by A30, GLIB_001:def 23;
then P .first() <> P .last() by A27, A30, GLIB_001:def 23;
then not P is closed by GLIB_001:def 24;
then reconsider P2 = P .addEdge (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) as Path of G by A28, A33, A32, GLIB_001:151;
take P2 = P2; :: thesis: ( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
thus P2 is_augmenting_wrt EL by A6, A9, A18, A29, A33, A32, Th3; :: thesis: ( P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
thus P2 is_Walk_from source,v by A30, A28, GLIB_001:66; :: thesis: P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))

now

let x be set ; :: thesis: ( x in P2 .vertices() implies x in dom ((AP:CompSeq (EL,source)) . (n + 1)) )
assume x in P2 .vertices() ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))
then A34: x in (P .vertices()) \/ {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by A18, A28, A33, GLIB_001:95;

now

per cases ( x in P .vertices() or x in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} ) by A34, XBOOLE_0:def 3;

suppose x in P .vertices() ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))

then x in dom ((AP:CompSeq (EL,source)) . n) by A31;
hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A13; :: thesis: verum

end;

suppose x in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))

hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A11, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) ; :: thesis: verum

end;

hence P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ) ; :: thesis: verum

end;

end;

end;

hence ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ) ; :: thesis: verum

end;

suppose A35: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) is_backward_edge_wrt (AP:CompSeq (EL,source)) . n ; :: thesis: for v being set st v in dom ((AP:CompSeq (EL,source)) . (n + 1)) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

then A36: 0 < EL . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) by Def7;
let v be set ; :: thesis: ( v in dom ((AP:CompSeq (EL,source)) . (n + 1)) implies ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ) )
assume A37: v in dom ((AP:CompSeq (EL,source)) . (n + 1)) ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
A38: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) in the_Edges_of G by A35, Def7;
then A39: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) DJoins (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),G by GLIB_000:def 14;
A40: not (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . n) by A35, Def7;
then (AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))) .--> (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))) by A3, A4, Def10;
then A41: dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by Lm1;
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by TARSKI:def 1;
then A42: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A41, XBOOLE_0:def 3;
A43: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . n) by A35, Def7;
A44: dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by A41, XBOOLE_1:7;
then A45: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A43;

now

per cases ( v in dom ((AP:CompSeq (EL,source)) . n) or v in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} ) by A41, A37, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

then consider P being Path of G such that
A46: P is_augmenting_wrt EL and
A47: P is_Walk_from source,v and
A48: P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) by A2;
take P = P; :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
thus ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ) by A44, A46, A47, A48, XBOOLE_1:1; :: thesis: verum

end;

suppose v in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

then A49: v = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) by TARSKI:def 1;

now

per cases ( (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) = source or (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) <> source ) ;

suppose A50: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) = source ; :: thesis: ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

set P = G .walkOf (((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))));
take P = G .walkOf (((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))); :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
A51: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) Joins (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),G by A38, GLIB_000:def 13;

now

let n be odd Nat; :: thesis: ( n < len P implies ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) ) )
assume n < len P ; :: thesis: ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) )
then n < 2 + 1 by A51, GLIB_001:14;
then n <= 2 * 1 by NAT_1:13;
then n < 1 + 1 by XXREAL_0:1;
then A52: n <= 1 by NAT_1:13;
1 <= n by ABIAN:12;
then A53: n = 1 by A52, XXREAL_0:1;
A54: P = <*((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))*> by A51, GLIB_001:def 5;
then A55: P . (n + 1) = choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) by A53, FINSEQ_1:45;
P . n = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) by A53, A54, FINSEQ_1:45;
hence ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) by A43, A40, A55, GLIB_000:def 14; :: thesis: ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) )
assume not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: 0 < EL . (P . (n + 1))
thus 0 < EL . (P . (n + 1)) by A35, A55, Def7; :: thesis: verum

end;

hence P is_augmenting_wrt EL by Def8; :: thesis: ( P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
thus P is_Walk_from source,v by A49, A50, A51, GLIB_001:15; :: thesis: P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))

now

let x be set ; :: thesis: ( x in P .vertices() implies x in dom ((AP:CompSeq (EL,source)) . (n + 1)) )
assume x in P .vertices() ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))
then x in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by A51, GLIB_001:91;
hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A42, A45, TARSKI:def 2; :: thesis: verum

end;

hence P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by TARSKI:def 3; :: thesis: verum

end;

suppose A56: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) <> source ; :: thesis: ex P2 being Path of G st
( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )

A57: choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) Joins (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))),v,G by A38, A49, GLIB_000:def 13;
consider P being Path of G such that
A58: P is_augmenting_wrt EL and
A59: P is_Walk_from source,(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) and
A60: P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) by A2, A43;
set P2 = P .addEdge (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)));
A61: not v in P .vertices() by A35, A49, A60, Def7;
A62: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) = P .last() by A59, GLIB_001:def 23;
then P .first() <> P .last() by A56, A59, GLIB_001:def 23;
then not P is closed by GLIB_001:def 24;
then reconsider P2 = P .addEdge (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))) as Path of G by A57, A62, A61, GLIB_001:151;
take P2 = P2; :: thesis: ( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
thus P2 is_augmenting_wrt EL by A36, A39, A49, A58, A62, A61, Th3; :: thesis: ( P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )
thus P2 is_Walk_from source,v by A59, A57, GLIB_001:66; :: thesis: P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))

now

let x be set ; :: thesis: ( x in P2 .vertices() implies x in dom ((AP:CompSeq (EL,source)) . (n + 1)) )
assume x in P2 .vertices() ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))
then A63: x in (P .vertices()) \/ {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} by A49, A57, A62, GLIB_001:95;

now

per cases ( x in P .vertices() or x in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} ) by A63, XBOOLE_0:def 3;

suppose x in P .vertices() ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))

then x in dom ((AP:CompSeq (EL,source)) . n) by A60;
hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A44; :: thesis: verum

end;

suppose x in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))))} ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))

hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A41, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) ; :: thesis: verum

end;

hence P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ) ; :: thesis: verum

end;

end;

end;

hence ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ) ; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

now

let v be set ; :: thesis: ( v in dom ((AP:CompSeq (EL,source)) . 0) implies ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) ) )
assume A64: v in dom ((AP:CompSeq (EL,source)) . 0) ; :: thesis: ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) )
then reconsider v9 = v as Vertex of G ;
set P = G .walkOf v9;
take P = G .walkOf v9; :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) )
thus P is_augmenting_wrt EL by Th1; :: thesis: ( P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) )
v in {source} by A64, Th4;
then v = source by TARSKI:def 1;
hence P is_Walk_from source,v by GLIB_001:13; :: thesis: P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0)
P .vertices() = {v9} by GLIB_001:90;
hence P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) by A64, ZFMISC_1:31; :: thesis: verum

end;

then A65: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A65, A1);
hence for n being Nat
for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) ) ; :: thesis: verum