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 :: thesis: not for n being Nat holds (FF:CompSeq (G,source,sink)) . n <> (FF:CompSeq (G,source,sink)) . (n + 1)
set V = {source};
defpred S1[ 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 Nat holds (FF:CompSeq (G,source,sink)) . n <> (FF:CompSeq (G,source,sink)) . (n + 1) ; :: thesis: contradiction
now :: thesis: for n being Nat st n <= ((FF:CompSeq (G,source,sink)) . n) .flow (source,sink) & ((FF:CompSeq (G,source,sink)) . n) .flow (source,sink) is Element of NAT holds
( 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 )
let n be 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 :: thesis: sink in dom (AP:FindAugPath (((FF:CompSeq (G,source,sink)) . n),source))
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 by ORDINAL1:def 12;
(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:127;
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:15;
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, ORDINAL1:def 12; :: thesis: verum
end;
then A12: for n being Nat st S1[n] holds
S1[n + 1] ;
now :: thesis: ( ((FF:CompSeq (G,source,sink)) . 0) .flow (source,sink) = 0 - 0 & ((FF:CompSeq (G,source,sink)) . 0) .flow (source,sink) is Element of NAT )
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 :: thesis: for e being set st e in G .edgesInto {sink} holds
(((FF:CompSeq (G,source,sink)) . 0) | (G .edgesInto {sink})) . e = (EmptyBag (G .edgesInto {sink})) . e
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:49
.= 0 by A13, A14, FUNCOP_1:7
.= (EmptyBag (G .edgesInto {sink})) . e by PBOOLE:5 ;
:: 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:11 ;
now :: thesis: for e being set st e in G .edgesOutOf {sink} holds
(((FF:CompSeq (G,source,sink)) . 0) | (G .edgesOutOf {sink})) . e = (EmptyBag (G .edgesOutOf {sink})) . e
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:49
.= 0 by A13, A16, FUNCOP_1:7
.= (EmptyBag (G .edgesOutOf {sink})) . e by PBOOLE:5 ;
:: 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:11 ;
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: S1[ 0 ] ;
A19: for n being Nat holds S1[n] from NAT_1:sch 2(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 ; :: thesis: verum