:: MSAFREE2 semantic presentation

K37() is non empty non trivial V7() V8() V9() non finite countable denumerable Element of bool K33()

K33() is set

bool K33() is set

K32() is non empty non trivial V7() V8() V9() non finite countable denumerable set

bool K32() is set

bool K37() is set

{} is empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

1 is non empty set

{{},1} is non empty finite countable set

Trees is non empty constituted-Trees set

bool Trees is set

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

PeanoNat is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of PeanoNat is non empty set

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

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

bool (FinTrees the carrier of PeanoNat) is set

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

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

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

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

K34() is set

K35() is set

K36() is set

[:K34(),K34():] is Relation-like set

bool [:K34(),K34():] is set

[:K34(),K33():] is Relation-like set

bool [:K34(),K33():] is set

2 is non empty set

3 is non empty set

K38() is empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of K37()

elementary_tree K38() is non empty finite countable Tree-like set

{{}} is non empty functional finite V36() with_common_domain countable Tree-like set

S is non empty V55() ManySortedSign

the carrier of S is non empty set

{ b

bool the carrier of S is set

{ b

S is non empty V55() ManySortedSign

the carrier of S is non empty set

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

the carrier' of S is set

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

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

rng the ResultSort of S is Element of bool the carrier of S

bool the carrier of S is set

the carrier of S \ (rng the ResultSort of S) is Element of bool the carrier of S

S is non empty void V55() trivial' ManySortedSign

(S) is Element of bool the carrier of S

the carrier of S is non empty set

bool the carrier of S is set

the ResultSort of S is empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding the carrier' of S -defined the carrier of S -valued Function-like one-to-one constant functional V29( the carrier' of S, the carrier of S) finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is empty trivial V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set

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

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

rng the ResultSort of S is empty trivial V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of bool the carrier of S

the carrier of S \ (rng the ResultSort of S) is Element of bool the carrier of S

S is non empty non void V55() ManySortedSign

the carrier of S is non empty set

(S) is Element of bool the carrier of S

bool 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 V29( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

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

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

rng the ResultSort of S is Element of bool the carrier of S

the carrier of S \ (rng the ResultSort of S) is Element of bool the carrier of S

X is Element of the carrier of S

v is Element of the carrier' of S

the_result_sort_of v is Element of the carrier of S

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

dom the ResultSort of S is Element of bool the carrier' of S

bool the carrier' of S is set

S is non empty V55() ManySortedSign

(S) is Element of bool the carrier of S

the carrier of S is non empty set

bool the carrier of S is set

(S) is Element of bool the carrier of S

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

the carrier' of S is set

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

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

rng the ResultSort of S is Element of bool the carrier of S

X is set

{ b

v is Element of the carrier of S

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding V41() Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

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

e is Element of the carrier' of S

the Arity of S . e is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable set

the ResultSort of S . e is set

S is non empty V55() ManySortedSign

(S) is Element of bool the carrier of S

the carrier of S is non empty set

bool 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 V29( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is set

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

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

rng the ResultSort of S is Element of bool the carrier of S

the carrier of S \ (rng the ResultSort of S) is Element of bool the carrier of S

(S) is Element of bool the carrier of S

(S) is Element of bool the carrier of S

{{},{{}}} is non empty finite V36() countable set

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

bool [:{{}},{{},{{}}}:] is finite V36() countable set

{{}} --> {} is non empty Relation-like {{}} -defined {{}} -valued Function-like constant total V29({{}},{{}}) finite Function-yielding V41() countable DecoratedTree-like Element of bool [:{{}},{{}}:]

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

bool [:{{}},{{}}:] is finite V36() countable set

{{},{{}}} * is non empty functional FinSequence-membered M8({{},{{}}})

[:{{}},({{},{{}}} *):] is Relation-like set

bool [:{{}},({{},{{}}} *):] is set

X is Relation-like {{}} -defined {{},{{}}} * -valued Function-like V29({{}},{{},{{}}} * ) finite Function-yielding V41() countable DecoratedTree-like Element of bool [:{{}},({{},{{}}} *):]

S is Relation-like {{}} -defined {{},{{}}} -valued Function-like V29({{}},{{},{{}}}) finite countable DecoratedTree-like Element of bool [:{{}},{{},{{}}}:]

ManySortedSign(# {{},{{}}},{{}},X,S #) is non empty V55() strict ManySortedSign

v is non empty V55() strict ManySortedSign

the carrier of v is non empty set

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

the carrier' of v is set

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

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

rng the ResultSort of v is Element of bool the carrier of v

bool the carrier of v is set

(v) is Element of bool the carrier of v

the carrier of v \ (rng the ResultSort of v) is Element of bool the carrier of v

S is non empty V55() () ManySortedSign

(S) is Element of bool the carrier of S

the carrier of S is non empty set

bool 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 V29( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is set

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

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

rng the ResultSort of S is Element of bool the carrier of S

the carrier of S \ (rng the ResultSort of S) is Element of bool the carrier of S

S is non empty non void V55() ManySortedSign

(S) is Element of bool the carrier of S

the carrier of S is non empty set

bool 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 V29( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

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

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

rng the ResultSort of S is Element of bool the carrier of S

dom the ResultSort of S is Element of bool the carrier' of S

bool the carrier' of S is set

S is non empty V55() ManySortedSign

(S) is Element of bool the carrier of S

the carrier of S is non empty set

bool 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 V29( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is set

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

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

rng the ResultSort of S is Element of bool the carrier of S

the carrier of S \ (rng the ResultSort of S) is Element of bool the carrier of S

X is non-empty MSAlgebra over S

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

product the Sorts of X is non empty functional with_common_domain product-like set

the non empty Relation-like the carrier of S -defined Function-like the Sorts of X -compatible total Element of product the Sorts of X is non empty Relation-like the carrier of S -defined Function-like the Sorts of X -compatible total Element of product the Sorts of X

the non empty Relation-like the carrier of S -defined Function-like the Sorts of X -compatible total Element of product the Sorts of X | (S) is Relation-like (S) -defined the carrier of S -defined (S) -defined Function-like the Sorts of X -compatible total Element of sproduct the Sorts of X

sproduct the Sorts of X is non empty functional set

dom the Sorts of X is non empty Element of bool the carrier of S

dt is Relation-like (S) -defined Function-like total set

domdt is Element of the carrier of S

dt . domdt is set

the Sorts of X . domdt is non empty set

the non empty Relation-like the carrier of S -defined Function-like the Sorts of X -compatible total Element of product the Sorts of X . domdt is set

c

dom c

S is non empty V55() ManySortedSign

X is non empty non void V55() ManySortedSign

the carrier' of X is non empty set

v is Element of the carrier' of X

the_result_sort_of v is Element of the carrier of X

the carrier of X is non empty set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V29( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

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

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

the ResultSort of X . v is Element of the carrier of X

e is Element of the carrier' of X

the_result_sort_of e is Element of the carrier of X

the ResultSort of X . e is Element of the carrier of X

{{}} * is non empty functional FinSequence-membered M8({{}})

[:{{}},({{}} *):] is Relation-like set

bool [:{{}},({{}} *):] is set

{{}} --> {} is non empty Relation-like {{}} -defined {{}} -valued Function-like constant total V29({{}},{{}}) finite Function-yielding V41() countable DecoratedTree-like Element of bool [:{{}},{{}}:]

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

bool [:{{}},{{}}:] is finite V36() countable set

S is Relation-like {{}} -defined {{}} * -valued Function-like V29({{}},{{}} * ) finite Function-yielding V41() countable DecoratedTree-like Element of bool [:{{}},({{}} *):]

X is Relation-like {{}} -defined {{}} -valued Function-like V29({{}},{{}}) finite Function-yielding V41() countable DecoratedTree-like Element of bool [:{{}},{{}}:]

ManySortedSign(# {{}},{{}},S,X #) is non empty V55() strict ManySortedSign

v is non empty V55() strict ManySortedSign

e is non empty non void V55() ManySortedSign

the carrier' of e is non empty set

dt is Element of the carrier' of e

the_result_sort_of dt is Element of the carrier of e

the carrier of e is non empty set

the ResultSort of e is Relation-like the carrier' of e -defined the carrier of e -valued Function-like V29( the carrier' of e, the carrier of e) Element of bool [: the carrier' of e, the carrier of e:]

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

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

the ResultSort of e . dt is Element of the carrier of e

domdt is Element of the carrier' of e

the_result_sort_of domdt is Element of the carrier of e

the ResultSort of e . domdt is Element of the carrier of e

S is non empty non void V55() () ManySortedSign

the carrier of S is non empty set

X is Element of the carrier of S

(S) is non empty Element of bool the carrier of S

bool 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 V29( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]

the carrier' of S is non empty set

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

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

rng the ResultSort of S is Element of bool the carrier of S

dom the ResultSort of S is Element of bool the carrier' of S

bool the carrier' of S is set

v is set

the ResultSort of S . v is set

e is Element of the carrier' of S

the_result_sort_of e is Element of the carrier of S

the ResultSort of S . e is Element of the carrier of S

v is Element of the carrier' of S

the_result_sort_of v is Element of the carrier of S

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

e is Element of the carrier' of S

the_result_sort_of e is Element of the carrier of S

the ResultSort of S . e is Element of the carrier of S

S is non empty non void V55() ManySortedSign

the carrier' of S is non empty set

the carrier of S is non empty set

X is MSAlgebra over S

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

v is Element of the carrier' of S

the_arity_of v is Relation-like K37() -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S *

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

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding V41() 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 Arity of S . v is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S *

len (the_arity_of v) is V7() V8() V9() V13() Element of K37()

Args (v,X) is Element of rng ( the Sorts of X #)

the Sorts of X # is non empty Relation-like the carrier of S * -defined Function-like total set

rng ( the Sorts of X #) is non empty set

the Arity of S * ( the Sorts of X #) is non empty Relation-like the carrier' of S -defined Function-like total set

( the Arity of S * ( the Sorts of X #)) . v is set

e is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable set

len e is V7() V8() V9() V13() Element of K37()

dom e is finite countable Element of bool K37()

(the_arity_of v) * the Sorts of X is Relation-like K37() -defined Function-like finite countable set

dom (the_arity_of v) is finite countable Element of bool K37()

rng (the_arity_of v) is finite countable Element of bool the carrier of S

bool the carrier of S is set

dom the Sorts of X is non empty Element of bool the carrier of S

dom ((the_arity_of v) * the Sorts of X) is finite countable Element of bool K37()

domdt is set

c

((the_arity_of v) * the Sorts of X) . c

(the_arity_of v) . c

the Sorts of X . ((the_arity_of v) . c

(the_arity_of v) /. c

the Sorts of X . ((the_arity_of v) /. c

e . domdt is set

((the_arity_of v) * the Sorts of X) . domdt is set

dom the Arity of S is Element of bool the carrier' of S

bool the carrier' of S is set

( the Sorts of X #) . (the_arity_of v) is set

product ((the_arity_of v) * the Sorts of X) is functional with_common_domain product-like set

S is non empty non void V55() ManySortedSign

X is non-empty MSAlgebra over S

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

the carrier of S is non empty set

FreeMSA the Sorts of X is strict non-empty MSAlgebra over S

S is non empty non void V55() ManySortedSign

the carrier of S is non empty set

X is non-empty MSAlgebra over S

(S,X) is strict non-empty free MSAlgebra over S

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

FreeMSA the Sorts of X is strict non-empty MSAlgebra over S

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

FreeGen the Sorts of X is non empty Relation-like the carrier of S -defined Function-like total GeneratorSet of FreeMSA the Sorts of X

v is non empty Relation-like the carrier of S -defined Function-like total free GeneratorSet of (S,X)

e is set

dt is Element of the carrier of S

v . dt is set

the Sorts of X . dt is non empty set

domdt is set

FreeGen (dt, the Sorts of X) is non empty Element of bool ((FreeSort the Sorts of X) . dt)

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

(FreeSort the Sorts of X) . dt is non empty set

bool ((FreeSort the Sorts of X) . dt) is set

domdt is Relation-like Function-like set

dom domdt is set

rng domdt is set

[:(v . dt),( the Sorts of X . dt):] is Relation-like set

bool [:(v . dt),( the Sorts of X . dt):] is set

c

p is set

x is set

[x,dt] is set

{x,dt} is non empty finite countable set

{x} is non empty finite countable set

{{x,dt},{x}} is non empty finite V36() countable set

root-tree [x,dt] is Relation-like Function-like finite countable DecoratedTree-like set

c

domdt . p is set

[(domdt . p),dt] is set

{(domdt . p),dt} is non empty finite countable set

{(domdt . p)} is non empty finite countable set

{{(domdt . p),dt},{(domdt . p)}} is non empty finite V36() countable set

root-tree [(domdt . p),dt] is Relation-like Function-like finite countable DecoratedTree-like set

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

dt is set

dom e is non empty Element of bool the carrier of S

bool the carrier of S is set

e . dt is set

domdt is Element of the carrier of S

v . domdt is set

the Sorts of X . domdt is non empty set

[:(v . domdt),( the Sorts of X . domdt):] is Relation-like set

bool [:(v . domdt),( the Sorts of X . domdt):] is set

c

domdt is set

dt is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V41() set

dt . domdt is Relation-like Function-like set

v . domdt is set

the Sorts of X . domdt is set

[:(v . domdt),( the Sorts of X . domdt):] is Relation-like set

bool [:(v . domdt),( the Sorts of X . domdt):] is set

c

v . c

the Sorts of X . c

[:(v . c

bool [:(v . c

x is Relation-like v . c

domdt is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V41() ManySortedFunction of v, the Sorts of X

c

c

x is Element of the carrier of S

FreeSort ( the Sorts of X,x) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA the Sorts of X))

DTConMSA the Sorts of X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

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

the carrier of (DTConMSA the Sorts of X) is non empty set

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

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

bool (TS (DTConMSA the Sorts of X)) is set

the Sorts of X . x is non empty set

c

the Sorts of (S,X) . x is non empty set

[:( the Sorts of (S,X) . x),( the Sorts of X . x):] is Relation-like set

bool [:( the Sorts of (S,X) . x),( the Sorts of X . x):] is set

o9 is set

p is set

[p,x] is set

{p,x} is non empty finite countable set

{p} is non empty finite countable set

{{p,x},{p}} is non empty finite V36() countable set

root-tree [p,x] is Relation-like Function-like finite countable DecoratedTree-like set

(c

v . x is set

domdt . x is Relation-like v . x -defined the Sorts of X . x -valued Function-like V29(v . x, the Sorts of X . x) Element of bool [:(v . x),( the Sorts of X . x):]

[:(v . x),( the Sorts of X . x):] is Relation-like set

bool [:(v . x),( the Sorts of X . x):] is set

FreeGen (x, the Sorts of X) is non empty Element of bool ((FreeSort the Sorts of X) . x)

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

(FreeSort the Sorts of X) . x is non empty set

bool ((FreeSort the Sorts of X) . x) is set

(c

((c

(domdt . x) . o9 is set

ts is Element of the carrier of S

v . ts is set

the Sorts of X . ts is non empty set

[:(v . ts),( the Sorts of X . ts):] is Relation-like set

bool [:(v . ts),( the Sorts of X . ts):] is set

ts is Relation-like v . ts -defined the Sorts of X . ts -valued Function-like V29(v . ts, the Sorts of X . ts) Element of bool [:(v . ts),( the Sorts of X . ts):]

v is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Sorts of (S,X), the Sorts of X

e is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Sorts of (S,X), the Sorts of X

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

dt is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Sorts of (FreeMSA the Sorts of X), the Sorts of X

c

FreeGen (c

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

(FreeSort the Sorts of X) . c

bool ((FreeSort the Sorts of X) . c

dt . c

the Sorts of (FreeMSA the Sorts of X) . c

the Sorts of X . c

[:( the Sorts of (FreeMSA the Sorts of X) . c

bool [:( the Sorts of (FreeMSA the Sorts of X) . c

p is set

(dt . c

x is set

[x,c

{x,c

{x} is non empty finite countable set

{{x,c

root-tree [x,c

o9 is set

[o9,c

{o9,c

{o9} is non empty finite countable set

{{o9,c

root-tree [o9,c

FreeSort ( the Sorts of X,c

DTConMSA the Sorts of X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

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

the carrier of (DTConMSA the Sorts of X) is non empty set

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

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

bool (TS (DTConMSA the Sorts of X)) is set

domdt is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Sorts of (FreeMSA the Sorts of X), the Sorts of X

c

FreeGen (c

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

(FreeSort the Sorts of X) . c

bool ((FreeSort the Sorts of X) . c

domdt . c

the Sorts of (FreeMSA the Sorts of X) . c

the Sorts of X . c

[:( the Sorts of (FreeMSA the Sorts of X) . c

bool [:( the Sorts of (FreeMSA the Sorts of X) . c

p is set

(domdt . c

x is set

[x,c

{x,c

{x} is non empty finite countable set

{{x,c

root-tree [x,c

o9 is set

[o9,c

{o9,c

{o9} is non empty finite countable set

{{o9,c

root-tree [o9,c

FreeSort ( the Sorts of X,c

DTConMSA the Sorts of X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

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

the carrier of (DTConMSA the Sorts of X) is non empty set

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

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

bool (TS (DTConMSA the Sorts of X)) is set

S is non empty non void V55() ManySortedSign

the carrier of S is non empty set

X is non-empty MSAlgebra over S

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

the Charact of X is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ( the Sorts of X #), the ResultSort of S * the Sorts of X

the carrier' of S is non empty set

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding V41() Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

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

the Sorts of X # is non empty Relation-like the carrier of S * -defined Function-like total set

the Arity of S * ( the Sorts of X #) is non empty Relation-like the carrier' of S -defined Function-like total set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( 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 * the Sorts of X is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

MSAlgebra(# the Sorts of X, the Charact of X #) is strict non-empty MSAlgebra over S

v is non-empty MSAlgebra over S

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

e is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total ManySortedSubset of the Sorts of v

GenMSAlg e is strict non-empty MSSubAlgebra of v

the Sorts of (GenMSAlg e) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

domdt is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of X

c

x is Element of the carrier' of S

Result (x,MSAlgebra(# the Sorts of X, the Charact of X #)) is non empty Element of rng the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #)

the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

rng the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) is non empty set

the ResultSort of S * the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

( the ResultSort of S * the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #)) . x is non empty set

Args (x,MSAlgebra(# the Sorts of X, the Charact of X #)) is non empty Element of rng ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #)

the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) # is non empty Relation-like the carrier of S * -defined Function-like total set

rng ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #) is non empty set

the Arity of S * ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #) is non empty Relation-like the carrier' of S -defined Function-like total set

( the Arity of S * ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #)) . x is set

Den (x,MSAlgebra(# the Sorts of X, the Charact of X #)) is Relation-like Args (x,MSAlgebra(# the Sorts of X, the Charact of X #)) -defined Result (x,MSAlgebra(# the Sorts of X, the Charact of X #)) -valued Function-like V29( Args (x,MSAlgebra(# the Sorts of X, the Charact of X #)), Result (x,MSAlgebra(# the Sorts of X, the Charact of X #))) Element of bool [:(Args (x,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (x,MSAlgebra(# the Sorts of X, the Charact of X #))):]

[:(Args (x,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (x,MSAlgebra(# the Sorts of X, the Charact of X #))):] is Relation-like set

bool [:(Args (x,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (x,MSAlgebra(# the Sorts of X, the Charact of X #))):] is set

the Charact of MSAlgebra(# the Sorts of X, the Charact of X #) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #), the ResultSort of S * the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #)

the Charact of MSAlgebra(# the Sorts of X, the Charact of X #) . x is Relation-like Function-like set

c

the Arity of S * (c

( the Arity of S * (c

(Den (x,MSAlgebra(# the Sorts of X, the Charact of X #))) | (( the Arity of S * (c

rng ((Den (x,MSAlgebra(# the Sorts of X, the Charact of X #))) | (( the Arity of S * (c

bool (Result (x,MSAlgebra(# the Sorts of X, the Charact of X #))) is set

the ResultSort of S * c

( the ResultSort of S * c

Args (x,X) is non empty Element of rng ( the Sorts of X #)

rng ( the Sorts of X #) is non empty set

( the Arity of S * ( the Sorts of X #)) . x is set

Result (x,X) is non empty Element of rng the Sorts of X

rng the Sorts of X is non empty set

( the ResultSort of S * the Sorts of X) . x is non empty set

Den (x,X) is Relation-like Args (x,X) -defined Result (x,X) -valued Function-like V29( Args (x,X), Result (x,X)) Element of bool [:(Args (x,X)),(Result (x,X)):]

[:(Args (x,X)),(Result (x,X)):] is Relation-like set

bool [:(Args (x,X)),(Result (x,X)):] is set

the Charact of X . x is Relation-like Function-like set

Opers (X,domdt) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (domdt #), the ResultSort of S * domdt

domdt # is non empty Relation-like the carrier of S * -defined Function-like total set

the Arity of S * (domdt #) is non empty Relation-like the carrier' of S -defined Function-like total set

the ResultSort of S * domdt is non empty Relation-like the carrier' of S -defined Function-like total set

p is Element of the carrier' of S

Args (p,X) is non empty Element of rng ( the Sorts of X #)

( the Arity of S * ( the Sorts of X #)) . p is set

Result (p,X) is non empty Element of rng the Sorts of X

( the ResultSort of S * the Sorts of X) . p is non empty set

Args (p,MSAlgebra(# the Sorts of X, the Charact of X #)) is non empty Element of rng ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #)

( the Arity of S * ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #)) . p is set

Result (p,MSAlgebra(# the Sorts of X, the Charact of X #)) is non empty Element of rng the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #)

( the ResultSort of S * the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #)) . p is non empty set

Den (p,X) is Relation-like Args (p,X) -defined Result (p,X) -valued Function-like V29( Args (p,X), Result (p,X)) Element of bool [:(Args (p,X)),(Result (p,X)):]

[:(Args (p,X)),(Result (p,X)):] is Relation-like set

bool [:(Args (p,X)),(Result (p,X)):] is set

the Charact of X . p is Relation-like Function-like set

Den (p,MSAlgebra(# the Sorts of X, the Charact of X #)) is Relation-like Args (p,MSAlgebra(# the Sorts of X, the Charact of X #)) -defined Result (p,MSAlgebra(# the Sorts of X, the Charact of X #)) -valued Function-like V29( Args (p,MSAlgebra(# the Sorts of X, the Charact of X #)), Result (p,MSAlgebra(# the Sorts of X, the Charact of X #))) Element of bool [:(Args (p,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (p,MSAlgebra(# the Sorts of X, the Charact of X #))):]

[:(Args (p,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (p,MSAlgebra(# the Sorts of X, the Charact of X #))):] is Relation-like set

bool [:(Args (p,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (p,MSAlgebra(# the Sorts of X, the Charact of X #))):] is set

the Charact of MSAlgebra(# the Sorts of X, the Charact of X #) . p is Relation-like Function-like set

x is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (c

x . p is Relation-like ( the Arity of S * (c

( the Arity of S * (c

( the ResultSort of S * c

[:(( the Arity of S * (c

bool [:(( the Arity of S * (c

p /. domdt is Relation-like ( the Arity of S * (domdt #)) . p -defined ( the ResultSort of S * domdt) . p -valued Function-like V29(( the Arity of S * (domdt #)) . p,( the ResultSort of S * domdt) . p) Element of bool [:(( the Arity of S * (domdt #)) . p),(( the ResultSort of S * domdt) . p):]

( the Arity of S * (domdt #)) . p is set

( the ResultSort of S * domdt) . p is set

[:(( the Arity of S * (domdt #)) . p),(( the ResultSort of S * domdt) . p):] is Relation-like set

bool [:(( the Arity of S * (domdt #)) . p),(( the ResultSort of S * domdt) . p):] is set

(Den (p,X)) | (( the Arity of S * (domdt #)) . p) is Relation-like Args (p,X) -defined ( the Arity of S * (domdt #)) . p -defined Args (p,X) -defined Result (p,X) -valued Function-like Element of bool [:(Args (p,X)),(Result (p,X)):]

p /. c

the Charact of (GenMSAlg e) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ( the Sorts of (GenMSAlg e) #), the ResultSort of S * the Sorts of (GenMSAlg e)

the Sorts of (GenMSAlg e) # is non empty Relation-like the carrier of S * -defined Function-like total set

the Arity of S * ( the Sorts of (GenMSAlg e) #) is non empty Relation-like the carrier' of S -defined Function-like total set

the ResultSort of S * the Sorts of (GenMSAlg e) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set

Opers (v,c

p is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of v

x is MSSubAlgebra of X

the Sorts of x is non empty Relation-like the carrier of S -defined Function-like total set

o9 is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of X

ts is Element of the carrier' of S

Result (ts,X) is non empty Element of rng the Sorts of X

( the ResultSort of S * the Sorts of X) . ts is non empty set

Args (ts,X) is non empty Element of rng ( the Sorts of X #)

( the Arity of S * ( the Sorts of X #)) . ts is set

Den (ts,X) is Relation-like Args (ts,X) -defined Result (ts,X) -valued Function-like V29( Args (ts,X), Result (ts,X)) Element of bool [:(Args (ts,X)),(Result (ts,X)):]

[:(Args (ts,X)),(Result (ts,X)):] is Relation-like set

bool [:(Args (ts,X)),(Result (ts,X)):] is set

the Charact of X . ts is Relation-like Function-like set

o9 # is non empty Relation-like the carrier of S * -defined Function-like total set

the Arity of S * (o9 #) is non empty Relation-like the carrier' of S -defined Function-like total set

( the Arity of S * (o9 #)) . ts is set

(Den (ts,X)) | (( the Arity of S * (o9 #)) . ts) is Relation-like Args (ts,X) -defined ( the Arity of S * (o9 #)) . ts -defined Args (ts,X) -defined Result (ts,X) -valued Function-like Element of bool [:(Args (ts,X)),(Result (ts,X)):]

rng ((Den (ts,X)) | (( the Arity of S * (o9 #)) . ts)) is Element of bool (Result (ts,X))

bool (Result (ts,X)) is set

the ResultSort of S * o9 is non empty Relation-like the carrier' of S -defined Function-like total set

( the ResultSort of S * o9) . ts is set

Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) is non empty Element of rng ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #)

( the Arity of S * ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #)) . ts is set

Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) is non empty Element of rng the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #)

( the ResultSort of S * the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #)) . ts is non empty set

Den (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) is Relation-like Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) -defined Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) -valued Function-like V29( Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #)), Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #))) Element of bool [:(Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #))):]

[:(Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #))):] is Relation-like set

bool [:(Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #))):] is set

the Charact of MSAlgebra(# the Sorts of X, the Charact of X #) . ts is Relation-like Function-like set

Opers (v,p) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (p #), the ResultSort of S * p

p # is non empty Relation-like the carrier of S * -defined Function-like total set

the Arity of S * (p #) is non empty Relation-like the carrier' of S -defined Function-like total set

the ResultSort of S * p is non empty Relation-like the carrier' of S -defined Function-like total set

ts is Element of the carrier' of S

Args (ts,X) is non empty Element of rng ( the Sorts of X #)

( the Arity of S * ( the Sorts of X #)) . ts is set

Result (ts,X) is non empty Element of rng the Sorts of X

( the ResultSort of S * the Sorts of X) . ts is non empty set

Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) is non empty Element of rng ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #)

( the Arity of S * ( the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #) #)) . ts is set

Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) is non empty Element of rng the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #)

( the ResultSort of S * the Sorts of MSAlgebra(# the Sorts of X, the Charact of X #)) . ts is non empty set

Den (ts,X) is Relation-like Args (ts,X) -defined Result (ts,X) -valued Function-like V29( Args (ts,X), Result (ts,X)) Element of bool [:(Args (ts,X)),(Result (ts,X)):]

[:(Args (ts,X)),(Result (ts,X)):] is Relation-like set

bool [:(Args (ts,X)),(Result (ts,X)):] is set

the Charact of X . ts is Relation-like Function-like set

Den (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) is Relation-like Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) -defined Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #)) -valued Function-like V29( Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #)), Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #))) Element of bool [:(Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #))):]

[:(Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #))):] is Relation-like set

bool [:(Args (ts,MSAlgebra(# the Sorts of X, the Charact of X #))),(Result (ts,MSAlgebra(# the Sorts of X, the Charact of X #))):] is set

the Charact of MSAlgebra(# the Sorts of X, the Charact of X #) . ts is Relation-like Function-like set

ts is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (o9 #), the ResultSort of S * o9

ts . ts is Relation-like ( the Arity of S * (o9 #)) . ts -defined ( the ResultSort of S * o9) . ts -valued Function-like V29(( the Arity of S * (o9 #)) . ts,( the ResultSort of S * o9) . ts) Element of bool [:(( the Arity of S * (o9 #)) . ts),(( the ResultSort of S * o9) . ts):]

( the Arity of S * (o9 #)) . ts is set

( the ResultSort of S * o9) . ts is set

[:(( the Arity of S * (o9 #)) . ts),(( the ResultSort of S * o9) . ts):] is Relation-like set

bool [:(( the Arity of S * (o9 #)) . ts),(( the ResultSort of S * o9) . ts):] is set

ts /. p is Relation-like ( the Arity of S * (p #)) . ts -defined ( the ResultSort of S * p) . ts -valued Function-like V29(( the Arity of S * (p #)) . ts,( the ResultSort of S * p) . ts) Element of bool [:(( the Arity of S * (p #)) . ts),(( the ResultSort of S * p) . ts):]

( the Arity of S * (p #)) . ts is set

( the ResultSort of S * p) . ts is set

[:(( the Arity of S * (p #)) . ts),(( the ResultSort of S * p) . ts):] is Relation-like set

bool [:(( the Arity of S * (p #)) . ts),(( the ResultSort of S * p) . ts):] is set

(Den (ts,X)) | (( the Arity of S * (p #)) . ts) is Relation-like Args (ts,X) -defined ( the Arity of S * (p #)) . ts -defined Args (ts,X) -defined Result (ts,X) -valued Function-like Element of bool [:(Args (ts,X)),(Result (ts,X)):]

ts /. o9 is Relation-like ( the Arity of S * (o9 #)) . ts -defined ( the ResultSort of S * o9) . ts -valued Function-like V29(( the Arity of S * (o9 #)) . ts,( the ResultSort of S * o9) . ts) Element of bool [:(( the Arity of S * (o9 #)) . ts),(( the ResultSort of S * o9) . ts):]

the Charact of x is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ( the Sorts of x #), the ResultSort of S * the Sorts of x

the Sorts of x # is non empty Relation-like the carrier of S * -defined Function-like total set

the Arity of S * ( the Sorts of x #) is non empty Relation-like the carrier' of S -defined Function-like total set

the ResultSort of S * the Sorts of x is non empty Relation-like the carrier' of S -defined Function-like total set

Opers (X,o9) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (o9 #), the ResultSort of S * o9

c

domdt is strict non-empty MSSubAlgebra of X

p is MSSubAlgebra of v

GenMSAlg c

the Sorts of (GenMSAlg c

S is non empty V55() ManySortedSign

S is non empty V55() ManySortedSign

S is non empty V55() ManySortedSign

X is non-empty MSAlgebra over S

v is non empty non void V55() ManySortedSign

the carrier of v is non empty set

e is MSAlgebra over v

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

the carrier of S is non empty set

dt is non empty Relation-like the carrier of v -defined Function-like total GeneratorSet of e

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

the carrier of S is non empty set

S is non empty V55() ManySortedSign

the carrier of S is non empty set

the carrier of S --> {{}} is non empty Relation-like non-empty non empty-yielding the carrier of S -defined {{{}}} -valued Function-like constant total V29( the carrier of S,{{{}}}) Element of bool [: the carrier of S,{{{}}}:]

{{{}}} is non empty finite V36() countable set

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

bool [: the carrier of S,{{{}}}:] is set

the carrier' of S is set

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding V41() Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

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

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

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

the Arity of S * (X #) is Relation-like the carrier' of S -defined Function-like total set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( 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 * X is Relation-like the carrier' of S -defined Function-like total set

the Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (X #), the ResultSort of S * X is Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (X #), the ResultSort of S * X

MSAlgebra(# X, the Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (X #), the ResultSort of S * X #) is strict MSAlgebra over S

the Sorts of MSAlgebra(# X, the Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (X #), the ResultSort of S * X #) is non empty Relation-like the carrier of S -defined Function-like total set

X is strict MSAlgebra over S

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

v is strict MSAlgebra over S

the Sorts of v is non empty Relation-like the carrier of S -defined Function-like total 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 V29( 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

dom the ResultSort of S is Element of bool the carrier' of S

bool the carrier' of S is set

the ResultSort of S * the Sorts of X is Relation-like the carrier' of S -defined Function-like total set

dt is set

( the ResultSort of S * the Sorts of X) . dt is set

the ResultSort of S . dt is set

the Sorts of X . ( the ResultSort of S . dt) is set

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Function-yielding V41() Element of bool [: the carrier' of S,( the carrier of S *):]

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

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

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

the Sorts of X # is non empty Relation-like the carrier of S * -defined Function-like total set

the Arity of S * ( the Sorts of X #) is Relation-like the carrier' of S -defined Function-like total set

( the Arity of S * ( the Sorts of X #)) . dt is set

c

[:(( the Arity of S * ( the Sorts of X #)) . dt),c

bool [:(( the Arity of S * ( the Sorts of X #)) . dt),c

the Charact of X is Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ( the Sorts of X #), the ResultSort of S * the Sorts of X

the Charact of X . dt is Relation-like Function-like set

the Charact of v is Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ( the Sorts of v #), the ResultSort of S * the Sorts of v

the Sorts of v # is non empty Relation-like the carrier of S * -defined Function-like total set

the Arity of S * ( the Sorts of v #) is Relation-like the carrier' of S -defined Function-like total set

the ResultSort of S * the Sorts of v is Relation-like the carrier' of S -defined Function-like total set

the Charact of v . dt is Relation-like Function-like set

o9 is set

x is Relation-like ( the Arity of S * ( the Sorts of X #)) . dt -defined c

x . o9 is set

p is Relation-like ( the Arity of S * ( the Sorts of X #)) . dt -defined c

p . o9 is set

S is non empty V55() ManySortedSign

(S) is strict MSAlgebra over S

X is strict MSAlgebra over S

the carrier of S is non empty set

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

the carrier of S --> {{}} is non empty Relation-like non-empty non empty-yielding the carrier of S -defined {{{}}} -valued Function-like constant total V29( the carrier of S,{{{}}}) Element of bool [: the carrier of S,{{{}}}:]

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

bool [: the carrier of S,{{{}}}:] is set

v is set

the Sorts of X . v is set

{{}} * is non empty functional FinSequence-membered M8({{}})

[{},{{}}] is set

{{},{{}}} is non empty finite V36() countable set

{{{},{{}}},{{}}} is non empty finite V36() countable set

{[{},{{}}]} is non empty Relation-like Function-like finite countable set

[:{[{},{{}}]},({{}} *):] is Relation-like set

bool [:{[{},{{}}]},({{}} *):] is set

{[{},{{}}]} --> {} is non empty Relation-like {[{},{{}}]} -defined {{}} -valued Function-like constant total V29({[{},{{}}]},{{}}) finite Function-yielding V41() countable Element of bool [:{[{},{{}}]},{{}}:]

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

bool [:{[{},{{}}]},{{}}:] is finite V36() countable set

S is Relation-like {[{},{{}}]} -defined {{}} * -valued Function-like V29({[{},{{}}]},{{}} * ) finite Function-yielding V41() countable Element of bool [:{[{},{{}}]},({{}} *):]

X is Relation-like {[{},{{}}]} -defined {{}} -valued Function-like V29({[{},{{}}]},{{}}) finite Function-yielding V41() countable Element of bool [:{[{},{{}}]},{{}}:]

ManySortedSign(# {{}},{[{},{{}}]},S,X #) is non empty V55() strict ManySortedSign

v is non empty V55() strict ManySortedSign

dt is non-empty (v) MSAlgebra over v

e is non empty non void V55() ManySortedSign

the carrier of e is non empty set

the Element of the carrier of e is Element of the carrier of e

domdt is non-empty MSAlgebra over e

x is non empty Relation-like the carrier of e -defined Function-like total GeneratorSet of domdt

x . the Element of the carrier of e is set

the carrier' of e is non empty set

the Element of the carrier' of e is Element of the carrier' of e

Den ( the Element of the carrier' of e,domdt) is Relation-like Args ( the Element of the carrier' of e,domdt) -defined Result ( the Element of the carrier' of e,domdt) -valued Function-like V29( Args ( the Element of the carrier' of e,domdt), Result ( the Element of the carrier' of e,domdt)) Element of bool [:(Args ( the Element of the carrier' of e,domdt)),(Result ( the Element of the carrier' of e,domdt)):]

Args ( the Element of the carrier' of e,domdt) is non empty Element of rng ( the Sorts of domdt #)

the Sorts of domdt is non empty Relation-like non-empty non empty-yielding the carrier of e -defined Function-like total set

the Sorts of domdt # is non empty Relation-like the carrier of e * -defined Function-like total set

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

rng ( the Sorts of domdt #) is non empty set

the Arity of e is Relation-like the carrier' of e -defined the carrier of e * -valued Function-like V29( the carrier' of e, the carrier of e * ) Function-yielding V41() Element of bool [: the carrier' of e,( the carrier of e *):]

[: the carrier' of e,( the carrier of e *):] is Relation-like set

bool [: the carrier' of e,( the carrier of e *):] is set

the Arity of e * ( the Sorts of domdt #) is non empty Relation-like the carrier' of e -defined Function-like total set

( the Arity of e * ( the Sorts of domdt #)) . the Element of the carrier' of e is set

Result ( the Element of the carrier' of e,domdt) is non empty Element of rng the Sorts of domdt

rng the Sorts of domdt is non empty set

the ResultSort of e is Relation-like the carrier' of e -defined the carrier of e -valued Function-like V29( the carrier' of e, the carrier of e) Element of bool [: the carrier' of e, the carrier of e:]

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

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

the ResultSort of e * the Sorts of domdt is non empty Relation-like non-empty non empty-yielding the carrier' of e -defined Function-like total set

( the ResultSort of e * the Sorts of domdt) . the Element of the carrier' of e is non empty set

[:(Args ( the Element of the carrier' of e,domdt)),(Result ( the Element of the carrier' of e,domdt)):] is Relation-like set

bool [:(Args ( the Element of the carrier' of e,domdt)),(Result ( the Element of the carrier' of e,domdt)):] is set

the Charact of domdt is non empty Relation-like the carrier' of e -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of e * ( the Sorts of domdt #), the ResultSort of e * the Sorts of domdt

the Charact of domdt . the Element of the carrier' of e is Relation-like Function-like set

(Den ( the Element of the carrier' of e,domdt)) . {} is set

{((Den ( the Element of the carrier' of e,domdt)) . {})} is non empty finite countable set

(x . the Element of the carrier of e) \/ {((Den ( the Element of the carrier' of e,domdt)) . {})} is non empty set

the Element of the carrier of e .--> ((x . the Element of the carrier of e) \/ {((Den ( the Element of the carrier' of e,domdt)) . {})}) is Relation-like the carrier of e -defined { the Element of the carrier of e} -defined Function-like one-to-one finite countable set

{ the Element of the carrier of e} is non empty finite countable set

{ the Element of the carrier of e} --> ((x . the Element of the carrier of e) \/ {((Den ( the Element of the carrier' of e,domdt)) . {})}) is non empty Relation-like non-empty non empty-yielding { the Element of the carrier of e} -defined {((x . the Element of the carrier of e) \/ {((Den ( the Element of the carrier' of e,domdt)) . {})})} -valued Function-like constant total V29({ the Element of the carrier of e},{((x . the Element of the carrier of e) \/ {((Den ( the Element of the carrier' of e,domdt)) . {})})}) finite countable Element of bool [:{ the Element of the carrier of e},{((x . the Element of the carrier of e) \/ {((Den ( the Element of the carrier' of e,domdt)) . {})})}:]

{((x . the Element of the carrier of e) \/ {((Den ( the Element of the carrier' of e,domdt)) . {})})} is non empty finite countable set

[:{ the Element of the carrier of e},{((x . the Element of the carrier of e) \/ {((Den ( the Element of the carrier' of e,domdt)) . {})})}:] is Relation-like finite countable set

bool [:{ the Element of the carrier of e},{((x . the Element of the carrier of e) \/ {((Den ( the Element of the carrier' of e,domdt)) . {})})}:] is finite V36() countable set

the Element of the carrier' of e .--> (Den ( the Element of the carrier' of e,domdt)) is Relation-like the carrier' of e -defined { the Element of the carrier' of e} -defined Function-like one-to-one finite Function-yielding V41() countable set

{ the Element of the carrier' of e} is non empty finite countable set

{ the Element of the carrier' of e} --> (Den ( the Element of the carrier' of e,domdt)) is non empty Relation-like { the Element of the carrier' of e} -defined {(Den ( the Element of the carrier' of e,domdt))} -valued Function-like constant total V29({ the Element of the carrier' of e},{(Den ( the Element of the carrier' of e,domdt))}) finite Function-yielding V41() countable Element of bool [:{ the Element of the carrier' of e},{(Den ( the Element of the carrier' of e,domdt))}:]

{(Den ( the Element of the carrier' of e,domdt))} is non empty functional finite with_common_domain countable set

[:{ the Element of the carrier' of e},{(Den ( the Element of the carrier' of e,domdt))}:] is Relation-like finite countable set

bool [:{ the Element of the carrier' of e},{(Den ( the Element of the carrier' of e,domdt))}:] is finite V36() countable set

ts9 is set

the carrier of v is non empty set

the Sorts of dt is non empty Relation-like non-empty non empty-yielding the carrier of v -defined Function-like total set

the Sorts of dt . ts9 is set

b is non empty Relation-like non-empty non empty-yielding the carrier of v -defined Function-like total set

the Arity of v is Relation-like the carrier' of v -defined the carrier of v * -valued Function-like V29( the carrier' of v, the carrier of v * ) Function-yielding V41() Element of bool [: the carrier' of v,( the carrier of v *):]

the carrier' of v is set

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

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

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

the Arity of v . the Element of the carrier' of e is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable set

( the Sorts of domdt #) . ( the Arity of v . the Element of the carrier' of e) is set

<*> the carrier of e is empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined the carrier of e -valued Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of the carrier of e *

( the Sorts of domdt #) . (<*> the carrier of e) is set

dom (Den ( the Element of the carrier' of e,domdt)) is Element of bool (Args ( the Element of the carrier' of e,domdt))

bool (Args ( the Element of the carrier' of e,domdt)) is set

ts is set

b # is non empty Relation-like the carrier of v * -defined Function-like total set

the Arity of v * (b #) is Relation-like the carrier' of v -defined Function-like total set

( the Arity of v * (b #)) . ts is set

the Arity of v . ts is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable set

(b #) . ( the Arity of v . ts) is set

<*> the carrier of v is empty V7() V8() V9() V11() V12() V13() Relation-like non-empty empty-yielding K37() -defined the carrier of v -valued Function-like one-to-one constant functional finite finite-yielding V36() Function-yielding V41() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of the carrier of v *

(b #) . (<*> the carrier of v) is set

[:(( the Arity of v * (b #)) . ts),(Result ( the Element of the carrier' of e,domdt)):] is Relation-like set

bool [:(( the Arity of v * (b #)) . ts),(Result ( the Element of the carrier' of e,domdt)):] is set

( the Element of the carrier' of e .--> (Den ( the Element of the carrier' of e,domdt))) . ts is Relation-like Function-like set

A99 is Relation-like ( the Arity of v * (b #)) . ts -defined Result ( the Element of the carrier' of e,domdt) -valued Function-like V29(( the Arity of v * (b #)) . ts, Result ( the Element of the carrier' of e,domdt)) Element of bool [:(( the Arity of v * (b #)) . ts),(Result ( the Element of the carrier' of e,domdt)):]

rng A99 is Element of bool (Result ( the Element of the carrier' of e,domdt))

bool (Result ( the Element of the carrier' of e,domdt)) is set

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

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

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

the ResultSort of v * b is Relation-like non-empty the carrier' of v -defined Function-like total set

( the ResultSort of v * b) . ts is set

the ResultSort of v . ts is set

b . ( the ResultSort of v . ts) is set

b . the Element of the carrier of e is set

[:(( the Arity of v * (b #)) . ts),(( the ResultSort of v * b) . ts):] is Relation-like set

bool [:(( the Arity of v * (b #)) . ts),(( the ResultSort of v * b) . ts):] is set

A99 is non empty Relation-like the carrier of e -defined Function-like total ManySortedSubset of the Sorts of domdt

ts is Relation-like the carrier' of v -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of v * (b #), the ResultSort of v * b

MSAlgebra(# b,ts #) is strict MSAlgebra over v

the Sorts of MSAlgebra(# b,ts #) is non empty Relation-like the carrier of v -defined Function-like total set

A99 is Element of the carrier' of e

i is set

Den (A99,domdt) is Relation-like Args (A99,domdt) -defined Result (A99,domdt) -valued Function-like V29(