:: Proof of Ford/Fulkerson's Maximum Network Flow Algorithm
:: by Gilbert Lee
::
:: Received February 22, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users


Lm1: for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
proof end;

Lm2: for F being Function
for x, y being set holds x in dom (F +* (x .--> y))
proof end;

Lm3: for F being Function
for x, y being set holds (F +* (x .--> y)) . x = y
proof end;

Lm4: for F being Function
for x, y, z being set st x <> z holds
(F +* (x .--> y)) . z = F . z
proof end;

definition
let G be WGraph;
attr G is natural-weighted means :Def1: :: GLIB_005:def 1
 the_Weight_of G is natural-valued ;
end;

:: deftheorem Def1 defines natural-weighted GLIB_005:def 1 :
for G being WGraph holds
( G is natural-weighted iff the_Weight_of G is natural-valued );

registration
cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] natural-weighted -> nonnegative-weighted for set ;
coherence
for b1 being WGraph st b1 is natural-weighted holds
b1 is nonnegative-weighted
proof end;
end;

registration
cluster Relation-like NAT -defined Function-like finite finite-support [Graph-like] _finite _trivial Tree-like [Weighted] natural-weighted for set ;
existence
ex b1 being WGraph st
( b1 is _finite & b1 is _trivial & b1 is Tree-like & b1 is natural-weighted )
proof end;
end;

registration
let G be natural-weighted WGraph;
cluster the_Weight_of G -> natural-valued ;
coherence
the_Weight_of G is natural-valued by Def1;
end;

definition
let G be _Graph;
mode FF:ELabeling of G is natural-valued ManySortedSet of the_Edges_of G;
end;

:: NAT can be replaced by RAT but then we can convert it to the NAT case
:: as the graphs are finite
definition
let G be _finite real-weighted WGraph;
let EL be FF:ELabeling of G;
let source, sink be set ;
pred EL has_valid_flow_from source,sink means :Def2: :: GLIB_005:def 2
( source is Vertex of G & sink is Vertex of G & ( for e being set st e in the_Edges_of G holds
( 0 <= EL . e & EL . e <= (the_Weight_of G) . e ) ) & ( for v being Vertex of G st v <> source & v <> sink holds
Sum (EL | (v .edgesIn())) = Sum (EL | (v .edgesOut())) ) );
end;

:: deftheorem Def2 defines has_valid_flow_from GLIB_005:def 2 :
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set holds
( EL has_valid_flow_from source,sink iff ( source is Vertex of G & sink is Vertex of G & ( for e being set st e in the_Edges_of G holds
( 0 <= EL . e & EL . e <= (the_Weight_of G) . e ) ) & ( for v being Vertex of G st v <> source & v <> sink holds
Sum (EL | (v .edgesIn())) = Sum (EL | (v .edgesOut())) ) ) );

definition
let G be _finite real-weighted WGraph;
let EL be FF:ELabeling of G;
let source, sink be set ;
func EL .flow (source,sink) -> Real equals :: GLIB_005:def 3
(Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})));
coherence
(Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink}))) is Real ;
end;

:: deftheorem defines .flow GLIB_005:def 3 :
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set holds EL .flow (source,sink) = (Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})));

definition
let G be _finite real-weighted WGraph;
let EL be FF:ELabeling of G;
let source, sink be set ;
pred EL has_maximum_flow_from source,sink means :: GLIB_005:def 4
( EL has_valid_flow_from source,sink & ( for E2 being FF:ELabeling of G st E2 has_valid_flow_from source,sink holds
E2 .flow (source,sink) <= EL .flow (source,sink) ) );
end;

:: deftheorem defines has_maximum_flow_from GLIB_005:def 4 :
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set holds
( EL has_maximum_flow_from source,sink iff ( EL has_valid_flow_from source,sink & ( for E2 being FF:ELabeling of G st E2 has_valid_flow_from source,sink holds
E2 .flow (source,sink) <= EL .flow (source,sink) ) ) );

