NAT is Element of bool REAL
REAL is set
bool REAL is set
NAT is set
bool NAT is set
bool NAT is set
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
1 is non empty set
{{},1} is non empty set
Trees is non empty constituted-Trees set
bool Trees is set
FinTrees is non empty constituted-Trees constituted-FinTrees Element of bool Trees
PeanoNat is non empty strict L13()
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 set
[:(TS PeanoNat),NAT:] is Relation-like set
bool [:(TS PeanoNat),NAT:] is set
[:NAT,(TS PeanoNat):] is Relation-like set
bool [:NAT,(TS PeanoNat):] is set
2 is non empty set
3 is non empty set
dom {} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding set
rng {} is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding V133() set
K33() is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() FinSequence-like FinSubsequence-like FinSequence-membered V53() V54() constituted-Trees constituted-FinTrees constituted-DTrees Tree-yielding FinTree-yielding DTree-yielding Element of NAT
K300(K33()) is non empty V113() set
S1 is non empty non void feasible ManySortedSign
the carrier' of S1 is non empty set
the carrier of S1 is non empty set
S2 is Element of the carrier' of S1
S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
DTConMSA S3 is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA S3) is non empty set
FinTrees the carrier of (DTConMSA S3) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA S3)
Sym (S2,S3) is Element of K358((DTConMSA S3))
K358((DTConMSA S3)) is non empty Element of bool the carrier of (DTConMSA S3)
bool the carrier of (DTConMSA S3) is set
FreeMSA S3 is strict non-empty V132(S1) MSAlgebra over S1
Args (S2,(FreeMSA S3)) is non empty functional Element of rng ( the Sorts of (FreeMSA S3) #)
the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
the Sorts of (FreeMSA S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of (FreeMSA S3) #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of (FreeMSA S3) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (FreeMSA S3) #)) . S2 is set
X is set
TS (DTConMSA S3) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))
bool (FinTrees the carrier of (DTConMSA S3)) is set
S1 -Terms S3 is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))
FreeSort S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeOper S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ((FreeSort S3) #), the ResultSort of S1 * (FreeSort S3)
(FreeSort S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ((FreeSort S3) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * (FreeSort S3) is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set
MSAlgebra(# (FreeSort S3),(FreeOper S3) #) is strict MSAlgebra over S1
f1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() DTree-yielding ArgumentSeq of Sym (S2,S3)
g1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() FinSequence of TS (DTConMSA S3)
roots g1 is Relation-like NAT -defined the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA S3)
f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of Args (S2,(FreeMSA S3))
rng f1 is set
g1 is set
dom f1 is Element of bool NAT
f2 is set
f1 . f2 is set
the_arity_of S2 is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
the Arity of S1 . S2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
g2 is Element of NAT
(the_arity_of S2) /. g2 is Element of the carrier of S1
(FreeSort S3) . ((the_arity_of S2) /. g2) is non empty set
FreeSort (S3,((the_arity_of S2) /. g2)) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA S3))
bool (TS (DTConMSA S3)) is set
dom (the_arity_of S2) is Element of bool NAT
g1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() FinSequence of TS (DTConMSA S3)
roots g1 is Relation-like NAT -defined the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA S3)
S1 is non empty non void feasible ManySortedSign
the carrier of S1 is non empty set
the carrier' of S1 is non empty set
S3 is Element of the carrier' of S1
S2 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA S2 is strict non-empty V132(S1) MSAlgebra over S1
Args (S3,(FreeMSA S2)) is non empty functional Element of rng ( the Sorts of (FreeMSA S2) #)
the Sorts of (FreeMSA S2) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
the Sorts of (FreeMSA S2) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of (FreeMSA S2) #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of (FreeMSA S2) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (FreeMSA S2) #)) . S3 is set
X is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of Args (S3,(FreeMSA S2))
S1 is non empty non void feasible ManySortedSign
the carrier of S1 is non empty set
the carrier' of S1 is non empty set
S2 is MSAlgebra over S1
the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set
S3 is MSAlgebra over S1
the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set
X is Element of the carrier' of S1
Args (X,S2) is Element of rng ( the Sorts of S2 #)
the Sorts of S2 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of S2 #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of S2 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of S2 #)) . X is set
Args (X,S3) is Element of rng ( the Sorts of S3 #)
the Sorts of S3 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
rng ( the Sorts of S3 #) is non empty set
the Arity of S1 * ( the Sorts of S3 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of S3 #)) . X is set
f1 is Element of NAT
the_arity_of X is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
the Arity of S1 . X is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
dom (the_arity_of X) is Element of bool NAT
(the_arity_of X) /. f1 is Element of the carrier of S1
the Sorts of S2 . ((the_arity_of X) /. f1) is set
the Sorts of S3 . ((the_arity_of X) /. f1) is set
S1 is non empty non void feasible ManySortedSign
the carrier' of S1 is non empty set
the carrier of S1 is non empty set
S2 is Element of the carrier' of S1
[S2, the carrier of S1] is set
{S2, the carrier of S1} is non empty set
{S2} is non empty set
{{S2, the carrier of S1},{S2}} is non empty set
S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA S3 is strict non-empty V132(S1) MSAlgebra over S1
Args (S2,(FreeMSA S3)) is non empty functional Element of rng ( the Sorts of (FreeMSA S3) #)
the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
the Sorts of (FreeMSA S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of (FreeMSA S3) #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of (FreeMSA S3) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (FreeMSA S3) #)) . S2 is set
Result (S2,(FreeMSA S3)) is non empty Element of rng the Sorts of (FreeMSA S3)
rng the Sorts of (FreeMSA S3) is non empty V133() set
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set
( the ResultSort of S1 * the Sorts of (FreeMSA S3)) . S2 is non empty set
Den (S2,(FreeMSA S3)) is non empty Relation-like Args (S2,(FreeMSA S3)) -defined Result (S2,(FreeMSA S3)) -valued Function-like total V29( Args (S2,(FreeMSA S3)), Result (S2,(FreeMSA S3))) Element of bool [:(Args (S2,(FreeMSA S3))),(Result (S2,(FreeMSA S3))):]
[:(Args (S2,(FreeMSA S3))),(Result (S2,(FreeMSA S3))):] is Relation-like set
bool [:(Args (S2,(FreeMSA S3))),(Result (S2,(FreeMSA S3))):] is set
the Charact of (FreeMSA S3) is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of (FreeMSA S3) #), the ResultSort of S1 * the Sorts of (FreeMSA S3)
the Charact of (FreeMSA S3) . S2 is Relation-like Function-like set
X is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like DTree-yielding Element of Args (S2,(FreeMSA S3))
(Den (S2,(FreeMSA S3))) . X is Element of Result (S2,(FreeMSA S3))
[S2, the carrier of S1] -tree X is Relation-like Function-like V117() set
FreeSort S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeOper S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ((FreeSort S3) #), the ResultSort of S1 * (FreeSort S3)
(FreeSort S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ((FreeSort S3) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * (FreeSort S3) is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set
MSAlgebra(# (FreeSort S3),(FreeOper S3) #) is strict MSAlgebra over S1
DTConMSA S3 is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA S3) is non empty set
FinTrees the carrier of (DTConMSA S3) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA S3)
Sym (S2,S3) is Element of K358((DTConMSA S3))
K358((DTConMSA S3)) is non empty Element of bool the carrier of (DTConMSA S3)
bool the carrier of (DTConMSA S3) is set
f1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() DTree-yielding ArgumentSeq of Sym (S2,S3)
TS (DTConMSA S3) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))
bool (FinTrees the carrier of (DTConMSA S3)) is set
roots f1 is Relation-like NAT -defined the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of (DTConMSA S3)
DenOp (S2,S3) is Relation-like ( the Arity of S1 * ((FreeSort S3) #)) . S2 -defined ( the ResultSort of S1 * (FreeSort S3)) . S2 -valued Function-like total V29(( the Arity of S1 * ((FreeSort S3) #)) . S2,( the ResultSort of S1 * (FreeSort S3)) . S2) Element of bool [:(( the Arity of S1 * ((FreeSort S3) #)) . S2),(( the ResultSort of S1 * (FreeSort S3)) . S2):]
( the Arity of S1 * ((FreeSort S3) #)) . S2 is set
( the ResultSort of S1 * (FreeSort S3)) . S2 is non empty set
[:(( the Arity of S1 * ((FreeSort S3) #)) . S2),(( the ResultSort of S1 * (FreeSort S3)) . S2):] is Relation-like set
bool [:(( the Arity of S1 * ((FreeSort S3) #)) . S2),(( the ResultSort of S1 * (FreeSort S3)) . S2):] is set
(DenOp (S2,S3)) . X is set
S1 is non empty non void feasible ManySortedSign
the carrier' of S1 is non empty set
S2 is MSAlgebra over S1
the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set
the carrier of S1 is non empty set
the Charact of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S2 #), the ResultSort of S1 * the Sorts of S2
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Sorts of S2 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of S2 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of S2, the Charact of S2 #) is strict MSAlgebra over S1
S3 is MSAlgebra over S1
the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S3 #), the ResultSort of S1 * the Sorts of S3
the Sorts of S3 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of S3 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of S3, the Charact of S3 #) is strict MSAlgebra over S1
X is Element of the carrier' of S1
Den (X,S2) is Relation-like Args (X,S2) -defined Result (X,S2) -valued Function-like V29( Args (X,S2), Result (X,S2)) Element of bool [:(Args (X,S2)),(Result (X,S2)):]
Args (X,S2) is Element of rng ( the Sorts of S2 #)
rng ( the Sorts of S2 #) is non empty set
( the Arity of S1 * ( the Sorts of S2 #)) . X is set
Result (X,S2) is Element of rng the Sorts of S2
rng the Sorts of S2 is non empty set
( the ResultSort of S1 * the Sorts of S2) . X is set
[:(Args (X,S2)),(Result (X,S2)):] is Relation-like set
bool [:(Args (X,S2)),(Result (X,S2)):] is set
the Charact of S2 . X is Relation-like Function-like set
Den (X,S3) is Relation-like Args (X,S3) -defined Result (X,S3) -valued Function-like V29( Args (X,S3), Result (X,S3)) Element of bool [:(Args (X,S3)),(Result (X,S3)):]
Args (X,S3) is Element of rng ( the Sorts of S3 #)
rng ( the Sorts of S3 #) is non empty set
( the Arity of S1 * ( the Sorts of S3 #)) . X is set
Result (X,S3) is Element of rng the Sorts of S3
rng the Sorts of S3 is non empty set
( the ResultSort of S1 * the Sorts of S3) . X is set
[:(Args (X,S3)),(Result (X,S3)):] is Relation-like set
bool [:(Args (X,S3)),(Result (X,S3)):] is set
the Charact of S3 . X is Relation-like Function-like set
S1 is non empty non void feasible ManySortedSign
the carrier of S1 is non empty set
the carrier' of S1 is non empty set
S2 is MSAlgebra over S1
the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S2 #), the ResultSort of S1 * the Sorts of S2
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Sorts of S2 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of S2 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of S2, the Charact of S2 #) is strict MSAlgebra over S1
X is MSAlgebra over S1
the Sorts of X is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of X is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of X #), the ResultSort of S1 * the Sorts of X
the Sorts of X # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of X #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of X is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of X, the Charact of X #) is strict MSAlgebra over S1
S3 is MSAlgebra over S1
the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S3 #), the ResultSort of S1 * the Sorts of S3
the Sorts of S3 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of S3 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of S3, the Charact of S3 #) is strict MSAlgebra over S1
f1 is MSAlgebra over S1
the Sorts of f1 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of f1 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of f1 #), the ResultSort of S1 * the Sorts of f1
the Sorts of f1 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of f1 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of f1 is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of f1, the Charact of f1 #) is strict MSAlgebra over S1
g1 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of S2, the Sorts of S3
f2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of X, the Sorts of f1
g2 is Element of the carrier' of S1
Args (g2,S2) is Element of rng ( the Sorts of S2 #)
rng ( the Sorts of S2 #) is non empty set
( the Arity of S1 * ( the Sorts of S2 #)) . g2 is set
Args (g2,S3) is Element of rng ( the Sorts of S3 #)
rng ( the Sorts of S3 #) is non empty set
( the Arity of S1 * ( the Sorts of S3 #)) . g2 is set
Args (g2,X) is Element of rng ( the Sorts of X #)
rng ( the Sorts of X #) is non empty set
( the Arity of S1 * ( the Sorts of X #)) . g2 is set
f is Element of Args (g2,S2)
g1 # f is Element of Args (g2,S3)
g is Element of Args (g2,X)
f2 # g is Element of Args (g2,f1)
Args (g2,f1) is Element of rng ( the Sorts of f1 #)
rng ( the Sorts of f1 #) is non empty set
( the Arity of S1 * ( the Sorts of f1 #)) . g2 is set
the_arity_of g2 is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
the Arity of S1 . g2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
(the_arity_of g2) * g1 is Relation-like NAT -defined Function-like V53() V54() set
Frege ((the_arity_of g2) * g1) is Relation-like product K180(((the_arity_of g2) * g1)) -defined Function-like total V53() V54() set
K180(((the_arity_of g2) * g1)) is Relation-like Function-like set
product K180(((the_arity_of g2) * g1)) is set
(Frege ((the_arity_of g2) * g1)) . f is Relation-like Function-like set
S1 is non empty non void feasible ManySortedSign
the carrier of S1 is non empty set
S2 is MSAlgebra over S1
the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S2 #), the ResultSort of S1 * the Sorts of S2
the carrier' of S1 is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Sorts of S2 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of S2 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of S2 is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of S2, the Charact of S2 #) is strict MSAlgebra over S1
X is MSAlgebra over S1
the Sorts of X is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of X is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of X #), the ResultSort of S1 * the Sorts of X
the Sorts of X # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of X #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of X is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of X, the Charact of X #) is strict MSAlgebra over S1
S3 is MSAlgebra over S1
the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S3 #), the ResultSort of S1 * the Sorts of S3
the Sorts of S3 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of S3 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of S3, the Charact of S3 #) is strict MSAlgebra over S1
f1 is MSAlgebra over S1
the Sorts of f1 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of f1 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of f1 #), the ResultSort of S1 * the Sorts of f1
the Sorts of f1 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of f1 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of f1 is non empty Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of f1, the Charact of f1 #) is strict MSAlgebra over S1
g1 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of S2, the Sorts of S3
f2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of X, the Sorts of f1
g2 is Element of the carrier' of S1
Args (g2,X) is Element of rng ( the Sorts of X #)
rng ( the Sorts of X #) is non empty set
( the Arity of S1 * ( the Sorts of X #)) . g2 is set
the_result_sort_of g2 is Element of the carrier of S1
the ResultSort of S1 . g2 is Element of the carrier of S1
f2 . (the_result_sort_of g2) is Relation-like the Sorts of X . (the_result_sort_of g2) -defined the Sorts of f1 . (the_result_sort_of g2) -valued Function-like V29( the Sorts of X . (the_result_sort_of g2), the Sorts of f1 . (the_result_sort_of g2)) Element of bool [:( the Sorts of X . (the_result_sort_of g2)),( the Sorts of f1 . (the_result_sort_of g2)):]
the Sorts of X . (the_result_sort_of g2) is set
the Sorts of f1 . (the_result_sort_of g2) is set
[:( the Sorts of X . (the_result_sort_of g2)),( the Sorts of f1 . (the_result_sort_of g2)):] is Relation-like set
bool [:( the Sorts of X . (the_result_sort_of g2)),( the Sorts of f1 . (the_result_sort_of g2)):] is set
Den (g2,X) is Relation-like Args (g2,X) -defined Result (g2,X) -valued Function-like V29( Args (g2,X), Result (g2,X)) Element of bool [:(Args (g2,X)),(Result (g2,X)):]
Result (g2,X) is Element of rng the Sorts of X
rng the Sorts of X is non empty set
( the ResultSort of S1 * the Sorts of X) . g2 is set
[:(Args (g2,X)),(Result (g2,X)):] is Relation-like set
bool [:(Args (g2,X)),(Result (g2,X)):] is set
the Charact of X . g2 is Relation-like Function-like set
Den (g2,f1) is Relation-like Args (g2,f1) -defined Result (g2,f1) -valued Function-like V29( Args (g2,f1), Result (g2,f1)) Element of bool [:(Args (g2,f1)),(Result (g2,f1)):]
Args (g2,f1) is Element of rng ( the Sorts of f1 #)
rng ( the Sorts of f1 #) is non empty set
( the Arity of S1 * ( the Sorts of f1 #)) . g2 is set
Result (g2,f1) is Element of rng the Sorts of f1
rng the Sorts of f1 is non empty set
( the ResultSort of S1 * the Sorts of f1) . g2 is set
[:(Args (g2,f1)),(Result (g2,f1)):] is Relation-like set
bool [:(Args (g2,f1)),(Result (g2,f1)):] is set
the Charact of f1 . g2 is Relation-like Function-like set
f is Element of Args (g2,X)
(Den (g2,X)) . f is set
(f2 . (the_result_sort_of g2)) . ((Den (g2,X)) . f) is set
f2 # f is Element of Args (g2,f1)
(Den (g2,f1)) . (f2 # f) is set
Args (g2,S2) is Element of rng ( the Sorts of S2 #)
rng ( the Sorts of S2 #) is non empty set
( the Arity of S1 * ( the Sorts of S2 #)) . g2 is set
g1 . (the_result_sort_of g2) is Relation-like the Sorts of S2 . (the_result_sort_of g2) -defined the Sorts of S3 . (the_result_sort_of g2) -valued Function-like V29( the Sorts of S2 . (the_result_sort_of g2), the Sorts of S3 . (the_result_sort_of g2)) Element of bool [:( the Sorts of S2 . (the_result_sort_of g2)),( the Sorts of S3 . (the_result_sort_of g2)):]
the Sorts of S2 . (the_result_sort_of g2) is set
the Sorts of S3 . (the_result_sort_of g2) is set
[:( the Sorts of S2 . (the_result_sort_of g2)),( the Sorts of S3 . (the_result_sort_of g2)):] is Relation-like set
bool [:( the Sorts of S2 . (the_result_sort_of g2)),( the Sorts of S3 . (the_result_sort_of g2)):] is set
Den (g2,S2) is Relation-like Args (g2,S2) -defined Result (g2,S2) -valued Function-like V29( Args (g2,S2), Result (g2,S2)) Element of bool [:(Args (g2,S2)),(Result (g2,S2)):]
Result (g2,S2) is Element of rng the Sorts of S2
rng the Sorts of S2 is non empty set
( the ResultSort of S1 * the Sorts of S2) . g2 is set
[:(Args (g2,S2)),(Result (g2,S2)):] is Relation-like set
bool [:(Args (g2,S2)),(Result (g2,S2)):] is set
the Charact of S2 . g2 is Relation-like Function-like set
g is Element of Args (g2,S2)
(Den (g2,S2)) . g is set
(g1 . (the_result_sort_of g2)) . ((Den (g2,S2)) . g) is set
Den (g2,S3) is Relation-like Args (g2,S3) -defined Result (g2,S3) -valued Function-like V29( Args (g2,S3), Result (g2,S3)) Element of bool [:(Args (g2,S3)),(Result (g2,S3)):]
Args (g2,S3) is Element of rng ( the Sorts of S3 #)
rng ( the Sorts of S3 #) is non empty set
( the Arity of S1 * ( the Sorts of S3 #)) . g2 is set
Result (g2,S3) is Element of rng the Sorts of S3
rng the Sorts of S3 is non empty set
( the ResultSort of S1 * the Sorts of S3) . g2 is set
[:(Args (g2,S3)),(Result (g2,S3)):] is Relation-like set
bool [:(Args (g2,S3)),(Result (g2,S3)):] is set
the Charact of S3 . g2 is Relation-like Function-like set
g1 # g is Element of Args (g2,S3)
(Den (g2,S3)) . (g1 # g) is set
S1 is ManySortedSign
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
the carrier' of S1 is set
the carrier of S1 is set
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
dom the ResultSort of S1 is set
S1 is ManySortedSign
the carrier of S1 is set
the carrier' of S1 is set
S1 is ManySortedSign
the carrier of S1 is set
the carrier' of S1 is set
S1 is ManySortedSign
the carrier of S1 is set
the carrier' of S1 is set
S1 is ManySortedSign
the non empty non void feasible () ManySortedSign is non empty non void feasible () ManySortedSign
S1 is () ManySortedSign
the carrier of S1 is set
id the carrier of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total V29( the carrier of S1, the carrier of S1) Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is set
the carrier' of S1 is set
id the carrier' of S1 is Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total V29( the carrier' of S1, the carrier' of S1) Element of bool [: the carrier' of S1, the carrier' of S1:]
[: the carrier' of S1, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is set
S2 is non empty non void feasible () ManySortedSign
S1 is ManySortedSign
S2 is ManySortedSign
the carrier of S1 is set
the carrier of S2 is set
[: the carrier of S1, the carrier of S2:] is Relation-like set
bool [: the carrier of S1, the carrier of S2:] is set
the carrier' of S1 is set
the carrier' of S2 is set
[: the carrier' of S1, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S2:] is set
S3 is Relation-like Function-like set
X is Relation-like Function-like set
dom S3 is set
rng S3 is set
dom X is set
rng X is set
S1 is () ManySortedSign
the carrier of S1 is set
id the carrier of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total V29( the carrier of S1, the carrier of S1) Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is set
the carrier' of S1 is set
id the carrier' of S1 is Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total V29( the carrier' of S1, the carrier' of S1) Element of bool [: the carrier' of S1, the carrier' of S1:]
[: the carrier' of S1, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is set
S1 is () ManySortedSign
the carrier of S1 is set
the carrier' of S1 is set
S2 is (S1)
the carrier of S2 is set
the carrier' of S2 is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
rng (id the carrier of S2) is set
rng (id the carrier' of S2) is set
S1 is () ManySortedSign
S2 is (S1)
the carrier of S2 is set
id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
the carrier' of S2 is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
dom (id the carrier' of S2) is set
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
(id the carrier of S2) * the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
the carrier' of S1 is set
the carrier of S1 is set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * (id the carrier' of S2) is Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S2, the carrier of S1:]
[: the carrier' of S2, the carrier of S1:] is Relation-like set
bool [: the carrier' of S2, the carrier of S1:] is set
dom the ResultSort of S1 is set
rng (id the carrier' of S2) is set
S1 is () ManySortedSign
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
the carrier' of S1 is set
the carrier of S1 is set
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
S2 is () (S1)
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
the carrier' of S2 is set
the carrier of S2 is set
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
dom the Arity of S2 is set
rng the Arity of S2 is set
f1 is set
the Arity of S2 . f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
(id the carrier' of S2) . f1 is set
g1 is Relation-like NAT -defined the carrier of S2 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *
rng g1 is set
(id the carrier of S2) * g1 is Relation-like NAT -defined the carrier of S2 -valued Function-like Element of bool [:NAT, the carrier of S2:]
[:NAT, the carrier of S2:] is Relation-like set
bool [:NAT, the carrier of S2:] is set
the Arity of S1 . f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
(id the carrier of S2) * the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
the ResultSort of S1 * (id the carrier' of S2) is Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S2, the carrier of S1:]
[: the carrier' of S2, the carrier of S1:] is Relation-like set
bool [: the carrier' of S2, the carrier of S1:] is set
dom the Arity of S1 is set
S1 is () ManySortedSign
the carrier' of S1 is set
the carrier of S1 is set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
S2 is () (S1)
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier' of S2 is set
the carrier of S2 is set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S1 | the carrier' of S2 is Relation-like the carrier' of S1 -defined the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 * -valued Function-like V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S1 | the carrier' of S2 is Relation-like the carrier' of S1 -defined the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S1, the carrier of S1:]
dom the ResultSort of S2 is set
dom the Arity of S2 is set
S2 is () ManySortedSign
the carrier of S2 is set
S1 is () ManySortedSign
the carrier of S1 is set
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier' of S2 is set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier' of S1 is set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
dom (id the carrier of S2) is set
dom (id the carrier' of S2) is set
rng (id the carrier of S2) is set
rng (id the carrier' of S2) is set
the ResultSort of S2 * (id the carrier of S2) is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like set
(id the carrier' of S2) * the ResultSort of S1 is Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like set
dom the Arity of S2 is set
dom the Arity of S1 is set
dom the ResultSort of S2 is set
rng the ResultSort of S2 is set
(id the carrier of S2) * the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
the ResultSort of S1 | the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S1, the carrier of S1:]
the ResultSort of S1 * (id the carrier' of S2) is Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S2, the carrier of S1:]
[: the carrier' of S2, the carrier of S1:] is Relation-like set
bool [: the carrier' of S2, the carrier of S1:] is set
f1 is set
the Arity of S2 . f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
(id the carrier' of S2) . f1 is set
the Arity of S1 . ((id the carrier' of S2) . f1) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
g1 is Relation-like Function-like set
g1 * (id the carrier of S2) is Relation-like the carrier of S2 -valued Function-like set
f2 is Relation-like NAT -defined the carrier of S2 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *
rng f2 is set
the Arity of S1 . f1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
S2 is () ManySortedSign
the carrier of S2 is set
S1 is () ManySortedSign
the carrier of S1 is set
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier' of S2 is set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the carrier' of S1 is set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 | the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 * -valued Function-like V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 | the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S1 -defined the carrier of S1 -valued Function-like Element of bool [: the carrier' of S1, the carrier of S1:]
S1 is () ManySortedSign
the carrier of S1 is set
id the carrier of S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total V29( the carrier of S1, the carrier of S1) Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is set
the carrier' of S1 is set
id the carrier' of S1 is Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total V29( the carrier' of S1, the carrier' of S1) Element of bool [: the carrier' of S1, the carrier' of S1:]
[: the carrier' of S1, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is set
S1 is () ManySortedSign
S2 is () (S1)
S3 is () (S2)
the carrier of S3 is set
id the carrier of S3 is Relation-like the carrier of S3 -defined the carrier of S3 -valued Function-like one-to-one total V29( the carrier of S3, the carrier of S3) Element of bool [: the carrier of S3, the carrier of S3:]
[: the carrier of S3, the carrier of S3:] is Relation-like set
bool [: the carrier of S3, the carrier of S3:] is set
rng (id the carrier of S3) is set
the carrier of S2 is set
id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
(id the carrier of S2) * (id the carrier of S3) is Relation-like the carrier of S3 -defined the carrier of S2 -valued Function-like one-to-one Element of bool [: the carrier of S3, the carrier of S2:]
[: the carrier of S3, the carrier of S2:] is Relation-like set
bool [: the carrier of S3, the carrier of S2:] is set
the carrier' of S3 is set
id the carrier' of S3 is Relation-like the carrier' of S3 -defined the carrier' of S3 -valued Function-like one-to-one total V29( the carrier' of S3, the carrier' of S3) Element of bool [: the carrier' of S3, the carrier' of S3:]
[: the carrier' of S3, the carrier' of S3:] is Relation-like set
bool [: the carrier' of S3, the carrier' of S3:] is set
rng (id the carrier' of S3) is set
the carrier' of S2 is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
(id the carrier' of S2) * (id the carrier' of S3) is Relation-like the carrier' of S3 -defined the carrier' of S2 -valued Function-like one-to-one Element of bool [: the carrier' of S3, the carrier' of S2:]
[: the carrier' of S3, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S3, the carrier' of S2:] is set
S1 is () ManySortedSign
the carrier of S1 is set
the carrier' of S1 is set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) is strict ManySortedSign
S2 is () (S1)
the carrier of S2 is set
the carrier' of S2 is set
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) is strict ManySortedSign
S1 is non empty feasible () ManySortedSign
S2 is () (S1)
S1 is non empty non void feasible () ManySortedSign
S2 is () (S1)
S1 is () ManySortedSign
S2 is () (S1)
the carrier of S2 is set
the carrier' of S2 is set
S3 is ManySortedSign
X is Relation-like Function-like set
f1 is Relation-like Function-like set
X | the carrier of S2 is Relation-like Function-like set
f1 | the carrier' of S2 is Relation-like Function-like set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
(id the carrier' of S2) * f1 is Relation-like the carrier' of S2 -defined Function-like set
id the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
(id the carrier of S2) * X is Relation-like the carrier of S2 -defined Function-like set
S1 is ManySortedSign
S2 is () ManySortedSign
S3 is () (S2)
X is Relation-like Function-like set
f1 is Relation-like Function-like set
rng X is set
the carrier of S3 is set
id the carrier of S3 is Relation-like the carrier of S3 -defined the carrier of S3 -valued Function-like one-to-one total V29( the carrier of S3, the carrier of S3) Element of bool [: the carrier of S3, the carrier of S3:]
[: the carrier of S3, the carrier of S3:] is Relation-like set
bool [: the carrier of S3, the carrier of S3:] is set
X * (id the carrier of S3) is Relation-like the carrier of S3 -valued Function-like set
rng f1 is set
the carrier' of S3 is set
id the carrier' of S3 is Relation-like the carrier' of S3 -defined the carrier' of S3 -valued Function-like one-to-one total V29( the carrier' of S3, the carrier' of S3) Element of bool [: the carrier' of S3, the carrier' of S3:]
[: the carrier' of S3, the carrier' of S3:] is Relation-like set
bool [: the carrier' of S3, the carrier' of S3:] is set
f1 * (id the carrier' of S3) is Relation-like the carrier' of S3 -valued Function-like set
S1 is ManySortedSign
S2 is () ManySortedSign
S3 is () (S2)
the carrier of S3 is set
the carrier' of S3 is set
X is Relation-like Function-like set
f1 is Relation-like Function-like set
rng X is set
rng f1 is set
dom X is set
the carrier of S1 is set
dom f1 is set
the carrier' of S1 is set
the carrier of S2 is set
the carrier' of S2 is set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * X is Relation-like the carrier' of S1 -defined Function-like set
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
f1 * the ResultSort of S2 is Relation-like the carrier of S2 -valued Function-like set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the ResultSort of S3 is Relation-like the carrier' of S3 -defined the carrier of S3 -valued Function-like V29( the carrier' of S3, the carrier of S3) Element of bool [: the carrier' of S3, the carrier of S3:]
[: the carrier' of S3, the carrier of S3:] is Relation-like set
bool [: the carrier' of S3, the carrier of S3:] is set
f1 * the ResultSort of S3 is Relation-like the carrier of S3 -valued Function-like set
the Arity of S3 is Relation-like the carrier' of S3 -defined the carrier of S3 * -valued Function-like total V29( the carrier' of S3, the carrier of S3 * ) V53() V54() Element of bool [: the carrier' of S3,( the carrier of S3 *):]
the carrier of S3 * is non empty functional FinSequence-membered M12( the carrier of S3)
[: the carrier' of S3,( the carrier of S3 *):] is Relation-like set
bool [: the carrier' of S3,( the carrier of S3 *):] is set
id the carrier' of S3 is Relation-like the carrier' of S3 -defined the carrier' of S3 -valued Function-like one-to-one total V29( the carrier' of S3, the carrier' of S3) Element of bool [: the carrier' of S3, the carrier' of S3:]
[: the carrier' of S3, the carrier' of S3:] is Relation-like set
bool [: the carrier' of S3, the carrier' of S3:] is set
f1 * (id the carrier' of S3) is Relation-like the carrier' of S3 -valued Function-like set
(f1 * (id the carrier' of S3)) * the ResultSort of S2 is Relation-like the carrier of S2 -valued Function-like set
the ResultSort of S2 * (id the carrier' of S3) is Relation-like the carrier' of S3 -defined the carrier of S2 -valued Function-like Element of bool [: the carrier' of S3, the carrier of S2:]
[: the carrier' of S3, the carrier of S2:] is Relation-like set
bool [: the carrier' of S3, the carrier of S2:] is set
f1 * ( the ResultSort of S2 * (id the carrier' of S3)) is Relation-like the carrier of S2 -valued Function-like set
the ResultSort of S2 | the carrier' of S3 is Relation-like the carrier' of S3 -defined the carrier' of S2 -defined the carrier of S2 -valued Function-like Element of bool [: the carrier' of S2, the carrier of S2:]
f1 * ( the ResultSort of S2 | the carrier' of S3) is Relation-like the carrier of S2 -valued Function-like set
g1 is set
the Arity of S1 . g1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
f1 . g1 is set
the Arity of S3 . (f1 . g1) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
f2 is Relation-like Function-like set
f2 * X is Relation-like Function-like set
dom the Arity of S3 is set
the Arity of S2 . (f1 . g1) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
S2 is non empty feasible () ManySortedSign
S1 is non empty feasible () ManySortedSign
X is Relation-like Function-like set
f1 is Relation-like Function-like set
S3 is MSAlgebra over S2
the Sorts of S3 is non empty Relation-like the carrier of S2 -defined Function-like total set
the carrier of S2 is non empty set
X * the Sorts of S3 is Relation-like Function-like set
the Charact of S3 is Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of S3 #), the ResultSort of S2 * the Sorts of S3
the carrier' of S2 is set
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Sorts of S3 # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the Arity of S2 * ( the Sorts of S3 #) is Relation-like the carrier' of S2 -defined Function-like total set
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S2 * the Sorts of S3 is Relation-like the carrier' of S2 -defined Function-like total set
f1 * the Charact of S3 is Relation-like Function-like V53() V54() set
dom X is set
the carrier of S1 is non empty set
rng X is set
[: the carrier of S1, the carrier of S2:] is Relation-like set
bool [: the carrier of S1, the carrier of S2:] is set
rng f1 is set
dom f1 is set
the carrier' of S1 is set
[: the carrier' of S1, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S2:] is set
dom the Charact of S3 is set
f2 is Relation-like the carrier' of S1 -defined the carrier' of S2 -valued Function-like V29( the carrier' of S1, the carrier' of S2) Element of bool [: the carrier' of S1, the carrier' of S2:]
f2 * the Charact of S3 is Relation-like the carrier' of S1 -defined Function-like V53() V54() set
dom (f2 * the Charact of S3) is set
g2 is Relation-like the carrier' of S1 -defined Function-like total set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
g1 is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier of S1, the carrier of S2) Element of bool [: the carrier of S1, the carrier of S2:]
g1 * the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set
(g1 * the Sorts of S3) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ((g1 * the Sorts of S3) #) is Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * (g1 * the Sorts of S3) is Relation-like the carrier' of S1 -defined Function-like total set
f is set
g2 . f is set
( the Arity of S1 * ((g1 * the Sorts of S3) #)) . f is set
( the ResultSort of S1 * (g1 * the Sorts of S3)) . f is set
[:(( the Arity of S1 * ((g1 * the Sorts of S3) #)) . f),(( the ResultSort of S1 * (g1 * the Sorts of S3)) . f):] is Relation-like set
bool [:(( the Arity of S1 * ((g1 * the Sorts of S3) #)) . f),(( the ResultSort of S1 * (g1 * the Sorts of S3)) . f):] is set
the Arity of S1 . f is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
f1 . f is set
the Arity of S2 . (f1 . f) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
Af1 is Element of the carrier' of S1
g2 . Af1 is set
f2 . Af1 is set
the Charact of S3 . (f2 . Af1) is Relation-like Function-like set
g1 * the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S1, the carrier of S2) Element of bool [: the carrier' of S1, the carrier of S2:]
[: the carrier' of S1, the carrier of S2:] is Relation-like set
bool [: the carrier' of S1, the carrier of S2:] is set
(g1 * the ResultSort of S1) * the Sorts of S3 is Relation-like the carrier' of S1 -defined Function-like total set
f1 * the ResultSort of S2 is Relation-like the carrier of S2 -valued Function-like set
(f1 * the ResultSort of S2) * the Sorts of S3 is Relation-like Function-like set
f1 * ( the ResultSort of S2 * the Sorts of S3) is Relation-like Function-like set
( the ResultSort of S1 * (g1 * the Sorts of S3)) . Af1 is set
( the ResultSort of S2 * the Sorts of S3) . (f2 . Af1) is set
g is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
g * (g1 * the Sorts of S3) is Relation-like NAT -defined Function-like set
g1 * g is Relation-like NAT -defined the carrier of S2 -valued Function-like Element of bool [:NAT, the carrier of S2:]
[:NAT, the carrier of S2:] is Relation-like set
bool [:NAT, the carrier of S2:] is set
(g1 * g) * the Sorts of S3 is Relation-like NAT -defined Function-like set
Af is Relation-like NAT -defined the carrier of S2 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *
Af * the Sorts of S3 is Relation-like NAT -defined Function-like set
( the Arity of S1 * ((g1 * the Sorts of S3) #)) . Af1 is set
((g1 * the Sorts of S3) #) . g is set
product (g * (g1 * the Sorts of S3)) is set
( the Sorts of S3 #) . Af is set
( the Arity of S2 * ( the Sorts of S3 #)) . (f2 . Af1) is set
f is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ((g1 * the Sorts of S3) #), the ResultSort of S1 * (g1 * the Sorts of S3)
MSAlgebra(# (g1 * the Sorts of S3),f #) is strict MSAlgebra over S1
the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of MSAlgebra(# (g1 * the Sorts of S3),f #) is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) #), the ResultSort of S1 * the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #)
the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) #) is Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of MSAlgebra(# (g1 * the Sorts of S3),f #) is Relation-like the carrier' of S1 -defined Function-like total set
g1 is strict MSAlgebra over S1
the Sorts of g1 is non empty Relation-like the carrier of S1 -defined Function-like total set
the carrier of S1 is non empty set
the Charact of g1 is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of g1 #), the ResultSort of S1 * the Sorts of g1
the carrier' of S1 is set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Sorts of g1 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of g1 #) is Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of g1 is Relation-like the carrier' of S1 -defined Function-like total set
f2 is strict MSAlgebra over S1
the Sorts of f2 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of f2 is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of f2 #), the ResultSort of S1 * the Sorts of f2
the Sorts of f2 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of f2 #) is Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of f2 is Relation-like the carrier' of S1 -defined Function-like total set
S1 is non empty feasible () ManySortedSign
S2 is non empty feasible () ManySortedSign
S3 is MSAlgebra over S1
the carrier of S2 is non empty set
id the carrier of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
the carrier' of S2 is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
(S2,S1,S3,(id the carrier of S2),(id the carrier' of S2)) is strict MSAlgebra over S2
S2 is non empty feasible () ManySortedSign
S1 is non empty feasible () ManySortedSign
S3 is MSAlgebra over S2
the Sorts of S3 is non empty Relation-like the carrier of S2 -defined Function-like total set
the carrier of S2 is non empty set
the Charact of S3 is Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of S3 #), the ResultSort of S2 * the Sorts of S3
the carrier' of S2 is set
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Sorts of S3 # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the Arity of S2 * ( the Sorts of S3 #) is Relation-like the carrier' of S2 -defined Function-like total set
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S2 * the Sorts of S3 is Relation-like the carrier' of S2 -defined Function-like total set
MSAlgebra(# the Sorts of S3, the Charact of S3 #) is strict MSAlgebra over S2
X is MSAlgebra over S2
the Sorts of X is non empty Relation-like the carrier of S2 -defined Function-like total set
the Charact of X is Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of X #), the ResultSort of S2 * the Sorts of X
the Sorts of X # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the Arity of S2 * ( the Sorts of X #) is Relation-like the carrier' of S2 -defined Function-like total set
the ResultSort of S2 * the Sorts of X is Relation-like the carrier' of S2 -defined Function-like total set
MSAlgebra(# the Sorts of X, the Charact of X #) is strict MSAlgebra over S2
f1 is Relation-like Function-like set
g1 is Relation-like Function-like set
(S1,S2,S3,f1,g1) is strict MSAlgebra over S1
(S1,S2,X,f1,g1) is strict MSAlgebra over S1
the Sorts of (S1,S2,S3,f1,g1) is non empty Relation-like the carrier of S1 -defined Function-like total set
the carrier of S1 is non empty set
f1 * the Sorts of S3 is Relation-like Function-like set
the Charact of (S1,S2,S3,f1,g1) is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of (S1,S2,S3,f1,g1) #), the ResultSort of S1 * the Sorts of (S1,S2,S3,f1,g1)
the carrier' of S1 is set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Sorts of (S1,S2,S3,f1,g1) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of (S1,S2,S3,f1,g1) #) is Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of (S1,S2,S3,f1,g1) is Relation-like the carrier' of S1 -defined Function-like total set
g1 * the Charact of S3 is Relation-like Function-like V53() V54() set
S2 is non empty feasible () ManySortedSign
S1 is non empty feasible () ManySortedSign
S3 is non-empty MSAlgebra over S2
X is Relation-like Function-like set
f1 is Relation-like Function-like set
(S1,S2,S3,X,f1) is strict MSAlgebra over S1
the Sorts of (S1,S2,S3,X,f1) is non empty Relation-like the carrier of S1 -defined Function-like total set
the carrier of S1 is non empty set
the Sorts of S3 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
the carrier of S2 is non empty set
X * the Sorts of S3 is Relation-like non-empty Function-like set
S1 is non empty feasible () ManySortedSign
S2 is non empty feasible () (S1)
S3 is non-empty MSAlgebra over S1
(S1,S2,S3) is strict MSAlgebra over S2
the carrier of S2 is non empty set
id the carrier of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
the carrier' of S2 is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
(S2,S1,S3,(id the carrier of S2),(id the carrier' of S2)) is strict MSAlgebra over S2
S1 is non empty non void feasible () ManySortedSign
S2 is non empty non void feasible () ManySortedSign
the carrier' of S1 is non empty set
the carrier' of S2 is non empty set
S3 is Relation-like Function-like set
X is Relation-like Function-like set
[: the carrier' of S1, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S2:] is set
g1 is MSAlgebra over S2
(S1,S2,g1,S3,X) is strict MSAlgebra over S1
f2 is Element of the carrier' of S1
X . f2 is set
Den (f2,(S1,S2,g1,S3,X)) is Relation-like Args (f2,(S1,S2,g1,S3,X)) -defined Result (f2,(S1,S2,g1,S3,X)) -valued Function-like V29( Args (f2,(S1,S2,g1,S3,X)), Result (f2,(S1,S2,g1,S3,X))) Element of bool [:(Args (f2,(S1,S2,g1,S3,X))),(Result (f2,(S1,S2,g1,S3,X))):]
Args (f2,(S1,S2,g1,S3,X)) is Element of rng ( the Sorts of (S1,S2,g1,S3,X) #)
the carrier of S1 is non empty set
the Sorts of (S1,S2,g1,S3,X) is non empty Relation-like the carrier of S1 -defined Function-like total set
the Sorts of (S1,S2,g1,S3,X) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of (S1,S2,g1,S3,X) #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #)) . f2 is set
Result (f2,(S1,S2,g1,S3,X)) is Element of rng the Sorts of (S1,S2,g1,S3,X)
rng the Sorts of (S1,S2,g1,S3,X) is non empty set
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of (S1,S2,g1,S3,X) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the ResultSort of S1 * the Sorts of (S1,S2,g1,S3,X)) . f2 is set
[:(Args (f2,(S1,S2,g1,S3,X))),(Result (f2,(S1,S2,g1,S3,X))):] is Relation-like set
bool [:(Args (f2,(S1,S2,g1,S3,X))),(Result (f2,(S1,S2,g1,S3,X))):] is set
the Charact of (S1,S2,g1,S3,X) is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #), the ResultSort of S1 * the Sorts of (S1,S2,g1,S3,X)
the Charact of (S1,S2,g1,S3,X) . f2 is Relation-like Function-like set
g2 is Element of the carrier' of S2
Den (g2,g1) is Relation-like Args (g2,g1) -defined Result (g2,g1) -valued Function-like V29( Args (g2,g1), Result (g2,g1)) Element of bool [:(Args (g2,g1)),(Result (g2,g1)):]
Args (g2,g1) is Element of rng ( the Sorts of g1 #)
the carrier of S2 is non empty set
the Sorts of g1 is non empty Relation-like the carrier of S2 -defined Function-like total set
the Sorts of g1 # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
rng ( the Sorts of g1 #) is non empty set
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S2 * ( the Sorts of g1 #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of g1 #)) . g2 is set
Result (g2,g1) is Element of rng the Sorts of g1
rng the Sorts of g1 is non empty set
the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S2 * the Sorts of g1 is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the ResultSort of S2 * the Sorts of g1) . g2 is set
[:(Args (g2,g1)),(Result (g2,g1)):] is Relation-like set
bool [:(Args (g2,g1)),(Result (g2,g1)):] is set
the Charact of g1 is non empty Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of g1 #), the ResultSort of S2 * the Sorts of g1
the Charact of g1 . g2 is Relation-like Function-like set
the Charact of g1 . g2 is Relation-like ( the Arity of S2 * ( the Sorts of g1 #)) . g2 -defined ( the ResultSort of S2 * the Sorts of g1) . g2 -valued Function-like V29(( the Arity of S2 * ( the Sorts of g1 #)) . g2,( the ResultSort of S2 * the Sorts of g1) . g2) Element of bool [:(( the Arity of S2 * ( the Sorts of g1 #)) . g2),(( the ResultSort of S2 * the Sorts of g1) . g2):]
[:(( the Arity of S2 * ( the Sorts of g1 #)) . g2),(( the ResultSort of S2 * the Sorts of g1) . g2):] is Relation-like set
bool [:(( the Arity of S2 * ( the Sorts of g1 #)) . g2),(( the ResultSort of S2 * the Sorts of g1) . g2):] is set
f1 is non empty Relation-like the carrier' of S1 -defined the carrier' of S2 -valued Function-like total V29( the carrier' of S1, the carrier' of S2) Element of bool [: the carrier' of S1, the carrier' of S2:]
f1 * the Charact of g1 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() set
(f1 * the Charact of g1) . f2 is Relation-like Function-like set
the Charact of (S1,S2,g1,S3,X) . f2 is Relation-like ( the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #)) . f2 -defined ( the ResultSort of S1 * the Sorts of (S1,S2,g1,S3,X)) . f2 -valued Function-like V29(( the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #)) . f2,( the ResultSort of S1 * the Sorts of (S1,S2,g1,S3,X)) . f2) Element of bool [:(( the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #)) . f2),(( the ResultSort of S1 * the Sorts of (S1,S2,g1,S3,X)) . f2):]
[:(( the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #)) . f2),(( the ResultSort of S1 * the Sorts of (S1,S2,g1,S3,X)) . f2):] is Relation-like set
bool [:(( the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #)) . f2),(( the ResultSort of S1 * the Sorts of (S1,S2,g1,S3,X)) . f2):] is set
S1 is non empty non void feasible () ManySortedSign
S2 is non empty non void feasible () ManySortedSign
the carrier' of S1 is non empty set
the carrier' of S2 is non empty set
S3 is Relation-like Function-like set
X is Relation-like Function-like set
dom S3 is set
the carrier of S1 is non empty set
f1 is MSAlgebra over S2
(S1,S2,f1,S3,X) is strict MSAlgebra over S1
g1 is Element of the carrier' of S1
X . g1 is set
Args (g1,(S1,S2,f1,S3,X)) is Element of rng ( the Sorts of (S1,S2,f1,S3,X) #)
the Sorts of (S1,S2,f1,S3,X) is non empty Relation-like the carrier of S1 -defined Function-like total set
the Sorts of (S1,S2,f1,S3,X) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of (S1,S2,f1,S3,X) #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of (S1,S2,f1,S3,X) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (S1,S2,f1,S3,X) #)) . g1 is set
Result (g1,(S1,S2,f1,S3,X)) is Element of rng the Sorts of (S1,S2,f1,S3,X)
rng the Sorts of (S1,S2,f1,S3,X) is non empty set
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of (S1,S2,f1,S3,X) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the ResultSort of S1 * the Sorts of (S1,S2,f1,S3,X)) . g1 is set
f2 is Element of the carrier' of S2
Args (f2,f1) is Element of rng ( the Sorts of f1 #)
the carrier of S2 is non empty set
the Sorts of f1 is non empty Relation-like the carrier of S2 -defined Function-like total set
the Sorts of f1 # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
rng ( the Sorts of f1 #) is non empty set
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S2 * ( the Sorts of f1 #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of f1 #)) . f2 is set
Result (f2,f1) is Element of rng the Sorts of f1
rng the Sorts of f1 is non empty set
the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S2 * the Sorts of f1 is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the ResultSort of S2 * the Sorts of f1) . f2 is set
the_arity_of f2 is Relation-like NAT -defined the carrier of S2 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *
the Arity of S2 . f2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *
(the_arity_of f2) * the Sorts of f1 is Relation-like NAT -defined Function-like set
product ((the_arity_of f2) * the Sorts of f1) is set
the_arity_of g1 is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
the Arity of S1 . g1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
(the_arity_of g1) * S3 is Relation-like NAT -defined Function-like set
((the_arity_of g1) * S3) * the Sorts of f1 is Relation-like NAT -defined Function-like set
product (((the_arity_of g1) * S3) * the Sorts of f1) is set
S3 * the Sorts of f1 is Relation-like Function-like set
(the_arity_of g1) * (S3 * the Sorts of f1) is Relation-like NAT -defined Function-like set
product ((the_arity_of g1) * (S3 * the Sorts of f1)) is set
(the_arity_of g1) * the Sorts of (S1,S2,f1,S3,X) is Relation-like NAT -defined Function-like set
product ((the_arity_of g1) * the Sorts of (S1,S2,f1,S3,X)) is set
dom X is set
the_result_sort_of f2 is Element of the carrier of S2
the ResultSort of S2 . f2 is Element of the carrier of S2
X * the ResultSort of S2 is Relation-like the carrier of S2 -valued Function-like set
(X * the ResultSort of S2) . g1 is set
the ResultSort of S1 * S3 is Relation-like the carrier' of S1 -defined Function-like set
( the ResultSort of S1 * S3) . g1 is set
the_result_sort_of g1 is Element of the carrier of S1
the ResultSort of S1 . g1 is Element of the carrier of S1
S3 . (the_result_sort_of g1) is set
the Sorts of f1 . (S3 . (the_result_sort_of g1)) is set
(S3 * the Sorts of f1) . (the_result_sort_of g1) is set
the Sorts of (S1,S2,f1,S3,X) . (the_result_sort_of g1) is set
S1 is non empty feasible () ManySortedSign
the carrier of S1 is non empty set
id the carrier of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total V29( the carrier of S1, the carrier of S1) Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is set
the carrier' of S1 is set
id the carrier' of S1 is Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total V29( the carrier' of S1, the carrier' of S1) Element of bool [: the carrier' of S1, the carrier' of S1:]
[: the carrier' of S1, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is set
S2 is MSAlgebra over S1
(S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) is strict MSAlgebra over S1
the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of S2 is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S2 #), the ResultSort of S1 * the Sorts of S2
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Sorts of S2 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of S2 #) is Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of S2 is Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of S2, the Charact of S2 #) is strict MSAlgebra over S1
dom the Charact of S2 is set
the Charact of MSAlgebra(# the Sorts of S2, the Charact of S2 #) is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of MSAlgebra(# the Sorts of S2, the Charact of S2 #) #), the ResultSort of S1 * the Sorts of MSAlgebra(# the Sorts of S2, the Charact of S2 #)
the Sorts of MSAlgebra(# the Sorts of S2, the Charact of S2 #) is non empty Relation-like the carrier of S1 -defined Function-like total set
the Sorts of MSAlgebra(# the Sorts of S2, the Charact of S2 #) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of MSAlgebra(# the Sorts of S2, the Charact of S2 #) #) is Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 * the Sorts of MSAlgebra(# the Sorts of S2, the Charact of S2 #) is Relation-like the carrier' of S1 -defined Function-like total set
(id the carrier' of S1) * the Charact of S2 is Relation-like the carrier' of S1 -defined Function-like V53() V54() set
dom the Sorts of S2 is non empty set
(id the carrier of S1) * the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set
S1 is non empty feasible () ManySortedSign
S2 is MSAlgebra over S1
(S1,S1,S2) is strict MSAlgebra over S1
the carrier of S1 is non empty set
id the carrier of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total V29( the carrier of S1, the carrier of S1) Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is set
the carrier' of S1 is set
id the carrier' of S1 is Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total V29( the carrier' of S1, the carrier' of S1) Element of bool [: the carrier' of S1, the carrier' of S1:]
[: the carrier' of S1, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is set
(S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) is strict MSAlgebra over S1
the Sorts of S2 is non empty Relation-like the carrier of S1 -defined Function-like total set
the Charact of S2 is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S2 #), the ResultSort of S1 * the Sorts of S2
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Sorts of S2 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of S2 #) is Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of S2 is Relation-like the carrier' of S1 -defined Function-like total set
MSAlgebra(# the Sorts of S2, the Charact of S2 #) is strict MSAlgebra over S1
S1 is non empty feasible () ManySortedSign
S2 is non empty feasible () ManySortedSign
S3 is non empty feasible () ManySortedSign
X is Relation-like Function-like set
f1 is Relation-like Function-like set
g1 is Relation-like Function-like set
f2 is Relation-like Function-like set
X * g1 is Relation-like Function-like set
f1 * f2 is Relation-like Function-like set
g2 is MSAlgebra over S3
(S1,S3,g2,(X * g1),(f1 * f2)) is strict MSAlgebra over S1
(S2,S3,g2,g1,f2) is strict MSAlgebra over S2
(S1,S2,(S2,S3,g2,g1,f2),X,f1) is strict MSAlgebra over S1
the Charact of (S1,S2,(S2,S3,g2,g1,f2),X,f1) is Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of (S1,S2,(S2,S3,g2,g1,f2),X,f1) #), the ResultSort of S1 * the Sorts of (S1,S2,(S2,S3,g2,g1,f2),X,f1)
the carrier' of S1 is set
the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 is non empty set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Sorts of (S1,S2,(S2,S3,g2,g1,f2),X,f1) is non empty Relation-like the carrier of S1 -defined Function-like total set
the Sorts of (S1,S2,(S2,S3,g2,g1,f2),X,f1) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ( the Sorts of (S1,S2,(S2,S3,g2,g1,f2),X,f1) #) is Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * the Sorts of (S1,S2,(S2,S3,g2,g1,f2),X,f1) is Relation-like the carrier' of S1 -defined Function-like total set
the Charact of (S2,S3,g2,g1,f2) is Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of (S2,S3,g2,g1,f2) #), the ResultSort of S2 * the Sorts of (S2,S3,g2,g1,f2)
the carrier' of S2 is set
the Arity of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier of S2 is non empty set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Sorts of (S2,S3,g2,g1,f2) is non empty Relation-like the carrier of S2 -defined Function-like total set
the Sorts of (S2,S3,g2,g1,f2) # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the Arity of S2 * ( the Sorts of (S2,S3,g2,g1,f2) #) is Relation-like the carrier' of S2 -defined Function-like total set
the ResultSort of S2 is Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S2 * the Sorts of (S2,S3,g2,g1,f2) is Relation-like the carrier' of S2 -defined Function-like total set
f1 * the Charact of (S2,S3,g2,g1,f2) is Relation-like Function-like V53() V54() set
the Charact of g2 is Relation-like the carrier' of S3 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S3 * ( the Sorts of g2 #), the ResultSort of S3 * the Sorts of g2
the carrier' of S3 is set
the Arity of S3 is Relation-like the carrier' of S3 -defined the carrier of S3 * -valued Function-like total V29( the carrier' of S3, the carrier of S3 * ) V53() V54() Element of bool [: the carrier' of S3,( the carrier of S3 *):]
the carrier of S3 is non empty set
the carrier of S3 * is non empty functional FinSequence-membered M12( the carrier of S3)
[: the carrier' of S3,( the carrier of S3 *):] is Relation-like set
bool [: the carrier' of S3,( the carrier of S3 *):] is set
the Sorts of g2 is non empty Relation-like the carrier of S3 -defined Function-like total set
the Sorts of g2 # is non empty Relation-like the carrier of S3 * -defined Function-like total set
the Arity of S3 * ( the Sorts of g2 #) is Relation-like the carrier' of S3 -defined Function-like total set
the ResultSort of S3 is Relation-like the carrier' of S3 -defined the carrier of S3 -valued Function-like total V29( the carrier' of S3, the carrier of S3) Element of bool [: the carrier' of S3, the carrier of S3:]
[: the carrier' of S3, the carrier of S3:] is Relation-like set
bool [: the carrier' of S3, the carrier of S3:] is set
the ResultSort of S3 * the Sorts of g2 is Relation-like the carrier' of S3 -defined Function-like total set
f2 * the Charact of g2 is Relation-like Function-like V53() V54() set
f1 * (f2 * the Charact of g2) is Relation-like Function-like V53() V54() set
(f1 * f2) * the Charact of g2 is Relation-like Function-like V53() V54() set
X * the Sorts of (S2,S3,g2,g1,f2) is Relation-like Function-like set
g1 * the Sorts of g2 is Relation-like Function-like set
X * (g1 * the Sorts of g2) is Relation-like Function-like set
(X * g1) * the Sorts of g2 is Relation-like Function-like set
S1 is non empty feasible () ManySortedSign
S2 is non empty feasible () (S1)
S3 is non empty feasible () (S2)
X is MSAlgebra over S1
(S1,S3,X) is strict MSAlgebra over S3
the carrier of S3 is non empty set
id the carrier of S3 is non empty Relation-like the carrier of S3 -defined the carrier of S3 -valued Function-like one-to-one total V29( the carrier of S3, the carrier of S3) Element of bool [: the carrier of S3, the carrier of S3:]
[: the carrier of S3, the carrier of S3:] is Relation-like set
bool [: the carrier of S3, the carrier of S3:] is set
the carrier' of S3 is set
id the carrier' of S3 is Relation-like the carrier' of S3 -defined the carrier' of S3 -valued Function-like one-to-one total V29( the carrier' of S3, the carrier' of S3) Element of bool [: the carrier' of S3, the carrier' of S3:]
[: the carrier' of S3, the carrier' of S3:] is Relation-like set
bool [: the carrier' of S3, the carrier' of S3:] is set
(S3,S1,X,(id the carrier of S3),(id the carrier' of S3)) is strict MSAlgebra over S3
(S1,S2,X) is strict MSAlgebra over S2
the carrier of S2 is non empty set
id the carrier of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
the carrier' of S2 is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
(S2,S1,X,(id the carrier of S2),(id the carrier' of S2)) is strict MSAlgebra over S2
(S2,S3,(S1,S2,X)) is strict MSAlgebra over S3
(S3,S2,(S1,S2,X),(id the carrier of S3),(id the carrier' of S3)) is strict MSAlgebra over S3
rng (id the carrier of S3) is non empty set
(id the carrier of S2) * (id the carrier of S3) is Relation-like the carrier of S3 -defined the carrier of S2 -valued Function-like one-to-one Element of bool [: the carrier of S3, the carrier of S2:]
[: the carrier of S3, the carrier of S2:] is Relation-like set
bool [: the carrier of S3, the carrier of S2:] is set
rng (id the carrier' of S3) is set
(id the carrier' of S2) * (id the carrier' of S3) is Relation-like the carrier' of S3 -defined the carrier' of S2 -valued Function-like one-to-one Element of bool [: the carrier' of S3, the carrier' of S2:]
[: the carrier' of S3, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S3, the carrier' of S2:] is set
S1 is non empty feasible () ManySortedSign
the carrier of S1 is non empty set
S2 is non empty feasible () ManySortedSign
the carrier of S2 is non empty set
[: the carrier of S1, the carrier of S2:] is Relation-like set
bool [: the carrier of S1, the carrier of S2:] is set
S3 is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier of S1, the carrier of S2) Element of bool [: the carrier of S1, the carrier of S2:]
X is Relation-like Function-like set
f1 is MSAlgebra over S2
the Sorts of f1 is non empty Relation-like the carrier of S2 -defined Function-like total set
g1 is MSAlgebra over S2
the Sorts of g1 is non empty Relation-like the carrier of S2 -defined Function-like total set
(S1,S2,f1,S3,X) is strict MSAlgebra over S1
the Sorts of (S1,S2,f1,S3,X) is non empty Relation-like the carrier of S1 -defined Function-like total set
(S1,S2,g1,S3,X) is strict MSAlgebra over S1
the Sorts of (S1,S2,g1,S3,X) is non empty Relation-like the carrier of S1 -defined Function-like total set
f2 is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of f1, the Sorts of g1
S3 * f2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() set
g is set
(S3 * f2) . g is Relation-like Function-like set
the Sorts of (S1,S2,f1,S3,X) . g is set
the Sorts of (S1,S2,g1,S3,X) . g is set
[:( the Sorts of (S1,S2,f1,S3,X) . g),( the Sorts of (S1,S2,g1,S3,X) . g):] is Relation-like set
bool [:( the Sorts of (S1,S2,f1,S3,X) . g),( the Sorts of (S1,S2,g1,S3,X) . g):] is set
Af is Element of the carrier of S1
S3 . Af is Element of the carrier of S2
(S3 * f2) . Af is Relation-like Function-like set
Af1 is Element of the carrier of S2
f2 . Af1 is Relation-like the Sorts of f1 . Af1 -defined the Sorts of g1 . Af1 -valued Function-like V29( the Sorts of f1 . Af1, the Sorts of g1 . Af1) Element of bool [:( the Sorts of f1 . Af1),( the Sorts of g1 . Af1):]
the Sorts of f1 . Af1 is set
the Sorts of g1 . Af1 is set
[:( the Sorts of f1 . Af1),( the Sorts of g1 . Af1):] is Relation-like set
bool [:( the Sorts of f1 . Af1),( the Sorts of g1 . Af1):] is set
S3 * the Sorts of f1 is non empty Relation-like the carrier of S1 -defined Function-like total set
(S3 * the Sorts of f1) . Af is set
S3 * the Sorts of g1 is non empty Relation-like the carrier of S1 -defined Function-like total set
(S3 * the Sorts of g1) . Af is set
S1 is non empty feasible () ManySortedSign
the carrier of S1 is non empty set
S2 is non empty feasible () (S1)
the carrier of S2 is non empty set
id the carrier of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
the carrier' of S2 is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
f1 is MSAlgebra over S1
the Sorts of f1 is non empty Relation-like the carrier of S1 -defined Function-like total set
g1 is MSAlgebra over S1
the Sorts of g1 is non empty Relation-like the carrier of S1 -defined Function-like total set
(S1,S2,f1) is strict MSAlgebra over S2
(S2,S1,f1,(id the carrier of S2),(id the carrier' of S2)) is strict MSAlgebra over S2
the Sorts of (S1,S2,f1) is non empty Relation-like the carrier of S2 -defined Function-like total set
(S1,S2,g1) is strict MSAlgebra over S2
(S2,S1,g1,(id the carrier of S2),(id the carrier' of S2)) is strict MSAlgebra over S2
the Sorts of (S1,S2,g1) is non empty Relation-like the carrier of S2 -defined Function-like total set
f2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of f1, the Sorts of g1
f2 | the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S1 -defined Function-like V53() V54() set
[: the carrier of S2, the carrier of S1:] is Relation-like set
bool [: the carrier of S2, the carrier of S1:] is set
g2 is non empty Relation-like the carrier of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier of S2, the carrier of S1) Element of bool [: the carrier of S2, the carrier of S1:]
g2 * f2 is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() set
(S2,S1,f1,g2,(id the carrier' of S2)) is strict MSAlgebra over S2
the Sorts of (S2,S1,f1,g2,(id the carrier' of S2)) is non empty Relation-like the carrier of S2 -defined Function-like total set
(S2,S1,g1,g2,(id the carrier' of S2)) is strict MSAlgebra over S2
the Sorts of (S2,S1,g1,g2,(id the carrier' of S2)) is non empty Relation-like the carrier of S2 -defined Function-like total set
S1 is non empty feasible () ManySortedSign
S2 is non empty feasible () ManySortedSign
the carrier of S2 is non empty set
the carrier of S1 is non empty set
S3 is Relation-like Function-like set
X is Relation-like Function-like set
dom S3 is set
rng S3 is set
[: the carrier of S1, the carrier of S2:] is Relation-like set
bool [: the carrier of S1, the carrier of S2:] is set
g1 is MSAlgebra over S2
the Sorts of g1 is non empty Relation-like the carrier of S2 -defined Function-like total set
id the Sorts of g1 is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of g1, the Sorts of g1
S3 * (id the Sorts of g1) is Relation-like Function-like V53() V54() set
(S1,S2,g1,S3,X) is strict MSAlgebra over S1
the Sorts of (S1,S2,g1,S3,X) is non empty Relation-like the carrier of S1 -defined Function-like total set
id the Sorts of (S1,S2,g1,S3,X) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (S1,S2,g1,S3,X), the Sorts of (S1,S2,g1,S3,X)
f2 is set
f1 is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier of S1, the carrier of S2) Element of bool [: the carrier of S1, the carrier of S2:]
f1 * (id the Sorts of g1) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() set
(f1 * (id the Sorts of g1)) . f2 is Relation-like Function-like set
g2 is Element of the carrier of S1
f1 . g2 is Element of the carrier of S2
(id the Sorts of g1) . (f1 . g2) is Relation-like the Sorts of g1 . (f1 . g2) -defined the Sorts of g1 . (f1 . g2) -valued Function-like total V29( the Sorts of g1 . (f1 . g2), the Sorts of g1 . (f1 . g2)) Element of bool [:( the Sorts of g1 . (f1 . g2)),( the Sorts of g1 . (f1 . g2)):]
the Sorts of g1 . (f1 . g2) is set
[:( the Sorts of g1 . (f1 . g2)),( the Sorts of g1 . (f1 . g2)):] is Relation-like set
bool [:( the Sorts of g1 . (f1 . g2)),( the Sorts of g1 . (f1 . g2)):] is set
id ( the Sorts of g1 . (f1 . g2)) is Relation-like the Sorts of g1 . (f1 . g2) -defined the Sorts of g1 . (f1 . g2) -valued Function-like one-to-one total V29( the Sorts of g1 . (f1 . g2), the Sorts of g1 . (f1 . g2)) Element of bool [:( the Sorts of g1 . (f1 . g2)),( the Sorts of g1 . (f1 . g2)):]
f1 * the Sorts of g1 is non empty Relation-like the carrier of S1 -defined Function-like total set
(f1 * the Sorts of g1) . g2 is set
id ((f1 * the Sorts of g1) . g2) is Relation-like (f1 * the Sorts of g1) . g2 -defined (f1 * the Sorts of g1) . g2 -valued Function-like one-to-one total V29((f1 * the Sorts of g1) . g2,(f1 * the Sorts of g1) . g2) Element of bool [:((f1 * the Sorts of g1) . g2),((f1 * the Sorts of g1) . g2):]
[:((f1 * the Sorts of g1) . g2),((f1 * the Sorts of g1) . g2):] is Relation-like set
bool [:((f1 * the Sorts of g1) . g2),((f1 * the Sorts of g1) . g2):] is set
(S1,S2,g1,f1,X) is strict MSAlgebra over S1
the Sorts of (S1,S2,g1,f1,X) is non empty Relation-like the carrier of S1 -defined Function-like total set
the Sorts of (S1,S2,g1,f1,X) . g2 is set
id ( the Sorts of (S1,S2,g1,f1,X) . g2) is Relation-like the Sorts of (S1,S2,g1,f1,X) . g2 -defined the Sorts of (S1,S2,g1,f1,X) . g2 -valued Function-like one-to-one total V29( the Sorts of (S1,S2,g1,f1,X) . g2, the Sorts of (S1,S2,g1,f1,X) . g2) Element of bool [:( the Sorts of (S1,S2,g1,f1,X) . g2),( the Sorts of (S1,S2,g1,f1,X) . g2):]
[:( the Sorts of (S1,S2,g1,f1,X) . g2),( the Sorts of (S1,S2,g1,f1,X) . g2):] is Relation-like set
bool [:( the Sorts of (S1,S2,g1,f1,X) . g2),( the Sorts of (S1,S2,g1,f1,X) . g2):] is set
id the Sorts of (S1,S2,g1,f1,X) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (S1,S2,g1,f1,X), the Sorts of (S1,S2,g1,f1,X)
(id the Sorts of (S1,S2,g1,f1,X)) . f2 is Relation-like Function-like set
S1 is non empty feasible () ManySortedSign
the carrier of S1 is non empty set
S2 is non empty feasible () (S1)
the carrier of S2 is non empty set
id the carrier of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
the carrier' of S2 is set
id the carrier' of S2 is Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
f1 is MSAlgebra over S1
the Sorts of f1 is non empty Relation-like the carrier of S1 -defined Function-like total set
id the Sorts of f1 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of f1, the Sorts of f1
(id the Sorts of f1) | the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S1 -defined Function-like V53() V54() set
(S1,S2,f1) is strict MSAlgebra over S2
(S2,S1,f1,(id the carrier of S2),(id the carrier' of S2)) is strict MSAlgebra over S2
the Sorts of (S1,S2,f1) is non empty Relation-like the carrier of S2 -defined Function-like total set
id the Sorts of (S1,S2,f1) is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (S1,S2,f1), the Sorts of (S1,S2,f1)
(id the carrier of S2) * (id the Sorts of f1) is Relation-like the carrier of S2 -defined Function-like V53() V54() set
S1 is non empty non void feasible () ManySortedSign
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
the carrier of S1 is non empty set
the carrier' of S1 is non empty set
the carrier' of S2 is non empty set
S3 is Relation-like Function-like set
X is Relation-like Function-like set
f1 is MSAlgebra over S2
the Sorts of f1 is non empty Relation-like the carrier of S2 -defined Function-like total set
g1 is MSAlgebra over S2
the Sorts of g1 is non empty Relation-like the carrier of S2 -defined Function-like total set
(S1,S2,f1,S3,X) is strict MSAlgebra over S1
the Sorts of (S1,S2,f1,S3,X) is non empty Relation-like the carrier of S1 -defined Function-like total set
(S1,S2,g1,S3,X) is strict MSAlgebra over S1
the Sorts of (S1,S2,g1,S3,X) is non empty Relation-like the carrier of S1 -defined Function-like total set
f is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of f1, the Sorts of g1
S3 * f is Relation-like Function-like V53() V54() set
g is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (S1,S2,f1,S3,X), the Sorts of (S1,S2,g1,S3,X)
Af is Element of the carrier' of S1
X . Af is set
Args (Af,(S1,S2,f1,S3,X)) is Element of rng ( the Sorts of (S1,S2,f1,S3,X) #)
the Sorts of (S1,S2,f1,S3,X) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of (S1,S2,f1,S3,X) #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of (S1,S2,f1,S3,X) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (S1,S2,f1,S3,X) #)) . Af is set
Af1 is Element of the carrier' of S2
Args (Af1,f1) is Element of rng ( the Sorts of f1 #)
the Sorts of f1 # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
rng ( the Sorts of f1 #) is non empty set
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S2 * ( the Sorts of f1 #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of f1 #)) . Af1 is set
Args (Af1,g1) is Element of rng ( the Sorts of g1 #)
the Sorts of g1 # is non empty Relation-like the carrier of S2 * -defined Function-like total set
rng ( the Sorts of g1 #) is non empty set
the Arity of S2 * ( the Sorts of g1 #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of g1 #)) . Af1 is set
hf1 is Element of Args (Af1,f1)
f # hf1 is Element of Args (Af1,g1)
hh is Element of Args (Af,(S1,S2,f1,S3,X))
g # hh is Element of Args (Af,(S1,S2,g1,S3,X))
Args (Af,(S1,S2,g1,S3,X)) is Element of rng ( the Sorts of (S1,S2,g1,S3,X) #)
the Sorts of (S1,S2,g1,S3,X) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
rng ( the Sorts of (S1,S2,g1,S3,X) #) is non empty set
the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (S1,S2,g1,S3,X) #)) . Af is set
hf1h is Relation-like Function-like set
dom hf1h is set
the_arity_of Af is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
the Arity of S1 . Af is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
dom (the_arity_of Af) is Element of bool NAT
s is Relation-like Function-like set
dom s is set
the_arity_of Af1 is Relation-like NAT -defined the carrier of S2 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *
the Arity of S2 . Af1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *
dom (the_arity_of Af1) is Element of bool NAT
t is V10() set
dom S3 is set
(the_arity_of Af) /. t is Element of the carrier of S1
g . ((the_arity_of Af) /. t) is Relation-like the Sorts of (S1,S2,f1,S3,X) . ((the_arity_of Af) /. t) -defined the Sorts of (S1,S2,g1,S3,X) . ((the_arity_of Af) /. t) -valued Function-like V29( the Sorts of (S1,S2,f1,S3,X) . ((the_arity_of Af) /. t), the Sorts of (S1,S2,g1,S3,X) . ((the_arity_of Af) /. t)) Element of bool [:( the Sorts of (S1,S2,f1,S3,X) . ((the_arity_of Af) /. t)),( the Sorts of (S1,S2,g1,S3,X) . ((the_arity_of Af) /. t)):]
the Sorts of (S1,S2,f1,S3,X) . ((the_arity_of Af) /. t) is set
the Sorts of (S1,S2,g1,S3,X) . ((the_arity_of Af) /. t) is set
[:( the Sorts of (S1,S2,f1,S3,X) . ((the_arity_of Af) /. t)),( the Sorts of (S1,S2,g1,S3,X) . ((the_arity_of Af) /. t)):] is Relation-like set
bool [:( the Sorts of (S1,S2,f1,S3,X) . ((the_arity_of Af) /. t)),( the Sorts of (S1,S2,g1,S3,X) . ((the_arity_of Af) /. t)):] is set
S3 . ((the_arity_of Af) /. t) is set
f . (S3 . ((the_arity_of Af) /. t)) is Relation-like Function-like set
(the_arity_of Af) . t is set
S3 . ((the_arity_of Af) . t) is set
f . (S3 . ((the_arity_of Af) . t)) is Relation-like Function-like set
(the_arity_of Af) * S3 is Relation-like NAT -defined Function-like set
((the_arity_of Af) * S3) . t is set
f . (((the_arity_of Af) * S3) . t) is Relation-like Function-like set
(the_arity_of Af1) . t is set
f . ((the_arity_of Af1) . t) is Relation-like Function-like set
(the_arity_of Af1) /. t is Element of the carrier of S2
f . ((the_arity_of Af1) /. t) is Relation-like the Sorts of f1 . ((the_arity_of Af1) /. t) -defined the Sorts of g1 . ((the_arity_of Af1) /. t) -valued Function-like V29( the Sorts of f1 . ((the_arity_of Af1) /. t), the Sorts of g1 . ((the_arity_of Af1) /. t)) Element of bool [:( the Sorts of f1 . ((the_arity_of Af1) /. t)),( the Sorts of g1 . ((the_arity_of Af1) /. t)):]
the Sorts of f1 . ((the_arity_of Af1) /. t) is set
the Sorts of g1 . ((the_arity_of Af1) /. t) is set
[:( the Sorts of f1 . ((the_arity_of Af1) /. t)),( the Sorts of g1 . ((the_arity_of Af1) /. t)):] is Relation-like set
bool [:( the Sorts of f1 . ((the_arity_of Af1) /. t)),( the Sorts of g1 . ((the_arity_of Af1) /. t)):] is set
x is Relation-like Function-like set
x . t is set
hf1h . t is set
(g . ((the_arity_of Af) /. t)) . (hf1h . t) is set
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
[: the carrier of S2, the carrier of S1:] is Relation-like set
bool [: the carrier of S2, the carrier of S1:] is set
S3 is MSAlgebra over S1
the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set
X is MSAlgebra over S1
the Sorts of X is non empty Relation-like the carrier of S1 -defined Function-like total set
f1 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of S3, the Sorts of X
g1 is non empty Relation-like the carrier of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier of S2, the carrier of S1) Element of bool [: the carrier of S2, the carrier of S1:]
g1 * f1 is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() set
f2 is Relation-like Function-like set
(S2,S1,S3,g1,f2) is strict MSAlgebra over S2
the Sorts of (S2,S1,S3,g1,f2) is non empty Relation-like the carrier of S2 -defined Function-like total set
(S2,S1,X,g1,f2) is strict MSAlgebra over S2
the Sorts of (S2,S1,X,g1,f2) is non empty Relation-like the carrier of S2 -defined Function-like total set
dom f2 is set
the carrier' of S2 is non empty set
rng f2 is set
the carrier' of S1 is non empty set
[: the carrier' of S2, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S1:] is set
the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
g1 * the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S2, the carrier of S1) Element of bool [: the carrier' of S2, the carrier of S1:]
[: the carrier' of S2, the carrier of S1:] is Relation-like set
bool [: the carrier' of S2, the carrier of S1:] is set
g is non empty Relation-like the carrier' of S2 -defined the carrier' of S1 -valued Function-like total V29( the carrier' of S2, the carrier' of S1) Element of bool [: the carrier' of S2, the carrier' of S1:]
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * g is non empty Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S2, the carrier of S1) Element of bool [: the carrier' of S2, the carrier of S1:]
Af is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (S2,S1,S3,g1,f2), the Sorts of (S2,S1,X,g1,f2)
Af1 is Element of the carrier' of S2
Args (Af1,(S2,S1,S3,g1,f2)) is Element of rng ( the Sorts of (S2,S1,S3,g1,f2) #)
the Sorts of (S2,S1,S3,g1,f2) # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
rng ( the Sorts of (S2,S1,S3,g1,f2) #) is non empty set
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S2 * ( the Sorts of (S2,S1,S3,g1,f2) #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of (S2,S1,S3,g1,f2) #)) . Af1 is set
the_result_sort_of Af1 is Element of the carrier of S2
the ResultSort of S2 . Af1 is Element of the carrier of S2
Af . (the_result_sort_of Af1) is Relation-like the Sorts of (S2,S1,S3,g1,f2) . (the_result_sort_of Af1) -defined the Sorts of (S2,S1,X,g1,f2) . (the_result_sort_of Af1) -valued Function-like V29( the Sorts of (S2,S1,S3,g1,f2) . (the_result_sort_of Af1), the Sorts of (S2,S1,X,g1,f2) . (the_result_sort_of Af1)) Element of bool [:( the Sorts of (S2,S1,S3,g1,f2) . (the_result_sort_of Af1)),( the Sorts of (S2,S1,X,g1,f2) . (the_result_sort_of Af1)):]
the Sorts of (S2,S1,S3,g1,f2) . (the_result_sort_of Af1) is set
the Sorts of (S2,S1,X,g1,f2) . (the_result_sort_of Af1) is set
[:( the Sorts of (S2,S1,S3,g1,f2) . (the_result_sort_of Af1)),( the Sorts of (S2,S1,X,g1,f2) . (the_result_sort_of Af1)):] is Relation-like set
bool [:( the Sorts of (S2,S1,S3,g1,f2) . (the_result_sort_of Af1)),( the Sorts of (S2,S1,X,g1,f2) . (the_result_sort_of Af1)):] is set
Den (Af1,(S2,S1,S3,g1,f2)) is Relation-like Args (Af1,(S2,S1,S3,g1,f2)) -defined Result (Af1,(S2,S1,S3,g1,f2)) -valued Function-like V29( Args (Af1,(S2,S1,S3,g1,f2)), Result (Af1,(S2,S1,S3,g1,f2))) Element of bool [:(Args (Af1,(S2,S1,S3,g1,f2))),(Result (Af1,(S2,S1,S3,g1,f2))):]
Result (Af1,(S2,S1,S3,g1,f2)) is Element of rng the Sorts of (S2,S1,S3,g1,f2)
rng the Sorts of (S2,S1,S3,g1,f2) is non empty set
the ResultSort of S2 * the Sorts of (S2,S1,S3,g1,f2) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the ResultSort of S2 * the Sorts of (S2,S1,S3,g1,f2)) . Af1 is set
[:(Args (Af1,(S2,S1,S3,g1,f2))),(Result (Af1,(S2,S1,S3,g1,f2))):] is Relation-like set
bool [:(Args (Af1,(S2,S1,S3,g1,f2))),(Result (Af1,(S2,S1,S3,g1,f2))):] is set
the Charact of (S2,S1,S3,g1,f2) is non empty Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of (S2,S1,S3,g1,f2) #), the ResultSort of S2 * the Sorts of (S2,S1,S3,g1,f2)
the Charact of (S2,S1,S3,g1,f2) . Af1 is Relation-like Function-like set
Den (Af1,(S2,S1,X,g1,f2)) is Relation-like Args (Af1,(S2,S1,X,g1,f2)) -defined Result (Af1,(S2,S1,X,g1,f2)) -valued Function-like V29( Args (Af1,(S2,S1,X,g1,f2)), Result (Af1,(S2,S1,X,g1,f2))) Element of bool [:(Args (Af1,(S2,S1,X,g1,f2))),(Result (Af1,(S2,S1,X,g1,f2))):]
Args (Af1,(S2,S1,X,g1,f2)) is Element of rng ( the Sorts of (S2,S1,X,g1,f2) #)
the Sorts of (S2,S1,X,g1,f2) # is non empty Relation-like the carrier of S2 * -defined Function-like total set
rng ( the Sorts of (S2,S1,X,g1,f2) #) is non empty set
the Arity of S2 * ( the Sorts of (S2,S1,X,g1,f2) #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of (S2,S1,X,g1,f2) #)) . Af1 is set
Result (Af1,(S2,S1,X,g1,f2)) is Element of rng the Sorts of (S2,S1,X,g1,f2)
rng the Sorts of (S2,S1,X,g1,f2) is non empty set
the ResultSort of S2 * the Sorts of (S2,S1,X,g1,f2) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the ResultSort of S2 * the Sorts of (S2,S1,X,g1,f2)) . Af1 is set
[:(Args (Af1,(S2,S1,X,g1,f2))),(Result (Af1,(S2,S1,X,g1,f2))):] is Relation-like set
bool [:(Args (Af1,(S2,S1,X,g1,f2))),(Result (Af1,(S2,S1,X,g1,f2))):] is set
the Charact of (S2,S1,X,g1,f2) is non empty Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of (S2,S1,X,g1,f2) #), the ResultSort of S2 * the Sorts of (S2,S1,X,g1,f2)
the Charact of (S2,S1,X,g1,f2) . Af1 is Relation-like Function-like set
g . Af1 is Element of the carrier' of S1
hh is Element of Args (Af1,(S2,S1,S3,g1,f2))
(Den (Af1,(S2,S1,S3,g1,f2))) . hh is set
(Af . (the_result_sort_of Af1)) . ((Den (Af1,(S2,S1,S3,g1,f2))) . hh) is set
Af # hh is Element of Args (Af1,(S2,S1,X,g1,f2))
(Den (Af1,(S2,S1,X,g1,f2))) . (Af # hh) is set
Args ((g . Af1),S3) is Element of rng ( the Sorts of S3 #)
the Sorts of S3 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of S3 #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of S3 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of S3 #)) . (g . Af1) is set
g1 . (the_result_sort_of Af1) is Element of the carrier of S1
f1 . (g1 . (the_result_sort_of Af1)) is Relation-like the Sorts of S3 . (g1 . (the_result_sort_of Af1)) -defined the Sorts of X . (g1 . (the_result_sort_of Af1)) -valued Function-like V29( the Sorts of S3 . (g1 . (the_result_sort_of Af1)), the Sorts of X . (g1 . (the_result_sort_of Af1))) Element of bool [:( the Sorts of S3 . (g1 . (the_result_sort_of Af1))),( the Sorts of X . (g1 . (the_result_sort_of Af1))):]
the Sorts of S3 . (g1 . (the_result_sort_of Af1)) is set
the Sorts of X . (g1 . (the_result_sort_of Af1)) is set
[:( the Sorts of S3 . (g1 . (the_result_sort_of Af1))),( the Sorts of X . (g1 . (the_result_sort_of Af1))):] is Relation-like set
bool [:( the Sorts of S3 . (g1 . (the_result_sort_of Af1))),( the Sorts of X . (g1 . (the_result_sort_of Af1))):] is set
( the ResultSort of S1 * g) . Af1 is Element of the carrier of S1
f1 . (( the ResultSort of S1 * g) . Af1) is Relation-like the Sorts of S3 . (( the ResultSort of S1 * g) . Af1) -defined the Sorts of X . (( the ResultSort of S1 * g) . Af1) -valued Function-like V29( the Sorts of S3 . (( the ResultSort of S1 * g) . Af1), the Sorts of X . (( the ResultSort of S1 * g) . Af1)) Element of bool [:( the Sorts of S3 . (( the ResultSort of S1 * g) . Af1)),( the Sorts of X . (( the ResultSort of S1 * g) . Af1)):]
the Sorts of S3 . (( the ResultSort of S1 * g) . Af1) is set
the Sorts of X . (( the ResultSort of S1 * g) . Af1) is set
[:( the Sorts of S3 . (( the ResultSort of S1 * g) . Af1)),( the Sorts of X . (( the ResultSort of S1 * g) . Af1)):] is Relation-like set
bool [:( the Sorts of S3 . (( the ResultSort of S1 * g) . Af1)),( the Sorts of X . (( the ResultSort of S1 * g) . Af1)):] is set
the_result_sort_of (g . Af1) is Element of the carrier of S1
the ResultSort of S1 . (g . Af1) is Element of the carrier of S1
f1 . (the_result_sort_of (g . Af1)) is Relation-like the Sorts of S3 . (the_result_sort_of (g . Af1)) -defined the Sorts of X . (the_result_sort_of (g . Af1)) -valued Function-like V29( the Sorts of S3 . (the_result_sort_of (g . Af1)), the Sorts of X . (the_result_sort_of (g . Af1))) Element of bool [:( the Sorts of S3 . (the_result_sort_of (g . Af1))),( the Sorts of X . (the_result_sort_of (g . Af1))):]
the Sorts of S3 . (the_result_sort_of (g . Af1)) is set
the Sorts of X . (the_result_sort_of (g . Af1)) is set
[:( the Sorts of S3 . (the_result_sort_of (g . Af1))),( the Sorts of X . (the_result_sort_of (g . Af1))):] is Relation-like set
bool [:( the Sorts of S3 . (the_result_sort_of (g . Af1))),( the Sorts of X . (the_result_sort_of (g . Af1))):] is set
Den ((g . Af1),S3) is Relation-like Args ((g . Af1),S3) -defined Result ((g . Af1),S3) -valued Function-like V29( Args ((g . Af1),S3), Result ((g . Af1),S3)) Element of bool [:(Args ((g . Af1),S3)),(Result ((g . Af1),S3)):]
Result ((g . Af1),S3) is Element of rng the Sorts of S3
rng the Sorts of S3 is non empty set
the ResultSort of S1 * the Sorts of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the ResultSort of S1 * the Sorts of S3) . (g . Af1) is set
[:(Args ((g . Af1),S3)),(Result ((g . Af1),S3)):] is Relation-like set
bool [:(Args ((g . Af1),S3)),(Result ((g . Af1),S3)):] is set
the Charact of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S3 #), the ResultSort of S1 * the Sorts of S3
the Charact of S3 . (g . Af1) is Relation-like Function-like set
Den ((g . Af1),X) is Relation-like Args ((g . Af1),X) -defined Result ((g . Af1),X) -valued Function-like V29( Args ((g . Af1),X), Result ((g . Af1),X)) Element of bool [:(Args ((g . Af1),X)),(Result ((g . Af1),X)):]
Args ((g . Af1),X) is Element of rng ( the Sorts of X #)
the Sorts of X # is non empty Relation-like the carrier of S1 * -defined Function-like total set
rng ( the Sorts of X #) is non empty set
the Arity of S1 * ( the Sorts of X #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of X #)) . (g . Af1) is set
Result ((g . Af1),X) is Element of rng the Sorts of X
rng the Sorts of X is non empty set
the ResultSort of S1 * the Sorts of X is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the ResultSort of S1 * the Sorts of X) . (g . Af1) is set
[:(Args ((g . Af1),X)),(Result ((g . Af1),X)):] is Relation-like set
bool [:(Args ((g . Af1),X)),(Result ((g . Af1),X)):] is set
the Charact of X is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of X #), the ResultSort of S1 * the Sorts of X
the Charact of X . (g . Af1) is Relation-like Function-like set
hf1h is Element of Args ((g . Af1),S3)
f1 # hf1h is Element of Args ((g . Af1),X)
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
S2 is non empty non void feasible () (S1)
the carrier of S2 is non empty set
S3 is MSAlgebra over S1
the Sorts of S3 is non empty Relation-like the carrier of S1 -defined Function-like total set
X is MSAlgebra over S1
the Sorts of X is non empty Relation-like the carrier of S1 -defined Function-like total set
(S1,S2,S3) is strict MSAlgebra over S2
id the carrier of S2 is non empty Relation-like the carrier of S2 -defined the carrier of S2 -valued Function-like one-to-one total V29( the carrier of S2, the carrier of S2) Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
the carrier' of S2 is non empty set
id the carrier' of S2 is non empty Relation-like the carrier' of S2 -defined the carrier' of S2 -valued Function-like one-to-one total V29( the carrier' of S2, the carrier' of S2) Element of bool [: the carrier' of S2, the carrier' of S2:]
[: the carrier' of S2, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S2:] is set
(S2,S1,S3,(id the carrier of S2),(id the carrier' of S2)) is strict MSAlgebra over S2
the Sorts of (S1,S2,S3) is non empty Relation-like the carrier of S2 -defined Function-like total set
(S1,S2,X) is strict MSAlgebra over S2
(S2,S1,X,(id the carrier of S2),(id the carrier' of S2)) is strict MSAlgebra over S2
the Sorts of (S1,S2,X) is non empty Relation-like the carrier of S2 -defined Function-like total set
[: the carrier of S2, the carrier of S1:] is Relation-like set
bool [: the carrier of S2, the carrier of S1:] is set
g2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of S3, the Sorts of X
g2 | the carrier of S2 is Relation-like the carrier of S2 -defined the carrier of S1 -defined Function-like V53() V54() set
f2 is non empty Relation-like the carrier of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier of S2, the carrier of S1) Element of bool [: the carrier of S2, the carrier of S1:]
(S2,S1,S3,f2,(id the carrier' of S2)) is strict MSAlgebra over S2
the Sorts of (S2,S1,S3,f2,(id the carrier' of S2)) is non empty Relation-like the carrier of S2 -defined Function-like total set
(S2,S1,X,f2,(id the carrier' of S2)) is strict MSAlgebra over S2
the Sorts of (S2,S1,X,f2,(id the carrier' of S2)) is non empty Relation-like the carrier of S2 -defined Function-like total set
f2 * g2 is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() set
f is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (S2,S1,S3,f2,(id the carrier' of S2)), the Sorts of (S2,S1,X,f2,(id the carrier' of S2))
g is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (S1,S2,S3), the Sorts of (S1,S2,X)
S1 is non empty non void feasible () ManySortedSign
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
the carrier of S1 is non empty set
[: the carrier of S2, the carrier of S1:] is Relation-like set
bool [: the carrier of S2, the carrier of S1:] is set
S3 is non-empty MSAlgebra over S1
X is non empty Relation-like the carrier of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier of S2, the carrier of S1) Element of bool [: the carrier of S2, the carrier of S1:]
f1 is Relation-like Function-like set
(S2,S1,S3,X,f1) is strict MSAlgebra over S2
dom f1 is set
the carrier' of S2 is non empty set
rng f1 is set
the carrier' of S1 is non empty set
g1 is non-empty MSAlgebra over S2
[: the carrier' of S2, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S2, the carrier' of S1:] is set
g2 is Element of the carrier of S2
f is Element of the carrier of S2
X . g2 is Element of the carrier of S1
X . f is Element of the carrier of S1
g is Relation-like Function-like set
Af is Element of the carrier' of S2
the_result_sort_of Af is Element of the carrier of S2
the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S2 . Af is Element of the carrier of S2
the_arity_of Af is Relation-like NAT -defined the carrier of S2 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S2 . Af is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S2 *
dom (the_arity_of Af) is Element of bool NAT
Args (Af,g1) is non empty functional Element of rng ( the Sorts of g1 #)
the Sorts of g1 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
the Sorts of g1 # is non empty Relation-like the carrier of S2 * -defined Function-like total set
rng ( the Sorts of g1 #) is non empty set
the Arity of S2 * ( the Sorts of g1 #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of g1 #)) . Af is set
X * (the_arity_of Af) is Relation-like NAT -defined the carrier of S1 -valued Function-like Element of bool [:NAT, the carrier of S1:]
[:NAT, the carrier of S1:] is Relation-like set
bool [:NAT, the carrier of S1:] is set
f2 is non empty Relation-like the carrier' of S2 -defined the carrier' of S1 -valued Function-like total V29( the carrier' of S2, the carrier' of S1) Element of bool [: the carrier' of S2, the carrier' of S1:]
f2 . Af is Element of the carrier' of S1
the_arity_of (f2 . Af) is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 . (f2 . Af) is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
the_result_sort_of (f2 . Af) is Element of the carrier of S1
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 . (f2 . Af) is Element of the carrier of S1
dom (the_arity_of (f2 . Af)) is Element of bool NAT
Args ((f2 . Af),S3) is non empty functional Element of rng ( the Sorts of S3 #)
the Sorts of S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
the Sorts of S3 # is non empty Relation-like the carrier of S1 * -defined Function-like total set
rng ( the Sorts of S3 #) is non empty set
the Arity of S1 * ( the Sorts of S3 #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of S3 #)) . (f2 . Af) is set
X * the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S2, the carrier of S1) Element of bool [: the carrier' of S2, the carrier of S1:]
[: the carrier' of S2, the carrier of S1:] is Relation-like set
bool [: the carrier' of S2, the carrier of S1:] is set
the ResultSort of S1 * f2 is non empty Relation-like the carrier' of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S2, the carrier of S1) Element of bool [: the carrier' of S2, the carrier of S1:]
(X * the ResultSort of S2) . Af is Element of the carrier of S1
Af1 is Element of NAT
(the_arity_of Af) /. Af1 is Element of the carrier of S2
hf1 is Relation-like Function-like set
transl (Af,Af1,hf1,g1) is Relation-like Function-like set
Af1 is Element of NAT
(the_arity_of Af) /. Af1 is Element of the carrier of S2
hf1 is Relation-like Function-like set
transl (Af,Af1,hf1,g1) is Relation-like Function-like set
(the_arity_of (f2 . Af)) /. Af1 is Element of the carrier of S1
rng (the_arity_of Af) is set
dom X is non empty set
(the_arity_of (f2 . Af)) . Af1 is set
(the_arity_of Af) . Af1 is set
X . ((the_arity_of Af) . Af1) is set
transl ((f2 . Af),Af1,hf1,S3) is Relation-like Function-like set
dom (transl ((f2 . Af),Af1,hf1,S3)) is set
the Sorts of S3 . (X . g2) is non empty set
X * the Sorts of S3 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
the Sorts of g1 . g2 is non empty set
hh is set
g . hh is set
Den (Af,g1) is non empty Relation-like Args (Af,g1) -defined Result (Af,g1) -valued Function-like total V29( Args (Af,g1), Result (Af,g1)) Element of bool [:(Args (Af,g1)),(Result (Af,g1)):]
Result (Af,g1) is non empty Element of rng the Sorts of g1
rng the Sorts of g1 is non empty V133() set
the ResultSort of S2 * the Sorts of g1 is non empty Relation-like non-empty non empty-yielding the carrier' of S2 -defined Function-like total set
( the ResultSort of S2 * the Sorts of g1) . Af is non empty set
[:(Args (Af,g1)),(Result (Af,g1)):] is Relation-like set
bool [:(Args (Af,g1)),(Result (Af,g1)):] is set
the Charact of g1 is non empty Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of g1 #), the ResultSort of S2 * the Sorts of g1
the Charact of g1 . Af is Relation-like Function-like set
hf1 +* (Af1,hh) is Relation-like Function-like set
(Den (Af,g1)) . (hf1 +* (Af1,hh)) is set
(transl ((f2 . Af),Af1,hf1,S3)) . hh is set
Den ((f2 . Af),S3) is non empty Relation-like Args ((f2 . Af),S3) -defined Result ((f2 . Af),S3) -valued Function-like total V29( Args ((f2 . Af),S3), Result ((f2 . Af),S3)) Element of bool [:(Args ((f2 . Af),S3)),(Result ((f2 . Af),S3)):]
Result ((f2 . Af),S3) is non empty Element of rng the Sorts of S3
rng the Sorts of S3 is non empty V133() set
the ResultSort of S1 * the Sorts of S3 is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set
( the ResultSort of S1 * the Sorts of S3) . (f2 . Af) is non empty set
[:(Args ((f2 . Af),S3)),(Result ((f2 . Af),S3)):] is Relation-like set
bool [:(Args ((f2 . Af),S3)),(Result ((f2 . Af),S3)):] is set
the Charact of S3 is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of S3 #), the ResultSort of S1 * the Sorts of S3
the Charact of S3 . (f2 . Af) is Relation-like Function-like set
(Den ((f2 . Af),S3)) . (hf1 +* (Af1,hh)) is set
dom g is set
S1 is non empty non void feasible () ManySortedSign
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
the carrier of S1 is non empty set
[: the carrier of S2, the carrier of S1:] is Relation-like set
bool [: the carrier of S2, the carrier of S1:] is set
TranslationRel S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
TranslationRel S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is set
S3 is non-empty MSAlgebra over S1
the Sorts of S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
X is non empty Relation-like the carrier of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier of S2, the carrier of S1) Element of bool [: the carrier of S2, the carrier of S1:]
f1 is Relation-like Function-like set
(S2,S1,S3,X,f1) is strict MSAlgebra over S2
g1 is non-empty MSAlgebra over S2
the Sorts of g1 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
f2 is Element of the carrier of S2
g2 is Element of the carrier of S2
the Sorts of g1 . f2 is non empty set
the Sorts of g1 . g2 is non empty set
X . f2 is Element of the carrier of S1
X . g2 is Element of the carrier of S1
the Sorts of S3 . (X . f2) is non empty set
the Sorts of S3 . (X . g2) is non empty set
f is Element of the carrier of S2
X . f is Element of the carrier of S1
the Sorts of S3 . (X . f) is non empty set
g is non empty Relation-like the Sorts of g1 . f2 -defined the Sorts of g1 . g2 -valued Function-like total V29( the Sorts of g1 . f2, the Sorts of g1 . g2) Translation of g1,f2,g2
Af is Relation-like Function-like set
g * Af is Relation-like the Sorts of g1 . f2 -defined Function-like set
[(X . g2),(X . f)] is set
{(X . g2),(X . f)} is non empty set
{(X . g2)} is non empty set
{{(X . g2),(X . f)},{(X . g2)}} is non empty set
f2 is Element of the carrier of S2
g2 is Element of the carrier of S2
X . f2 is Element of the carrier of S1
X . g2 is Element of the carrier of S1
the Sorts of g1 . f2 is non empty set
the Sorts of g1 . g2 is non empty set
the Sorts of S3 . (X . f2) is non empty set
the Sorts of S3 . (X . g2) is non empty set
f is Element of the carrier of S2
the Sorts of g1 . f is non empty set
id ( the Sorts of g1 . f) is non empty Relation-like the Sorts of g1 . f -defined the Sorts of g1 . f -valued Function-like one-to-one total V29( the Sorts of g1 . f, the Sorts of g1 . f) Element of bool [:( the Sorts of g1 . f),( the Sorts of g1 . f):]
[:( the Sorts of g1 . f),( the Sorts of g1 . f):] is Relation-like set
bool [:( the Sorts of g1 . f),( the Sorts of g1 . f):] is set
X . f is Element of the carrier of S1
the Sorts of S3 . (X . f) is non empty set
X * the Sorts of S3 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
f is non empty Relation-like the Sorts of g1 . f2 -defined the Sorts of g1 . g2 -valued Function-like total V29( the Sorts of g1 . f2, the Sorts of g1 . g2) Translation of g1,f2,g2
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
[: the carrier of S2, the carrier of S1:] is Relation-like set
bool [: the carrier of S2, the carrier of S1:] is set
TranslationRel S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
TranslationRel S1 is Relation-like the carrier of S1 -defined the carrier of S1 -valued Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is set
the non-empty MSAlgebra over S1 is non-empty MSAlgebra over S1
X is non empty Relation-like the carrier of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier of S2, the carrier of S1) Element of bool [: the carrier of S2, the carrier of S1:]
f1 is Relation-like Function-like set
(S2,S1, the non-empty MSAlgebra over S1,X,f1) is strict MSAlgebra over S2
g1 is Element of the carrier of S2
f2 is Element of the carrier of S2
X . g1 is Element of the carrier of S1
X . f2 is Element of the carrier of S1
S1 is non empty non void feasible () ManySortedSign
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
the carrier of S1 is non empty set
[: the carrier of S2, the carrier of S1:] is Relation-like set
bool [: the carrier of S2, the carrier of S1:] is set
g1 is non-empty MSAlgebra over S2
the Sorts of g1 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
f2 is Element of the carrier of S2
the Sorts of g1 . f2 is non empty set
g2 is Element of the carrier of S2
the Sorts of g1 . g2 is non empty set
X is non empty Relation-like the carrier of S2 -defined the carrier of S1 -valued Function-like total V29( the carrier of S2, the carrier of S1) Element of bool [: the carrier of S2, the carrier of S1:]
f1 is Relation-like Function-like set
S3 is non-empty MSAlgebra over S1
(S2,S1,S3,X,f1) is strict MSAlgebra over S2
TranslationRel S2 is Relation-like the carrier of S2 -defined the carrier of S2 -valued Element of bool [: the carrier of S2, the carrier of S2:]
[: the carrier of S2, the carrier of S2:] is Relation-like set
bool [: the carrier of S2, the carrier of S2:] is set
f is non empty Relation-like the Sorts of g1 . f2 -defined the Sorts of g1 . g2 -valued Function-like total V29( the Sorts of g1 . f2, the Sorts of g1 . g2) Translation of g1,f2,g2
the Sorts of S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
X . f2 is Element of the carrier of S1
the Sorts of S3 . (X . f2) is non empty set
X . g2 is Element of the carrier of S1
the Sorts of S3 . (X . g2) is non empty set
F1() is non empty non void feasible () ManySortedSign
the carrier of F1() is non empty set
F3() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
F2() is non-empty MSAlgebra over F1()
the Sorts of F2() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
FreeMSA F3() is strict non-empty V132(F1()) MSAlgebra over F1()
the Sorts of (FreeMSA F3()) is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
FreeGen F3() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total V131(F1(), FreeMSA F3()) GeneratorSet of FreeMSA F3()
S1 is set
(FreeGen F3()) . S1 is set
the Sorts of F2() . S1 is set
[:((FreeGen F3()) . S1),( the Sorts of F2() . S1):] is Relation-like set
bool [:((FreeGen F3()) . S1),( the Sorts of F2() . S1):] is set
F3() . S1 is set
S2 is Element of the carrier of F1()
F3() . S2 is non empty set
(FreeGen F3()) . S2 is non empty set
FreeGen (S2,F3()) is non empty Element of bool ((FreeSort F3()) . S2)
FreeSort F3() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
(FreeSort F3()) . S2 is non empty set
bool ((FreeSort F3()) . S2) is set
the Sorts of F2() . S2 is non empty set
S3 is set
X is set
[X,S2] is set
{X,S2} is non empty set
{X} is non empty set
{{X,S2},{X}} is non empty set
root-tree [X,S2] is Relation-like Function-like V117() set
f1 is Element of F3() . S2
F4(f1,S2) is set
g1 is set
[f1,S2] is set
{f1,S2} is non empty set
{f1} is non empty set
{{f1,S2},{f1}} is non empty set
root-tree [f1,S2] is Relation-like Function-like V117() set
S3 is Relation-like Function-like set
dom S3 is set
rng S3 is set
X is Relation-like (FreeGen F3()) . S1 -defined the Sorts of F2() . S1 -valued Function-like V29((FreeGen F3()) . S1, the Sorts of F2() . S1) Element of bool [:((FreeGen F3()) . S1),( the Sorts of F2() . S1):]
f1 is Relation-like (FreeGen F3()) . S1 -defined the Sorts of F2() . S1 -valued Function-like V29((FreeGen F3()) . S1, the Sorts of F2() . S1) Element of bool [:((FreeGen F3()) . S1),( the Sorts of F2() . S1):]
g1 is Element of F3() . S1
[g1,S1] is set
{g1,S1} is non empty set
{g1} is non empty set
{{g1,S1},{g1}} is non empty set
root-tree [g1,S1] is Relation-like Function-like V117() set
X . (root-tree [g1,S1]) is set
F4(g1,S1) is set
[g1,S2] is set
{g1,S2} is non empty set
{{g1,S2},{g1}} is non empty set
root-tree [g1,S2] is Relation-like Function-like V117() set
X . (root-tree [g1,S2]) is set
f2 is Element of F3() . S2
[f2,S2] is set
{f2,S2} is non empty set
{f2} is non empty set
{{f2,S2},{f2}} is non empty set
root-tree [f2,S2] is Relation-like Function-like V117() set
F4(f2,S2) is set
S1 is Relation-like Function-like set
dom S1 is set
S2 is non empty Relation-like the carrier of F1() -defined Function-like total set
S3 is set
S2 . S3 is set
(FreeGen F3()) . S3 is set
the Sorts of F2() . S3 is set
[:((FreeGen F3()) . S3),( the Sorts of F2() . S3):] is Relation-like set
bool [:((FreeGen F3()) . S3),( the Sorts of F2() . S3):] is set
F3() . S3 is set
X is Relation-like (FreeGen F3()) . S3 -defined the Sorts of F2() . S3 -valued Function-like V29((FreeGen F3()) . S3, the Sorts of F2() . S3) Element of bool [:((FreeGen F3()) . S3),( the Sorts of F2() . S3):]
S3 is non empty Relation-like the carrier of F1() -defined Function-like total V53() V54() ManySortedFunction of FreeGen F3(), the Sorts of F2()
X is non empty Relation-like the carrier of F1() -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA F3()), the Sorts of F2()
X || (FreeGen F3()) is non empty Relation-like the carrier of F1() -defined Function-like total V53() V54() ManySortedFunction of FreeGen F3(), the Sorts of F2()
f1 is Element of the carrier of F1()
F3() . f1 is non empty set
X . f1 is non empty Relation-like the Sorts of (FreeMSA F3()) . f1 -defined the Sorts of F2() . f1 -valued Function-like total V29( the Sorts of (FreeMSA F3()) . f1, the Sorts of F2() . f1) Element of bool [:( the Sorts of (FreeMSA F3()) . f1),( the Sorts of F2() . f1):]
the Sorts of (FreeMSA F3()) . f1 is non empty set
the Sorts of F2() . f1 is non empty set
[:( the Sorts of (FreeMSA F3()) . f1),( the Sorts of F2() . f1):] is Relation-like set
bool [:( the Sorts of (FreeMSA F3()) . f1),( the Sorts of F2() . f1):] is set
g1 is Element of F3() . f1
[g1,f1] is set
{g1,f1} is non empty set
{g1} is non empty set
{{g1,f1},{g1}} is non empty set
root-tree [g1,f1] is Relation-like Function-like V117() set
(X . f1) . (root-tree [g1,f1]) is set
F4(g1,f1) is set
(FreeGen F3()) . f1 is non empty set
[:((FreeGen F3()) . f1),( the Sorts of F2() . f1):] is Relation-like set
bool [:((FreeGen F3()) . f1),( the Sorts of F2() . f1):] is set
S3 . f1 is non empty Relation-like (FreeGen F3()) . f1 -defined the Sorts of F2() . f1 -valued Function-like total V29((FreeGen F3()) . f1, the Sorts of F2() . f1) Element of bool [:((FreeGen F3()) . f1),( the Sorts of F2() . f1):]
DTConMSA F3() is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA F3()) is non empty set
FinTrees the carrier of (DTConMSA F3()) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA F3())
F1() -Terms F3() is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA F3()))
bool (FinTrees the carrier of (DTConMSA F3())) is set
FreeGen (f1,F3()) is non empty Element of bool ((FreeSort F3()) . f1)
FreeSort F3() is non empty Relation-like non-empty non empty-yielding the carrier of F1() -defined Function-like total set
(FreeSort F3()) . f1 is non empty set
bool ((FreeSort F3()) . f1) is set
f2 is Relation-like the carrier of (DTConMSA F3()) -valued Function-like V32() V117() Element of F1() -Terms F3()
(X . f1) | ((FreeGen F3()) . f1) is Relation-like the Sorts of (FreeMSA F3()) . f1 -defined (FreeGen F3()) . f1 -defined the Sorts of (FreeMSA F3()) . f1 -defined the Sorts of F2() . f1 -valued Function-like Element of bool [:( the Sorts of (FreeMSA F3()) . f1),( the Sorts of F2() . f1):]
(S3 . f1) . (root-tree [g1,f1]) is set
g2 is non empty Relation-like (FreeGen F3()) . f1 -defined the Sorts of F2() . f1 -valued Function-like total V29((FreeGen F3()) . f1, the Sorts of F2() . f1) Element of bool [:((FreeGen F3()) . f1),( the Sorts of F2() . f1):]
S1 is set
S2 is Relation-like S1 -defined Function-like total set
S3 is Relation-like S1 -defined Function-like total set
X is Relation-like S1 -defined Function-like total ManySortedSubset of S2
f1 is Relation-like S1 -defined Function-like total V53() V54() ManySortedFunction of S2,S3
f1 || X is Relation-like S1 -defined Function-like total V53() V54() ManySortedFunction of X,S3
g1 is set
f1 . g1 is Relation-like Function-like set
(f1 || X) . g1 is Relation-like Function-like set
X . g1 is set
S2 . g1 is set
S3 . g1 is set
[:(S2 . g1),(S3 . g1):] is Relation-like set
bool [:(S2 . g1),(S3 . g1):] is set
g2 is Relation-like Function-like set
f is Relation-like Function-like set
g is set
f . g is set
g2 . g is set
f2 is Relation-like S2 . g1 -defined S3 . g1 -valued Function-like V29(S2 . g1,S3 . g1) Element of bool [:(S2 . g1),(S3 . g1):]
f2 | (X . g1) is Relation-like X . g1 -defined S2 . g1 -defined S3 . g1 -valued Function-like Element of bool [:(S2 . g1),(S3 . g1):]
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
S2 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeGen S2 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total V131(S1, FreeMSA S2) GeneratorSet of FreeMSA S2
FreeMSA S2 is strict non-empty V132(S1) MSAlgebra over S1
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
[: the carrier of S1, the carrier of S2:] is Relation-like set
bool [: the carrier of S1, the carrier of S2:] is set
X is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier of S1, the carrier of S2) Element of bool [: the carrier of S1, the carrier of S2:]
f1 is Relation-like Function-like set
S3 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
X * S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA (X * S3) is strict non-empty V132(S1) MSAlgebra over S1
the Sorts of (FreeMSA (X * S3)) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA S3 is strict non-empty V132(S2) MSAlgebra over S2
(S1,S2,(FreeMSA S3),X,f1) is strict MSAlgebra over S1
the Sorts of (S1,S2,(FreeMSA S3),X,f1) is non empty Relation-like the carrier of S1 -defined Function-like total set
the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
X * the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
g2 is Element of the carrier of S1
(X * S3) . g2 is non empty set
X . g2 is Element of the carrier of S2
g is Element of the carrier of S2
S3 . g is non empty set
f is Element of (X * S3) . g2
DTConMSA S3 is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA S3) is non empty set
FinTrees the carrier of (DTConMSA S3) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA S3)
S2 -Terms S3 is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))
bool (FinTrees the carrier of (DTConMSA S3)) is set
Af is Element of S3 . g
[Af,g] is set
{Af,g} is non empty set
{Af} is non empty set
{{Af,g},{Af}} is non empty set
root-tree [Af,g] is Relation-like Function-like V117() set
Af1 is Relation-like the carrier of (DTConMSA S3) -valued Function-like V32() V117() Element of S2 -Terms S3
the_sort_of Af1 is Element of the carrier of S2
FreeSort (S3,g) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA S3))
TS (DTConMSA S3) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))
bool (TS (DTConMSA S3)) is set
FreeSort S3 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
(FreeSort S3) . g is non empty set
FreeOper S3 is non empty Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ((FreeSort S3) #), the ResultSort of S2 * (FreeSort S3)
the carrier' of S2 is non empty set
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
(FreeSort S3) # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the Arity of S2 * ((FreeSort S3) #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S2 * (FreeSort S3) is non empty Relation-like non-empty non empty-yielding the carrier' of S2 -defined Function-like total set
MSAlgebra(# (FreeSort S3),(FreeOper S3) #) is strict MSAlgebra over S2
f2 is non-empty MSAlgebra over S1
the Sorts of f2 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
X . g2 is set
[f,(X . g2)] is set
{f,(X . g2)} is non empty set
{f} is non empty set
{{f,(X . g2)},{f}} is non empty set
root-tree [f,(X . g2)] is Relation-like Function-like V117() set
the Sorts of f2 . g2 is non empty set
g2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (X * S3)), the Sorts of f2
f is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (X * S3)), the Sorts of (S1,S2,(FreeMSA S3),X,f1)
g is Element of the carrier of S1
(X * S3) . g is non empty set
f . g is Relation-like the Sorts of (FreeMSA (X * S3)) . g -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . g -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . g, the Sorts of (S1,S2,(FreeMSA S3),X,f1) . g) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . g),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . g):]
the Sorts of (FreeMSA (X * S3)) . g is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . g is set
[:( the Sorts of (FreeMSA (X * S3)) . g),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . g):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . g),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . g):] is set
Af is Element of (X * S3) . g
[Af,g] is set
{Af,g} is non empty set
{Af} is non empty set
{{Af,g},{Af}} is non empty set
root-tree [Af,g] is Relation-like Function-like V117() set
(f . g) . (root-tree [Af,g]) is set
X . g is Element of the carrier of S2
[Af,(X . g)] is set
{Af,(X . g)} is non empty set
{{Af,(X . g)},{Af}} is non empty set
root-tree [Af,(X . g)] is Relation-like Function-like V117() set
f2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (X * S3)), the Sorts of (S1,S2,(FreeMSA S3),X,f1)
g2 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (X * S3)), the Sorts of (S1,S2,(FreeMSA S3),X,f1)
Af is set
FreeGen (X * S3) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total V131(S1, FreeMSA (X * S3)) GeneratorSet of FreeMSA (X * S3)
Af1 is Element of the carrier of S1
(FreeGen (X * S3)) . Af1 is non empty set
g1 is non-empty MSAlgebra over S1
the Sorts of g1 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
the Sorts of g1 . Af1 is non empty set
[:((FreeGen (X * S3)) . Af1),( the Sorts of g1 . Af1):] is Relation-like set
bool [:((FreeGen (X * S3)) . Af1),( the Sorts of g1 . Af1):] is set
f2 || (FreeGen (X * S3)) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of FreeGen (X * S3), the Sorts of (S1,S2,(FreeMSA S3),X,f1)
(f2 || (FreeGen (X * S3))) . Af1 is Relation-like (FreeGen (X * S3)) . Af1 -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1 -valued Function-like V29((FreeGen (X * S3)) . Af1, the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1) Element of bool [:((FreeGen (X * S3)) . Af1),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1):]
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1 is set
[:((FreeGen (X * S3)) . Af1),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1):] is Relation-like set
bool [:((FreeGen (X * S3)) . Af1),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1):] is set
g2 || (FreeGen (X * S3)) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of FreeGen (X * S3), the Sorts of (S1,S2,(FreeMSA S3),X,f1)
(g2 || (FreeGen (X * S3))) . Af1 is Relation-like (FreeGen (X * S3)) . Af1 -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1 -valued Function-like V29((FreeGen (X * S3)) . Af1, the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1) Element of bool [:((FreeGen (X * S3)) . Af1),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1):]
FreeGen (Af1,(X * S3)) is non empty Element of bool ((FreeSort (X * S3)) . Af1)
FreeSort (X * S3) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
(FreeSort (X * S3)) . Af1 is non empty set
bool ((FreeSort (X * S3)) . Af1) is set
(X * S3) . Af1 is non empty set
hf1h is Element of (FreeGen (X * S3)) . Af1
s is set
[s,Af1] is set
{s,Af1} is non empty set
{s} is non empty set
{{s,Af1},{s}} is non empty set
root-tree [s,Af1] is Relation-like Function-like V117() set
hf1 is non empty Relation-like (FreeGen (X * S3)) . Af1 -defined the Sorts of g1 . Af1 -valued Function-like total V29((FreeGen (X * S3)) . Af1, the Sorts of g1 . Af1) Element of bool [:((FreeGen (X * S3)) . Af1),( the Sorts of g1 . Af1):]
hf1 . hf1h is Element of the Sorts of g1 . Af1
f2 . Af1 is Relation-like the Sorts of (FreeMSA (X * S3)) . Af1 -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1 -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . Af1, the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . Af1),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1):]
the Sorts of (FreeMSA (X * S3)) . Af1 is non empty set
[:( the Sorts of (FreeMSA (X * S3)) . Af1),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . Af1),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1):] is set
(f2 . Af1) . hf1h is set
x is Element of (X * S3) . Af1
X . Af1 is Element of the carrier of S2
[x,(X . Af1)] is set
{x,(X . Af1)} is non empty set
{x} is non empty set
{{x,(X . Af1)},{x}} is non empty set
root-tree [x,(X . Af1)] is Relation-like Function-like V117() set
g2 . Af1 is Relation-like the Sorts of (FreeMSA (X * S3)) . Af1 -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1 -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . Af1, the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . Af1),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . Af1):]
(g2 . Af1) . hf1h is set
hh is non empty Relation-like (FreeGen (X * S3)) . Af1 -defined the Sorts of g1 . Af1 -valued Function-like total V29((FreeGen (X * S3)) . Af1, the Sorts of g1 . Af1) Element of bool [:((FreeGen (X * S3)) . Af1),( the Sorts of g1 . Af1):]
hh . hf1h is Element of the Sorts of g1 . Af1
(f2 || (FreeGen (X * S3))) . Af is Relation-like Function-like set
(g2 || (FreeGen (X * S3))) . Af is Relation-like Function-like set
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
[: the carrier of S1, the carrier of S2:] is Relation-like set
bool [: the carrier of S1, the carrier of S2:] is set
the carrier' of S1 is non empty set
S3 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
FreeMSA S3 is strict non-empty V132(S2) MSAlgebra over S2
X is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier of S1, the carrier of S2) Element of bool [: the carrier of S1, the carrier of S2:]
X * S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA (X * S3) is strict non-empty V132(S1) MSAlgebra over S1
the Sorts of (FreeMSA (X * S3)) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
f1 is Relation-like Function-like set
(S1,S2,(FreeMSA S3),X,f1) is strict MSAlgebra over S1
(S1,S2,S3,X,f1) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (X * S3)), the Sorts of (S1,S2,(FreeMSA S3),X,f1)
the Sorts of (S1,S2,(FreeMSA S3),X,f1) is non empty Relation-like the carrier of S1 -defined Function-like total set
the carrier' of S2 is non empty set
[: the carrier' of S1, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S2:] is set
g2 is Element of the carrier' of S1
Args (g2,(FreeMSA (X * S3))) is non empty functional Element of rng ( the Sorts of (FreeMSA (X * S3)) #)
the Sorts of (FreeMSA (X * S3)) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of (FreeMSA (X * S3)) #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of (FreeMSA (X * S3)) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (FreeMSA (X * S3)) #)) . g2 is set
the_result_sort_of g2 is Element of the carrier of S1
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 . g2 is Element of the carrier of S1
(S1,S2,S3,X,f1) . (the_result_sort_of g2) is Relation-like the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of g2) -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of g2) -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of g2), the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of g2)) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of g2)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of g2)):]
the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of g2) is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of g2) is set
[:( the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of g2)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of g2)):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of g2)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of g2)):] is set
[g2, the carrier of S1] is set
{g2, the carrier of S1} is non empty set
{g2} is non empty set
{{g2, the carrier of S1},{g2}} is non empty set
f1 . g2 is set
[(f1 . g2), the carrier of S2] is set
{(f1 . g2), the carrier of S2} is non empty set
{(f1 . g2)} is non empty set
{{(f1 . g2), the carrier of S2},{(f1 . g2)}} is non empty set
f is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like DTree-yielding Element of Args (g2,(FreeMSA (X * S3)))
(S1,S2,S3,X,f1) # f is Element of Args (g2,(S1,S2,(FreeMSA S3),X,f1))
Args (g2,(S1,S2,(FreeMSA S3),X,f1)) is Element of rng ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #)
the Sorts of (S1,S2,(FreeMSA S3),X,f1) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
rng ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #) is non empty set
the Arity of S1 * ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #)) . g2 is set
[g2, the carrier of S1] -tree f is Relation-like Function-like V117() set
((S1,S2,S3,X,f1) . (the_result_sort_of g2)) . ([g2, the carrier of S1] -tree f) is set
g is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like set
[(f1 . g2), the carrier of S2] -tree g is Relation-like Function-like V117() set
f2 is non empty Relation-like the carrier' of S1 -defined the carrier' of S2 -valued Function-like total V29( the carrier' of S1, the carrier' of S2) Element of bool [: the carrier' of S1, the carrier' of S2:]
f2 . g2 is Element of the carrier' of S2
Args ((f2 . g2),(FreeMSA S3)) is non empty functional Element of rng ( the Sorts of (FreeMSA S3) #)
the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
the Sorts of (FreeMSA S3) # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
rng ( the Sorts of (FreeMSA S3) #) is non empty set
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S2 * ( the Sorts of (FreeMSA S3) #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of (FreeMSA S3) #)) . (f2 . g2) is set
Result (g2,(FreeMSA (X * S3))) is non empty Element of rng the Sorts of (FreeMSA (X * S3))
rng the Sorts of (FreeMSA (X * S3)) is non empty V133() set
the ResultSort of S1 * the Sorts of (FreeMSA (X * S3)) is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set
( the ResultSort of S1 * the Sorts of (FreeMSA (X * S3))) . g2 is non empty set
Den (g2,(FreeMSA (X * S3))) is non empty Relation-like Args (g2,(FreeMSA (X * S3))) -defined Result (g2,(FreeMSA (X * S3))) -valued Function-like total V29( Args (g2,(FreeMSA (X * S3))), Result (g2,(FreeMSA (X * S3)))) Element of bool [:(Args (g2,(FreeMSA (X * S3)))),(Result (g2,(FreeMSA (X * S3)))):]
[:(Args (g2,(FreeMSA (X * S3)))),(Result (g2,(FreeMSA (X * S3)))):] is Relation-like set
bool [:(Args (g2,(FreeMSA (X * S3)))),(Result (g2,(FreeMSA (X * S3)))):] is set
the Charact of (FreeMSA (X * S3)) is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of (FreeMSA (X * S3)) #), the ResultSort of S1 * the Sorts of (FreeMSA (X * S3))
the Charact of (FreeMSA (X * S3)) . g2 is Relation-like Function-like set
(Den (g2,(FreeMSA (X * S3)))) . f is Element of Result (g2,(FreeMSA (X * S3)))
((S1,S2,S3,X,f1) . (the_result_sort_of g2)) . ((Den (g2,(FreeMSA (X * S3)))) . f) is set
Den (g2,(S1,S2,(FreeMSA S3),X,f1)) is Relation-like Args (g2,(S1,S2,(FreeMSA S3),X,f1)) -defined Result (g2,(S1,S2,(FreeMSA S3),X,f1)) -valued Function-like V29( Args (g2,(S1,S2,(FreeMSA S3),X,f1)), Result (g2,(S1,S2,(FreeMSA S3),X,f1))) Element of bool [:(Args (g2,(S1,S2,(FreeMSA S3),X,f1))),(Result (g2,(S1,S2,(FreeMSA S3),X,f1))):]
Result (g2,(S1,S2,(FreeMSA S3),X,f1)) is Element of rng the Sorts of (S1,S2,(FreeMSA S3),X,f1)
rng the Sorts of (S1,S2,(FreeMSA S3),X,f1) is non empty set
the ResultSort of S1 * the Sorts of (S1,S2,(FreeMSA S3),X,f1) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the ResultSort of S1 * the Sorts of (S1,S2,(FreeMSA S3),X,f1)) . g2 is set
[:(Args (g2,(S1,S2,(FreeMSA S3),X,f1))),(Result (g2,(S1,S2,(FreeMSA S3),X,f1))):] is Relation-like set
bool [:(Args (g2,(S1,S2,(FreeMSA S3),X,f1))),(Result (g2,(S1,S2,(FreeMSA S3),X,f1))):] is set
the Charact of (S1,S2,(FreeMSA S3),X,f1) is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #), the ResultSort of S1 * the Sorts of (S1,S2,(FreeMSA S3),X,f1)
the Charact of (S1,S2,(FreeMSA S3),X,f1) . g2 is Relation-like Function-like set
(Den (g2,(S1,S2,(FreeMSA S3),X,f1))) . g is set
Den ((f2 . g2),(FreeMSA S3)) is non empty Relation-like Args ((f2 . g2),(FreeMSA S3)) -defined Result ((f2 . g2),(FreeMSA S3)) -valued Function-like total V29( Args ((f2 . g2),(FreeMSA S3)), Result ((f2 . g2),(FreeMSA S3))) Element of bool [:(Args ((f2 . g2),(FreeMSA S3))),(Result ((f2 . g2),(FreeMSA S3))):]
Result ((f2 . g2),(FreeMSA S3)) is non empty Element of rng the Sorts of (FreeMSA S3)
rng the Sorts of (FreeMSA S3) is non empty V133() set
the ResultSort of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 -valued Function-like total V29( the carrier' of S2, the carrier of S2) Element of bool [: the carrier' of S2, the carrier of S2:]
[: the carrier' of S2, the carrier of S2:] is Relation-like set
bool [: the carrier' of S2, the carrier of S2:] is set
the ResultSort of S2 * the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier' of S2 -defined Function-like total set
( the ResultSort of S2 * the Sorts of (FreeMSA S3)) . (f2 . g2) is non empty set
[:(Args ((f2 . g2),(FreeMSA S3))),(Result ((f2 . g2),(FreeMSA S3))):] is Relation-like set
bool [:(Args ((f2 . g2),(FreeMSA S3))),(Result ((f2 . g2),(FreeMSA S3))):] is set
the Charact of (FreeMSA S3) is non empty Relation-like the carrier' of S2 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S2 * ( the Sorts of (FreeMSA S3) #), the ResultSort of S2 * the Sorts of (FreeMSA S3)
the Charact of (FreeMSA S3) . (f2 . g2) is Relation-like Function-like set
(Den ((f2 . g2),(FreeMSA S3))) . g is set
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
[: the carrier of S1, the carrier of S2:] is Relation-like set
bool [: the carrier of S1, the carrier of S2:] is set
S3 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
FreeMSA S3 is strict non-empty V132(S2) MSAlgebra over S2
DTConMSA S3 is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA S3) is non empty set
X is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier of S1, the carrier of S2) Element of bool [: the carrier of S1, the carrier of S2:]
X * S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
DTConMSA (X * S3) is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA (X * S3)) is non empty set
FinTrees the carrier of (DTConMSA (X * S3)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA (X * S3))
S1 -Terms (X * S3) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (X * S3)))
bool (FinTrees the carrier of (DTConMSA (X * S3))) is set
FreeMSA (X * S3) is strict non-empty V132(S1) MSAlgebra over S1
the Sorts of (FreeMSA (X * S3)) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
f1 is Relation-like Function-like set
(S1,S2,(FreeMSA S3),X,f1) is strict MSAlgebra over S1
the Sorts of (S1,S2,(FreeMSA S3),X,f1) is non empty Relation-like the carrier of S1 -defined Function-like total set
(S1,S2,S3,X,f1) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (X * S3)), the Sorts of (S1,S2,(FreeMSA S3),X,f1)
the carrier' of S1 is non empty set
the carrier' of S2 is non empty set
[: the carrier' of S1, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S2:] is set
f2 is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of f2 is Element of the carrier of S1
(S1,S2,S3,X,f1) . (the_sort_of f2) is Relation-like the Sorts of (FreeMSA (X * S3)) . (the_sort_of f2) -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of f2) -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . (the_sort_of f2), the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of f2)) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of f2)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of f2)):]
the Sorts of (FreeMSA (X * S3)) . (the_sort_of f2) is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of f2) is set
[:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of f2)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of f2)):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of f2)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of f2)):] is set
((S1,S2,S3,X,f1) . (the_sort_of f2)) . f2 is set
f2 . {} is set
{ the carrier of S1} is non empty set
[: the carrier' of S1,{ the carrier of S1}:] is Relation-like set
f is Element of the carrier of S1
(X * S3) . f is non empty set
g is Element of (X * S3) . f
[g,f] is set
{g,f} is non empty set
{g} is non empty set
{{g,f},{g}} is non empty set
root-tree [g,f] is Relation-like Function-like V117() set
(S1,S2,S3,X,f1) . f is Relation-like the Sorts of (FreeMSA (X * S3)) . f -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . f -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . f, the Sorts of (S1,S2,(FreeMSA S3),X,f1) . f) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . f),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . f):]
the Sorts of (FreeMSA (X * S3)) . f is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . f is set
[:( the Sorts of (FreeMSA (X * S3)) . f),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . f):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . f),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . f):] is set
((S1,S2,S3,X,f1) . f) . f2 is set
X . f is Element of the carrier of S2
[g,(X . f)] is set
{g,(X . f)} is non empty set
{{g,(X . f)},{g}} is non empty set
root-tree [g,(X . f)] is Relation-like Function-like V117() set
g2 is Relation-like the carrier of (DTConMSA S3) -valued Function-like V32() V117() CompoundTerm of S2,S3
g2 . {} is set
{ the carrier of S2} is non empty set
[: the carrier' of S2,{ the carrier of S2}:] is Relation-like set
g2 is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() CompoundTerm of S1,X * S3
g2 . {} is set
f is set
g is set
[f,g] is set
{f,g} is non empty set
{f} is non empty set
{{f,g},{f}} is non empty set
Af is Element of the carrier' of S1
Sym (Af,(X * S3)) is Element of K358((DTConMSA (X * S3)))
K358((DTConMSA (X * S3))) is non empty Element of bool the carrier of (DTConMSA (X * S3))
bool the carrier of (DTConMSA (X * S3)) is set
[Af, the carrier of S1] is set
{Af, the carrier of S1} is non empty set
{Af} is non empty set
{{Af, the carrier of S1},{Af}} is non empty set
Af1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA (X * S3)) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() DTree-yielding ArgumentSeq of Sym (Af,(X * S3))
[Af, the carrier of S1] -tree Af1 is Relation-like Function-like V117() set
Args (Af,(FreeMSA (X * S3))) is non empty functional Element of rng ( the Sorts of (FreeMSA (X * S3)) #)
the Sorts of (FreeMSA (X * S3)) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
rng ( the Sorts of (FreeMSA (X * S3)) #) is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
the Arity of S1 * ( the Sorts of (FreeMSA (X * S3)) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (FreeMSA (X * S3)) #)) . Af is set
g1 is non empty Relation-like the carrier' of S1 -defined the carrier' of S2 -valued Function-like total V29( the carrier' of S1, the carrier' of S2) Element of bool [: the carrier' of S1, the carrier' of S2:]
g1 . Af is Element of the carrier' of S2
Args ((g1 . Af),(FreeMSA S3)) is non empty functional Element of rng ( the Sorts of (FreeMSA S3) #)
the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
the Sorts of (FreeMSA S3) # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
rng ( the Sorts of (FreeMSA S3) #) is non empty set
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S2 * ( the Sorts of (FreeMSA S3) #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of (FreeMSA S3) #)) . (g1 . Af) is set
hf1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like DTree-yielding Element of Args (Af,(FreeMSA (X * S3)))
(S1,S2,S3,X,f1) # hf1 is Element of Args (Af,(S1,S2,(FreeMSA S3),X,f1))
Args (Af,(S1,S2,(FreeMSA S3),X,f1)) is Element of rng ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #)
the Sorts of (S1,S2,(FreeMSA S3),X,f1) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
rng ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #) is non empty set
the Arity of S1 * ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #)) . Af is set
the_result_sort_of Af is Element of the carrier of S1
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 . Af is Element of the carrier of S1
(S1,S2,S3,X,f1) . (the_result_sort_of Af) is Relation-like the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of Af) -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of Af) -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of Af), the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of Af)) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of Af)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of Af)):]
the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of Af) is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of Af) is set
[:( the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of Af)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of Af)):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . (the_result_sort_of Af)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_result_sort_of Af)):] is set
[Af, the carrier of S1] -tree hf1 is Relation-like Function-like V117() set
((S1,S2,S3,X,f1) . (the_result_sort_of Af)) . ([Af, the carrier of S1] -tree hf1) is set
f1 . Af is set
[(f1 . Af), the carrier of S2] is set
{(f1 . Af), the carrier of S2} is non empty set
{(f1 . Af)} is non empty set
{{(f1 . Af), the carrier of S2},{(f1 . Af)}} is non empty set
hh is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like DTree-yielding Element of Args ((g1 . Af),(FreeMSA S3))
[(f1 . Af), the carrier of S2] -tree hh is Relation-like Function-like V117() set
the_sort_of g2 is Element of the carrier of S1
FinTrees the carrier of (DTConMSA S3) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA S3)
Sym ((g1 . Af),S3) is Element of K358((DTConMSA S3))
K358((DTConMSA S3)) is non empty Element of bool the carrier of (DTConMSA S3)
bool the carrier of (DTConMSA S3) is set
hf1h is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() DTree-yielding ArgumentSeq of Sym ((g1 . Af),S3)
(Sym ((g1 . Af),S3)) -tree hf1h is Relation-like the carrier of (DTConMSA S3) -valued Function-like V32() V117() Element of S2 -Terms S3
S2 -Terms S3 is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))
bool (FinTrees the carrier of (DTConMSA S3)) is set
[(g1 . Af), the carrier of S2] is set
{(g1 . Af), the carrier of S2} is non empty set
{(g1 . Af)} is non empty set
{{(g1 . Af), the carrier of S2},{(g1 . Af)}} is non empty set
[(g1 . Af), the carrier of S2] -tree hf1h is Relation-like Function-like V117() set
s is Relation-like the carrier of (DTConMSA S3) -valued Function-like V32() V117() Element of S2 -Terms S3
s . {} is set
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
[: the carrier of S1, the carrier of S2:] is Relation-like set
bool [: the carrier of S1, the carrier of S2:] is set
S3 is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
FreeMSA S3 is strict non-empty V132(S2) MSAlgebra over S2
X is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier of S1, the carrier of S2) Element of bool [: the carrier of S1, the carrier of S2:]
X * S3 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA (X * S3) is strict non-empty V132(S1) MSAlgebra over S1
f1 is Relation-like Function-like one-to-one set
(S1,S2,(FreeMSA S3),X,f1) is strict MSAlgebra over S1
(S1,S2,S3,X,f1) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (X * S3)), the Sorts of (S1,S2,(FreeMSA S3),X,f1)
the Sorts of (FreeMSA (X * S3)) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) is non empty Relation-like the carrier of S1 -defined Function-like total set
DTConMSA (X * S3) is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA (X * S3)) is non empty set
FinTrees the carrier of (DTConMSA (X * S3)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA (X * S3))
S1 -Terms (X * S3) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (X * S3)))
bool (FinTrees the carrier of (DTConMSA (X * S3))) is set
FreeSort (X * S3) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeOper (X * S3) is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ((FreeSort (X * S3)) #), the ResultSort of S1 * (FreeSort (X * S3))
the carrier' of S1 is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
(FreeSort (X * S3)) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ((FreeSort (X * S3)) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * (FreeSort (X * S3)) is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set
MSAlgebra(# (FreeSort (X * S3)),(FreeOper (X * S3)) #) is strict MSAlgebra over S1
the carrier' of S2 is non empty set
[: the carrier' of S1, the carrier' of S2:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S2:] is set
f is non-empty MSAlgebra over S1
the Sorts of f is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
Af is Element of the carrier' of S1
Sym (Af,(X * S3)) is Element of K358((DTConMSA (X * S3)))
K358((DTConMSA (X * S3))) is non empty Element of bool the carrier of (DTConMSA (X * S3))
bool the carrier of (DTConMSA (X * S3)) is set
[Af, the carrier of S1] is set
{Af, the carrier of S1} is non empty set
{Af} is non empty set
{{Af, the carrier of S1},{Af}} is non empty set
Af1 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA (X * S3)) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() DTree-yielding ArgumentSeq of Sym (Af,(X * S3))
rng Af1 is set
[Af, the carrier of S1] -tree Af1 is Relation-like Function-like V117() set
dom Af1 is Element of bool NAT
the_arity_of Af is Relation-like NAT -defined the carrier of S1 -valued Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
the Arity of S1 . Af is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of S1 *
dom (the_arity_of Af) is Element of bool NAT
Args (Af,(FreeMSA (X * S3))) is non empty functional Element of rng ( the Sorts of (FreeMSA (X * S3)) #)
the Sorts of (FreeMSA (X * S3)) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
rng ( the Sorts of (FreeMSA (X * S3)) #) is non empty set
the Arity of S1 * ( the Sorts of (FreeMSA (X * S3)) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (FreeMSA (X * S3)) #)) . Af is set
g2 is non empty Relation-like the carrier' of S1 -defined the carrier' of S2 -valued Function-like total V29( the carrier' of S1, the carrier' of S2) Element of bool [: the carrier' of S1, the carrier' of S2:]
g2 . Af is Element of the carrier' of S2
[(g2 . Af), the carrier of S2] is set
{(g2 . Af), the carrier of S2} is non empty set
{(g2 . Af)} is non empty set
{{(g2 . Af), the carrier of S2},{(g2 . Af)}} is non empty set
{ the carrier of S2} is non empty set
[: the carrier' of S2,{ the carrier of S2}:] is Relation-like set
Args ((g2 . Af),(FreeMSA S3)) is non empty functional Element of rng ( the Sorts of (FreeMSA S3) #)
the Sorts of (FreeMSA S3) is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
the Sorts of (FreeMSA S3) # is non empty Relation-like the carrier of S2 * -defined Function-like total set
the carrier of S2 * is non empty functional FinSequence-membered M12( the carrier of S2)
rng ( the Sorts of (FreeMSA S3) #) is non empty set
the Arity of S2 is non empty Relation-like the carrier' of S2 -defined the carrier of S2 * -valued Function-like total V29( the carrier' of S2, the carrier of S2 * ) V53() V54() Element of bool [: the carrier' of S2,( the carrier of S2 *):]
[: the carrier' of S2,( the carrier of S2 *):] is Relation-like set
bool [: the carrier' of S2,( the carrier of S2 *):] is set
the Arity of S2 * ( the Sorts of (FreeMSA S3) #) is non empty Relation-like the carrier' of S2 -defined Function-like total set
( the Arity of S2 * ( the Sorts of (FreeMSA S3) #)) . (g2 . Af) is set
hf1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like DTree-yielding Element of Args (Af,(FreeMSA (X * S3)))
(S1,S2,S3,X,f1) # hf1 is Element of Args (Af,(S1,S2,(FreeMSA S3),X,f1))
Args (Af,(S1,S2,(FreeMSA S3),X,f1)) is Element of rng ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #)
the Sorts of (S1,S2,(FreeMSA S3),X,f1) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
rng ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #) is non empty set
the Arity of S1 * ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #)) . Af is set
(Sym (Af,(X * S3))) -tree Af1 is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
hf1h is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of hf1h is Element of the carrier of S1
(S1,S2,S3,X,f1) . (the_sort_of hf1h) is Relation-like the Sorts of (FreeMSA (X * S3)) . (the_sort_of hf1h) -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of hf1h) -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . (the_sort_of hf1h), the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of hf1h)) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of hf1h)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of hf1h)):]
the Sorts of (FreeMSA (X * S3)) . (the_sort_of hf1h) is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of hf1h) is set
[:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of hf1h)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of hf1h)):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of hf1h)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of hf1h)):] is set
((S1,S2,S3,X,f1) . (the_sort_of hf1h)) . hf1h is set
DTConMSA S3 is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA S3) is non empty set
FinTrees the carrier of (DTConMSA S3) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA S3)
Sym ((g2 . Af),S3) is Element of K358((DTConMSA S3))
K358((DTConMSA S3)) is non empty Element of bool the carrier of (DTConMSA S3)
bool the carrier of (DTConMSA S3) is set
hh is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like DTree-yielding Element of Args ((g2 . Af),(FreeMSA S3))
x is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of x is Element of the carrier of S1
((S1,S2,S3,X,f1) . (the_sort_of hf1h)) . x is set
the_result_sort_of Af is Element of the carrier of S1
the ResultSort of S1 . Af is Element of the carrier of S1
f1 . Af is set
[(f1 . Af), the carrier of S2] is set
{(f1 . Af), the carrier of S2} is non empty set
{(f1 . Af)} is non empty set
{{(f1 . Af), the carrier of S2},{(f1 . Af)}} is non empty set
[(f1 . Af), the carrier of S2] -tree hh is Relation-like Function-like V117() set
s is Relation-like NAT -defined FinTrees the carrier of (DTConMSA S3) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() DTree-yielding ArgumentSeq of Sym ((g2 . Af),S3)
(Sym ((g2 . Af),S3)) -tree s is Relation-like the carrier of (DTConMSA S3) -valued Function-like V32() V117() Element of S2 -Terms S3
S2 -Terms S3 is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA S3))
bool (FinTrees the carrier of (DTConMSA S3)) is set
((Sym ((g2 . Af),S3)) -tree s) . {} is set
[(g2 . Af), the carrier of S2] -tree s is Relation-like Function-like V117() set
x . {} is set
{ the carrier of S1} is non empty set
[: the carrier' of S1,{ the carrier of S1}:] is Relation-like set
t is set
v is set
[t,v] is set
{t,v} is non empty set
{t} is non empty set
{{t,v},{t}} is non empty set
t1 is Element of the carrier' of S1
[t1, the carrier of S1] is set
{t1, the carrier of S1} is non empty set
{t1} is non empty set
{{t1, the carrier of S1},{t1}} is non empty set
Sym (t1,(X * S3)) is Element of K358((DTConMSA (X * S3)))
t2 is Relation-like NAT -defined FinTrees the carrier of (DTConMSA (X * S3)) -valued Function-like V32() FinSequence-like FinSubsequence-like V53() V54() DTree-yielding ArgumentSeq of Sym (t1,(X * S3))
[t1, the carrier of S1] -tree t2 is Relation-like Function-like V117() set
Args (t1,(FreeMSA (X * S3))) is non empty functional Element of rng ( the Sorts of (FreeMSA (X * S3)) #)
( the Arity of S1 * ( the Sorts of (FreeMSA (X * S3)) #)) . t1 is set
g2 . t1 is Element of the carrier' of S2
Args ((g2 . t1),(FreeMSA S3)) is non empty functional Element of rng ( the Sorts of (FreeMSA S3) #)
( the Arity of S2 * ( the Sorts of (FreeMSA S3) #)) . (g2 . t1) is set
s2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like DTree-yielding Element of Args (t1,(FreeMSA (X * S3)))
(S1,S2,S3,X,f1) # s2 is Element of Args (t1,(S1,S2,(FreeMSA S3),X,f1))
Args (t1,(S1,S2,(FreeMSA S3),X,f1)) is Element of rng ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #)
( the Arity of S1 * ( the Sorts of (S1,S2,(FreeMSA S3),X,f1) #)) . t1 is set
the_result_sort_of t1 is Element of the carrier of S1
the ResultSort of S1 . t1 is Element of the carrier of S1
f1 . t1 is set
[(f1 . t1), the carrier of S2] is set
{(f1 . t1), the carrier of S2} is non empty set
{(f1 . t1)} is non empty set
{{(f1 . t1), the carrier of S2},{(f1 . t1)}} is non empty set
v2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like DTree-yielding Element of Args ((g2 . t1),(FreeMSA S3))
[(f1 . t1), the carrier of S2] -tree v2 is Relation-like Function-like V117() set
dom t2 is Element of bool NAT
g is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (X * S3)), the Sorts of f
g # s2 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of Args (t1,f)
Args (t1,f) is non empty functional Element of rng ( the Sorts of f #)
the Sorts of f # is non empty Relation-like the carrier of S1 * -defined Function-like total set
rng ( the Sorts of f #) is non empty set
the Arity of S1 * ( the Sorts of f #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
( the Arity of S1 * ( the Sorts of f #)) . t1 is set
i is V10() set
Af1 . i is Relation-like Function-like set
t2 . i is Relation-like Function-like set
w1 is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of w1 is Element of the carrier of S1
(the_arity_of Af) /. i is Element of the carrier of S1
g # hf1 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like Element of Args (Af,f)
Args (Af,f) is non empty functional Element of rng ( the Sorts of f #)
( the Arity of S1 * ( the Sorts of f #)) . Af is set
hh . i is set
(S1,S2,S3,X,f1) . (the_sort_of w1) is Relation-like the Sorts of (FreeMSA (X * S3)) . (the_sort_of w1) -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of w1) -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . (the_sort_of w1), the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of w1)) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of w1)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of w1)):]
the Sorts of (FreeMSA (X * S3)) . (the_sort_of w1) is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of w1) is set
[:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of w1)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of w1)):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of w1)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of w1)):] is set
((S1,S2,S3,X,f1) . (the_sort_of w1)) . w1 is set
w2 is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
((S1,S2,S3,X,f1) . (the_sort_of w1)) . w2 is set
the_sort_of w2 is Element of the carrier of S1
c27 is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of c27 is Element of the carrier of S1
(S1,S2,S3,X,f1) . (the_sort_of c27) is Relation-like the Sorts of (FreeMSA (X * S3)) . (the_sort_of c27) -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of c27) -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . (the_sort_of c27), the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of c27)) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of c27)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of c27)):]
the Sorts of (FreeMSA (X * S3)) . (the_sort_of c27) is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of c27) is set
[:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of c27)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of c27)):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of c27)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of c27)):] is set
((S1,S2,S3,X,f1) . (the_sort_of c27)) . c27 is set
Af is set
dom (S1,S2,S3,X,f1) is non empty set
(S1,S2,S3,X,f1) . Af is Relation-like Function-like set
Af1 is Relation-like Function-like set
dom Af1 is set
g is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (X * S3)), the Sorts of f
hf1 is Element of the carrier of S1
g . hf1 is non empty Relation-like the Sorts of (FreeMSA (X * S3)) . hf1 -defined the Sorts of f . hf1 -valued Function-like total V29( the Sorts of (FreeMSA (X * S3)) . hf1, the Sorts of f . hf1) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . hf1),( the Sorts of f . hf1):]
the Sorts of (FreeMSA (X * S3)) . hf1 is non empty set
the Sorts of f . hf1 is non empty set
[:( the Sorts of (FreeMSA (X * S3)) . hf1),( the Sorts of f . hf1):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . hf1),( the Sorts of f . hf1):] is set
dom (g . hf1) is non empty set
(FreeSort (X * S3)) . hf1 is non empty set
FreeSort ((X * S3),hf1) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA (X * S3)))
TS (DTConMSA (X * S3)) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA (X * S3)))
bool (TS (DTConMSA (X * S3))) is set
hh is set
hf1h is set
Af1 . hh is set
Af1 . hf1h is set
t is Element of the carrier of S1
(X * S3) . t is non empty set
v is Element of (X * S3) . t
[v,t] is set
{v,t} is non empty set
{v} is non empty set
{{v,t},{v}} is non empty set
root-tree [v,t] is Relation-like Function-like V117() set
t1 is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of t1 is Element of the carrier of S1
(S1,S2,S3,X,f1) . (the_sort_of t1) is Relation-like the Sorts of (FreeMSA (X * S3)) . (the_sort_of t1) -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t1) -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . (the_sort_of t1), the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t1)) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of t1)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t1)):]
the Sorts of (FreeMSA (X * S3)) . (the_sort_of t1) is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t1) is set
[:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of t1)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t1)):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of t1)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t1)):] is set
((S1,S2,S3,X,f1) . (the_sort_of t1)) . t1 is set
t2 is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of t2 is Element of the carrier of S1
((S1,S2,S3,X,f1) . (the_sort_of t1)) . t2 is set
(S1,S2,S3,X,f1) . t is Relation-like the Sorts of (FreeMSA (X * S3)) . t -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . t -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . t, the Sorts of (S1,S2,(FreeMSA S3),X,f1) . t) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . t),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . t):]
the Sorts of (FreeMSA (X * S3)) . t is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . t is set
[:( the Sorts of (FreeMSA (X * S3)) . t),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . t):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . t),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . t):] is set
((S1,S2,S3,X,f1) . t) . (root-tree [v,t]) is set
X . t is Element of the carrier of S2
[v,(X . t)] is set
{v,(X . t)} is non empty set
{{v,(X . t)},{v}} is non empty set
root-tree [v,(X . t)] is Relation-like Function-like V117() set
t2 . {} is set
{ the carrier of S1} is non empty set
[: the carrier' of S1,{ the carrier of S1}:] is Relation-like set
(root-tree [v,(X . t)]) . {} is set
DTConMSA S3 is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA S3) is non empty set
{ the carrier of S2} is non empty set
[: the carrier' of S2,{ the carrier of S2}:] is Relation-like set
s2 is Element of the carrier of S1
(X * S3) . s2 is non empty set
v2 is Element of (X * S3) . s2
[v2,s2] is set
{v2,s2} is non empty set
{v2} is non empty set
{{v2,s2},{v2}} is non empty set
root-tree [v2,s2] is Relation-like Function-like V117() set
((S1,S2,S3,X,f1) . t) . t2 is set
[v2,(X . t)] is set
{v2,(X . t)} is non empty set
{{v2,(X . t)},{v2}} is non empty set
root-tree [v2,(X . t)] is Relation-like Function-like V117() set
s is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of s is Element of the carrier of S1
x is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of x is Element of the carrier of S1
t is Relation-like the carrier of (DTConMSA (X * S3)) -valued Function-like V32() V117() Element of S1 -Terms (X * S3)
the_sort_of t is Element of the carrier of S1
(S1,S2,S3,X,f1) . (the_sort_of t) is Relation-like the Sorts of (FreeMSA (X * S3)) . (the_sort_of t) -defined the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t) -valued Function-like V29( the Sorts of (FreeMSA (X * S3)) . (the_sort_of t), the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t)) Element of bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of t)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t)):]
the Sorts of (FreeMSA (X * S3)) . (the_sort_of t) is non empty set
the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t) is set
[:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of t)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t)):] is Relation-like set
bool [:( the Sorts of (FreeMSA (X * S3)) . (the_sort_of t)),( the Sorts of (S1,S2,(FreeMSA S3),X,f1) . (the_sort_of t)):] is set
((S1,S2,S3,X,f1) . (the_sort_of t)) . t is set
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
id the carrier of S1 is non empty Relation-like the carrier of S1 -defined the carrier of S1 -valued Function-like one-to-one total V29( the carrier of S1, the carrier of S1) Element of bool [: the carrier of S1, the carrier of S1:]
[: the carrier of S1, the carrier of S1:] is Relation-like set
bool [: the carrier of S1, the carrier of S1:] is set
the carrier' of S1 is non empty set
id the carrier' of S1 is non empty Relation-like the carrier' of S1 -defined the carrier' of S1 -valued Function-like one-to-one total V29( the carrier' of S1, the carrier' of S1) Element of bool [: the carrier' of S1, the carrier' of S1:]
[: the carrier' of S1, the carrier' of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier' of S1:] is set
S2 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
(S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA ((id the carrier of S1) * S2)), the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1))
(id the carrier of S1) * S2 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA ((id the carrier of S1) * S2) is strict non-empty V132(S1) MSAlgebra over S1
the Sorts of (FreeMSA ((id the carrier of S1) * S2)) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA S2 is strict non-empty V132(S1) MSAlgebra over S1
(S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) is strict MSAlgebra over S1
the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) is non empty Relation-like the carrier of S1 -defined Function-like total set
the Sorts of (FreeMSA S2) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
id the Sorts of (FreeMSA S2) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA S2), the Sorts of (FreeMSA S2)
dom S2 is non empty set
f2 is set
FreeGen S2 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total V131(S1, FreeMSA S2) GeneratorSet of FreeMSA S2
g2 is Element of the carrier of S1
(FreeGen S2) . g2 is non empty set
the Sorts of (FreeMSA S2) . g2 is non empty set
(id the Sorts of (FreeMSA S2)) . g2 is non empty Relation-like the Sorts of (FreeMSA S2) . g2 -defined the Sorts of (FreeMSA S2) . g2 -valued Function-like total V29( the Sorts of (FreeMSA S2) . g2, the Sorts of (FreeMSA S2) . g2) Element of bool [:( the Sorts of (FreeMSA S2) . g2),( the Sorts of (FreeMSA S2) . g2):]
[:( the Sorts of (FreeMSA S2) . g2),( the Sorts of (FreeMSA S2) . g2):] is Relation-like set
bool [:( the Sorts of (FreeMSA S2) . g2),( the Sorts of (FreeMSA S2) . g2):] is set
((id the Sorts of (FreeMSA S2)) . g2) | ((FreeGen S2) . g2) is Relation-like (FreeGen S2) . g2 -defined the Sorts of (FreeMSA S2) . g2 -defined the Sorts of (FreeMSA S2) . g2 -valued Function-like Element of bool [:( the Sorts of (FreeMSA S2) . g2),( the Sorts of (FreeMSA S2) . g2):]
[:((FreeGen S2) . g2),( the Sorts of (FreeMSA S2) . g2):] is Relation-like set
bool [:((FreeGen S2) . g2),( the Sorts of (FreeMSA S2) . g2):] is set
dom (((id the Sorts of (FreeMSA S2)) . g2) | ((FreeGen S2) . g2)) is set
f is set
g is Element of the Sorts of (FreeMSA S2) . g2
FreeGen (g2,S2) is non empty Element of bool ((FreeSort S2) . g2)
FreeSort S2 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
(FreeSort S2) . g2 is non empty set
bool ((FreeSort S2) . g2) is set
S2 . g2 is non empty set
Af is set
[Af,g2] is set
{Af,g2} is non empty set
{Af} is non empty set
{{Af,g2},{Af}} is non empty set
root-tree [Af,g2] is Relation-like Function-like V117() set
(((id the Sorts of (FreeMSA S2)) . g2) | ((FreeGen S2) . g2)) . f is set
((id the Sorts of (FreeMSA S2)) . g2) . g is Element of the Sorts of (FreeMSA S2) . g2
id ( the Sorts of (FreeMSA S2) . g2) is non empty Relation-like the Sorts of (FreeMSA S2) . g2 -defined the Sorts of (FreeMSA S2) . g2 -valued Function-like one-to-one total V29( the Sorts of (FreeMSA S2) . g2, the Sorts of (FreeMSA S2) . g2) Element of bool [:( the Sorts of (FreeMSA S2) . g2),( the Sorts of (FreeMSA S2) . g2):]
(id ( the Sorts of (FreeMSA S2) . g2)) . g is Element of the Sorts of (FreeMSA S2) . g2
(id the carrier of S1) . g2 is Element of the carrier of S1
[Af,((id the carrier of S1) . g2)] is set
{Af,((id the carrier of S1) . g2)} is non empty set
{{Af,((id the carrier of S1) . g2)},{Af}} is non empty set
root-tree [Af,((id the carrier of S1) . g2)] is Relation-like Function-like V117() set
(S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) . g2 is Relation-like the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2 -defined the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2 -valued Function-like V29( the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2, the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2) Element of bool [:( the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2),( the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2):]
the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2 is non empty set
the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2 is set
[:( the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2),( the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2):] is Relation-like set
bool [:( the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2),( the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2):] is set
((S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) . g2) . g is set
((S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) . g2) | ((FreeGen S2) . g2) is Relation-like (FreeGen S2) . g2 -defined the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2 -defined the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2 -valued Function-like Element of bool [:( the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2),( the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2):]
(((S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) . g2) | ((FreeGen S2) . g2)) . f is set
dom (((S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) . g2) | ((FreeGen S2) . g2)) is set
(id the Sorts of (FreeMSA S2)) || (FreeGen S2) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of FreeGen S2, the Sorts of (FreeMSA S2)
((id the Sorts of (FreeMSA S2)) || (FreeGen S2)) . g2 is non empty Relation-like (FreeGen S2) . g2 -defined the Sorts of (FreeMSA S2) . g2 -valued Function-like total V29((FreeGen S2) . g2, the Sorts of (FreeMSA S2) . g2) Element of bool [:((FreeGen S2) . g2),( the Sorts of (FreeMSA S2) . g2):]
FreeGen ((id the carrier of S1) * S2) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total V131(S1, FreeMSA ((id the carrier of S1) * S2)) GeneratorSet of FreeMSA ((id the carrier of S1) * S2)
(S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) || (FreeGen ((id the carrier of S1) * S2)) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of FreeGen ((id the carrier of S1) * S2), the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1))
((S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) || (FreeGen ((id the carrier of S1) * S2))) . g2 is Relation-like (FreeGen ((id the carrier of S1) * S2)) . g2 -defined the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2 -valued Function-like V29((FreeGen ((id the carrier of S1) * S2)) . g2, the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2) Element of bool [:((FreeGen ((id the carrier of S1) * S2)) . g2),( the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2):]
(FreeGen ((id the carrier of S1) * S2)) . g2 is non empty set
[:((FreeGen ((id the carrier of S1) * S2)) . g2),( the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2):] is Relation-like set
bool [:((FreeGen ((id the carrier of S1) * S2)) . g2),( the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2):] is set
((S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) . g2) | ((FreeGen ((id the carrier of S1) * S2)) . g2) is Relation-like the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2 -defined (FreeGen ((id the carrier of S1) * S2)) . g2 -defined the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2 -defined the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2 -valued Function-like Element of bool [:( the Sorts of (FreeMSA ((id the carrier of S1) * S2)) . g2),( the Sorts of (S1,S1,(FreeMSA S2),(id the carrier of S1),(id the carrier' of S1)) . g2):]
((id the Sorts of (FreeMSA S2)) || (FreeGen S2)) . f2 is Relation-like Function-like set
((S1,S1,S2,(id the carrier of S1),(id the carrier' of S1)) || (FreeGen ((id the carrier of S1) * S2))) . f2 is Relation-like Function-like set
S3 is non empty non void feasible () ManySortedSign
the carrier of S3 is non empty set
S1 is non empty non void feasible () ManySortedSign
the carrier of S1 is non empty set
S2 is non empty non void feasible () ManySortedSign
the carrier of S2 is non empty set
[: the carrier of S1, the carrier of S2:] is Relation-like set
bool [: the carrier of S1, the carrier of S2:] is set
[: the carrier of S2, the carrier of S3:] is Relation-like set
bool [: the carrier of S2, the carrier of S3:] is set
X is non empty Relation-like non-empty non empty-yielding the carrier of S3 -defined Function-like total set
f1 is non empty Relation-like the carrier of S1 -defined the carrier of S2 -valued Function-like total V29( the carrier of S1, the carrier of S2) Element of bool [: the carrier of S1, the carrier of S2:]
g1 is Relation-like Function-like set
f2 is non empty Relation-like the carrier of S2 -defined the carrier of S3 -valued Function-like total V29( the carrier of S2, the carrier of S3) Element of bool [: the carrier of S2, the carrier of S3:]
f2 * f1 is non empty Relation-like the carrier of S1 -defined the carrier of S3 -valued Function-like total V29( the carrier of S1, the carrier of S3) Element of bool [: the carrier of S1, the carrier of S3:]
[: the carrier of S1, the carrier of S3:] is Relation-like set
bool [: the carrier of S1, the carrier of S3:] is set
f2 * X is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
(S1,S2,(f2 * X),f1,g1) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (f1 * (f2 * X))), the Sorts of (S1,S2,(FreeMSA (f2 * X)),f1,g1)
f1 * (f2 * X) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA (f1 * (f2 * X)) is strict non-empty V132(S1) MSAlgebra over S1
the Sorts of (FreeMSA (f1 * (f2 * X))) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA (f2 * X) is strict non-empty V132(S2) MSAlgebra over S2
(S1,S2,(FreeMSA (f2 * X)),f1,g1) is strict MSAlgebra over S1
the Sorts of (S1,S2,(FreeMSA (f2 * X)),f1,g1) is non empty Relation-like the carrier of S1 -defined Function-like total set
g2 is Relation-like Function-like set
g1 * g2 is Relation-like Function-like set
(S1,S3,X,(f2 * f1),(g1 * g2)) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA ((f2 * f1) * X)), the Sorts of (S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2))
(f2 * f1) * X is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA ((f2 * f1) * X) is strict non-empty V132(S1) MSAlgebra over S1
the Sorts of (FreeMSA ((f2 * f1) * X)) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeMSA X is strict non-empty V132(S3) MSAlgebra over S3
(S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2)) is strict MSAlgebra over S1
the Sorts of (S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2)) is non empty Relation-like the carrier of S1 -defined Function-like total set
(S2,S3,X,f2,g2) is non empty Relation-like the carrier of S2 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA (f2 * X)), the Sorts of (S2,S3,(FreeMSA X),f2,g2)
the Sorts of (FreeMSA (f2 * X)) is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
(S2,S3,(FreeMSA X),f2,g2) is strict MSAlgebra over S2
the Sorts of (S2,S3,(FreeMSA X),f2,g2) is non empty Relation-like the carrier of S2 -defined Function-like total set
f1 * (S2,S3,X,f2,g2) is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() set
(f1 * (S2,S3,X,f2,g2)) ** (S1,S2,(f2 * X),f1,g1) is Relation-like Function-like V53() V54() set
hf1 is set
the Sorts of (S2,S3,(FreeMSA X),f2,g2) . hf1 is set
the Sorts of (FreeMSA (f2 * X)) . hf1 is set
hh is Element of the carrier of S2
the Sorts of (S2,S3,(FreeMSA X),f2,g2) . hh is set
the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S3 -defined Function-like total set
f2 * the Sorts of (FreeMSA X) is non empty Relation-like non-empty non empty-yielding the carrier of S2 -defined Function-like total set
(f2 * the Sorts of (FreeMSA X)) . hh is non empty set
(S1,S2,(S2,S3,(FreeMSA X),f2,g2),f1,g1) is strict MSAlgebra over S1
Af1 is non-empty MSAlgebra over S1
the Sorts of Af1 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
Af is non-empty MSAlgebra over S1
the Sorts of Af is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
hf1 is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of Af1, the Sorts of Af
hh is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA ((f2 * f1) * X)), the Sorts of Af1
hf1 ** hh is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA ((f2 * f1) * X)), the Sorts of Af
s is Element of the carrier of S1
((f2 * f1) * X) . s is non empty set
DTConMSA ((f2 * f1) * X) is non empty strict with_terminals with_nonterminals with_useful_nonterminals L13()
the carrier of (DTConMSA ((f2 * f1) * X)) is non empty set
FinTrees the carrier of (DTConMSA ((f2 * f1) * X)) is non empty functional constituted-DTrees DTree-set of the carrier of (DTConMSA ((f2 * f1) * X))
S1 -Terms ((f2 * f1) * X) is non empty functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ((f2 * f1) * X)))
bool (FinTrees the carrier of (DTConMSA ((f2 * f1) * X))) is set
x is Element of ((f2 * f1) * X) . s
[x,s] is set
{x,s} is non empty set
{x} is non empty set
{{x,s},{x}} is non empty set
root-tree [x,s] is Relation-like Function-like V117() set
FreeSort ((f2 * f1) * X) is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like total set
FreeOper ((f2 * f1) * X) is non empty Relation-like the carrier' of S1 -defined Function-like total V53() V54() ManySortedFunction of the Arity of S1 * ((FreeSort ((f2 * f1) * X)) #), the ResultSort of S1 * (FreeSort ((f2 * f1) * X))
the carrier' of S1 is non empty set
the Arity of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like total V29( the carrier' of S1, the carrier of S1 * ) V53() V54() Element of bool [: the carrier' of S1,( the carrier of S1 *):]
the carrier of S1 * is non empty functional FinSequence-membered M12( the carrier of S1)
[: the carrier' of S1,( the carrier of S1 *):] is Relation-like set
bool [: the carrier' of S1,( the carrier of S1 *):] is set
(FreeSort ((f2 * f1) * X)) # is non empty Relation-like the carrier of S1 * -defined Function-like total set
the Arity of S1 * ((FreeSort ((f2 * f1) * X)) #) is non empty Relation-like the carrier' of S1 -defined Function-like total set
the ResultSort of S1 is non empty Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like total V29( the carrier' of S1, the carrier of S1) Element of bool [: the carrier' of S1, the carrier of S1:]
[: the carrier' of S1, the carrier of S1:] is Relation-like set
bool [: the carrier' of S1, the carrier of S1:] is set
the ResultSort of S1 * (FreeSort ((f2 * f1) * X)) is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like total set
MSAlgebra(# (FreeSort ((f2 * f1) * X)),(FreeOper ((f2 * f1) * X)) #) is strict MSAlgebra over S1
t is Relation-like the carrier of (DTConMSA ((f2 * f1) * X)) -valued Function-like V32() V117() Element of S1 -Terms ((f2 * f1) * X)
the_sort_of t is Element of the carrier of S1
(FreeSort ((f2 * f1) * X)) . s is non empty set
FreeSort (((f2 * f1) * X),s) is non empty functional constituted-DTrees Element of bool (TS (DTConMSA ((f2 * f1) * X)))
TS (DTConMSA ((f2 * f1) * X)) is functional constituted-DTrees Element of bool (FinTrees the carrier of (DTConMSA ((f2 * f1) * X)))
bool (TS (DTConMSA ((f2 * f1) * X))) is set
the Sorts of (FreeMSA ((f2 * f1) * X)) . s is non empty set
f1 . s is Element of the carrier of S2
(f2 * X) . (f1 . s) is non empty set
hf1h is non empty Relation-like the carrier of S1 -defined Function-like total V53() V54() ManySortedFunction of the Sorts of (FreeMSA ((f2 * f1) * X)), the Sorts of (S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2))
hf1h . s is Relation-like the Sorts of (FreeMSA ((f2 * f1) * X)) . s -defined the Sorts of (S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2)) . s -valued Function-like V29( the Sorts of (FreeMSA ((f2 * f1) * X)) . s, the Sorts of (S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2)) . s) Element of bool [:( the Sorts of (FreeMSA ((f2 * f1) * X)) . s),( the Sorts of (S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2)) . s):]
the Sorts of (S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2)) . s is set
[:( the Sorts of (FreeMSA ((f2 * f1) * X)) . s),( the Sorts of (S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2)) . s):] is Relation-like set
bool [:( the Sorts of (FreeMSA ((f2 * f1) * X)) . s),( the Sorts of (S1,S3,(FreeMSA X),(f2 * f1),(g1 * g2)) . s):] is set
(hf1h . s) . (root-tree [x,s]) is set
the Sorts of (FreeMSA (f1 * (f2 * X))) . s is non empty set
the Sorts of (S1,S2,(FreeMSA (f2 * X)),f1,g1) . s is set
the Sorts of Af1 . s is non empty set
the Sorts of Af . s is non empty set
(S1,S2,(f2 * X),f1,g1) . s is Relation-like the Sorts of (FreeMSA (f1 * (f2 * X))) . s -defined the Sorts of (S1,S2,(FreeMSA (f2 * X)),f1,g1) . s -valued Function-like V29( the Sorts of (FreeMSA (f1 * (f2 * X))) . s, the Sorts of (S1,S2,(FreeMSA (f2 * X)),f1,g1) . s) Element of bool [:( the Sorts of (FreeMSA (f1 * (f2 * X))) . s),( the Sorts of (S1,S2,(FreeMSA (f2 * X)),f1,g1) . s):]
[:( the Sorts of (FreeMSA (f1 * (f2 * X))) . s),( the Sorts of (S1,S2,(FreeMSA (f2 * X)),f1,g1) . s):] is Relation-like set
bool [:( the Sorts of (FreeMSA (f1 * (f2 * X))) . s),( the Sorts of (S1,S2,(FreeMSA (f2 * X)),f1,g1) . s):] is set
hf1 . s is non empty Relation-like the Sorts of Af1 . s -defined the Sorts of Af . s -valued Function-like total V29( the Sorts of Af1 . s, the Sorts of Af . s) Element of bool [:( the Sorts of Af1 . s),( the Sorts of Af . s):]
[:( the Sorts of Af1 . s),( the Sorts of Af . s):] is Relation-like set
bool [:( the Sorts of Af1 . s),( the Sorts of Af . s):] is set
(hf1 . s) * ((S1,S2,(f2 * X),f1,g1) . s) is Relation-like the Sorts of (FreeMSA (f1 * (f2 * X))) . s -defined the Sorts of Af . s -valued Function-like Element of bool [:( the Sorts of (FreeMSA (f1 * (f2 * X))) . s),( the Sorts of Af . s):]
[:( the Sorts of (FreeMSA (f1 * (f2 * X))) . s),( the Sorts of Af . s):] is Relation-like set
bool [:( the Sorts of (FreeMSA (f1 * (f2 * X))) . s),( the Sorts of Af . s):] is set
((hf1 . s) * ((S1,S2,(f2 * X),f1,g1) . s)) . (root-tree [x,s]) is set
((S1,S2,(f2 * X),f1,g1) . s) . (root-tree [x,s]) is set
(hf1 . s) . (((S1,S2,(f2 * X),f1,g1) . s) . (root-tree [x,s])) is set
[x,(f1 . s)] is set
{x,(f1 . s)} is non empty set
{{x,(f1 . s)},{x}} is non empty set
root-tree [x,(f1 . s)] is Relation-like Function-like V117() set
(hf1 . s) . (root-tree [x,(f1 . s)]) is set
(S2,S3,X,f2,g2) . (f1 . s) is Relation-like the Sorts of (FreeMSA (f2 * X)) . (f1 . s) -defined the Sorts of (S2,S3,(FreeMSA X),f2,g2) . (f1 . s) -valued Function-like V29( the Sorts of (FreeMSA (f2 * X)) . (f1 . s), the Sorts of (S2,S3,(FreeMSA X),f2,g2) . (f1 . s)) Element of bool [:( the Sorts of (FreeMSA (f2 * X)) . (f1 . s)),( the Sorts of (S2,S3,(FreeMSA X),f2,g2) . (f1 . s)):]
the Sorts of (FreeMSA (f2 * X)) . (f1 . s) is non empty set
the Sorts of (S2,S3,(FreeMSA X),f2,g2) . (f1 . s) is set
[:( the Sorts of (FreeMSA (f2 * X)) . (f1 . s)),( the Sorts of (S2,S3,(FreeMSA X),f2,g2) . (f1 . s)):] is Relation-like set
bool [:( the Sorts of (FreeMSA (f2 * X)) . (f1 . s)),( the Sorts of (S2,S3,(FreeMSA X),f2,g2) . (f1 . s)):] is set
((S2,S3,X,f2,g2) . (f1 . s)) . (root-tree [x,(f1 . s)]) is set
f2 . (f1 . s) is Element of the carrier of S3
[x,(f2 . (f1 . s))] is set
{x,(f2 . (f1 . s))} is non empty set
{{x,(f2 . (f1 . s))},{x}} is non empty set
root-tree [x,(f2 . (f1 . s))] is Relation-like Function-like V117() set
(f2 * f1) . s is Element of the carrier of S3
[x,((f2 * f1) . s)] is set
{x,((f2 * f1) . s)} is non empty set
{{x,((f2 * f1) . s)},{x}} is non empty set
root-tree [x,((f2 * f1) . s)] is Relation-like Function-like V117() set