let G be finite natural-weighted WGraph; :: thesis: for source, sink being Vertex of G st source <> sink holds
FF:CompSeq G,source,sink is halting
let source, sink be Vertex of G; :: thesis: ( source <> sink implies FF:CompSeq G,source,sink is halting )
set CS = FF:CompSeq G,source,sink;
assume A1: source <> sink ; :: thesis: FF:CompSeq G,source,sink is halting

now

set V = {source};
defpred S₁[ Element of NAT ] means ( $1 <= ((FF:CompSeq G,source,sink) . $1) .flow source,sink & ((FF:CompSeq G,source,sink) . $1) .flow source,sink is Element of NAT );
A2: source in {source} by TARSKI:def 1;
set W1 = (the_Weight_of G) | (G .edgesDBetween {source},((the_Vertices_of G) \ {source}));
degree ((the_Weight_of G) | (G .edgesDBetween {source},((the_Vertices_of G) \ {source}))) = Sum ((the_Weight_of G) | (G .edgesDBetween {source},((the_Vertices_of G) \ {source}))) ;
then reconsider N = Sum ((the_Weight_of G) | (G .edgesDBetween {source},((the_Vertices_of G) \ {source}))) as Element of NAT ;
set Gn1 = (FF:CompSeq G,source,sink) . (N + 1);
assume A3: for n being Element of NAT holds (FF:CompSeq G,source,sink) . n <> (FF:CompSeq G,source,sink) . (n + 1) ; :: thesis: contradiction

now

let n be Element of NAT ; :: thesis: ( n <= ((FF:CompSeq G,source,sink) . n) .flow source,sink & ((FF:CompSeq G,source,sink) . n) .flow source,sink is Element of NAT implies ( n + 1 <= ((FF:CompSeq G,source,sink) . (n + 1)) .flow source,sink & ((FF:CompSeq G,source,sink) . (n + 1)) .flow source,sink is Element of NAT ) )
set Gn = (FF:CompSeq G,source,sink) . n;
set Gn1 = (FF:CompSeq G,source,sink) . (n + 1);
assume that
A4: n <= ((FF:CompSeq G,source,sink) . n) .flow source,sink and
A5: ((FF:CompSeq G,source,sink) . n) .flow source,sink is Element of NAT ; :: thesis: ( n + 1 <= ((FF:CompSeq G,source,sink) . (n + 1)) .flow source,sink & ((FF:CompSeq G,source,sink) . (n + 1)) .flow source,sink is Element of NAT )
reconsider GnF = ((FF:CompSeq G,source,sink) . n) .flow source,sink as Element of NAT by A5;
set P = AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink;
A6: (FF:CompSeq G,source,sink) . (n + 1) = FF:Step ((FF:CompSeq G,source,sink) . n),source,sink by Def20;

A7: now

assume not sink in dom (AP:FindAugPath ((FF:CompSeq G,source,sink) . n),source) ; :: thesis: contradiction
then (FF:CompSeq G,source,sink) . (n + 1) = (FF:CompSeq G,source,sink) . n by A6, Def18;
hence contradiction by A3; :: thesis: verum

end;

then A8: AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink is_augmenting_wrt (FF:CompSeq G,source,sink) . n by Def14;
A9: AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink is_Walk_from source,sink by A7, Def14;
then A10: (AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink) .last() = sink by GLIB_001:def 23;
(FF:CompSeq G,source,sink) . (n + 1) = FF:PushFlow ((FF:CompSeq G,source,sink) . n),(AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink) by A6, A7, Def18;
then A11: GnF + ((AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink) .tolerance ((FF:CompSeq G,source,sink) . n)) = ((FF:CompSeq G,source,sink) . (n + 1)) .flow source,sink by A1, A8, A9, Th15;
then reconsider Gn1F = ((FF:CompSeq G,source,sink) . (n + 1)) .flow source,sink as Element of NAT ;
(AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink) .first() = source by A9, GLIB_001:def 23;
then 0 < (AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink) .tolerance ((FF:CompSeq G,source,sink) . n) by A1, A8, A10, Th13, GLIB_001:128;
then (GnF + ((AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink) .tolerance ((FF:CompSeq G,source,sink) . n))) - ((AP:GetAugPath ((FF:CompSeq G,source,sink) . n),source,sink) .tolerance ((FF:CompSeq G,source,sink) . n)) < Gn1F - 0 by A11, XREAL_1:17;
then n < Gn1F by A4, XXREAL_0:2;
hence n + 1 <= ((FF:CompSeq G,source,sink) . (n + 1)) .flow source,sink by NAT_1:13; :: thesis: ((FF:CompSeq G,source,sink) . (n + 1)) .flow source,sink is Element of NAT
thus ((FF:CompSeq G,source,sink) . (n + 1)) .flow source,sink is Element of NAT by A11; :: thesis: verum

