:: 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 finite set
{vk} is non empty trivial finite 1 -element set
{{vk,o},{vk}} is non empty finite V28() set
t is Element of the carrier' of S
[t, the carrier of S] is V21() set
{t, the carrier of S} is non empty finite set
{t} is non empty trivial finite 1 -element set
{{t, the carrier of S},{t}} is non empty finite V28() set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
X is MSAlgebra over S
the Sorts of X is Relation-like the carrier of S -defined Function-like non empty total set
v is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of X
vk is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of X
GenMSAlg vk is strict MSSubAlgebra of X
the Sorts of (GenMSAlg vk) is Relation-like the carrier of S -defined Function-like non empty total set
GenMSAlg v is strict MSSubAlgebra of X
the Sorts of (GenMSAlg v) is Relation-like the carrier of S -defined Function-like non empty total set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
X is non-empty finitely-generated MSAlgebra over S
v is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of X
the Sorts of X is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
vk is Relation-like the carrier of S -defined Function-like non empty total set
o is Relation-like the carrier of S -defined Function-like non empty total set
v \/ o is Relation-like the carrier of S -defined Function-like non empty total set
a is set
vk . a is set
the Sorts of X . a is set
{(vk . a)} is non empty trivial finite 1 -element set
o . a is set
a is set
o . a is set
vk . a is set
{(vk . a)} is non empty trivial finite 1 -element set
a is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of X
k is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of X
ak is set
k . ak is set
o . ak is set
vk . ak is set
{(vk . ak)} is non empty trivial finite 1 -element set
v . ak is set
(v . ak) \/ (o . ak) is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
X is non-empty MSAlgebra over S
the Sorts of X is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
v is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total GeneratorSet of X
FreeMSA v is strict non-empty MSAlgebra over S
FreeSort v is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
FreeOper v is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of S * ((FreeSort v) #), the ResultSort of S * (FreeSort v)
the carrier' of S is non empty set
the Arity 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 functional non empty FinSequence-membered M8( 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
(FreeSort v) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((FreeSort v) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort 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 ResultSort of S * (FreeSort v) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (FreeSort v),(FreeOper v) #) is strict MSAlgebra over S
the Sorts of (FreeMSA v) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
o is set
Reverse v is Relation-like the carrier of S -defined Function-like non empty total Function-yielding ManySortedFunction of FreeGen v,v
FreeGen v is Relation-like the carrier of S -defined Function-like non empty total GeneratorSet of FreeMSA v
(Reverse v) . o is set
(FreeGen v) . o is set
v . o is set
[:((FreeGen v) . o),(v . o):] is Relation-like set
bool [:((FreeGen v) . o),(v . o):] is set
the Sorts of X . o is set
[:((FreeGen v) . o),( the Sorts of X . o):] is Relation-like set
bool [:((FreeGen v) . o),( the Sorts of X . o):] is set
o is Relation-like the carrier of S -defined Function-like non empty total Function-yielding ManySortedFunction of FreeGen v, the Sorts of X
t is Relation-like the carrier of S -defined Function-like non empty total Function-yielding ManySortedFunction of the Sorts of (FreeMSA v), the Sorts of X
t || (FreeGen v) is Relation-like the carrier of S -defined Function-like non empty total Function-yielding ManySortedFunction of FreeGen v, the Sorts of X
a is set
t . a is set
proj2 (t . a) is set
the Sorts of X . a is set
k is Element of the carrier of S
t . k is Relation-like the Sorts of (FreeMSA v) . k -defined the Sorts of X . k -valued Function-like V36( the Sorts of (FreeMSA v) . k, the Sorts of X . k) Element of bool [:( the Sorts of (FreeMSA v) . k),( the Sorts of X . k):]
the Sorts of (FreeMSA v) . k is non empty set
the Sorts of X . k is non empty set
[:( the Sorts of (FreeMSA v) . k),( the Sorts of X . k):] is Relation-like set
bool [:( the Sorts of (FreeMSA v) . k),( the Sorts of X . k):] is set
Image t is strict non-empty MSSubAlgebra of X
the Sorts of (Image t) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
a9 is Relation-like the carrier of S -defined Function-like non empty total Function-yielding ManySortedFunction of the Sorts of (FreeMSA v), the Sorts of (Image t)
Image a9 is strict non-empty MSSubAlgebra of Image t
da is set
v . da is set
the Sorts of (Image t) . da is set
dtk is Element of the carrier of S
proj1 (Reverse v) is non empty set
rngs (Reverse v) is Relation-like Function-like set
(rngs (Reverse v)) . dtk is set
(Reverse v) . dtk is Relation-like (FreeGen v) . dtk -defined v . dtk -valued Function-like V36((FreeGen v) . dtk,v . dtk) Element of bool [:((FreeGen v) . dtk),(v . dtk):]
(FreeGen v) . dtk is set
v . dtk is non empty set
[:((FreeGen v) . dtk),(v . dtk):] is Relation-like set
bool [:((FreeGen v) . dtk),(v . dtk):] is set
proj2 ((Reverse v) . dtk) is set
the Sorts of (FreeMSA v) . dtk is non empty set
the Sorts of X . dtk is non empty set
[:( the Sorts of (FreeMSA v) . dtk),( the Sorts of X . dtk):] is Relation-like set
bool [:( the Sorts of (FreeMSA v) . dtk),( the Sorts of X . dtk):] is set
t . dtk is Relation-like the Sorts of (FreeMSA v) . dtk -defined the Sorts of X . dtk -valued Function-like V36( the Sorts of (FreeMSA v) . dtk, the Sorts of X . dtk) Element of bool [:( the Sorts of (FreeMSA v) . dtk),( the Sorts of X . dtk):]
t is set
t .:.: the Sorts of (FreeMSA v) is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of (Image t) . dtk is non empty set
ttk is Relation-like the Sorts of (FreeMSA v) . dtk -defined the Sorts of X . dtk -valued Function-like V36( the Sorts of (FreeMSA v) . dtk, the Sorts of X . dtk) Element of bool [:( the Sorts of (FreeMSA v) . dtk),( the Sorts of X . dtk):]
ttk .: ( the Sorts of (FreeMSA v) . dtk) is set
o . dtk is Relation-like (FreeGen v) . dtk -defined the Sorts of X . dtk -valued Function-like V36((FreeGen v) . dtk, the Sorts of X . dtk) Element of bool [:((FreeGen v) . dtk),( the Sorts of X . dtk):]
[:((FreeGen v) . dtk),( the Sorts of X . dtk):] is Relation-like set
bool [:((FreeGen v) . dtk),( the Sorts of X . dtk):] is set
proj1 (o . dtk) is set
c is set
(o . dtk) . c is set
ttk | ((FreeGen v) . dtk) is Relation-like (FreeGen v) . dtk -defined the Sorts of (FreeMSA v) . dtk -defined the Sorts of X . dtk -valued Function-like Element of bool [:( the Sorts of (FreeMSA v) . dtk),( the Sorts of X . dtk):]
proj1 ttk is set
(proj1 ttk) /\ ((FreeGen v) . dtk) is set
ttk . c is set
vk is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of the Sorts of X
GenMSAlg vk is strict MSSubAlgebra of X
the Sorts of (GenMSAlg vk) is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of (Image a9) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
t .:.: the Sorts of (FreeMSA v) is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of (Image a9) . a is set
the Sorts of (FreeMSA v) . a is set
(t . k) .: ( the Sorts of (FreeMSA v) . a) is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
X is non-empty MSAlgebra over S
v is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total GeneratorSet of X
FreeMSA v is strict non-empty MSAlgebra over S
FreeSort v is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
FreeOper v is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of S * ((FreeSort v) #), the ResultSort of S * (FreeSort v)
the carrier' of S is non empty set
the Arity 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 functional non empty FinSequence-membered M8( 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
(FreeSort v) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((FreeSort v) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort 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 ResultSort of S * (FreeSort v) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (FreeSort v),(FreeOper v) #) is strict MSAlgebra over S
the Sorts of X is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
vk is set
the Sorts of X . vk is set
the Sorts of (FreeMSA v) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (FreeMSA v) . vk is set
a is Relation-like the carrier of S -defined Function-like non empty total Function-yielding ManySortedFunction of the Sorts of (FreeMSA v), the Sorts of X
o is non empty set
t is non empty set
[:o,t:] is Relation-like set
bool [:o,t:] is set
k is Element of the carrier of S
a . k is Relation-like the Sorts of (FreeMSA v) . k -defined the Sorts of X . k -valued Function-like V36( the Sorts of (FreeMSA v) . k, the Sorts of X . k) Element of bool [:( the Sorts of (FreeMSA v) . k),( the Sorts of X . k):]
the Sorts of (FreeMSA v) . k is non empty set
the Sorts of X . k is non empty set
[:( the Sorts of (FreeMSA v) . k),( the Sorts of X . k):] is Relation-like set
bool [:( the Sorts of (FreeMSA v) . k),( the Sorts of X . k):] is set
ak is Relation-like o -defined t -valued Function-like V36(o,t) Element of bool [:o,t:]
proj2 ak is set
S is non empty non void V54() ManySortedSign
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 finite-yielding total set
v is Element of the carrier of S
FreeGen (v,X) is non empty Element of bool ((FreeSort X) . v)
FreeSort X is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
(FreeSort X) . v is non empty set
bool ((FreeSort X) . v) is set
X . v is non empty finite set
{ [b₁,(root-tree [b₁,v])] where b₁ is Element of X . v : verum } is set
o is set
[o,v] is V21() set
{o,v} is non empty finite set
{o} is non empty trivial finite 1 -element set
{{o,v},{o}} is non empty finite V28() set
root-tree [o,v] is Relation-like Function-like constant trivial finite DecoratedTree-like set
t is set
a is set
[o,a] is V21() set
{o,a} is non empty finite set
{{o,a},{o}} is non empty finite V28() set
o is set
t is set
[t,v] is V21() set
{t,v} is non empty finite set
{t} is non empty trivial finite 1 -element set
{{t,v},{t}} is non empty finite V28() set
root-tree [t,v] is Relation-like Function-like constant trivial finite DecoratedTree-like set
a is set
[a,o] is V21() set
{a,o} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,o},{a}} is non empty finite V28() set
o is set
t is set
[o,t] is V21() set
{o,t} is non empty finite set
{o} is non empty trivial finite 1 -element set
{{o,t},{o}} is non empty finite V28() set
a is set
k is set
[a,k] is V21() set
{a,k} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,k},{a}} is non empty finite V28() set
ak is Element of X . v
[ak,v] is V21() set
{ak,v} is non empty finite set
{ak} is non empty trivial finite 1 -element set
{{ak,v},{ak}} is non empty finite V28() set
root-tree [ak,v] is Relation-like Function-like constant trivial finite DecoratedTree-like set
[ak,(root-tree [ak,v])] is V21() set
{ak,(root-tree [ak,v])} is non empty finite set
{{ak,(root-tree [ak,v])},{ak}} is non empty finite V28() set
a9 is Element of X . v
[a9,v] is V21() set
{a9,v} is non empty finite set
{a9} is non empty trivial finite 1 -element set
{{a9,v},{a9}} is non empty finite V28() set
root-tree [a9,v] is Relation-like Function-like constant trivial finite DecoratedTree-like set
[a9,(root-tree [a9,v])] is V21() set
{a9,(root-tree [a9,v])} is non empty finite set
{{a9,(root-tree [a9,v])},{a9}} is non empty finite V28() set
dom {} 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 bool NAT
proj2 {} 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
[:{},{}:] is Relation-like finite set
bool [:{},{}:] is finite V28() set
X is non empty non void V54() ManySortedSign
the carrier' of X is non empty set
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M8( the carrier of X)
the Arity of X is Relation-like the carrier' of X -defined the carrier of X * -valued Function-like V36( the carrier' of X, the carrier of X * ) Element of bool [: the carrier' of X,( the carrier of X *):]
[: the carrier' of X,( the carrier of X *):] is Relation-like set
bool [: the carrier' of X,( the carrier of X *):] is set
v is non-empty MSAlgebra over X
vk is Element of the carrier' of X
the Arity of X . vk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of X *
Den (vk,v) is Relation-like Args (vk,v) -defined Result (vk,v) -valued Function-like V36( Args (vk,v), Result (vk,v)) Element of bool [:(Args (vk,v)),(Result (vk,v)):]
Args (vk,v) is non empty Element of proj2 ( the Sorts of v #)
the Sorts of v is Relation-like non-empty non empty-yielding the carrier of X -defined Function-like non empty total set
the Sorts of v # is Relation-like the carrier of X * -defined Function-like non empty total set
proj2 ( the Sorts of v #) is non empty set
Result (vk,v) is non empty Element of proj2 the Sorts of v
proj2 the Sorts of v is non empty set
[:(Args (vk,v)),(Result (vk,v)):] is Relation-like set
bool [:(Args (vk,v)),(Result (vk,v)):] is set
proj1 (Den (vk,v)) is set
proj1 the Arity of X is set
proj1 ( the Sorts of v #) is non empty set
the carrier of X * is functional non empty FinSequence-membered set
proj2 the Arity of X is set
the Arity of X * ( the Sorts of v #) is Relation-like the carrier' of X -defined Function-like non empty total set
proj1 ( the Arity of X * ( the Sorts of v #)) is non empty set
( the Arity of X * ( the Sorts of v #)) . vk is set
( the Sorts of v #) . ( the Arity of X . vk) is set
the_arity_of vk is Relation-like NAT -defined the carrier of X -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of X *
( the Sorts of v #) . (the_arity_of vk) is set
(the_arity_of vk) * the Sorts of v is Relation-like non-empty NAT -defined Function-like finite set
product ((the_arity_of vk) * the Sorts of v) is set
S is Relation-like non-empty empty-yielding {} -defined {} -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( {} , {} ) constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() Element of bool [:{},{}:]
S * the Sorts of v is Relation-like non-empty empty-yielding NAT -defined {} -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
product (S * the Sorts of v) is set
S is non empty non void V54() ManySortedSign
the carrier of S is non empty set
X is non-empty MSAlgebra over S
v is Element of the carrier of S
Constants (X,v) is Element of bool ( the Sorts of X . v)
the Sorts of X is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of X . v is non empty set
bool ( the Sorts of X . v) is set
the carrier' of S is non empty set
{ b₁ where b₁ is Element of the carrier' of S : the_result_sort_of b₁ = v } is set
the carrier of S * is functional non empty FinSequence-membered M8( the carrier of S)
the Arity 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 ResultSort 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
o is non empty set
{ b₁ where b₁ is Element of o : ex b₂ being Element of the carrier' of S st
( the Arity of S . b₂ = {} & the ResultSort of S . b₂ = v & b₁ in proj2 (Den (b₂,X)) ) } is set
t is non empty set
{ b₁ where b₁ is Element of t : S₁[b₁] } is set
{ H₁(b₁) where b₁ is Element of the carrier' of S : b₁ in { b₁ where b₂ is Element of t : S₁[b₁] } } is set
ak is set
a9 is Element of o
da is Element of the carrier' of S
the Arity of S . da is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . da is Element of the carrier of S
Den (da,X) is Relation-like Args (da,X) -defined Result (da,X) -valued Function-like V36( Args (da,X), Result (da,X)) Element of bool [:(Args (da,X)),(Result (da,X)):]
Args (da,X) is non empty Element of proj2 ( the Sorts of X #)
the Sorts of X # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of X #) is non empty set
Result (da,X) is non empty Element of proj2 the Sorts of X
proj2 the Sorts of X is non empty set
[:(Args (da,X)),(Result (da,X)):] is Relation-like set
bool [:(Args (da,X)),(Result (da,X)):] is set
proj2 (Den (da,X)) is set
da is Element of the carrier' of S
the Arity of S . da is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . da is Element of the carrier of S
Den (da,X) is Relation-like Args (da,X) -defined Result (da,X) -valued Function-like V36( Args (da,X), Result (da,X)) Element of bool [:(Args (da,X)),(Result (da,X)):]
Args (da,X) is non empty Element of proj2 ( the Sorts of X #)
the Sorts of X # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of X #) is non empty set
Result (da,X) is non empty Element of proj2 the Sorts of X
proj2 the Sorts of X is non empty set
[:(Args (da,X)),(Result (da,X)):] is Relation-like set
bool [:(Args (da,X)),(Result (da,X)):] is set
proj2 (Den (da,X)) is set
the_result_sort_of da is Element of the carrier of S
dtk is Element of t
proj1 (Den (da,X)) is set
t is set
(Den (da,X)) . t is set
bool t is set
t is set
a is Element of o
k is Element of the carrier' of S
the Arity of S . k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . k is Element of the carrier of S
Den (k,X) is Relation-like Args (k,X) -defined Result (k,X) -valued Function-like V36( Args (k,X), Result (k,X)) Element of bool [:(Args (k,X)),(Result (k,X)):]
Args (k,X) is non empty Element of proj2 ( the Sorts of X #)
the Sorts of X # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of X #) is non empty set
Result (k,X) is non empty Element of proj2 the Sorts of X
proj2 the Sorts of X is non empty set
[:(Args (k,X)),(Result (k,X)):] is Relation-like set
bool [:(Args (k,X)),(Result (k,X)):] is set
proj2 (Den (k,X)) is set
k is Element of the carrier' of S
the Arity of S . k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . k is Element of the carrier of S
Den (k,X) is Relation-like Args (k,X) -defined Result (k,X) -valued Function-like V36( Args (k,X), Result (k,X)) Element of bool [:(Args (k,X)),(Result (k,X)):]
Args (k,X) is non empty Element of proj2 ( the Sorts of X #)
the Sorts of X # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of X #) is non empty set
Result (k,X) is non empty Element of proj2 the Sorts of X
proj2 the Sorts of X is non empty set
[:(Args (k,X)),(Result (k,X)):] is Relation-like set
bool [:(Args (k,X)),(Result (k,X)):] is set
proj2 (Den (k,X)) is set
the_result_sort_of k is Element of the carrier of S
S is non empty non void V54() ManySortedSign
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
FreeMSA X is strict non-empty MSAlgebra over S
FreeSort X is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
FreeOper X is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of S * ((FreeSort X) #), the ResultSort of S * (FreeSort X)
the carrier' of S is non empty set
the Arity 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 functional non empty FinSequence-membered M8( 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
(FreeSort X) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((FreeSort X) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort 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 ResultSort of S * (FreeSort X) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (FreeSort X),(FreeOper X) #) is strict MSAlgebra over S
the Sorts of (FreeMSA X) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
v is Element of the carrier of S
the Sorts of (FreeMSA X) . v is non empty set
{ b₁ where b₁ is Relation-like Function-like non empty finite DecoratedTree-like Element of the Sorts of (FreeMSA X) . v : depth b₁ = 0 } is set
FreeGen (v,X) is non empty Element of bool ((FreeSort X) . v)
(FreeSort X) . v is non empty set
bool ((FreeSort X) . v) is set
Constants ((FreeMSA X),v) is Element of bool ( the Sorts of (FreeMSA X) . v)
bool ( the Sorts of (FreeMSA X) . v) is set
(FreeGen (v,X)) \/ (Constants ((FreeMSA X),v)) is non empty set
t is set
a is Relation-like Function-like non empty finite DecoratedTree-like Element of the Sorts of (FreeMSA X) . v
depth a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set
FreeSort (X,v) is functional non empty constituted-DTrees Element of bool (TS (DTConMSA X))
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()
TS (DTConMSA X) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
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)
bool (FinTrees the carrier of (DTConMSA X)) is set
bool (TS (DTConMSA X)) is set
X . v is non empty set
{ b₁ where b₁ is Relation-like the carrier of (DTConMSA X) -valued Function-like Element of TS (DTConMSA X) : ( ex b₂ being set st
( b₂ in X . v & b₁ = root-tree [b₂,v] ) or ex b₂ being Element of the carrier' of S st
( [b₂, the carrier of S] = b₁ . {} & the_result_sort_of b₂ = v ) ) } is set
k is Relation-like Function-like Element of TS (DTConMSA X)
k . {} is set
ak is Relation-like Function-like finite DecoratedTree-like set
a9 is non empty finite Tree-like finite-order set
proj1 ak is non empty finite Tree-like finite-order set
height a9 is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
da is set
[da,v] is V21() set
{da,v} is non empty finite set
{da} is non empty trivial finite 1 -element set
{{da,v},{da}} is non empty finite V28() set
root-tree [da,v] is Relation-like Function-like constant trivial finite DecoratedTree-like set
da is Element of the carrier' of S
[da, the carrier of S] is V21() set
{da, the carrier of S} is non empty finite set
{da} is non empty trivial finite 1 -element set
{{da, the carrier of S},{da}} is non empty finite V28() set
the_result_sort_of da is Element of the carrier of S
da is Element of the carrier' of S
[da, the carrier of S] is V21() set
{da, the carrier of S} is non empty finite set
{da} is non empty trivial finite 1 -element set
{{da, the carrier of S},{da}} is non empty finite V28() set
the_result_sort_of da is Element of the carrier of S
the ResultSort of S . da is Element of the carrier of S
<*> (TS (DTConMSA X)) is Relation-like non-empty empty-yielding NAT -defined TS (DTConMSA X) -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 constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() Element of (TS (DTConMSA X)) *
(TS (DTConMSA X)) * is functional non empty FinSequence-membered M8( TS (DTConMSA X))
S -Terms X is functional non empty constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
Sym (da,X) is Element of K315((DTConMSA X))
K315((DTConMSA X)) is non empty Element of bool the carrier of (DTConMSA X)
bool the carrier of (DTConMSA X) is set
ttk is Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like Element of S -Terms X
t is Relation-like NAT -defined FinTrees the carrier of (DTConMSA X) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (da,X)
[da, the carrier of S] -tree t is Relation-like Function-like DecoratedTree-like set
ak . {} is set
root-tree (ak . {}) is Relation-like Function-like constant trivial finite DecoratedTree-like set
len t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
the_arity_of da is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
len (the_arity_of da) is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
the Arity of S . da is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
Den (da,(FreeMSA X)) is Relation-like Args (da,(FreeMSA X)) -defined Result (da,(FreeMSA X)) -valued Function-like V36( Args (da,(FreeMSA X)), Result (da,(FreeMSA X))) Element of bool [:(Args (da,(FreeMSA X))),(Result (da,(FreeMSA X))):]
Args (da,(FreeMSA X)) is non empty Element of proj2 ( the Sorts of (FreeMSA X) #)
the Sorts of (FreeMSA X) # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of (FreeMSA X) #) is non empty set
Result (da,(FreeMSA X)) is non empty Element of proj2 the Sorts of (FreeMSA X)
proj2 the Sorts of (FreeMSA X) is non empty set
[:(Args (da,(FreeMSA X))),(Result (da,(FreeMSA X))):] is Relation-like set
bool [:(Args (da,(FreeMSA X))),(Result (da,(FreeMSA X))):] is set
proj1 (Den (da,(FreeMSA X))) is set
roots t is Relation-like NAT -defined the carrier of (DTConMSA X) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA X)
DenOp (da,X) is Relation-like ( the Arity of S * ((FreeSort X) #)) . da -defined ( the ResultSort of S * (FreeSort X)) . da -valued Function-like V36(( the Arity of S * ((FreeSort X) #)) . da,( the ResultSort of S * (FreeSort X)) . da) Element of bool [:(( the Arity of S * ((FreeSort X) #)) . da),(( the ResultSort of S * (FreeSort X)) . da):]
( the Arity of S * ((FreeSort X) #)) . da is set
( the ResultSort of S * (FreeSort X)) . da is non empty set
[:(( the Arity of S * ((FreeSort X) #)) . da),(( the ResultSort of S * (FreeSort X)) . da):] is Relation-like set
bool [:(( the Arity of S * ((FreeSort X) #)) . da),(( the ResultSort of S * (FreeSort X)) . da):] is set
(DenOp (da,X)) . (<*> (TS (DTConMSA X))) is set
(FreeOper X) . da is Relation-like ( the Arity of S * ((FreeSort X) #)) . da -defined ( the ResultSort of S * (FreeSort X)) . da -valued Function-like V36(( the Arity of S * ((FreeSort X) #)) . da,( the ResultSort of S * (FreeSort X)) . da) Element of bool [:(( the Arity of S * ((FreeSort X) #)) . da),(( the ResultSort of S * (FreeSort X)) . da):]
proj2 (Den (da,(FreeMSA X))) is set
c is non empty set
{ b₁ where b₁ is Element of c : ex b₂ being Element of the carrier' of S st
( the Arity of S . b₂ = {} & the ResultSort of S . b₂ = v & b₁ in proj2 (Den (b₂,(FreeMSA X))) ) } is set
da is set
[da,v] is V21() set
{da,v} is non empty finite set
{da} is non empty trivial finite 1 -element set
{{da,v},{da}} is non empty finite V28() set
root-tree [da,v] is Relation-like Function-like constant trivial finite DecoratedTree-like set
dtk is Element of the carrier' of S
[dtk, the carrier of S] is V21() set
{dtk, the carrier of S} is non empty finite set
{dtk} is non empty trivial finite 1 -element set
{{dtk, the carrier of S},{dtk}} is non empty finite V28() set
the_result_sort_of dtk is Element of the carrier of S
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()
TS (DTConMSA X) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
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)
bool (FinTrees the carrier of (DTConMSA X)) is set
<*> (TS (DTConMSA X)) is Relation-like non-empty empty-yielding NAT -defined TS (DTConMSA X) -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 constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V139() V140() ext-real non positive non negative V144() Element of (TS (DTConMSA X)) *
(TS (DTConMSA X)) * is functional non empty FinSequence-membered M8( TS (DTConMSA X))
a is set
k is non empty set
{ b₁ where b₁ is Element of k : ex b₂ being Element of the carrier' of S st
( the Arity of S . b₂ = {} & the ResultSort of S . b₂ = v & b₁ in proj2 (Den (b₂,(FreeMSA X))) ) } is set
ak is Element of k
a9 is Element of the carrier' of S
the Arity of S . a9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . a9 is Element of the carrier of S
Den (a9,(FreeMSA X)) is Relation-like Args (a9,(FreeMSA X)) -defined Result (a9,(FreeMSA X)) -valued Function-like V36( Args (a9,(FreeMSA X)), Result (a9,(FreeMSA X))) Element of bool [:(Args (a9,(FreeMSA X))),(Result (a9,(FreeMSA X))):]
Args (a9,(FreeMSA X)) is non empty Element of proj2 ( the Sorts of (FreeMSA X) #)
the Sorts of (FreeMSA X) # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of (FreeMSA X) #) is non empty set
Result (a9,(FreeMSA X)) is non empty Element of proj2 the Sorts of (FreeMSA X)
proj2 the Sorts of (FreeMSA X) is non empty set
[:(Args (a9,(FreeMSA X))),(Result (a9,(FreeMSA X))):] is Relation-like set
bool [:(Args (a9,(FreeMSA X))),(Result (a9,(FreeMSA X))):] is set
proj2 (Den (a9,(FreeMSA X))) is set
a9 is Element of the carrier' of S
the Arity of S . a9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . a9 is Element of the carrier of S
Den (a9,(FreeMSA X)) is Relation-like Args (a9,(FreeMSA X)) -defined Result (a9,(FreeMSA X)) -valued Function-like V36( Args (a9,(FreeMSA X)), Result (a9,(FreeMSA X))) Element of bool [:(Args (a9,(FreeMSA X))),(Result (a9,(FreeMSA X))):]
Args (a9,(FreeMSA X)) is non empty Element of proj2 ( the Sorts of (FreeMSA X) #)
the Sorts of (FreeMSA X) # is Relation-like the carrier of S * -defined Function-like non empty total set
proj2 ( the Sorts of (FreeMSA X) #) is non empty set
Result (a9,(FreeMSA X)) is non empty Element of proj2 the Sorts of (FreeMSA X)
proj2 the Sorts of (FreeMSA X) is non empty set
[:(Args (a9,(FreeMSA X))),(Result (a9,(FreeMSA X))):] is Relation-like set
bool [:(Args (a9,(FreeMSA X))),(Result (a9,(FreeMSA X))):] is set
proj2 (Den (a9,(FreeMSA X))) is set
proj1 (Den (a9,(FreeMSA X))) is set
( the Arity of S * ((FreeSort X) #)) . a9 is set
Sym (a9,X) is Element of K315((DTConMSA X))
K315((DTConMSA X)) is non empty Element of bool the carrier of (DTConMSA X)
bool the carrier of (DTConMSA X) is set
[a9, the carrier of S] is V21() set
{a9, the carrier of S} is non empty finite set
{a9} is non empty trivial finite 1 -element set
{{a9, the carrier of S},{a9}} is non empty finite V28() set
roots (<*> (TS (DTConMSA X))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
DenOp (a9,X) is Relation-like ( the Arity of S * ((FreeSort X) #)) . a9 -defined ( the ResultSort of S * (FreeSort X)) . a9 -valued Function-like V36(( the Arity of S * ((FreeSort X) #)) . a9,( the ResultSort of S * (FreeSort X)) . a9) Element of bool [:(( the Arity of S * ((FreeSort X) #)) . a9),(( the ResultSort of S * (FreeSort X)) . a9):]
( the ResultSort of S * (FreeSort X)) . a9 is non empty set
[:(( the Arity of S * ((FreeSort X) #)) . a9),(( the ResultSort of S * (FreeSort X)) . a9):] is Relation-like set
bool [:(( the Arity of S * ((FreeSort X) #)) . a9),(( the ResultSort of S * (FreeSort X)) . a9):] is set
(DenOp (a9,X)) . (<*> (TS (DTConMSA X))) is set
(Sym (a9,X)) -tree (<*> (TS (DTConMSA X))) is Relation-like Function-like DecoratedTree-like set
da is Relation-like Function-like non empty finite DecoratedTree-like Element of the Sorts of (FreeMSA X) . v
dtk is set
(Den (a9,(FreeMSA X))) . dtk is set
depth da is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set
ttk is Relation-like Function-like finite DecoratedTree-like set
t is non empty finite Tree-like finite-order set
proj1 ttk is non empty finite Tree-like finite-order set
height t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
(FreeOper X) . a9 is Relation-like ( the Arity of S * ((FreeSort X) #)) . a9 -defined ( the ResultSort of S * (FreeSort X)) . a9 -valued Function-like V36(( the Arity of S * ((FreeSort X) #)) . a9,( the ResultSort of S * (FreeSort X)) . a9) Element of bool [:(( the Arity of S * ((FreeSort X) #)) . a9),(( the ResultSort of S * (FreeSort X)) . a9):]
root-tree (Sym (a9,X)) is Relation-like K315((DTConMSA X)) -valued Function-like constant trivial finite DecoratedTree-like Element of FinTrees K315((DTConMSA X))
FinTrees K315((DTConMSA X)) is functional non empty constituted-DTrees DTree-set of K315((DTConMSA X))
t is set
a is Relation-like Function-like non empty finite DecoratedTree-like Element of the Sorts of (FreeMSA X) . v
depth a is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set
k is Relation-like Function-like finite DecoratedTree-like set
ak is non empty finite Tree-like finite-order set
proj1 k is non empty finite Tree-like finite-order set
height ak is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
X . v is non empty set
a9 is set
[a9,v] is V21() set
{a9,v} is non empty finite set
{a9} is non empty trivial finite 1 -element set
{{a9,v},{a9}} is non empty finite V28() set
root-tree [a9,v] is Relation-like Function-like constant trivial finite DecoratedTree-like 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
FreeMSA X is strict non-empty MSAlgebra over S
FreeSort X is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
FreeOper X is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding ManySortedFunction of the Arity of S * ((FreeSort X) #), the ResultSort of S * (FreeSort X)
the Arity 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 functional non empty FinSequence-membered M8( 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
(FreeSort X) # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ((FreeSort X) #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort 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 ResultSort of S * (FreeSort X) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (FreeSort X),(FreeOper X) #) is strict MSAlgebra over S
the Sorts of (FreeMSA 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)
v is Element of the carrier of S
the Sorts of (FreeMSA X) . v is non empty set
vk is Element of the carrier of S
the Sorts of (FreeMSA X) . vk is non empty set
o is Element of the carrier' of S
Sym (o,X) is Element of K315((DTConMSA X))
K315((DTConMSA X)) is non empty Element of bool the carrier of (DTConMSA X)
bool the carrier of (DTConMSA X) is set
[o, the carrier of S] is V21() set
{o, the carrier of S} is non empty finite set
{o} is non empty trivial finite 1 -element set
{{o, the carrier of S},{o}} is non empty finite V28() set
t is Relation-like Function-like non empty finite DecoratedTree-like Element of the Sorts of (FreeMSA X) . v
depth t is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set
a is Relation-like NAT -defined FinTrees the carrier of (DTConMSA X) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (o,X)
[o, the carrier of S] -tree a is Relation-like Function-like DecoratedTree-like set
dom a is finite Element of bool NAT
k is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
a . k is Relation-like Function-like set
ak is Relation-like Function-like non empty finite DecoratedTree-like Element of the Sorts of (FreeMSA X) . vk
depth ak is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() set
a9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
proj1 t is non empty finite Tree-like finite-order set
doms a is Relation-like NAT -defined FinTrees -valued Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding FinSequence of FinTrees
dtk is Relation-like Function-like finite DecoratedTree-like set
ttk is non empty finite Tree-like finite-order set
proj1 dtk is non empty finite Tree-like finite-order set
height ttk is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
doms a9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding set
dom (doms a9) is finite Element of bool NAT
dom a9 is finite Element of bool NAT
da is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set
da . k is set
proj2 da is finite set
t is Relation-like Function-like finite DecoratedTree-like set
c is non empty finite Tree-like finite-order set
proj1 t is non empty finite Tree-like finite-order set
height c is V6() V7() V8() V12() finite cardinal V139() V140() ext-real non negative V144() Element of NAT
E2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
doms E2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding set
tree (doms E2) is non empty Tree-like set