:: MSAFREE3 semantic presentation

REAL is set

NAT is non empty V17() V18() V19() Element of bool REAL

bool REAL is non empty set

NAT is non empty V17() V18() V19() set

bool NAT is non empty set

bool NAT is non empty set

{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V163() V164() ext-real set

the empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V163() V164() ext-real set is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V163() V164() ext-real set

1 is non empty V17() V18() V19() V23() V163() V164() ext-real Element of NAT

{{},1} is non empty set

Trees is non empty constituted-Trees set

bool Trees is non empty set

FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees

PeanoNat is non empty strict 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 functional constituted-DTrees Element of bool (FinTrees the carrier of PeanoNat)

bool (FinTrees the carrier of PeanoNat) is non empty set

[:(TS PeanoNat),NAT:] is Relation-like set

bool [:(TS PeanoNat),NAT:] is non empty set

[:NAT,(TS PeanoNat):] is Relation-like set

bool [:NAT,(TS PeanoNat):] is non empty set

COMPLEX is set

RAT is set

INT is set

[:COMPLEX,COMPLEX:] is Relation-like set

bool [:COMPLEX,COMPLEX:] is non empty set

[:COMPLEX,REAL:] is Relation-like set

bool [:COMPLEX,REAL:] is non empty set

2 is non empty V17() V18() V19() V23() V163() V164() ext-real Element of NAT

3 is non empty V17() V18() V19() V23() V163() V164() ext-real Element of NAT

proj1 {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V163() V164() ext-real set

proj2 {} is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V163() V164() ext-real set

0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V163() V164() ext-real Element of NAT

K169(0) is non empty V39() set

{{}} is non empty functional set

<*> NAT is empty proper Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V163() V164() ext-real FinSequence of NAT

[:NAT,NAT:] is non empty Relation-like set

S is non empty non void feasible V159() ManySortedSign

X is non empty MSAlgebra over S

the Sorts of X is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

the carrier of S is non empty set

Union the Sorts of X is set

dom the Sorts of X is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

Y is set

the Sorts of X . Y is set

the Element of the Sorts of X . Y is Element of the Sorts of X . Y

S is non empty non void feasible V159() ManySortedSign

S is set

X is Relation-like S -defined Function-like V24(S) set

Y is Relation-like S -defined Function-like V24(S) Function-yielding V54() set

doms Y is Relation-like S -defined Function-like V24(S) set

Y .:.: X is Relation-like S -defined Function-like V24(S) set

Y "" (Y .:.: X) is Relation-like S -defined Function-like V24(S) set

dom Y is Element of bool S

bool S is non empty set

A is set

Y . A is Relation-like Function-like set

X . A is set

(doms Y) . A is set

proj1 (Y . A) is set

(Y "" (Y .:.: X)) . A is set

(Y .:.: X) . A is set

(Y . A) " ((Y .:.: X) . A) is set

(Y . A) .: (X . A) is set

(Y . A) " ((Y . A) .: (X . A)) is set

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

{0} is non empty functional Element of bool NAT

the carrier of S --> {0} is non empty Relation-like non-empty non empty-yielding the carrier of S -defined bool NAT -valued Function-like constant V24( the carrier of S) V25( the carrier of S, bool NAT) Element of bool [: the carrier of S,(bool NAT):]

[: the carrier of S,(bool NAT):] is non empty Relation-like set

bool [: the carrier of S,(bool NAT):] is non empty set

X \/ ( the carrier of S --> {0}) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

FreeMSA (X \/ ( the carrier of S --> {0})) is strict non-empty free feasible non empty MSAlgebra over S

the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

Reverse (X \/ ( the carrier of S --> {0})) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) Function-yielding V54() ManySortedFunction of FreeGen (X \/ ( the carrier of S --> {0})),X \/ ( the carrier of S --> {0})

FreeGen (X \/ ( the carrier of S --> {0})) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) free GeneratorSet of FreeMSA (X \/ ( the carrier of S --> {0}))

(Reverse (X \/ ( the carrier of S --> {0}))) "" X is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

Y is strict MSAlgebra over S

o is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0})))

GenMSAlg o is strict MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))

A is strict MSAlgebra over S

a is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0})))

GenMSAlg a is strict MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))

a is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0})))

GenMSAlg a is strict MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))

S is set

X is non empty non void feasible V159() ManySortedSign

the carrier of X is non empty set

Y is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

DTConMSA Y is non empty strict DTConstrStr

the carrier of (DTConMSA Y) is non empty set

A is Element of the carrier of X

[S,A] is V1() set

{S,A} is non empty set

{S} is non empty set

{{S,A},{S}} is non empty set

Y . A is set

the carrier' of X is non empty set

{ the carrier of X} is non empty set

[: the carrier' of X,{ the carrier of X}:] is non empty Relation-like set

coprod Y is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

Union (coprod Y) is set

[: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y)) is non empty set

