environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI;
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;
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;
constructors HIDDEN, DOMAIN_1, FUNCT_4, NAT_D, GRAPH_2, GRAPH_5, UPROOTS, GLIB_004, XXREAL_2, RELSET_1;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
equalities GLIB_000, GLIB_003, FUNCOP_1;
expansions TARSKI, GLIB_000, GLIB_003;
Lm1:
for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
Lm2:
for F being Function
for x, y being set holds x in dom (F +* (x .--> y))
Lm3:
for F being Function
for x, y being set holds (F +* (x .--> y)) . x = y
Lm4:
for F being Function
for x, y, z being set st x <> z holds
(F +* (x .--> y)) . z = F . z
definition
let G be
finite real-weighted WGraph;
let EL be
FF:ELabeling of
G;
let source,
sink be
Vertex of
G;
existence
( ( sink in dom (AP:FindAugPath (EL,source)) implies ex b1 being vertex-distinct Path of G st
( b1 is_Walk_from source,sink & b1 is_augmenting_wrt EL & ( for n being even Nat st n in dom b1 holds
b1 . n = (AP:FindAugPath (EL,source)) . (b1 . (n + 1)) ) ) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies ex b1 being vertex-distinct Path of G st b1 = G .walkOf source ) )
uniqueness
for b1, b2 being vertex-distinct Path of G holds
( ( sink in dom (AP:FindAugPath (EL,source)) & b1 is_Walk_from source,sink & b1 is_augmenting_wrt EL & ( for n being even Nat st n in dom b1 holds
b1 . n = (AP:FindAugPath (EL,source)) . (b1 . (n + 1)) ) & b2 is_Walk_from source,sink & b2 is_augmenting_wrt EL & ( for n being even Nat st n in dom b2 holds
b2 . n = (AP:FindAugPath (EL,source)) . (b2 . (n + 1)) ) implies b1 = b2 ) & ( not sink in dom (AP:FindAugPath (EL,source)) & b1 = G .walkOf source & b2 = G .walkOf source implies b1 = b2 ) )
consistency
for b1 being vertex-distinct Path of G holds verum
;
end;
definition
let G be
natural-weighted WGraph;
let EL be
FF:ELabeling of
G;
let W be
Walk of
G;
assume A1:
W is_augmenting_wrt EL
;
defpred S1[
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)) ) );
existence
ex b1 being FinSequence of NAT st
( dom b1 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b1 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b1 . 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 b1 . n = EL . (W . (2 * n)) ) ) ) )
uniqueness
for b1, b2 being FinSequence of NAT st dom b1 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b1 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b1 . 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 b1 . n = EL . (W . (2 * n)) ) ) ) & dom b2 = dom (W .edgeSeq()) & ( for n being Nat st n in dom b2 holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b2 . 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 b2 . n = EL . (W . (2 * n)) ) ) ) holds
b1 = b2
end;
definition
let G be
natural-weighted WGraph;
let EL be
FF:ELabeling of
G;
let P be
Path of
G;
assume A1:
P is_augmenting_wrt EL
;
existence
ex b1 being FF:ELabeling of G st
( ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b1 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) )
uniqueness
for b1, b2 being FF:ELabeling of G st ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b1 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b1 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) & ( for e being set st e in the_Edges_of G & not e in P .edges() holds
b2 . e = EL . e ) & ( for n being odd Nat st n < len P holds
( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies b2 . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies b2 . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) ) ) holds
b1 = b2
end;
::
deftheorem Def18 defines
FF:Step GLIB_005:def 18 :
for G being finite natural-weighted WGraph
for EL being FF:ELabeling of G
for sink, source being Vertex of G holds
( ( sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = FF:PushFlow (EL,(AP:GetAugPath (EL,source,sink))) ) & ( not sink in dom (AP:FindAugPath (EL,source)) implies FF:Step (EL,source,sink) = EL ) );
:: as the graphs are finite