:: LEXBFS semantic presentation

REAL is complex-membered ext-real-membered real-membered V30() V33() V34() V36() set

NAT is non empty non trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V31() V33() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty cup-closed diff-closed preBoolean set

NAT is non empty non trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V31() V33() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool NAT is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

bool NAT is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

COMPLEX is complex-membered V30() set

RAT is complex-membered ext-real-membered real-membered rational-membered V30() set

INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V30() set

{} is empty Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() complex-valued ext-real-valued real-valued natural-valued FinSequence-yielding finite-support Function-yielding V264() set

2 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

[:NAT,REAL:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:NAT,REAL:] is non empty cup-closed diff-closed preBoolean set

1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

K216(1,NAT) is M10( NAT )

{{},1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered set

3 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

_GraphSelectors is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V33() Element of bool NAT

VertexSelector is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

EdgeSelector is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

SourceSelector is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

TargetSelector is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

4 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

{VertexSelector,EdgeSelector,SourceSelector,TargetSelector} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT

card {} is empty Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() complex-valued ext-real-valued real-valued natural-valued FinSequence-yielding finite-support Function-yielding V264() set

0 is empty Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() V59() complex-valued ext-real-valued real-valued natural-valued FinSequence-yielding finite-support Function-yielding V264() Element of NAT

proj1 {} is empty Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() complex-valued ext-real-valued real-valued natural-valued FinSequence-yielding finite-support Function-yielding V264() set

proj2 {} is empty trivial Relation-like non-zero empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V30() V33() V34() V35() V36() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() real V57() complex-valued ext-real-valued real-valued natural-valued V72() decreasing non-decreasing non-increasing FinSequence-yielding finite-support V224() Function-yielding V264() set

6 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

5 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G is Relation-like Function-like set

proj1 G is set

L is set

V is set

L .--> V is Relation-like {L} -defined Function-like one-to-one finite finite-support set

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

{L} --> V is non empty Relation-like {L} -defined {V} -valued Function-like constant total quasi_total finite finite-support Element of bool [:{L},{V}:]

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

[:{L},{V}:] is non empty Relation-like finite set

bool [:{L},{V}:] is non empty finite finite-membered cup-closed diff-closed preBoolean V225() set

G +* (L .--> V) is Relation-like Function-like set

proj1 (G +* (L .--> V)) is set

(proj1 G) \/ {L} is non empty set

dom (L .--> V) is trivial finite Element of bool {L}

bool {L} is non empty finite finite-membered cup-closed diff-closed preBoolean V225() set

(proj1 G) \/ (dom (L .--> V)) is set

G is Relation-like Function-like one-to-one set

L is set

V is set

G | L is Relation-like Function-like set

(G | L) " is Relation-like Function-like set

proj1 ((G | L) ") is set

G | V is Relation-like Function-like set

(G | V) " is Relation-like Function-like set

(G | L) ~ is Relation-like set

(G | V) ~ is Relation-like set

a is set

((G | L) ") . a is set

((G | V) ") . a is set

G is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G + L is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

V is non empty set

[:NAT,V:] is non empty non trivial Relation-like non finite set

bool [:NAT,V:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

a is Relation-like NAT -defined V -valued Function-like quasi_total Element of bool [:NAT,V:]

{ (a . b

card { (a . b

{ (a . b

card { (a . b

dom a is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool NAT

b is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G + b is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

{ (a . b

card { (a . b

b + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G + (b + 1) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

{ (a . b

card { (a . b

(b + 1) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(G + b) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

{ (a . b

vc is set

P is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

a . P is Element of V

a . ((G + b) + 1) is Element of V

{(a . ((G + b) + 1))} is non empty trivial finite 1 -element Element of bool V

bool V is non empty cup-closed diff-closed preBoolean V225() set

va is finite set

va \/ {(a . ((G + b) + 1))} is non empty finite set

va is finite set

a . ((G + b) + 1) is Element of V

{(a . ((G + b) + 1))} is non empty trivial finite 1 -element Element of bool V

bool V is non empty cup-closed diff-closed preBoolean V225() set

va \/ {(a . ((G + b) + 1))} is non empty finite set

va is finite set

a . ((G + b) + 1) is Element of V

{(a . ((G + b) + 1))} is non empty trivial finite 1 -element Element of bool V

bool V is non empty cup-closed diff-closed preBoolean V225() set

va \/ {(a . ((G + b) + 1))} is non empty finite set

va is finite set

a . ((G + b) + 1) is Element of V

{(a . ((G + b) + 1))} is non empty trivial finite 1 -element Element of bool V

bool V is non empty cup-closed diff-closed preBoolean V225() set

va \/ {(a . ((G + b) + 1))} is non empty finite set

P is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

a . P is Element of V

{ (a . b

{ (a . b

{ (a . b

vc is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

a . vc is Element of V

card (va \/ {(a . ((G + b) + 1))}) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

b is set

G + 0 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

{ (a . b

c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

a . c is Element of V

a . G is Element of V

{(a . G)} is non empty trivial finite 1 -element Element of bool V

bool V is non empty cup-closed diff-closed preBoolean V225() set

card { (a . b

0 + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L is ext-real V55() real set

G is ext-real V55() real set

V is ext-real V55() real set

V - G is ext-real V55() real set

(V - G) + 1 is ext-real V55() real set

V - L is ext-real V55() real set

(V - L) + 1 is ext-real V55() real set

L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

G is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

V -' G is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

V -' L is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

V - G is ext-real V55() real V57() set

V - L is ext-real V55() real V57() set

bool (bool NAT) is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

{1} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element Element of bool NAT

{{1}} is non empty trivial finite finite-membered 1 -element Element of bool (bool NAT)

L is Element of bool (bool NAT)

G is Relation-like Function-like set

proj1 G is set

L is Relation-like Function-like set

proj1 L is set

(proj1 G) \/ (proj1 L) is set

a is set

G . a is set

L . a is set

(G . a) \/ (L . a) is set

a is Relation-like Function-like set

proj1 a is set

a is Relation-like Function-like set

proj1 a is set

b is set

a . b is set

G . b is set

L . b is set

(G . b) \/ (L . b) is set

V is Relation-like Function-like set

proj1 V is set

a is Relation-like Function-like set

proj1 a is set

b is set

V . b is set

G . b is set

L . b is set

(G . b) \/ (L . b) is set

a . b is set

G is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

Seg V is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite V -element Element of bool NAT

L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

V -' L is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

Seg (V -' L) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite V -' L -element Element of bool NAT

(Seg V) \ (Seg (V -' L)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT

0 + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

Seg L is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -element Element of bool NAT

L -' G is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

Seg (L -' G) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -' G -element Element of bool NAT

(Seg L) \ (Seg (L -' G)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT

L -' V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

Seg (L -' V) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -' V -element Element of bool NAT

(Seg L) \ (Seg (L -' V)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT

a is set

a is set

b is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

G is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

Seg L is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -element Element of bool NAT

L -' G is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

Seg (L -' G) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -' G -element Element of bool NAT

(Seg L) \ (Seg (L -' G)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT

{(L -' G)} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element Element of bool NAT

((Seg L) \ (Seg (L -' G))) \/ {(L -' G)} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT

G + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L -' (G + 1) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

Seg (L -' (G + 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite L -' (G + 1) -element Element of bool NAT

(Seg L) \ (Seg (L -' (G + 1))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT

b is set

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

b is set

c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(L -' (G + 1)) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

NAT --> {} is non empty Relation-like NAT -defined RAT -valued INT -valued {{}} -valued Function-like constant total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued natural-valued Function-yielding V264() Element of bool [:NAT,{{}}:]

{{}} is non empty trivial functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element set

[:NAT,{{}}:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

bool [:NAT,{{}}:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

rng (NAT --> {}) is non empty trivial functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element Element of bool {{}}

bool {{}} is non empty finite finite-membered cup-closed diff-closed preBoolean V225() set

L is set

L is set

G is Relation-like Function-like finite-yielding () set

L is set

G . L is finite set

proj1 G is set

proj2 G is finite-membered set

proj1 G is set

proj1 G is set

G is epsilon-transitive epsilon-connected ordinal set

bool G is non empty cup-closed diff-closed preBoolean set

L is finite Element of bool G

V is finite Element of bool G

(L,1) -bag is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags G

Bags G is non empty set

Bags G is non empty functional Element of bool (Bags G)

bool (Bags G) is non empty cup-closed diff-closed preBoolean V225() set

(V,1) -bag is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags G

a is set

((V,1) -bag) . a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

proj1 G is set

L is set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

L /\ (proj1 G) is set

a is Relation-like Function-like set

proj1 a is set

b is set

proj2 a is set

c is set

a . c is set

G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(G . c) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G +* a is Relation-like Function-like set

proj2 (G +* a) is set

rng G is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool RAT

bool RAT is non empty cup-closed diff-closed preBoolean set

(rng G) \/ (proj2 a) is set

b is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

proj1 b is set

(proj1 G) \/ (L /\ (proj1 G)) is set

c is set

b . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

a . c is set

G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(G . c) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

c is set

b . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(G . c) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

va is set

b . va is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . va is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

a is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

proj1 a is set

b is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

proj1 b is set

c is set

a . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(G . c) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

b . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

a . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

b . c is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G is epsilon-transitive epsilon-connected ordinal set

Bags G is non empty functional Element of bool (Bags G)

Bags G is non empty set

bool (Bags G) is non empty cup-closed diff-closed preBoolean V225() set

[:(Bags G),(Bags G):] is non empty Relation-like set

bool [:(Bags G),(Bags G):] is non empty cup-closed diff-closed preBoolean V225() set

bool (Bags G) is non empty cup-closed diff-closed preBoolean V225() set

V is non empty functional finite Element of bool (Bags G)

L is Relation-like Bags G -defined Bags G -valued total reflexive antisymmetric connected transitive Element of bool [:(Bags G),(Bags G):]

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

proj2 a is finite set

len a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

dom a is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT

b is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

b + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

a . (b + 1) is set

va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

a . va is set

vb is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

a . va is set

vb is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

c is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

max (vb,c,L) is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

a . P is set

e1 is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

P is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

a . P is set

e1 is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

a . 1 is set

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

a . c is set

va is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

b is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

a . b is set

c is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

va is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

vb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

a . vb is set

va is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

a is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

b is Relation-like G -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set

G is epsilon-transitive epsilon-connected ordinal set

InvLexOrder G is Relation-like Bags G -defined Bags G -valued total reflexive antisymmetric transitive admissible Element of bool [:(Bags G),(Bags G):]

Bags G is non empty functional Element of bool (Bags G)

Bags G is non empty set

bool (Bags G) is non empty cup-closed diff-closed preBoolean V225() set

[:(Bags G),(Bags G):] is non empty Relation-like set

bool [:(Bags G),(Bags G):] is non empty cup-closed diff-closed preBoolean V225() set

G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

the_Edges_of G is set

G . EdgeSelector is set

(the_Vertices_of G) \/ (the_Edges_of G) is non empty set

L 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

L .last() is Element of the_Vertices_of G

len L is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT

L . (len L) is set

L .length() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like finite-support EdgeSeq of G

len (L .edgeSeq()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(L .length()) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

a is set

V is set

L .addEdge V 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

(L .last()) .adj V is Element of the_Vertices_of G

G .walkOf ((L .last()),V,((L .last()) .adj V)) is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Trail-like Path-like Walk of G

L .append (G .walkOf ((L .last()),V,((L .last()) .adj V))) 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

(L .addEdge V) .length() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(L .addEdge V) .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like finite-support EdgeSeq of G

len ((L .addEdge V) .edgeSeq()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

<*V*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support set

(L .edgeSeq()) ^ <*V*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

len <*V*> is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

the_Edges_of G is set

G . EdgeSelector is set

(the_Vertices_of G) \/ (the_Edges_of G) is non empty set

L 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

L .length() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like finite-support EdgeSeq of G

len (L .edgeSeq()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

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

(L .reverse()) .length() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(L .reverse()) .edgeSeq() is Relation-like NAT -defined the_Edges_of G -valued Function-like finite FinSequence-like FinSubsequence-like finite-support EdgeSeq of G

len ((L .reverse()) .edgeSeq()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

len L is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT

2 * (L .length()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() even Element of NAT

(2 * (L .length())) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT

len (L .reverse()) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT

((2 * (L .length())) + 1) - 1 is ext-real V55() real V57() even set

2 * ((L .reverse()) .length()) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() even Element of NAT

(2 * ((L .reverse()) .length())) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT

((2 * ((L .reverse()) .length())) + 1) - 1 is ext-real V55() real V57() even set

G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] set

the_Vertices_of G is non empty set

G . VertexSelector is set

the_Edges_of G is set

G . EdgeSelector is set

(the_Vertices_of G) \/ (the_Edges_of G) is non empty set

L 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

L .last() is Element of the_Vertices_of G

len L is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT

L . (len L) is set

dom L is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT

a is set

V is set

L .addEdge V 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

(L .last()) .adj V is Element of the_Vertices_of G

G .walkOf ((L .last()),V,((L .last()) .adj V)) is Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Trail-like Path-like Walk of G

L .append (G .walkOf ((L .last()),V,((L .last()) .adj V))) 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

dom (L .addEdge V) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT

b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

(L .addEdge V) . b is set

L . b is set

(len L) + 2 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT

len (L .addEdge V) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() non even Element of NAT

NAT --> 1 is non empty Relation-like non-zero NAT -defined NAT -valued RAT -valued INT -valued Function-like constant total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]

[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

bool [:NAT,NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

{1} is non empty trivial complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite finite-membered 1 -element set

[:NAT,{1}:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

L is Relation-like NAT -defined Function-like total set

L . 0 is set

0 + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L . (0 + 1) is set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

L . V is set

a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

L . a is set

V + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L . (V + 1) is set

a + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L . (a + 1) is set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

L . V is set

G is Relation-like NAT -defined Function-like total set

G .Lifespan() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . (G .Lifespan()) is set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

(G .Lifespan()) + V is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . ((G .Lifespan()) + V) is set

V + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(G .Lifespan()) + (V + 1) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . ((G .Lifespan()) + (V + 1)) is set

(G .Lifespan()) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . ((G .Lifespan()) + 1) is set

((G .Lifespan()) + V) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . (((G .Lifespan()) + V) + 1) is set

(G .Lifespan()) + 0 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . ((G .Lifespan()) + 0) is set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

G . V is set

a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

(G .Lifespan()) + a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G is Relation-like NAT -defined Function-like total set

G is Relation-like NAT -defined Function-like total set

L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

G . L is set

L + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . (L + 1) is set

G is Relation-like NAT -defined Function-like total set

G is Relation-like NAT -defined Function-like total halting () () set

G .Lifespan() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . (G .Lifespan()) is set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

G . V is set

a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

(G .Lifespan()) + a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . ((G .Lifespan()) + a) is set

a + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(G .Lifespan()) + (a + 1) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . ((G .Lifespan()) + (a + 1)) is set

(G .Lifespan()) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . ((G .Lifespan()) + 1) is set

((G .Lifespan()) + a) + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . (((G .Lifespan()) + a) + 1) is set

(G .Lifespan()) + 0 is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G . ((G .Lifespan()) + 0) is set

a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

(G .Lifespan()) + a is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

G is Relation-like NAT -defined Function-like total halting () () set

G .Lifespan() is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

L is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

G . V is set

G . L is set

G . (G .Lifespan()) is set

G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite set

the_Vertices_of G is non empty finite set

G . VertexSelector is set

[:(the_Vertices_of G),NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

bool [:(the_Vertices_of G),NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

L is Relation-like NAT -defined Function-like total set

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

L . V is set

G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite set

L is Relation-like NAT -defined Function-like total (G)

V is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

L . V is set

the_Vertices_of G is non empty finite set

G . VertexSelector is set

[:(the_Vertices_of G),NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

bool [:(the_Vertices_of G),NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite set

G is Relation-like NAT -defined Function-like finite finite-support [Graph-like] finite set

the_Vertices_of G is non empty finite set

G . VertexSelector is set

card (the_Vertices_of G) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

canFS (the_Vertices_of G) is non empty Relation-like NAT -defined the_Vertices_of G -valued Function-like one-to-one onto finite FinSequence-like FinSubsequence-like finite-support FinSequence of the_Vertices_of G

[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

bool [:NAT,NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

a is Relation-like NAT -defined NAT -valued Function-like quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]

b is set

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT

(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]

[:NAT,(the_Vertices_of G):] is non empty non trivial Relation-like non finite set

bool [:NAT,(the_Vertices_of G):] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

((canFS (the_Vertices_of G)) | (Seg c)) " is Relation-like Function-like set

(((canFS (the_Vertices_of G)) | (Seg c)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

b is Relation-like NAT -defined Function-like total set

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

b . c is set

Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT

(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]

[:NAT,(the_Vertices_of G):] is non empty non trivial Relation-like non finite set

bool [:NAT,(the_Vertices_of G):] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

((canFS (the_Vertices_of G)) | (Seg c)) " is Relation-like Function-like set

(((canFS (the_Vertices_of G)) | (Seg c)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

Seg va is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite va -element Element of bool NAT

(canFS (the_Vertices_of G)) | (Seg va) is Relation-like NAT -defined Seg va -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]

((canFS (the_Vertices_of G)) | (Seg va)) " is Relation-like Function-like set

(((canFS (the_Vertices_of G)) | (Seg va)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

len (canFS (the_Vertices_of G)) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(canFS (the_Vertices_of G)) " is Relation-like Function-like one-to-one set

((canFS (the_Vertices_of G)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

dom (canFS (the_Vertices_of G)) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT

Seg (len (canFS (the_Vertices_of G))) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite len (canFS (the_Vertices_of G)) -element Element of bool NAT

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

b . c is set

Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT

(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]

[:NAT,(the_Vertices_of G):] is non empty non trivial Relation-like non finite set

bool [:NAT,(the_Vertices_of G):] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT

(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]

[:NAT,(the_Vertices_of G):] is non empty non trivial Relation-like non finite set

bool [:NAT,(the_Vertices_of G):] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

((canFS (the_Vertices_of G)) | (Seg c)) " is Relation-like Function-like set

(((canFS (the_Vertices_of G)) | (Seg c)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

vb is set

rng ((((canFS (the_Vertices_of G)) | (Seg c)) ") * a) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool RAT

bool RAT is non empty cup-closed diff-closed preBoolean set

rng a is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool NAT

((canFS (the_Vertices_of G)) | (Seg c)) ~ is Relation-like the_Vertices_of G -defined NAT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]

[:(the_Vertices_of G),NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set

bool [:(the_Vertices_of G),NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean V225() set

vb is set

proj1 ((((canFS (the_Vertices_of G)) | (Seg c)) ") * a) is set

proj1 (((canFS (the_Vertices_of G)) | (Seg c)) ") is set

rng ((canFS (the_Vertices_of G)) | (Seg c)) is finite Element of bool (the_Vertices_of G)

bool (the_Vertices_of G) is non empty finite finite-membered cup-closed diff-closed preBoolean V225() set

b . c is set

dom a is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() Element of bool NAT

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

b . c is set

card (b . c) is epsilon-transitive epsilon-connected ordinal cardinal set

Seg c is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite c -element Element of bool NAT

Seg (len (canFS (the_Vertices_of G))) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite len (canFS (the_Vertices_of G)) -element Element of bool NAT

(canFS (the_Vertices_of G)) | (Seg c) is Relation-like NAT -defined Seg c -defined NAT -defined the_Vertices_of G -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,(the_Vertices_of G):]

((canFS (the_Vertices_of G)) | (Seg c)) " is Relation-like Function-like set

(((canFS (the_Vertices_of G)) | (Seg c)) ") * a is Relation-like NAT -valued RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set

card (Seg c) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

dom (canFS (the_Vertices_of G)) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT

dom ((canFS (the_Vertices_of G)) | (Seg c)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() finite Element of bool NAT

proj2 (((canFS (the_Vertices_of G)) | (Seg c)) ") is set

proj1 ((((canFS (the_Vertices_of G)) | (Seg c)) ") * a) is set

proj1 (((canFS (the_Vertices_of G)) | (Seg c)) ") is set

rng ((canFS (the_Vertices_of G)) | (Seg c)) is finite Element of bool (the_Vertices_of G)

card (proj1 ((((canFS (the_Vertices_of G)) | (Seg c)) ") * a)) is epsilon-transitive epsilon-connected ordinal cardinal set

c is Relation-like NAT -defined Function-like total (G)

vb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

(G,c,va) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]

(G,c,vb) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]

va + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(G,c,(va + 1)) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]

vb + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

(G,c,(vb + 1)) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]

card (G,c,vb) is epsilon-transitive epsilon-connected ordinal cardinal set

proj2 ((canFS (the_Vertices_of G)) ") is set

vc is set

(canFS (the_Vertices_of G)) ~ is Relation-like Function-like set

proj2 ((canFS (the_Vertices_of G)) ~) is set

dom (canFS (the_Vertices_of G)) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT

card (G,c,vb) is epsilon-transitive epsilon-connected ordinal cardinal set

dom (G,c,vb) is finite Element of bool (the_Vertices_of G)

card (dom (G,c,vb)) is ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

proj1 ((canFS (the_Vertices_of G)) ") is set

card (proj1 ((canFS (the_Vertices_of G)) ")) is epsilon-transitive epsilon-connected ordinal cardinal set

rng (canFS (the_Vertices_of G)) is non empty finite Element of bool (the_Vertices_of G)

card (rng (canFS (the_Vertices_of G))) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

dom (canFS (the_Vertices_of G)) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() finite Element of bool NAT

card (dom (canFS (the_Vertices_of G))) is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

va is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

c . va is set

vb is ext-real non negative epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() set

c . vb is set

va + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

c . (va + 1) is set

vb + 1 is non empty ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V31() V32() V33() V34() V35() epsilon-transitive epsilon-connected ordinal natural finite cardinal V55() real V57() V59() Element of NAT

c . (vb + 1) is set

(G,c,va) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]

(G,c,vb) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]

(G,c,(va + 1)) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(the_Vertices_of G),NAT:]

(G,c,(vb + 1)) is Relation-like the_Vertices_of G -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued Element of bool