REL Y is Relation-like [: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y)) -defined ([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y))) * -valued Element of bool [:([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y))),(([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y))) *):]

([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y))) * is non empty functional FinSequence-membered M8([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y)))

[:([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y))),(([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y))) *):] is non empty Relation-like set

bool [:([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y))),(([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y))) *):] is non empty set

DTConstrStr(# ([: the carrier' of X,{ the carrier of X}:] \/ (Union (coprod Y))),(REL Y) #) is strict DTConstrStr

dom (coprod Y) is non empty Element of bool the carrier of X

bool the carrier of X is non empty set

o is set

(coprod Y) . o is set

coprod (o,Y) is set

Y . o is set

a is set

[a,o] is V1() set

{a,o} is non empty set

{a} is non empty set

{{a,o},{a}} is non empty set

coprod (A,Y) is set

(coprod Y) . A is set

S is set

X is non empty non void feasible V159() ManySortedSign

the carrier of X is non empty set

Y is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

Reverse Y is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) Function-yielding V54() ManySortedFunction of FreeGen Y,Y

FreeGen Y is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) free GeneratorSet of FreeMSA Y

FreeMSA Y is strict non-empty free feasible non empty MSAlgebra over X

A is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

(Reverse Y) "" A is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

o is Element of the carrier of X

A . o is set

Y . o is non empty set

[S,o] is V1() set

{S,o} is non empty set

{S} is non empty set

{{S,o},{S}} is non empty set

root-tree [S,o] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set

((Reverse Y) "" A) . o is set

(Reverse Y) . o is Relation-like (FreeGen Y) . o -defined Y . o -valued Function-like V25((FreeGen Y) . o,Y . o) Element of bool [:((FreeGen Y) . o),(Y . o):]

(FreeGen Y) . o is non empty set

[:((FreeGen Y) . o),(Y . o):] is non empty Relation-like set

bool [:((FreeGen Y) . o),(Y . o):] is non empty set

Reverse (o,Y) is Relation-like FreeGen (o,Y) -defined Y . o -valued Function-like V25( FreeGen (o,Y),Y . o) Element of bool [:(FreeGen (o,Y)),(Y . o):]

FreeGen (o,Y) is non empty Element of bool ((FreeSort Y) . o)

FreeSort Y is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

(FreeSort Y) . o is non empty set

bool ((FreeSort Y) . o) is non empty set

[:(FreeGen (o,Y)),(Y . o):] is non empty Relation-like set

bool [:(FreeGen (o,Y)),(Y . o):] is non empty set

dom (Reverse (o,Y)) is Element of bool (FreeGen (o,Y))

bool (FreeGen (o,Y)) is non empty set

DTConMSA Y is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA Y) is non empty set

((Reverse Y) . o) . (root-tree [S,o]) is set

