let IT1, IT2 be vertex-distinct Path of G; :: thesis: ( ( 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 ) )
set FAP = AP:FindAugPath EL,source;
set CS = AP:CompSeq EL,source;
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 let v be
set ;
:: thesis: 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;
:: thesis: ( 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 A59:
(
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)) ) )
;
:: thesis: P1 = P2then
v in {source}
by Th3;
then
v = source
by TARSKI:def 1;
then A60:
(
P1 . ((2 * 0 ) + 1) = v &
P1 . (len P1) = v &
P2 . ((2 * 0 ) + 1) = v &
P2 . (len P2) = v )
by A59, GLIB_001:18;
( 1
<= len P1 & 1
<= len P2 )
by HEYTING3:1;
then
(
len P1 = 1 &
len P2 = 1 )
by A60, GLIB_001:def 29;
then
(
P1 = <*v*> &
P2 = <*v*> )
by A60, FINSEQ_1:57;
hence
P1 = P2
;
:: thesis: verum end;
then A61:
S1[ 0 ]
;
now let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )assume A62:
S1[
n]
;
:: thesis: S1[n + 1]set Gn =
(AP:CompSeq EL,source) . n;
set Gn1 =
(AP:CompSeq EL,source) . (n + 1);
A63:
(AP:CompSeq EL,source) . (n + 1) = AP:Step ((AP:CompSeq EL,source) . n)
by Def15;
set Next =
AP:NextBestEdges ((AP:CompSeq EL,source) . n);
set e =
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n));
now per cases
( AP:NextBestEdges ((AP:CompSeq EL,source) . n) = {} or ( AP:NextBestEdges ((AP:CompSeq EL,source) . n) <> {} & not (the_Source_of G) . (choose (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) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n) ) )
;
suppose A65:
(
AP:NextBestEdges ((AP:CompSeq EL,source) . n) <> {} & not
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n) )
;
:: thesis: S1[n + 1]then A66:
(AP:CompSeq EL,source) . (n + 1) = ((AP:CompSeq EL,source) . n) +* (((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))
by A63, Def14;
A68:
dom ((AP:CompSeq EL,source) . (n + 1)) = (dom ((AP:CompSeq EL,source) . n)) \/ {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))}
by Tw0, A66;
(
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) is_forward_edge_wrt (AP:CompSeq EL,source) . n or
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) is_backward_edge_wrt (AP:CompSeq EL,source) . n )
by A65, Def13;
then A69:
(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n)
by A65, Def10, Def11;
source in {source}
by TARSKI:def 1;
then A70:
source in dom ((AP:CompSeq EL,source) . 0 )
by Th3;
dom ((AP:CompSeq EL,source) . 0 ) c= dom ((AP:CompSeq EL,source) . n)
by Th4;
then A71:
source in dom ((AP:CompSeq EL,source) . n)
by A70;
now let v be
set ;
:: thesis: 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;
:: thesis: ( 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 A72:
(
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)) ) )
;
:: thesis: P1 = P2then A73:
(
P1 . 1
= source &
P1 . (len P1) = v &
P2 . 1
= source &
P2 . (len P2) = v )
by GLIB_001:18;
now per cases
( v in dom ((AP:CompSeq EL,source) . n) or v in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} )
by A68, A72, XBOOLE_0:def 3;
suppose A74:
v in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))}
;
:: thesis: P1 = P2then A75:
v = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))
by TARSKI:def 1;
v <> source
by A65, A71, A74, TARSKI:def 1;
then
(
P1 . 1
<> P1 .last() &
P2 . 1
<> P2 .last() )
by A73, GLIB_001:def 7;
then
(
P1 .first() <> P1 .last() &
P2 .first() <> P2 .last() )
by GLIB_001:def 6;
then
( not
P1 is
trivial & not
P2 is
trivial )
by GLIB_001:128;
then A76:
( 3
<= len P1 & 3
<= len P2 )
by GLIB_001:126;
then
( 3
- 2
< (len P1) - 0 & 3
- 2
< (len P2) - 0 )
by XREAL_1:17;
then reconsider lenP11 =
(len P1) - 1,
lenP21 =
(len P2) - 1 as
even Element of
NAT by INT_1:18;
A77:
( 3
- 2
<= lenP11 & 3
- 2
<= lenP21 )
by A76, XREAL_1:17;
A78:
(
lenP11 + 1
= len P1 &
lenP21 + 1
= len P2 )
;
A79:
(
lenP11 < (len P1) - 0 &
lenP21 < (len P2) - 0 )
by XREAL_1:17;
then A80:
(
lenP11 in dom P1 &
lenP21 in dom P2 )
by A77, FINSEQ_3:27;
((AP:CompSeq EL,source) . (n + 1)) . v = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))
by Tw1, A66, A75;
then
(AP:FindAugPath EL,source) . v = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))
by A72, Th7;
then A81:
(
P1 . lenP11 = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) &
P2 . lenP21 = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) )
by A72, A73, A78, A80;
then consider lenP12 being
odd Element of
NAT such that A82:
(
lenP12 = lenP11 - 1 &
lenP11 - 1
in dom P1 &
lenP11 + 1
in dom P1 &
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins P1 . lenP12,
v,
G )
by A73, A80, GLIB_001:10;
A83:
P1 . lenP12 = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))
by A65, A69, A82, A75, GLIB_000:def 15;
consider lenP22 being
odd Element of
NAT such that A84:
(
lenP22 = lenP21 - 1 &
lenP21 - 1
in dom P2 &
lenP21 + 1
in dom P2 &
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins P2 . lenP22,
v,
G )
by A73, A80, A81, GLIB_001:10;
A85:
P2 . lenP22 = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))
by A65, A69, A84, A75, GLIB_000:def 15;
set P1A =
P1 .cut ((2 * 0 ) + 1),
lenP12;
set P2A =
P2 .cut ((2 * 0 ) + 1),
lenP22;
A86:
( 1
<= lenP12 & 1
<= lenP22 )
by HEYTING3:1;
A87:
(
lenP12 < len P1 &
lenP22 < len P2 )
by A79, A82, A84, XREAL_1:17;
then A88:
(
P1 .cut ((2 * 0 ) + 1),
lenP12 is_Walk_from source,
(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) &
P2 .cut ((2 * 0 ) + 1),
lenP22 is_Walk_from source,
(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) )
by A73, A83, A85, A86, GLIB_001:38;
A88a:
(
P1 .cut ((2 * 0 ) + 1),
lenP12 is_augmenting_wrt EL &
P2 .cut ((2 * 0 ) + 1),
lenP22 is_augmenting_wrt EL )
by A72, Th002;
A89:
now let n be
even Nat;
:: thesis: ( 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 A90:
n in dom (P1 .cut ((2 * 0 ) + 1),lenP12)
;
:: thesis: (P1 .cut ((2 * 0 ) + 1),lenP12) . n = (AP:FindAugPath EL,source) . ((P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1))then A91:
( 1
<= n &
n <= len (P1 .cut ((2 * 0 ) + 1),lenP12) )
by FINSEQ_3:27;
A92:
(P1 .cut ((2 * 0 ) + 1),lenP12) . n = P1 . n
by A87, A90, GLIB_001:47;
n < len (P1 .cut ((2 * 0 ) + 1),lenP12)
by A91, XXREAL_0:1;
then
( 1
<= n + 1 &
n + 1
<= len (P1 .cut ((2 * 0 ) + 1),lenP12) )
by NAT_1:13;
then
n + 1
in dom (P1 .cut ((2 * 0 ) + 1),lenP12)
by FINSEQ_3:27;
then A93:
(P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1) = P1 . (n + 1)
by A87, GLIB_001:47;
len (P1 .cut ((2 * 0 ) + 1),lenP12) = lenP12
by A87, GLIB_001:46;
then
n <= len P1
by A87, A91, XXREAL_0:2;
then
n in dom P1
by A91, FINSEQ_3:27;
hence
(P1 .cut ((2 * 0 ) + 1),lenP12) . n = (AP:FindAugPath EL,source) . ((P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1))
by A72, A92, A93;
:: thesis: verum end; A94:
now let n be
even Nat;
:: thesis: ( 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 A95:
n in dom (P2 .cut ((2 * 0 ) + 1),lenP22)
;
:: thesis: (P2 .cut ((2 * 0 ) + 1),lenP22) . n = (AP:FindAugPath EL,source) . ((P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1))then A96:
( 1
<= n &
n <= len (P2 .cut ((2 * 0 ) + 1),lenP22) )
by FINSEQ_3:27;
A97:
(P2 .cut ((2 * 0 ) + 1),lenP22) . n = P2 . n
by A87, A95, GLIB_001:47;
n < len (P2 .cut ((2 * 0 ) + 1),lenP22)
by A96, XXREAL_0:1;
then
( 1
<= n + 1 &
n + 1
<= len (P2 .cut ((2 * 0 ) + 1),lenP22) )
by NAT_1:13;
then
n + 1
in dom (P2 .cut ((2 * 0 ) + 1),lenP22)
by FINSEQ_3:27;
then A98:
(P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1) = P2 . (n + 1)
by A87, GLIB_001:47;
len (P2 .cut ((2 * 0 ) + 1),lenP22) = lenP22
by A87, GLIB_001:46;
then
n <= len P2
by A87, A96, XXREAL_0:2;
then
n in dom P2
by A96, FINSEQ_3:27;
hence
(P2 .cut ((2 * 0 ) + 1),lenP22) . n = (AP:FindAugPath EL,source) . ((P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1))
by A72, A97, A98;
:: thesis: verum end; A99:
(
lenP12 + 1
= lenP11 &
lenP22 + 1
= lenP21 )
by A82, A84;
(
lenP12 + (1 + 1) = len P1 &
lenP22 + (1 + 1) = len P2 )
by A82, A84;
then A100:
(
P1 .cut lenP12,
(len P1) = G .walkOf ((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),
(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),
v &
P2 .cut lenP22,
(len P2) = G .walkOf ((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),
(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),
v )
by A73, A81, A83, A85, A87, A99, GLIB_001:41;
A101:
(P1 .cut ((2 * 0 ) + 1),lenP12) .append (P1 .cut lenP12,(len P1)) =
P1 .cut ((2 * 0 ) + 1),
(len P1)
by A86, A87, GLIB_001:39
.=
P1
by GLIB_001:40
;
(P2 .cut ((2 * 0 ) + 1),lenP22) .append (P2 .cut lenP22,(len P2)) =
P2 .cut ((2 * 0 ) + 1),
(len P2)
by A86, A87, GLIB_001:39
.=
P2
by GLIB_001:40
;
hence
P1 = P2
by A62, A69, A88, A88a, A89, A94, A100, A101;
:: thesis: verum end; hence
P1 = P2
;
:: thesis: verum end; hence
S1[
n + 1]
;
:: thesis: verum end; suppose A102:
(
AP:NextBestEdges ((AP:CompSeq EL,source) . n) <> {} &
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n) )
;
:: thesis: S1[n + 1]then A103:
(AP:CompSeq EL,source) . (n + 1) = ((AP:CompSeq EL,source) . n) +* (((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))
by A63, Def14;
A105:
dom ((AP:CompSeq EL,source) . (n + 1)) = (dom ((AP:CompSeq EL,source) . n)) \/ {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))}
by A103, Tw0;
(
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) is_forward_edge_wrt (AP:CompSeq EL,source) . n or
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) is_backward_edge_wrt (AP:CompSeq EL,source) . n )
by A102, Def13;
then A106:
not
(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n)
by A102, Def10, Def11;
source in {source}
by TARSKI:def 1;
then A107:
source in dom ((AP:CompSeq EL,source) . 0 )
by Th3;
dom ((AP:CompSeq EL,source) . 0 ) c= dom ((AP:CompSeq EL,source) . n)
by Th4;
then A108:
source in dom ((AP:CompSeq EL,source) . n)
by A107;
now let v be
set ;
:: thesis: 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;
:: thesis: ( 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 A109:
(
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)) ) )
;
:: thesis: P1 = P2then A110:
(
P1 . 1
= source &
P1 . (len P1) = v &
P2 . 1
= source &
P2 . (len P2) = v )
by GLIB_001:18;
now per cases
( v in dom ((AP:CompSeq EL,source) . n) or v in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} )
by A105, A109, XBOOLE_0:def 3;
suppose A111:
v in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))}
;
:: thesis: P1 = P2then A112:
v = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))
by TARSKI:def 1;
v <> source
by A106, A108, A111, TARSKI:def 1;
then
(
P1 . 1
<> P1 .last() &
P2 . 1
<> P2 .last() )
by A110, GLIB_001:def 7;
then
(
P1 .first() <> P1 .last() &
P2 .first() <> P2 .last() )
by GLIB_001:def 6;
then
( not
P1 is
trivial & not
P2 is
trivial )
by GLIB_001:128;
then A113:
( 3
<= len P1 & 3
<= len P2 )
by GLIB_001:126;
then
( 3
- 2
< (len P1) - 0 & 3
- 2
< (len P2) - 0 )
by XREAL_1:17;
then reconsider lenP11 =
(len P1) - 1,
lenP21 =
(len P2) - 1 as
even Element of
NAT by INT_1:18;
A114:
( 3
- 2
<= lenP11 & 3
- 2
<= lenP21 )
by A113, XREAL_1:17;
A115:
(
lenP11 + 1
= len P1 &
lenP21 + 1
= len P2 )
;
A116:
(
lenP11 < (len P1) - 0 &
lenP21 < (len P2) - 0 )
by XREAL_1:17;
then A117:
(
lenP11 in dom P1 &
lenP21 in dom P2 )
by A114, FINSEQ_3:27;
((AP:CompSeq EL,source) . (n + 1)) . v = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))
by A103, A112, Tw1;
then
(AP:FindAugPath EL,source) . v = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))
by A109, Th7;
then A118:
(
P1 . lenP11 = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) &
P2 . lenP21 = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) )
by A109, A110, A115, A117;
then consider lenP12 being
odd Element of
NAT such that A119:
(
lenP12 = lenP11 - 1 &
lenP11 - 1
in dom P1 &
lenP11 + 1
in dom P1 &
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins P1 . lenP12,
v,
G )
by A110, A117, GLIB_001:10;
A120:
P1 . lenP12 = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))
by A102, A106, A119, A112, GLIB_000:def 15;
consider lenP22 being
odd Element of
NAT such that A121:
(
lenP22 = lenP21 - 1 &
lenP21 - 1
in dom P2 &
lenP21 + 1
in dom P2 &
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins P2 . lenP22,
v,
G )
by A110, A117, A118, GLIB_001:10;
A122:
P2 . lenP22 = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))
by A102, A106, A121, A112, GLIB_000:def 15;
set P1A =
P1 .cut ((2 * 0 ) + 1),
lenP12;
set P2A =
P2 .cut ((2 * 0 ) + 1),
lenP22;
A123:
( 1
<= lenP12 & 1
<= lenP22 )
by HEYTING3:1;
A124:
(
lenP12 < len P1 &
lenP22 < len P2 )
by A116, A119, A121, XREAL_1:17;
then A125:
(
P1 .cut ((2 * 0 ) + 1),
lenP12 is_Walk_from source,
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) &
P2 .cut ((2 * 0 ) + 1),
lenP22 is_Walk_from source,
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) )
by A110, A120, A122, A123, GLIB_001:38;
A125a:
(
P1 .cut ((2 * 0 ) + 1),
lenP12 is_augmenting_wrt EL &
P2 .cut ((2 * 0 ) + 1),
lenP22 is_augmenting_wrt EL )
by A109, Th002;
A126:
now let n be
even Nat;
:: thesis: ( 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 A127:
n in dom (P1 .cut ((2 * 0 ) + 1),lenP12)
;
:: thesis: (P1 .cut ((2 * 0 ) + 1),lenP12) . n = (AP:FindAugPath EL,source) . ((P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1))then A128:
( 1
<= n &
n <= len (P1 .cut ((2 * 0 ) + 1),lenP12) )
by FINSEQ_3:27;
A129:
(P1 .cut ((2 * 0 ) + 1),lenP12) . n = P1 . n
by A124, A127, GLIB_001:47;
n < len (P1 .cut ((2 * 0 ) + 1),lenP12)
by A128, XXREAL_0:1;
then
( 1
<= n + 1 &
n + 1
<= len (P1 .cut ((2 * 0 ) + 1),lenP12) )
by NAT_1:13;
then
n + 1
in dom (P1 .cut ((2 * 0 ) + 1),lenP12)
by FINSEQ_3:27;
then A130:
(P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1) = P1 . (n + 1)
by A124, GLIB_001:47;
len (P1 .cut ((2 * 0 ) + 1),lenP12) = lenP12
by A124, GLIB_001:46;
then
n <= len P1
by A124, A128, XXREAL_0:2;
then
n in dom P1
by A128, FINSEQ_3:27;
hence
(P1 .cut ((2 * 0 ) + 1),lenP12) . n = (AP:FindAugPath EL,source) . ((P1 .cut ((2 * 0 ) + 1),lenP12) . (n + 1))
by A109, A129, A130;
:: thesis: verum end; A131:
now let n be
even Nat;
:: thesis: ( 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 A132:
n in dom (P2 .cut ((2 * 0 ) + 1),lenP22)
;
:: thesis: (P2 .cut ((2 * 0 ) + 1),lenP22) . n = (AP:FindAugPath EL,source) . ((P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1))then A133:
( 1
<= n &
n <= len (P2 .cut ((2 * 0 ) + 1),lenP22) )
by FINSEQ_3:27;
A134:
(P2 .cut ((2 * 0 ) + 1),lenP22) . n = P2 . n
by A124, A132, GLIB_001:47;
n < len (P2 .cut ((2 * 0 ) + 1),lenP22)
by A133, XXREAL_0:1;
then
( 1
<= n + 1 &
n + 1
<= len (P2 .cut ((2 * 0 ) + 1),lenP22) )
by NAT_1:13;
then
n + 1
in dom (P2 .cut ((2 * 0 ) + 1),lenP22)
by FINSEQ_3:27;
then A135:
(P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1) = P2 . (n + 1)
by A124, GLIB_001:47;
len (P2 .cut ((2 * 0 ) + 1),lenP22) = lenP22
by A124, GLIB_001:46;
then
n <= len P2
by A124, A133, XXREAL_0:2;
then
n in dom P2
by A133, FINSEQ_3:27;
hence
(P2 .cut ((2 * 0 ) + 1),lenP22) . n = (AP:FindAugPath EL,source) . ((P2 .cut ((2 * 0 ) + 1),lenP22) . (n + 1))
by A109, A134, A135;
:: thesis: verum end; A136:
(
lenP12 + 1
= lenP11 &
lenP22 + 1
= lenP21 )
by A119, A121;
(
lenP12 + (1 + 1) = len P1 &
lenP22 + (1 + 1) = len P2 )
by A119, A121;
then A137:
(
P1 .cut lenP12,
(len P1) = G .walkOf ((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),
(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),
v &
P2 .cut lenP22,
(len P2) = G .walkOf ((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),
(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),
v )
by A110, A118, A120, A122, A124, A136, GLIB_001:41;
A138:
(P1 .cut ((2 * 0 ) + 1),lenP12) .append (P1 .cut lenP12,(len P1)) =
P1 .cut ((2 * 0 ) + 1),
(len P1)
by A123, A124, GLIB_001:39
.=
P1
by GLIB_001:40
;
(P2 .cut ((2 * 0 ) + 1),lenP22) .append (P2 .cut lenP22,(len P2)) =
P2 .cut ((2 * 0 ) + 1),
(len P2)
by A123, A124, GLIB_001:39
.=
P2
by GLIB_001:40
;
hence
P1 = P2
by A62, A102, A125, A125a, A126, A131, A137, A138;
:: thesis: verum end; hence
P1 = P2
;
:: thesis: verum end; hence
S1[
n + 1]
;
:: thesis: verum end; hence
S1[
n + 1]
;
:: thesis: verum end;
then A139:
for n being Nat st S1[n] holds
S1[n + 1]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A61, A139);
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 )
; :: thesis: ( 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 )
; :: thesis: verum