:: by Gilbert Lee

::

:: Received February 22, 2005

:: Copyright (c) 2005-2018 Association of Mizar Users

Lm1: for F being Function

for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}

proof end;

Lm2: for F being Function

for x, y being set holds x in dom (F +* (x .--> y))

proof end;

Lm3: for F being Function

for x, y being set holds (F +* (x .--> y)) . x = y

proof end;

Lm4: for F being Function

for x, y, z being set st x <> z holds

(F +* (x .--> y)) . z = F . z

proof end;

:: deftheorem Def1 defines natural-weighted GLIB_005:def 1 :

for G being WGraph holds

( G is natural-weighted iff the_Weight_of G is natural-valued );

for G being WGraph holds

( G is natural-weighted iff the_Weight_of G is natural-valued );

registration

for b_{1} being WGraph st b_{1} is natural-weighted holds

b_{1} is nonnegative-weighted
end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] natural-weighted -> nonnegative-weighted for WGraph;

coherence for b

b

proof end;

registration

ex b_{1} being WGraph st

( b_{1} is finite & b_{1} is trivial & b_{1} is Tree-like & b_{1} is natural-weighted )
end;

cluster Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite trivial Tree-like [Weighted] natural-weighted for WGraph;

existence ex b

( b

proof end;

registration
end;

definition
end;

definition

let G be finite real-weighted WGraph;

let EL be FF:ELabeling of G;

let source, sink be set ;

end;
let EL be FF:ELabeling of G;

let source, sink be set ;

pred EL has_valid_flow_from source,sink means :Def2: :: GLIB_005:def 2

( source is Vertex of G & sink is Vertex of G & ( for e being set st e in the_Edges_of G holds

( 0 <= EL . e & EL . e <= (the_Weight_of G) . e ) ) & ( for v being Vertex of G st v <> source & v <> sink holds

Sum (EL | (v .edgesIn())) = Sum (EL | (v .edgesOut())) ) );

( source is Vertex of G & sink is Vertex of G & ( for e being set st e in the_Edges_of G holds

( 0 <= EL . e & EL . e <= (the_Weight_of G) . e ) ) & ( for v being Vertex of G st v <> source & v <> sink holds

Sum (EL | (v .edgesIn())) = Sum (EL | (v .edgesOut())) ) );

:: deftheorem Def2 defines has_valid_flow_from GLIB_005:def 2 :

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set holds

( EL has_valid_flow_from source,sink iff ( source is Vertex of G & sink is Vertex of G & ( for e being set st e in the_Edges_of G holds

( 0 <= EL . e & EL . e <= (the_Weight_of G) . e ) ) & ( for v being Vertex of G st v <> source & v <> sink holds

Sum (EL | (v .edgesIn())) = Sum (EL | (v .edgesOut())) ) ) );

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set holds

( EL has_valid_flow_from source,sink iff ( source is Vertex of G & sink is Vertex of G & ( for e being set st e in the_Edges_of G holds

( 0 <= EL . e & EL . e <= (the_Weight_of G) . e ) ) & ( for v being Vertex of G st v <> source & v <> sink holds

Sum (EL | (v .edgesIn())) = Sum (EL | (v .edgesOut())) ) ) );

definition

let G be finite real-weighted WGraph;

let EL be FF:ELabeling of G;

let source, sink be set ;

(Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink}))) is Real ;

end;
let EL be FF:ELabeling of G;

let source, sink be set ;

func EL .flow (source,sink) -> Real equals :: GLIB_005:def 3

(Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})));

coherence (Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})));

(Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink}))) is Real ;

:: deftheorem defines .flow GLIB_005:def 3 :

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set holds EL .flow (source,sink) = (Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})));

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set holds EL .flow (source,sink) = (Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})));

definition

let G be finite real-weighted WGraph;

let EL be FF:ELabeling of G;

let source, sink be set ;

end;
let EL be FF:ELabeling of G;

let source, sink be set ;

pred EL has_maximum_flow_from source,sink means :: GLIB_005:def 4

( EL has_valid_flow_from source,sink & ( for E2 being FF:ELabeling of G st E2 has_valid_flow_from source,sink holds

E2 .flow (source,sink) <= EL .flow (source,sink) ) );

( EL has_valid_flow_from source,sink & ( for E2 being FF:ELabeling of G st E2 has_valid_flow_from source,sink holds

E2 .flow (source,sink) <= EL .flow (source,sink) ) );

:: deftheorem defines has_maximum_flow_from GLIB_005:def 4 :

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set holds

( EL has_maximum_flow_from source,sink iff ( EL has_valid_flow_from source,sink & ( for E2 being FF:ELabeling of G st E2 has_valid_flow_from source,sink holds

E2 .flow (source,sink) <= EL .flow (source,sink) ) ) );

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set holds

