:: Proof of Ford/Fulkerson's Maximum Network Flow Algorithm
:: by Gilbert Lee
::
:: Received February 22, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, XBOOLE_0, TARSKI,
GLIB_003, VALUED_0, SUBSET_1, REAL_1, GRAPH_5, FINSET_1, ZFMISC_1,
TREES_1, GLIB_000, PBOOLE, CARD_1, XXREAL_0, CARD_3, ARYTM_1, PARTFUN1,
ARYTM_3, GLIB_001, ABIAN, NAT_1, FINSEQ_1, GRAPH_1, RCOMP_1, INT_1,
PRE_POLY, UPROOTS, SGRAPH1, GLIB_005, XCMPLX_0;
notations TARSKI, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, XCMPLX_0,
XXREAL_0, XREAL_0, DOMAIN_1, RELAT_1, VALUED_0, PARTFUN1, FUNCT_1,
PBOOLE, FINSEQ_1, FUNCT_2, GRAPH_5, UPROOTS, RELSET_1, FINSET_1, INT_1,
NAT_1, FUNCOP_1, FUNCT_4, GLIB_000, GLIB_001, ABIAN, GLIB_002, GLIB_003,
PRE_POLY;
constructors DOMAIN_1, FUNCT_4, NAT_D, GRAPH_2, GRAPH_5, UPROOTS, GLIB_004,
XXREAL_2, RELSET_1, FINSEQ_6;
registrations XBOOLE_0, RELAT_1, PARTFUN1, INT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, GLIB_000, ABIAN, GLIB_001,
GLIB_002, GLIB_003, VALUED_0, FUNCT_2, CARD_1, PRE_CIRC, PRE_POLY,
RELSET_1;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions TARSKI;
equalities GLIB_000, GLIB_003, FUNCOP_1;
expansions TARSKI, GLIB_000, GLIB_003;
theorems CARD_1, CARD_2, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCT_1,
FUNCT_2, FUNCT_4, GLIB_000, GLIB_001, GLIB_004, GRAPH_5, ABIAN, INT_1,
NAT_1, PBOOLE, PEPIN, TARSKI, UPROOTS, XBOOLE_0, XBOOLE_1, ZFMISC_1,
XREAL_1, XXREAL_0, ORDINAL1, NAT_D, VALUED_0, RELSET_1, PARTFUN1,
RELAT_1;
schemes NAT_1, SUBSET_1, FINSEQ_1, CLASSES1, RECDEF_1, PRE_CIRC;
begin
Lm1: for F being Function, x,y being set holds dom(F+*(x.-->y)) = dom F \/ {x}
proof
let F be Function, x,y be set;
thus dom(F+*(x.-->y)) = dom F \/ dom(x.-->y) by FUNCT_4:def 1
.= dom F \/ {x};
end;
Lm2: for F being Function, x,y being set holds x in dom (F+*(x.-->y))
proof
let F be Function, x,y being set;
A1: x in dom (x.-->y) by TARSKI:def 1;
dom (x.-->y) c= dom (F+*(x.-->y)) by FUNCT_4:10;
hence thesis by A1;
end;
Lm3: for F being Function, x,y being set holds (F+*(x.-->y)).x = y
proof
let F be Function, x,y be set;
x in dom (x.-->y) by TARSKI:def 1;
hence (F+*(x.-->y)).x = (x.-->y).x by FUNCT_4:13
.= y by FUNCOP_1:72;
end;
Lm4: for F being Function, x,y,z being set st x <> z holds (F+*(x.-->y)).z = F
.z
proof
let F be Function, x,y,z be set;
assume x <> z;
then not z in dom (x.-->y) by TARSKI:def 1;
hence thesis by FUNCT_4:11;
end;
begin ::Preliminaries definitions for Maximum Flow Algorithm
definition
let G be WGraph;
attr G is natural-weighted means
:Def1:
the_Weight_of G is natural-valued;
end;
registration
cluster natural-weighted -> nonnegative-weighted for WGraph;
coherence
proof
let G be WGraph;
assume G is natural-weighted;
then
A1: the_Weight_of G is natural-valued;
for y being object st y in rng the_Weight_of G
holds y in Real>=0 by GRAPH_5:def 12,A1;
then rng the_Weight_of G c= Real>=0;
hence thesis;
end;
end;
registration
cluster _finite _trivial Tree-like natural-weighted for WGraph;
existence
proof
set E = {};
set V = {1};
reconsider S = {} as Function of E,V by RELSET_1:12;
set G1 = createGraph(V,E,S,S);
set WL = the Function of the_Edges_of G1, NAT;
set G2 = G1.set(WeightSelector, WL);
take G2;
thus G2 is _finite & G2 is _trivial & G2 is Tree-like;
the_Weight_of G2 = WL by GLIB_000:8;
hence thesis;
end;
end;
registration
let G be natural-weighted WGraph;
cluster the_Weight_of G -> natural-valued;
coherence by Def1;
end;
definition
let G be _Graph;
mode FF:ELabeling of G is natural-valued ManySortedSet of the_Edges_of G;
end;
:: NAT can be replaced by RAT but then we can convert it to the NAT case
:: as the graphs are finite
definition
let G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source,sink
be set;
pred EL has_valid_flow_from source,sink means
:Def2:
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());
end;
definition
let G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source, sink
be set;
func EL.flow(source,sink) -> Real equals
Sum (EL | G.edgesInto({sink}
)) - Sum (EL | G.edgesOutOf({sink}));
coherence;
end;
definition
let G be _finite real-weighted WGraph, EL being FF:ELabeling of G, source,
sink be set;
pred EL has_maximum_flow_from source,sink means
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);
end;
definition
let G be _Graph, EL be FF:ELabeling of G;
mode AP:VLabeling of EL -> PartFunc of the_Vertices_of G, {1} \/
the_Edges_of G means
:Def5:
not contradiction;
existence;
end;
:: 1 used to mark source at the sart
definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G, VL be AP:VLabeling of EL;
let e be set;
pred e is_forward_edge_wrt VL means
:Def6:
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;
end;
definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G, VL be AP:VLabeling of EL;
let e be set;
pred e is_backward_edge_wrt VL means
:Def7:
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;
end;
:: attribute with alternative structures
definition
let G be real-weighted WGraph, EL be FF:ELabeling of G, W be Walk of G;
pred W is_augmenting_wrt EL means
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)));
end;
theorem Th1:
for G being real-weighted WGraph, EL be FF:ELabeling of G, W
being Walk of G st W is trivial holds W is_augmenting_wrt EL
proof
let G be real-weighted WGraph, EL be FF:ELabeling of G;
let W be Walk of G;
assume
A1: W is trivial;
now
let n be odd Nat;
assume n < len W;
then n < 1 by A1,GLIB_001:126;
hence
(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)))
by ABIAN:12;
end;
hence thesis;
end;
theorem Th2:
for G being real-weighted WGraph, EL be FF:ELabeling of G, W
being Walk of G, m,n be Nat st W is_augmenting_wrt EL holds W.cut(m,n)
is_augmenting_wrt EL
proof
let G be real-weighted WGraph, EL be FF:ELabeling of G, W being Walk of G, m
,n be Nat;
set W2 = W.cut(m,n);
assume
A1: W is_augmenting_wrt EL;
now
per cases;
suppose
A2: m is odd & n is odd & m <= n & n <= len W;
then reconsider m9=m, n9 = n as odd Element of NAT by ORDINAL1:def 12;
now
let x be odd Nat;
reconsider x9 = x as Element of NAT by ORDINAL1:def 12;
set v1b = W2.x, eb = W2.(x+1), v2b = W2.(x+2);
assume
A3: x < len W2;
then
A4: x9 in dom W2 by GLIB_001:12;
A5: m9 <= n9 by A2;
A6: x9+2 in dom W2 by A3,GLIB_001:12;
then
A7: W2.(x9+2) = W.(m9+(x9+2)-1) by A2,A5,GLIB_001:47;
x9+1 in dom W2 by A3,GLIB_001:12;
then
A8: W2.(x9+1) = W.(m9+(x9+1)-1) by A2,A5,GLIB_001:47;
(m9+x9-1) in dom W by A2,A4,A5,GLIB_001:47;
then reconsider
a = m9+x-1,a2=m+(x+2)-1 as Element of NAT by A8;
reconsider a as odd Element of NAT;
set v1a = W.a, ea = W.(a+1), v2a = W.(a+2);
(m9+(x9+2)-1) in dom W by A2,A6,A5,GLIB_001:47;
then a2 <= len W by FINSEQ_3:25;
then
A9: m+(x+2)-1-2 < len W - 0 by XREAL_1:15;
hereby
assume eb DJoins v1b,v2b,G;
then ea DJoins v1a,v2a,G by A2,A4,A5,A8,A7,GLIB_001:47;
hence EL.eb < (the_Weight_of G).eb by A1,A8,A9;
end;
assume not eb DJoins v1b,v2b,G;
then not ea DJoins v1a,v2a,G by A2,A4,A5,A8,A7,GLIB_001:47;
hence 0 < EL.eb by A1,A8,A9;
end;
hence thesis;
end;
suppose
not (m is odd & n is odd & m <= n & n <= len W);
hence thesis by A1,GLIB_001:def 11;
end;
end;
hence thesis;
end;
theorem Th3:
for G being real-weighted WGraph, EL being FF:ELabeling of G, W
being Walk of G, e,v being set st W is_augmenting_wrt EL & not v in W
.vertices() & ( e DJoins W.last(),v,G & EL.e < (the_Weight_of G).e or e DJoins
v,W.last(),G & 0 < (EL.e) ) holds W.addEdge(e) is_augmenting_wrt EL
proof
let G be real-weighted WGraph, EL being FF:ELabeling of G, W be Walk of G, e
,v be set;
assume
A1: W is_augmenting_wrt EL;
set W2 = W.addEdge(e);
assume that
A2: not v in W.vertices() and
A3: e DJoins W.last(),v,G & EL.e < (the_Weight_of G).e or e DJoins v,W
.last(),G & 0 < EL.e;
let n be odd Nat;
A4: e Joins W.last(),v,G by A3;
assume
A5: n < len W2;
now
per cases;
suppose
A6: n < len W;
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
n9+1 in dom W by A6,GLIB_001:12;
then
A7: W.(n+1) = W2.(n+1) by A4,GLIB_001:65;
n9+2 in dom W by A6,GLIB_001:12;
then
A8: W.(n+2) = W2.(n+2) by A4,GLIB_001:65;
n9 in dom W by A6,GLIB_001:12;
then W.n = W2.n by A4,GLIB_001:65;
hence thesis by A1,A6,A7,A8;
end;
suppose
A9: n >= len W;
n+1 <= len W2 by A5,NAT_1:13;
then n+1 <= len W + 2*1 by A4,GLIB_001:64;
then n+1 < len W + 1+1 by XXREAL_0:1;
then n+1 <= len W + 1 by NAT_1:13;
then
A10: n <= len W by XREAL_1:6;
then
A11: n = len W by A9,XXREAL_0:1;
then
A12: W2.(n+1) = e by A4,GLIB_001:65;
1 <= n by ABIAN:12;
then n in dom W by A10,FINSEQ_3:25;
then
A13: W2.n = W.n by A4,GLIB_001:65
.= W.last() by A11,GLIB_001:def 7;
not e DJoins W.last(),v,G or not e DJoins v,W.last(),G
by A2,GLIB_001:88;
hence W2.(n+1) DJoins W2.n, W2.(n+2),G implies EL.(W2.(n+1)) < (
the_Weight_of G).(W2.(n+1)) by A3,A13,A12;
assume not W2.(n+1) DJoins W2.n, W2.(n+2),G;
hence 0 < EL.(W2.(n+1)) by A3,A4,A11,A13,A12,GLIB_001:65;
end;
end;
hence thesis;
end;
begin :: Finding an Augmenting Path in a Graph
definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G, VL be AP:VLabeling of EL;
func AP:NextBestEdges(VL) -> Subset of the_Edges_of G means
:Def9:
for e
being set holds e in it iff (e is_forward_edge_wrt VL or e is_backward_edge_wrt
VL);
existence
proof
defpred P[set] means $1 is_forward_edge_wrt VL or $1 is_backward_edge_wrt
VL;
consider IT being Subset of the_Edges_of G such that
A1: for e being set holds e in IT iff e in the_Edges_of G & P[e] from
SUBSET_1:sch 1;
take IT;
let e be set;
thus e in IT implies P[e] by A1;
assume
A2: P[e];
then e in the_Edges_of G by Def6,Def7;
hence thesis by A1,A2;
end;
uniqueness
proof
let IT1,IT2 be Subset of the_Edges_of G such that
A3: for e being set holds e in IT1 iff (e is_forward_edge_wrt VL or e
is_backward_edge_wrt VL) and
A4: for e being set holds e in IT2 iff (e is_forward_edge_wrt VL or e
is_backward_edge_wrt VL);
now
let e be object;
reconsider ee=e as set by TARSKI:1;
hereby
assume e in IT1;
then ee is_forward_edge_wrt VL or ee is_backward_edge_wrt VL by A3;
hence e in IT2 by A4;
end;
assume e in IT2;
then ee is_forward_edge_wrt VL or ee is_backward_edge_wrt VL by A4;
hence e in IT1 by A3;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let G be real-weighted WGraph;
let EL be FF:ELabeling of G, VL be AP:VLabeling of EL;
func AP:Step(VL) -> AP:VLabeling of EL equals
:Def10:
VL if AP:NextBestEdges
(VL) = {}, VL+*((the_Source_of G).(
the Element of AP:NextBestEdges(VL)) .--> the Element of
AP:NextBestEdges(VL)) if AP:NextBestEdges(VL) <> {} & not (the_Source_of G).(
the Element of AP:NextBestEdges(VL)) in dom VL
otherwise VL+*((the_Target_of G).
(the Element of
AP:NextBestEdges(VL)) .--> the Element of AP:NextBestEdges(VL));
coherence
proof
set cNB = the Element of AP:NextBestEdges(VL);
set SG = the_Source_of G, TG = the_Target_of G, VG = the_Vertices_of G, EG
= the_Edges_of G, NB = AP:NextBestEdges(VL);
per cases;
suppose
NB = {};
hence thesis;
end;
suppose
NB <> {};
then
A1: cNB in NB;
A2: {SG.cNB} c= VG
proof
let x be object;
assume x in {SG.cNB};
then x = SG.cNB by TARSKI:def 1;
hence thesis by A1,FUNCT_2:5;
end;
{cNB} c= EG
proof
let x be object;
assume x in {cNB};
then x = cNB by TARSKI:def 1;
hence thesis by A1;
end;
then
A3: {cNB} c= {1} \/ EG by XBOOLE_1:10;
rng (TG.cNB .--> cNB) c= {cNB} by FUNCOP_1:13;
then rng (TG.cNB .--> cNB) c= {1} \/ EG by A3;
then
A4: rng VL \/ rng (TG.cNB .--> cNB) c= {1} \/ EG by XBOOLE_1:8;
rng (VL+*(TG.cNB .--> cNB)) c= rng VL \/ rng (TG.cNB .--> cNB) by
FUNCT_4:17;
then
A5: rng (VL+*(TG.cNB .--> cNB)) c= {1} \/ EG by A4;
{cNB} c= EG
proof
let x be object;
assume x in {cNB};
then x = cNB by TARSKI:def 1;
hence thesis by A1;
end;
then
A6: {cNB} c= {1} \/ EG by XBOOLE_1:10;
rng (SG.cNB .--> cNB) c= {cNB} by FUNCOP_1:13;
then rng (SG.cNB .--> cNB) c= {1} \/ EG by A6;
then
A7: rng VL \/ rng (SG.cNB .--> cNB) c= {1} \/ EG by XBOOLE_1:8;
rng (VL+*(SG.cNB .--> cNB)) c= rng VL \/ rng (SG.cNB .--> cNB) by
FUNCT_4:17;
then
A8: rng (VL+*(SG.cNB .--> cNB)) c= {1} \/ EG by A7;
A9: {TG.cNB} c= VG
proof
let x be object;
assume x in {TG.cNB};
then x = TG.cNB by TARSKI:def 1;
hence thesis by A1,FUNCT_2:5;
end;
dom (VL+*(TG.cNB .--> cNB)) = dom VL \/ dom (TG.cNB .--> cNB) by
FUNCT_4:def 1
.= dom VL \/ {TG.cNB};
then
A10: VL+*(TG.cNB .--> cNB) is Relation of VG, {1} \/ EG by A9,A5,RELSET_1:4
,XBOOLE_1:8;
dom (VL+*(SG.cNB .--> cNB)) = dom VL \/ dom (SG.cNB .--> cNB) by
FUNCT_4:def 1
.= dom VL \/ {SG.cNB};
then VL+*(SG.cNB .--> cNB) is Relation of VG, {1} \/ EG by A2,A8,
RELSET_1:4,XBOOLE_1:8;
hence thesis by A10,Def5;
end;
end;
consistency;
end;
definition
let G be _Graph, EL be FF:ELabeling of G;
mode AP:VLabelingSeq of EL -> ManySortedSet of NAT means
:Def11:
for n being Nat holds it.n is AP:VLabeling of EL;
existence
proof
set f = NAT --> {};
reconsider f as ManySortedSet of NAT;
take f;
let n be Nat;
f.n = {};
then f.n is PartFunc of the_Vertices_of G, {1} \/ the_Edges_of G by
RELSET_1:12;
hence thesis by Def5;
end;
end;
definition
let G be _Graph, EL be FF:ELabeling of G;
let VS be AP:VLabelingSeq of EL, n be Nat;
redefine func VS.n -> AP:VLabeling of EL; :: redefines . (FUNCT_1, definition)
coherence by Def11;
end;
definition
let G be real-weighted WGraph, EL be FF:ELabeling of G;
let source be Vertex of G;
func AP:CompSeq(EL,source) -> AP:VLabelingSeq of EL means
:Def12:
it.0 = source .--> 1 & for n being Nat holds it.(n+1) = AP:Step(it.n);
existence
proof
defpred P[set,set,set] means ($2 is AP:VLabeling of EL & ex Gn,Gn1 being
AP:VLabeling of EL st $2 = Gn & $3 = Gn1 & Gn1 = AP:Step(Gn)) or (not $2 is
AP:VLabeling of EL & $2 = $3);
A1: rng (source .--> 1) = {1} by FUNCOP_1:8;
now
let n,x be set;
now
per cases;
suppose
x is AP:VLabeling of EL;
then reconsider Gn=x as AP:VLabeling of EL;
P[n,x,AP:Step(Gn)];
hence ex y being set st P[n,x,y];
end;
suppose
not x is AP:VLabeling of EL;
hence ex y being set st P[n,x,y];
end;
end;
hence ex y being set st P[n,x,y];
end;
then
A2: for n being Nat for x being set ex y being set st P[n,x,y];
consider IT being Function such that
A3: dom IT = NAT & IT.0 = source.--> 1 & for n being Nat
holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A2);
reconsider IT as ManySortedSet of NAT by A3,PARTFUN1:def 2,RELAT_1:def 18;
defpred P2[Nat] means IT.$1 is AP:VLabeling of EL;
A4: now
let n be Nat;
assume
A5: P2[n];
ex Gn,Gn1 being AP:VLabeling of EL st IT.n = Gn & IT.(n+1 ) = Gn1
& Gn1 = AP:Step(Gn) by A3,A5;
hence P2[n+1];
end;
dom (source .--> 1) = {source};
then
source .--> 1 is Relation of the_Vertices_of G, {1} \/ the_Edges_of G
by A1,RELSET_1:4,XBOOLE_1:7;
then
A6: P2[ 0 ] by A3,Def5;
for n being Nat holds P2[n] from NAT_1:sch 2(A6,A4);
then reconsider IT as AP:VLabelingSeq of EL by Def11;
take IT;
thus IT.0 = source.-->1 by A3;
let n be Nat;
ex Gn,Gn1 being AP:VLabeling of EL st IT.n = Gn & IT.(n+1) = Gn1 &
Gn1 = AP:Step(Gn) by A3;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be AP:VLabelingSeq of EL such that
A7: IT1.0 = source.-->1 and
A8: for n being Nat holds IT1.(n+1) = AP:Step(IT1.n) and
A9: IT2.0 = source.-->1 and
A10: for n being Nat holds IT2.(n+1) = AP:Step(IT2.n);
defpred P[Nat] means IT1.$1 = IT2.$1;
now
let n be Nat;
assume P[n];
then IT1.(n+1) = AP:Step(IT2.n) by A8
.= IT2.(n+1) by A10;
hence P[n+1];
end;
then
A11: for n being Nat st P[n] holds P[n+1];
A12: P[ 0 ] by A7,A9;
for n being Nat holds P[n] from NAT_1:sch 2(A12,A11);
then for n being object st n in NAT holds IT1.n = IT2.n;
hence IT1 = IT2 by PBOOLE:3;
end;
end;
theorem Th4:
for G being real-weighted WGraph, EL be FF:ELabeling of G, source
being Vertex of G holds dom (AP:CompSeq(EL,source).0) = {source}
proof
let G be real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of
G;
AP:CompSeq(EL,source).0 = source .--> 1 by Def12;
hence thesis;
end;
theorem Th5:
for G being real-weighted WGraph, EL being FF:ELabeling of G,
source being Vertex of G, i,j being Nat st i <= j holds dom (AP:CompSeq(EL,
source).i) c= dom (AP:CompSeq(EL,source).j)
proof
let G be real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of
G, i,j be Nat;
set CS = AP:CompSeq(EL,source);
defpred P[Nat] means dom (CS.i) c= dom (CS.(i+$1));
assume i <= j;
then consider k being Nat such that
A1: j = i+k by NAT_1:10;
A2: now
let n be Nat;
set Gn = (CS.(i+n)), Gn1 = (CS.(i+(n+1)));
set Next = AP:NextBestEdges(Gn), e = the Element of Next;
Gn1 = (CS.(i+n+1));
then
A3: Gn1 = AP:Step(Gn) by Def12;
assume
A4: P[n];
now
per cases;
suppose
Next = {};
hence P[n+1] by A4,A3,Def10;
end;
suppose
Next <> {} & not (the_Source_of G).e in dom Gn;
then Gn1 = Gn+*((the_Source_of G).e .--> e) by A3,Def10;
then dom Gn c= dom Gn1 by FUNCT_4:10;
hence P[n+1] by A4,XBOOLE_1:1;
end;
suppose
Next <> {} & (the_Source_of G).e in dom Gn;
then Gn1 = Gn+*((the_Target_of G).e .--> e) by A3,Def10;
then dom Gn c= dom Gn1 by FUNCT_4:10;
hence P[n+1] by A4,XBOOLE_1:1;
end;
end;
hence P[n+1];
end;
A5: P[ 0 ];
A6: for n being Nat holds P[n] from NAT_1:sch 2(A5,A2);
thus thesis by A6,A1;
end;
definition
let G be real-weighted WGraph, EL be FF:ELabeling of G, source be Vertex of
G;
func AP:FindAugPath(EL,source) -> AP:VLabeling of EL equals
AP:CompSeq(EL,
source).Result();
coherence
proof
set CS = AP:CompSeq(EL,source);
CS.Result() = CS.(CS.Lifespan());
hence thesis;
end;
end;
theorem Th6:
for G being _finite real-weighted WGraph, EL be FF:ELabeling of G,
source being Vertex of G holds AP:CompSeq(EL,source) is halting
proof
let G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source be
Vertex of G;
set CS = AP:CompSeq(EL,source);
now
set x = card the_Vertices_of G;
defpred P[Nat] means card dom (CS.$1) = $1+1;
assume
A1: for n being Nat holds CS.n <> CS.(n+1);
A2: now
let n be Nat;
set Gn = CS.n, Gn1 = CS.(n+1);
set Next = AP:NextBestEdges(Gn), e = the Element of Next;
A3: Gn1 = AP:Step(Gn) by Def12;
assume
A4: P[n];
now
per cases;
suppose
Next = {};
then Gn = CS.(n+1) by A3,Def10;
hence P[n+1] by A1;
end;
suppose
A5: Next <> {} & not (the_Source_of G).e in dom Gn;
then Gn1 = Gn+*((the_Source_of G).e .--> e) by A3,Def10;
then dom Gn1 = dom Gn \/ {(the_Source_of G).e} by Lm1;
hence P[n+1] by A4,A5,CARD_2:41;
end;
suppose
A6: Next <> {} & (the_Source_of G).e in dom Gn;
then Gn1 = Gn+*((the_Target_of G).e .--> e) by A3,Def10;
then
A7: dom Gn1 = dom Gn \/ {(the_Target_of G).e} by Lm1;
e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by A6,Def9;
then not (the_Target_of G).e in dom Gn by A6;
hence P[n+1] by A4,A7,CARD_2:41;
end;
end;
hence P[n+1];
end;
dom (CS.0) = {source} by Th4;
then
A8: P[ 0 ] by CARD_1:30;
for n being Nat holds P[n] from NAT_1:sch 2(A8,A2);
then card dom (CS.x) = card the_Vertices_of G + 1;
then 1+card the_Vertices_of G<=card the_Vertices_of G+0 by NAT_1:43;
hence contradiction by XREAL_1:6;
end;
hence thesis;
end;
theorem Th7:
for G being _finite real-weighted WGraph, EL being FF:ELabeling of
G, source being Vertex of G, n being Nat, v being set st v in dom (AP:CompSeq(
EL,source).n) holds (AP:CompSeq(EL,source).n).v = (AP:FindAugPath(EL,source)).v
proof
let G be _finite real-weighted WGraph, EL being FF:ELabeling of G, source be
Vertex of G, n be Nat, v be set;
set SG = the_Source_of G, TG = the_Target_of G;
set CS = AP:CompSeq(EL,source);
set L = CS.Lifespan(), GL = CS.L, GL1 = CS.(L+1);
defpred P[Nat] means
for v being set st v in dom (CS.n) holds (CS.n).v = (CS.(n+$1)).v;
defpred P2[Nat] means GL = CS.(L+$1);
A1: CS is halting by Th6;
A2: now
let k be Nat;
set Gn1 = CS.(L+k+1);
assume P2[k];
then Gn1 = AP:Step(GL) by Def12
.= GL1 by Def12;
hence P2[k+1] by A1,GLIB_000:def 56;
end;
A3: P2[ 0 ];
A4: for k being Nat holds P2[k] from NAT_1:sch 2(A3,A2);
now
let k be Nat;
assume
A5: P[k];
set Gn = CS.(n+k), Gn1 = CS.(n+k+1);
set Next = AP:NextBestEdges(Gn), e = the Element of Next;
A6: Gn1 = AP:Step(Gn) by Def12;
now
per cases;
suppose
Next = {};
then Gn1 = Gn by A6,Def10;
hence P[k+1] by A5;
end;
suppose
A7: Next <> {} & not SG.e in dom Gn;
then
A8: Gn1 = Gn+*(SG.e .--> e) by A6,Def10;
now
let v be set;
assume
A9: v in dom (CS.n);
then
A10: (CS.n).v = Gn.v by A5;
dom (CS.n) c= dom Gn by Th5,NAT_1:11;
then v <> SG.e by A7,A9;
hence (CS.n).v = Gn1.v by A8,A10,Lm4;
end;
hence P[k+1];
end;
suppose
A11: Next <> {} & SG.e in dom Gn;
then
A12: e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by Def9;
A13: Gn1 = Gn+*(TG.e .--> e) by A6,A11,Def10;
now
let v be set;
assume
A14: v in dom (CS.n);
then
A15: (CS.n).v = Gn.v by A5;
dom (CS.n) c= dom Gn by Th5,NAT_1:11;
then v <> TG.e by A11,A12,A14;
hence (CS.n).v = Gn1.v by A13,A15,Lm4;
end;
hence P[k+1];
end;
end;
hence P[k+1];
end;
then
A16: for k being Nat st P[k] holds P[k+1];
A17: P[ 0 ];
A18: for k being Nat holds P[k] from NAT_1:sch 2(A17,A16);
assume
A19: v in dom (CS.n);
now
per cases;
suppose
n <= CS.Lifespan();
then consider k being Nat such that
A20: n + k = CS.Lifespan() by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
n + k = CS.Lifespan() by A20;
hence thesis by A19,A18;
end;
suppose
CS.Lifespan() < n;
then consider k being Nat such that
A21: CS.Lifespan() + k = n by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
CS.Lifespan() + k = n by A21;
hence thesis by A4;
end;
end;
hence thesis;
end;
definition
let G be _finite real-weighted WGraph, EL be FF:ELabeling of G, 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
proof
set CS = AP:CompSeq(EL,source), FAP = AP:FindAugPath(EL,source);
defpred P[Nat] means for v being set st v in dom (CS.$1) ex P being
vertex-distinct Path of G st P is_Walk_from source,v & P is_augmenting_wrt EL &
P.vertices() c= dom (CS.$1) & for n being even Nat st n in dom P holds P.n =
FAP.(P.(n+1));
now
let n be Nat;
assume
A1: P[n];
set Gn = CS.n, Gn1 = CS.(n+1);
set Next = AP:NextBestEdges(Gn), e = the Element of Next;
A2: Gn1 = AP:Step(Gn) by Def12;
now
per cases;
suppose
Next = {};
then Gn1 = Gn by A2,Def10;
hence P[n+1] by A1;
end;
suppose
A3: Next <> {} & not (the_Source_of G).e in dom Gn;
then
A4: e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by Def9;
then
A5: 0 < EL.e by A3;
A6: e in Next by A3;
A7: Gn1 = Gn+*((the_Source_of G).e .--> e) by A2,A3,Def10;
then
A8: dom Gn1 = dom Gn \/ {(the_Source_of G).e} by Lm1;
A9: (the_Target_of G).e in dom Gn by A3,A4;
now
let v be set;
assume
A10: v in dom Gn1;
now
per cases by A8,A10,XBOOLE_0:def 3;
suppose
v in dom Gn;
then consider P being vertex-distinct Path of G such that
A11: P is_Walk_from source,v and
A12: P is_augmenting_wrt EL and
A13: P.vertices() c= dom Gn and
A14: for n being even Nat st n in dom P holds P.n = FAP.(P
.(n+1)) by A1;
take P;
dom Gn c= dom Gn1 by Th5,NAT_1:11;
hence P is_Walk_from source,v & P is_augmenting_wrt EL & P
.vertices() c= dom Gn1 & for n being even Nat st n in dom P holds P.n = FAP.(P.
(n+1)) by A11,A12,A13,A14;
end;
suppose
A15: v in {(the_Source_of G).e};
then
A16: v = (the_Source_of G).e by TARSKI:def 1;
now
consider W being vertex-distinct Path of G such that
A17: W is_Walk_from source, (the_Target_of G).e and
A18: W is_augmenting_wrt EL and
A19: W.vertices() c= dom Gn and
A20: for n being even Nat st n in dom W holds W.n = FAP.
(W.(n+1)) by A1,A9;
set W2 = W.addEdge(e);
A21: W.last() = (the_Target_of G).e by A17,GLIB_001:def 23;
then
A22: e Joins W.last(),(the_Source_of G).e,G by A6;
A23: not (the_Source_of G).e in W.vertices() by A3,A19;
then reconsider W2 as vertex-distinct Walk of G by A22,
GLIB_001:155;
take W2;
W.first() = source by A17,GLIB_001:def 23;
hence W2 is_Walk_from source,v by A16,A22,GLIB_001:63;
e DJoins (the_Source_of G).e,W.last(),G by A6,A21;
hence W2 is_augmenting_wrt EL by A5,A18,A23,Th3;
A24: W2.vertices() = W.vertices() \/ {v} by A16,A22,GLIB_001:95;
now
let x be object;
assume
A25: x in W2.vertices();
now
per cases by A24,A25,XBOOLE_0:def 3;
suppose
A26: x in W.vertices();
A27: dom Gn c= dom Gn1 by Th5,NAT_1:11;
x in dom Gn by A19,A26;
hence x in dom Gn1 by A27;
end;
suppose
x in {v};
hence x in dom Gn1 by A8,A16,XBOOLE_0:def 3;
end;
end;
hence x in dom Gn1;
end;
hence W2.vertices() c= dom Gn1;
let n be even Nat;
assume
A28: n in dom W2;
then
A29: n <= len W2 by FINSEQ_3:25;
A30: 1 <= n by A28,FINSEQ_3:25;
now
per cases;
suppose
A31: n <= len W;
then n < len W by XXREAL_0:1;
then
A32: n+1 <= len W by NAT_1:13;
1 <= 1+n by NAT_1:11;
then n+1 in dom W by A32,FINSEQ_3:25;
then
A33: W2.(n+1) = W.(n+1) by A22,GLIB_001:65;
A34: n in dom W by A30,A31,FINSEQ_3:25;
then W2.n = W.n by A22,GLIB_001:65;
hence W2.n = FAP.(W2.(n+1)) by A20,A34,A33;
end;
suppose
A35: n > len W;
n <= len W + 2*1 by A22,A29,GLIB_001:64;
then n < len W + 1+1 by XXREAL_0:1;
then
A36: n <= len W + 1 by NAT_1:13;
len W + 1 <= n by A35,NAT_1:13;
then
A37: n = len W + 1 by A36,XXREAL_0:1;
then
A38: W2.n = e by A22,GLIB_001:65;
n+1 = len W + (1+1) by A37;
then
A39: W2.(n+1) = v by A16,A22,GLIB_001:65;
A40: v in dom Gn1 by A8,A15,XBOOLE_0:def 3;
Gn1.v = e by A7,A16,Lm3;
hence W2.n = FAP.(W2.(n+1)) by A38,A39,A40,Th7;
end;
end;
hence W2.n = FAP.(W2.(n+1));
end;
hence ex P being vertex-distinct Path of G st P is_Walk_from
source,v & P is_augmenting_wrt EL & P.vertices() c=dom Gn1 & for n being even
Nat st n in dom P holds P.n = FAP.(P.(n+1));
end;
end;
hence
ex P being vertex-distinct Path of G st P is_Walk_from source
,v & P is_augmenting_wrt EL & P.vertices() c=dom Gn1 & for n being even Nat st
n in dom P holds P.n = FAP.(P.(n+1));
end;
hence P[n+1];
end;
suppose
A41: Next <> {} & (the_Source_of G).e in dom Gn;
then
A42: Gn1 = Gn+*((the_Target_of G).e .--> e) by A2,Def10;
then
A43: dom Gn1 = dom Gn \/ {(the_Target_of G).e} by Lm1;
A44: e in Next by A41;
A45: e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by A41,Def9;
then
A46: EL.e < (the_Weight_of G).e by A41;
now
let v be set;
assume
A47: v in dom Gn1;
now
per cases by A43,A47,XBOOLE_0:def 3;
suppose
v in dom Gn;
then consider P being vertex-distinct Path of G such that
A48: P is_Walk_from source,v and
A49: P is_augmenting_wrt EL and
A50: P.vertices() c= dom Gn and
A51: for n being even Nat st n in dom P holds P.n = FAP.(P
.(n+1)) by A1;
take P;
dom Gn c= dom Gn1 by Th5,NAT_1:11;
hence P is_Walk_from source,v & P is_augmenting_wrt EL & P
.vertices()c= dom Gn1 & for n being even Nat st n in dom P holds P.n = FAP.(P.(
n+1)) by A48,A49,A50,A51;
end;
suppose
A52: v in {(the_Target_of G).e};
then
A53: v = (the_Target_of G).e by TARSKI:def 1;
now
consider W being vertex-distinct Path of G such that
A54: W is_Walk_from source, (the_Source_of G).e and
A55: W is_augmenting_wrt EL and
A56: W.vertices() c= dom Gn and
A57: for n being even Nat st n in dom W holds W.n = FAP.
(W.(n+1)) by A1,A41;
set W2 = W.addEdge(e);
A58: W.last() = (the_Source_of G).e by A54,GLIB_001:def 23;
then
A59: e Joins W.last(),(the_Target_of G).e,G by A44;
A60: not (the_Target_of G).e in W.vertices() by A41,A45,A56;
then reconsider W2 as vertex-distinct Walk of G by A59,
GLIB_001:155;
take W2;
W.first() = source by A54,GLIB_001:def 23;
hence W2 is_Walk_from source,v by A53,A59,GLIB_001:63;
e DJoins W.last(),(the_Target_of G).e,G by A44,A58;
hence W2 is_augmenting_wrt EL by A46,A55,A60,Th3;
A61: W2.vertices() = W.vertices() \/ {v} by A53,A59,GLIB_001:95;
now
let x be object;
assume
A62: x in W2.vertices();
now
per cases by A61,A62,XBOOLE_0:def 3;
suppose
A63: x in W.vertices();
A64: dom Gn c= dom Gn1 by Th5,NAT_1:11;
x in dom Gn by A56,A63;
hence x in dom Gn1 by A64;
end;
suppose
x in {v};
hence x in dom Gn1 by A43,A53,XBOOLE_0:def 3;
end;
end;
hence x in dom Gn1;
end;
hence W2.vertices() c= dom Gn1;
let n be even Nat;
assume
A65: n in dom W2;
then
A66: n <= len W2 by FINSEQ_3:25;
A67: 1 <= n by A65,FINSEQ_3:25;
now
per cases;
suppose
A68: n <= len W;
then n < len W by XXREAL_0:1;
then
A69: n+1 <= len W by NAT_1:13;
1 <= 1+n by NAT_1:11;
then n+1 in dom W by A69,FINSEQ_3:25;
then
A70: W2.(n+1) = W.(n+1) by A59,GLIB_001:65;
A71: n in dom W by A67,A68,FINSEQ_3:25;
then W2.n = W.n by A59,GLIB_001:65;
hence W2.n = FAP.(W2.(n+1)) by A57,A71,A70;
end;
suppose
A72: n > len W;
n <= len W + 2*1 by A59,A66,GLIB_001:64;
then n < len W + 1+1 by XXREAL_0:1;
then
A73: n <= len W + 1 by NAT_1:13;
len W + 1 <= n by A72,NAT_1:13;
then
A74: n = len W + 1 by A73,XXREAL_0:1;
then
A75: W2.n = e by A59,GLIB_001:65;
n+1 = len W + (1+1) by A74;
then
A76: W2.(n+1) = v by A53,A59,GLIB_001:65;
A77: v in dom Gn1 by A43,A52,XBOOLE_0:def 3;
Gn1.v = e by A42,A53,Lm3;
hence W2.n = FAP.(W2.(n+1)) by A75,A76,A77,Th7;
end;
end;
hence W2.n = FAP.(W2.(n+1));
end;
hence ex P being vertex-distinct Path of G st P is_Walk_from
source,v & P is_augmenting_wrt EL & P.vertices() c=dom Gn1 & for n being even
Nat st n in dom P holds P.n = FAP.(P.(n+1));
end;
end;
hence
ex P being vertex-distinct Path of G st P is_Walk_from source
,v & P is_augmenting_wrt EL & P.vertices() c=dom Gn1 & for n being even Nat st
n in dom P holds P.n = FAP.(P.(n+1));
end;
hence P[n+1];
end;
end;
hence P[n+1];
end;
then
A78: for n being Nat st P[n] holds P[n+1];
now
set P = G.walkOf(source);
let v be set;
assume
A79: v in dom (CS.0);
take P;
v in {source} by A79,Th4;
then v = source by TARSKI:def 1;
hence P is_Walk_from source,v by GLIB_001:13;
thus P is_augmenting_wrt EL by Th1;
P.vertices() = {source} by GLIB_001:90;
hence P.vertices() c= dom (CS.0) by Th4;
let n be even Nat;
assume
A80: n in dom P;
then n <= len P by FINSEQ_3:25;
then
A81: n < len P by XXREAL_0:1;
1 <= n by A80,FINSEQ_3:25;
hence P.n = FAP.(P.(n+1)) by A81,GLIB_001:13;
end;
then
A82: P[ 0 ];
A83: for n being Nat holds P[n] from NAT_1:sch 2(A82,A78);
hereby
assume sink in dom FAP;
then consider W being vertex-distinct Path of G such that
A84: W is_Walk_from source,sink and
A85: W is_augmenting_wrt EL and
W.vertices() c= dom FAP and
A86: for n being even Nat st n in dom W holds W.n = FAP.((W.(n+1))) by A83;
take W;
thus W is_Walk_from source,sink & W is_augmenting_wrt EL & for n being
even Nat st n in dom W holds W.n = FAP.((W.(n+1))) by A84,A85,A86;
end;
thus thesis;
end;
uniqueness
proof
set FAP = AP:FindAugPath(EL,source), CS = AP:CompSeq(EL,source);
let IT1, IT2 be vertex-distinct Path of G;
defpred P[Nat] means for v being set, P1,P2 being vertex-distinct Path of
G st v in dom (CS.$1) & P1 is_Walk_from source,v & P1 is_augmenting_wrt EL & P2
is_Walk_from source,v & P2 is_augmenting_wrt EL & (for n being even Nat st n in
dom P1 holds P1.n = FAP.(P1.(n+1))) & (for n being even Nat st n in dom P2
holds P2.n = FAP.(P2.(n+1))) holds P1 = P2;
set G0 = CS.0;
now
let n be Nat;
assume
A87: P[n];
set Gn = CS.n, Gn1 = CS.(n+1);
set Next = AP:NextBestEdges(Gn), e = the Element of Next;
A88: Gn1 = AP:Step(Gn) by Def12;
now
per cases;
suppose
Next = {};
then Gn1 = Gn by A88,Def10;
hence P[n+1] by A87;
end;
suppose
A89: Next <> {} & not (the_Source_of G).e in dom Gn;
source in {source} by TARSKI:def 1;
then
A90: source in dom G0 by Th4;
dom G0 c= dom Gn by Th5;
then
A91: source in dom Gn by A90;
e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by A89,Def9;
then
A92: (the_Target_of G).e in dom Gn by A89;
A93: Gn1 = Gn+*((the_Source_of G).e .--> e) by A88,A89,Def10;
then
A94: dom Gn1 = dom Gn \/ {(the_Source_of G). e} by Lm1;
now
let v be set,P1,P2 be vertex-distinct Path of G;
assume that
A95: v in dom Gn1 and
A96: P1 is_Walk_from source,v and
A97: P1 is_augmenting_wrt EL and
A98: P2 is_Walk_from source,v and
A99: P2 is_augmenting_wrt EL and
A100: for n being even Nat st n in dom P1 holds P1.n = FAP.(P1
.(n+1)) and
A101: for n being even Nat st n in dom P2 holds P2.n = FAP.(P2 .(n+1));
A102: P1.(len P1) = v by A96,GLIB_001:17;
A103: P2.1 = source by A98,GLIB_001:17;
A104: P2.(len P2) = v by A98,GLIB_001:17;
A105: P1.1 = source by A96,GLIB_001:17;
now
per cases by A94,A95,XBOOLE_0:def 3;
suppose
v in dom Gn;
hence P1 = P2 by A87,A96,A97,A98,A99,A100,A101;
end;
suppose
A106: v in {(the_Source_of G).e};
then
A107: v = (the_Source_of G).e by TARSKI:def 1;
then Gn1.v = e by A93,Lm3;
then
A108: FAP.v = e by A95,Th7;
A109: v <> source by A89,A91,A106,TARSKI:def 1;
then P1.1 <> P1.last() by A105,A102,GLIB_001:def 7;
then P1.first() <> P1.last() by GLIB_001:def 6;
then P1 is non trivial by GLIB_001:127;
then
A110: 3 <= len P1 by GLIB_001:125;
P2.1 <> P2.last() by A103,A104,A109,GLIB_001:def 7;
then P2.first() <> P2.last() by GLIB_001:def 6;
then P2 is non trivial by GLIB_001:127;
then
A111: 3 <= len P2 by GLIB_001:125;
then
A112: 3-2 < len P2-0 by XREAL_1:15;
3-2 < len P1-0 by A110,XREAL_1:15;
then reconsider
lenP11 = len P1 - 1, lenP21 = len P2 - 1 as even
Element of NAT by A112,INT_1:5;
A113: lenP11 < len P1-0 by XREAL_1:15;
3-2 <= lenP11 by A110,XREAL_1:15;
then
A114: lenP11 in dom P1 by A113,FINSEQ_3:25;
lenP11+1 = len P1;
then
A115: P1.lenP11 = e by A100,A102,A114,A108;
then consider lenP12 being odd Element of NAT such that
A116: lenP12 = lenP11 - 1 and
lenP11-1 in dom P1 and
lenP11+1 in dom P1 and
A117: e Joins P1.lenP12,v,G by A102,A114,GLIB_001:9;
A118: P1.lenP12 = (the_Target_of G).e by A107,A117;
set P1A = P1.cut(2*0+1,lenP12);
A119: lenP12 < len P1 by A113,A116,XREAL_1:15;
A120: now
let n be even Nat;
assume
A121: n in dom P1A;
then
A122: 1 <= n by FINSEQ_3:25;
A123: n <= len P1A by A121,FINSEQ_3:25;
then n < len P1A by XXREAL_0:1;
then
A124: n+1 <= len P1A by NAT_1:13;
1 <= n+1 by A121,NAT_1:13;
then n+1 in dom P1A by A124,FINSEQ_3:25;
then
A125: P1A.(n+1) = P1.(n+1) by A119,GLIB_001:46;
len P1A = lenP12 by A119,GLIB_001:45;
then n <= len P1 by A119,A123,XXREAL_0:2;
then
A126: n in dom P1 by A122,FINSEQ_3:25;
P1A.n = P1.n by A119,A121,GLIB_001:46;
hence P1A.n = FAP.(P1A.(n+1)) by A100,A125,A126;
end;
A127: lenP12+(1+1) = len P1 by A116;
lenP12 + 1 = lenP11 by A116;
then
A128: P1.cut(lenP12,len P1) = G.walkOf(( the_Target_of G).e,e,
v) by A102,A115,A118,A119,A127,GLIB_001:40;
A129: P1A is_augmenting_wrt EL by A97,Th2;
A130: 1 <= lenP12 by ABIAN:12;
then
A131: P1A.append(P1.cut(lenP12,len P1)) = P1.cut(2*0+1, len P1
) by A119,GLIB_001:38
.= P1 by GLIB_001:39;
A132: lenP21 < len P2-0 by XREAL_1:15;
3-2 <= lenP21 by A111,XREAL_1:15;
then
A133: lenP21 in dom P2 by A132,FINSEQ_3:25;
lenP21+1 = len P2;
then
A134: P2.lenP21 = e by A101,A104,A133,A108;
then consider lenP22 being odd Element of NAT such that
A135: lenP22 = lenP21 - 1 and
lenP21-1 in dom P2 and
lenP21+1 in dom P2 and
A136: e Joins P2.lenP22,v,G by A104,A133,GLIB_001:9;
A137: lenP22+(1+1) = len P2 by A135;
set P2A = P2.cut(2*0+1,lenP22);
A138: lenP22 < len P2 by A132,A135,XREAL_1:15;
A139: now
let n be even Nat;
assume
A140: n in dom P2A;
then
A141: 1 <= n by FINSEQ_3:25;
A142: n <= len P2A by A140,FINSEQ_3:25;
then n < len P2A by XXREAL_0:1;
then
A143: n+1 <= len P2A by NAT_1:13;
1 <= n+1 by A140,NAT_1:13;
then n+1 in dom P2A by A143,FINSEQ_3:25;
then
A144: P2A.(n+1) = P2.(n+1) by A138,GLIB_001:46;
len P2A = lenP22 by A138,GLIB_001:45;
then n <= len P2 by A138,A142,XXREAL_0:2;
then
A145: n in dom P2 by A141,FINSEQ_3:25;
P2A.n = P2.n by A138,A140,GLIB_001:46;
hence P2A.n = FAP.(P2A.(n+1)) by A101,A144,A145;
end;
A146: 1 <= lenP22 by ABIAN:12;
then
A147: P2A.append(P2.cut(lenP22, len P2)) = P2.cut(2*0+1, len
P2) by A138,GLIB_001:38
.= P2 by GLIB_001:39;
A148: P2.lenP22 = (the_Target_of G).e by A107,A136;
then
A149: P2A
is_Walk_from source,(the_Target_of G).e by A103,A146,A138,GLIB_001:37;
lenP22 + 1 = lenP21 by A135;
then
A150: P2.cut(lenP22,len P2) = G.walkOf((the_Target_of G).e,e,v
) by A104,A134,A148,A138,A137,GLIB_001:40;
A151: P2A is_augmenting_wrt EL by A99,Th2;
P1A is_Walk_from source,(the_Target_of G).e by A105,A118,A130
,A119,GLIB_001:37;
hence P1 = P2 by A87,A92,A149,A129,A151,A120,A139,A128,A150
,A131,A147;
end;
end;
hence P1 = P2;
end;
hence P[n+1];
end;
suppose
A152: Next <> {} & (the_Source_of G).e in dom Gn;
source in {source} by TARSKI:def 1;
then
A153: source in dom G0 by Th4;
dom G0 c= dom Gn by Th5;
then
A154: source in dom Gn by A153;
e is_forward_edge_wrt Gn or e is_backward_edge_wrt Gn by A152,Def9;
then
A155: not (the_Target_of G).e in dom Gn by A152;
A156: Gn1 = Gn+*((the_Target_of G).e.--> e) by A88,A152,Def10;
then
A157: dom Gn1 = dom Gn \/ {(the_Target_of G). e} by Lm1;
now
let v be set,P1,P2 be vertex-distinct Path of G;
assume that
A158: v in dom Gn1 and
A159: P1 is_Walk_from source,v and
A160: P1 is_augmenting_wrt EL and
A161: P2 is_Walk_from source,v and
A162: P2 is_augmenting_wrt EL and
A163: for n being even Nat st n in dom P1 holds P1.n = FAP.(P1
.(n+1)) and
A164: for n being even Nat st n in dom P2 holds P2.n = FAP.(P2 .(n+1));
A165: P1.(len P1) = v by A159,GLIB_001:17;
A166: P2.1 = source by A161,GLIB_001:17;
A167: P2.(len P2) = v by A161,GLIB_001:17;
A168: P1.1 = source by A159,GLIB_001:17;
now
per cases by A157,A158,XBOOLE_0:def 3;
suppose
v in dom Gn;
hence P1 = P2 by A87,A159,A160,A161,A162,A163,A164;
end;
suppose
A169: v in {(the_Target_of G).e};
then
A170: v = (the_Target_of G).e by TARSKI:def 1;
then Gn1.v = e by A156,Lm3;
then
A171: FAP.v = e by A158,Th7;
A172: v <> source by A155,A154,A169,TARSKI:def 1;
then P1.1 <> P1.last() by A168,A165,GLIB_001:def 7;
then P1.first() <> P1.last() by GLIB_001:def 6;
then P1 is non trivial by GLIB_001:127;
then
A173: 3 <= len P1 by GLIB_001:125;
P2.1 <> P2.last() by A166,A167,A172,GLIB_001:def 7;
then P2.first() <> P2.last() by GLIB_001:def 6;
then P2 is non trivial by GLIB_001:127;
then
A174: 3 <= len P2 by GLIB_001:125;
then
A175: 3-2 < len P2-0 by XREAL_1:15;
3-2 < len P1-0 by A173,XREAL_1:15;
then reconsider
lenP11 = len P1 - 1, lenP21 = len P2 - 1 as even
Element of NAT by A175,INT_1:5;
A176: lenP11 < len P1-0 by XREAL_1:15;
3-2 <= lenP11 by A173,XREAL_1:15;
then
A177: lenP11 in dom P1 by A176,FINSEQ_3:25;
lenP11+1 = len P1;
then
A178: P1.lenP11 = e by A163,A165,A177,A171;
then consider lenP12 being odd Element of NAT such that
A179: lenP12 = lenP11 - 1 and
lenP11-1 in dom P1 and
lenP11+1 in dom P1 and
A180: e Joins P1.lenP12,v,G by A165,A177,GLIB_001:9;
A181: P1.lenP12 = (the_Source_of G).e by A170,A180;
set P1A = P1.cut(2*0+1,lenP12);
A182: lenP12 < len P1 by A176,A179,XREAL_1:15;
A183: now
let n be even Nat;
assume
A184: n in dom P1A;
then
A185: 1 <= n by FINSEQ_3:25;
A186: n <= len P1A by A184,FINSEQ_3:25;
then n < len P1A by XXREAL_0:1;
then
A187: n+1 <= len P1A by NAT_1:13;
1 <= n+1 by A184,NAT_1:13;
then n+1 in dom P1A by A187,FINSEQ_3:25;
then
A188: P1A.(n+1) = P1.(n+1) by A182,GLIB_001:46;
len P1A = lenP12 by A182,GLIB_001:45;
then n <= len P1 by A182,A186,XXREAL_0:2;
then
A189: n in dom P1 by A185,FINSEQ_3:25;
P1A.n = P1.n by A182,A184,GLIB_001:46;
hence P1A.n = FAP.(P1A.(n+1)) by A163,A188,A189;
end;
A190: lenP12+(1+1) = len P1 by A179;
lenP12 + 1 = lenP11 by A179;
then
A191: P1.cut(lenP12,len P1) = G.walkOf(( the_Source_of G).e,e,
v) by A165,A178,A181,A182,A190,GLIB_001:40;
A192: P1A is_augmenting_wrt EL by A160,Th2;
A193: 1 <= lenP12 by ABIAN:12;
then
A194: P1A.append(P1.cut(lenP12,len P1)) = P1.cut(2*0+1, len P1
) by A182,GLIB_001:38
.= P1 by GLIB_001:39;
A195: lenP21 < len P2-0 by XREAL_1:15;
3-2 <= lenP21 by A174,XREAL_1:15;
then
A196: lenP21 in dom P2 by A195,FINSEQ_3:25;
lenP21+1 = len P2;
then
A197: P2.lenP21 = e by A164,A167,A196,A171;
then consider lenP22 being odd Element of NAT such that
A198: lenP22 = lenP21 - 1 and
lenP21-1 in dom P2 and
lenP21+1 in dom P2 and
A199: e Joins P2.lenP22,v,G by A167,A196,GLIB_001:9;
A200: lenP22+(1+1) = len P2 by A198;
set P2A = P2.cut(2*0+1,lenP22);
A201: lenP22 < len P2 by A195,A198,XREAL_1:15;
A202: now
let n be even Nat;
assume
A203: n in dom P2A;
then
A204: 1 <= n by FINSEQ_3:25;
A205: n <= len P2A by A203,FINSEQ_3:25;
then n < len P2A by XXREAL_0:1;
then
A206: n+1 <= len P2A by NAT_1:13;
1 <= n+1 by A203,NAT_1:13;
then n+1 in dom P2A by A206,FINSEQ_3:25;
then
A207: P2A.(n+1) = P2.(n+1) by A201,GLIB_001:46;
len P2A = lenP22 by A201,GLIB_001:45;
then n <= len P2 by A201,A205,XXREAL_0:2;
then
A208: n in dom P2 by A204,FINSEQ_3:25;
P2A.n = P2.n by A201,A203,GLIB_001:46;
hence P2A.n = FAP.(P2A.(n+1)) by A164,A207,A208;
end;
A209: 1 <= lenP22 by ABIAN:12;
then
A210: P2A.append(P2.cut(lenP22, len P2)) = P2.cut(2*0+1, len
P2) by A201,GLIB_001:38
.= P2 by GLIB_001:39;
A211: P2.lenP22 = (the_Source_of G).e by A170,A199;
then
A212: P2A
is_Walk_from source,(the_Source_of G).e by A166,A209,A201,GLIB_001:37;
lenP22 + 1 = lenP21 by A198;
then
A213: P2.cut(lenP22,len P2) = G.walkOf((the_Source_of G).e,e,v
) by A167,A197,A211,A201,A200,GLIB_001:40;
A214: P2A is_augmenting_wrt EL by A162,Th2;
P1A is_Walk_from source,(the_Source_of G).e by A168,A181,A193
,A182,GLIB_001:37;
hence P1 = P2 by A87,A152,A212,A192,A214,A183,A202,A191,A213
,A194,A210;
end;
end;
hence P1 = P2;
end;
hence P[n+1];
end;
end;
hence P[n+1];
end;
then
A215: for n being Nat st P[n] holds P[n+1];
now
let v be set, P1,P2 be vertex-distinct Path of G;
assume that
A216: v in dom G0 and
A217: P1 is_Walk_from source,v and
P1 is_augmenting_wrt EL and
A218: P2 is_Walk_from source,v and
P2 is_augmenting_wrt EL and
for n being even Nat st n in dom P1 holds P1.n = FAP.(P1.(n+1)) and
for n being even Nat st n in dom P2 holds P2.n = FAP.(P2.(n+1));
v in {source} by A216,Th4;
then
A219: v = source by TARSKI:def 1;
then
A220: P1.(2*0+1) = v by A217,GLIB_001:17;
A221: P2.(2*0+1) = v by A218,A219,GLIB_001:17;
A222: 1 <= len P1 by ABIAN:12;
P1.(len P1) = v by A217,GLIB_001:17;
then len P1 = 1 by A220,A222,GLIB_001:def 29;
then
A223: P1 = <*v*> by A220,FINSEQ_1:40;
A224: 1 <= len P2 by ABIAN:12;
P2.(len P2 ) = v by A218,GLIB_001:17;
then len P2 = 1 by A221,A224,GLIB_001:def 29;
hence P1 = P2 by A221,A223,FINSEQ_1:40;
end;
then
A225: P[ 0 ];
for n being Nat holds P[n] from NAT_1:sch 2(A225,A215);
hence sink in dom FAP & (IT1 is_Walk_from source,sink & IT1
is_augmenting_wrt EL & for n being even Nat st n in dom IT1 holds IT1.n = (
AP:FindAugPath(EL,source)).(IT1.(n+1))) & (IT2 is_Walk_from source,sink & IT2
is_augmenting_wrt EL & for n being even Nat st n in dom IT2 holds IT2.n = (
AP:FindAugPath(EL,source)).(IT2.(n+1))) implies IT1 = IT2;
thus thesis;
end;
consistency;
end;
theorem Th8:
for G being real-weighted WGraph, EL being FF:ELabeling of G,
source being Vertex of G, n being Nat, v being set st v in dom (AP:CompSeq(EL,
source).n) holds ex P being Path of G st P is_augmenting_wrt EL & P
is_Walk_from source,v & P.vertices() c= dom (AP:CompSeq(EL,source).n)
proof
let G be real-weighted WGraph, EL being FF:ELabeling of G, source be Vertex
of G;
set CS = AP:CompSeq(EL,source), G0 = CS.0;
defpred P[Nat] means for v being set st v in dom (CS.$1) holds ex P being
Path of G st P is_augmenting_wrt EL & P is_Walk_from source,v & P.vertices() c=
dom (CS.$1);
A1: now
let n be Nat;
set Gn = CS.n, Gn1 = CS.(n+1);
set Next = AP:NextBestEdges(Gn), e = the Element of Next;
assume
A2: P[n];
A3: Gn1 = AP:Step(Gn) by Def12;
now
per cases;
suppose
Next = {};
then Gn1 = Gn by A3,Def10;
hence P[n+1] by A2;
end;
suppose
A4: Next <> {};
set se = (the_Source_of G).e, te = (the_Target_of G).e;
now
per cases by A4,Def9;
suppose
A5: e is_forward_edge_wrt Gn;
then
A6: EL.e < (the_Weight_of G).e;
let v be set;
assume
A7: v in dom Gn1;
A8: e in the_Edges_of G by A5;
then
A9: e DJoins se,te,G;
A10: se in dom Gn by A5;
then Gn1 = Gn+*(te .--> e) by A3,A4,Def10;
then
A11: dom Gn1 = dom Gn \/ {te} by Lm1;
te in {te} by TARSKI:def 1;
then
A12: te in dom Gn1 by A11,XBOOLE_0:def 3;
A13: dom Gn c= dom Gn1 by A11,XBOOLE_1:7;
then
A14: se in dom Gn1 by A10;
now
per cases by A11,A7,XBOOLE_0:def 3;
suppose
v in dom Gn;
then consider P being Path of G such that
A15: P is_augmenting_wrt EL and
A16: P is_Walk_from source,v and
A17: P.vertices() c= dom Gn by A2;
take P;
thus P is_augmenting_wrt EL & P is_Walk_from source,v & P
.vertices() c= dom Gn1 by A13,A15,A16,A17;
end;
suppose
v in {te};
then
A18: v = te by TARSKI:def 1;
now
per cases;
suppose
A19: se = source;
set P = G.walkOf(se,e,te);
take P;
A20: e Joins se,te,G by A8;
now
let n be odd Nat;
assume n < len P;
then n < 2+1 by A20,GLIB_001:14;
then n <= 2*1 by NAT_1:13;
then n < 1+1 by XXREAL_0:1;
then
A21: n <= 1 by NAT_1:13;
1 <= n by ABIAN:12;
then
A22: n = 1 by A21,XXREAL_0:1;
A23: P = <*se,e,te*> by A20,GLIB_001:def 5;
then
A24: P.n = se by A22;
A25: P.(n+ 2) = te by A22,A23;
A26: P.(n+1) = e by A22,A23;
hence
P.(n+1) DJoins P.n,P.(n+2),G implies EL.(P.(n+1)) <
(the_Weight_of G).(P.(n+1)) by A5;
assume not P.(n+1) DJoins P.n,P.(n+2),G;
hence 0 < EL.(P.(n+1)) by A8,A24,A26,A25;
end;
hence P is_augmenting_wrt EL;
thus P is_Walk_from source,v by A18,A19,A20,GLIB_001:15;
now
let x be object;
assume x in P.vertices();
then x in {se,te} by A20,GLIB_001:91;
hence x in dom Gn1 by A12,A14,TARSKI:def 2;
end;
hence P.vertices() c= dom Gn1;
end;
suppose
A27: se <> source;
A28: e Joins se,v,G by A8,A18;
consider P being Path of G such that
A29: P is_augmenting_wrt EL and
A30: P is_Walk_from source,se and
A31: P.vertices() c= dom Gn by A2,A10;
set P2 = P.addEdge(e);
A32: not v in P.vertices() by A5,A18,A31;
A33: se = P.last() by A30,GLIB_001:def 23;
then P.first() <> P.last() by A27,A30,GLIB_001:def 23;
then P is open by GLIB_001:def 24;
then reconsider P2 as Path of G by A28,A33,A32,GLIB_001:151
;
take P2;
thus P2 is_augmenting_wrt EL by A6,A9,A18,A29,A33,A32,Th3;
thus P2 is_Walk_from source,v by A30,A28,GLIB_001:66;
now
let x be object;
assume x in P2.vertices();
then
A34: x in P.vertices()\/{te} by A28,A33,GLIB_001:95;
now
per cases by A34,XBOOLE_0:def 3;
suppose
x in P.vertices();
then x in dom Gn by A31;
hence x in dom Gn1 by A13;
end;
suppose
x in {te};
hence x in dom Gn1 by A11,XBOOLE_0:def 3;
end;
end;
hence x in dom Gn1;
end;
hence P2.vertices() c= dom Gn1;
end;
end;
hence ex P being Path of G st P is_augmenting_wrt EL & P
is_Walk_from source,v & P.vertices() c= dom Gn1;
end;
end;
hence ex P being Path of G st P is_augmenting_wrt EL & P
is_Walk_from source,v & P.vertices() c= dom Gn1;
end;
suppose
A35: e is_backward_edge_wrt Gn;
then
A36: 0 < EL.e;
let v be set;
assume
A37: v in dom Gn1;
A38: e in the_Edges_of G by A35;
then
A39: e DJoins se,te,G;
A40: not se in dom Gn by A35;
then Gn1 = Gn+*(se .--> e) by A3,A4,Def10;
then
A41: dom Gn1 = dom Gn \/ {se} by Lm1;
se in {se} by TARSKI:def 1;
then
A42: se in dom Gn1 by A41,XBOOLE_0:def 3;
A43: te in dom Gn by A35;
A44: dom Gn c= dom Gn1 by A41,XBOOLE_1:7;
then
A45: te in dom Gn1 by A43;
now
per cases by A41,A37,XBOOLE_0:def 3;
suppose
v in dom Gn;
then consider P being Path of G such that
A46: P is_augmenting_wrt EL and
A47: P is_Walk_from source,v and
A48: P.vertices() c= dom Gn by A2;
take P;
thus P is_augmenting_wrt EL & P is_Walk_from source,v & P
.vertices() c= dom Gn1 by A44,A46,A47,A48;
end;
suppose
v in {se};
then
A49: v = se by TARSKI:def 1;
now
per cases;
suppose
A50: te = source;
set P = G.walkOf(te,e,se);
take P;
A51: e Joins te,se,G by A38;
now
let n be odd Nat;
assume n < len P;
then n < 2+1 by A51,GLIB_001:14;
then n <= 2*1 by NAT_1:13;
then n < 1+1 by XXREAL_0:1;
then
A52: n <= 1 by NAT_1:13;
1 <= n by ABIAN:12;
then
A53: n = 1 by A52,XXREAL_0:1;
A54: P = <*te,e,se*> by A51,GLIB_001:def 5;
then
A55: P.(n+1) = e by A53;
P.n = te by A53,A54;
hence
P.(n+1) DJoins P.n,P.(n+2),G implies EL.(P.(n+1)) <
(the_Weight_of G).(P.(n+1)) by A43,A40,A55;
assume not P.(n+1) DJoins P.n,P.(n+2),G;
thus 0 < EL.(P.(n+1)) by A35,A55;
end;
hence P is_augmenting_wrt EL;
thus P is_Walk_from source,v by A49,A50,A51,GLIB_001:15;
now
let x be object;
assume x in P.vertices();
then x in {se,te} by A51,GLIB_001:91;
hence x in dom Gn1 by A42,A45,TARSKI:def 2;
end;
hence P.vertices() c= dom Gn1;
end;
suppose
A56: te <> source;
A57: e Joins te,v,G by A38,A49;
consider P being Path of G such that
A58: P is_augmenting_wrt EL and
A59: P is_Walk_from source,te and
A60: P.vertices() c= dom Gn by A2,A43;
set P2 = P.addEdge(e);
A61: not v in P.vertices() by A35,A49,A60;
A62: te = P.last() by A59,GLIB_001:def 23;
then P.first() <> P.last() by A56,A59,GLIB_001:def 23;
then P is open by GLIB_001:def 24;
then reconsider P2 as Path of G by A57,A62,A61,GLIB_001:151
;
take P2;
thus P2 is_augmenting_wrt EL by A36,A39,A49,A58,A62,A61,Th3
;
thus P2 is_Walk_from source,v by A59,A57,GLIB_001:66;
now
let x be object;
assume x in P2.vertices();
then
A63: x in P.vertices()\/{se} by A57,A62,GLIB_001:95;
now
per cases by A63,XBOOLE_0:def 3;
suppose
x in P.vertices();
then x in dom Gn by A60;
hence x in dom Gn1 by A44;
end;
suppose
x in {se};
hence x in dom Gn1 by A41,XBOOLE_0:def 3;
end;
end;
hence x in dom Gn1;
end;
hence P2.vertices() c= dom Gn1;
end;
end;
hence ex P being Path of G st P is_augmenting_wrt EL & P
is_Walk_from source,v & P.vertices() c= dom Gn1;
end;
end;
hence ex P being Path of G st P is_augmenting_wrt EL & P
is_Walk_from source,v & P.vertices() c= dom Gn1;
end;
end;
hence P[n+1];
end;
end;
hence P[n+1];
end;
now
let v be set;
assume
A64: v in dom G0;
then reconsider v9=v as Vertex of G;
set P = G.walkOf(v9);
take P;
thus P is_augmenting_wrt EL by Th1;
v in {source} by A64,Th4;
then v = source by TARSKI:def 1;
hence P is_Walk_from source,v by GLIB_001:13;
P.vertices() = {v9} by GLIB_001:90;
hence P.vertices() c= dom G0 by A64,ZFMISC_1:31;
end;
then
A65: P[ 0 ];
for n being Nat holds P[n] from NAT_1:sch 2(A65,A1);
hence thesis;
end;
theorem Th9:
for G being _finite real-weighted WGraph, EL being FF:ELabeling of
G, source being Vertex of G, v being set holds v in dom AP:FindAugPath(EL,
source) iff ex P being Path of G st P is_Walk_from source,v & P
is_augmenting_wrt EL
proof
let G be _finite real-weighted WGraph, EL be FF:ELabeling of G, source be
Vertex of G, v be set;
set CS = AP:CompSeq(EL,source), V = dom AP:FindAugPath(EL,source);
hereby
assume v in V;
then ex P being Path of G st P is_augmenting_wrt EL & P is_Walk_from
source,v & P.vertices() c= V by Th8;
hence
ex P being Path of G st P is_Walk_from source,v & P is_augmenting_wrt EL;
end;
given P being Path of G such that
A1: P is_Walk_from source,v and
A2: P is_augmenting_wrt EL;
now
P.(2*0+1) = source by A1,GLIB_001:17;
then P.(2*0+1) in {source} by TARSKI:def 1;
then
A3: P.(2*0+1) in dom (CS.0) by Th4;
set Gn = CS.(CS.Lifespan()), Gn1 = CS.(CS.Lifespan()+1);
defpred P[Nat] means $1 is odd & $1 <= len P & not P.$1 in V;
assume
A4: not v in V;
P.(len P) = v by A1,GLIB_001:17;
then
A5: ex n being Nat st P[n] by A4;
consider n being Nat such that
A6: P[n] & for k being Nat st P[k] holds n <= k from NAT_1:sch 5(A5);
reconsider n9=n as odd Element of NAT by A6,ORDINAL1:def 12;
A7: 1 <= n by A6,ABIAN:12;
dom (CS.0) c= V by Th5;
then n <> 1 by A6,A3;
then 1 < n by A7,XXREAL_0:1;
then 1+1 <= n by NAT_1:13;
then reconsider n2 = n9-2*1 as odd Element of NAT by INT_1:5;
A8: n2 < n - 0 by XREAL_1:15;
then
A9: n2 < len P by A6,XXREAL_0:2;
then
A10: P.n2 in V by A6,A8;
set Next = AP:NextBestEdges(Gn), en = the Element of Next;
AP:CompSeq(EL,source) is halting by Th6;
then
A11: Gn = CS.(CS.Lifespan()+1) by GLIB_000:def 56;
set e = P.(n2+1);
A12: P.(n2+2) = P.n;
then
A13: e Joins P.n2, P.n, G by A9,GLIB_001:def 3;
A14: now
per cases;
suppose
A15: e DJoins P.n2, P.n, G;
then
A16: (the_Source_of G).e in dom Gn by A10;
A17: e in the_Edges_of G by A15;
A18: not (the_Target_of G).e in dom Gn by A6,A15;
(EL).e<(the_Weight_of G).e by A2,A9,A12,A15;
then e is_forward_edge_wrt Gn by A17,A16,A18;
hence Next <> {} by Def9;
end;
suppose
A19: not e DJoins P.n2,P.n, G;
then
A20: e DJoins P.n,P.n2,G by A13;
then
A21: e in the_Edges_of G;
A22: (the_Target_of G).e in dom Gn by A10,A20;
A23: not (the_Source_of G).e in dom Gn by A6,A20;
0 < (EL).e by A2,A9,A12,A19;
then e is_backward_edge_wrt Gn by A21,A23,A22;
hence Next <> {} by Def9;
end;
end;
A24: Gn1 = AP:Step(Gn) by Def12;
now
per cases;
suppose
A25: not (the_Source_of G).en in dom Gn;
then Gn = Gn+*((the_Source_of G).en .--> en) by A24,A11,A14,Def10;
then
A26: dom Gn = dom Gn \/ {(the_Source_of G).en} by Lm1;
(the_Source_of G).en in {(the_Source_of G).en} by TARSKI:def 1;
hence contradiction by A25,A26,XBOOLE_0:def 3;
end;
suppose
A27: (the_Source_of G).en in dom Gn;
en is_forward_edge_wrt Gn or en is_backward_edge_wrt Gn by A14,Def9;
then
A28: not (the_Target_of G).en in dom Gn by A27;
Gn = Gn+*((the_Target_of G).en .--> en) by A24,A11,A14,A27,Def10;
then
A29: dom Gn = dom Gn \/ {(the_Target_of G).en} by Lm1;
(the_Target_of G).en in {(the_Target_of G).en} by TARSKI:def 1;
hence contradiction by A28,A29,XBOOLE_0:def 3;
end;
end;
hence contradiction;
end;
hence thesis;
end;
theorem Th10:
for G being _finite real-weighted WGraph, EL being FF:ELabeling
of G, source being Vertex of G holds source in dom AP:FindAugPath(EL,source)
proof
let G be _finite real-weighted WGraph, EL being FF:ELabeling of G, source be
Vertex of G;
set CS = AP:CompSeq(EL,source);
dom (CS.0) = {source} by Th4;
then
A1: source in dom (CS.0) by TARSKI:def 1;
dom (CS.0) c= dom AP:FindAugPath(EL,source) by Th5;
hence thesis by A1;
end;
begin :: Ford-Fulkerson Algorithm definitions
definition
let G be natural-weighted WGraph, EL be FF:ELabeling of G, W be Walk of G;
assume
A1: W is_augmenting_wrt EL;
defpred P[Nat,object] 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
proof
now
let k be Nat;
assume k in Seg len W.edgeSeq();
now
per cases;
suppose
W.(2*k) DJoins W.(2*k-1),W.(2*k+1),G;
hence ex x being set st P[k,x];
end;
suppose
not W.(2*k) DJoins W.(2*k-1),W.(2*k+1),G;
hence ex x being set st P[k,x];
end;
end;
hence ex x being object st P[k,x];
end;
then
A2: for k being Nat st k in Seg len W.edgeSeq() ex x being object st P[k, x];
consider IT being FinSequence such that
A3: dom IT = Seg len W.edgeSeq() and
A4: for k being Nat st k in Seg len W.edgeSeq() holds P[k,IT.k] from
FINSEQ_1:sch 1(A2);
now
let y be object;
assume y in rng IT;
then consider x being object such that
A5: x in dom IT and
A6: IT.x = y by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A5;
per cases;
suppose
A7: W.(2*n) DJoins W.(2*n-1),W.(2*n+1),G;
n in dom W.edgeSeq() by A3,A5,FINSEQ_1:def 3;
then
A8: 2*n in dom W by GLIB_001:78;
then 1 <= 2*n by FINSEQ_3:25;
then reconsider 2n1 = 2*n-1 as odd Element of NAT by INT_1:5;
2*n <= len W by A8,FINSEQ_3:25;
then
A9: 2n1 < len W - 0 by XREAL_1:15;
A10: 2n1+(1+1) = 2*n+1;
A11: IT.n = (the_Weight_of G).(W.(2*n))-EL.(W.(2*n)) by A3,A4,A5,A7;
2n1+1 = 2*n;
then EL.(W.(2*n)) < (the_Weight_of G).(W.(2*n)) by A1,A7,A9,A10;
hence y in NAT by A6,A11,INT_1:5;
end;
suppose
not W.(2*n) DJoins W.(2*n-1),W.(2*n+1),G;
then IT.n = EL.(W.(2*n)) by A3,A4,A5;
hence y in NAT by A6,ORDINAL1:def 12;
end;
end;
then rng IT c= NAT;
then reconsider IT as FinSequence of NAT by FINSEQ_1:def 4;
take IT;
thus dom IT = dom W.edgeSeq() by A3,FINSEQ_1:def 3;
let n be Nat;
assume n in dom IT;
hence thesis by A3,A4;
end;
uniqueness
proof
let IT1,IT2 be FinSequence of NAT such that
A12: dom IT1 = dom W.edgeSeq() and
A13: for n being Nat st n in dom IT1 holds P[n,IT1.n] and
A14: dom IT2 = dom W.edgeSeq() and
A15: for n being Nat st n in dom IT2 holds P[n,IT2.n];
now
let n be Nat;
assume
A16: n in dom IT1;
now
per cases;
suppose
A17: W.(2*n) DJoins W.(2*n-1),W.(2*n+1),G;
then IT1.n = (the_Weight_of G).(W.(2*n))-EL.(W.(2* n)) by A13,A16;
hence IT1.n = IT2.n by A12,A14,A15,A16,A17;
end;
suppose
A18: not W.(2*n) DJoins W.(2*n-1),W.(2*n+1),G;
then IT1.n = EL.(W.(2*n)) by A13,A16;
hence IT1.n = IT2.n by A12,A14,A15,A16,A18;
end;
end;
hence IT1.n = IT2.n;
end;
hence IT1 = IT2 by A12,A14,FINSEQ_1:13;
end;
end;
definition
let G be natural-weighted WGraph, EL being FF:ELabeling of G, W be Walk of G;
assume
A1: W is_augmenting_wrt EL;
func W.tolerance(EL) -> Nat means
:Def16:
it in rng (W.flowSeq(EL)) & for k
being Real st k in rng (W.flowSeq(EL)) holds it <= k if W is non trivial
otherwise it = 0;
existence
proof
set D = rng (W.flowSeq(EL));
now
assume W is non trivial;
then W.edges() <> {} by GLIB_001:136;
then rng W.edgeSeq() <> {} by GLIB_001:def 17;
then consider y being object such that
A2: y in rng W.edgeSeq() by XBOOLE_0:def 1;
consider x being object such that
A3: x in dom W.edgeSeq() and
y = W.edgeSeq().x by A2,FUNCT_1:def 3;
x in dom (W.flowSeq(EL)) by A1,A3,Def15;
then (W.flowSeq(EL)).x in D by FUNCT_1:def 3;
then reconsider D as non empty finite Subset of NAT;
deffunc F(Nat) = $1;
consider IT being Element of D such that
A4: for k being Element of D holds F(IT) <= F(k) from PRE_CIRC:sch 5;
reconsider IT as Nat;
take IT;
thus IT in rng (W.flowSeq(EL));
let k be Real;
assume k in rng (W.flowSeq(EL));
hence IT <= k by A4;
end;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be Nat;
hereby
assume W is non trivial;
assume that
A5: IT1 in rng (W.flowSeq(EL)) and
A6: for k being Real st k in rng (W.flowSeq(EL)) holds IT1 <= k;
assume that
A7: IT2 in rng (W.flowSeq(EL)) and
A8: for k being Real st k in rng (W.flowSeq(EL)) holds IT2 <= k;
A9: IT2 <= IT1 by A5,A8;
IT1 <= IT2 by A6,A7;
hence IT1 = IT2 by A9,XXREAL_0:1;
end;
thus thesis;
end;
consistency;
end;
definition
let G be natural-weighted WGraph, EL being FF:ELabeling of G, 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
proof
defpred P[object,object] means
($1 in the_Edges_of G & not $1 in P.edges()
implies $2 = EL.$1) & (for n being odd Element of NAT st n < len P & $1 = P.(n+
1) holds ((P.(n+1) DJoins P.n,P.(n+2),G) implies $2 = EL.(P.(n+1)) + P
.tolerance(EL)) & (not P.(n+1) DJoins P.n,P.(n+2),G implies $2 = EL.(P.(n+1)) -
P.tolerance(EL)));
now
let x be object;
assume x in the_Edges_of G;
now
per cases;
suppose
A2: not x in P.edges();
set y = EL.x;
for n being odd Element of NAT st n < len P & x = P.(n+1) holds
( P.(n+1) DJoins P.n,P.(n+2),G implies y = EL.(P.(n+1)) + P.tolerance(EL)) & (
not P.(n+1) DJoins P.n,P.(n+2),G implies y = EL.(P.(n+1)) - P.tolerance(EL))
by A2,GLIB_001:100;
hence ex y being set st P[x,y];
end;
suppose
A3: x in P.edges();
then consider n being odd Element of NAT such that
A4: n < len P and
A5: P.(n+1) = x by GLIB_001:100;
A6: 1 <= n+1 by NAT_1:11;
A7: n+1 <= len P by A4,NAT_1:13;
now
per cases;
suppose
A8: P.(n+1) DJoins P.n,P.(n+2),G;
set y = EL.(P.(n+1)) + P.tolerance(EL);
now
thus x in the_Edges_of G & not x in P.edges() implies y = EL.x
by A3;
let m be odd Element of NAT such that
A9: m < len P and
A10: P.(m+1) = x;
1 <= m+1 by NAT_1:11;
then
A11: n+1 <= m+1 by A5,A7,A10,GLIB_001:138;
thus P.(m+1) DJoins P.m,P.(m+2),G implies y = y;
assume
A12: not P.(m+1) DJoins P.m,P.(m+2),G;
m+1 <= len P by A9,NAT_1:13;
then m+1 <= n+1 by A5,A6,A10,GLIB_001:138;
then m+1 = n+1 by A11,XXREAL_0:1;
hence y = EL.(P.(m+1)) - P.tolerance(EL) by A8,A12;
end;
then P[x,y] by A5;
hence ex y being set st P[x,y];
end;
suppose
A13: not P.(n+1) DJoins P.n,P.(n+2),G;
set y =EL.(P.(n+1)) - P.tolerance(EL);
now
thus x in the_Edges_of G & not x in P.edges() implies y = EL.x
by A3;
let m be odd Element of NAT such that
A14: m < len P and
A15: P.(m+1) = x;
1 <= m+1 by NAT_1:11;
then
A16: n+1 <= m+1 by A5,A7,A15,GLIB_001:138;
m+1 <= len P by A14,NAT_1:13;
then m+1 <= n+1 by A5,A6,A15,GLIB_001:138;
then m+1 = n+1 by A16,XXREAL_0:1;
hence
P.(m+1) DJoins P.m,P.(m+2),G implies y = EL.(P.(n+1)) + P
.tolerance(EL) by A13;
assume not P.(m+1) DJoins P.m,P.(m+2),G;
thus y = EL.(P.(n+1)) - P.tolerance(EL);
end;
then P[x,y] by A5;
hence ex y being set st P[x,y];
end;
end;
hence ex y being set st P[x,y];
end;
end;
hence ex y being object st P[x,y];
end;
then
A17: for x being object st x in the_Edges_of G
ex y being object st P[ x,y ];
consider IT being Function such that
A18: dom IT = the_Edges_of G and
A19: for e being object st e in the_Edges_of G holds P[e,IT.e] from
CLASSES1:sch 1(A17);
rng IT c= NAT
proof
let y be object;
assume y in rng IT;
then consider e being object such that
A20: e in dom IT and
A21: IT.e = y by FUNCT_1:def 3;
now
per cases;
suppose
not e in P.edges();
then y = EL.e by A18,A19,A20,A21;
hence thesis by ORDINAL1:def 12;
end;
suppose
A22: e in P.edges();
then consider n being odd Element of NAT such that
A23: n < len P and
A24: P.(n+1) = e by GLIB_001:100;
A25: P is non trivial by A22,GLIB_001:136;
now
per cases;
suppose
P.(n+1) DJoins P.n, P.(n+2), G;
then
y = EL.(P.(n+1))+P.tolerance(EL) by A19,A21,A23,A24;
hence thesis by ORDINAL1:def 12;
end;
suppose
A26: not P.(n+1) DJoins P.n,P.(n+2),G;
set n1div2 = (n+1) div 2;
A27: 1 <= n+1 by NAT_1:11;
n+1 <= len P by A23,NAT_1:13;
then n1div2 in dom P.edgeSeq() by A27,GLIB_001:77;
then
A28: n1div2 in dom (P.flowSeq(EL)) by A1,Def15;
2 divides n+1 by PEPIN:22;
then
A29: 2*n1div2 = n+1 by NAT_D:3;
then
A30: 2*n1div2+1 = n+(1+1);
2*n1div2-1 = n by A29;
then (P.flowSeq(EL)).n1div2 = EL.e by A1,A24,A26,A28,A30,Def15;
then EL.e in rng (P.flowSeq(EL)) by A28,FUNCT_1:def 3;
then
A31: P.tolerance(EL) <= EL.e by A1,A25,Def16;
y = EL.e-P.tolerance(EL) by A18,A19,A20,A21,A23,A24,A26;
hence thesis by A31,INT_1:5;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then reconsider
IT as natural-valued ManySortedSet of the_Edges_of G by A18,PARTFUN1:def 2
,RELAT_1:def 18,VALUED_0:def 6;
take IT;
thus for e being set st e in the_Edges_of G & not e in P.edges() holds IT.
e = EL.e by A19;
let n be odd Nat;
reconsider n9 = n as odd Element of NAT by ORDINAL1:def 12;
A32: n9 = n;
assume
A33: n < len P;
then P.(n+1) Joins P.n, P.(n9+2), G by GLIB_001:def 3;
then
A34: P.(n+1) in the_Edges_of G;
thus P.(n+1) DJoins P.n,P.(n+2),G implies IT.(P.(n+1)) = EL.(P.(n+1)) + P
.tolerance(EL) by A19,A32,A33;
assume not P.(n+1) DJoins P.n, P.(n+2), G;
hence thesis by A19,A32,A33,A34;
end;
uniqueness
proof
let IT1,IT2 be FF:ELabeling of G such that
A35: for e being set st e in the_Edges_of G & not e in P.edges() holds
IT1. e = EL.e and
A36: for n being odd Nat st n < len P holds (P.(n+1) DJoins P.n, P.(n+
2 ),G implies IT1.(P.(n+1)) = EL.(P.(n+1)) + P.tolerance(EL)) & (not P.(n+1)
DJoins P.n,P.(n+2),G implies IT1.(P.(n+1)) = EL.(P.(n+1)) - P.tolerance(EL))
and
A37: for e being set st e in the_Edges_of G & not e in P.edges() holds
IT2.e = EL.e and
A38: for n being odd Nat st n < len P holds (P.(n+1) DJoins P.n, P.(n+
2 ),G implies IT2.(P.(n+1)) = EL.(P.(n+1)) + P.tolerance(EL)) & (not P.(n+1)
DJoins P.n,P.(n+2),G implies IT2.(P.(n+1)) = EL.(P.(n+1)) - P.tolerance(EL));
now
let e be object;
assume
A39: e in the_Edges_of G;
now
per cases;
suppose
A40: not e in P.edges();
then IT1.e = EL.e by A35,A39;
hence IT1.e = IT2.e by A37,A39,A40;
end;
suppose
e in P.edges();
then consider n being odd Element of NAT such that
A41: n < len P and
A42: P.(n+1) = e by GLIB_001:100;
now
per cases;
suppose
A43: P.(n+1) DJoins P.n,P.(n+2),G;
then IT1.e = EL.(P.(n+1)) + P.tolerance(EL) by A36,A41,A42;
hence IT1.e = IT2.e by A38,A41,A42,A43;
end;
suppose
A44: not P.(n+1) DJoins P.n,P.(n+2),G;
then IT1.e = EL.(P.(n+1)) - P.tolerance(EL) by A36,A41,A42;
hence IT1.e = IT2.e by A38,A41,A42,A44;
end;
end;
hence IT1.e = IT2.e;
end;
end;
hence IT1.e = IT2.e;
end;
hence thesis by PBOOLE:3;
end;
end;
definition
let G be _finite natural-weighted WGraph, EL being FF:ELabeling of G, 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;
end;
definition
let G be _Graph;
mode FF:ELabelingSeq of G -> ManySortedSet of NAT means
:Def19:
for n being Nat holds it.n is FF:ELabeling of G;
existence
proof
take NAT --> (the_Edges_of G --> 0);
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by FUNCOP_1:7;
end;
end;
registration
let G be _Graph, ES be FF:ELabelingSeq of G, n be Nat;
cluster ES.n -> Function-like Relation-like;
coherence by Def19;
end;
registration
let G be _Graph, ES be FF:ELabelingSeq of G, n be Nat;
cluster ES.n -> the_Edges_of G -defined;
coherence by Def19;
end;
registration
let G be _Graph, ES be FF:ELabelingSeq of G, n be Nat;
cluster ES.n -> natural-valued total;
coherence by Def19;
end;
definition
let G be _finite natural-weighted WGraph, 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
proof
defpred P[set,set,set] means (ex e being FF:ELabeling of G st e = $2 & $3
= FF:Step(e,source,sink)) or (not ex e being FF:ELabeling of G st e = $2) & $3
= $2;
now
let n,x be set;
now
per cases;
suppose
ex e being FF:ELabeling of G st e = x;
then consider e being FF:ELabeling of G such that
A1: e = x;
set y = FF:Step(e,source,sink);
P[n,x,y] by A1;
hence ex y being set st P[n,x,y];
end;
suppose
not ex e being FF:ELabeling of G st e = x;
hence ex y being set st P[n,x,y];
end;
end;
hence ex y being set st P[n,x,y];
end;
then
A2: for n being Nat for x being set ex y being set st P[n,x,y];
consider IT being Function such that
A3: dom IT = NAT & IT.0 = the_Edges_of G --> 0 &
for n being Nat holds P[n,IT.n,IT.(n+1)] from RECDEF_1:sch 1(A2);
reconsider IT as ManySortedSet of NAT by A3,PARTFUN1:def 2,RELAT_1:def 18;
defpred P2[Nat] means ex Gn being FF:ELabeling of G st IT.$1 = Gn;
A4: now
let n be Nat;
assume P2[n];
then consider Gn being FF:ELabeling of G such that
A5: IT.n = Gn;
P[n,Gn,IT.(n+1)] by A3,A5;
hence P2[n+1];
end;
A6: P2[ 0 ] by A3;
A7: for n being Nat holds P2[n] from NAT_1:sch 2(A6,A4);
now
let n be Nat;
ex Gn being FF:ELabeling of G st IT.n = Gn by A7;
hence IT.n is FF:ELabeling of G;
end;
then reconsider IT as FF:ELabelingSeq of G by Def19;
take IT;
thus IT.0 = the_Edges_of G --> 0 by A3;
let n be Nat;
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
ex X being FF:ELabeling of G st X = IT.n & IT.(n9+1) = FF:Step(X,
source,sink) by A3;
hence thesis;
end;
uniqueness
proof
let IT1,IT2 be FF:ELabelingSeq of G such that
A8: IT1.0 = the_Edges_of G --> 0 and
A9: for n being Nat holds IT1.(n+1) = FF:Step(IT1.n,source,sink) and
A10: IT2.0 = the_Edges_of G --> 0 and
A11: for n being Nat holds IT2.(n+1) = FF:Step(IT2.n,source,sink);
defpred P[Nat] means IT1.$1 = IT2.$1;
A12: now
let n be Nat;
assume
A13: P[n];
IT2.(n+1) = FF:Step(IT2.n,source,sink) by A11;
hence P[n+1] by A9,A13;
end;
A14: P[ 0 ] by A8,A10;
for n being Nat holds P[n] from NAT_1:sch 2(A14,A12);
then for n being object st n in NAT holds IT1.n = IT2.n;
hence IT1 = IT2 by PBOOLE:3;
end;
end;
definition
let G be _finite natural-weighted WGraph, sink,source be Vertex of G;
func FF:MaxFlow(G,source, sink) -> FF:ELabeling of G equals
FF:CompSeq(G,source,sink).Result();
coherence;
end;
begin :: Ford Fulkerson Maximum Flow Theorems
theorem Th11:
for G being _finite real-weighted WGraph, EL being FF:ELabeling
of G, source, sink being set, V being Subset of the_Vertices_of G st EL
has_valid_flow_from source,sink & source in V & not sink in V holds EL.flow(
source,sink) = Sum (EL | G.edgesDBetween(V, the_Vertices_of G \ V)) - Sum (EL |
G.edgesDBetween(the_Vertices_of G \ V, V))
proof
let G be _finite real-weighted WGraph, EL being FF:ELabeling of G, source,
sink be set, V be Subset of the_Vertices_of G;
assume that
A1: EL has_valid_flow_from source,sink and
A2: source in V and
A3: not sink in V;
set VG = the_Vertices_of G;
set n = card (VG \ V);
A4: now
assume n = 0;
then
A5: VG \ V = {};
sink is Vertex of G by A1;
hence contradiction by A3,A5,XBOOLE_0:def 5;
end;
defpred P[Nat] means for V being Subset of VG st card (VG \ V) = $1 & source
in V & not sink in V holds EL.flow(source,sink) = Sum (EL | G.edgesDBetween(V,
VG \ V)) - Sum (EL | G.edgesDBetween(VG \ V, V));
set TG = the_Target_of G;
set SG = the_Source_of G;
A6: now
let n be non zero Nat;
assume
A7: P[n];
now
let V2 be Subset of VG;
assume that
A8: card (VG\V2) = n+1 and
A9: source in V2 and
A10: not sink in V2;
set x = the Element of (VG \ V2) \ {sink};
set V1 = V2 \/ {x};
set EV1V1a = G.edgesDBetween(V1, VG \ V1);
set EV1V1b = G.edgesDBetween(VG \ V1, V1);
set EXV1c = G.edgesDBetween({x},VG\V1);
set EV1Xd = G.edgesDBetween(VG\V1,{x});
sink is Vertex of G by A1;
then sink in (VG \ V2) by A10,XBOOLE_0:def 5;
then {sink} c= (VG \ V2) by ZFMISC_1:31;
then
A11: card ((VG\V2)\{sink}) = n+1-card {sink} by A8,CARD_2:44
.= n+1-1 by CARD_1:30
.= n;
then
A12: x in (VG)\V2 by CARD_1:27,XBOOLE_0:def 5;
then {x} c= VG by ZFMISC_1:31;
then reconsider V1 as Subset of VG by XBOOLE_1:8;
A13: VG \ V1 = (VG \ V2) \ {x} by XBOOLE_1:41;
{x} c= VG \ V2 by A12,ZFMISC_1:31;
then
A14: card (VG \ V1) = card (VG \ V2) - card {x} by A13,CARD_2:44
.= n + 1 - 1 by A8,CARD_1:30
.= n;
A15: source in V1 by A9,XBOOLE_0:def 3;
not x in {sink} by A11,CARD_1:27,XBOOLE_0:def 5;
then
A16: x <> sink by TARSKI:def 1;
then not sink in {x} by TARSKI:def 1;
then not sink in V1 by A10,XBOOLE_0:def 3;
then
A17: EL.flow(source,sink) = Sum (EL|EV1V1a) - Sum (EL|EV1V1b) by A7,A14,A15;
set EXXe = G.edgesDBetween({x}, VG \ {x});
set EXV2 = G.edgesDBetween({x},V2);
set EV2X = G.edgesDBetween(V2,{x});
reconsider EA = EV1V1a \/ EV2X as Subset of the_Edges_of G;
reconsider E1 = EA \ EXV1c as Subset of the_Edges_of G;
reconsider EB = EA \ EV2X as Subset of the_Edges_of G;
reconsider EC = EV1V1b \/ EXV2 as Subset of the_Edges_of G;
reconsider E2 = EC \ EV1Xd as Subset of the_Edges_of G;
reconsider ED = EC \ EXV2 as Subset of the_Edges_of G;
A18: dom (EL|EA) = EA by PARTFUN1:def 2;
now
set e = the Element of EV1V1b /\ EXV2;
assume EV1V1b meets EXV2;
then
A19: EV1V1b /\ EXV2 <> {} by XBOOLE_0:def 7;
then e in EV1V1b by XBOOLE_0:def 4;
then e DSJoins VG\V1,V1,G by GLIB_000:def 31;
then SG.e in VG \ V1;
then
A20: not SG.e in V1 by XBOOLE_0:def 5;
e in EXV2 by A19,XBOOLE_0:def 4;
then e DSJoins {x},V2,G by GLIB_000:def 31;
then SG.e in {x};
hence contradiction by A20,XBOOLE_0:def 3;
end;
then EV1V1b \ EXV2 = EV1V1b by XBOOLE_1:83;
then
A21: ED = EV1V1b by XBOOLE_1:40;
now
let e be object;
assume
A22: e in EXV1c;
then
A23: e DSJoins {x},VG \ V1, G by GLIB_000:def 31;
then SG.e in {x};
then
A24: SG.e in V1 by XBOOLE_0:def 3;
TG.e in VG \ V1 by A23;
then e DSJoins V1,VG \ V1, G by A22,A24;
hence e in EV1V1a by GLIB_000:def 31;
end;
then
A25: EXV1c c= EV1V1a;
now
set e = the Element of EV1V1a /\ EV2X;
assume EV1V1a meets EV2X;
then
A26: EV1V1a /\ EV2X <> {} by XBOOLE_0:def 7;
then e in EV1V1a by XBOOLE_0:def 4;
then e DSJoins V1,VG\V1,G by GLIB_000:def 31;
then TG.e in VG \ V1;
then
A27: not TG.e in V1 by XBOOLE_0:def 5;
e in EV2X by A26,XBOOLE_0:def 4;
then e DSJoins V2,{x},G by GLIB_000:def 31;
then TG.e in {x};
hence contradiction by A27,XBOOLE_0:def 3;
end;
then EV1V1a \ EV2X = EV1V1a by XBOOLE_1:83;
then
A28: EB = EV1V1a by XBOOLE_1:40;
A29: dom (EL|EB) = EB by PARTFUN1:def 2;
A30: now
let e be object;
assume e in dom (EL|EA);
then
A31: e in EA;
now
per cases;
suppose
not e in EV2X;
then
A32: e in EB by A31,XBOOLE_0:def 5;
hence (EL|EV2X +* EL|EB).e = (EL|EB).e by A29,FUNCT_4:13
.= EL.e by A32,FUNCT_1:49;
end;
suppose
A33: e in EV2X;
then not e in EB by XBOOLE_0:def 5;
hence (EL|EV2X +* EL|EB).e = (EL|EV2X).e by A29,FUNCT_4:11
.= EL.e by A33,FUNCT_1:49;
end;
end;
hence (EL|EA).e = (EL|EV2X +* EL|EB).e by A31,FUNCT_1:49;
end;
now
let e be object;
hereby
assume
A34: e in EXXe \ EXV2;
then e in EXXe by XBOOLE_0:def 5;
then
A35: e DSJoins {x},VG\{x}, G by GLIB_000:def 31;
then
A36: SG.e in {x};
A37: TG.e in VG \ {x } by A35;
then
A38: not TG.e in {x } by XBOOLE_0:def 5;
not e in EXV2 by A34,XBOOLE_0:def 5;
then not e DSJoins {x},V2,G by GLIB_000:def 31;
then not TG.e in V2 by A34,A36;
then not TG.e in V1 by A38,XBOOLE_0:def 3;
then TG.e in VG \ V1 by A37,XBOOLE_0:def 5;
then e DSJoins {x}, VG \ V1, G by A34,A36;
hence e in EXV1c by GLIB_000:def 31;
end;
assume
A39: e in EXV1c;
then
A40: e DSJoins {x}, VG \ V1, G by GLIB_000:def 31;
then
A41: TG.e in VG \ V1;
then
A42: not TG.e in V1 by XBOOLE_0:def 5;
then not TG.e in {x} by XBOOLE_0:def 3;
then
A43: TG.e in VG \ {x} by A41,XBOOLE_0:def 5;
not TG.e in V2 by A42,XBOOLE_0:def 3;
then not e DSJoins {x},V2,G;
then
A44: not e in EXV2 by GLIB_000:def 31;
SG.e in {x} by A40;
then e DSJoins {x}, VG \ {x}, G by A39,A43;
then e in EXXe by GLIB_000:def 31;
hence e in EXXe \ EXV2 by A44,XBOOLE_0:def 5;
end;
then
A45: EXXe \ EXV2 = EXV1c by TARSKI:2;
A46: dom (EL|ED) = ED by PARTFUN1:def 2;
A47: now
let e be object;
assume e in dom (EL|EC);
then
A48: e in EC;
now
per cases;
suppose
not e in EXV2;
then
A49: e in ED by A48,XBOOLE_0:def 5;
hence (EL|EXV2 +* EL|ED).e = (EL|ED).e by A46,FUNCT_4:13
.= EL.e by A49,FUNCT_1:49;
end;
suppose
A50: e in EXV2;
then not e in ED by XBOOLE_0:def 5;
hence (EL|EXV2 +* EL|ED).e = (EL|EXV2).e by A46,FUNCT_4:11
.= EL.e by A50,FUNCT_1:49;
end;
end;
hence (EL|EC).e = (EL|EXV2 +* EL|ED).e by A48,FUNCT_1:49;
end;
reconsider EXV1cb = EXXe \ EXV2 as Subset of the_Edges_of G;
set EXXf = G.edgesDBetween(VG \ {x}, {x});
A51: dom (EL|EC) = EC by PARTFUN1:def 2;
now
let e be object;
hereby
assume
A52: e in EXXf \ EV2X;
then e in EXXf by XBOOLE_0:def 5;
then
A53: e DSJoins VG \ {x}, {x}, G by GLIB_000:def 31;
then
A54: TG.e in {x};
A55: SG.e in VG \ {x } by A53;
then
A56: not SG.e in {x } by XBOOLE_0:def 5;
not e in EV2X by A52,XBOOLE_0:def 5;
then not e DSJoins V2, {x}, G by GLIB_000:def 31;
then not SG.e in V2 by A52,A54;
then not SG.e in V1 by A56,XBOOLE_0:def 3;
then SG.e in VG \ V1 by A55,XBOOLE_0:def 5;
then e DSJoins VG \ V1, {x}, G by A52,A54;
hence e in EV1Xd by GLIB_000:def 31;
end;
assume
A57: e in EV1Xd;
then
A58: e DSJoins VG \ V1, {x}, G by GLIB_000:def 31;
then
A59: SG.e in VG \ V1;
then
A60: not SG.e in V1 by XBOOLE_0:def 5;
then not SG.e in {x} by XBOOLE_0:def 3;
then
A61: SG.e in VG \ {x} by A59,XBOOLE_0:def 5;
not SG.e in V2 by A60,XBOOLE_0:def 3;
then not e DSJoins V2,{x},G;
then
A62: not e in EV2X by GLIB_000:def 31;
TG.e in {x} by A58;
then e DSJoins VG \ {x}, {x}, G by A57,A61;
then e in EXXf by GLIB_000:def 31;
hence e in EXXf \ EV2X by A62,XBOOLE_0:def 5;
end;
then
A63: EXXf \ EV2X = EV1Xd by TARSKI:2;
now
let e be object;
assume
A64: e in EV1Xd;
then
A65: e DSJoins VG\V1,{x}, G by GLIB_000:def 31;
then TG.e in {x};
then
A66: TG.e in V1 by XBOOLE_0:def 3;
SG.e in VG \ V1 by A65;
then e DSJoins VG\V1,V1, G by A64,A66;
hence e in EV1V1b by GLIB_000:def 31;
end;
then
A67: EV1Xd c= EV1V1b;
A68: not x in V2 by A12,XBOOLE_0:def 5;
now
let e be object;
assume
A69: e in EV2X;
then
A70: e DSJoins V2,{x},G by GLIB_000:def 31;
then
A71: SG.e in V2;
then not SG.e in {x} by A68,TARSKI:def 1;
then
A72: SG.e in VG \ {x} by A71,XBOOLE_0:def 5;
TG.e in {x} by A70;
then e DSJoins VG\{x}, {x}, G by A69,A72;
hence e in EXXf by GLIB_000:def 31;
end;
then
A73: EV2X c= EXXf;
A74: V2 qua set \ {x} is Subset of V2;
now
let e be object;
A75: EV1V1a \/ EV2X qua set \ EXV1c is Subset of EV1V1a \/ EV2X;
hereby
assume
A76: e in G.edgesDBetween(V2, VG \ V2);
then
A77: e DSJoins V2, VG \ V2, G by GLIB_000:def 31;
then
A78: SG.e in V2;
A79: now
assume e in EXV1c;
then e DSJoins {x},VG \ V1,G by GLIB_000:def 31;
then SG.e in {x};
hence contradiction by A68,A78,TARSKI:def 1;
end;
A80: TG.e in VG \ V2 by A77;
A81: SG.e in V1 by A78,XBOOLE_0:def 3;
now
per cases;
suppose
TG.e in {x};
then e DSJoins V2,{x},G by A76,A78;
then e in EV2X by GLIB_000:def 31;
then e in EV1V1a \/ EV2X by XBOOLE_0:def 3;
hence e in EV1V1a \/ EV2X \ EXV1c by A79,XBOOLE_0:def 5;
end;
suppose
not TG.e in {x};
then TG.e in VG \ V1 by A13,A80,XBOOLE_0:def 5;
then e DSJoins V1, VG \ V1, G by A76,A81;
then e in EV1V1a by GLIB_000:def 31;
then e in EV1V1a \/ EV2X by XBOOLE_0:def 3;
hence e in EV1V1a \/ EV2X \ EXV1c by A79,XBOOLE_0:def 5;
end;
end;
hence e in EV1V1a \/ EV2X \ EXV1c;
end;
assume
A82: e in EV1V1a \/ EV2X \ EXV1c;
then not e in EXV1c by XBOOLE_0:def 5;
then
A83: not e DSJoins {x}, VG \ V1,G by GLIB_000:def 31;
now
per cases by A82,A75,XBOOLE_0:def 3;
suppose
A84: e in EV1V1a;
then
A85: e DSJoins V1, VG\V1, G by GLIB_000:def 31;
then
A86: SG.e in V1;
A87: TG.e in VG \ V1 by A85;
then not TG.e in V1 by XBOOLE_0:def 5;
then not TG.e in V2 by XBOOLE_0:def 3;
then
A88: TG.e in VG \ V2 by A87,XBOOLE_0:def 5;
not SG.e in {x} by A83,A84,A87;
then SG.e in V1 \ {x} by A86,XBOOLE_0:def 5;
then SG.e in V2 \ {x} by XBOOLE_1:40;
hence e DSJoins V2, VG \ V2, G by A74,A84,A88;
end;
suppose
A89: e in EV2X;
then
A90: e DSJoins V2, {x}, G by GLIB_000:def 31;
then
A91: SG.e in V2;
TG.e in {x} by A90;
then
A92: not TG.e in V2 by A68,TARSKI:def 1;
TG.e in VG by A89,FUNCT_2:5;
then TG.e in VG \ V2 by A92,XBOOLE_0:def 5;
hence e DSJoins V2, VG \ V2, G by A89,A91;
end;
end;
hence e in G.edgesDBetween(V2, VG \ V2) by GLIB_000:def 31;
end;
then
A93: G.edgesDBetween(V2, VG \ V2) = EV1V1a \/ EV2X \ EXV1c by TARSKI:2;
now
let e be object;
A94: EV1V1b \/ EXV2 qua set \ EV1Xd is Subset of EV1V1b \/ EXV2;
hereby
assume
A95: e in G.edgesDBetween(VG \ V2, V2);
then
A96: e DSJoins VG\V2, V2, G by GLIB_000:def 31;
then
A97: TG.e in V2;
A98: now
assume e in EV1Xd;
then e DSJoins VG \ V1,{x},G by GLIB_000:def 31;
then TG.e in {x};
hence contradiction by A68,A97,TARSKI:def 1;
end;
A99: SG.e in VG \ V2 by A96;
A100: TG.e in V1 by A97,XBOOLE_0:def 3;
now
per cases;
suppose
SG.e in {x};
then e DSJoins {x},V2,G by A95,A97;
then e in EXV2 by GLIB_000:def 31;
then e in EV1V1b \/ EXV2 by XBOOLE_0:def 3;
hence e in EV1V1b \/ EXV2 \ EV1Xd by A98,XBOOLE_0:def 5;
end;
suppose
not SG.e in {x};
then SG.e in VG \ V1 by A13,A99,XBOOLE_0:def 5;
then e DSJoins VG \ V1, V1, G by A95,A100;
then e in EV1V1b by GLIB_000:def 31;
then e in EV1V1b \/ EXV2 by XBOOLE_0:def 3;
hence e in EV1V1b \/ EXV2 \ EV1Xd by A98,XBOOLE_0:def 5;
end;
end;
hence e in EV1V1b \/ EXV2 \ EV1Xd;
end;
assume
A101: e in EV1V1b \/ EXV2 \ EV1Xd;
then not e in EV1Xd by XBOOLE_0:def 5;
then
A102: not e DSJoins VG \ V1, {x}, G by GLIB_000:def 31;
now
per cases by A101,A94,XBOOLE_0:def 3;
suppose
A103: e in EV1V1b;
then
A104: e DSJoins VG\V1, V1, G by GLIB_000:def 31;
then
A105: TG.e in V1;
A106: SG.e in VG \ V1 by A104;
then not SG.e in V1 by XBOOLE_0:def 5;
then not SG.e in V2 by XBOOLE_0:def 3;
then
A107: SG.e in VG \ V2 by A106,XBOOLE_0:def 5;
not TG.e in {x} by A102,A103,A106;
then TG.e in V1 \ {x} by A105,XBOOLE_0:def 5;
then TG.e in V2 \ {x} by XBOOLE_1:40;
hence e DSJoins VG \ V2, V2, G by A74,A103,A107;
end;
suppose
A108: e in EXV2;
then
A109: e DSJoins {x},V2, G by GLIB_000:def 31;
then
A110: TG.e in V2;
SG.e in {x} by A109;
then
A111: not SG.e in V2 by A68,TARSKI:def 1;
SG.e in VG by A108,FUNCT_2:5;
then SG.e in VG \ V2 by A111,XBOOLE_0:def 5;
hence e DSJoins VG \ V2, V2, G by A108,A110;
end;
end;
hence e in G.edgesDBetween(VG\V2,V2) by GLIB_000:def 31;
end;
then
A112: G.edgesDBetween(VG \ V2, V2) = E2 by TARSKI:2;
A113: dom (EL|E2)=EC\EV1Xd by PARTFUN1:def 2;
A114: now
let e be object;
assume e in dom (EL|EC);
then
A115: e in EC;
now
per cases;
suppose
not e in EV1Xd;
then
A116: e in E2 by A115,XBOOLE_0:def 5;
hence (EL|EV1Xd +* EL|E2).e = (EL|E2).e by A113,FUNCT_4:13
.= EL.e by A116,FUNCT_1:49;
end;
suppose
A117: e in EV1Xd;
then not e in E2 by XBOOLE_0:def 5;
hence (EL|EV1Xd +* EL|E2).e = (EL|EV1Xd).e by A113,FUNCT_4:11
.= EL.e by A117,FUNCT_1:49;
end;
end;
hence (EL|EC).e = (EL|EV1Xd +* EL|E2).e by A115,FUNCT_1:49;
end;
dom (EL|EXV2)=EXV2 by PARTFUN1:def 2;
then dom (EL|EXV2 +* EL|ED) = EXV2 \/ ED by A46,FUNCT_4:def 1
.= EXV2 \/ (EV1V1b \/ EXV2) by XBOOLE_1:39
.= EC by XBOOLE_1:6;
then
A118: Sum (EL|EC) = Sum (EL|EXV2) + Sum (EL|EV1V1b) by A21,A51,A47,FUNCT_1:2
,GLIB_004:3;
dom (EL|EV1Xd) = EV1Xd by PARTFUN1:def 2;
then dom (EL|EV1Xd +* EL|E2) = EV1Xd \/ (EC \ EV1Xd) by A113,
FUNCT_4:def 1
.= EV1Xd \/ (EV1V1b \/ EXV2) by XBOOLE_1:39
.= EC by A67,XBOOLE_1:10,12;
then
A119: Sum (EL|EC) = Sum (EL|E2) + Sum (EL|EV1Xd) by A51,A114,FUNCT_1:2
,GLIB_004:3;
dom (EL|EV2X)=EV2X by PARTFUN1:def 2;
then dom (EL|EV2X +* EL|EB) = EV2X \/ EB by A29,FUNCT_4:def 1
.= EV2X \/ (EV1V1a \/ EV2X) by XBOOLE_1:39
.= EA by XBOOLE_1:6;
then
A120: Sum (EL|EA) = Sum (EL|EV2X) + Sum (EL|EV1V1a) by A28,A18,A30,FUNCT_1:2
,GLIB_004:3;
reconsider EV1Xdb = EXXf \ EV2X as Subset of the_Edges_of G;
A121: dom (EL|EV1Xdb) = EXXf \ EV2X by PARTFUN1:def 2;
now
let e be object;
assume
A122: e in EXV2;
then
A123: e DSJoins {x},V2,G by GLIB_000:def 31;
then
A124: TG.e in V2;
then not TG.e in {x} by A68,TARSKI:def 1;
then
A125: TG.e in VG \ {x} by A124,XBOOLE_0:def 5;
SG.e in {x} by A123;
then e DSJoins {x},VG\{x}, G by A122,A125;
hence e in EXXe by GLIB_000:def 31;
end;
then
A126: EXV2 c= EXXe;
A127: dom (EL|E1)=EA \ EXV1c by PARTFUN1:def 2;
A128: now
let e be object;
assume e in dom (EL|EA);
then
A129: e in EA;
now
per cases;
suppose
not e in EXV1c;
then
A130: e in E1 by A129,XBOOLE_0:def 5;
hence (EL|EXV1c +* EL|E1).e = (EL|E1).e by A127,FUNCT_4:13
.= EL.e by A130,FUNCT_1:49;
end;
suppose
A131: e in EXV1c;
then not e in E1 by XBOOLE_0:def 5;
hence (EL|EXV1c +* EL|E1).e = (EL|EXV1c).e by A127,FUNCT_4:11
.= EL.e by A131,FUNCT_1:49;
end;
end;
hence (EL|EA).e = (EL|EXV1c +* EL|E1).e by A129,FUNCT_1:49;
end;
A132: dom (EL|EXXf) = EXXf by PARTFUN1:def 2;
A133: now
let e be object;
assume
A134: e in dom (EL|EXXf);
then
A135: e in EXXf;
now
per cases;
suppose
A136: e in EV2X;
then not e in EV1Xdb by XBOOLE_0:def 5;
hence (EL|EV2X +* EL|EV1Xdb).e=(EL|EV2X).e by A121,FUNCT_4:11
.=EL.e by A136,FUNCT_1:49;
end;
suppose
not e in EV2X;
then
A137: e in EV1Xdb by A135,XBOOLE_0:def 5;
hence (EL|EV2X +* EL|EV1Xdb).e = (EL|EV1Xdb).e by A121,FUNCT_4:13
.= EL.e by A137,FUNCT_1:49;
end;
end;
hence (EL|EXXf).e = (EL|EV2X +* EL|EV1Xdb).e by A134,FUNCT_1:49;
end;
dom (EL|EV2X) = EV2X by PARTFUN1:def 2;
then dom (EL|EV2X +* EL|(EXXf \ EV2X)) = EV2X \/ (EXXf \ EV2X) by A121,
FUNCT_4:def 1
.= EV2X \/ EXXf by XBOOLE_1:39
.= EXXf by A73,XBOOLE_1:12;
then
A138: Sum (EL|EV2X) + Sum (EL|EV1Xd) = Sum (EL|EXXf) by A63,A132,A133,FUNCT_1:2
,GLIB_004:3;
dom (EL|EXV1c) = EXV1c by PARTFUN1:def 2;
then dom (EL|EXV1c +* EL|E1) = EXV1c \/ (EA \ EXV1c) by A127,
FUNCT_4:def 1
.= EXV1c \/ (EV1V1a \/ EV2X) by XBOOLE_1:39
.= EA by A25,XBOOLE_1:10,12;
then
A139: Sum (EL|EA) = Sum (EL|E1) + Sum (EL|EXV1c) by A18,A128,FUNCT_1:2
,GLIB_004:3;
A140: dom (EL|EXV1cb) = EXXe \ EXV2 by PARTFUN1:def 2;
A141: dom (EL|EXXe) = EXXe by PARTFUN1:def 2;
A142: now
let e be object;
assume
A143: e in dom (EL|EXXe);
then
A144: e in EXXe;
now
per cases;
suppose
A145: e in EXV2;
then not e in EXV1cb by XBOOLE_0:def 5;
hence (EL|EXV2 +* EL|EXV1cb).e=(EL|EXV2).e by A140,FUNCT_4:11
.=EL.e by A145,FUNCT_1:49;
end;
suppose
not e in EXV2;
then
A146: e in EXV1cb by A144,XBOOLE_0:def 5;
hence (EL|EXV2 +* EL|EXV1cb).e = (EL|EXV1cb).e by A140,FUNCT_4:13
.= EL.e by A146,FUNCT_1:49;
end;
end;
hence (EL|EXXe).e = (EL|EXV2 +* EL|EXV1cb).e by A143,FUNCT_1:49;
end;
dom (EL|EXV2) = EXV2 by PARTFUN1:def 2;
then dom (EL|EXV2 +* EL|(EXXe \ EXV2)) = EXV2 \/ (EXXe \ EXV2) by A140,
FUNCT_4:def 1
.= EXV2 \/ EXXe by XBOOLE_1:39
.= EXXe by A126,XBOOLE_1:12;
then
A147: Sum (EL|EXV2) + Sum (EL|EXV1c) = Sum (EL|EXXe) by A45,A141,A142,FUNCT_1:2
,GLIB_004:3;
reconsider x as Vertex of G by A12;
A148: x.edgesOut() = G.edgesDBetween({x},VG) by GLIB_000:39;
reconsider EXXeb = G.edgesDBetween({x},VG)\G.edgesDBetween({x},{x}) as
Subset of the_Edges_of G;
reconsider EXXfb = G.edgesDBetween(VG,{x})\G.edgesDBetween({x},{x}) as
Subset of the_Edges_of G;
A149: dom (EL|G.edgesDBetween(VG,{x})) = G.edgesDBetween(VG,{x}) by
PARTFUN1:def 2;
now
let e be object;
hereby
assume
A150: e in G.edgesDBetween(VG,{x}) \ G.edgesDBetween({x},{x});
then e in G.edgesDBetween(VG,{x}) by XBOOLE_0:def 5;
then
A151: e DSJoins VG,{x},G by GLIB_000:def 31;
then
A152: SG.e in VG;
A153: TG.e in {x} by A151;
not e in G.edgesDBetween({x},{x}) by A150,XBOOLE_0:def 5;
then not e DSJoins {x},{x},G by GLIB_000:def 31;
then not SG.e in {x} by A150,A153;
then SG.e in VG\{x} by A152,XBOOLE_0:def 5;
then e DSJoins VG\{x},{x},G by A150,A153;
hence e in EXXf by GLIB_000:def 31;
end;
assume
A154: e in EXXf;
then
A155: e DSJoins VG \{x}, {x}, G by GLIB_000:def 31;
then
A156: SG.e in VG \ {x};
then not SG.e in {x} by XBOOLE_0:def 5;
then not e DSJoins {x},{x},G;
then
A157: not e in G.edgesDBetween({x},{x}) by GLIB_000:def 31;
TG.e in {x} by A155;
then e DSJoins VG,{x},G by A154,A156;
then e in G.edgesDBetween(VG,{x}) by GLIB_000:def 31;
hence e in G.edgesDBetween(VG,{x}) \ G.edgesDBetween({x},{x}) by A157,
XBOOLE_0:def 5;
end;
then
A158: G.edgesDBetween(VG,{x}) \ G.edgesDBetween({x},{x}) = EXXf by TARSKI:2;
A159: dom (EL|EXXfb) = EXXfb by PARTFUN1:def 2;
A160: now
let e be object;
assume e in dom (EL|G.edgesDBetween(VG,{x}));
then
A161: e in G.edgesDBetween(VG,{x});
now
per cases;
suppose
A162: e in G.edgesDBetween({x},{x});
then not e in EXXfb by XBOOLE_0:def 5;
hence (EL|G.edgesDBetween({x},{x}) +* EL|EXXfb).e = (EL|G
.edgesDBetween({x},{x})).e by A159,FUNCT_4:11
.= EL.e by A162,FUNCT_1:49;
end;
suppose
not e in G.edgesDBetween({x},{x});
then
A163: e in EXXfb by A161,XBOOLE_0:def 5;
hence
(EL|G.edgesDBetween({x},{x}) +* EL|EXXfb).e = (EL|EXXfb).e by A159,
FUNCT_4:13
.= EL.e by A163,FUNCT_1:49;
end;
end;
hence (EL|G.edgesDBetween(VG,{x})).e = (EL|G.edgesDBetween({x},{x}) +*
EL|EXXfb).e by A161,FUNCT_1:49;
end;
now
let e be object;
hereby
assume
A164: e in G.edgesDBetween({x},VG) \ G.edgesDBetween({x},{x});
then e in G.edgesDBetween({x},VG) by XBOOLE_0:def 5;
then
A165: e DSJoins {x},VG,G by GLIB_000:def 31;
then
A166: TG.e in VG;
A167: SG.e in {x} by A165;
not e in G.edgesDBetween({x},{x}) by A164,XBOOLE_0:def 5;
then not e DSJoins {x},{x},G by GLIB_000:def 31;
then not TG.e in {x} by A164,A167;
then TG.e in VG\{x} by A166,XBOOLE_0:def 5;
then e DSJoins {x},VG\{x},G by A164,A167;
hence e in EXXe by GLIB_000:def 31;
end;
assume
A168: e in EXXe;
then
A169: e DSJoins {x}, VG \{x}, G by GLIB_000:def 31;
then
A170: TG.e in VG \ {x};
then not TG.e in {x} by XBOOLE_0:def 5;
then not e DSJoins {x},{x},G;
then
A171: not e in G.edgesDBetween({x},{x}) by GLIB_000:def 31;
SG.e in {x} by A169;
then e DSJoins {x},VG,G by A168,A170;
then e in G.edgesDBetween({x},VG) by GLIB_000:def 31;
hence e in G.edgesDBetween({x},VG) \ G.edgesDBetween({x},{x}) by A171,
XBOOLE_0:def 5;
end;
then
A172: G.edgesDBetween({x},VG) \ G.edgesDBetween({x},{x}) = EXXe by TARSKI:2;
A173: dom (EL|G.edgesDBetween({x},VG)) = G.edgesDBetween({x},VG) by
PARTFUN1:def 2;
A174: dom (EL|EXXeb) = EXXeb by PARTFUN1:def 2;
A175: now
let e be object;
assume e in dom (EL|G.edgesDBetween({x},VG));
then
A176: e in G.edgesDBetween({x},VG);
now
per cases;
suppose
A177: e in G.edgesDBetween({x},{x});
then not e in EXXeb by XBOOLE_0:def 5;
hence (EL|G.edgesDBetween({x},{x}) +* EL|EXXeb).e = (EL|G
.edgesDBetween({x},{x})).e by A174,FUNCT_4:11
.= EL.e by A177,FUNCT_1:49;
end;
suppose
not e in G.edgesDBetween({x},{x});
then
A178: e in EXXeb by A176,XBOOLE_0:def 5;
hence
(EL|G.edgesDBetween({x},{x}) +* EL|EXXeb).e = (EL|EXXeb).e by A174,
FUNCT_4:13
.= EL.e by A178,FUNCT_1:49;
end;
end;
hence (EL|G.edgesDBetween({x},VG)).e = (EL|G.edgesDBetween({x},{x}) +*
EL|EXXeb).e by A176,FUNCT_1:49;
end;
A179: dom (EL|G.edgesDBetween({x},{x})) = G.edgesDBetween({x},{x}) by
PARTFUN1:def 2;
then dom (EL|G.edgesDBetween({x},{x}) +* EL|EXXfb) = G.edgesDBetween({x
},{x}) \/ EXXfb by A159,FUNCT_4:def 1
.= G.edgesDBetween({x},{x}) \/ G.edgesDBetween(VG,{x}) by XBOOLE_1:39
.= G.edgesDBetween(VG,{x}) by GLIB_000:38,XBOOLE_1:12;
then
A180: Sum (EL|G.edgesDBetween(VG,{x})) = Sum (EL|EXXf) + Sum (EL|G
.edgesDBetween({x},{x})) by A158,A149,A160,FUNCT_1:2,GLIB_004:3;
dom (EL|G.edgesDBetween({x},{x}) +* EL|EXXeb) = G.edgesDBetween({x
},{x}) \/ EXXeb by A179,A174,FUNCT_4:def 1
.= G.edgesDBetween({x},{x}) \/ G.edgesDBetween({x},VG) by XBOOLE_1:39
.= G.edgesDBetween({x},VG) by GLIB_000:38,XBOOLE_1:12;
then
A181: Sum (EL|G.edgesDBetween({x},VG)) = Sum (EL|EXXe) + Sum (EL|G
.edgesDBetween({x},{x})) by A172,A173,A175,FUNCT_1:2,GLIB_004:3;
x.edgesIn() = G.edgesDBetween(VG,{x}) by GLIB_000:39;
then Sum (EL|G.edgesDBetween(VG,{x}))= Sum (EL|G.edgesDBetween({x } ,VG
) ) by A1,A9,A68,A16,A148;
hence
EL.flow(source,sink) = Sum(EL | G.edgesDBetween(V2, VG \ V2)) - Sum
(EL | G.edgesDBetween(VG \ V2, V2)) by A17,A93,A139,A120,A112,A119,A118,A138
,A147,A180,A181;
end;
hence P[n+1];
end;
now
set ESS = G.edgesDBetween({sink},{sink});
let V be Subset of VG;
assume that
A182: card (VG \ V) = 1 and
source in V and
A183: not sink in V;
reconsider EOUT= G.edgesOutOf({sink})\ ESS as Subset of the_Edges_of G;
consider v being object such that
A184: VG \ V = {v} by A182,CARD_2:42;
sink is Vertex of G by A1;
then sink in VG \ V by A183,XBOOLE_0:def 5;
then
A185: v = sink by A184,TARSKI:def 1;
A186: now
let x be object;
hereby
assume
A187: x in VG \ {sink};
then not x in {sink} by XBOOLE_0:def 5;
hence x in V by A184,A185,A187,XBOOLE_0:def 5;
end;
assume
A188: x in V;
then not x in {sink} by A183,TARSKI:def 1;
hence x in VG \ {sink} by A188,XBOOLE_0:def 5;
end;
then
A189: V = VG \ {sink} by TARSKI:2;
now
let e be object;
hereby
assume
A190: e in G.edgesDBetween(VG \ V, V);
then
A191: e DSJoins {sink},(VG \ {sink}),G by A184,A185,A189,GLIB_000:def 31;
then
A192: TG.e in (VG \ {sink});
A193: now
assume e in ESS;
then e DSJoins {sink},{sink},G by GLIB_000:def 31;
then TG.e in {sink};
hence contradiction by A192,XBOOLE_0:def 5;
end;
SG.e in {sink} by A191;
then e in G.edgesOutOf({sink}) by A190,GLIB_000:def 27;
hence e in EOUT by A193,XBOOLE_0:def 5;
end;
assume
A194: e in EOUT;
G.edgesOutOf({sink}) qua set \ ESS is Subset of G.edgesOutOf({sink} );
then
A195: SG.e in {sink} by A194,GLIB_000:def 27;
A196: not e in ESS by A194,XBOOLE_0:def 5;
now
assume
A197: not TG.e in V;
TG.e in VG by A194,FUNCT_2:5;
then TG.e in {sink} by A189,A197,XBOOLE_0:def 5;
then e DSJoins {sink},{sink},G by A194,A195;
hence contradiction by A196,GLIB_000:def 31;
end;
then e DSJoins (VG \ V),V,G by A184,A185,A194,A195;
hence e in G.edgesDBetween(VG \ V, V) by GLIB_000:def 31;
end;
then
A198: G.edgesDBetween(VG \ V, V) = EOUT by TARSKI:2;
set EESS = EL|ESS;
reconsider EIN = G.edgesInto({sink}) \ ESS as Subset of the_Edges_of G;
A199: dom (EL|G.edgesInto({sink})) = G.edgesInto({sink}) by PARTFUN1:def 2;
now
let e be object;
hereby
assume
A200: e in G.edgesDBetween(V, VG \ V);
then
A201: e DSJoins VG \ {sink}, {sink},G by A184,A185,A189,GLIB_000:def 31;
then
A202: SG.e in VG \ {sink};
A203: now
assume e in ESS;
then e DSJoins {sink},{sink},G by GLIB_000:def 31;
then SG.e in {sink};
hence contradiction by A202,XBOOLE_0:def 5;
end;
TG.e in {sink} by A201;
then e in G.edgesInto({sink}) by A200,GLIB_000:def 26;
hence e in EIN by A203,XBOOLE_0:def 5;
end;
assume
A204: e in EIN;
G.edgesInto({sink}) qua set \ ESS is Subset of G.edgesInto({sink});
then
A205: TG.e in {sink} by A204,GLIB_000:def 26;
A206: not e in ESS by A204,XBOOLE_0:def 5;
now
assume not SG.e in V;
then
A207: not SG.e in VG \ {sink} by A186;
SG.e in VG by A204,FUNCT_2:5;
then SG.e in {sink} by A207,XBOOLE_0:def 5;
then e DSJoins {sink},{sink},G by A204,A205;
hence contradiction by A206,GLIB_000:def 31;
end;
then e DSJoins V, {sink}, G by A204,A205;
hence e in G.edgesDBetween(V, VG \ V) by A184,A185,GLIB_000:def 31;
end;
then
A208: G.edgesDBetween(V, VG \ V) = EIN by TARSKI:2;
now
let e be object;
assume
A209: e in ESS;
then e DSJoins {sink},{sink},G by GLIB_000:def 31;
then SG.e in {sink};
hence e in G.edgesOutOf({sink}) by A209,GLIB_000:def 27;
end;
then
A210: ESS c= G.edgesOutOf({sink});
now
let e be object;
assume
A211: e in ESS;
then e DSJoins {sink},{sink},G by GLIB_000:def 31;
then TG.e in {sink};
hence e in G.edgesInto({sink}) by A211,GLIB_000:def 26;
end;
then
A212: ESS c= G.edgesInto({sink});
A213: dom (EL|ESS)=ESS by PARTFUN1:def 2;
A214: dom (EL|EOUT)=EOUT by PARTFUN1:def 2;
A215: now
let e be object;
assume
A216: e in dom (EL|G.edgesOutOf({sink}));
then
A217: e in G.edgesOutOf({sink});
now
per cases;
suppose
A218: e in ESS;
then not e in EOUT by XBOOLE_0:def 5;
hence (EL|ESS +* EL|EOUT).e = (EL|ESS).e by A214,FUNCT_4:11
.= EL.e by A213,A218,FUNCT_1:47;
end;
suppose
not e in ESS;
then
A219: e in EOUT by A217,XBOOLE_0:def 5;
hence (EL|ESS +* EL|EOUT).e = (EL|EOUT).e by A214,FUNCT_4:13
.= EL.e by A214,A219,FUNCT_1:47;
end;
end;
hence EL|G.edgesOutOf({sink}).e = (EL|ESS +* EL|EOUT).e by A216,
FUNCT_1:47;
end;
A220: dom (EL|EIN)=EIN by PARTFUN1:def 2;
A221: now
let e be object;
assume
A222: e in dom (EL|G.edgesInto({sink}));
then
A223: e in G.edgesInto({sink});
now
per cases;
suppose
A224: e in ESS;
then not e in EIN by XBOOLE_0:def 5;
hence (EL|ESS +* EL|EIN).e = (EL|ESS).e by A220,FUNCT_4:11
.= EL.e by A213,A224,FUNCT_1:47;
end;
suppose
not e in ESS;
then
A225: e in EIN by A223,XBOOLE_0:def 5;
hence (EL|ESS +* EL|EIN).e = (EL|EIN).e by A220,FUNCT_4:13
.= EL.e by A220,A225,FUNCT_1:47;
end;
end;
hence EL|G.edgesInto({sink}).e = (EL|ESS +* EL|EIN).e by A222,FUNCT_1:47;
end;
A226: ESS \/ EIN = G.edgesInto({sink}) \/ ESS by XBOOLE_1:39
.= G.edgesInto({sink}) by A212,XBOOLE_1:12;
dom (EL|ESS +* EL|EIN) = ESS \/ EIN by A213,A220,FUNCT_4:def 1;
then
A227: Sum (EL|G.edgesInto({sink})) = Sum (EL|EIN) + Sum EESS by A226,A199,A221,
FUNCT_1:2,GLIB_004:3;
ESS \/ EOUT = G.edgesOutOf({sink}) \/ ESS by XBOOLE_1:39
.= G.edgesOutOf({sink}) by A210,XBOOLE_1:12;
then
A228: dom (EL|ESS +* EL|EOUT) = G.edgesOutOf({sink}) by A213,A214,FUNCT_4:def 1
;
dom (EL|G.edgesOutOf({sink})) = G.edgesOutOf({sink}) by PARTFUN1:def 2;
then EL.flow(source,sink) = Sum (EL|EIN)+Sum EESS -(Sum EESS + Sum (EL|
EOUT)) by A227,A228,A215,FUNCT_1:2,GLIB_004:3
.= Sum (EL|EIN) - Sum (EL|EOUT);
hence EL.flow(source,sink) = Sum (EL | G.edgesDBetween(V, VG \ V)) - Sum (
EL | G.edgesDBetween(VG \ V, V)) by A208,A198;
end;
then
A229: P[1];
for n being non zero Nat holds P[n] from NAT_1:sch 10(A229,A6);
hence thesis by A2,A3,A4;
end;
theorem Th12:
for G being _finite real-weighted WGraph, EL being FF:ELabeling
of G, source,sink being set, V being Subset of the_Vertices_of G st EL
has_valid_flow_from source,sink & source in V & not sink in V holds EL.flow(
source,sink) <= Sum ((the_Weight_of G) | G.edgesDBetween(V,the_Vertices_of G \
V))
proof
let G be _finite real-weighted WGraph, EL being FF:ELabeling of G, source,
sink be set, V be Subset of the_Vertices_of G;
assume that
A1: EL has_valid_flow_from source,sink and
A2: source in V and
A3: not sink in V;
set W1 = (the_Weight_of G) | G.edgesDBetween(V, the_Vertices_of G \ V);
set E2 = EL | G.edgesDBetween(the_Vertices_of G \ V, V);
set E1 = EL | G.edgesDBetween(V, the_Vertices_of G \ V);
now
let e be set;
assume
A4: e in G.edgesDBetween(V, the_Vertices_of G\V);
then
A5: W1.e = (the_Weight_of G).e by FUNCT_1:49;
E1.e = EL.e by A4,FUNCT_1:49;
hence E1.e <= W1.e by A1,A4,A5;
end;
then Sum E1 <= Sum W1 by GLIB_004:5;
then
A6: Sum E1 - Sum E2 <= Sum W1 - Sum E2 by XREAL_1:9;
set B1 = EmptyBag G.edgesDBetween(the_Vertices_of G \ V, V);
A7: now
let e be set;
A8: B1 = G.edgesDBetween(the_Vertices_of G \ V, V)-->0 by PBOOLE:def 3;
assume e in G.edgesDBetween(the_Vertices_of G \ V, V);
hence B1.e <= E2.e by A8,FUNCOP_1:7;
end;
Sum B1 = 0 by UPROOTS:11;
then 0 <= Sum E2 by A7,GLIB_004:5;
then
A9: Sum W1 - Sum E2 <= Sum W1 - 0 by XREAL_1:13;
EL.flow(source,sink) = Sum E1 - Sum E2 by A1,A2,A3,Th11;
hence thesis by A9,A6,XXREAL_0:2;
end;
theorem Th13:
for G being _finite natural-weighted WGraph, EL being
FF:ELabeling of G, W being Walk of G st W is non trivial & W is_augmenting_wrt
EL holds 0 < W.tolerance(EL)
proof
let G be _finite natural-weighted WGraph, EL being FF:ELabeling of G, W be
Walk of G such that
A1: W is non trivial and
A2: W is_augmenting_wrt EL;
set T = W.tolerance(EL);
T in rng (W.flowSeq(EL)) by A1,A2,Def16;
then consider n being Nat such that
A3: n in dom (W.flowSeq(EL)) and
A4: T = (W.flowSeq(EL)).n by FINSEQ_2:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
dom (W.flowSeq(EL)) = dom W.edgeSeq() by A2,Def15;
then
A5: 2*n in dom W by A3,GLIB_001:78;
then 1 <= 2*n by FINSEQ_3:25;
then reconsider 2n1 = 2*n-1 as odd Element of NAT by INT_1:5;
2*n <= len W by A5,FINSEQ_3:25;
then
A6: 2*n-1 < len W - 0 by XREAL_1:15;
set v1 = W.(2n1), e = W.(2*n), v2 = W.(2*n+1);
A7: 2*n-1 + 2 = 2*n+1;
A8: 2*n-1 + 1 = 2*n;
now
per cases;
suppose
A9: e DJoins v1,v2,G;
then
A10: T = (the_Weight_of G).e - EL.e by A2,A3,A4,Def15;
EL.e < (the_Weight_of G).e by A2,A6,A8,A7,A9;
then EL.e - EL.e < T by A10,XREAL_1:14;
hence thesis;
end;
suppose
A11: not e DJoins v1,v2,G;
then T = EL.e by A2,A3,A4,Def15;
hence thesis by A2,A6,A8,A7,A11;
end;
end;
hence thesis;
end;
theorem Th14:
for G being _finite natural-weighted WGraph, EL being
FF:ELabeling of G, source,sink being set, P being Path of G st source <> sink &
EL has_valid_flow_from source,sink & P is_Walk_from source,sink & P
is_augmenting_wrt EL holds FF:PushFlow(EL,P) has_valid_flow_from source,sink
proof
let G be _finite natural-weighted WGraph, EL being FF:ELabeling of G, source,
sink be set, P be Path of G;
assume that
A1: source <> sink and
A2: EL has_valid_flow_from source,sink and
A3: P is_Walk_from source,sink and
A4: P is_augmenting_wrt EL;
set EL2 = FF:PushFlow(EL,P);
now
thus source is Vertex of G & sink is Vertex of G by A2;
now
let e be set;
assume
A5: e in the_Edges_of G;
then
A6: EL.e <= (the_Weight_of G).e by A2;
now
per cases;
suppose
not e in P.edges();
hence 0 <= EL2.e & EL2.e <= (the_Weight_of G).e by A4,A5,A6,Def17;
end;
suppose
e in P.edges();
then consider n being odd Element of NAT such that
A7: n < len P and
A8: P.(n+1) = e by GLIB_001:100;
set PFS = P.flowSeq(EL), n1div2 = (n+1) div 2;
A9: 1 <= n+1 by NAT_1:11;
n+1 <= len P by A7,NAT_1:13;
then n1div2 in dom P.edgeSeq() by A9,GLIB_001:77;
then
A10: n1div2 in dom PFS by A4,Def15;
A11: now
A12: n + 0 < n+2 by XREAL_1:8;
assume that
A13: e DJoins P.n,P.(n+2),G and
A14: e DJoins P.(n+2),P.n,G;
A15: (the_Source_of G).e = P.n by A13;
A16: (the_Source_of G).e = P.(n+2) by A14;
A17: n+2 <= len P by A7,GLIB_001:1;
then n = 1 by A15,A16,A12,GLIB_001:def 28;
then
A18: P.n = source by A3,GLIB_001:17;
n+2 = len P by A15,A16,A12,A17,GLIB_001:def 28;
hence contradiction by A1,A3,A15,A16,A18,GLIB_001:17;
end;
A19: P.last() = sink by A3,GLIB_001:def 23;
P.first() = source by A3,GLIB_001:def 23;
then
A20: P is non trivial by A1,A19,GLIB_001:127;
2 divides n+1 by PEPIN:22;
then
A21: 2 * n1div2 = n+1 by NAT_D:3;
then
A22: 2 * n1div2 - 1 = n;
A23: 2 * n1div2 + 1 = n + 2 by A21;
A24: e Joins P.n,P.(n+2),G by A7,A8,GLIB_001:def 3;
now
per cases by A24;
suppose
A25: e DJoins P.n,P.(n+2),G;
then PFS.n1div2 = (the_Weight_of G).e - EL.e by A4,A8,A10,A22,A23
,Def15;
then (the_Weight_of G).e - EL.e in rng PFS by A10,FUNCT_1:def 3;
then
A26: P.tolerance(EL) <= (the_Weight_of G).e-EL.e by A4,A20,Def16;
thus 0 <= EL2.e;
EL.e + P.tolerance(EL) = EL2.e by A4,A7,A8,A25,Def17;
then EL2.e <= (the_Weight_of G).e - EL.e + EL.e by A26,XREAL_1:7;
hence EL2.e <= (the_Weight_of G).e;
end;
suppose
A27: e DJoins P.(n+2),P.n,G;
thus 0 <= EL2.e;
EL2.e = EL.e - P.tolerance(EL) by A4,A7,A8,A11,A27,Def17;
then EL2.e <= EL.e - 0 by XREAL_1:13;
hence EL2.e <= (the_Weight_of G).e by A6,XXREAL_0:2;
end;
end;
hence 0 <= EL2.e & EL2.e <= (the_Weight_of G).e;
end;
end;
hence 0 <= EL2.e & EL2.e <= (the_Weight_of G).e;
end;
hence for e being set st e in the_Edges_of G holds 0 <= EL2.e & EL2.e <= (
the_Weight_of G).e;
let v be Vertex of G;
assume that
A28: v <> source and
A29: v <> sink;
A30: Sum (EL | v.edgesIn()) = Sum (EL | v.edgesOut()) by A2,A28,A29;
now
per cases;
suppose
v in P.vertices();
then consider n being odd Element of NAT such that
A31: n <= len P and
A32: P.n = v by GLIB_001:87;
A33: now
assume n = len P;
then v = P.last() by A32,GLIB_001:def 7
.= sink by A3,GLIB_001:def 23;
hence contradiction by A29;
end;
then
A34: n < len P by A31,XXREAL_0:1;
A35: now
assume n = 1;
then v = P.first() by A32,GLIB_001:def 6
.= source by A3,GLIB_001:def 23;
hence contradiction by A28;
end;
A36: now
A37: n+0 < n+2 by XREAL_1:8;
assume
A38: v = P.(n+2);
n+2 <= len P by A34,GLIB_001:1;
hence contradiction by A32,A35,A38,A37,GLIB_001:def 28;
end;
1 <= n by ABIAN:12;
then 1 < n by A35,XXREAL_0:1;
then 1+1 <= n by NAT_1:13;
then reconsider n2 = n-2*1 as odd Element of NAT by INT_1:5;
set e1 = P.(n2+1), e2 = P.(n+1), T = P.tolerance(EL);
A39: 1 <= n2+1 by NAT_1:11;
A40: P.(n2+2) = v by A32;
A41: now
let e be set;
assume that
A42: e in v.edgesIn() or e in v.edgesOut() and
A43: e <> e1 and
A44: e <> e2;
now
assume e in P.edges();
then consider
v1,v2 being Vertex of G, m being odd Element of NAT such
that
A45: m+2 <= len P and
A46: v1 = P.m and
A47: e = P.(m+1) and
A48: v2 = P.(m+2) and
A49: e Joins v1,v2,G by GLIB_001:103;
A50: now
per cases by A42;
suppose
e in v.edgesIn();
then (the_Target_of G).e = v by GLIB_000:56;
hence v1 = v or v2 = v by A49;
end;
suppose
e in v.edgesOut();
then (the_Source_of G).e = v by GLIB_000:58;
hence v1 = v or v2 = v by A49;
end;
end;
A51: m+2-2 < len P - 0 by A45,XREAL_1:15;
now
per cases by A50;
suppose
A52: v1 = v;
now
per cases by XXREAL_0:1;
suppose
m < n;
hence contradiction by A31,A32,A33,A46,A52,GLIB_001:def 28;
end;
suppose
m = n;
hence contradiction by A44,A47;
end;
suppose
n < m;
hence contradiction by A32,A46,A51,A52,GLIB_001:def 28;
end;
end;
hence contradiction;
end;
suppose
A53: v2 = v;
now
per cases by XXREAL_0:1;
suppose
m+2 < n;
hence contradiction by A31,A32,A33,A48,A53,GLIB_001:def 28;
end;
suppose
m+2 = n;
hence contradiction by A43,A47;
end;
suppose
n < m+2;
hence contradiction by A32,A35,A45,A48,A53,GLIB_001:def 28;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence not e in P.edges();
end;
A54: now
A55: n+2 <= len P by A34,GLIB_001:1;
A56: n + 0 < n+2 by XREAL_1:8;
assume that
A57: e2 DJoins v,P.(n+2),G and
A58: e2 DJoins P.(n+2),v,G;
P.n = (the_Source_of G).e2 by A32,A57
.= P.(n+2) by A58;
hence contradiction by A35,A56,A55,GLIB_001:def 28;
end;
n2 < n - 0 by XREAL_1:15;
then
A59: n2+1 < n+1 by XREAL_1:8;
n+1 <= len P by A34,NAT_1:13;
then
A60: e1 <> e2 by A39,A59,GLIB_001:138;
A61: now
n2 < n - 0 by XREAL_1:15;
hence P.n2 <> v by A31,A32,A33,GLIB_001:def 28;
end;
A62: not e1 DJoins P.n2,v,G or not e1 DJoins v,P.n2,G by A61;
A63: n2 < len P - 0 by A31,XREAL_1:15;
then
A64: e1 Joins P.n2,P.(n2+2),G by GLIB_001:def 3;
A65: e2 Joins v,P.(n+2),G by A32,A34,GLIB_001:def 3;
now
per cases by A32,A64,A65;
suppose
A66: e1 DJoins P.n2,v,G & e2 DJoins v,P.(n+2),G;
set XIN = (EL|v.edgesIn()) +* (e1.-->(EL.e1 + T));
A67: e1 in v.edgesIn() by A66,GLIB_000:57;
dom (e1.-->(EL.e1+T)) = {e1};
then
A69: dom XIN = dom (EL|v.edgesIn()) \/ {e1} by FUNCT_4:def 1
.= v.edgesIn() \/ {e1} by PARTFUN1:def 2
.= v.edgesIn() by A67,ZFMISC_1:40;
then reconsider XIN as Rbag of v.edgesIn() by PARTFUN1:def 2
,RELAT_1:def 18;
A70: now
let e be object;
assume e in dom (EL2|v.edgesIn());
then
A71: e in v.edgesIn();
then
A72: (the_Target_of G).e = v by GLIB_000:56;
now
per cases;
suppose
A73: e = e1;
then e in dom (e1.-->(EL.e1+T)) by TARSKI:def 1;
hence XIN.e = (e1.-->(EL.e1+T)).e1 by A73,FUNCT_4:13
.= EL.e1 + T by FUNCOP_1:72
.= EL2.e by A4,A63,A40,A66,A73,Def17;
end;
suppose
A74: e <> e1;
A75: now
assume e in P.edges();
then consider
v1,v2 being Vertex of G,m being odd Element of
NAT such that
A76: m+2 <= len P and
A77: v1 = P.m and
A78: e = P.(m+1) and
A79: v2=P.(m+2) and
A80: e Joins v1,v2,G by GLIB_001:103;
A81: m+2-2 < len P - 0 by A76,XREAL_1:15;
now
per cases by A72,A80;
suppose
A82: v = v1;
now
per cases by XXREAL_0:1;
suppose
m < n;
hence contradiction by A31,A32,A33,A77,A82,
GLIB_001:def 28;
end;
suppose
A83: m = n;
A84: n+2-2 < n+2-0 by XREAL_1:15;
A85: n+2 <= len P by A34,GLIB_001:1;
P.(n+2) = P.n by A32,A66,A72,A78,A83;
hence contradiction by A35,A84,A85,GLIB_001:def 28;
end;
suppose
n < m;
hence contradiction by A32,A77,A81,A82,
GLIB_001:def 28;
end;
end;
hence contradiction;
end;
suppose
A86: v = v2;
now
per cases by XXREAL_0:1;
suppose
m+2 < n;
hence contradiction by A31,A32,A33,A79,A86,
GLIB_001:def 28;
end;
suppose
m+2 = n;
hence contradiction by A74,A78;
end;
suppose
n < m+2;
hence contradiction by A32,A35,A76,A79,A86,
GLIB_001:def 28;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
not e in dom (e1.-->(EL.e1+T)) by A74,TARSKI:def 1;
then XIN.e = (EL|v.edgesIn()).e by FUNCT_4:11
.= EL.e by A71,FUNCT_1:49;
hence EL2.e = XIN.e by A4,A71,A75,Def17;
end;
end;
hence (EL2|v.edgesIn()).e = XIN.e by A71,FUNCT_1:49;
end;
dom (EL2|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2;
then
A87: Sum (EL2|v.edgesIn())=Sum XIN by A69,A70,FUNCT_1:2;
A88: dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2;
set XOUT= (EL|v.edgesOut())+* (e2.-->(EL.e2 + T));
A89: e2 in v.edgesOut() by A66,GLIB_000:59;
dom (e2.-->(EL.e2+T)) = {e2};
then
A91: dom XOUT = dom (EL|v.edgesOut())\/{e2} by FUNCT_4:def 1
.= v.edgesOut() \/ {e2} by PARTFUN1:def 2
.= v.edgesOut() by A89,ZFMISC_1:40;
then reconsider XOUT as Rbag of v.edgesOut() by PARTFUN1:def 2
,RELAT_1:def 18;
A92: now
let e be object;
assume e in dom (EL2|v.edgesOut());
then
A93: e in v.edgesOut();
then
A94: (the_Source_of G).e = v by GLIB_000:58;
now
per cases;
suppose
A95: e = e2;
then e in dom (e2.-->(EL.e2+T)) by TARSKI:def 1;
hence XOUT.e = (e2.-->(EL.e2+T)).e2 by A95,FUNCT_4:13
.= EL.e2 + T by FUNCOP_1:72
.= EL2.e by A4,A32,A34,A66,A95,Def17;
end;
suppose
A96: e <> e2;
A97: now
assume e in P.edges();
then consider
v1,v2 being Vertex of G,m being odd Element of
NAT such that
A98: m+2 <= len P and
A99: v1 = P.m and
A100: e = P.(m+1) and
A101: v2=P.(m+2) and
A102: e Joins v1,v2,G by GLIB_001:103;
A103: m+2-2 < len P - 0 by A98,XREAL_1:15;
now
per cases by A94,A102;
suppose
A104: v = v1;
now
per cases by XXREAL_0:1;
suppose
m < n;
hence contradiction by A31,A32,A33,A99,A104,
GLIB_001:def 28;
end;
suppose
m = n;
hence contradiction by A96,A100;
end;
suppose
n < m;
hence contradiction by A32,A99,A103,A104,
GLIB_001:def 28;
end;
end;
hence contradiction;
end;
suppose
A105: v = v2;
now
per cases by XXREAL_0:1;
suppose
m+2 < n;
hence contradiction by A31,A32,A33,A101,A105,
GLIB_001:def 28;
end;
suppose
A106: m+2 = n;
A107: n2 < n - 0 by XREAL_1:15;
P.n2 = P.n by A32,A66,A94,A100,A106;
hence contradiction by A31,A33,A107,GLIB_001:def 28
;
end;
suppose
n < m+2;
hence contradiction by A32,A35,A98,A101,A105,
GLIB_001:def 28;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
not e in dom (e2.-->(EL.e2+T)) by A96,TARSKI:def 1;
then XOUT.e = (EL|v.edgesOut()).e by FUNCT_4:11
.= EL.e by A93,FUNCT_1:49;
hence EL2.e = XOUT.e by A4,A93,A97,Def17;
end;
end;
hence (EL2|v.edgesOut()).e = XOUT.e by A93,FUNCT_1:49;
end;
Sum XIN = Sum (EL|v.edgesIn()) + (T + EL.e1) - (EL|v
.edgesIn()).e1 by GLIB_004:9
.= Sum (EL|v.edgesOut()) + T + EL.e1 - EL.e1 by A30,A67,
FUNCT_1:49
.= Sum (EL|v.edgesOut()) + T + EL.e2 - EL.e2
.= Sum (EL|v.edgesOut()) + (T + EL.e2) - (EL|v.edgesOut()).e2
by A89,FUNCT_1:49
.= Sum XOUT by GLIB_004:9;
hence Sum (EL2 | v.edgesIn()) = Sum (EL2 | v.edgesOut()) by A91,A87
,A88,A92,FUNCT_1:2;
end;
suppose
A108: e1 DJoins P.n2,v,G & e2 DJoins P.(n+2),v,G;
A109: dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2;
A110: now
let e be object;
assume
A111: e in dom (EL2|v.edgesOut());
then
A112: (EL|v.edgesOut()).e = EL.e by FUNCT_1:49;
A113: e in v.edgesOut() by A111;
then
A114: (the_Source_of G).e = v by GLIB_000:58;
then
A115: e <> e2 by A36,A108;
e <> e1 by A61,A108,A114;
then
A116: not e in P.edges() by A41,A113,A115;
(EL2|v.edgesOut()).e = EL2.e by A111,FUNCT_1:49;
hence (EL2|v.edgesOut()).e = (EL|v.edgesOut()).e by A4,A113,A112
,A116,Def17;
end;
dom (EL|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2;
then
A117: EL2|v.edgesOut() = EL|v.edgesOut() by A109,A110,FUNCT_1:2;
set XIN1 = (EL|v.edgesIn())+*(e1.-->(EL.e1+T));
set XIN2 = XIN1 +* (e2.-->(EL.e2-T));
A118: dom (EL2|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2;
A119: e2 in v.edgesIn() by A108,GLIB_000:57;
A120: e1 in v.edgesIn() by A108,GLIB_000:57;
A121: EL2.e1 = EL.e1 + T by A4,A63,A40,A108,Def17;
A123: dom XIN1 = dom (EL|v.edgesIn()) \/ dom (e1.-->(EL.e1+T)) by
FUNCT_4:def 1
.= dom (EL|v.edgesIn()) \/ {e1}
.= v.edgesIn() \/ {e1} by PARTFUN1:def 2
.= v.edgesIn() by A120,ZFMISC_1:40;
then reconsider XIN1 as Rbag of v.edgesIn() by PARTFUN1:def 2
,RELAT_1:def 18;
A124: dom XIN2 = dom XIN1 \/ dom (e2.-->(EL.e2-T)) by FUNCT_4:def 1
.= v.edgesIn() \/ {e2} by A123
.= v.edgesIn() by A119,ZFMISC_1:40;
then reconsider XIN2 as Rbag of v.edgesIn() by PARTFUN1:def 2
,RELAT_1:def 18;
A126: EL2.e2 = EL.e2 - T by A4,A32,A34,A54,A108,Def17;
A127: now
let e be object;
assume
A128: e in dom (EL2|v.edgesIn());
then
A129: e in v.edgesIn();
A130: (EL2|v.edgesIn()).e = EL2.e by A128,FUNCT_1:49;
now
per cases;
suppose
A131: e = e1;
then
A132: e in dom (e1.-->(EL.e1+T)) by TARSKI:def 1;
not e in dom (e2.-->(EL.e2-T)) by A60,A131,TARSKI:def 1;
then XIN2.e = XIN1.e by FUNCT_4:11
.= (e1.-->(EL.e1+T)).e by A132,FUNCT_4:13
.= EL2.e by A121,A131,FUNCOP_1:72;
hence (EL2|v.edgesIn()).e = XIN2.e by A128,FUNCT_1:49;
end;
suppose
A133: e = e2;
then e in dom (e2.-->(EL.e2-T)) by TARSKI:def 1;
then XIN2.e = (e2.-->(EL.e2-T)).e2 by A133,FUNCT_4:13
.= EL2.e by A126,A133,FUNCOP_1:72;
hence (EL2|v.edgesIn()).e = XIN2.e by A128,FUNCT_1:49;
end;
suppose
A134: e <> e1 & e <> e2;
then
A135: not e in dom (e1.-->(EL.e1+T)) by TARSKI:def 1;
A136: not e in P.edges() by A41,A129,A134;
not e in dom (e2.-->(EL.e2-T)) by A134,TARSKI:def 1;
then XIN2.e = XIN1.e by FUNCT_4:11
.= (EL|v.edgesIn()).e by A135,FUNCT_4:11
.= EL.e by A129,FUNCT_1:49;
hence (EL2|v.edgesIn()).e = XIN2.e by A4,A129,A130,A136,Def17
;
end;
end;
hence (EL2|v.edgesIn()).e = XIN2.e;
end;
not e2 in dom (e1.-->(EL.e1+T)) by A60,TARSKI:def 1;
then XIN1.e2 = (EL|v.edgesIn()).e2 by FUNCT_4:11
.= EL.e2 by A119,FUNCT_1:49;
then Sum (EL2|v.edgesIn()) = Sum XIN1 + (EL.e2-T) - EL.e2 by A124
,A118,A127,FUNCT_1:2,GLIB_004:9
.= Sum XIN1 - (EL.e2 - (EL.e2 - T))
.= Sum (EL|v.edgesIn())+(EL.e1+T)-(EL|v.edgesIn()).e1-T by
GLIB_004:9
.= Sum (EL|v.edgesIn())+T+EL.e1-EL.e1-T by A120,FUNCT_1:49
.= Sum (EL|v.edgesIn());
hence
Sum (EL2|v.edgesIn()) = Sum (EL2|v.edgesOut()) by A2,A28,A29,A117;
end;
suppose
A137: e1 DJoins v,P.n2,G & e2 DJoins v,P.(n+2),G;
A138: dom (EL2|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2;
A139: now
let e be object;
assume
A140: e in dom (EL2|v.edgesIn());
then
A141: (EL|v.edgesIn()).e = EL.e by FUNCT_1:49;
A142: e in v.edgesIn() by A140;
then
A143: (the_Target_of G).e = v by GLIB_000:56;
then
A144: e <> e2 by A36,A137;
e <> e1 by A61,A137,A143;
then
A145: not e in P.edges() by A41,A142,A144;
(EL2|v.edgesIn()).e = EL2.e by A140,FUNCT_1:49;
hence (EL2|v.edgesIn()).e = (EL|v.edgesIn()).e by A4,A142,A141
,A145,Def17;
end;
set XOUT1 = (EL|v.edgesOut())+*(e1.-->(EL.e1-T));
set XOUT2 = XOUT1 +* (e2.-->(EL.e2+T));
A146: dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2;
A147: e2 in v.edgesOut() by A137,GLIB_000:59;
A148: dom (EL|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2;
A149: e1 in v.edgesOut() by A137,GLIB_000:59;
A150: EL2.e2 = EL.e2 + T by A4,A32,A34,A137,Def17;
A152: dom XOUT1 = dom (EL|v.edgesOut()) \/ dom (e1.-->(EL.e1-T))
by FUNCT_4:def 1
.= dom (EL|v.edgesOut()) \/ {e1}
.= v.edgesOut() \/ {e1} by PARTFUN1:def 2
.= v.edgesOut() by A149,ZFMISC_1:40;
then reconsider XOUT1 as Rbag of v.edgesOut() by PARTFUN1:def 2
,RELAT_1:def 18;
A153: dom XOUT2 = dom XOUT1\/dom (e2.-->(EL.e2+T)) by FUNCT_4:def 1
.= v.edgesOut() \/ {e2} by A152
.= v.edgesOut() by A147,ZFMISC_1:40;
then reconsider XOUT2 as Rbag of v.edgesOut() by PARTFUN1:def 2
,RELAT_1:def 18;
A155: EL2.e1 = EL.e1 - T by A4,A63,A40,A62,A137,Def17;
A156: now
let e be object;
assume
A157: e in dom (EL2|v.edgesOut());
then
A158: e in v.edgesOut();
A159: (EL2|v.edgesOut()).e = EL2.e by A157,FUNCT_1:49;
now
per cases;
suppose
A160: e = e1;
then
A161: e in dom (e1.-->(EL.e1-T)) by TARSKI:def 1;
not e in dom (e2.-->(EL.e2+T)) by A60,A160,TARSKI:def 1;
then XOUT2.e = XOUT1.e by FUNCT_4:11
.= (e1.-->(EL.e1-T)).e by A161,FUNCT_4:13
.= EL2.e by A155,A160,FUNCOP_1:72;
hence (EL2|v.edgesOut()).e=XOUT2.e by A157,FUNCT_1:49;
end;
suppose
A162: e = e2;
then e in dom (e2.-->(EL.e2+T)) by TARSKI:def 1;
then XOUT2.e = (e2.-->(EL.e2+T)).e by FUNCT_4:13
.= EL2.e by A150,A162,FUNCOP_1:72;
hence (EL2|v.edgesOut()).e=XOUT2.e by A157,FUNCT_1:49;
end;
suppose
A163: e <> e1 & e <> e2;
then
A164: not e in dom (e1.-->(EL.e1-T)) by TARSKI:def 1;
A165: not e in P.edges() by A41,A158,A163;
not e in dom (e2.-->(EL.e2+T)) by A163,TARSKI:def 1;
then XOUT2.e = XOUT1.e by FUNCT_4:11
.= (EL|v.edgesOut()).e by A164,FUNCT_4:11
.= EL.e by A158,FUNCT_1:49;
hence (EL2|v.edgesOut()).e = XOUT2.e by A4,A158,A159,A165
,Def17;
end;
end;
hence (EL2|v.edgesOut()).e = XOUT2.e;
end;
not e2 in dom (e1.-->(EL.e1-T)) by A60,TARSKI:def 1;
then XOUT1.e2 = (EL|v.edgesOut()).e2 by FUNCT_4:11
.= EL.e2 by A147,FUNCT_1:49;
then Sum (EL2|v.edgesOut()) = Sum XOUT1 + (EL.e2+T) - EL.e2 by A153
,A146,A156,FUNCT_1:2,GLIB_004:9
.= Sum XOUT1 - EL.e2 + EL.e2 + T
.= Sum (EL|v.edgesOut()) + (EL.e1 - T) - (EL|v.edgesOut()).e1
+ T by GLIB_004:9
.= Sum (EL|v.edgesOut()) + EL.e1 - T - EL.e1 + T by A149,
FUNCT_1:49
.= Sum (EL|v.edgesOut());
hence Sum (EL2|v.edgesIn()) = Sum (EL2|v.edgesOut()) by A30,A138
,A148,A139,FUNCT_1:2;
end;
suppose
A166: e1 DJoins v,P.n2,G & e2 DJoins P.(n+2),v,G;
set XIN = (EL|v.edgesIn())+*(e2.-->(EL.e2-T));
A167: e2 in v.edgesIn() by A166,GLIB_000:57;
dom (e2.-->(EL.e2-T)) = {e2};
then
A169: dom XIN = dom (EL|v.edgesIn()) \/ {e2} by FUNCT_4:def 1
.= v.edgesIn() \/ {e2} by PARTFUN1:def 2
.= v.edgesIn() by A167,ZFMISC_1:40;
then reconsider XIN as Rbag of v.edgesIn() by PARTFUN1:def 2
,RELAT_1:def 18;
A170: EL2.e2 = EL.e2 - T by A4,A32,A34,A54,A166,Def17;
A171: now
let e be object;
assume e in dom (EL2|v.edgesIn());
then
A172: e in v.edgesIn();
then
A173: (the_Target_of G).e = v by GLIB_000:56;
now
per cases;
suppose
A174: e = e2;
then e in dom (e2.-->(EL.e2-T)) by TARSKI:def 1;
hence XIN.e = (e2.-->(EL.e2-T)).e2 by A174,FUNCT_4:13
.= EL2.e by A170,A174,FUNCOP_1:72;
end;
suppose
A175: e <> e2;
then not e in dom (e2.-->(EL.e2-T)) by TARSKI:def 1;
then
A176: XIN.e = (EL|v.edgesIn()).e by FUNCT_4:11
.= EL.e by A172,FUNCT_1:49;
e <> e1 by A61,A166,A173;
then not e in P.edges() by A41,A172,A175;
hence EL2.e = XIN.e by A4,A172,A176,Def17;
end;
end;
hence XIN.e = (EL2|v.edgesIn()).e by A172,FUNCT_1:49;
end;
dom (EL2|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2;
then
A177: Sum (EL2|v.edgesIn()) = Sum (EL|v.edgesIn()) + (EL.e2-T) - (
EL|v.edgesIn()).e2 by A169,A171,FUNCT_1:2,GLIB_004:9
.= Sum (EL|v.edgesIn()) + EL.e2 - T - EL.e2 by A167,FUNCT_1:49
.= Sum (EL|v.edgesIn()) - T;
set XOUT= (EL|v.edgesOut())+*(e1.-->(EL.e1-T));
A178: e1 in v.edgesOut() by A166,GLIB_000:59;
dom (e1.-->(EL.e1-T)) = {e1};
then
A180: dom XOUT = dom (EL|v.edgesOut())\/{e1} by FUNCT_4:def 1
.= v.edgesOut() \/ {e1} by PARTFUN1:def 2
.= v.edgesOut() by A178,ZFMISC_1:40;
then reconsider XOUT as Rbag of v.edgesOut() by PARTFUN1:def 2
,RELAT_1:def 18;
A181: EL2.e1 = EL.e1 - T by A4,A63,A40,A62,A166,Def17;
A182: now
let e be object;
assume e in dom (EL2|v.edgesOut());
then
A183: e in v.edgesOut();
then
A184: (the_Source_of G).e = v by GLIB_000:58;
now
per cases;
suppose
A185: e = e1;
then e in dom (e1.-->(EL.e1-T)) by TARSKI:def 1;
hence XOUT.e = (e1.-->(EL.e1-T)).e1 by A185,FUNCT_4:13
.= EL2.e by A181,A185,FUNCOP_1:72;
end;
suppose
A186: e <> e1;
then not e in dom (e1.-->(EL.e1-T)) by TARSKI:def 1;
then
A187: XOUT.e = (EL|v.edgesOut()).e by FUNCT_4:11
.= EL.e by A183,FUNCT_1:49;
e <> e2 by A36,A166,A184;
then not e in P.edges() by A41,A183,A186;
hence EL2.e = XOUT.e by A4,A183,A187,Def17;
end;
end;
hence XOUT.e = (EL2|v.edgesOut()).e by A183,FUNCT_1:49;
end;
dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2;
then Sum (EL2|v.edgesOut()) = Sum (EL|v.edgesOut()) + (EL.e1-T)-(
EL|v.edgesOut()).e1 by A180,A182,FUNCT_1:2,GLIB_004:9
.= Sum (EL|v.edgesOut()) + EL.e1 - T - EL.e1 by A178,FUNCT_1:49
.= Sum (EL|v.edgesIn()) - T by A30;
hence Sum (EL2 | v.edgesIn()) = Sum (EL2 | v.edgesOut()) by A177;
end;
end;
hence Sum (EL2 | v.edgesIn()) = Sum (EL2 | v.edgesOut());
end;
suppose
A188: not v in P.vertices();
A189: dom (EL|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2;
A190: now
let e be object;
assume
A191: e in dom (EL|v.edgesOut());
then
A192: (EL2|v.edgesOut()).e = EL2.e by FUNCT_1:49;
A193: e in v.edgesOut() by A191;
A194: now
consider x being set such that
A195: e DJoins v,x,G by A193,GLIB_000:59;
assume
A196: e in P.edges();
e Joins v,x,G by A195;
hence contradiction by A188,A196,GLIB_001:105;
end;
(EL|v.edgesOut()).e = EL.e by A191,FUNCT_1:49;
hence (EL|v.edgesOut()).e = (EL2|v.edgesOut()).e by A4,A193,A192,A194
,Def17;
end;
A197: dom (EL|v.edgesIn()) = v.edgesIn() by PARTFUN1:def 2;
A198: now
let e be object;
assume
A199: e in dom (EL|v.edgesIn());
then
A200: (EL2|v.edgesIn()).e = EL2.e by FUNCT_1:49;
A201: now
consider x being set such that
A202: e DJoins x,v,G by A199,GLIB_000:57;
assume
A203: e in P.edges();
e Joins x,v,G by A202;
hence contradiction by A188,A203,GLIB_001:105;
end;
(EL|v.edgesIn()).e = EL.e by A199,FUNCT_1:49;
hence (EL|v.edgesIn()).e = (EL2|v.edgesIn()).e by A4,A197,A199,A200
,A201,Def17;
end;
dom (EL2|v.edgesOut()) = v.edgesOut() by PARTFUN1:def 2;
then
A204: EL | v.edgesOut() = EL2 | v.edgesOut() by A189,A190,FUNCT_1:2;
dom (EL|v.edgesIn()) = dom (EL2|v.edgesIn()) by A197,PARTFUN1:def 2;
hence Sum (EL2|v.edgesIn()) = Sum (EL|v.edgesIn()) by A198,FUNCT_1:2
.= Sum (EL2|v.edgesOut()) by A2,A28,A29,A204;
end;
end;
hence Sum (EL2 | v.edgesIn()) = Sum (EL2 | v.edgesOut());
end;
hence thesis;
end;
theorem Th15:
for G being _finite natural-weighted WGraph, EL being
FF:ELabeling of G, source,sink being set, P being Path of G st source <> sink &
P is_Walk_from source,sink & P is_augmenting_wrt EL holds EL.flow(source,sink)
+ P.tolerance(EL) = (FF:PushFlow(EL,P)).flow(source,sink)
proof
let G be _finite natural-weighted WGraph, EL being FF:ELabeling of G, source,
sink be set, P be Path of G such that
A1: source <> sink and
A2: P is_Walk_from source,sink and
A3: P is_augmenting_wrt EL;
A4: P.last() = sink by A2,GLIB_001:def 23;
P.first() = source by A2,GLIB_001:def 23;
then P is non trivial by A1,A4,GLIB_001:127;
then 3 <= len P by GLIB_001:125;
then reconsider lenP2g = len P - 2*1 as odd Element of NAT by INT_1:5
,XXREAL_0:2;
set e1 = P.(lenP2g+1);
set EI1 = EL|G.edgesInto({sink}), EO1 = EL|G.edgesOutOf({sink});
set EL2 = FF:PushFlow(EL,P), T = P.tolerance(EL);
A5: P.(len P) = sink by A2,GLIB_001:17;
A6: lenP2g < len P - 0 by XREAL_1:15;
then
A7: e1 Joins P.lenP2g, P.(lenP2g+2), G by GLIB_001:def 3;
then
A8: e1 in the_Edges_of G;
now
per cases;
suppose
A9: e1 DJoins P.lenP2g, P.(lenP2g+2), G;
then (the_Target_of G).e1 = P.(lenP2g+2)
.= sink by A2,GLIB_001:17;
then (the_Target_of G).e1 in {sink} by TARSKI:def 1;
then
A10: e1 in G.edgesInto({sink}) by A8,GLIB_000:def 26;
set EI2 = EI1+*(e1.-->(EI1.e1 + T));
A11: dom (EL2|G.edgesInto({sink})) = G.edgesInto({sink}) by PARTFUN1:def 2;
A12: dom EI2 = dom EI1 \/ dom (e1.-->(EI1.e1 + T)) by FUNCT_4:def 1
.= dom EI1 \/ {e1}
.= G.edgesInto({sink}) \/ {e1} by PARTFUN1:def 2
.= G.edgesInto({sink}) by A10,ZFMISC_1:40;
then reconsider EI2 as Rbag of G.edgesInto({sink}) by PARTFUN1:def 2
,RELAT_1:def 18;
A13: EL2.e1 = EL.e1 + T by A3,A6,A9,Def17;
now
let e be object;
assume
A14: e in dom (EL2|G.edgesInto({sink}));
then
A15: e in G.edgesInto({sink});
A16: (EL2|G.edgesInto({sink})).e = EL2.e by A14,FUNCT_1:49;
(the_Target_of G).e in {sink} by A15,GLIB_000:def 26;
then
A17: (the_Target_of G).e = sink by TARSKI:def 1;
now
per cases;
suppose
A18: e = e1;
then e in {e1} by TARSKI:def 1;
then e in dom (e1.-->(EI1.e1+T));
then EI2.e = (e1.-->(EI1.e1+T)).e1 by A18,FUNCT_4:13
.= EI1.e1 + T by FUNCOP_1:72
.= EL2.e1 by A13,A15,A18,FUNCT_1:49;
hence (EL2|G.edgesInto({sink})).e = EI2.e by A14,A18,FUNCT_1:49;
end;
suppose
A19: e <> e1;
A20: now
assume e in P.edges();
then consider
v1,v2 being Vertex of G,m being odd Element of NAT such
that
A21: m+2 <= len P and
A22: v1 = P.m and
A23: e = P.(m+1) and
A24: v2 = P.(m+2) and
A25: e Joins v1,v2,G by GLIB_001:103;
now
per cases by A17,A25;
suppose
A26: v1 = sink;
A27: m+2-2 < len P - 0 by A21,XREAL_1:15;
P.m = P.(len P) by A2,A22,A26,GLIB_001:17;
then m = 1 by A27,GLIB_001:def 28;
hence contradiction by A1,A2,A22,A26,GLIB_001:17;
end;
suppose
v2 = sink;
then
A28: P.(m+2) = P.(len P) by A2,A24,GLIB_001:17;
now
assume m+2 < len P;
then m+2 = 1 by A28,GLIB_001:def 28;
then m = 1-2;
hence contradiction by ABIAN:12;
end;
then m + 2 = len P by A21,XXREAL_0:1;
hence contradiction by A19,A23;
end;
end;
hence contradiction;
end;
not e in {e1} by A19,TARSKI:def 1;
then not e in dom (e1.-->(EI1.e1+T));
then EI2.e = EI1.e by FUNCT_4:11
.= EL.e by A15,FUNCT_1:49;
hence (EL2|G.edgesInto({sink})).e = EI2.e by A3,A15,A16,A20,Def17;
end;
end;
hence (EL2|G.edgesInto({sink})).e = EI2.e;
end;
then
A29: Sum (EL2|G.edgesInto({sink})) = Sum EI1 + (T + EI1.e1) - EI1.e1 by A12
,A11,FUNCT_1:2,GLIB_004:9
.= Sum EI1 + T;
A30: dom (EL2|G.edgesOutOf({sink})) = G.edgesOutOf({sink}) by PARTFUN1:def 2;
A31: now
let e be object;
assume
A32: e in dom (EL2|G.edgesOutOf({sink}));
then
A33: e in G.edgesOutOf({sink});
then (the_Source_of G).e in {sink} by GLIB_000:def 27;
then
A34: (the_Source_of G).e = sink by TARSKI:def 1;
now
assume e in P.edges();
then consider
v1,v2 being Vertex of G, m being odd Element of NAT such
that
A35: m+2 <= len P and
A36: v1 = P.m and
A37: e = P.(m+1) and
A38: v2 = P.(m+2) and
A39: e Joins v1,v2,G by GLIB_001:103;
now
per cases by A34,A39;
suppose
A40: v1 = sink;
A41: m+2-2 < len P - 0 by A35,XREAL_1:15;
P.m = P.(len P) by A2,A36,A40,GLIB_001:17;
then m = 1 by A41,GLIB_001:def 28;
hence contradiction by A1,A2,A36,A40,GLIB_001:17;
end;
suppose
v2 = sink;
then
A42: P.(m+2) = P.(len P) by A2,A38,GLIB_001:17;
now
assume m+2 < len P;
then m+2 = 1 by A42,GLIB_001:def 28;
then 1 <= 1-2 by ABIAN:12;
hence contradiction;
end;
then m + 2 = len P by A35,XXREAL_0:1;
then
A43: P.lenP2g = sink by A9,A34,A37;
then lenP2g = 1 by A6,A5,GLIB_001:def 28;
hence contradiction by A1,A2,A43,GLIB_001:17;
end;
end;
hence contradiction;
end;
then EL2.e = EL.e by A3,A33,Def17
.= EO1.e by A33,FUNCT_1:49;
hence (EL2|G.edgesOutOf({sink})).e = EO1.e by A32,FUNCT_1:49;
end;
dom EO1 = G.edgesOutOf({sink}) by PARTFUN1:def 2;
hence EL2.flow(source,sink) = Sum EI1 + T - Sum EO1 by A29,A30,A31,
FUNCT_1:2
.= Sum EI1 - Sum EO1 + T
.= EL.flow(source,sink) + T;
end;
suppose
A44: not e1 DJoins P.lenP2g, P.(lenP2g+2), G;
then
A45: e1 DJoins P.(lenP2g+2),P.lenP2g,G by A7;
then (the_Source_of G).e1 = P.(lenP2g+2)
.= sink by A2,GLIB_001:17;
then (the_Source_of G).e1 in {sink} by TARSKI:def 1;
then
A46: e1 in G.edgesOutOf({sink}) by A8,GLIB_000:def 27;
set EO2 = EO1+*(e1.-->(EO1.e1-T));
A47: dom (EL2|G.edgesOutOf({sink})) = G.edgesOutOf({sink}) by PARTFUN1:def 2;
A48: dom EO2 = dom EO1 \/ dom (e1.-->(EO1.e1 - T)) by FUNCT_4:def 1
.= dom EO1 \/ {e1}
.= G.edgesOutOf({sink}) \/ {e1} by PARTFUN1:def 2
.= G.edgesOutOf({sink}) by A46,ZFMISC_1:40;
then reconsider EO2 as Rbag of G.edgesOutOf({sink}) by PARTFUN1:def 2
,RELAT_1:def 18;
A49: EL2.e1 = EL.e1 - T by A3,A6,A44,Def17;
now
let e be object;
assume
A50: e in dom (EL2|G.edgesOutOf({sink}));
then
A51: e in G.edgesOutOf({sink});
A52: (EL2|G.edgesOutOf({sink})).e = EL2.e by A50,FUNCT_1:49;
(the_Source_of G).e in {sink} by A51,GLIB_000:def 27;
then
A53: (the_Source_of G).e = sink by TARSKI:def 1;
now
per cases;
suppose
A54: e = e1;
then e in {e1} by TARSKI:def 1;
then e in dom (e1.-->(EO1.e1-T));
then EO2.e = (e1.-->(EO1.e1-T)).e1 by A54,FUNCT_4:13
.= EO1.e1 - T by FUNCOP_1:72
.= EL2.e by A49,A51,A54,FUNCT_1:49;
hence (EL2|G.edgesOutOf({sink})).e = EO2.e by A50,FUNCT_1:49;
end;
suppose
A55: e <> e1;
A56: now
assume e in P.edges();
then consider
v1,v2 being Vertex of G, m being odd Element of NAT
such that
A57: m+2 <= len P and
A58: v1 = P.m and
A59: e = P.(m+1) and
A60: v2 = P.(m+2) and
A61: e Joins v1,v2,G by GLIB_001:103;
now
per cases by A53,A61;
suppose
A62: v1 = sink;
A63: m+2-2 < len P - 0 by A57,XREAL_1:15;
P.m = P.(len P) by A2,A58,A62,GLIB_001:17;
then m = 1 by A63,GLIB_001:def 28;
hence contradiction by A1,A2,A58,A62,GLIB_001:17;
end;
suppose
v2 = sink;
then
A64: P.(m+2) = P.(len P) by A2,A60,GLIB_001:17;
now
assume m+2 < len P;
then m+2 = 1 by A64,GLIB_001:def 28;
then 1 <= 1-2 by ABIAN:12;
hence contradiction;
end;
then m + 2 = len P by A57,XXREAL_0:1;
hence contradiction by A55,A59;
end;
end;
hence contradiction;
end;
not e in {e1} by A55,TARSKI:def 1;
then not e in dom (e1.-->(EO1.e1-T));
then EO2.e = EO1.e by FUNCT_4:11
.= EL.e by A51,FUNCT_1:49;
hence (EL2|G.edgesOutOf({sink})).e = EO2.e by A3,A51,A52,A56,Def17;
end;
end;
hence (EL2|G.edgesOutOf({sink})).e = EO2.e;
end;
then
A65: Sum (EL2|G.edgesOutOf({sink})) = Sum EO1 + (EO1.e1 - T) - EO1.e1
by A48,A47,FUNCT_1:2,GLIB_004:9
.= Sum EO1 - T;
A66: dom (EL2|G.edgesInto({sink})) = G.edgesInto({sink}) by PARTFUN1:def 2;
A67: now
let e be object;
assume
A68: e in dom (EL2|G.edgesInto({sink}));
then
A69: e in G.edgesInto({sink});
then (the_Target_of G).e in {sink} by GLIB_000:def 26;
then
A70: (the_Target_of G).e = sink by TARSKI:def 1;
now
assume e in P.edges();
then consider
v1,v2 being Vertex of G, m being odd Element of NAT such
that
A71: m+2 <= len P and
A72: v1 = P.m and
A73: e = P.(m+1) and
A74: v2 = P.(m+2) and
A75: e Joins v1,v2,G by GLIB_001:103;
now
per cases by A70,A75;
suppose
A76: v1 = sink;
A77: m+2-2 < len P - 0 by A71,XREAL_1:15;
P.m = P.(len P) by A2,A72,A76,GLIB_001:17;
then m = 1 by A77,GLIB_001:def 28;
hence contradiction by A1,A2,A72,A76,GLIB_001:17;
end;
suppose
v2 = sink;
then
A78: P.(m+2) = P.(len P) by A2,A74,GLIB_001:17;
now
assume m+2 < len P;
then m+2 = 1 by A78,GLIB_001:def 28;
then 1 <= 1-2 by ABIAN:12;
hence contradiction;
end;
then m + 2 = len P by A71,XXREAL_0:1;
then
A79: P.lenP2g = sink by A45,A70,A73;
then lenP2g = 1 by A6,A5,GLIB_001:def 28;
hence contradiction by A1,A2,A79,GLIB_001:17;
end;
end;
hence contradiction;
end;
then EL2.e = EL.e by A3,A69,Def17
.= EI1.e by A69,FUNCT_1:49;
hence (EL2|G.edgesInto({sink})).e = EI1.e by A68,FUNCT_1:49;
end;
dom EI1 = G.edgesInto({sink}) by PARTFUN1:def 2;
hence EL2.flow(source,sink) = Sum EI1 - (Sum EO1 - T) by A65,A66,A67,
FUNCT_1:2
.= Sum EI1 - Sum EO1 + T
.= EL.flow(source,sink) + T;
end;
end;
hence thesis;
end;
theorem Th16:
for G being _finite natural-weighted WGraph, source,sink being
Vertex of G, n being Nat st source <> sink holds FF:CompSeq(G,source,sink).n
has_valid_flow_from source,sink
proof
let G be _finite natural-weighted WGraph, source,sink be Vertex of G, n be
Nat;
set CS = FF:CompSeq(G,source,sink);
defpred P[Nat] means (CS.$1) has_valid_flow_from source,sink;
now
set G0 = CS.0;
A1: G0 = the_Edges_of G --> 0 by Def20;
hence for e being set st e in the_Edges_of G holds 0 <= G0.e & G0.e <= (
the_Weight_of G).e by FUNCOP_1:7;
let v be Vertex of G;
set B1 = EmptyBag v.edgesIn(), B2 = EmptyBag v.edgesOut();
set E1 = (G0|v.edgesIn()), E2 = (G0|v.edgesOut());
now
let e be set;
assume
A2: e in v.edgesOut();
then E2.e = G0.e by FUNCT_1:49
.= 0 by A1,A2,FUNCOP_1:7;
hence B2.e = E2.e by PBOOLE:5;
end;
then
A3: Sum E2 = Sum B2 by GLIB_004:6
.= 0 by UPROOTS:11;
assume that
v <> source and
v <> sink;
now
let e be set;
assume
A4: e in v.edgesIn();
then E1.e = G0.e by FUNCT_1:49
.= 0 by A1,A4,FUNCOP_1:7;
hence B1.e = E1.e by PBOOLE:5;
end;
then Sum E1 = Sum B1 by GLIB_004:6
.= 0 by UPROOTS:11;
hence Sum E1 = Sum E2 by A3;
end;
then
A5: P[ 0 ] by Def2;
assume
A6: source <> sink;
now
let n be Nat;
set Gn = CS.n, Gn1 = CS.(n+1);
assume
A7: Gn has_valid_flow_from source,sink;
A8: Gn1 = FF:Step(Gn,source,sink) by Def20;
now
per cases;
suppose
A9: sink in dom AP:FindAugPath(Gn,source);
set P = AP:GetAugPath(Gn,source,sink);
A10: P is_Walk_from source,sink by A9,Def14;
A11: P is_augmenting_wrt Gn by A9,Def14;
Gn1 = FF:PushFlow(Gn, P) by A8,A9,Def18;
hence P[n+1] by A6,A7,A10,A11,Th14;
end;
suppose
not sink in dom AP:FindAugPath(Gn,source);
hence P[n+1] by A7,A8,Def18;
end;
end;
hence P[n+1];
end;
then
A12: for n being Nat st P[n] holds P[n+1];
for n being Nat holds P[n] from NAT_1:sch 2(A5,A12);
hence thesis;
end;
theorem Th17:
for G being _finite natural-weighted WGraph,source,sink being
Vertex of G st source <> sink holds FF:CompSeq(G,source,sink) is halting
proof
let G be _finite natural-weighted WGraph, source, sink be Vertex of G;
set CS = FF:CompSeq(G,source,sink);
assume
A1: source <> sink;
now
set V = {source};
defpred P[Nat] means
$1 <= (CS.$1).flow(source,sink) & (CS.$1)
.flow(source,sink) is Element of NAT;
A2: source in V by TARSKI:def 1;
set W1 = (the_Weight_of G)|G.edgesDBetween(V,the_Vertices_of G \ V);
degree W1 = Sum W1;
then reconsider N = Sum W1 as Element of NAT;
set Gn1 = CS.(N+1);
assume
A3: for n being Nat holds CS.n <> CS.(n+1);
now
let n be Nat;
set Gn = CS.n, Gn1 = CS.(n+1);
assume that
A4: n <= Gn.flow(source,sink) and
A5: Gn.flow(source,sink) is Element of NAT;
reconsider GnF = Gn.flow(source,sink) as Element of NAT by A5;
set P = AP:GetAugPath(Gn,source,sink);
A6: Gn1 = FF:Step(Gn, source,sink) by Def20;
A7: now
assume not sink in dom AP:FindAugPath(Gn,source);
then Gn1 = Gn by A6,Def18;
hence contradiction by A3;
end;
then
A8: P is_augmenting_wrt Gn by Def14;
A9: P is_Walk_from source,sink by A7,Def14;
then
A10: P.last() = sink by GLIB_001:def 23;
Gn1 = FF:PushFlow(Gn,AP:GetAugPath(Gn,source,sink)) by A6,A7,Def18;
then
A11: GnF + P.tolerance(Gn) = Gn1.flow(source,sink) by A1,A8,A9,Th15;
then reconsider Gn1F = Gn1.flow(source,sink) as Element of NAT
by ORDINAL1:def 12;
P.first() = source by A9,GLIB_001:def 23;
then 0 < P.tolerance(Gn) by A1,A8,A10,Th13,GLIB_001:127;
then GnF + P.tolerance(Gn)-P.tolerance(Gn) < Gn1F-0 by A11,XREAL_1:15;
then n < Gn1F by A4,XXREAL_0:2;
hence n+1 <= Gn1.flow(source,sink) by NAT_1:13;
thus Gn1.flow(source,sink) is Element of NAT by A11,ORDINAL1:def 12;
end;
then
A12: for n being Nat st P[n] holds P[n+1];
now
set B1 = EmptyBag G.edgesInto({sink}),B2 = EmptyBag G.edgesOutOf({sink});
set G0 = CS.0;
set E1 = G0 | G.edgesInto({sink}), E2 = G0 | G.edgesOutOf({sink});
A13: G0 = the_Edges_of G --> 0 by Def20;
now
let e be set;
assume
A14: e in G.edgesInto({sink});
hence E1.e = G0.e by FUNCT_1:49
.= 0 by A13,A14,FUNCOP_1:7
.= B1.e by PBOOLE:5;
end;
then
A15: Sum E1 = Sum B1 by GLIB_004:6
.= 0 by UPROOTS:11;
now
let e be set;
assume
A16: e in G.edgesOutOf({sink});
hence E2.e = G0.e by FUNCT_1:49
.= 0 by A13,A16,FUNCOP_1:7
.= B2.e by PBOOLE:5;
end;
then
A17: Sum E2 = Sum B2 by GLIB_004:6
.= 0 by UPROOTS:11;
hence G0.flow(source,sink) = 0 qua Nat - 0 by A15;
thus G0.flow(source,sink) is Element of NAT by A15,A17;
end;
then
A18: P[ 0 ];
A19: for n being Nat holds P[n] from NAT_1:sch 2(A18,A12);
then reconsider Gn1F = Gn1.flow(source,sink) as Element of NAT;
Sum W1 + 1 <= Gn1F by A19;
then
A20: Sum W1 < Gn1.flow(source,sink) by NAT_1:13;
not sink in V by A1,TARSKI:def 1;
hence contradiction by A2,A20,Th12,Th16;
end;
hence thesis;
end;
theorem Th18:
for G being _finite natural-weighted WGraph, EL being
FF:ELabeling of G, source,sink being set st EL has_valid_flow_from source,sink
& not ex P being Path of G st P is_Walk_from source,sink & P is_augmenting_wrt
EL holds EL has_maximum_flow_from source,sink
proof
let G be _finite natural-weighted WGraph, EL be FF:ELabeling of G, source,
sink be set;
assume that
A1: EL has_valid_flow_from source,sink and
A2: not ex P being Path of G st P is_Walk_from source,sink & P
is_augmenting_wrt EL;
reconsider src = source as Vertex of G by A1;
set CS = AP:CompSeq(EL,src), Gn = AP:FindAugPath(EL,src);
set Gn1 = CS.(CS.Lifespan()+1);
reconsider V = dom Gn as Subset of the_Vertices_of G;
set E1 = G.edgesDBetween(V, the_Vertices_of G \ V);
set A1 = EL|E1, B1 = (the_Weight_of G)|E1;
set e = the Element of AP:NextBestEdges(Gn);
AP:CompSeq(EL,src) is halting by Th6;
then
A3: Gn1 = Gn by GLIB_000:def 56;
A4: Gn1 = AP:Step(Gn) by Def12;
A5: now
assume
A6: AP:NextBestEdges(Gn) <> {};
now
per cases by A6,Def9;
suppose
A7: e is_forward_edge_wrt Gn;
then (the_Source_of G).e in V;
then
A8: Gn = Gn+*((the_Target_of G).e .--> e) by A4,A3,A6,Def10;
not (the_Target_of G).e in V by A7;
hence contradiction by A8,Lm2;
end;
suppose
e is_backward_edge_wrt Gn;
then
A9: not (the_Source_of G).e in V;
then Gn = Gn+*((the_Source_of G).e .--> e) by A4,A3,A6,Def10;
hence contradiction by A9,Lm2;
end;
end;
hence contradiction;
end;
A10: now
let x be set;
assume
A11: x in E1;
then
A12: A1.x = EL.x by FUNCT_1:49;
A13: x DSJoins V, the_Vertices_of G \ V, G by A11,GLIB_000:def 31;
then (the_Target_of G).x in the_Vertices_of G \ V;
then
A14: not (the_Target_of G).x in V by XBOOLE_0:def 5;
A15: B1.x = (the_Weight_of G).x by A11,FUNCT_1:49;
A16: (the_Source_of G).x in V by A13;
A17: now
assume A1.x < B1.x;
then x is_forward_edge_wrt Gn by A11,A12,A15,A16,A14;
hence contradiction by A5,Def9;
end;
A1.x <= B1.x by A1,A11,A12,A15;
hence A1.x = B1.x by A17,XXREAL_0:1;
end;
set E2 = G.edgesDBetween(the_Vertices_of G \ V, V);
set A2 = EL|E2, B2 = EmptyBag E2;
now
let x be set;
assume
A18: x in E2;
then
A19: x DSJoins the_Vertices_of G \ V, V, G by GLIB_000:def 31;
then
A20: (the_Target_of G).x in V;
(the_Source_of G).x in the_Vertices_of G \ V by A19;
then
A21: not (the_Source_of G).x in V by XBOOLE_0:def 5;
A22: A2.x = EL.x by A18,FUNCT_1:49;
A23: now
assume 0 < A2.x;
then x is_backward_edge_wrt Gn by A18,A22,A20,A21;
hence contradiction by A5,Def9;
end;
B2 = E2 --> 0 by PBOOLE:def 3;
then B2.x = 0 by A18,FUNCOP_1:7;
hence A2.x = B2.x by A23;
end;
then Sum (EL | E2) = Sum B2 by GLIB_004:6;
then
A24: Sum (EL | E2) = 0 by UPROOTS:11;
A25: not sink in dom Gn by A2,Th9;
then EL.flow(source,sink) = Sum(EL|E1)-Sum(EL|E2) by A1,Th10,Th11;
then EL.flow(source,sink) = Sum ((the_Weight_of G)|E1) by A10,A24,GLIB_004:6;
then
for X be FF:ELabeling of G st X has_valid_flow_from source,sink holds X
.flow(source,sink) <= EL.flow(source,sink) by A25,Th10,Th12;
hence thesis by A1;
end;
::$N Ford/Fulkerson maximum flow algorithm
::$L https://en.wikipedia.org/wiki/FordâFulkerson_algorithm Ford/Fulkerson algorithm
theorem
for G being _finite natural-weighted WGraph, source, sink being Vertex
of G st sink <> source holds FF:MaxFlow(G,source,sink) has_maximum_flow_from
source,sink
proof
let G be _finite natural-weighted WGraph, source, sink be Vertex of G;
set CS = FF:CompSeq(G,source,sink);
set n = CS.Lifespan(), Gn = CS.n, Gn1 = CS.(n+1);
A1: Gn1 = FF:Step(Gn,source,sink) by Def20;
assume
A2: sink <> source;
then CS is halting by Th17;
then
A3: Gn = CS.(n+1) by GLIB_000:def 56;
now
given P being Path of G such that
A4: P is_Walk_from source,sink and
A5: P is_augmenting_wrt Gn;
set P = AP:GetAugPath(Gn,source,sink);
A6: sink in dom AP:FindAugPath(Gn,source) by A4,A5,Th9;
then
A7: P is_Walk_from source,sink by Def14;
then
A8: P.first() = source by GLIB_001:def 23;
A9: P.last() = sink by A7,GLIB_001:def 23;
A10: P is_augmenting_wrt Gn by A6,Def14;
Gn1 = FF:PushFlow(Gn, AP:GetAugPath(Gn,source,sink)) by A1,A6,Def18;
then
Gn.flow(source,sink) + P.tolerance(Gn) = Gn1.flow(source,sink) by A2,A7,A10
,Th15;
hence contradiction by A2,A3,A8,A9,A10,Th13,GLIB_001:127;
end;
hence thesis by A2,Th16,Th18;
end;