:: 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₁ where b₁ is Element of the carrier of S : b₁ is with_const_op } is set
bool the carrier of S is set
{ b₁ where b₁ is Element of the carrier of S : S₁[b₁] } 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
{ b₁ where b₁ is Element of the carrier of S : b₁ 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
c₇ is Relation-like Function-like set
dom c₇ 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
c₇ is V7() V8() V9() V13() set
((the_arity_of v) * the Sorts of X) . c₇ is set
(the_arity_of v) . c₇ is set
the Sorts of X . ((the_arity_of v) . c₇) is set
(the_arity_of v) /. c₇ is Element of the carrier of S
the Sorts of X . ((the_arity_of v) /. c₇) 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
c₇ 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
c₇ . 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
c₇ 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
c₇ is Element of the carrier of S
v . c₇ is set
the Sorts of X . c₇ is non empty set
[:(v . c₇),( the Sorts of X . c₇):] is Relation-like set
bool [:(v . c₇),( the Sorts of X . c₇):] is set
x is Relation-like v . c₇ -defined the Sorts of X . c₇ -valued Function-like V29(v . c₇, the Sorts of X . c₇) Element of bool [:(v . c₇),( the Sorts of X . 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₇ 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
c₇ || 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
c₇ . 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
(c₇ . 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
(c₇ . 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):]
((c₇ . 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
c₇ is Element of the carrier of S
FreeGen (c₇, the Sorts of X) is non empty Element of bool ((FreeSort the Sorts of X) . 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₇ is non empty set
bool ((FreeSort the Sorts of X) . c₇) is set
dt . c₇ is Relation-like the Sorts of (FreeMSA the Sorts of X) . c₇ -defined the Sorts of X . c₇ -valued Function-like V29( the Sorts of (FreeMSA the Sorts of X) . c₇, the Sorts of X . c₇) Element of bool [:( the Sorts of (FreeMSA the Sorts of X) . c₇),( the Sorts of X . c₇):]
the Sorts of (FreeMSA the Sorts of X) . c₇ is non empty set
the Sorts of X . c₇ is non empty set
[:( the Sorts of (FreeMSA the Sorts of X) . c₇),( the Sorts of X . c₇):] is Relation-like set
bool [:( the Sorts of (FreeMSA the Sorts of X) . c₇),( the Sorts of X . c₇):] is set
p is set
(dt . c₇) . p is set
x is set
[x,c₇] is set
{x,c₇} is non empty finite countable set
{x} is non empty finite countable set
{{x,c₇},{x}} is non empty finite V36() countable set
root-tree [x,c₇] is Relation-like Function-like finite countable DecoratedTree-like set
o9 is set
[o9,c₇] is set
{o9,c₇} is non empty finite countable set
{o9} is non empty finite countable set
{{o9,c₇},{o9}} is non empty finite V36() countable set
root-tree [o9,c₇] is Relation-like Function-like finite countable DecoratedTree-like set
FreeSort ( the Sorts of X,c₇) 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
c₇ is Element of the carrier of S
FreeGen (c₇, the Sorts of X) is non empty Element of bool ((FreeSort the Sorts of X) . 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₇ is non empty set
bool ((FreeSort the Sorts of X) . c₇) is set
domdt . c₇ is Relation-like the Sorts of (FreeMSA the Sorts of X) . c₇ -defined the Sorts of X . c₇ -valued Function-like V29( the Sorts of (FreeMSA the Sorts of X) . c₇, the Sorts of X . c₇) Element of bool [:( the Sorts of (FreeMSA the Sorts of X) . c₇),( the Sorts of X . c₇):]
the Sorts of (FreeMSA the Sorts of X) . c₇ is non empty set
the Sorts of X . c₇ is non empty set
[:( the Sorts of (FreeMSA the Sorts of X) . c₇),( the Sorts of X . c₇):] is Relation-like set
bool [:( the Sorts of (FreeMSA the Sorts of X) . c₇),( the Sorts of X . c₇):] is set
p is set
(domdt . c₇) . p is set
x is set
[x,c₇] is set
{x,c₇} is non empty finite countable set
{x} is non empty finite countable set
{{x,c₇},{x}} is non empty finite V36() countable set
root-tree [x,c₇] is Relation-like Function-like finite countable DecoratedTree-like set
o9 is set
[o9,c₇] is set
{o9,c₇} is non empty finite countable set
{o9} is non empty finite countable set
{{o9,c₇},{o9}} is non empty finite V36() countable set
root-tree [o9,c₇] is Relation-like Function-like finite countable DecoratedTree-like set
FreeSort ( the Sorts of X,c₇) 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
c₇ 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
c₇ # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * (c₇ #) is non empty Relation-like the carrier' of S -defined Function-like total set
( the Arity of S * (c₇ #)) . x is set
(Den (x,MSAlgebra(# the Sorts of X, the Charact of X #))) | (( the Arity of S * (c₇ #)) . x) is Relation-like Args (x,MSAlgebra(# the Sorts of X, the Charact of X #)) -defined ( the Arity of S * (c₇ #)) . 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 * (c₇ #)) . 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 * c₇ is non empty Relation-like the carrier' of S -defined Function-like total set
( the ResultSort of S * c₇) . 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 * (c₇ #), the ResultSort of S * c₇
x . p is Relation-like ( the Arity of S * (c₇ #)) . p -defined ( the ResultSort of S * c₇) . p -valued Function-like V29(( the Arity of S * (c₇ #)) . p,( the ResultSort of S * c₇) . p) Element of bool [:(( the Arity of S * (c₇ #)) . p),(( the ResultSort of S * c₇) . p):]
( the Arity of S * (c₇ #)) . p is set
( the ResultSort of S * c₇) . p is set
[:(( the Arity of S * (c₇ #)) . p),(( the ResultSort of S * c₇) . p):] is Relation-like set
bool [:(( the Arity of S * (c₇ #)) . p),(( the ResultSort of S * c₇) . 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 /. c₇ is Relation-like ( the Arity of S * (c₇ #)) . p -defined ( the ResultSort of S * c₇) . p -valued Function-like V29(( the Arity of S * (c₇ #)) . p,( the ResultSort of S * c₇) . p) Element of bool [:(( the Arity of S * (c₇ #)) . p),(( the ResultSort of S * c₇) . 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,c₇) is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * (c₇ #), the ResultSort of S * 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₇ 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 c₇ is strict MSSubAlgebra of X
the Sorts of (GenMSAlg c₇) 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
c₇ is non empty set
[:(( the Arity of S * ( the Sorts of X #)) . dt),c₇:] is Relation-like set
bool [:(( the Arity of S * ( the Sorts of X #)) . dt),c₇:] 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 c₇ -valued Function-like V29(( the Arity of S * ( the Sorts of X #)) . dt,c₇) Element of bool [:(( the Arity of S * ( the Sorts of X #)) . dt),c₇:]
x . o9 is set
p is Relation-like ( the Arity of S * ( the Sorts of X #)) . dt -defined c₇ -valued Function-like V29(( the Arity of S * ( the Sorts of X #)) . dt,c₇) Element of bool [:(( the Arity of S * ( the Sorts of X #)) . dt),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( Args (A99,domdt), Result (A99,domdt)) Element of bool [:(Args (A99,domdt)),(Result (A99,domdt)):]
Args (A99,domdt) is non empty Element of rng ( the Sorts of domdt #)
( the Arity of e * ( the Sorts of domdt #)) . A99 is set
Result (A99,domdt) is non empty Element of rng the Sorts of domdt
( the ResultSort of e * the Sorts of domdt) . A99 is non empty set
[:(Args (A99,domdt)),(Result (A99,domdt)):] is Relation-like set
bool [:(Args (A99,domdt)),(Result (A99,domdt)):] is set
the Charact of domdt . A99 is Relation-like Function-like set
A99 # is non empty Relation-like the carrier of e * -defined Function-like total set
the Arity of e * (A99 #) is non empty Relation-like the carrier' of e -defined Function-like total set
( the Arity of e * (A99 #)) . A99 is set
(Den (A99,domdt)) | (( the Arity of e * (A99 #)) . A99) is Relation-like ( the Arity of e * (A99 #)) . A99 -defined Args (A99,domdt) -defined Result (A99,domdt) -valued Function-like set
rng ((Den (A99,domdt)) | (( the Arity of e * (A99 #)) . A99)) is set
the ResultSort of e * A99 is non empty Relation-like the carrier' of e -defined Function-like total set
( the ResultSort of e * A99) . A99 is set
(Den (A99,domdt)) | (( the Arity of e * (A99 #)) . A99) is Relation-like Args (A99,domdt) -defined ( the Arity of e * (A99 #)) . A99 -defined Args (A99,domdt) -defined Result (A99,domdt) -valued Function-like Element of bool [:(Args (A99,domdt)),(Result (A99,domdt)):]
rng ((Den (A99,domdt)) | (( the Arity of e * (A99 #)) . A99)) is Element of bool (Result (A99,domdt))
bool (Result (A99,domdt)) is set
dom the ResultSort of e is Element of bool the carrier' of e
bool the carrier' of e is set
the ResultSort of e . 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 {{}} -defined Args ( the Element of the carrier' of e,domdt) -defined Result ( the Element of the carrier' of e,domdt) -valued Function-like finite countable Element of bool [:(Args ( the Element of the carrier' of e,domdt)),(Result ( the Element of the carrier' of e,domdt)):]
the Arity of v * (A99 #) is Relation-like the carrier' of v -defined Function-like set
( the Arity of v * (A99 #)) . the Element of the carrier' of e is set
(A99 #) . ( the Arity of v . the Element of the carrier' of e) is set
b is set
(Den ( the Element of the carrier' of e,domdt)) . b is set
A99 . the Element of the carrier of e is set
A99 # is non empty Relation-like the carrier of e * -defined Function-like total set
the Arity of e * (A99 #) is non empty Relation-like the carrier' of e -defined Function-like total set
( the Arity of e * (A99 #)) . the Element of the carrier' of e is set
the Arity of e . the Element of the carrier' of e is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of e *
(A99 #) . ( the Arity of e . the Element of the carrier' of e) is set
(b #) . (<*> the carrier of e) is set
(Den ( the Element of the carrier' of e,domdt)) | (( the Arity of e * (A99 #)) . the Element of the carrier' of e) is Relation-like Args ( the Element of the carrier' of e,domdt) -defined ( the Arity of e * (A99 #)) . the Element of the carrier' of e -defined Args ( the Element of the carrier' of e,domdt) -defined Result ( the Element of the carrier' of e,domdt) -valued Function-like Element of bool [:(Args ( the Element of the carrier' of e,domdt)),(Result ( the Element of the carrier' of e,domdt)):]
the Charact of MSAlgebra(# b,ts #) is Relation-like the carrier' of v -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of v * ( the Sorts of MSAlgebra(# b,ts #) #), the ResultSort of v * the Sorts of MSAlgebra(# b,ts #)
the Sorts of MSAlgebra(# b,ts #) # is non empty Relation-like the carrier of v * -defined Function-like total set
the Arity of v * ( the Sorts of MSAlgebra(# b,ts #) #) is Relation-like the carrier' of v -defined Function-like total set
the ResultSort of v * the Sorts of MSAlgebra(# b,ts #) is Relation-like the carrier' of v -defined Function-like total set
the Charact of MSAlgebra(# b,ts #) . the Element of the carrier' of e is Relation-like Function-like set
A99 is Element of the carrier' of e
the Charact of MSAlgebra(# b,ts #) . A99 is Relation-like Function-like set
A99 /. A99 is Relation-like ( the Arity of e * (A99 #)) . A99 -defined ( the ResultSort of e * A99) . A99 -valued Function-like V29(( the Arity of e * (A99 #)) . A99,( the ResultSort of e * A99) . A99) Element of bool [:(( the Arity of e * (A99 #)) . A99),(( the ResultSort of e * A99) . A99):]
( the Arity of e * (A99 #)) . A99 is set
the ResultSort of e * A99 is non empty Relation-like the carrier' of e -defined Function-like total set
( the ResultSort of e * A99) . A99 is set
[:(( the Arity of e * (A99 #)) . A99),(( the ResultSort of e * A99) . A99):] is Relation-like set
bool [:(( the Arity of e * (A99 #)) . A99),(( the ResultSort of e * A99) . A99):] is set
Opers (domdt,A99) is non empty Relation-like the carrier' of e -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of e * (A99 #), the ResultSort of e * A99
the ResultSort of v . the Element of the carrier' of e is set
the Sorts of domdt . ( the ResultSort of v . the Element of the carrier' of e) is set
the Sorts of domdt . {} is set
b is non empty Relation-like the carrier of e -defined Function-like total set
A99 is set
b . A99 is set
the Sorts of domdt . A99 is set
rng (Den ( the Element of the carrier' of e,domdt)) is Element of bool (Result ( the Element of the carrier' of e,domdt))
A99 is non-empty MSAlgebra over e
ts is non empty Relation-like the carrier of e -defined Function-like total ManySortedSubset of the Sorts of domdt
i is MSSubAlgebra of domdt
the Sorts of i is non empty Relation-like the carrier of e -defined Function-like total set
Constants domdt is non empty Relation-like the carrier of e -defined Function-like total ManySortedSubset of the Sorts of domdt
(Constants domdt) . the Element of the carrier of e is set
the Sorts of i . the Element of the carrier of e is set
Constants (domdt, the Element of the carrier of e) is Element of bool ( the Sorts of domdt . the Element of the carrier of e)
the Sorts of domdt . the Element of the carrier of e is non empty set
bool ( the Sorts of domdt . the Element of the carrier of e) is set
rng (Den ( the Element of the carrier' of e,domdt)) is Element of bool (Result ( the Element of the carrier' of e,domdt))
b is Element of the Sorts of domdt . the Element of the carrier of e
c₂₃ is non empty set
{ b₁ where b₁ is Element of c₂₃ : ex b₂ being Element of the carrier' of e st
( the Arity of e . b₂ = {} & the ResultSort of e . b₂ = the Element of the carrier of e & b₁ in rng (Den (b₂,domdt)) ) } is set
A99 is strict MSSubAlgebra of domdt
the Sorts of A99 is non empty Relation-like the carrier of e -defined Function-like total set
the Sorts of A99 . the Element of the carrier of e is set
i is set
the Sorts of A99 . i is set
the Sorts of i . i is set
i is set
ts . i is set
the Sorts of A99 . i is set
GenMSAlg x is strict MSSubAlgebra of domdt
the Sorts of (GenMSAlg x) is non empty Relation-like the carrier of e -defined Function-like total set
p is finite countable set
p \/ {((Den ( the Element of the carrier' of e,domdt)) . {})} is non empty finite countable set
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 non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeMSA X is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
v is Element of the carrier of S
the Sorts of (FreeMSA X) . v is non empty set
e is Element of the Sorts of (FreeMSA X) . v
FreeSort X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeOper X is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ((FreeSort X) #), the ResultSort of S * (FreeSort X)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like 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
(FreeSort X) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((FreeSort 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 * (FreeSort X) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (FreeSort X),(FreeOper X) #) is strict MSAlgebra over S
FreeSort (X,v) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA X))
DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
TS (DTConMSA X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
the carrier of (DTConMSA X) is non empty set
FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)
bool (FinTrees the carrier of (DTConMSA X)) is set
bool (TS (DTConMSA X)) is set
dt is Relation-like Function-like DecoratedTree-like set
dom dt is non empty Tree-like set
S is non empty non void V55() ManySortedSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total finite-yielding set
FreeMSA X is strict non-empty MSAlgebra over S
FreeGen X is non empty Relation-like the carrier of S -defined Function-like total GeneratorSet of FreeMSA X
e is non empty non void V55() ManySortedSign
the carrier of e is non empty set
dt is MSAlgebra over e
v is non empty Relation-like the carrier of S -defined Function-like total GeneratorSet of FreeMSA X
domdt is non empty Relation-like the carrier of e -defined Function-like total GeneratorSet of dt
c₇ is set
domdt . c₇ is set
p is Element of the carrier of S
X . p is non empty finite countable set
x is set
o9 is non empty finite countable set
FreeGen (p,X) is non empty Element of bool ((FreeSort X) . p)
FreeSort X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(FreeSort X) . p is non empty set
bool ((FreeSort X) . p) is set
ts is set
ts is set
[ts,c₇] is set
{ts,c₇} is non empty finite countable set
{ts} is non empty finite countable set
{{ts,c₇},{ts}} is non empty finite V36() countable set
root-tree [ts,c₇] is Relation-like Function-like finite countable DecoratedTree-like set
ts is Relation-like Function-like set
dom ts is set
rng ts is set
ts is Relation-like Function-like set
ts is set
dom ts is set
ts9 is set
ts . ts is set
ts . ts9 is set
[(ts . ts9),c₇] is set
{(ts . ts9),c₇} is non empty finite countable set
{(ts . ts9)} is non empty finite countable set
{{(ts . ts9),c₇},{(ts . ts9)}} is non empty finite V36() countable set
root-tree [(ts . ts9),c₇] is Relation-like Function-like finite countable DecoratedTree-like set
card x is cardinal set
card o9 is V7() V8() V9() V13() Element of K32()
ts is Relation-like Function-like set
dom ts is set
rng ts is set
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
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 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
v is Element of the carrier of S
the Sorts of (S,X) . v is non empty set
the Sorts of X . v is non empty set
e is Element of the Sorts of (S,X) . v
FreeSort the Sorts of X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeOper the Sorts of X is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ((FreeSort the Sorts of X) #), the ResultSort of S * (FreeSort the Sorts of X)
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
(FreeSort the Sorts of X) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((FreeSort the Sorts of X) #) is non empty Relation-like the carrier' of S -defined Function-like total set
the ResultSort of S * (FreeSort the Sorts of X) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (FreeSort the Sorts of X),(FreeOper the Sorts of X) #) is strict MSAlgebra over S
(FreeSort the Sorts of X) . v is non empty set
FreeSort ( the Sorts of X,v) 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
{ b₁ where b₁ is Relation-like the carrier of (DTConMSA the Sorts of X) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of X) : ( ex b₂ being set st
( b₂ in the Sorts of X . v & b₁ = root-tree [b₂,v] ) or ex b₂ being Element of the carrier' of S st
( [b₂, the carrier of S] = b₁ . {} & the_result_sort_of b₂ = v ) ) } is set
dt is Relation-like the carrier of (DTConMSA the Sorts of X) -valued Function-like DecoratedTree-like Element of TS (DTConMSA the Sorts of X)
dt . {} is set
domdt is set
[domdt,v] is set
{domdt,v} is non empty finite countable set
{domdt} is non empty finite countable set
{{domdt,v},{domdt}} is non empty finite V36() countable set
root-tree [domdt,v] is Relation-like Function-like finite countable DecoratedTree-like set
c₇ is Element of the carrier' of S
[c₇, the carrier of S] is set
{c₇, the carrier of S} is non empty finite countable set
{c₇} is non empty finite countable set
{{c₇, the carrier of S},{c₇}} is non empty finite V36() countable set
the_result_sort_of c₇ is Element of the carrier of S
the ResultSort of S . c₇ is Element of the carrier of S
domdt is set
[domdt,v] is set
{domdt,v} is non empty finite countable set
{domdt} is non empty finite countable set
{{domdt,v},{domdt}} is non empty finite V36() countable set
root-tree [domdt,v] is Relation-like Function-like finite countable DecoratedTree-like set
c₇ is Element of the Sorts of X . v
[c₇,v] is set
{c₇,v} is non empty finite countable set
{c₇} is non empty finite countable set
{{c₇,v},{c₇}} is non empty finite V36() countable set
root-tree [c₇,v] is Relation-like Function-like finite countable DecoratedTree-like set
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 non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeMSA X is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
v is Element of the carrier' of S
[v, the carrier of S] is set
{v, the carrier of S} is non empty finite countable set
{v} is non empty finite countable set
{{v, the carrier of S},{v}} is non empty finite V36() countable set
the_result_sort_of v is Element of 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, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . v is Element of the carrier of S
the Sorts of (FreeMSA X) . (the_result_sort_of v) is non empty set
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()
e is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[v, the carrier of S] -tree e is Relation-like Function-like DecoratedTree-like set
len e is V7() V8() V9() V13() Element of K37()
FreeSort X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeOper X is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ((FreeSort X) #), the ResultSort of S * (FreeSort X)
(FreeSort X) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((FreeSort X) #) is non empty Relation-like the carrier' of S -defined Function-like total set
the ResultSort of S * (FreeSort X) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (FreeSort X),(FreeOper X) #) is strict MSAlgebra over S
FreeSort (X,(the_result_sort_of v)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA X))
DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
TS (DTConMSA X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
the carrier of (DTConMSA X) is non empty set
FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)
bool (FinTrees the carrier of (DTConMSA X)) is set
bool (TS (DTConMSA X)) is set
X . (the_result_sort_of v) is non empty set
{ b₁ where b₁ is Relation-like the carrier of (DTConMSA X) -valued Function-like DecoratedTree-like Element of TS (DTConMSA X) : ( ex b₂ being set st
( b₂ in X . (the_result_sort_of v) & b₁ = root-tree [b₂,(the_result_sort_of v)] ) or ex b₂ being Element of the carrier' of S st
( [b₂, the carrier of S] = b₁ . {} & the_result_sort_of b₂ = the_result_sort_of v ) ) } is set
{ the carrier of S} is non empty finite countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
NonTerminals (DTConMSA X) is non empty Element of bool the carrier of (DTConMSA X)
bool the carrier of (DTConMSA X) is set
coprod X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod X) is non empty set
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) is non empty set
c₇ is non empty set
c₇ * is non empty functional FinSequence-membered M8(c₇)
[:c₇,(c₇ *):] is Relation-like set
bool [:c₇,(c₇ *):] is set
REL X is Relation-like [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) -defined ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * -valued Element of bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):]
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * is non empty functional FinSequence-membered M8([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)))
[:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is Relation-like set
bool [:([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *):] is set
x is Relation-like c₇ -defined c₇ * -valued Element of bool [:c₇,(c₇ *):]
DTConstrStr(# c₇,x #) is non empty strict DTConstrStr
FinTrees c₇ is non empty functional constituted-DTrees DTree-set of c₇
bool (FinTrees c₇) is set
domdt is Element of NonTerminals (DTConMSA X)
p is functional constituted-DTrees Element of bool (FinTrees c₇)
ts is set
ts is Relation-like the carrier of (DTConMSA X) -valued Function-like DecoratedTree-like Element of TS (DTConMSA X)
ts . {} is set
ts is Relation-like K37() -defined FinTrees the carrier of (DTConMSA X) -valued Function-like finite Function-yielding V41() FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA X)
domdt -tree ts is Relation-like the carrier of (DTConMSA X) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA X)
roots ts is Relation-like K37() -defined the carrier of (DTConMSA X) -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (DTConMSA X)
ts is non empty functional constituted-DTrees DTree-set of c₇
ts9 is Relation-like K37() -defined ts -valued Function-like finite Function-yielding V41() FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of ts
roots ts9 is Relation-like K37() -defined c₇ -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of c₇
b is Relation-like K37() -defined c₇ -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of c₇
o9 is Element of c₇
b is Relation-like K37() -defined c₇ -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of c₇ *
[o9,b] is set
{o9,b} is non empty finite countable set
{o9} is non empty finite countable set
{{o9,b},{o9}} is non empty finite V36() countable set
len (roots ts) is V7() V8() V9() V13() Element of K37()
ts is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
roots ts is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable set
dom (roots ts) is finite countable Element of bool K37()
dom ts is finite countable Element of bool K37()
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 non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeMSA X is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
v is Element of the carrier' of S
[v, the carrier of S] is set
{v, the carrier of S} is non empty finite countable set
{v} is non empty finite countable set
{{v, the carrier of S},{v}} is non empty finite V36() countable set
the_result_sort_of v is Element of 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, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S . v is Element of the carrier of S
the Sorts of (FreeMSA X) . (the_result_sort_of v) is non empty set
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 *
dom (the_arity_of v) is finite countable Element of bool K37()
e is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
[v, the carrier of S] -tree e is Relation-like Function-like DecoratedTree-like set
FreeSort X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeOper X is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ((FreeSort X) #), the ResultSort of S * (FreeSort X)
(FreeSort X) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((FreeSort X) #) is non empty Relation-like the carrier' of S -defined Function-like total set
the ResultSort of S * (FreeSort X) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (FreeSort X),(FreeOper X) #) is strict MSAlgebra over S
{ the carrier of S} is non empty finite countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA X) is non empty set
NonTerminals (DTConMSA X) is non empty Element of bool the carrier of (DTConMSA X)
bool the carrier of (DTConMSA X) is set
x is V7() V8() V9() V13() set
c₇ is Relation-like K37() -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S *
c₇ . x is set
rng c₇ is finite countable Element of bool the carrier of S
bool the carrier of S is set
p is Element of the carrier of S
the Sorts of (FreeMSA X) . p is non empty set
FreeSort (X,p) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA X))
TS (DTConMSA X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)
bool (FinTrees the carrier of (DTConMSA X)) is set
bool (TS (DTConMSA X)) is set
(the_arity_of v) /. x is Element of the carrier of S
FreeSort (X,((the_arity_of v) /. x)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA X))
FreeSort (X,(the_result_sort_of v)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA X))
X . (the_result_sort_of v) is non empty set
{ b₁ where b₁ is Relation-like the carrier of (DTConMSA X) -valued Function-like DecoratedTree-like Element of TS (DTConMSA X) : ( ex b₂ being set st
( b₂ in X . (the_result_sort_of v) & b₁ = root-tree [b₂,(the_result_sort_of v)] ) or ex b₂ being Element of the carrier' of S st
( [b₂, the carrier of S] = b₁ . {} & the_result_sort_of b₂ = the_result_sort_of v ) ) } is set
o9 is Relation-like the carrier of (DTConMSA X) -valued Function-like DecoratedTree-like Element of TS (DTConMSA X)
o9 . {} is set
dt is Element of NonTerminals (DTConMSA X)
ts is Relation-like K37() -defined FinTrees the carrier of (DTConMSA X) -valued Function-like finite Function-yielding V41() FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA X)
dt -tree ts is Relation-like the carrier of (DTConMSA X) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA X)
roots ts is Relation-like K37() -defined the carrier of (DTConMSA X) -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (DTConMSA X)
Sym (v,X) is Element of the carrier of (DTConMSA X)
( the Arity of S * ((FreeSort X) #)) . v is set
dom e is finite countable Element of bool K37()
len e is V7() V8() V9() V13() Element of K37()
Seg (len e) is finite len e -element countable Element of bool K37()
len (the_arity_of v) is V7() V8() V9() V13() Element of K37()
Seg (len (the_arity_of v)) is finite len (the_arity_of v) -element countable Element of bool K37()
ts is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable DTree-yielding set
e . x is set
(the_arity_of v) . x is set
the Sorts of (FreeMSA X) . ((the_arity_of v) . x) is set
dt is V7() V8() V9() V13() set
e . dt is set
(the_arity_of v) . dt is set
the Sorts of (FreeMSA X) . ((the_arity_of v) . dt) is set
S is non empty non void V55() ManySortedSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeMSA X is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
v is Element of the carrier of S
the Sorts of (FreeMSA X) . v is non empty set
e is Element of the Sorts of (FreeMSA X) . v
dt is Relation-like Function-like DecoratedTree-like set
dom dt is non empty Tree-like set
S is non empty non void V55() ManySortedSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeMSA X is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
v is Element of the carrier of S
the Sorts of (FreeMSA X) . v is non empty set
the non empty Relation-like Function-like finite countable Element of the Sorts of (FreeMSA X) . v is non empty Relation-like Function-like finite countable Element of the Sorts of (FreeMSA X) . v
S is non empty non void V55() ManySortedSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeMSA X is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
v is Element of the carrier of S
the Sorts of (FreeMSA X) . v is non empty set
e is non empty Relation-like Function-like finite countable Element of the Sorts of (FreeMSA X) . v
S is non empty non void V55() ManySortedSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeMSA X is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
v is Element of the carrier of S
the Sorts of (FreeMSA X) . v is non empty set
the non empty Relation-like Function-like finite countable DecoratedTree-like Element of the Sorts of (FreeMSA X) . v is non empty Relation-like Function-like finite countable DecoratedTree-like Element of the Sorts of (FreeMSA X) . v
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 non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeMSA X is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
v is Element of the carrier of S
the Sorts of (FreeMSA X) . v is non empty set
e is Element of the carrier' of S
[e, the carrier of S] is set
{e, the carrier of S} is non empty finite countable set
{e} is non empty finite countable set
{{e, the carrier of S},{e}} is non empty finite V36() countable set
the_arity_of e 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 . e is Relation-like K37() -defined Function-like finite FinSequence-like FinSubsequence-like countable Element of the carrier of S *
len (the_arity_of e) is V7() V8() V9() V13() Element of K37()
dt is non empty Relation-like Function-like finite countable DecoratedTree-like Element of the Sorts of (FreeMSA X) . v
dt . {} is set
{ the carrier of S} is non empty finite countable set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA X) is non empty set
NonTerminals (DTConMSA X) is non empty Element of bool the carrier of (DTConMSA X)
bool the carrier of (DTConMSA X) is set
FreeSort X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeOper X is non empty Relation-like the carrier' of S -defined Function-like total Function-yielding V41() ManySortedFunction of the Arity of S * ((FreeSort X) #), the ResultSort of S * (FreeSort X)
(FreeSort X) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((FreeSort 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 * (FreeSort X) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
MSAlgebra(# (FreeSort X),(FreeOper X) #) is strict MSAlgebra over S
FreeSort (X,v) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA X))
TS (DTConMSA X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)
bool (FinTrees the carrier of (DTConMSA X)) is set
bool (TS (DTConMSA X)) is set
X . v is non empty set
{ b₁ where b₁ is Relation-like the carrier of (DTConMSA X) -valued Function-like DecoratedTree-like Element of TS (DTConMSA X) : ( ex b₂ being set st
( b₂ in X . v & b₁ = root-tree [b₂,v] ) or ex b₂ being Element of the carrier' of S st
( [b₂, the carrier of S] = b₁ . {} & the_result_sort_of b₂ = v ) ) } is set
c₇ is Relation-like the carrier of (DTConMSA X) -valued Function-like DecoratedTree-like Element of TS (DTConMSA X)
c₇ . {} is set
x is set
[x,v] is set
{x,v} is non empty finite countable set
{x} is non empty finite countable set
{{x,v},{x}} is non empty finite V36() countable set
root-tree [x,v] is Relation-like Function-like finite countable DecoratedTree-like set
p is Element of the carrier' of S
[p, the carrier of S] is set
{p, the carrier of S} is non empty finite countable set
{p} is non empty finite countable set
{{p, the carrier of S},{p}} is non empty finite V36() countable set
the_result_sort_of p is Element of the carrier of S
the ResultSort of S . p is Element of the carrier of S
x is set
[x,v] is set
{x,v} is non empty finite countable set
{x} is non empty finite countable set
{{x,v},{x}} is non empty finite V36() countable set
root-tree [x,v] is Relation-like Function-like finite countable DecoratedTree-like set
domdt is Element of NonTerminals (DTConMSA X)
p is Relation-like K37() -defined FinTrees the carrier of (DTConMSA X) -valued Function-like finite Function-yielding V41() FinSequence-like FinSubsequence-like countable DTree-yielding FinSequence of TS (DTConMSA X)
domdt -tree p is Relation-like the carrier of (DTConMSA X) -valued Function-like finite countable DecoratedTree-like Element of FinTrees the carrier of (DTConMSA X)
roots p is Relation-like K37() -defined the carrier of (DTConMSA X) -valued Function-like finite FinSequence-like FinSubsequence-like countable FinSequence of the carrier of (DTConMSA X)
o9 is set
o9 is Element of the carrier' of S
[o9, the carrier of S] is set
{o9, the carrier of S} is non empty finite countable set
{o9} is non empty finite countable set
{{o9, the carrier of S},{o9}} is non empty finite V36() countable set
the_result_sort_of o9 is Element of the carrier of S
the ResultSort of S . o9 is Element of the carrier of S
o9 is Element of the carrier' of S
[o9, the carrier of S] is set
{o9, the carrier of S} is non empty finite countable set
{o9} is non empty finite countable set
{{o9, the carrier of S},{o9}} is non empty finite V36() countable set
the_result_sort_of o9 is Element of the carrier of S
the ResultSort of S . o9 is Element of the carrier of S
len p is V7() V8() V9() V13() Element of K37()
dom p is finite countable Element of bool K37()
Seg (len (the_arity_of e)) is finite len (the_arity_of e) -element countable Element of bool K37()
dom (the_arity_of e) is finite countable Element of bool K37()
ts is V7() V8() V9() V13() set
p . ts is Relation-like Function-like set
(the_arity_of e) . ts is set
the Sorts of (FreeMSA X) . ((the_arity_of e) . ts) is set
S is non empty non void V55() ManySortedSign
the carrier of S is non empty set
X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
FreeMSA X is strict non-empty MSAlgebra over S
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
v is Element of the carrier of S
the Sorts of (FreeMSA X) . v is non empty set
e is non empty Relation-like Function-like finite countable DecoratedTree-like Element of the Sorts of (FreeMSA X) . v
dt is Relation-like Function-like finite countable DecoratedTree-like set
dom dt is non empty finite countable Tree-like set
domdt is non empty finite countable Tree-like set
height domdt is V7() V8() V9() V13() Element of K37()
c₇ is Relation-like Function-like finite countable DecoratedTree-like set
x is non empty finite countable Tree-like set
dom c₇ is non empty finite countable Tree-like set
dt is V7() V8() V9() V13() set
height x is V7() V8() V9() V13() Element of K37()
p is Relation-like Function-like finite countable DecoratedTree-like set
o9 is non empty finite countable Tree-like set
dom p is non empty finite countable Tree-like set
domdt is V7() V8() V9() V13() set
height o9 is V7() V8() V9() V13() Element of K37()