:: MSSCYC_1 semantic presentation

REAL is set

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal Element of bool REAL

bool REAL is set

NAT is V6() V7() V8() non empty non trivial non finite cardinal limit_cardinal set

bool NAT is non trivial non finite set

bool NAT is non trivial non finite set

{} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() set

1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

{{},1} is non empty finite V28() set

Trees is non empty constituted-Trees set

bool Trees is set

FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees

PeanoNat is non empty strict L13()

the carrier of PeanoNat is non empty set

FinTrees the carrier of PeanoNat is functional non empty constituted-DTrees DTree-set of the carrier of PeanoNat

TS PeanoNat is functional constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)

bool (FinTrees the carrier of PeanoNat) is set

[:(TS PeanoNat),NAT:] is Relation-like set

bool [:(TS PeanoNat),NAT:] is set

[:NAT,(TS PeanoNat):] is Relation-like set

bool [:NAT,(TS PeanoNat):] is set

COMPLEX is set

RAT is set

INT is set

2 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

3 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() Element of NAT

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

product {} is set

{{}} is functional non empty trivial finite V28() 1 -element Tree-like finite-order set

elementary_tree 0 is non empty finite Tree-like finite-order set

height (elementary_tree 0) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

S is non empty V54() MultiGraphStruct

the carrier' of S is set

the carrier of S is non empty set

X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set

dom v is finite Element of bool NAT

v . vk is set

vk is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

o is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

o /. t is Element of the carrier of S

t + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

o /. (t + 1) is Element of the carrier of S

X . t is set

o . (t + 1) is set

o . t is set

a is Element of the carrier of S

k is Element of the carrier of S

v is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

dom X is finite Element of bool NAT

X . vk is set

proj2 X is finite set

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

dom v is finite Element of bool NAT

v . vk is set

proj2 v is finite set

vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

v . vk is set

vk + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

v . (vk + 1) is set

X . vk is set

v /. vk is Element of the carrier of S

o is Element of the carrier of S

v /. (vk + 1) is Element of the carrier of S

t is Element of the carrier of S

S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(1,S) -cut X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

X ^ v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(1,S) -cut (X ^ v) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len ((1,S) -cut X) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len ((1,S) -cut X)) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

len (X ^ v) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len X) + (len v) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len ((1,S) -cut (X ^ v)) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len ((1,S) -cut (X ^ v))) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set

dom X is finite Element of bool NAT

0 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

((1,S) -cut X) . t is set

X . t is set

(X ^ v) . t is set

((1,S) -cut (X ^ v)) . t is set

a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S is non empty V54() MultiGraphStruct

S is non empty V54() MultiGraphStruct

{1} is non empty trivial finite V28() 1 -element set

[:{},{1}:] is Relation-like finite set

bool [:{},{1}:] is finite V28() set

the Relation-like non-empty empty-yielding {} -defined {1} -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V36( {} ,{1}) constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() Element of bool [:{},{1}:] is Relation-like non-empty empty-yielding {} -defined {1} -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V36( {} ,{1}) constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() Element of bool [:{},{1}:]

