REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is set
COMPLEX is set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
bool NAT is set
bool NAT is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
{{},1} is non empty finite 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),NAT:] is Relation-like set
bool [:(TS PeanoNat),NAT:] is set
[:NAT,(TS PeanoNat):] is Relation-like set
bool [:NAT,(TS PeanoNat):] is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT
<*> NAT is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() ext-real Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional V32() finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding FinSequence of NAT
elementary_tree 0 is non empty finite Tree-like finite-order finite-branching set
{{}} is non empty functional finite V39() Tree-like finite-order finite-branching set
S is set
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom A is finite Element of bool NAT
len A is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
V is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
1 + f is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
o + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
A is set
S is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
S + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
V is Relation-like NAT -defined A -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of A
len V is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom V is finite Element of bool NAT
V . (S + 1) is set
proj2 V is finite set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like the carrier of S -defined Function-like total set
DTConMSA A is non empty strict DTConstrStr
TS (DTConMSA A) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
bool (FinTrees the carrier of (DTConMSA A)) is set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,A) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A 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
Sym (V,A) is Element of the carrier of (DTConMSA A)
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
{ the carrier of S} is non empty finite set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
[V, the carrier of S] is V26() set
{V, the carrier of S} is non empty finite set
{V} is non empty finite set
{{V, the carrier of S},{V}} is non empty finite V39() set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Element of NonTerminals (DTConMSA A)
the Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding SubtreeSeq of V is Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding SubtreeSeq of V
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Element of the carrier' of S
[V, the carrier of S] is V26() set
{V, the carrier of S} is non empty finite set
{V} is non empty finite set
{{V, the carrier of S},{V}} is non empty finite V39() set
(S,A,V) is Element of NonTerminals (DTConMSA A)
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[V, the carrier of S] -tree f is Relation-like Function-like DecoratedTree-like set
o is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
o . {} is set
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (DTConMSA A)
(S,A,V) -tree p is Relation-like the carrier of (DTConMSA A) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (DTConMSA A)
roots p is Relation-like NAT -defined the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA A)
o is Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (S,A,(S,A,V))
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (DTConMSA A)
roots p is Relation-like NAT -defined the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA A)
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
the carrier of (DTConMSA A) is non empty set
bool the carrier of (DTConMSA A) is set
coprod A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (coprod A) is non empty set
V is set
proj1 (coprod A) is non empty set
p is set
(coprod A) . p is set
q is Element of the carrier of S
(coprod A) . q is non empty set
coprod (q,A) is set
A . q is non empty set
vt is set
[vt,q] is V26() set
{vt,q} is non empty finite set
{vt} is non empty finite set
{{vt,q},{vt}} is non empty finite V39() set
p is Element of the carrier of S
A . p is non empty set
q is Element of A . p
[q,p] is V26() set
{q,p} is non empty finite set
{q} is non empty finite set
{{q,p},{q}} is non empty finite V39() set
coprod (p,A) is set
(coprod A) . p is non empty set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of A \/ V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of A \/ V) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
coprod ( the Sorts of A \/ V) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
proj1 (coprod ( the Sorts of A \/ V)) is non empty set
Terminals (DTConMSA ( the Sorts of A \/ V)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of A \/ V))
the carrier of (DTConMSA ( the Sorts of A \/ V)) is non empty set
bool the carrier of (DTConMSA ( the Sorts of A \/ V)) is set
Union (coprod ( the Sorts of A \/ V)) is non empty set
f is set
q is set
(coprod ( the Sorts of A \/ V)) . q is set
vt is Element of the carrier of S
(coprod ( the Sorts of A \/ V)) . vt is non empty set
coprod (vt,( the Sorts of A \/ V)) is set
( the Sorts of A \/ V) . vt is non empty set
r is set
[r,vt] is V26() set
{r,vt} is non empty finite set
{r} is non empty finite set
{{r,vt},{r}} is non empty finite V39() set
the Sorts of A . vt is set
V . vt is non empty set
( the Sorts of A . vt) \/ (V . vt) is non empty set
q is Element of the carrier of S
( the Sorts of A \/ V) . q is non empty set
the Sorts of A . q is set
V . q is non empty set
( the Sorts of A . q) \/ (V . q) is non empty set
vt is set
[vt,q] is V26() set
{vt,q} is non empty finite set
{vt} is non empty finite set
{{vt,q},{vt}} is non empty finite V39() set
coprod (q,( the Sorts of A \/ V)) is set
(coprod ( the Sorts of A \/ V)) . q is non empty set
vt is Element of V . q
[vt,q] is V26() set
{vt,q} is non empty finite set
{vt} is non empty finite set
{{vt,q},{vt}} is non empty finite V39() set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
the carrier of (DTConMSA A) is non empty set
bool the carrier of (DTConMSA A) is set
the carrier' of S is non empty set
{ the carrier of S} is non empty finite set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
f is set
F1() is non empty non void V75() ManySortedSign
the carrier of F1() is non empty set
F2() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
the carrier' of F1() is non empty set
DTConMSA F2() is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA F2()) is non empty set
FinTrees the carrier of (DTConMSA F2()) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA F2())
(F1(),F2()) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA F2()))
bool (FinTrees the carrier of (DTConMSA F2())) is set
TS (DTConMSA F2()) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA F2()))
V is Element of the carrier of (DTConMSA F2())
f is Relation-like NAT -defined FinTrees the carrier of (DTConMSA F2()) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (DTConMSA F2())
roots f is Relation-like NAT -defined the carrier of (DTConMSA F2()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA F2())
proj2 f is finite set
V -tree f is Relation-like the carrier of (DTConMSA F2()) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (DTConMSA F2())
{ b1 where b1 is Element of the carrier of (DTConMSA F2()) : ex b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
NonTerminals (DTConMSA F2()) is non empty Element of bool the carrier of (DTConMSA F2())
bool the carrier of (DTConMSA F2()) is set
o is Element of NonTerminals (DTConMSA F2())
{ the carrier of F1()} is non empty finite set
[: the carrier' of F1(),{ the carrier of F1()}:] is Relation-like set
q is Element of the carrier' of F1()
vt is Element of { the carrier of F1()}
[q,vt] is V26() set
{q,vt} is non empty finite set
{q} is non empty finite set
{{q,vt},{q}} is non empty finite V39() set
[q, the carrier of F1()] is V26() set
{q, the carrier of F1()} is non empty finite set
{{q, the carrier of F1()},{q}} is non empty finite V39() set
(F1(),F2(),q) is Element of NonTerminals (DTConMSA F2())
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA F2()) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (F1(),F2())
r is Relation-like NAT -defined FinTrees the carrier of (DTConMSA F2()) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (F1(),F2(),(F1(),F2(),q))
proj2 r is finite set
i is Relation-like the carrier of (DTConMSA F2()) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (F1(),F2())
Terminals (DTConMSA F2()) is non empty Element of bool the carrier of (DTConMSA F2())
bool the carrier of (DTConMSA F2()) is set
V is Element of the carrier of (DTConMSA F2())
root-tree V is trivial Relation-like the carrier of (DTConMSA F2()) -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees the carrier of (DTConMSA F2())
f is Element of the carrier of F1()
F2() . f is non empty set
o is Element of F2() . f
[o,f] is V26() set
{o,f} is non empty finite set
{o} is non empty finite set
{{o,f},{o}} is non empty finite V39() set
V is Relation-like the carrier of (DTConMSA F2()) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (F1(),F2())
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
F1() is non empty non void V75() ManySortedSign
the carrier of F1() is non empty set
F2() is non-empty MSAlgebra over F1()
the Sorts of F2() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
F3() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
the carrier' of F1() is non empty set
the Sorts of F2() \/ F3() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
DTConMSA ( the Sorts of F2() \/ F3()) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
(F1(),( the Sorts of F2() \/ F3())) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))) is set
TS (DTConMSA ( the Sorts of F2() \/ F3())) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())))
V is Element of the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
f is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (DTConMSA ( the Sorts of F2() \/ F3()))
roots f is Relation-like NAT -defined the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
proj2 f is finite set
V -tree f is Relation-like the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
{ b1 where b1 is Element of the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) : ex b2 being Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set st b1 ==> b2 } is set
NonTerminals (DTConMSA ( the Sorts of F2() \/ F3())) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
bool the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) is set
o is Element of NonTerminals (DTConMSA ( the Sorts of F2() \/ F3()))
{ the carrier of F1()} is non empty finite set
[: the carrier' of F1(),{ the carrier of F1()}:] is Relation-like set
q is Element of the carrier' of F1()
vt is Element of { the carrier of F1()}
[q,vt] is V26() set
{q,vt} is non empty finite set
{q} is non empty finite set
{{q,vt},{q}} is non empty finite V39() set
[q, the carrier of F1()] is V26() set
{q, the carrier of F1()} is non empty finite set
{{q, the carrier of F1()},{q}} is non empty finite V39() set
(F1(),( the Sorts of F2() \/ F3()),q) is Element of NonTerminals (DTConMSA ( the Sorts of F2() \/ F3()))
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (F1(),( the Sorts of F2() \/ F3()))
r is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (F1(), the Sorts of F2() \/ F3(),(F1(),( the Sorts of F2() \/ F3()),q))
proj2 r is finite set
i is Relation-like the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (F1(),( the Sorts of F2() \/ F3()))
Terminals (DTConMSA ( the Sorts of F2() \/ F3())) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
bool the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) is set
V is Element of the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
root-tree V is trivial Relation-like the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
p is Element of the carrier of F1()
F3() . p is non empty set
o is set
f is Element of the carrier of F1()
the Sorts of F2() . f is non empty set
[o,f] is V26() set
{o,f} is non empty finite set
{o} is non empty finite set
{{o,f},{o}} is non empty finite V39() set
q is Element of F3() . p
[q,p] is V26() set
{q,p} is non empty finite set
{q} is non empty finite set
{{q,p},{q}} is non empty finite V39() set
V is Relation-like the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (F1(),( the Sorts of F2() \/ F3()))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
proj1 V is non empty finite Tree-like finite-order finite-branching set
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 V
V . f is set
o is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
p is Relation-like the carrier of (DTConMSA A) -valued Function-like DecoratedTree-like set
proj1 p is non empty Tree-like set
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 p
p . q is Element of the carrier of (DTConMSA A)
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
S is non empty with_terminals with_nonterminals DTConstrStr
the carrier of S is non empty set
Terminals S is non empty Element of bool the carrier of S
bool the carrier of S is set
NonTerminals S is non empty Element of bool the carrier of S
(Terminals S) \/ (NonTerminals S) is non empty Element of bool the carrier of S
A is Element of the carrier of S
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
{ the carrier of S} is non empty finite set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
V . {} is set
Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
(Terminals (DTConMSA A)) \/ (NonTerminals (DTConMSA A)) is non empty Element of bool the carrier of (DTConMSA A)
proj1 V is non empty finite Tree-like finite-order finite-branching set
o is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 V
(S,A,V,o) is Element of the carrier of (DTConMSA A)
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
{ the carrier of S} is non empty finite set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
V is MSAlgebra over S
the Sorts of V is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of V \/ A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of V \/ A) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of V \/ A))
(S,( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A))) is set
TS (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of V \/ A))
f . {} is set
Terminals (DTConMSA ( the Sorts of V \/ A)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of V \/ A))
bool the carrier of (DTConMSA ( the Sorts of V \/ A)) is set
NonTerminals (DTConMSA ( the Sorts of V \/ A)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of V \/ A))
(Terminals (DTConMSA ( the Sorts of V \/ A))) \/ (NonTerminals (DTConMSA ( the Sorts of V \/ A))) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of V \/ A))
proj1 f is non empty finite Tree-like finite-order finite-branching set
p is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 f
(S,( the Sorts of V \/ A),f,p) is Element of the carrier of (DTConMSA ( the Sorts of V \/ A))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Element of the carrier of S
A . V is non empty set
f is Element of A . V
[f,V] is V26() set
{f,V} is non empty finite set
{f} is non empty finite set
{{f,V},{f}} is non empty finite V39() set
root-tree [f,V] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
o is Element of Terminals (DTConMSA A)
root-tree o is trivial Relation-like the carrier of (DTConMSA A) -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
V . {} is set
f is Element of the carrier of S
A . f is non empty set
o is Element of A . f
[o,f] is V26() set
{o,f} is non empty finite set
{o} is non empty finite set
{{o,f},{o}} is non empty finite V39() set
root-tree [o,f] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
vt is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
vt . {} is set
q is Element of Terminals (DTConMSA A)
root-tree q is trivial Relation-like the carrier of (DTConMSA A) -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
V is MSAlgebra over S
the Sorts of V is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of V \/ A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of V \/ A) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of V \/ A))
(S,( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A))) is set
TS (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
f is Element of the carrier of S
the Sorts of V . f is set
o is set
[o,f] is V26() set
{o,f} is non empty finite set
{o} is non empty finite set
{{o,f},{o}} is non empty finite V39() set
root-tree [o,f] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
( the Sorts of V \/ A) . f is non empty set
A . f is non empty set
( the Sorts of V . f) \/ (A . f) is non empty set
Terminals (DTConMSA ( the Sorts of V \/ A)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of V \/ A))
bool the carrier of (DTConMSA ( the Sorts of V \/ A)) is set
p is Element of Terminals (DTConMSA ( the Sorts of V \/ A))
root-tree p is trivial Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA ( the Sorts of V \/ A))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
V is MSAlgebra over S
the Sorts of V is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of V \/ A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of V \/ A) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of V \/ A))
(S,( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A))) is set
TS (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of V \/ A))
f . {} is set
o is Element of the carrier of S
the Sorts of V . o is set
p is set
[p,o] is V26() set
{p,o} is non empty finite set
{p} is non empty finite set
{{p,o},{p}} is non empty finite V39() set
root-tree [p,o] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
Terminals (DTConMSA ( the Sorts of V \/ A)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of V \/ A))
bool the carrier of (DTConMSA ( the Sorts of V \/ A)) is set
vt is Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA ( the Sorts of V \/ A))
vt . {} is set
r is Element of Terminals (DTConMSA ( the Sorts of V \/ A))
root-tree r is trivial Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA ( the Sorts of V \/ A))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
V is MSAlgebra over S
the Sorts of V is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of V \/ A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of V \/ A) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of V \/ A))
(S,( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A))) is set
TS (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
f is Element of the carrier of S
A . f is non empty set
o is Element of A . f
[o,f] is V26() set
{o,f} is non empty finite set
{o} is non empty finite set
{{o,f},{o}} is non empty finite V39() set
root-tree [o,f] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
( the Sorts of V \/ A) . f is non empty set
the Sorts of V . f is set
( the Sorts of V . f) \/ (A . f) is non empty set
Terminals (DTConMSA ( the Sorts of V \/ A)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of V \/ A))
bool the carrier of (DTConMSA ( the Sorts of V \/ A)) is set
p is Element of Terminals (DTConMSA ( the Sorts of V \/ A))
root-tree p is trivial Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA ( the Sorts of V \/ A))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
V is MSAlgebra over S
the Sorts of V is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of V \/ A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of V \/ A) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of V \/ A))
(S,( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A))) is set
TS (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of V \/ A))
f . {} is set
o is Element of the carrier of S
A . o is non empty set
p is Element of A . o
[p,o] is V26() set
{p,o} is non empty finite set
{p} is non empty finite set
{{p,o},{p}} is non empty finite V39() set
root-tree [p,o] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
Terminals (DTConMSA ( the Sorts of V \/ A)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of V \/ A))
bool the carrier of (DTConMSA ( the Sorts of V \/ A)) is set
r is Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA ( the Sorts of V \/ A))
r . {} is set
vt is Element of Terminals (DTConMSA ( the Sorts of V \/ A))
root-tree vt is trivial Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA ( the Sorts of V \/ A))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
V . {} is set
f is Element of the carrier' of S
[f, the carrier of S] is V26() set
{f, the carrier of S} is non empty finite set
{f} is non empty finite set
{{f, the carrier of S},{f}} is non empty finite V39() set
(S,A,f) is Element of NonTerminals (DTConMSA A)
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
q is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
vt is Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of TS (DTConMSA A)
(S,A,f) -tree vt is Relation-like the carrier of (DTConMSA A) -valued Function-like DecoratedTree-like Element of FinTrees the carrier of (DTConMSA A)
roots vt is Relation-like NAT -defined the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA A)
r is Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (S,A)
i is Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (S,A,(S,A,f))
[f, the carrier of S] -tree i is Relation-like Function-like DecoratedTree-like set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non-empty MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
f is Element of the carrier of S
the Sorts of A . f is non empty set
o is Element of the Sorts of A . f
[o,f] is V26() set
{o,f} is non empty finite set
{o} is non empty finite set
{{o,f},{o}} is non empty finite V39() set
root-tree [o,f] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of A \/ V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of A \/ V) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of A \/ V)) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of A \/ V))
(S,( the Sorts of A \/ V)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V))) is set
TS (DTConMSA ( the Sorts of A \/ V)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
f is Element of the carrier of S
V . f is non empty set
o is Element of V . f
[o,f] is V26() set
{o,f} is non empty finite set
{o} is non empty finite set
{{o,f},{o}} is non empty finite V39() set
root-tree [o,f] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of A \/ V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of A \/ V) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of A \/ V)) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of A \/ V))
(S,( the Sorts of A \/ V)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V))) is set
TS (DTConMSA ( the Sorts of A \/ V)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
V is Element of NonTerminals (DTConMSA A)
f is Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (S,A,V)
V -tree f is Relation-like Function-like DecoratedTree-like set
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
the carrier' of S is non empty set
{ the carrier of S} is non empty finite set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
o is Element of the carrier' of S
p is Element of { the carrier of S}
[o,p] is V26() set
{o,p} is non empty finite set
{o} is non empty finite set
{{o,p},{o}} is non empty finite V39() set
(S,A,o) is Element of NonTerminals (DTConMSA A)
F1() is non empty non void V75() ManySortedSign
the carrier of F1() is non empty set
F2() is non-empty MSAlgebra over F1()
the Sorts of F2() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
F3() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
the carrier' of F1() is non empty set
the Sorts of F2() \/ F3() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
DTConMSA ( the Sorts of F2() \/ F3()) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
(F1(),( the Sorts of F2() \/ F3())) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))) is set
TS (DTConMSA ( the Sorts of F2() \/ F3())) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())))
S is Element of the carrier of F1()
the Sorts of F2() . S is non empty set
A is Element of the Sorts of F2() . S
(F1(),F2(),F3(),S,A) is Relation-like the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (F1(),( the Sorts of F2() \/ F3()))
[A,S] is V26() set
{A,S} is non empty finite set
{A} is non empty finite set
{{A,S},{A}} is non empty finite V39() set
root-tree [A,S] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
S is Element of the carrier of F1()
F3() . S is non empty set
A is Element of F3() . S
(F1(),F2(),F3(),S,A) is Relation-like the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (F1(),( the Sorts of F2() \/ F3()))
[A,S] is V26() set
{A,S} is non empty finite set
{A} is non empty finite set
{{A,S},{A}} is non empty finite V39() set
root-tree [A,S] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
S is Element of the carrier' of F1()
(F1(),( the Sorts of F2() \/ F3()),S) is Element of NonTerminals (DTConMSA ( the Sorts of F2() \/ F3()))
NonTerminals (DTConMSA ( the Sorts of F2() \/ F3())) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of F2() \/ F3()))
bool the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) is set
A is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (F1(), the Sorts of F2() \/ F3(),(F1(),( the Sorts of F2() \/ F3()),S))
proj2 A is finite set
(F1(),( the Sorts of F2() \/ F3()),(F1(),( the Sorts of F2() \/ F3()),S),A) is Relation-like the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (F1(),( the Sorts of F2() \/ F3()))
S is Relation-like the carrier of (DTConMSA ( the Sorts of F2() \/ F3())) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (F1(),( the Sorts of F2() \/ F3()))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
proj1 V is non empty finite Tree-like finite-order finite-branching set
V . {} is set
Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
q is Element of Terminals (DTConMSA A)
r is set
vt is Element of the carrier of S
A . vt is non empty set
[r,vt] is V26() set
{r,vt} is non empty finite set
{r} is non empty finite set
{{r,vt},{r}} is non empty finite V39() set
FreeSort (A,vt) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
bool (TS (DTConMSA A)) is set
root-tree [r,vt] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
the carrier' of S is non empty set
{ b1 where b1 is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A) : ( ex b2 being set st
( b2 in A . vt & b1 = root-tree [b2,vt] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = vt ) ) } is set
V . {} is set
Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
p is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 V
(S,A,V,p) is Element of the carrier of (DTConMSA A)
q is Element of NonTerminals (DTConMSA A)
the carrier' of S is non empty set
{ the carrier of S} is non empty finite set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
vt is Element of the carrier' of S
r is Element of { the carrier of S}
[vt,r] is V26() set
{vt,r} is non empty finite set
{vt} is non empty finite set
{{vt,r},{vt}} is non empty finite V39() set
the_result_sort_of vt is Element of the carrier of S
i is Element of the carrier of S
FreeSort (A,i) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
bool (TS (DTConMSA A)) is set
A . i is non empty set
{ b1 where b1 is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A) : ( ex b2 being set st
( b2 in A . i & b1 = root-tree [b2,i] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = i ) ) } is set
V . {} is set
Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A 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
FreeSort (A,V) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
bool (FinTrees the carrier of (DTConMSA A)) is set
bool (TS (DTConMSA A)) is set
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
FreeSort A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
Union (FreeSort A) is non empty set
proj1 (FreeSort A) is non empty set
o is set
p is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
q is Element of the carrier of S
FreeSort (A,q) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
bool (TS (DTConMSA A)) is set
(FreeSort A) . q is non empty set
o is set
p is set
(FreeSort A) . p is set
q is Element of the carrier of S
FreeSort (A,q) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
S is set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
o is Element of the carrier of S
FreeSort (A,o) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
bool (TS (DTConMSA A)) is set
p is Element of the carrier of S
FreeSort (A,p) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
A . o is non empty set
the carrier' of S is non empty set
{ b1 where b1 is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A) : ( ex b2 being set st
( b2 in A . o & b1 = root-tree [b2,o] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = o ) ) } is set
q is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
q . {} is set
A . p is non empty set
{ b1 where b1 is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A) : ( ex b2 being set st
( b2 in A . p & b1 = root-tree [b2,p] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = p ) ) } is set
vt is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
vt . {} is set
r is set
[r,o] is V26() set
{r,o} is non empty finite set
{r} is non empty finite set
{{r,o},{r}} is non empty finite V39() set
root-tree [r,o] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
r is set
[r,o] is V26() set
{r,o} is non empty finite set
{r} is non empty finite set
{{r,o},{r}} is non empty finite V39() set
root-tree [r,o] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
i is Element of the carrier' of S
[i, the carrier of S] is V26() set
{i, the carrier of S} is non empty finite set
{i} is non empty finite set
{{i, the carrier of S},{i}} is non empty finite V39() set
i is set
[i,p] is V26() set
{i,p} is non empty finite set
{i} is non empty finite set
{{i,p},{i}} is non empty finite V39() set
root-tree [i,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
t is Element of the carrier' of S
[t, the carrier of S] is V26() set
{t, the carrier of S} is non empty finite set
{t} is non empty finite set
{{t, the carrier of S},{t}} is non empty finite V39() set
the_result_sort_of t is Element of the carrier of S
i is set
[i,p] is V26() set
{i,p} is non empty finite set
{i} is non empty finite set
{{i,p},{i}} is non empty finite V39() set
root-tree [i,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
r is Element of the carrier' of S
[r, the carrier of S] is V26() set
{r, the carrier of S} is non empty finite set
{r} is non empty finite set
{{r, the carrier of S},{r}} is non empty finite V39() set
the_result_sort_of r is Element of the carrier of S
r is Element of the carrier' of S
[r, the carrier of S] is V26() set
{r, the carrier of S} is non empty finite set
{r} is non empty finite set
{{r, the carrier of S},{r}} is non empty finite V39() set
the_result_sort_of r is Element of the carrier of S
i is set
[i,p] is V26() set
{i,p} is non empty finite set
{i} is non empty finite set
{{i,p},{i}} is non empty finite V39() set
root-tree [i,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
i is set
[i,p] is V26() set
{i,p} is non empty finite set
{i} is non empty finite set
{{i,p},{i}} is non empty finite V39() set
root-tree [i,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
t is Element of the carrier' of S
[t, the carrier of S] is V26() set
{t, the carrier of S} is non empty finite set
{t} is non empty finite set
{{t, the carrier of S},{t}} is non empty finite V39() set
the_result_sort_of t is Element of the carrier of S
r is set
[r,o] is V26() set
{r,o} is non empty finite set
{r} is non empty finite set
{{r,o},{r}} is non empty finite V39() set
root-tree [r,o] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
i is Element of the carrier' of S
[i, the carrier of S] is V26() set
{i, the carrier of S} is non empty finite set
{i} is non empty finite set
{{i, the carrier of S},{i}} is non empty finite V39() set
the_result_sort_of i is Element of the carrier of S
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,V) is Element of the carrier of S
f is Element of the carrier of S
A . f is non empty set
o is Element of A . f
[o,f] is V26() set
{o,f} is non empty finite set
{o} is non empty finite set
{{o,f},{o}} is non empty finite V39() set
root-tree [o,f] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
FreeSort (A,(S,A,V)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
bool (TS (DTConMSA A)) is set
A . (S,A,V) is non empty set
the carrier' of S is non empty set
{ b1 where b1 is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A) : ( ex b2 being set st
( b2 in A . (S,A,V) & b1 = root-tree [b2,(S,A,V)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = (S,A,V) ) ) } is set
r is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
r . {} is set
Terminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
V . {} is set
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
{ the carrier of S} is non empty finite set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
i is set
[i,(S,A,V)] is V26() set
{i,(S,A,V)} is non empty finite set
{i} is non empty finite set
{{i,(S,A,V)},{i}} is non empty finite V39() set
root-tree [i,(S,A,V)] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
t is Element of the carrier' of S
[t, the carrier of S] is V26() set
{t, the carrier of S} is non empty finite set
{t} is non empty finite set
{{t, the carrier of S},{t}} is non empty finite V39() set
the_result_sort_of t is Element of the carrier of S
i is set
[i,(S,A,V)] is V26() set
{i,(S,A,V)} is non empty finite set
{i} is non empty finite set
{{i,(S,A,V)},{i}} is non empty finite V39() set
root-tree [i,(S,A,V)] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
V is MSAlgebra over S
the Sorts of V is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of V \/ A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of V \/ A) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of V \/ A))
(S,( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A))) is set
TS (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of V \/ A))
(S,( the Sorts of V \/ A),f) is Element of the carrier of S
o is Element of the carrier of S
the Sorts of V . o is set
p is set
[p,o] is V26() set
{p,o} is non empty finite set
{p} is non empty finite set
{{p,o},{p}} is non empty finite V39() set
root-tree [p,o] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
A . o is non empty set
( the Sorts of V . o) \/ (A . o) is non empty set
( the Sorts of V \/ A) . o is non empty set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
V is MSAlgebra over S
the Sorts of V is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of V \/ A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA ( the Sorts of V \/ A) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty set
FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ( the Sorts of V \/ A))
(S,( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A))) is set
TS (DTConMSA ( the Sorts of V \/ A)) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ( the Sorts of V \/ A)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of V \/ A)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of V \/ A))
(S,( the Sorts of V \/ A),f) is Element of the carrier of S
o is Element of the carrier of S
A . o is non empty set
p is Element of A . o
[p,o] is V26() set
{p,o} is non empty finite set
{p} is non empty finite set
{{p,o},{p}} is non empty finite V39() set
root-tree [p,o] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
the Sorts of V . o is set
( the Sorts of V . o) \/ (A . o) is non empty set
( the Sorts of V \/ A) . o is non empty set
S is non empty non void V75() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
DTConMSA A is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA A) is non empty set
FinTrees the carrier of (DTConMSA A) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA A)
(S,A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
bool (FinTrees the carrier of (DTConMSA A)) is set
TS (DTConMSA A) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA A))
V is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
V . {} is set
(S,A,V) is Element of the carrier of S
f is Element of the carrier' of S
[f, the carrier of S] is V26() set
{f, the carrier of S} is non empty finite set
{f} is non empty finite set
{{f, the carrier of S},{f}} is non empty finite V39() set
the_result_sort_of f is Element of the carrier of S
FreeSort (A,(S,A,V)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
bool (TS (DTConMSA A)) is set
A . (S,A,V) is non empty set
{ b1 where b1 is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A) : ( ex b2 being set st
( b2 in A . (S,A,V) & b1 = root-tree [b2,(S,A,V)] ) or ex b2 being Element of the carrier' of S st
( [b2, the carrier of S] = b1 . {} & the_result_sort_of b2 = (S,A,V) ) ) } is set
vt is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of TS (DTConMSA A)
vt . {} is set
r is set
[r,(S,A,V)] is V26() set
{r,(S,A,V)} is non empty finite set
{r} is non empty finite set
{{r,(S,A,V)},{r}} is non empty finite V39() set
root-tree [r,(S,A,V)] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
r is set
[r,(S,A,V)] is V26() set