:: 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<sub>1</sub> `1) where b₁ is Element of proj2 X : b₁ `2 = a<sub>1</sub> } is set
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<sub>1</sub> `1) where b₁ is Element of proj2 X : b₁ `2 = o } is set
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<sub>1</sub> `1) where b₁ is Element of proj2 Y : b₁ `2 = o } is set
(X . o) /\ { (b<sub>1</sub> `1) where b₁ is Element of proj2 Y : b₁ `2 = o } is set
o is set
A . o is set
X . o is set
{ (b<sub>1</sub> `1) where b₁ is Element of proj2 Y : b₁ `2 = o } is set
(X . o) /\ { (b<sub>1</sub> `1) where b₁ is Element of proj2 Y : b₁ `2 = o } is set
(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<sub>1</sub> `1) where b₁ is Element of proj2 A : b₁ `2 = X } is set
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<sub>1</sub> `1) where b₁ is Element of proj2 A : b₁ `2 = o } is set
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<sub>1</sub> `1) where b₁ is Element of proj2 a : b₁ `2 = A } is set
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<sub>1</sub> `1) where b₁ is Element of proj2 t : b₁ `2 = A } is set
(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<sub>1</sub> `1) where b₁ is Element of proj2 z : b₁ `2 = A } is set
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<sub>1</sub> `1) where b₁ is Element of proj2 o : b₁ `2 = a } is set
(X . a) /\ { (b<sub>1</sub> `1) where b₁ is Element of proj2 o : b₁ `2 = a } is set
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<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = a<sub>1</sub> & (S,X,b<sub>1</sub>) c= Y ) } is set
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<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = a & (S,X,b<sub>1</sub>) c= Y ) } is set
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<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = a & (S,X,b<sub>1</sub>) c= Y ) } is 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)
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<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = a & (S,X,b<sub>1</sub>) c= Y ) } is set
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<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = o & (X,Y,b<sub>1</sub>) c= A ) } 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
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<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = o & (S,X,b<sub>1</sub>) c= Y ) } is 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
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<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = o & (X,Y,b<sub>1</sub>) c= A ) } 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
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 set
{A} is non empty set
{{A, the carrier of S},{A}} is non empty set
{ b<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = the_result_sort_of A & (S,X,b<sub>1</sub>) c= Y ) } is set
[A, the carrier of S] -tree o is non empty Relation-like Function-like DecoratedTree-like set
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
z is set
dom o is Element of bool NAT
q is set
o . q is Relation-like Function-like set
s9 is V17() V18() V19() V23() V163() V164() ext-real set
o . s9 is Relation-like Function-like set
v 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,v) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X
(S,v) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
p2 is set
(S,X,v) . p2 is set
Y . p2 is set
a is set
(S,X,z) . p2 is set
the_sort_of v is Element of the carrier of S
(S,X,Y) . (the_sort_of v) is set
{ b<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = the_sort_of v & (S,X,b<sub>1</sub>) c= Y ) } is set
(S,X,((Sym (A,X)) -tree o)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X
(S,((Sym (A,X)) -tree o)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
z is set
(S,X,((Sym (A,X)) -tree o)) . z is set
Y . z is set
q is set
s9 is non empty Relation-like Function-like DecoratedTree-like set
(S,s9) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
(S,s9) . z is set
v is set
(S,X,Y) . v is set
{ b<sub>1</sub> where b<sub>1</sub> 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 b<sub>1</sub> = v & (S,X,b<sub>1</sub>) c= Y ) } is 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
the_sort_of p2 is Element of the carrier of S
(S,X,p2) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X
(S,p2) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
(S,X,p2) . z is set
the_sort_of ((Sym (A,X)) -tree 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 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)
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)
Union A is set
o is Element of the carrier' of S
Sym (o,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
Result (o,(FreeMSA X)) is non empty Element of proj2 the Sorts of (FreeMSA X)
proj2 the Sorts of (FreeMSA X) is non empty set
Args (o,(FreeMSA X)) is non empty functional Element of proj2 ( the Sorts of (FreeMSA X) #)
the Sorts of (FreeMSA X) # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of (FreeMSA X) #) is non empty set
Den (o,(FreeMSA X)) is Relation-like Args (o,(FreeMSA X)) -defined Result (o,(FreeMSA X)) -valued Function-like V25( Args (o,(FreeMSA X)), Result (o,(FreeMSA X))) Element of bool [:(Args (o,(FreeMSA X))),(Result (o,(FreeMSA X))):]
[:(Args (o,(FreeMSA X))),(Result (o,(FreeMSA X))):] is non empty Relation-like set
bool [:(Args (o,(FreeMSA X))),(Result (o,(FreeMSA X))):] 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
A # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
( the Arity of S * (A #)) . o is set
(Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o) is Relation-like Args (o,(FreeMSA X)) -defined ( the Arity of S * (A #)) . o -defined Args (o,(FreeMSA X)) -defined Result (o,(FreeMSA X)) -valued Function-like Element of bool [:(Args (o,(FreeMSA X))),(Result (o,(FreeMSA X))):]
rng ((Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o)) is Element of bool (Result (o,(FreeMSA X)))
bool (Result (o,(FreeMSA X))) is non empty 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 * A is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
( the ResultSort of S * A) . o is 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 (o,X)
dom a is Element of bool NAT
the_arity_of o is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
dom (the_arity_of o) is Element of bool NAT
dom A is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
rng a is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
bool (FinTrees the carrier of (DTConMSA X)) is non empty set
z is set
S -Terms X is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
z is V17() V18() V19() V23() V163() V164() ext-real set
a . z is Relation-like Function-like set
q 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 q is Element of the carrier of S
(the_arity_of o) . z is set
(the_arity_of o) * A is Relation-like NAT -defined Function-like set
((the_arity_of o) * A) . z is set
A . ((the_arity_of o) . z) is set
a . z is Relation-like Function-like set
s9 is set
A . s9 is set
the Sorts of (FreeMSA X) . s9 is set
rng (the_arity_of o) is Element of bool the carrier of S
dom ((the_arity_of o) * A) is Element of bool NAT
product ((the_arity_of o) * A) is set
the Arity of S . o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(A #) . ( the Arity of S . o) is set
(A #) . (the_arity_of o) is set
((Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o)) . a is set
(Den (o,(FreeMSA X))) . a is set
dom (Den (o,(FreeMSA X))) is functional Element of bool (Args (o,(FreeMSA X)))
bool (Args (o,(FreeMSA X))) is non empty set
dom ((Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o)) is Element of bool (( the Arity of S * (A #)) . o)
bool (( the Arity of S * (A #)) . o) is non empty set
the ResultSort of S . o is set
A . ( the ResultSort of S . o) is set
the_result_sort_of o is Element of the carrier of S
A . (the_result_sort_of o) is set
[o, the carrier of S] is V1() set
{o, the carrier of S} is non empty set
{o} is non empty set
{{o, the carrier of S},{o}} is non empty set
(Sym (o,X)) -tree 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
o is Element of the carrier' of S
a is set
Den (o,(FreeMSA X)) is Relation-like Args (o,(FreeMSA X)) -defined Result (o,(FreeMSA X)) -valued Function-like V25( Args (o,(FreeMSA X)), Result (o,(FreeMSA X))) Element of bool [:(Args (o,(FreeMSA X))),(Result (o,(FreeMSA X))):]
Args (o,(FreeMSA X)) is non empty functional Element of proj2 ( the Sorts of (FreeMSA X) #)
Result (o,(FreeMSA X)) is non empty Element of proj2 the Sorts of (FreeMSA X)
[:(Args (o,(FreeMSA X))),(Result (o,(FreeMSA X))):] is non empty Relation-like set
bool [:(Args (o,(FreeMSA X))),(Result (o,(FreeMSA X))):] is non empty set
( the Arity of S * (A #)) . o is set
(Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o) is Relation-like ( the Arity of S * (A #)) . o -defined Args (o,(FreeMSA X)) -defined Result (o,(FreeMSA X)) -valued Function-like set
proj2 ((Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o)) is set
( the ResultSort of S * A) . o is set
the ResultSort of S . o is set
A . ( the ResultSort of S . o) is set
the_result_sort_of o is Element of the carrier of S
A . (the_result_sort_of o) is set
(Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o) is Relation-like Args (o,(FreeMSA X)) -defined ( the Arity of S * (A #)) . o -defined Args (o,(FreeMSA X)) -defined Result (o,(FreeMSA X)) -valued Function-like Element of bool [:(Args (o,(FreeMSA X))),(Result (o,(FreeMSA X))):]
rng ((Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o)) is Element of bool (Result (o,(FreeMSA X)))
bool (Result (o,(FreeMSA X))) is non empty set
dom ((Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o)) is Element of bool (( the Arity of S * (A #)) . o)
bool (( the Arity of S * (A #)) . o) is non empty set
z is set
((Den (o,(FreeMSA X))) | (( the Arity of S * (A #)) . o)) . z is set
dom (Den (o,(FreeMSA X))) is functional Element of bool (Args (o,(FreeMSA X)))
bool (Args (o,(FreeMSA X))) is non empty set
Sym (o,X) is Element of NonTerminals (DTConMSA X)
z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of Args (o,(FreeMSA X))
the Arity of S . o is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(A #) . ( the Arity of S . o) is set
the_arity_of o is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
(A #) . (the_arity_of o) is set
(the_arity_of o) * A is Relation-like NAT -defined Function-like set
product ((the_arity_of o) * A) is set
q 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 (o,X)
rng q is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
s9 is set
dom q is Element of bool NAT
v is set
q . v is Relation-like Function-like set
dom ((the_arity_of o) * A) is Element of bool NAT
((the_arity_of o) * A) . v is set
(the_arity_of o) . v is set
A . ((the_arity_of o) . v) is set
rng (the_arity_of o) is Element of bool the carrier of S
dom (the_arity_of o) is Element of bool NAT
(Den (o,(FreeMSA X))) . z is set
[o, the carrier of S] is V1() set
{o, the carrier of S} is non empty set
{o} is non empty set
{{o, the carrier of S},{o}} is non empty set
[o, the carrier of S] -tree z is non empty Relation-like Function-like DecoratedTree-like set
(Sym (o,X)) -tree q 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 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
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)
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
the carrier' of S is non empty 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)
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
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)
rng o is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
bool (FinTrees the carrier of (DTConMSA X)) is non empty set
(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))
the_result_sort_of A is Element of the carrier of S
(S,X,Y) . (the_result_sort_of 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 non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set
Reverse X is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) Function-yielding V54() ManySortedFunction of FreeGen X,X
FreeGen X 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
FreeMSA X is strict non-empty free feasible non empty MSAlgebra over S
Y is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
(Reverse 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)
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 set
((Reverse X) "" Y) . A is set
(S,X,Y) . A is set
a is set
o is Element of the carrier of S
(FreeGen X) . o is non empty set
X . o is non empty set
(Reverse X) . o is Relation-like (FreeGen X) . o -defined X . o -valued Function-like V25((FreeGen X) . o,X . o) Element of bool [:((FreeGen X) . o),(X . o):]
[:((FreeGen X) . o),(X . o):] is non empty Relation-like set
bool [:((FreeGen X) . o),(X . o):] is non empty set
Y . o is set
((Reverse X) . o) " (Y . o) is Element of bool ((FreeGen X) . o)
bool ((FreeGen X) . o) is non empty set
(Reverse X) . A is Relation-like Function-like set
proj1 ((Reverse X) . A) is set
((Reverse X) . A) . a is set
Y . A is set
Reverse (o,X) is Relation-like FreeGen (o,X) -defined X . o -valued Function-like V25( FreeGen (o,X),X . o) Element of bool [:(FreeGen (o,X)),(X . o):]
FreeGen (o,X) is non empty Element of bool ((FreeSort X) . o)
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
(FreeSort X) . o is non empty set
bool ((FreeSort X) . o) is non empty set
[:(FreeGen (o,X)),(X . o):] is non empty Relation-like set
bool [:(FreeGen (o,X)),(X . o):] is non empty set
z is set
[z,o] is V1() set
{z,o} is non empty set
{z} is non empty set
{{z,o},{z}} is non empty set
root-tree [z,o] is non empty trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA X) is non empty set
Terminals (DTConMSA X) is set
{ (root-tree b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of (DTConMSA X) : ( b<sub>1</sub> in Terminals (DTConMSA X) & b<sub>1</sub> `2 = A ) } is set
z is Element of the carrier of (DTConMSA X)
root-tree z is non empty trivial Relation-like the carrier of (DTConMSA X) -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees the carrier of (DTConMSA X)
FinTrees the carrier of (DTConMSA X) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA X)
z `2 is set
(Reverse (o,X)) . a is set
z `1 is set
[z,A] is V1() set
{z,A} is non empty set
{{z,A},{z}} is non empty set
[z,A] `1 is set
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 the carrier of S -defined Function-like V24( the carrier of S) 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
(S,(X \/ ( the carrier of S --> {0})),X) 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})))
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
(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
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 carrier' of S is non empty set
a is Element of the carrier' of S
Sym (a,(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
z 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 (a,(X \/ ( the carrier of S --> {0})))
rng z is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))))
[a, the carrier of S] is V1() set
{a, the carrier of S} is non empty set
{a} is non empty set
{{a, the carrier of S},{a}} is non empty set
[a, the carrier of S] -tree z is non empty Relation-like Function-like DecoratedTree-like set
z is Element of the carrier of S
(S,(X \/ ( the carrier of S --> {0})),X) . z is set
the Sorts of (S,X) . z is set
(Sym (a,(X \/ ( the carrier of S --> {0})))) -tree z is non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0}))
the_sort_of ((Sym (a,(X \/ ( the carrier of S --> {0})))) -tree z) is Element of the carrier of S
the_result_sort_of a is Element of the carrier of S
Union (S,(X \/ ( the carrier of S --> {0})),X) is 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 \/ ( the carrier of S --> {0})))
Union o is set
q is set
dom (S,(X \/ ( the carrier of S --> {0})),X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
s9 is set
(S,(X \/ ( the carrier of S --> {0})),X) . s9 is set
v is Element of the carrier of S
(S,(X \/ ( the carrier of S --> {0})),X) . v is set
dom the Sorts of (S,X) is non empty Element of bool the carrier of S
p2 is non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0}))
the Sorts of (S,X) . v is set
q 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 q is strict MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))
a is Element of the carrier of S
(X \/ ( the carrier of S --> {0})) . a is non empty set
[:((X \/ ( the carrier of S --> {0})) . a), the carrier of S:] is non empty Relation-like set
z is Element of (X \/ ( the carrier of S --> {0})) . a
[z,a] is V1() Element of [:((X \/ ( the carrier of S --> {0})) . a), the carrier of S:]
{z,a} is non empty set
{z} is non empty set
{{z,a},{z}} is non empty set
root-tree [z,a] is non empty trivial Relation-like [:((X \/ ( the carrier of S --> {0})) . a), the carrier of S:] -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees [:((X \/ ( the carrier of S --> {0})) . a), the carrier of S:]
FinTrees [:((X \/ ( the carrier of S --> {0})) . a), the carrier of S:] is non empty functional constituted-DTrees DTree-set of [:((X \/ ( the carrier of S --> {0})) . a), the carrier of S:]
q is Element of the carrier of S
(S,(X \/ ( the carrier of S --> {0})),X) . q is set
the Sorts of (S,X) . q is set
the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) . q is non empty set
z is non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0}))
the_sort_of z is Element of the carrier of S
X . q is set
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 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
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
(S,(X \/ ( the carrier of S --> {0})),X) 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})))
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
Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(X \/ ( the carrier of S --> {0})),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 * ((S,(X \/ ( the carrier of S --> {0})),X) #), the ResultSort of S * (S,(X \/ ( the carrier of S --> {0})),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
(S,(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
the Arity of S * ((S,(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
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 * (S,(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
MSAlgebra(# (S,(X \/ ( the carrier of S --> {0})),X),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(X \/ ( the carrier of S --> {0})),X))) #) is strict MSAlgebra over S
the Sorts of MSAlgebra(# (S,(X \/ ( the carrier of S --> {0})),X),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(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
the Charact of MSAlgebra(# (S,(X \/ ( the carrier of S --> {0})),X),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(X \/ ( the carrier of S --> {0})),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 * ( the Sorts of MSAlgebra(# (S,(X \/ ( the carrier of S --> {0})),X),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(X \/ ( the carrier of S --> {0})),X))) #) #), the ResultSort of S * the Sorts of MSAlgebra(# (S,(X \/ ( the carrier of S --> {0})),X),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(X \/ ( the carrier of S --> {0})),X))) #)
the Sorts of MSAlgebra(# (S,(X \/ ( the carrier of S --> {0})),X),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(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
the Arity of S * ( the Sorts of MSAlgebra(# (S,(X \/ ( the carrier of S --> {0})),X),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(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
the ResultSort of S * the Sorts of MSAlgebra(# (S,(X \/ ( the carrier of S --> {0})),X),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(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
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})))
Opers ((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) Function-yielding V54() ManySortedFunction of the Arity of S * (o #), the ResultSort of S * o
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 ResultSort of S * o is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
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
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})))
(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 * (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
dom (FreeSort (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
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
o is MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))
the Sorts of o is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
a is Element of the carrier of S
the Sorts of (S,X) . a is set
(S,(X \/ ( the carrier of S --> {0})),X) . a is 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}))
z is set
the Sorts of (FreeMSA (X \/ ( the carrier of S --> {0}))) . a is non empty set
Union (FreeSort (X \/ ( the carrier of S --> {0}))) is non empty 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
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 the carrier of S -defined Function-like V24( the carrier of S) 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
(S,(X \/ ( the carrier of S --> {0})),X) 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})))
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
(FreeMSA (X \/ ( the carrier of S --> {0}))) | (S,(X \/ ( the carrier of S --> {0})),X) is strict MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))
(S,X) is strict MSAlgebra over S
Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(X \/ ( the carrier of S --> {0})),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 * ((S,(X \/ ( the carrier of S --> {0})),X) #), the ResultSort of S * (S,(X \/ ( the carrier of S --> {0})),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
(S,(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
the Arity of S * ((S,(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
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 * (S,(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
MSAlgebra(# (S,(X \/ ( the carrier of S --> {0})),X),(Opers ((FreeMSA (X \/ ( the carrier of S --> {0}))),(S,(X \/ ( the carrier of S --> {0})),X))) #) is strict MSAlgebra over S
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}))
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
Y is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) set
FreeMSA Y is strict non-empty free feasible non empty MSAlgebra over S
A is MSSubAlgebra of FreeMSA X
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
the Charact of A 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 * ( the Sorts of A #), the ResultSort of S * the Sorts of A
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
the Sorts of A # 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 A #) 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 * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
MSAlgebra(# the Sorts of A, the Charact of A #) is strict MSAlgebra over S
o is MSSubAlgebra of FreeMSA Y
the Sorts of o is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
the Charact of o 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 * ( the Sorts of o #), the ResultSort of S * the Sorts of o
the Sorts of o # 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 o #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
the ResultSort of S * the Sorts of o is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
MSAlgebra(# the Sorts of o, the Charact of o #) is strict MSAlgebra over S
the Sorts of (FreeMSA Y) 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) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) 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)
a is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of (FreeMSA Y)
z is set
q is Element of the carrier' of S
the Charact of A . q is Relation-like ( the Arity of S * ( the Sorts of A #)) . q -defined ( the ResultSort of S * the Sorts of A) . q -valued Function-like V25(( the Arity of S * ( the Sorts of A #)) . q,( the ResultSort of S * the Sorts of A) . q) Element of bool [:(( the Arity of S * ( the Sorts of A #)) . q),(( the ResultSort of S * the Sorts of A) . q):]
( the Arity of S * ( the Sorts of A #)) . q is set
( the ResultSort of S * the Sorts of A) . q is set
[:(( the Arity of S * ( the Sorts of A #)) . q),(( the ResultSort of S * the Sorts of A) . q):] is Relation-like set
bool [:(( the Arity of S * ( the Sorts of A #)) . q),(( the ResultSort of S * the Sorts of A) . q):] is non empty set
z # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
the Arity of S * (z #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
the ResultSort of S * z is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
Opers ((FreeMSA X),z) 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 * (z #), the ResultSort of S * z
(Opers ((FreeMSA X),z)) . q is Relation-like ( the Arity of S * (z #)) . q -defined ( the ResultSort of S * z) . q -valued Function-like V25(( the Arity of S * (z #)) . q,( the ResultSort of S * z) . q) Element of bool [:(( the Arity of S * (z #)) . q),(( the ResultSort of S * z) . q):]
( the Arity of S * (z #)) . q is set
( the ResultSort of S * z) . q is set
[:(( the Arity of S * (z #)) . q),(( the ResultSort of S * z) . q):] is Relation-like set
bool [:(( the Arity of S * (z #)) . q),(( the ResultSort of S * z) . q):] is non empty set
q /. z is Relation-like ( the Arity of S * (z #)) . q -defined ( the ResultSort of S * z) . q -valued Function-like V25(( the Arity of S * (z #)) . q,( the ResultSort of S * z) . q) Element of bool [:(( the Arity of S * (z #)) . q),(( the ResultSort of S * z) . q):]
Args (q,(FreeMSA X)) is non empty functional Element of proj2 ( the Sorts of (FreeMSA X) #)
the Sorts of (FreeMSA X) # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
proj2 ( the Sorts of (FreeMSA X) #) is non empty set
Result (q,(FreeMSA X)) is non empty Element of proj2 the Sorts of (FreeMSA X)
proj2 the Sorts of (FreeMSA X) is non empty set
Den (q,(FreeMSA X)) is Relation-like Args (q,(FreeMSA X)) -defined Result (q,(FreeMSA X)) -valued Function-like V25( Args (q,(FreeMSA X)), Result (q,(FreeMSA X))) Element of bool [:(Args (q,(FreeMSA X))),(Result (q,(FreeMSA X))):]
[:(Args (q,(FreeMSA X))),(Result (q,(FreeMSA X))):] is non empty Relation-like set
bool [:(Args (q,(FreeMSA X))),(Result (q,(FreeMSA X))):] is non empty set
(Den (q,(FreeMSA X))) | (( the Arity of S * (z #)) . q) is Relation-like ( the Arity of S * (z #)) . q -defined Args (q,(FreeMSA X)) -defined Result (q,(FreeMSA X)) -valued Function-like Element of bool [:(Args (q,(FreeMSA X))),(Result (q,(FreeMSA X))):]
the Arity of S * ( the Sorts of (FreeMSA X) #) 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) #)) . q is set
dom (Den (q,(FreeMSA X))) is functional Element of bool (Args (q,(FreeMSA X)))
bool (Args (q,(FreeMSA X))) is non empty set
dom ( the Charact of A . q) is Element of bool (( the Arity of S * ( the Sorts of A #)) . q)
bool (( the Arity of S * ( the Sorts of A #)) . q) is non empty set
a # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
the Arity of S * (a #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
( the Arity of S * (a #)) . q is set
the Sorts of (FreeMSA Y) # 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 Y) #) 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 Y) #)) . q is set
the Charact of o . q is Relation-like ( the Arity of S * ( the Sorts of o #)) . q -defined ( the ResultSort of S * the Sorts of o) . q -valued Function-like V25(( the Arity of S * ( the Sorts of o #)) . q,( the ResultSort of S * the Sorts of o) . q) Element of bool [:(( the Arity of S * ( the Sorts of o #)) . q),(( the ResultSort of S * the Sorts of o) . q):]
( the Arity of S * ( the Sorts of o #)) . q is set
( the ResultSort of S * the Sorts of o) . q is set
[:(( the Arity of S * ( the Sorts of o #)) . q),(( the ResultSort of S * the Sorts of o) . q):] is Relation-like set
bool [:(( the Arity of S * ( the Sorts of o #)) . q),(( the ResultSort of S * the Sorts of o) . q):] is non empty set
the ResultSort of S * a is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
Opers ((FreeMSA Y),a) 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 * (a #), the ResultSort of S * a
(Opers ((FreeMSA Y),a)) . q is Relation-like ( the Arity of S * (a #)) . q -defined ( the ResultSort of S * a) . q -valued Function-like V25(( the Arity of S * (a #)) . q,( the ResultSort of S * a) . q) Element of bool [:(( the Arity of S * (a #)) . q),(( the ResultSort of S * a) . q):]
( the ResultSort of S * a) . q is set
[:(( the Arity of S * (a #)) . q),(( the ResultSort of S * a) . q):] is Relation-like set
bool [:(( the Arity of S * (a #)) . q),(( the ResultSort of S * a) . q):] is non empty set
q /. a is Relation-like ( the Arity of S * (a #)) . q -defined ( the ResultSort of S * a) . q -valued Function-like V25(( the Arity of S * (a #)) . q,( the ResultSort of S * a) . q) Element of bool [:(( the Arity of S * (a #)) . q),(( the ResultSort of S * a) . q):]
Args (q,(FreeMSA Y)) is non empty functional Element of proj2 ( the Sorts of (FreeMSA Y) #)
proj2 ( the Sorts of (FreeMSA Y) #) is non empty set
Result (q,(FreeMSA Y)) is non empty Element of proj2 the Sorts of (FreeMSA Y)
proj2 the Sorts of (FreeMSA Y) is non empty set
Den (q,(FreeMSA Y)) is Relation-like Args (q,(FreeMSA Y)) -defined Result (q,(FreeMSA Y)) -valued Function-like V25( Args (q,(FreeMSA Y)), Result (q,(FreeMSA Y))) Element of bool [:(Args (q,(FreeMSA Y))),(Result (q,(FreeMSA Y))):]
[:(Args (q,(FreeMSA Y))),(Result (q,(FreeMSA Y))):] is non empty Relation-like set
bool [:(Args (q,(FreeMSA Y))),(Result (q,(FreeMSA Y))):] is non empty set
(Den (q,(FreeMSA Y))) | (( the Arity of S * (a #)) . q) is Relation-like ( the Arity of S * (a #)) . q -defined Args (q,(FreeMSA Y)) -defined Result (q,(FreeMSA Y)) -valued Function-like Element of bool [:(Args (q,(FreeMSA Y))),(Result (q,(FreeMSA Y))):]
dom (Den (q,(FreeMSA Y))) is functional Element of bool (Args (q,(FreeMSA Y)))
bool (Args (q,(FreeMSA Y))) is non empty set
dom ( the Charact of o . q) is Element of bool (( the Arity of S * ( the Sorts of o #)) . q)
bool (( the Arity of S * ( the Sorts of o #)) . q) is non empty set
s9 is set
( the Charact of A . q) . s9 is set
v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of Args (q,(FreeMSA X))
(Den (q,(FreeMSA X))) . v is set
[q, the carrier of S] is V1() set
{q, the carrier of S} is non empty set
{q} is non empty set
{{q, the carrier of S},{q}} is non empty set
[q, the carrier of S] -tree v is non empty Relation-like Function-like DecoratedTree-like set
p2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Element of Args (q,(FreeMSA Y))
(Den (q,(FreeMSA Y))) . p2 is set
( the Charact of o . q) . s9 is set
the Charact of A . z is Relation-like Function-like set
the Charact of o . z is Relation-like Function-like 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
A is non empty Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of Union the Sorts of (S,X)
(S,A) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) 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
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 non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0}))
(S,(X \/ ( the carrier of S --> {0})),X) 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})))
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
Union (S,(X \/ ( the carrier of S --> {0})),X) is set
dom (S,(X \/ ( the carrier of S --> {0})),X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
(S,(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 X \/ ( the carrier of S --> {0})
(S,a) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
z is set
(S,(X \/ ( the carrier of S --> {0})),X) . z 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
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
the carrier' of S is non empty 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
[A, the carrier of S] is V1() set
{A, the carrier of S} is non empty set
{A} is non empty set
{{A, the carrier of S},{A}} is non empty 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)
rng o is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
[A, the carrier of S] -tree o is non empty Relation-like Function-like DecoratedTree-like set
(S,([A, the carrier of S] -tree o)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
a is set
(S,([A, the carrier of S] -tree o)) . a is set
X . a is set
z is set
z is non empty Relation-like Function-like DecoratedTree-like set
(S,z) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
(S,z) . a is set
dom o is Element of bool NAT
q is set
o . q is Relation-like Function-like set
s9 is V17() V18() V19() V23() V163() V164() ext-real set
o . s9 is Relation-like Function-like set
v 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,v) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
(S,v) . a is set
A is Element of the carrier of S
X . A is non empty set
[:(X . A), the carrier of S:] is non empty Relation-like set
o is Element of X . A
[o,A] is V1() Element of [:(X . A), the carrier of S:]
{o,A} is non empty set
{o} is non empty set
{{o,A},{o}} is non empty set
root-tree [o,A] is non empty trivial Relation-like [:(X . A), the carrier of S:] -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees [:(X . A), the carrier of S:]
FinTrees [:(X . A), the carrier of S:] is non empty functional constituted-DTrees DTree-set of [:(X . A), the carrier of S:]
(S,(root-tree [o,A])) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
a is set
(S,(root-tree [o,A])) . a is set
X . a is set
(S,(root-tree [o,A])) . A is set
{o} is non empty Element of bool (X . A)
bool (X . A) is non empty 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 non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) 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)
S -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 (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 non empty Relation-like the carrier of (DTConMSA Y) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms Y
the_sort_of o is Element of the carrier of S
A . {} is set
a is Element of the carrier of S
X . a is non empty set
z is Element of X . a
[z,a] is V1() Element of [:(X . a), the carrier of S:]
[:(X . a), the carrier of S:] is non empty Relation-like set
{z,a} is non empty set
{z} is non empty set
{{z,a},{z}} is non empty set
a is Element of the carrier of S
X . a is non empty set
z is Element of X . a
[z,a] is V1() Element of [:(X . a), the carrier of S:]
[:(X . a), the carrier of S:] is non empty Relation-like set
{z,a} is non empty set
{z} is non empty set
{{z,a},{z}} is non empty set
{ the carrier of S} is non empty set
the carrier' of S is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
o . {} is set
z is Element of the carrier of S
Y . z is non empty set
q is Element of Y . z
[q,z] is V1() Element of [:(Y . z), the carrier of S:]
[:(Y . z), the carrier of S:] is non empty Relation-like set
{q,z} is non empty set
{q} is non empty set
{{q,z},{q}} is non empty set
root-tree [z,a] is non empty trivial Relation-like [:(X . a), the carrier of S:] -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees [:(X . a), the carrier of S:]
FinTrees [:(X . a), the carrier of S:] is non empty functional constituted-DTrees DTree-set of [:(X . a), the carrier of S:]
root-tree [q,z] is non empty trivial Relation-like [:(Y . z), the carrier of S:] -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees [:(Y . z), the carrier of S:]
FinTrees [:(Y . z), the carrier of S:] is non empty functional constituted-DTrees DTree-set of [:(Y . z), the carrier of S:]
A . {} is set
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
a is set
z is set
[a,z] is V1() set
{a,z} is non empty set
{a} is non empty set
{{a,z},{a}} is non empty set
z is Element of the carrier' of S
the_result_sort_of z is Element of the carrier of S
A . {} is set
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
S is non empty non void feasible V159() ManySortedSign
the carrier of S is non empty set
Y is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V24( the carrier of S) 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)
S -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
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
A is non empty Relation-like the carrier of (DTConMSA Y) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms Y
(S,Y,A) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of Y
(S,A) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
the carrier' of S is non empty set
o is Element of the carrier' of S
Sym (o,Y) is Element of NonTerminals (DTConMSA Y)
NonTerminals (DTConMSA Y) is non empty Element of bool the carrier of (DTConMSA Y)
bool the carrier of (DTConMSA Y) is non empty set
[o, the carrier of S] is V1() set
{o, the carrier of S} is non empty set
{o} is non empty set
{{o, the carrier of S},{o}} is non empty set
a is Relation-like NAT -defined FinTrees the carrier of (DTConMSA Y) -valued Function-like finite FinSequence-like FinSubsequence-like DTree-yielding Function-yielding V54() ArgumentSeq of Sym (o,Y)
rng a is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA Y))
[o, the carrier of S] -tree a is non empty Relation-like Function-like DecoratedTree-like set
(S,Y,([o, the carrier of S] -tree a)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of Y
(S,([o, the carrier of S] -tree a)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
Y /\ (S,([o, the carrier of S] -tree a)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
z is V17() V18() V19() V23() V163() V164() ext-real set
dom a is Element of bool NAT
a . z is Relation-like Function-like set
z is non empty Relation-like the carrier of (DTConMSA Y) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms Y
(S,Y,z) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of Y
(S,z) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
Y /\ (S,z) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
q is set
(S,Y,z) . q is set
X . q is set
v is set
s9 is Element of the carrier of S
(S,Y,([o, the carrier of S] -tree a)) . s9 is set
X . s9 is non empty set
q 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
s9 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
the_arity_of o is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
(the_arity_of o) . z is set
the_sort_of s9 is Element of the carrier of S
len a is V17() V18() V19() V23() V163() V164() ext-real Element of NAT
len (the_arity_of o) is V17() V18() V19() V23() V163() V164() ext-real Element of NAT
Sym (o,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
z 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 (o,X)
(Sym (o,X)) -tree 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
(S,Y,A) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of Y
Y /\ (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
Y . o is non empty set
[:(Y . o), the carrier of S:] is non empty Relation-like set
a is Element of Y . o
[a,o] is V1() Element of [:(Y . o), the carrier of S:]
{a,o} is non empty set
{a} is non empty set
{{a,o},{a}} is non empty set
root-tree [a,o] is non empty trivial Relation-like [:(Y . o), the carrier of S:] -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees [:(Y . o), the carrier of S:]
FinTrees [:(Y . o), the carrier of S:] is non empty functional constituted-DTrees DTree-set of [:(Y . o), the carrier of S:]
(S,Y,(root-tree [a,o])) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of Y
(S,(root-tree [a,o])) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
Y /\ (S,(root-tree [a,o])) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
(S,Y,(root-tree [a,o])) . o is set
X . o is non empty set
{a} is non empty Element of bool (Y . o)
bool (Y . o) is non empty 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
(S,X) is strict non empty MSAlgebra over S
FreeMSA X is strict non-empty free feasible non empty MSAlgebra over S
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
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
(S,(X \/ ( the carrier of S --> {0})),X) 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})))
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
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
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 Element of the carrier of S
the Sorts of (S,X) . A is set
the Sorts of (FreeMSA X) . A is non empty set
a is 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
z is non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0}))
(S,(X \/ ( the carrier of S --> {0})),z) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X \/ ( the carrier of S --> {0})
(S,z) is non empty Relation-like 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_sort_of z is Element of the carrier of S
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
o is Element of the carrier of S
FreeSort (X,o) 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
z is set
a is Element of the carrier of S
FreeSort (X,a) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA X))
DTConMSA X is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
TS (DTConMSA X) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
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)
bool (FinTrees the carrier of (DTConMSA X)) is non empty set
bool (TS (DTConMSA X)) is non empty set
S -Terms X is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA X))
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
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
(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
q is non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0}))
(S,(X \/ ( the carrier of S --> {0})),q) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X \/ ( the carrier of S --> {0})
(S,q) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
the_sort_of z is Element of the carrier of S
the_sort_of q is Element of the carrier of S
{ b<sub>1</sub> where b<sub>1</sub> is non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0})) : ( the_sort_of b<sub>1</sub> = a & (S,(X \/ ( the carrier of S --> {0})),b<sub>1</sub>) c= X ) } 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}))
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
proj1 Y is non empty finite V39() finite-order finite-branching set
(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
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 Y
Y | A is non empty Relation-like the carrier of (DTConMSA X) -valued the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X
(S,X,(Y | A)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X
(S,(Y | A)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
a is set
(S,X,(Y | A)) . a is set
(S,X,Y) . a is set
z is set
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
rng o is non empty Element of bool the carrier of (DTConMSA X)
bool the carrier of (DTConMSA X) is non empty set
{ (b<sub>1</sub> `1) where b₁ is Element of rng o : b₁ `2 = a } is set
rng (Y | A) is non empty Element of bool the carrier of (DTConMSA X)
z is Element of rng (Y | A)
z `1 is set
z `2 is set
rng Y is non empty Element of bool the carrier of (DTConMSA X)
{ (b<sub>1</sub> `1) where b₁ is Element of rng Y : b₁ `2 = 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 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 non empty Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of Union the Sorts of (S,X)
proj1 Y is non empty V39() finite-order finite-branching set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 Y
Y | A is non empty Relation-like Function-like finite DecoratedTree-like finite-order finite-branching 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
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 non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0}))
proj1 a is non empty finite V39() finite-order finite-branching set
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 a
a | z is non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0}))
(S,(X \/ ( the carrier of S --> {0})),(a | z)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of X \/ ( the carrier of S --> {0})
(S,(a | z)) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
(S,(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 X \/ ( the carrier of S --> {0})
(S,a) is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
(S,(X \/ ( the carrier of S --> {0})),X) 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})))
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
dom (S,(X \/ ( the carrier of S --> {0})),X) is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
z is set
(S,(X \/ ( the carrier of S --> {0})),X) . z is set
the_sort_of (a | z) is Element of the carrier of S
{ b<sub>1</sub> where b<sub>1</sub> is non empty Relation-like the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms (X \/ ( the carrier of S --> {0})) : ( the_sort_of b<sub>1</sub> = the_sort_of (a | z) & (S,(X \/ ( the carrier of S --> {0})),b<sub>1</sub>) c= X ) } is set
(S,(X \/ ( the carrier of S --> {0})),X) . (the_sort_of (a | z)) 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
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
rng Y is non empty Element of bool the carrier of (DTConMSA X)
bool the carrier of (DTConMSA X) is non empty set
A is Element of rng Y
A `1 is set
A `2 is set
[(A `1),(A `2)] is V1() set
{(A `1),(A `2)} is non empty set
{(A `1)} is non empty set
{{(A `1),(A `2)},{(A `1)}} is non empty set
proj1 Y is non empty finite V39() finite-order finite-branching set
o is set
Y . o is set
a is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 Y
Y | a is non empty Relation-like the carrier of (DTConMSA X) -valued the carrier of (DTConMSA X) -valued Function-like finite DecoratedTree-like finite-order finite-branching Element of S -Terms X
(Y | a) . {} is set
the carrier' of S is non empty set
{ the carrier of S} is non empty set
[: the carrier' of S,{ the carrier of S}:] is non empty Relation-like set
z is Element of the carrier of S
X . z is non empty set
z is Element of X . z
[z,z] is V1() Element of [:(X . z), the carrier of S:]
[:(X . z), the carrier of S:] is non empty Relation-like set
{z,z} is non empty set
{z} is non empty set
{{z,z},{z}} is non empty 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-yielding the carrier of X -defined Function-like V24( the carrier of X) set
(X,Y) is strict non empty MSAlgebra over X
the Sorts of (X,Y) is non empty Relation-like non empty-yielding the carrier of X -defined Function-like V24( the carrier of X) set
Union the Sorts of (X,Y) is non empty set
A is non empty Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of Union the Sorts of (X,Y)
(X,A) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set
proj2 A is non empty set
o is Element of the carrier of X
(X,A) . o is set
[S,o] is V1() set
{S,o} is non empty set
{S} is non empty set
{{S,o},{S}} is non empty set
Y . o 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
{ (b<sub>1</sub> `1) where b₁ is Element of proj2 A : b₁ `2 = o } is set
z is Element of proj2 A
z `1 is set
z `2 is set
DTConMSA (Y \/ ( the carrier of X --> {0})) is non empty strict with_terminals with_nonterminals with_useful_nonterminals DTConstrStr
the carrier of (DTConMSA (Y \/ ( the carrier of X --> {0}))) is non empty set
FinTrees the carrier of (DTConMSA (Y \/ ( the carrier of X --> {0}))) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA (Y \/ ( the carrier of X --> {0})))
X -Terms (Y \/ ( the carrier of X --> {0})) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (Y \/ ( the carrier of X --> {0}))))
bool (FinTrees the carrier of (DTConMSA (Y \/ ( the carrier of X --> {0})))) is non empty set
proj1 A is non empty V39() finite-order finite-branching set
z is set
A . z is set
z is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of proj1 A
A | z is non empty Relation-like Function-like finite DecoratedTree-like finite-order finite-branching set
q is non empty Relation-like Function-like finite DecoratedTree-like finite-order finite-branching Element of Union the Sorts of (X,Y)
q . {} is set
[S,o] `1 is set
[S,o] `2 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
s9 is Element of the carrier of X
(Y \/ ( the carrier of X --> {0})) . s9 is non empty set
v is Element of (Y \/ ( the carrier of X --> {0})) . s9
[v,s9] is V1() Element of [:((Y \/ ( the carrier of X --> {0})) . s9), the carrier of X:]
[:((Y \/ ( the carrier of X --> {0})) . s9), the carrier of X:] is non empty Relation-like set
{v,s9} is non empty set
{v} is non empty set
{{v,s9},{v}} is non empty set
(X,q) is non empty Relation-like the carrier of X -defined Function-like V24( the carrier of X) set
(X,q) . s9 is set
Y . s9 is set
root-tree [v,s9] is non empty trivial Relation-like [:((Y \/ ( the carrier of X --> {0})) . s9), the carrier of X:] -valued Function-like constant finite DecoratedTree-like finite-order finite-branching Element of FinTrees [:((Y \/ ( the carrier of X --> {0})) . s9), the carrier of X:]
FinTrees [:((Y \/ ( the carrier of X --> {0})) . s9), the carrier of X:] is non empty functional constituted-DTrees DTree-set of [:((Y \/ ( the carrier of X --> {0})) . s9), the carrier of X:]
{v} is non empty Element of bool ((Y \/ ( the carrier of X --> {0})) . s9)
bool ((Y \/ ( the carrier of X --> {0})) . s9) 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
proj2 the Sorts of (S,X) is non empty set
dom the Sorts of (S,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 (S,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
a is Element of the carrier' of S
the_result_sort_of a is Element of the carrier of S
the_arity_of a is Relation-like NAT -defined the carrier of S -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of S *
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
[ the 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 non empty trivial Relation-like Function-like constant finite DecoratedTree-like finite-order finite-branching set
the Sorts of (S,X) . A is set
S is non empty non void feasible V159() ManySortedSign
the carrier' of S is non empty set
X is MSAlgebra over S
Y is MSSubAlgebra of X
the carrier of S is non empty set
the Sorts of X is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
the Sorts of Y 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
Args (o,Y) is Element of proj2 ( the Sorts of Y #)
the Sorts of Y # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of Y #) is non empty set
Args (o,X) is Element of proj2 ( the Sorts of X #)
the Sorts of X # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
proj2 ( the Sorts of X #) 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
A is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of X
A # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
( the Arity of S * (A #)) . o is set
a is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of X
a # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
the Arity of S * (a #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
( the Arity of S * (a #)) . o is set
S is non empty non void feasible V159() ManySortedSign
X is feasible MSAlgebra over S
Y is MSSubAlgebra of X
the carrier of S is non empty set
the Sorts of X is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
the Sorts of Y is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) set
the carrier' of S is non empty set
o is Element of the carrier' of S
Args (o,Y) is Element of proj2 ( the Sorts of Y #)
the Sorts of Y # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
the carrier of S * is non empty functional FinSequence-membered M8( the carrier of S)
proj2 ( the Sorts of Y #) is non empty set
Result (o,Y) is Element of proj2 the Sorts of Y
proj2 the Sorts of Y is non empty set
the Element of Args (o,Y) is Element of Args (o,Y)
Args (o,X) is Element of proj2 ( the Sorts of X #)
the Sorts of X # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
proj2 ( the Sorts of X #) is non empty set
Result (o,X) is Element of proj2 the Sorts of X
proj2 the Sorts of X is non empty set
Den (o,X) is Relation-like Args (o,X) -defined Result (o,X) -valued Function-like V25( Args (o,X), Result (o,X)) Element of bool [:(Args (o,X)),(Result (o,X)):]
[:(Args (o,X)),(Result (o,X)):] is Relation-like set
bool [:(Args (o,X)),(Result (o,X)):] is non empty set
dom (Den (o,X)) is Element of bool (Args (o,X))
bool (Args (o,X)) is non empty set
(Den (o,X)) | (Args (o,Y)) is Relation-like Args (o,Y) -defined Args (o,X) -defined Result (o,X) -valued Function-like Element of bool [:(Args (o,X)),(Result (o,X)):]
dom ((Den (o,X)) | (Args (o,Y))) is Element of bool (Args (o,X))
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
A is non empty Relation-like the carrier of S -defined Function-like V24( the carrier of S) ManySortedSubset of the Sorts of X
the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
( the ResultSort of S * A) . o is set
((Den (o,X)) | (Args (o,Y))) . the Element of Args (o,Y) is set
rng ((Den (o,X)) | (Args (o,Y))) is Element of bool (Result (o,X))
bool (Result (o,X)) 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
A # is non empty Relation-like the carrier of S * -defined Function-like V24( the carrier of S * ) set
the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V24( the carrier' of S) set
( the Arity of S * (A #)) . o is set
(Den (o,X)) | (( the Arity of S * (A #)) . o) is Relation-like Args (o,X) -defined ( the Arity of S * (A #)) . o -defined Args (o,X) -defined Result (o,X) -valued Function-like Element of bool [:(Args (o,X)),(Result (o,X)):]
rng ((Den (o,X)) | (( the Arity of S * (A #)) . o)) is Element of bool (Result (o,X))
S is non empty non void feasible V159() ManySortedSign
X is feasible MSAlgebra over S
Y is MSSubAlgebra of X
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
(S,X) is strict MSAlgebra over S
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
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 feasible MSSubAlgebra of FreeMSA (X \/ ( the carrier of S --> {0}))
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
(S,X) is strict MSAlgebra over S