MultiGraphStruct(# {1},{}, the Relation-like non-empty empty-yielding {} -defined {1} -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V36( {} ,{1}) constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() Element of bool [:{},{1}:], the Relation-like non-empty empty-yielding {} -defined {1} -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V36( {} ,{1}) constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() Element of bool [:{},{1}:] #) is strict MultiGraphStruct

vk is non empty V54() MultiGraphStruct

the carrier' of vk is set

S is non empty V54() MultiGraphStruct

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is set

the carrier of S is non empty set

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

proj2 the Source of S is set

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

proj2 the Target of S is set

(proj2 the Source of S) \/ (proj2 the Target of S) is set

{1,2} is non empty finite V28() set

{1} is non empty trivial finite V28() 1 -element set

[:{1},{1,2}:] is Relation-like finite set

bool [:{1},{1,2}:] is finite V28() set

{1} --> 1 is Relation-like {1} -defined NAT -valued Function-like finite V36({1}, NAT ) Element of bool [:{1},NAT:]

[:{1},NAT:] is Relation-like non trivial non finite set

bool [:{1},NAT:] is non trivial non finite set

{1} --> 2 is Relation-like {1} -defined NAT -valued Function-like finite V36({1}, NAT ) Element of bool [:{1},NAT:]

v is Relation-like {1} -defined {1,2} -valued Function-like finite V36({1},{1,2}) Element of bool [:{1},{1,2}:]

vk is Relation-like {1} -defined {1,2} -valued Function-like finite V36({1},{1,2}) Element of bool [:{1},{1,2}:]

MultiGraphStruct(# {1,2},{1},v,vk #) is strict MultiGraphStruct

o is non empty V54() MultiGraphStruct

v . 1 is set

the carrier' of o is set

the Source of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like V36( the carrier' of o, the carrier of o) Element of bool [: the carrier' of o, the carrier of o:]

the carrier of o is non empty set

[: the carrier' of o, the carrier of o:] is Relation-like set

bool [: the carrier' of o, the carrier of o:] is set

the Target of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like V36( the carrier' of o, the carrier of o) Element of bool [: the carrier' of o, the carrier of o:]

t is set

the Source of o . t is set

the Target of o . t is set

vk . 1 is set

the carrier of o is non empty set

the carrier' of o is set

the Source of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like V36( the carrier' of o, the carrier of o) Element of bool [: the carrier' of o, the carrier of o:]

[: the carrier' of o, the carrier of o:] is Relation-like set

bool [: the carrier' of o, the carrier of o:] is set

the Target of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like V36( the carrier' of o, the carrier of o) Element of bool [: the carrier' of o, the carrier of o:]

MultiGraphStruct(# the carrier of o, the carrier' of o, the Source of o, the Target of o #) is strict MultiGraphStruct

a is non empty V54() MultiGraphStruct

the carrier of a is non empty set

k is non empty V54() MultiGraphStruct

the carrier of k is non empty set

a \/ k is non empty V54() strict MultiGraphStruct

the Target of a is Relation-like the carrier' of a -defined the carrier of a -valued Function-like V36( the carrier' of a, the carrier of a) Element of bool [: the carrier' of a, the carrier of a:]

the carrier' of a is set

[: the carrier' of a, the carrier of a:] is Relation-like set

bool [: the carrier' of a, the carrier of a:] is set

the Target of k is Relation-like the carrier' of k -defined the carrier of k -valued Function-like V36( the carrier' of k, the carrier of k) Element of bool [: the carrier' of k, the carrier of k:]

the carrier' of k is set

[: the carrier' of k, the carrier of k:] is Relation-like set

bool [: the carrier' of k, the carrier of k:] is set

the Source of a is Relation-like the carrier' of a -defined the carrier of a -valued Function-like V36( the carrier' of a, the carrier of a) Element of bool [: the carrier' of a, the carrier of a:]

the Source of k is Relation-like the carrier' of k -defined the carrier of k -valued Function-like V36( the carrier' of k, the carrier of k) Element of bool [: the carrier' of k, the carrier of k:]

proj2 the Source of a is set

proj2 the Target of a is set

(proj2 the Source of a) \/ (proj2 the Target of a) is set

proj2 the Source of k is set

proj2 the Target of k is set

(proj2 the Source of k) \/ (proj2 the Target of k) is set

the carrier of MultiGraphStruct(# the carrier of o, the carrier' of o, the Source of o, the Target of o #) is set

the carrier of a \/ the carrier of k is non empty set

the carrier' of MultiGraphStruct(# the carrier of o, the carrier' of o, the Source of o, the Target of o #) is set

the carrier' of a \/ the carrier' of k is set

the Source of k . 1 is set

the Source of a . 1 is set

the Target of a . 1 is set

the Source of a . 1 is set

the Target of k . 1 is set

the Source of k . 1 is set

S is non empty V54() MultiGraphStruct

the carrier of S is non empty set

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is set

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

X is set

the Source of S . X is set

the Target of S . X is set

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

v is Element of the carrier of S

vk is Element of the carrier of S

<*v,vk*> is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)

1 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

<*v,vk*> /. (1 + 1) is Element of the carrier of S

len <*X*> is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

len <*v,vk*> is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len <*X*>) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

<*v,vk*> /. a is Element of the carrier of S

a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

<*v,vk*> /. (a + 1) is Element of the carrier of S

<*X*> . a is set

<*X*> . 1 is set

<*v,vk*> /. 1 is Element of the carrier of S

S is non empty V54() MultiGraphStruct

the carrier' of S is set

X is set

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

the carrier of S is non empty set

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

the Source of S . X is set

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the Target of S . X is set

o is non empty set

v is Element of the carrier of S

vk is Element of the carrier of S

<*v,vk*> is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)

t is Element of o

<*t*> is Relation-like NAT -defined o -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of o *

o * is functional non empty FinSequence-membered M8(o)

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of S

k is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

k + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

a . (k + 1) is set

the Source of S . (a . (k + 1)) is set

a . k is set

the Target of S . (a . k) is set

S is non empty non void V54() MultiGraphStruct

the carrier' of S is non empty set

the Element of the carrier' of S is Element of the carrier' of S

<* the Element of the carrier' of S*> is Relation-like NAT -defined the carrier' of S -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of the carrier' of S *

the carrier' of S * is functional non empty FinSequence-membered M8( the carrier' of S)

v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

v . vk is set

v . o is set

S is non empty V54() MultiGraphStruct

the carrier of S is non empty set

X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of S

v is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

v . 1 is set

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

v . (len v) is set

vk is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

vk . 1 is set

len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

vk . (len vk) is set

card the carrier of S is V6() V7() V8() non empty cardinal set

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

card the carrier of S is V6() V7() V8() non empty cardinal set

len X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is set

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

proj2 v is finite set

X . 1 is set

the Source of S . (X . 1) is set

the Target of S . (X . 1) is set

{( the Source of S . (X . 1)),( the Target of S . (X . 1))} is non empty finite set

dom v is finite Element of bool NAT

proj2 vk is finite set

dom vk is finite Element of bool NAT

card the carrier of S is V6() V7() V8() non empty cardinal set

S is non empty V54() MultiGraphStruct

the carrier of S is non empty set

X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of S

v is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

v . 1 is set

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

v . (len v) is set

S is non empty V54() MultiGraphStruct

the carrier' of S is set

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier of S is non empty set

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

X is set

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

the Source of S . X is set

the Target of S . X is set

<*( the Source of S . X),( the Target of S . X)*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set

v is Element of the carrier of S

vk is Element of the carrier of S

<*v,vk*> is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)

t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

vertex-seq t is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

len t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

o is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len t) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

o /. a is Element of the carrier of S

a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

o /. (a + 1) is Element of the carrier of S

t . a is set

o /. 2 is Element of the carrier of S

o /. 1 is Element of the carrier of S

t . 1 is set

o . 1 is set

the Source of S . (t . 1) is set

S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(S,X) -cut v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len ((S,X) -cut v) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len ((S,X) -cut v)) + S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

X + ((len ((S,X) -cut v)) + S) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(X + 1) + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

1 + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

X + (1 + (len v)) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

((len ((S,X) -cut v)) + S) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S + (1 + (len v)) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len ((S,X) -cut v)) + (S + 1) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(S + 1) + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

v is non empty non void V54() MultiGraphStruct

vk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of v

len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(S,X) -cut vk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of v

len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len o) + S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

0 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S + a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

S + (a + 1) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(S + a) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

t + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

o . (t + 1) is set

S + t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

vk . (S + t) is set

o . (a + 1) is set

vk . (S + a) is set

the Source of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like V36( the carrier' of v, the carrier of v) Element of bool [: the carrier' of v, the carrier of v:]

the carrier' of v is non empty set

the carrier of v is non empty set

[: the carrier' of v, the carrier of v:] is Relation-like set

bool [: the carrier' of v, the carrier of v:] is set

the Source of v . (o . (t + 1)) is set

the Target of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like V36( the carrier' of v, the carrier of v) Element of bool [: the carrier' of v, the carrier of v:]

o . t is set

the Target of v . (o . t) is set

S is non empty non void V54() MultiGraphStruct

X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

the carrier of S is non empty set

len (vertex-seq X) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S is non empty non void V54() MultiGraphStruct

X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

the carrier of S is non empty set

len (vertex-seq X) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S is non empty non void V54() MultiGraphStruct

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

the carrier of S is non empty set

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(vertex-seq X) . t is set

X . t is set

the Source of S . (X . t) is set

t + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . (t + 1) is set

the Target of S . (X . t) is set

X . (t + 1) is set

the Source of S . (X . (t + 1)) is set

(t + 1) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . ((t + 1) + 1) is set

the Target of S . (X . (t + 1)) is set

(vertex-seq X) /. 1 is Element of the carrier of S

1 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) /. (1 + 1) is Element of the carrier of S

dom (vertex-seq X) is non empty finite Element of bool NAT

(vertex-seq X) . 1 is set

len (vertex-seq X) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . (1 + 1) is set

X . 1 is set

(vertex-seq X) /. (t + 1) is Element of the carrier of S

(vertex-seq X) /. ((t + 1) + 1) is Element of the carrier of S

len (vertex-seq X) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

dom (vertex-seq X) is non empty finite Element of bool NAT

(vertex-seq X) . 0 is set

X . 0 is set

the Source of S . (X . 0) is set

0 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . (0 + 1) is set

the Target of S . (X . 0) is set

S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

v is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

len v is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(S,X) -cut v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len ((S,X) -cut v) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len ((S,X) -cut v)) + S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(X + 1) - (X + 1) is V139() V140() ext-real V144() set

S - ((len ((S,X) -cut v)) + S) is V139() V140() ext-real V144() set

- (len ((S,X) -cut v)) is V139() V140() ext-real non positive V144() set

- (- (len ((S,X) -cut v))) is V139() V140() ext-real non negative V144() set

S is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

v is non empty non void V54() MultiGraphStruct

the carrier of v is non empty set

vk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of v

len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of v

(S,X) -cut vk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

vertex-seq o is Relation-like NAT -defined the carrier of v -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of v

vertex-seq vk is Relation-like NAT -defined the carrier of v -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of v

(S,(X + 1)) -cut (vertex-seq vk) is Relation-like NAT -defined the carrier of v -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of v

len (vertex-seq vk) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

0 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

o . (0 + 1) is set

S + 0 is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

vk . (S + 0) is set

len ((S,(X + 1)) -cut (vertex-seq vk)) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(vertex-seq vk) . (S + 0) is set

((S,(X + 1)) -cut (vertex-seq vk)) . (0 + 1) is set

((S,(X + 1)) -cut (vertex-seq vk)) . 1 is set

the Source of v is Relation-like the carrier' of v -defined the carrier of v -valued Function-like V36( the carrier' of v, the carrier of v) Element of bool [: the carrier' of v, the carrier of v:]

the carrier' of v is non empty set

[: the carrier' of v, the carrier of v:] is Relation-like set

bool [: the carrier' of v, the carrier of v:] is set

o . 1 is set

the Source of v . (o . 1) is set

S is non empty non void V54() MultiGraphStruct

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

the carrier of S is non empty set

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . ((len X) + 1) is set

X . (len X) is set

the Target of S . (X . (len X)) is set

dom X is non empty finite Element of bool NAT

S is non empty non void V54() MultiGraphStruct

X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

the carrier of S is non empty set

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . ((len X) + 1) is set

v is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

vertex-seq v is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

(vertex-seq v) . 1 is set

X ^ v is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

len (X ^ v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

len v is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

len (vertex-seq X) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of S

a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

a + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

t . (a + 1) is set

the Source of S . (t . (a + 1)) is set

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

t . a is set

the Target of S . (t . a) is set

dom X is non empty finite Element of bool NAT

X . (a + 1) is set

X . a is set

dom X is non empty finite Element of bool NAT

X . a is set

dom v is non empty finite Element of bool NAT

v . 1 is set

X . (len X) is set

the Target of S . (X . (len X)) is set

a - (len X) is V139() V140() ext-real V144() set

k is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len X) + k is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

k + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + (k + 1) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

dom v is non empty finite Element of bool NAT

v . (k + 1) is set

v . k is set

a is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

len a is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

dom X is non empty finite Element of bool NAT

a . (len X) is set

X . (len X) is set

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

a . ((len X) + 1) is set

the Source of S . (a . ((len X) + 1)) is set

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the Target of S . (a . (len X)) is set

dom v is non empty finite Element of bool NAT

v . 1 is set

the Target of S . (X . (len X)) is set

S is non empty non void V54() MultiGraphStruct

X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

v is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

vk is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

v ^ vk is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

the carrier of S is non empty set

(vertex-seq X) . 1 is set

vertex-seq v is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

(vertex-seq v) . 1 is set

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . ((len X) + 1) is set

vertex-seq vk is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

len vk is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq vk) . ((len vk) + 1) is set

dom X is non empty finite Element of bool NAT

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

X . 1 is set

the Source of S . (X . 1) is set

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

X . (len X) is set

the Target of S . (X . (len X)) is set

dom v is non empty finite Element of bool NAT

len v is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

v . 1 is set

the Source of S . (v . 1) is set

dom vk is non empty finite Element of bool NAT

vk . (len vk) is set

the Target of S . (vk . (len vk)) is set

(len v) + (len vk) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S is non empty non void V54() MultiGraphStruct

X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

the carrier of S is non empty set

(vertex-seq X) . 1 is set

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . ((len X) + 1) is set

len (vertex-seq X) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

S is non empty non void V54() MultiGraphStruct

X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of S

proj2 X is non empty finite set

the carrier' of S is non empty set

len X is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

dom X is non empty finite Element of bool NAT

X . (len X) is set

v is Element of the carrier' of S

<*v*> is Relation-like NAT -defined the carrier' of S -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of the carrier' of S *

the carrier' of S * is functional non empty FinSequence-membered M8( the carrier' of S)

vk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

proj2 vk is finite set

{(X . (len X))} is non empty trivial finite 1 -element set

len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

o + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

proj2 t is finite set

len t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

t ^ X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

vk ^ X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

vertex-seq vk is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

the carrier of S is non empty set

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

the Source of S . v is Element of the carrier of S

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the Target of S . v is Element of the carrier of S

<*( the Source of S . v),( the Target of S . v)*> is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)

(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq vk) . ((len vk) + 1) is set

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . ((len X) + 1) is set

(vertex-seq X) . 1 is set

dom t is finite Element of bool NAT

t . 1 is set

a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set

X . a is set

vertex-seq vk is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

the carrier of S is non empty set

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

the Source of S . v is Element of the carrier of S

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the Target of S . v is Element of the carrier of S

<*( the Source of S . v),( the Target of S . v)*> is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)

(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq vk) . ((len vk) + 1) is set

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

(len X) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq X) . ((len X) + 1) is set

