:: 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

proj1 c

c

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

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

c

(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

the_sort_of c

[: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

o1 is Element of the carrier of S

[c

{c

{c

{{c

<*[c

<*[c

[c

{c

{{c

rs1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier' of (S) *

c

o1 is Element of the carrier of S

[c

{c

{c

{{c

<*[c

<*[c

[c

{c

{{c

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

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

<*( the Source of (S) . [c

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

the ResultSort of S . ([c

the ResultSort of S . c

the_result_sort_of c

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

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

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

{o1,c

{{o1,c

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

proj1 c

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

c

ak . (c

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

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

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