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