(vertex-seq X) . 1 is set

the Source of S . (t . 1) is set

vertex-seq t is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

(vertex-seq t) . 1 is set

vk ^ t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

ak is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

a9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

proj2 a9 is finite set

(proj2 vk) \/ (proj2 t) is finite set

len a9 is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

vertex-seq a9 is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

(len a9) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq a9) . ((len a9) + 1) is set

(len t) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq t) . ((len t) + 1) is set

a9 ^ X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

1 + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

k is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

k + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

X . k is set

ak is Element of the carrier' of S

<*ak*> is Relation-like NAT -defined the carrier' of S -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of the carrier' of S *

a9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

vertex-seq a9 is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

the carrier of S is non empty set

len a9 is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

the Source of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

[: the carrier' of S, the carrier of S:] is Relation-like set

bool [: the carrier' of S, the carrier of S:] is set

the Source of S . ak is Element of the carrier of S

the Target of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V36( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the Target of S . ak is Element of the carrier of S

<*( the Source of S . ak),( the Target of S . ak)*> is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of S *

the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)

(len a9) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq a9) . ((len a9) + 1) is set

the Source of S . (t . 1) is set

vertex-seq t is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

(vertex-seq t) . 1 is set

a9 ^ t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

dtk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

proj2 a9 is finite set

{(X . k)} is non empty trivial finite 1 -element set

ttk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

proj2 ttk is finite set

(proj2 a9) \/ (proj2 t) is finite set

len ttk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

vertex-seq ttk is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

(len ttk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq ttk) . ((len ttk) + 1) is set

(len t) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq t) . ((len t) + 1) is set