[S,o] `1 is set

((Reverse Y) . o) " (A . o) is Element of bool ((FreeGen Y) . o)

bool ((FreeGen Y) . o) is non empty set

(Reverse (o,Y)) . (root-tree [S,o]) is set

a is set

[a,o] is V1() set

{a,o} is non empty set

{a} is non empty set

{{a,o},{a}} is non empty set

root-tree [a,o] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set

S is set

X is non empty non void feasible V159() ManySortedSign

the carrier of X is non empty set

Y is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

(X,Y) is strict MSAlgebra over X

the Sorts of (X,Y) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

A is Element of the carrier of X

Y . A is set

[S,A] is V1() set

{S,A} is non empty set

{S} is non empty set

{{S,A},{S}} is non empty set

root-tree [S,A] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set

the Sorts of (X,Y) . A is set

the carrier of X --> {0} is non empty Relation-like non-empty non empty-yielding the carrier of X -defined bool NAT -valued Function-like constant V24( the carrier of X) V25( the carrier of X, bool NAT) Element of bool [: the carrier of X,(bool NAT):]

[: the carrier of X,(bool NAT):] is non empty Relation-like set

bool [: the carrier of X,(bool NAT):] is non empty set

Y \/ ( the carrier of X --> {0}) is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

FreeMSA (Y \/ ( the carrier of X --> {0})) is strict non-empty free feasible non empty MSAlgebra over X

the Sorts of (FreeMSA (Y \/ ( the carrier of X --> {0}))) is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

Reverse (Y \/ ( the carrier of X --> {0})) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) Function-yielding V54() ManySortedFunction of FreeGen (Y \/ ( the carrier of X --> {0})),Y \/ ( the carrier of X --> {0})

FreeGen (Y \/ ( the carrier of X --> {0})) is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) free GeneratorSet of FreeMSA (Y \/ ( the carrier of X --> {0}))

(Reverse (Y \/ ( the carrier of X --> {0}))) "" Y is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

a is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) ManySortedSubset of the Sorts of (FreeMSA (Y \/ ( the carrier of X --> {0})))

GenMSAlg a is strict MSSubAlgebra of FreeMSA (Y \/ ( the carrier of X --> {0}))

a . A is set

(Y \/ ( the carrier of X --> {0})) . A is non empty set

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

the carrier' of S is non empty set

X is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,X) is strict MSAlgebra over S

the Sorts of (S,X) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

Y is Element of the carrier' of S

the_arity_of Y 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)

[Y, the carrier of S] is V1() set

{Y, the carrier of S} is non empty set

{Y} is non empty set

{{Y, the carrier of S},{Y}} is non empty set

root-tree [Y, the carrier of S] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set

the_result_sort_of Y is Element of the carrier of S

the Sorts of (S,X) . (the_result_sort_of Y) is set

the carrier of S --> {0} is non empty Relation-like non-empty non empty-yielding the carrier of S -defined bool NAT -valued Function-like constant V24( the carrier of S) V25( the carrier of S, bool NAT) Element of bool [: the carrier of S,(bool NAT):]

[: the carrier of S,(bool NAT):] is non empty Relation-like set

bool [: the carrier of S,(bool NAT):] is non empty set

X \/ ( the carrier of S --> {0}) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

FreeMSA (X \/ ( the carrier of S --> {0})) is strict non-empty free feasible non empty MSAlgebra over S

Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))) is non empty functional Element of proj2 ( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #)

the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set

proj2 ( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) is non empty set

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V25( the carrier' of S, the carrier of S * ) Function-yielding V54() Element of bool [: the carrier' of S,( the carrier of S *):]

[: the carrier' of S,( the carrier of S *):] is non empty Relation-like set

bool [: the carrier' of S,( the carrier of S *):] is non empty set

the Arity of S * ( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set

( the Arity of S * ( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #)) . Y is set

the Arity of S . Y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) . ( the Arity of S . Y) is set

<*> the carrier of S is empty proper Relation-like non-empty empty-yielding NAT -defined the carrier of S -valued Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() finite FinSequence-like FinSubsequence-like FinSequence-membered constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Function-yielding V54() V163() V164() ext-real FinSequence of the carrier of S

[:NAT, the carrier of S:] is non empty Relation-like set

( the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) #) . (<*> the carrier of S) is set

Den (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))) is Relation-like Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))) -defined Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))) -valued Function-like V25( Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))), Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))) Element of bool [:(Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))),(Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))):]

Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))) is non empty Element of proj2 the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0})))

proj2 the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) is non empty set

[:(Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))),(Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))):] is non empty Relation-like set

bool [:(Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))),(Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))):] is non empty set

dom (Den (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))) is functional Element of bool (Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))))

bool (Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))) is non empty set

Reverse (X \/ ( the carrier of S --> {0})) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) Function-yielding V54() ManySortedFunction of FreeGen (X \/ ( the carrier of S --> {0})),X \/ ( the carrier of S --> {0})

FreeGen (X \/ ( the carrier of S --> {0})) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) free GeneratorSet of FreeMSA (X \/ ( the carrier of S --> {0}))

(Reverse (X \/ ( the carrier of S --> {0}))) "" X is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

a is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0})))

GenMSAlg a is strict MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))

o is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0})))

o # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set

the Arity of S * (o #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set

( the Arity of S * (o #)) . Y is set

(o #) . ( the Arity of S . Y) is set

(o #) . (<*> the carrier of S) is set

(Den (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))) | (( the Arity of S * (o #)) . Y) is Relation-like Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))) -defined ( the Arity of S * (o #)) . Y -defined Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))) -defined Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))) -valued Function-like Element of bool [:(Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))),(Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))):]

DTConMSA (X \/ ( the carrier of S --> {0})) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) is non empty set

FinTrees the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA (X \/ ( the carrier of S --> {0})))

Sym (Y,(X \/ ( the carrier of S --> {0}))) is Element of NonTerminals (DTConMSA (X \/ ( the carrier of S --> {0})))

NonTerminals (DTConMSA (X \/ ( the carrier of S --> {0}))) is non empty Element of bool the carrier of (DTConMSA (X \/ ( the carrier of S --> {0})))

bool the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) is non empty set

the Relation-like NAT -defined FinTrees the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() ArgumentSeq of Sym (Y,(X \/ ( the carrier of S --> {0}))) is Relation-like NAT -defined FinTrees the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() ArgumentSeq of Sym (Y,(X \/ ( the carrier of S --> {0})))

z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of Args (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))

[Y, the carrier of S] -tree z is Relation-like Function-like DecoratedTree-like set

(Den (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))) . z is set

rng (Den (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))) is Element of bool (Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))))

bool (Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))) is non empty set

z is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0})))

GenMSAlg z is strict MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))

rng ((Den (Y,(FreeMSA (X \/ ( the carrier of S --> {0}))))) | (( the Arity of S * (o #)) . Y)) is Element of bool (Result (Y,(FreeMSA (X \/ ( the carrier of S --> {0})))))

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V25( 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 non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * o is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set

( the ResultSort of S * o) . Y is set

the ResultSort of S . Y is set

o . ( the ResultSort of S . Y) is set

o . (the_result_sort_of Y) is set

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

(S,X) is strict MSAlgebra over S

Y is set

X . Y is set

A is Element of the carrier of S

X . A is set

the Element of X . A is Element of X . A

[ the Element of X . A,A] is V1() set

{ the Element of X . A,A} is non empty set

{ the Element of X . A} is non empty set

{{ the Element of X . A,A},{ the Element of X . A}} is non empty set

root-tree [ the Element of X . A,A] is trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set

the Sorts of (S,X) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

the Sorts of (S,X) . A is set

S is set

X is non empty non void feasible V159() ManySortedSign

the carrier of X is non empty set

Y is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

FreeMSA Y is strict non-empty free feasible non empty MSAlgebra over X

the Sorts of (FreeMSA Y) is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

Union the Sorts of (FreeMSA Y) is non empty set

DTConMSA Y is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA Y) is non empty set

FinTrees the carrier of (DTConMSA Y) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA Y)

X -Terms Y is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA Y))

bool (FinTrees the carrier of (DTConMSA Y)) is non empty set

TS (DTConMSA Y) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA Y))

FreeSort Y is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

proj2 (FreeSort Y) is non empty set

union (proj2 (FreeSort Y)) is set

Union (FreeSort Y) is non empty set

FreeOper Y is non empty Relation-like the carrier' of X -defined Function-like V24( the carrier' of X) Function-yielding V54() ManySortedFunction of the Arity of X * ((FreeSort Y) #), the ResultSort of X * (FreeSort Y)

the carrier' of X is non empty set

the Arity of X is Relation-like the carrier' of X -defined the carrier of X * -valued Function-like V25( the carrier' of X, the carrier of X * ) Function-yielding V54() Element of bool [: the carrier' of X,( the carrier of X *):]

the carrier of X * is non empty functional FinSequence-membered M8( the carrier of X)

[: the carrier' of X,( the carrier of X *):] is non empty Relation-like set

bool [: the carrier' of X,( the carrier of X *):] is non empty set

(FreeSort Y) # is non empty Relation-like the carrier of X * -defined Function-like V24( the carrier of X * ) set

the Arity of X * ((FreeSort Y) #) is non empty Relation-like the carrier' of X -defined Function-like V24( the carrier' of X) set

the ResultSort of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like V25( the carrier' of X, the carrier of X) Element of bool [: the carrier' of X, the carrier of X:]

[: the carrier' of X, the carrier of X:] is non empty Relation-like set

bool [: the carrier' of X, the carrier of X:] is non empty set

the ResultSort of X * (FreeSort Y) is non empty Relation-like non-empty non empty-yielding the carrier' of X -defined Function-like V24( the carrier' of X) set

MSAlgebra(# (FreeSort Y),(FreeOper Y) #) is strict MSAlgebra over X

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA X) is non empty set

FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)

S -Terms X is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

bool (FinTrees the carrier of (DTConMSA X)) is non empty set

FreeMSA X is strict non-empty free feasible non empty MSAlgebra over S

the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

Y is Element of the carrier of S

the Sorts of (FreeMSA X) . Y is non empty set

FreeSort X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

FreeOper X is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) Function-yielding V54() ManySortedFunction of the Arity of S * ((FreeSort X) #), the ResultSort of S * (FreeSort X)

the carrier' of S is non empty set

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V25( the carrier' of S, the carrier of S * ) Function-yielding V54() Element of bool [: the carrier' of S,( the carrier of S *):]

the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)

[: the carrier' of S,( the carrier of S *):] is non empty Relation-like set

bool [: the carrier' of S,( the carrier of S *):] is non empty set

(FreeSort X) # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set

the Arity of S * ((FreeSort X) #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V25( 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 non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * (FreeSort X) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V24( the carrier' of S) set

MSAlgebra(# (FreeSort X),(FreeOper X) #) is strict MSAlgebra over S

FreeSort (X,Y) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA X))

TS (DTConMSA X) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

bool (TS (DTConMSA X)) is non empty set

A is Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

the_sort_of A is Element of the carrier of S

o is Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

the_sort_of o is Element of the carrier of S

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

the carrier of S --> {0} is non empty Relation-like non-empty non empty-yielding the carrier of S -defined bool NAT -valued Function-like constant V24( the carrier of S) V25( the carrier of S, bool NAT) Element of bool [: the carrier of S,(bool NAT):]

[: the carrier of S,(bool NAT):] is non empty Relation-like set

bool [: the carrier of S,(bool NAT):] is non empty set

X is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

(S,X) is strict non empty MSAlgebra over S

the Sorts of (S,X) is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

Union the Sorts of (S,X) is non empty set

X \/ ( the carrier of S --> {0}) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

DTConMSA (X \/ ( the carrier of S --> {0})) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) is non empty set

FinTrees the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA (X \/ ( the carrier of S --> {0})))

S -Terms (X \/ ( the carrier of S --> {0})) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))))

bool (FinTrees the carrier of (DTConMSA (X \/ ( the carrier of S --> {0})))) is non empty set

A is Element of Union the Sorts of (S,X)

TS (DTConMSA (X \/ ( the carrier of S --> {0}))) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))))

FreeSort (X \/ ( the carrier of S --> {0})) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

proj2 (FreeSort (X \/ ( the carrier of S --> {0}))) is non empty set

union (proj2 (FreeSort (X \/ ( the carrier of S --> {0})))) is set

Union (FreeSort (X \/ ( the carrier of S --> {0}))) is non empty set

FreeMSA (X \/ ( the carrier of S --> {0})) is strict non-empty free feasible non empty MSAlgebra over S

FreeOper (X \/ ( the carrier of S --> {0})) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) Function-yielding V54() ManySortedFunction of the Arity of S * ((FreeSort (X \/ ( the carrier of S --> {0}))) #), the ResultSort of S * (FreeSort (X \/ ( the carrier of S --> {0})))

the carrier' of S is non empty set

the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V25( the carrier' of S, the carrier of S * ) Function-yielding V54() Element of bool [: the carrier' of S,( the carrier of S *):]

the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)

[: the carrier' of S,( the carrier of S *):] is non empty Relation-like set

bool [: the carrier' of S,( the carrier of S *):] is non empty set

(FreeSort (X \/ ( the carrier of S --> {0}))) # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set

the Arity of S * ((FreeSort (X \/ ( the carrier of S --> {0}))) #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set

the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V25( 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 non empty Relation-like set

bool [: the carrier' of S, the carrier of S:] is non empty set

the ResultSort of S * (FreeSort (X \/ ( the carrier of S --> {0}))) is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V24( the carrier' of S) set

MSAlgebra(# (FreeSort (X \/ ( the carrier of S --> {0}))),(FreeOper (X \/ ( the carrier of S --> {0}))) #) is strict MSAlgebra over S

the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

dom the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

dom the Sorts of (S,X) is non empty Element of bool the carrier of S

o is set

the Sorts of (S,X) . o is set

Reverse (X \/ ( the carrier of S --> {0})) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) Function-yielding V54() ManySortedFunction of FreeGen (X \/ ( the carrier of S --> {0})),X \/ ( the carrier of S --> {0})

FreeGen (X \/ ( the carrier of S --> {0})) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) free GeneratorSet of FreeMSA (X \/ ( the carrier of S --> {0}))

(Reverse (X \/ ( the carrier of S --> {0}))) "" X is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

a is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0})))

GenMSAlg a is strict MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))

the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) . o is set

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

(S,X) is strict non empty MSAlgebra over S

the Sorts of (S,X) is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

Union the Sorts of (S,X) is non empty set

Y is Element of Union the Sorts of (S,X)

A is Element of Union the Sorts of (S,X)

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

(S,X) is strict non empty MSAlgebra over S

the Sorts of (S,X) is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

Union the Sorts of (S,X) is non empty set

Y is Relation-like Function-like Element of Union the Sorts of (S,X)

A is Relation-like Function-like Element of Union the Sorts of (S,X)

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

(S,X) is strict non empty MSAlgebra over S

the Sorts of (S,X) is non empty Relation-like non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

Union the Sorts of (S,X) is non empty set

Y is Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of Union the Sorts of (S,X)

S is Relation-like Function-like DecoratedTree-like set

S is ManySortedSign

the carrier of S is set

X is non empty Relation-like set

proj2 X is non empty set

{ (b

Y is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

Y is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

A is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

o is set

Y . o is set

{ (b

A . o is set

S is ManySortedSign

the carrier of S is set

X is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

Y is non empty Relation-like set

(S,Y) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

X /\ (S,Y) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

S is ManySortedSign

the carrier of S is set

X is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

Y is non empty Relation-like set

(S,X,Y) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

(S,Y) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

X /\ (S,Y) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

proj2 Y is non empty set

A is Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

o is set

A . o is set

X . o is set

(S,Y) . o is set

(X . o) /\ ((S,Y) . o) is set

{ (b

(X . o) /\ { (b

o is set

A . o is set

X . o is set

{ (b

(X . o) /\ { (b

(S,Y) . o is set

(X . o) /\ ((S,Y) . o) is set

S is ManySortedSign

the carrier of S is set

X is set

Y is set

[Y,X] is V1() set

{Y,X} is non empty set

{Y} is non empty set

{{Y,X},{Y}} is non empty set

root-tree [Y,X] is non empty trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set

(S,(root-tree [Y,X])) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,(root-tree [Y,X])) . X is set

[Y,X] `2 is set