( EL has_maximum_flow_from source,sink iff ( EL has_valid_flow_from source,sink & ( for E2 being FF:ELabeling of G st E2 has_valid_flow_from source,sink holds

E2 .flow (source,sink) <= EL .flow (source,sink) ) ) );

definition

let G be _Graph;

let EL be FF:ELabeling of G;

ex b_{1} being PartFunc of (the_Vertices_of G),({1} \/ (the_Edges_of G)) st verum
;

end;
let EL be FF:ELabeling of G;

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

verum;

existence verum;

ex b

:: deftheorem Def5 defines AP:VLabeling GLIB_005:def 5 :

for G being _Graph

for EL being FF:ELabeling of G

for b_{3} being PartFunc of (the_Vertices_of G),({1} \/ (the_Edges_of G)) holds

( b_{3} is AP:VLabeling of EL iff verum );

for G being _Graph

for EL being FF:ELabeling of G

for b

( b

:: 1 used to mark source at the sart

definition

let G be real-weighted WGraph;

let EL be FF:ELabeling of G;

let VL be AP:VLabeling of EL;

let e be set ;

end;
let EL be FF:ELabeling of G;

let VL be AP:VLabeling of EL;

let e be set ;

pred e is_forward_edge_wrt VL means :Def6: :: GLIB_005:def 6

( e in the_Edges_of G & (the_Source_of G) . e in dom VL & not (the_Target_of G) . e in dom VL & EL . e < (the_Weight_of G) . e );

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

:: deftheorem Def6 defines is_forward_edge_wrt GLIB_005:def 6 :

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for VL being AP:VLabeling of EL

for e being set holds

( e is_forward_edge_wrt VL iff ( e in the_Edges_of G & (the_Source_of G) . e in dom VL & not (the_Target_of G) . e in dom VL & EL . e < (the_Weight_of G) . e ) );

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for VL being AP:VLabeling of EL

for e being set holds

( e is_forward_edge_wrt VL iff ( e in the_Edges_of G & (the_Source_of G) . e in dom VL & not (the_Target_of G) . e in dom VL & EL . e < (the_Weight_of G) . e ) );

definition

let G be real-weighted WGraph;

let EL be FF:ELabeling of G;

let VL be AP:VLabeling of EL;

let e be set ;

end;
let EL be FF:ELabeling of G;

let VL be AP:VLabeling of EL;

let e be set ;

pred e is_backward_edge_wrt VL means :Def7: :: GLIB_005:def 7

( e in the_Edges_of G & (the_Target_of G) . e in dom VL & not (the_Source_of G) . e in dom VL & 0 < EL . e );

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

:: deftheorem Def7 defines is_backward_edge_wrt GLIB_005:def 7 :

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for VL being AP:VLabeling of EL

for e being set holds

( e is_backward_edge_wrt VL iff ( e in the_Edges_of G & (the_Target_of G) . e in dom VL & not (the_Source_of G) . e in dom VL & 0 < EL . e ) );

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for VL being AP:VLabeling of EL

for e being set holds

( e is_backward_edge_wrt VL iff ( e in the_Edges_of G & (the_Target_of G) . e in dom VL & not (the_Source_of G) . e in dom VL & 0 < EL . e ) );

:: attribute with alternative structures

:: deftheorem defines is_augmenting_wrt GLIB_005:def 8 :

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G holds

( W is_augmenting_wrt EL iff for n being odd Nat st n < len W holds

( ( W . (n + 1) DJoins W . n,W . (n + 2),G implies EL . (W . (n + 1)) < (the_Weight_of G) . (W . (n + 1)) ) & ( not W . (n + 1) DJoins W . n,W . (n + 2),G implies 0 < EL . (W . (n + 1)) ) ) );

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G holds

( W is_augmenting_wrt EL iff for n being odd Nat st n < len W holds

( ( W . (n + 1) DJoins W . n,W . (n + 2),G implies EL . (W . (n + 1)) < (the_Weight_of G) . (W . (n + 1)) ) & ( not W . (n + 1) DJoins W . n,W . (n + 2),G implies 0 < EL . (W . (n + 1)) ) ) );

theorem Th1: :: GLIB_005:1

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G st W is trivial holds

W is_augmenting_wrt EL

for EL being FF:ELabeling of G

for W being Walk of G st W is trivial holds

W is_augmenting_wrt EL

proof end;

theorem Th2: :: GLIB_005:2

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G

for m, n being Nat st W is_augmenting_wrt EL holds

W .cut (m,n) is_augmenting_wrt EL

for EL being FF:ELabeling of G

for W being Walk of G

for m, n being Nat st W is_augmenting_wrt EL holds

W .cut (m,n) is_augmenting_wrt EL

proof end;

theorem Th3: :: GLIB_005:3

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G

for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds

W .addEdge e is_augmenting_wrt EL

for EL being FF:ELabeling of G

for W being Walk of G

for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds

W .addEdge e is_augmenting_wrt EL

proof end;

definition

let G be real-weighted WGraph;

let EL be FF:ELabeling of G;

let VL be AP:VLabeling of EL;

ex b_{1} being Subset of (the_Edges_of G) st

for e being set holds

( e in b_{1} iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) )

for b_{1}, b_{2} being Subset of (the_Edges_of G) st ( for e being set holds

( e in b_{1} iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) ) & ( for e being set holds

( e in b_{2} iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) ) holds

b_{1} = b_{2}

end;
let EL be FF:ELabeling of G;

let VL be AP:VLabeling of EL;

func AP:NextBestEdges VL -> Subset of (the_Edges_of G) means :Def9: :: GLIB_005:def 9

for e being set holds

( e in it iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) );

existence for e being set holds

( e in it iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) );

ex b

for e being set holds

( e in b

proof end;

uniqueness for b

( e in b

( e in b

b

proof end;

:: deftheorem Def9 defines AP:NextBestEdges GLIB_005:def 9 :

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for VL being AP:VLabeling of EL

for b_{4} being Subset of (the_Edges_of G) holds

( b_{4} = AP:NextBestEdges VL iff for e being set holds

( e in b_{4} iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) );

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for VL being AP:VLabeling of EL

for b

( b

( e in b

definition

let G be real-weighted WGraph;

let EL be FF:ELabeling of G;

let VL be AP:VLabeling of EL;

( ( AP:NextBestEdges VL = {} implies VL is AP:VLabeling of EL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) )

for b_{1} being AP:VLabeling of EL st AP:NextBestEdges VL = {} & AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL holds

( b_{1} = VL iff b_{1} = VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) )
;

end;
let EL be FF:ELabeling of G;

let VL be AP:VLabeling of EL;

func AP:Step VL -> AP:VLabeling of EL equals :Def10: :: GLIB_005:def 10

VL if AP:NextBestEdges VL = {}

VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) if ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL )

otherwise VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL);

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

( ( AP:NextBestEdges VL = {} implies VL is AP:VLabeling of EL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) )

proof end;

consistency for b

( b

:: deftheorem Def10 defines AP:Step GLIB_005:def 10 :

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for VL being AP:VLabeling of EL holds

( ( AP:NextBestEdges VL = {} implies AP:Step VL = VL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies AP:Step VL = VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies AP:Step VL = VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) ) );

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for VL being AP:VLabeling of EL holds

( ( AP:NextBestEdges VL = {} implies AP:Step VL = VL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies AP:Step VL = VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies AP:Step VL = VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) ) );

definition

let G be _Graph;

let EL be FF:ELabeling of G;

ex b_{1} being ManySortedSet of NAT st

for n being Nat holds b_{1} . n is AP:VLabeling of EL

end;
let EL be FF:ELabeling of G;

mode AP:VLabelingSeq of EL -> ManySortedSet of NAT means :Def11: :: GLIB_005:def 11

for n being Nat holds it . n is AP:VLabeling of EL;

existence for n being Nat holds it . n is AP:VLabeling of EL;

ex b

for n being Nat holds b

proof end;

:: deftheorem Def11 defines AP:VLabelingSeq GLIB_005:def 11 :

for G being _Graph

for EL being FF:ELabeling of G

for b_{3} being ManySortedSet of NAT holds

( b_{3} is AP:VLabelingSeq of EL iff for n being Nat holds b_{3} . n is AP:VLabeling of EL );

for G being _Graph

for EL being FF:ELabeling of G

for b