vertex-seq X is Relation-like NAT -defined the carrier of S -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

(vertex-seq X) . 1 is set

ttk ^ X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

proj2 k is finite set

len k is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

k ^ X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

vk is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding oriented cyclic V139() V140() ext-real non positive non negative V144() Chain of S

o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

proj2 o is finite set

len o is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

o ^ X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

vk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

proj2 vk is finite set

len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

vk ^ X is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

S is non empty V54() MultiGraphStruct

X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

the carrier' of S is set

S is non empty void V54() trivial' () MultiGraphStruct

X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Chain of S

the carrier' of S is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty trivial finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() set

S is non empty V54() MultiGraphStruct

the carrier of S is non empty set

v is Element of the carrier of S

vk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of S

vertex-seq vk is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of S

len vk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len vk) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq vk) . ((len vk) + 1) is set

X is non empty void V54() trivial' () MultiGraphStruct

o is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding oriented cyclic V139() V140() ext-real non positive non negative V144() Chain of X

S is non empty V54() MultiGraphStruct

the non empty void V54() trivial' () () MultiGraphStruct is non empty void V54() trivial' () () MultiGraphStruct

S is non empty V54() MultiGraphStruct

X is non empty void V54() trivial' () () MultiGraphStruct

X is non empty non void V54() MultiGraphStruct