A is non empty Relation-like Function-like DecoratedTree-like set

[{},[Y,X]] is V1() set

{{},[Y,X]} is non empty set

{{{},[Y,X]},{{}}} is non empty set

{[{},[Y,X]]} is non empty Relation-like Function-like set

proj2 A is non empty set

{[Y,X]} is non empty Relation-like Function-like set

[Y,X] `1 is set

(S,A) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,A) . X is set

{ (b

o is set

a is Element of proj2 A

a `1 is set

a `2 is set

o is set

(S,(root-tree [Y,X])) . o is set

the Element of (S,(root-tree [Y,X])) . o is Element of (S,(root-tree [Y,X])) . o

(S,A) . o is set

dom (S,A) is Element of bool the carrier of S

bool the carrier of S is non empty set

{ (b

z is Element of proj2 A

z `1 is set

z `2 is set

S is set

X is set

Y is ManySortedSign

the carrier of Y is set

[X, the carrier of Y] is V1() set

{X, the carrier of Y} is non empty set

{X} is non empty set

{{X, the carrier of Y},{X}} is non empty set

A is set

o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set

[X, the carrier of Y] -tree o is non empty Relation-like Function-like DecoratedTree-like set

(Y,([X, the carrier of Y] -tree o)) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,([X, the carrier of Y] -tree o)) . A is set

proj2 o is set

a is non empty Relation-like Function-like DecoratedTree-like set

(Y,a) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,a) . A is set

proj2 a is non empty set

{ (b

proj1 a is non empty V39() set

doms o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Tree-yielding set

tree (doms o) is non empty V39() set

dom (doms o) is Element of bool NAT

dom o is Element of bool NAT

len o is V17() V18() V19() V23() V163() V164() ext-real Element of NAT

len (doms o) is V17() V18() V19() V23() V163() V164() ext-real Element of NAT

z is Element of proj2 a

z `1 is set