definition
let G be _Graph;
let EL be FF:ELabeling of G;
mode AP:VLabeling of EL -> PartFunc of (the_Vertices_of G),({1} \/ (the_Edges_of G)) means :Def5: :: GLIB_005:def 5
verum;
existence
ex b1 being PartFunc of (the_Vertices_of G),({1} \/ (the_Edges_of G)) st verum ;
end;

:: deftheorem Def5 defines AP:VLabeling GLIB_005:def 5 :
for G being _Graph
for EL being FF:ELabeling of G
for b3 being PartFunc of (the_Vertices_of G),({1} \/ (the_Edges_of G)) holds
( b3 is AP:VLabeling of EL iff verum );

:: 1 used to mark source at the sart
definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G;
let VL be AP:VLabeling of EL;
let e be set ;
pred e is_forward_edge_wrt VL means :Def6: :: GLIB_005:def 6
( e in the_Edges_of G & (the_Source_of G) . e in dom VL & not (the_Target_of G) . e in dom VL & EL . e < (the_Weight_of G) . e );
end;

:: deftheorem Def6 defines is_forward_edge_wrt GLIB_005:def 6 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for VL being AP:VLabeling of EL
for e being set holds
( e is_forward_edge_wrt VL iff ( e in the_Edges_of G & (the_Source_of G) . e in dom VL & not (the_Target_of G) . e in dom VL & EL . e < (the_Weight_of G) . e ) );

definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G;
let VL be AP:VLabeling of EL;
let e be set ;
pred e is_backward_edge_wrt VL means :Def7: :: GLIB_005:def 7
( e in the_Edges_of G & (the_Target_of G) . e in dom VL & not (the_Source_of G) . e in dom VL & 0 < EL . e );
end;

:: deftheorem Def7 defines is_backward_edge_wrt GLIB_005:def 7 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for VL being AP:VLabeling of EL
for e being set holds
( e is_backward_edge_wrt VL iff ( e in the_Edges_of G & (the_Target_of G) . e in dom VL & not (the_Source_of G) . e in dom VL & 0 < EL . e ) );

:: attribute with alternative structures
definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G;
let W be Walk of G;
pred W is_augmenting_wrt EL means :: GLIB_005:def 8
 for n being odd Nat st n < len W holds
( ( W . (n + 1) DJoins W . n,W . (n + 2),G implies EL . (W . (n + 1)) < (the_Weight_of G) . (W . (n + 1)) ) & ( not W . (n + 1) DJoins W . n,W . (n + 2),G implies 0 < EL . (W . (n + 1)) ) );
end;

:: deftheorem defines is_augmenting_wrt GLIB_005:def 8 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G holds
( W is_augmenting_wrt EL iff for n being odd Nat st n < len W holds
( ( W . (n + 1) DJoins W . n,W . (n + 2),G implies EL . (W . (n + 1)) < (the_Weight_of G) . (W . (n + 1)) ) & ( not W . (n + 1) DJoins W . n,W . (n + 2),G implies 0 < EL . (W . (n + 1)) ) ) );

theorem Th1: :: GLIB_005:1
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G st W is V5() holds
W is_augmenting_wrt EL
proof end;

theorem Th2: :: GLIB_005:2
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G
for m, n being Nat st W is_augmenting_wrt EL holds
W .cut (m,n) is_augmenting_wrt EL
proof end;

theorem Th3: :: GLIB_005:3
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G
for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds
W .addEdge e is_augmenting_wrt EL
proof end;

definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G;
let VL be AP:VLabeling of EL;
func AP:NextBestEdges VL -> Subset of (the_Edges_of G) means :Def9: :: GLIB_005:def 9
 for e being set holds
