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
{ b1 where b1 is Element of the carrier of S : b1 is with_const_op } is set
bool the carrier of S is set
{ b1 where b1 is Element of the carrier of S : S1[b1] } is set
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
{ b1 where b1 is Element of the carrier of S : b1 is with_const_op } is set
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
c7 is Relation-like Function-like set
dom c7 is set
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
c7 is V7() V8() V9() V13() set
((the_arity_of v) * the Sorts of X) . c7 is set
(the_arity_of v) . c7 is set
the Sorts of X . ((the_arity_of v) . c7) is set
(the_arity_of v) /. c7 is Element of the carrier of S
the Sorts of X . ((the_arity_of v) /. c7) is set
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
c7 is Relation-like v . dt -defined the Sorts of X . dt -valued Function-like V29(v . dt, the Sorts of X . dt) Element of bool [:(v . dt),( the Sorts of X . dt):]
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
c7 . p is set
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
c7 is Relation-like v . domdt -defined the Sorts of X . domdt -valued Function-like V29(v . domdt, the Sorts of X . domdt) Element of bool [:(v . domdt),( the Sorts of X . domdt):]
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
c7 is Element of the carrier of S
v . c7 is set
the Sorts of X . c7 is non empty set
[:(v . c7),( the Sorts of X . c7):] is Relation-like set
bool [:(v . c7),( the Sorts of X . c7):] is set
x is Relation-like v . c7 -defined the Sorts of X . c7 -valued Function-like V29(v . c7, the Sorts of X . c7) Element of bool [:(v . c7),( the Sorts of X . c7):]
domdt is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V41() ManySortedFunction of v, the Sorts of X
c7 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
c7 || v is non empty Relation-like the carrier of S -defined Function-like total Function-yielding V41() ManySortedFunction of v, the Sorts of X
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
c7 . x is Relation-like the Sorts of (S,X) . x -defined the Sorts of X . x -valued Function-like V29( the Sorts of (S,X) . x, the Sorts of X . x) Element of bool [:( the Sorts of (S,X) . x),( the Sorts of X . x):]
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
(c7 . x) . o9 is set
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
(c7 . x) | (v . x) is Relation-like the Sorts of (S,X) . x -defined v . x -defined the Sorts of (S,X) . x -defined the Sorts of X . x -valued Function-like Element of bool [:( the Sorts of (S,X) . x),( the Sorts of X . x):]
((c7 . x) | (v . x)) . o9 is set
(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
c7 is Element of the carrier of S
FreeGen (c7, the Sorts of X) is non empty Element of bool ((FreeSort the Sorts of X) . c7)
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) . c7 is non empty set
bool ((FreeSort the Sorts of X) . c7) is set
dt . c7 is Relation-like the Sorts of (FreeMSA the Sorts of X) . c7 -defined the Sorts of X . c7 -valued Function-like V29( the Sorts of (FreeMSA the Sorts of X) . c7, the Sorts of X . c7) Element of bool [:( the Sorts of (FreeMSA the Sorts of X) . c7),( the Sorts of X . c7):]
the Sorts of (FreeMSA the Sorts of X) . c7 is non empty set
the Sorts of X . c7 is non empty set
[:( the Sorts of (FreeMSA the Sorts of X) . c7),( the Sorts of X . c7):] is Relation-like set
bool [:( the Sorts of (FreeMSA the Sorts of X) . c7),( the Sorts of X . c7):] is set
p is set
(dt . c7) . p is set
x is set
[x,c7] is set
{x,c7} is non empty finite countable set
{x} is non empty finite countable set
{{x,c7},{x}} is non empty finite V36() countable set
root-tree [x,c7] is Relation-like Function-like finite countable DecoratedTree-like set
o9 is set
[o9,c7] is set
{o9,c7} is non empty finite countable set
{o9} is non empty finite countable set
{{o9,c7},{o9}} is non empty finite V36() countable set
root-tree [o9,c7] is Relation-like Function-like finite countable DecoratedTree-like set
FreeSort ( the Sorts of X,c7) 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
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
c7 is Element of the carrier of S
FreeGen (c7, the Sorts of X) is non empty Element of bool ((FreeSort the Sorts of X) . c7)
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) . c7 is non empty set
bool ((FreeSort the Sorts of X) . c7) is set
domdt . c7 is Relation-like the Sorts of (FreeMSA the Sorts of X) . c7 -defined the Sorts of X . c7 -valued Function-like V29( the Sorts of (FreeMSA the Sorts of X) . c7, the Sorts of X . c7) Element of bool [:( the Sorts of (FreeMSA the Sorts of X) . c7),( the Sorts of X . c7):]
the Sorts of (FreeMSA the Sorts of X) . c7 is non empty set
the Sorts of X . c7 is non empty set
[:( the Sorts of (FreeMSA the Sorts of X) . c7),( the Sorts of X . c7):] is Relation-like set
bool [:( the Sorts of (FreeMSA the Sorts of X) . c7),( the Sorts of X . c7):] is set
p is set
(domdt . c7) . p is set
x is set
[x,c7] is set
{x,c7} is non empty finite countable set
{x} is non empty finite countable set
{{x,c7},{x}} is non empty finite V36() countable set
root-tree [x,c7] is Relation-like Function-like finite countable DecoratedTree-like set
o9 is set
[o9,c7] is set
{o9,c7} is non empty finite countable set
{o9} is non empty finite countable set
{{o9,c7},{o9}} is non empty finite V36() countable set
root-tree [o9,c7] is Relation-like Function-like finite countable DecoratedTree-like set
FreeSort ( the Sorts of X,c7) 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
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
c7 is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of v
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
c7 # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * (c7 #) is non empty Relation-like the carrier' of S -defined Function-like total set
( the Arity of S * (c7 #)) . x is set
(Den (x,MSAlgebra(# the Sorts of X, the Charact of X #))) | (( the Arity of S * (c7 #)) . x) is Relation-like Args (x,MSAlgebra(# the Sorts of X, the Charact of X #)) -defined ( the Arity of S * (c7 #)) . x -defined 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 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 #))):]
rng ((Den (x,MSAlgebra(# the Sorts of X, the Charact of X #))) | (( the Arity of S * (c7 #)) . x)) is Element of bool (Result (x,MSAlgebra(# the Sorts of X, the Charact of X #)))
bool (Result (x,MSAlgebra(# the Sorts of X, the Charact of X #))) is set
the ResultSort of S * c7 is non empty Relation-like the carrier' of S -defined Function-like total set
( the ResultSort of S * c7) . x is set
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 * (c7 #), the ResultSort of S * c7
x . p is Relation-like ( the Arity of S * (c7 #)) . p -defined ( the ResultSort of S * c7) . p -valued Function-like V29(( the Arity of S * (c7 #)) . p,( the ResultSort of S * c7) . p) Element of bool [:(( the Arity of S * (c7 #)) . p),(( the ResultSort of S * c7) . p):]
( the Arity of S * (c7 #)) . p is set
( the ResultSort of S * c7) . p is set
[:(( the Arity of S * (c7 #)) . p),(( the ResultSort of S * c7) . p):] is Relation-like set
bool [:(( the Arity of S * (c7 #)) . p),(( the ResultSort of S * c7) . p):] is set
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 /. c7 is Relation-like ( the Arity of S * (c7 #)) . p -defined ( the ResultSort of S * c7) . p -valued Function-like V29(( the Arity of S * (c7 #)) . p,( the ResultSort of S * c7) . p) Element of bool [:(( the Arity of S * (c7 #)) . p),(( the ResultSort of S * c7) . p):]
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,c7) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (c7 #), the ResultSort of S * c7
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
c7 is non empty Relation-like the carrier of S -defined Function-like total ManySortedSubset of the Sorts of X
domdt is strict non-empty MSSubAlgebra of X
p is MSSubAlgebra of v
GenMSAlg c7 is strict MSSubAlgebra of X
the Sorts of (GenMSAlg c7) is non empty Relation-like the carrier of S -defined Function-like total set
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
c7 is non empty set
[:(( the Arity of S * ( the Sorts of X #)) . dt),c7:] is Relation-like set
bool [:(( the Arity of S * ( the Sorts of X #)) . dt),c7:] is set
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 c7 -valued Function-like V29(( the Arity of S * ( the Sorts of X #)) . dt,c7) Element of bool [:(( the Arity of S * ( the Sorts of X #)) . dt),c7:]
x . o9 is set
p is Relation-like ( the Arity of S * ( the Sorts of X #)) . dt -defined c7 -valued Function-like V29(( the Arity of S * ( the Sorts of X #)) . dt,c7) Element of bool [:(( the Arity of S * ( the Sorts of X #)) . dt),c7:]
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(