v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of X

vertex-seq v is Relation-like NAT -defined the carrier of X -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X

the carrier of X is non empty set

len (vertex-seq v) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

len v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

(len v) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

dom (vertex-seq v) is finite Element of bool NAT

the carrier of S is non empty set

(vertex-seq v) . 1 is set

o is Element of the carrier of S

t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

t + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of X

len a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

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

k is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of X

k ^ v is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

(vertex-seq v) . ((len v) + 1) is set

ak is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like oriented Chain of X

vertex-seq ak is Relation-like NAT -defined the carrier of X -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of X

len ak is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(len ak) + 1 is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

(vertex-seq ak) . ((len ak) + 1) is set

(t + 1) + (len v) is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

{1} is non empty trivial finite V28() 1 -element set

[:{1},{1}:] is Relation-like finite set

bool [:{1},{1}:] is finite V28() set

v is finite Element of {1}

{1} --> v is Relation-like {1} -defined {1} -valued Function-like finite V36({1},{1}) Element of bool [:{1},{1}:]

vk is Relation-like {1} -defined {1} -valued Function-like finite V36({1},{1}) Element of bool [:{1},{1}:]

o is Relation-like {1} -defined {1} -valued Function-like finite V36({1},{1}) Element of bool [:{1},{1}:]

MultiGraphStruct(# {1},{1},vk,o #) is strict MultiGraphStruct

t is non empty V54() MultiGraphStruct

the carrier of t is non empty set

vk . 1 is set

<*1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like Element of NAT *

NAT * is functional non empty FinSequence-membered M8( NAT )

k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of t

a is Element of the carrier of t

<*a,a*> is Relation-like NAT -defined the carrier of t -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like Element of the carrier of t *

the carrier of t * is functional non empty FinSequence-membered M8( the carrier of t)

<*a,a*> . 2 is set

len <*a,a*> is V6() V7() V8() V12() non empty finite cardinal V139() V140() ext-real positive non negative V144() Element of NAT

<*a,a*> . 1 is set

k is non empty V54() () () MultiGraphStruct

the non empty V54() () () MultiGraphStruct is non empty V54() () () MultiGraphStruct

S is Relation-like Function-like DecoratedTree-like set

proj1 S is non empty Tree-like set

X is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 S

v is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT

X | v is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

Seg v is finite v -element Element of bool NAT

X | (Seg v) is Relation-like NAT -defined Seg v -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]

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

bool [:NAT,NAT:] is non trivial non finite set

S is non empty non void V54() ManySortedSign

the carrier of S is non empty set

the carrier' of S is non empty set

X is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()

{ the carrier of S} is non empty trivial finite 1 -element set

[: the carrier' of S,{ the carrier of S}:] is Relation-like set

coprod X is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set

Union (coprod X) is non empty set

[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set

REL X is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]

([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is functional non empty FinSequence-membered M8([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))

[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is Relation-like set

bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is set

G13(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X)) is strict L13()

the carrier of (DTConMSA X) is non empty set

FinTrees the carrier of (DTConMSA X) is functional non empty constituted-DTrees DTree-set of the carrier of (DTConMSA X)

S -Terms X is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

bool (FinTrees the carrier of (DTConMSA X)) is set

v is Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like Element of S -Terms X

v . {} is set

vk is Element of the carrier of S

X . vk is non empty set

o is Element of X . vk

[o,vk] is V21() set

{o,vk} is non empty finite set

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

{{o,vk},{o}} is non empty finite V28() set

vk is Element of the carrier of S

X . vk is non empty set

o is Element of X . vk

[o,vk] is V21() set

{o,vk} is non empty finite set

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

{{o,vk},{o}} is non empty finite V28() set

root-tree [o,vk] is Relation-like Function-like constant trivial finite DecoratedTree-like set

vk is set

o is set

[vk,o] is V21() set

{vk,o} is non empty