( e in it iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) );
existence
ex b1 being Subset of (the_Edges_of G) st
for e being set holds
( e in b1 iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) )
proof end;
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e being set holds
( e in b1 iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) ) & ( for e being set holds
( e in b2 iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines AP:NextBestEdges GLIB_005:def 9 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for VL being AP:VLabeling of EL
for b4 being Subset of (the_Edges_of G) holds
( b4 = AP:NextBestEdges VL iff for e being set holds
( e in b4 iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) );

definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G;
let VL be AP:VLabeling of EL;
func AP:Step VL -> AP:VLabeling of EL equals :Def10: :: GLIB_005:def 10
VL if AP:NextBestEdges VL = {}
VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) if ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL )
otherwise VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL);
coherence
( ( AP:NextBestEdges VL = {} implies VL is AP:VLabeling of EL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) )
proof end;
consistency
for b1 being AP:VLabeling of EL st AP:NextBestEdges VL = {} & AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL holds
( b1 = VL iff b1 = VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) ) ;
end;

:: deftheorem Def10 defines AP:Step GLIB_005:def 10 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for VL being AP:VLabeling of EL holds
( ( AP:NextBestEdges VL = {} implies AP:Step VL = VL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies AP:Step VL = VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies AP:Step VL = VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) ) );

definition
let G be _Graph;
let EL be FF:ELabeling of G;
mode AP:VLabelingSeq of EL -> ManySortedSet of NAT means :Def11: :: GLIB_005:def 11
 for n being Nat holds it . n is AP:VLabeling of EL;
existence
ex b1 being ManySortedSet of NAT st
for n being Nat holds b1 . n is AP:VLabeling of EL
proof end;
end;

:: deftheorem Def11 defines AP:VLabelingSeq GLIB_005:def 11 :
for G being _Graph
for EL being FF:ELabeling of G
for b3 being ManySortedSet of NAT holds
( b3 is AP:VLabelingSeq of EL iff for n being Nat holds b3 . n is AP:VLabeling of EL );

definition
let G be _Graph;
let EL be FF:ELabeling of G;
let VS be AP:VLabelingSeq of EL;
let n be Nat;
:: original: .
redefine func VS . n -> AP:VLabeling of EL;
coherence
VS . n is AP:VLabeling of EL by Def11;
end;

definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G;
let source be Vertex of G;
func AP:CompSeq (EL,source) -> AP:VLabelingSeq of EL means :Def12: :: GLIB_005:def 12
( it . 0 = source .--> 1 & ( for n being Nat holds it . (n + 1) = AP:Step (it . n) ) );
existence
ex b1 being AP:VLabelingSeq of EL st
( b1 . 0 = source .--> 1 & ( for n being Nat holds b1 . (n + 1) = AP:Step (b1 . n) ) )
proof end;
uniqueness
for b1, b2 being AP:VLabelingSeq of EL st b1 . 0 = source .--> 1 & ( for n being Nat holds b1 . (n + 1) = AP:Step (b1 . n) ) & b2 . 0 = source .--> 1 & ( for n being Nat holds b2 . (n + 1) = AP:Step (b2 . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines AP:CompSeq GLIB_005:def 12 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G
for b4 being AP:VLabelingSeq of EL holds
( b4 = AP:CompSeq (EL,source) iff ( b4 . 0 = source .--> 1 & ( for n being Nat holds b4 . (n + 1) = AP:Step (b4 . n) ) ) );

theorem Th4: :: GLIB_005:4
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G holds dom ((AP:CompSeq (EL,source)) . 0) = {source}
proof end;

theorem Th5: :: GLIB_005:5
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G
for i, j being Nat st i <= j holds
dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)
proof end;

definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G;
let source be Vertex of G;
func AP:FindAugPath (EL,source) -> AP:VLabeling of EL equals :: GLIB_005:def 13
(AP:CompSeq (EL,source)) .Result() ;
coherence
(AP:CompSeq (EL,source)) .Result() is AP:VLabeling of EL
proof end;
end;

:: deftheorem defines AP:FindAugPath GLIB_005:def 13 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G holds AP:FindAugPath (EL,source) = (AP:CompSeq (EL,source)) .Result() ;

theorem Th6: :: GLIB_005:6
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G holds AP:CompSeq (EL,source) is halting
proof end;

theorem Th7: :: GLIB_005:7
for G being _finite real-weighted WGraph
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
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
proof end;

definition
let G be _finite real-weighted WGraph;
let EL be FF:ELabeling of G;
let source, sink be Vertex of G;
func AP:GetAugPath (EL,source,sink) -> vertex-distinct Path of G means :Def14: :: GLIB_005:def 14
( it is_Walk_from source,sink & it is_augmenting_wrt EL & ( for n being even Nat st n in dom it holds
it . n = (AP:FindAugPath (EL,source)) . (it . (n + 1)) ) ) if sink in dom (AP:FindAugPath (EL,source))
otherwise it = G .walkOf source;
existence
( ( sink in dom (AP:FindAugPath (EL,source)) implies ex b1 being vertex-distinct Path of G st
( b1 is_Walk_from source,sink & b1 is_augmenting_wrt EL & ( for n being even Nat st n in dom b1 holds
b1 . n = (AP:FindAugPath (EL,source)) . (b1 . (n + 1)) ) ) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies ex b1 being vertex-distinct Path of G st b1 = G .walkOf source ) )
proof end;
uniqueness
for b1, b2 being vertex-distinct Path of G holds
( ( sink in dom (AP:FindAugPath (EL,source)) & b1 is_Walk_from source,sink & b1 is_augmenting_wrt EL & ( for n being even Nat st n in dom b1 holds
b1 . n = (AP:FindAugPath (EL,source)) . (b1 . (n + 1)) ) & b2 is_Walk_from source,sink & b2 is_augmenting_wrt EL & ( for n being even Nat st n in dom b2 holds
b2 . n = (AP:FindAugPath (EL,source)) . (b2 . (n + 1)) ) implies b1 = b2 ) & ( not sink in dom (AP:FindAugPath (EL,source)) & b1 = G .walkOf source & b2 = G .walkOf source implies b1 = b2 ) )
proof end;
consistency
for b1 being vertex-distinct Path of G holds verum ;
end;

:: deftheorem Def14 defines AP:GetAugPath GLIB_005:def 14 :
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being Vertex of G
for b5 being vertex-distinct Path of G holds
( ( sink in dom (AP:FindAugPath (EL,source)) implies ( b5 = AP:GetAugPath (EL,source,sink) iff ( b5 is_Walk_from source,sink & b5 is_augmenting_wrt EL & ( for n being even Nat st n in dom b5 holds
b5 . n = (AP:FindAugPath (EL,source)) . (b5 . (n + 1)) ) ) ) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies ( b5 = AP:GetAugPath (EL,source,sink) iff b5 = G .walkOf source ) ) );

theorem Th8: :: GLIB_005:8
for G being real-weighted WGraph
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) )
proof end;

theorem Th9: :: GLIB_005:9
for G being _finite real-weighted WGraph
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 ) )
proof end;

theorem Th10: :: GLIB_005:10
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G holds source in dom (AP:FindAugPath (EL,source))
proof end;

definition
let G be natural-weighted WGraph;
let EL be FF:ELabeling of G;
let W be Walk of G;
assume A1: W is_augmenting_wrt EL ;
defpred S1[ Nat, object ] means ( ( W . (2 * $1) DJoins W . ((2 * $1) - 1),W . ((2 * $1) + 1),G implies $2 = ((the_Weight_of G) . (W . (2 * $1))) - (EL . (W . (2 * $1))) ) & ( not W . (2 * $1) DJoins W . ((2 * $1) - 1),W . ((2 * $1) + 1),G implies $2 = EL . (W . (2 * $1)) ) );
func W .flowSeq EL -> FinSequence of NAT means :Def15: :: GLIB_005:def 15
( dom it = dom (W .edgeSeq()) & ( for n being Nat st n in dom it holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies it . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies it . n = EL . (W . (2 * n)) ) ) ) );
existence
ex b1 being FinSequence of NAT st
( dom b1 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b1 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b1 . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b1 . n = EL . (W . (2 * n)) ) ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st dom b1 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b1 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b1 . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b1 . n = EL . (W . (2 * n)) ) ) ) & dom b2 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b2 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b2 . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b2 . n = EL . (W . (2 * n)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines .flowSeq GLIB_005:def 15 :
for G being natural-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G st W is_augmenting_wrt EL holds
for b4 being FinSequence of NAT holds
( b4 = W .flowSeq EL iff ( dom b4 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b4 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b4 . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b4 . n = EL . (W . (2 * n)) ) ) ) ) );

definition
let G be natural-weighted WGraph;
let EL be FF:ELabeling of G;
let W be Walk of G;
assume A1: W is_augmenting_wrt EL ;
func W .tolerance EL -> Nat means :Def16: :: GLIB_005:def 16
( it in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
it <= k ) ) if W is V5()
otherwise it = 0 ;
existence
( ( W is V5() implies ex b1 being Nat st
( b1 in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
b1 <= k ) ) ) & ( W is V5() implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( W is V5() & b1 in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
b1 <= k ) & b2 in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
b2 <= k ) implies b1 = b2 ) & ( W is V5() & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Nat holds verum ;
end;

:: deftheorem Def16 defines .tolerance GLIB_005:def 16 :
for G being natural-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G st W is_augmenting_wrt EL holds
for b4 being Nat holds
( ( W is V5() implies ( b4 = W .tolerance EL iff ( b4 in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds
b4 <= k ) ) ) ) & ( W is V5() implies ( b4 = W .tolerance EL iff b4 = 0 ) ) );

definition
let G be natural-weighted WGraph;
let EL be FF:ELabeling of G;
let P be Path of G;
assume A1: P is_augmenting_wrt EL ;
func FF:PushFlow (EL,P) -> FF:ELabeling of G means :Def17: :: GLIB_005:def 17
( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
it . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies it . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies it . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) );
existence
ex b1 being FF:ELabeling of G st
( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b1 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) )
proof end;
uniqueness
for b1, b2 being FF:ELabeling of G st ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b1 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) & ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b2 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b2 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b2 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines FF:PushFlow GLIB_005:def 17 :
for G being natural-weighted WGraph
for EL being FF:ELabeling of G
for P being Path of G st P is_augmenting_wrt EL holds
for b4 being FF:ELabeling of G holds
( b4 = FF:PushFlow (EL,P) iff ( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b4 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b4 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b4 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) ) );

definition
let G be _finite natural-weighted WGraph;
let EL be FF:ELabeling of G;
let sink, source be Vertex of G;
func FF:Step (EL,source,sink) -> FF:ELabeling of G equals :Def18: :: GLIB_005:def 18
 FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) if sink in dom (AP:FindAugPath (EL,source))
otherwise EL;
correctness
coherence
( ( sink in dom (AP:FindAugPath (EL,source)) implies FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) is FF:ELabeling of G ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies EL is FF:ELabeling of G ) );
consistency
for b1 being FF:ELabeling of G holds verum;
;
end;

:: deftheorem Def18 defines FF:Step GLIB_005:def 18 :
for G being _finite natural-weighted WGraph
for EL being FF:ELabeling of G
for sink, source being Vertex of G holds
( ( sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = EL ) );

definition
let G be _Graph;
mode FF:ELabelingSeq of G -> ManySortedSet of NAT means :Def19: :: GLIB_005:def 19
 for n being Nat holds it . n is FF:ELabeling of G;
existence
ex b1 being ManySortedSet of NAT st
for n being Nat holds b1 . n is FF:ELabeling of G
proof end;
end;

:: deftheorem Def19 defines FF:ELabelingSeq GLIB_005:def 19 :
for G being _Graph
for b2 being ManySortedSet of NAT holds
( b2 is FF:ELabelingSeq of G iff for n being Nat holds b2 . n is FF:ELabeling of G );

registration
let G be _Graph;
let ES be FF:ELabelingSeq of G;
let n be Nat;
cluster ES . n -> Relation-like Function-like ;
coherence
( ES . n is Function-like & ES . n is Relation-like ) by Def19;
end;

registration
let G be _Graph;
let ES be FF:ELabelingSeq of G;
let n be Nat;
cluster ES . n -> the_Edges_of G -defined ;
coherence
ES . n is the_Edges_of G -defined by Def19;
end;

registration
let G be _Graph;
let ES be FF:ELabelingSeq of G;
let n be Nat;
cluster ES . n -> total natural-valued ;
coherence
( ES . n is natural-valued & ES . n is total ) by Def19;
end;

definition
let G be _finite natural-weighted WGraph;
let source, sink be Vertex of G;
func FF:CompSeq (G,source,sink) -> FF:ELabelingSeq of G means :Def20: :: GLIB_005:def 20
( it . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds it . (n + 1) = FF:Step ((it . n),source,sink) ) );
existence
ex b1 being FF:ELabelingSeq of G st
( b1 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b1 . (n + 1) = FF:Step ((b1 . n),source,sink) ) )
proof end;
uniqueness
for b1, b2 being FF:ELabelingSeq of G st b1 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b1 . (n + 1) = FF:Step ((b1 . n),source,sink) ) & b2 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b2 . (n + 1) = FF:Step ((b2 . n),source,sink) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines FF:CompSeq GLIB_005:def 20 :
for G being _finite natural-weighted WGraph
for source, sink being Vertex of G
for b4 being FF:ELabelingSeq of G holds
( b4 = FF:CompSeq (G,source,sink) iff ( b4 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b4 . (n + 1) = FF:Step ((b4 . n),source,sink) ) ) );

definition
let G be _finite natural-weighted WGraph;
let sink, source be Vertex of G;
func FF:MaxFlow (G,source,sink) -> FF:ELabeling of G equals :: GLIB_005:def 21
(FF:CompSeq (G,source,sink)) .Result() ;
coherence
(FF:CompSeq (G,source,sink)) .Result() is FF:ELabeling of G ;
end;

:: deftheorem defines FF:MaxFlow GLIB_005:def 21 :
for G being _finite natural-weighted WGraph
for sink, source being Vertex of G holds FF:MaxFlow (G,source,sink) = (FF:CompSeq (G,source,sink)) .Result() ;

theorem Th11: :: GLIB_005:11
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set
for V being Subset of (the_Vertices_of G) st EL has_valid_flow_from source,sink & source in V & not sink in V holds
EL .flow (source,sink) = (Sum (EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V))))) - (Sum (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))))
proof end;

theorem Th12: :: GLIB_005:12
for G being _finite real-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set
for V being Subset of (the_Vertices_of G) st EL has_valid_flow_from source,sink & source in V & not sink in V holds
EL .flow (source,sink) <= Sum ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V))))
proof end;

theorem Th13: :: GLIB_005:13
for G being _finite natural-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G st W is V5() & W is_augmenting_wrt EL holds
0 < W .tolerance EL
proof end;

theorem Th14: :: GLIB_005:14
for G being _finite natural-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set
for P being Path of G st source <> sink & EL has_valid_flow_from source,sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds
FF:PushFlow (EL,P) has_valid_flow_from source,sink
proof end;

theorem Th15: :: GLIB_005:15
for G being _finite natural-weighted WGraph
for EL being FF:ELabeling of G
for source, sink being set
for P being Path of G st source <> sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds
(EL .flow (source,sink)) + (P .tolerance EL) = (FF:PushFlow (EL,P)) .flow (source,sink)
proof end;

theorem Th16: :: GLIB_005:16
for G being _finite natural-weighted WGraph
for source, sink being Vertex of G
for n being Nat st source <> sink holds
(FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink
proof end;

theorem Th17: :: GLIB_005:17
for G being _finite natural-weighted WGraph
for source, sink being Vertex of G st source <> sink holds
FF:CompSeq (G,source,sink) is halting
proof end;

theorem Th18: :: GLIB_005:18
for G being _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
proof end;

:: WP: Ford/Fulkerson maximum flow algorithm
theorem :: GLIB_005:19
for G being _finite natural-weighted WGraph
for source, sink being Vertex of G st sink <> source holds
FF:MaxFlow (G,source,sink) has_maximum_flow_from source,sink
proof end;