let G be _finite natural-weighted WGraph; :: thesis: for source, sink being Vertex of G st sink <> source holds
FF:MaxFlow (G,source,sink) has_maximum_flow_from source,sink
let source, sink be Vertex of G; :: thesis: ( sink <> source implies FF:MaxFlow (G,source,sink) has_maximum_flow_from source,sink )
set CS = FF:CompSeq (G,source,sink);
set n = (FF:CompSeq (G,source,sink)) .Lifespan() ;
set Gn = (FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan());
set Gn1 = (FF:CompSeq (G,source,sink)) . (((FF:CompSeq (G,source,sink)) .Lifespan()) + 1);
A1: (FF:CompSeq (G,source,sink)) . (((FF:CompSeq (G,source,sink)) .Lifespan()) + 1) = FF:Step (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),source,sink) by Def20;
assume A2: sink <> source ; :: thesis: FF:MaxFlow (G,source,sink) has_maximum_flow_from source,sink
then FF:CompSeq (G,source,sink) is halting by Th17;
then A3: (FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan()) = (FF:CompSeq (G,source,sink)) . (((FF:CompSeq (G,source,sink)) .Lifespan()) + 1) by GLIB_000:def 56;
now :: thesis: for P being Path of G holds
( not P is_Walk_from source,sink or not P is_augmenting_wrt (FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan()) )
given P being Path of G such that A4: P is_Walk_from source,sink and
A5: P is_augmenting_wrt (FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan()) ; :: thesis: contradiction
set P = AP:GetAugPath (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),source,sink);
A6: sink in dom (AP:FindAugPath (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),source)) by A4, A5, Th9;
then A7: AP:GetAugPath (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),source,sink) is_Walk_from source,sink by Def14;
then A8: (AP:GetAugPath (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),source,sink)) .first() = source by GLIB_001:def 23;
A9: (AP:GetAugPath (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),source,sink)) .last() = sink by A7, GLIB_001:def 23;
A10: AP:GetAugPath (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),source,sink) is_augmenting_wrt (FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan()) by A6, Def14;
(FF:CompSeq (G,source,sink)) . (((FF:CompSeq (G,source,sink)) .Lifespan()) + 1) = FF:PushFlow (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),(AP:GetAugPath (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),source,sink))) by A1, A6, Def18;
then (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())) .flow (source,sink)) + ((AP:GetAugPath (((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan())),source,sink)) .tolerance ((FF:CompSeq (G,source,sink)) . ((FF:CompSeq (G,source,sink)) .Lifespan()))) = ((FF:CompSeq (G,source,sink)) . (((FF:CompSeq (G,source,sink)) .Lifespan()) + 1)) .flow (source,sink) by A2, A7, A10, Th15;
hence contradiction by A2, A3, A8, A9, A10, Th13, GLIB_001:127; :: thesis: verum
end;
hence FF:MaxFlow (G,source,sink) has_maximum_flow_from source,sink by A2, Th16, Th18; :: thesis: verum