:: Proof of Ford/Fulkerson's Maximum Network Flow Algorithm :: by Gilbert Lee :: :: Received February 22, 2005 :: Copyright (c) 2005-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, XBOOLE_0, TARSKI, GLIB_003, VALUED_0, SUBSET_1, REAL_1, GRAPH_5, FINSET_1, ZFMISC_1, TREES_1, GLIB_000, PBOOLE, CARD_1, XXREAL_0, CARD_3, ARYTM_1, PARTFUN1, ARYTM_3, GLIB_001, ABIAN, NAT_1, FINSEQ_1, GRAPH_1, RCOMP_1, INT_1, PRE_POLY, UPROOTS, SGRAPH1, GLIB_005, XCMPLX_0; notations TARSKI, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, XCMPLX_0, XXREAL_0, XREAL_0, DOMAIN_1, RELAT_1, VALUED_0, PARTFUN1, FUNCT_1, PBOOLE, FINSEQ_1, FUNCT_2, GRAPH_5, UPROOTS, RELSET_1, FINSET_1, INT_1, NAT_1, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001, ABIAN, GLIB_002, GLIB_003, PRE_POLY; constructors DOMAIN_1, FUNCT_4, NAT_D, GRAPH_2, GRAPH_5, UPROOTS, GLIB_004, XXREAL_2, RELSET_1, FINSEQ_6; registrations XBOOLE_0, RELAT_1, PARTFUN1, INT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, GLIB_000, ABIAN, GLIB_001, GLIB_002, GLIB_003, VALUED_0, FUNCT_2, CARD_1, PRE_CIRC, PRE_POLY, RELSET_1; requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET; begin begin ::Preliminaries definitions for Maximum Flow Algorithm definition let G be WGraph; attr G is natural-weighted means :: GLIB_005:def 1 the_Weight_of G is natural-valued; end; registration cluster natural-weighted -> nonnegative-weighted for WGraph; end; registration cluster _finite _trivial Tree-like natural-weighted for WGraph; end; registration let G be natural-weighted WGraph; cluster the_Weight_of G -> natural-valued; 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, EL be FF:ELabeling of G, source,sink be set; pred EL has_valid_flow_from source,sink means :: 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; definition let G be _finite real-weighted WGraph, EL be FF:ELabeling of G, 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})); end; definition let G be _finite real-weighted WGraph, EL being FF:ELabeling of G, 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; definition let G be _Graph, EL be FF:ELabeling of G; mode AP:VLabeling of EL -> PartFunc of the_Vertices_of G, {1} \/ the_Edges_of G means :: GLIB_005:def 5 not contradiction; end; :: 1 used to mark source at the sart definition let G be real-weighted WGraph; let EL be FF:ELabeling of G, VL be AP:VLabeling of EL; let e be set; pred e is_forward_edge_wrt VL means :: 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; definition let G be real-weighted WGraph; let EL be FF:ELabeling of G, VL be AP:VLabeling of EL; let e be set; pred e is_backward_edge_wrt VL means :: 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; :: attribute with alternative structures definition let G be real-weighted WGraph, EL be FF:ELabeling of G, 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; theorem :: GLIB_005:1 for G being real-weighted WGraph, EL be FF:ELabeling of G, W being Walk of G st W is trivial holds W is_augmenting_wrt EL; theorem :: GLIB_005:2 for G being real-weighted WGraph, EL be FF:ELabeling of G, W being Walk of G, m,n be Nat st W is_augmenting_wrt EL holds W.cut(m,n) is_augmenting_wrt EL; theorem :: GLIB_005:3 for G being real-weighted WGraph, EL being FF:ELabeling of G, W being Walk of G, 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; begin :: Finding an Augmenting Path in a Graph definition let G be real-weighted WGraph; let EL be FF:ELabeling of G, VL be AP:VLabeling of EL; func AP:NextBestEdges(VL) -> Subset of the_Edges_of G means :: 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); end; definition let G be real-weighted WGraph; let EL be FF:ELabeling of G, VL be AP:VLabeling of EL; func AP:Step(VL) -> AP:VLabeling of EL equals :: 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)); end; definition let G be _Graph, EL be FF:ELabeling of G; mode AP:VLabelingSeq of EL -> ManySortedSet of NAT means :: GLIB_005:def 11 for n being Nat holds it.n is AP:VLabeling of EL; end; definition let G be _Graph, EL be FF:ELabeling of G; let VS be AP:VLabelingSeq of EL, n be Nat; redefine func VS.n -> AP:VLabeling of EL; end; definition let G be real-weighted WGraph, EL be FF:ELabeling of G; let source be Vertex of G; func AP:CompSeq(EL,source) -> AP:VLabelingSeq of EL means :: GLIB_005:def 12 it.0 = source .--> 1 & for n being Nat holds it.(n+1) = AP:Step(it.n); end; theorem :: GLIB_005:4 for G being real-weighted WGraph, EL be FF:ELabeling of G, source being Vertex of G holds dom (AP:CompSeq(EL,source).0) = {source}; theorem :: GLIB_005:5 for G being real-weighted WGraph, EL being FF:ELabeling of G, source being Vertex of G, i,j being Nat st i <= j holds dom (AP:CompSeq(EL, source).i) c= dom (AP:CompSeq(EL,source).j); definition let G be real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G; func AP:FindAugPath(EL,source) -> AP:VLabeling of EL equals :: GLIB_005:def 13 AP:CompSeq(EL, source).Result(); end; theorem :: GLIB_005:6 for G being _finite real-weighted WGraph, EL be FF:ELabeling of G, source being Vertex of G holds AP:CompSeq(EL,source) is halting; theorem :: GLIB_005:7 for G being _finite real-weighted WGraph, EL being FF:ELabeling of G, source being Vertex of G, n being Nat, v being set st v in dom (AP:CompSeq( EL,source).n) holds (AP:CompSeq(EL,source).n).v = (AP:FindAugPath(EL,source)).v ; definition let G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source,sink be Vertex of G; func AP:GetAugPath(EL,source,sink) -> vertex-distinct Path of G means :: 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); end; theorem :: GLIB_005:8 for G being real-weighted WGraph, EL being FF:ELabeling of G, source being Vertex of G, n being Nat, 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); theorem :: GLIB_005:9 for G being _finite real-weighted WGraph, EL being FF:ELabeling of G, source being Vertex of G, 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; theorem :: GLIB_005:10 for G being _finite real-weighted WGraph, EL being FF:ELabeling of G, source being Vertex of G holds source in dom AP:FindAugPath(EL,source); begin :: Ford-Fulkerson Algorithm definitions definition let G be natural-weighted WGraph, EL be FF:ELabeling of G, W be Walk of G; assume W is_augmenting_wrt EL; func W.flowSeq(EL) -> FinSequence of NAT means :: 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))); end; definition let G be natural-weighted WGraph, EL being FF:ELabeling of G, W be Walk of G; assume W is_augmenting_wrt EL; func W.tolerance(EL) -> Nat means :: 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 non trivial otherwise it = 0; end; definition let G be natural-weighted WGraph, EL being FF:ELabeling of G, P be Path of G; assume P is_augmenting_wrt EL; func FF:PushFlow(EL,P) -> FF:ELabeling of G means :: 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)); end; definition let G be _finite natural-weighted WGraph, EL being FF:ELabeling of G, sink, source be Vertex of G; func FF:Step(EL, source, sink) -> FF:ELabeling of G equals :: GLIB_005:def 18 FF:PushFlow(EL, AP:GetAugPath(EL,source,sink)) if sink in dom AP:FindAugPath(EL ,source) otherwise EL; end; definition let G be _Graph; mode FF:ELabelingSeq of G -> ManySortedSet of NAT means :: GLIB_005:def 19 for n being Nat holds it.n is FF:ELabeling of G; end; registration let G be _Graph, ES be FF:ELabelingSeq of G, n be Nat; cluster ES.n -> Function-like Relation-like; end; registration let G be _Graph, ES be FF:ELabelingSeq of G, n be Nat; cluster ES.n -> the_Edges_of G -defined; end; registration let G be _Graph, ES be FF:ELabelingSeq of G, n be Nat; cluster ES.n -> natural-valued total; end; definition let G be _finite natural-weighted WGraph, source, sink be Vertex of G; func FF:CompSeq(G,source,sink) -> FF:ELabelingSeq of G means :: 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); end; definition let G be _finite natural-weighted WGraph, 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(); end; begin :: Ford Fulkerson Maximum Flow Theorems theorem :: GLIB_005:11 for G being _finite real-weighted WGraph, EL being FF:ELabeling of G, source, sink being set, 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)); theorem :: GLIB_005:12 for G being _finite real-weighted WGraph, EL being FF:ELabeling of G, source,sink being set, 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)); theorem :: GLIB_005:13 for G being _finite natural-weighted WGraph, EL being FF:ELabeling of G, W being Walk of G st W is non trivial & W is_augmenting_wrt EL holds 0 < W.tolerance(EL); theorem :: GLIB_005:14 for G being _finite natural-weighted WGraph, EL being FF:ELabeling of G, source,sink being set, 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; theorem :: GLIB_005:15 for G being _finite natural-weighted WGraph, EL being FF:ELabeling of G, source,sink being set, 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); theorem :: GLIB_005:16 for G being _finite natural-weighted WGraph, source,sink being Vertex of G, n being Nat st source <> sink holds FF:CompSeq(G,source,sink).n has_valid_flow_from source,sink; theorem :: GLIB_005:17 for G being _finite natural-weighted WGraph,source,sink being Vertex of G st source <> sink holds FF:CompSeq(G,source,sink) is halting; theorem :: GLIB_005:18 for G being _finite natural-weighted WGraph, EL being FF:ELabeling of G, source,sink being set st EL has_valid_flow_from source,sink & not ex P being Path of G st P is_Walk_from source,sink & P is_augmenting_wrt EL holds EL has_maximum_flow_from source,sink; ::$N Ford/Fulkerson maximum flow algorithm theorem :: GLIB_005:19 for G being _finite natural-weighted WGraph, source, sink being Vertex of G st sink <> source holds FF:MaxFlow(G,source,sink) has_maximum_flow_from source,sink;