set FAP = AP:FindAugPath (EL,source);
set CS = AP:CompSeq (EL,source);
let IT1, IT2 be vertex-distinct Path of G; ( ( sink in dom (AP:FindAugPath (EL,source)) & 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 ) & ( not sink in dom (AP:FindAugPath (EL,source)) & IT1 = G .walkOf source & IT2 = G .walkOf source implies IT1 = IT2 ) )
defpred S1[ Nat] means for v being set
for P1, P2 being vertex-distinct Path of G st v in dom ((AP:CompSeq (EL,source)) . $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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) holds
P1 = P2;
set G0 = (AP:CompSeq (EL,source)) . 0;
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A87:
S1[
n]
;
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);
A88:
(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) <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) ) or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) ) )
;
suppose A89:
(
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & not
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) )
;
S1[n + 1]
source in {source}
by TARSKI:def 1;
then A90:
source in dom ((AP:CompSeq (EL,source)) . 0)
by Th4;
dom ((AP:CompSeq (EL,source)) . 0) c= dom ((AP:CompSeq (EL,source)) . n)
by Th5;
then A91:
source in dom ((AP:CompSeq (EL,source)) . n)
by A90;
( 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 A89, Def9;
then A92:
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n)
by A89;
A93:
(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 A88, A89, Def10;
then A94:
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;
now for v being set
for P1, P2 being vertex-distinct Path of G st v in dom ((AP:CompSeq (EL,source)) . (n + 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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) holds
P1 = P2let v be
set ;
for P1, P2 being vertex-distinct Path of G st v in dom ((AP:CompSeq (EL,source)) . (n + 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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) holds
P1 = P2let P1,
P2 be
vertex-distinct Path of
G;
( v in dom ((AP:CompSeq (EL,source)) . (n + 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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) implies P1 = P2 )assume that A95:
v in dom ((AP:CompSeq (EL,source)) . (n + 1))
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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1))
and A101:
for
n being
even Nat st
n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1))
;
P1 = P2A102:
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 P1 = P2per 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 A94, A95, XBOOLE_0:def 3;
suppose A106:
v in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
;
P1 = P2then A107:
v = (the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by TARSKI:def 1;
then
((AP:CompSeq (EL,source)) . (n + 1)) . v = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A93, Lm3;
then A108:
(AP:FindAugPath (EL,source)) . v = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
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
V5()
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
V5()
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 = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
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:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins P1 . lenP12,
v,
G
by A102, A114, GLIB_001:9;
A118:
P1 . lenP12 = (the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A107, A117;
set P1A =
P1 .cut (
((2 * 0) + 1),
lenP12);
A119:
lenP12 < len P1
by A113, A116, XREAL_1:15;
A120:
now for n being even Nat st n in dom (P1 .cut (((2 * 0) + 1),lenP12)) holds
(P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1))let n be
even Nat;
( n in dom (P1 .cut (((2 * 0) + 1),lenP12)) implies (P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1)) )assume A121:
n in dom (P1 .cut (((2 * 0) + 1),lenP12))
;
(P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1))then A122:
1
<= n
by FINSEQ_3:25;
A123:
n <= len (P1 .cut (((2 * 0) + 1),lenP12))
by A121, FINSEQ_3:25;
then
n < len (P1 .cut (((2 * 0) + 1),lenP12))
by XXREAL_0:1;
then A124:
n + 1
<= len (P1 .cut (((2 * 0) + 1),lenP12))
by NAT_1:13;
1
<= n + 1
by A121, NAT_1:13;
then
n + 1
in dom (P1 .cut (((2 * 0) + 1),lenP12))
by A124, FINSEQ_3:25;
then A125:
(P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1) = P1 . (n + 1)
by A119, GLIB_001:46;
len (P1 .cut (((2 * 0) + 1),lenP12)) = 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;
(P1 .cut (((2 * 0) + 1),lenP12)) . n = P1 . n
by A119, A121, GLIB_001:46;
hence
(P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1))
by A100, A125, A126;
verum 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
v)
by A102, A115, A118, A119, A127, GLIB_001:40;
A129:
P1 .cut (
((2 * 0) + 1),
lenP12)
is_augmenting_wrt EL
by A97, Th2;
A130:
1
<= lenP12
by ABIAN:12;
then A131:
(P1 .cut (((2 * 0) + 1),lenP12)) .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 = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
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:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) 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 for n being even Nat st n in dom (P2 .cut (((2 * 0) + 1),lenP22)) holds
(P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1))let n be
even Nat;
( n in dom (P2 .cut (((2 * 0) + 1),lenP22)) implies (P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1)) )assume A140:
n in dom (P2 .cut (((2 * 0) + 1),lenP22))
;
(P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1))then A141:
1
<= n
by FINSEQ_3:25;
A142:
n <= len (P2 .cut (((2 * 0) + 1),lenP22))
by A140, FINSEQ_3:25;
then
n < len (P2 .cut (((2 * 0) + 1),lenP22))
by XXREAL_0:1;
then A143:
n + 1
<= len (P2 .cut (((2 * 0) + 1),lenP22))
by NAT_1:13;
1
<= n + 1
by A140, NAT_1:13;
then
n + 1
in dom (P2 .cut (((2 * 0) + 1),lenP22))
by A143, FINSEQ_3:25;
then A144:
(P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1) = P2 . (n + 1)
by A138, GLIB_001:46;
len (P2 .cut (((2 * 0) + 1),lenP22)) = 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;
(P2 .cut (((2 * 0) + 1),lenP22)) . n = P2 . n
by A138, A140, GLIB_001:46;
hence
(P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1))
by A101, A144, A145;
verum end; A146:
1
<= lenP22
by ABIAN:12;
then A147:
(P2 .cut (((2 * 0) + 1),lenP22)) .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) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A107, A136;
then A149:
P2 .cut (
((2 * 0) + 1),
lenP22)
is_Walk_from source,
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
v)
by A104, A134, A148, A138, A137, GLIB_001:40;
A151:
P2 .cut (
((2 * 0) + 1),
lenP22)
is_augmenting_wrt EL
by A99, Th2;
P1 .cut (
((2 * 0) + 1),
lenP12)
is_Walk_from source,
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A105, A118, A130, A119, GLIB_001:37;
hence
P1 = P2
by A87, A92, A149, A129, A151, A120, A139, A128, A150, A131, A147;
verum end; hence
P1 = P2
;
verum end; hence
S1[
n + 1]
;
verum end; suppose A152:
(
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} &
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) )
;
S1[n + 1]
source in {source}
by TARSKI:def 1;
then A153:
source in dom ((AP:CompSeq (EL,source)) . 0)
by Th4;
dom ((AP:CompSeq (EL,source)) . 0) c= dom ((AP:CompSeq (EL,source)) . n)
by Th5;
then A154:
source in dom ((AP:CompSeq (EL,source)) . n)
by A153;
( 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 A152, Def9;
then A155:
not
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n)
by A152;
A156:
(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 A88, A152, Def10;
then A157:
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;
now for v being set
for P1, P2 being vertex-distinct Path of G st v in dom ((AP:CompSeq (EL,source)) . (n + 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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) holds
P1 = P2let v be
set ;
for P1, P2 being vertex-distinct Path of G st v in dom ((AP:CompSeq (EL,source)) . (n + 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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) holds
P1 = P2let P1,
P2 be
vertex-distinct Path of
G;
( v in dom ((AP:CompSeq (EL,source)) . (n + 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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) implies P1 = P2 )assume that A158:
v in dom ((AP:CompSeq (EL,source)) . (n + 1))
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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1))
and A164:
for
n being
even Nat st
n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1))
;
P1 = P2A165:
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 P1 = P2per 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 A157, A158, XBOOLE_0:def 3;
suppose A169:
v in {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
;
P1 = P2then A170:
v = (the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by TARSKI:def 1;
then
((AP:CompSeq (EL,source)) . (n + 1)) . v = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A156, Lm3;
then A171:
(AP:FindAugPath (EL,source)) . v = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
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
V5()
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
V5()
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 = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
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:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins P1 . lenP12,
v,
G
by A165, A177, GLIB_001:9;
A181:
P1 . lenP12 = (the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A170, A180;
set P1A =
P1 .cut (
((2 * 0) + 1),
lenP12);
A182:
lenP12 < len P1
by A176, A179, XREAL_1:15;
A183:
now for n being even Nat st n in dom (P1 .cut (((2 * 0) + 1),lenP12)) holds
(P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1))let n be
even Nat;
( n in dom (P1 .cut (((2 * 0) + 1),lenP12)) implies (P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1)) )assume A184:
n in dom (P1 .cut (((2 * 0) + 1),lenP12))
;
(P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1))then A185:
1
<= n
by FINSEQ_3:25;
A186:
n <= len (P1 .cut (((2 * 0) + 1),lenP12))
by A184, FINSEQ_3:25;
then
n < len (P1 .cut (((2 * 0) + 1),lenP12))
by XXREAL_0:1;
then A187:
n + 1
<= len (P1 .cut (((2 * 0) + 1),lenP12))
by NAT_1:13;
1
<= n + 1
by A184, NAT_1:13;
then
n + 1
in dom (P1 .cut (((2 * 0) + 1),lenP12))
by A187, FINSEQ_3:25;
then A188:
(P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1) = P1 . (n + 1)
by A182, GLIB_001:46;
len (P1 .cut (((2 * 0) + 1),lenP12)) = 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;
(P1 .cut (((2 * 0) + 1),lenP12)) . n = P1 . n
by A182, A184, GLIB_001:46;
hence
(P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1))
by A163, A188, A189;
verum 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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
v)
by A165, A178, A181, A182, A190, GLIB_001:40;
A192:
P1 .cut (
((2 * 0) + 1),
lenP12)
is_augmenting_wrt EL
by A160, Th2;
A193:
1
<= lenP12
by ABIAN:12;
then A194:
(P1 .cut (((2 * 0) + 1),lenP12)) .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 = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
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:
the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) 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 for n being even Nat st n in dom (P2 .cut (((2 * 0) + 1),lenP22)) holds
(P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1))let n be
even Nat;
( n in dom (P2 .cut (((2 * 0) + 1),lenP22)) implies (P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1)) )assume A203:
n in dom (P2 .cut (((2 * 0) + 1),lenP22))
;
(P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1))then A204:
1
<= n
by FINSEQ_3:25;
A205:
n <= len (P2 .cut (((2 * 0) + 1),lenP22))
by A203, FINSEQ_3:25;
then
n < len (P2 .cut (((2 * 0) + 1),lenP22))
by XXREAL_0:1;
then A206:
n + 1
<= len (P2 .cut (((2 * 0) + 1),lenP22))
by NAT_1:13;
1
<= n + 1
by A203, NAT_1:13;
then
n + 1
in dom (P2 .cut (((2 * 0) + 1),lenP22))
by A206, FINSEQ_3:25;
then A207:
(P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1) = P2 . (n + 1)
by A201, GLIB_001:46;
len (P2 .cut (((2 * 0) + 1),lenP22)) = 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;
(P2 .cut (((2 * 0) + 1),lenP22)) . n = P2 . n
by A201, A203, GLIB_001:46;
hence
(P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1))
by A164, A207, A208;
verum end; A209:
1
<= lenP22
by ABIAN:12;
then A210:
(P2 .cut (((2 * 0) + 1),lenP22)) .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) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A170, A199;
then A212:
P2 .cut (
((2 * 0) + 1),
lenP22)
is_Walk_from source,
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
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) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),
v)
by A167, A197, A211, A201, A200, GLIB_001:40;
A214:
P2 .cut (
((2 * 0) + 1),
lenP22)
is_augmenting_wrt EL
by A162, Th2;
P1 .cut (
((2 * 0) + 1),
lenP12)
is_Walk_from source,
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)
by A168, A181, A193, A182, GLIB_001:37;
hence
P1 = P2
by A87, A152, A212, A192, A214, A183, A202, A191, A213, A194, A210;
verum end; hence
P1 = P2
;
verum end; hence
S1[
n + 1]
;
verum end; hence
S1[
n + 1]
;
verum end;
then A215:
for n being Nat st S1[n] holds
S1[n + 1]
;
now for v being set
for P1, P2 being vertex-distinct Path of G st v in dom ((AP:CompSeq (EL,source)) . 0) & 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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) holds
P1 = P2let v be
set ;
for P1, P2 being vertex-distinct Path of G st v in dom ((AP:CompSeq (EL,source)) . 0) & 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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) holds
P1 = P2let P1,
P2 be
vertex-distinct Path of
G;
( v in dom ((AP:CompSeq (EL,source)) . 0) & 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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) implies P1 = P2 )assume that A216:
v in dom ((AP:CompSeq (EL,source)) . 0)
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 = (AP:FindAugPath (EL,source)) . (P1 . (n + 1))
and
for
n being
even Nat st
n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1))
;
P1 = P2
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;
verum end;
then A225:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A225, A215);
hence
( sink in dom (AP:FindAugPath (EL,source)) & 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 )
; ( not sink in dom (AP:FindAugPath (EL,source)) & IT1 = G .walkOf source & IT2 = G .walkOf source implies IT1 = IT2 )
thus
( not sink in dom (AP:FindAugPath (EL,source)) & IT1 = G .walkOf source & IT2 = G .walkOf source implies IT1 = IT2 )
; verum