let G be finite real-weighted WGraph; :: thesis: for EL being FF:ELabeling of
for source being Vertex of G
for 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 ) )
let EL be FF:ELabeling of ; :: thesis: for source being Vertex of G
for 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 ) )
let source be Vertex of G; :: thesis: for 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 ) )
let v be set ; :: thesis: ( 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 ) )
set CS = AP:CompSeq EL,source;
set V = dom (AP:FindAugPath EL,source);
given P being Path of G such that A2:
( P is_Walk_from source,v & P is_augmenting_wrt EL )
; :: thesis: v in dom (AP:FindAugPath EL,source)
now assume A3:
not
v in dom (AP:FindAugPath EL,source)
;
:: thesis: contradictiondefpred S1[
Nat]
means ( not $1 is
even & $1
<= len P & not
P . $1
in dom (AP:FindAugPath EL,source) );
P . (len P) = v
by A2, GLIB_001:18;
then A4:
ex
n being
Nat st
S1[
n]
by A3;
consider n being
Nat such that A5:
(
S1[
n] & ( for
k being
Nat st
S1[
k] holds
n <= k ) )
from NAT_1:sch 5(A4);
P . ((2 * 0 ) + 1) = source
by A2, GLIB_001:18;
then
P . ((2 * 0 ) + 1) in {source}
by TARSKI:def 1;
then A6:
P . ((2 * 0 ) + 1) in dom ((AP:CompSeq EL,source) . 0 )
by Th3;
dom ((AP:CompSeq EL,source) . 0 ) c= dom (AP:FindAugPath EL,source)
by Th4;
then A7:
n <> 1
by A5, A6;
reconsider n' =
n as
odd Element of
NAT by A5, ORDINAL1:def 13;
1
<= n
by A5, HEYTING3:1;
then
1
< n
by A7, 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:18;
A8:
n2 < n - 0
by XREAL_1:17;
then A9:
n2 < len P
by A5, XXREAL_0:2;
then A10:
P . n2 in dom (AP:FindAugPath EL,source)
by A5, A8;
set Gn =
(AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() );
set Gn1 =
(AP:CompSeq EL,source) . (((AP:CompSeq EL,source) .Lifespan() ) + 1);
set Next =
AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ));
set en =
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )));
A11:
(AP:CompSeq EL,source) . (((AP:CompSeq EL,source) .Lifespan() ) + 1) = AP:Step ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))
by Def15;
AP:CompSeq EL,
source is
halting
by Th6;
then A12:
(AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) = (AP:CompSeq EL,source) . (((AP:CompSeq EL,source) .Lifespan() ) + 1)
by GLIB_000:def 57;
set e =
P . (n2 + 1);
A13:
P . (n2 + 2) = P . n
;
A16:
P . (n2 + 1) Joins P . n2,
P . n,
G
by A9, A13, GLIB_001:def 3;
A17:
now per cases
( P . (n2 + 1) DJoins P . n2,P . n,G or not P . (n2 + 1) DJoins P . n2,P . n,G )
;
suppose A18:
P . (n2 + 1) DJoins P . n2,
P . n,
G
;
:: thesis: AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) <> {} then A19:
EL . (P . (n2 + 1)) < (the_Weight_of G) . (P . (n2 + 1))
by A2, A9, A13, Def12;
(
P . (n2 + 1) in the_Edges_of G &
(the_Source_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) & not
(the_Target_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) )
by A5, A10, A18, GLIB_000:def 16;
then
P . (n2 + 1) is_forward_edge_wrt (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )
by A19, Def10;
hence
AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) <> {}
by Def13;
:: thesis: verum end; suppose A20:
not
P . (n2 + 1) DJoins P . n2,
P . n,
G
;
:: thesis: AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) <> {} then A21:
0 < EL . (P . (n2 + 1))
by A2, A9, A13, Def12;
P . (n2 + 1) DJoins P . n,
P . n2,
G
by A16, A20, GLIB_000:19;
then
(
P . (n2 + 1) in the_Edges_of G & not
(the_Source_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) &
(the_Target_of G) . (P . (n2 + 1)) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) )
by A5, A10, GLIB_000:def 16;
then
P . (n2 + 1) is_backward_edge_wrt (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )
by A21, Def11;
hence
AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) <> {}
by Def13;
:: thesis: verum end; now per cases
( not (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) or (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) )
;
suppose A23:
not
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))
;
:: thesis: contradictionthen
(AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) = ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) +* (((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))
by A11, A12, A17, Def14;
then A24:
dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) = (dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))) \/ {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))}
by Tw0;
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))}
by TARSKI:def 1;
hence
contradiction
by A23, A24, XBOOLE_0:def 3;
:: thesis: verum end; suppose A25:
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))
;
:: thesis: contradictionthen A26:
(AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) = ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) +* (((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))
by A11, A12, A17, Def14;
(
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))) is_forward_edge_wrt (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) or
choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))) is_backward_edge_wrt (AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ) )
by A17, Def13;
then A27:
not
(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))
by A25, Def10, Def11;
A28:
dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )) = (dom ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() ))) \/ {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))}
by A26, Tw0;
(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))) in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . ((AP:CompSeq EL,source) .Lifespan() )))))}
by TARSKI:def 1;
hence
contradiction
by A27, A28, XBOOLE_0:def 3;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end;
hence
v in dom (AP:FindAugPath EL,source)
; :: thesis: verum