end;

then A12: for n being Element of NAT st S₁[n] holds
S₁[n + 1] ;

now

set B1 = EmptyBag (G .edgesInto {sink});
set B2 = EmptyBag (G .edgesOutOf {sink});
set G0 = (FF:CompSeq G,source,sink) . 0 ;
set E1 = ((FF:CompSeq G,source,sink) . 0 ) | (G .edgesInto {sink});
set E2 = ((FF:CompSeq G,source,sink) . 0 ) | (G .edgesOutOf {sink});
A13: (FF:CompSeq G,source,sink) . 0 = (the_Edges_of G) --> 0 by Def20;

now

let e be set ; :: thesis: ( e in G .edgesInto {sink} implies (((FF:CompSeq G,source,sink) . 0 ) | (G .edgesInto {sink})) . e = (EmptyBag (G .edgesInto {sink})) . e )
assume A14: e in G .edgesInto {sink} ; :: thesis: (((FF:CompSeq G,source,sink) . 0 ) | (G .edgesInto {sink})) . e = (EmptyBag (G .edgesInto {sink})) . e
hence (((FF:CompSeq G,source,sink) . 0 ) | (G .edgesInto {sink})) . e = ((FF:CompSeq G,source,sink) . 0 ) . e by FUNCT_1:72
.= 0 by A13, A14, FUNCOP_1:13
.= (EmptyBag (G .edgesInto {sink})) . e by PRE_POLY:52 ;
:: thesis: verum

end;

then A15: Sum (((FF:CompSeq G,source,sink) . 0 ) | (G .edgesInto {sink})) = Sum (EmptyBag (G .edgesInto {sink})) by GLIB_004:6
.= 0 by UPROOTS:13 ;

now

let e be set ; :: thesis: ( e in G .edgesOutOf {sink} implies (((FF:CompSeq G,source,sink) . 0 ) | (G .edgesOutOf {sink})) . e = (EmptyBag (G .edgesOutOf {sink})) . e )
assume A16: e in G .edgesOutOf {sink} ; :: thesis: (((FF:CompSeq G,source,sink) . 0 ) | (G .edgesOutOf {sink})) . e = (EmptyBag (G .edgesOutOf {sink})) . e
hence (((FF:CompSeq G,source,sink) . 0 ) | (G .edgesOutOf {sink})) . e = ((FF:CompSeq G,source,sink) . 0 ) . e by FUNCT_1:72
.= 0 by A13, A16, FUNCOP_1:13
.= (EmptyBag (G .edgesOutOf {sink})) . e by PRE_POLY:52 ;
:: thesis: verum

end;

then A17: Sum (((FF:CompSeq G,source,sink) . 0 ) | (G .edgesOutOf {sink})) = Sum (EmptyBag (G .edgesOutOf {sink})) by GLIB_004:6
.= 0 by UPROOTS:13 ;
hence ((FF:CompSeq G,source,sink) . 0 ) .flow source,sink = 0 - 0 by A15; :: thesis: ((FF:CompSeq G,source,sink) . 0 ) .flow source,sink is Element of NAT
thus ((FF:CompSeq G,source,sink) . 0 ) .flow source,sink is Element of NAT by A15, A17; :: thesis: verum

end;

then A18: S₁[ 0 ] ;
A19: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A18, A12);
then reconsider Gn1F = ((FF:CompSeq G,source,sink) . (N + 1)) .flow source,sink as Element of NAT ;
(Sum ((the_Weight_of G) | (G .edgesDBetween {source},((the_Vertices_of G) \ {source})))) + 1 <= Gn1F by A19;
then A20: Sum ((the_Weight_of G) | (G .edgesDBetween {source},((the_Vertices_of G) \ {source}))) < ((FF:CompSeq G,source,sink) . (N + 1)) .flow source,sink by NAT_1:13;
not sink in {source} by A1, TARSKI:def 1;
hence contradiction by A2, A20, Th12, Th16; :: thesis: verum

end;

hence FF:CompSeq G,source,sink is halting by GLIB_000:def 56; :: thesis: verum