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:]
[: