:: MSSCYC_2 semantic presentation

REAL is V142() V143() V144() V148() V151() V152() V154() set
NAT is V6() V7() V8() non empty V142() V143() V144() V145() V146() V147() V148() V149() V151() Element of bool REAL
bool REAL is set
NAT is V6() V7() V8() non empty V142() V143() V144() V145() V146() V147() V148() V149() V151() set
bool NAT is set
bool NAT is set
{} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty V16() V17() ext-real non positive non negative Function-like one-to-one constant functional finite finite-yielding V37() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V142() V143() V144() V145() V146() V147() V148() V151() V152() V153() V154() set
1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
{{},1} is non empty finite V142() V143() V144() V145() V146() V147() V149() V150() V151() V152() V153() set
Trees is non empty constituted-Trees set
bool Trees is set
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
K333() is non empty V112() L13()
the carrier of K333() is non empty set
FinTrees the carrier of K333() is non empty functional constituted-DTrees DTree-set of the carrier of K333()
K332(K333()) is functional constituted-DTrees Element of bool (FinTrees the carrier of K333())
bool (FinTrees the carrier of K333()) is set
[:K332(K333()),NAT:] is Relation-like set
bool [:K332(K333()),NAT:] is set
[:NAT,K332(K333()):] is Relation-like set
bool [:NAT,K332(K333()):] is set
2 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
3 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty V16() V17() ext-real non positive non negative Function-like one-to-one constant functional finite finite-yielding V37() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V142() V143() V144() V145() V146() V147() V148() V151() V152() V153() V154() Element of NAT
len {} is V38() set
elementary_tree 0 is non empty finite Tree-like set
height (elementary_tree 0) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
S is ManySortedSign
the carrier' of S is set
the carrier of S is set
the carrier of S * is non empty functional FinSequence-membered set
the Arity of S is Relation-like the carrier' of S -defined K202( the carrier of S) -valued Function-like V30( the carrier' of S,K202( the carrier of S)) Element of bool [: the carrier' of S,K202( the carrier of S):]
K202( the carrier of S) is non empty functional FinSequence-membered M11( the carrier of S)
[: the carrier' of S,K202( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K202( the carrier of S):] is set
[: the carrier' of S, the carrier of S:] is Relation-like set
A is set
GS is set
gs is set
v is set
[gs,v] is V12() V27() set
{gs,v} is non empty finite set
{gs} is non empty finite set
{{gs,v},{gs}} is non empty finite V37() set
the Arity of S . gs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
v is V6() V7() V8() V12() V16() V17() ext-real non negative set
dom n is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
n . v is set
gs is set
v is set
[gs,v] is V12() V27() set
{gs,v} is non empty finite set
{gs} is non empty finite set
{{gs,v},{gs}} is non empty finite V37() set
the Arity of S . gs is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
v is V6() V7() V8() V12() V16() V17() ext-real non negative set
dom n is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
n . v is set
G is set
A is set
S is ManySortedSign
(S) is set
the carrier' of S is set
the carrier of S is set
[: the carrier' of S, the carrier of S:] is Relation-like set
G is set
the carrier of S * is non empty functional FinSequence-membered set
the Arity of S is Relation-like the carrier' of S -defined K202( the carrier of S) -valued Function-like V30( the carrier' of S,K202( the carrier of S)) Element of bool [: the carrier' of S,K202( the carrier of S):]
K202( the carrier of S) is non empty functional FinSequence-membered M11( the carrier of S)
[: the carrier' of S,K202( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K202( the carrier of S):] is set
A is set
GS is set
[A,GS] is V12() V27() set
{A,GS} is non empty finite set
{A} is non empty finite set
{{A,GS},{A}} is non empty finite V37() set
the Arity of S . A 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 Element of the carrier of S *
gs is V6() V7() V8() V12() V16() V17() ext-real non negative set
dom v is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
v . gs is set
S is ManySortedSign
(S) is set
the carrier of S is set
[:(S), the carrier of S:] is Relation-like set
bool [:(S), the carrier of S:] is set
GS is set
GS `2 is set
the carrier' of S is set
[: the carrier' of S, the carrier of S:] is Relation-like set
GS is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
GS is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
gs is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
v is set
GS . v is set
v `2 is set
gs . v is set
the carrier' of S is set
[: the carrier' of S, the carrier of S:] is Relation-like set
proj1 GS is set
proj1 gs is set
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 V30( 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
v is set
v `1 is set
the ResultSort of S . (v `1) is set
v `2 is set
v is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
v is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
v is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
n is set
v . n is set
n `1 is set
the ResultSort of S . (n `1) is set
v . n is set
proj1 v is set
proj1 v is set
S is non empty V57() ManySortedSign
the carrier of S is non empty set
(S) is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
[:(S), the carrier of S:] is Relation-like set
bool [:(S), the carrier of S:] is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
MultiGraphStruct(# the carrier of S,(S),(S),(S) #) is strict MultiGraphStruct
S is non empty non void V57() ManySortedSign
the carrier of S is non empty set
(S) is non empty V57() MultiGraphStruct
(S) is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
[:(S), the carrier of S:] is Relation-like set
bool [:(S), the carrier of S:] is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
MultiGraphStruct(# the carrier of S,(S),(S),(S) #) is strict MultiGraphStruct
G is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
FreeMSA G is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA G) is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
A is Element of the carrier of S
the Sorts of (FreeMSA G) . A is non empty set
GS is V6() V7() V8() V12() V16() V17() ext-real non negative set
FreeSort G is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
FreeOper G is Relation-like the carrier' of S -defined non empty Function-like total ManySortedFunction of the Arity of S * K205( the carrier of S,(FreeSort G)), the ResultSort of S * (FreeSort G)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K202( the carrier of S) -valued Function-like V30( the carrier' of S,K202( the carrier of S)) Element of bool [: the carrier' of S,K202( the carrier of S):]
K202( the carrier of S) is non empty functional FinSequence-membered M11( the carrier of S)
[: the carrier' of S,K202( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K202( the carrier of S):] is set
K205( the carrier of S,(FreeSort G)) is Relation-like K202( the carrier of S) -defined non empty Function-like total set
the Arity of S * K205( the carrier of S,(FreeSort G)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V30( 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 G) is Relation-like non-empty the carrier' of S -defined Function-like set
MSAlgebra(# (FreeSort G),(FreeOper G) #) is strict MSAlgebra over S
FreeSort (G,A) is non empty functional constituted-DTrees Element of bool K332((DTConMSA G))
DTConMSA G is non empty V112() V116() V117() V118() L13()
K332((DTConMSA G)) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA G))
the carrier of (DTConMSA G) is non empty set
FinTrees the carrier of (DTConMSA G) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA G)
bool (FinTrees the carrier of (DTConMSA G)) is set
bool K332((DTConMSA G)) is set
S -Terms G is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA G))
the carrier' of (S) is set
the carrier' of (S) * is non empty functional FinSequence-membered set
n is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . A
depth n is V6() V7() V8() V12() V16() V17() ext-real non negative set
Vn is Relation-like Function-like finite DecoratedTree-like set
t is non empty finite Tree-like set
proj1 Vn is non empty finite Tree-like set
height t is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
V is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
V . {} is set
t is Element of the carrier' of S
[t, the carrier of S] is V12() V27() set
{t, the carrier of S} is non empty finite set
{t} is non empty finite set
{{t, the carrier of S},{t}} is non empty finite V37() set
Sym (t,G) is Element of K335((DTConMSA G))
K335((DTConMSA G)) is non empty Element of bool the carrier of (DTConMSA G)
bool the carrier of (DTConMSA G) is set
dvsk is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (t,G)
[t, the carrier of S] -tree dvsk is Relation-like Function-like DecoratedTree-like set
the_arity_of t is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like M12( the carrier of S,K202( the carrier of S))
dom dvsk is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
dom (the_arity_of t) is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
davsk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len davsk is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
len dvsk is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
nS is Relation-like Function-like DecoratedTree-like set
proj1 nS is non empty Tree-like set
avsk is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
avsk + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
dvsk . (avsk + 1) is Relation-like Function-like set
<*avsk*> is Relation-like NAT -defined NAT -valued non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 nS
<*avsk*> ^ x is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(the_arity_of t) . (avsk + 1) is set
k is Element of the carrier of S
[t,k] is V12() V27() set
{t,k} is non empty finite set
{{t,k},{t}} is non empty finite V37() set
the Arity of S . t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of K202( the carrier of S)
x is non empty set
k is Element of x
<*k*> is Relation-like NAT -defined x -valued non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of x
v is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
ak is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
davsk | ak is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n | (davsk | ak) is Relation-like Function-like DecoratedTree-like set
ak + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
davsk | (ak + 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n | (davsk | (ak + 1)) is Relation-like Function-like DecoratedTree-like set
davsk /^ ak is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ak + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
Seg ak is finite V40(ak) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Seg (ak + 1) is non empty finite V40(ak + 1) V142() V143() V144() V145() V146() V147() V149() V150() V151() V152() V153() Element of bool NAT
proj1 n is non empty finite Tree-like set
davsk | (ak + 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
len (davsk /^ ak) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
GS - ak is V16() V17() ext-real set
dom (davsk /^ ak) is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
o is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 n
V | o is Relation-like Function-like DecoratedTree-like set
Cn is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 n
V | Cn is Relation-like Function-like DecoratedTree-like set
o ^ (davsk /^ ak) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
t | o is non empty Tree-like set
c<sub>28</sub> is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
proj1 c<sub>28</sub> is non empty finite Tree-like set
c<sub>28</sub> . {} is set
rs1 is Element of the carrier' of S
[rs1, the carrier of S] is V12() V27() set
{rs1, the carrier of S} is non empty finite set
{rs1} is non empty finite set
{{rs1, the carrier of S},{rs1}} is non empty finite V37() set
Sym (rs1,G) is Element of K335((DTConMSA G))
Ck9 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (rs1,G)
[rs1, the carrier of S] -tree Ck9 is Relation-like Function-like DecoratedTree-like set
(davsk /^ ak) | 1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(davsk /^ ak) /. 1 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
<*((davsk /^ ak) /. 1)*> is Relation-like NAT -defined NAT -valued non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(davsk /^ ak) . 1 is set
<*((davsk /^ ak) . 1)*> is Relation-like NAT -defined non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like set
len Ck9 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
a is Relation-like Function-like DecoratedTree-like set
proj1 a is non empty Tree-like set
Ck1 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
Ck1 + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
Ck9 . (Ck1 + 1) is Relation-like Function-like set
<*Ck1*> is Relation-like NAT -defined NAT -valued non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
ck1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 a
<*Ck1*> ^ ck1 is Relation-like NAT -defined NAT -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
0 + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
o9 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 c<sub>28</sub>
o9 | (0 + 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
rs19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 c<sub>28</sub>
c<sub>28</sub> | rs19 is Relation-like the carrier of (DTConMSA G) -valued the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
(davsk | (ak + 1)) | ak is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
(davsk | (ak + 1)) | (Seg ak) is Relation-like NAT -defined Seg ak -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
[:NAT,NAT:] is Relation-like set
bool [:NAT,NAT:] is set
davsk | (Seg (ak + 1)) is Relation-like NAT -defined Seg (ak + 1) -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
(davsk | (Seg (ak + 1))) | (Seg ak) is Relation-like NAT -defined Seg ak -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
davsk | (Seg ak) is Relation-like NAT -defined Seg ak -defined NAT -defined NAT -valued Function-like finite FinSubsequence-like Element of bool [:NAT,NAT:]
the_arity_of rs1 is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like M12( the carrier of S,K202( the carrier of S))
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier' of (S) *
dom Ck9 is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
dom (the_arity_of rs1) is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
dom davsk is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
len Cn is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
dom Cn is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
davsk . (ak + 1) is set
<*(davsk . (ak + 1))*> is Relation-like NAT -defined non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like set
davsk /. (ak + 1) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
<*(davsk /. (ak + 1))*> is Relation-like NAT -defined NAT -valued non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
(davsk | (ak + 1)) /. (ak + 1) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
<*((davsk | (ak + 1)) /. (ak + 1))*> is Relation-like NAT -defined NAT -valued non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
Cn . (ak + 1) is set
<*(Cn . (ak + 1))*> is Relation-like NAT -defined non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like set
o ^ rs19 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ck1 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
o1 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
(the_arity_of rs1) . (Ck1 + 1) is set
args is Element of the carrier of S
[rs1,args] is V12() V27() set
{rs1,args} is non empty finite set
{{rs1,args},{rs1}} is non empty finite V37() set
the Arity of S . rs1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of K202( the carrier of S)
t is non empty set
dt is Element of t
<*dt*> is Relation-like NAT -defined t -valued non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of t
t9 is Relation-like NAT -defined t -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
<*dt*> ^ t9 is Relation-like NAT -defined t -valued non empty Function-like finite FinSequence-like FinSubsequence-like FinSequence of t
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier' of (S) *
the_sort_of o1 is Element of the carrier of S
n | (davsk | (ak + 1)) is Relation-like Function-like DecoratedTree-like set
<*[rs1,args]*> is Relation-like NAT -defined non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like set
<*[rs1,args]*> ^ i is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
o9 | 1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
ak is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier' of (S) *
ak is Relation-like NAT -defined the carrier' of (S) * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier' of (S) *
len ak is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
ak . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
nSk is V6() V7() V8() V12() V16() V17() ext-real non negative set
ak . nSk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
davsk | nSk is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n | (davsk | nSk) is Relation-like Function-like DecoratedTree-like set
nSk + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
ak . (nSk + 1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
davsk | (nSk + 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n | (davsk | (nSk + 1)) is Relation-like Function-like DecoratedTree-like set
<*[t,k]*> is Relation-like NAT -defined non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like set
proj1 n is non empty finite Tree-like set
0 + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
davsk | (0 + 1) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Cn is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 n
V | Cn is Relation-like Function-like DecoratedTree-like set
o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
len o is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
vertex-seq o 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 o) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq o) . ((len o) + 1) is set
(vertex-seq o) . 1 is set
c<sub>28</sub> is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
the_sort_of c<sub>28</sub> is Element of the carrier of S
[:NAT,NAT:] is Relation-like set
bool [:NAT,NAT:] is set
the Source of (S) is Relation-like the carrier' of (S) -defined the carrier of (S) -valued Function-like V30( 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) . [t,k] is set
the Target of (S) is Relation-like the carrier' of (S) -defined the carrier of (S) -valued Function-like V30( the carrier' of (S), the carrier of (S)) Element of bool [: the carrier' of (S), the carrier of (S):]
the Target of (S) . [t,k] is set
<*( the Source of (S) . [t,k]),( the Target of (S) . [t,k])*> is Relation-like NAT -defined non empty Function-like finite V40(2) FinSequence-like FinSubsequence-like set
1 + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq o) . (1 + 1) is set
[t,k] `1 is set
the ResultSort of S . ([t,k] `1) is set
the ResultSort of S . t is Element of the carrier of S
the_result_sort_of t is Element of the carrier of S
the_sort_of V is Element of the carrier of S
dom davsk is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
davsk | 1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
o1 is Relation-like NAT -defined NAT -valued Function-like Element of bool [:NAT,NAT:]
o1 /. 1 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
<*(o1 /. 1)*> is Relation-like NAT -defined NAT -valued non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like FinSequence of NAT
davsk . 1 is set
<*(davsk . 1)*> is Relation-like NAT -defined non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like set
[t,k] `2 is set
o is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
Cn is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
o . {} is set
the_sort_of Cn is Element of the carrier of S
rs1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier' of (S) *
c₂₈ is Element of the carrier' of S
o1 is Element of the carrier of S
[c₂₈,o1] is V12() V27() set
{c₂₈,o1} is non empty finite set
{c₂₈} is non empty finite set
{{c₂₈,o1},{c₂₈}} is non empty finite V37() set
<*[c₂₈,o1]*> is Relation-like NAT -defined non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like set
<*[c₂₈,o1]*> ^ rs1 is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
[c₂₈, the carrier of S] is V12() V27() set
{c₂₈, the carrier of S} is non empty finite set
{{c₂₈, the carrier of S},{c₂₈}} is non empty finite V37() set
rs1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier' of (S) *
c₂₈ is Element of the carrier' of S
o1 is Element of the carrier of S
[c₂₈,o1] is V12() V27() set
{c₂₈,o1} is non empty finite set
{c₂₈} is non empty finite set
{{c₂₈,o1},{c₂₈}} is non empty finite V37() set
<*[c₂₈,o1]*> is Relation-like NAT -defined non empty Function-like finite V40(1) FinSequence-like FinSubsequence-like set
<*[c₂₈,o1]*> ^ rs1 is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set
[c₂₈, the carrier of S] is V12() V27() set
{c₂₈, the carrier of S} is non empty finite set
{{c₂₈, the carrier of S},{c₂₈}} is non empty finite V37() set
Ck9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
vertex-seq Ck9 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 V30( 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) . [c₂₈,o1] is set
the Target of (S) is Relation-like the carrier' of (S) -defined the carrier of (S) -valued Function-like V30( the carrier' of (S), the carrier of (S)) Element of bool [: the carrier' of (S), the carrier of (S):]
the Target of (S) . [c₂₈,o1] is set
<*( the Source of (S) . [c₂₈,o1]),( the Target of (S) . [c₂₈,o1])*> is Relation-like NAT -defined non empty Function-like finite V40(2) FinSequence-like FinSubsequence-like set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
len a is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
ck1 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
vertex-seq a is Relation-like NAT -defined the carrier of (S) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (S)
(len a) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq a) . ((len a) + 1) is set
(vertex-seq a) . 1 is set
the_sort_of ck1 is Element of the carrier of S
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
len a is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
ck1 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
vertex-seq a is Relation-like NAT -defined the carrier of (S) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (S)
(len a) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq a) . ((len a) + 1) is set
(vertex-seq a) . 1 is set
the_sort_of ck1 is Element of the carrier of S
len Ck9 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
(len Ck9) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq Ck9) . ((len Ck9) + 1) is set
1 + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq Ck9) . (1 + 1) is set
[c₂₈,o1] `1 is set
the ResultSort of S . ([c<sub>28</sub>,o1] `1) is set
the ResultSort of S . c₂₈ is Element of the carrier of S
the_result_sort_of c₂₈ is Element of the carrier of S
the_sort_of o is Element of the carrier of S
Ck9 ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
o9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
len o9 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
vertex-seq o9 is Relation-like NAT -defined the carrier of (S) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (S)
(len o9) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq o9) . ((len o9) + 1) is set
(vertex-seq o9) . 1 is set
(len Ck9) + nSk is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
(vertex-seq Ck9) . 1 is set
[c₂₈,o1] `2 is set
ak . 0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
davsk | 0 is Relation-like non-empty empty-yielding NAT -defined NAT -valued V6() V7() V8() V10() V11() V12() empty V16() V17() ext-real non positive non negative Function-like one-to-one constant functional finite finite-yielding V37() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V142() V143() V144() V145() V146() V147() V148() V151() V152() V153() V154() FinSequence of NAT
n | (davsk | 0) is Relation-like Function-like DecoratedTree-like set
ak . GS is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
davsk | GS is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
n | (davsk | GS) is Relation-like Function-like DecoratedTree-like set
nSk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
len nSk is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
o is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
vertex-seq nSk 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 nSk) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq nSk) . ((len nSk) + 1) is set
(vertex-seq nSk) . 1 is set
the_sort_of o is Element of the carrier of S
v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
len v is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
vertex-seq v 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 v) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq v) . ((len v) + 1) is set
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 V30( 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) is Relation-like the carrier' of (S) -defined the carrier of (S) -valued Function-like V30( the carrier' of (S), the carrier of (S)) Element of bool [: the carrier' of (S), the carrier of (S):]
dvsk is set
G . dvsk is set
dvsk is Relation-like the carrier of S -defined non empty Function-like total set
dom v is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
v . 1 is set
the carrier of S * is non empty functional FinSequence-membered set
davsk is set
avsk is set
[davsk,avsk] is V12() V27() set
{davsk,avsk} is non empty finite set
{davsk} is non empty finite set
{{davsk,avsk},{davsk}} is non empty finite V37() set
the Arity of S . davsk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is Element of the carrier' of S
the_arity_of x is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like M12( the carrier of S,K202( the carrier of S))
len (the_arity_of x) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len k is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
dom k is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Seg (len k) is finite V40( len k) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
nSk is V6() V7() V8() V12() V16() V17() ext-real non negative set
k . nSk is set
(the_arity_of x) . nSk is set
dom (the_arity_of x) is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Seg (len (the_arity_of x)) is finite V40( len (the_arity_of x)) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
dvsk . ((the_arity_of x) . nSk) is set
k is Element of the carrier of S
G . k is non empty set
ak is Element of G . k
[ak,k] is V12() V27() set
{ak,k} is non empty finite set
{ak} is non empty finite set
{{ak,k},{ak}} is non empty finite V37() set
root-tree [ak,k] is Relation-like Function-like finite DecoratedTree-like set
nSk is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
the_sort_of nSk is Element of the carrier of S
Seg (len (the_arity_of x)) is finite V40( len (the_arity_of x)) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Sym (x,G) is Element of K335((DTConMSA G))
K335((DTConMSA G)) is non empty Element of bool the carrier of (DTConMSA G)
bool the carrier of (DTConMSA G) is set
[x, the carrier of S] is V12() V27() set
{x, the carrier of S} is non empty finite set
{x} is non empty finite set
{{x, the carrier of S},{x}} is non empty finite V37() set
nSk is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (x,G)
[x, the carrier of S] -tree nSk is Relation-like Function-like DecoratedTree-like set
n is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
ak is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
ak + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
v . (ak + 1) is set
ak + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
o is non empty set
v . (ak + 1) is set
nSk is Relation-like Function-like finite DecoratedTree-like Element of S -Terms G
ak is Element of o
o is set
Cn is set
[o,Cn] is V12() V27() set
{o,Cn} is non empty finite set
{o} is non empty finite set
{{o,Cn},{o}} is non empty finite V37() set
the Arity of S . o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
o1 is Element of the carrier' of S
the_arity_of o1 is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like M12( the carrier of S,K202( the carrier of S))
dom (the_arity_of o1) is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
c<sub>28</sub> is Element of the carrier of S
the_sort_of nSk is Element of the carrier of S
Ck1 is set
(the_arity_of o1) . Ck1 is set
dvsk . ((the_arity_of o1) . Ck1) is set
[(dvsk . ((the_arity_of o1) . Ck1)),((the_arity_of o1) . Ck1)] is V12() V27() set
{(dvsk . ((the_arity_of o1) . Ck1)),((the_arity_of o1) . Ck1)} is non empty finite set
{(dvsk . ((the_arity_of o1) . Ck1))} is non empty finite set
{{(dvsk . ((the_arity_of o1) . Ck1)),((the_arity_of o1) . Ck1)},{(dvsk . ((the_arity_of o1) . Ck1))}} is non empty finite V37() set
root-tree [(dvsk . ((the_arity_of o1) . Ck1)),((the_arity_of o1) . Ck1)] is Relation-like Function-like finite DecoratedTree-like set
a is Element of the carrier of S
G . a is non empty set
ck1 is Element of G . a
[ck1,a] is V12() V27() set
{ck1,a} is non empty finite set
{ck1} is non empty finite set
{{ck1,a},{ck1}} is non empty finite V37() set
root-tree [ck1,a] is Relation-like Function-like finite DecoratedTree-like set
o9 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
[:(dom (the_arity_of o1)),(S -Terms G):] is Relation-like set
bool [:(dom (the_arity_of o1)),(S -Terms G):] is set
Ck1 is Relation-like dom (the_arity_of o1) -defined S -Terms G -valued Function-like V30( dom (the_arity_of o1),S -Terms G) finite Element of bool [:(dom (the_arity_of o1)),(S -Terms G):]
len (the_arity_of o1) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
Seg (len (the_arity_of o1)) is finite V40( len (the_arity_of o1)) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
a is Relation-like NAT -defined S -Terms G -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of S -Terms G
dom a is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
ck1 is V6() V7() V8() V12() V16() V17() ext-real non negative set
a . ck1 is Relation-like Function-like set
o9 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
rs19 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
(the_arity_of o1) . ck1 is set
the_sort_of rs19 is Element of the carrier of S
(the_arity_of o1) . ck1 is set
dvsk . ((the_arity_of o1) . ck1) is set
ck1 is Element of the carrier of S
G . ck1 is non empty set
[(dvsk . ((the_arity_of o1) . ck1)),((the_arity_of o1) . ck1)] is V12() V27() set
{(dvsk . ((the_arity_of o1) . ck1)),((the_arity_of o1) . ck1)} is non empty finite set
{(dvsk . ((the_arity_of o1) . ck1))} is non empty finite set
{{(dvsk . ((the_arity_of o1) . ck1)),((the_arity_of o1) . ck1)},{(dvsk . ((the_arity_of o1) . ck1))}} is non empty finite V37() set
root-tree [(dvsk . ((the_arity_of o1) . ck1)),((the_arity_of o1) . ck1)] is Relation-like Function-like finite DecoratedTree-like set
the_sort_of rs19 is Element of the carrier of S
(the_arity_of o1) . ck1 is set
Sym (o1,G) is Element of K335((DTConMSA G))
[o1, the carrier of S] is V12() V27() set
{o1, the carrier of S} is non empty finite set
{o1} is non empty finite set
{{o1, the carrier of S},{o1}} is non empty finite V37() set
ck1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (o1,G)
[o1, the carrier of S] -tree ck1 is Relation-like Function-like DecoratedTree-like set
o9 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
[o1,c<sub>28</sub>] is V12() V27() set
{o1,c<sub>28</sub>} is non empty finite set
{{o1,c<sub>28</sub>},{o1}} is non empty finite V37() set
dom ck1 is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
rs19 is V6() V7() V8() V12() V16() V17() ext-real non negative set
ck1 . rs19 is Relation-like Function-like set
(the_arity_of o1) . rs19 is set
ck1 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
the_sort_of ck1 is Element of the carrier of S
dvsk . (the_sort_of ck1) is set
[(dvsk . (the_sort_of ck1)),(the_sort_of ck1)] is V12() V27() set
{(dvsk . (the_sort_of ck1)),(the_sort_of ck1)} is non empty finite set
{(dvsk . (the_sort_of ck1))} is non empty finite set
{{(dvsk . (the_sort_of ck1)),(the_sort_of ck1)},{(dvsk . (the_sort_of ck1))}} is non empty finite V37() set
root-tree [(dvsk . (the_sort_of ck1)),(the_sort_of ck1)] is Relation-like Function-like finite DecoratedTree-like set
k is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
ak is Relation-like NAT -defined S -Terms G -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of S -Terms G
len ak is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
ak . 1 is Relation-like Function-like set
ak is V6() V7() V8() V12() V16() V17() ext-real non negative set
ak . ak is Relation-like Function-like set
v . ak is set
(v . ak) `1 is set
ak + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
ak . (ak + 1) is Relation-like Function-like set
v . (ak + 1) is set
(v . (ak + 1)) `1 is set
the_sort_of k is Element of the carrier of S
proj1 k is non empty finite Tree-like set
height (proj1 k) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
the_result_sort_of x is Element of the carrier of S
doms nSk is Relation-like NAT -defined FinTrees -valued Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding FinSequence of FinTrees
dom (doms nSk) is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
dom nSk is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
k . {} is set
the Arity of S . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of K202( the carrier of S)
nS is Element of the carrier of S
Cn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
o is V6() V7() V8() V12() V16() V17() ext-real non negative set
dom Cn is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Cn . o is set
Cn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
o is V6() V7() V8() V12() V16() V17() ext-real non negative set
dom Cn is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Cn . o is set
len Cn is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
Seg (len Cn) is finite V40( len Cn) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
nSk . o is Relation-like Function-like set
(doms nSk) . o is set
c<sub>28</sub> is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
proj1 c<sub>28</sub> is non empty finite Tree-like set
tree (doms nSk) is non empty finite Tree-like set
nSk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set
proj2 nSk is finite set
(the_arity_of x) . o is set
dvsk . ((the_arity_of x) . o) is set
[(dvsk . ((the_arity_of x) . o)),((the_arity_of x) . o)] is V12() V27() set
{(dvsk . ((the_arity_of x) . o)),((the_arity_of x) . o)} is non empty finite set
{(dvsk . ((the_arity_of x) . o))} is non empty finite set
{{(dvsk . ((the_arity_of x) . o)),((the_arity_of x) . o)},{(dvsk . ((the_arity_of x) . o))}} is non empty finite V37() set
root-tree [(dvsk . ((the_arity_of x) . o)),((the_arity_of x) . o)] is Relation-like Function-like finite DecoratedTree-like set
rs1 is non empty finite Tree-like set
dom nSk is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Ck9 is V6() V7() V8() V12() V16() V17() ext-real non negative set
nSk . Ck9 is set
nSk . Ck9 is Relation-like Function-like set
(the_arity_of x) . Ck9 is set
dvsk . ((the_arity_of x) . Ck9) is set
[(dvsk . ((the_arity_of x) . Ck9)),((the_arity_of x) . Ck9)] is V12() V27() set
{(dvsk . ((the_arity_of x) . Ck9)),((the_arity_of x) . Ck9)} is non empty finite set
{(dvsk . ((the_arity_of x) . Ck9))} is non empty finite set
{{(dvsk . ((the_arity_of x) . Ck9)),((the_arity_of x) . Ck9)},{(dvsk . ((the_arity_of x) . Ck9))}} is non empty finite V37() set
root-tree [(dvsk . ((the_arity_of x) . Ck9)),((the_arity_of x) . Ck9)] is Relation-like Function-like finite DecoratedTree-like set
Ck1 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
proj1 Ck1 is non empty finite Tree-like set
height rs1 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
o1 is non empty finite Tree-like set
height o1 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
o is non empty set
o is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
Cn is Element of the carrier' of S
the_sort_of o is Element of the carrier of S
the_result_sort_of Cn is Element of the carrier of S
proj1 o is non empty finite Tree-like set
height (proj1 o) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
o is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
Cn is Element of the carrier' of S
the_sort_of o is Element of the carrier of S
the_result_sort_of Cn is Element of the carrier of S
proj1 o is non empty finite Tree-like set
height (proj1 o) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
c<sub>28</sub> is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
c<sub>28</sub> + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
ak . (c<sub>28</sub> + 1) is Relation-like Function-like set
o1 is Element of the carrier' of S
Sym (o1,G) is Element of K335((DTConMSA G))
Ck9 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
Ck1 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
rs1 is Element of the carrier of S
[o1,rs1] is V12() V27() set
{o1,rs1} is non empty finite set
{o1} is non empty finite set
{{o1,rs1},{o1}} is non empty finite V37() set
[o1, the carrier of S] is V12() V27() set
{o1, the carrier of S} is non empty finite set
{{o1, the carrier of S},{o1}} is non empty finite V37() set
a is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (o1,G)
[o1, the carrier of S] -tree a is Relation-like Function-like DecoratedTree-like set
dom a is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
the_arity_of o1 is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like M12( the carrier of S,K202( the carrier of S))
the_sort_of Ck9 is Element of the carrier of S
v . (c<sub>28</sub> + 1) is set
o9 is set
rs19 is set
[o9,rs19] is V12() V27() set
{o9,rs19} is non empty finite set
{o9} is non empty finite set
{{o9,rs19},{o9}} is non empty finite V37() set
the Arity of S . o9 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
the_sort_of Ck1 is Element of the carrier of S
proj1 Ck1 is non empty finite Tree-like set
height (proj1 Ck1) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
the_result_sort_of o1 is Element of the carrier of S
Ck1 . {} is set
doms a is Relation-like NAT -defined FinTrees -valued Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding FinSequence of FinTrees
tree (doms a) is non empty finite Tree-like set
len a is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
len (the_arity_of o1) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
Seg (len a) is finite V40( len a) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
args is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
i is V6() V7() V8() V12() V16() V17() ext-real non negative set
dom args is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
args . i is set
args is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
i is V6() V7() V8() V12() V16() V17() ext-real non negative set
dom args is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
args . i is set
len args is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
Seg (len args) is finite V40( len args) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
o9 is Element of the carrier' of S
the_arity_of o9 is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like M12( the carrier of S,K202( the carrier of S))
a . i is Relation-like Function-like set
(the_arity_of o1) . i is set
t is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
the_sort_of t is Element of the carrier of S
dvsk . (the_sort_of t) is set
[(dvsk . (the_sort_of t)),(the_sort_of t)] is V12() V27() set
{(dvsk . (the_sort_of t)),(the_sort_of t)} is non empty finite set
{(dvsk . (the_sort_of t))} is non empty finite set
{{(dvsk . (the_sort_of t)),(the_sort_of t)},{(dvsk . (the_sort_of t))}} is non empty finite V37() set
root-tree [(dvsk . (the_sort_of t)),(the_sort_of t)] is Relation-like Function-like finite DecoratedTree-like set
proj1 t is non empty finite Tree-like set
dom (doms a) is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
t9 is non empty finite Tree-like set
w is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set
proj2 w is finite set
dom w is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
j is V6() V7() V8() V12() V16() V17() ext-real non negative set
w . j is set
a . j is Relation-like Function-like set
(the_arity_of o1) . j is set
t99 is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
the_sort_of t99 is Element of the carrier of S
dvsk . (the_sort_of t99) is set
[(dvsk . (the_sort_of t99)),(the_sort_of t99)] is V12() V27() set
{(dvsk . (the_sort_of t99)),(the_sort_of t99)} is non empty finite set
{(dvsk . (the_sort_of t99))} is non empty finite set
{{(dvsk . (the_sort_of t99)),(the_sort_of t99)},{(dvsk . (the_sort_of t99))}} is non empty finite V37() set
root-tree [(dvsk . (the_sort_of t99)),(the_sort_of t99)] is Relation-like Function-like finite DecoratedTree-like set
proj1 t99 is non empty finite Tree-like set
height t9 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
dt is non empty finite Tree-like set
height dt is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
height t9 is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
dt is non empty finite Tree-like set
height dt is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
dt is non empty finite Tree-like set
height dt is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
dt is non empty finite Tree-like set
height dt is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
(doms a) . i is set
nSk is Element of o
nSk `1 is set
the ResultSort of S . (nSk `1) is set
the Target of (S) . nSk is set
(vertex-seq v) . (c<sub>28</sub> + 1) is set
ck1 is Element of o
the Source of (S) . ck1 is set
ck1 `2 is set
v . (len v) is set
ak . 0 is Relation-like Function-like set
v . 0 is set
(v . 0) `1 is set
ak . GS is Relation-like Function-like set
v . GS is set
(v . GS) `1 is set
nSk is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
o is Element of the carrier' of S
the_sort_of nSk is Element of the carrier of S
the_result_sort_of o is Element of the carrier of S
proj1 nSk is non empty finite Tree-like set
height (proj1 nSk) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
the Target of (S) . (v . (len v)) is set
(v . (len v)) `1 is set
the ResultSort of S . ((v . (len v)) `1) is set
Cn is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . A
depth Cn is V6() V7() V8() V12() V16() V17() ext-real non negative set
S is non empty void V57() trivial' Circuit-like ManySortedSign
(S) is non empty V57() MultiGraphStruct
the carrier of S is non empty set
(S) is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
[:(S), the carrier of S:] is Relation-like set
bool [:(S), the carrier of S:] is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
MultiGraphStruct(# the carrier of S,(S),(S),(S) #) is strict MultiGraphStruct
the carrier' of S is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty trivial V16() V17() ext-real non positive non negative Function-like one-to-one constant functional finite finite-yielding V37() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V142() V143() V144() V145() V146() V147() V148() V151() V152() V153() V154() set
the Arity of S is Relation-like non-empty empty-yielding the carrier' of S -defined K202( the carrier of S) -valued V6() V7() V8() V10() V11() V12() empty V16() V17() ext-real non positive non negative Function-like one-to-one constant functional V30( the carrier' of S,K202( the carrier of S)) finite finite-yielding V37() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V142() V143() V144() V145() V146() V147() V148() V151() V152() V153() V154() Element of bool [: the carrier' of S,K202( the carrier of S):]
K202( the carrier of S) is non empty functional FinSequence-membered M11( the carrier of S)
[: the carrier' of S,K202( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K202( the carrier of S):] is set
the carrier of (S) is non empty set
v is Element of the carrier of (S)
v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
vertex-seq v is Relation-like NAT -defined the carrier of (S) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (S)
len v is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
(len v) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq v) . ((len v) + 1) is set
the carrier' of (S) is set
proj2 v is finite set
dom v is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
v . 1 is set
the carrier of S * is non empty functional FinSequence-membered set
n is set
V is set
[n,V] is V12() V27() set
{n,V} is non empty finite set
{n} is non empty finite set
{{n,V},{n}} is non empty finite V37() set
the Arity of S . n is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() empty V16() V17() ext-real non positive non negative Function-like one-to-one constant functional finite finite-yielding V37() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V142() V143() V144() V145() V146() V147() V148() V151() V152() V153() V154() set
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
Vn is V6() V7() V8() V12() V16() V17() ext-real non negative set
dom t is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
t . Vn is set
v is non-empty finitely-generated MSAlgebra over S
the Sorts of v is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
S is non empty non void V57() ManySortedSign
(S) is non empty V57() MultiGraphStruct
the carrier of S is non empty set
(S) is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
[:(S), the carrier of S:] is Relation-like set
bool [:(S), the carrier of S:] is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
MultiGraphStruct(# the carrier of S,(S),(S),(S) #) is strict MultiGraphStruct
A is non empty non void V57() monotonic ManySortedSign
the non-empty finitely-generated finite-yielding MSAlgebra over A is non-empty finitely-generated finite-yielding MSAlgebra over A
the carrier of (S) is non empty set
gs is Element of the carrier of (S)
the carrier of A is non empty set
FreeEnv the non-empty finitely-generated finite-yielding MSAlgebra over A is strict non-empty V120(A) MSAlgebra over A
the Sorts of the non-empty finitely-generated finite-yielding MSAlgebra over A is Relation-like non-empty non empty-yielding the carrier of A -defined non empty Function-like total set
FreeMSA the Sorts of the non-empty finitely-generated finite-yielding MSAlgebra over A is strict non-empty MSAlgebra over A
the Sorts of (FreeEnv the non-empty finitely-generated finite-yielding MSAlgebra over A) is Relation-like non-empty non empty-yielding the carrier of A -defined non empty Function-like total set
v is Element of the carrier of A
the Sorts of (FreeEnv the non-empty finitely-generated finite-yielding MSAlgebra over A) . v is non empty set
{ (depth b₁) where b₁ is Element of the Sorts of (FreeEnv the non-empty finitely-generated finite-yielding MSAlgebra over A) . v : verum } is set
depth (v, the non-empty finitely-generated finite-yielding MSAlgebra over A) is V6() V7() V8() V12() V16() V17() ext-real non negative set
v is non empty finite V142() V143() V144() V145() V146() V147() V149() V150() V151() V152() V153() Element of bool NAT
max v is V6() V7() V8() V12() V16() V17() ext-real non negative set
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
vertex-seq n is Relation-like NAT -defined the carrier of (S) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (S)
len n is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
(len n) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq n) . ((len n) + 1) is set
the Sorts of (FreeMSA the Sorts of the non-empty finitely-generated finite-yielding MSAlgebra over A) is Relation-like non-empty non empty-yielding the carrier of A -defined non empty Function-like total set
the Sorts of (FreeMSA the Sorts of the non-empty finitely-generated finite-yielding MSAlgebra over A) . v is non empty set
V is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of the non-empty finitely-generated finite-yielding MSAlgebra over A) . v
depth V is V6() V7() V8() V12() V16() V17() ext-real non negative set
Vn is Element of the Sorts of (FreeEnv the non-empty finitely-generated finite-yielding MSAlgebra over A) . v
depth Vn is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
t is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA the Sorts of the non-empty finitely-generated finite-yielding MSAlgebra over A) . v
depth t is V6() V7() V8() V12() V16() V17() ext-real non negative set
S is non empty non void V57() ManySortedSign
the carrier of S is non empty set
G is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total finite-yielding set
FreeMSA G is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA G) is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
FreeSort G is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
FreeOper G is Relation-like the carrier' of S -defined non empty Function-like total ManySortedFunction of the Arity of S * K205( the carrier of S,(FreeSort G)), the ResultSort of S * (FreeSort G)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined K202( the carrier of S) -valued Function-like V30( the carrier' of S,K202( the carrier of S)) Element of bool [: the carrier' of S,K202( the carrier of S):]
K202( the carrier of S) is non empty functional FinSequence-membered M11( the carrier of S)
[: the carrier' of S,K202( the carrier of S):] is Relation-like set
bool [: the carrier' of S,K202( the carrier of S):] is set
K205( the carrier of S,(FreeSort G)) is Relation-like K202( the carrier of S) -defined non empty Function-like total set
the Arity of S * K205( the carrier of S,(FreeSort G)) is Relation-like the carrier' of S -defined Function-like set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V30( 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 G) is Relation-like non-empty the carrier' of S -defined Function-like set
MSAlgebra(# (FreeSort G),(FreeOper G) #) is strict MSAlgebra over S
GS is V6() V7() V8() V12() V16() V17() ext-real non negative set
GS + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
gs is Element of the carrier of S
the Sorts of (FreeMSA G) . gs is non empty set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : depth b₁ <= GS + 1 } is set
{ H₁(b₁) where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : S₃[b₁] } is set
{ H₁(b₁) where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : S₄[b₁] } is set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : S₂[b₁] } is set
{ b₁ where b₁ is Element of the carrier' of S : the_result_sort_of b₁ = gs } is set
FreeSort (G,gs) is non empty functional constituted-DTrees Element of bool K332((DTConMSA G))
DTConMSA G is non empty V112() V116() V117() V118() L13()
K332((DTConMSA G)) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA G))
the carrier of (DTConMSA G) is non empty set
FinTrees the carrier of (DTConMSA G) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA G)
bool (FinTrees the carrier of (DTConMSA G)) is set
bool K332((DTConMSA G)) is set
Vn is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 Vn is finite set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : ( depth b₁ = GS + 1 & b₁ . {} = [(Vn . a₁), the carrier of S] ) } is set
len Vn is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len t is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
dom t is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
dom Vn is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Seg (len Vn) is finite V40( len Vn) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Seg (len t) is finite V40( len t) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
S -Terms G is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA G))
Union t is set
t is set
dvsk is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs
depth dvsk is V6() V7() V8() V12() V16() V17() ext-real non negative set
o is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
davsk is Relation-like Function-like finite DecoratedTree-like set
avsk is non empty finite Tree-like set
proj1 davsk is non empty finite Tree-like set
height avsk is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
o . {} is set
davsk is Element of the carrier' of S
[davsk, the carrier of S] is V12() V27() set
{davsk, the carrier of S} is non empty finite set
{davsk} is non empty finite set
{{davsk, the carrier of S},{davsk}} is non empty finite V37() set
the_result_sort_of davsk is Element of the carrier of S
the_sort_of o is Element of the carrier of S
avsk is set
Vn . avsk is set
t . avsk is set
[(Vn . avsk), the carrier of S] is V12() V27() set
{(Vn . avsk), the carrier of S} is non empty finite set
{(Vn . avsk)} is non empty finite set
{{(Vn . avsk), the carrier of S},{(Vn . avsk)}} is non empty finite V37() set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : ( depth b₁ = GS + 1 & b₁ . {} = [(Vn . avsk), the carrier of S] ) } is set
proj2 t is finite set
union (proj2 t) is set
t is set
t . t is set
Vn . t is set
[(Vn . t), the carrier of S] is V12() V27() set
{(Vn . t), the carrier of S} is non empty finite set
{(Vn . t)} is non empty finite set
{{(Vn . t), the carrier of S},{(Vn . t)}} is non empty finite V37() set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : ( depth b₁ = GS + 1 & b₁ . {} = [(Vn . t), the carrier of S] ) } is set
o is Element of the carrier' of S
the_result_sort_of o is Element of the carrier of S
(S -Terms G) * is non empty functional FinSequence-membered set
[o, the carrier of S] is V12() V27() set
{o, the carrier of S} is non empty finite set
{o} is non empty finite set
{{o, the carrier of S},{o}} is non empty finite V37() set
Sym (o,G) is Element of K335((DTConMSA G))
K335((DTConMSA G)) is non empty Element of bool the carrier of (DTConMSA G)
bool the carrier of (DTConMSA G) is set
{ ([o, the carrier of S] -tree b₁) where b₁ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (S -Terms G) * : ( b₁ is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (o,G) & ex b₂ being Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs st
( depth b₂ = GS + 1 & b₂ = [o, the carrier of S] -tree b₁ ) ) } is set
avsk is set
nS is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs
depth nS is V6() V7() V8() V12() V16() V17() ext-real non negative set
nS . {} is set
x is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
k is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (o,G)
[o, the carrier of S] -tree k is Relation-like Function-like DecoratedTree-like set
nSk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (S -Terms G) *
[o, the carrier of S] -tree nSk is Relation-like Function-like DecoratedTree-like set
the_arity_of o is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like M12( the carrier of S,K202( the carrier of S))
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . ((the_arity_of o) /. a₁) : depth b₁ <= GS } is set
{ b₁ where b₁ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (S -Terms G) * : ( b₁ is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (o,G) & ex b₂ being Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs st
( depth b₂ = GS + 1 & b₂ = [o, the carrier of S] -tree b₁ ) ) } is set
{ [b₁,([o, the carrier of S] -tree b₁)] where b₁ is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (S -Terms G) * : ( b₁ is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (o,G) & ex b₂ being Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs st
( depth b₂ = GS + 1 & b₂ = [o, the carrier of S] -tree b₁ ) ) } is set
x is set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (S -Terms G) *
[o, the carrier of S] -tree k is Relation-like Function-like DecoratedTree-like set
nSk is set
x is set
k is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs
depth k is V6() V7() V8() V12() V16() V17() ext-real non negative set
[x,x] is V12() V27() set
{x,x} is non empty finite set
{x} is non empty finite set
{{x,x},{x}} is non empty finite V37() set
k is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs
depth k is V6() V7() V8() V12() V16() V17() ext-real non negative set
x is set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (S -Terms G) *
[o, the carrier of S] -tree k is Relation-like Function-like DecoratedTree-like set
nSk is set
x is set
k is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs
depth k is V6() V7() V8() V12() V16() V17() ext-real non negative set
[x,x] is V12() V27() set
{x,x} is non empty finite set
{x} is non empty finite set
{{x,x},{x}} is non empty finite V37() set
k is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs
depth k is V6() V7() V8() V12() V16() V17() ext-real non negative set
x is set
k is set
[x,k] is V12() V27() set
{x,k} is non empty finite set
{x} is non empty finite set
{{x,k},{x}} is non empty finite V37() set
nSk is set
x is set
[nSk,x] is V12() V27() set
{nSk,x} is non empty finite set
{nSk} is non empty finite set
{{nSk,x},{nSk}} is non empty finite V37() set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (S -Terms G) *
[o, the carrier of S] -tree k is Relation-like Function-like DecoratedTree-like set
[k,([o, the carrier of S] -tree k)] is V12() V27() set
{k,([o, the carrier of S] -tree k)} is non empty functional finite set
{k} is non empty functional finite V37() set
{{k,([o, the carrier of S] -tree k)},{k}} is non empty finite V37() set
ak is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (S -Terms G) *
[o, the carrier of S] -tree ak is Relation-like Function-like DecoratedTree-like set
[ak,([o, the carrier of S] -tree ak)] is V12() V27() set
{ak,([o, the carrier of S] -tree ak)} is non empty functional finite set
{ak} is non empty functional finite V37() set
{{ak,([o, the carrier of S] -tree ak)},{ak}} is non empty finite V37() set
len (the_arity_of o) is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
nS is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len nS is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
dom nS is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Seg (len nS) is finite V40( len nS) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Seg (len (the_arity_of o)) is finite V40( len (the_arity_of o)) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
product nS is set
x is set
k is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (S -Terms G) *
[o, the carrier of S] -tree k is Relation-like Function-like DecoratedTree-like set
nSk is Relation-like NAT -defined FinTrees the carrier of (DTConMSA G) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding ArgumentSeq of Sym (o,G)
len nSk is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
dom nSk is finite V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
Seg (len nSk) is finite V40( len nSk) V142() V143() V144() V145() V146() V147() V151() V152() V153() Element of bool NAT
x is set
k is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
nSk . k is Relation-like Function-like set
ak is Relation-like the carrier of (DTConMSA G) -valued Function-like finite DecoratedTree-like M25( the carrier of (DTConMSA G), FinTrees the carrier of (DTConMSA G),S -Terms G)
the_sort_of ak is Element of the carrier of S
(the_arity_of o) /. k is Element of the carrier of S
the Sorts of (FreeMSA G) . (the_sort_of ak) is non empty set
FreeSort (G,(the_sort_of ak)) is non empty functional constituted-DTrees Element of bool K332((DTConMSA G))
the Sorts of (FreeMSA G) . ((the_arity_of o) /. k) is non empty set
ak is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . ((the_arity_of o) /. k)
depth ak is V6() V7() V8() V12() V16() V17() ext-real non negative set
nSk is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs
depth nSk is V6() V7() V8() V12() V16() V17() ext-real non negative set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . ((the_arity_of o) /. k) : depth b₁ <= GS } is set
nS . x is set
nSk . x is Relation-like Function-like set
x is set
k is V6() V7() V8() V12() V16() V17() ext-real non negative set
(the_arity_of o) /. k is Element of the carrier of S
the Sorts of (FreeMSA G) . ((the_arity_of o) /. k) is non empty set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . ((the_arity_of o) /. k) : depth b₁ <= GS } is set
nS . k is set
nS . x is set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : S₅[b₁] } is set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : ( S₅[b₁] or S₂[b₁] ) } is set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : S₅[b₁] } \/ { b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs : S₂[b₁] } is set
dvsk is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs
depth dvsk is V6() V7() V8() V12() V16() V17() ext-real non negative set
o is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . gs
depth o is V6() V7() V8() V12() V16() V17() ext-real non negative set
GS is Element of the carrier of S
the Sorts of (FreeMSA G) . GS is non empty set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . GS : depth b₁ <= 0 } is set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . GS : depth b₁ = 0 } is set
v is set
n is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA G) . GS
depth n is V6() V7() V8() V12() V16() V17() ext-real non negative set
Constants ((FreeMSA G),GS) is Element of bool ( the Sorts of (FreeMSA G) . GS)
bool ( the Sorts of (FreeMSA G) . GS) is set
FreeGen (GS,G) is non empty finite Element of bool ((FreeSort G) . GS)
(FreeSort G) . GS is non empty set
bool ((FreeSort G) . GS) is set
(FreeGen (GS,G)) \/ (Constants ((FreeMSA G),GS)) is non empty set
S is non empty non void V57() ManySortedSign
(S) is non empty V57() MultiGraphStruct
the carrier of S is non empty set
(S) is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
[:(S), the carrier of S:] is Relation-like set
bool [:(S), the carrier of S:] is set
(S) is Relation-like (S) -defined the carrier of S -valued Function-like V30((S), the carrier of S) Element of bool [:(S), the carrier of S:]
MultiGraphStruct(# the carrier of S,(S),(S),(S) #) is strict MultiGraphStruct
A is non-empty finitely-generated MSAlgebra over S
the Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total finite-yielding GeneratorSet of A is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total finite-yielding GeneratorSet of A
gs is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total finite-yielding set
FreeMSA gs is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA gs) is Relation-like non-empty non empty-yielding the carrier of S -defined non empty Function-like total set
v is set
the Sorts of (FreeMSA gs) . v is set
v is Element of the carrier of S
n is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
the Sorts of (FreeMSA gs) . v is non empty set
{ b₁ where b₁ is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA gs) . v : depth b₁ <= n } is set
t is set
t is Relation-like non empty Function-like finite DecoratedTree-like Element of the Sorts of (FreeMSA gs) . v
depth t is V6() V7() V8() V12() V16() V17() ext-real non negative set
dvsk is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like oriented Chain of (S)
len dvsk is V6() V7() V8() V12() V16() V17() ext-real non negative V142() V143() V144() V145() V146() V147() V151() Element of NAT
vertex-seq dvsk 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 dvsk) + 1 is V6() V7() V8() V12() non empty V16() V17() ext-real positive non negative V142() V143() V144() V145() V146() V147() V149() V151() Element of NAT
(vertex-seq dvsk) . ((len dvsk) + 1) is set