:: GLIB_005 semantic presentation

registration

let c₁ be set ;
let c₂ be real number ;
cluster a₁ .--> a₂ -> real-yielding ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be natural number ;
cluster K380(a₁,a₂) -> natural-yielding ;
coherence

proof end;

end;

registration

let c₁, c₂ be real-yielding Function;
cluster a₁ +* a₂ -> real-yielding ;
coherence

proof end;

end;

definition

let c₁ be EGraph;
attr a₁ is complete-elabeled means :Def1: :: GLIB_005:def 1
dom (the_ELabel_of a₁) = the_Edges_of a₁;

end;

:: deftheorem Def1 defines complete-elabeled GLIB_005:def 1 :

registration

let c₁ be _Graph;
let c₂ be ManySortedSet of the_Edges_of c₁;
cluster a₁ .set ELabelSelector ,a₂ -> complete-elabeled ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be non empty set ;
let c₃ be Function of the_Edges_of c₁,c₂;
cluster a₁ .set ELabelSelector ,a₃ -> complete-elabeled ;
coherence

proof end;

end;

definition

let c₁ be EGraphSeq;
attr a₁ is complete-elabeled means :Def2: :: GLIB_005:def 2
for b₁ being Nat holds a₁ .-> b₁ is complete-elabeled;

end;

:: deftheorem Def2 defines complete-elabeled GLIB_005:def 2 :

definition

let c₁ be WGraph;
attr a₁ is natural-weighted means :Def3: :: GLIB_005:def 3
the_Weight_of a₁ is natural-yielding;

end;

:: deftheorem Def3 defines natural-weighted GLIB_005:def 3 :

definition

let c₁ be EGraph;
attr a₁ is natural-elabeled means :Def4: :: GLIB_005:def 4
the_ELabel_of a₁ is natural-yielding;

end;

:: deftheorem Def4 defines natural-elabeled GLIB_005:def 4 :

definition

let c₁ be WGraphSeq;
attr a₁ is natural-weighted means :Def5: :: GLIB_005:def 5
for b₁ being Nat holds a₁ .-> b₁ is natural-weighted;

end;

:: deftheorem Def5 defines natural-weighted GLIB_005:def 5 :

definition

let c₁ be EGraphSeq;
attr a₁ is natural-elabeled means :Def6: :: GLIB_005:def 6
for b₁ being Nat holds a₁ .-> b₁ is natural-elabeled;

end;

:: deftheorem Def6 defines natural-elabeled GLIB_005:def 6 :

registration

cluster natural-weighted -> nonnegative-weighted GraphStruct ;
coherence

proof end;

end;

registration

cluster natural-elabeled -> real-elabeled GraphStruct ;
coherence

proof end;

end;

registration

cluster finite trivial Tree-like nonnegative-weighted real-elabeled real-vlabeled complete-elabeled natural-weighted natural-elabeled GraphStruct ;
existence

proof end;

end;

registration

cluster finite real-WEV complete-elabeled natural-weighted natural-elabeled ManySortedSet of NAT ;
existence

proof end;

end;

registration

let c₁ be complete-elabeled EGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> complete-elabeled ;
coherence by Def2;

end;

registration

let c₁ be natural-elabeled EGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> real-elabeled natural-elabeled ;
coherence by Def6;

end;

registration

let c₁ be natural-weighted WGraphSeq;
let c₂ be Nat;
cluster a₁ .-> a₂ -> nonnegative-weighted natural-weighted ;
coherence by Def5;

end;

registration

let c₁ be natural-weighted WGraph;
cluster the_Weight_of a₁ -> natural-yielding ;
coherence by Def3;

end;

registration

let c₁ be natural-elabeled EGraph;
cluster the_ELabel_of a₁ -> natural-yielding ;
coherence by Def4;

end;

definition

let c₁ be complete-elabeled EGraph;
redefine func the_ELabel_of as the_ELabel_of c₁ -> ManySortedSet of the_Edges_of a₁;
coherence

proof end;

end;

registration

let c₁ be natural-weighted WGraph;
let c₂ be set ;
cluster a₁ .set ELabelSelector ,a₂ -> natural-weighted ;
coherence