( b

definition

let G be _Graph;

let EL be FF:ELabeling of G;

let VS be AP:VLabelingSeq of EL;

let n be Nat;

:: original: .

redefine func VS . n -> AP:VLabeling of EL;

coherence

VS . n is AP:VLabeling of EL by Def11;

end;
let EL be FF:ELabeling of G;

let VS be AP:VLabelingSeq of EL;

let n be Nat;

:: original: .

redefine func VS . n -> AP:VLabeling of EL;

coherence

VS . n is AP:VLabeling of EL by Def11;

definition

let G be real-weighted WGraph;

let EL be FF:ELabeling of G;

let source be Vertex of G;

ex b_{1} being AP:VLabelingSeq of EL st

( b_{1} . 0 = source .--> 1 & ( for n being Nat holds b_{1} . (n + 1) = AP:Step (b_{1} . n) ) )

for b_{1}, b_{2} being AP:VLabelingSeq of EL st b_{1} . 0 = source .--> 1 & ( for n being Nat holds b_{1} . (n + 1) = AP:Step (b_{1} . n) ) & b_{2} . 0 = source .--> 1 & ( for n being Nat holds b_{2} . (n + 1) = AP:Step (b_{2} . n) ) holds

b_{1} = b_{2}

end;
let EL be FF:ELabeling of G;

let source be Vertex of G;

func AP:CompSeq (EL,source) -> AP:VLabelingSeq of EL means :Def12: :: GLIB_005:def 12

( it . 0 = source .--> 1 & ( for n being Nat holds it . (n + 1) = AP:Step (it . n) ) );

existence ( it . 0 = source .--> 1 & ( for n being Nat holds it . (n + 1) = AP:Step (it . n) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines AP:CompSeq GLIB_005:def 12 :

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G

for b_{4} being AP:VLabelingSeq of EL holds

( b_{4} = AP:CompSeq (EL,source) iff ( b_{4} . 0 = source .--> 1 & ( for n being Nat holds b_{4} . (n + 1) = AP:Step (b_{4} . n) ) ) );

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G

for b

( b

theorem Th4: :: GLIB_005:4

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G holds dom ((AP:CompSeq (EL,source)) . 0) = {source}

for EL being FF:ELabeling of G

for source being Vertex of G holds dom ((AP:CompSeq (EL,source)) . 0) = {source}

proof end;

theorem Th5: :: GLIB_005:5

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G

for i, j being Nat st i <= j holds

dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)

for EL being FF:ELabeling of G

for source being Vertex of G

for i, j being Nat st i <= j holds

dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)

proof end;

definition

let G be real-weighted WGraph;

let EL be FF:ELabeling of G;

let source be Vertex of G;

(AP:CompSeq (EL,source)) .Result() is AP:VLabeling of EL

end;
let EL be FF:ELabeling of G;

let source be Vertex of G;

func AP:FindAugPath (EL,source) -> AP:VLabeling of EL equals :: GLIB_005:def 13

(AP:CompSeq (EL,source)) .Result() ;

coherence (AP:CompSeq (EL,source)) .Result() ;

(AP:CompSeq (EL,source)) .Result() is AP:VLabeling of EL

proof end;

:: deftheorem defines AP:FindAugPath GLIB_005:def 13 :

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G holds AP:FindAugPath (EL,source) = (AP:CompSeq (EL,source)) .Result() ;

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G holds AP:FindAugPath (EL,source) = (AP:CompSeq (EL,source)) .Result() ;

theorem Th6: :: GLIB_005:6

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G holds AP:CompSeq (EL,source) is halting

for EL being FF:ELabeling of G

for source being Vertex of G holds AP:CompSeq (EL,source) is halting

proof end;

theorem Th7: :: GLIB_005:7

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G

for n being Nat

for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds

((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v

for EL being FF:ELabeling of G

for source being Vertex of G

for n being Nat

for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds

((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v

proof end;

definition

let G be finite real-weighted WGraph;

let EL be FF:ELabeling of G;

let source, sink be Vertex of G;

( ( sink in dom (AP:FindAugPath (EL,source)) implies ex b_{1} being vertex-distinct Path of G st

( b_{1} is_Walk_from source,sink & b_{1} is_augmenting_wrt EL & ( for n being even Nat st n in dom b_{1} holds

b_{1} . n = (AP:FindAugPath (EL,source)) . (b_{1} . (n + 1)) ) ) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies ex b_{1} being vertex-distinct Path of G st b_{1} = G .walkOf source ) )

for b_{1}, b_{2} being vertex-distinct Path of G holds

( ( sink in dom (AP:FindAugPath (EL,source)) & b_{1} is_Walk_from source,sink & b_{1} is_augmenting_wrt EL & ( for n being even Nat st n in dom b_{1} holds

b_{1} . n = (AP:FindAugPath (EL,source)) . (b_{1} . (n + 1)) ) & b_{2} is_Walk_from source,sink & b_{2} is_augmenting_wrt EL & ( for n being even Nat st n in dom b_{2} holds

b_{2} . n = (AP:FindAugPath (EL,source)) . (b_{2} . (n + 1)) ) implies b_{1} = b_{2} ) & ( not sink in dom (AP:FindAugPath (EL,source)) & b_{1} = G .walkOf source & b_{2} = G .walkOf source implies b_{1} = b_{2} ) )

for b_{1} being vertex-distinct Path of G holds verum
;

end;
let EL be FF:ELabeling of G;

let source, sink be Vertex of G;

func AP:GetAugPath (EL,source,sink) -> vertex-distinct Path of G means :Def14: :: GLIB_005:def 14

( it is_Walk_from source,sink & it is_augmenting_wrt EL & ( for n being even Nat st n in dom it holds

it . n = (AP:FindAugPath (EL,source)) . (it . (n + 1)) ) ) if sink in dom (AP:FindAugPath (EL,source))

otherwise it = G .walkOf source;

existence ( it is_Walk_from source,sink & it is_augmenting_wrt EL & ( for n being even Nat st n in dom it holds

it . n = (AP:FindAugPath (EL,source)) . (it . (n + 1)) ) ) if sink in dom (AP:FindAugPath (EL,source))

otherwise it = G .walkOf source;

( ( sink in dom (AP:FindAugPath (EL,source)) implies ex b

( b

b

proof end;

uniqueness for b

( ( sink in dom (AP:FindAugPath (EL,source)) & b

b

b

proof end;

consistency for b

:: deftheorem Def14 defines AP:GetAugPath GLIB_005:def 14 :

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being Vertex of G

for b_{5} being vertex-distinct Path of G holds

( ( sink in dom (AP:FindAugPath (EL,source)) implies ( b_{5} = AP:GetAugPath (EL,source,sink) iff ( b_{5} is_Walk_from source,sink & b_{5} is_augmenting_wrt EL & ( for n being even Nat st n in dom b_{5} holds

b_{5} . n = (AP:FindAugPath (EL,source)) . (b_{5} . (n + 1)) ) ) ) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies ( b_{5} = AP:GetAugPath (EL,source,sink) iff b_{5} = G .walkOf source ) ) );

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being Vertex of G

for b

( ( sink in dom (AP:FindAugPath (EL,source)) implies ( b

b

theorem Th8: :: GLIB_005:8

for G being real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G

for n being Nat

for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds

ex P being Path of G st

( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) )

for EL being FF:ELabeling of G

for source being Vertex of G

for n being Nat

for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds

ex P being Path of G st

( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) )

proof end;

theorem Th9: :: GLIB_005:9

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G

for v being set holds

( v in dom (AP:FindAugPath (EL,source)) iff ex P being Path of G st

( P is_Walk_from source,v & P is_augmenting_wrt EL ) )

for EL being FF:ELabeling of G

for source being Vertex of G

for v being set holds

( v in dom (AP:FindAugPath (EL,source)) iff ex P being Path of G st

( P is_Walk_from source,v & P is_augmenting_wrt EL ) )

proof end;

theorem Th10: :: GLIB_005:10

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source being Vertex of G holds source in dom (AP:FindAugPath (EL,source))

for EL being FF:ELabeling of G

for source being Vertex of G holds source in dom (AP:FindAugPath (EL,source))

proof end;

definition

let G be natural-weighted WGraph;

let EL be FF:ELabeling of G;

let W be Walk of G;

assume A1: W is_augmenting_wrt EL ;

defpred S_{1}[ 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)) ) );

ex b_{1} being FinSequence of NAT st

( dom b_{1} = dom (W .edgeSeq()) & ( for n being Nat st n in dom b_{1} holds

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b_{1} . 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 b_{1} . n = EL . (W . (2 * n)) ) ) ) )

for b_{1}, b_{2} being FinSequence of NAT st dom b_{1} = dom (W .edgeSeq()) & ( for n being Nat st n in dom b_{1} holds

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b_{1} . 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 b_{1} . n = EL . (W . (2 * n)) ) ) ) & dom b_{2} = dom (W .edgeSeq()) & ( for n being Nat st n in dom b_{2} holds

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b_{2} . 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 b_{2} . n = EL . (W . (2 * n)) ) ) ) holds

b_{1} = b_{2}

end;
let EL be FF:ELabeling of G;

let W be Walk of G;

assume A1: W is_augmenting_wrt EL ;

defpred S

func W .flowSeq EL -> FinSequence of NAT means :Def15: :: GLIB_005:def 15

( dom it = dom (W .edgeSeq()) & ( for n being Nat st n in dom it holds

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies it . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies it . n = EL . (W . (2 * n)) ) ) ) );

existence ( dom it = dom (W .edgeSeq()) & ( for n being Nat st n in dom it holds

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies it . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies it . n = EL . (W . (2 * n)) ) ) ) );

