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
{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 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 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
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
V is non-empty MSAlgebra over S
the Sorts of V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
f is Element of the carrier of S
the Sorts of V . f is non empty set
A is non empty Relation-like non-empty non empty-yielding 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
o is Element of the Sorts of V . f
(S,V,A,f,o) 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))
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)))
[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
(S,( the Sorts of V \/ A),(S,V,A,f,o)) 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
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
f is Element of the carrier of S
A . f is non empty set
o is Element of A . f
(S,V,A,f,o) 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))
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)))
[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
(S,( the Sorts of V \/ A),(S,V,A,f,o)) is Element of the carrier of S
( 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
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)
V is Element of the carrier' of S
(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
the_result_sort_of V is Element of the carrier of S
f 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))
(S,A,(S,A,V),f) is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,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))
(S,A,(S,A,(S,A,V),f)) 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
[V, the carrier of S] -tree f is Relation-like Function-like DecoratedTree-like set
([V, the carrier of S] -tree f) . {} is 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 Element of the carrier' of S
(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 FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (S,A)
roots f 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
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
(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
the_arity_of V is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
len (the_arity_of V) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom (the_arity_of V) is finite Element of bool NAT
f 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))
len f is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom f is finite Element of bool NAT
roots f 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)
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)
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of bool [: the carrier' of S,( the carrier of S *):]
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
FreeSort A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(FreeSort A) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((FreeSort A) #) is non empty Relation-like the carrier' of S -defined Function-like total set
( the Arity of S * ((FreeSort A) #)) . V is set
dom p is finite Element of bool NAT
q is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
f . q is Relation-like Function-like set
f /. q is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(the_arity_of V) . q is set
(the_arity_of V) /. q is Element of the carrier of S
vt is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,vt) is Element of the carrier of S
FreeSort (A,((the_arity_of V) /. q)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
bool (TS (DTConMSA A)) is 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 Element of the carrier' of S
(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
the_arity_of V is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
len (the_arity_of V) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom (the_arity_of V) is finite Element of bool NAT
f 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))
len f is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom f is finite Element of bool NAT
o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
f . o is Relation-like Function-like set
f /. o is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(the_arity_of V) . o is set
(the_arity_of V) /. o is Element of the carrier of S
p is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,p) 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
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
(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
the_arity_of V is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
f 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))
dom f is finite Element of bool NAT
o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
f . o is Relation-like Function-like set
f /. o is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(the_arity_of V) . o is set
(the_arity_of V) /. o is Element of the carrier of S
p is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,p) is Element of the carrier of S
q is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,q) 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
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))
f is Element of the carrier' of S
the_arity_of f is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
len (the_arity_of f) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom (the_arity_of f) is finite Element of bool NAT
(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
o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom o is finite Element of bool NAT
proj2 o is finite set
p is set
q is set
o . q is set
vt is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
o . vt is set
(the_arity_of f) . vt is set
(the_arity_of f) /. vt is Element of the carrier of S
r is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,r) is Element of the carrier of S
i is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,i) is Element of the carrier of S
q is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() 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)
dom p is finite Element of bool NAT
p . q is Relation-like Function-like set
(the_arity_of f) /. q is Element of the carrier of S
FreeSort (A,((the_arity_of f) /. q)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA A))
bool (TS (DTConMSA A)) is set
o . q is set
(the_arity_of f) . q is set
vt is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,vt) is Element of the carrier of S
vt is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,vt) is Element of the carrier of S
o . q is set
vt is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,vt) is Element of the carrier of S
o . q is set
(the_arity_of f) . q is set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of bool [: the carrier' of S,( the carrier of S *):]
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
FreeSort A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(FreeSort A) # is non empty Relation-like the carrier of S * -defined Function-like total set
the Arity of S * ((FreeSort A) #) is non empty Relation-like the carrier' of S -defined Function-like total set
( the Arity of S * ((FreeSort A) #)) . f is set
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
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
the_arity_of V is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
len (the_arity_of V) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom (the_arity_of V) is finite Element of bool NAT
(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 FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (S,A)
len f is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom f is finite Element of bool NAT
o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
f . o is Relation-like Function-like set
proj2 f is finite set
o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
f . o is Relation-like Function-like 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 Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,q) is Element of the carrier of S
(the_arity_of V) . o is set
o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
f . o is Relation-like Function-like 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 Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,q) is Element of the carrier of S
(the_arity_of V) /. o is Element of the carrier of S
o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
p is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
f . o is Relation-like Function-like set
(S,A,p) is Element of the carrier of S
(the_arity_of V) . o is set
q is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
vt is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
f . q is Relation-like Function-like set
(S,A,vt) is Element of the carrier of S
(the_arity_of V) /. q 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
V 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))
DTConMSA V is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA V) is non empty set
FinTrees the carrier of (DTConMSA V) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA V)
(S,V) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA V))
bool (FinTrees the carrier of (DTConMSA V)) is set
TS (DTConMSA V) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA V))
the carrier' of S is non empty set
f is Element of the carrier' of S
(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
[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
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,f))
proj2 o is finite set
[f, the carrier of S] -tree o is Relation-like Function-like DecoratedTree-like set
p is set
q is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
q is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA V) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding FinSequence of (S,V)
dom p is finite Element of bool NAT
p . q is Relation-like Function-like set
o /. q is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
the_arity_of f is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
(the_arity_of f) . q is set
(the_arity_of f) /. q is Element of the carrier of S
vt is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,vt) is Element of the carrier of S
r is Relation-like the carrier of (DTConMSA V) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,V)
i is Relation-like the carrier of (DTConMSA V) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,V)
(S,V,i) is Element of the carrier of S
vt . {} is set
t is Element of the carrier of S
A . t is non empty set
vt is Element of A . t
[vt,t] is V26() set
{vt,t} is non empty finite set
{vt} is non empty finite set
{{vt,t},{vt}} is non empty finite V39() set
t is Element of the carrier of S
A . t is non empty set
vt is Element of A . t
[vt,t] is V26() set
{vt,t} is non empty finite set
{vt} is non empty finite set
{{vt,t},{vt}} is non empty finite V39() set
root-tree [vt,t] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
V . t is non empty set
vt . {} is set
{ the carrier of S} is non empty finite set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
t is Element of the carrier' of S
vt is Element of { the carrier of S}
[t,vt] is V26() set
{t,vt} is non empty finite set
{t} is non empty finite set
{{t,vt},{t}} is non empty finite V39() set
the_result_sort_of t is Element of the carrier of S
vt . {} is set
{ the carrier of S} is non empty finite set
[: the carrier' of S,{ the carrier of S}:] is Relation-like set
len o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
len (the_arity_of f) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
(S,V,f) is Element of NonTerminals (DTConMSA V)
NonTerminals (DTConMSA V) is non empty Element of bool the carrier of (DTConMSA V)
bool the carrier of (DTConMSA 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
V . f is non empty set
f 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 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
DTConMSA V is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA V) is non empty set
FinTrees the carrier of (DTConMSA V) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA V)
(S,V) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA V))
bool (FinTrees the carrier of (DTConMSA V)) is set
TS (DTConMSA V) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA V))
f is Relation-like the carrier of (DTConMSA V) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,V)
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
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))
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
the Element of the carrier' of S is Element of the carrier' of S
NonTerminals (DTConMSA A) is non empty Element of bool the carrier of (DTConMSA A)
bool the carrier of (DTConMSA A) is set
(S,A, the Element of the carrier' of S) is Element of NonTerminals (DTConMSA A)
f 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 f is Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding SubtreeSeq of f
f -tree the Relation-like NAT -defined FinTrees the carrier of (DTConMSA A) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding SubtreeSeq of f 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 finite DecoratedTree-like finite-order finite-branching Element of (S,A)
p . {} is set
[ the Element of the carrier' of S, the carrier of S] is V26() set
{ the Element of the carrier' of S, the carrier of S} is non empty finite set
{ the Element of the carrier' of S} is non empty finite set
{{ the Element of the carrier' of S, the carrier of S},{ the Element of the carrier' of S}} 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
(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))
bool (S,A) is set
the Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching (S,A) is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching (S,A)
{ the Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching (S,A)} is non empty functional finite V39() constituted-DTrees set
f is non empty functional constituted-DTrees Element of bool (S,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
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
V . {} 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
V . {} 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
S 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
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len A is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom A is finite Element of bool NAT
A . (S + 1) is set
proj2 A 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 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
o is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
<*o*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of NAT
f ^ <*o*> is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
V | f is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching set
p is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
proj1 p is non empty finite Tree-like finite-order finite-branching set
(proj1 V) | f is non empty finite Tree-like finite-order finite-branching set
p . {} is set
q is Element of the carrier of S
A . q is non empty set
vt is Element of A . 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
root-tree [vt,q] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching 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
q is Element of the carrier of S
A . q is non empty set
vt is Element of A . 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
q is Element of the carrier' of S
vt is Element of { the carrier of S}
[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
(S,A,q) 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, the carrier of S] is V26() set
{q, the carrier of S} is non empty finite set
{{q, the carrier of S},{q}} is non empty finite V39() set
r 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,q))
[q, the carrier of S] -tree r is Relation-like Function-like DecoratedTree-like set
len r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
t is Relation-like Function-like DecoratedTree-like set
proj1 t is non empty Tree-like set
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
i + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
r . (i + 1) is Relation-like Function-like set
<*i*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of NAT
vt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 t
<*i*> ^ vt is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*o*> . 1 is set
p | <*o*> is Relation-like Function-like DecoratedTree-like set
o + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
r . (o + 1) is Relation-like Function-like set
T is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 V
V | T is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching set
dom r is finite Element of bool NAT
r /. (o + 1) is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
the_arity_of q is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
(the_arity_of q) . (o + 1) is set
(the_arity_of q) /. (o + 1) is Element of the carrier of S
T is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,A)
(S,A,T) is Element of the carrier of S
f is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 V
V | f is Relation-like the carrier of (DTConMSA A) -valued Function-like finite DecoratedTree-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 Relation-like the carrier of (DTConMSA A) -valued Function-like 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
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 Relation-like the carrier of (DTConMSA A) -valued Function-like 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 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 the carrier of S -defined Function-like total set
f is set
V . f is set
the Sorts of A . f is set
{( the Sorts of A . f)} is non empty finite set
f is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
o is set
f . o is set
the Sorts of A . o is set
{( the Sorts of A . o)} is non empty finite set
p is 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 (S,A)
f is Element of the carrier of S
the Sorts of A . f is set
V . f is non empty set
o is set
p is Element of V . f
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
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
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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
o is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
p is Element of the carrier of S
the Sorts of A . p is non empty set
q is Element of the Sorts 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
root-tree [q,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
root-tree q is trivial Relation-like the Sorts of A . p -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . p)
FinTrees ( the Sorts of A . p) is non empty functional constituted-DTrees DTree-set of the Sorts of A . p
f . {} is set
proj1 (root-tree q) is non empty trivial finite Tree-like finite-order finite-branching set
proj1 f is non empty finite Tree-like finite-order finite-branching set
the carrier' of S is non empty set
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (root-tree q)
f . r is set
(root-tree q) . r is set
succ ((root-tree q),r) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
t is Element of the carrier of S
V . t is non empty set
vt is Element of V . t
[vt,t] is V26() set
{vt,t} is non empty finite set
{vt} is non empty finite set
{{vt,t},{vt}} is non empty finite V39() set
i 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
f . i is set
(root-tree q) . r is Element of the Sorts of A . p
the Sorts of A . t is non empty set
o . t is Relation-like V . t -defined the Sorts of A . t -valued Function-like V29(V . t, the Sorts of A . t) Element of bool [:(V . t),( the Sorts of A . t):]
[:(V . t),( the Sorts of A . t):] is Relation-like set
bool [:(V . t),( the Sorts of A . t):] is set
(o . t) . vt is Element of the Sorts of A . t
(root-tree q) . {} is set
t is Element of the carrier of S
the Sorts of A . t is non empty set
vt is Element of the Sorts of A . t
[vt,t] is V26() set
{vt,t} is non empty finite set
{vt} is non empty finite set
{{vt,t},{vt}} is non empty finite V39() 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
Den (t,A) is Relation-like Args (t,A) -defined Result (t,A) -valued Function-like V29( Args (t,A), Result (t,A)) Element of bool [:(Args (t,A)),(Result (t,A)):]
Args (t,A) is non empty Element of proj2 ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of A #) is non empty set
Result (t,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (t,A)),(Result (t,A)):] is Relation-like set
bool [:(Args (t,A)),(Result (t,A)):] is set
(Den (t,A)) . (succ ((root-tree q),r)) is set
(f . i) `2 is 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
o is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
p is Element of the carrier of S
V . p is non empty set
the Sorts of A . p is non empty set
o . p is Relation-like V . p -defined the Sorts of A . p -valued Function-like V29(V . p, the Sorts of A . p) Element of bool [:(V . p),( the Sorts of A . p):]
[:(V . p),( the Sorts of A . p):] is Relation-like set
bool [:(V . p),( the Sorts of A . p):] is set
q is Element of V . 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
root-tree [q,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
(o . p) . q is Element of the Sorts of A . p
root-tree ((o . p) . q) is trivial Relation-like the Sorts of A . p -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . p)
FinTrees ( the Sorts of A . p) is non empty functional constituted-DTrees DTree-set of the Sorts of A . p
proj1 (root-tree ((o . p) . q)) is non empty trivial finite Tree-like finite-order finite-branching set
proj1 f is non empty finite Tree-like finite-order finite-branching set
the carrier' of S is non empty set
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (root-tree ((o . p) . q))
f . r is set
(root-tree ((o . p) . q)) . r is set
succ ((root-tree ((o . p) . q)),r) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f . {} is set
t is Element of the carrier of S
V . t is non empty set
i 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
vt is Element of V . t
[vt,t] is V26() set
{vt,t} is non empty finite set
{vt} is non empty finite set
{{vt,t},{vt}} is non empty finite V39() set
f . i is set
(root-tree ((o . p) . q)) . r is Element of the Sorts of A . p
the Sorts of A . t is non empty set
o . t is Relation-like V . t -defined the Sorts of A . t -valued Function-like V29(V . t, the Sorts of A . t) Element of bool [:(V . t),( the Sorts of A . t):]
[:(V . t),( the Sorts of A . t):] is Relation-like set
bool [:(V . t),( the Sorts of A . t):] is set
(o . t) . vt is Element of the Sorts of A . t
t is Element of the carrier of S
the Sorts of A . t is non empty set
vt is Element of the Sorts of A . t
[vt,t] is V26() set
{vt,t} is non empty finite set
{vt} is non empty finite set
{{vt,t},{vt}} is non empty finite V39() 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
Den (t,A) is Relation-like Args (t,A) -defined Result (t,A) -valued Function-like V29( Args (t,A), Result (t,A)) Element of bool [:(Args (t,A)),(Result (t,A)):]
Args (t,A) is non empty Element of proj2 ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of A #) is non empty set
Result (t,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (t,A)),(Result (t,A)):] is Relation-like set
bool [:(Args (t,A)),(Result (t,A)):] is set
(Den (t,A)) . (succ ((root-tree ((o . p) . q)),r)) is set
(f . i) `2 is 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 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
o is Element of the carrier' of S
(S,( the Sorts of A \/ V),o) is Element of NonTerminals (DTConMSA ( the Sorts of A \/ V))
NonTerminals (DTConMSA ( the Sorts of A \/ V)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of A \/ V))
bool the carrier of (DTConMSA ( the Sorts of A \/ V)) is set
Den (o,A) is Relation-like Args (o,A) -defined Result (o,A) -valued Function-like V29( Args (o,A), Result (o,A)) Element of bool [:(Args (o,A)),(Result (o,A)):]
Args (o,A) is non empty Element of proj2 ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of A #) is non empty set
Result (o,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (o,A)),(Result (o,A)):] is Relation-like set
bool [:(Args (o,A)),(Result (o,A)):] is set
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (S, the Sorts of A \/ V,(S,( the Sorts of A \/ V),o))
len p is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom p is finite Element of bool NAT
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o),p) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
[o, the carrier of S] is V26() set
{o, the carrier of S} is non empty finite set
{o} is non empty finite set
{{o, the carrier of S},{o}} is non empty finite V39() set
doms p is Relation-like NAT -defined FinTrees -valued Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding FinSequence of FinTrees
dom (doms p) is finite Element of bool NAT
tree (doms p) is non empty finite Tree-like finite-order finite-branching set
[o, the carrier of S] -tree p is Relation-like Function-like DecoratedTree-like set
proj1 ([o, the carrier of S] -tree p) is non empty Tree-like set
Seg (len p) is finite V42( len p) Element of bool NAT
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
len q is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
roots q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (o,A)) . (roots q) is set
((Den (o,A)) . (roots q)) -tree q is Relation-like Function-like DecoratedTree-like set
dom q is finite Element of bool NAT
Seg (len q) is finite V42( len q) Element of bool NAT
proj2 p is finite set
vt is set
doms q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding set
dom (doms q) is finite Element of bool NAT
p . vt is Relation-like Function-like set
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
q . i is set
r is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
t is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
(doms q) . vt is set
proj1 t is non empty finite Tree-like finite-order finite-branching set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
p . r is Relation-like Function-like set
q . r is set
i is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
t is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
vt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding set
vt . r is set
proj1 t is non empty finite Tree-like finite-order finite-branching set
proj1 i is non empty finite Tree-like finite-order finite-branching set
(doms p) . r is set
len (doms q) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
proj1 (((Den (o,A)) . (roots q)) -tree q) is non empty Tree-like set
tree vt is non empty finite Tree-like finite-order finite-branching set
i is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 i is non empty finite Tree-like finite-order finite-branching set
proj1 (S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o),p) is non empty finite Tree-like finite-order finite-branching set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 i
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o),p) . t is set
i . t is set
succ (i,t) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
([o, the carrier of S] -tree p) . {} is set
vt is Element of the carrier of S
V . vt is non empty set
T is Element of V . vt
[T,vt] is V26() set
{T,vt} is non empty finite set
{T} is non empty finite set
{{T,vt},{T}} is non empty finite V39() set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
<*r*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*r*> ^ T is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
r + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
(doms q) . (r + 1) is set
p . (r + 1) is Relation-like Function-like set
q . (r + 1) is set
e is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
r1 is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 r1 is non empty finite Tree-like finite-order finite-branching set
proj1 e is non empty finite Tree-like finite-order finite-branching set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 r1
e . w is set
r1 . w is set
the Sorts of A . vt is non empty set
f . vt is Relation-like V . vt -defined the Sorts of A . vt -valued Function-like V29(V . vt, the Sorts of A . vt) Element of bool [:(V . vt),( the Sorts of A . vt):]
[:(V . vt),( the Sorts of A . vt):] is Relation-like set
bool [:(V . vt),( the Sorts of A . vt):] is set
(f . vt) . T is Element of the Sorts of A . vt
vt is Element of the carrier of S
the Sorts of A . vt is non empty set
T is Element of the Sorts of A . vt
[T,vt] is V26() set
{T,vt} is non empty finite set
{T} is non empty finite set
{{T,vt},{T}} is non empty finite V39() set
r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
<*r*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*r*> ^ T is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
r + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
(doms q) . (r + 1) is set
p . (r + 1) is Relation-like Function-like set
q . (r + 1) is set
e is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
r1 is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 r1 is non empty finite Tree-like finite-order finite-branching set
proj1 e is non empty finite Tree-like finite-order finite-branching set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 r1
e . w is set
r1 . w is set
vt is Element of the carrier' of S
[vt, the carrier of S] is V26() set
{vt, the carrier of S} is non empty finite set
{vt} is non empty finite set
{{vt, the carrier of S},{vt}} is non empty finite V39() set
Den (vt,A) is Relation-like Args (vt,A) -defined Result (vt,A) -valued Function-like V29( Args (vt,A), Result (vt,A)) Element of bool [:(Args (vt,A)),(Result (vt,A)):]
Args (vt,A) is non empty Element of proj2 ( the Sorts of A #)
Result (vt,A) is non empty Element of proj2 the Sorts of A
[:(Args (vt,A)),(Result (vt,A)):] is Relation-like set
bool [:(Args (vt,A)),(Result (vt,A)):] is set
(Den (vt,A)) . (succ (i,t)) is set
T is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
<*T*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*T*> ^ T is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
T + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
(doms q) . (T + 1) is set
p . (T + 1) is Relation-like Function-like set
q . (T + 1) is set
e is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
r1 is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 i
i | r is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 r1 is non empty finite Tree-like finite-order finite-branching set
proj1 e is non empty finite Tree-like finite-order finite-branching set
w is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 r1
e . w is set
r1 . w is set
succ (r1,w) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (vt,A)) . (succ (r1,w)) is 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
o is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
proj1 o is non empty finite Tree-like finite-order finite-branching set
p is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 p is non empty finite Tree-like finite-order finite-branching set
the carrier' of S is non empty set
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 o
(S,( the Sorts of A \/ V),o,q) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
vt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 p
p | vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 (p | vt) is non empty finite Tree-like finite-order finite-branching set
(proj1 p) | vt is non empty finite Tree-like finite-order finite-branching set
proj1 (S,( the Sorts of A \/ V),o,q) is non empty finite Tree-like finite-order finite-branching set
t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 (p | vt)
(S,( the Sorts of A \/ V),o,q) . t is set
(p | vt) . t is set
succ ((p | vt),t) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
vt ^ t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
q ^ t is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
T is Element of the carrier of S
V . T is non empty set
r is Element of V . T
[r,T] is V26() set
{r,T} is non empty finite set
{r} is non empty finite set
{{r,T},{r}} is non empty finite V39() set
T is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 o
(S,( the Sorts of A \/ V),o,T) is Element of the carrier of (DTConMSA ( the Sorts of A \/ V))
vt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 p
p . vt is set
the Sorts of A . T is non empty set
f . T is Relation-like V . T -defined the Sorts of A . T -valued Function-like V29(V . T, the Sorts of A . T) Element of bool [:(V . T),( the Sorts of A . T):]
[:(V . T),( the Sorts of A . T):] is Relation-like set
bool [:(V . T),( the Sorts of A . T):] is set
(f . T) . r is Element of the Sorts of A . T
T is Element of the carrier of S
the Sorts of A . T is non empty set
r is Element of the Sorts of A . T
[r,T] is V26() set
{r,T} is non empty finite set
{r} is non empty finite set
{{r,T},{r}} is non empty finite V39() 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
Den (T,A) is Relation-like Args (T,A) -defined Result (T,A) -valued Function-like V29( Args (T,A), Result (T,A)) Element of bool [:(Args (T,A)),(Result (T,A)):]
Args (T,A) is non empty Element of proj2 ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of A #) is non empty set
Result (T,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (T,A)),(Result (T,A)):] is Relation-like set
bool [:(Args (T,A)),(Result (T,A)):] is set
(Den (T,A)) . (succ ((p | vt),t)) is set
succ (p,vt) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (T,A)) . (succ (p,vt)) is set
succ (p,(vt ^ t)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (T,A)) . (succ (p,(vt ^ t))) is 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 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
o is Element of the carrier' of S
(S,( the Sorts of A \/ V),o) is Element of NonTerminals (DTConMSA ( the Sorts of A \/ V))
NonTerminals (DTConMSA ( the Sorts of A \/ V)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of A \/ V))
bool the carrier of (DTConMSA ( the Sorts of A \/ V)) is set
Den (o,A) is Relation-like Args (o,A) -defined Result (o,A) -valued Function-like V29( Args (o,A), Result (o,A)) Element of bool [:(Args (o,A)),(Result (o,A)):]
Args (o,A) is non empty Element of proj2 ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of A #) is non empty set
Result (o,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (o,A)),(Result (o,A)):] is Relation-like set
bool [:(Args (o,A)),(Result (o,A)):] is set
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (S, the Sorts of A \/ V,(S,( the Sorts of A \/ V),o))
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o),p) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
len p is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom p is finite Element of bool NAT
q is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 q is non empty finite Tree-like finite-order finite-branching set
r is set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
r -tree i is Relation-like Function-like DecoratedTree-like set
doms i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding set
tree (doms i) is non empty Tree-like set
len i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
roots i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (o,A)) . (roots i) is set
((Den (o,A)) . (roots i)) -tree i is Relation-like Function-like DecoratedTree-like set
len (doms i) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
[o, the carrier of S] is V26() set
{o, the carrier of S} is non empty finite set
{o} is non empty finite set
{{o, the carrier of S},{o}} is non empty finite V39() set
[o, the carrier of S] -tree p is Relation-like Function-like DecoratedTree-like set
proj1 ([o, the carrier of S] -tree p) is non empty Tree-like set
doms p is Relation-like NAT -defined FinTrees -valued Function-like finite FinSequence-like FinSubsequence-like Tree-yielding FinTree-yielding FinSequence of FinTrees
tree (doms p) is non empty finite Tree-like finite-order finite-branching set
vt 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 Element of proj1 q
([o, the carrier of S] -tree p) . vt is set
q . vt is set
succ (q,vt) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (o,A)) . (succ (q,vt)) is set
t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
p . t is Relation-like Function-like set
i . t is set
vt is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
proj1 vt is non empty finite Tree-like finite-order finite-branching set
T is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
T + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
<*T*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V42(1) FinSequence-like FinSubsequence-like FinSequence of NAT
T is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 vt
<*T*> ^ T is non empty Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
r is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 q
q | r is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
e is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
len (doms p) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
r1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 ([o, the carrier of S] -tree p)
([o, the carrier of S] -tree p) | r1 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
o is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
the carrier' of S is non empty set
p is Element of the carrier' of S
(S,( the Sorts of A \/ V),p) is Element of NonTerminals (DTConMSA ( the Sorts of A \/ V))
NonTerminals (DTConMSA ( the Sorts of A \/ V)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of A \/ V))
bool the carrier of (DTConMSA ( the Sorts of A \/ V)) is set
q is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (S, the Sorts of A \/ V,(S,( the Sorts of A \/ V),p))
proj2 q is finite set
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),p),q) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
dom q is finite Element of bool NAT
vt is set
q . vt is Relation-like Function-like set
r is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
i is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
t is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
vt is Relation-like Function-like set
proj1 vt is set
len q is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
Seg (len q) is finite V42( len q) Element of bool NAT
r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
i is set
dom r is finite Element of bool NAT
r . i is set
q . i is Relation-like Function-like set
vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
t is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
i . t is set
q . t is Relation-like Function-like set
vt is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
T is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
T is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
Den (p,A) is Relation-like Args (p,A) -defined Result (p,A) -valued Function-like V29( Args (p,A), Result (p,A)) Element of bool [:(Args (p,A)),(Result (p,A)):]
Args (p,A) is non empty Element of proj2 ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of A #) is non empty set
Result (p,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (p,A)),(Result (p,A)):] is Relation-like set
bool [:(Args (p,A)),(Result (p,A)):] is set
roots i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (p,A)) . (roots i) is set
((Den (p,A)) . (roots i)) -tree i is Relation-like Function-like DecoratedTree-like set
t is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
p is Element of the carrier of S
V . p is non empty set
q is Element of V . 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
root-tree [q,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
vt is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
the Sorts of A . p is non empty set
o . p is Relation-like V . p -defined the Sorts of A . p -valued Function-like V29(V . p, the Sorts of A . p) Element of bool [:(V . p),( the Sorts of A . p):]
[:(V . p),( the Sorts of A . p):] is Relation-like set
bool [:(V . p),( the Sorts of A . p):] is set
(o . p) . q is Element of the Sorts of A . p
root-tree ((o . p) . q) is trivial Relation-like the Sorts of A . p -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . p)
FinTrees ( the Sorts of A . p) is non empty functional constituted-DTrees DTree-set of the Sorts of A . p
p is Element of the carrier of S
the Sorts of A . p is non empty set
q is Element of the Sorts 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
root-tree [q,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
vt is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
root-tree q is trivial Relation-like the Sorts of A . p -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . p)
FinTrees ( the Sorts of A . p) is non empty functional constituted-DTrees DTree-set of the Sorts of A . p
p is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
q is Relation-like Function-like 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 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
o is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
p is Element of the carrier of S
V . p is non empty set
q is Element of V . p
(S,A,V,p,q) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
[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
root-tree [q,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
r is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 vt is non empty finite Tree-like finite-order finite-branching set
proj1 (S,A,V,p,q) is non empty finite Tree-like finite-order finite-branching set
(root-tree [q,p]) . {} is set
vt . {} is set
the Sorts of A . p is non empty set
o . p is Relation-like V . p -defined the Sorts of A . p -valued Function-like V29(V . p, the Sorts of A . p) Element of bool [:(V . p),( the Sorts of A . p):]
[:(V . p),( the Sorts of A . p):] is Relation-like set
bool [:(V . p),( the Sorts of A . p):] is set
(o . p) . q is Element of the Sorts of A . p
root-tree ((o . p) . q) is trivial Relation-like the Sorts of A . p -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . p)
FinTrees ( the Sorts of A . p) is non empty functional constituted-DTrees DTree-set of the Sorts of A . p
proj1 r is non empty finite Tree-like finite-order finite-branching set
r . {} is set
the carrier' of S is non empty set
p is Element of the carrier' of S
(S,( the Sorts of A \/ V),p) is Element of NonTerminals (DTConMSA ( the Sorts of A \/ V))
NonTerminals (DTConMSA ( the Sorts of A \/ V)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of A \/ V))
bool the carrier of (DTConMSA ( the Sorts of A \/ V)) is set
q is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (S, the Sorts of A \/ V,(S,( the Sorts of A \/ V),p))
proj2 q is finite set
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),p),q) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
r is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
i is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
len q is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
Den (p,A) is Relation-like Args (p,A) -defined Result (p,A) -valued Function-like V29( Args (p,A), Result (p,A)) Element of bool [:(Args (p,A)),(Result (p,A)):]
Args (p,A) is non empty Element of proj2 ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of A #) is non empty set
Result (p,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (p,A)),(Result (p,A)):] is Relation-like set
bool [:(Args (p,A)),(Result (p,A)):] is set
dom q is finite Element of bool NAT
t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
len t is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
roots t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (p,A)) . (roots t) is set
((Den (p,A)) . (roots t)) -tree t is Relation-like Function-like DecoratedTree-like set
vt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
len vt is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
roots vt is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (p,A)) . (roots vt) is set
((Den (p,A)) . (roots vt)) -tree vt is Relation-like Function-like DecoratedTree-like set
T is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
T + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
q . (T + 1) is Relation-like Function-like set
vt . (T + 1) is set
T is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
t . (T + 1) is set
r is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
e is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
T is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() set
dom t is finite Element of bool NAT
t . T is set
vt . T is set
T is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
T + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom vt is finite Element of bool NAT
Seg (len vt) is finite V42( len vt) Element of bool NAT
Seg (len t) is finite V42( len t) Element of bool NAT
p is Element of the carrier of S
the Sorts of A . p is non empty set
q is Element of the Sorts of A . p
(S,A,V,p,q) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
[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
root-tree [q,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
r is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
proj1 vt is non empty finite Tree-like finite-order finite-branching set
proj1 (S,A,V,p,q) is non empty finite Tree-like finite-order finite-branching set
(root-tree [q,p]) . {} is set
vt . {} is set
root-tree q is trivial Relation-like the Sorts of A . p -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . p)
FinTrees ( the Sorts of A . p) is non empty functional constituted-DTrees DTree-set of the Sorts of A . p
proj1 r is non empty finite Tree-like finite-order finite-branching set
r . {} is set
p is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
q is Relation-like Function-like 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 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
(S,( the Sorts of A \/ V),f) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),f) is non empty set
o is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
p is Element of the carrier of S
V . p is non empty set
q is Element of V . p
(S,A,V,p,q) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
[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
root-tree [q,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
(S,( the Sorts of A \/ V),(S,A,V,p,q)) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),(S,A,V,p,q)) is non empty set
vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
vt . {} is set
the Sorts of A . p is non empty set
o . p is Relation-like V . p -defined the Sorts of A . p -valued Function-like V29(V . p, the Sorts of A . p) Element of bool [:(V . p),( the Sorts of A . p):]
[:(V . p),( the Sorts of A . p):] is Relation-like set
bool [:(V . p),( the Sorts of A . p):] is set
(o . p) . q is Element of the Sorts of A . p
root-tree ((o . p) . q) is trivial Relation-like the Sorts of A . p -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . p)
FinTrees ( the Sorts of A . p) is non empty functional constituted-DTrees DTree-set of the Sorts of A . p
the carrier' of S is non empty set
p is Element of the carrier' of S
(S,( the Sorts of A \/ V),p) is Element of NonTerminals (DTConMSA ( the Sorts of A \/ V))
NonTerminals (DTConMSA ( the Sorts of A \/ V)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of A \/ V))
bool the carrier of (DTConMSA ( the Sorts of A \/ V)) is set
q is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (S, the Sorts of A \/ V,(S,( the Sorts of A \/ V),p))
proj2 q is finite set
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),p),q) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),p),q)) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),p),q)) is non empty set
vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
vt . {} is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V29( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
proj1 ( the ResultSort of S * the Sorts of A) is non empty set
len q is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
Den (p,A) is Relation-like Args (p,A) -defined Result (p,A) -valued Function-like V29( Args (p,A), Result (p,A)) Element of bool [:(Args (p,A)),(Result (p,A)):]
Args (p,A) is non empty Element of proj2 ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of A #) is non empty set
Result (p,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (p,A)),(Result (p,A)):] is Relation-like set
bool [:(Args (p,A)),(Result (p,A)):] is set
dom q is finite Element of bool NAT
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
len i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
roots i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (p,A)) . (roots i) is set
((Den (p,A)) . (roots i)) -tree i is Relation-like Function-like DecoratedTree-like set
the_arity_of p is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
proj2 (the_arity_of p) is finite set
proj1 the Sorts of A is non empty set
dom (roots i) is finite Element of bool NAT
dom i is finite Element of bool NAT
Seg (len i) is finite V42( len i) Element of bool NAT
len (the_arity_of p) is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
Seg (len (the_arity_of p)) is finite V42( len (the_arity_of p)) Element of bool NAT
dom (the_arity_of p) is finite Element of bool NAT
(the_arity_of p) * the Sorts of A is Relation-like non-empty NAT -defined Function-like finite set
proj1 ((the_arity_of p) * the Sorts of A) is finite set
t is set
vt is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
vt + 1 is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
i . (vt + 1) is set
(roots i) . (vt + 1) is set
q . (vt + 1) is Relation-like Function-like set
q /. (vt + 1) is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
(the_arity_of p) . (vt + 1) is set
(the_arity_of p) /. (vt + 1) is Element of the carrier of S
T is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
T is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
T . {} is set
(S,( the Sorts of A \/ V),T) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),T) is non empty set
(roots i) . t is set
((the_arity_of p) * the Sorts of A) . t is set
r is Relation-like Function-like DecoratedTree-like set
r . {} is set
e is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
(S,( the Sorts of A \/ V),e) is Element of the carrier of S
product ((the_arity_of p) * the Sorts of A) is set
( the Sorts of A #) . (the_arity_of p) is set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V29( the carrier' of S, the carrier of S * ) Element of bool [: the carrier' of S,( the carrier of S *):]
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
the Arity of S . p is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of A #) . ( the Arity of S . p) is set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like total set
proj1 ( the Arity of S * ( the Sorts of A #)) is non empty set
( the Arity of S * ( the Sorts of A #)) . p is set
( the ResultSort of S * the Sorts of A) . p is non empty set
the ResultSort of S . p is Element of the carrier of S
the Sorts of A . ( the ResultSort of S . p) is non empty set
the_result_sort_of p is Element of the carrier of S
the Sorts of A . (the_result_sort_of p) is non empty set
p is Element of the carrier of S
the Sorts of A . p is non empty set
q is Element of the Sorts of A . p
(S,A,V,p,q) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
[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
root-tree [q,p] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
(S,( the Sorts of A \/ V),(S,A,V,p,q)) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),(S,A,V,p,q)) is non empty set
vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
vt . {} is set
root-tree q is trivial Relation-like the Sorts of A . p -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . p)
FinTrees ( the Sorts of A . p) is non empty functional constituted-DTrees DTree-set of the Sorts of A . p
p is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
p . {} is 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
(S,( the Sorts of A \/ V),f) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),f) is non empty set
o is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
p is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
p . {} is set
q is Element of the Sorts of A . (S,( the Sorts of A \/ V),f)
vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
p is Element of the Sorts of A . (S,( the Sorts of A \/ V),f)
vt . {} is set
r is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
q is Element of the Sorts of A . (S,( the Sorts of A \/ V),f)
r . {} is 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
o is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
(S,A,V,o,f) is Element of the Sorts of A . (S,( the Sorts of A \/ V),o)
(S,( the Sorts of A \/ V),o) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),o) is non empty set
p is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
p . {} is set
q is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
q . {} is 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
o is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
proj1 o is non empty finite Tree-like finite-order finite-branching set
p is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 o
p . q is set
(S,( the Sorts of A \/ V),o,q) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
(S,A,V,(S,( the Sorts of A \/ V),o,q),f) is Element of the Sorts of A . (S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o,q))
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o,q)) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o,q)) is non empty set
proj1 p is non empty finite Tree-like finite-order finite-branching set
vt is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 p
vt ^ {} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(proj1 p) | q is non empty Tree-like set
p | vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
(p | vt) . (<*> NAT) is 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
f is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
o is Element of the carrier of S
the Sorts of A . o is non empty set
p is Element of the Sorts of A . o
(S,A,V,o,p) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
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)))
[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
(S,A,V,(S,A,V,o,p),f) is Element of the Sorts of A . (S,( the Sorts of A \/ V),(S,A,V,o,p))
(S,( the Sorts of A \/ V),(S,A,V,o,p)) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),(S,A,V,o,p)) is non empty set
root-tree p is trivial Relation-like the Sorts of A . o -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . o)
FinTrees ( the Sorts of A . o) is non empty functional constituted-DTrees DTree-set of the Sorts of A . o
(root-tree p) . {} is 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
f is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
o is Element of the carrier of S
V . o is non empty set
the Sorts of A . o is non empty set
f . o is Relation-like V . o -defined the Sorts of A . o -valued Function-like V29(V . o, the Sorts of A . o) Element of bool [:(V . o),( the Sorts of A . o):]
[:(V . o),( the Sorts of A . o):] is Relation-like set
bool [:(V . o),( the Sorts of A . o):] is set
p is Element of V . o
(S,A,V,o,p) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
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)))
[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
(S,A,V,(S,A,V,o,p),f) is Element of the Sorts of A . (S,( the Sorts of A \/ V),(S,A,V,o,p))
(S,( the Sorts of A \/ V),(S,A,V,o,p)) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),(S,A,V,o,p)) is non empty set
(f . o) . p is Element of the Sorts of A . o
root-tree ((f . o) . p) is trivial Relation-like the Sorts of A . o -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees ( the Sorts of A . o)
FinTrees ( the Sorts of A . o) is non empty functional constituted-DTrees DTree-set of the Sorts of A . o
(root-tree ((f . o) . p)) . {} is 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 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
V is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total (S,A)
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)))
f is non empty Relation-like the carrier of S -defined Function-like total V60() ManySortedFunction of V, the Sorts of A
o is Element of the carrier' of S
(S,( the Sorts of A \/ V),o) is Element of NonTerminals (DTConMSA ( the Sorts of A \/ V))
NonTerminals (DTConMSA ( the Sorts of A \/ V)) is non empty Element of bool the carrier of (DTConMSA ( the Sorts of A \/ V))
bool the carrier of (DTConMSA ( the Sorts of A \/ V)) is set
Den (o,A) is Relation-like Args (o,A) -defined Result (o,A) -valued Function-like V29( Args (o,A), Result (o,A)) Element of bool [:(Args (o,A)),(Result (o,A)):]
Args (o,A) is non empty Element of proj2 ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of A #) is non empty set
Result (o,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (o,A)),(Result (o,A)):] is Relation-like set
bool [:(Args (o,A)),(Result (o,A)):] is set
p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding (S, the Sorts of A \/ V,(S,( the Sorts of A \/ V),o))
len p is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
dom p is finite Element of bool NAT
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o),p) is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
(S,A,V,(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o),p),f) is Element of the Sorts of A . (S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o),p))
(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o),p)) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),(S,( the Sorts of A \/ V),o),p)) is non empty set
q is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len q is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
(Den (o,A)) . q is set
vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set
len r is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
roots r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Den (o,A)) . (roots r) is set
((Den (o,A)) . (roots r)) -tree r is Relation-like Function-like DecoratedTree-like set
dom q is finite Element of bool NAT
dom r is finite Element of bool NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() ext-real V32() Element of NAT
p . i is Relation-like Function-like set
r . i is set
t is Relation-like the carrier of (DTConMSA ( the Sorts of A \/ V)) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of (S,( the Sorts of A \/ V))
vt is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
T is Relation-like Function-like DecoratedTree-like set
T is Relation-like Function-like DecoratedTree-like set
q . i is set
(S,A,V,t,f) is Element of the Sorts of A . (S,( the Sorts of A \/ V),t)
(S,( the Sorts of A \/ V),t) is Element of the carrier of S
the Sorts of A . (S,( the Sorts of A \/ V),t) is non empty set
T . {} is set
((Den (o,A)) . q) -tree r is Relation-like Function-like DecoratedTree-like set
(((Den (o,A)) . q) -tree r) . {} is set