let G be real-weighted WGraph; for EL being FF:ELabeling of G
for source being Vertex of G
for n being Nat
for 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) )
let EL be FF:ELabeling of G; for source being Vertex of G
for n being Nat
for 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) )
let source be Vertex of G; for n being Nat
for 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) )
set CS = AP:CompSeq (EL,source);
set G0 = (AP:CompSeq (EL,source)) . 0;
defpred S1[ Nat] means for v being set st v in dom ((AP:CompSeq (EL,source)) . $1) 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)) . $1) );
A1:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )set Gn =
(AP:CompSeq (EL,source)) . n;
set Gn1 =
(AP:CompSeq (EL,source)) . (n + 1);
set Next =
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
set e = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
assume A2:
S1[
n]
;
S1[n + 1]A3:
(AP:CompSeq (EL,source)) . (n + 1) = AP:Step ((AP:CompSeq (EL,source)) . n)
by Def12;
now S1[n + 1]per cases
( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} or AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} )
;
suppose A4:
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {}
;
S1[n + 1]set se =
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
set te =
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
now for v being set st v in dom ((AP:CompSeq (EL,source)) . (n + 1)) 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 + 1)) )per cases
( the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n or the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_backward_edge_wrt (AP:CompSeq (EL,source)) . n )
by A4, Def9;
suppose A5:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n
;
for v being set st v in dom ((AP:CompSeq (EL,source)) . (n + 1)) 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 + 1)) )then A6:
EL . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) < (the_Weight_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
;
let v be
set ;
( v in dom ((AP:CompSeq (EL,source)) . (n + 1)) implies 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 + 1)) ) )assume A7:
v in dom ((AP:CompSeq (EL,source)) . (n + 1))
;
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 + 1)) )A8:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in the_Edges_of G
by A5;
then A9:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) DJoins (the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
G
;
A10:
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n)
by A5;
then
(AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))
by A3, A4, Def10;
then A11:
dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
by Lm1;
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
by TARSKI:def 1;
then A12:
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . (n + 1))
by A11, XBOOLE_0:def 3;
A13:
dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + 1))
by A11, XBOOLE_1:7;
then A14:
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . (n + 1))
by A10;
now 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 + 1)) )per cases
( v in dom ((AP:CompSeq (EL,source)) . n) or v in {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} )
by A11, A7, XBOOLE_0:def 3;
suppose
v in {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
;
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 + 1)) )then A18:
v = (the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by TARSKI:def 1;
now ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )per cases
( (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = source or (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> source )
;
suppose A19:
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = source
;
ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )set P =
G .walkOf (
((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)));
take P =
G .walkOf (
((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)));
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )A20:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins (the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
G
by A8;
now for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) )let n be
odd Nat;
( n < len P implies ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) ) )assume
n < len P
;
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) )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 = <*((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))*>
by A20, GLIB_001:def 5;
then A24:
P . n = (the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A22, FINSEQ_1:45;
A25:
P . (n + 2) = (the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A22, A23, FINSEQ_1:45;
A26:
P . (n + 1) = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A22, A23, FINSEQ_1:45;
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;
( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) )assume
not
P . (n + 1) DJoins P . n,
P . (n + 2),
G
;
0 < EL . (P . (n + 1))hence
0 < EL . (P . (n + 1))
by A8, A24, A26, A25;
verum end; hence
P is_augmenting_wrt EL
;
( P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )thus
P is_Walk_from source,
v
by A18, A19, A20, GLIB_001:15;
P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))hence
P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))
;
verum end; suppose A27:
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> source
;
ex P2 being Path of G st
( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )A28:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins (the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
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,
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
and A31:
P .vertices() c= dom ((AP:CompSeq (EL,source)) . n)
by A2, A10;
set P2 =
P .addEdge the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
A32:
not
v in P .vertices()
by A5, A18, A31;
A33:
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = 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 =
P .addEdge the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) as
Path of
G by A28, A33, A32, GLIB_001:151;
take P2 =
P2;
( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )thus
P2 is_augmenting_wrt EL
by A6, A9, A18, A29, A33, A32, Th3;
( P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )thus
P2 is_Walk_from source,
v
by A30, A28, GLIB_001:66;
P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))hence
P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))
;
verum end; 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 ((AP:CompSeq (EL,source)) . (n + 1)) )
;
verum end; 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 ((AP:CompSeq (EL,source)) . (n + 1)) )
;
verum end; suppose A35:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_backward_edge_wrt (AP:CompSeq (EL,source)) . n
;
for v being set st v in dom ((AP:CompSeq (EL,source)) . (n + 1)) 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 + 1)) )then A36:
0 < EL . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
;
let v be
set ;
( v in dom ((AP:CompSeq (EL,source)) . (n + 1)) implies 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 + 1)) ) )assume A37:
v in dom ((AP:CompSeq (EL,source)) . (n + 1))
;
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 + 1)) )A38:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in the_Edges_of G
by A35;
then A39:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) DJoins (the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
G
;
A40:
not
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n)
by A35;
then
(AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))
by A3, A4, Def10;
then A41:
dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
by Lm1;
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
by TARSKI:def 1;
then A42:
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . (n + 1))
by A41, XBOOLE_0:def 3;
A43:
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n)
by A35;
A44:
dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + 1))
by A41, XBOOLE_1:7;
then A45:
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . (n + 1))
by A43;
now 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 + 1)) )per cases
( v in dom ((AP:CompSeq (EL,source)) . n) or v in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} )
by A41, A37, XBOOLE_0:def 3;
suppose
v in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
;
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 + 1)) )then A49:
v = (the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by TARSKI:def 1;
now ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )per cases
( (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = source or (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> source )
;
suppose A50:
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = source
;
ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )set P =
G .walkOf (
((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)));
take P =
G .walkOf (
((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)));
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )A51:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins (the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
G
by A38;
now for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) )let n be
odd Nat;
( n < len P implies ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) ) )assume
n < len P
;
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) )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 = <*((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))*>
by A51, GLIB_001:def 5;
then A55:
P . (n + 1) = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A53, FINSEQ_1:45;
P . n = (the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A53, A54, FINSEQ_1:45;
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;
( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) )assume
not
P . (n + 1) DJoins P . n,
P . (n + 2),
G
;
0 < EL . (P . (n + 1))thus
0 < EL . (P . (n + 1))
by A35, A55;
verum end; hence
P is_augmenting_wrt EL
;
( P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )thus
P is_Walk_from source,
v
by A49, A50, A51, GLIB_001:15;
P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))hence
P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))
;
verum end; suppose A56:
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> source
;
ex P2 being Path of G st
( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )A57:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins (the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
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,
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
and A60:
P .vertices() c= dom ((AP:CompSeq (EL,source)) . n)
by A2, A43;
set P2 =
P .addEdge the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
A61:
not
v in P .vertices()
by A35, A49, A60;
A62:
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = 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 =
P .addEdge the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) as
Path of
G by A57, A62, A61, GLIB_001:151;
take P2 =
P2;
( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )thus
P2 is_augmenting_wrt EL
by A36, A39, A49, A58, A62, A61, Th3;
( P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) )thus
P2 is_Walk_from source,
v
by A59, A57, GLIB_001:66;
P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))hence
P2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1))
;
verum end; 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 ((AP:CompSeq (EL,source)) . (n + 1)) )
;
verum end; 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 ((AP:CompSeq (EL,source)) . (n + 1)) )
;
verum end; end; end; hence
S1[
n + 1]
;
verum end; end; end; hence
S1[
n + 1]
;
verum end;
now for v being set st v in dom ((AP:CompSeq (EL,source)) . 0) holds
ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) )let v be
set ;
( v in dom ((AP:CompSeq (EL,source)) . 0) implies ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) ) )assume A64:
v in dom ((AP:CompSeq (EL,source)) . 0)
;
ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) )then reconsider v9 =
v as
Vertex of
G ;
set P =
G .walkOf v9;
take P =
G .walkOf v9;
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) )thus
P is_augmenting_wrt EL
by Th1;
( P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) )
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() c= dom ((AP:CompSeq (EL,source)) . 0)
P .vertices() = {v9}
by GLIB_001:90;
hence
P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0)
by A64, ZFMISC_1:31;
verum end;
then A65:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A65, A1);
hence
for n being Nat
for 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) )
; verum