let G be finite natural-weighted WGraph; for EL being FF:ELabeling of G
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 G; 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 ; ( 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
A1:
EL has_valid_flow_from source,sink
and
A2:
for P being Path of G holds
( not P is_Walk_from source,sink or not P is_augmenting_wrt EL )
; EL has_maximum_flow_from source,sink
reconsider src = source as Vertex of G by A1, Def2;
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 A1 = EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)));
set B1 = (the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)));
set e = choose (AP:NextBestEdges (AP:FindAugPath (EL,src)));
AP:CompSeq (EL,src) is halting
by Th6;
then A3:
(AP:CompSeq (EL,src)) . (((AP:CompSeq (EL,src)) .Lifespan()) + 1) = AP:FindAugPath (EL,src)
by GLIB_000:def 55;
A4:
(AP:CompSeq (EL,src)) . (((AP:CompSeq (EL,src)) .Lifespan()) + 1) = AP:Step (AP:FindAugPath (EL,src))
by Def12;
A5:
now assume A6:
AP:NextBestEdges (AP:FindAugPath (EL,src)) <> {}
;
contradictionnow 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 A6, Def9;
suppose A7:
choose (AP:NextBestEdges (AP:FindAugPath (EL,src))) is_forward_edge_wrt AP:FindAugPath (
EL,
src)
;
contradictionthen
(the_Source_of G) . (choose (AP:NextBestEdges (AP:FindAugPath (EL,src)))) in V
by Def6;
then A8:
AP:FindAugPath (
EL,
src)
= (AP:FindAugPath (EL,src)) +* (((the_Target_of G) . (choose (AP:NextBestEdges (AP:FindAugPath (EL,src))))) .--> (choose (AP:NextBestEdges (AP:FindAugPath (EL,src)))))
by A4, A3, A6, Def10;
not
(the_Target_of G) . (choose (AP:NextBestEdges (AP:FindAugPath (EL,src)))) in V
by A7, Def6;
hence
contradiction
by A8, Lm2;
verum end; hence
contradiction
;
verum end;
A10:
now let x be
set ;
( 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 A11:
x in G .edgesDBetween (
V,
((the_Vertices_of G) \ V))
;
(EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x = ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . xthen A12:
(EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x = EL . x
by FUNCT_1:49;
A13:
x DSJoins V,
(the_Vertices_of G) \ V,
G
by A11, GLIB_000:def 31;
then
(the_Target_of G) . x in (the_Vertices_of G) \ V
by GLIB_000:def 16;
then A14:
not
(the_Target_of G) . x in V
by XBOOLE_0:def 5;
A15:
((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x = (the_Weight_of G) . x
by A11, FUNCT_1:49;
A16:
(the_Source_of G) . x in V
by A13, GLIB_000:def 16;
(EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x <= ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V)))) . x
by A1, A11, A12, A15, Def2;
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 A17, XXREAL_0:1;
verum end;
set E2 = G .edgesDBetween (((the_Vertices_of G) \ V),V);
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 ;
( 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 A18:
x in G .edgesDBetween (
((the_Vertices_of G) \ V),
V)
;
(EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x = (EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . xthen A19:
x DSJoins (the_Vertices_of G) \ V,
V,
G
by GLIB_000:def 31;
then A20:
(the_Target_of G) . x in V
by GLIB_000:def 16;
(the_Source_of G) . x in (the_Vertices_of G) \ V
by A19, GLIB_000:def 16;
then A21:
not
(the_Source_of G) . x in V
by XBOOLE_0:def 5;
A22:
(EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x = EL . x
by A18, FUNCT_1:49;
EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V)) = (G .edgesDBetween (((the_Vertices_of G) \ V),V)) --> 0
by PRE_POLY:def 13;
then
(EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x = 0
by A18, FUNCOP_1:7;
hence
(EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x = (EmptyBag (G .edgesDBetween (((the_Vertices_of G) \ V),V))) . x
by A23;
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 A24:
Sum (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))) = 0
by UPROOTS:11;
A25:
not sink in dom (AP:FindAugPath (EL,src))
by A2, Th9;
then
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 A1, Th10, Th11;
then
EL .flow (source,sink) = Sum ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V))))
by A10, A24, GLIB_004:6;
then
for X being FF:ELabeling of G st X has_valid_flow_from source,sink holds
X .flow (source,sink) <= EL .flow (source,sink)
by A25, Th10, Th12;
hence
EL has_maximum_flow_from source,sink
by A1, Def4; verum