proof end;

cluster a₁ .set VLabelSelector ,a₂ -> natural-weighted ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be natural-yielding ManySortedSet of the_Edges_of c₁;
cluster a₁ .set ELabelSelector ,a₂ -> complete-elabeled natural-elabeled ;
coherence

proof end;

end;

definition

let c₁ be finite real-weighted real-elabeled complete-elabeled WEGraph;
let c₂, c₃ be set ;
pred c₁ has_valid_flow_from c₂,c₃ means :Def7: :: GLIB_005:def 7
( a₂ is Vertex of a₁ & a₃ is Vertex of a₁ & ( for b₁ being set st b₁ in the_Edges_of a₁ holds
( 0 <= (the_ELabel_of a₁) . b₁ & (the_ELabel_of a₁) . b₁ <= (the_Weight_of a₁) . b₁ ) ) & ( for b₁ being Vertex of a₁ st b₁ <> a₂ & b₁ <> a₃ holds
Sum ((the_ELabel_of a₁) | (b₁ .edgesIn() )) = Sum ((the_ELabel_of a₁) | (b₁ .edgesOut() )) ) );

end;

:: deftheorem Def7 defines has_valid_flow_from GLIB_005:def 7 :

definition

let c₁ be finite real-weighted real-elabeled complete-elabeled WEGraph;
let c₂, c₃ be set ;
assume c₁ has_valid_flow_from c₂,c₃ ;
func c₁ .flow c₂,c₃ -> real number equals :Def8: :: GLIB_005:def 8
(Sum ((the_ELabel_of a₁) | (a₁ .edgesInto {a₃}))) - (Sum ((the_ELabel_of a₁) | (a₁ .edgesOutOf {a₃})));
coherence ;

end;

:: deftheorem Def8 defines .flow GLIB_005:def 8 :

definition

let c₁ be finite real-weighted real-elabeled complete-elabeled WEGraph;
let c₂, c₃ be set ;
pred c₁ has_maximum_flow_from c₂,c₃ means :Def9: :: GLIB_005:def 9
( a₁ has_valid_flow_from a₂,a₃ & ( for b₁ being finite real-weighted real-elabeled complete-elabeled WEGraph st b₁ == a₁ & the_Weight_of a₁ = the_Weight_of b₁ & b₁ has_valid_flow_from a₂,a₃ holds
b₁ .flow a₂,a₃ <= a₁ .flow a₂,a₃ ) );

end;

:: deftheorem Def9 defines has_maximum_flow_from GLIB_005:def 9 :

definition

let c₁ be real-weighted real-elabeled WEVGraph;
let c₂ be set ;
pred c₂ is_forward_labeling_in c₁ means :Def10: :: GLIB_005:def 10
( a₂ in the_Edges_of a₁ & (the_Source_of a₁) . a₂ in a₁ .labeledV() & not (the_Target_of a₁) . a₂ in a₁ .labeledV() & (the_ELabel_of a₁) . a₂ < (the_Weight_of a₁) . a₂ );

end;

:: deftheorem Def10 defines is_forward_labeling_in GLIB_005:def 10 :

definition

let c₁ be real-elabeled EVGraph;
let c₂ be set ;
pred c₂ is_backward_labeling_in c₁ means :Def11: :: GLIB_005:def 11
( a₂ in the_Edges_of a₁ & (the_Target_of a₁) . a₂ in a₁ .labeledV() & not (the_Source_of a₁) . a₂ in a₁ .labeledV() & 0 < (the_ELabel_of a₁) . a₂ );

end;

:: deftheorem Def11 defines is_backward_labeling_in GLIB_005:def 11 :

definition

let c₁ be real-weighted real-elabeled WEGraph;
let c₂ be Walk of c₁;
attr a₂ is augmenting means :Def12: :: GLIB_005:def 12
for b₁ being odd Nat st b₁ < len a₂ holds
( ( a₂ . (b₁ + 1) DJoins a₂ . b₁,a₂ . (b₁ + 2),a₁ implies (the_ELabel_of a₁) . (a₂ . (b₁ + 1)) < (the_Weight_of a₁) . (a₂ . (b₁ + 1)) ) & ( not a₂ . (b₁ + 1) DJoins a₂ . b₁,a₂ . (b₁ + 2),a₁ implies 0 < (the_ELabel_of a₁) . (a₂ . (b₁ + 1)) ) );

