:: Proof of Ford/Fulkerson's Maximum Network Flow AlgorithmRevised by Piotr Rudnicki, September 2008
:: by Gilbert Lee
::
:: Received February 22, 2005
:: Copyright (c) 2005 Association of Mizar Users
Tw0:
for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
Tw0a:
for F being Function
for x, y being set holds x in dom (F +* (x .--> y))
Tw1:
for F being Function
for x, y being set holds (F +* (x .--> y)) . x = y
Tw2:
for F being Function
for x, y, z being set st x <> z holds
(F +* (x .--> y)) . z = F . z
:: deftheorem Def3 defines natural-weighted GLIB_005:def 1 :
:: deftheorem Def7 defines has_valid_flow_from GLIB_005:def 2 :
:: deftheorem Def8 defines .flow GLIB_005:def 3 :
:: deftheorem Def9 defines has_maximum_flow_from GLIB_005:def 4 :
:: deftheorem HeHe defines AP:VLabeling GLIB_005:def 5 :
:: deftheorem Def10 defines is_forward_edge_wrt GLIB_005:def 6 :
:: deftheorem Def11 defines is_backward_edge_wrt GLIB_005:def 7 :
:: deftheorem Def12 defines is_augmenting_wrt GLIB_005:def 8 :
theorem Th001: :: GLIB_005:1
theorem Th002: :: GLIB_005:2
theorem Th2: :: GLIB_005:3
:: deftheorem Def13 defines AP:NextBestEdges GLIB_005:def 9 :
:: deftheorem Def14 defines AP:Step GLIB_005:def 10 :
:: deftheorem DEF1 defines AP:VLabelingSeq GLIB_005:def 11 :
:: deftheorem Def15 defines AP:CompSeq GLIB_005:def 12 :
theorem Th3: :: GLIB_005:4
theorem Th4: :: GLIB_005:5
:: deftheorem defines AP:FindAugPath GLIB_005:def 13 :
theorem Th6: :: GLIB_005:6
theorem Th7: :: GLIB_005:7
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 :
Def17:
:: 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
( ( 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 Def17 defines AP:GetAugPath GLIB_005:def 14 :
theorem Th8: :: GLIB_005:8
theorem Th9: :: GLIB_005:9
theorem Th10: :: GLIB_005:10
definition
let G be
natural-weighted WGraph;
let EL be
FF:ELabeling of
G;
let W be
Walk of
G;
assume A:
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 :
Def18:
:: 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
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 Def18 defines .flowSeq GLIB_005:def 15 :
:: deftheorem Def19 defines .tolerance GLIB_005:def 16 :
definition
let G be
natural-weighted WGraph;
let EL be
FF:ELabeling of
G;
let P be
Path of
G;
assume A:
P is_augmenting_wrt EL
;
func FF:PushFlow EL,
P -> FF:ELabeling of
G means :
Def20:
:: 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
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 Def20 defines FF:PushFlow GLIB_005:def 17 :
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 :
Def22:
:: GLIB_005:def 18
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 Def22 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 dFFELS defines FF:ELabelingSeq GLIB_005:def 19 :
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 :
Def23:
:: 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
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 Def23 defines FF:CompSeq GLIB_005:def 20 :
:: deftheorem defines FF:MaxFlow GLIB_005:def 21 :
theorem Th11: :: GLIB_005:11
theorem Th12: :: GLIB_005:12
theorem Th14: :: GLIB_005:13
theorem Th15: :: GLIB_005:14
theorem Th16: :: GLIB_005:15
theorem Th18: :: GLIB_005:16
theorem Th19: :: GLIB_005:17
theorem Th20: :: GLIB_005:18
theorem :: GLIB_005:19