REAL is non empty non trivial non finite V100() V101() V102() V106() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V100() V101() V102() V103() V104() V105() V106() Element of K32(REAL)
K32(REAL) is non trivial non finite V79() set
COMPLEX is non empty non trivial non finite V100() V106() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V100() V101() V102() V103() V104() V105() V106() set
K32(NAT) is non trivial non finite V79() set
K32(NAT) is non trivial non finite V79() set
K232() is set
K32(K232()) is set
K32(K32(K232())) is set
K240() is Element of K32(K32(K232()))
Real>=0 is set
RAT is non empty non trivial non finite V100() V101() V102() V103() V106() set
INT is non empty non trivial non finite V100() V101() V102() V103() V104() V106() set
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real integer finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V100() V101() V102() V103() V104() V105() V106() FinSequence-yielding finite-support Function-yielding V199() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
K33(NAT,REAL) is non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
K32(K33(NAT,REAL)) is non trivial non finite set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
K224(1,NAT) is M11( NAT )
{{},1} is non empty finite V36() V100() V101() V102() V103() V104() V105() set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
_GraphSelectors is non empty V100() V101() V102() V103() V104() V105() Element of K32(NAT)
VertexSelector is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
EdgeSelector is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
SourceSelector is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
TargetSelector is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
{VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is finite V100() V101() V102() V103() V104() V105() Element of K32(NAT)
card {} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real integer finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V100() V101() V102() V103() V104() V105() V106() FinSequence-yielding finite-support Function-yielding V199() set
0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real integer finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V77() complex-valued ext-real-valued real-valued natural-valued V100() V101() V102() V103() V104() V105() V106() FinSequence-yielding finite-support Function-yielding V199() Element of NAT
Real>=0 is V100() V101() V102() Element of K32(REAL)
{ b1 where b1 is V28() real ext-real Element of REAL : 0 <= b1 } is set
G is Relation-like Function-like set
dom G is set
source is set
sink is set
source .--> sink is Relation-like {source} -defined Function-like one-to-one finite finite-support set
{source} is non empty trivial finite 1 -element set
{source} --> sink is non empty Relation-like {source} -defined {sink} -valued Function-like constant total V18({source},{sink}) finite finite-support Element of K32(K33({source},{sink}))
{sink} is non empty trivial finite 1 -element set
K33({source},{sink}) is Relation-like finite set
K32(K33({source},{sink})) is finite V36() set
G +* (source .--> sink) is Relation-like Function-like set
dom (G +* (source .--> sink)) is set
(dom G) \/ {source} is non empty set
dom (source .--> sink) is finite Element of K32({source})
K32({source}) is finite V36() V79() set
(dom G) \/ (dom (source .--> sink)) is set
G is Relation-like Function-like set
source is set
sink is set
source .--> sink is Relation-like {source} -defined Function-like one-to-one finite finite-support set
{source} is non empty trivial finite 1 -element set
{source} --> sink is non empty Relation-like {source} -defined {sink} -valued Function-like constant total V18({source},{sink}) finite finite-support Element of K32(K33({source},{sink}))
{sink} is non empty trivial finite 1 -element set
K33({source},{sink}) is Relation-like finite set
K32(K33({source},{sink})) is finite V36() set
G +* (source .--> sink) is Relation-like Function-like set
dom (G +* (source .--> sink)) is set
dom (source .--> sink) is finite Element of K32({source})
K32({source}) is finite V36() V79() set
G is Relation-like Function-like set
source is set
sink is set
source .--> sink is Relation-like {source} -defined Function-like one-to-one finite finite-support set
{source} is non empty trivial finite 1 -element set
{source} --> sink is non empty Relation-like {source} -defined {sink} -valued Function-like constant total V18({source},{sink}) finite finite-support Element of K32(K33({source},{sink}))
{sink} is non empty trivial finite 1 -element set
K33({source},{sink}) is Relation-like finite set
K32(K33({source},{sink})) is finite V36() set
G +* (source .--> sink) is Relation-like Function-like set
(G +* (source .--> sink)) . source is set
dom (source .--> sink) is finite Element of K32({source})
K32({source}) is finite V36() V79() set
(source .--> sink) . source is set
G is Relation-like Function-like set
source is set
CS is set
sink is set
source .--> sink is Relation-like {source} -defined Function-like one-to-one finite finite-support set
{source} is non empty trivial finite 1 -element set
{source} --> sink is non empty Relation-like {source} -defined {sink} -valued Function-like constant total V18({source},{sink}) finite finite-support Element of K32(K33({source},{sink}))
{sink} is non empty trivial finite 1 -element set
K33({source},{sink}) is Relation-like finite set
K32(K33({source},{sink})) is finite V36() set
G +* (source .--> sink) is Relation-like Function-like set
(G +* (source .--> sink)) . CS is set
G . CS is set
dom (source .--> sink) is finite Element of K32({source})
K32({source}) is finite V36() V79() set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] set
the_Weight_of G is Relation-like the_Edges_of G -defined Function-like total set
the_Edges_of G is set
G . EdgeSelector is set
WeightSelector is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
G . WeightSelector is set
source is set
rng (the_Weight_of G) is set
sink is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
{1} is non empty trivial finite V36() 1 -element V100() V101() V102() V103() V104() V105() Element of K32(NAT)
K33({},{1}) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K32(K33({},{1})) is finite V36() set
sink is empty Relation-like non-empty empty-yielding {} -defined {1} -valued Function-like one-to-one constant functional total V18( {} ,{1}) epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real integer finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V100() V101() V102() V103() V104() V105() V106() FinSequence-yielding finite-support Function-yielding V199() Element of K32(K33({},{1}))
createGraph ({1},{},sink,sink) is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite loopless trivial non-multi non-Dmulti simple Dsimple V221() V222() Tree-like set
the_Edges_of (createGraph ({1},{},sink,sink)) is finite set
(createGraph ({1},{},sink,sink)) . EdgeSelector is set
K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT)) is set
the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT)) is Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT))
WeightSelector is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(createGraph ({1},{},sink,sink)) .set (WeightSelector, the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT))) is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite loopless trivial non-multi non-Dmulti simple Dsimple V221() V222() Tree-like [Weighted] set
WeightSelector .--> the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT)) is Relation-like NAT -defined {WeightSelector} -defined Function-like one-to-one finite finite-support Function-yielding V199() set
{WeightSelector} is non empty trivial finite V36() 1 -element V100() V101() V102() V103() V104() V105() set
{WeightSelector} --> the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT)) is non empty Relation-like {WeightSelector} -defined { the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT))} -valued Function-like constant total V18({WeightSelector},{ the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT))}) finite finite-support Function-yielding V199() Element of K32(K33({WeightSelector},{ the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT))}))
{ the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT))} is non empty trivial functional finite V36() 1 -element set
K33({WeightSelector},{ the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT))}) is Relation-like finite set
K32(K33({WeightSelector},{ the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT))})) is finite V36() set
(createGraph ({1},{},sink,sink)) +* (WeightSelector .--> the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT))) is Relation-like Function-like finite finite-support set
the_Weight_of ((createGraph ({1},{},sink,sink)) .set (WeightSelector, the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT)))) is Relation-like the_Edges_of ((createGraph ({1},{},sink,sink)) .set (WeightSelector, the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT)))) -defined Function-like total finite finite-support set
the_Edges_of ((createGraph ({1},{},sink,sink)) .set (WeightSelector, the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT)))) is finite set
((createGraph ({1},{},sink,sink)) .set (WeightSelector, the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT)))) . EdgeSelector is set
((createGraph ({1},{},sink,sink)) .set (WeightSelector, the Relation-like the_Edges_of (createGraph ({1},{},sink,sink)) -defined NAT -valued Function-like total V18( the_Edges_of (createGraph ({1},{},sink,sink)), NAT ) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33((the_Edges_of (createGraph ({1},{},sink,sink))),NAT)))) . WeightSelector is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted nonnegative-weighted () set
the_Weight_of G is Relation-like the_Edges_of G -defined Function-like total complex-valued ext-real-valued real-valued set
the_Edges_of G is set
G . EdgeSelector is set
WeightSelector is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
G . WeightSelector is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] real-weighted set
the_Edges_of G is finite set
G . EdgeSelector is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] real-weighted set
the_Edges_of G is finite set
G . EdgeSelector is set
CS is set
{CS} is non empty trivial finite 1 -element set
G .edgesInto {CS} is finite Element of K32((the_Edges_of G))
K32((the_Edges_of G)) is finite V36() set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
source | (G .edgesInto {CS}) is Relation-like the_Edges_of G -defined G .edgesInto {CS} -defined the_Edges_of G -defined RAT -valued Function-like total finite complex-valued ext-real-valued real-valued natural-valued finite-support set
Sum (source | (G .edgesInto {CS})) is V28() real ext-real set
G .edgesOutOf {CS} is finite Element of K32((the_Edges_of G))
source | (G .edgesOutOf {CS}) is Relation-like the_Edges_of G -defined G .edgesOutOf {CS} -defined the_Edges_of G -defined RAT -valued Function-like total finite complex-valued ext-real-valued real-valued natural-valued finite-support set
Sum (source | (G .edgesOutOf {CS})) is V28() real ext-real set
(Sum (source | (G .edgesInto {CS}))) - (Sum (source | (G .edgesOutOf {CS}))) is V28() real ext-real set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] real-weighted set
the_Edges_of G is finite set
G . EdgeSelector is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
{1} is non empty trivial finite V36() 1 -element V100() V101() V102() V103() V104() V105() Element of K32(NAT)
{1} \/ (the_Edges_of G) is non empty set
K33((the_Vertices_of G),({1} \/ (the_Edges_of G))) is Relation-like set
K32(K33((the_Vertices_of G),({1} \/ (the_Edges_of G)))) is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
{1} \/ (the_Edges_of G) is non empty set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
{1} \/ (the_Edges_of G) is non empty set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
(the_Vertices_of G) \/ (the_Edges_of G) is non empty set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
(the_Vertices_of G) \/ (the_Edges_of G) is non empty set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
sink is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
len sink is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
CS is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative non even set
sink . CS is set
CS + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
sink . (CS + 2) is set
CS + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() even Element of NAT
sink . (CS + 1) is set
the_Weight_of G is Relation-like the_Edges_of G -defined Function-like total complex-valued ext-real-valued real-valued set
G . WeightSelector is set
(the_Weight_of G) . (sink . (CS + 1)) is V28() real ext-real set
source . (sink . (CS + 1)) is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
(the_Vertices_of G) \/ (the_Edges_of G) is non empty set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
sink is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
CS is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
sink .cut (CS,n) is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
len sink is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
P is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative non even set
(sink .cut (CS,n)) . P is set
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() even Element of NAT
(sink .cut (CS,n)) . (P + 1) is set
P + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
(sink .cut (CS,n)) . (P + 2) is set
len (sink .cut (CS,n)) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
E1 is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
dom (sink .cut (CS,n)) is finite V100() V101() V102() V103() V104() V105() Element of K32(NAT)
Gn1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
P is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
E1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(sink .cut (CS,n)) . (E1 + 2) is set
Gn1 + (E1 + 2) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(Gn1 + (E1 + 2)) - 1 is V28() real integer ext-real set
sink . ((Gn1 + (E1 + 2)) - 1) is set
E1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(sink .cut (CS,n)) . (E1 + 1) is set
Gn1 + (E1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(Gn1 + (E1 + 1)) - 1 is V28() real integer ext-real set
sink . ((Gn1 + (E1 + 1)) - 1) is set
Gn1 + E1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(Gn1 + E1) - 1 is V28() real integer ext-real set
dom sink is finite V100() V101() V102() V103() V104() V105() Element of K32(NAT)
Gn1 + P is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() even Element of NAT
(Gn1 + P) - 1 is non empty V28() real integer ext-real non even set
CS + (P + 2) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(CS + (P + 2)) - 1 is V28() real integer ext-real set
E2 is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
B2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
sink . B2 is set
B2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() even Element of NAT
sink . (B2 + 1) is set
B2 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
sink . (B2 + 2) is set
A2 is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(len sink) - 0 is non empty V28() real integer ext-real positive non negative set
((CS + (P + 2)) - 1) - 2 is V28() real integer ext-real set
the_Weight_of G is Relation-like the_Edges_of G -defined Function-like total complex-valued ext-real-valued real-valued set
G . WeightSelector is set
(the_Weight_of G) . ((sink .cut (CS,n)) . (P + 1)) is V28() real ext-real set
source . ((sink .cut (CS,n)) . (P + 1)) is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() set
len sink is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
len sink is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
(the_Vertices_of G) \/ (the_Edges_of G) is non empty set
the_Weight_of G is Relation-like the_Edges_of G -defined Function-like total complex-valued ext-real-valued real-valued set
G . WeightSelector is set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
sink is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
sink .vertices() is finite Element of K32((the_Vertices_of G))
K32((the_Vertices_of G)) is V79() set
sink .last() is Element of the_Vertices_of G
n is set
CS is set
(the_Weight_of G) . CS is V28() real ext-real set
source . CS is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() set
sink .addEdge CS is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Walk of G
len (sink .addEdge CS) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
Gn1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative non even set
(sink .addEdge CS) . Gn1 is set
Gn1 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
(sink .addEdge CS) . (Gn1 + 2) is set
Gn1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() even Element of NAT
(sink .addEdge CS) . (Gn1 + 1) is set
(the_Weight_of G) . ((sink .addEdge CS) . (Gn1 + 1)) is V28() real ext-real set
source . ((sink .addEdge CS) . (Gn1 + 1)) is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() set
len sink is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
dom sink is finite V100() V101() V102() V103() V104() V105() Element of K32(NAT)
sink . (Gn1 + 1) is set
P + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
sink . (Gn1 + 2) is set
sink . Gn1 is set
len sink is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
2 * 1 is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() even Element of NAT
(len sink) + (2 * 1) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
(len sink) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() even Element of NAT
((len sink) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
dom sink is finite V100() V101() V102() V103() V104() V105() Element of K32(NAT)
sink . Gn1 is set
the_Source_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
K33((the_Edges_of G),(the_Vertices_of G)) is Relation-like set
K32(K33((the_Edges_of G),(the_Vertices_of G))) is set
G . SourceSelector is set
(the_Source_of G) . CS is set
len sink is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() non even Element of NAT
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
{1} \/ (the_Edges_of G) is non empty set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
K32((the_Edges_of G)) is set
sink is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
CS is Element of K32((the_Edges_of G))
n is set
CS is Element of K32((the_Edges_of G))
n is Element of K32((the_Edges_of G))
Gn is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
{1} \/ (the_Edges_of G) is non empty set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
sink is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,sink) is Element of K32((the_Edges_of G))
K32((the_Edges_of G)) is set
the_Source_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
K33((the_Edges_of G),(the_Vertices_of G)) is Relation-like set
K32(K33((the_Edges_of G),(the_Vertices_of G))) is set
G . SourceSelector is set
choose (G,source,sink) is Element of (G,source,sink)
(the_Source_of G) . (choose (G,source,sink)) is set
dom sink is Element of K32((the_Vertices_of G))
K32((the_Vertices_of G)) is V79() set
((the_Source_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)) is Relation-like {((the_Source_of G) . (choose (G,source,sink)))} -defined Function-like one-to-one finite finite-support set
{((the_Source_of G) . (choose (G,source,sink)))} is non empty trivial finite 1 -element set
{((the_Source_of G) . (choose (G,source,sink)))} --> (choose (G,source,sink)) is non empty Relation-like {((the_Source_of G) . (choose (G,source,sink)))} -defined {(choose (G,source,sink))} -valued Function-like constant total V18({((the_Source_of G) . (choose (G,source,sink)))},{(choose (G,source,sink))}) finite finite-support Element of K32(K33({((the_Source_of G) . (choose (G,source,sink)))},{(choose (G,source,sink))}))
{(choose (G,source,sink))} is non empty trivial finite 1 -element set
K33({((the_Source_of G) . (choose (G,source,sink)))},{(choose (G,source,sink))}) is Relation-like finite set
K32(K33({((the_Source_of G) . (choose (G,source,sink)))},{(choose (G,source,sink))})) is finite V36() set
sink +* (((the_Source_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink))) is Relation-like Function-like set
the_Target_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
G . TargetSelector is set
(the_Target_of G) . (choose (G,source,sink)) is set
((the_Target_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)) is Relation-like {((the_Target_of G) . (choose (G,source,sink)))} -defined Function-like one-to-one finite finite-support set
{((the_Target_of G) . (choose (G,source,sink)))} is non empty trivial finite 1 -element set
{((the_Target_of G) . (choose (G,source,sink)))} --> (choose (G,source,sink)) is non empty Relation-like {((the_Target_of G) . (choose (G,source,sink)))} -defined {(choose (G,source,sink))} -valued Function-like constant total V18({((the_Target_of G) . (choose (G,source,sink)))},{(choose (G,source,sink))}) finite finite-support Element of K32(K33({((the_Target_of G) . (choose (G,source,sink)))},{(choose (G,source,sink))}))
K33({((the_Target_of G) . (choose (G,source,sink)))},{(choose (G,source,sink))}) is Relation-like finite set
K32(K33({((the_Target_of G) . (choose (G,source,sink)))},{(choose (G,source,sink))})) is finite V36() set
sink +* (((the_Target_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink))) is Relation-like Function-like set
E1 is set
E1 is set
rng (((the_Target_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink))) is finite set
rng sink is Element of K32(({1} \/ (the_Edges_of G)))
K32(({1} \/ (the_Edges_of G))) is V79() set
(rng sink) \/ (rng (((the_Target_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
rng (sink +* (((the_Target_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
E1 is set
rng (((the_Source_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink))) is finite set
(rng sink) \/ (rng (((the_Source_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
rng (sink +* (((the_Source_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
E1 is set
dom (sink +* (((the_Target_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
dom (((the_Target_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink))) is finite Element of K32({((the_Target_of G) . (choose (G,source,sink)))})
K32({((the_Target_of G) . (choose (G,source,sink)))}) is finite V36() V79() set
(dom sink) \/ (dom (((the_Target_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
(dom sink) \/ {((the_Target_of G) . (choose (G,source,sink)))} is non empty set
K33((the_Vertices_of G),({1} \/ (the_Edges_of G))) is Relation-like set
K32(K33((the_Vertices_of G),({1} \/ (the_Edges_of G)))) is set
dom (sink +* (((the_Source_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
dom (((the_Source_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink))) is finite Element of K32({((the_Source_of G) . (choose (G,source,sink)))})
K32({((the_Source_of G) . (choose (G,source,sink)))}) is finite V36() V79() set
(dom sink) \/ (dom (((the_Source_of G) . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
(dom sink) \/ {((the_Source_of G) . (choose (G,source,sink)))} is non empty set
CS is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
{1} \/ (the_Edges_of G) is non empty set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
NAT --> {} is non empty Relation-like NAT -defined RAT -valued INT -valued {{}} -valued Function-like constant total V18( NAT ,{{}}) T-Sequence-like complex-valued ext-real-valued real-valued natural-valued Function-yielding V199() Element of K32(K33(NAT,{{}}))
{{}} is non empty trivial functional finite V36() 1 -element V100() V101() V102() V103() V104() V105() set
K33(NAT,{{}}) is non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
K32(K33(NAT,{{}})) is non trivial non finite set
CS is Relation-like NAT -defined Function-like total set
n is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
CS . n is set
K33((the_Vertices_of G),({1} \/ (the_Edges_of G))) is Relation-like set
K32(K33((the_Vertices_of G),({1} \/ (the_Edges_of G)))) is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] set
the_Edges_of G is set
G . EdgeSelector is set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
sink is Relation-like NAT -defined Function-like total (G,source)
CS is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
sink . CS is set
the_Vertices_of G is non empty set
G . VertexSelector is set
{1} \/ (the_Edges_of G) is non empty set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
sink is Element of the_Vertices_of G
sink .--> 1 is Relation-like the_Vertices_of G -defined {sink} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one finite complex-valued ext-real-valued real-valued natural-valued finite-support set
{sink} is non empty trivial finite 1 -element set
{sink} --> 1 is non empty Relation-like non-empty {sink} -defined NAT -valued RAT -valued INT -valued {1} -valued Function-like constant total V18({sink},{1}) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33({sink},{1}))
{1} is non empty trivial finite V36() 1 -element V100() V101() V102() V103() V104() V105() set
K33({sink},{1}) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K32(K33({sink},{1})) is finite V36() set
{1} \/ (the_Edges_of G) is non empty set
rng (sink .--> 1) is finite V100() V101() V102() V103() V104() V105() Element of K32(RAT)
K32(RAT) is non trivial non finite V79() set
n is set
CS is set
Gn is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,Gn) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
Gn1 is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
P is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,Gn1) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
n is set
CS is set
n is set
CS is set
CS is set
n is set
Gn1 is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
Gn is set
P is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,Gn1) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
P is set
n is set
CS is Relation-like Function-like set
dom CS is set
CS . 0 is set
n is Relation-like NAT -defined Function-like total set
Gn is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
n . Gn is set
Gn + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
n . (Gn + 1) is set
Gn1 is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
P is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,Gn1) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
dom (sink .--> 1) is finite Element of K32({sink})
K32({sink}) is finite V36() V79() set
{sink} is non empty trivial finite 1 -element Element of K32((the_Vertices_of G))
K32((the_Vertices_of G)) is V79() set
K33((the_Vertices_of G),({1} \/ (the_Edges_of G))) is Relation-like set
K32(K33((the_Vertices_of G),({1} \/ (the_Edges_of G)))) is set
n . 0 is set
Gn is Relation-like NAT -defined Function-like total (G,source)
(G,source,Gn,0) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
Gn1 is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
Gn1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,Gn,(Gn1 + 1)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,Gn,Gn1) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,(G,source,Gn,Gn1)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
P is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
P is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,P) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
CS is Relation-like NAT -defined Function-like total (G,source)
(G,source,CS,0) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
n is Relation-like NAT -defined Function-like total (G,source)
(G,source,n,0) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
Gn is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
(G,source,CS,Gn) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,n,Gn) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
Gn + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,CS,(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,(G,source,n,Gn)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,n,(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
Gn is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
(G,source,CS,Gn) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,n,Gn) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
Gn + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,CS,(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,n,(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
Gn is set
CS . Gn is set
n . Gn is set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
sink is Element of the_Vertices_of G
(G,source,sink) is Relation-like NAT -defined Function-like total (G,source)
(G,source,(G,source,sink),0) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
{1} \/ (the_Edges_of G) is non empty set
dom (G,source,(G,source,sink),0) is Element of K32((the_Vertices_of G))
K32((the_Vertices_of G)) is V79() set
{sink} is non empty trivial finite 1 -element Element of K32((the_Vertices_of G))
sink .--> 1 is Relation-like the_Vertices_of G -defined {sink} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one finite complex-valued ext-real-valued real-valued natural-valued finite-support set
{sink} is non empty trivial finite 1 -element set
{sink} --> 1 is non empty Relation-like non-empty {sink} -defined NAT -valued RAT -valued INT -valued {1} -valued Function-like constant total V18({sink},{1}) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of K32(K33({sink},{1}))
K33({sink},{1}) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K32(K33({sink},{1})) is finite V36() set
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
sink is Element of the_Vertices_of G
(G,source,sink) is Relation-like NAT -defined Function-like total (G,source)
CS is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
n is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
(G,source,(G,source,sink),CS) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
{1} \/ (the_Edges_of G) is non empty set
dom (G,source,(G,source,sink),CS) is Element of K32((the_Vertices_of G))
K32((the_Vertices_of G)) is V79() set
(G,source,(G,source,sink),n) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
dom (G,source,(G,source,sink),n) is Element of K32((the_Vertices_of G))
Gn1 is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
CS + Gn1 is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative set
P is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
CS + P is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,(G,source,sink),(CS + P)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
CS + (P + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,(G,source,sink),(CS + (P + 1))) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,(G,source,(G,source,sink),(CS + P))) is Element of K32((the_Edges_of G))
K32((the_Edges_of G)) is set
choose (G,source,(G,source,(G,source,sink),(CS + P))) is Element of (G,source,(G,source,(G,source,sink),(CS + P)))
(CS + P) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,(G,source,sink),((CS + P) + 1)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
(G,source,(G,source,(G,source,sink),(CS + P))) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
dom (G,source,(G,source,sink),(CS + P)) is Element of K32((the_Vertices_of G))
dom (G,source,(G,source,sink),(CS + (P + 1))) is Element of K32((the_Vertices_of G))
the_Source_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
K33((the_Edges_of G),(the_Vertices_of G)) is Relation-like set
K32(K33((the_Edges_of G),(the_Vertices_of G))) is set
G . SourceSelector is set
(the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is set
((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P))))) .--> (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is Relation-like {((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} -defined Function-like one-to-one finite finite-support set
{((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} is non empty trivial finite 1 -element set
{((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} --> (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is non empty Relation-like {((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} -defined {(choose (G,source,(G,source,(G,source,sink),(CS + P))))} -valued Function-like constant total V18({((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))},{(choose (G,source,(G,source,(G,source,sink),(CS + P))))}) finite finite-support Element of K32(K33({((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))},{(choose (G,source,(G,source,(G,source,sink),(CS + P))))}))
{(choose (G,source,(G,source,(G,source,sink),(CS + P))))} is non empty trivial finite 1 -element set
K33({((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))},{(choose (G,source,(G,source,(G,source,sink),(CS + P))))}) is Relation-like finite set
K32(K33({((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))},{(choose (G,source,(G,source,(G,source,sink),(CS + P))))})) is finite V36() set
(G,source,(G,source,sink),(CS + P)) +* (((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P))))) .--> (choose (G,source,(G,source,(G,source,sink),(CS + P))))) is Relation-like Function-like set
dom (G,source,(G,source,sink),(CS + (P + 1))) is Element of K32((the_Vertices_of G))
the_Source_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
K33((the_Edges_of G),(the_Vertices_of G)) is Relation-like set
K32(K33((the_Edges_of G),(the_Vertices_of G))) is set
G . SourceSelector is set
(the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is set
the_Target_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
G . TargetSelector is set
(the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is set
((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P))))) .--> (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is Relation-like {((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} -defined Function-like one-to-one finite finite-support set
{((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} is non empty trivial finite 1 -element set
{((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} --> (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is non empty Relation-like {((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} -defined {(choose (G,source,(G,source,(G,source,sink),(CS + P))))} -valued Function-like constant total V18({((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))},{(choose (G,source,(G,source,(G,source,sink),(CS + P))))}) finite finite-support Element of K32(K33({((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))},{(choose (G,source,(G,source,(G,source,sink),(CS + P))))}))
{(choose (G,source,(G,source,(G,source,sink),(CS + P))))} is non empty trivial finite 1 -element set
K33({((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))},{(choose (G,source,(G,source,(G,source,sink),(CS + P))))}) is Relation-like finite set
K32(K33({((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))},{(choose (G,source,(G,source,(G,source,sink),(CS + P))))})) is finite V36() set
(G,source,(G,source,sink),(CS + P)) +* (((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P))))) .--> (choose (G,source,(G,source,(G,source,sink),(CS + P))))) is Relation-like Function-like set
dom (G,source,(G,source,sink),(CS + (P + 1))) is Element of K32((the_Vertices_of G))
the_Source_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
K33((the_Edges_of G),(the_Vertices_of G)) is Relation-like set
K32(K33((the_Edges_of G),(the_Vertices_of G))) is set
G . SourceSelector is set
(the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is set
dom (G,source,(G,source,sink),(CS + (P + 1))) is Element of K32((the_Vertices_of G))
dom (G,source,(G,source,sink),(CS + (P + 1))) is Element of K32((the_Vertices_of G))
CS + 0 is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,(G,source,sink),(CS + 0)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
dom (G,source,(G,source,sink),(CS + 0)) is Element of K32((the_Vertices_of G))
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] [Weighted] real-weighted set
the_Edges_of G is set
G . EdgeSelector is set
the_Vertices_of G is non empty set
G . VertexSelector is set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued set
sink is Element of the_Vertices_of G
(G,source,sink) is Relation-like NAT -defined Function-like total (G,source)
(G,source,sink) .Result() is set
(G,source,sink) .Lifespan() is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,sink) . ((G,source,sink) .Lifespan()) is set
{1} \/ (the_Edges_of G) is non empty set
(G,source,(G,source,sink),((G,source,sink) .Lifespan())) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like (G,source)
G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite [Weighted] real-weighted set
the_Edges_of G is finite set
G . EdgeSelector is set
the_Vertices_of G is non empty finite set
G . VertexSelector is set
source is Relation-like the_Edges_of G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
sink is Element of the_Vertices_of G
(G,source,sink) is Relation-like NAT -defined Function-like total (G,source)
card (the_Vertices_of G) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
Gn is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,(G,source,sink),Gn) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like finite finite-support (G,source)
{1} \/ (the_Edges_of G) is non empty finite set
Gn + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(G,source,(G,source,sink),(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like finite finite-support (G,source)
(G,source,(G,source,(G,source,sink),Gn)) is finite Element of K32((the_Edges_of G))
K32((the_Edges_of G)) is finite V36() set
choose (G,source,(G,source,(G,source,sink),Gn)) is Element of (G,source,(G,source,(G,source,sink),Gn))
(G,source,(G,source,(G,source,sink),Gn)) is Relation-like the_Vertices_of G -defined {1} \/ (the_Edges_of G) -valued Function-like finite finite-support (G,source)
dom (G,source,(G,source,sink),Gn) is finite Element of K32((the_Vertices_of G))
K32((the_Vertices_of G)) is finite V36() V79() set
card (dom (G,source,(G,source,sink),Gn)) is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
dom (G,source,(G,source,sink),(Gn + 1)) is finite Element of K32((the_Vertices_of G))
card (dom (G,source,(G,source,sink),(Gn + 1))) is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(Gn + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
the_Source_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) finite finite-support Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
K33((the_Edges_of G),(the_Vertices_of G)) is Relation-like finite set
K32(K33((the_Edges_of G),(the_Vertices_of G))) is finite V36() set
G . SourceSelector is set
(the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))) is set
((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn)))) .--> (choose (G,source,(G,source,(G,source,sink),Gn))) is Relation-like {((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))} -defined Function-like one-to-one finite finite-support set
{((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))} is non empty trivial finite 1 -element set
{((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))} --> (choose (G,source,(G,source,(G,source,sink),Gn))) is non empty Relation-like {((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))} -defined {(choose (G,source,(G,source,(G,source,sink),Gn)))} -valued Function-like constant total V18({((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))},{(choose (G,source,(G,source,(G,source,sink),Gn)))}) finite finite-support Element of K32(K33({((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))},{(choose (G,source,(G,source,(G,source,sink),Gn)))}))
{(choose (G,source,(G,source,(G,source,sink),Gn)))} is non empty trivial finite 1 -element set
K33({((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))},{(choose (G,source,(G,source,(G,source,sink),Gn)))}) is Relation-like finite set
K32(K33({((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))},{(choose (G,source,(G,source,(G,source,sink),Gn)))})) is finite V36() set
(G,source,(G,source,sink),Gn) +* (((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn)))) .--> (choose (G,source,(G,source,(G,source,sink),Gn)))) is Relation-like Function-like finite finite-support set
dom (G,source,(G,source,sink),(Gn + 1)) is finite Element of K32((the_Vertices_of G))
(dom (G,source,(G,source,sink),Gn)) \/ {((the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))} is non empty finite set
card (dom (G,source,(G,source,sink),(Gn + 1))) is epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
(Gn + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real integer finite cardinal ext-real positive non negative V77() V100() V101() V102() V103() V104() V105() Element of NAT
the_Source_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) finite finite-support Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
K33((the_Edges_of G),(the_Vertices_of G)) is Relation-like finite set
K32(K33((the_Edges_of G),(the_Vertices_of G))) is finite V36() set
G . SourceSelector is set
(the_Source_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))) is set
the_Target_of G is Relation-like the_Edges_of G -defined the_Vertices_of G -valued Function-like total V18( the_Edges_of G, the_Vertices_of G) finite finite-support Element of K32(K33((the_Edges_of G),(the_Vertices_of G)))
G . TargetSelector is set
(the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))) is set
((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),Gn)))) .--> (choose (G,source,(G,source,(G,source,sink),Gn))) is Relation-like {((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))} -defined Function-like one-to-one finite finite-support set
{((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))} is non empty trivial finite 1 -element set
{((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))} --> (choose (G,source,(G,source,(G,source,sink),Gn))) is non empty Relation-like {((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))} -defined {(choose (G,source,(G,source,(G,source,sink),Gn)))} -valued Function-like constant total V18({((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))},{(choose (G,source,(G,source,(G,source,sink),Gn)))}) finite finite-support Element of K32(K33({((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))},{(choose (G,source,(G,source,(G,source,sink),Gn)))}))
{(choose (G,source,(G,source,(G,source,sink),Gn)))} is non empty trivial finite 1 -element set
K33({((the_Target_of G) . (choose (G,source,(G,source,(G,source,sink),Gn))))},{(choose (G,source,(G,source,(G,source,sink),Gn)))}) is Relation-like