:: GLIB_005 semantic presentation

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

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()))

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

K32(K33(NAT,REAL)) is non trivial non finite set

K224(1,NAT) is M11( NAT )
{{},1} is non empty finite V36() V100() V101() V102() V103() V104() V105() set

_GraphSelectors is non empty V100() V101() V102() V103() V104() V105() Element of K32(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

dom G is set
source is set
sink is 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

source is set
sink is 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

source is set
sink is 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

source is set
CS is set
sink is 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

source is set
rng () is set

{1} is non empty trivial finite V36() 1 -element V100() V101() V102() V103() V104() V105() Element of K32(NAT)

K32(K33({},{1})) is finite V36() set

the_Edges_of (createGraph ({1},{},sink,sink)) is finite set
(createGraph ({1},{},sink,sink)) . EdgeSelector is 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))

is non empty trivial finite V36() 1 -element V100() V101() V102() V103() V104() V105() 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 non empty Relation-like -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(,{ 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(,{ 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(,{ 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(,{ 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

CS is set
{CS} is non empty trivial finite 1 -element set
G .edgesInto {CS} is finite Element of K32(())
K32(()) is finite V36() set

Sum (source | (G .edgesInto {CS})) is V28() real ext-real set
G .edgesOutOf {CS} is finite Element of K32(())

Sum (source | ()) is V28() real ext-real set
(Sum (source | (G .edgesInto {CS}))) - (Sum (source | ())) is V28() real ext-real set

the_Vertices_of G is non empty set

{1} is non empty trivial finite V36() 1 -element V100() V101() V102() V103() V104() V105() Element of K32(NAT)
{1} \/ () is non empty set
K33((),({1} \/ ())) is Relation-like set
K32(K33((),({1} \/ ()))) is set

the_Vertices_of G is non empty set

{1} \/ () is non empty set

the_Vertices_of G is non empty set

{1} \/ () is non empty set

the_Vertices_of G is non empty set

() \/ () is non empty set

the_Vertices_of G is non empty set

() \/ () is non empty 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

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

sink . (CS + 1) is set

() . (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

the_Vertices_of G is non empty set

() \/ () is non empty 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

(sink .cut (CS,n)) . P is set

(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

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

(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

(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) - 1 is V28() real integer ext-real set
dom sink is finite V100() V101() V102() V103() V104() V105() Element of K32(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

sink . B2 is set

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

(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

() . ((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

the_Vertices_of G is non empty set

() \/ () is non empty set

sink .vertices() is finite Element of K32(())
K32(()) is V79() set
sink .last() is Element of the_Vertices_of G
n is set
CS is set
() . CS is V28() real ext-real set

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

(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

(sink .addEdge CS) . (Gn1 + 1) is set
() . ((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

dom sink is finite V100() V101() V102() V103() V104() V105() Element of K32(NAT)
sink . (Gn1 + 1) is set

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

(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

K33((),()) is Relation-like set
K32(K33((),())) is set

() . 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

the_Vertices_of G is non empty set

{1} \/ () is non empty set

K32(()) is set
sink is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
CS is Element of K32(())
n is set
CS is Element of K32(())
n is Element of K32(())
Gn is set

the_Vertices_of G is non empty set

{1} \/ () is non empty set

sink is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,sink) is Element of K32(())
K32(()) is set

K33((),()) is Relation-like set
K32(K33((),())) is set

choose (G,source,sink) is Element of (G,source,sink)
() . (choose (G,source,sink)) is set
dom sink is Element of K32(())
K32(()) is V79() set
(() . (choose (G,source,sink))) .--> (choose (G,source,sink)) is Relation-like {(() . (choose (G,source,sink)))} -defined Function-like one-to-one finite finite-support set
{(() . (choose (G,source,sink)))} is non empty trivial finite 1 -element set
{(() . (choose (G,source,sink)))} --> (choose (G,source,sink)) is non empty Relation-like {(() . (choose (G,source,sink)))} -defined {(choose (G,source,sink))} -valued Function-like constant total V18({(() . (choose (G,source,sink)))},{(choose (G,source,sink))}) finite finite-support Element of K32(K33({(() . (choose (G,source,sink)))},{(choose (G,source,sink))}))
{(choose (G,source,sink))} is non empty trivial finite 1 -element set
K33({(() . (choose (G,source,sink)))},{(choose (G,source,sink))}) is Relation-like finite set
K32(K33({(() . (choose (G,source,sink)))},{(choose (G,source,sink))})) is finite V36() set
sink +* ((() . (choose (G,source,sink))) .--> (choose (G,source,sink))) is Relation-like Function-like set

() . (choose (G,source,sink)) is set
(() . (choose (G,source,sink))) .--> (choose (G,source,sink)) is Relation-like {(() . (choose (G,source,sink)))} -defined Function-like one-to-one finite finite-support set
{(() . (choose (G,source,sink)))} is non empty trivial finite 1 -element set
{(() . (choose (G,source,sink)))} --> (choose (G,source,sink)) is non empty Relation-like {(() . (choose (G,source,sink)))} -defined {(choose (G,source,sink))} -valued Function-like constant total V18({(() . (choose (G,source,sink)))},{(choose (G,source,sink))}) finite finite-support Element of K32(K33({(() . (choose (G,source,sink)))},{(choose (G,source,sink))}))
K33({(() . (choose (G,source,sink)))},{(choose (G,source,sink))}) is Relation-like finite set
K32(K33({(() . (choose (G,source,sink)))},{(choose (G,source,sink))})) is finite V36() set
sink +* ((() . (choose (G,source,sink))) .--> (choose (G,source,sink))) is Relation-like Function-like set
E1 is set
E1 is set
rng ((() . (choose (G,source,sink))) .--> (choose (G,source,sink))) is finite set
rng sink is Element of K32(({1} \/ ()))
K32(({1} \/ ())) is V79() set
(rng sink) \/ (rng ((() . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
rng (sink +* ((() . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
E1 is set
rng ((() . (choose (G,source,sink))) .--> (choose (G,source,sink))) is finite set
(rng sink) \/ (rng ((() . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
rng (sink +* ((() . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
E1 is set
dom (sink +* ((() . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
dom ((() . (choose (G,source,sink))) .--> (choose (G,source,sink))) is finite Element of K32({(() . (choose (G,source,sink)))})
K32({(() . (choose (G,source,sink)))}) is finite V36() V79() set
(dom sink) \/ (dom ((() . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
(dom sink) \/ {(() . (choose (G,source,sink)))} is non empty set
K33((),({1} \/ ())) is Relation-like set
K32(K33((),({1} \/ ()))) is set
dom (sink +* ((() . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
dom ((() . (choose (G,source,sink))) .--> (choose (G,source,sink))) is finite Element of K32({(() . (choose (G,source,sink)))})
K32({(() . (choose (G,source,sink)))}) is finite V36() V79() set
(dom sink) \/ (dom ((() . (choose (G,source,sink))) .--> (choose (G,source,sink)))) is set
(dom sink) \/ {(() . (choose (G,source,sink)))} is non empty set
CS is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)

the_Vertices_of G is non empty set

{1} \/ () is non empty set

is non empty trivial functional finite V36() 1 -element V100() V101() V102() V103() V104() V105() set

K32(K33(NAT,)) is non trivial non finite set

CS . n is set
K33((),({1} \/ ())) is Relation-like set
K32(K33((),({1} \/ ()))) is set

sink is Relation-like NAT -defined Function-like total (G,source)

sink . CS is set
the_Vertices_of G is non empty set

{1} \/ () is non empty set

the_Vertices_of G is non empty set

sink is Element of the_Vertices_of G

{sink} is non empty trivial finite 1 -element set

{1} is non empty trivial finite V36() 1 -element V100() V101() V102() V103() V104() V105() set

K32(K33({sink},{1})) is finite V36() set
{1} \/ () 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} \/ () -valued Function-like (G,source)
(G,source,Gn) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
Gn1 is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
P is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,Gn1) is Relation-like the_Vertices_of G -defined {1} \/ () -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} \/ () -valued Function-like (G,source)
Gn is set
P is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,Gn1) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
P is set
n is set

dom CS is set
CS . 0 is set

n . Gn is set

n . (Gn + 1) is set
Gn1 is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
P is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,Gn1) is Relation-like the_Vertices_of G -defined {1} \/ () -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(())
K32(()) is V79() set
K33((),({1} \/ ())) is Relation-like set
K32(K33((),({1} \/ ()))) 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} \/ () -valued Function-like (G,source)

(G,source,Gn,(Gn1 + 1)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,Gn,Gn1) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,(G,source,Gn,Gn1)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
P is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
P is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,P) is Relation-like the_Vertices_of G -defined {1} \/ () -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} \/ () -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} \/ () -valued Function-like (G,source)

(G,source,CS,Gn) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,n,Gn) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)

(G,source,CS,(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,(G,source,n,Gn)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,n,(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)

(G,source,CS,Gn) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,n,Gn) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)

(G,source,CS,(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
(G,source,n,(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
Gn is set
CS . Gn is set
n . Gn is set

the_Vertices_of G is non empty 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} \/ () -valued Function-like (G,source)
{1} \/ () is non empty set
dom (G,source,(G,source,sink),0) is Element of K32(())
K32(()) is V79() set
{sink} is non empty trivial finite 1 -element Element of K32(())

{sink} is non empty trivial finite 1 -element set

K32(K33({sink},{1})) is finite V36() set

the_Vertices_of G is non empty 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),CS) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
{1} \/ () is non empty set
dom (G,source,(G,source,sink),CS) is Element of K32(())
K32(()) is V79() set
(G,source,(G,source,sink),n) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
dom (G,source,(G,source,sink),n) is Element of K32(())

(G,source,(G,source,sink),(CS + P)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)

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} \/ () -valued Function-like (G,source)
(G,source,(G,source,(G,source,sink),(CS + P))) is Element of K32(())
K32(()) 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} \/ () -valued Function-like (G,source)
(G,source,(G,source,(G,source,sink),(CS + P))) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
dom (G,source,(G,source,sink),(CS + P)) is Element of K32(())
dom (G,source,(G,source,sink),(CS + (P + 1))) is Element of K32(())

K33((),()) is Relation-like set
K32(K33((),())) is set

() . (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is set
(() . (choose (G,source,(G,source,(G,source,sink),(CS + P))))) .--> (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is Relation-like {(() . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} -defined Function-like one-to-one finite finite-support set
{(() . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} is non empty trivial finite 1 -element set
{(() . (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 {(() . (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({(() . (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({(() . (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({(() . (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({(() . (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)) +* ((() . (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(())

K33((),()) is Relation-like set
K32(K33((),())) is set

() . (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is set

() . (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is set
(() . (choose (G,source,(G,source,(G,source,sink),(CS + P))))) .--> (choose (G,source,(G,source,(G,source,sink),(CS + P)))) is Relation-like {(() . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} -defined Function-like one-to-one finite finite-support set
{(() . (choose (G,source,(G,source,(G,source,sink),(CS + P)))))} is non empty trivial finite 1 -element set
{(() . (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 {(() . (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({(() . (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({(() . (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({(() . (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({(() . (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)) +* ((() . (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(())

K33((),()) is Relation-like set
K32(K33((),())) is set

() . (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(())
dom (G,source,(G,source,sink),(CS + (P + 1))) is Element of K32(())

(G,source,(G,source,sink),(CS + 0)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)
dom (G,source,(G,source,sink),(CS + 0)) is Element of K32(())

the_Vertices_of G is non empty 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} \/ () is non empty set
(G,source,(G,source,sink),((G,source,sink) .Lifespan())) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like (G,source)

the_Vertices_of G is non empty finite 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),Gn) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like finite finite-support (G,source)
{1} \/ () is non empty finite set

(G,source,(G,source,sink),(Gn + 1)) is Relation-like the_Vertices_of G -defined {1} \/ () -valued Function-like finite finite-support (G,source)
(G,source,(G,source,(G,source,sink),Gn)) is finite Element of K32(())
K32(()) 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} \/ () -valued Function-like finite finite-support (G,source)
dom (G,source,(G,source,sink),Gn) is finite Element of K32(())
K32(()) 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(())
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

K33((),()) is Relation-like finite set
K32(K33((),())) is finite V36() set

() . (choose (G,source,(G,source,(G,source,sink),Gn))) is set
(() . (choose (G,source,(G,source,(G,source,sink),Gn)))) .--> (choose (G,source,(G,source,(G,source,sink),Gn))) is Relation-like {(() . (choose (G,source,(G,source,(G,source,sink),Gn))))} -defined Function-like one-to-one finite finite-support set
{(() . (choose (G,source,(G,source,(G,source,sink),Gn))))} is non empty trivial finite 1 -element set
{(() . (choose (G,source,(G,source,(G,source,sink),Gn))))} --> (choose (G,source,(G,source,(G,source,sink),Gn))) is non empty Relation-like {(() . (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({(() . (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({(() . (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({(() . (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({(() . (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) +* ((() . (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(())
(dom (G,source,(G,source,sink),Gn)) \/ {(() . (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

K33((),()) is Relation-like finite set
K32(K33((),())) is finite V36() set

() . (choose (G,source,(G,source,(G,source,sink),Gn))) is set

() . (choose (G,source,(G,source,(G,source,sink),Gn))) is set
(() . (choose (G,source,(G,source,(G,source,sink),Gn)))) .--> (choose (G,source,(G,source,(G,source,sink),Gn))) is Relation-like {(() . (choose (G,source,(G,source,(G,source,sink),Gn))))} -defined Function-like one-to-one finite finite-support set
{(() . (choose (G,source,(G,source,(G,source,sink),Gn))))} is non empty trivial finite 1 -element set
{(() . (choose (G,source,(G,source,(G,source,sink),Gn))))} --> (choose (G,source,(G,source,(G,source,sink),Gn))) is non empty Relation-like {(() . (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({(() . (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({(() . (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({(() . (choose (G,source,(G,source,(G,source,sink),Gn))))},{(choose (G,source,(G,source,(G,source,sink),Gn)))}) is Relation-like