:: Proof of Ford/Fulkerson's Maximum Network Flow Algorithm :: by Gilbert Lee :: :: Received February 22, 2005 :: Copyright (c) 2005-2016 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; 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; definitions TARSKI; equalities GLIB_000, GLIB_003, FUNCOP_1; expansions TARSKI, GLIB_000, GLIB_003; theorems CARD_1, CARD_2, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, GLIB_001, GLIB_004, GRAPH_5, ABIAN, INT_1, NAT_1, PBOOLE, PEPIN, TARSKI, UPROOTS, XBOOLE_0, XBOOLE_1, ZFMISC_1, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, VALUED_0, RELSET_1, PARTFUN1, RELAT_1; schemes NAT_1, SUBSET_1, FINSEQ_1, CLASSES1, RECDEF_1, PRE_CIRC; begin Lm1: for F being Function, x,y being set holds dom(F+*(x.-->y)) = dom F \/ {x} proof let F be Function, x,y be set; thus dom(F+*(x.-->y)) = dom F \/ dom(x.-->y) by FUNCT_4:def 1 .= dom F \/ {x} by FUNCOP_1:13; end; Lm2: for F being Function, x,y being set holds x in dom (F+*(x.-->y)) proof let F be Function, x,y being set; dom (x.-->y) = {x} by FUNCOP_1:13; then A1: x in dom (x.-->y) by TARSKI:def 1; dom (x.-->y) c= dom (F+*(x.-->y)) by FUNCT_4:10; hence thesis by A1; end; Lm3: for F being Function, x,y being set holds (F+*(x.-->y)).x = y proof let F be Function, x,y be set; dom (x.-->y) = {x} by FUNCOP_1:13; then x in dom (x.-->y) by TARSKI:def 1; hence (F+*(x.-->y)).x = (x.-->y).x by FUNCT_4:13 .= y by FUNCOP_1:72; end; Lm4: for F being Function, x,y,z being set st x <> z holds (F+*(x.-->y)).z = F .z proof let F be Function, x,y,z be set; assume x <> z; then not z in dom (x.-->y) by TARSKI:def 1; hence thesis by FUNCT_4:11; end; begin ::Preliminaries definitions for Maximum Flow Algorithm definition let G be WGraph; attr G is natural-weighted means :Def1: the_Weight_of G is natural-valued; end; registration cluster natural-weighted -> nonnegative-weighted for WGraph; coherence proof let G be WGraph; assume G is natural-weighted; then A1: the_Weight_of G is natural-valued; for y being object st y in rng the_Weight_of G holds y in Real>=0 by GRAPH_5:def 12,A1; then rng the_Weight_of G c= Real>=0; hence thesis; end; end; registration cluster finite trivial Tree-like natural-weighted for WGraph; existence proof set E = {}; set V = {1}; reconsider S = {} as Function of E,V by RELSET_1:12; set G1 = createGraph(V,E,S,S); set WL = the Function of the_Edges_of G1, NAT; set G2 = G1.set(WeightSelector, WL); take G2; thus G2 is finite & G2 is trivial & G2 is Tree-like; the_Weight_of G2 = WL by GLIB_000:8; hence thesis; end; end; registration let G be natural-weighted WGraph; cluster the_Weight_of G -> natural-valued; coherence 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, EL be FF:ELabeling of G, source,sink be set; pred EL has_valid_flow_from source,sink means :Def2: 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 Sum (EL | G.edgesInto({sink} )) - Sum (EL | G.edgesOutOf({sink})); coherence; 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 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 :Def5: not contradiction; existence; 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 :Def6: 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 :Def7: 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 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 Th1: 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 proof let G be real-weighted WGraph, EL be FF:ELabeling of G; let W be Walk of G; assume A1: W is trivial; now let n be odd Nat; assume n < len W; then n < 1 by A1,GLIB_001:126; hence (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))) by ABIAN:12; end; hence thesis; end; theorem Th2: 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 proof let G be real-weighted WGraph, EL be FF:ELabeling of G, W being Walk of G, m ,n be Nat; set W2 = W.cut(m,n); assume A1: W is_augmenting_wrt EL; now per cases; suppose A2: m is odd & n is odd & m <= n & n <= len W; then reconsider m9=m, n9 = n as odd Element of NAT by ORDINAL1:def 12; now let x be odd Nat; reconsider x9 = x as Element of NAT by ORDINAL1:def 12; set v1b = W2.x, eb = W2.(x+1), v2b = W2.(x+2); assume A3: x < len W2; then A4: x9 in dom W2 by GLIB_001:12; A5: m9 <= n9 by A2; A6: x9+2 in dom W2 by A3,GLIB_001:12; then A7: W2.(x9+2) = W.(m9+(x9+2)-1) by A2,A5,GLIB_001:47; x9+1 in dom W2 by A3,GLIB_001:12; then A8: W2.(x9+1) = W.(m9+(x9+1)-1) by A2,A5,GLIB_001:47; (m9+x9-1) in dom W by A2,A4,A5,GLIB_001:47; then reconsider a = m9+x-1,a2=m+(x+2)-1 as Element of NAT by A8; reconsider a as odd Element of NAT; set v1a = W.a, ea = W.(a+1), v2a = W.(a+2); (m9+(x9+2)-1) in dom W by A2,A6,A5,GLIB_001:47; then a2 <= len W by FINSEQ_3:25; then A9: m+(x+2)-1-2 < len W - 0 by XREAL_1:15; hereby assume eb DJoins v1b,v2b,G; then ea DJoins v1a,v2a,G by A2,A4,A5,A8,A7,GLIB_001:47; hence EL.eb < (the_Weight_of G).eb by A1,A8,A9; end; assume not eb DJoins v1b,v2b,G; then not ea DJoins v1a,v2a,G by A2,A4,A5,A8,A7,GLIB_001:47; hence 0 < EL.eb by A1,A8,A9; end; hence thesis; end; suppose not (m is odd & n is odd & m <= n & n <= len W); hence thesis by A1,GLIB_001:def 11; end; end; hence thesis; end; theorem Th3: 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 proof let G be real-weighted WGraph, EL being FF:ELabeling of G, W be Walk of G, e ,v be set; assume A1: W is_augmenting_wrt EL; set W2 = W.addEdge(e); assume that A2: not v in W.vertices() and A3: e DJoins W.last(),v,G & EL.e < (the_Weight_of G).e or e DJoins v,W .last(),G & 0 < EL.e; let n be odd Nat; A4: e Joins W.last(),v,G by A3; assume A5: n < len W2; now per cases; suppose A6: n < len W; reconsider n9 = n as Element of NAT by ORDINAL1:def 12; n9+1 in dom W by A6,GLIB_001:12; then A7: W.(n+1) = W2.(n+1) by A4,GLIB_001:65; n9+2 in dom W by A6,GLIB_001:12; then A8: W.(n+2) = W2.(n+2) by A4,GLIB_001:65; n9 in dom W by A6,GLIB_001:12; then W.n = W2.n by A4,GLIB_001:65; hence thesis by A1,A6,A7,A8; end; suppose A9: n >= len W; n+1 <= len W2 by A5,NAT_1:13; then n+1 <= len W + 2*1 by A4,GLIB_001:64; then n+1 < len W + 1+1 by XXREAL_0:1; then n+1 <= len W + 1 by NAT_1:13; then A10: n <= len W by XREAL_1:6; then A11: n = len W by A9,XXREAL_0:1; then A12: W2.(n+1) = e by A4,GLIB_001:65; 1 <= n by ABIAN:12; then n in dom W by A10,FINSEQ_3:25; then A13: W2.n = W.n by A4,GLIB_001:65 .= W.last() by A11,GLIB_001:def 7; not e DJoins W.last(),v,G or not e DJoins v,W.last(),G by A2,GLIB_001:88; hence W2.(n+1) DJoins W2.n, W2.(n+2),G implies EL.(W2.(n+1)) < ( the_Weight_of G).(W2.(n+1)) by A3,A13,A12; assume not W2.(n+1) DJoins W2.n, W2.(n+2),G; hence 0 < EL.(W2.(n+1)) by A3,A4,A11,A13,A12,GLIB_001:65; end; end; hence thesis; end; 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 :Def9: for e being set holds e in it iff (e is_forward_edge_wrt VL or e is_backward_edge_wrt VL); existence proof defpred P[set] means $1 is_forward_edge_wrt VL or $1 is_backward_edge_wrt VL; consider IT being Subset of the_Edges_of G such that A1: for e being set holds e in IT iff e in the_Edges_of G & P[e] from SUBSET_1:sch 1; take IT; let e be set; thus e in IT implies P[e] by A1; assume A2: P[e]; then e in the_Edges_of G by Def6,Def7; hence thesis by A1,A2; end; uniqueness proof let IT1,IT2 be Subset of the_Edges_of G such that A3: for e being set holds e in IT1 iff (e is_forward_edge_wrt VL or e is_backward_edge_wrt VL) and A4: for e being set holds e in IT2 iff (e is_forward_edge_wrt VL or e is_backward_edge_wrt VL); now let e be object; reconsider ee=e as set by TARSKI:1; hereby assume e in IT1; then ee is_forward_edge_wrt VL or ee is_backward_edge_wrt VL by A3; hence e in IT2 by A4; end; assume e in IT2; then ee is_forward_edge_wrt VL or ee is_backward_edge_wrt VL by A4; hence e in IT1 by A3; end; hence thesis by TARSKI:2; end; 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 :Def10: 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 proof set cNB = the Element of AP:NextBestEdges(VL); set SG = the_Source_of G, TG = the_Target_of G, VG = the_Vertices_of G, EG = the_Edges_of G, NB = AP:NextBestEdges(VL); per cases; suppose NB = {}; hence thesis; end; suppose NB <> {}; then A1: cNB in NB; A2: {SG.cNB} c= VG proof let x be object; assume x in {SG.cNB}; then x = SG.cNB by TARSKI:def 1; hence thesis by A1,FUNCT_2:5; end; {cNB} c= EG proof let x be object; assume x in {cNB}; then x = cNB by TARSKI:def 1; hence thesis by A1; end; then A3: {cNB} c= {1} \/ EG by XBOOLE_1:10; rng (TG.cNB .--> cNB) c= {cNB} by FUNCOP_1:13; then rng (TG.cNB .--> cNB) c= {1} \/ EG by A3; then A4: rng VL \/ rng (TG.cNB .--> cNB) c= {1} \/ EG by XBOOLE_1:8; rng (VL+*(TG.cNB .--> cNB)) c= rng VL \/ rng (TG.cNB .--> cNB) by FUNCT_4:17; then A5: rng (VL+*(TG.cNB .--> cNB)) c= {1} \/ EG by A4; {cNB} c= EG proof let x be object; assume x in {cNB}; then x = cNB by TARSKI:def 1; hence thesis by A1; end; then A6: {cNB} c= {1} \/ EG by XBOOLE_1:10; rng (SG.cNB .--> cNB) c= {cNB} by FUNCOP_1:13; then rng (SG.cNB .--> cNB) c= {1} \/ EG by A6; then A7: rng VL \/ rng (SG.cNB .--> cNB) c= {1} \/ EG by XBOOLE_1:8; rng (VL+*(SG.cNB .--> cNB)) c= rng VL \/ rng (SG.cNB .--> cNB) by FUNCT_4:17; then A8: rng (VL+*(SG.cNB .--> cNB)) c= {1} \/ EG by A7; A9: {TG.cNB} c= VG proof let x be object; assume x in {TG.cNB}; then x = TG.cNB by TARSKI:def 1; hence thesis by A1,FUNCT_2:5; end; dom (VL+*(TG.cNB .--> cNB)) = dom VL \/ dom (TG.cNB .--> cNB) by FUNCT_4:def 1 .= dom VL \/ {TG.cNB} by FUNCOP_1:13; then A10: VL+*(TG.cNB .--> cNB) is Relation of VG, {1} \/ EG by A9,A5,RELSET_1:4 ,XBOOLE_1:8; dom (VL+*(SG.cNB .--> cNB)) = dom VL \/ dom (SG.cNB .--> cNB) by FUNCT_4:def 1 .= dom VL \/ {SG.cNB} by FUNCOP_1:13; then VL+*(SG.cNB .--> cNB) is Relation of VG, {1} \/ EG by A2,A8, RELSET_1:4,XBOOLE_1:8; hence thesis by A10,Def5; end; end; consistency; end; definition let G be _Graph, EL be FF:ELabeling of G; mode AP:VLabelingSeq of EL -> ManySortedSet of NAT means :Def11: for n being Nat holds it.n is AP:VLabeling of EL; existence proof set f = NAT --> {}; reconsider f as ManySortedSet of NAT; take f; let n be Nat; n in NAT by ORDINAL1:def 12; then f.n = {} by FUNCOP_1:7; then f.n is PartFunc of the_Vertices_of G, {1} \/ the_Edges_of G by RELSET_1:12; hence thesis by Def5; end; 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; coherence by Def11; 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 :Def12: it.0 = source .--> 1 & for n being Nat holds it.(n+1) = AP:Step(it.n); existence proof defpred P[set,set,set] means ($2 is AP:VLabeling of EL & ex Gn,Gn1 being AP:VLabeling of EL st $2 = Gn & $3 = Gn1 & Gn1 = AP:Step(Gn)) or (not $2 is AP:VLabeling of EL & $2 = $3); A1: rng (source .--> 1) = {1} by FUNCOP_1:8; now let n,x be set; now per cases; suppose x is AP:VLabeling of EL; then reconsider Gn=x as AP:VLabeling of EL; P[n,x,AP:Step(Gn)]; hence ex y being set st P[n,x,y]; end; suppose not x is AP:VLabeling of EL; hence ex y being set st P[n,x,y]; end; end; hence ex y being set st P[n,x,y]; end; then A2: for n being Nat for x being set ex y being set st P[n,x,y]; consider IT being Function such that A3: dom IT = NAT & IT.0 = source.--> 1 & for n being Nat holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A2); reconsider IT as ManySortedSet of NAT by A3,PARTFUN1:def 2,RELAT_1:def 18; defpred P2[Nat] means IT.$1 is AP:VLabeling of EL; A4: now let n be Nat; assume A5: P2[n]; ex Gn,Gn1 being AP:VLabeling of EL st IT.n = Gn & IT.(n+1 ) = Gn1 & Gn1 = AP:Step(Gn) by A3,A5; hence P2[n+1]; end; dom (source .--> 1) = {source} by FUNCOP_1:13; then source .--> 1 is Relation of the_Vertices_of G, {1} \/ the_Edges_of G by A1,RELSET_1:4,XBOOLE_1:7; then A6: P2[ 0 ] by A3,Def5; for n being Nat holds P2[n] from NAT_1:sch 2(A6,A4); then reconsider IT as AP:VLabelingSeq of EL by Def11; take IT; thus IT.0 = source.-->1 by A3; let n be Nat; ex Gn,Gn1 being AP:VLabeling of EL st IT.n = Gn & IT.(n+1) = Gn1 & Gn1 = AP:Step(Gn) by A3; hence thesis; end; uniqueness proof let IT1,IT2 be AP:VLabelingSeq of EL such that A7: IT1.0 = source.-->1 and A8: for n being Nat holds IT1.(n+1) = AP:Step(IT1.n) and A9: IT2.0 = source.-->1 and A10: for n being Nat holds IT2.(n+1) = AP:Step(IT2.n); defpred P[Nat] means IT1.$1 = IT2.$1; now let n be Nat; assume P[n]; then IT1.(n+1) = AP:Step(IT2.n) by A8 .= IT2.(n+1) by A10; hence P[n+1]; end; then A11: for n being Nat st P[n] holds P[n+1]; A12: P[ 0 ] by A7,A9; for n being Nat holds P[n] from NAT_1:sch 2(A12,A11); then for n being object st n in NAT holds IT1.n = IT2.n; hence IT1 = IT2 by PBOOLE:3; end; end; theorem Th4: 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} proof let G be real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G; AP:CompSeq(EL,source).0 = source .--> 1 by Def12; hence thesis by FUNCOP_1:13; end; theorem Th5: 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) proof let G be real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G, i,j be Nat; set CS = AP:CompSeq(EL,source); defpred P[Nat] means dom (CS.i) c= dom (CS.(i+$1)); assume i <= j; then consider k being Nat such that A1: j = i+k by NAT_1:10; A2: now let n be Nat; set Gn = (CS.(i+n)), Gn1 = (CS.(i+(n+1))); set Next = AP:NextBestEdges(Gn), e = the Element of Next; Gn1 = (CS.(i+n+1)); then A3: Gn1 = AP:Step(Gn) by Def12; assume A4: P[n]; now per cases; suppose Next = {}; hence P[n+1] by A4,A3,Def10; end; suppose Next <> {} & not (the_Source_of G).e in dom Gn; then Gn1 = Gn+*((the_Source_of G).e .--> e) by A3,Def10; then dom Gn c= dom Gn1 by FUNCT_4:10; hence P[n+1] by A4,XBOOLE_1:1; end; suppose Next <> {} & (the_Source_of G).e in dom Gn; then Gn1 = Gn+*((the_Target_of G).e .--> e) by A3,Def10; then dom Gn c= dom Gn1 by FUNCT_4:10; hence P[n+1] by A4,XBOOLE_1:1; end; end; hence P[n+1]; end; A5: P[ 0 ]; A6: for n being Nat holds P[n] from NAT_1:sch 2(A5,A2); thus thesis by A6,A1; end; 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 AP:CompSeq(EL, source).Result(); coherence proof set CS = AP:CompSeq(EL,source); CS.Result() = CS.(CS.Lifespan()); hence thesis; end; end; theorem Th6: 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 proof let G be finite real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G; set CS = AP:CompSeq(EL,source); now set x = card the_Vertices_of G; defpred P[Nat] means card dom (CS.$1) = $1+1; assume A1: for n being Nat holds CS.n <> CS.(n+1); A2: now let n be Nat; set Gn = CS.n, Gn1 = CS.(n+1); set Next = AP:NextBestEdges(Gn), e = the Element of Next; A3: Gn1 = AP:Step(Gn) by Def12; assume A4: P[n]; now per cases; suppose Next = {}; then Gn = CS.(n+1) by A3,Def10; hence P[n+1] by A1; end; suppose A5: Next <> {} & not (the_Source_of G).e in dom Gn; then Gn1 = Gn+*((the_Source_of G).e .--> e) by A3,Def10; then dom Gn1 = dom Gn \/ {(the_Source_of G).e} by Lm1; hence P[n+1] by A4,A5,CARD_2:41; end; suppose A6: Next <> {} & (the_Source_of G).e in dom Gn; then Gn1 = Gn+*((the_Target_of G).e .--> e) by A3,Def10; then A7: dom Gn1 = dom Gn \/ {(the_Target_of G).e} by Lm1; e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by A6,Def9; then not (the_Target_of G).e in dom Gn by A6; hence P[n+1] by A4,A7,CARD_2:41; end; end; hence P[n+1]; end; dom (CS.0) = {source} by Th4; then A8: P[ 0 ] by CARD_1:30; for n being Nat holds P[n] from NAT_1:sch 2(A8,A2); then card dom (CS.x) = card the_Vertices_of G + 1; then 1+card the_Vertices_of G<=card the_Vertices_of G+0 by NAT_1:43; hence contradiction by XREAL_1:6; end; hence thesis; end; theorem Th7: 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 proof let G be finite real-weighted WGraph, EL being FF:ELabeling of G, source be Vertex of G, n be Nat, v be set; set SG = the_Source_of G, TG = the_Target_of G; set CS = AP:CompSeq(EL,source); set L = CS.Lifespan(), GL = CS.L, GL1 = CS.(L+1); defpred P[Nat] means for v being set st v in dom (CS.n) holds (CS.n).v = (CS.(n+$1)).v; defpred P2[Nat] means GL = CS.(L+$1); A1: CS is halting by Th6; A2: now let k be Nat; set Gn1 = CS.(L+k+1); assume P2[k]; then Gn1 = AP:Step(GL) by Def12 .= GL1 by Def12; hence P2[k+1] by A1,GLIB_000:def 55; end; A3: P2[ 0 ]; A4: for k being Nat holds P2[k] from NAT_1:sch 2(A3,A2); now let k be Nat; assume A5: P[k]; set Gn = CS.(n+k), Gn1 = CS.(n+k+1); set Next = AP:NextBestEdges(Gn), e = the Element of Next; A6: Gn1 = AP:Step(Gn) by Def12; now per cases; suppose Next = {}; then Gn1 = Gn by A6,Def10; hence P[k+1] by A5; end; suppose A7: Next <> {} & not SG.e in dom Gn; then A8: Gn1 = Gn+*(SG.e .--> e) by A6,Def10; now let v be set; assume A9: v in dom (CS.n); then A10: (CS.n).v = Gn.v by A5; dom (CS.n) c= dom Gn by Th5,NAT_1:11; then v <> SG.e by A7,A9; hence (CS.n).v = Gn1.v by A8,A10,Lm4; end; hence P[k+1]; end; suppose A11: Next <> {} & SG.e in dom Gn; then A12: e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by Def9; A13: Gn1 = Gn+*(TG.e .--> e) by A6,A11,Def10; now let v be set; assume A14: v in dom (CS.n); then A15: (CS.n).v = Gn.v by A5; dom (CS.n) c= dom Gn by Th5,NAT_1:11; then v <> TG.e by A11,A12,A14; hence (CS.n).v = Gn1.v by A13,A15,Lm4; end; hence P[k+1]; end; end; hence P[k+1]; end; then A16: for k being Nat st P[k] holds P[k+1]; A17: P[ 0 ]; A18: for k being Nat holds P[k] from NAT_1:sch 2(A17,A16); assume A19: v in dom (CS.n); now per cases; suppose n <= CS.Lifespan(); then consider k being Nat such that A20: n + k = CS.Lifespan() by NAT_1:10; reconsider k as Element of NAT by ORDINAL1:def 12; n + k = CS.Lifespan() by A20; hence thesis by A19,A18; end; suppose CS.Lifespan() < n; then consider k being Nat such that A21: CS.Lifespan() + k = n by NAT_1:10; reconsider k as Element of NAT by ORDINAL1:def 12; CS.Lifespan() + k = n by A21; hence thesis by A4; end; end; hence thesis; end; 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 :Def14 : 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 proof set CS = AP:CompSeq(EL,source), FAP = AP:FindAugPath(EL,source); defpred P[Nat] means for v being set st v in dom (CS.$1) ex P being vertex-distinct Path of G st P is_Walk_from source,v & P is_augmenting_wrt EL & P.vertices() c= dom (CS.$1) & for n being even Nat st n in dom P holds P.n = FAP.(P.(n+1)); now let n be Nat; assume A1: P[n]; set Gn = CS.n, Gn1 = CS.(n+1); set Next = AP:NextBestEdges(Gn), e = the Element of Next; A2: Gn1 = AP:Step(Gn) by Def12; now per cases; suppose Next = {}; then Gn1 = Gn by A2,Def10; hence P[n+1] by A1; end; suppose A3: Next <> {} & not (the_Source_of G).e in dom Gn; then A4: e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by Def9; then A5: 0 < EL.e by A3; A6: e in Next by A3; A7: Gn1 = Gn+*((the_Source_of G).e .--> e) by A2,A3,Def10; then A8: dom Gn1 = dom Gn \/ {(the_Source_of G).e} by Lm1; A9: (the_Target_of G).e in dom Gn by A3,A4; now let v be set; assume A10: v in dom Gn1; now per cases by A8,A10,XBOOLE_0:def 3; suppose v in dom Gn; then consider P being vertex-distinct Path of G such that A11: P is_Walk_from source,v and A12: P is_augmenting_wrt EL and A13: P.vertices() c= dom Gn and A14: for n being even Nat st n in dom P holds P.n = FAP.(P .(n+1)) by A1; take P; dom Gn c= dom Gn1 by Th5,NAT_1:11; hence P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom Gn1 & for n being even Nat st n in dom P holds P.n = FAP.(P. (n+1)) by A11,A12,A13,A14; end; suppose A15: v in {(the_Source_of G).e}; then A16: v = (the_Source_of G).e by TARSKI:def 1; now consider W being vertex-distinct Path of G such that A17: W is_Walk_from source, (the_Target_of G).e and A18: W is_augmenting_wrt EL and A19: W.vertices() c= dom Gn and A20: for n being even Nat st n in dom W holds W.n = FAP. (W.(n+1)) by A1,A9; set W2 = W.addEdge(e); A21: W.last() = (the_Target_of G).e by A17,GLIB_001:def 23; then A22: e Joins W.last(),(the_Source_of G).e,G by A6; A23: not (the_Source_of G).e in W.vertices() by A3,A19; then reconsider W2 as vertex-distinct Walk of G by A22, GLIB_001:155; take W2; W.first() = source by A17,GLIB_001:def 23; hence W2 is_Walk_from source,v by A16,A22,GLIB_001:63; e DJoins (the_Source_of G).e,W.last(),G by A6,A21; hence W2 is_augmenting_wrt EL by A5,A18,A23,Th3; A24: W2.vertices() = W.vertices() \/ {v} by A16,A22,GLIB_001:95; now let x be object; assume A25: x in W2.vertices(); now per cases by A24,A25,XBOOLE_0:def 3; suppose A26: x in W.vertices(); A27: dom Gn c= dom Gn1 by Th5,NAT_1:11; x in dom Gn by A19,A26; hence x in dom Gn1 by A27; end; suppose x in {v}; hence x in dom Gn1 by A8,A16,XBOOLE_0:def 3; end; end; hence x in dom Gn1; end; hence W2.vertices() c= dom Gn1; let n be even Nat; assume A28: n in dom W2; then A29: n <= len W2 by FINSEQ_3:25; A30: 1 <= n by A28,FINSEQ_3:25; now per cases; suppose A31: n <= len W; then n < len W by XXREAL_0:1; then A32: n+1 <= len W by NAT_1:13; 1 <= 1+n by NAT_1:11; then n+1 in dom W by A32,FINSEQ_3:25; then A33: W2.(n+1) = W.(n+1) by A22,GLIB_001:65; A34: n in dom W by A30,A31,FINSEQ_3:25; then W2.n = W.n by A22,GLIB_001:65; hence W2.n = FAP.(W2.(n+1)) by A20,A34,A33; end; suppose A35: n > len W; n <= len W + 2*1 by A22,A29,GLIB_001:64; then n < len W + 1+1 by XXREAL_0:1; then A36: n <= len W + 1 by NAT_1:13; len W + 1 <= n by A35,NAT_1:13; then A37: n = len W + 1 by A36,XXREAL_0:1; then A38: W2.n = e by A22,GLIB_001:65; n+1 = len W + (1+1) by A37; then A39: W2.(n+1) = v by A16,A22,GLIB_001:65; A40: v in dom Gn1 by A8,A15,XBOOLE_0:def 3; Gn1.v = e by A7,A16,Lm3; hence W2.n = FAP.(W2.(n+1)) by A38,A39,A40,Th7; end; end; hence W2.n = FAP.(W2.(n+1)); end; hence ex P being vertex-distinct Path of G st P is_Walk_from source,v & P is_augmenting_wrt EL & P.vertices() c=dom Gn1 & for n being even Nat st n in dom P holds P.n = FAP.(P.(n+1)); end; end; hence ex P being vertex-distinct Path of G st P is_Walk_from source ,v & P is_augmenting_wrt EL & P.vertices() c=dom Gn1 & for n being even Nat st n in dom P holds P.n = FAP.(P.(n+1)); end; hence P[n+1]; end; suppose A41: Next <> {} & (the_Source_of G).e in dom Gn; then A42: Gn1 = Gn+*((the_Target_of G).e .--> e) by A2,Def10; then A43: dom Gn1 = dom Gn \/ {(the_Target_of G).e} by Lm1; A44: e in Next by A41; A45: e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by A41,Def9; then A46: EL.e < (the_Weight_of G).e by A41; now let v be set; assume A47: v in dom Gn1; now per cases by A43,A47,XBOOLE_0:def 3; suppose v in dom Gn; then consider P being vertex-distinct Path of G such that A48: P is_Walk_from source,v and A49: P is_augmenting_wrt EL and A50: P.vertices() c= dom Gn and A51: for n being even Nat st n in dom P holds P.n = FAP.(P .(n+1)) by A1; take P; dom Gn c= dom Gn1 by Th5,NAT_1:11; hence P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices()c= dom Gn1 & for n being even Nat st n in dom P holds P.n = FAP.(P.( n+1)) by A48,A49,A50,A51; end; suppose A52: v in {(the_Target_of G).e}; then A53: v = (the_Target_of G).e by TARSKI:def 1; now consider W being vertex-distinct Path of G such that A54: W is_Walk_from source, (the_Source_of G).e and A55: W is_augmenting_wrt EL and A56: W.vertices() c= dom Gn and A57: for n being even Nat st n in dom W holds W.n = FAP. (W.(n+1)) by A1,A41; set W2 = W.addEdge(e); A58: W.last() = (the_Source_of G).e by A54,GLIB_001:def 23; then A59: e Joins W.last(),(the_Target_of G).e,G by A44; A60: not (the_Target_of G).e in W.vertices() by A41,A45,A56; then reconsider W2 as vertex-distinct Walk of G by A59, GLIB_001:155; take W2; W.first() = source by A54,GLIB_001:def 23; hence W2 is_Walk_from source,v by A53,A59,GLIB_001:63; e DJoins W.last(),(the_Target_of G).e,G by A44,A58; hence W2 is_augmenting_wrt EL by A46,A55,A60,Th3; A61: W2.vertices() = W.vertices() \/ {v} by A53,A59,GLIB_001:95; now let x be object; assume A62: x in W2.vertices(); now per cases by A61,A62,XBOOLE_0:def 3; suppose A63: x in W.vertices(); A64: dom Gn c= dom Gn1 by Th5,NAT_1:11; x in dom Gn by A56,A63; hence x in dom Gn1 by A64; end; suppose x in {v}; hence x in dom Gn1 by A43,A53,XBOOLE_0:def 3; end; end; hence x in dom Gn1; end; hence W2.vertices() c= dom Gn1; let n be even Nat; assume A65: n in dom W2; then A66: n <= len W2 by FINSEQ_3:25; A67: 1 <= n by A65,FINSEQ_3:25; now per cases; suppose A68: n <= len W; then n < len W by XXREAL_0:1; then A69: n+1 <= len W by NAT_1:13; 1 <= 1+n by NAT_1:11; then n+1 in dom W by A69,FINSEQ_3:25; then A70: W2.(n+1) = W.(n+1) by A59,GLIB_001:65; A71: n in dom W by A67,A68,FINSEQ_3:25; then W2.n = W.n by A59,GLIB_001:65; hence W2.n = FAP.(W2.(n+1)) by A57,A71,A70; end; suppose A72: n > len W; n <= len W + 2*1 by A59,A66,GLIB_001:64; then n < len W + 1+1 by XXREAL_0:1; then A73: n <= len W + 1 by NAT_1:13; len W + 1 <= n by A72,NAT_1:13; then A74: n = len W + 1 by A73,XXREAL_0:1; then A75: W2.n = e by A59,GLIB_001:65; n+1 = len W + (1+1) by A74; then A76: W2.(n+1) = v by A53,A59,GLIB_001:65; A77: v in dom Gn1 by A43,A52,XBOOLE_0:def 3; Gn1.v = e by A42,A53,Lm3; hence W2.n = FAP.(W2.(n+1)) by A75,A76,A77,Th7; end; end; hence W2.n = FAP.(W2.(n+1)); end; hence ex P being vertex-distinct Path of G st P is_Walk_from source,v & P is_augmenting_wrt EL & P.vertices() c=dom Gn1 & for n being even Nat st n in dom P holds P.n = FAP.(P.(n+1)); end; end; hence ex P being vertex-distinct Path of G st P is_Walk_from source ,v & P is_augmenting_wrt EL & P.vertices() c=dom Gn1 & for n being even Nat st n in dom P holds P.n = FAP.(P.(n+1)); end; hence P[n+1]; end; end; hence P[n+1]; end; then A78: for n being Nat st P[n] holds P[n+1]; now set P = G.walkOf(source); let v be set; assume A79: v in dom (CS.0); take P; v in {source} by A79,Th4; then v = source by TARSKI:def 1; hence P is_Walk_from source,v by GLIB_001:13; thus P is_augmenting_wrt EL by Th1; P.vertices() = {source} by GLIB_001:90; hence P.vertices() c= dom (CS.0) by Th4; let n be even Nat; assume A80: n in dom P; then n <= len P by FINSEQ_3:25; then A81: n < len P by XXREAL_0:1; 1 <= n by A80,FINSEQ_3:25; hence P.n = FAP.(P.(n+1)) by A81,GLIB_001:13; end; then A82: P[ 0 ]; A83: for n being Nat holds P[n] from NAT_1:sch 2(A82,A78); hereby assume sink in dom FAP; then consider W being vertex-distinct Path of G such that A84: W is_Walk_from source,sink and A85: W is_augmenting_wrt EL and W.vertices() c= dom FAP and A86: for n being even Nat st n in dom W holds W.n = FAP.((W.(n+1))) by A83; take W; thus W is_Walk_from source,sink & W is_augmenting_wrt EL & for n being even Nat st n in dom W holds W.n = FAP.((W.(n+1))) by A84,A85,A86; end; thus thesis; end; uniqueness proof set FAP = AP:FindAugPath(EL,source), CS = AP:CompSeq(EL,source); let IT1, IT2 be vertex-distinct Path of G; defpred P[Nat] means for v being set, P1,P2 being vertex-distinct Path of G st v in dom (CS.$1) & P1 is_Walk_from source,v & P1 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 is_augmenting_wrt EL & (for n being even Nat st n in dom P1 holds P1.n = FAP.(P1.(n+1))) & (for n being even Nat st n in dom P2 holds P2.n = FAP.(P2.(n+1))) holds P1 = P2; set G0 = CS.0; now let n be Nat; assume A87: P[n]; set Gn = CS.n, Gn1 = CS.(n+1); set Next = AP:NextBestEdges(Gn), e = the Element of Next; A88: Gn1 = AP:Step(Gn) by Def12; now per cases; suppose Next = {}; then Gn1 = Gn by A88,Def10; hence P[n+1] by A87; end; suppose A89: Next <> {} & not (the_Source_of G).e in dom Gn; source in {source} by TARSKI:def 1; then A90: source in dom G0 by Th4; dom G0 c= dom Gn by Th5; then A91: source in dom Gn by A90; e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by A89,Def9; then A92: (the_Target_of G).e in dom Gn by A89; A93: Gn1 = Gn+*((the_Source_of G).e .--> e) by A88,A89,Def10; then A94: dom Gn1 = dom Gn \/ {(the_Source_of G). e} by Lm1; now let v be set,P1,P2 be vertex-distinct Path of G; assume that A95: v in dom Gn1 and A96: P1 is_Walk_from source,v and A97: P1 is_augmenting_wrt EL and A98: P2 is_Walk_from source,v and A99: P2 is_augmenting_wrt EL and A100: for n being even Nat st n in dom P1 holds P1.n = FAP.(P1 .(n+1)) and A101: for n being even Nat st n in dom P2 holds P2.n = FAP.(P2 .(n+1)); A102: P1.(len P1) = v by A96,GLIB_001:17; A103: P2.1 = source by A98,GLIB_001:17; A104: P2.(len P2) = v by A98,GLIB_001:17; A105: P1.1 = source by A96,GLIB_001:17; now per cases by A94,A95,XBOOLE_0:def 3; suppose v in dom Gn; hence P1 = P2 by A87,A96,A97,A98,A99,A100,A101; end; suppose A106: v in {(the_Source_of G).e}; then A107: v = (the_Source_of G).e by TARSKI:def 1; then Gn1.v = e by A93,Lm3; then A108: FAP.v = e by A95,Th7; A109: v <> source by A89,A91,A106,TARSKI:def 1; then P1.1 <> P1.last() by A105,A102,GLIB_001:def 7; then P1.first() <> P1.last() by GLIB_001:def 6; then P1 is non trivial by GLIB_001:127; then A110: 3 <= len P1 by GLIB_001:125; P2.1 <> P2.last() by A103,A104,A109,GLIB_001:def 7; then P2.first() <> P2.last() by GLIB_001:def 6; then P2 is non trivial by GLIB_001:127; then A111: 3 <= len P2 by GLIB_001:125; then A112: 3-2 < len P2-0 by XREAL_1:15; 3-2 < len P1-0 by A110,XREAL_1:15; then reconsider lenP11 = len P1 - 1, lenP21 = len P2 - 1 as even Element of NAT by A112,INT_1:5; A113: lenP11 < len P1-0 by XREAL_1:15; 3-2 <= lenP11 by A110,XREAL_1:15; then A114: lenP11 in dom P1 by A113,FINSEQ_3:25; lenP11+1 = len P1; then A115: P1.lenP11 = e by A100,A102,A114,A108; then consider lenP12 being odd Element of NAT such that A116: lenP12 = lenP11 - 1 and lenP11-1 in dom P1 and lenP11+1 in dom P1 and A117: e Joins P1.lenP12,v,G by A102,A114,GLIB_001:9; A118: P1.lenP12 = (the_Target_of G).e by A107,A117; set P1A = P1.cut(2*0+1,lenP12); A119: lenP12 < len P1 by A113,A116,XREAL_1:15; A120: now let n be even Nat; assume A121: n in dom P1A; then A122: 1 <= n by FINSEQ_3:25; A123: n <= len P1A by A121,FINSEQ_3:25; then n < len P1A by XXREAL_0:1; then A124: n+1 <= len P1A by NAT_1:13; 1 <= n+1 by A121,NAT_1:13; then n+1 in dom P1A by A124,FINSEQ_3:25; then A125: P1A.(n+1) = P1.(n+1) by A119,GLIB_001:46; len P1A = lenP12 by A119,GLIB_001:45; then n <= len P1 by A119,A123,XXREAL_0:2; then A126: n in dom P1 by A122,FINSEQ_3:25; P1A.n = P1.n by A119,A121,GLIB_001:46; hence P1A.n = FAP.(P1A.(n+1)) by A100,A125,A126; end; A127: lenP12+(1+1) = len P1 by A116; lenP12 + 1 = lenP11 by A116; then A128: P1.cut(lenP12,len P1) = G.walkOf(( the_Target_of G).e,e, v) by A102,A115,A118,A119,A127,GLIB_001:40; A129: P1A is_augmenting_wrt EL by A97,Th2; A130: 1 <= lenP12 by ABIAN:12; then A131: P1A.append(P1.cut(lenP12,len P1)) = P1.cut(2*0+1, len P1 ) by A119,GLIB_001:38 .= P1 by GLIB_001:39; A132: lenP21 < len P2-0 by XREAL_1:15; 3-2 <= lenP21 by A111,XREAL_1:15; then A133: lenP21 in dom P2 by A132,FINSEQ_3:25; lenP21+1 = len P2; then A134: P2.lenP21 = e by A101,A104,A133,A108; then consider lenP22 being odd Element of NAT such that A135: lenP22 = lenP21 - 1 and lenP21-1 in dom P2 and lenP21+1 in dom P2 and A136: e Joins P2.lenP22,v,G by A104,A133,GLIB_001:9; A137: lenP22+(1+1) = len P2 by A135; set P2A = P2.cut(2*0+1,lenP22); A138: lenP22 < len P2 by A132,A135,XREAL_1:15; A139: now let n be even Nat; assume A140: n in dom P2A; then A141: 1 <= n by FINSEQ_3:25; A142: n <= len P2A by A140,FINSEQ_3:25; then n < len P2A by XXREAL_0:1; then A143: n+1 <= len P2A by NAT_1:13; 1 <= n+1 by A140,NAT_1:13; then n+1 in dom P2A by A143,FINSEQ_3:25; then A144: P2A.(n+1) = P2.(n+1) by A138,GLIB_001:46; len P2A = lenP22 by A138,GLIB_001:45; then n <= len P2 by A138,A142,XXREAL_0:2; then A145: n in dom P2 by A141,FINSEQ_3:25; P2A.n = P2.n by A138,A140,GLIB_001:46; hence P2A.n = FAP.(P2A.(n+1)) by A101,A144,A145; end; A146: 1 <= lenP22 by ABIAN:12; then A147: P2A.append(P2.cut(lenP22, len P2)) = P2.cut(2*0+1, len P2) by A138,GLIB_001:38 .= P2 by GLIB_001:39; A148: P2.lenP22 = (the_Target_of G).e by A107,A136; then A149: P2A is_Walk_from source,(the_Target_of G).e by A103,A146,A138,GLIB_001:37; lenP22 + 1 = lenP21 by A135; then A150: P2.cut(lenP22,len P2) = G.walkOf((the_Target_of G).e,e,v ) by A104,A134,A148,A138,A137,GLIB_001:40; A151: P2A is_augmenting_wrt EL by A99,Th2; P1A is_Walk_from source,(the_Target_of G).e by A105,A118,A130 ,A119,GLIB_001:37; hence P1 = P2 by A87,A92,A149,A129,A151,A120,A139,A128,A150 ,A131,A147; end; end; hence P1 = P2; end; hence P[n+1]; end; suppose A152: Next <> {} & (the_Source_of G).e in dom Gn; source in {source} by TARSKI:def 1; then A153: source in dom G0 by Th4; dom G0 c= dom Gn by Th5; then A154: source in dom Gn by A153; e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by A152,Def9; then A155: not (the_Target_of G).e in dom Gn by A152; A156: Gn1 = Gn+*((the_Target_of G).e.--> e) by A88,A152,Def10; then A157: dom Gn1 = dom Gn \/ {(the_Target_of G). e} by Lm1; now let v be set,P1,P2 be vertex-distinct Path of G; assume that A158: v in dom Gn1 and A159: P1 is_Walk_from source,v and A160: P1 is_augmenting_wrt EL and A161: P2 is_Walk_from source,v and A162: P2 is_augmenting_wrt EL and A163: for n being even Nat st n in dom P1 holds P1.n = FAP.(P1 .(n+1)) and A164: for n being even Nat st n in dom P2 holds P2.n = FAP.(P2 .(n+1)); A165: P1.(len P1) = v by A159,GLIB_001:17; A166: P2.1 = source by A161,GLIB_001:17; A167: P2.(len P2) = v by A161,GLIB_001:17; A168: P1.1 = source by A159,GLIB_001:17; now per cases by A157,A158,XBOOLE_0:def 3; suppose v in dom Gn; hence P1 = P2 by A87,A159,A160,A161,A162,A163,A164; end; suppose A169: v in {(the_Target_of G).e}; then A170: v = (the_Target_of G).e by TARSKI:def 1; then Gn1.v = e by A156,Lm3; then A171: FAP.v = e by A158,Th7; A172: v <> source by A155,A154,A169,TARSKI:def 1; then P1.1 <> P1.last() by A168,A165,GLIB_001:def 7; then P1.first() <> P1.last() by GLIB_001:def 6; then P1 is non trivial by GLIB_001:127; then A173: 3 <= len P1 by GLIB_001:125; P2.1 <> P2.last() by A166,A167,A172,GLIB_001:def 7; then P2.first() <> P2.last() by GLIB_001:def 6; then P2 is non trivial by GLIB_001:127; then A174: 3 <= len P2 by GLIB_001:125; then A175: 3-2 < len P2-0 by XREAL_1:15; 3-2 < len P1-0 by A173,XREAL_1:15; then reconsider lenP11 = len P1 - 1, lenP21 = len P2 - 1 as even Element of NAT by A175,INT_1:5; A176: lenP11 < len P1-0 by XREAL_1:15; 3-2 <= lenP11 by A173,XREAL_1:15; then A177: lenP11 in dom P1 by A176,FINSEQ_3:25; lenP11+1 = len P1; then A178: P1.lenP11 = e by A163,A165,A177,A171; then consider lenP12 being odd Element of NAT such that A179: lenP12 = lenP11 - 1 and lenP11-1 in dom P1 and lenP11+1 in dom P1 and A180: e Joins P1.lenP12,v,G by A165,A177,GLIB_001:9; A181: P1.lenP12 = (the_Source_of G).e by A170,A180; set P1A = P1.cut(2*0+1,lenP12); A182: lenP12 < len P1 by A176,A179,XREAL_1:15; A183: now let n be even Nat; assume A184: n in dom P1A; then A185: 1 <= n by FINSEQ_3:25; A186: n <= len P1A by A184,FINSEQ_3:25; then n < len P1A by XXREAL_0:1; then A187: n+1 <= len P1A by NAT_1:13; 1 <= n+1 by A184,NAT_1:13; then n+1 in dom P1A by A187,FINSEQ_3:25; then A188: P1A.(n+1) = P1.(n+1) by A182,GLIB_001:46; len P1A = lenP12 by A182,GLIB_001:45; then n <= len P1 by A182,A186,XXREAL_0:2; then A189: n in dom P1 by A185,FINSEQ_3:25; P1A.n = P1.n by A182,A184,GLIB_001:46; hence P1A.n = FAP.(P1A.(n+1)) by A163,A188,A189; end; A190: lenP12+(1+1) = len P1 by A179; lenP12 + 1 = lenP11 by A179; then A191: P1.cut(lenP12,len P1) = G.walkOf(( the_Source_of G).e,e, v) by A165,A178,A181,A182,A190,GLIB_001:40; A192: P1A is_augmenting_wrt EL by A160,Th2; A193: 1 <= lenP12 by ABIAN:12; then A194: P1A.append(P1.cut(lenP12,len P1)) = P1.cut(2*0+1, len P1 ) by A182,GLIB_001:38 .= P1 by GLIB_001:39; A195: lenP21 < len P2-0 by XREAL_1:15; 3-2 <= lenP21 by A174,XREAL_1:15; then A196: lenP21 in dom P2 by A195,FINSEQ_3:25; lenP21+1 = len P2; then A197: P2.lenP21 = e by A164,A167,A196,A171; then consider lenP22 being odd Element of NAT such that A198: lenP22 = lenP21 - 1 and lenP21-1 in dom P2 and lenP21+1 in dom P2 and A199: e Joins P2.lenP22,v,G by A167,A196,GLIB_001:9; A200: lenP22+(1+1) = len P2 by A198; set P2A = P2.cut(2*0+1,lenP22); A201: lenP22 < len P2 by A195,A198,XREAL_1:15; A202: now let n be even Nat; assume A203: n in dom P2A; then A204: 1 <= n by FINSEQ_3:25; A205: n <= len P2A by A203,FINSEQ_3:25; then n < len P2A by XXREAL_0:1; then A206: n+1 <= len P2A by NAT_1:13; 1 <= n+1 by A203,NAT_1:13; then n+1 in dom P2A by A206,FINSEQ_3:25; then A207: P2A.(n+1) = P2.(n+1) by A201,GLIB_001:46; len P2A = lenP22 by A201,GLIB_001:45; then n <= len P2 by A201,A205,XXREAL_0:2; then A208: n in dom P2 by A204,FINSEQ_3:25; P2A.n = P2.n by A201,A203,GLIB_001:46; hence P2A.n = FAP.(P2A.(n+1)) by A164,A207,A208; end; A209: 1 <= lenP22 by ABIAN:12; then A210: P2A.append(P2.cut(lenP22, len P2)) = P2.cut(2*0+1, len P2) by A201,GLIB_001:38 .= P2 by GLIB_001:39; A211: P2.lenP22 = (the_Source_of G).e by A170,A199; then A212: P2A is_Walk_from source,(the_Source_of G).e by A166,A209,A201,GLIB_001:37; lenP22 + 1 = lenP21 by A198; then A213: P2.cut(lenP22,len P2) = G.walkOf((the_Source_of G).e,e,v ) by A167,A197,A211,A201,A200,GLIB_001:40; A214: P2A is_augmenting_wrt EL by A162,Th2; P1A is_Walk_from source,(the_Source_of G).e by A168,A181,A193 ,A182,GLIB_001:37; hence P1 = P2 by A87,A152,A212,A192,A214,A183,A202,A191,A213 ,A194,A210; end; end; hence P1 = P2; end; hence P[n+1]; end; end; hence P[n+1]; end; then A215: for n being Nat st P[n] holds P[n+1]; now let v be set, P1,P2 be vertex-distinct Path of G; assume that A216: v in dom G0 and A217: P1 is_Walk_from source,v and P1 is_augmenting_wrt EL and A218: P2 is_Walk_from source,v and P2 is_augmenting_wrt EL and for n being even Nat st n in dom P1 holds P1.n = FAP.(P1.(n+1)) and for n being even Nat st n in dom P2 holds P2.n = FAP.(P2.(n+1)); v in {source} by A216,Th4; then A219: v = source by TARSKI:def 1; then A220: P1.(2*0+1) = v by A217,GLIB_001:17; A221: P2.(2*0+1) = v by A218,A219,GLIB_001:17; A222: 1 <= len P1 by ABIAN:12; P1.(len P1) = v by A217,GLIB_001:17; then len P1 = 1 by A220,A222,GLIB_001:def 29; then A223: P1 = <*v*> by A220,FINSEQ_1:40; A224: 1 <= len P2 by ABIAN:12; P2.(len P2 ) = v by A218,GLIB_001:17; then len P2 = 1 by A221,A224,GLIB_001:def 29; hence P1 = P2 by A221,A223,FINSEQ_1:40; end; then A225: P[ 0 ]; for n being Nat holds P[n] from NAT_1:sch 2(A225,A215); hence sink in dom FAP & (IT1 is_Walk_from source,sink & IT1 is_augmenting_wrt EL & for n being even Nat st n in dom IT1 holds IT1.n = ( AP:FindAugPath(EL,source)).(IT1.(n+1))) & (IT2 is_Walk_from source,sink & IT2 is_augmenting_wrt EL & for n being even Nat st n in dom IT2 holds IT2.n = ( AP:FindAugPath(EL,source)).(IT2.(n+1))) implies IT1 = IT2; thus thesis; end; consistency; end; theorem Th8: 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) proof let G be real-weighted WGraph, EL being FF:ELabeling of G, source be Vertex of G; set CS = AP:CompSeq(EL,source), G0 = CS.0; defpred P[Nat] means for v being set st v in dom (CS.$1) holds ex P being Path of G st P is_augmenting_wrt EL & P is_Walk_from source,v & P.vertices() c= dom (CS.$1); A1: now let n be Nat; set Gn = CS.n, Gn1 = CS.(n+1); set Next = AP:NextBestEdges(Gn), e = the Element of Next; assume A2: P[n]; A3: Gn1 = AP:Step(Gn) by Def12; now per cases; suppose Next = {}; then Gn1 = Gn by A3,Def10; hence P[n+1] by A2; end; suppose A4: Next <> {}; set se = (the_Source_of G).e, te = (the_Target_of G).e; now per cases by A4,Def9; suppose A5: e is_forward_edge_wrt Gn; then A6: EL.e < (the_Weight_of G).e; let v be set; assume A7: v in dom Gn1; A8: e in the_Edges_of G by A5; then A9: e DJoins se,te,G; A10: se in dom Gn by A5; then Gn1 = Gn+*(te .--> e) by A3,A4,Def10; then A11: dom Gn1 = dom Gn \/ {te} by Lm1; te in {te} by TARSKI:def 1; then A12: te in dom Gn1 by A11,XBOOLE_0:def 3; A13: dom Gn c= dom Gn1 by A11,XBOOLE_1:7; then A14: se in dom Gn1 by A10; now per cases by A11,A7,XBOOLE_0:def 3; suppose v in dom Gn; then consider P being Path of G such that A15: P is_augmenting_wrt EL and A16: P is_Walk_from source,v and A17: P.vertices() c= dom Gn by A2; take P; thus P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom Gn1 by A13,A15,A16,A17; end; suppose v in {te}; then A18: v = te by TARSKI:def 1; now per cases; suppose A19: se = source; set P = G.walkOf(se,e,te); take P; A20: e Joins se,te,G by A8; now let n be odd Nat; assume n < len P; then n < 2+1 by A20,GLIB_001:14; then n <= 2*1 by NAT_1:13; then n < 1+1 by XXREAL_0:1; then A21: n <= 1 by NAT_1:13; 1 <= n by ABIAN:12; then A22: n = 1 by A21,XXREAL_0:1; A23: P = <*se,e,te*> by A20,GLIB_001:def 5; then A24: P.n = se by A22,FINSEQ_1:45; A25: P.(n+ 2) = te by A22,A23,FINSEQ_1:45; A26: P.(n+1) = e by A22,A23,FINSEQ_1:45; hence P.(n+1) DJoins P.n,P.(n+2),G implies EL.(P.(n+1)) < (the_Weight_of G).(P.(n+1)) by A5; assume not P.(n+1) DJoins P.n,P.(n+2),G; hence 0 < EL.(P.(n+1)) by A8,A24,A26,A25; end; hence P is_augmenting_wrt EL; thus P is_Walk_from source,v by A18,A19,A20,GLIB_001:15; now let x be object; assume x in P.vertices(); then x in {se,te} by A20,GLIB_001:91; hence x in dom Gn1 by A12,A14,TARSKI:def 2; end; hence P.vertices() c= dom Gn1; end; suppose A27: se <> source; A28: e Joins se,v,G by A8,A18; consider P being Path of G such that A29: P is_augmenting_wrt EL and A30: P is_Walk_from source,se and A31: P.vertices() c= dom Gn by A2,A10; set P2 = P.addEdge(e); A32: not v in P.vertices() by A5,A18,A31; A33: se = P.last() by A30,GLIB_001:def 23; then P.first() <> P.last() by A27,A30,GLIB_001:def 23; then P is open by GLIB_001:def 24; then reconsider P2 as Path of G by A28,A33,A32,GLIB_001:151 ; take P2; thus P2 is_augmenting_wrt EL by A6,A9,A18,A29,A33,A32,Th3; thus P2 is_Walk_from source,v by A30,A28,GLIB_001:66; now let x be object; assume x in P2.vertices(); then A34: x in P.vertices()\/{te} by A28,A33,GLIB_001:95; now per cases by A34,XBOOLE_0:def 3; suppose x in P.vertices(); then x in dom Gn by A31; hence x in dom Gn1 by A13; end; suppose x in {te}; hence x in dom Gn1 by A11,XBOOLE_0:def 3; end; end; hence x in dom Gn1; end; hence P2.vertices() c= dom Gn1; end; end; hence ex P being Path of G st P is_augmenting_wrt EL & P is_Walk_from source,v & P.vertices() c= dom Gn1; end; end; hence ex P being Path of G st P is_augmenting_wrt EL & P is_Walk_from source,v & P.vertices() c= dom Gn1; end; suppose A35: e is_backward_edge_wrt Gn; then A36: 0 < EL.e; let v be set; assume A37: v in dom Gn1; A38: e in the_Edges_of G by A35; then A39: e DJoins se,te,G; A40: not se in dom Gn by A35; then Gn1 = Gn+*(se .--> e) by A3,A4,Def10; then A41: dom Gn1 = dom Gn \/ {se} by Lm1; se in {se} by TARSKI:def 1; then A42: se in dom Gn1 by A41,XBOOLE_0:def 3; A43: te in dom Gn by A35; A44: dom Gn c= dom Gn1 by A41,XBOOLE_1:7; then A45: te in dom Gn1 by A43; now per cases by A41,A37,XBOOLE_0:def 3; suppose v in dom Gn; then consider P being Path of G such that A46: P is_augmenting_wrt EL and A47: P is_Walk_from source,v and A48: P.vertices() c= dom Gn by A2; take P; thus P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom Gn1 by A44,A46,A47,A48; end; suppose v in {se}; then A49: v = se by TARSKI:def 1; now per cases; suppose A50: te = source; set P = G.walkOf(te,e,se); take P; A51: e Joins te,se,G by A38; now let n be odd Nat; assume n < len P; then n < 2+1 by A51,GLIB_001:14; then n <= 2*1 by NAT_1:13; then n < 1+1 by XXREAL_0:1; then A52: n <= 1 by NAT_1:13; 1 <= n by ABIAN:12; then A53: n = 1 by A52,XXREAL_0:1; A54: P = <*te,e,se*> by A51,GLIB_001:def 5; then A55: P.(n+1) = e by A53,FINSEQ_1:45; P.n = te by A53,A54,FINSEQ_1:45; hence P.(n+1) DJoins P.n,P.(n+2),G implies EL.(P.(n+1)) < (the_Weight_of G).(P.(n+1)) by A43,A40,A55; assume not P.(n+1) DJoins P.n,P.(n+2),G; thus 0 < EL.(P.(n+1)) by A35,A55; end; hence P is_augmenting_wrt EL; thus P is_Walk_from source,v by A49,A50,A51,GLIB_001:15; now let x be object; assume x in P.vertices(); then x in {se,te} by A51,GLIB_001:91; hence x in dom Gn1 by A42,A45,TARSKI:def 2; end; hence P.vertices() c= dom Gn1; end; suppose A56: te <> source; A57: e Joins te,v,G by A38,A49; consider P being Path of G such that A58: P is_augmenting_wrt EL and A59: P is_Walk_from source,te and A60: P.vertices() c= dom Gn by A2,A43; set P2 = P.addEdge(e); A61: not v in P.vertices() by A35,A49,A60; A62: te = P.last() by A59,GLIB_001:def 23; then P.first() <> P.last() by A56,A59,GLIB_001:def 23; then P is open by GLIB_001:def 24; then reconsider P2 as Path of G by A57,A62,A61,GLIB_001:151 ; take P2; thus P2 is_augmenting_wrt EL by A36,A39,A49,A58,A62,A61,Th3 ; thus P2 is_Walk_from source,v by A59,A57,GLIB_001:66; now let x be object; assume x in P2.vertices(); then A63: x in P.vertices()\/{se} by A57,A62,GLIB_001:95; now per cases by A63,XBOOLE_0:def 3; suppose x in P.vertices(); then x in dom Gn by A60; hence x in dom Gn1 by A44; end; suppose x in {se}; hence x in dom Gn1 by A41,XBOOLE_0:def 3; end; end; hence x in dom Gn1; end; hence P2.vertices() c= dom Gn1; end; end; hence ex P being Path of G st P is_augmenting_wrt EL & P is_Walk_from source,v & P.vertices() c= dom Gn1; end; end; hence ex P being Path of G st P is_augmenting_wrt EL & P is_Walk_from source,v & P.vertices() c= dom Gn1; end; end; hence P[n+1]; end; end; hence P[n+1]; end; now let v be set; assume A64: v in dom G0; then reconsider v9=v as Vertex of G; set P = G.walkOf(v9); take P; thus P is_augmenting_wrt EL by Th1; v in {source} by A64,Th4; then v = source by TARSKI:def 1; hence P is_Walk_from source,v by GLIB_001:13; P.vertices() = {v9} by GLIB_001:90; hence P.vertices() c= dom G0 by A64,ZFMISC_1:31; end; then A65: P[ 0 ]; for n being Nat holds P[n] from NAT_1:sch 2(A65,A1); hence thesis; end; theorem Th9: 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 proof let G be finite real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G, v be set; set CS = AP:CompSeq(EL,source), V = dom AP:FindAugPath(EL,source); hereby assume v in V; then ex P being Path of G st P is_augmenting_wrt EL & P is_Walk_from source,v & P.vertices() c= V by Th8; hence ex P being Path of G st P is_Walk_from source,v & P is_augmenting_wrt EL; end; given P being Path of G such that A1: P is_Walk_from source,v and A2: P is_augmenting_wrt EL; now P.(2*0+1) = source by A1,GLIB_001:17; then P.(2*0+1) in {source} by TARSKI:def 1; then A3: P.(2*0+1) in dom (CS.0) by Th4; set Gn = CS.(CS.Lifespan()), Gn1 = CS.(CS.Lifespan()+1); defpred P[Nat] means $1 is odd & $1 <= len P & not P.$1 in V; assume A4: not v in V; P.(len P) = v by A1,GLIB_001:17; then A5: ex n being Nat st P[n] by A4; consider n being Nat such that A6: P[n] & for k being Nat st P[k] holds n <= k from NAT_1:sch 5(A5); reconsider n9=n as odd Element of NAT by A6,ORDINAL1:def 12; A7: 1 <= n by A6,ABIAN:12; dom (CS.0) c= V by Th5; then n <> 1 by A6,A3; then 1 < n by A7,XXREAL_0:1; then 1+1 <= n by NAT_1:13; then reconsider n2 = n9-2*1 as odd Element of NAT by INT_1:5; A8: n2 < n - 0 by XREAL_1:15; then A9: n2 < len P by A6,XXREAL_0:2; then A10: P.n2 in V by A6,A8; set Next = AP:NextBestEdges(Gn), en = the Element of Next; AP:CompSeq(EL,source) is halting by Th6; then A11: Gn = CS.(CS.Lifespan()+1) by GLIB_000:def 55; set e = P.(n2+1); A12: P.(n2+2) = P.n; then A13: e Joins P.n2, P.n, G by A9,GLIB_001:def 3; A14: now per cases; suppose A15: e DJoins P.n2, P.n, G; then A16: (the_Source_of G).e in dom Gn by A10; A17: e in the_Edges_of G by A15; A18: not (the_Target_of G).e in dom Gn by A6,A15; (EL).e<(the_Weight_of G).e by A2,A9,A12,A15; then e is_forward_edge_wrt Gn by A17,A16,A18; hence Next <> {} by Def9; end; suppose A19: not e DJoins P.n2,P.n, G; then A20: e DJoins P.n,P.n2,G by A13; then A21: e in the_Edges_of G; A22: (the_Target_of G).e in dom Gn by A10,A20; A23: not (the_Source_of G).e in dom Gn by A6,A20; 0 < (EL).e by A2,A9,A12,A19; then e is_backward_edge_wrt Gn by A21,A23,A22; hence Next <> {} by Def9; end; end; A24: Gn1 = AP:Step(Gn) by Def12; now per cases; suppose A25: not (the_Source_of G).en in dom Gn; then Gn = Gn+*((the_Source_of G).en .--> en) by A24,A11,A14,Def10; then A26: dom Gn = dom Gn \/ {(the_Source_of G).en} by Lm1; (the_Source_of G).en in {(the_Source_of G).en} by TARSKI:def 1; hence contradiction by A25,A26,XBOOLE_0:def 3; end; suppose A27: (the_Source_of G).en in dom Gn; en is_forward_edge_wrt Gn or en is_backward_edge_wrt Gn by A14,Def9; then A28: not (the_Target_of G).en in dom Gn by A27; Gn = Gn+*((the_Target_of G).en .--> en) by A24,A11,A14,A27,Def10; then A29: dom Gn = dom Gn \/ {(the_Target_of G).en} by Lm1; (the_Target_of G).en in {(the_Target_of G).en} by TARSKI:def 1; hence contradiction by A28,A29,XBOOLE_0:def 3; end; end; hence contradiction; end; hence thesis; end; theorem Th10: 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) proof let G be finite real-weighted WGraph, EL being FF:ELabeling of G, source be Vertex of G; set CS = AP:CompSeq(EL,source); dom (CS.0) = {source} by Th4; then A1: source in dom (CS.0) by TARSKI:def 1; dom (CS.0) c= dom AP:FindAugPath(EL,source) by Th5; hence thesis by A1; end; begin :: Ford-Fulkerson Algorithm definitions definition let G be natural-weighted WGraph, EL be FF:ELabeling of G, W be Walk of G; assume A1: W is_augmenting_wrt EL; defpred P[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: 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 proof now let k be Nat; assume k in Seg len W.edgeSeq(); now per cases; suppose W.(2*k) DJoins W.(2*k-1),W.(2*k+1),G; hence ex x being set st P[k,x]; end; suppose not W.(2*k) DJoins W.(2*k-1),W.(2*k+1),G; hence ex x being set st P[k,x]; end; end; hence ex x being object st P[k,x]; end; then A2: for k being Nat st k in Seg len W.edgeSeq() ex x being object st P[k, x]; consider IT being FinSequence such that A3: dom IT = Seg len W.edgeSeq() and A4: for k being Nat st k in Seg len W.edgeSeq() holds P[k,IT.k] from FINSEQ_1:sch 1(A2); now let y be object; assume y in rng IT; then consider x being object such that A5: x in dom IT and A6: IT.x = y by FUNCT_1:def 3; reconsider n = x as Element of NAT by A5; per cases; suppose A7: W.(2*n) DJoins W.(2*n-1),W.(2*n+1),G; n in dom W.edgeSeq() by A3,A5,FINSEQ_1:def 3; then A8: 2*n in dom W by GLIB_001:78; then 1 <= 2*n by FINSEQ_3:25; then reconsider 2n1 = 2*n-1 as odd Element of NAT by INT_1:5; 2*n <= len W by A8,FINSEQ_3:25; then A9: 2n1 < len W - 0 by XREAL_1:15; A10: 2n1+(1+1) = 2*n+1; A11: IT.n = (the_Weight_of G).(W.(2*n))-EL.(W.(2*n)) by A3,A4,A5,A7; 2n1+1 = 2*n; then EL.(W.(2*n)) < (the_Weight_of G).(W.(2*n)) by A1,A7,A9,A10; hence y in NAT by A6,A11,INT_1:5; end; suppose not W.(2*n) DJoins W.(2*n-1),W.(2*n+1),G; then IT.n = EL.(W.(2*n)) by A3,A4,A5; hence y in NAT by A6,ORDINAL1:def 12; end; end; then rng IT c= NAT; then reconsider IT as FinSequence of NAT by FINSEQ_1:def 4; take IT; thus dom IT = dom W.edgeSeq() by A3,FINSEQ_1:def 3; let n be Nat; assume n in dom IT; hence thesis by A3,A4; end; uniqueness proof let IT1,IT2 be FinSequence of NAT such that A12: dom IT1 = dom W.edgeSeq() and A13: for n being Nat st n in dom IT1 holds P[n,IT1.n] and A14: dom IT2 = dom W.edgeSeq() and A15: for n being Nat st n in dom IT2 holds P[n,IT2.n]; now let n be Nat; assume A16: n in dom IT1; now per cases; suppose A17: W.(2*n) DJoins W.(2*n-1),W.(2*n+1),G; then IT1.n = (the_Weight_of G).(W.(2*n))-EL.(W.(2* n)) by A13,A16; hence IT1.n = IT2.n by A12,A14,A15,A16,A17; end; suppose A18: not W.(2*n) DJoins W.(2*n-1),W.(2*n+1),G; then IT1.n = EL.(W.(2*n)) by A13,A16; hence IT1.n = IT2.n by A12,A14,A15,A16,A18; end; end; hence IT1.n = IT2.n; end; hence IT1 = IT2 by A12,A14,FINSEQ_1:13; end; end; definition let G be natural-weighted WGraph, EL being FF:ELabeling of G, W be Walk of G; assume A1: W is_augmenting_wrt EL; func W.tolerance(EL) -> Nat means :Def16: 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; existence proof set D = rng (W.flowSeq(EL)); now assume W is non trivial; then W.edges() <> {} by GLIB_001:136; then rng W.edgeSeq() <> {} by GLIB_001:def 17; then consider y being object such that A2: y in rng W.edgeSeq() by XBOOLE_0:def 1; consider x being object such that A3: x in dom W.edgeSeq() and y = W.edgeSeq().x by A2,FUNCT_1:def 3; x in dom (W.flowSeq(EL)) by A1,A3,Def15; then (W.flowSeq(EL)).x in D by FUNCT_1:def 3; then reconsider D as non empty finite Subset of NAT; deffunc F(Nat) = $1; consider IT being Element of D such that A4: for k being Element of D holds F(IT) <= F(k) from PRE_CIRC:sch 5; reconsider IT as Nat; take IT; thus IT in rng (W.flowSeq(EL)); let k be Real; assume k in rng (W.flowSeq(EL)); hence IT <= k by A4; end; hence thesis; end; uniqueness proof let IT1,IT2 be Nat; hereby assume W is non trivial; assume that A5: IT1 in rng (W.flowSeq(EL)) and A6: for k being Real st k in rng (W.flowSeq(EL)) holds IT1 <= k; assume that A7: IT2 in rng (W.flowSeq(EL)) and A8: for k being Real st k in rng (W.flowSeq(EL)) holds IT2 <= k; A9: IT2 <= IT1 by A5,A8; IT1 <= IT2 by A6,A7; hence IT1 = IT2 by A9,XXREAL_0:1; end; thus thesis; end; consistency; end; definition let G be natural-weighted WGraph, EL being FF:ELabeling of G, P be Path of G; assume A1: P is_augmenting_wrt EL; func FF:PushFlow(EL,P) -> FF:ELabeling of G means :Def17: (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 proof defpred P[object,object] means ($1 in the_Edges_of G & not $1 in P.edges() implies $2 = EL.$1) & (for n being odd Element of NAT st n < len P & $1 = P.(n+ 1) holds ((P.(n+1) DJoins P.n,P.(n+2),G) implies $2 = EL.(P.(n+1)) + P .tolerance(EL)) & (not P.(n+1) DJoins P.n,P.(n+2),G implies $2 = EL.(P.(n+1)) - P.tolerance(EL))); now let x be object; assume x in the_Edges_of G; now per cases; suppose A2: not x in P.edges(); set y = EL.x; for n being odd Element of NAT st n < len P & x = P.(n+1) holds ( P.(n+1) DJoins P.n,P.(n+2),G implies y = EL.(P.(n+1)) + P.tolerance(EL)) & ( not P.(n+1) DJoins P.n,P.(n+2),G implies y = EL.(P.(n+1)) - P.tolerance(EL)) by A2,GLIB_001:100; hence ex y being set st P[x,y]; end; suppose A3: x in P.edges(); then consider n being odd Element of NAT such that A4: n < len P and A5: P.(n+1) = x by GLIB_001:100; A6: 1 <= n+1 by NAT_1:11; A7: n+1 <= len P by A4,NAT_1:13; now per cases; suppose A8: P.(n+1) DJoins P.n,P.(n+2),G; set y = EL.(P.(n+1)) + P.tolerance(EL); now thus x in the_Edges_of G & not x in P.edges() implies y = EL.x by A3; let m be odd Element of NAT such that A9: m < len P and A10: P.(m+1) = x; 1 <= m+1 by NAT_1:11; then A11: n+1 <= m+1 by A5,A7,A10,GLIB_001:138; thus P.(m+1) DJoins P.m,P.(m+2),G implies y = y; assume A12: not P.(m+1) DJoins P.m,P.(m+2),G; m+1 <= len P by A9,NAT_1:13; then m+1 <= n+1 by A5,A6,A10,GLIB_001:138; then m+1 = n+1 by A11,XXREAL_0:1; hence y = EL.(P.(m+1)) - P.tolerance(EL) by A8,A12; end; then P[x,y] by A5; hence ex y being set st P[x,y]; end; suppose A13: not P.(n+1) DJoins P.n,P.(n+2),G; set y =EL.(P.(n+1)) - P.tolerance(EL); now thus x in the_Edges_of G & not x in P.edges() implies y = EL.x by A3; let m be odd Element of NAT such that A14: m < len P and A15: P.(m+1) = x; 1 <= m+1 by NAT_1:11; then A16: n+1 <= m+1 by A5,A7,A15,GLIB_001:138; m+1 <= len P by A14,NAT_1:13; then m+1 <= n+1 by A5,A6,A15,GLIB_001:138; then m+1 = n+1 by A16,XXREAL_0:1; hence P.(m+1) DJoins P.m,P.(m+2),G implies y = EL.(P.(n+1)) + P .tolerance(EL) by A13; assume not P.(m+1) DJoins P.m,P.(m+2),G; thus y = EL.(P.(n+1)) - P.tolerance(EL); end; then P[x,y] by A5; hence ex y being set st P[x,y]; end; end; hence ex y being set st P[x,y]; end; end; hence ex y being object st P[x,y]; end; then A17: for x being object st x in the_Edges_of G ex y being object st P[ x,y ]; consider IT being Function such that A18: dom IT = the_Edges_of G and A19: for e being object st e in the_Edges_of G holds P[e,IT.e] from CLASSES1:sch 1(A17); rng IT c= NAT proof let y be object; assume y in rng IT; then consider e being object such that A20: e in dom IT and A21: IT.e = y by FUNCT_1:def 3; now per cases; suppose not e in P.edges(); then y = EL.e by A18,A19,A20,A21; hence thesis by ORDINAL1:def 12; end; suppose A22: e in P.edges(); then consider n being odd Element of NAT such that A23: n < len P and A24: P.(n+1) = e by GLIB_001:100; A25: P is non trivial by A22,GLIB_001:136; now per cases; suppose P.(n+1) DJoins P.n, P.(n+2), G; then y = EL.(P.(n+1))+P.tolerance(EL) by A19,A21,A23,A24; hence thesis by ORDINAL1:def 12; end; suppose A26: not P.(n+1) DJoins P.n,P.(n+2),G; set n1div2 = (n+1) div 2; A27: 1 <= n+1 by NAT_1:11; n+1 <= len P by A23,NAT_1:13; then n1div2 in dom P.edgeSeq() by A27,GLIB_001:77; then A28: n1div2 in dom (P.flowSeq(EL)) by A1,Def15; 2 divides n+1 by PEPIN:22; then A29: 2*n1div2 = n+1 by NAT_D:3; then A30: 2*n1div2+1 = n+(1+1); 2*n1div2-1 = n by A29; then (P.flowSeq(EL)).n1div2 = EL.e by A1,A24,A26,A28,A30,Def15; then EL.e in rng (P.flowSeq(EL)) by A28,FUNCT_1:def 3; then A31: P.tolerance(EL) <= EL.e by A1,A25,Def16; y = EL.e-P.tolerance(EL) by A18,A19,A20,A21,A23,A24,A26; hence thesis by A31,INT_1:5; end; end; hence thesis; end; end; hence thesis; end; then reconsider IT as natural-valued ManySortedSet of the_Edges_of G by A18,PARTFUN1:def 2 ,RELAT_1:def 18,VALUED_0:def 6; take IT; thus for e being set st e in the_Edges_of G & not e in P.edges() holds IT. e = EL.e by A19; let n be odd Nat; reconsider n9 = n as odd Element of NAT by ORDINAL1:def 12; A32: n9 = n; assume A33: n < len P; then P.(n+1) Joins P.n, P.(n9+2), G by GLIB_001:def 3; then A34: P.(n+1) in the_Edges_of G; thus P.(n+1) DJoins P.n,P.(n+2),G implies IT.(P.(n+1)) = EL.(P.(n+1)) + P .tolerance(EL) by A19,A32,A33; assume not P.(n+1) DJoins P.n, P.(n+2), G; hence thesis by A19,A32,A33,A34; end; uniqueness proof let IT1,IT2 be FF:ELabeling of G such that A35: for e being set st e in the_Edges_of G & not e in P.edges() holds IT1. e = EL.e and A36: for n being odd Nat st n < len P holds (P.(n+1) DJoins P.n, P.(n+ 2 ),G implies IT1.(P.(n+1)) = EL.(P.(n+1)) + P.tolerance(EL)) & (not P.(n+1) DJoins P.n,P.(n+2),G implies IT1.(P.(n+1)) = EL.(P.(n+1)) - P.tolerance(EL)) and A37: for e being set st e in the_Edges_of G & not e in P.edges() holds IT2.e = EL.e and A38: for n being odd Nat st n < len P holds (P.(n+1) DJoins P.n, P.(n+ 2 ),G implies IT2.(P.(n+1)) = EL.(P.(n+1)) + P.tolerance(EL)) & (not P.(n+1) DJoins P.n,P.(n+2),G implies IT2.(P.(n+1)) = EL.(P.(n+1)) - P.tolerance(EL)); now let e be object; assume A39: e in the_Edges_of G; now per cases; suppose A40: not e in P.edges(); then IT1.e = EL.e by A35,A39; hence IT1.e = IT2.e by A37,A39,A40; end; suppose e in P.edges(); then consider n being odd Element of NAT such that A41: n < len P and A42: P.(n+1) = e by GLIB_001:100; now per cases; suppose A43: P.(n+1) DJoins P.n,P.(n+2),G; then IT1.e = EL.(P.(n+1)) + P.tolerance(EL) by A36,A41,A42; hence IT1.e = IT2.e by A38,A41,A42,A43; end; suppose A44: not P.(n+1) DJoins P.n,P.(n+2),G; then IT1.e = EL.(P.(n+1)) - P.tolerance(EL) by A36,A41,A42; hence IT1.e = IT2.e by A38,A41,A42,A44; end; end; hence IT1.e = IT2.e; end; end; hence IT1.e = IT2.e; end; hence thesis by PBOOLE:3; end; 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 :Def18: FF:PushFlow(EL, AP:GetAugPath(EL,source,sink)) if sink in dom AP:FindAugPath(EL ,source) otherwise EL; correctness; end; definition let G be _Graph; mode FF:ELabelingSeq of G -> ManySortedSet of NAT means :Def19: for n being Nat holds it.n is FF:ELabeling of G; existence proof take NAT --> (the_Edges_of G --> 0); let n be Nat; n in NAT by ORDINAL1:def 12; hence thesis by FUNCOP_1:7; end; end; registration let G be _Graph, ES be FF:ELabelingSeq of G, n be Nat; cluster ES.n -> Function-like Relation-like; coherence by Def19; end; registration let G be _Graph, ES be FF:ELabelingSeq of G, n be Nat; cluster ES.n -> the_Edges_of G -defined; coherence by Def19; end; registration let G be _Graph, ES be FF:ELabelingSeq of G, n be Nat; cluster ES.n -> natural-valued total; coherence by Def19; 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 :Def20: it.0 = the_Edges_of G --> 0 & for n being Nat holds it.(n+1) = FF:Step(it.n,source, sink); existence proof defpred P[set,set,set] means (ex e being FF:ELabeling of G st e = $2 & $3 = FF:Step(e,source,sink)) or (not ex e being FF:ELabeling of G st e = $2) & $3 = $2; now let n,x be set; now per cases; suppose ex e being FF:ELabeling of G st e = x; then consider e being FF:ELabeling of G such that A1: e = x; set y = FF:Step(e,source,sink); P[n,x,y] by A1; hence ex y being set st P[n,x,y]; end; suppose not ex e being FF:ELabeling of G st e = x; hence ex y being set st P[n,x,y]; end; end; hence ex y being set st P[n,x,y]; end; then A2: for n being Nat for x being set ex y being set st P[n,x,y]; consider IT being Function such that A3: dom IT = NAT & IT.0 = the_Edges_of G --> 0 & for n being Nat holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A2); reconsider IT as ManySortedSet of NAT by A3,PARTFUN1:def 2,RELAT_1:def 18; defpred P2[Nat] means ex Gn being FF:ELabeling of G st IT.$1 = Gn; A4: now let n be Nat; assume P2[n]; then consider Gn being FF:ELabeling of G such that A5: IT.n = Gn; P[n,Gn,IT.(n+1)] by A3,A5; hence P2[n+1]; end; A6: P2[ 0 ] by A3; A7: for n being Nat holds P2[n] from NAT_1:sch 2(A6,A4); now let n be Nat; ex Gn being FF:ELabeling of G st IT.n = Gn by A7; hence IT.n is FF:ELabeling of G; end; then reconsider IT as FF:ELabelingSeq of G by Def19; take IT; thus IT.0 = the_Edges_of G --> 0 by A3; let n be Nat; reconsider n9 = n as Element of NAT by ORDINAL1:def 12; ex X being FF:ELabeling of G st X = IT.n & IT.(n9+1) = FF:Step(X, source,sink) by A3; hence thesis; end; uniqueness proof let IT1,IT2 be FF:ELabelingSeq of G such that A8: IT1.0 = the_Edges_of G --> 0 and A9: for n being Nat holds IT1.(n+1) = FF:Step(IT1.n,source,sink) and A10: IT2.0 = the_Edges_of G --> 0 and A11: for n being Nat holds IT2.(n+1) = FF:Step(IT2.n,source,sink); defpred P[Nat] means IT1.$1 = IT2.$1; A12: now let n be Nat; assume A13: P[n]; IT2.(n+1) = FF:Step(IT2.n,source,sink) by A11; hence P[n+1] by A9,A13; end; A14: P[ 0 ] by A8,A10; for n being Nat holds P[n] from NAT_1:sch 2(A14,A12); then for n being object st n in NAT holds IT1.n = IT2.n; hence IT1 = IT2 by PBOOLE:3; end; 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 FF:CompSeq(G,source,sink).Result(); coherence; end; begin :: Ford Fulkerson Maximum Flow Theorems theorem Th11: 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)) proof let G be finite real-weighted WGraph, EL being FF:ELabeling of G, source, sink be set, V be Subset of the_Vertices_of G; assume that A1: EL has_valid_flow_from source,sink and A2: source in V and A3: not sink in V; set VG = the_Vertices_of G; set n = card (VG \ V); A4: now assume n = 0; then A5: VG \ V = {}; sink is Vertex of G by A1; hence contradiction by A3,A5,XBOOLE_0:def 5; end; defpred P[Nat] means for V being Subset of VG st card (VG \ V) = $1 & source in V & not sink in V holds EL.flow(source,sink) = Sum (EL | G.edgesDBetween(V, VG \ V)) - Sum (EL | G.edgesDBetween(VG \ V, V)); set TG = the_Target_of G; set SG = the_Source_of G; A6: now let n be non zero Nat; assume A7: P[n]; now let V2 be Subset of VG; assume that A8: card (VG\V2) = n+1 and A9: source in V2 and A10: not sink in V2; set x = the Element of (VG \ V2) \ {sink}; set V1 = V2 \/ {x}; set EV1V1a = G.edgesDBetween(V1, VG \ V1); set EV1V1b = G.edgesDBetween(VG \ V1, V1); set EXV1c = G.edgesDBetween({x},VG\V1); set EV1Xd = G.edgesDBetween(VG\V1,{x}); sink is Vertex of G by A1; then sink in (VG \ V2) by A10,XBOOLE_0:def 5; then {sink} c= (VG \ V2) by ZFMISC_1:31; then A11: card ((VG\V2)\{sink}) = n+1-card {sink} by A8,CARD_2:44 .= n+1-1 by CARD_1:30 .= n; then A12: x in (VG)\V2 by CARD_1:27,XBOOLE_0:def 5; then {x} c= VG by ZFMISC_1:31; then reconsider V1 as Subset of VG by XBOOLE_1:8; A13: VG \ V1 = (VG \ V2) \ {x} by XBOOLE_1:41; {x} c= VG \ V2 by A12,ZFMISC_1:31; then A14: card (VG \ V1) = card (VG \ V2) - card {x} by A13,CARD_2:44 .= n + 1 - 1 by A8,CARD_1:30 .= n; A15: source in V1 by A9,XBOOLE_0:def 3; not x in {sink} by A11,CARD_1:27,XBOOLE_0:def 5; then A16: x <> sink by TARSKI:def 1; then not sink in {x} by TARSKI:def 1; then not sink in V1 by A10,XBOOLE_0:def 3; then A17: EL.flow(source,sink) = Sum (EL|EV1V1a) - Sum (EL|EV1V1b) by A7,A14,A15; set EXXe = G.edgesDBetween({x}, VG \ {x}); set EXV2 = G.edgesDBetween({x},V2); set EV2X = G.edgesDBetween(V2,{x}); reconsider EA = EV1V1a \/ EV2X as Subset of the_Edges_of G; reconsider E1 = EA \ EXV1c as Subset of the_Edges_of G; reconsider EB = EA \ EV2X as Subset of the_Edges_of G; reconsider EC = EV1V1b \/ EXV2 as Subset of the_Edges_of G; reconsider E2 = EC \ EV1Xd as Subset of the_Edges_of G; reconsider ED = EC \ EXV2 as Subset of the_Edges_of G; A18: dom (EL|EA) = EA by PARTFUN1:def 2; now set e = the Element of EV1V1b /\ EXV2; assume EV1V1b meets EXV2; then A19: EV1V1b /\ EXV2 <> {} by XBOOLE_0:def 7; then e in EV1V1b by XBOOLE_0:def 4; then e DSJoins VG\V1,V1,G by GLIB_000:def 31; then SG.e in VG \ V1; then A20: not SG.e in V1 by XBOOLE_0:def 5; e in EXV2 by A19,XBOOLE_0:def 4; then e DSJoins {x},V2,G by GLIB_000:def 31; then SG.e in {x}; hence contradiction by A20,XBOOLE_0:def 3; end; then EV1V1b \ EXV2 = EV1V1b by XBOOLE_1:83; then A21: ED = EV1V1b by XBOOLE_1:40; now let e be object; assume A22: e in EXV1c; then A23: e DSJoins {x},VG \ V1, G by GLIB_000:def 31; then SG.e in {x}; then A24: SG.e in V1 by XBOOLE_0:def 3; TG.e in VG \ V1 by A23; then e DSJoins V1,VG \ V1, G by A22,A24; hence e in EV1V1a by GLIB_000:def 31; end; then A25: EXV1c c= EV1V1a; now set e = the Element of EV1V1a /\ EV2X; assume EV1V1a meets EV2X; then A26: EV1V1a /\ EV2X <> {} by XBOOLE_0:def 7; then e in EV1V1a by XBOOLE_0:def 4; then e DSJoins V1,VG\V1,G by GLIB_000:def 31; then TG.e in VG \ V1; then A27: not TG.e in V1 by XBOOLE_0:def 5; e in EV2X by A26,XBOOLE_0:def 4; then e DSJoins V2,{x},G by GLIB_000:def 31; then TG.e in {x}; hence contradiction by A27,XBOOLE_0:def 3; end; then EV1V1a \ EV2X = EV1V1a by XBOOLE_1:83; then A28: EB = EV1V1a by XBOOLE_1:40; A29: dom (EL|EB) = EB by PARTFUN1:def 2; A30: now let e be object; assume e in dom (EL|EA); then A31: e in EA; now per cases; suppose not e in EV2X; then A32: e in EB by A31,XBOOLE_0:def 5; hence (EL|EV2X +* EL|EB).e = (EL|EB).e by A29,FUNCT_4:13 .= EL.e by A32,FUNCT_1:49; end; suppose A33: e in EV2X; then not e in EB by XBOOLE_0:def 5; hence (EL|EV2X +* EL|EB).e = (EL|EV2X).e by A29,FUNCT_4:11 .= EL.e by A33,FUNCT_1:49; end; end; hence (EL|EA).e = (EL|EV2X +* EL|EB).e by A31,FUNCT_1:49; end; now let e be object; hereby assume A34: e in EXXe \ EXV2; then e in EXXe by XBOOLE_0:def 5; then A35: e DSJoins {x},VG\{x}, G by GLIB_000:def 31; then A36: SG.e in {x}; A37: TG.e in VG \ {x } by A35; then A38: not TG.e in {x } by XBOOLE_0:def 5; not e in EXV2 by A34,XBOOLE_0:def 5; then not e DSJoins {x},V2,G by GLIB_000:def 31; then not TG.e in V2 by A34,A36; then not TG.e in V1 by A38,XBOOLE_0:def 3; then TG.e in VG \ V1 by A37,XBOOLE_0:def 5; then e DSJoins {x}, VG \ V1, G by A34,A36; hence e in EXV1c by GLIB_000:def 31; end; assume A39: e in EXV1c; then A40: e DSJoins {x}, VG \ V1, G by GLIB_000:def 31; then A41: TG.e in VG \ V1; then A42: not TG.e in V1 by XBOOLE_0:def 5; then not TG.e in {x} by XBOOLE_0:def 3; then A43: TG.e in VG \ {x} by A41,XBOOLE_0:def 5; not TG.e in V2 by A42,XBOOLE_0:def 3; then not e DSJoins {x},V2,G; then A44: not e in EXV2 by GLIB_000:def 31; SG.e in {x} by A40; then e DSJoins {x}, VG \ {x}, G by A39,A43; then e in EXXe by GLIB_000:def 31; hence e in EXXe \ EXV2 by A44,XBOOLE_0:def 5; end; then A45: EXXe \ EXV2 = EXV1c by TARSKI:2; A46: dom (EL|ED) = ED by PARTFUN1:def 2; A47: now let e be object; assume e in dom (EL|EC); then A48: e in EC; now per cases; suppose not e in EXV2; then A49: e in ED by A48,XBOOLE_0:def 5; hence (EL|EXV2 +* EL|ED).e = (EL|ED).e by A46,FUNCT_4:13 .= EL.e by A49,FUNCT_1:49; end; suppose A50: e in EXV2; then not e in ED by XBOOLE_0:def 5; hence (EL|EXV2 +* EL|ED).e = (EL|EXV2).e by A46,FUNCT_4:11 .= EL.e by A50,FUNCT_1:49; end; end; hence (EL|EC).e = (EL|EXV2 +* EL|ED).e by A48,FUNCT_1:49; end; reconsider EXV1cb = EXXe \ EXV2 as Subset of the_Edges_of G; set EXXf = G.edgesDBetween(VG \ {x}, {x}); A51: dom (EL|EC) = EC by PARTFUN1:def 2; now let e be object; hereby assume A52: e in EXXf \ EV2X; then e in EXXf by XBOOLE_0:def 5; then A53: e DSJoins VG \ {x}, {x}, G by GLIB_000:def 31; then A54: TG.e in {x}; A55: SG.e in VG \ {x } by A53; then A56: not SG.e in {x } by XBOOLE_0:def 5; not e in EV2X by A52,XBOOLE_0:def 5; then not e DSJoins V2, {x}, G by GLIB_000:def 31; then not SG.e in V2 by A52,A54; then not SG.e in V1 by A56,XBOOLE_0:def 3; then SG.e in VG \ V1 by A55,XBOOLE_0:def 5; then e DSJoins VG \ V1, {x}, G by A52,A54; hence e in EV1Xd by GLIB_000:def 31; end; assume A57: e in EV1Xd; then A58: e DSJoins VG \ V1, {x}, G by GLIB_000:def 31; then A59: SG.e in VG \ V1; then A60: not SG.e in V1 by XBOOLE_0:def 5; then not SG.e in {x} by XBOOLE_0:def 3; then A61: SG.e in VG \ {x} by A59,XBOOLE_0:def 5; not SG.e in V2 by A60,XBOOLE_0:def 3; then not e DSJoins V2,{x},G; then A62: not e in EV2X by GLIB_000:def 31; TG.e in {x} by A58; then e DSJoins VG \ {x}, {x}, G by A57,A61; then e in EXXf by GLIB_000:def 31; hence e in EXXf \ EV2X by A62,XBOOLE_0:def 5; end; then A63: EXXf \ EV2X = EV1Xd by TARSKI:2; now let e be object; assume A64: e in EV1Xd; then A65: e DSJoins VG\V1,{x}, G by GLIB_000:def 31; then TG.e in {x}; then A66: TG.e in V1 by XBOOLE_0:def 3; SG.e in VG \ V1 by A65; then e DSJoins VG\V1,V1, G by A64,A66; hence e in EV1V1b by GLIB_000:def 31; end; then A67: EV1Xd c= EV1V1b; A68: not x in V2 by A12,XBOOLE_0:def 5; now let e be object; assume A69: e in EV2X; then A70: e DSJoins V2,{x},G by GLIB_000:def 31; then A71: SG.e in V2; then not SG.e in {x} by A68,TARSKI:def 1; then A72: SG.e in VG \ {x} by A71,XBOOLE_0:def 5; TG.e in {x} by A70; then e DSJoins VG\{x}, {x}, G by A69,A72; hence e in EXXf by GLIB_000:def 31; end; then A73: EV2X c= EXXf; A74: V2 qua set \ {x} is Subset of V2; now let e be object; A75: EV1V1a \/ EV2X qua set \ EXV1c is Subset of EV1V1a \/ EV2X; hereby assume A76: e in G.edgesDBetween(V2, VG \ V2); then A77: e DSJoins V2, VG \ V2, G by GLIB_000:def 31; then A78: SG.e in V2; A79: now assume e in EXV1c; then e DSJoins {x},VG \ V1,G by GLIB_000:def 31; then SG.e in {x}; hence contradiction by A68,A78,TARSKI:def 1; end; A80: TG.e in VG \ V2 by A77; A81: SG.e in V1 by A78,XBOOLE_0:def 3; now per cases; suppose TG.e in {x}; then e DSJoins V2,{x},G by A76,A78; then e in EV2X by GLIB_000:def 31; then e in EV1V1a \/ EV2X by XBOOLE_0:def 3; hence e in EV1V1a \/ EV2X \ EXV1c by A79,XBOOLE_0:def 5; end; suppose not TG.e in {x}; then TG.e in VG \ V1 by A13,A80,XBOOLE_0:def 5; then e DSJoins V1, VG \ V1, G by A76,A81; then e in EV1V1a by GLIB_000:def 31; then e in EV1V1a \/ EV2X by XBOOLE_0:def 3; hence e in EV1V1a \/ EV2X \ EXV1c by A79,XBOOLE_0:def 5; end; end; hence e in EV1V1a \/ EV2X \ EXV1c; end; assume A82: e in EV1V1a \/ EV2X \ EXV1c; then not e in EXV1c by XBOOLE_0:def 5; then A83: not e DSJoins {x}, VG \ V1,G by GLIB_000:def 31; now per cases by A82,A75,XBOOLE_0:def 3; suppose A84: e in EV1V1a; then A85: e DSJoins V1, VG\V1, G by GLIB_000:def 31; then A86: SG.e in V1; A87: TG.e in VG \ V1 by A85; then not TG.e in V1 by XBOOLE_0:def 5; then not TG.e in V2 by XBOOLE_0:def 3; then A88: TG.e in VG \ V2 by A87,XBOOLE_0:def 5; not SG.e in {x} by A83,A84,A87; then SG.e in V1 \ {x} by A86,XBOOLE_0:def 5; then SG.e in V2 \ {x} by XBOOLE_1:40; hence e DSJoins V2, VG \ V2, G by A74,A84,A88; end; suppose A89: e in EV2X; then A90: e DSJoins V2, {x}, G by GLIB_000:def 31; then A91: SG.e in V2; TG.e in {x} by A90; then A92: not TG.e in V2 by A68,TARSKI:def 1; TG.e in VG by A89,FUNCT_2:5; then TG.e in VG \ V2 by A92,XBOOLE_0:def 5; hence e DSJoins V2, VG \ V2, G by A89,A91; end; end; hence e in G.edgesDBetween(V2, VG \ V2) by GLIB_000:def 31; end; then A93: G.edgesDBetween(V2, VG \ V2) = EV1V1a \/ EV2X \ EXV1c by TARSKI:2; now let e be object; A94: EV1V1b \/ EXV2 qua set \ EV1Xd is Subset of EV1V1b \/ EXV2; hereby assume A95: e in G.edgesDBetween(VG \ V2, V2); then A96: e DSJoins VG\V2, V2, G by GLIB_000:def 31; then A97: TG.e in V2; A98: now assume e in EV1Xd; then e DSJoins VG \ V1,{x},G by GLIB_000:def 31; then TG.e in {x}; hence contradiction by A68,A97,TARSKI:def 1; end; A99: SG.e in VG \ V2 by A96; A100: TG.e in V1 by A97,XBOOLE_0:def 3; now per cases; suppose SG.e in {x}; then e DSJoins {x},V2,G by A95,A97; then e in EXV2 by GLIB_000:def 31; then e in EV1V1b \/ EXV2 by XBOOLE_0:def 3; hence e in EV1V1b \/ EXV2 \ EV1Xd by A98,XBOOLE_0:def 5; end; suppose not SG.e in {x}; then SG.e in VG \ V1 by A13,A99,XBOOLE_0:def 5; then e DSJoins VG \ V1, V1, G by A95,A100; then e in EV1V1b by GLIB_000:def 31; then e in EV1V1b \/ EXV2 by XBOOLE_0:def 3; hence e in EV1V1b \/ EXV2 \ EV1Xd by A98,XBOOLE_0:def 5; end; end; hence e in EV1V1b \/ EXV2 \ EV1Xd; end; assume A101: e in EV1V1b \/ EXV2 \ EV1Xd; then not e in EV1Xd by XBOOLE_0:def 5; then A102: not e DSJoins VG \ V1, {x}, G by GLIB_000:def 31; now per cases by A101,A94,XBOOLE_0:def 3; suppose A103: e in EV1V1b; then A104: e DSJoins VG\V1, V1, G by GLIB_000:def 31; then A105: TG.e in V1; A106: SG.e in VG \ V1 by A104; then not SG.e in V1 by XBOOLE_0:def 5; then not SG.e in V2 by XBOOLE_0:def 3; then A107: SG.e in VG \ V2 by A106,XBOOLE_0:def 5; not TG.e in {x} by A102,A103,A106; then TG.e in V1 \ {x} by A105,XBOOLE_0:def 5; then TG.e in V2 \ {x} by XBOOLE_1:40; hence e DSJoins VG \ V2, V2, G by A74,A103,A107; end; suppose A108: e in EXV2; then A109: e DSJoins {x},V2, G by GLIB_000:def 31; then A110: TG.e in V2; SG.e in {x} by A109; then A111: not SG.e in V2 by A68,TARSKI:def 1; SG.e in VG by A108,FUNCT_2:5; then SG.e in VG \ V2 by A111,XBOOLE_0:def 5; hence e DSJoins VG \ V2, V2, G by A108,A110; end; end; hence e in G.edgesDBetween(VG\V2,V2) by GLIB_000:def 31; end; then A112: G.edgesDBetween(VG \ V2, V2) = E2 by TARSKI:2; A113: dom (EL|E2)=EC\EV1Xd by PARTFUN1:def 2; A114: now let e be object; assume e in dom (EL|EC); then A115: e in EC; now per cases; suppose not e in EV1Xd; then A116: e in E2 by A115,XBOOLE_0:def 5; hence (EL|EV1Xd +* EL|E2).e = (EL|E2).e by A113,FUNCT_4:13 .= EL.e by A116,FUNCT_1:49; end; suppose A117: e in EV1Xd; then not e in E2 by XBOOLE_0:def 5; hence (EL|EV1Xd +* EL|E2).e = (EL|EV1Xd).e by A113,FUNCT_4:11 .= EL.e by A117,FUNCT_1:49; end; end; hence (EL|EC).e = (EL|EV1Xd +* EL|E2).e by A115,FUNCT_1:49; end; dom (EL|EXV2)=EXV2 by PARTFUN1:def 2; then dom (EL|EXV2 +* EL|ED) = EXV2 \/ ED by A46,FUNCT_4:def 1 .= EXV2 \/ (EV1V1b \/ EXV2) by XBOOLE_1:39 .= EC by XBOOLE_1:6; then A118: Sum (EL|EC) = Sum (EL|EXV2) + Sum (EL|EV1V1b) by A21,A51,A47,FUNCT_1:2 ,GLIB_004:3; dom (EL|EV1Xd) = EV1Xd by PARTFUN1:def 2; then dom (EL|EV1Xd +* EL|E2) = EV1Xd \/ (EC \ EV1Xd) by A113, FUNCT_4:def 1 .= EV1Xd \/ (EV1V1b \/ EXV2) by XBOOLE_1:39 .= EC by A67,XBOOLE_1:10,12; then A119: Sum (EL|EC) = Sum (EL|E2) + Sum (EL|EV1Xd) by A51,A114,FUNCT_1:2 ,GLIB_004:3; dom (EL|EV2X)=EV2X by PARTFUN1:def 2; then dom (EL|EV2X +* EL|EB) = EV2X \/ EB by A29,FUNCT_4:def 1 .= EV2X \/ (EV1V1a \/ EV2X) by XBOOLE_1:39 .= EA by XBOOLE_1:6; then A120: Sum (EL|EA) = Sum (EL|EV2X) + Sum (EL|EV1V1a) by A28,A18,A30,FUNCT_1:2 ,GLIB_004:3; reconsider EV1Xdb = EXXf \ EV2X as Subset of the_Edges_of G; A121: dom (EL|EV1Xdb) = EXXf \ EV2X by PARTFUN1:def 2; now let e be object; assume A122: e in EXV2; then A123: e DSJoins {x},V2,G by GLIB_000:def 31; then A124: TG.e in V2; then not TG.e in {x} by A68,TARSKI:def 1; then A125: TG.e in VG \ {x} by A124,XBOOLE_0:def 5; SG.e in {x} by A123; then e DSJoins {x},VG\{x}, G by A122,A125; hence e in EXXe by GLIB_000:def 31; end; then A126: EXV2 c= EXXe; A127: dom (EL|E1)=EA \ EXV1c by PARTFUN1:def 2; A128: now let e be object; assume e in dom (EL|EA); then A129: e in EA; now per cases; suppose not e in EXV1c; then A130: e in E1 by A129,XBOOLE_0:def 5; hence (EL|EXV1c +* EL|E1).e = (EL|E1).e by A127,FUNCT_4:13 .= EL.e by A130,FUNCT_1:49; end; suppose A131: e in EXV1c; then not e in E1 by XBOOLE_0:def 5; hence (EL|EXV1c +* EL|E1).e = (EL|EXV1c).e by A127,FUNCT_4:11 .= EL.e by A131,FUNCT_1:49; end; end; hence (EL|EA).e = (EL|EXV1c +* EL|E1).e by A129,FUNCT_1:49; end; A132: dom (EL|EXXf) = EXXf by PARTFUN1:def 2; A133: now let e be object; assume A134: e in dom (EL|EXXf); then A135: e in EXXf; now per cases; suppose A136: e in EV2X; then not e in EV1Xdb by XBOOLE_0:def 5; hence (EL|EV2X +* EL|EV1Xdb).e=(EL|EV2X).e by A121,FUNCT_4:11 .=EL.e by A136,FUNCT_1:49; end; suppose not e in EV2X; then A137: e in EV1Xdb by A135,XBOOLE_0:def 5; hence (EL|EV2X +* EL|EV1Xdb).e = (EL|EV1Xdb).e by A121,FUNCT_4:13 .= EL.e by A137,FUNCT_1:49; end; end; hence (EL|EXXf).e = (EL|EV2X +* EL|EV1Xdb).e by A134,FUNCT_1:49; end; dom (EL|EV2X) = EV2X by PARTFUN1:def 2; then dom (EL|EV2X +* EL|(EXXf \ EV2X)) = EV2X \/ (EXXf \ EV2X) by A121, FUNCT_4:def 1 .= EV2X \/ EXXf by XBOOLE_1:39 .= EXXf by A73,XBOOLE_1:12; then A138: Sum (EL|EV2X) + Sum (EL|EV1Xd) = Sum (EL|EXXf) by A63,A132,A133,FUNCT_1:2 ,GLIB_004:3; dom (EL|EXV1c) = EXV1c by PARTFUN1:def 2; then dom (EL|EXV1c +* EL|E1) = EXV1c \/ (EA \ EXV1c) by A127, FUNCT_4:def 1 .= EXV1c \/ (EV1V1a \/ EV2X) by XBOOLE_1:39 .= EA by A25,XBOOLE_1:10,12; then A139: Sum (EL|EA) = Sum (EL|E1) + Sum (EL|EXV1c) by A18,A128,FUNCT_1:2 ,GLIB_004:3; A140: dom (EL|EXV1cb) = EXXe \ EXV2 by PARTFUN1:def 2; A141: dom (EL|EXXe) = EXXe by PARTFUN1:def 2; A142: now let e be object; assume A143: e in dom (EL|EXXe); then A144: e in EXXe; now per cases; suppose A145: e in EXV2; then not e in EXV1cb by XBOOLE_0:def 5; hence (EL|EXV2 +* EL|EXV1cb).e=(EL|EXV2).e by A140,FUNCT_4:11 .=EL.e by A145,FUNCT_1:49; end; suppose not e in EXV2; then A146: e in EXV1cb by A144,XBOOLE_0:def 5; hence (EL|EXV2 +* EL|EXV1cb).e = (EL|EXV1cb).e by A140,FUNCT_4:13 .= EL.e by A146,FUNCT_1:49; end; end; hence (EL|EXXe).e = (EL|EXV2 +* EL|EXV1cb).e by A143,FUNCT_1:49; end; dom (EL|EXV2) = EXV2 by PARTFUN1:def 2; then dom (EL|EXV2 +* EL|(EXXe \ EXV2)) = EXV2 \/ (EXXe \ EXV2) by A140, FUNCT_4:def 1 .= EXV2 \/ EXXe by XBOOLE_1:39 .= EXXe by A126,XBOOLE_1:12; then A147: Sum (EL|EXV2) + Sum (EL|EXV1c) = Sum (EL|EXXe) by A45,A141,A142,FUNCT_1:2 ,GLIB_004:3; reconsider x as Vertex of G by A12; A148: x.edgesOut() = G.edgesDBetween({x},VG) by GLIB_000:39; reconsider EXXeb = G.edgesDBetween({x},VG)\G.edgesDBetween({x},{x}) as Subset of the_Edges_of G; reconsider EXXfb = G.edgesDBetween(VG,{x})\G.edgesDBetween({x},{x}) as Subset of the_Edges_of G; A149: dom (EL|G.edgesDBetween(VG,{x})) = G.edgesDBetween(VG,{x}) by PARTFUN1:def 2; now let e be object; hereby assume A150: e in G.edgesDBetween(VG,{x}) \ G.edgesDBetween({x},{x}); then e in G.edgesDBetween(VG,{x}) by XBOOLE_0:def 5; then A151: e DSJoins VG,{x},G by GLIB_000:def 31; then A152: SG.e in VG; A153: TG.e in {x} by A151; not e in G.edgesDBetween({x},{x}) by A150,XBOOLE_0:def 5; then not e DSJoins {x},{x},G by GLIB_000:def 31; then not SG.e in {x} by A150,A153; then SG.e in VG\{x} by A152,XBOOLE_0:def 5; then e DSJoins VG\{x},{x},G by A150,A153; hence e in EXXf by GLIB_000:def 31; end; assume A154: e in EXXf; then A155: e DSJoins VG \{x}, {x}, G by GLIB_000:def 31; then A156: SG.e in VG \ {x}; then not SG.e in {x} by XBOOLE_0:def 5; then not e DSJoins {x},{x},G; then A157: not e in G.edgesDBetween({x},{x}) by GLIB_000:def 31; TG.e in {x} by A155; then e DSJoins VG,{x},G by A154,A156; then e in G.edgesDBetween(VG,{x}) by GLIB_000:def 31; hence e in G.edgesDBetween(VG,{x}) \ G.edgesDBetween({x},{x}) by A157, XBOOLE_0:def 5; end; then A158: G.edgesDBetween(VG,{x}) \ G.edgesDBetween({x},{x}) = EXXf by TARSKI:2; A159: dom (EL|EXXfb) = EXXfb by PARTFUN1:def 2; A160: now let e be object; assume e in dom (EL|G.edgesDBetween(VG,{x})); then A161: e in G.edgesDBetween(VG,{x}); now per cases; suppose A162: e in G.edgesDBetween({x},{x}); then not e in EXXfb by XBOOLE_0:def 5; hence (EL|G.edgesDBetween({x},{x}) +* EL|EXXfb).e = (EL|G .edgesDBetween({x},{x})).e by A159,FUNCT_4:11 .= EL.e by A162,FUNCT_1:49; end; suppose not e in G.edgesDBetween({x},{x}); then A163: e in EXXfb by A161,XBOOLE_0:def 5; hence (EL|G.edgesDBetween({x},{x}) +* EL|EXXfb).e = (EL|EXXfb).e by A159, FUNCT_4:13 .= EL.e by A163,FUNCT_1:49; end; end; hence (EL|G.edgesDBetween(VG,{x})).e = (EL|G.edgesDBetween({x},{x}) +* EL|EXXfb).e by A161,FUNCT_1:49; end; now let e be object; hereby assume A164: e in G.edgesDBetween({x},VG) \ G.edgesDBetween({x},{x}); then e in G.edgesDBetween({x},VG) by XBOOLE_0:def 5; then A165: e DSJoins {x},VG,G by GLIB_000:def 31; then A166: TG.e in VG; A167: SG.e in {x} by A165; not e in G.edgesDBetween({x},{x}) by A164,XBOOLE_0:def 5; then not e DSJoins {x},{x},G by GLIB_000:def 31; then not TG.e in {x} by A164,A167; then TG.e in VG\{x} by A166,XBOOLE_0:def 5; then e DSJoins {x},VG\{x},G by A164,A167; hence e in EXXe by GLIB_000:def 31; end; assume A168: e in EXXe; then A169: e DSJoins {x}, VG \{x}, G by GLIB_000:def 31; then A170: TG.e in VG \ {x}; then not TG.e in {x} by XBOOLE_0:def 5; then not e DSJoins {x},{x},G; then A171: not e in G.edgesDBetween({x},{x}) by GLIB_000:def 31; SG.e in {x} by A169; then e DSJoins {x},VG,G by A168,A170; then e in G.edgesDBetween({x},VG) by GLIB_000:def 31; hence e in G.edgesDBetween({x},VG) \ G.edgesDBetween({x},{x}) by A171, XBOOLE_0:def 5; end; then A172: G.edgesDBetween({x},VG) \ G.edgesDBetween({x},{x}) = EXXe by TARSKI:2; A173: dom (EL|G.edgesDBetween({x},VG)) = G.edgesDBetween({x},VG) by PARTFUN1:def 2; A174: dom (EL|EXXeb) = EXXeb by PARTFUN1:def 2; A175: now let e be object; assume e in dom (EL|G.edgesDBetween({x},VG)); then A176: e in G.edgesDBetween({x},VG); now per cases; suppose A177: e in G.edgesDBetween({x},{x}); then not e in EXXeb by XBOOLE_0:def 5; hence (EL|G.edgesDBetween({x},{x}) +* EL|EXXeb).e = (EL|G .edgesDBetween({x},{x})).e by A174,FUNCT_4:11 .= EL.e by A177,FUNCT_1:49; end; suppose not e in G.edgesDBetween({x},{x}); then A178: e in EXXeb by A176,XBOOLE_0:def 5; hence (EL|G.edgesDBetween({x},{x}) +* EL|EXXeb).e = (EL|EXXeb).e by A174, FUNCT_4:13 .= EL.e by A178,FUNCT_1:49; end; end; hence (EL|G.edgesDBetween({x},VG)).e = (EL|G.edgesDBetween({x},{x}) +* EL|EXXeb).e by A176,FUNCT_1:49; end; A179: dom (EL|G.edgesDBetween({x},{x})) = G.edgesDBetween({x},{x}) by PARTFUN1:def 2; then dom (EL|G.edgesDBetween({x},{x}) +* EL|EXXfb) = G.edgesDBetween({x },{x}) \/ EXXfb by A159,FUNCT_4:def 1 .= G.edgesDBetween({x},{x}) \/ G.edgesDBetween(VG,{x}) by XBOOLE_1:39 .= G.edgesDBetween(VG,{x}) by GLIB_000:38,XBOOLE_1:12; then A180: Sum (EL|G.edgesDBetween(VG,{x})) = Sum (EL|EXXf) + Sum (EL|G .edgesDBetween({x},{x})) by A158,A149,A160,FUNCT_1:2,GLIB_004:3; dom (EL|G.edgesDBetween({x},{x}) +* EL|EXXeb) = G.edgesDBetween({x },{x}) \/ EXXeb by A179,A174,FUNCT_4:def 1 .= G.edgesDBetween({x},{x}) \/ G.edgesDBetween({x},VG) by XBOOLE_1:39 .= G.edgesDBetween({x},VG) by GLIB_000:38,XBOOLE_1:12; then A181: Sum (EL|G.edgesDBetween({x},VG)) = Sum (EL|EXXe) + Sum (EL|G .edgesDBetween({x},{x})) by A172,A173,A175,FUNCT_1:2,GLIB_004:3; x.edgesIn() = G.edgesDBetween(VG,{x}) by GLIB_000:39; then Sum (EL|G.edgesDBetween(VG,{x}))= Sum (EL|G.edgesDBetween({x } ,VG ) ) by A1,A9,A68,A16,A148; hence EL.flow(source,sink) = Sum(EL | G.edgesDBetween(V2, VG \ V2)) - Sum (EL | G.edgesDBetween(VG \ V2, V2)) by A17,A93,A139,A120,A112,A119,A118,A138 ,A147,A180,A181; end; hence P[n+1]; end; now set ESS = G.edgesDBetween({sink},{sink}); let V be Subset of VG; assume that A182: card (VG \ V) = 1 and source in V and A183: not sink in V; reconsider EOUT= G.edgesOutOf({sink})\ ESS as Subset of the_Edges_of G; consider v being object such that A184: VG \ V = {v} by A182,CARD_2:42; sink is Vertex of G by A1; then sink in VG \ V by A183,XBOOLE_0:def 5; then A185: v = sink by A184,TARSKI:def 1; A186: now let x be object; hereby assume A187: x in VG \ {sink}; then not x in {sink} by XBOOLE_0:def 5; hence x in V by A184,A185,A187,XBOOLE_0:def 5; end; assume A188: x in V; then not x in {sink} by A183,TARSKI:def 1; hence x in VG \ {sink} by A188,XBOOLE_0:def 5; end; then A189: V = VG \ {sink} by TARSKI:2; now let e be object; hereby assume A190: e in G.edgesDBetween(VG \ V, V); then A191: e DSJoins {sink},(VG \ {sink}),G by A184,A185,A189,GLIB_000:def 31; then A192: TG.e in (VG \ {sink}); A193: now assume e in ESS; then e DSJoins {sink},{sink},G by GLIB_000:def 31; then TG.e in {sink}; hence contradiction by A192,XBOOLE_0:def 5; end; SG.e in {sink} by A191; then e in G.edgesOutOf({sink}) by A190,GLIB_000:def 27; hence e in EOUT by A193,XBOOLE_0:def 5; end; assume A194: e in EOUT; G.edgesOutOf({sink}) qua set \ ESS is Subset of G.edgesOutOf({sink} ); then A195: SG.e in {sink} by A194,GLIB_000:def 27; A196: not e in ESS by A194,XBOOLE_0:def 5; now assume A197: not TG.e in V; TG.e in VG by A194,FUNCT_2:5; then TG.e in {sink} by A189,A197,XBOOLE_0:def 5; then e DSJoins {sink},{sink},G by A194,A195; hence contradiction by A196,GLIB_000:def 31; end; then e DSJoins (VG \ V),V,G by A184,A185,A194,A195; hence e in G.edgesDBetween(VG \ V, V) by GLIB_000:def 31; end; then A198: G.edgesDBetween(VG \ V, V) = EOUT by TARSKI:2; set EESS = EL|ESS; reconsider EIN = G.edgesInto({sink}) \ ESS as Subset of the_Edges_of G; A199: dom (EL|G.edgesInto({sink})) = G.edgesInto({sink}) by PARTFUN1:def 2; now let e be object; hereby assume A200: e in G.edgesDBetween(V, VG \ V); then A201: e DSJoins VG \ {sink}, {sink},G by A184,A185,A189,GLIB_000:def 31; then A202: SG.e in VG \ {sink}; A203: now assume e in ESS; then e DSJoins {sink},{sink},G by GLIB_000:def 31; then SG.e in {sink}; hence contradiction by A202,XBOOLE_0:def 5; end; TG.e in {sink} by A201; then e in G.edgesInto({sink}) by A200,GLIB_000:def 26; hence e in EIN by A203,XBOOLE_0:def 5; end; assume A204: e in EIN; G.edgesInto({sink}) qua set \ ESS is Subset of G.edgesInto({sink}); then A205: TG.e in {sink} by A204,GLIB_000:def 26; A206: not e in ESS by A204,XBOOLE_0:def 5; now assume not SG.e in V; then A207: not SG.e in VG \ {sink} by A186; SG.e in VG by A204,FUNCT_2:5; then SG.e in {sink} by A207,XBOOLE_0:def 5; then e DSJoins {sink},{sink},G by A204,A205; hence contradiction by A206,GLIB_000:def 31; end; then e DSJoins V, {sink}, G by A204,A205; hence e in G.edgesDBetween(V, VG \ V) by A184,A185,GLIB_000:def 31; end; then A208: G.edgesDBetween(V, VG \ V) = EIN by TARSKI:2; now let e be object; assume A209: e in ESS; then e DSJoins {sink},{sink},G by GLIB_000:def 31; then SG.e in {sink}; hence e in G.edgesOutOf({sink}) by A209,GLIB_000:def 27; end; then A210: ESS c= G.edgesOutOf({sink}); now let e be object; assume A211: e in ESS; then e DSJoins {sink},{sink},G by GLIB_000:def 31; then TG.e in {sink}; hence e in G.edgesInto({sink}) by A211,GLIB_000:def 26; end; then A212: ESS c= G.edgesInto({sink}); A213: dom (EL|ESS)=ESS by PARTFUN1:def 2; A214: dom (EL|EOUT)=EOUT by PARTFUN1:def 2; A215: now let e be object; assume A216: e in dom (EL|G.edgesOutOf({sink})); then A217: e in G.edgesOutOf({sink}); now per cases; suppose A218: e in ESS; then not e in EOUT by XBOOLE_0:def 5; hence (EL|ESS +* EL|EOUT).e = (EL|ESS).e by A214,FUNCT_4:11 .= EL.e by A213,A218,FUNCT_1:47; end; suppose not e in ESS; then A219: e in EOUT by A217,XBOOLE_0:def 5; hence (EL|ESS +* EL|EOUT).e = (EL|EOUT).e by A214,FUNCT_4:13 .= EL.e by A214,A219,FUNCT_1:47; end; end; hence EL|G.edgesOutOf({sink}).e = (EL|ESS +* EL|EOUT).e by A216, FUNCT_1:47; end; A220: dom (EL|EIN)=EIN by PARTFUN1:def 2; A221: now let e be object; assume A222: e in dom (EL|G.edgesInto({sink})); then A223: e in G.edgesInto({sink}); now per cases; suppose A224: e in ESS; then not e in EIN by XBOOLE_0:def 5; hence (EL|ESS +* EL|EIN).e = (EL|ESS).e by A220,FUNCT_4:11 .= EL.e by A213,A224,FUNCT_1:47; end; suppose not e in ESS; then A225: e in EIN by A223,XBOOLE_0:def 5; hence (EL|ESS +* EL|EIN).e = (EL|EIN).e by A220,FUNCT_4:13 .= EL.e by A220,A225,FUNCT_1:47; end; end; hence EL|G.edgesInto({sink}).e = (EL|ESS +* EL|EIN).e by A222,FUNCT_1:47; end; A226: ESS \/ EIN = G.edgesInto({sink}) \/ ESS by XBOOLE_1:39 .= G.edgesInto({sink}) by A212,XBOOLE_1:12; dom (EL|ESS +* EL|EIN) = ESS \/ EIN by A213,A220,FUNCT_4:def 1; then A227: Sum (EL|G.edgesInto({sink})) = Sum (EL|EIN) + Sum EESS by A226,A199,A221, FUNCT_1:2,GLIB_004:3; ESS \/ EOUT = G.edgesOutOf({sink}) \/ ESS by XBOOLE_1:39 .= G.edgesOutOf({sink}) by A210,XBOOLE_1:12; then A228: dom (EL|ESS +* EL|EOUT) = G.edgesOutOf({sink}) by A213,A214,FUNCT_4:def 1 ; dom (EL|G.edgesOutOf({sink})) = G.edgesOutOf({sink}) by PARTFUN1:def 2; then EL.flow(source,sink) = Sum (EL|EIN)+Sum EESS -(Sum EESS + Sum (EL| EOUT)) by A227,A228,A215,FUNCT_1:2,GLIB_004:3 .= Sum (EL|EIN) - Sum (EL|EOUT); hence EL.flow(source,sink) = Sum (EL | G.edgesDBetween(V, VG \ V)) - Sum ( EL | G.edgesDBetween(VG \ V, V)) by A208,A198; end; then A229: P[1]; for n being non zero Nat holds P[n] from NAT_1:sch 10(A229,A6); hence thesis by A2,A3,A4; end; theorem Th12: 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)) proof let G be finite real-weighted WGraph, EL being FF:ELabeling of G, source, sink be set, V be Subset of the_Vertices_of G; assume that A1: EL has_valid_flow_from source,sink and A2: source in V and A3: not sink in V; set W1 = (the_Weight_of G) | G.edgesDBetween(V, the_Vertices_of G \ V); set E2 = EL | G.edgesDBetween(the_Vertices_of G \ V, V); set E1 = EL | G.edgesDBetween(V, the_Vertices_of G \ V); now let e be set; assume A4: e in G.edgesDBetween(V, the_Vertices_of G\V); then A5: W1.e = (the_Weight_of G).e by FUNCT_1:49; E1.e = EL.e by A4,FUNCT_1:49; hence E1.e <= W1.e by A1,A4,A5; end; then Sum E1 <= Sum W1 by GLIB_004:5; then A6: Sum E1 - Sum E2 <= Sum W1 - Sum E2 by XREAL_1:9; set B1 = EmptyBag G.edgesDBetween(the_Vertices_of G \ V, V); A7: now let e be set; A8: B1 = G.edgesDBetween(the_Vertices_of G \ V, V)-->0 by PBOOLE:def 3; assume e in G.edgesDBetween(the_Vertices_of G \ V, V); hence B1.e <= E2.e by A8,FUNCOP_1:7; end; Sum B1 = 0 by UPROOTS:11; then 0 <= Sum E2 by A7,GLIB_004:5; then A9: Sum W1 - Sum E2 <= Sum W1 - 0 by XREAL_1:13; EL.flow(source,sink) = Sum E1 - Sum E2 by A1,A2,A3,Th11; hence thesis by A9,A6,XXREAL_0:2; end; theorem Th13: 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) proof let G be finite natural-weighted WGraph, EL being FF:ELabeling of G, W be Walk of G such that A1: W is non trivial and A2: W is_augmenting_wrt EL; set T = W.tolerance(EL); T in rng (W.flowSeq(EL)) by A1,A2,Def16; then consider n being Nat such that A3: n in dom (W.flowSeq(EL)) and A4: T = (W.flowSeq(EL)).n by FINSEQ_2:10; reconsider n as Element of NAT by ORDINAL1:def 12; dom (W.flowSeq(EL)) = dom W.edgeSeq() by A2,Def15; then A5: 2*n in dom W by A3,GLIB_001:78; then 1 <= 2*n by FINSEQ_3:25; then reconsider 2n1 = 2*n-1 as odd Element of NAT by INT_1:5; 2*n <= len W by A5,FINSEQ_3:25; then A6: 2*n-1 < len W - 0 by XREAL_1:15; set v1 = W.(2n1), e = W.(2*n), v2 = W.(2*n+1); A7: 2*n-1 + 2 = 2*n+1; A8: 2*n-1 + 1 = 2*n; now per cases; suppose A9: e DJoins v1,v2,G; then A10: T = (the_Weight_of G).e - EL.e by A2,A3,A4,Def15; EL.e < (the_Weight_of G).e by A2,A6,A8,A7,A9; then EL.e - EL.e < T by A10,XREAL_1:14; hence thesis; end; suppose A11: not e DJoins v1,v2,G; then T = EL.e by A2,A3,A4,Def15; hence thesis by A2,A6,A8,A7,A11; end; end; hence thesis; end; theorem Th14: 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 proof let G be finite natural-weighted WGraph, EL being FF:ELabeling of G, source, sink be set, P be Path of G; assume that A1: source <> sink and A2: EL has_valid_flow_from source,sink and A3: P is_Walk_from source,sink and A4: P is_augmenting_wrt EL; set EL2 = FF:PushFlow(EL,P); now thus source is Vertex of G & sink is Vertex of G by A2; now let e be set; assume A5: e in the_Edges_of G; then A6: EL.e <= (the_Weight_of G).e by A2; now per cases; suppose not e in P.edges(); hence 0 <= EL2.e & EL2.e <= (the_Weight_of G).e by A4,A5,A6,Def17; end; suppose e in P.edges(); then consider n being odd Element of NAT such that A7: n < len P and A8: P.(n+1) = e by GLIB_001:100; set PFS = P.flowSeq(EL), n1div2 = (n+1) div 2; A9: 1 <= n+1 by NAT_1:11; n+1 <= len P by A7,NAT_1:13; then n1div2 in dom P.edgeSeq() by A9,GLIB_001:77; then A10: n1div2 in dom PFS by A4,Def15; A11: now A12: n + 0 < n+2 by XREAL_1:8; assume that A13: e DJoins P.n,P.(n+2),G and A14: e DJoins P.(n+2),P.n,G; A15: (the_Source_of G).e = P.n by A13; A16: (the_Source_of G).e = P.(n+2) by A14; A17: n+2 <= len P by A7,GLIB_001:1; then n = 1 by A15,A16,A12,GLIB_001:def 28; then A18: P.n = source by A3,GLIB_001:17; n+2 = len P by A15,A16,A12,A17,GLIB_001:def 28; hence contradiction by A1,A3,A15,A16,A18,GLIB_001:17; end; A19: P.last() = sink by A3,GLIB_001:def 23; P.first() = source by A3,GLIB_001:def 23; then A20: P is non trivial by A1,A19,GLIB_001:127; 2 divides n+1 by PEPIN:22; then A21: 2 * n1div2 = n+1 by NAT_D:3; then A22: 2 * n1div2 - 1 = n; A23: 2 * n1div2 + 1 = n + 2 by A21; A24: e Joins P.n,P.(n+2),G by A7,A8,GLIB_001:def 3; now per cases by A24; suppose A25: e DJoins P.n,P.(n+2),G; then PFS.n1div2 = (the_Weight_of G).e - EL.e by A4,A8,A10,A22,A23 ,Def15; then (the_Weight_of G).e - EL.e in rng PFS by A10,FUNCT_1:def 3; then A26: P.tolerance(EL) <= (the_Weight_of G).e-EL.e by A4,A20,Def16; thus 0 <= EL2.e; EL.e + P.tolerance(EL) = EL2.e by A4,A7,A8,A25,Def17; then EL2.e <= (the_Weight_of G).e - EL.e + EL.e by A26,XREAL_1:7; hence EL2.e <= (the_Weight_of G).e; end; suppose A27: e DJoins P.(n+2),P.n,G; thus 0 <= EL2.e; EL2.e = EL.e - P.tolerance(EL) by A4,A7,A8,A11,A27,Def17; then EL2.e <= EL.e - 0 by XREAL_1:13; hence EL2.e <= (the_Weight_of G).e by A6,XXREAL_0:2; end; end; hence 0 <= EL2.e & EL2.e <= (the_Weight_of G).e; end; end; hence 0 <= EL2.e & EL2.e <= (the_Weight_of G).e; end; hence for e being set st e in the_Edges_of G holds 0 <= EL2.e & EL2.e <= ( the_Weight_of G).e; let v be Vertex of G; assume that A28: v <> source and A29: v <> sink; A30: Sum (EL | v.edgesIn()) = Sum (EL | v.edgesOut()) by A2,A28,A29; now per cases; suppose v in P.vertices(); then consider n being odd Element of NAT such that A31: n <= len P and A32: P.n = v by GLIB_001:87; A33: now assume n = len P; then v = P.last() by A32,GLIB_001:def 7 .= sink by A3,GLIB_001:def 23; hence contradiction by A29; end; then A34: n < len P by A31,XXREAL_0:1; A35: now assume n = 1; then v = P.first() by A32,GLIB_001:def 6 .= source by A3,GLIB_001:def 23; hence contradiction by A28; end; A36: now A37: n+0 < n+2 by XREAL_1:8; assume A38: v = P.(n+2); n+2 <= len P by A34,GLIB_001:1; hence contradiction by A32,A35,A38,A37,GLIB_001:def 28; end; 1 <= n by ABIAN:12; then 1 < n by A35,XXREAL_0:1; then 1+1 <= n by NAT_1:13; then reconsider n2 = n-2*1 as odd Element of NAT by INT_1:5; set e1 = P.(n2+1), e2 = P.(n+1), T = P.tolerance(EL); A39: 1 <= n2+1 by NAT_1:11; A40: P.(n2+2) = v by A32; A41: now let e be set; assume that A42: e in v.edgesIn() or e in v.edgesOut() and A43: e <> e1 and A44: e <> e2; now assume e in P.edges(); then consider v1,v2 being Vertex of G, m being odd Element of NAT such that A45: m+2 <= len P and A46: v1 = P.m and A47: e = P.(m+1) and A48: v2 = P.(m+2) and A49: e Joins v1,v2,G by GLIB_001:103; A50: now per cases by A42; suppose e in v.edgesIn(); then (the_Target_of G).e = v by GLIB_000:56; hence v1 = v or v2 = v by A49; end; suppose e in v.edgesOut(); then (the_Source_of G).e = v by GLIB_000:58; hence v1 = v or v2 = v by A49; end; end; A51: m+2-2 < len P - 0 by A45,XREAL_1:15; now per cases by A50; suppose A52: v1 = v; now per cases by XXREAL_0:1; suppose m < n; hence contradiction by A31,A32,A33,A46,A52,GLIB_001:def 28; end; suppose m = n; hence contradiction by A44,A47; end; suppose n < m; hence contradiction by A32,A46,A51,A52,GLIB_001:def 28; end; end; hence contradiction; end; suppose A53: v2 = v; now per cases by XXREAL_0:1; suppose m+2 < n; hence contradiction by A31,A32,A33,A48,A53,GLIB_001:def 28; end; suppose m+2 = n; hence contradiction by A43,A47; end; suppose n < m+2; hence contradiction by A32,A35,A45,A48,A53,GLIB_001:def 28; end; end; hence contradiction; end; end; hence contradiction; end; hence not e in P.edges(); end; A54: now A55: n+2 <= len P by A34,GLIB_001:1; A56: n + 0 < n+2 by XREAL_1:8; assume that A57: e2 DJoins v,P.(n+2),G and A58: e2 DJoins P.(n+2),v,G; P.n = (the_Source_of G).e2 by A32,A57 .= P.(n+2) by A58; hence contradiction by A35,A56,A55,GLIB_001:def 28; end; n2 < n - 0 by XREAL_1:15; then A59: n2+1 < n+1 by XREAL_1:8; n+1 <= len P by A34,NAT_1:13; then A60: e1 <> e2 by A39,A59,GLIB_001:138; A61: now n2 < n - 0 by XREAL_1:15; hence P.n2 <> v by A31,A32,A33,GLIB_001:def 28; end; A62: not e1 DJoins P.n2,v,G or not e1 DJoins v,P.n2,G by A61; A63: n2 < len P - 0 by A31,XREAL_1:15; then A64: e1 Joins P.n2,P.(n2+2),G by GLIB_001:def 3; A65: e2 Joins v,P.(n+2),G by A32,A34,GLIB_001:def 3; now per cases by A32,A64,A65; suppose A66: e1 DJoins P.n2,v,G & e2 DJoins v,P.(n+2),G; set XIN = (EL|v.edgesIn()) +* (e1.-->(EL.e1 + T)); A67: e1 in v.edgesIn() by A66,GLIB_000:57; A68: dom (e1.-->(EL.e1+T)) = {e1} by FUNCOP_1:13; then A69: dom XIN = dom (EL|v.edgesIn()) \/ {e1} by FUNCT_4:def 1 .= v.edgesIn() \/ {e1} by PARTFUN1:def 2 .= v.edgesIn() by A67,ZFMISC_1:40; then reconsider XIN as Rbag of v.edgesIn() by PARTFUN1:def 2 ,RELAT_1:def 18; A70: now let e be object; assume e in dom (EL2|v.edgesIn()); then A71: e in v.edgesIn(); then A72: (the_Target_of G).e = v by GLIB_000:56; now per cases; suppose A73: e = e1; then e in dom (e1.-->(EL.e1+T)) by A68,TARSKI:def 1; hence XIN.e = (e1.-->(EL.e1+T)).e1 by A73,FUNCT_4:13 .= EL.e1 + T by FUNCOP_1:72 .= EL2.e by A4,A63,A40,A66,A73,Def17; end; suppose A74: e <> e1; A75: now assume e in P.edges(); then consider v1,v2 being Vertex of G,m being odd Element of NAT such that A76: m+2 <= len P and A77: v1 = P.m and A78: e = P.(m+1) and A79: v2=P.(m+2) and A80: e Joins v1,v2,G by GLIB_001:103; A81: m+2-2 < len P - 0 by A76,XREAL_1:15; now per cases by A72,A80; suppose A82: v = v1; now per cases by XXREAL_0:1; suppose m < n; hence contradiction by A31,A32,A33,A77,A82, GLIB_001:def 28; end; suppose A83: m = n; A84: n+2-2 < n+2-0 by XREAL_1:15; A85: n+2 <= len P by A34,GLIB_001:1; P.(n+2) = P.n by A32,A66,A72,A78,A83; hence contradiction by A35,A84,A85,GLIB_001:def 28; end; suppose n < m; hence contradiction by A32,A77,A81,A82, GLIB_001:def 28; end; end; hence contradiction; end; suppose A86: v = v2; now per cases by XXREAL_0:1; suppose m+2 < n; hence contradiction by A31,A32,A33,A79,A86, GLIB_001:def 28; end; suppose m+2 = n; hence contradiction by A74,A78; end; suppose n < m+2; hence contradiction by A32,A35,A76,A79,A86, GLIB_001:def 28; end; end; hence contradiction; end; end; hence contradiction; end; not e in dom (e1.-->(EL.e1+T)) by A74,TARSKI:def 1; then XIN.e = (EL|v.edgesIn()).e by FUNCT_4:11 .= EL.e by A71,FUNCT_1:49; hence EL2.e = XIN.e by A4,A71,A75,Def17; end; end; hence (EL2|v.edgesIn()).e = XIN.e by A71,FUNCT_1:49; end; dom (EL2|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2; then A87: Sum (EL2|v.edgesIn())=Sum XIN by A69,A70,FUNCT_1:2; A88: dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2; set XOUT= (EL|v.edgesOut())+* (e2.-->(EL.e2 + T)); A89: e2 in v.edgesOut() by A66,GLIB_000:59; A90: dom (e2.-->(EL.e2+T)) = {e2} by FUNCOP_1:13; then A91: dom XOUT = dom (EL|v.edgesOut())\/{e2} by FUNCT_4:def 1 .= v.edgesOut() \/ {e2} by PARTFUN1:def 2 .= v.edgesOut() by A89,ZFMISC_1:40; then reconsider XOUT as Rbag of v.edgesOut() by PARTFUN1:def 2 ,RELAT_1:def 18; A92: now let e be object; assume e in dom (EL2|v.edgesOut()); then A93: e in v.edgesOut(); then A94: (the_Source_of G).e = v by GLIB_000:58; now per cases; suppose A95: e = e2; then e in dom (e2.-->(EL.e2+T)) by A90,TARSKI:def 1; hence XOUT.e = (e2.-->(EL.e2+T)).e2 by A95,FUNCT_4:13 .= EL.e2 + T by FUNCOP_1:72 .= EL2.e by A4,A32,A34,A66,A95,Def17; end; suppose A96: e <> e2; A97: now assume e in P.edges(); then consider v1,v2 being Vertex of G,m being odd Element of NAT such that A98: m+2 <= len P and A99: v1 = P.m and A100: e = P.(m+1) and A101: v2=P.(m+2) and A102: e Joins v1,v2,G by GLIB_001:103; A103: m+2-2 < len P - 0 by A98,XREAL_1:15; now per cases by A94,A102; suppose A104: v = v1; now per cases by XXREAL_0:1; suppose m < n; hence contradiction by A31,A32,A33,A99,A104, GLIB_001:def 28; end; suppose m = n; hence contradiction by A96,A100; end; suppose n < m; hence contradiction by A32,A99,A103,A104, GLIB_001:def 28; end; end; hence contradiction; end; suppose A105: v = v2; now per cases by XXREAL_0:1; suppose m+2 < n; hence contradiction by A31,A32,A33,A101,A105, GLIB_001:def 28; end; suppose A106: m+2 = n; A107: n2 < n - 0 by XREAL_1:15; P.n2 = P.n by A32,A66,A94,A100,A106; hence contradiction by A31,A33,A107,GLIB_001:def 28 ; end; suppose n < m+2; hence contradiction by A32,A35,A98,A101,A105, GLIB_001:def 28; end; end; hence contradiction; end; end; hence contradiction; end; not e in dom (e2.-->(EL.e2+T)) by A96,TARSKI:def 1; then XOUT.e = (EL|v.edgesOut()).e by FUNCT_4:11 .= EL.e by A93,FUNCT_1:49; hence EL2.e = XOUT.e by A4,A93,A97,Def17; end; end; hence (EL2|v.edgesOut()).e = XOUT.e by A93,FUNCT_1:49; end; Sum XIN = Sum (EL|v.edgesIn()) + (T + EL.e1) - (EL|v .edgesIn()).e1 by GLIB_004:9 .= Sum (EL|v.edgesOut()) + T + EL.e1 - EL.e1 by A30,A67, FUNCT_1:49 .= Sum (EL|v.edgesOut()) + T + EL.e2 - EL.e2 .= Sum (EL|v.edgesOut()) + (T + EL.e2) - (EL|v.edgesOut()).e2 by A89,FUNCT_1:49 .= Sum XOUT by GLIB_004:9; hence Sum (EL2 | v.edgesIn()) = Sum (EL2 | v.edgesOut()) by A91,A87 ,A88,A92,FUNCT_1:2; end; suppose A108: e1 DJoins P.n2,v,G & e2 DJoins P.(n+2),v,G; A109: dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2; A110: now let e be object; assume A111: e in dom (EL2|v.edgesOut()); then A112: (EL|v.edgesOut()).e = EL.e by FUNCT_1:49; A113: e in v.edgesOut() by A111; then A114: (the_Source_of G).e = v by GLIB_000:58; then A115: e <> e2 by A36,A108; e <> e1 by A61,A108,A114; then A116: not e in P.edges() by A41,A113,A115; (EL2|v.edgesOut()).e = EL2.e by A111,FUNCT_1:49; hence (EL2|v.edgesOut()).e = (EL|v.edgesOut()).e by A4,A113,A112 ,A116,Def17; end; dom (EL|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2; then A117: EL2|v.edgesOut() = EL|v.edgesOut() by A109,A110,FUNCT_1:2; set XIN1 = (EL|v.edgesIn())+*(e1.-->(EL.e1+T)); set XIN2 = XIN1 +* (e2.-->(EL.e2-T)); A118: dom (EL2|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2; A119: e2 in v.edgesIn() by A108,GLIB_000:57; A120: e1 in v.edgesIn() by A108,GLIB_000:57; A121: EL2.e1 = EL.e1 + T by A4,A63,A40,A108,Def17; A122: dom (e2.-->(EL.e2-T)) = {e2} by FUNCOP_1:13; A123: dom XIN1 = dom (EL|v.edgesIn()) \/ dom (e1.-->(EL.e1+T)) by FUNCT_4:def 1 .= dom (EL|v.edgesIn()) \/ {e1} by FUNCOP_1:13 .= v.edgesIn() \/ {e1} by PARTFUN1:def 2 .= v.edgesIn() by A120,ZFMISC_1:40; then reconsider XIN1 as Rbag of v.edgesIn() by PARTFUN1:def 2 ,RELAT_1:def 18; A124: dom XIN2 = dom XIN1 \/ dom (e2.-->(EL.e2-T)) by FUNCT_4:def 1 .= v.edgesIn() \/ {e2} by A123,FUNCOP_1:13 .= v.edgesIn() by A119,ZFMISC_1:40; then reconsider XIN2 as Rbag of v.edgesIn() by PARTFUN1:def 2 ,RELAT_1:def 18; A125: dom (e1.-->(EL.e1+T)) = {e1} by FUNCOP_1:13; A126: EL2.e2 = EL.e2 - T by A4,A32,A34,A54,A108,Def17; A127: now let e be object; assume A128: e in dom (EL2|v.edgesIn()); then A129: e in v.edgesIn(); A130: (EL2|v.edgesIn()).e = EL2.e by A128,FUNCT_1:49; now per cases; suppose A131: e = e1; then A132: e in dom (e1.-->(EL.e1+T)) by A125,TARSKI:def 1; not e in dom (e2.-->(EL.e2-T)) by A60,A131,TARSKI:def 1; then XIN2.e = XIN1.e by FUNCT_4:11 .= (e1.-->(EL.e1+T)).e by A132,FUNCT_4:13 .= EL2.e by A121,A131,FUNCOP_1:72; hence (EL2|v.edgesIn()).e = XIN2.e by A128,FUNCT_1:49; end; suppose A133: e = e2; then e in dom (e2.-->(EL.e2-T)) by A122,TARSKI:def 1; then XIN2.e = (e2.-->(EL.e2-T)).e2 by A133,FUNCT_4:13 .= EL2.e by A126,A133,FUNCOP_1:72; hence (EL2|v.edgesIn()).e = XIN2.e by A128,FUNCT_1:49; end; suppose A134: e <> e1 & e <> e2; then A135: not e in dom (e1.-->(EL.e1+T)) by TARSKI:def 1; A136: not e in P.edges() by A41,A129,A134; not e in dom (e2.-->(EL.e2-T)) by A134,TARSKI:def 1; then XIN2.e = XIN1.e by FUNCT_4:11 .= (EL|v.edgesIn()).e by A135,FUNCT_4:11 .= EL.e by A129,FUNCT_1:49; hence (EL2|v.edgesIn()).e = XIN2.e by A4,A129,A130,A136,Def17 ; end; end; hence (EL2|v.edgesIn()).e = XIN2.e; end; not e2 in dom (e1.-->(EL.e1+T)) by A60,TARSKI:def 1; then XIN1.e2 = (EL|v.edgesIn()).e2 by FUNCT_4:11 .= EL.e2 by A119,FUNCT_1:49; then Sum (EL2|v.edgesIn()) = Sum XIN1 + (EL.e2-T) - EL.e2 by A124 ,A118,A127,FUNCT_1:2,GLIB_004:9 .= Sum XIN1 - (EL.e2 - (EL.e2 - T)) .= Sum (EL|v.edgesIn())+(EL.e1+T)-(EL|v.edgesIn()).e1-T by GLIB_004:9 .= Sum (EL|v.edgesIn())+T+EL.e1-EL.e1-T by A120,FUNCT_1:49 .= Sum (EL|v.edgesIn()); hence Sum (EL2|v.edgesIn()) = Sum (EL2|v.edgesOut()) by A2,A28,A29,A117; end; suppose A137: e1 DJoins v,P.n2,G & e2 DJoins v,P.(n+2),G; A138: dom (EL2|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2; A139: now let e be object; assume A140: e in dom (EL2|v.edgesIn()); then A141: (EL|v.edgesIn()).e = EL.e by FUNCT_1:49; A142: e in v.edgesIn() by A140; then A143: (the_Target_of G).e = v by GLIB_000:56; then A144: e <> e2 by A36,A137; e <> e1 by A61,A137,A143; then A145: not e in P.edges() by A41,A142,A144; (EL2|v.edgesIn()).e = EL2.e by A140,FUNCT_1:49; hence (EL2|v.edgesIn()).e = (EL|v.edgesIn()).e by A4,A142,A141 ,A145,Def17; end; set XOUT1 = (EL|v.edgesOut())+*(e1.-->(EL.e1-T)); set XOUT2 = XOUT1 +* (e2.-->(EL.e2+T)); A146: dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2; A147: e2 in v.edgesOut() by A137,GLIB_000:59; A148: dom (EL|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2; A149: e1 in v.edgesOut() by A137,GLIB_000:59; A150: EL2.e2 = EL.e2 + T by A4,A32,A34,A137,Def17; A151: dom (e2.-->(EL.e2+T)) = {e2} by FUNCOP_1:13; A152: dom XOUT1 = dom (EL|v.edgesOut()) \/ dom (e1.-->(EL.e1-T)) by FUNCT_4:def 1 .= dom (EL|v.edgesOut()) \/ {e1} by FUNCOP_1:13 .= v.edgesOut() \/ {e1} by PARTFUN1:def 2 .= v.edgesOut() by A149,ZFMISC_1:40; then reconsider XOUT1 as Rbag of v.edgesOut() by PARTFUN1:def 2 ,RELAT_1:def 18; A153: dom XOUT2 = dom XOUT1\/dom (e2.-->(EL.e2+T)) by FUNCT_4:def 1 .= v.edgesOut() \/ {e2} by A152,FUNCOP_1:13 .= v.edgesOut() by A147,ZFMISC_1:40; then reconsider XOUT2 as Rbag of v.edgesOut() by PARTFUN1:def 2 ,RELAT_1:def 18; A154: dom (e1.-->(EL.e1-T)) = {e1} by FUNCOP_1:13; A155: EL2.e1 = EL.e1 - T by A4,A63,A40,A62,A137,Def17; A156: now let e be object; assume A157: e in dom (EL2|v.edgesOut()); then A158: e in v.edgesOut(); A159: (EL2|v.edgesOut()).e = EL2.e by A157,FUNCT_1:49; now per cases; suppose A160: e = e1; then A161: e in dom (e1.-->(EL.e1-T)) by A154,TARSKI:def 1; not e in dom (e2.-->(EL.e2+T)) by A60,A160,TARSKI:def 1; then XOUT2.e = XOUT1.e by FUNCT_4:11 .= (e1.-->(EL.e1-T)).e by A161,FUNCT_4:13 .= EL2.e by A155,A160,FUNCOP_1:72; hence (EL2|v.edgesOut()).e=XOUT2.e by A157,FUNCT_1:49; end; suppose A162: e = e2; then e in dom (e2.-->(EL.e2+T)) by A151,TARSKI:def 1; then XOUT2.e = (e2.-->(EL.e2+T)).e by FUNCT_4:13 .= EL2.e by A150,A162,FUNCOP_1:72; hence (EL2|v.edgesOut()).e=XOUT2.e by A157,FUNCT_1:49; end; suppose A163: e <> e1 & e <> e2; then A164: not e in dom (e1.-->(EL.e1-T)) by TARSKI:def 1; A165: not e in P.edges() by A41,A158,A163; not e in dom (e2.-->(EL.e2+T)) by A163,TARSKI:def 1; then XOUT2.e = XOUT1.e by FUNCT_4:11 .= (EL|v.edgesOut()).e by A164,FUNCT_4:11 .= EL.e by A158,FUNCT_1:49; hence (EL2|v.edgesOut()).e = XOUT2.e by A4,A158,A159,A165 ,Def17; end; end; hence (EL2|v.edgesOut()).e = XOUT2.e; end; not e2 in dom (e1.-->(EL.e1-T)) by A60,TARSKI:def 1; then XOUT1.e2 = (EL|v.edgesOut()).e2 by FUNCT_4:11 .= EL.e2 by A147,FUNCT_1:49; then Sum (EL2|v.edgesOut()) = Sum XOUT1 + (EL.e2+T) - EL.e2 by A153 ,A146,A156,FUNCT_1:2,GLIB_004:9 .= Sum XOUT1 - EL.e2 + EL.e2 + T .= Sum (EL|v.edgesOut()) + (EL.e1 - T) - (EL|v.edgesOut()).e1 + T by GLIB_004:9 .= Sum (EL|v.edgesOut()) + EL.e1 - T - EL.e1 + T by A149, FUNCT_1:49 .= Sum (EL|v.edgesOut()); hence Sum (EL2|v.edgesIn()) = Sum (EL2|v.edgesOut()) by A30,A138 ,A148,A139,FUNCT_1:2; end; suppose A166: e1 DJoins v,P.n2,G & e2 DJoins P.(n+2),v,G; set XIN = (EL|v.edgesIn())+*(e2.-->(EL.e2-T)); A167: e2 in v.edgesIn() by A166,GLIB_000:57; A168: dom (e2.-->(EL.e2-T)) = {e2} by FUNCOP_1:13; then A169: dom XIN = dom (EL|v.edgesIn()) \/ {e2} by FUNCT_4:def 1 .= v.edgesIn() \/ {e2} by PARTFUN1:def 2 .= v.edgesIn() by A167,ZFMISC_1:40; then reconsider XIN as Rbag of v.edgesIn() by PARTFUN1:def 2 ,RELAT_1:def 18; A170: EL2.e2 = EL.e2 - T by A4,A32,A34,A54,A166,Def17; A171: now let e be object; assume e in dom (EL2|v.edgesIn()); then A172: e in v.edgesIn(); then A173: (the_Target_of G).e = v by GLIB_000:56; now per cases; suppose A174: e = e2; then e in dom (e2.-->(EL.e2-T)) by A168,TARSKI:def 1; hence XIN.e = (e2.-->(EL.e2-T)).e2 by A174,FUNCT_4:13 .= EL2.e by A170,A174,FUNCOP_1:72; end; suppose A175: e <> e2; then not e in dom (e2.-->(EL.e2-T)) by TARSKI:def 1; then A176: XIN.e = (EL|v.edgesIn()).e by FUNCT_4:11 .= EL.e by A172,FUNCT_1:49; e <> e1 by A61,A166,A173; then not e in P.edges() by A41,A172,A175; hence EL2.e = XIN.e by A4,A172,A176,Def17; end; end; hence XIN.e = (EL2|v.edgesIn()).e by A172,FUNCT_1:49; end; dom (EL2|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2; then A177: Sum (EL2|v.edgesIn()) = Sum (EL|v.edgesIn()) + (EL.e2-T) - ( EL|v.edgesIn()).e2 by A169,A171,FUNCT_1:2,GLIB_004:9 .= Sum (EL|v.edgesIn()) + EL.e2 - T - EL.e2 by A167,FUNCT_1:49 .= Sum (EL|v.edgesIn()) - T; set XOUT= (EL|v.edgesOut())+*(e1.-->(EL.e1-T)); A178: e1 in v.edgesOut() by A166,GLIB_000:59; A179: dom (e1.-->(EL.e1-T)) = {e1} by FUNCOP_1:13; then A180: dom XOUT = dom (EL|v.edgesOut())\/{e1} by FUNCT_4:def 1 .= v.edgesOut() \/ {e1} by PARTFUN1:def 2 .= v.edgesOut() by A178,ZFMISC_1:40; then reconsider XOUT as Rbag of v.edgesOut() by PARTFUN1:def 2 ,RELAT_1:def 18; A181: EL2.e1 = EL.e1 - T by A4,A63,A40,A62,A166,Def17; A182: now let e be object; assume e in dom (EL2|v.edgesOut()); then A183: e in v.edgesOut(); then A184: (the_Source_of G).e = v by GLIB_000:58; now per cases; suppose A185: e = e1; then e in dom (e1.-->(EL.e1-T)) by A179,TARSKI:def 1; hence XOUT.e = (e1.-->(EL.e1-T)).e1 by A185,FUNCT_4:13 .= EL2.e by A181,A185,FUNCOP_1:72; end; suppose A186: e <> e1; then not e in dom (e1.-->(EL.e1-T)) by TARSKI:def 1; then A187: XOUT.e = (EL|v.edgesOut()).e by FUNCT_4:11 .= EL.e by A183,FUNCT_1:49; e <> e2 by A36,A166,A184; then not e in P.edges() by A41,A183,A186; hence EL2.e = XOUT.e by A4,A183,A187,Def17; end; end; hence XOUT.e = (EL2|v.edgesOut()).e by A183,FUNCT_1:49; end; dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2; then Sum (EL2|v.edgesOut()) = Sum (EL|v.edgesOut()) + (EL.e1-T)-( EL|v.edgesOut()).e1 by A180,A182,FUNCT_1:2,GLIB_004:9 .= Sum (EL|v.edgesOut()) + EL.e1 - T - EL.e1 by A178,FUNCT_1:49 .= Sum (EL|v.edgesIn()) - T by A30; hence Sum (EL2 | v.edgesIn()) = Sum (EL2 | v.edgesOut()) by A177; end; end; hence Sum (EL2 | v.edgesIn()) = Sum (EL2 | v.edgesOut()); end; suppose A188: not v in P.vertices(); A189: dom (EL|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2; A190: now let e be object; assume A191: e in dom (EL|v.edgesOut()); then A192: (EL2|v.edgesOut()).e = EL2.e by FUNCT_1:49; A193: e in v.edgesOut() by A191; A194: now consider x being set such that A195: e DJoins v,x,G by A193,GLIB_000:59; assume A196: e in P.edges(); e Joins v,x,G by A195; hence contradiction by A188,A196,GLIB_001:105; end; (EL|v.edgesOut()).e = EL.e by A191,FUNCT_1:49; hence (EL|v.edgesOut()).e = (EL2|v.edgesOut()).e by A4,A193,A192,A194 ,Def17; end; A197: dom (EL|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2; A198: now let e be object; assume A199: e in dom (EL|v.edgesIn()); then A200: (EL2|v.edgesIn()).e = EL2.e by FUNCT_1:49; A201: now consider x being set such that A202: e DJoins x,v,G by A199,GLIB_000:57; assume A203: e in P.edges(); e Joins x,v,G by A202; hence contradiction by A188,A203,GLIB_001:105; end; (EL|v.edgesIn()).e = EL.e by A199,FUNCT_1:49; hence (EL|v.edgesIn()).e = (EL2|v.edgesIn()).e by A4,A197,A199,A200 ,A201,Def17; end; dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2; then A204: EL | v.edgesOut() = EL2 | v.edgesOut() by A189,A190,FUNCT_1:2; dom (EL|v.edgesIn()) = dom (EL2|v.edgesIn()) by A197,PARTFUN1:def 2; hence Sum (EL2|v.edgesIn()) = Sum (EL|v.edgesIn()) by A198,FUNCT_1:2 .= Sum (EL2|v.edgesOut()) by A2,A28,A29,A204; end; end; hence Sum (EL2 | v.edgesIn()) = Sum (EL2 | v.edgesOut()); end; hence thesis; end; theorem Th15: 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) proof let G be finite natural-weighted WGraph, EL being FF:ELabeling of G, source, sink be set, P be Path of G such that A1: source <> sink and A2: P is_Walk_from source,sink and A3: P is_augmenting_wrt EL; A4: P.last() = sink by A2,GLIB_001:def 23; P.first() = source by A2,GLIB_001:def 23; then P is non trivial by A1,A4,GLIB_001:127; then 3 <= len P by GLIB_001:125; then reconsider lenP2g = len P - 2*1 as odd Element of NAT by INT_1:5 ,XXREAL_0:2; set e1 = P.(lenP2g+1); set EI1 = EL|G.edgesInto({sink}), EO1 = EL|G.edgesOutOf({sink}); set EL2 = FF:PushFlow(EL,P), T = P.tolerance(EL); A5: P.(len P) = sink by A2,GLIB_001:17; A6: lenP2g < len P - 0 by XREAL_1:15; then A7: e1 Joins P.lenP2g, P.(lenP2g+2), G by GLIB_001:def 3; then A8: e1 in the_Edges_of G; now per cases; suppose A9: e1 DJoins P.lenP2g, P.(lenP2g+2), G; then (the_Target_of G).e1 = P.(lenP2g+2) .= sink by A2,GLIB_001:17; then (the_Target_of G).e1 in {sink} by TARSKI:def 1; then A10: e1 in G.edgesInto({sink}) by A8,GLIB_000:def 26; set EI2 = EI1+*(e1.-->(EI1.e1 + T)); A11: dom (EL2|G.edgesInto({sink})) = G.edgesInto({sink}) by PARTFUN1:def 2; A12: dom EI2 = dom EI1 \/ dom (e1.-->(EI1.e1 + T)) by FUNCT_4:def 1 .= dom EI1 \/ {e1} by FUNCOP_1:13 .= G.edgesInto({sink}) \/ {e1} by PARTFUN1:def 2 .= G.edgesInto({sink}) by A10,ZFMISC_1:40; then reconsider EI2 as Rbag of G.edgesInto({sink}) by PARTFUN1:def 2 ,RELAT_1:def 18; A13: EL2.e1 = EL.e1 + T by A3,A6,A9,Def17; now let e be object; assume A14: e in dom (EL2|G.edgesInto({sink})); then A15: e in G.edgesInto({sink}); A16: (EL2|G.edgesInto({sink})).e = EL2.e by A14,FUNCT_1:49; (the_Target_of G).e in {sink} by A15,GLIB_000:def 26; then A17: (the_Target_of G).e = sink by TARSKI:def 1; now per cases; suppose A18: e = e1; then e in {e1} by TARSKI:def 1; then e in dom (e1.-->(EI1.e1+T)) by FUNCOP_1:13; then EI2.e = (e1.-->(EI1.e1+T)).e1 by A18,FUNCT_4:13 .= EI1.e1 + T by FUNCOP_1:72 .= EL2.e1 by A13,A15,A18,FUNCT_1:49; hence (EL2|G.edgesInto({sink})).e = EI2.e by A14,A18,FUNCT_1:49; end; suppose A19: e <> e1; A20: now assume e in P.edges(); then consider v1,v2 being Vertex of G,m being odd Element of NAT such that A21: m+2 <= len P and A22: v1 = P.m and A23: e = P.(m+1) and A24: v2 = P.(m+2) and A25: e Joins v1,v2,G by GLIB_001:103; now per cases by A17,A25; suppose A26: v1 = sink; A27: m+2-2 < len P - 0 by A21,XREAL_1:15; P.m = P.(len P) by A2,A22,A26,GLIB_001:17; then m = 1 by A27,GLIB_001:def 28; hence contradiction by A1,A2,A22,A26,GLIB_001:17; end; suppose v2 = sink; then A28: P.(m+2) = P.(len P) by A2,A24,GLIB_001:17; now assume m+2 < len P; then m+2 = 1 by A28,GLIB_001:def 28; then m = 1-2; hence contradiction by ABIAN:12; end; then m + 2 = len P by A21,XXREAL_0:1; hence contradiction by A19,A23; end; end; hence contradiction; end; not e in {e1} by A19,TARSKI:def 1; then not e in dom (e1.-->(EI1.e1+T)); then EI2.e = EI1.e by FUNCT_4:11 .= EL.e by A15,FUNCT_1:49; hence (EL2|G.edgesInto({sink})).e = EI2.e by A3,A15,A16,A20,Def17; end; end; hence (EL2|G.edgesInto({sink})).e = EI2.e; end; then A29: Sum (EL2|G.edgesInto({sink})) = Sum EI1 + (T + EI1.e1) - EI1.e1 by A12 ,A11,FUNCT_1:2,GLIB_004:9 .= Sum EI1 + T; A30: dom (EL2|G.edgesOutOf({sink})) = G.edgesOutOf({sink}) by PARTFUN1:def 2; A31: now let e be object; assume A32: e in dom (EL2|G.edgesOutOf({sink})); then A33: e in G.edgesOutOf({sink}); then (the_Source_of G).e in {sink} by GLIB_000:def 27; then A34: (the_Source_of G).e = sink by TARSKI:def 1; now assume e in P.edges(); then consider v1,v2 being Vertex of G, m being odd Element of NAT such that A35: m+2 <= len P and A36: v1 = P.m and A37: e = P.(m+1) and A38: v2 = P.(m+2) and A39: e Joins v1,v2,G by GLIB_001:103; now per cases by A34,A39; suppose A40: v1 = sink; A41: m+2-2 < len P - 0 by A35,XREAL_1:15; P.m = P.(len P) by A2,A36,A40,GLIB_001:17; then m = 1 by A41,GLIB_001:def 28; hence contradiction by A1,A2,A36,A40,GLIB_001:17; end; suppose v2 = sink; then A42: P.(m+2) = P.(len P) by A2,A38,GLIB_001:17; now assume m+2 < len P; then m+2 = 1 by A42,GLIB_001:def 28; then 1 <= 1-2 by ABIAN:12; hence contradiction; end; then m + 2 = len P by A35,XXREAL_0:1; then A43: P.lenP2g = sink by A9,A34,A37; then lenP2g = 1 by A6,A5,GLIB_001:def 28; hence contradiction by A1,A2,A43,GLIB_001:17; end; end; hence contradiction; end; then EL2.e = EL.e by A3,A33,Def17 .= EO1.e by A33,FUNCT_1:49; hence (EL2|G.edgesOutOf({sink})).e = EO1.e by A32,FUNCT_1:49; end; dom EO1 = G.edgesOutOf({sink}) by PARTFUN1:def 2; hence EL2.flow(source,sink) = Sum EI1 + T - Sum EO1 by A29,A30,A31, FUNCT_1:2 .= Sum EI1 - Sum EO1 + T .= EL.flow(source,sink) + T; end; suppose A44: not e1 DJoins P.lenP2g, P.(lenP2g+2), G; then A45: e1 DJoins P.(lenP2g+2),P.lenP2g,G by A7; then (the_Source_of G).e1 = P.(lenP2g+2) .= sink by A2,GLIB_001:17; then (the_Source_of G).e1 in {sink} by TARSKI:def 1; then A46: e1 in G.edgesOutOf({sink}) by A8,GLIB_000:def 27; set EO2 = EO1+*(e1.-->(EO1.e1-T)); A47: dom (EL2|G.edgesOutOf({sink})) = G.edgesOutOf({sink}) by PARTFUN1:def 2; A48: dom EO2 = dom EO1 \/ dom (e1.-->(EO1.e1 - T)) by FUNCT_4:def 1 .= dom EO1 \/ {e1} by FUNCOP_1:13 .= G.edgesOutOf({sink}) \/ {e1} by PARTFUN1:def 2 .= G.edgesOutOf({sink}) by A46,ZFMISC_1:40; then reconsider EO2 as Rbag of G.edgesOutOf({sink}) by PARTFUN1:def 2 ,RELAT_1:def 18; A49: EL2.e1 = EL.e1 - T by A3,A6,A44,Def17; now let e be object; assume A50: e in dom (EL2|G.edgesOutOf({sink})); then A51: e in G.edgesOutOf({sink}); A52: (EL2|G.edgesOutOf({sink})).e = EL2.e by A50,FUNCT_1:49; (the_Source_of G).e in {sink} by A51,GLIB_000:def 27; then A53: (the_Source_of G).e = sink by TARSKI:def 1; now per cases; suppose A54: e = e1; then e in {e1} by TARSKI:def 1; then e in dom (e1.-->(EO1.e1-T)) by FUNCOP_1:13; then EO2.e = (e1.-->(EO1.e1-T)).e1 by A54,FUNCT_4:13 .= EO1.e1 - T by FUNCOP_1:72 .= EL2.e by A49,A51,A54,FUNCT_1:49; hence (EL2|G.edgesOutOf({sink})).e = EO2.e by A50,FUNCT_1:49; end; suppose A55: e <> e1; A56: now assume e in P.edges(); then consider v1,v2 being Vertex of G, m being odd Element of NAT such that A57: m+2 <= len P and A58: v1 = P.m and A59: e = P.(m+1) and A60: v2 = P.(m+2) and A61: e Joins v1,v2,G by GLIB_001:103; now per cases by A53,A61; suppose A62: v1 = sink; A63: m+2-2 < len P - 0 by A57,XREAL_1:15; P.m = P.(len P) by A2,A58,A62,GLIB_001:17; then m = 1 by A63,GLIB_001:def 28; hence contradiction by A1,A2,A58,A62,GLIB_001:17; end; suppose v2 = sink; then A64: P.(m+2) = P.(len P) by A2,A60,GLIB_001:17; now assume m+2 < len P; then m+2 = 1 by A64,GLIB_001:def 28; then 1 <= 1-2 by ABIAN:12; hence contradiction; end; then m + 2 = len P by A57,XXREAL_0:1; hence contradiction by A55,A59; end; end; hence contradiction; end; not e in {e1} by A55,TARSKI:def 1; then not e in dom (e1.-->(EO1.e1-T)); then EO2.e = EO1.e by FUNCT_4:11 .= EL.e by A51,FUNCT_1:49; hence (EL2|G.edgesOutOf({sink})).e = EO2.e by A3,A51,A52,A56,Def17; end; end; hence (EL2|G.edgesOutOf({sink})).e = EO2.e; end; then A65: Sum (EL2|G.edgesOutOf({sink})) = Sum EO1 + (EO1.e1 - T) - EO1.e1 by A48,A47,FUNCT_1:2,GLIB_004:9 .= Sum EO1 - T; A66: dom (EL2|G.edgesInto({sink})) = G.edgesInto({sink}) by PARTFUN1:def 2; A67: now let e be object; assume A68: e in dom (EL2|G.edgesInto({sink})); then A69: e in G.edgesInto({sink}); then (the_Target_of G).e in {sink} by GLIB_000:def 26; then A70: (the_Target_of G).e = sink by TARSKI:def 1; now assume e in P.edges(); then consider v1,v2 being Vertex of G, m being odd Element of NAT such that A71: m+2 <= len P and A72: v1 = P.m and A73: e = P.(m+1) and A74: v2 = P.(m+2) and A75: e Joins v1,v2,G by GLIB_001:103; now per cases by A70,A75; suppose A76: v1 = sink; A77: m+2-2 < len P - 0 by A71,XREAL_1:15; P.m = P.(len P) by A2,A72,A76,GLIB_001:17; then m = 1 by A77,GLIB_001:def 28; hence contradiction by A1,A2,A72,A76,GLIB_001:17; end; suppose v2 = sink; then A78: P.(m+2) = P.(len P) by A2,A74,GLIB_001:17; now assume m+2 < len P; then m+2 = 1 by A78,GLIB_001:def 28; then 1 <= 1-2 by ABIAN:12; hence contradiction; end; then m + 2 = len P by A71,XXREAL_0:1; then A79: P.lenP2g = sink by A45,A70,A73; then lenP2g = 1 by A6,A5,GLIB_001:def 28; hence contradiction by A1,A2,A79,GLIB_001:17; end; end; hence contradiction; end; then EL2.e = EL.e by A3,A69,Def17 .= EI1.e by A69,FUNCT_1:49; hence (EL2|G.edgesInto({sink})).e = EI1.e by A68,FUNCT_1:49; end; dom EI1 = G.edgesInto({sink}) by PARTFUN1:def 2; hence EL2.flow(source,sink) = Sum EI1 - (Sum EO1 - T) by A65,A66,A67, FUNCT_1:2 .= Sum EI1 - Sum EO1 + T .= EL.flow(source,sink) + T; end; end; hence thesis; end; theorem Th16: 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 proof let G be finite natural-weighted WGraph, source,sink be Vertex of G, n be Nat; set CS = FF:CompSeq(G,source,sink); defpred P[Nat] means (CS.$1) has_valid_flow_from source,sink; now set G0 = CS.0; A1: G0 = the_Edges_of G --> 0 by Def20; hence for e being set st e in the_Edges_of G holds 0 <= G0.e & G0.e <= ( the_Weight_of G).e by FUNCOP_1:7; let v be Vertex of G; set B1 = EmptyBag v.edgesIn(), B2 = EmptyBag v.edgesOut(); set E1 = (G0|v.edgesIn()), E2 = (G0|v.edgesOut()); now let e be set; assume A2: e in v.edgesOut(); then E2.e = G0.e by FUNCT_1:49 .= 0 by A1,A2,FUNCOP_1:7; hence B2.e = E2.e by PBOOLE:5; end; then A3: Sum E2 = Sum B2 by GLIB_004:6 .= 0 by UPROOTS:11; assume that v <> source and v <> sink; now let e be set; assume A4: e in v.edgesIn(); then E1.e = G0.e by FUNCT_1:49 .= 0 by A1,A4,FUNCOP_1:7; hence B1.e = E1.e by PBOOLE:5; end; then Sum E1 = Sum B1 by GLIB_004:6 .= 0 by UPROOTS:11; hence Sum E1 = Sum E2 by A3; end; then A5: P[ 0 ] by Def2; assume A6: source <> sink; now let n be Nat; set Gn = CS.n, Gn1 = CS.(n+1); assume A7: Gn has_valid_flow_from source,sink; A8: Gn1 = FF:Step(Gn,source,sink) by Def20; now per cases; suppose A9: sink in dom AP:FindAugPath(Gn,source); set P = AP:GetAugPath(Gn,source,sink); A10: P is_Walk_from source,sink by A9,Def14; A11: P is_augmenting_wrt Gn by A9,Def14; Gn1 = FF:PushFlow(Gn, P) by A8,A9,Def18; hence P[n+1] by A6,A7,A10,A11,Th14; end; suppose not sink in dom AP:FindAugPath(Gn,source); hence P[n+1] by A7,A8,Def18; end; end; hence P[n+1]; end; then A12: for n being Nat st P[n] holds P[n+1]; for n being Nat holds P[n] from NAT_1:sch 2(A5,A12); hence thesis; end; theorem Th17: for G being finite natural-weighted WGraph,source,sink being Vertex of G st source <> sink holds FF:CompSeq(G,source,sink) is halting proof let G be finite natural-weighted WGraph, source, sink be Vertex of G; set CS = FF:CompSeq(G,source,sink); assume A1: source <> sink; now set V = {source}; defpred P[Nat] means $1 <= (CS.$1).flow(source,sink) & (CS.$1) .flow(source,sink) is Element of NAT; A2: source in V by TARSKI:def 1; set W1 = (the_Weight_of G)|G.edgesDBetween(V,the_Vertices_of G \ V); degree W1 = Sum W1; then reconsider N = Sum W1 as Element of NAT; set Gn1 = CS.(N+1); assume A3: for n being Nat holds CS.n <> CS.(n+1); now let n be Nat; set Gn = CS.n, Gn1 = CS.(n+1); assume that A4: n <= Gn.flow(source,sink) and A5: Gn.flow(source,sink) is Element of NAT; reconsider GnF = Gn.flow(source,sink) as Element of NAT by A5; set P = AP:GetAugPath(Gn,source,sink); A6: Gn1 = FF:Step(Gn, source,sink) by Def20; A7: now assume not sink in dom AP:FindAugPath(Gn,source); then Gn1 = Gn by A6,Def18; hence contradiction by A3; end; then A8: P is_augmenting_wrt Gn by Def14; A9: P is_Walk_from source,sink by A7,Def14; then A10: P.last() = sink by GLIB_001:def 23; Gn1 = FF:PushFlow(Gn,AP:GetAugPath(Gn,source,sink)) by A6,A7,Def18; then A11: GnF + P.tolerance(Gn) = Gn1.flow(source,sink) by A1,A8,A9,Th15; then reconsider Gn1F = Gn1.flow(source,sink) as Element of NAT by ORDINAL1:def 12; P.first() = source by A9,GLIB_001:def 23; then 0 < P.tolerance(Gn) by A1,A8,A10,Th13,GLIB_001:127; then GnF + P.tolerance(Gn)-P.tolerance(Gn) < Gn1F-0 by A11,XREAL_1:15; then n < Gn1F by A4,XXREAL_0:2; hence n+1 <= Gn1.flow(source,sink) by NAT_1:13; thus Gn1.flow(source,sink) is Element of NAT by A11,ORDINAL1:def 12; end; then A12: for n being Nat st P[n] holds P[n+1]; now set B1 = EmptyBag G.edgesInto({sink}),B2 = EmptyBag G.edgesOutOf({sink}); set G0 = CS.0; set E1 = G0 | G.edgesInto({sink}), E2 = G0 | G.edgesOutOf({sink}); A13: G0 = the_Edges_of G --> 0 by Def20; now let e be set; assume A14: e in G.edgesInto({sink}); hence E1.e = G0.e by FUNCT_1:49 .= 0 by A13,A14,FUNCOP_1:7 .= B1.e by PBOOLE:5; end; then A15: Sum E1 = Sum B1 by GLIB_004:6 .= 0 by UPROOTS:11; now let e be set; assume A16: e in G.edgesOutOf({sink}); hence E2.e = G0.e by FUNCT_1:49 .= 0 by A13,A16,FUNCOP_1:7 .= B2.e by PBOOLE:5; end; then A17: Sum E2 = Sum B2 by GLIB_004:6 .= 0 by UPROOTS:11; hence G0.flow(source,sink) = 0 qua Nat - 0 by A15; thus G0.flow(source,sink) is Element of NAT by A15,A17; end; then A18: P[ 0 ]; A19: for n being Nat holds P[n] from NAT_1:sch 2(A18,A12); then reconsider Gn1F = Gn1.flow(source,sink) as Element of NAT; Sum W1 + 1 <= Gn1F by A19; then A20: Sum W1 < Gn1.flow(source,sink) by NAT_1:13; not sink in V by A1,TARSKI:def 1; hence contradiction by A2,A20,Th12,Th16; end; hence thesis; end; theorem Th18: 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 proof let G be finite natural-weighted WGraph, EL be FF:ELabeling of G, source, sink be set; assume that A1: EL has_valid_flow_from source,sink and A2: not ex P being Path of G st P is_Walk_from source,sink & P is_augmenting_wrt EL; reconsider src = source as Vertex of G by A1; set CS = AP:CompSeq(EL,src), Gn = AP:FindAugPath(EL,src); set Gn1 = CS.(CS.Lifespan()+1); reconsider V = dom Gn as Subset of the_Vertices_of G; set E1 = G.edgesDBetween(V, the_Vertices_of G \ V); set A1 = EL|E1, B1 = (the_Weight_of G)|E1; set e = the Element of AP:NextBestEdges(Gn); AP:CompSeq(EL,src) is halting by Th6; then A3: Gn1 = Gn by GLIB_000:def 55; A4: Gn1 = AP:Step(Gn) by Def12; A5: now assume A6: AP:NextBestEdges(Gn) <> {}; now per cases by A6,Def9; suppose A7: e is_forward_edge_wrt Gn; then (the_Source_of G).e in V; then A8: Gn = Gn+*((the_Target_of G).e .--> e) by A4,A3,A6,Def10; not (the_Target_of G).e in V by A7; hence contradiction by A8,Lm2; end; suppose e is_backward_edge_wrt Gn; then A9: not (the_Source_of G).e in V; then Gn = Gn+*((the_Source_of G).e .--> e) by A4,A3,A6,Def10; hence contradiction by A9,Lm2; end; end; hence contradiction; end; A10: now let x be set; assume A11: x in E1; then A12: A1.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; then A14: not (the_Target_of G).x in V by XBOOLE_0:def 5; A15: B1.x = (the_Weight_of G).x by A11,FUNCT_1:49; A16: (the_Source_of G).x in V by A13; A17: now assume A1.x < B1.x; then x is_forward_edge_wrt Gn by A11,A12,A15,A16,A14; hence contradiction by A5,Def9; end; A1.x <= B1.x by A1,A11,A12,A15; hence A1.x = B1.x by A17,XXREAL_0:1; end; set E2 = G.edgesDBetween(the_Vertices_of G \ V, V); set A2 = EL|E2, B2 = EmptyBag E2; now let x be set; assume A18: x in E2; then A19: x DSJoins the_Vertices_of G \ V, V, G by GLIB_000:def 31; then A20: (the_Target_of G).x in V; (the_Source_of G).x in the_Vertices_of G \ V by A19; then A21: not (the_Source_of G).x in V by XBOOLE_0:def 5; A22: A2.x = EL.x by A18,FUNCT_1:49; A23: now assume 0 < A2.x; then x is_backward_edge_wrt Gn by A18,A22,A20,A21; hence contradiction by A5,Def9; end; B2 = E2 --> 0 by PBOOLE:def 3; then B2.x = 0 by A18,FUNCOP_1:7; hence A2.x = B2.x by A23; end; then Sum (EL | E2) = Sum B2 by GLIB_004:6; then A24: Sum (EL | E2) = 0 by UPROOTS:11; A25: not sink in dom Gn by A2,Th9; then EL.flow(source,sink) = Sum(EL|E1)-Sum(EL|E2) by A1,Th10,Th11; then EL.flow(source,sink) = Sum ((the_Weight_of G)|E1) by A10,A24,GLIB_004:6; then for X be 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 thesis by A1; end; ::$N Ford/Fulkerson maximum flow algorithm theorem 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 proof let G be finite natural-weighted WGraph, source, sink be Vertex of G; set CS = FF:CompSeq(G,source,sink); set n = CS.Lifespan(), Gn = CS.n, Gn1 = CS.(n+1); A1: Gn1 = FF:Step(Gn,source,sink) by Def20; assume A2: sink <> source; then CS is halting by Th17; then A3: Gn = CS.(n+1) by GLIB_000:def 55; now given P being Path of G such that A4: P is_Walk_from source,sink and A5: P is_augmenting_wrt Gn; set P = AP:GetAugPath(Gn,source,sink); A6: sink in dom AP:FindAugPath(Gn,source) by A4,A5,Th9; then A7: P is_Walk_from source,sink by Def14; then A8: P.first() = source by GLIB_001:def 23; A9: P.last() = sink by A7,GLIB_001:def 23; A10: P is_augmenting_wrt Gn by A6,Def14; Gn1 = FF:PushFlow(Gn, AP:GetAugPath(Gn,source,sink)) by A1,A6,Def18; then Gn.flow(source,sink) + P.tolerance(Gn) = Gn1.flow(source,sink) by A2,A7,A10 ,Th15; hence contradiction by A2,A3,A8,A9,A10,Th13,GLIB_001:127; end; hence thesis by A2,Th16,Th18; end;