:: ABCMIZ_A semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
{} is empty trivial Relation-like non-empty empty-yielding NAT -defined non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative set
the empty trivial Relation-like non-empty empty-yielding NAT -defined non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative set is empty trivial Relation-like non-empty empty-yielding NAT -defined non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative set
1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative Element of NAT
{{},1} is non empty finite V32() non with_pair set
Trees is non empty constituted-Trees set
bool Trees is non empty set
COMPLEX is set
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
K422() is non empty V137() L15()
the carrier of K422() is non empty set
FinTrees the carrier of K422() is non empty functional constituted-DTrees DTree-set of the carrier of K422()
K421(K422()) is functional constituted-DTrees Element of bool (FinTrees the carrier of K422())
bool (FinTrees the carrier of K422()) is non empty set
[:K421(K422()),NAT:] is Relation-like set
bool [:K421(K422()),NAT:] is non empty set
[:NAT,K421(K422()):] is Relation-like set
bool [:NAT,K421(K422()):] is non empty set
K488() is set
2 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative Element of NAT
2 -tuples_on K488() is FinSequenceSet of K488()
[:(2 -tuples_on K488()),K488():] is Relation-like set
bool [:(2 -tuples_on K488()),K488():] is non empty set
3 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative Element of NAT
3 -tuples_on K488() is FinSequenceSet of K488()
[:(3 -tuples_on K488()),K488():] is Relation-like set
bool [:(3 -tuples_on K488()),K488():] is non empty set
K524() is Relation-like 2 -tuples_on K488() -defined K488() -valued Function-like V25(2 -tuples_on K488(),K488()) Element of bool [:(2 -tuples_on K488()),K488():]
Vars is non empty set
bool Vars is non empty set
[:Vars,NAT:] is non empty non trivial Relation-like non finite set
bool [:Vars,NAT:] is non empty non trivial non finite set
QuasiLoci is non empty FinSequenceSet of Vars
a_Type is set
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative Element of NAT
an_Adj is set
a_Term is set
{a_Type,an_Adj,a_Term} is non empty finite set
[:QuasiLoci,NAT:] is non empty non trivial Relation-like non finite set
VarPoset is non empty V261() V263() V264() V265() L25()
the carrier of VarPoset is non empty set
RAT is set
INT is set
<*> NAT is empty trivial proper Relation-like non-empty empty-yielding NAT -defined NAT -valued non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative FinSequence of NAT
[:NAT,NAT:] is non empty non trivial Relation-like non finite set
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{ b₁ where b₁ is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial finite V32() 1 -element non with_pair set
Seg 2 is non empty finite 2 -element Element of bool NAT
{ b₁ where b₁ is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty finite V32() non with_pair set
K179(0) is non empty V39() set
{0} is non empty trivial functional finite V32() 1 -element non with_pair Element of bool NAT
{0,1,2} is non empty finite non with_pair Element of bool NAT
{ [(varcl b₁),b₂] where b₁ is Element of bool Vars, b₂ is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT : b₁ is finite } is set
K829(Vars) is empty trivial Relation-like non-empty empty-yielding NAT -defined Vars -valued non pair Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V105() V106() non with_pair ext-real non negative Element of Vars *
Vars * is non empty functional FinSequence-membered FinSequenceSet of Vars
* is set
non_op is set
{*,non_op} is non empty finite set
<*an_Adj,a_Type*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
<*an_Adj*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,an_Adj] is non empty pair set
{1,an_Adj} is non empty finite set
{{1,an_Adj},{1}} is non empty finite V32() set
{[1,an_Adj]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*a_Type*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,a_Type] is non empty pair set
{1,a_Type} is non empty finite set
{{1,a_Type},{1}} is non empty finite V32() set
{[1,a_Type]} is non empty trivial Relation-like Function-like constant finite 1 -element set
<*an_Adj*> ^ <*a_Type*> is non empty Relation-like NAT -defined Function-like finite K747(1,1) -element FinSequence-like FinSubsequence-like set
K747(1,1) is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative Element of NAT
{a_Term} is non empty trivial finite 1 -element set
{a_Term} * is non empty functional FinSequence-membered FinSequenceSet of {a_Term}
Constructors is non empty set
Modes is non empty set
{a_Type} is non empty trivial finite 1 -element set
[:{a_Type},[:QuasiLoci,NAT:]:] is non empty non trivial Relation-like non finite set
Attrs is non empty set
{an_Adj} is non empty trivial finite 1 -element set
[:{an_Adj},[:QuasiLoci,NAT:]:] is non empty non trivial Relation-like non finite set
Modes \/ Attrs is non empty set
Funcs is non empty set
[:{a_Term},[:QuasiLoci,NAT:]:] is non empty non trivial Relation-like non finite set
(Modes \/ Attrs) \/ Funcs is non empty set
MaxConstrSign is non empty non void V68() strict V146() constructor initialized with_an_operation_for_each_sort ManySortedSign
{*,non_op} \/ Constructors is non empty set
MC is non empty pair set
MC `1 is set
MC `2 is set
[(MC `1),(MC `2)] is non empty pair set
{(MC `1),(MC `2)} is non empty finite set
{(MC `1)} is non empty trivial finite 1 -element set
{{(MC `1),(MC `2)},{(MC `1)}} is non empty finite V32() set
F₁() is non empty finite set
card F₁() is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
the Element of F₁() is Element of F₁()
(card F₁()) + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
f is set
the set is set
x is set
d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
d . 1 is set
dom d is finite Element of bool NAT
d . 0 is set
f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
d . f is set
f + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
d . (f + 1) is set
0 + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
proj2 d is finite set
f is set
x is set
d . x is set
f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
x is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
d . x is set
d . f is set
f + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
T is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
(f + 1) + T is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
(f + 1) + 0 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
d . ((f + 1) + 0) is set
p is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
(f + 1) + p is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
d . ((f + 1) + p) is set
p + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
(f + 1) + (p + 1) is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
d . ((f + 1) + (p + 1)) is set
((f + 1) + p) + 1 is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
f + p is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + (f + p) is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
Seg ((card F₁()) + 1) is non empty finite (card F₁()) + 1 -element Element of bool NAT
{ b₁ where b₁ is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= (card F₁()) + 1 ) } is set
card (Seg ((card F₁()) + 1)) is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
card (proj2 d) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
f is set
x is set
d . f is set
d . x is set
T is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
p is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
d . T is set
F₁() is finite set
bool F₁() is non empty finite V32() set
MC is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
l is finite Element of bool F₁()
card l is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
d is set
f is finite Element of bool F₁()
card f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
card F₁() is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
[#] F₁() is non proper finite Element of bool F₁()
MC is finite Element of bool F₁()
card MC is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
F₁() is finite set
MC is Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like set
proj2 MC is finite set
dom MC is finite Element of bool NAT
l is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
MC . l is set
MC . d is set
bool F₁() is non empty finite V32() set
MC is finite Element of bool F₁()
l is Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like set
proj2 l is finite set
dom l is finite Element of bool NAT
l is non empty finite set
d is set
f is set
d is set
f is set
x is set
d is set
{d} is non empty trivial finite 1 -element set
MC \ {d} is finite Element of bool F₁()
x is Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like set
proj2 x is finite set
dom x is finite Element of bool NAT
<*d*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
[1,d] is non empty pair set
{1,d} is non empty finite set
{{1,d},{1}} is non empty finite V32() set
{[1,d]} is non empty trivial Relation-like Function-like constant finite 1 -element set
proj2 <*d*> is non empty trivial finite 1 -element set
<*d*> ^ x is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len <*d*> is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
T is Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like set
proj2 T is finite set
dom T is finite Element of bool NAT
(proj2 <*d*>) \/ (proj2 x) is non empty finite set
{d} \/ (MC \ {d}) is non empty finite set
p is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
T . p is set
o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
T . o is set
dom <*d*> is non empty trivial finite 1 -element Element of bool NAT
o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
x . o is set
o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
q is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + q is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
o is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + o is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
q is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative set
1 + q is non empty non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real positive non negative set
x . o is set
x . q is set
MC is Element of Vars
vars MC is finite Element of bool Vars
varcl (vars MC) is set
l is Element of bool Vars
varcl l is set
d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
[(varcl l),d] is non empty pair set
{(varcl l),d} is non empty finite set
{(varcl l)} is non empty trivial finite 1 -element set
{{(varcl l),d},{(varcl l)}} is non empty finite V32() set
MC is non empty non void V68() V146() constructor initialized ManySortedSign
MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set
the carrier of MC is non empty set
Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC
the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set
Union the Sorts of (Free (MC,(MSVars MC))) is non empty set
l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))
the carrier' of MC is non empty set
QuasiTerms MC is non empty functional constituted-DTrees Element of bool (Union the Sorts of (Free (MC,(MSVars MC))))
bool (Union the Sorts of (Free (MC,(MSVars MC)))) is non empty set
a_Term MC is Element of the carrier of MC
the Sorts of (Free (MC,(MSVars MC))) . (a_Term MC) is set
an_Adj MC is Element of the carrier of MC
non_op MC is OperSymbol of an_Adj MC
a_Type MC is Element of the carrier of MC
ast MC is OperSymbol of a_Type MC
d is Element of Vars
d -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC
[d,a_Term] is non empty pair set
{d,a_Term} is non empty finite set
{d} is non empty trivial finite 1 -element set
{{d,a_Term},{d}} is non empty finite V32() set
root-tree [d,a_Term] is non empty Relation-like Function-like DecoratedTree-like set
f is Element of Vars
f -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC
[f,a_Term] is non empty pair set
{f,a_Term} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,a_Term},{f}} is non empty finite V32() set
root-tree [f,a_Term] is non empty Relation-like Function-like DecoratedTree-like set
T is Relation-like NAT -defined Union the Sorts of (Free (MC,(MSVars MC))) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of QuasiTerms MC
len T is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
x is constructor Element of the carrier' of MC
the_arity_of x is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC
the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]
[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set
bool [: the carrier' of MC,( the carrier of MC *):] is non empty set
K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,x) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
len (the_arity_of x) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
x -trm T is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching compound Element of Union the Sorts of (Free (MC,(MSVars MC)))
p is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching expression of MC, an_Adj MC
(non_op MC) term p is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching compound Element of Union the Sorts of (Free (MC,(MSVars MC)))
o is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching expression of MC, an_Adj MC
o is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching expression of MC, a_Type MC
(ast MC) term (o,o) is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching compound Element of Union the Sorts of (Free (MC,(MSVars MC)))
MC is non empty non void V68() V146() constructor ManySortedSign
the carrier' of MC is non empty set
l is Element of the carrier' of MC
the carrier' of MaxConstrSign is non empty set
MC is Element of the carrier' of MaxConstrSign
MC `1 is set
the_result_sort_of MC is Element of the carrier of MaxConstrSign
the carrier of MaxConstrSign is non empty set
the ResultSort of MaxConstrSign is Relation-like the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign -valued Function-like V25( the carrier' of MaxConstrSign, the carrier of MaxConstrSign) Element of bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:]
[: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:] is non empty Relation-like set
bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:] is non empty set
K122( the carrier' of MaxConstrSign, the carrier of MaxConstrSign, the ResultSort of MaxConstrSign,MC) is Element of the carrier of MaxConstrSign
MC `2 is set
(MC `2) `1 is set
card ((MC `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set
the_arity_of MC is Relation-like NAT -defined the carrier of MaxConstrSign -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MaxConstrSign *
the carrier of MaxConstrSign * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MaxConstrSign
the Arity of MaxConstrSign is Relation-like the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign * -valued Function-like V25( the carrier' of MaxConstrSign, the carrier of MaxConstrSign * ) Function-yielding V54() Element of bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):]
[: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):] is non empty Relation-like set
bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):] is non empty set
K122( the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *), the Arity of MaxConstrSign,MC) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MaxConstrSign *
len (the_arity_of MC) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
the ResultSort of MaxConstrSign . MC is set
the Arity of MaxConstrSign . MC is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
card ( the Arity of MaxConstrSign . MC) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
MC is non empty non void V68() V146() constructor initialized () ManySortedSign
the carrier' of MC is non empty set
l is constructor Element of the carrier' of MC
l `2 is set
(l `2) `1 is set
d is Element of Constructors
loci_of d is Relation-like NAT -defined Vars -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Element of QuasiLoci
d `2 is Element of [:QuasiLoci,NAT:]
(d `2) `1 is Relation-like NAT -defined Vars -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Element of QuasiLoci
MC is non empty non void V68() V146() constructor ManySortedSign
l is V146() Subsignature of MC
MC is non empty non void V68() V146() constructor initialized ManySortedSign
l is non empty non void V68() V146() constructor Subsignature of MC
MC is non empty non void V68() V146() constructor () ManySortedSign
l is non empty non void V68() V146() constructor Subsignature of MC
the carrier' of l is non empty set
d is Element of the carrier' of l
d `1 is set
the_result_sort_of d is Element of the carrier of l
the carrier of l is non empty set
the ResultSort of l is Relation-like the carrier' of l -defined the carrier of l -valued Function-like V25( the carrier' of l, the carrier of l) Element of bool [: the carrier' of l, the carrier of l:]
[: the carrier' of l, the carrier of l:] is non empty Relation-like set
bool [: the carrier' of l, the carrier of l:] is non empty set
K122( the carrier' of l, the carrier of l, the ResultSort of l,d) is Element of the carrier of l
d `2 is set
(d `2) `1 is set
card ((d `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set
the_arity_of d is Relation-like NAT -defined the carrier of l -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of l *
the carrier of l * is non empty functional FinSequence-membered FinSequenceSet of the carrier of l
the Arity of l is Relation-like the carrier' of l -defined the carrier of l * -valued Function-like V25( the carrier' of l, the carrier of l * ) Function-yielding V54() Element of bool [: the carrier' of l,( the carrier of l *):]
[: the carrier' of l,( the carrier of l *):] is non empty Relation-like set
bool [: the carrier' of l,( the carrier of l *):] is non empty set
K122( the carrier' of l,( the carrier of l *), the Arity of l,d) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of l *
len (the_arity_of d) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
the carrier' of MC is non empty set
f is Element of the carrier' of MC
the carrier of MC is non empty set
the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC
the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]
[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set
bool [: the carrier' of MC,( the carrier of MC *):] is non empty set
the Arity of MC | the carrier' of l is Relation-like the carrier' of l -defined the carrier' of MC -defined the carrier of MC * -valued Function-like Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]
the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]
[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set
bool [: the carrier' of MC, the carrier of MC:] is non empty set
the ResultSort of MC | the carrier' of l is Relation-like the carrier' of l -defined the carrier' of MC -defined the carrier of MC -valued Function-like Element of bool [: the carrier' of MC, the carrier of MC:]
the_result_sort_of f is Element of the carrier of MC
K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,f) is Element of the carrier of MC
the_arity_of f is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
MC is non empty non void V68() V146() constructor () ManySortedSign
the carrier' of MC is non empty set
l is non empty non void V68() V146() constructor () ManySortedSign
the carrier' of l is non empty set
the carrier of MC is non empty set
the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]
the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC
[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set
bool [: the carrier' of MC,( the carrier of MC *):] is non empty set
the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]
[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set
bool [: the carrier' of MC, the carrier of MC:] is non empty set
ManySortedSign(# the carrier of MC, the carrier' of MC, the Arity of MC, the ResultSort of MC #) is non empty V68() strict V146() ManySortedSign
the carrier of l is non empty set
the Arity of l is Relation-like the carrier' of l -defined the carrier of l * -valued Function-like V25( the carrier' of l, the carrier of l * ) Function-yielding V54() Element of bool [: the carrier' of l,( the carrier of l *):]
the carrier of l * is non empty functional FinSequence-membered FinSequenceSet of the carrier of l
[: the carrier' of l,( the carrier of l *):] is non empty Relation-like set
bool [: the carrier' of l,( the carrier of l *):] is non empty set
the ResultSort of l is Relation-like the carrier' of l -defined the carrier of l -valued Function-like V25( the carrier' of l, the carrier of l) Element of bool [: the carrier' of l, the carrier of l:]
[: the carrier' of l, the carrier of l:] is non empty Relation-like set
bool [: the carrier' of l, the carrier of l:] is non empty set
ManySortedSign(# the carrier of l, the carrier' of l, the Arity of l, the ResultSort of l #) is non empty V68() strict V146() ManySortedSign
d is Element of the carrier' of MC
the Arity of MC . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
the Arity of l . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Element of the carrier' of l
d `2 is set
(d `2) `1 is set
card ((d `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set
the_arity_of d is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,d) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
len (the_arity_of d) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
the_arity_of f is Relation-like NAT -defined the carrier of l -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of l *
K122( the carrier' of l,( the carrier of l *), the Arity of l,f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of l *
len (the_arity_of f) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
(len (the_arity_of d)) |-> a_Term is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(len (the_arity_of f)) |-> a_Term is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
the Arity of MC . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
the Arity of l . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Element of the carrier' of l
d is Element of the carrier' of MC
the ResultSort of MC . d is set
the ResultSort of l . d is set
f is Element of the carrier' of l
the_result_sort_of d is Element of the carrier of MC
K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,d) is Element of the carrier of MC
d `1 is set
the_result_sort_of f is Element of the carrier of l
K122( the carrier' of l, the carrier of l, the ResultSort of l,f) is Element of the carrier of l
the ResultSort of MC . d is set
the ResultSort of l . d is set
f is Element of the carrier' of l
MC is non empty non void V68() V146() constructor ManySortedSign
the carrier' of MaxConstrSign is non empty set
the Arity of MaxConstrSign is Relation-like the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign * -valued Function-like V25( the carrier' of MaxConstrSign, the carrier of MaxConstrSign * ) Function-yielding V54() Element of bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):]
the carrier of MaxConstrSign is non empty set
the carrier of MaxConstrSign * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MaxConstrSign
[: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):] is non empty Relation-like set
bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):] is non empty set
dom the Arity of MaxConstrSign is Element of bool the carrier' of MaxConstrSign
bool the carrier' of MaxConstrSign is non empty set
the ResultSort of MaxConstrSign is Relation-like the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign -valued Function-like V25( the carrier' of MaxConstrSign, the carrier of MaxConstrSign) Element of bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:]
[: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:] is non empty Relation-like set
bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:] is non empty set
dom the ResultSort of MaxConstrSign is Element of bool the carrier' of MaxConstrSign
the carrier' of MC is non empty set
the carrier of MC is non empty set
the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC
the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]
[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set
bool [: the carrier' of MC,( the carrier of MC *):] is non empty set
l is set
d is set
[l,d] is non empty pair set
{l,d} is non empty finite set
{l} is non empty trivial finite 1 -element set
{{l,d},{l}} is non empty finite V32() set
f is Element of the carrier' of MC
the Arity of MC . f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is Element of the carrier' of MaxConstrSign
the Arity of MaxConstrSign . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
x is Element of the carrier' of MaxConstrSign
f `2 is set
(f `2) `1 is set
card ((f `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set
the_arity_of f is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
len (the_arity_of f) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
card d is epsilon-transitive epsilon-connected ordinal cardinal set
the Arity of MaxConstrSign . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
card ( the Arity of MaxConstrSign . x) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]
[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set
bool [: the carrier' of MC, the carrier of MC:] is non empty set
l is set
d is set
[l,d] is non empty pair set
{l,d} is non empty finite set
{l} is non empty trivial finite 1 -element set
{{l,d},{l}} is non empty finite V32() set
f is Element of the carrier' of MC
the ResultSort of MC . f is set
x is Element of the carrier' of MaxConstrSign
the ResultSort of MaxConstrSign . x is set
x is Element of the carrier' of MaxConstrSign
f `1 is set
the_result_sort_of f is Element of the carrier of MC
K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,f) is Element of the carrier of MC
the_result_sort_of x is Element of the carrier of MaxConstrSign
K122( the carrier' of MaxConstrSign, the carrier of MaxConstrSign, the ResultSort of MaxConstrSign,x) is Element of the carrier of MaxConstrSign
the ResultSort of MaxConstrSign . x is set
x is Element of the carrier' of MaxConstrSign
the carrier' of MC is non empty set
l is Element of the carrier' of MC
l `1 is set
the_result_sort_of l is Element of the carrier of MC
the carrier of MC is non empty set
the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]
[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set
bool [: the carrier' of MC, the carrier of MC:] is non empty set
K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,l) is Element of the carrier of MC
l `2 is set
(l `2) `1 is set
card ((l `2) `1) is epsilon-transitive epsilon-connected ordinal cardinal set
the_arity_of l is Relation-like NAT -defined the carrier of MC -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC
the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]
[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set
bool [: the carrier' of MC,( the carrier of MC *):] is non empty set
K122( the carrier' of MC,( the carrier of MC *), the Arity of MC,l) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of MC *
len (the_arity_of l) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
d is Element of the carrier' of MaxConstrSign
the ResultSort of MaxConstrSign . d is set
the ResultSort of MaxConstrSign | the carrier' of MC is Relation-like the carrier' of MaxConstrSign -defined the carrier' of MC -defined the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign -valued Function-like Element of bool [: the carrier' of MaxConstrSign, the carrier of MaxConstrSign:]
( the ResultSort of MaxConstrSign | the carrier' of MC) . l is set
the ResultSort of MC . l is set
the Arity of MaxConstrSign . d is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
card ( the Arity of MaxConstrSign . d) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
the Arity of MaxConstrSign | the carrier' of MC is Relation-like the carrier' of MaxConstrSign -defined the carrier' of MC -defined the carrier' of MaxConstrSign -defined the carrier of MaxConstrSign * -valued Function-like Function-yielding V54() Element of bool [: the carrier' of MaxConstrSign,( the carrier of MaxConstrSign *):]
( the Arity of MaxConstrSign | the carrier' of MC) . l is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
card (( the Arity of MaxConstrSign | the carrier' of MC) . l) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
the Arity of MC . l is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
card ( the Arity of MC . l) is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of omega
MC is non empty non void V68() V146() constructor initialized ManySortedSign
a_Term MC is Element of the carrier of MC
the carrier of MC is non empty set
MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set
the Element of Vars is Element of Vars
the Element of Vars -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC
[ the Element of Vars ,a_Term] is non empty pair set
{ the Element of Vars ,a_Term} is non empty finite set
{ the Element of Vars } is non empty trivial finite 1 -element set
{{ the Element of Vars ,a_Term},{ the Element of Vars }} is non empty finite V32() set
root-tree [ the Element of Vars ,a_Term] is non empty Relation-like Function-like DecoratedTree-like set
MC is Element of Vars
l is Element of bool Vars
varcl l is set
d is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
[(varcl l),d] is non empty pair set
{(varcl l),d} is non empty finite set
{(varcl l)} is non empty trivial finite 1 -element set
{{(varcl l),d},{(varcl l)}} is non empty finite V32() set
MC is non empty pair Element of Vars
vars MC is finite Element of bool Vars
MC `1 is finite set
d is Element of bool Vars
varcl d is set
f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
[(varcl d),f] is non empty pair set
{(varcl d),f} is non empty finite set
{(varcl d)} is non empty trivial finite 1 -element set
{{(varcl d),f},{(varcl d)}} is non empty finite V32() set
l is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
the epsilon-transitive epsilon-connected ordinal Element of l is epsilon-transitive epsilon-connected ordinal Element of l
T is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
MC is set
l is non empty pair Element of Vars
d is Element of bool Vars
varcl d is set
f is non pair epsilon-transitive epsilon-connected ordinal natural finite cardinal V105() V106() ext-real non negative Element of NAT
[(varcl d),f] is non empty pair set
{(varcl d),f} is non empty finite set
{(varcl d)} is non empty trivial finite 1 -element set
{{(varcl d),f},{(varcl d)}} is non empty finite V32() set
l `2 is set
x is set
T is set
[x,T] is non empty pair set
{x,T} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,T},{x}} is non empty finite V32() set
MC is non empty pair Element of Vars
l is non empty pair Element of Vars
MC is non empty non void V68() V146() constructor () ManySortedSign
the carrier' of MC is non empty set
l is set
d is non empty pair Element of Vars
f is Element of the carrier' of MC
MC is non empty non void V68() V146() constructor initialized () ManySortedSign
MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set
the carrier of MC is non empty set
Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC
the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set
Union the Sorts of (Free (MC,(MSVars MC))) is non empty set
the carrier' of MC is non empty set
l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))
l . {} is set
the carrier of MC --> {0} is non empty Relation-like non-empty non empty-yielding the carrier of MC -defined the carrier of MC -defined bool NAT -valued Function-like constant total total V25( the carrier of MC, bool NAT) with_missing_variables Element of bool [: the carrier of MC,(bool NAT):]
[: the carrier of MC,(bool NAT):] is non empty non trivial Relation-like non finite set
bool [: the carrier of MC,(bool NAT):] is non empty non trivial non finite set
(MSVars MC) \/ ( the carrier of MC --> {0}) is non empty Relation-like non-empty non empty-yielding the carrier of MC -defined the carrier of MC -defined Function-like total total with_missing_variables set
DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})) is L15()
{ the carrier of MC} is non empty trivial finite 1 -element set
[: the carrier' of MC,{ the carrier of MC}:] is non empty Relation-like set
coprod ((MSVars MC) \/ ( the carrier of MC --> {0})) is Relation-like Function-like set
Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))) is Relation-like set
[: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty Relation-like set
REL ((MSVars MC) \/ ( the carrier of MC --> {0})) is Relation-like [: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0})))) -defined ([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) * -valued Element of bool [:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):]
([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) * is non empty functional FinSequence-membered FinSequenceSet of [: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))
[:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):] is non empty Relation-like set
bool [:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):] is non empty set
G15(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(REL ((MSVars MC) \/ ( the carrier of MC --> {0})))) is V137() L15()
the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is set
FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))
MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))))
bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty set
x is non empty Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like finite DecoratedTree-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})))
x . {} is set
T is Element of the carrier of MC
((MSVars MC) \/ ( the carrier of MC --> {0})) . T is non empty set
p is Element of ((MSVars MC) \/ ( the carrier of MC --> {0})) . T
[p,T] is non empty pair Element of [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:]
[:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:] is non empty Relation-like set
{p,T} is non empty finite set
{p} is non empty trivial finite 1 -element set
{{p,T},{p}} is non empty finite V32() set
T is Element of the carrier of MC
((MSVars MC) \/ ( the carrier of MC --> {0})) . T is non empty set
p is Element of ((MSVars MC) \/ ( the carrier of MC --> {0})) . T
[p,T] is non empty pair Element of [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:]
[:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:] is non empty Relation-like set
{p,T} is non empty finite set
{p} is non empty trivial finite 1 -element set
{{p,T},{p}} is non empty finite V32() set
dom the Sorts of (Free (MC,(MSVars MC))) is non empty Element of bool the carrier of MC
bool the carrier of MC is non empty set
o is set
the Sorts of (Free (MC,(MSVars MC))) . o is set
o is Element of the carrier of MC
root-tree [p,T] is non empty Relation-like [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:] -valued Function-like DecoratedTree-like Element of FinTrees [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:]
FinTrees [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:] is non empty functional constituted-DTrees DTree-set of [:(((MSVars MC) \/ ( the carrier of MC --> {0})) . T), the carrier of MC:]
the_sort_of x is Element of the carrier of MC
MC -Terms ((MSVars MC),((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty Relation-like the carrier of MC -defined Function-like total ManySortedSubset of the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))
FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0})) is MSAlgebra over MC
FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty Relation-like the carrier of MC -defined Function-like total set
FreeOper ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty Relation-like the carrier' of MC -defined Function-like total ManySortedFunction of the Arity of MC * ((FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) #), the ResultSort of MC * (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0})))
the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]
the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC
[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set
bool [: the carrier' of MC,( the carrier of MC *):] is non empty set
(FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) # is non empty Relation-like the carrier of MC * -defined Function-like total set
the Arity of MC * ((FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) #) is Relation-like the carrier' of MC -defined Function-like set
the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]
[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set
bool [: the carrier' of MC, the carrier of MC:] is non empty set
the ResultSort of MC * (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) is Relation-like the carrier' of MC -defined Function-like set
MSAlgebra(# (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))),(FreeOper ((MSVars MC) \/ ( the carrier of MC --> {0}))) #) is strict MSAlgebra over MC
the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty Relation-like the carrier of MC -defined Function-like total set
the Sorts of (Free (MC,(MSVars MC))) . o is set
the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) . o is set
FreeSort (((MSVars MC) \/ ( the carrier of MC --> {0})),o) is functional constituted-DTrees Element of bool K421((DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))))
K421((DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))))
bool K421((DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty set
((MSVars MC) \/ ( the carrier of MC --> {0})) . o is non empty set
{ b₁ where b₁ is Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),K421((DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))))) : ( ex b₂ being set st
( b₂ in ((MSVars MC) \/ ( the carrier of MC --> {0})) . o & b₁ = root-tree [b₂,o] ) or ex b₂ being Element of the carrier' of MC st
( [b₂, the carrier of MC] = b₁ . {} & the_result_sort_of b₂ = o ) ) } is set
(MSVars MC) . o is set
q is non empty pair Element of Vars
q -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC
a_Term MC is Element of the carrier of MC
[q,a_Term] is non empty pair set
{q,a_Term} is non empty finite set
{q} is non empty trivial Relation-like finite 1 -element set
{{q,a_Term},{q}} is non empty finite V32() set
root-tree [q,a_Term] is non empty Relation-like Function-like DecoratedTree-like set
x is non empty Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like finite DecoratedTree-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})))
x . {} is set
T is set
p is set
[T,p] is non empty pair set
{T,p} is non empty finite set
{T} is non empty trivial finite 1 -element set
{{T,p},{T}} is non empty finite V32() set
o is Element of the carrier' of MC
x is non empty Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like finite DecoratedTree-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})))
x . {} is set
MC is non empty non void V68() V146() constructor initialized () ManySortedSign
MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set
the carrier of MC is non empty set
Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC
the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set
Union the Sorts of (Free (MC,(MSVars MC))) is non empty set
l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))
l . {} is set
the carrier' of MC is non empty set
d is non empty pair Element of Vars
d -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC
a_Term MC is Element of the carrier of MC
[d,a_Term] is non empty pair set
{d,a_Term} is non empty finite set
{d} is non empty trivial Relation-like finite 1 -element set
{{d,a_Term},{d}} is non empty finite V32() set
root-tree [d,a_Term] is non empty Relation-like Function-like DecoratedTree-like set
f is Element of the carrier' of MC
[f, the carrier of MC] is non empty pair set
{f, the carrier of MC} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f, the carrier of MC},{f}} is non empty finite V32() set
MC is non empty non void V68() V146() constructor initialized ManySortedSign
MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set
the carrier of MC is non empty set
Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC
the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set
Union the Sorts of (Free (MC,(MSVars MC))) is non empty set
the carrier' of MC is non empty set
l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))
l . {} is set
d is Element of the carrier' of MC
[d, the carrier of MC] is non empty pair set
{d, the carrier of MC} is non empty finite set
{d} is non empty trivial finite 1 -element set
{{d, the carrier of MC},{d}} is non empty finite V32() set
the_result_sort_of d is Element of the carrier of MC
the ResultSort of MC is Relation-like the carrier' of MC -defined the carrier of MC -valued Function-like V25( the carrier' of MC, the carrier of MC) Element of bool [: the carrier' of MC, the carrier of MC:]
[: the carrier' of MC, the carrier of MC:] is non empty Relation-like set
bool [: the carrier' of MC, the carrier of MC:] is non empty set
K122( the carrier' of MC, the carrier of MC, the ResultSort of MC,d) is Element of the carrier of MC
the carrier of MC --> {0} is non empty Relation-like non-empty non empty-yielding the carrier of MC -defined the carrier of MC -defined bool NAT -valued Function-like constant total total V25( the carrier of MC, bool NAT) with_missing_variables Element of bool [: the carrier of MC,(bool NAT):]
[: the carrier of MC,(bool NAT):] is non empty non trivial Relation-like non finite set
bool [: the carrier of MC,(bool NAT):] is non empty non trivial non finite set
(MSVars MC) \/ ( the carrier of MC --> {0}) is non empty Relation-like non-empty non empty-yielding the carrier of MC -defined the carrier of MC -defined Function-like total total with_missing_variables set
DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})) is L15()
{ the carrier of MC} is non empty trivial finite 1 -element set
[: the carrier' of MC,{ the carrier of MC}:] is non empty Relation-like set
coprod ((MSVars MC) \/ ( the carrier of MC --> {0})) is Relation-like Function-like set
Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))) is Relation-like set
[: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty Relation-like set
REL ((MSVars MC) \/ ( the carrier of MC --> {0})) is Relation-like [: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0})))) -defined ([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) * -valued Element of bool [:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):]
([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) * is non empty functional FinSequence-membered FinSequenceSet of [: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))
[:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):] is non empty Relation-like set
bool [:([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))) *):] is non empty set
G15(([: the carrier' of MC,{ the carrier of MC}:] \/ (Union (coprod ((MSVars MC) \/ ( the carrier of MC --> {0}))))),(REL ((MSVars MC) \/ ( the carrier of MC --> {0})))) is V137() L15()
the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is set
FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))
MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))))
bool (FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))) is non empty set
T is non empty Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like finite DecoratedTree-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0})))
variables_in T is non empty Relation-like the carrier of MC -defined Function-like total ManySortedSubset of (MSVars MC) \/ ( the carrier of MC --> {0})
MC variables_in T is non empty Relation-like the carrier of MC -defined Function-like total set
the_sort_of T is Element of the carrier of MC
{ b₁ where b₁ is non empty Relation-like the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) -valued Function-like finite DecoratedTree-like M31( the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))), FinTrees the carrier of (DTConMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))),MC -Terms ((MSVars MC) \/ ( the carrier of MC --> {0}))) : ( the_sort_of b₁ = the_sort_of T & variables_in b₁ c= MSVars MC ) } is set
MC -Terms ((MSVars MC),((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty Relation-like the carrier of MC -defined Function-like total ManySortedSubset of the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0})))
FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0})) is MSAlgebra over MC
FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty Relation-like the carrier of MC -defined Function-like total set
FreeOper ((MSVars MC) \/ ( the carrier of MC --> {0})) is non empty Relation-like the carrier' of MC -defined Function-like total ManySortedFunction of the Arity of MC * ((FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) #), the ResultSort of MC * (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0})))
the Arity of MC is Relation-like the carrier' of MC -defined the carrier of MC * -valued Function-like V25( the carrier' of MC, the carrier of MC * ) Function-yielding V54() Element of bool [: the carrier' of MC,( the carrier of MC *):]
the carrier of MC * is non empty functional FinSequence-membered FinSequenceSet of the carrier of MC
[: the carrier' of MC,( the carrier of MC *):] is non empty Relation-like set
bool [: the carrier' of MC,( the carrier of MC *):] is non empty set
(FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) # is non empty Relation-like the carrier of MC * -defined Function-like total set
the Arity of MC * ((FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) #) is Relation-like the carrier' of MC -defined Function-like set
the ResultSort of MC * (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))) is Relation-like the carrier' of MC -defined Function-like set
MSAlgebra(# (FreeSort ((MSVars MC) \/ ( the carrier of MC --> {0}))),(FreeOper ((MSVars MC) \/ ( the carrier of MC --> {0}))) #) is strict MSAlgebra over MC
the Sorts of (FreeMSA ((MSVars MC) \/ ( the carrier of MC --> {0}))) is non empty Relation-like the carrier of MC -defined Function-like total set
(MC -Terms ((MSVars MC),((MSVars MC) \/ ( the carrier of MC --> {0})))) . (the_sort_of T) is set
the Sorts of (Free (MC,(MSVars MC))) . (the_sort_of T) is set
MC is non empty non void V68() V146() constructor initialized () ManySortedSign
MSVars MC is non empty Relation-like non empty-yielding the carrier of MC -defined Function-like total with_missing_variables set
the carrier of MC is non empty set
Free (MC,(MSVars MC)) is strict non-empty non empty MSAlgebra over MC
the Sorts of (Free (MC,(MSVars MC))) is non empty Relation-like the carrier of MC -defined Function-like total set
Union the Sorts of (Free (MC,(MSVars MC))) is non empty set
a_Type MC is Element of the carrier of MC
an_Adj MC is Element of the carrier of MC
l is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free (MC,(MSVars MC)))
l . {} is non empty pair set
(l . {}) `1 is set
d is non empty pair Element of Vars
d -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC
a_Term MC is Element of the carrier of MC
[d,a_Term] is non empty pair set
{d,a_Term} is non empty finite set
{d} is non empty trivial Relation-like finite 1 -element set
{{d,a_Term},{d}} is non empty finite V32() set
root-tree [d,a_Term] is non empty Relation-like Function-like DecoratedTree-like set
d is non empty pair Element of Vars
d -term MC is non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound expression of MC, a_Term MC
a_Term MC is Element of the carrier of MC
[d,a_Term] is non empty