:: MSATERM semantic presentation

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

F

the carrier of F

F

the carrier' of F

DTConMSA F

the carrier of (DTConMSA F

FinTrees the carrier of (DTConMSA F

(F

bool (FinTrees the carrier of (DTConMSA F

TS (DTConMSA F

V is Element of the carrier of (DTConMSA F

f is Relation-like NAT -defined FinTrees the carrier of (DTConMSA F

roots f is Relation-like NAT -defined the carrier of (DTConMSA F

proj2 f is finite set

V -tree f is Relation-like the carrier of (DTConMSA F

{ b

NonTerminals (DTConMSA F

bool the carrier of (DTConMSA F

o is Element of NonTerminals (DTConMSA F

{ the carrier of F

[: the carrier' of F

q is Element of the carrier' of F

vt is Element of { the carrier of F

[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 F

{q, the carrier of F

{{q, the carrier of F

(F

p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA F

r is Relation-like NAT -defined FinTrees the carrier of (DTConMSA F

proj2 r is finite set

i is Relation-like the carrier of (DTConMSA F

Terminals (DTConMSA F

bool the carrier of (DTConMSA F

V is Element of the carrier of (DTConMSA F

root-tree V is trivial Relation-like the carrier of (DTConMSA F

f is Element of the carrier of F

F

o is Element of 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 F

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

F

the carrier of F

F

the Sorts of F

F

the carrier' of F

the Sorts of F

DTConMSA ( the Sorts of F

the carrier of (DTConMSA ( the Sorts of F

FinTrees the carrier of (DTConMSA ( the Sorts of F

(F

bool (FinTrees the carrier of (DTConMSA ( the Sorts of F

TS (DTConMSA ( the Sorts of F

V is Element of the carrier of (DTConMSA ( the Sorts of F

f is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of F

roots f is Relation-like NAT -defined the carrier of (DTConMSA ( the Sorts of F

proj2 f is finite set

V -tree f is Relation-like the carrier of (DTConMSA ( the Sorts of F

{ b

NonTerminals (DTConMSA ( the Sorts of F

bool the carrier of (DTConMSA ( the Sorts of F

o is Element of NonTerminals (DTConMSA ( the Sorts of F

{ the carrier of F

[: the carrier' of F

q is Element of the carrier' of F

vt is Element of { the carrier of F

[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 F

{q, the carrier of F

{{q, the carrier of F

(F

p is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of F

r is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of F

proj2 r is finite set

i is Relation-like the carrier of (DTConMSA ( the Sorts of F

Terminals (DTConMSA ( the Sorts of F

bool the carrier of (DTConMSA ( the Sorts of F

V is Element of the carrier of (DTConMSA ( the Sorts of F

root-tree V is trivial Relation-like the carrier of (DTConMSA ( the Sorts of F

p is Element of the carrier of F

F

o is set

f is Element of the carrier of F

the Sorts of 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

q is Element of F

[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 F

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)

F

the carrier of F

F

the Sorts of F

F

the carrier' of F

the Sorts of F

DTConMSA ( the Sorts of F

the carrier of (DTConMSA ( the Sorts of F

FinTrees the carrier of (DTConMSA ( the Sorts of F

(F

bool (FinTrees the carrier of (DTConMSA ( the Sorts of F

TS (DTConMSA ( the Sorts of F

S is Element of the carrier of F

the Sorts of F

A is Element of the Sorts of F

(F

[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 F

F

A is Element of F

(F

[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 F

(F

NonTerminals (DTConMSA ( the Sorts of F

bool the carrier of (DTConMSA ( the Sorts of F

A is Relation-like NAT -defined FinTrees the carrier of (DTConMSA ( the Sorts of F

proj2 A is finite set

(F

S is Relation-like the carrier of (DTConMSA ( the Sorts of F

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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

{ b

( b

( [b

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