:: GLIB_005 semantic presentation

registration

let x be set ;
let y be real number ;
cluster x .--> y -> real-yielding ;
coherence

proof end;

end;

registration

let x be set ;
let y be natural number ;
cluster K380(x,y) -> natural-yielding ;
coherence

proof end;

end;

registration

let f, g be real-yielding Function;
cluster f +* g -> real-yielding ;
coherence

proof end;

end;

definition

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

end;

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

registration

let G be _Graph;
let X be ManySortedSet of the_Edges_of G;
cluster G .set ELabelSelector ,X -> complete-elabeled ;
coherence

proof end;

end;

registration

let G be _Graph;
let Y be non empty set ;
let X be Function of the_Edges_of G,Y;
cluster G .set ELabelSelector ,X -> complete-elabeled ;
coherence

proof end;

end;

definition

let GSq be EGraphSeq;
attr GSq is complete-elabeled means :Def2: :: GLIB_005:def 2
for x being Nat holds GSq .-> x is complete-elabeled;

end;

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

definition

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

end;

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

definition

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

end;

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

definition

let GSq be WGraphSeq;
attr GSq is natural-weighted means :Def5: :: GLIB_005:def 5
for x being Nat holds GSq .-> x is natural-weighted;

end;

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

definition

let GSq be EGraphSeq;
attr GSq is natural-elabeled means :Def6: :: GLIB_005:def 6
for x being Nat holds GSq .-> x 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 GSq be complete-elabeled EGraphSeq;
let x be Nat;
cluster GSq .-> x -> complete-elabeled ;
coherence by Def2;

end;

registration

let GSq be natural-elabeled EGraphSeq;
let x be Nat;
cluster GSq .-> x -> real-elabeled natural-elabeled ;
coherence by Def6;

end;

registration

let GSq be natural-weighted WGraphSeq;
let x be Nat;
cluster GSq .-> x -> nonnegative-weighted natural-weighted ;
coherence by Def5;

end;

registration

let G be natural-weighted WGraph;
cluster the_Weight_of G -> natural-yielding ;
coherence by Def3;

end;

registration

let G be natural-elabeled EGraph;
cluster the_ELabel_of G -> natural-yielding ;
coherence by Def4;

end;

definition

let G be complete-elabeled EGraph;
:: original: the_ELabel_of
redefine func the_ELabel_of G -> ManySortedSet of the_Edges_of G;
coherence

proof end;

end;

registration

let G be natural-weighted WGraph;
let X be set ;
cluster G .set ELabelSelector ,X -> natural-weighted ;
coherence

proof end;

cluster G .set VLabelSelector ,X -> natural-weighted ;
coherence

proof end;

end;

registration

let G be _Graph;
let X be natural-yielding ManySortedSet of the_Edges_of G;
cluster G .set ELabelSelector ,X -> complete-elabeled natural-elabeled ;
coherence

proof end;

end;

definition

let G be finite real-weighted real-elabeled complete-elabeled WEGraph;
let source, sink be set ;
pred G has_valid_flow_from source,sink means :Def7: :: GLIB_005:def 7
( source is Vertex of G & sink is Vertex of G & ( for e being set st e in the_Edges_of G holds
( 0 <= (the_ELabel_of G) . e & (the_ELabel_of G) . e <= (the_Weight_of G) . e ) ) & ( for v being Vertex of G st v <> source & v <> sink holds
Sum ((the_ELabel_of G) | (v .edgesIn() )) = Sum ((the_ELabel_of G) | (v .edgesOut() )) ) );

end;

:: deftheorem Def7 defines has_valid_flow_from GLIB_005:def 7 :

definition

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

end;

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

definition

let G be finite real-weighted real-elabeled complete-elabeled WEGraph;
let source, sink be set ;
pred G has_maximum_flow_from source,sink means :Def9: :: GLIB_005:def 9
( G has_valid_flow_from source,sink & ( for G2 being finite real-weighted real-elabeled complete-elabeled WEGraph st G2 == G & the_Weight_of G = the_Weight_of G2 & G2 has_valid_flow_from source,sink holds
G2 .flow source,sink <= G .flow source,sink ) );

end;

:: deftheorem Def9 defines has_maximum_flow_from GLIB_005:def 9 :

definition

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

end;

:: deftheorem Def10 defines is_forward_labeling_in GLIB_005:def 10 :

definition

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

end;

:: deftheorem Def11 defines is_backward_labeling_in GLIB_005:def 11 :

definition

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

end;

:: deftheorem Def12 defines augmenting GLIB_005:def 12 :

registration

let G be real-weighted real-elabeled WEGraph;
cluster trivial -> augmenting Walk of G;
coherence

proof end;

end;

registration

let G be real-weighted real-elabeled WEGraph;
cluster vertex-distinct augmenting Walk of G;
existence

proof end;

end;

registration

let G be real-weighted real-elabeled WEGraph;
let W be augmenting Walk of G;
let m, n be Nat;
cluster W .cut m,n -> augmenting ;
coherence

proof end;

end;

theorem :: GLIB_005:1

for G1, G2 being real-weighted real-elabeled WEGraph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 is augmenting & G1 == G2 & the_Weight_of G1 = the_Weight_of G2 & the_ELabel_of G1 = the_ELabel_of G2 & W1 = W2 holds
W2 is augmenting

proof end;

theorem Th2: :: GLIB_005:2

for G being real-weighted real-elabeled WEGraph
for W being augmenting Walk of G
for e, v being set st not v in W .vertices() & ( ( e DJoins W .last() ,v,G & (the_ELabel_of G) . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < (the_ELabel_of G) . e ) ) holds
W .addEdge e is augmenting

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

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

definition

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

end;

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

registration

let G be finite real-weighted real-elabeled WEVGraph;
cluster AP:Step G -> finite real-weighted real-elabeled ;
coherence

proof end;

end;

definition

let G be real-weighted real-elabeled WEGraph;
let source be Vertex of G;
func AP:CompSeq G,source -> real-weighted real-elabeled WEVGraphSeq means :Def15: :: GLIB_005:def 15
( it .-> 0 = G .set VLabelSelector ,(source .--> 1) & ( for n being Nat holds it .-> (n + 1) = AP:Step (it .-> n) ) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let G be finite real-weighted real-elabeled WEGraph;
let source be Vertex of G;
cluster AP:CompSeq G,source -> finite real-weighted real-elabeled ;
coherence

proof end;

end;

theorem Th3: :: GLIB_005:3

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

proof end;

theorem Th4: :: GLIB_005:4

for G being real-weighted real-elabeled WEGraph
for source being Vertex of G
for i, j being Nat st i <= j holds
((AP:CompSeq G,source) .-> i) .labeledV() c= ((AP:CompSeq G,source) .-> j) .labeledV()

proof end;

theorem Th5: :: GLIB_005:5

for G being real-weighted real-elabeled WEGraph
for source being Vertex of G
for n being Nat holds
( G == (AP:CompSeq G,source) .-> n & the_Weight_of G = the_Weight_of ((AP:CompSeq G,source) .-> n) & the_ELabel_of G = the_ELabel_of ((AP:CompSeq G,source) .-> n) )

proof end;

definition

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

proof end;

end;

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

theorem Th6: :: GLIB_005:6

for G being finite real-weighted real-elabeled WEGraph
for source being Vertex of G holds AP:CompSeq G,source is halting

proof end;

theorem Th7: :: GLIB_005:7

for G being finite real-weighted real-elabeled WEGraph
for source being Vertex of G
for n being Nat
for v being set st v in ((AP:CompSeq G,source) .-> n) .labeledV() holds
(the_VLabel_of ((AP:CompSeq G,source) .-> n)) . v = (the_VLabel_of (AP:FindAugPath G,source)) . v

proof end;

definition

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

proof end;

uniqueness

proof end;

consistency ;

end;

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

theorem Th8: :: GLIB_005:8

for G being real-weighted real-elabeled WEGraph
for source being Vertex of G
for n being Nat
for v being set st v in ((AP:CompSeq G,source) .-> n) .labeledV() holds
ex P being Path of G st
( P is augmenting & P is_Walk_from source,v & P .vertices() c= ((AP:CompSeq G,source) .-> n) .labeledV() )

proof end;

theorem Th9: :: GLIB_005:9

for G being finite real-weighted real-elabeled WEGraph
for source being Vertex of G
for v being set holds
( v in (AP:FindAugPath G,source) .labeledV() iff ex P being Path of G st
( P is augmenting & P is_Walk_from source,v ) )

proof end;

theorem Th10: :: GLIB_005:10

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

proof end;

definition

let G be real-weighted real-elabeled WEGraph;
let W be augmenting Walk of G;
func W .flowSeq() -> FinSequence of REAL means :Def18: :: GLIB_005:def 18
( 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))) - ((the_ELabel_of G) . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies it . n = (the_ELabel_of G) . (W . (2 * n)) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

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

proof end;

uniqueness

proof end;

consistency ;

end;

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

definition

let G be natural-weighted natural-elabeled WEGraph;
let W be augmenting Walk of G;
:: original: .tolerance()
redefine func W .tolerance() -> Nat;
coherence

proof end;

end;

definition

let G be real-weighted real-elabeled WEGraph;
let P be augmenting Path of G;
func FF:PushFlow G,P -> ManySortedSet of the_Edges_of G means :Def20: :: GLIB_005:def 20
( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
it . e = (the_ELabel_of G) . 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)) = ((the_ELabel_of G) . (P . (n + 1))) + (P .tolerance() ) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies it . (P . (n + 1)) = ((the_ELabel_of G) . (P . (n + 1))) - (P .tolerance() ) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let G be real-weighted real-elabeled WEGraph;
let P be augmenting Path of G;
cluster FF:PushFlow G,P -> real-yielding ;
coherence

proof end;

end;

registration

let G be natural-weighted natural-elabeled WEGraph;
let P be augmenting Path of G;
cluster FF:PushFlow G,P -> real-yielding natural-yielding ;
coherence

