let G be real-weighted WGraph; :: thesis:
let EL be FF:ELabeling of G; :: thesis:
let source be Vertex of G; :: thesis:
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 :: thesis:

let n be Nat; :: thesis:
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 = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
assume A2: S₁[n] ; :: thesis:
A3: (AP:CompSeq (EL,source)) . (n + 1) = AP:Step ((AP:CompSeq (EL,source)) . n) by Def12;

now :: thesis:

per cases ;

suppose AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} ; :: thesis:

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

end;

suppose A4: AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} ; :: thesis:

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

now :: thesis:

per cases by A4, Def9;

suppose A5: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n ; :: thesis:

now :: thesis:

per cases by A11, A7, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis:

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:
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; :: thesis:

end;

suppose v in {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ; :: thesis:

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

now :: thesis:

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

suppose A19: (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = source ; :: thesis:

now :: thesis:

let n be odd Nat; :: thesis:
assume n < len P ; :: thesis:
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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))*> by A20, GLIB_001:def 5;
then A24: P . n = (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A22;
A25: P . (n + 2) = (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A22, A23;
A26: P . (n + 1) = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A22, A23;
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; :: thesis:
assume not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis:
hence 0 < EL . (P . (n + 1)) by A8, A24, A26, A25; :: thesis:

end;

hence P is_augmenting_wrt EL ; :: thesis:
thus P is_Walk_from source,v by A18, A19, A20, GLIB_001:15; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in P .vertices() ; :: thesis:
then x in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)),((the_Target_of G) . the Element of 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:

end;

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

end;

suppose A27: (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> source ; :: thesis:

A28: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),v,G by A8, A18;
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) . the Element of 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 the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
A32: not v in P .vertices() by A5, A18, A31;
A33: (the_Source_of G) . the Element of 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 P is open by GLIB_001:def 24;
then reconsider P2 = P .addEdge the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) as Path of G by A28, A33, A32, GLIB_001:151;
take P2 = P2; :: thesis:
thus P2 is_augmenting_wrt EL by A6, A9, A18, A29, A33, A32, Th3; :: thesis:
thus P2 is_Walk_from source,v by A30, A28, GLIB_001:66; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in P2 .vertices() ; :: thesis:
then A34: x in (P .vertices()) \/ {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} by A28, A33, GLIB_001:95;

now :: thesis:

per cases by A34, XBOOLE_0:def 3;

suppose x in P .vertices() ; :: thesis:

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

end;

suppose x in {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ; :: thesis:

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

end;

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

end;

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

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:

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:

end;

suppose A35: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_backward_edge_wrt (AP:CompSeq (EL,source)) . n ; :: thesis:

now :: thesis:

per cases by A41, A37, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis:

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:
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; :: thesis:

end;

suppose v in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ; :: thesis:

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

now :: thesis:

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

suppose A50: (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = source ; :: thesis:

now :: thesis:

let n be odd Nat; :: thesis:
assume n < len P ; :: thesis:
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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))*> by A51, GLIB_001:def 5;
then A55: P . (n + 1) = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A53;
P . n = (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A53, A54;
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; :: thesis:
assume not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis:
thus 0 < EL . (P . (n + 1)) by A35, A55; :: thesis:

end;

hence P is_augmenting_wrt EL ; :: thesis:
thus P is_Walk_from source,v by A49, A50, A51, GLIB_001:15; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in P .vertices() ; :: thesis:
then x in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)),((the_Target_of G) . the Element of 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:

end;

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

end;

suppose A56: (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> source ; :: thesis:

A57: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),v,G by A38, A49;
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) . the Element of 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 the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
A61: not v in P .vertices() by A35, A49, A60;
A62: (the_Target_of G) . the Element of 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 P is open by GLIB_001:def 24;
then reconsider P2 = P .addEdge the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) as Path of G by A57, A62, A61, GLIB_001:151;
take P2 = P2; :: thesis:
thus P2 is_augmenting_wrt EL by A36, A39, A49, A58, A62, A61, Th3; :: thesis:
thus P2 is_Walk_from source,v by A59, A57, GLIB_001:66; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in P2 .vertices() ; :: thesis:
then A63: x in (P .vertices()) \/ {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} by A57, A62, GLIB_001:95;

now :: thesis:

per cases by A63, XBOOLE_0:def 3;

suppose x in P .vertices() ; :: thesis:

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

end;

suppose x in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ; :: thesis:

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

end;

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

end;

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

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:

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:

end;

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

end;

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

end;

now :: thesis:

let v be set ; :: thesis:
assume A64: v in dom ((AP:CompSeq (EL,source)) . 0) ; :: thesis:
then reconsider v9 = v as Vertex of G ;
set P = G .walkOf v9;
take P = G .walkOf v9; :: thesis:
thus P is_augmenting_wrt EL by Th1; :: thesis:
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() = {v9} by GLIB_001:90;
hence P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) by A64, ZFMISC_1:31; :: thesis:

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: