:: Proof of Ford/Fulkerson's Maximum Network Flow Algorithm :: by Gilbert Lee :: :: Received February 22, 2005 :: Copyright (c) 2005-2012 Association of Mizar Users begin Lm1: for F being Function for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x} proofend; Lm2: for F being Function for x, y being set holds x in dom (F +* (x .--> y)) proofend; Lm3: for F being Function for x, y being set holds (F +* (x .--> y)) . x = y proofend; Lm4: for F being Function for x, y, z being set st x <> z holds (F +* (x .--> y)) . z = F . z proofend; begin definition let G be WGraph; attrG 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 proofend; 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 ) proofend; 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 ; predEL 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 ; funcEL .flow (source,sink) -> real number 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 number ; 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 ; predEL has_maximum_flow_from source,sink means :Def4: :: 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 Def4 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 ; prede 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 ; prede 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; predW is_augmenting_wrt EL means :Def8: :: 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 Def8 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 trivial holds W is_augmenting_wrt EL proofend; 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 proofend; 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 proofend; begin 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 ) ) proofend; 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 proofend; 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) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) if ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL ) otherwise VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))); coherence ( ( AP:NextBestEdges VL = {} implies VL is AP:VLabeling of EL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL implies VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL ) implies VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) is AP:VLabeling of EL ) ) proofend; consistency for b1 being AP:VLabeling of EL st AP:NextBestEdges VL = {} & AP:NextBestEdges VL <> {} & not (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL holds ( b1 = VL iff b1 = VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (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) . (choose (AP:NextBestEdges VL)) in dom VL implies AP:Step VL = VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL ) implies AP:Step VL = VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (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 proofend; 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 funcVS . 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) ) ) proofend; 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 proofend; 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} proofend; 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) proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) ) proofend; 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 ) ) proofend; 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) ) proofend; 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 ) ) proofend; 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)) proofend; begin 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, set ] 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)) ) ); funcW .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)) ) ) ) ) proofend; 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 proofend; 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 ; funcW .tolerance EL -> Nat means :Def16: :: GLIB_005:def 16 ( it in rng (W .flowSeq EL) & ( for k being real number st k in rng (W .flowSeq EL) holds it <= k ) ) if not W is trivial otherwise it = 0 ; existence ( ( not W is trivial implies ex b1 being Nat st ( b1 in rng (W .flowSeq EL) & ( for k being real number st k in rng (W .flowSeq EL) holds b1 <= k ) ) ) & ( W is trivial implies ex b1 being Nat st b1 = 0 ) ) proofend; uniqueness for b1, b2 being Nat holds ( ( not W is trivial & b1 in rng (W .flowSeq EL) & ( for k being real number st k in rng (W .flowSeq EL) holds b1 <= k ) & b2 in rng (W .flowSeq EL) & ( for k being real number st k in rng (W .flowSeq EL) holds b2 <= k ) implies b1 = b2 ) & ( W is trivial & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proofend; 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 ( ( not W is trivial implies ( b4 = W .tolerance EL iff ( b4 in rng (W .flowSeq EL) & ( for k being real number st k in rng (W .flowSeq EL) holds b4 <= k ) ) ) ) & ( W is trivial 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) ) ) ) ) proofend; 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 proofend; 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 proofend; 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; clusterES . 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; clusterES . 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; clusterES . 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) ) ) proofend; 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 proofend; 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() ; begin 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)))) proofend; 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)))) proofend; 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 not W is trivial & W is_augmenting_wrt EL holds 0 < W .tolerance EL proofend; 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 proofend; 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) proofend; 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 proofend; 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 proofend; 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 proofend; :: [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 proofend;