ex b

( dom b

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b

proof end;

uniqueness for b

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b

b

proof end;

:: deftheorem Def15 defines .flowSeq GLIB_005:def 15 :

for G being natural-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G st W is_augmenting_wrt EL holds

for b_{4} being FinSequence of NAT holds

( b_{4} = W .flowSeq EL iff ( dom b_{4} = dom (W .edgeSeq()) & ( for n being Nat st n in dom b_{4} holds

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b_{4} . 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 b_{4} . n = EL . (W . (2 * n)) ) ) ) ) );

for G being natural-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G st W is_augmenting_wrt EL holds

for b

( b

( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b

definition

let G be natural-weighted WGraph;

let EL be FF:ELabeling of G;

let W be Walk of G;

assume A1: W is_augmenting_wrt EL ;

( ( not W is trivial implies ex b_{1} being Nat st

( b_{1} in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds

b_{1} <= k ) ) ) & ( W is trivial implies ex b_{1} being Nat st b_{1} = 0 ) )

for b_{1}, b_{2} being Nat holds

( ( not W is trivial & b_{1} in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds

b_{1} <= k ) & b_{2} in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds

b_{2} <= k ) implies b_{1} = b_{2} ) & ( W is trivial & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Nat holds verum
;

end;
let EL be FF:ELabeling of G;

let W be Walk of G;

assume A1: W is_augmenting_wrt EL ;

func W .tolerance EL -> Nat means :Def16: :: GLIB_005:def 16

( it in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds

it <= k ) ) if not W is trivial

