let G be finite natural-weighted WGraph; :: thesis: for EL being FF:ELabeling of
for source, sink being set st EL has_valid_flow_from source,sink & ( for P being Path of G holds
( not P is_Walk_from source,sink or not P is_augmenting_wrt EL ) ) holds
EL has_maximum_flow_from source,sink
let EL be FF:ELabeling of ; :: thesis: for source, sink being set st EL has_valid_flow_from source,sink & ( for P being Path of G holds
( not P is_Walk_from source,sink or not P is_augmenting_wrt EL ) ) holds
EL has_maximum_flow_from source,sink
let source, sink be set ; :: thesis: ( EL has_valid_flow_from source,sink & ( for P being Path of G holds
( not P is_Walk_from source,sink or not P is_augmenting_wrt EL ) ) implies EL has_maximum_flow_from source,sink )
assume that
A1a: EL has_valid_flow_from source,sink and
A1b: for P being Path of G holds
( not P is_Walk_from source,sink or not P is_augmenting_wrt EL ) ; :: thesis: EL has_maximum_flow_from source,sink
reconsider src = source as Vertex of G by A1a, Def7;
set CS = AP:CompSeq EL,src;
set Gn = AP:FindAugPath EL,src;
set Gn1 = (AP:CompSeq EL,src) . (((AP:CompSeq EL,src) .Lifespan() ) + 1);
reconsider V = dom (AP:FindAugPath EL,src) as Subset of (the_Vertices_of G) ;
set E1 = G .edgesDBetween V,((the_Vertices_of G) \ V);
set E2 = G .edgesDBetween ((the_Vertices_of G) \ V),V;
A5: not sink in dom (AP:FindAugPath EL,src) by A1b, Th9;
then A6: EL .flow source,sink = (Sum (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V))) by A1a, Th10, Th11;
set A1 = EL | (G .edgesDBetween V,((the_Vertices_of G) \ V));
set B1 = (the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V));
A7: AP:CompSeq EL,src is halting by Th6;
A8: (AP:CompSeq EL,src) . (((AP:CompSeq EL,src) .Lifespan() ) + 1) = AP:Step (AP:FindAugPath EL,src) by Def15;
A9: (AP:CompSeq EL,src) . (((AP:CompSeq EL,src) .Lifespan() ) + 1) = AP:FindAugPath EL,src by A7, GLIB_000:def 57;
set e = choose (AP:NextBestEdges (AP:FindAugPath EL,src));
A10: now
assume A11: AP:NextBestEdges (AP:FindAugPath EL,src) <> {} ; :: thesis: contradiction
now
per cases ( choose (AP:NextBestEdges (AP:FindAugPath EL,src)) is_forward_edge_wrt AP:FindAugPath EL,src or choose (AP:NextBestEdges (AP:FindAugPath EL,src)) is_backward_edge_wrt AP:FindAugPath EL,src ) by A11, Def13;
end;
end;
hence contradiction ; :: thesis: verum
end;
A17: now
let x be set ; :: thesis: ( x in G .edgesDBetween V,((the_Vertices_of G) \ V) implies (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x = ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x )
assume A18: x in G .edgesDBetween V,((the_Vertices_of G) \ V) ; :: thesis: (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x = ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x
then A19: ( (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x = EL . x & ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x = (the_Weight_of G) . x ) by FUNCT_1:72;
x DSJoins V,(the_Vertices_of G) \ V,G by A18, GLIB_000:def 33;
then A20: ( x in the_Edges_of G & (the_Source_of G) . x in V & (the_Target_of G) . x in (the_Vertices_of G) \ V ) by GLIB_000:def 18;
then A21: not (the_Target_of G) . x in V by XBOOLE_0:def 5;
A22: (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x <= ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x by A1a, A19, A20, Def7;
set e = choose (AP:NextBestEdges (AP:FindAugPath EL,src));
now
assume (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x < ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x ; :: thesis: contradiction
then x is_forward_edge_wrt AP:FindAugPath EL,src by A19, A20, A21, Def10;
hence contradiction by A10, Def13; :: thesis: verum
end;
hence (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x = ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x by A22, XXREAL_0:1; :: thesis: verum
end;
set A2 = EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V);
set B2 = EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V);
now
let x be set ; :: thesis: ( x in G .edgesDBetween ((the_Vertices_of G) \ V),V implies (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x = (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x )
assume A23: x in G .edgesDBetween ((the_Vertices_of G) \ V),V ; :: thesis: (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x = (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x
then A24: (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x = EL . x by FUNCT_1:72;
EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V) = (G .edgesDBetween ((the_Vertices_of G) \ V),V) --> 0 by POLYNOM1:def 15;
then A25: (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x = 0 by A23, FUNCOP_1:13;
x DSJoins (the_Vertices_of G) \ V,V,G by A23, GLIB_000:def 33;
then A26: ( x in the_Edges_of G & (the_Source_of G) . x in (the_Vertices_of G) \ V & (the_Target_of G) . x in V ) by GLIB_000:def 18;
then A27: not (the_Source_of G) . x in V by XBOOLE_0:def 5;
set e = choose (AP:NextBestEdges (AP:FindAugPath EL,src));
now
assume 0 < (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x ; :: thesis: contradiction
then x is_backward_edge_wrt AP:FindAugPath EL,src by A24, A26, A27, Def11;
hence contradiction by A10, Def13; :: thesis: verum
end;
hence (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x = (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x by A25; :: thesis: verum
end;
then Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) = Sum (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) by GLIB_004:6;
then Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) = 0 by UPROOTS:13;
then A28: EL .flow source,sink = Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) by A6, A17, GLIB_004:6;
for X being FF:ELabeling of st X has_valid_flow_from source,sink holds
X .flow source,sink <= EL .flow source,sink by Th10, A5, A28, Th12;
hence EL has_maximum_flow_from source,sink by A1a, Def9; :: thesis: verum