z `2 is set

z is set

a . z is set

a . {} is set

q is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 a

s9 is V17() V18() V19() V23() V163() V164() ext-real Element of NAT

v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

s9 + 1 is V17() V18() V19() V23() V163() V164() ext-real Element of NAT

(doms o) . (s9 + 1) is set

<*s9*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V35(1) FinSequence-like FinSubsequence-like FinSequence of NAT

<*s9*> ^ v is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

o . (s9 + 1) is set

p2 is non empty Relation-like Function-like DecoratedTree-like set

t is non empty Relation-like Function-like DecoratedTree-like set

proj1 t is non empty V39() set

a | <*s9*> is non empty Relation-like Function-like DecoratedTree-like set

(proj1 a) | <*s9*> is non empty V39() set

a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

t . a is set

proj2 t is non empty set

{ (b

(Y,t) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,t) . A is set

z is non empty Relation-like Function-like DecoratedTree-like set

(Y,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,z) . A is set

z is set

o . z is set

q is V17() V18() V19() V23() V163() V164() ext-real Element of NAT

s9 is V17() V18() V19() V23() V163() V164() ext-real set

1 + s9 is V17() V18() V19() V23() V163() V164() ext-real Element of NAT

v is V17() V18() V19() V23() V163() V164() ext-real Element of NAT

<*v*> is non empty Relation-like NAT -defined NAT -valued Function-like finite V35(1) FinSequence-like FinSubsequence-like FinSequence of NAT

a | <*v*> is non empty Relation-like Function-like DecoratedTree-like set

proj1 z is non empty V39() set

<*v*> ^ {} is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

v + 1 is V17() V18() V19() V23() V163() V164() ext-real Element of NAT

(doms o) . (v + 1) is set

proj2 z is non empty set

{ (b

p2 is Element of proj2 z

p2 `1 is set

