glib_005.miz



    begin

    

     Lm1: for F be Function, x,y be 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});

    end;

    

     Lm2: for F be Function, x,y be set holds x in ( dom (F +* (x .--> y)))

    proof

      let F be Function, x,y be set;

      

       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 be Function, x,y be set holds ((F +* (x .--> y)) . x) = y

    proof

      let F be Function, x,y be set;

      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 be Function, x,y,z be 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

    definition

      let G be WGraph;

      :: GLIB_005:def1

      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 be 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

    definition

      let G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source,sink be set;

      :: GLIB_005:def2

      pred EL has_valid_flow_from source,sink means

      : Def2: source is Vertex of G & sink is Vertex of G & (for e be set st e in ( the_Edges_of G) holds 0 <= (EL . e) & (EL . e) <= (( the_Weight_of G) . e)) & for v be 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;

      :: GLIB_005:def3

      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 be FF:ELabeling of G, source,sink be set;

      :: GLIB_005:def4

      pred EL has_maximum_flow_from source,sink means EL has_valid_flow_from (source,sink) & for E2 be 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;

      :: GLIB_005:def5

      mode AP:VLabeling of EL -> PartFunc of ( the_Vertices_of G), ( {1} \/ ( the_Edges_of G)) means

      : Def5: not contradiction;

      existence ;

    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;

      :: GLIB_005:def6

      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;

      :: GLIB_005:def7

      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

    definition

      let G be real-weighted WGraph, EL be FF:ELabeling of G, W be Walk of G;

      :: GLIB_005:def8

      pred W is_augmenting_wrt EL means for n be odd Nat st n < ( len W) holds ((W . (n + 1)) DJoins ((W . n),(W . (n + 2)),G) implies (EL . (W . (n + 1))) < (( the_Weight_of G) . (W . (n + 1)))) & ( not (W . (n + 1)) DJoins ((W . n),(W . (n + 2)),G) implies 0 < (EL . (W . (n + 1))));

    end

    theorem :: GLIB_005:1

    

     Th1: for G be real-weighted WGraph, EL be FF:ELabeling of G, W be 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 :: GLIB_005:2

    

     Th2: for G be real-weighted WGraph, EL be FF:ELabeling of G, W be 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 be 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 :: GLIB_005:3

    

     Th3: for G be real-weighted WGraph, EL be FF:ELabeling of G, W be Walk of G, e,v be 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 be 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

    definition

      let G be real-weighted WGraph;

      let EL be FF:ELabeling of G, VL be AP:VLabeling of EL;

      :: GLIB_005:def9

      func AP:NextBestEdges (VL) -> Subset of ( the_Edges_of G) means

      : Def9: for e be 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 be Subset of ( the_Edges_of G) such that

         A1: for e be 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 be set holds e in IT1 iff (e is_forward_edge_wrt VL or e is_backward_edge_wrt VL) and

         A4: for e be 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;

      :: GLIB_005:def10

      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)});

          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)});

          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;

      :: GLIB_005:def11

      mode AP:VLabelingSeq of EL -> ManySortedSet of NAT means

      : Def11: for n be 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;

        (f . n) = {} ;

        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;

      :: original: .

      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;

      :: GLIB_005:def12

      func AP:CompSeq (EL,source) -> AP:VLabelingSeq of EL means

      : Def12: (it . 0 ) = (source .--> 1) & for n be 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 be 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 be set st P[n, x, y];

            end;

              suppose not x is AP:VLabeling of EL;

              hence ex y be set st P[n, x, y];

            end;

          end;

          hence ex y be set st P[n, x, y];

        end;

        then

         A2: for n be Nat holds for x be set holds ex y be set st P[n, x, y];

        consider IT be Function such that

         A3: ( dom IT) = NAT & (IT . 0 ) = (source .--> 1) & for n be 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 be 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};

        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 be 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 be 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 be Nat holds (IT1 . (n + 1)) = ( AP:Step (IT1 . n)) and

         A9: (IT2 . 0 ) = (source .--> 1) and

         A10: for n be 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 be Nat st P[n] holds P[(n + 1)];

        

         A12: P[ 0 ] by A7, A9;

        for n be Nat holds P[n] from NAT_1:sch 2( A12, A11);

        then for n be object st n in NAT holds (IT1 . n) = (IT2 . n);

        hence IT1 = IT2 by PBOOLE: 3;

      end;

    end

    theorem :: GLIB_005:4

    

     Th4: for G be real-weighted WGraph, EL be FF:ELabeling of G, source be 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;

    end;

    theorem :: GLIB_005:5

    

     Th5: for G be real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G, i,j be 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 be 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 be 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;

      :: GLIB_005:def13

      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 :: GLIB_005:6

    

     Th6: for G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source be 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 be 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 be 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 :: GLIB_005:7

    

     Th7: for G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G, n be Nat, v be 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 be 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 be 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 56;

      end;

      

       A3: P2[ 0 ];

      

       A4: for k be 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 be Nat st P[k] holds P[(k + 1)];

      

       A17: P[ 0 ];

      

       A18: for k be 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 be 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 be 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;

      :: GLIB_005:def14

      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 be 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 be set st v in ( dom (CS . $1)) holds ex P be 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 be 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 be 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 be 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 be 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 be 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 be 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 be vertex-distinct Path of G st P is_Walk_from (source,v) & P is_augmenting_wrt EL & (P .vertices() ) c= ( dom Gn1) & for n be even Nat st n in ( dom P) holds (P . n) = (FAP . (P . (n + 1)));

                  end;

                end;

                hence ex P be vertex-distinct Path of G st P is_Walk_from (source,v) & P is_augmenting_wrt EL & (P .vertices() ) c= ( dom Gn1) & for n be 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 be 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 be 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 be 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 be 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 be 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 be vertex-distinct Path of G st P is_Walk_from (source,v) & P is_augmenting_wrt EL & (P .vertices() ) c= ( dom Gn1) & for n be even Nat st n in ( dom P) holds (P . n) = (FAP . (P . (n + 1)));

                  end;

                end;

                hence ex P be vertex-distinct Path of G st P is_Walk_from (source,v) & P is_augmenting_wrt EL & (P .vertices() ) c= ( dom Gn1) & for n be 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 be 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 be Nat holds P[n] from NAT_1:sch 2( A82, A78);

        hereby

          assume sink in ( dom FAP);

          then

          consider W be 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 be 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 be 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 be set, P1,P2 be 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 be even Nat st n in ( dom P1) holds (P1 . n) = (FAP . (P1 . (n + 1)))) & (for n be 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 be even Nat st n in ( dom P1) holds (P1 . n) = (FAP . (P1 . (n + 1))) and

                 A101: for n be 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 be 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 be 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 be even Nat st n in ( dom P1) holds (P1 . n) = (FAP . (P1 . (n + 1))) and

                 A164: for n be 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 be 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 be 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 be 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 be even Nat st n in ( dom P1) holds (P1 . n) = (FAP . (P1 . (n + 1))) and for n be 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 be 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 be 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 be 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 :: GLIB_005:8

    

     Th8: for G be real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G, n be Nat, v be set st v in ( dom (( AP:CompSeq (EL,source)) . n)) holds ex P be 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 be FF:ELabeling of G, source be Vertex of G;

      set CS = ( AP:CompSeq (EL,source)), G0 = (CS . 0 );

      defpred P[ Nat] means for v be set st v in ( dom (CS . $1)) holds ex P be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be Nat holds P[n] from NAT_1:sch 2( A65, A1);

      hence thesis;

    end;

    theorem :: GLIB_005:9

    

     Th9: for G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G, v be set holds v in ( dom ( AP:FindAugPath (EL,source))) iff ex P be 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 be Path of G st P is_augmenting_wrt EL & P is_Walk_from (source,v) & (P .vertices() ) c= V by Th8;

        hence ex P be Path of G st P is_Walk_from (source,v) & P is_augmenting_wrt EL;

      end;

      given P be 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 be Nat st P[n] by A4;

        consider n be Nat such that

         A6: P[n] & for k be 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 56;

        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 :: GLIB_005:10

    

     Th10: for G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of G holds source in ( dom ( AP:FindAugPath (EL,source)))

    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));

      ( 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

    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))));

      :: GLIB_005:def15

      func W .flowSeq (EL) -> FinSequence of NAT means

      : Def15: ( dom it ) = ( dom (W .edgeSeq() )) & for n be 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 be set st P[k, x];

            end;

              suppose not (W . (2 * k)) DJoins ((W . ((2 * k) - 1)),(W . ((2 * k) + 1)),G);

              hence ex x be set st P[k, x];

            end;

          end;

          hence ex x be object st P[k, x];

        end;

        then

         A2: for k be Nat st k in ( Seg ( len (W .edgeSeq() ))) holds ex x be object st P[k, x];

        consider IT be FinSequence such that

         A3: ( dom IT) = ( Seg ( len (W .edgeSeq() ))) and

         A4: for k be 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 be 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 be Nat st n in ( dom IT1) holds P[n, (IT1 . n)] and

         A14: ( dom IT2) = ( dom (W .edgeSeq() )) and

         A15: for n be 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 be FF:ELabeling of G, W be Walk of G;

      assume

       A1: W is_augmenting_wrt EL;

      :: GLIB_005:def16

      func W .tolerance (EL) -> Nat means

      : Def16: it in ( rng (W .flowSeq EL)) & for k be 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 be object such that

           A2: y in ( rng (W .edgeSeq() )) by XBOOLE_0:def 1;

          consider x be 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 be Element of D such that

           A4: for k be 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 be Real st k in ( rng (W .flowSeq EL)) holds IT1 <= k;

          assume that

           A7: IT2 in ( rng (W .flowSeq EL)) and

           A8: for k be 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 be FF:ELabeling of G, P be Path of G;

      assume

       A1: P is_augmenting_wrt EL;

      :: GLIB_005:def17

      func FF:PushFlow (EL,P) -> FF:ELabeling of G means

      : Def17: (for e be set st e in ( the_Edges_of G) & not e in (P .edges() ) holds (it . e) = (EL . e)) & for n be 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 be 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 be 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 be set st P[x, y];

            end;

              suppose

               A3: x in (P .edges() );

              then

              consider n be 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 be 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 be set st P[x, y];

                end;

              end;

              hence ex y be set st P[x, y];

            end;

          end;

          hence ex y be object st P[x, y];

        end;

        then

         A17: for x be object st x in ( the_Edges_of G) holds ex y be object st P[x, y];

        consider IT be Function such that

         A18: ( dom IT) = ( the_Edges_of G) and

         A19: for e be 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 be 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 be 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 be 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 be set st e in ( the_Edges_of G) & not e in (P .edges() ) holds (IT1 . e) = (EL . e) and

         A36: for n be 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 be set st e in ( the_Edges_of G) & not e in (P .edges() ) holds (IT2 . e) = (EL . e) and

         A38: for n be 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 be 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 be FF:ELabeling of G, sink,source be Vertex of G;

      :: GLIB_005:def18

      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;

      :: GLIB_005:def19

      mode FF:ELabelingSeq of G -> ManySortedSet of NAT means

      : Def19: for n be 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;

      :: GLIB_005:def20

      func FF:CompSeq (G,source,sink) -> FF:ELabelingSeq of G means

      : Def20: (it . 0 ) = (( the_Edges_of G) --> 0 ) & for n be Nat holds (it . (n + 1)) = ( FF:Step ((it . n),source,sink));

      existence

      proof

        defpred P[ set, set, set] means (ex e be FF:ELabeling of G st e = $2 & $3 = ( FF:Step (e,source,sink))) or ( not ex e be FF:ELabeling of G st e = $2) & $3 = $2;

        now

          let n,x be set;

          now

            per cases ;

              suppose ex e be FF:ELabeling of G st e = x;

              then

              consider e be 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 be set st P[n, x, y];

            end;

              suppose not ex e be FF:ELabeling of G st e = x;

              hence ex y be set st P[n, x, y];

            end;

          end;

          hence ex y be set st P[n, x, y];

        end;

        then

         A2: for n be Nat holds for x be set holds ex y be set st P[n, x, y];

        consider IT be Function such that

         A3: ( dom IT) = NAT & (IT . 0 ) = (( the_Edges_of G) --> 0 ) & for n be 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 be FF:ELabeling of G st (IT . $1) = Gn;

         A4:

        now

          let n be Nat;

          assume P2[n];

          then

          consider Gn be 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 be Nat holds P2[n] from NAT_1:sch 2( A6, A4);

        now

          let n be Nat;

          ex Gn be 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 be 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 be Nat holds (IT1 . (n + 1)) = ( FF:Step ((IT1 . n),source,sink)) and

         A10: (IT2 . 0 ) = (( the_Edges_of G) --> 0 ) and

         A11: for n be 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 be Nat holds P[n] from NAT_1:sch 2( A14, A12);

        then for n be 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;

      :: GLIB_005:def21

      func FF:MaxFlow (G,source,sink) -> FF:ELabeling of G equals (( FF:CompSeq (G,source,sink)) .Result() );

      coherence ;

    end

    begin

    theorem :: GLIB_005:11

    

     Th11: for G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source,sink be set, V be 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 be 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 be 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, XBOOLE_1: 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, XBOOLE_1: 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 be 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 be non zero Nat holds P[n] from NAT_1:sch 10( A229, A6);

      hence thesis by A2, A3, A4;

    end;

    theorem :: GLIB_005:12

    

     Th12: for G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source,sink be set, V be 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 be 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 :: GLIB_005:13

    

     Th13: for G be _finite natural-weighted WGraph, EL be FF:ELabeling of G, W be 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 be 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 be 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 :: GLIB_005:14

    

     Th14: for G be _finite natural-weighted WGraph, EL be FF:ELabeling of G, source,sink be set, P be 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 be 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 be 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 be 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 be 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 be Vertex of G, m be 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;

                ( dom (e1 .--> ((EL . e1) + T))) = {e1};

                

                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 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 be Vertex of G, m be 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;

                ( dom (e2 .--> ((EL . e2) + T))) = {e2};

                

                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 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 be Vertex of G, m be 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;

                

                 A123: ( dom XIN1) = (( dom (EL | (v .edgesIn() ))) \/ ( dom (e1 .--> ((EL . e1) + T)))) by FUNCT_4:def 1

                .= (( dom (EL | (v .edgesIn() ))) \/ {e1})

                .= ((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

                .= (v .edgesIn() ) by A119, ZFMISC_1: 40;

                then

                reconsider XIN2 as Rbag of (v .edgesIn() ) by PARTFUN1:def 2, RELAT_1:def 18;

                

                 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 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 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;

                

                 A152: ( dom XOUT1) = (( dom (EL | (v .edgesOut() ))) \/ ( dom (e1 .--> ((EL . e1) - T)))) by FUNCT_4:def 1

                .= (( dom (EL | (v .edgesOut() ))) \/ {e1})

                .= ((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

                .= (v .edgesOut() ) by A147, ZFMISC_1: 40;

                then

                reconsider XOUT2 as Rbag of (v .edgesOut() ) by PARTFUN1:def 2, RELAT_1:def 18;

                

                 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 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 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;

                ( dom (e2 .--> ((EL . e2) - T))) = {e2};

                

                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 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;

                ( dom (e1 .--> ((EL . e1) - T))) = {e1};

                

                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 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 be 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 be 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 :: GLIB_005:15

    

     Th15: for G be _finite natural-weighted WGraph, EL be FF:ELabeling of G, source,sink be set, P be 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 be 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})

          .= ((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)));

                

                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 be Vertex of G, m be 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 be Vertex of G, m be 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})

          .= ((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)));

                

                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 be Vertex of G, m be 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 be Vertex of G, m be 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 :: GLIB_005:16

    

     Th16: for G be _finite natural-weighted WGraph, source,sink be Vertex of G, n be 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 be 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 be Nat st P[n] holds P[(n + 1)];

      for n be Nat holds P[n] from NAT_1:sch 2( A5, A12);

      hence thesis;

    end;

    theorem :: GLIB_005:17

    

     Th17: for G be _finite natural-weighted WGraph, source,sink be 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 be 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 be 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 be 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 :: GLIB_005:18

    

     Th18: for G be _finite natural-weighted WGraph, EL be FF:ELabeling of G, source,sink be set st EL has_valid_flow_from (source,sink) & not ex P be 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 be 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 56;

      

       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;

    ::$Notion-Name

    theorem :: GLIB_005:19

    for G be _finite natural-weighted WGraph, source,sink be 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 56;

      now

        given P be 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;