end;

:: deftheorem Def12 defines augmenting GLIB_005:def 12 :

registration

let c₁ be real-weighted real-elabeled WEGraph;
cluster trivial -> augmenting Walk of a₁;
coherence

proof end;

end;

registration

let c₁ be real-weighted real-elabeled WEGraph;
cluster vertex-distinct augmenting Walk of a₁;
existence

proof end;

end;

registration

let c₁ be real-weighted real-elabeled WEGraph;
let c₂ be augmenting Walk of c₁;
let c₃, c₄ be Nat;
cluster a₂ .cut a₃,a₄ -> augmenting ;
coherence

proof end;

end;

theorem Th1: :: GLIB_005:1

for b₁, b₂ being real-weighted real-elabeled WEGraph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ is augmenting & b₁ == b₂ & the_Weight_of b₁ = the_Weight_of b₂ & the_ELabel_of b₁ = the_ELabel_of b₂ & b₃ = b₄ holds
b₄ is augmenting

proof end;

theorem Th2: :: GLIB_005:2

for b₁ being real-weighted real-elabeled WEGraph
for b₂ being augmenting Walk of b₁
for b₃, b₄ being set st not b₄ in b₂ .vertices() & ( ( b₃ DJoins b₂ .last() ,b₄,b₁ & (the_ELabel_of b₁) . b₃ < (the_Weight_of b₁) . b₃ ) or ( b₃ DJoins b₄,b₂ .last() ,b₁ & 0 < (the_ELabel_of b₁) . b₃ ) ) holds
b₂ .addEdge b₃ is augmenting

proof end;

definition

