begin
Lm1:
for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
Lm2:
for F being Function
for x, y being set holds x in dom (F +* (x .--> y))
Lm3:
for F being Function
for x, y being set holds (F +* (x .--> y)) . x = y
Lm4:
for F being Function
for x, y, z being set st x <> z holds
(F +* (x .--> y)) . z = F . z
begin
:: 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 );
:: 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())) ) ) );
:: 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})));
:: deftheorem Def4 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) ) ) );
:: deftheorem Def5 defines AP:VLabeling GLIB_005:def 5 :
for G being _Graph
for EL being FF:ELabeling of G
for b3 being PartFunc of (the_Vertices_of G),({1} \/ (the_Edges_of G)) holds
( b3 is AP:VLabeling of EL iff verum );
:: 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 ) );
:: 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 ) );
:: deftheorem Def8 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)) ) ) );
theorem Th1:
theorem Th2:
theorem Th3:
begin
:: 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 b4 being Subset of (the_Edges_of G) holds
( b4 = AP:NextBestEdges VL iff for e being set holds
( e in b4 iff ( e is_forward_edge_wrt VL or e is_backward_edge_wrt VL ) ) );
:: 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) . (choose (AP:NextBestEdges VL)) in dom VL implies AP:Step VL = VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL ) implies AP:Step VL = VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) ) );
:: deftheorem Def11 defines AP:VLabelingSeq GLIB_005:def 11 :
for G being _Graph
for EL being FF:ELabeling of G
for b3 being ManySortedSet of NAT holds
( b3 is AP:VLabelingSeq of EL iff for n being Nat holds b3 . n is AP:VLabeling of EL );
:: 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 b4 being AP:VLabelingSeq of EL holds
( b4 = AP:CompSeq (EL,source) iff ( b4 . 0 = source .--> 1 & ( for n being Nat holds b4 . (n + 1) = AP:Step (b4 . n) ) ) );
theorem Th4:
theorem Th5:
:: 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() ;
theorem Th6:
theorem Th7:
definition
let G be
finite real-weighted WGraph;
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:
(
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
( ( sink in dom (AP:FindAugPath (EL,source)) implies ex b1 being vertex-distinct Path of G st
( b1 is_Walk_from source,sink & b1 is_augmenting_wrt EL & ( for n being even Nat st n in dom b1 holds
b1 . n = (AP:FindAugPath (EL,source)) . (b1 . (n + 1)) ) ) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies ex b1 being vertex-distinct Path of G st b1 = G .walkOf source ) )
uniqueness
for b1, b2 being vertex-distinct Path of G holds
( ( sink in dom (AP:FindAugPath (EL,source)) & b1 is_Walk_from source,sink & b1 is_augmenting_wrt EL & ( for n being even Nat st n in dom b1 holds
b1 . n = (AP:FindAugPath (EL,source)) . (b1 . (n + 1)) ) & b2 is_Walk_from source,sink & b2 is_augmenting_wrt EL & ( for n being even Nat st n in dom b2 holds
b2 . n = (AP:FindAugPath (EL,source)) . (b2 . (n + 1)) ) implies b1 = b2 ) & ( not sink in dom (AP:FindAugPath (EL,source)) & b1 = G .walkOf source & b2 = G .walkOf source implies b1 = b2 ) )
consistency
for b1 being vertex-distinct Path of G holds verum
;
end;
:: 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 b5 being vertex-distinct Path of G holds
( ( sink in dom (AP:FindAugPath (EL,source)) implies ( b5 = AP:GetAugPath (EL,source,sink) iff ( b5 is_Walk_from source,sink & b5 is_augmenting_wrt EL & ( for n being even Nat st n in dom b5 holds
b5 . n = (AP:FindAugPath (EL,source)) . (b5 . (n + 1)) ) ) ) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies ( b5 = AP:GetAugPath (EL,source,sink) iff b5 = G .walkOf source ) ) );
theorem Th8:
theorem Th9:
theorem Th10:
begin
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 S1[
Nat,
set ]
means ( (
W . (2 * $1) DJoins W . ((2 * $1) - 1),
W . ((2 * $1) + 1),
G implies $2
= ((the_Weight_of G) . (W . (2 * $1))) - (EL . (W . (2 * $1))) ) & ( not
W . (2 * $1) DJoins W . ((2 * $1) - 1),
W . ((2 * $1) + 1),
G implies $2
= EL . (W . (2 * $1)) ) );
func W .flowSeq EL -> FinSequence of
NAT means :
Def15:
(
dom it = dom (W .edgeSeq()) & ( for
n being
Nat st
n in dom it holds
( (
W . (2 * n) DJoins W . ((2 * n) - 1),
W . ((2 * n) + 1),
G implies
it . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not
W . (2 * n) DJoins W . ((2 * n) - 1),
W . ((2 * n) + 1),
G implies
it . n = EL . (W . (2 * n)) ) ) ) );
existence
ex b1 being FinSequence of NAT st
( dom b1 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b1 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b1 . 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 b1 . n = EL . (W . (2 * n)) ) ) ) )
uniqueness
for b1, b2 being FinSequence of NAT st dom b1 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b1 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b1 . 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 b1 . n = EL . (W . (2 * n)) ) ) ) & dom b2 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b2 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b2 . 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 b2 . n = EL . (W . (2 * n)) ) ) ) holds
b1 = b2
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 b4 being FinSequence of NAT holds
( b4 = W .flowSeq EL iff ( dom b4 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b4 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b4 . 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 b4 . n = EL . (W . (2 * n)) ) ) ) ) );
:: 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 b4 being Nat holds
( ( not W is trivial implies ( b4 = W .tolerance EL iff ( b4 in rng (W .flowSeq EL) & ( for k being real number st k in rng (W .flowSeq EL) holds
b4 <= k ) ) ) ) & ( W is trivial implies ( b4 = W .tolerance EL iff b4 = 0 ) ) );
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
;
func FF:PushFlow (
EL,
P)
-> FF:ELabeling of
G means :
Def17:
( ( for
e being
set st
e in the_Edges_of G & not
e in P .edges() holds
it . e = EL . e ) & ( for
n being
odd Nat st
n < len P holds
( (
P . (n + 1) DJoins P . n,
P . (n + 2),
G implies
it . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not
P . (n + 1) DJoins P . n,
P . (n + 2),
G implies
it . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) );
existence
ex b1 being FF:ELabeling of G st
( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b1 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) )
uniqueness
for b1, b2 being FF:ELabeling of G st ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b1 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (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
b2 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b2 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b2 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) holds
b1 = b2
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 b4 being FF:ELabeling of G holds
( b4 = FF:PushFlow (EL,P) iff ( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b4 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b4 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b4 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) ) );
definition
let G be
finite natural-weighted WGraph;
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:
FF:PushFlow (
EL,
(AP:GetAugPath (EL,source,sink)))
if sink in dom (AP:FindAugPath (EL,source)) otherwise EL;
correctness
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 b1 being FF:ELabeling of G holds verum;
;
end;
:: 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 ) );
:: deftheorem Def19 defines FF:ELabelingSeq GLIB_005:def 19 :
for G being _Graph
for b2 being ManySortedSet of NAT holds
( b2 is FF:ELabelingSeq of G iff for n being Nat holds b2 . n is FF:ELabeling of G );
definition
let G be
finite natural-weighted WGraph;
let source,
sink be
Vertex of
G;
func FF:CompSeq (
G,
source,
sink)
-> FF:ELabelingSeq of
G means :
Def20:
(
it . 0 = (the_Edges_of G) --> 0 & ( for
n being
Nat holds
it . (n + 1) = FF:Step (
(it . n),
source,
sink) ) );
existence
ex b1 being FF:ELabelingSeq of G st
( b1 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b1 . (n + 1) = FF:Step ((b1 . n),source,sink) ) )
uniqueness
for b1, b2 being FF:ELabelingSeq of G st b1 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b1 . (n + 1) = FF:Step ((b1 . n),source,sink) ) & b2 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b2 . (n + 1) = FF:Step ((b2 . n),source,sink) ) holds
b1 = b2
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 b4 being FF:ELabelingSeq of G holds
( b4 = FF:CompSeq (G,source,sink) iff ( b4 . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b4 . (n + 1) = FF:Step ((b4 . n),source,sink) ) ) );
:: 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() ;
begin
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem