:: 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

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)

{ b

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