let c₁ be real-weighted real-elabeled WEVGraph;
func AP:NextBestEdges c₁ -> Subset of (the_Edges_of a₁) means :Def13: :: GLIB_005:def 13
for b₁ being set holds
( b₁ in a₂ iff ( b₁ is_forward_labeling_in a₁ or b₁ is_backward_labeling_in a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines AP:NextBestEdges GLIB_005:def 13 :

definition

let c₁ be real-weighted real-elabeled WEVGraph;
set c₂ = choose (AP:NextBestEdges c₁);
func AP:Step c₁ -> real-weighted real-elabeled WEVGraph equals :Def14: :: GLIB_005:def 14
a₁ if AP:NextBestEdges a₁ = {}
a₁ .labelVertex ((the_Source_of a₁) . (choose (AP:NextBestEdges a₁))),(choose (AP:NextBestEdges a₁)) if ( AP:NextBestEdges a₁ <> {} & not (the_Source_of a₁) . (choose (AP:NextBestEdges a₁)) in a₁ .labeledV() )
otherwise a₁ .labelVertex ((the_Target_of a₁) . (choose (AP:NextBestEdges a₁))),(choose (AP:NextBestEdges a₁));
coherence ;
consistency ;

end;

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

registration

let c₁ be finite real-weighted real-elabeled WEVGraph;
cluster AP:Step a₁ -> finite real-weighted real-elabeled ;
coherence

proof end;

end;

definition

let c₁ be real-weighted real-elabeled WEGraph;
let c₂ be Vertex of c₁;
func AP:CompSeq c₁,c₂ -> real-weighted real-elabeled WEVGraphSeq means :Def15: :: GLIB_005:def 15
( a₃ .-> 0 = a₁ .set VLabelSelector ,(a₂ .--> 1) & ( for b₁ being Nat holds a₃ .-> (b₁ + 1) = AP:Step (a₃ .-> b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines AP:CompSeq GLIB_005:def 15 :

registration

let c₁ be finite real-weighted real-elabeled WEGraph;
let c₂ be Vertex of c₁;
cluster AP:CompSeq a₁,a₂ -> finite real-weighted real-elabeled ;
coherence

proof end;

end;

theorem Th3: :: GLIB_005:3

for b₁ being real-weighted real-elabeled WEGraph
for b₂ being Vertex of b₁ holds
( b₁ == (AP:CompSeq b₁,b₂) .-> 0 & the_Weight_of b₁ = the_Weight_of ((AP:CompSeq b₁,b₂) .-> 0) & the_ELabel_of b₁ = the_ELabel_of ((AP:CompSeq b₁,b₂) .-> 0) & ((AP:CompSeq b₁,b₂) .-> 0) .labeledV() = {b₂} )

proof end;

theorem Th4: :: GLIB_005:4

for b₁ being real-weighted real-elabeled WEGraph
for b₂ being Vertex of b₁
for b₃, b₄ being Nat st b₃ <= b₄ holds
((AP:CompSeq b₁,b₂) .-> b₃) .labeledV() c= ((AP:CompSeq b₁,b₂) .-> b₄) .labeledV()

proof end;

theorem Th5: :: GLIB_005:5

for b₁ being real-weighted real-elabeled WEGraph
for b₂ being Vertex of b₁
for b₃ being Nat holds
( b₁ == (AP:CompSeq b₁,b₂) .-> b₃ & the_Weight_of b₁ = the_Weight_of ((AP:CompSeq b₁,b₂) .-> b₃) & the_ELabel_of b₁ = the_ELabel_of ((AP:CompSeq b₁,b₂) .-> b₃) )

proof end;

definition

let c₁ be real-weighted real-elabeled WEGraph;
let c₂ be Vertex of c₁;
func AP:FindAugPath c₁,c₂ -> real-weighted real-elabeled WEVGraph equals :: GLIB_005:def 16
(AP:CompSeq a₁,a₂) .Result() ;
coherence

proof end;

end;

:: deftheorem Def16 defines AP:FindAugPath GLIB_005:def 16 :

theorem Th6: :: GLIB_005:6

for b₁ being finite real-weighted real-elabeled WEGraph
for b₂ being Vertex of b₁ holds AP:CompSeq b₁,b₂ is halting

proof end;

theorem Th7: :: GLIB_005:7

for b₁ being finite real-weighted real-elabeled WEGraph
for b₂ being Vertex of b₁
for b₃ being Nat
for b₄ being set st b₄ in ((AP:CompSeq b₁,b₂) .-> b₃) .labeledV() holds
(the_VLabel_of ((AP:CompSeq b₁,b₂) .-> b₃)) . b₄ = (the_VLabel_of (AP:FindAugPath b₁,b₂)) . b₄

proof end;

definition

let c₁ be finite real-weighted real-elabeled WEGraph;
let c₂, c₃ be Vertex of c₁;
func AP:GetAugPath c₁,c₂,c₃ -> vertex-distinct augmenting Path of a₁ means :Def17: :: GLIB_005:def 17
( a₄ is_Walk_from a₂,a₃ & ( for b₁ being even Nat st b₁ in dom a₄ holds
a₄ . b₁ = (the_VLabel_of (AP:FindAugPath a₁,a₂)) . (a₄ . (b₁ + 1)) ) ) if a₃ in (AP:FindAugPath a₁,a₂) .labeledV()
otherwise a₄ = a₁ .walkOf a₂;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def17 defines AP:GetAugPath GLIB_005:def 17 :

theorem Th8: :: GLIB_005:8

for b₁ being real-weighted real-elabeled WEGraph
for b₂ being Vertex of b₁
for b₃ being Nat
for b₄ being set st b₄ in ((AP:CompSeq b₁,b₂) .-> b₃) .labeledV() holds
ex b₅ being Path of b₁ st
( b₅ is augmenting & b₅ is_Walk_from b₂,b₄ & b₅ .vertices() c= ((AP:CompSeq b₁,b₂) .-> b₃) .labeledV() )

proof end;

theorem Th9: :: GLIB_005:9

for b₁ being finite real-weighted real-elabeled WEGraph
for b₂ being Vertex of b₁
for b₃ being set holds
( b₃ in (AP:FindAugPath b₁,b₂) .labeledV() iff ex b₄ being Path of b₁ st
( b₄ is augmenting & b₄ is_Walk_from b₂,b₃ ) )

proof end;

theorem Th10: :: GLIB_005:10

for b₁ being finite real-weighted real-elabeled WEGraph
for b₂ being Vertex of b₁ holds
( b₂ in (AP:FindAugPath b₁,b₂) .labeledV() & b₁ == AP:FindAugPath b₁,b₂ & the_Weight_of b₁ = the_Weight_of (AP:FindAugPath b₁,b₂) & the_ELabel_of b₁ = the_ELabel_of (AP:FindAugPath b₁,b₂) )

proof end;

definition

let c₁ be real-weighted real-elabeled WEGraph;
let c₂ be augmenting Walk of c₁;
func c₂ .flowSeq() -> FinSequence of REAL means :Def18: :: GLIB_005:def 18
( dom a₃ = dom (a₂ .edgeSeq() ) & ( for b₁ being Nat st b₁ in dom a₃ holds
( ( a₂ . (2 * b₁) DJoins a₂ . ((2 * b₁) - 1),a₂ . ((2 * b₁) + 1),a₁ implies a₃ . b₁ = ((the_Weight_of a₁) . (a₂ . (2 * b₁))) - ((the_ELabel_of a₁) . (a₂ . (2 * b₁))) ) & ( not a₂ . (2 * b₁) DJoins a₂ . ((2 * b₁) - 1),a₂ . ((2 * b₁) + 1),a₁ implies a₃ . b₁ = (the_ELabel_of a₁) . (a₂ . (2 * b₁)) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines .flowSeq() GLIB_005:def 18 :

definition

let c₁ be real-weighted real-elabeled WEGraph;
let c₂ be augmenting Walk of c₁;
func c₂ .tolerance() -> Real means :Def19: :: GLIB_005:def 19
( a₃ in rng (a₂ .flowSeq() ) & ( for b₁ being Real st b₁ in rng (a₂ .flowSeq() ) holds
a₃ <= b₁ ) ) if not a₂ is trivial
otherwise a₃ = 0;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def19 defines .tolerance() GLIB_005:def 19 :

definition

let c₁ be natural-weighted natural-elabeled WEGraph;
let c₂ be augmenting Walk of c₁;
redefine func .tolerance() as c₂ .tolerance() -> Nat;
coherence

proof end;

end;

definition

let c₁ be real-weighted real-elabeled WEGraph;
let c₂ be augmenting Path of c₁;
func FF:PushFlow c₁,c₂ -> ManySortedSet of the_Edges_of a₁ means :Def20: :: GLIB_005:def 20
( ( for b₁ being set st b₁ in the_Edges_of a₁ & not b₁ in a₂ .edges() holds
a₃ . b₁ = (the_ELabel_of a₁) . b₁ ) & ( for b₁ being odd Nat st b₁ < len a₂ holds
( ( a₂ . (b₁ + 1) DJoins a₂ . b₁,a₂ . (b₁ + 2),a₁ implies a₃ . (a₂ . (b₁ + 1)) = ((the_ELabel_of a₁) . (a₂ . (b₁ + 1))) + (a₂ .tolerance() ) ) & ( not a₂ . (b₁ + 1) DJoins a₂ . b₁,a₂ . (b₁ + 2),a₁ implies a₃ . (a₂ . (b₁ + 1)) = ((the_ELabel_of a₁) . (a₂ . (b₁ + 1))) - (a₂ .tolerance() ) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let c₁ be real-weighted real-elabeled WEGraph;
let c₂ be augmenting Path of c₁;
cluster FF:PushFlow a₁,a₂ -> real-yielding ;
coherence

proof end;

end;

registration

let c₁ be natural-weighted natural-elabeled WEGraph;
let c₂ be augmenting Path of c₁;
cluster FF:PushFlow a₁,a₂ -> real-yielding natural-yielding ;
coherence

proof end;

end;

definition

let c₁ be real-weighted real-elabeled WEGraph;
let c₂ be augmenting Path of c₁;
func FF:AugmentPath c₁,c₂ -> real-weighted real-elabeled complete-elabeled WEGraph equals :: GLIB_005:def 21
a₁ .set ELabelSelector ,(FF:PushFlow a₁,a₂);
coherence ;

end;

:: deftheorem Def21 defines FF:AugmentPath GLIB_005:def 21 :

registration

let c₁ be finite real-weighted real-elabeled WEGraph;
let c₂ be augmenting Path of c₁;
cluster FF:AugmentPath a₁,a₂ -> finite real-weighted real-elabeled complete-elabeled ;
coherence ;

end;

registration

let c₁ be finite nonnegative-weighted real-elabeled WEGraph;
let c₂ be augmenting Path of c₁;
cluster FF:AugmentPath a₁,a₂ -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled ;
coherence ;

end;

registration

let c₁ be finite natural-weighted natural-elabeled WEGraph;
let c₂ be augmenting Path of c₁;
cluster FF:AugmentPath a₁,a₂ -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled natural-weighted natural-elabeled ;
coherence ;

end;

definition

let c₁ be finite real-weighted real-elabeled complete-elabeled WEGraph;
let c₂, c₃ be Vertex of c₁;
func FF:Step c₁,c₃,c₂ -> finite real-weighted real-elabeled complete-elabeled WEGraph equals :Def22: :: GLIB_005:def 22
FF:AugmentPath a₁,(AP:GetAugPath a₁,a₃,a₂) if a₂ in (AP:FindAugPath a₁,a₃) .labeledV()
otherwise a₁;
coherence ;
consistency ;

end;

:: deftheorem Def22 defines FF:Step GLIB_005:def 22 :

registration

let c₁ be finite nonnegative-weighted real-elabeled complete-elabeled WEGraph;
let c₂, c₃ be Vertex of c₁;
cluster FF:Step a₁,a₂,a₃ -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled ;
coherence

proof end;

end;

registration

let c₁ be finite complete-elabeled natural-weighted natural-elabeled WEGraph;
let c₂, c₃ be Vertex of c₁;
cluster FF:Step a₁,a₂,a₃ -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled natural-weighted natural-elabeled ;
coherence

proof end;

end;

definition

let c₁ be finite real-weighted WGraph;
let c₂, c₃ be Vertex of c₁;
func FF:CompSeq c₁,c₂,c₃ -> finite real-weighted real-elabeled complete-elabeled WEGraphSeq means :Def23: :: GLIB_005:def 23
( a₄ .-> 0 = a₁ .set ELabelSelector ,((the_Edges_of a₁) --> 0) & ( for b₁ being Nat ex b₂, b₃ being Vertex of (a₄ .-> b₁) st
( b₂ = a₂ & b₃ = a₃ & a₄ .-> (b₁ + 1) = FF:Step (a₄ .-> b₁),b₂,b₃ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines FF:CompSeq GLIB_005:def 23 :

registration

let c₁ be finite nonnegative-weighted WGraph;
let c₂, c₃ be Vertex of c₁;
cluster FF:CompSeq a₁,a₃,a₂ -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled ;
coherence

proof end;

end;

registration

let c₁ be finite natural-weighted WGraph;
let c₂, c₃ be Vertex of c₁;
cluster FF:CompSeq a₁,a₃,a₂ -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled natural-weighted natural-elabeled ;
coherence

proof end;

end;

definition

let c₁ be finite real-weighted WGraph;
let c₂, c₃ be Vertex of c₁;
func FF:MaxFlow c₁,c₃,c₂ -> finite real-weighted real-elabeled complete-elabeled WEGraph equals :: GLIB_005:def 24
(FF:CompSeq a₁,a₃,a₂) .Result() ;
coherence

proof end;

end;

:: deftheorem Def24 defines FF:MaxFlow GLIB_005:def 24 :

theorem Th11: :: GLIB_005:11

for b₁ being finite real-weighted real-elabeled complete-elabeled WEGraph
for b₂, b₃ being set
for b₄ being Subset of (the_Vertices_of b₁) st b₁ has_valid_flow_from b₂,b₃ & b₂ in b₄ & not b₃ in b₄ holds
b₁ .flow b₂,b₃ = (Sum ((the_ELabel_of b₁) | (b₁ .edgesDBetween b₄,((the_Vertices_of b₁) \ b₄)))) - (Sum ((the_ELabel_of b₁) | (b₁ .edgesDBetween ((the_Vertices_of b₁) \ b₄),b₄)))

proof end;

theorem Th12: :: GLIB_005:12

for b₁ being finite real-weighted real-elabeled complete-elabeled WEGraph
for b₂, b₃ being set
for b₄ being Subset of (the_Vertices_of b₁) st b₁ has_valid_flow_from b₂,b₃ & b₂ in b₄ & not b₃ in b₄ holds
b₁ .flow b₂,b₃ <= Sum ((the_Weight_of b₁) | (b₁ .edgesDBetween b₄,((the_Vertices_of b₁) \ b₄)))

proof end;

theorem Th13: :: GLIB_005:13

for b₁ being real-weighted real-elabeled WEGraph
for b₂ being augmenting Path of b₁ holds
( b₁ == FF:AugmentPath b₁,b₂ & the_Weight_of b₁ = the_Weight_of (FF:AugmentPath b₁,b₂) ) by GLIB_003:11, GLIB_003:8;

theorem Th14: :: GLIB_005:14

for b₁ being finite real-weighted real-elabeled WEGraph
for b₂ being augmenting Walk of b₁ st not b₂ is trivial holds
0 < b₂ .tolerance()

proof end;

theorem Th15: :: GLIB_005:15

for b₁ being finite real-weighted real-elabeled complete-elabeled WEGraph
for b₂, b₃ being set
for b₄ being augmenting Path of b₁ st b₂ <> b₃ & b₁ has_valid_flow_from b₂,b₃ & b₄ is_Walk_from b₂,b₃ holds
FF:AugmentPath b₁,b₄ has_valid_flow_from b₂,b₃

proof end;

theorem Th16: :: GLIB_005:16

for b₁ being finite real-weighted real-elabeled complete-elabeled WEGraph
for b₂, b₃ being set
for b₄ being augmenting Path of b₁ st b₂ <> b₃ & b₁ has_valid_flow_from b₂,b₃ & b₄ is_Walk_from b₂,b₃ holds
(b₁ .flow b₂,b₃) + (b₄ .tolerance() ) = (FF:AugmentPath b₁,b₄) .flow b₂,b₃

proof end;

theorem Th17: :: GLIB_005:17

for b₁ being finite real-weighted WGraph
for b₂, b₃ being Vertex of b₁
for b₄ being Nat holds
( (FF:CompSeq b₁,b₂,b₃) .-> b₄ == b₁ & the_Weight_of b₁ = the_Weight_of ((FF:CompSeq b₁,b₂,b₃) .-> b₄) )

proof end;

theorem Th18: :: GLIB_005:18

for b₁ being finite nonnegative-weighted WGraph
for b₂, b₃ being Vertex of b₁
for b₄ being Nat st b₂ <> b₃ holds
(FF:CompSeq b₁,b₂,b₃) .-> b₄ has_valid_flow_from b₂,b₃

proof end;

theorem Th19: :: GLIB_005:19

for b₁ being finite natural-weighted WGraph
for b₂, b₃ being Vertex of b₁ st b₂ <> b₃ holds
FF:CompSeq b₁,b₂,b₃ is halting

proof end;

theorem Th20: :: GLIB_005:20

for b₁ being finite real-weighted real-elabeled complete-elabeled WEGraph
for b₂, b₃ being set st b₂ <> b₃ & b₁ has_valid_flow_from b₂,b₃ & ( for b₄ being augmenting Path of b₁ holds not b₄ is_Walk_from b₂,b₃ ) holds
b₁ has_maximum_flow_from b₂,b₃

proof end;

theorem Th21: :: GLIB_005:21

for b₁ being finite real-weighted WGraph
for b₂, b₃ being Vertex of b₁ holds
( b₁ == FF:MaxFlow b₁,b₂,b₃ & the_Weight_of b₁ = the_Weight_of (FF:MaxFlow b₁,b₂,b₃) )

proof end;

theorem Th22: :: GLIB_005:22

for b₁ being finite natural-weighted WGraph
for b₂, b₃ being Vertex of b₁ st b₃ <> b₂ holds
FF:MaxFlow b₁,b₂,b₃ has_maximum_flow_from b₂,b₃

proof end;