otherwise it = 0 ;

existence ( it in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds

it <= k ) ) if not W is trivial

otherwise it = 0 ;

( ( not W is trivial implies ex b

( b

b

proof end;

uniqueness for b

( ( not W is trivial & b

b

b

proof end;

consistency for b

:: deftheorem Def16 defines .tolerance GLIB_005:def 16 :

for G being natural-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G st W is_augmenting_wrt EL holds

for b_{4} being Nat holds

( ( not W is trivial implies ( b_{4} = W .tolerance EL iff ( b_{4} in rng (W .flowSeq EL) & ( for k being Real st k in rng (W .flowSeq EL) holds

b_{4} <= k ) ) ) ) & ( W is trivial implies ( b_{4} = W .tolerance EL iff b_{4} = 0 ) ) );

for G being natural-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G st W is_augmenting_wrt EL holds

for b

( ( not W is trivial implies ( b

b

definition

let G be natural-weighted WGraph;

let EL be FF:ELabeling of G;

let P be Path of G;

assume A1: P is_augmenting_wrt EL ;

ex b_{1} being FF:ELabeling of G st

( ( for e being set st e in the_Edges_of G & not e in P .edges() holds

b_{1} . e = EL . e ) & ( for n being odd Nat st n < len P holds

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b_{1} . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b_{1} . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) )

for b_{1}, b_{2} being FF:ELabeling of G st ( for e being set st e in the_Edges_of G & not e in P .edges() holds

b_{1} . e = EL . e ) & ( for n being odd Nat st n < len P holds

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b_{1} . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b_{1} . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) & ( for e being set st e in the_Edges_of G & not e in P .edges() holds

b_{2} . e = EL . e ) & ( for n being odd Nat st n < len P holds

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b_{2} . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b_{2} . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) holds

b_{1} = b_{2}

end;
let EL be FF:ELabeling of G;

let P be Path of G;

assume A1: P is_augmenting_wrt EL ;

func FF:PushFlow (EL,P) -> FF:ELabeling of G means :Def17: :: GLIB_005:def 17

( ( for e being set st e in the_Edges_of G & not e in P .edges() holds

it . e = EL . e ) & ( for n being odd Nat st n < len P holds

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies it . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies it . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) );

existence ( ( for e being set st e in the_Edges_of G & not e in P .edges() holds

it . e = EL . e ) & ( for n being odd Nat st n < len P holds

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies it . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies it . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) );

ex b

( ( for e being set st e in the_Edges_of G & not e in P .edges() holds

b

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b

proof end;

uniqueness for b

b

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b

b

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b

b

proof end;

:: deftheorem Def17 defines FF:PushFlow GLIB_005:def 17 :

for G being natural-weighted WGraph

for EL being FF:ELabeling of G

for P being Path of G st P is_augmenting_wrt EL holds

for b_{4} being FF:ELabeling of G holds

( b_{4} = FF:PushFlow (EL,P) iff ( ( for e being set st e in the_Edges_of G & not e in P .edges() holds

b_{4} . e = EL . e ) & ( for n being odd Nat st n < len P holds

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b_{4} . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b_{4} . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) ) );

for G being natural-weighted WGraph

for EL being FF:ELabeling of G

for P being Path of G st P is_augmenting_wrt EL holds

for b

( b

b

( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b

definition

let G be finite natural-weighted WGraph;

let EL be FF:ELabeling of G;

let sink, source be Vertex of G;

coherence

( ( sink in dom (AP:FindAugPath (EL,source)) implies FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) is FF:ELabeling of G ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies EL is FF:ELabeling of G ) );

consistency

for b_{1} being FF:ELabeling of G holds verum;

;

end;
let EL be FF:ELabeling of G;

let sink, source be Vertex of G;

func FF:Step (EL,source,sink) -> FF:ELabeling of G equals :Def18: :: GLIB_005:def 18

FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) if sink in dom (AP:FindAugPath (EL,source))

otherwise EL;

correctness FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) if sink in dom (AP:FindAugPath (EL,source))

otherwise EL;

coherence

( ( sink in dom (AP:FindAugPath (EL,source)) implies FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) is FF:ELabeling of G ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies EL is FF:ELabeling of G ) );

consistency

for b

;

:: deftheorem Def18 defines FF:Step GLIB_005:def 18 :

for G being finite natural-weighted WGraph

for EL being FF:ELabeling of G

for sink, source being Vertex of G holds

( ( sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = EL ) );

for G being finite natural-weighted WGraph

for EL being FF:ELabeling of G

for sink, source being Vertex of G holds

( ( sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = EL ) );

definition

let G be _Graph;

ex b_{1} being ManySortedSet of NAT st

for n being Nat holds b_{1} . n is FF:ELabeling of G

end;
mode FF:ELabelingSeq of G -> ManySortedSet of NAT means :Def19: :: GLIB_005:def 19

for n being Nat holds it . n is FF:ELabeling of G;

existence for n being Nat holds it . n is FF:ELabeling of G;

ex b

for n being Nat holds b

proof end;

:: deftheorem Def19 defines FF:ELabelingSeq GLIB_005:def 19 :

for G being _Graph

for b_{2} being ManySortedSet of NAT holds

( b_{2} is FF:ELabelingSeq of G iff for n being Nat holds b_{2} . n is FF:ELabeling of G );

for G being _Graph

for b

( b

registration

let G be _Graph;

let ES be FF:ELabelingSeq of G;

let n be Nat;

coherence

( ES . n is Function-like & ES . n is Relation-like ) by Def19;

end;
let ES be FF:ELabelingSeq of G;

let n be Nat;

coherence

( ES . n is Function-like & ES . n is Relation-like ) by Def19;

registration

let G be _Graph;

let ES be FF:ELabelingSeq of G;

let n be Nat;

coherence

ES . n is the_Edges_of G -defined by Def19;

end;
let ES be FF:ELabelingSeq of G;

let n be Nat;

coherence

ES . n is the_Edges_of G -defined by Def19;

registration

let G be _Graph;

let ES be FF:ELabelingSeq of G;

let n be Nat;

coherence

( ES . n is natural-valued & ES . n is total ) by Def19;

end;
let ES be FF:ELabelingSeq of G;

let n be Nat;

coherence

( ES . n is natural-valued & ES . n is total ) by Def19;

definition

let G be finite natural-weighted WGraph;

let source, sink be Vertex of G;

ex b_{1} being FF:ELabelingSeq of G st

( b_{1} . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b_{1} . (n + 1) = FF:Step ((b_{1} . n),source,sink) ) )

for b_{1}, b_{2} being FF:ELabelingSeq of G st b_{1} . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b_{1} . (n + 1) = FF:Step ((b_{1} . n),source,sink) ) & b_{2} . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b_{2} . (n + 1) = FF:Step ((b_{2} . n),source,sink) ) holds

b_{1} = b_{2}

end;
let source, sink be Vertex of G;

func FF:CompSeq (G,source,sink) -> FF:ELabelingSeq of G means :Def20: :: GLIB_005:def 20

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

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

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def20 defines FF:CompSeq GLIB_005:def 20 :

for G being finite natural-weighted WGraph

for source, sink being Vertex of G

for b_{4} being FF:ELabelingSeq of G holds

( b_{4} = FF:CompSeq (G,source,sink) iff ( b_{4} . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b_{4} . (n + 1) = FF:Step ((b_{4} . n),source,sink) ) ) );

for G being finite natural-weighted WGraph

for source, sink being Vertex of G

for b

( b

definition

let G be finite natural-weighted WGraph;

let sink, source be Vertex of G;

(FF:CompSeq (G,source,sink)) .Result() is FF:ELabeling of G ;

end;
let sink, source be Vertex of G;

func FF:MaxFlow (G,source,sink) -> FF:ELabeling of G equals :: GLIB_005:def 21

(FF:CompSeq (G,source,sink)) .Result() ;

coherence (FF:CompSeq (G,source,sink)) .Result() ;

(FF:CompSeq (G,source,sink)) .Result() is FF:ELabeling of G ;

:: deftheorem defines FF:MaxFlow GLIB_005:def 21 :

for G being finite natural-weighted WGraph

for sink, source being Vertex of G holds FF:MaxFlow (G,source,sink) = (FF:CompSeq (G,source,sink)) .Result() ;

for G being finite natural-weighted WGraph

for sink, source being Vertex of G holds FF:MaxFlow (G,source,sink) = (FF:CompSeq (G,source,sink)) .Result() ;

theorem Th11: :: GLIB_005:11

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set

for V being Subset of (the_Vertices_of G) st EL has_valid_flow_from source,sink & source in V & not sink in V holds

EL .flow (source,sink) = (Sum (EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V))))) - (Sum (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))))

for EL being FF:ELabeling of G

for source, sink being set

for V being Subset of (the_Vertices_of G) st EL has_valid_flow_from source,sink & source in V & not sink in V holds

EL .flow (source,sink) = (Sum (EL | (G .edgesDBetween (V,((the_Vertices_of G) \ V))))) - (Sum (EL | (G .edgesDBetween (((the_Vertices_of G) \ V),V))))

proof end;

theorem Th12: :: GLIB_005:12

for G being finite real-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set

for V being Subset of (the_Vertices_of G) st EL has_valid_flow_from source,sink & source in V & not sink in V holds

EL .flow (source,sink) <= Sum ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V))))

for EL being FF:ELabeling of G

for source, sink being set

for V being Subset of (the_Vertices_of G) st EL has_valid_flow_from source,sink & source in V & not sink in V holds

EL .flow (source,sink) <= Sum ((the_Weight_of G) | (G .edgesDBetween (V,((the_Vertices_of G) \ V))))

proof end;

theorem Th13: :: GLIB_005:13

for G being finite natural-weighted WGraph

for EL being FF:ELabeling of G

for W being Walk of G st not W is trivial & W is_augmenting_wrt EL holds

0 < W .tolerance EL

for EL being FF:ELabeling of G

for W being Walk of G st not W is trivial & W is_augmenting_wrt EL holds

0 < W .tolerance EL

proof end;

theorem Th14: :: GLIB_005:14

for G being finite natural-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set

for P being Path of G st source <> sink & EL has_valid_flow_from source,sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds

FF:PushFlow (EL,P) has_valid_flow_from source,sink

for EL being FF:ELabeling of G

for source, sink being set

for P being Path of G st source <> sink & EL has_valid_flow_from source,sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds

FF:PushFlow (EL,P) has_valid_flow_from source,sink

proof end;

theorem Th15: :: GLIB_005:15

for G being finite natural-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set

for P being Path of G st source <> sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds

(EL .flow (source,sink)) + (P .tolerance EL) = (FF:PushFlow (EL,P)) .flow (source,sink)

for EL being FF:ELabeling of G

for source, sink being set

for P being Path of G st source <> sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds

(EL .flow (source,sink)) + (P .tolerance EL) = (FF:PushFlow (EL,P)) .flow (source,sink)

proof end;

theorem Th16: :: GLIB_005:16

for G being finite natural-weighted WGraph

for source, sink being Vertex of G

for n being Nat st source <> sink holds

(FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink

for source, sink being Vertex of G

for n being Nat st source <> sink holds

(FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink

proof end;

theorem Th17: :: GLIB_005:17

for G being finite natural-weighted WGraph

for source, sink being Vertex of G st source <> sink holds

FF:CompSeq (G,source,sink) is halting

for source, sink being Vertex of G st source <> sink holds

FF:CompSeq (G,source,sink) is halting

proof end;

theorem Th18: :: GLIB_005:18

for G being finite natural-weighted WGraph

for EL being FF:ELabeling of G

for source, sink being set st EL has_valid_flow_from source,sink & ( for P being Path of G holds

( not P is_Walk_from source,sink or not P is_augmenting_wrt EL ) ) holds

EL has_maximum_flow_from source,sink

for EL being FF:ELabeling of G

for source, sink being set st EL has_valid_flow_from source,sink & ( for P being Path of G holds

( not P is_Walk_from source,sink or not P is_augmenting_wrt EL ) ) holds

EL has_maximum_flow_from source,sink

proof end;

theorem :: GLIB_005:19

for G being finite natural-weighted WGraph

for source, sink being Vertex of G st sink <> source holds

FF:MaxFlow (G,source,sink) has_maximum_flow_from source,sink

for source, sink being Vertex of G st sink <> source holds

FF:MaxFlow (G,source,sink) has_maximum_flow_from source,sink

proof end;

:: as the graphs are finite