p2 `2 is set

S is ManySortedSign

the carrier of S is set

X is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

A is set

Y is set

X . Y is set

[A,Y] is V1() set

{A,Y} is non empty set

{A} is non empty set

{{A,Y},{A}} is non empty set

root-tree [A,Y] is non empty trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set

(S,X,(root-tree [A,Y])) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

(S,(root-tree [A,Y])) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

X /\ (S,(root-tree [A,Y])) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,X,(root-tree [A,Y])) . Y is set

[A,Y] `1 is set

[A,Y] `2 is set

dom X is Element of bool the carrier of S

bool the carrier of S is non empty set

(S,(root-tree [A,Y])) . Y is set

(X . Y) /\ ((S,(root-tree [A,Y])) . Y) is set

a is set

(S,X,(root-tree [A,Y])) . a is set

the Element of (S,X,(root-tree [A,Y])) . a is Element of (S,X,(root-tree [A,Y])) . a

o is non empty Relation-like Function-like DecoratedTree-like set

(S,X,o) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

(S,o) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

X /\ (S,o) is Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

dom (S,X,o) is Element of bool the carrier of S

(S,X,o) . a is set

X . a is set

proj2 o is non empty set

{ (b

(X . a) /\ { (b

z is Element of proj2 o

z `1 is set

z `2 is set

[{},[A,Y]] is V1() set

{{},[A,Y]} is non empty set

{{{},[A,Y]},{{}}} is non empty set

{[{},[A,Y]]} is non empty Relation-like Function-like set

{[A,Y]} is non empty Relation-like Function-like set

S is set

X is set

Y is ManySortedSign

the carrier of Y is set

[X, the carrier of Y] is V1() set

{X, the carrier of Y} is non empty set

{X} is non empty set

{{X, the carrier of Y},{X}} is non empty set

A is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

o is set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding set

[X, the carrier of Y] -tree a is non empty Relation-like Function-like DecoratedTree-like set

(Y,A,([X, the carrier of Y] -tree a)) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) ManySortedSubset of A

(Y,([X, the carrier of Y] -tree a)) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

A /\ (Y,([X, the carrier of Y] -tree a)) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,A,([X, the carrier of Y] -tree a)) . o is set

proj2 a is set

z is non empty Relation-like Function-like DecoratedTree-like set

(Y,A,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) ManySortedSubset of A

(Y,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

A /\ (Y,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,A,z) . o is set

A . o is set

(Y,z) . o is set

(A . o) /\ ((Y,z) . o) is set

(Y,([X, the carrier of Y] -tree a)) . o is set

z is non empty Relation-like Function-like DecoratedTree-like set

(Y,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,z) . o is set

z is non empty Relation-like Function-like DecoratedTree-like set

(Y,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,z) . o is set

z is non empty Relation-like Function-like DecoratedTree-like set

(Y,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,z) . o is set

q is non empty Relation-like Function-like DecoratedTree-like set

(Y,q) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,q) . o is set

(A . o) /\ ((Y,q) . o) is set

(Y,A,q) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) ManySortedSubset of A

A /\ (Y,q) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,A,q) . o is set

z is non empty Relation-like Function-like DecoratedTree-like set

(Y,A,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) ManySortedSubset of A

(Y,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

A /\ (Y,z) is Relation-like the carrier of Y -defined Function-like V24( the carrier of Y) set

(Y,A,z) . o is set

(Y,z) . o is set

(A . o) /\ ((Y,z) . o) is set

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA X) is non empty set

FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)

S -Terms X is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

bool (FinTrees the carrier of (DTConMSA X)) is non empty set

the carrier' of S is non empty set

Y is Element of the carrier' of S

Sym (Y,X) is Element of NonTerminals (DTConMSA X)

NonTerminals (DTConMSA X) is non empty Element of bool the carrier of (DTConMSA X)

bool the carrier of (DTConMSA X) is non empty set

[Y, the carrier of S] is V1() set

{Y, the carrier of S} is non empty set

{Y} is non empty set

{{Y, the carrier of S},{Y}} is non empty set

A is Relation-like NAT -defined FinTrees the carrier of (DTConMSA X) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() ArgumentSeq of Sym (Y,X)

rng A is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

[Y, the carrier of S] -tree A is non empty Relation-like Function-like DecoratedTree-like set

(S,([Y, the carrier of S] -tree A)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

a is set

(S,([Y, the carrier of S] -tree A)) . a is set

X . a is set

z is set

z is Element of the carrier of S

q is non empty Relation-like Function-like DecoratedTree-like set

(S,q) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,q) . z is set

dom A is Element of bool NAT

s9 is set

A . s9 is Relation-like Function-like set

v is V17() V18() V19() V23() V163() V164() ext-real set

A . v is Relation-like Function-like set

p2 is non empty Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

(S,p2) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,p2) . z is set

X . z is non empty set

Y is Element of the carrier of S

X . Y is non empty set

[:(X . Y), the carrier of S:] is non empty Relation-like set

A is Element of X . Y

[A,Y] is V1() Element of [:(X . Y), the carrier of S:]

{A,Y} is non empty set

{A} is non empty set

{{A,Y},{A}} is non empty set

root-tree [A,Y] is non empty trivial Relation-like [:(X . Y), the carrier of S:] -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees [:(X . Y), the carrier of S:]

FinTrees [:(X . Y), the carrier of S:] is non empty functional constituted-DTrees DTree-set of [:(X . Y), the carrier of S:]

(S,(root-tree [A,Y])) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

o is set

(S,(root-tree [A,Y])) . o is set

X . o is set

z is set

a is Element of the carrier of S

{A} is non empty Element of bool (X . Y)

bool (X . Y) is non empty set

Y is non empty Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

(S,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA X) is non empty set

FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)

S -Terms X is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

bool (FinTrees the carrier of (DTConMSA X)) is non empty set

Y is non empty Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

(S,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,X,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

X /\ (S,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA X) is non empty set

FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)

S -Terms X is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

bool (FinTrees the carrier of (DTConMSA X)) is non empty set

Y is non empty Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

(S,X,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

(S,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,X,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

X /\ (S,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

FreeMSA X is strict non-empty free feasible non empty MSAlgebra over S

the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA X) is non empty set

FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)

S -Terms X is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

bool (FinTrees the carrier of (DTConMSA X)) is non empty set

Y is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

{ b

A is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

o is set

A . o is set

the Sorts of (FreeMSA X) . o is set

z is set

a is Element of the carrier of S

A . a is set

{ b

z is non empty Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

the_sort_of z is Element of the carrier of S

(S,X,z) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

(S,z) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

o is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA X)

a is Element of the carrier of S

o . a is set

{ b

A is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA X)

o is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA X)

a is set

A . a is set

{ b

o . a is set

S is set

X is non empty non void feasible V159() ManySortedSign

the carrier of X is non empty set

Y is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

DTConMSA Y is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA Y) is non empty set

FinTrees the carrier of (DTConMSA Y) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA Y)

X -Terms Y is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA Y))

bool (FinTrees the carrier of (DTConMSA Y)) is non empty set

A is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

(X,Y,A) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) ManySortedSubset of the Sorts of (FreeMSA Y)

FreeMSA Y is strict non-empty free feasible non empty MSAlgebra over X

the Sorts of (FreeMSA Y) is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

o is Element of the carrier of X

(X,Y,A) . o is set

{ b

a is non empty Relation-like the carrier of (DTConMSA Y) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of X -Terms Y

the_sort_of a is Element of the carrier of X

(X,Y,a) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) ManySortedSubset of Y

(X,a) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA X) is non empty set

FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)

S -Terms X is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

bool (FinTrees the carrier of (DTConMSA X)) is non empty set

Y is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,X,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA X)

FreeMSA X is strict non-empty free feasible non empty MSAlgebra over S

the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

A is non empty Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

the_sort_of A is Element of the carrier of S

(S,X,A) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

(S,A) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

o is Element of the carrier of S

(S,X,Y) . o is set

{ b

a is non empty Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

the_sort_of a is Element of the carrier of S

(S,X,a) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X

(S,a) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

S is set

X is non empty non void feasible V159() ManySortedSign

the carrier of X is non empty set

Y is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

A is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

(X,Y,A) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) ManySortedSubset of the Sorts of (FreeMSA Y)

FreeMSA Y is strict non-empty free feasible non empty MSAlgebra over X

the Sorts of (FreeMSA Y) is non empty Relation-like non-empty non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set

o is Element of the carrier of X

[S,o] is V1() set

{S,o} is non empty set

{S} is non empty set

{{S,o},{S}} is non empty set

root-tree [S,o] is non empty trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set

(X,Y,A) . o is set

A . o is set

Y . o is non empty set

DTConMSA Y is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA Y) is non empty set

FinTrees the carrier of (DTConMSA Y) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA Y)

X -Terms Y is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA Y))

bool (FinTrees the carrier of (DTConMSA Y)) is non empty set

{ b

a is non empty Relation-like the carrier of (DTConMSA Y) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of X -Terms Y

the_sort_of a is Element of the carrier of X

(X,Y,a) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) ManySortedSubset of Y

(X,a) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

a . {} is set

{ the carrier of X} is non empty set

the carrier' of X is non empty set

[: the carrier' of X,{ the carrier of X}:] is non empty Relation-like set

z is Element of the carrier of X

Y . z is non empty set

z is Element of Y . z

[z,z] is V1() Element of [:(Y . z), the carrier of X:]

[:(Y . z), the carrier of X:] is non empty Relation-like set

{z,z} is non empty set

{z} is non empty set

{{z,z},{z}} is non empty set

(X,a) . o is set

(X,Y,a) . o is set

a is non empty Relation-like the carrier of (DTConMSA Y) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of X -Terms Y

(X,Y,a) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) ManySortedSubset of Y

(X,a) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set

z is set

(X,Y,a) . z is set

A . z is set

(X,a) . o is set

(X,a) . z is set

the_sort_of a is Element of the carrier of X

S is non empty non void feasible V159() ManySortedSign

the carrier of S is non empty set

the carrier' of S is non empty set

X is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr

the carrier of (DTConMSA X) is non empty set

FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)

Y is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set

(S,X,Y) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA X)

FreeMSA X is strict non-empty free feasible non empty MSAlgebra over S

the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set

Union (S,X,Y) is set

A is Element of the carrier' of S

Sym (A,X) is Element of NonTerminals (DTConMSA X)

NonTerminals (DTConMSA X) is non empty Element of bool the carrier of (DTConMSA X)

bool the carrier of (DTConMSA X) is non empty set

the_result_sort_of A is Element of the carrier of S

(S,X,Y) . (the_result_sort_of A) is set

o is Relation-like NAT -defined FinTrees the carrier of (DTConMSA X) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() ArgumentSeq of Sym (A,X)

(Sym (A,X)) -tree o is non empty Relation-like the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X

S -Terms X is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

bool (FinTrees the carrier of (DTConMSA X)) is non empty set

rng o is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))

dom (S,X,Y) is non empty Element of bool the carrier of S

bool the carrier of S is non empty set

[A, the carrier of S] is V1() set

{A, the carrier of S} is non empty