proof end;

end;

definition

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

end;

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

registration

let G be finite real-weighted real-elabeled WEGraph;
let P be augmenting Path of G;
cluster FF:AugmentPath G,P -> finite real-weighted real-elabeled complete-elabeled ;
coherence ;

end;

registration

let G be finite nonnegative-weighted real-elabeled WEGraph;
let P be augmenting Path of G;
cluster FF:AugmentPath G,P -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled ;
coherence ;

end;

registration

let G be finite natural-weighted natural-elabeled WEGraph;
let P be augmenting Path of G;
cluster FF:AugmentPath G,P -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled natural-weighted natural-elabeled ;
coherence ;

end;

definition

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

end;

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

registration

let G be finite nonnegative-weighted real-elabeled complete-elabeled WEGraph;
let source, sink be Vertex of G;
cluster FF:Step G,source,sink -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled ;
coherence

proof end;

end;

registration

let G be finite complete-elabeled natural-weighted natural-elabeled WEGraph;
let source, sink be Vertex of G;
cluster FF:Step G,source,sink -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled natural-weighted natural-elabeled ;
coherence

proof end;

end;

definition

let G be finite real-weighted WGraph;
let source, sink be Vertex of G;
func FF:CompSeq G,source,sink -> finite real-weighted real-elabeled complete-elabeled WEGraphSeq means :Def23: :: GLIB_005:def 23
( it .-> 0 = G .set ELabelSelector ,((the_Edges_of G) --> 0) & ( for n being Nat ex source', sink' being Vertex of (it .-> n) st
( source' = source & sink' = sink & it .-> (n + 1) = FF:Step (it .-> n),source',sink' ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let G be finite nonnegative-weighted WGraph;
let sink, source be Vertex of G;
cluster FF:CompSeq G,source,sink -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled ;
coherence

proof end;

end;

registration

let G be finite natural-weighted WGraph;
let sink, source be Vertex of G;
cluster FF:CompSeq G,source,sink -> finite real-weighted nonnegative-weighted real-elabeled complete-elabeled natural-weighted natural-elabeled ;
coherence

proof end;

end;

definition

let G be finite real-weighted WGraph;
let sink, source be Vertex of G;
func FF:MaxFlow G,source,sink -> finite real-weighted real-elabeled complete-elabeled WEGraph equals :: GLIB_005:def 24
(FF:CompSeq G,source,sink) .Result() ;
coherence

proof end;

end;

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

theorem Th11: :: GLIB_005:11

for G being finite real-weighted real-elabeled complete-elabeled WEGraph
for source, sink being set
for V being Subset of (the_Vertices_of G) st G has_valid_flow_from source,sink & source in V & not sink in V holds
G .flow source,sink = (Sum ((the_ELabel_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - (Sum ((the_ELabel_of G) | (G .edgesDBetween ((the_Vertices_of G) \ V),V)))

proof end;

theorem Th12: :: GLIB_005:12

for G being finite real-weighted real-elabeled complete-elabeled WEGraph
for source, sink being set
for V being Subset of (the_Vertices_of G) st G has_valid_flow_from source,sink & source in V & not sink in V holds
G .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 real-weighted real-elabeled WEGraph
for P being augmenting Path of G holds
( G == FF:AugmentPath G,P & the_Weight_of G = the_Weight_of (FF:AugmentPath G,P) ) by GLIB_003:11, GLIB_003:8;

theorem Th14: :: GLIB_005:14

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

proof end;

theorem Th15: :: GLIB_005:15

for G being finite real-weighted real-elabeled complete-elabeled WEGraph
for source, sink being set
for P being augmenting Path of G st source <> sink & G has_valid_flow_from source,sink & P is_Walk_from source,sink holds
FF:AugmentPath G,P has_valid_flow_from source,sink

proof end;

theorem Th16: :: GLIB_005:16

proof end;

theorem Th17: :: GLIB_005:17

for G being finite real-weighted WGraph
for source, sink being Vertex of G
for n being Nat holds
( (FF:CompSeq G,source,sink) .-> n == G & the_Weight_of G = the_Weight_of ((FF:CompSeq G,source,sink) .-> n) )

proof end;

theorem Th18: :: GLIB_005:18

for G being finite nonnegative-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

proof end;

theorem Th19: :: GLIB_005:19

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

proof end;

theorem Th20: :: GLIB_005:20

for G being finite real-weighted real-elabeled complete-elabeled WEGraph
for source, sink being set st source <> sink & G has_valid_flow_from source,sink & ( for P being augmenting Path of G holds not P is_Walk_from source,sink ) holds
G has_maximum_flow_from source,sink

proof end;

theorem :: GLIB_005:21

for G being finite real-weighted WGraph
for source, sink being Vertex of G holds
( G == FF:MaxFlow G,source,sink & the_Weight_of G = the_Weight_of (FF:MaxFlow G,source,sink) )

proof end;

theorem :: GLIB_005:22

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

proof end;