REAL is set
NAT is non empty V4() V5() V6() V35() V40() V41() Element of bool REAL
bool REAL is set
COMPLEX is set
NAT is non empty V4() V5() V6() V35() V40() V41() set
bool NAT is V35() set
bool NAT is V35() set
[:NAT,NAT:] is Relation-like V35() set
[:[:NAT,NAT:],NAT:] is Relation-like V35() set
bool [:[:NAT,NAT:],NAT:] is V35() set
K281() is non empty V80() L9()
the carrier of K281() is non empty set
K284() is Element of bool NAT
[:K284(),K284():] is Relation-like set
[:[:K284(),K284():],K284():] is Relation-like set
bool [:[:K284(),K284():],K284():] is set
{} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete Function-yielding Relation-yielding FuncSeq-like irreflexive set
1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
2 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
3 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
Seg 1 is non empty trivial V35() V42(1) Element of bool NAT
{1} is non empty trivial V42(1) set
Seg 2 is non empty V35() V42(2) Element of bool NAT
{1,2} is non empty set
0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete Function-yielding Relation-yielding FuncSeq-like irreflexive Element of NAT
S is non empty feasible ManySortedSign
the carrier of S is non empty set
S is set
A is Relation-like S -defined Function-like total set
R is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,A
s is Relation-like S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of A,A
s ** R is Relation-like Function-like Function-yielding Relation-yielding set
dom s is Element of bool S
bool S is set
dom R is Element of bool S
proj1 (s ** R) is set
S /\ S is set
b is Relation-like S -defined Function-like total set
P is set
b . P is set
A . P is set
[:(A . P),(A . P):] is Relation-like set
bool [:(A . P),(A . P):] is set
R . P is Relation-like Function-like set
s . P is Relation-like Function-like set
P is Relation-like A . P -defined A . P -valued Function-like total V29(A . P,A . P) Element of bool [:(A . P),(A . P):]
P is Relation-like A . P -defined A . P -valued Function-like total V29(A . P,A . P) Element of bool [:(A . P),(A . P):]
P * P is Relation-like A . P -defined A . P -valued Function-like total V29(A . P,A . P) Element of bool [:(A . P),(A . P):]
S is non empty non void feasible ManySortedSign
the carrier' of S is non empty set
A is MSAlgebra over S
R is Element of the carrier' of S
Args (R,A) is Element of proj2 K225( the carrier of S, the Sorts of A)
the carrier of S is non empty set
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
proj2 K225( the carrier of S, the Sorts of A) is non empty set
s is set
the_arity_of R is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
(the_arity_of R) * the Sorts of A is Relation-like NAT -defined dom (the_arity_of R) -defined Function-like total set
dom (the_arity_of R) is Element of bool NAT
product ((the_arity_of R) * the Sorts of A) is set
dom ((the_arity_of R) * the Sorts of A) is Element of bool NAT
a is Relation-like Function-like set
proj1 a is set
S is non empty non void feasible ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
R is Element of the carrier' of S
Args (R,A) is Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
proj2 K225( the carrier of S, the Sorts of A) is non empty set
the_arity_of R is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
dom (the_arity_of R) is Element of bool NAT
s is Relation-like Function-like set
proj1 s is set
(the_arity_of R) * the Sorts of A is Relation-like NAT -defined dom (the_arity_of R) -defined Function-like total set
product ((the_arity_of R) * the Sorts of A) is set
dom ((the_arity_of R) * the Sorts of A) is Element of bool NAT
a is Relation-like Function-like set
proj1 a is set
a is set
s . a is set
(the_arity_of R) /. a is Element of the carrier of S
the Sorts of A . ((the_arity_of R) /. a) is set
(the_arity_of R) . a is set
((the_arity_of R) * the Sorts of A) . a is set
b is Relation-like Function-like set
proj1 b is set
S is non empty non void feasible ManySortedSign
S is non empty non void feasible ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty set
A is Element of the carrier' of S
the_arity_of A is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
dom (the_arity_of A) is Element of bool NAT
R is MSAlgebra over S
Args (A,R) is Element of proj2 K225( the carrier of S, the Sorts of R)
the Sorts of R is non empty Relation-like the carrier of S -defined Function-like total set
K225( the carrier of S, the Sorts of R) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of R) is non empty set
(the_arity_of A) * the Sorts of R is Relation-like NAT -defined dom (the_arity_of A) -defined Function-like total set
dom ((the_arity_of A) * the Sorts of R) is Element of bool NAT
product ((the_arity_of A) * the Sorts of R) is set
s is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of A) . s is set
the Sorts of R . ((the_arity_of A) . s) is set
((the_arity_of A) * the Sorts of R) . s is set
(the_arity_of A) /. s is Element of the carrier of S
proj2 ((the_arity_of A) * the Sorts of R) is set
the Sorts of R . ((the_arity_of A) /. s) is set
s is set
((the_arity_of A) * the Sorts of R) . s is set
a is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of A) /. a is Element of the carrier of S
(the_arity_of A) . a is set
the Sorts of R . ((the_arity_of A) /. a) is set
S is non empty non void feasible ManySortedSign
A is MSAlgebra over S
the carrier' of S is non empty set
s is Element of the carrier' of S
Args (s,A) is Element of proj2 K225( the carrier of S, the Sorts of A)
the carrier of S is non empty set
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
proj2 K225( the carrier of S, the Sorts of A) is non empty set
Result (s,A) is Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
R is non-empty MSAlgebra over S
Result (s,R) is non empty Element of proj2 the Sorts of R
the Sorts of R is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
proj2 the Sorts of R is non empty set
S is non empty non void feasible ManySortedSign
the non-empty (S) MSAlgebra over S is non-empty (S) MSAlgebra over S
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
id the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
id the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of A
R is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of A
( the carrier of S, the Sorts of A,R,s) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of A
b is Element of the carrier' of S
Args (b,A) is Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
proj2 K225( the carrier of S, the Sorts of A) is non empty set
P is Element of Args (b,A)
R # P is Element of Args (b,A)
s # (R # P) is Element of Args (b,A)
( the carrier of S, the Sorts of A,R,s) # P is Element of Args (b,A)
P is Relation-like Function-like set
proj1 P is set
the_arity_of b is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
dom (the_arity_of b) is Element of bool NAT
(the_arity_of b) * the Sorts of A is Relation-like NAT -defined dom (the_arity_of b) -defined Function-like total set
dom ((the_arity_of b) * the Sorts of A) is Element of bool NAT
product ((the_arity_of b) * the Sorts of A) is set
s is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() set
(the_arity_of b) /. s is Element of the carrier of S
the Sorts of A . ((the_arity_of b) /. s) is set
[:( the Sorts of A . ((the_arity_of b) /. s)),( the Sorts of A . ((the_arity_of b) /. s)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of b) /. s)),( the Sorts of A . ((the_arity_of b) /. s)):] is set
R . ((the_arity_of b) /. s) is Relation-like the Sorts of A . ((the_arity_of b) /. s) -defined the Sorts of A . ((the_arity_of b) /. s) -valued Function-like total V29( the Sorts of A . ((the_arity_of b) /. s), the Sorts of A . ((the_arity_of b) /. s)) Element of bool [:( the Sorts of A . ((the_arity_of b) /. s)),( the Sorts of A . ((the_arity_of b) /. s)):]
s . ((the_arity_of b) /. s) is Relation-like the Sorts of A . ((the_arity_of b) /. s) -defined the Sorts of A . ((the_arity_of b) /. s) -valued Function-like total V29( the Sorts of A . ((the_arity_of b) /. s), the Sorts of A . ((the_arity_of b) /. s)) Element of bool [:( the Sorts of A . ((the_arity_of b) /. s)),( the Sorts of A . ((the_arity_of b) /. s)):]
( the carrier of S, the Sorts of A,R,s) . ((the_arity_of b) /. s) is Relation-like the Sorts of A . ((the_arity_of b) /. s) -defined the Sorts of A . ((the_arity_of b) /. s) -valued Function-like total V29( the Sorts of A . ((the_arity_of b) /. s), the Sorts of A . ((the_arity_of b) /. s)) Element of bool [:( the Sorts of A . ((the_arity_of b) /. s)),( the Sorts of A . ((the_arity_of b) /. s)):]
x is Relation-like the Sorts of A . ((the_arity_of b) /. s) -defined the Sorts of A . ((the_arity_of b) /. s) -valued Function-like total V29( the Sorts of A . ((the_arity_of b) /. s), the Sorts of A . ((the_arity_of b) /. s)) Element of bool [:( the Sorts of A . ((the_arity_of b) /. s)),( the Sorts of A . ((the_arity_of b) /. s)):]
y is Relation-like the Sorts of A . ((the_arity_of b) /. s) -defined the Sorts of A . ((the_arity_of b) /. s) -valued Function-like total V29( the Sorts of A . ((the_arity_of b) /. s), the Sorts of A . ((the_arity_of b) /. s)) Element of bool [:( the Sorts of A . ((the_arity_of b) /. s)),( the Sorts of A . ((the_arity_of b) /. s)):]
y * x is Relation-like the Sorts of A . ((the_arity_of b) /. s) -defined the Sorts of A . ((the_arity_of b) /. s) -valued Function-like total V29( the Sorts of A . ((the_arity_of b) /. s), the Sorts of A . ((the_arity_of b) /. s)) Element of bool [:( the Sorts of A . ((the_arity_of b) /. s)),( the Sorts of A . ((the_arity_of b) /. s)):]
P . s is set
x . (P . s) is set
P is Relation-like Function-like set
P . s is set
proj1 P is set
y . (P . s) is set
i is Relation-like Function-like set
i . s is set
(the_arity_of b) . s is set
the Sorts of A . ((the_arity_of b) . s) is set
((the_arity_of b) * the Sorts of A) . s is set
(( the carrier of S, the Sorts of A,R,s) . ((the_arity_of b) /. s)) . (P . s) is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
( the carrier of S, the Sorts of A,R,s) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of A
the carrier' of S is non empty set
a is Element of the carrier' of S
Args (a,A) is Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
proj2 K225( the carrier of S, the Sorts of A) is non empty set
the_result_sort_of a is Element of the carrier of S
( the carrier of S, the Sorts of A,R,s) . (the_result_sort_of a) is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . (the_result_sort_of a), the Sorts of A . (the_result_sort_of a)) Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
the Sorts of A . (the_result_sort_of a) is set
[:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):] is set
Den (a,A) is Relation-like Args (a,A) -defined Result (a,A) -valued Function-like V29( Args (a,A), Result (a,A)) Element of bool [:(Args (a,A)),(Result (a,A)):]
Result (a,A) is Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (a,A)),(Result (a,A)):] is Relation-like set
bool [:(Args (a,A)),(Result (a,A)):] is set
P is Element of Args (a,A)
(Den (a,A)) . P is set
(( the carrier of S, the Sorts of A,R,s) . (the_result_sort_of a)) . ((Den (a,A)) . P) is set
( the carrier of S, the Sorts of A,R,s) # P is Element of Args (a,A)
(Den (a,A)) . (( the carrier of S, the Sorts of A,R,s) # P) is set
R . (the_result_sort_of a) is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . (the_result_sort_of a), the Sorts of A . (the_result_sort_of a)) Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
s . (the_result_sort_of a) is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . (the_result_sort_of a), the Sorts of A . (the_result_sort_of a)) Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
i is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . (the_result_sort_of a), the Sorts of A . (the_result_sort_of a)) Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
dom i is Element of bool ( the Sorts of A . (the_result_sort_of a))
bool ( the Sorts of A . (the_result_sort_of a)) is set
i . ((Den (a,A)) . P) is set
dom (Den (a,A)) is Element of bool (Args (a,A))
bool (Args (a,A)) is set
P is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . (the_result_sort_of a), the Sorts of A . (the_result_sort_of a)) Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
P is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . (the_result_sort_of a), the Sorts of A . (the_result_sort_of a)) Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
P * P is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . (the_result_sort_of a), the Sorts of A . (the_result_sort_of a)) Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
P . ((Den (a,A)) . P) is set
P . (P . ((Den (a,A)) . P)) is set
R # P is Element of Args (a,A)
(Den (a,A)) . (R # P) is set
(s . (the_result_sort_of a)) . ((Den (a,A)) . (R # P)) is set
s # (R # P) is Element of Args (a,A)
(Den (a,A)) . (s # (R # P)) is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is MSAlgebra over S
R is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
s ** R is Relation-like Function-like Function-yielding Relation-yielding set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
the carrier' of S is non empty set
A is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
A is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
R is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
S is non empty non void feasible ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty set
A is Element of the carrier' of S
the_arity_of A is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
R is MSAlgebra over S
Args (A,R) is Element of proj2 K225( the carrier of S, the Sorts of R)
the Sorts of R is non empty Relation-like the carrier of S -defined Function-like total set
K225( the carrier of S, the Sorts of R) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of R) is non empty set
(the_arity_of A) * the Sorts of R is Relation-like NAT -defined dom (the_arity_of A) -defined Function-like total set
dom (the_arity_of A) is Element of bool NAT
dom ((the_arity_of A) * the Sorts of R) is Element of bool NAT
s is Relation-like Function-like set
proj1 s is set
a is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of A) /. a is Element of the carrier of S
the Sorts of R . ((the_arity_of A) /. a) is set
b is Element of the Sorts of R . ((the_arity_of A) /. a)
s +* (a,b) is Relation-like Function-like set
product ((the_arity_of A) * the Sorts of R) is set
P is set
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
((the_arity_of A) * the Sorts of R) . P is set
(the_arity_of A) . P is set
the Sorts of R . ((the_arity_of A) . P) is set
(the_arity_of A) /. P is Element of the carrier of S
((the_arity_of A) * the Sorts of R) . P is set
(s +* (a,b)) . P is set
(s +* (a,b)) . P is set
s . P is set
proj1 (s +* (a,b)) is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
R is MSAlgebra over S
the Sorts of R is non empty Relation-like the carrier of S -defined Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of R
a is Element of the carrier' of S
Args (a,A) is Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
proj2 K225( the carrier of S, the Sorts of A) is non empty set
Args (a,R) is Element of proj2 K225( the carrier of S, the Sorts of R)
K225( the carrier of S, the Sorts of R) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of R) is non empty set
the_arity_of a is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
dom (the_arity_of a) is Element of bool NAT
b is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of a) /. b is Element of the carrier of S
the Sorts of A . ((the_arity_of a) /. b) is set
s . ((the_arity_of a) /. b) is Relation-like the Sorts of A . ((the_arity_of a) /. b) -defined the Sorts of R . ((the_arity_of a) /. b) -valued Function-like V29( the Sorts of A . ((the_arity_of a) /. b), the Sorts of R . ((the_arity_of a) /. b)) Element of bool [:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . ((the_arity_of a) /. b)):]
the Sorts of R . ((the_arity_of a) /. b) is set
[:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . ((the_arity_of a) /. b)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . ((the_arity_of a) /. b)):] is set
P is Element of the Sorts of A . ((the_arity_of a) /. b)
(s . ((the_arity_of a) /. b)) . P is set
S is non empty non void feasible ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty set
A is Element of the carrier' of S
the_arity_of A is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
dom (the_arity_of A) is Element of bool NAT
R is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of A) /. R is Element of the carrier of S
s is MSAlgebra over S
the Sorts of s is non empty Relation-like the carrier of S -defined Function-like total set
a is MSAlgebra over S
the Sorts of a is non empty Relation-like the carrier of S -defined Function-like total set
Args (A,s) is Element of proj2 K225( the carrier of S, the Sorts of s)
K225( the carrier of S, the Sorts of s) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of s) is non empty set
Args (A,a) is Element of proj2 K225( the carrier of S, the Sorts of a)
K225( the carrier of S, the Sorts of a) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of a) is non empty set
the Sorts of s . ((the_arity_of A) /. R) is set
b is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of s, the Sorts of a
b . ((the_arity_of A) /. R) is Relation-like the Sorts of s . ((the_arity_of A) /. R) -defined the Sorts of a . ((the_arity_of A) /. R) -valued Function-like V29( the Sorts of s . ((the_arity_of A) /. R), the Sorts of a . ((the_arity_of A) /. R)) Element of bool [:( the Sorts of s . ((the_arity_of A) /. R)),( the Sorts of a . ((the_arity_of A) /. R)):]
the Sorts of a . ((the_arity_of A) /. R) is set
[:( the Sorts of s . ((the_arity_of A) /. R)),( the Sorts of a . ((the_arity_of A) /. R)):] is Relation-like set
bool [:( the Sorts of s . ((the_arity_of A) /. R)),( the Sorts of a . ((the_arity_of A) /. R)):] is set
P is Element of Args (A,s)
b # P is Element of Args (A,a)
P is Element of Args (A,s)
b # P is Element of Args (A,a)
P is Relation-like Function-like set
proj1 P is set
i is Relation-like Function-like set
s is Relation-like Function-like set
x is Relation-like Function-like set
x . R is set
s +* (R,(x . R)) is Relation-like Function-like set
proj1 i is set
a is Element of the Sorts of s . ((the_arity_of A) /. R)
i +* (R,a) is Relation-like Function-like set
(b . ((the_arity_of A) /. R)) . a is set
P . R is set
y is Relation-like Function-like set
proj1 y is set
b is set
u is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
P . u is set
i . u is set
x . u is set
(the_arity_of A) /. u is Element of the carrier of S
b . ((the_arity_of A) /. u) is Relation-like the Sorts of s . ((the_arity_of A) /. u) -defined the Sorts of a . ((the_arity_of A) /. u) -valued Function-like V29( the Sorts of s . ((the_arity_of A) /. u), the Sorts of a . ((the_arity_of A) /. u)) Element of bool [:( the Sorts of s . ((the_arity_of A) /. u)),( the Sorts of a . ((the_arity_of A) /. u)):]
the Sorts of s . ((the_arity_of A) /. u) is set
the Sorts of a . ((the_arity_of A) /. u) is set
[:( the Sorts of s . ((the_arity_of A) /. u)),( the Sorts of a . ((the_arity_of A) /. u)):] is Relation-like set
bool [:( the Sorts of s . ((the_arity_of A) /. u)),( the Sorts of a . ((the_arity_of A) /. u)):] is set
(b . ((the_arity_of A) /. u)) . (P . u) is set
x . b is set
s . b is set
proj1 s is set
b is set
x . b is set
(s +* (R,(x . R))) . b is set
x . b is set
s . b is set
(s +* (R,(x . R))) . b is set
proj1 x is set
S is non empty non void feasible ManySortedSign
the carrier' of S is non empty set
s is MSAlgebra over S
the Sorts of s is non empty Relation-like the carrier of S -defined Function-like total set
the carrier of S is non empty set
A is Element of the carrier' of S
the_arity_of A is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
R is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of A) /. R is Element of the carrier of S
the Sorts of s . ((the_arity_of A) /. R) is set
Den (A,s) is Relation-like Args (A,s) -defined Result (A,s) -valued Function-like V29( Args (A,s), Result (A,s)) Element of bool [:(Args (A,s)),(Result (A,s)):]
Args (A,s) is Element of proj2 K225( the carrier of S, the Sorts of s)
K225( the carrier of S, the Sorts of s) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of s) is non empty set
Result (A,s) is Element of proj2 the Sorts of s
proj2 the Sorts of s is non empty set
[:(Args (A,s)),(Result (A,s)):] is Relation-like set
bool [:(Args (A,s)),(Result (A,s)):] is set
a is Relation-like Function-like set
b is Relation-like Function-like set
proj1 b is set
b is Relation-like Function-like set
proj1 b is set
P is Relation-like Function-like set
proj1 P is set
P is set
b . P is set
a +* (R,P) is Relation-like Function-like set
(Den (A,s)) . (a +* (R,P)) is set
P . P is set
S is non empty non void feasible ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty set
A is Element of the carrier' of S
the_arity_of A is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
the_result_sort_of A is Element of the carrier of S
R is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of A) /. R is Element of the carrier of S
s is (S) MSAlgebra over S
Args (A,s) is Element of proj2 K225( the carrier of S, the Sorts of s)
the Sorts of s is non empty Relation-like the carrier of S -defined Function-like total set
K225( the carrier of S, the Sorts of s) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of s) is non empty set
the Sorts of s . ((the_arity_of A) /. R) is set
the Sorts of s . (the_result_sort_of A) is set
[:( the Sorts of s . ((the_arity_of A) /. R)),( the Sorts of s . (the_result_sort_of A)):] is Relation-like set
bool [:( the Sorts of s . ((the_arity_of A) /. R)),( the Sorts of s . (the_result_sort_of A)):] is set
a is Relation-like Function-like set
(S,A,R,s,a) is Relation-like Function-like set
Result (A,s) is Element of proj2 the Sorts of s
proj2 the Sorts of s is non empty set
proj1 (S,A,R,s,a) is set
proj2 (S,A,R,s,a) is set
b is set
P is set
(S,A,R,s,a) . P is set
P is Element of the Sorts of s . ((the_arity_of A) /. R)
a +* (R,P) is Relation-like Function-like set
Den (A,s) is Relation-like Args (A,s) -defined Result (A,s) -valued Function-like V29( Args (A,s), Result (A,s)) Element of bool [:(Args (A,s)),(Result (A,s)):]
[:(Args (A,s)),(Result (A,s)):] is Relation-like set
bool [:(Args (A,s)),(Result (A,s)):] is set
(Den (A,s)) . (a +* (R,P)) is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is Element of the carrier of S
R is Element of the carrier of S
s is (S) MSAlgebra over S
the Sorts of s is non empty Relation-like the carrier of S -defined Function-like total set
the Sorts of s . A is set
the Sorts of s . R is set
[:( the Sorts of s . A),( the Sorts of s . R):] is Relation-like set
bool [:( the Sorts of s . A),( the Sorts of s . R):] is set
a is Relation-like Function-like set
the carrier' of S is non empty set
b is Element of the carrier' of S
the_result_sort_of b is Element of the carrier of S
the_arity_of b is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
dom (the_arity_of b) is Element of bool NAT
Args (b,s) is Element of proj2 K225( the carrier of S, the Sorts of s)
K225( the carrier of S, the Sorts of s) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of s) is non empty set
Result (b,s) is Element of proj2 the Sorts of s
proj2 the Sorts of s is non empty set
the Sorts of s . (the_result_sort_of b) is set
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of b) /. P is Element of the carrier of S
P is Relation-like Function-like set
(S,b,P,s,P) is Relation-like Function-like set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is Element of the carrier of S
R is Element of the carrier of S
[A,R] is V26() set
{A,R} is non empty set
{A} is non empty trivial V42(1) set
{{A,R},{A}} is non empty set
s is MSAlgebra over S
a is Relation-like Function-like set
the carrier' of S is non empty set
b is Element of the carrier' of S
the_result_sort_of b is Element of the carrier of S
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
the_arity_of b is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
dom (the_arity_of b) is Element of bool NAT
(the_arity_of b) /. P is Element of the carrier of S
P is Relation-like Function-like set
Args (b,s) is Element of proj2 K225( the carrier of S, the Sorts of s)
the Sorts of s is non empty Relation-like the carrier of S -defined Function-like total set
K225( the carrier of S, the Sorts of s) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of s) is non empty set
(S,b,P,s,P) is Relation-like Function-like set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is Element of the carrier of S
R is Element of the carrier of S
[A,R] is V26() set
{A,R} is non empty set
{A} is non empty trivial V42(1) set
{{A,R},{A}} is non empty set
s is non-empty (S) MSAlgebra over S
the carrier' of S is non empty set
a is Element of the carrier' of S
the_result_sort_of a is Element of the carrier of S
the_arity_of a is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
dom (the_arity_of a) is Element of bool NAT
Args (a,s) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of s)
the Sorts of s is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
K225( the carrier of S, the Sorts of s) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of s) is non empty set
the Relation-like Function-like Element of Args (a,s) is Relation-like Function-like Element of Args (a,s)
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of a) /. P is Element of the carrier of S
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of a) /. P is Element of the carrier of S
(S,a,P,s, the Relation-like Function-like Element of Args (a,s)) is Relation-like Function-like set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is (S) MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
R is Element of the carrier of S
s is Element of the carrier of S
the Sorts of A . R is set
the Sorts of A . s is set
[:( the Sorts of A . R),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . R),( the Sorts of A . s):] is set
a is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of (S)
len a is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a . 1 is set
a . (len a) is set
b is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
len b is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(len b) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
dom b is Element of bool NAT
compose (b,( the Sorts of A . R)) is Relation-like Function-like set
id ( the Sorts of A . R) is Relation-like the Sorts of A . R -defined the Sorts of A . R -valued Function-like one-to-one total V29( the Sorts of A . R, the Sorts of A . R) V30( the Sorts of A . R) V31( the Sorts of A . R, the Sorts of A . R) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . R),( the Sorts of A . R):]
[:( the Sorts of A . R),( the Sorts of A . R):] is Relation-like set
bool [:( the Sorts of A . R),( the Sorts of A . R):] is set
proj2 b is set
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
dom a is non empty Element of bool NAT
a . (1 + 1) is set
[(a . 1),(a . (1 + 1))] is V26() set
{(a . 1),(a . (1 + 1))} is non empty set
{(a . 1)} is non empty trivial V42(1) set
{{(a . 1),(a . (1 + 1))},{(a . 1)}} is non empty set
b . 1 is Relation-like Function-like set
Seg (len a) is non empty V35() V42( len a) Element of bool NAT
i is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len i is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
dom i is Element of bool NAT
P is Element of the carrier of S
P is Element of the carrier of S
P is Relation-like Function-like set
the Sorts of A . P is set
s is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
i . s is set
s + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
i . (s + 1) is set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a . s is set
a . (s + 1) is set
[(a . s),(a . (s + 1))] is V26() set
{(a . s),(a . (s + 1))} is non empty set
{(a . s)} is non empty trivial V42(1) set
{{(a . s),(a . (s + 1))},{(a . s)}} is non empty set
b . s is Relation-like Function-like set
x is Element of the carrier of S
y is Element of the carrier of S
a is Relation-like Function-like set
the Sorts of A . y is set
i . 0 is set
s is set
proj1 i is set
i . s is set
Seg (len b) is V35() V42( len b) Element of bool NAT
s is non empty Relation-like non-empty NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len s is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
x is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
b . x is Relation-like Function-like set
s . x is set
x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
s . (x + 1) is set
K97((s . x),(s . (x + 1))) is functional set
a . x is set
a . (x + 1) is set
[(a . x),(a . (x + 1))] is V26() set
{(a . x),(a . (x + 1))} is non empty set
{(a . x)} is non empty trivial V42(1) set
{{(a . x),(a . (x + 1))},{(a . x)}} is non empty set
b is Element of the carrier of S
the Sorts of A . b is set
a is Element of the carrier of S
y is Relation-like Function-like set
the Sorts of A . a is set
[:( the Sorts of A . a),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . b):] is set
s . 1 is set
x is Relation-like non-empty NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding FuncSeq-like FuncSequence of s
compose (x,( the Sorts of A . R)) is Relation-like Function-like set
proj1 (compose (x,( the Sorts of A . R))) is set
len s is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
s . (len s) is set
proj2 (compose (x,( the Sorts of A . R))) is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
R is Element of the carrier of S
s is Element of the carrier of S
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
the Sorts of A . R is non empty set
the Sorts of A . s is non empty set
[:( the Sorts of A . R),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . R),( the Sorts of A . s):] is set
a is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of (S)
a . 1 is set
len a is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a . (len a) is set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
b is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() set
1 + b is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
dom a is non empty Element of bool NAT
Seg (len a) is non empty V35() V42( len a) Element of bool NAT
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
Seg P is V35() V42(P) Element of bool NAT
P is set
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
P + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a . P is set
a . (P + 1) is set
[(a . P),(a . (P + 1))] is V26() set
{(a . P),(a . (P + 1))} is non empty set
{(a . P)} is non empty trivial V42(1) set
{{(a . P),(a . (P + 1))},{(a . P)}} is non empty set
the carrier' of S is non empty set
s is Element of the carrier of S
i is Element of the carrier of S
x is Element of the carrier' of S
the_result_sort_of x is Element of the carrier of S
the_arity_of x is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
dom (the_arity_of x) is Element of bool NAT
Args (x,A) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of A) is non empty set
the Relation-like Function-like Element of Args (x,A) is Relation-like Function-like Element of Args (x,A)
a is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of x) /. a is Element of the carrier of S
a is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of x) /. a is Element of the carrier of S
(S,x,a,A, the Relation-like Function-like Element of Args (x,A)) is Relation-like Function-like set
P is Relation-like Function-like set
proj1 P is set
P is set
P . P is set
i is Relation-like Function-like set
y is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
s is Element of the carrier of S
a . y is set
x is Element of the carrier of S
y + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a . (y + 1) is set
i is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
P is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
dom P is Element of bool NAT
P . i is Relation-like Function-like set
s is Relation-like Function-like set
x is Element of the carrier of S
a . i is set
y is Element of the carrier of S
i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a . (i + 1) is set
a is Relation-like Function-like set
v is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
b is Element of the carrier of S
a . v is set
u is Element of the carrier of S
v + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a . (v + 1) is set
len P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
compose (P,( the Sorts of A . R)) is Relation-like Function-like set
i is non empty Relation-like the Sorts of A . R -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . R, the Sorts of A . s) Element of bool [:( the Sorts of A . R),( the Sorts of A . s):]
(len P) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
s is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
x is Relation-like Function-like set
P . s is Relation-like Function-like set
y is Element of the carrier of S
a . s is set
a is Element of the carrier of S
s + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a . (s + 1) is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is Element of the carrier of S
s is Element of the carrier of S
the Sorts of A . R is non empty set
the Sorts of A . s is non empty set
a is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of (S)
len a is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a . 1 is set
a . (len a) is set
b is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
len b is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(len b) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
dom b is Element of bool NAT
compose (b,( the Sorts of A . R)) is Relation-like Function-like set
[:( the Sorts of A . R),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . R),( the Sorts of A . s):] is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is Element of the carrier of S
the Sorts of A . R is non empty set
id ( the Sorts of A . R) is non empty Relation-like the Sorts of A . R -defined the Sorts of A . R -valued Function-like one-to-one total V29( the Sorts of A . R, the Sorts of A . R) V30( the Sorts of A . R) V31( the Sorts of A . R, the Sorts of A . R) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . R),( the Sorts of A . R):]
[:( the Sorts of A . R),( the Sorts of A . R):] is Relation-like set
bool [:( the Sorts of A . R),( the Sorts of A . R):] is set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
<*R*> is non empty trivial Relation-like NAT -defined the carrier of S -valued Function-like constant V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of S
len <*R*> is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
len {} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete Function-yielding Relation-yielding FuncSeq-like irreflexive Element of NAT
dom {} is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete Function-yielding Relation-yielding FuncSeq-like irreflexive Element of bool NAT
s is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
a is Relation-like Function-like set
{} . s is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete Function-yielding Relation-yielding FuncSeq-like irreflexive set
b is Element of the carrier of S
<*R*> . s is set
P is Element of the carrier of S
s + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
<*R*> . (s + 1) is set
<*R*> . 1 is set
compose ({},( the Sorts of A . R)) is Relation-like Function-like set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is Element of the carrier of S
s is Element of the carrier of S
the Sorts of A . R is non empty set
the Sorts of A . s is non empty set
a is Relation-like Function-like set
<*R,s*> is non empty Relation-like NAT -defined Function-like V35() V42(2) FinSequence-like FinSubsequence-like set
len <*R,s*> is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
<*a*> is non empty trivial Relation-like NAT -defined Function-like constant V35() V42(1) FinSequence-like FinSubsequence-like Function-yielding Relation-yielding FuncSeq-like set
len <*a*> is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
[:( the Sorts of A . R),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . R),( the Sorts of A . s):] is set
<*R,s*> . 2 is set
<*R,s*> . 1 is set
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
dom <*a*> is non empty trivial V42(1) Element of bool NAT
P is Relation-like Function-like set
<*a*> . P is Relation-like Function-like set
P is Element of the carrier of S
<*R,s*> . P is set
i is Element of the carrier of S
P + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
<*R,s*> . (P + 1) is set
b is non empty Relation-like the Sorts of A . R -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . R, the Sorts of A . s) Element of bool [:( the Sorts of A . R),( the Sorts of A . s):]
dom b is non empty Element of bool ( the Sorts of A . R)
bool ( the Sorts of A . R) is set
compose (<*a*>,( the Sorts of A . R)) is Relation-like Function-like set
[R,s] is V26() set
{R,s} is non empty set
{R} is non empty trivial V42(1) set
{{R,s},{R}} is non empty set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is Element of the carrier of S
s is Element of the carrier of S
a is Element of the carrier of S
the Sorts of A . R is non empty set
the Sorts of A . s is non empty set
the Sorts of A . a is non empty set
b is non empty Relation-like the Sorts of A . R -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . R, the Sorts of A . s) (S,A,R,s)
P is non empty Relation-like the Sorts of A . s -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . s, the Sorts of A . a) (S,A,s,a)
P * b is non empty Relation-like the Sorts of A . R -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . R, the Sorts of A . a) Element of bool [:( the Sorts of A . R),( the Sorts of A . a):]
[:( the Sorts of A . R),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . R),( the Sorts of A . a):] is set
P is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
compose (P,( the Sorts of A . R)) is Relation-like Function-like set
P is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of (S)
len P is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
len P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(len P) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . 1 is set
P . (len P) is set
dom P is Element of bool NAT
s is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
compose (s,( the Sorts of A . s)) is Relation-like Function-like set
i is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of (S)
len i is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
len s is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(len s) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
i . 1 is set
i . (len i) is set
dom s is Element of bool NAT
P $^ i is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
x is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of (S)
len x is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
x . 1 is set
x . (len x) is set
P ^ s is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
y is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
compose (y,( the Sorts of A . R)) is Relation-like Function-like set
len y is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(len y) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
dom y is Element of bool NAT
proj2 b is non empty set
(len P) + (len s) is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
a is set
<*a*> is non empty trivial Relation-like NAT -defined Function-like constant V35() V42(1) FinSequence-like FinSubsequence-like set
b is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
<*a*> ^ b is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len b is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(len b) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
u is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
v is set
<*v*> is non empty trivial Relation-like NAT -defined Function-like constant V35() V42(1) FinSequence-like FinSubsequence-like set
u ^ <*v*> is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
u ^ i is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
len <*v*> is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
len u is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(len u) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
(len P) + (len i) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P ^ b is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
Seg (len u) is V35() V42( len u) Element of bool NAT
dom u is Element of bool NAT
u . 1 is set
{} ^ i is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
dom i is non empty Element of bool NAT
h is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
y . h is Relation-like Function-like set
x . h is set
h + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
x . (h + 1) is set
t is Relation-like Function-like set
s1 is Element of the carrier of S
s2 is Element of the carrier of S
dom P is non empty Element of bool NAT
P . (h + 1) is set
P . h is set
P . h is Relation-like Function-like set
k is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() set
((len P) + 1) + k is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
k + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
(k + 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
(len P) + ((k + 1) + 1) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
1 + k is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
(len P) + (1 + k) is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
i . (k + 1) is set
i . ((k + 1) + 1) is set
s . (k + 1) is Relation-like Function-like set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is Element of the carrier of S
s is Element of the carrier of S
the Sorts of A . R is non empty set
the Sorts of A . s is non empty set
a is Element of the carrier of S
the Sorts of A . a is non empty set
b is non empty Relation-like the Sorts of A . R -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . R, the Sorts of A . s) (S,A,R,s)
P is Relation-like Function-like set
b * P is Relation-like the Sorts of A . R -defined Function-like set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
s is Element of the carrier of S
a is Element of the carrier of S
R is Element of the carrier of S
the Sorts of A . s is non empty set
the Sorts of A . a is non empty set
the Sorts of A . R is non empty set
b is Relation-like Function-like set
P is non empty Relation-like the Sorts of A . s -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . s, the Sorts of A . a) (S,A,s,a)
b * P is Relation-like the Sorts of A . a -valued Function-like set
F1() is non empty non void feasible ManySortedSign
the carrier of F1() is non empty set
F2() is non-empty (F1()) 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
(F1()) is Relation-like the carrier of F1() -defined the carrier of F1() -valued Element of bool [: the carrier of F1(), the carrier of F1():]
[: the carrier of F1(), the carrier of F1():] is Relation-like set
bool [: the carrier of F1(), the carrier of F1():] is set
R is Element of the carrier of F1()
s is Element of the carrier of F1()
the Sorts of F2() . R is non empty set
the Sorts of F2() . s is non empty set
a is non empty Relation-like the Sorts of F2() . R -defined the Sorts of F2() . s -valued Function-like total V29( the Sorts of F2() . R, the Sorts of F2() . s) (F1(),F2(),R,s)
P is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
compose (P,( the Sorts of F2() . R)) is Relation-like Function-like set
b is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of (F1())
len b is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
len P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(len P) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
b . 1 is set
b . (len b) is set
dom P is Element of bool NAT
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
Seg P is V35() V42(P) Element of bool NAT
P | (Seg P) is Relation-like NAT -defined Seg P -defined NAT -defined Function-like FinSubsequence-like Function-yielding Relation-yielding set
P + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
b . (P + 1) is set
Seg (P + 1) is non empty V35() V42(P + 1) Element of bool NAT
P | (Seg (P + 1)) is Relation-like NAT -defined Seg (P + 1) -defined NAT -defined Function-like FinSubsequence-like Function-yielding Relation-yielding set
(P + 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
b . ((P + 1) + 1) is set
dom b is non empty Element of bool NAT
[(b . (P + 1)),(b . ((P + 1) + 1))] is V26() set
{(b . (P + 1)),(b . ((P + 1) + 1))} is non empty set
{(b . (P + 1))} is non empty trivial V42(1) set
{{(b . (P + 1)),(b . ((P + 1) + 1))},{(b . (P + 1))}} is non empty set
P . (P + 1) is Relation-like Function-like set
P is Element of the carrier of F1()
i is Element of the carrier of F1()
s is Relation-like Function-like set
the Sorts of F2() . P is non empty set
the Sorts of F2() . i is non empty set
x is non empty Relation-like the Sorts of F2() . P -defined the Sorts of F2() . i -valued Function-like total V29( the Sorts of F2() . P, the Sorts of F2() . i) (F1(),F2(),P,i)
P | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined Function-like FinSubsequence-like Function-yielding Relation-yielding set
id ( the Sorts of F2() . R) is non empty Relation-like the Sorts of F2() . R -defined the Sorts of F2() . R -valued Function-like one-to-one total V29( the Sorts of F2() . R, the Sorts of F2() . R) V30( the Sorts of F2() . R) V31( the Sorts of F2() . R, the Sorts of F2() . R) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of F2() . R),( the Sorts of F2() . R):]
[:( the Sorts of F2() . R),( the Sorts of F2() . R):] is Relation-like set
bool [:( the Sorts of F2() . R),( the Sorts of F2() . R):] is set
y is non empty Relation-like the Sorts of F2() . R -defined the Sorts of F2() . i -valued Function-like total V29( the Sorts of F2() . R, the Sorts of F2() . i) (F1(),F2(),R,i)
y * (id ( the Sorts of F2() . R)) is non empty Relation-like the Sorts of F2() . R -defined the Sorts of F2() . i -valued Function-like total V29( the Sorts of F2() . R, the Sorts of F2() . i) Element of bool [:( the Sorts of F2() . R),( the Sorts of F2() . i):]
[:( the Sorts of F2() . R),( the Sorts of F2() . i):] is Relation-like set
bool [:( the Sorts of F2() . R),( the Sorts of F2() . i):] is set
a is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
compose (a,( the Sorts of F2() . R)) is Relation-like Function-like set
dom y is non empty Element of bool ( the Sorts of F2() . R)
bool ( the Sorts of F2() . R) is set
a . 1 is Relation-like Function-like set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
len a is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
<*y*> is non empty trivial Relation-like NAT -defined Function-like constant V35() V42(1) FinSequence-like FinSubsequence-like Function-yielding Relation-yielding FuncSeq-like set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
a is Element of the carrier of F1()
the Sorts of F2() . a is non empty set
u is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
b is non empty Relation-like the Sorts of F2() . R -defined the Sorts of F2() . a -valued Function-like total V29( the Sorts of F2() . R, the Sorts of F2() . a) (F1(),F2(),R,a)
compose (u,( the Sorts of F2() . R)) is Relation-like Function-like set
a is Element of the carrier of F1()
the Sorts of F2() . a is non empty set
u is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
b is non empty Relation-like the Sorts of F2() . R -defined the Sorts of F2() . a -valued Function-like total V29( the Sorts of F2() . R, the Sorts of F2() . a) (F1(),F2(),R,a)
compose (u,( the Sorts of F2() . R)) is Relation-like Function-like set
x is non empty Relation-like the Sorts of F2() . P -defined the Sorts of F2() . i -valued Function-like total V29( the Sorts of F2() . P, the Sorts of F2() . i) (F1(),F2(),P,i)
x * b is Relation-like the Sorts of F2() . R -defined the Sorts of F2() . i -valued Function-like Element of bool [:( the Sorts of F2() . R),( the Sorts of F2() . i):]
[:( the Sorts of F2() . R),( the Sorts of F2() . i):] is Relation-like set
bool [:( the Sorts of F2() . R),( the Sorts of F2() . i):] is set
v is non empty Relation-like the Sorts of F2() . R -defined the Sorts of F2() . i -valued Function-like total V29( the Sorts of F2() . R, the Sorts of F2() . i) (F1(),F2(),R,i)
<*s*> is non empty trivial Relation-like NAT -defined Function-like constant V35() V42(1) FinSequence-like FinSubsequence-like Function-yielding Relation-yielding FuncSeq-like set
u ^ <*s*> is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
h is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
compose (h,( the Sorts of F2() . R)) is Relation-like Function-like set
len u is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
y is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like set
dom y is Element of bool NAT
t is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() set
dom u is Element of bool NAT
h . t is Relation-like Function-like set
u . t is Relation-like Function-like set
P . t is Relation-like Function-like set
y . t is set
len <*s*> is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
len h is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
(len u) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
dom h is non empty Element of bool NAT
Seg 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V35() V40() V42( 0 ) V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete Function-yielding Relation-yielding FuncSeq-like irreflexive Element of bool NAT
P | (Seg 0) is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined Function-like one-to-one constant functional V32() V35() V40() V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete Function-yielding Relation-yielding FuncSeq-like irreflexive set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
b . (0 + 1) is set
id ( the Sorts of F2() . R) is non empty Relation-like the Sorts of F2() . R -defined the Sorts of F2() . R -valued Function-like one-to-one total V29( the Sorts of F2() . R, the Sorts of F2() . R) V30( the Sorts of F2() . R) V31( the Sorts of F2() . R, the Sorts of F2() . R) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of F2() . R),( the Sorts of F2() . R):]
[:( the Sorts of F2() . R),( the Sorts of F2() . R):] is Relation-like set
bool [:( the Sorts of F2() . R),( the Sorts of F2() . R):] is set
P | (dom P) is Relation-like NAT -defined dom P -defined NAT -defined Function-like FinSubsequence-like Function-yielding Relation-yielding set
Seg (len P) is V35() V42( len P) Element of bool NAT
b . ((len P) + 1) is set
P is Element of the carrier of F1()
the Sorts of F2() . P is non empty set
i is Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding set
P is non empty Relation-like the Sorts of F2() . R -defined the Sorts of F2() . P -valued Function-like total V29( the Sorts of F2() . R, the Sorts of F2() . P) (F1(),F2(),R,P)
compose (i,( the Sorts of F2() . R)) is Relation-like Function-like set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non-empty (S) MSAlgebra over S
the Sorts of R is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of R
a is Element of the carrier' of S
the_arity_of a is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
dom (the_arity_of a) is Element of bool NAT
Args (a,A) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of A) is non empty set
the_result_sort_of a is Element of the carrier of S
s . (the_result_sort_of a) is non empty Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of R . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . (the_result_sort_of a), the Sorts of R . (the_result_sort_of a)) Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of R . (the_result_sort_of a)):]
the Sorts of A . (the_result_sort_of a) is non empty set
the Sorts of R . (the_result_sort_of a) is non empty set
[:( the Sorts of A . (the_result_sort_of a)),( the Sorts of R . (the_result_sort_of a)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of R . (the_result_sort_of a)):] is set
b is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of a) /. b is Element of the carrier of S
s . ((the_arity_of a) /. b) is non empty Relation-like the Sorts of A . ((the_arity_of a) /. b) -defined the Sorts of R . ((the_arity_of a) /. b) -valued Function-like total V29( the Sorts of A . ((the_arity_of a) /. b), the Sorts of R . ((the_arity_of a) /. b)) Element of bool [:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . ((the_arity_of a) /. b)):]
the Sorts of A . ((the_arity_of a) /. b) is non empty set
the Sorts of R . ((the_arity_of a) /. b) is non empty set
[:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . ((the_arity_of a) /. b)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . ((the_arity_of a) /. b)):] is set
P is Relation-like Function-like Element of Args (a,A)
(S,a,b,A,P) is Relation-like Function-like set
(S,a,b,A,P) * (s . (the_result_sort_of a)) is Relation-like the Sorts of R . (the_result_sort_of a) -valued Function-like set
s # P is Relation-like Function-like Element of Args (a,R)
Args (a,R) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of R)
K225( the carrier of S, the Sorts of R) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of R) is non empty set
(S,a,b,R,(s # P)) is Relation-like Function-like set
(s . ((the_arity_of a) /. b)) * (S,a,b,R,(s # P)) is Relation-like the Sorts of A . ((the_arity_of a) /. b) -defined Function-like set
[:( the Sorts of R . ((the_arity_of a) /. b)),( the Sorts of R . (the_result_sort_of a)):] is Relation-like set
bool [:( the Sorts of R . ((the_arity_of a) /. b)),( the Sorts of R . (the_result_sort_of a)):] is set
[:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of A . (the_result_sort_of a)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of A . (the_result_sort_of a)):] is set
x is Element of the Sorts of A . ((the_arity_of a) /. b)
P +* (b,x) is Relation-like Function-like set
y is Relation-like Function-like Element of Args (a,A)
s # y is Relation-like Function-like Element of Args (a,R)
(s # y) . b is set
(s # P) +* (b,((s # y) . b)) is Relation-like Function-like set
(s . ((the_arity_of a) /. b)) . x is Element of the Sorts of R . ((the_arity_of a) /. b)
s is non empty Relation-like the Sorts of A . ((the_arity_of a) /. b) -defined the Sorts of A . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . ((the_arity_of a) /. b), the Sorts of A . (the_result_sort_of a)) Element of bool [:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of A . (the_result_sort_of a)):]
(s . (the_result_sort_of a)) * s is non empty Relation-like the Sorts of A . ((the_arity_of a) /. b) -defined the Sorts of R . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . ((the_arity_of a) /. b), the Sorts of R . (the_result_sort_of a)) Element of bool [:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . (the_result_sort_of a)):]
[:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . (the_result_sort_of a)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . (the_result_sort_of a)):] is set
((s . (the_result_sort_of a)) * s) . x is Element of the Sorts of R . (the_result_sort_of a)
s . x is Element of the Sorts of A . (the_result_sort_of a)
(s . (the_result_sort_of a)) . (s . x) is Element of the Sorts of R . (the_result_sort_of a)
Result (a,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
Den (a,A) is non empty Relation-like Args (a,A) -defined Result (a,A) -valued Function-like total V29( Args (a,A), Result (a,A)) Element of bool [:(Args (a,A)),(Result (a,A)):]
[:(Args (a,A)),(Result (a,A)):] is Relation-like set
bool [:(Args (a,A)),(Result (a,A)):] is set
(Den (a,A)) . y is Element of Result (a,A)
(s . (the_result_sort_of a)) . ((Den (a,A)) . y) is set
Den (a,R) is non empty Relation-like Args (a,R) -defined Result (a,R) -valued Function-like total V29( Args (a,R), Result (a,R)) Element of bool [:(Args (a,R)),(Result (a,R)):]
Result (a,R) is non empty Element of proj2 the Sorts of R
proj2 the Sorts of R is non empty set
[:(Args (a,R)),(Result (a,R)):] is Relation-like set
bool [:(Args (a,R)),(Result (a,R)):] is set
(s # P) +* (b,((s . ((the_arity_of a) /. b)) . x)) is Relation-like Function-like set
(Den (a,R)) . ((s # P) +* (b,((s . ((the_arity_of a) /. b)) . x))) is set
i is non empty Relation-like the Sorts of R . ((the_arity_of a) /. b) -defined the Sorts of R . (the_result_sort_of a) -valued Function-like total V29( the Sorts of R . ((the_arity_of a) /. b), the Sorts of R . (the_result_sort_of a)) Element of bool [:( the Sorts of R . ((the_arity_of a) /. b)),( the Sorts of R . (the_result_sort_of a)):]
i . ((s . ((the_arity_of a) /. b)) . x) is Element of the Sorts of R . (the_result_sort_of a)
i * (s . ((the_arity_of a) /. b)) is non empty Relation-like the Sorts of A . ((the_arity_of a) /. b) -defined the Sorts of R . (the_result_sort_of a) -valued Function-like total V29( the Sorts of A . ((the_arity_of a) /. b), the Sorts of R . (the_result_sort_of a)) Element of bool [:( the Sorts of A . ((the_arity_of a) /. b)),( the Sorts of R . (the_result_sort_of a)):]
(i * (s . ((the_arity_of a) /. b))) . x is Element of the Sorts of R . (the_result_sort_of a)
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
s is Element of the carrier' of S
Args (s,A) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
proj2 K225( the carrier of S, the Sorts of A) is non empty set
a is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
the_arity_of s is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
dom (the_arity_of s) is Element of bool NAT
b is Relation-like Function-like Element of Args (s,A)
(S,s,a,A,b) is Relation-like Function-like set
the_result_sort_of s is Element of the carrier of S
R . (the_result_sort_of s) is non empty Relation-like the Sorts of A . (the_result_sort_of s) -defined the Sorts of A . (the_result_sort_of s) -valued Function-like total V29( the Sorts of A . (the_result_sort_of s), the Sorts of A . (the_result_sort_of s)) Element of bool [:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):]
the Sorts of A . (the_result_sort_of s) is non empty set
[:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):] is set
(S,s,a,A,b) * (R . (the_result_sort_of s)) is Relation-like the Sorts of A . (the_result_sort_of s) -valued Function-like set
(the_arity_of s) /. a is Element of the carrier of S
R . ((the_arity_of s) /. a) is non empty Relation-like the Sorts of A . ((the_arity_of s) /. a) -defined the Sorts of A . ((the_arity_of s) /. a) -valued Function-like total V29( the Sorts of A . ((the_arity_of s) /. a), the Sorts of A . ((the_arity_of s) /. a)) Element of bool [:( the Sorts of A . ((the_arity_of s) /. a)),( the Sorts of A . ((the_arity_of s) /. a)):]
the Sorts of A . ((the_arity_of s) /. a) is non empty set
[:( the Sorts of A . ((the_arity_of s) /. a)),( the Sorts of A . ((the_arity_of s) /. a)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of s) /. a)),( the Sorts of A . ((the_arity_of s) /. a)):] is set
R # b is Relation-like Function-like Element of Args (s,A)
(S,s,a,A,(R # b)) is Relation-like Function-like set
(R . ((the_arity_of s) /. a)) * (S,s,a,A,(R # b)) is Relation-like the Sorts of A . ((the_arity_of s) /. a) -defined Function-like set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non-empty (S) MSAlgebra over S
the Sorts of R is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of R
a is Element of the carrier of S
b is Element of the carrier of S
the Sorts of R . a is non empty set
the Sorts of R . b is non empty set
[:( the Sorts of R . a),( the Sorts of R . b):] is Relation-like set
bool [:( the Sorts of R . a),( the Sorts of R . b):] is set
the Sorts of A . a is non empty set
s . a is non empty Relation-like the Sorts of A . a -defined the Sorts of R . a -valued Function-like total V29( the Sorts of A . a, the Sorts of R . a) Element of bool [:( the Sorts of A . a),( the Sorts of R . a):]
[:( the Sorts of A . a),( the Sorts of R . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of R . a):] is set
s . b is non empty Relation-like the Sorts of A . b -defined the Sorts of R . b -valued Function-like total V29( the Sorts of A . b, the Sorts of R . b) Element of bool [:( the Sorts of A . b),( the Sorts of R . b):]
the Sorts of A . b is non empty set
[:( the Sorts of A . b),( the Sorts of R . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of R . b):] is set
P is Relation-like Function-like set
P * (s . b) is Relation-like the Sorts of R . b -valued Function-like set
the carrier' of S is non empty set
P is Element of the carrier' of S
the_result_sort_of P is Element of the carrier of S
the_arity_of P is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
dom (the_arity_of P) is Element of bool NAT
Args (P,A) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of A) is non empty set
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of P) /. P is Element of the carrier of S
i is Relation-like Function-like set
(S,P,P,A,i) is Relation-like Function-like set
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of P) /. P is Element of the carrier of S
i is Relation-like Function-like set
(S,P,P,A,i) is Relation-like Function-like set
s is Relation-like Function-like Element of Args (P,A)
s # s is Relation-like Function-like Element of Args (P,R)
Args (P,R) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of R)
K225( the carrier of S, the Sorts of R) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of R) is non empty set
(S,P,P,R,(s # s)) is Relation-like Function-like set
x is non empty Relation-like the Sorts of R . a -defined the Sorts of R . b -valued Function-like total V29( the Sorts of R . a, the Sorts of R . b) Element of bool [:( the Sorts of R . a),( the Sorts of R . b):]
x * (s . a) is non empty Relation-like the Sorts of A . a -defined the Sorts of R . b -valued Function-like total V29( the Sorts of A . a, the Sorts of R . b) Element of bool [:( the Sorts of A . a),( the Sorts of R . b):]
[:( the Sorts of A . a),( the Sorts of R . b):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of R . b):] is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
s is Element of the carrier of S
a is Element of the carrier of S
b is Relation-like Function-like set
the Sorts of A . s is non empty set
the Sorts of A . a is non empty set
[:( the Sorts of A . s),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . a):] is set
R . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
R . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . a, the Sorts of A . a) Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
b * (R . a) is Relation-like the Sorts of A . a -valued Function-like set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non-empty (S) MSAlgebra over S
the Sorts of R is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of R
a is Element of the carrier of S
b is Element of the carrier of S
the Sorts of A . a is non empty set
the Sorts of A . b is non empty set
the Sorts of R . a is non empty set
the Sorts of R . b is non empty set
s . a is non empty Relation-like the Sorts of A . a -defined the Sorts of R . a -valued Function-like total V29( the Sorts of A . a, the Sorts of R . a) Element of bool [:( the Sorts of A . a),( the Sorts of R . a):]
[:( the Sorts of A . a),( the Sorts of R . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of R . a):] is set
s . b is non empty Relation-like the Sorts of A . b -defined the Sorts of R . b -valued Function-like total V29( the Sorts of A . b, the Sorts of R . b) Element of bool [:( the Sorts of A . b),( the Sorts of R . b):]
[:( the Sorts of A . b),( the Sorts of R . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of R . b):] is set
P is Element of the carrier of S
the Sorts of R . P is non empty set
s . P is non empty Relation-like the Sorts of A . P -defined the Sorts of R . P -valued Function-like total V29( the Sorts of A . P, the Sorts of R . P) Element of bool [:( the Sorts of A . P),( the Sorts of R . P):]
the Sorts of A . P is non empty set
[:( the Sorts of A . P),( the Sorts of R . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of R . P):] is set
P is non empty Relation-like the Sorts of A . a -defined the Sorts of A . b -valued Function-like total V29( the Sorts of A . a, the Sorts of A . b) (S,A,a,b)
P * (s . b) is non empty Relation-like the Sorts of A . a -defined the Sorts of R . b -valued Function-like total set
(s . b) * P is non empty Relation-like the Sorts of A . a -defined the Sorts of R . b -valued Function-like total V29( the Sorts of A . a, the Sorts of R . b) Element of bool [:( the Sorts of A . a),( the Sorts of R . b):]
[:( the Sorts of A . a),( the Sorts of R . b):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of R . b):] is set
P is non empty Relation-like the Sorts of R . a -defined the Sorts of R . b -valued Function-like total V29( the Sorts of R . a, the Sorts of R . b) (S,R,a,b)
P * (s . a) is non empty Relation-like the Sorts of A . a -defined the Sorts of R . b -valued Function-like total V29( the Sorts of A . a, the Sorts of R . b) Element of bool [:( the Sorts of A . a),( the Sorts of R . b):]
i is Relation-like Function-like set
P * i is Relation-like the Sorts of A . a -defined Function-like set
(P * i) * (s . P) is Relation-like the Sorts of A . a -defined the Sorts of R . P -valued Function-like set
[:( the Sorts of R . b),( the Sorts of R . P):] is Relation-like set
bool [:( the Sorts of R . b),( the Sorts of R . P):] is set
i * (s . P) is Relation-like the Sorts of R . P -valued Function-like set
s is non empty Relation-like the Sorts of R . b -defined the Sorts of R . P -valued Function-like total V29( the Sorts of R . b, the Sorts of R . P) Element of bool [:( the Sorts of R . b),( the Sorts of R . P):]
s * (s . b) is non empty Relation-like the Sorts of A . b -defined the Sorts of R . P -valued Function-like total V29( the Sorts of A . b, the Sorts of R . P) Element of bool [:( the Sorts of A . b),( the Sorts of R . P):]
[:( the Sorts of A . b),( the Sorts of R . P):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of R . P):] is set
s * P is non empty Relation-like the Sorts of R . a -defined the Sorts of R . P -valued Function-like total V29( the Sorts of R . a, the Sorts of R . P) Element of bool [:( the Sorts of R . a),( the Sorts of R . P):]
[:( the Sorts of R . a),( the Sorts of R . P):] is Relation-like set
bool [:( the Sorts of R . a),( the Sorts of R . P):] is set
x is non empty Relation-like the Sorts of R . a -defined the Sorts of R . P -valued Function-like total V29( the Sorts of R . a, the Sorts of R . P) (S,R,a,P)
x * (s . a) is non empty Relation-like the Sorts of A . a -defined the Sorts of R . P -valued Function-like total V29( the Sorts of A . a, the Sorts of R . P) Element of bool [:( the Sorts of A . a),( the Sorts of R . P):]
[:( the Sorts of A . a),( the Sorts of R . P):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of R . P):] is set
s * (P * (s . a)) is non empty Relation-like the Sorts of A . a -defined the Sorts of R . P -valued Function-like total V29( the Sorts of A . a, the Sorts of R . P) Element of bool [:( the Sorts of A . a),( the Sorts of R . P):]
P * (i * (s . P)) is Relation-like the Sorts of A . a -defined the Sorts of R . P -valued Function-like set
a is Element of the carrier of S
the Sorts of A . a is non empty set
id ( the Sorts of A . a) is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like one-to-one total V29( the Sorts of A . a, the Sorts of A . a) V30( the Sorts of A . a) V31( the Sorts of A . a, the Sorts of A . a) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
the Sorts of R . a is non empty set
s . a is non empty Relation-like the Sorts of A . a -defined the Sorts of R . a -valued Function-like total V29( the Sorts of A . a, the Sorts of R . a) Element of bool [:( the Sorts of A . a),( the Sorts of R . a):]
[:( the Sorts of A . a),( the Sorts of R . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of R . a):] is set
(id ( the Sorts of A . a)) * (s . a) is non empty Relation-like the Sorts of A . a -defined the Sorts of R . a -valued Function-like total set
id ( the Sorts of R . a) is non empty Relation-like the Sorts of R . a -defined the Sorts of R . a -valued Function-like one-to-one total V29( the Sorts of R . a, the Sorts of R . a) V30( the Sorts of R . a) V31( the Sorts of R . a, the Sorts of R . a) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of R . a),( the Sorts of R . a):]
[:( the Sorts of R . a),( the Sorts of R . a):] is Relation-like set
bool [:( the Sorts of R . a),( the Sorts of R . a):] is set
(id ( the Sorts of R . a)) * (s . a) is non empty Relation-like the Sorts of A . a -defined the Sorts of R . a -valued Function-like total V29( the Sorts of A . a, the Sorts of R . a) Element of bool [:( the Sorts of A . a),( the Sorts of R . a):]
(s . a) * (id ( the Sorts of A . a)) is non empty Relation-like the Sorts of A . a -defined the Sorts of R . a -valued Function-like total V29( the Sorts of A . a, the Sorts of R . a) Element of bool [:( the Sorts of A . a),( the Sorts of R . a):]
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
s is Element of the carrier of S
the Sorts of A . s is non empty set
a is Element of the carrier of S
the Sorts of A . a is non empty set
R . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
b is non empty Relation-like the Sorts of A . s -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . s, the Sorts of A . a) (S,A,s,a)
R . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . a, the Sorts of A . a) Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
(R . a) * b is non empty Relation-like the Sorts of A . s -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . s, the Sorts of A . a) Element of bool [:( the Sorts of A . s),( the Sorts of A . a):]
[:( the Sorts of A . s),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . a):] is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
the carrier' of S is non empty set
s is Element of the carrier' of S
Args (s,A) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
proj2 K225( the carrier of S, the Sorts of A) is non empty set
a is Relation-like Function-like Element of Args (s,A)
proj1 a is set
b is Relation-like Function-like Element of Args (s,A)
the_arity_of s is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
dom (the_arity_of s) is Element of bool NAT
a . P is set
b . P is set
[(a . P),(b . P)] is V26() set
{(a . P),(b . P)} is non empty set
{(a . P)} is non empty trivial V42(1) set
{{(a . P),(b . P)},{(a . P)}} is non empty set
(the_arity_of s) /. P is Element of the carrier of S
R . ((the_arity_of s) /. P) is Relation-like the Sorts of A . ((the_arity_of s) /. P) -defined the Sorts of A . ((the_arity_of s) /. P) -valued total V29( the Sorts of A . ((the_arity_of s) /. P), the Sorts of A . ((the_arity_of s) /. P)) reflexive symmetric transitive Element of bool [:( the Sorts of A . ((the_arity_of s) /. P)),( the Sorts of A . ((the_arity_of s) /. P)):]
the Sorts of A . ((the_arity_of s) /. P) is non empty set
[:( the Sorts of A . ((the_arity_of s) /. P)),( the Sorts of A . ((the_arity_of s) /. P)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of s) /. P)),( the Sorts of A . ((the_arity_of s) /. P)):] is set
Result (s,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
Den (s,A) is non empty Relation-like Args (s,A) -defined Result (s,A) -valued Function-like total V29( Args (s,A), Result (s,A)) Element of bool [:(Args (s,A)),(Result (s,A)):]
[:(Args (s,A)),(Result (s,A)):] is Relation-like set
bool [:(Args (s,A)),(Result (s,A)):] is set
(Den (s,A)) . a is Element of Result (s,A)
(Den (s,A)) . b is Element of Result (s,A)
[((Den (s,A)) . a),((Den (s,A)) . b)] is V26() set
{((Den (s,A)) . a),((Den (s,A)) . b)} is non empty set
{((Den (s,A)) . a)} is non empty trivial V42(1) set
{{((Den (s,A)) . a),((Den (s,A)) . b)},{((Den (s,A)) . a)}} is non empty set
the_result_sort_of s is Element of the carrier of S
R . (the_result_sort_of s) is Relation-like the Sorts of A . (the_result_sort_of s) -defined the Sorts of A . (the_result_sort_of s) -valued total V29( the Sorts of A . (the_result_sort_of s), the Sorts of A . (the_result_sort_of s)) reflexive symmetric transitive Element of bool [:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):]
the Sorts of A . (the_result_sort_of s) is non empty set
[:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):] is set
s is Element of the carrier' of S
Args (s,A) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of A)
the_arity_of s is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
dom (the_arity_of s) is Element of bool NAT
Den (s,A) is non empty Relation-like Args (s,A) -defined Result (s,A) -valued Function-like total V29( Args (s,A), Result (s,A)) Element of bool [:(Args (s,A)),(Result (s,A)):]
Result (s,A) is non empty Element of proj2 the Sorts of A
[:(Args (s,A)),(Result (s,A)):] is Relation-like set
bool [:(Args (s,A)),(Result (s,A)):] is set
the_result_sort_of s is Element of the carrier of S
R . (the_result_sort_of s) is Relation-like the Sorts of A . (the_result_sort_of s) -defined the Sorts of A . (the_result_sort_of s) -valued Element of bool [:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):]
the Sorts of A . (the_result_sort_of s) is non empty set
[:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):] is set
a is Relation-like Function-like set
b is Relation-like Function-like set
(Den (s,A)) . a is set
(Den (s,A)) . b is set
[((Den (s,A)) . a),((Den (s,A)) . b)] is V26() set
{((Den (s,A)) . a),((Den (s,A)) . b)} is non empty set
{((Den (s,A)) . a)} is non empty trivial V42(1) set
{{((Den (s,A)) . a),((Den (s,A)) . b)},{((Den (s,A)) . a)}} is non empty set
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() set
P is Relation-like Function-like Element of Args (s,A)
proj1 P is set
P . P is set
P is Relation-like Function-like Element of Args (s,A)
P . P is set
[(P . P),(P . P)] is V26() set
{(P . P),(P . P)} is non empty set
{(P . P)} is non empty trivial V42(1) set
{{(P . P),(P . P)},{(P . P)}} is non empty set
(the_arity_of s) /. P is Element of the carrier of S
R . ((the_arity_of s) /. P) is Relation-like the Sorts of A . ((the_arity_of s) /. P) -defined the Sorts of A . ((the_arity_of s) /. P) -valued total V29( the Sorts of A . ((the_arity_of s) /. P), the Sorts of A . ((the_arity_of s) /. P)) reflexive symmetric transitive Element of bool [:( the Sorts of A . ((the_arity_of s) /. P)),( the Sorts of A . ((the_arity_of s) /. P)):]
the Sorts of A . ((the_arity_of s) /. P) is non empty set
[:( the Sorts of A . ((the_arity_of s) /. P)),( the Sorts of A . ((the_arity_of s) /. P)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of s) /. P)),( the Sorts of A . ((the_arity_of s) /. P)):] is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
a is Element of the carrier of S
the Sorts of A . s is non empty set
the Sorts of A . a is non empty set
R . s is set
R . a is set
b is Element of the carrier of S
R . b is set
P is non empty Relation-like the Sorts of A . s -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . s, the Sorts of A . a) (S,A,s,a)
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
P is Relation-like Function-like set
P * P is Relation-like the Sorts of A . s -defined Function-like set
P is set
i is set
[P,i] is V26() set
{P,i} is non empty set
{P} is non empty trivial V42(1) set
{{P,i},{P}} is non empty set
(P * P) . P is set
(P * P) . i is set
[((P * P) . P),((P * P) . i)] is V26() set
{((P * P) . P),((P * P) . i)} is non empty set
{((P * P) . P)} is non empty trivial V42(1) set
{{((P * P) . P),((P * P) . i)},{((P * P) . P)}} is non empty set
s is Element of the Sorts of A . s
P . s is Element of the Sorts of A . a
x is Element of the Sorts of A . s
P . x is Element of the Sorts of A . a
[(P . s),(P . x)] is V26() set
{(P . s),(P . x)} is non empty set
{(P . s)} is non empty trivial V42(1) set
{{(P . s),(P . x)},{(P . s)}} is non empty set
P . (P . s) is set
P . (P . x) is set
[(P . (P . s)),(P . (P . x))] is V26() set
{(P . (P . s)),(P . (P . x))} is non empty set
{(P . (P . s))} is non empty trivial V42(1) set
{{(P . (P . s)),(P . (P . x))},{(P . (P . s))}} is non empty set
R . b is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
the Sorts of A . b is non empty set
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
(P * P) . s is set
s is Element of the carrier of S
the Sorts of A . s is non empty set
id ( the Sorts of A . s) is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like one-to-one total V29( the Sorts of A . s, the Sorts of A . s) V30( the Sorts of A . s) V31( the Sorts of A . s, the Sorts of A . s) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
R . s is set
a is set
b is set
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
(id ( the Sorts of A . s)) . a is set
(id ( the Sorts of A . s)) . b is set
[((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] is V26() set
{((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)} is non empty set
{((id ( the Sorts of A . s)) . a)} is non empty trivial V42(1) set
{{((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)},{((id ( the Sorts of A . s)) . a)}} is non empty set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
H1(s) . a is set
s is Element of the carrier of S
a is Element of the carrier of S
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
the Sorts of A . s is non empty set
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
b is Relation-like Function-like set
P is set
P is set
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
b . P is set
b . P is set
[(b . P),(b . P)] is V26() set
{(b . P),(b . P)} is non empty set
{(b . P)} is non empty trivial V42(1) set
{{(b . P),(b . P)},{(b . P)}} is non empty set
S is non empty non void feasible ManySortedSign
A is non-empty (S) MSAlgebra over S
the carrier of S is non empty set
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
the carrier' of S is non empty set
s is Element of the carrier' of S
Args (s,A) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
proj2 K225( the carrier of S, the Sorts of A) is non empty set
the_arity_of s is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
dom (the_arity_of s) is Element of bool NAT
Den (s,A) is non empty Relation-like Args (s,A) -defined Result (s,A) -valued Function-like total V29( Args (s,A), Result (s,A)) Element of bool [:(Args (s,A)),(Result (s,A)):]
Result (s,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
[:(Args (s,A)),(Result (s,A)):] is Relation-like set
bool [:(Args (s,A)),(Result (s,A)):] is set
the_result_sort_of s is Element of the carrier of S
R . (the_result_sort_of s) is Relation-like the Sorts of A . (the_result_sort_of s) -defined the Sorts of A . (the_result_sort_of s) -valued Element of bool [:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):]
the Sorts of A . (the_result_sort_of s) is non empty set
[:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):] is Relation-like set
bool [:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):] is set
a is Relation-like Function-like set
b is Relation-like Function-like set
(Den (s,A)) . a is set
(Den (s,A)) . b is set
[((Den (s,A)) . a),((Den (s,A)) . b)] is V26() set
{((Den (s,A)) . a),((Den (s,A)) . b)} is non empty set
{((Den (s,A)) . a)} is non empty trivial V42(1) set
{{((Den (s,A)) . a),((Den (s,A)) . b)},{((Den (s,A)) . a)}} is non empty set
len (the_arity_of s) is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
Seg (len (the_arity_of s)) is V35() V42( len (the_arity_of s)) Element of bool NAT
(len (the_arity_of s)) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
b . P is set
P is Relation-like Function-like Element of Args (s,A)
(the_arity_of s) /. P is Element of the carrier of S
the Sorts of A . ((the_arity_of s) /. P) is non empty set
P +* (P,(b . P)) is Relation-like Function-like set
P is Relation-like Function-like Element of Args (s,A)
P is Relation-like NAT -defined Args (s,A) -valued Function-like V35() FinSequence-like FinSubsequence-like Function-yielding Relation-yielding FinSequence of Args (s,A)
len P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
P . 1 is Relation-like Function-like set
dom P is Element of bool NAT
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
P + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . (P + 1) is Relation-like Function-like set
Seg P is V35() V42(P) Element of bool NAT
(P + 1) + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . ((P + 1) + 1) is Relation-like Function-like set
Seg (P + 1) is non empty V35() V42(P + 1) Element of bool NAT
b . (P + 1) is set
i is Relation-like Function-like Element of Args (s,A)
i +* ((P + 1),(b . (P + 1))) is Relation-like Function-like set
(the_arity_of s) /. (P + 1) is Element of the carrier of S
the Sorts of A . ((the_arity_of s) /. (P + 1)) is non empty set
s is Relation-like Function-like Element of Args (s,A)
proj1 i is set
x is Relation-like Function-like Element of Args (s,A)
x is Relation-like Function-like Element of Args (s,A)
y is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
x . y is set
a . y is set
s . y is set
y is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() set
s . y is set
b . y is set
{(P + 1)} is non empty trivial V42(1) set
(Seg P) \/ {(P + 1)} is non empty set
i . y is set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . (0 + 1) is Relation-like Function-like set
Seg 0 is empty V4() V5() V6() V8() V9() V10() V11() ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V35() V40() V42( 0 ) V42( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete Function-yielding Relation-yielding FuncSeq-like irreflexive Element of bool NAT
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
P . P is set
a . P is set
i is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() set
P . i is set
b . i is set
P . ((len (the_arity_of s)) + 1) is Relation-like Function-like set
P is Relation-like Function-like Element of Args (s,A)
(Den (s,A)) . P is Element of Result (s,A)
R . (the_result_sort_of s) is Relation-like the Sorts of A . (the_result_sort_of s) -defined the Sorts of A . (the_result_sort_of s) -valued total V29( the Sorts of A . (the_result_sort_of s), the Sorts of A . (the_result_sort_of s)) reflexive symmetric transitive Element of bool [:( the Sorts of A . (the_result_sort_of s)),( the Sorts of A . (the_result_sort_of s)):]
i is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
P . i is Relation-like Function-like set
(Den (s,A)) . (P . i) is set
[((Den (s,A)) . P),((Den (s,A)) . (P . i))] is V26() set
{((Den (s,A)) . P),((Den (s,A)) . (P . i))} is non empty set
{((Den (s,A)) . P)} is non empty trivial V42(1) set
{{((Den (s,A)) . P),((Den (s,A)) . (P . i))},{((Den (s,A)) . P)}} is non empty set
i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . (i + 1) is Relation-like Function-like set
(Den (s,A)) . (P . (i + 1)) is set
[((Den (s,A)) . P),((Den (s,A)) . (P . (i + 1)))] is V26() set
{((Den (s,A)) . P),((Den (s,A)) . (P . (i + 1)))} is non empty set
{{((Den (s,A)) . P),((Den (s,A)) . (P . (i + 1)))},{((Den (s,A)) . P)}} is non empty set
s is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() set
1 + s is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
b . i is set
y is Relation-like Function-like Element of Args (s,A)
y +* (i,(b . i)) is Relation-like Function-like set
(the_arity_of s) /. i is Element of the carrier of S
the Sorts of A . ((the_arity_of s) /. i) is non empty set
y . i is set
x is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
x + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . (x + 1) is Relation-like Function-like set
Seg x is V35() V42(x) Element of bool NAT
a . i is set
u is Relation-like Function-like Element of Args (s,A)
b is Element of the Sorts of A . ((the_arity_of s) /. i)
a is Element of the Sorts of A . ((the_arity_of s) /. i)
[b,a] is V26() set
{b,a} is non empty set
{b} is non empty trivial V42(1) set
{{b,a},{b}} is non empty set
R . ((the_arity_of s) /. i) is Relation-like the Sorts of A . ((the_arity_of s) /. i) -defined the Sorts of A . ((the_arity_of s) /. i) -valued total V29( the Sorts of A . ((the_arity_of s) /. i), the Sorts of A . ((the_arity_of s) /. i)) reflexive symmetric transitive Element of bool [:( the Sorts of A . ((the_arity_of s) /. i)),( the Sorts of A . ((the_arity_of s) /. i)):]
[:( the Sorts of A . ((the_arity_of s) /. i)),( the Sorts of A . ((the_arity_of s) /. i)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of s) /. i)),( the Sorts of A . ((the_arity_of s) /. i)):] is set
y +* (i,a) is Relation-like Function-like set
u is Relation-like Function-like Element of Args (s,A)
(Den (s,A)) . u is Element of Result (s,A)
(S,s,i,A,y) is Relation-like Function-like set
(S,s,i,A,y) . a is set
y +* (i,b) is Relation-like Function-like set
(Den (s,A)) . y is Element of Result (s,A)
(S,s,i,A,y) . b is set
[((Den (s,A)) . y),((Den (s,A)) . u)] is V26() set
{((Den (s,A)) . y),((Den (s,A)) . u)} is non empty set
{((Den (s,A)) . y)} is non empty trivial V42(1) set
{{((Den (s,A)) . y),((Den (s,A)) . u)},{((Den (s,A)) . y)}} is non empty set
proj1 b is set
P . 0 is Relation-like Function-like set
(Den (s,A)) . (P . 0) is set
[((Den (s,A)) . P),((Den (s,A)) . (P . 0))] is V26() set
{((Den (s,A)) . P),((Den (s,A)) . (P . 0))} is non empty set
{((Den (s,A)) . P)} is non empty trivial V42(1) set
{{((Den (s,A)) . P),((Den (s,A)) . (P . 0))},{((Den (s,A)) . P)}} is non empty set
proj1 P is set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
the carrier' of S is non empty set
s is Element of the carrier of S
a is Element of the carrier of S
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
the Sorts of A . s is non empty set
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
b is Relation-like Function-like set
P is Element of the carrier' of S
the_result_sort_of P is Element of the carrier of S
the_arity_of P is Relation-like NAT -defined the carrier of S -valued Function-like V35() FinSequence-like FinSubsequence-like M13( the carrier of S,K222( the carrier of S))
K222( the carrier of S) is non empty functional FinSequence-membered M12( the carrier of S)
dom (the_arity_of P) is Element of bool NAT
Args (P,A) is non empty functional Element of proj2 K225( the carrier of S, the Sorts of A)
K225( the carrier of S, the Sorts of A) is non empty Relation-like K222( the carrier of S) -defined Function-like total set
proj2 K225( the carrier of S, the Sorts of A) is non empty set
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of P) /. P is Element of the carrier of S
P is Relation-like Function-like set
(S,P,P,A,P) is Relation-like Function-like set
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of P) /. P is Element of the carrier of S
P is Relation-like Function-like set
(S,P,P,A,P) is Relation-like Function-like set
i is set
s is set
[i,s] is V26() set
{i,s} is non empty set
{i} is non empty trivial V42(1) set
{{i,s},{i}} is non empty set
b . i is set
b . s is set
[(b . i),(b . s)] is V26() set
{(b . i),(b . s)} is non empty set
{(b . i)} is non empty trivial V42(1) set
{{(b . i),(b . s)},{(b . i)}} is non empty set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued total V29( the Sorts of A . s, the Sorts of A . s) reflexive symmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
P +* (P,i) is Relation-like Function-like set
P +* (P,s) is Relation-like Function-like set
Result (P,A) is non empty Element of proj2 the Sorts of A
proj2 the Sorts of A is non empty set
Den (P,A) is non empty Relation-like Args (P,A) -defined Result (P,A) -valued Function-like total V29( Args (P,A), Result (P,A)) Element of bool [:(Args (P,A)),(Result (P,A)):]
[:(Args (P,A)),(Result (P,A)):] is Relation-like set
bool [:(Args (P,A)),(Result (P,A)):] is set
y is Relation-like Function-like Element of Args (P,A)
(Den (P,A)) . y is Element of Result (P,A)
proj1 P is set
(the_arity_of P) * the Sorts of A is Relation-like non-empty NAT -defined dom (the_arity_of P) -defined Function-like total set
dom ((the_arity_of P) * the Sorts of A) is Element of bool NAT
a is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
(the_arity_of P) /. a is Element of the carrier of S
(the_arity_of P) . a is set
the Sorts of A . ((the_arity_of P) /. a) is non empty set
((the_arity_of P) * the Sorts of A) . a is set
x is Relation-like Function-like Element of Args (P,A)
x . a is set
y . a is set
P . a is set
[(x . a),(y . a)] is V26() set
{(x . a),(y . a)} is non empty set
{(x . a)} is non empty trivial V42(1) set
{{(x . a),(y . a)},{(x . a)}} is non empty set
R . ((the_arity_of P) /. a) is Relation-like the Sorts of A . ((the_arity_of P) /. a) -defined the Sorts of A . ((the_arity_of P) /. a) -valued total V29( the Sorts of A . ((the_arity_of P) /. a), the Sorts of A . ((the_arity_of P) /. a)) reflexive symmetric transitive Element of bool [:( the Sorts of A . ((the_arity_of P) /. a)),( the Sorts of A . ((the_arity_of P) /. a)):]
[:( the Sorts of A . ((the_arity_of P) /. a)),( the Sorts of A . ((the_arity_of P) /. a)):] is Relation-like set
bool [:( the Sorts of A . ((the_arity_of P) /. a)),( the Sorts of A . ((the_arity_of P) /. a)):] is set
(Den (P,A)) . x is Element of Result (P,A)
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued total V29( the Sorts of A . a, the Sorts of A . a) reflexive symmetric transitive Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
S is non empty set
id S is non empty Relation-like S -defined S -valued Function-like one-to-one total V29(S,S) V30(S) V31(S,S) reflexive symmetric antisymmetric transitive Element of bool [:S,S:]
[:S,S:] is Relation-like set
bool [:S,S:] is set
F1() is non empty set
F2() is non empty Relation-like non-empty non empty-yielding F1() -defined Function-like total set
S is Relation-like Function-like set
proj1 S is set
A is non empty Relation-like F1() -defined Function-like total set
R is set
A . R is set
F2() . R is set
[:(F2() . R),(F2() . R):] is Relation-like set
bool [:(F2() . R),(F2() . R):] is set
s is set
R is non empty Relation-like F1() -defined Function-like total Relation-yielding ManySortedRelation of F2(),F2()
s is Element of F1()
F2() . s is non empty set
R . s is Relation-like F2() . s -defined F2() . s -valued Element of bool [:(F2() . s),(F2() . s):]
[:(F2() . s),(F2() . s):] is Relation-like set
bool [:(F2() . s),(F2() . s):] is set
a is Element of F2() . s
b is Element of F2() . s
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
[a,b] `2 is set
[a,b] `1 is set
F1() is set
F2() is Relation-like F1() -defined Function-like total set
S is Relation-like F1() -defined Function-like total set
A is set
S . A is set
F2() . A is set
[:(F2() . A),(F2() . A):] is Relation-like set
bool [:(F2() . A),(F2() . A):] is set
F3(A) is set
A is Relation-like F1() -defined Function-like total Relation-yielding ManySortedRelation of F2(),F2()
R is Relation-like F1() -defined Function-like total Relation-yielding ManySortedRelation of F2(),F2()
s is set
A . s is set
F3(s) is set
R . s is set
S is set
A is Relation-like S -defined Function-like total set
R is set
A . R is set
id (A . R) is Relation-like A . R -defined A . R -valued Function-like one-to-one total V29(A . R,A . R) V30(A . R) V31(A . R,A . R) reflexive symmetric antisymmetric transitive Element of bool [:(A . R),(A . R):]
[:(A . R),(A . R):] is Relation-like set
bool [:(A . R),(A . R):] is set
R is Relation-like S -defined Function-like total Relation-yielding ManySortedRelation of A,A
s is Relation-like S -defined Function-like total Relation-yielding ManySortedRelation of A,A
a is Relation-like S -defined Function-like total Relation-yielding ManySortedRelation of A,A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
s is set
R . s is set
a is Element of the carrier of S
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
( the carrier of S, the Sorts of A) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
a is Element of the carrier of S
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
the Sorts of A . s is non empty set
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
b is Relation-like Function-like set
[:( the Sorts of A . s),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . a):] is set
P is set
P is set
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
b . P is set
b . P is set
[(b . P),(b . P)] is V26() set
{(b . P),(b . P)} is non empty set
{(b . P)} is non empty trivial V42(1) set
{{(b . P),(b . P)},{(b . P)}} is non empty set
P is non empty Relation-like the Sorts of A . s -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . s, the Sorts of A . a) Element of bool [:( the Sorts of A . s),( the Sorts of A . a):]
P . P is set
id ( the Sorts of A . s) is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like one-to-one total V29( the Sorts of A . s, the Sorts of A . s) V30( the Sorts of A . s) V31( the Sorts of A . s, the Sorts of A . s) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
id ( the Sorts of A . a) is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like one-to-one total V29( the Sorts of A . a, the Sorts of A . a) V30( the Sorts of A . a) V31( the Sorts of A . a, the Sorts of A . a) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
a is Element of the carrier of S
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
s . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . a, the Sorts of A . a) Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
b is set
P is set
[b,P] is V26() set
{b,P} is non empty set
{b} is non empty trivial V42(1) set
{{b,P},{b}} is non empty set
(s . a) . b is set
(s . a) . P is set
[((s . a) . b),((s . a) . P)] is V26() set
{((s . a) . b),((s . a) . P)} is non empty set
{((s . a) . b)} is non empty trivial V42(1) set
{{((s . a) . b),((s . a) . P)},{((s . a) . b)}} is non empty set
id ( the Sorts of A . a) is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like one-to-one total V29( the Sorts of A . a, the Sorts of A . a) V30( the Sorts of A . a) V31( the Sorts of A . a, the Sorts of A . a) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
s is set
the Sorts of A . s is set
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
R . s is set
a is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
b is Element of the carrier of S
the Sorts of A . b is non empty set
id ( the Sorts of A . b) is non empty Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Function-like one-to-one total V29( the Sorts of A . b, the Sorts of A . b) V30( the Sorts of A . b) V31( the Sorts of A . b, the Sorts of A . b) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
F1() is non empty non void feasible ManySortedSign
the carrier of F1() is non empty set
F2() is non-empty (F1()) 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
F4() is non empty Relation-like the carrier of F1() -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of F2(), the Sorts of F2()
F3() is non empty Relation-like the carrier of F1() -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of F2(), the Sorts of F2()
S is Element of the carrier of F1()
the Sorts of F2() . S is non empty set
A is Element of the carrier of F1()
the Sorts of F2() . A is non empty set
[:( the Sorts of F2() . S),( the Sorts of F2() . A):] is Relation-like set
bool [:( the Sorts of F2() . S),( the Sorts of F2() . A):] is set
s is non empty Relation-like the Sorts of F2() . S -defined the Sorts of F2() . A -valued Function-like total V29( the Sorts of F2() . S, the Sorts of F2() . A) Element of bool [:( the Sorts of F2() . S),( the Sorts of F2() . A):]
a is set
b is set
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
F4() . S is Relation-like the Sorts of F2() . S -defined the Sorts of F2() . S -valued Element of bool [:( the Sorts of F2() . S),( the Sorts of F2() . S):]
[:( the Sorts of F2() . S),( the Sorts of F2() . S):] is Relation-like set
bool [:( the Sorts of F2() . S),( the Sorts of F2() . S):] is set
P is Element of the carrier of F1()
the Sorts of F2() . P is non empty set
[:( the Sorts of F2() . P),( the Sorts of F2() . S):] is Relation-like set
bool [:( the Sorts of F2() . P),( the Sorts of F2() . S):] is set
P is non empty Relation-like the Sorts of F2() . P -defined the Sorts of F2() . S -valued Function-like total V29( the Sorts of F2() . P, the Sorts of F2() . S) Element of bool [:( the Sorts of F2() . P),( the Sorts of F2() . S):]
P is Element of the Sorts of F2() . P
i is Element of the Sorts of F2() . P
[P,i] is V26() set
{P,i} is non empty set
{P} is non empty trivial V42(1) set
{{P,i},{P}} is non empty set
F3() . P is Relation-like the Sorts of F2() . P -defined the Sorts of F2() . P -valued Element of bool [:( the Sorts of F2() . P),( the Sorts of F2() . P):]
[:( the Sorts of F2() . P),( the Sorts of F2() . P):] is Relation-like set
bool [:( the Sorts of F2() . P),( the Sorts of F2() . P):] is set
P . P is Element of the Sorts of F2() . S
P . i is Element of the Sorts of F2() . S
s . a is set
s * P is non empty Relation-like the Sorts of F2() . P -defined the Sorts of F2() . A -valued Function-like total V29( the Sorts of F2() . P, the Sorts of F2() . A) Element of bool [:( the Sorts of F2() . P),( the Sorts of F2() . A):]
[:( the Sorts of F2() . P),( the Sorts of F2() . A):] is Relation-like set
bool [:( the Sorts of F2() . P),( the Sorts of F2() . A):] is set
(s * P) . P is Element of the Sorts of F2() . A
s . b is set
(s * P) . i is Element of the Sorts of F2() . A
[(s . a),(s . b)] is V26() set
{(s . a),(s . b)} is non empty set
{(s . a)} is non empty trivial V42(1) set
{{(s . a),(s . b)},{(s . a)}} is non empty set
F4() . A is Relation-like the Sorts of F2() . A -defined the Sorts of F2() . A -valued Element of bool [:( the Sorts of F2() . A),( the Sorts of F2() . A):]
[:( the Sorts of F2() . A),( the Sorts of F2() . A):] is Relation-like set
bool [:( the Sorts of F2() . A),( the Sorts of F2() . A):] is set
S is set
F3() . S is set
F4() . S is set
A is Element of the carrier of F1()
the Sorts of F2() . A is non empty set
F3() . A is Relation-like the Sorts of F2() . A -defined the Sorts of F2() . A -valued Element of bool [:( the Sorts of F2() . A),( the Sorts of F2() . A):]
[:( the Sorts of F2() . A),( the Sorts of F2() . A):] is Relation-like set
bool [:( the Sorts of F2() . A),( the Sorts of F2() . A):] is set
F4() . A is Relation-like the Sorts of F2() . A -defined the Sorts of F2() . A -valued Element of bool [:( the Sorts of F2() . A),( the Sorts of F2() . A):]
id ( the Sorts of F2() . A) is non empty Relation-like the Sorts of F2() . A -defined the Sorts of F2() . A -valued Function-like one-to-one total V29( the Sorts of F2() . A, the Sorts of F2() . A) V30( the Sorts of F2() . A) V31( the Sorts of F2() . A, the Sorts of F2() . A) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of F2() . A),( the Sorts of F2() . A):]
s is set
a is set
[s,a] is V26() set
{s,a} is non empty set
{s} is non empty trivial V42(1) set
{{s,a},{s}} is non empty set
P is Element of the Sorts of F2() . A
(id ( the Sorts of F2() . A)) . P is Element of the Sorts of F2() . A
b is Element of the Sorts of F2() . A
(id ( the Sorts of F2() . A)) . b is Element of the Sorts of F2() . A
S is non empty Relation-like the carrier of F1() -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of F2(), the Sorts of F2()
A is set
F4() . A is set
S . A is set
R is Element of the carrier of F1()
the Sorts of F2() . R is non empty set
F4() . R is Relation-like the Sorts of F2() . R -defined the Sorts of F2() . R -valued Element of bool [:( the Sorts of F2() . R),( the Sorts of F2() . R):]
[:( the Sorts of F2() . R),( the Sorts of F2() . R):] is Relation-like set
bool [:( the Sorts of F2() . R),( the Sorts of F2() . R):] is set
S . R is Relation-like the Sorts of F2() . R -defined the Sorts of F2() . R -valued Element of bool [:( the Sorts of F2() . R),( the Sorts of F2() . R):]
s is set
a is set
[s,a] is V26() set
{s,a} is non empty set
{s} is non empty trivial V42(1) set
{{s,a},{s}} is non empty set
b is Element of the Sorts of F2() . R
P is Element of the Sorts of F2() . R
P is Element of the carrier of F1()
the Sorts of F2() . P is non empty set
[:( the Sorts of F2() . P),( the Sorts of F2() . R):] is Relation-like set
bool [:( the Sorts of F2() . P),( the Sorts of F2() . R):] is set
P is non empty Relation-like the Sorts of F2() . P -defined the Sorts of F2() . R -valued Function-like total V29( the Sorts of F2() . P, the Sorts of F2() . R) Element of bool [:( the Sorts of F2() . P),( the Sorts of F2() . R):]
i is Element of the Sorts of F2() . P
s is Element of the Sorts of F2() . P
[i,s] is V26() set
{i,s} is non empty set
{i} is non empty trivial V42(1) set
{{i,s},{i}} is non empty set
F3() . P is Relation-like the Sorts of F2() . P -defined the Sorts of F2() . P -valued Element of bool [:( the Sorts of F2() . P),( the Sorts of F2() . P):]
[:( the Sorts of F2() . P),( the Sorts of F2() . P):] is Relation-like set
bool [:( the Sorts of F2() . P),( the Sorts of F2() . P):] is set
P . i is Element of the Sorts of F2() . R
P . s is Element of the Sorts of F2() . R
S . P is Relation-like the Sorts of F2() . P -defined the Sorts of F2() . P -valued Element of bool [:( the Sorts of F2() . P),( the Sorts of F2() . P):]
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
a is Element of the carrier of S
b is Element of the carrier of S
the Sorts of A . b is non empty set
id ( the Sorts of A . b) is non empty Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Function-like one-to-one total V29( the Sorts of A . b, the Sorts of A . b) V30( the Sorts of A . b) V31( the Sorts of A . b, the Sorts of A . b) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
a is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
b is Element of the carrier of S
the Sorts of A . b is non empty set
P is Element of the carrier of S
the Sorts of A . P is non empty set
[:( the Sorts of A . b),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . P):] is set
P is non empty Relation-like the Sorts of A . b -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . b, the Sorts of A . P) Element of bool [:( the Sorts of A . b),( the Sorts of A . P):]
P is set
i is set
[P,i] is V26() set
{P,i} is non empty set
{P} is non empty trivial V42(1) set
{{P,i},{P}} is non empty set
a . b is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
P . P is set
P . i is set
[(P . P),(P . i)] is V26() set
{(P . P),(P . i)} is non empty set
{(P . P)} is non empty trivial V42(1) set
{{(P . P),(P . i)},{(P . P)}} is non empty set
a . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
[:( the Sorts of A . P),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . P):] is set
b is Element of the carrier of S
the Sorts of A . b is non empty set
P is Element of the carrier of S
the Sorts of A . P is non empty set
P is set
i is set
[P,i] is V26() set
{P,i} is non empty set
{P} is non empty trivial V42(1) set
{{P,i},{P}} is non empty set
a . b is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
P is non empty Relation-like the Sorts of A . b -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . b, the Sorts of A . P) (S,A,b,P)
P . P is set
P . i is set
[(P . P),(P . i)] is V26() set
{(P . P),(P . i)} is non empty set
{(P . P)} is non empty trivial V42(1) set
{{(P . P),(P . i)},{(P . P)}} is non empty set
a . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
[:( the Sorts of A . P),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . P):] is set
a is Element of the carrier of S
the Sorts of A . a is non empty set
b is Element of the carrier of S
the Sorts of A . b is non empty set
[:( the Sorts of A . a),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . b):] is set
P is Element of the carrier of S
the Sorts of A . P is non empty set
[:( the Sorts of A . b),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . P):] is set
P is non empty Relation-like the Sorts of A . a -defined the Sorts of A . b -valued Function-like total V29( the Sorts of A . a, the Sorts of A . b) Element of bool [:( the Sorts of A . a),( the Sorts of A . b):]
P is non empty Relation-like the Sorts of A . b -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . b, the Sorts of A . P) Element of bool [:( the Sorts of A . b),( the Sorts of A . P):]
P * P is non empty Relation-like the Sorts of A . a -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . a, the Sorts of A . P) Element of bool [:( the Sorts of A . a),( the Sorts of A . P):]
[:( the Sorts of A . a),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . P):] is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
a is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
a is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
b is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
the Sorts of A . s is non empty set
(S,A,R) . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
a is Element of the Sorts of A . s
b is Element of the Sorts of A . s
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,P) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
i is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
the Sorts of A . s is non empty set
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
x is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
y is Element of the Sorts of A . s
a is Element of the Sorts of A . s
[y,a] is V26() set
{y,a} is non empty set
{y} is non empty trivial V42(1) set
{{y,a},{y}} is non empty set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
x . y is Element of the Sorts of A . s
x . a is Element of the Sorts of A . s
s is Element of the carrier of S
the Sorts of A . s is non empty set
x is Element of the Sorts of A . s
y is Element of the Sorts of A . s
[x,y] is V26() set
{x,y} is non empty set
{x} is non empty trivial V42(1) set
{{x,y},{x}} is non empty set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
a is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) (S,A,s,s)
a . x is Element of the Sorts of A . s
a . y is Element of the Sorts of A . s
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
a is Element of the carrier of S
(S,A,R) . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
s . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . a, the Sorts of A . a) Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
b is set
P is set
[b,P] is V26() set
{b,P} is non empty set
{b} is non empty trivial V42(1) set
{{b,P},{b}} is non empty set
(s . a) . b is set
(s . a) . P is set
[((s . a) . b),((s . a) . P)] is V26() set
{((s . a) . b),((s . a) . P)} is non empty set
{((s . a) . b)} is non empty trivial V42(1) set
{{((s . a) . b),((s . a) . P)},{((s . a) . b)}} is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
P is Element of the carrier of S
the Sorts of A . P is non empty set
P is Element of the Sorts of A . P
i is Element of the Sorts of A . P
[P,i] is V26() set
{P,i} is non empty set
{P} is non empty trivial V42(1) set
{{P,i},{P}} is non empty set
R . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
[:( the Sorts of A . P),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . P):] is set
s is non empty Relation-like the Sorts of A . P -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . P, the Sorts of A . a) (S,A,P,a)
s . P is Element of the Sorts of A . a
s . i is Element of the Sorts of A . a
s . P is non empty Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . P, the Sorts of A . P) Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
(s . a) * s is non empty Relation-like the Sorts of A . P -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . P, the Sorts of A . a) Element of bool [:( the Sorts of A . P),( the Sorts of A . a):]
[:( the Sorts of A . P),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . a):] is set
x is non empty Relation-like the Sorts of A . P -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . P, the Sorts of A . a) (S,A,P,a)
x * (s . P) is non empty Relation-like the Sorts of A . P -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . P, the Sorts of A . a) Element of bool [:( the Sorts of A . P),( the Sorts of A . a):]
(x * (s . P)) . i is Element of the Sorts of A . a
(s . P) . i is Element of the Sorts of A . P
x . ((s . P) . i) is Element of the Sorts of A . a
(x * (s . P)) . P is Element of the Sorts of A . a
(s . P) . P is Element of the Sorts of A . P
x . ((s . P) . P) is Element of the Sorts of A . a
[((s . P) . P),((s . P) . i)] is V26() set
{((s . P) . P),((s . P) . i)} is non empty set
{((s . P) . P)} is non empty trivial V42(1) set
{{((s . P) . P),((s . P) . i)},{((s . P) . P)}} is non empty set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
a is Element of the carrier of S
the Sorts of A . a is non empty set
b is Element of the carrier of S
the Sorts of A . b is non empty set
[:( the Sorts of A . a),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . b):] is set
P is Element of the carrier of S
the Sorts of A . P is non empty set
[:( the Sorts of A . b),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . P):] is set
P is non empty Relation-like the Sorts of A . a -defined the Sorts of A . b -valued Function-like total V29( the Sorts of A . a, the Sorts of A . b) Element of bool [:( the Sorts of A . a),( the Sorts of A . b):]
P is non empty Relation-like the Sorts of A . b -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . b, the Sorts of A . P) Element of bool [:( the Sorts of A . b),( the Sorts of A . P):]
P * P is non empty Relation-like the Sorts of A . a -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . a, the Sorts of A . P) Element of bool [:( the Sorts of A . a),( the Sorts of A . P):]
[:( the Sorts of A . a),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . P):] is set
i is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
i . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . a, the Sorts of A . a) Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
s . b is non empty Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Function-like total V29( the Sorts of A . b, the Sorts of A . b) Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
(S,A,i,s) is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
x is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
x . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . a, the Sorts of A . a) Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
a is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
b is Element of the carrier of S
the Sorts of A . b is non empty set
P is Element of the carrier of S
the Sorts of A . P is non empty set
[:( the Sorts of A . b),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . P):] is set
P is non empty Relation-like the Sorts of A . b -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . b, the Sorts of A . P) Element of bool [:( the Sorts of A . b),( the Sorts of A . P):]
P is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
P . b is non empty Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Function-like total V29( the Sorts of A . b, the Sorts of A . b) Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
i is set
s is set
[i,s] is V26() set
{i,s} is non empty set
{i} is non empty trivial V42(1) set
{{i,s},{i}} is non empty set
a . b is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
P . i is set
P . s is set
[(P . i),(P . s)] is V26() set
{(P . i),(P . s)} is non empty set
{(P . i)} is non empty trivial V42(1) set
{{(P . i),(P . s)},{(P . i)}} is non empty set
a . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
[:( the Sorts of A . P),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . P):] is set
b is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
P is Element of the carrier of S
a . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
the Sorts of A . P is non empty set
[:( the Sorts of A . P),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . P):] is set
b . P is non empty Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . P, the Sorts of A . P) Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
P is set
P is set
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
(b . P) . P is set
(b . P) . P is set
[((b . P) . P),((b . P) . P)] is V26() set
{((b . P) . P),((b . P) . P)} is non empty set
{((b . P) . P)} is non empty trivial V42(1) set
{{((b . P) . P),((b . P) . P)},{((b . P) . P)}} is non empty set
id the Sorts of A is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding ManySortedFunction of the Sorts of A, the Sorts of A
b is Element of the carrier of S
the Sorts of A . b is non empty set
id ( the Sorts of A . b) is non empty Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Function-like one-to-one total V29( the Sorts of A . b, the Sorts of A . b) V30( the Sorts of A . b) V31( the Sorts of A . b, the Sorts of A . b) reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
a is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
a . b is non empty Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Function-like total V29( the Sorts of A . b, the Sorts of A . b) Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
a is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
a is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
b is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
the Sorts of A . s is non empty set
(S,A,R) . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
a is Element of the Sorts of A . s
b is Element of the Sorts of A . s
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,P) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
i is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
the Sorts of A . s is non empty set
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
x is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
b is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
b . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
y is Element of the Sorts of A . s
a is Element of the Sorts of A . s
[y,a] is V26() set
{y,a} is non empty set
{y} is non empty trivial V42(1) set
{{y,a},{y}} is non empty set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
x . y is Element of the Sorts of A . s
x . a is Element of the Sorts of A . s
s is Element of the Sorts of A . s
x is Element of the Sorts of A . s
[s,x] is V26() set
{s,x} is non empty set
{s} is non empty trivial V42(1) set
{{s,x},{s}} is non empty set
y is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
y . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
(y . s) . s is Element of the Sorts of A . s
(y . s) . x is Element of the Sorts of A . s
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,(S,A,R)) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
a is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,(S,A,R)) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
a is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is set
(S,A,R) . s is set
a is Element of the carrier of S
R . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
the Element of R . a is Element of R . a
(S,A,R) . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is set
(S,A,R) . s is set
a is Element of the carrier of S
R . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
the Element of R . a is Element of R . a
(S,A,R) . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is set
(S,A,R) . s is set
a is Element of the carrier of S
R . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
the Element of R . a is Element of R . a
(S,A,R) . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,(S,A,R)) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,(S,A,R)) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like set
bool [: the carrier of S, the carrier of S:] is set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
the Sorts of A . s is non empty set
(S,A,R) . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
a is Element of the Sorts of A . s
b is Element of the Sorts of A . s
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,(S,A,R)) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
P is Element of the carrier of S
the Sorts of A . P is non empty set
P is Element of the Sorts of A . P
P is Element of the Sorts of A . P
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
(S,A,R) . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
[:( the Sorts of A . P),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . P):] is set
i is non empty Relation-like the Sorts of A . P -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . P, the Sorts of A . s) (S,A,P,s)
i . P is Element of the Sorts of A . s
i . P is Element of the Sorts of A . s
s is Element of the carrier of S
the Sorts of A . s is non empty set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
y is Element of the Sorts of A . s
a is Element of the Sorts of A . s
[y,a] is V26() set
{y,a} is non empty set
{y} is non empty trivial V42(1) set
{{y,a},{y}} is non empty set
b is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
b . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
(b . s) . y is Element of the Sorts of A . s
(b . s) . a is Element of the Sorts of A . s
x is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) (S,A,s,s)
u is Element of the Sorts of A . s
v is Element of the Sorts of A . s
[u,v] is V26() set
{u,v} is non empty set
{u} is non empty trivial V42(1) set
{{u,v},{u}} is non empty set
t is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) (S,A,s,s)
h is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
h . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
(h . s) . u is Element of the Sorts of A . s
t . ((h . s) . u) is Element of the Sorts of A . s
(h . s) . v is Element of the Sorts of A . s
t . ((h . s) . v) is Element of the Sorts of A . s
P is Element of the carrier of S
the Sorts of A . P is non empty set
R . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
[:( the Sorts of A . P),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . P):] is set
P is Element of the Sorts of A . P
P is Element of the Sorts of A . P
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
s is non empty Relation-like the Sorts of A . P -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . P, the Sorts of A . s) (S,A,P,s)
i is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
i . P is non empty Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . P, the Sorts of A . P) Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
(i . P) . P is Element of the Sorts of A . P
s . ((i . P) . P) is Element of the Sorts of A . s
(i . P) . P is Element of the Sorts of A . P
s . ((i . P) . P) is Element of the Sorts of A . s
P is Element of the Sorts of A . P
P is Element of the Sorts of A . P
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
s is non empty Relation-like the Sorts of A . P -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . P, the Sorts of A . s) (S,A,P,s)
i is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
i . P is non empty Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Function-like total V29( the Sorts of A . P, the Sorts of A . P) Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
(i . P) . P is Element of the Sorts of A . P
s . ((i . P) . P) is Element of the Sorts of A . s
(i . P) . P is Element of the Sorts of A . P
s . ((i . P) . P) is Element of the Sorts of A . s
[((i . P) . P),((i . P) . P)] is V26() set
{((i . P) . P),((i . P) . P)} is non empty set
{((i . P) . P)} is non empty trivial V42(1) set
{{((i . P) . P),((i . P) . P)},{((i . P) . P)}} is non empty set
(S,A,R) . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
S is set
[:S,S:] is Relation-like set
bool [:S,S:] is set
R is Relation-like S -defined S -valued Element of bool [:S,S:]
A is Relation-like S -defined S -valued Element of bool [:S,S:]
a is set
[a,a] is V26() set
{a,a} is non empty set
{a} is non empty trivial V42(1) set
{{a,a},{a}} is non empty set
field R is set
proj1 R is set
proj2 R is set
(proj1 R) \/ (proj2 R) is set
dom R is Element of bool S
bool S is set
a is set
b is set
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
[b,a] is V26() set
{b,a} is non empty set
{b} is non empty trivial V42(1) set
{{b,a},{b}} is non empty set
a is set
b is set
P is set
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
[b,P] is V26() set
{b,P} is non empty set
{b} is non empty trivial V42(1) set
{{b,P},{b}} is non empty set
[a,P] is V26() set
{a,P} is non empty set
{{a,P},{a}} is non empty set
S is set
[:S,S:] is Relation-like set
bool [:S,S:] is set
A is Relation-like S -defined S -valued Element of bool [:S,S:]
R is Relation-like S -defined S -valued total V29(S,S) reflexive symmetric transitive Element of bool [:S,S:]
s is set
a is set
[s,a] is V26() set
{s,a} is non empty set
{s} is non empty trivial V42(1) set
{{s,a},{s}} is non empty set
A ~ is Relation-like S -defined S -valued Element of bool [:S,S:]
A \/ (A ~) is Relation-like S -defined S -valued Element of bool [:S,S:]
b is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of A \/ (A ~)
b . 1 is set
len b is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
b . (len b) is set
dom b is non empty Element of bool NAT
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
b . P is set
[s,(b . P)] is V26() set
{s,(b . P)} is non empty set
{{s,(b . P)},{s}} is non empty set
P + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
b . (P + 1) is set
[s,(b . (P + 1))] is V26() set
{s,(b . (P + 1))} is non empty set
{{s,(b . (P + 1))},{s}} is non empty set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
[(b . P),(b . (P + 1))] is V26() set
{(b . P),(b . (P + 1))} is non empty set
{(b . P)} is non empty trivial V42(1) set
{{(b . P),(b . (P + 1))},{(b . P)}} is non empty set
[(b . (P + 1)),(b . P)] is V26() set
{(b . (P + 1)),(b . P)} is non empty set
{(b . (P + 1))} is non empty trivial V42(1) set
{{(b . (P + 1)),(b . P)},{(b . (P + 1))}} is non empty set
P is Element of S
P is Element of S
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
b . 0 is set
[s,(b . 0)] is V26() set
{s,(b . 0)} is non empty set
{{s,(b . 0)},{s}} is non empty set
S is non empty set
[:S,S:] is Relation-like set
bool [:S,S:] is set
A is Relation-like S -defined S -valued Element of bool [:S,S:]
EqCl A is Relation-like S -defined S -valued total V29(S,S) reflexive symmetric transitive Element of bool [:S,S:]
R is Relation-like S -defined S -valued Element of bool [:S,S:]
s is set
a is set
[s,a] is V26() set
{s,a} is non empty set
{s} is non empty trivial V42(1) set
{{s,a},{s}} is non empty set
a is Relation-like S -defined S -valued total V29(S,S) reflexive symmetric transitive Element of bool [:S,S:]
s is Relation-like S -defined S -valued total V29(S,S) reflexive symmetric transitive Element of bool [:S,S:]
b is set
P is set
[b,P] is V26() set
{b,P} is non empty set
{b} is non empty trivial V42(1) set
{{b,P},{b}} is non empty set
a is set
b is set
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
a is Element of S
b is Element of S
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
P is Element of S
P is Element of S
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
S is non empty set
A is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
R is non empty Relation-like S -defined Function-like total Relation-yielding ManySortedRelation of A,A
EqCl R is non empty Relation-like S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of A,A
s is Element of S
A . s is non empty set
(EqCl R) . s is Relation-like A . s -defined A . s -valued Element of bool [:(A . s),(A . s):]
[:(A . s),(A . s):] is Relation-like set
bool [:(A . s),(A . s):] is set
R . s is Relation-like A . s -defined A . s -valued Element of bool [:(A . s),(A . s):]
EqCl (R . s) is Relation-like A . s -defined A . s -valued total V29(A . s,A . s) reflexive symmetric transitive Element of bool [:(A . s),(A . s):]
a is Element of A . s
b is Element of A . s
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
P is Element of A . s
P is Element of A . s
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
EqCl R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
EqCl R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
s is set
R . s is set
(S,A,R) . s is set
a is Element of the carrier of S
the Sorts of A . a is non empty set
(S,A,R) . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued total V29( the Sorts of A . a, the Sorts of A . a) reflexive symmetric transitive Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
EqCl (R . a) is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued total V29( the Sorts of A . a, the Sorts of A . a) reflexive symmetric transitive Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
EqCl R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
a is set
(S,A,R) . a is set
s . a is set
b is Element of the carrier of S
the Sorts of A . b is non empty set
(S,A,R) . b is non empty Relation-like the Sorts of A . b -defined the Sorts of A . b -valued total V29( the Sorts of A . b, the Sorts of A . b) reflexive symmetric transitive Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
R . b is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
EqCl (R . b) is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued total V29( the Sorts of A . b, the Sorts of A . b) reflexive symmetric transitive Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
s . b is non empty Relation-like the Sorts of A . b -defined the Sorts of A . b -valued total V29( the Sorts of A . b, the Sorts of A . b) reflexive symmetric transitive Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
the Sorts of A . s is non empty set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
a is Element of the Sorts of A . s
b is Element of the Sorts of A . s
(R . s) ~ is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
(R . s) \/ ((R . s) ~) is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
P is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of (R . s) \/ ((R . s) ~)
P . 1 is set
len P is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . (len P) is set
P is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
P . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Function-like total V29( the Sorts of A . s, the Sorts of A . s) Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
(P . s) . a is Element of the Sorts of A . s
(P . s) . b is Element of the Sorts of A . s
dom P is non empty Element of bool NAT
P is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
P . P is set
(P . s) . (P . P) is set
P + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . (P + 1) is set
(P . s) . (P . (P + 1)) is set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
[(P . P),(P . (P + 1))] is V26() set
{(P . P),(P . (P + 1))} is non empty set
{(P . P)} is non empty trivial V42(1) set
{{(P . P),(P . (P + 1))},{(P . P)}} is non empty set
[(P . (P + 1)),(P . P)] is V26() set
{(P . (P + 1)),(P . P)} is non empty set
{(P . (P + 1))} is non empty trivial V42(1) set
{{(P . (P + 1)),(P . P)},{(P . (P + 1))}} is non empty set
i is Element of the Sorts of A . s
(P . s) . i is Element of the Sorts of A . s
s is Element of the Sorts of A . s
(P . s) . s is Element of the Sorts of A . s
[((P . s) . i),((P . s) . s)] is V26() set
{((P . s) . i),((P . s) . s)} is non empty set
{((P . s) . i)} is non empty trivial V42(1) set
{{((P . s) . i),((P . s) . s)},{((P . s) . i)}} is non empty set
[((P . s) . s),((P . s) . i)] is V26() set
{((P . s) . s),((P . s) . i)} is non empty set
{((P . s) . s)} is non empty trivial V42(1) set
{{((P . s) . s),((P . s) . i)},{((P . s) . s)}} is non empty set
P . 0 is set
(P . s) . (P . 0) is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
EqCl R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
a is Element of the carrier of S
(S,A,R) . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
s . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . a, the Sorts of A . a) Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
b is set
P is set
[b,P] is V26() set
{b,P} is non empty set
{b} is non empty trivial V42(1) set
{{b,P},{b}} is non empty set
(s . a) . b is set
(s . a) . P is set
[((s . a) . b),((s . a) . P)] is V26() set
{((s . a) . b),((s . a) . P)} is non empty set
{((s . a) . b)} is non empty trivial V42(1) set
{{((s . a) . b),((s . a) . P)},{((s . a) . b)}} is non empty set
(S,A,R) . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued total V29( the Sorts of A . a, the Sorts of A . a) reflexive symmetric transitive Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
P is Element of the Sorts of A . a
P is Element of the Sorts of A . a
(s . a) . P is Element of the Sorts of A . a
(s . a) . P is Element of the Sorts of A . a
S is non empty non void feasible ManySortedSign
A is non-empty (S) MSAlgebra over S
the carrier of S is non empty set
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
EqCl R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
the Sorts of A . s is non empty set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
a is Element of the carrier of S
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
b is Element of the Sorts of A . s
P is Element of the Sorts of A . s
(R . s) ~ is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
(R . s) \/ ((R . s) ~) is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
P is non empty Relation-like NAT -defined Function-like V35() FinSequence-like FinSubsequence-like RedSequence of (R . s) \/ ((R . s) ~)
P . 1 is set
len P is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . (len P) is set
P is Relation-like Function-like set
P . b is set
P . P is set
dom P is non empty Element of bool NAT
i is V4() V5() V6() V10() V11() ext-real non negative V32() V35() V40() Element of NAT
P . i is set
P . (P . i) is set
i + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
P . (i + 1) is set
P . (P . (i + 1)) is set
0 + 1 is non empty V4() V5() V6() V10() V11() ext-real positive non negative V32() V35() V40() Element of NAT
[(P . i),(P . (i + 1))] is V26() set
{(P . i),(P . (i + 1))} is non empty set
{(P . i)} is non empty trivial V42(1) set
{{(P . i),(P . (i + 1))},{(P . i)}} is non empty set
[(P . (i + 1)),(P . i)] is V26() set
{(P . (i + 1)),(P . i)} is non empty set
{(P . (i + 1))} is non empty trivial V42(1) set
{{(P . (i + 1)),(P . i)},{(P . (i + 1))}} is non empty set
s is Element of the Sorts of A . s
P . s is set
x is Element of the Sorts of A . s
P . x is set
[(P . s),(P . x)] is V26() set
{(P . s),(P . x)} is non empty set
{(P . s)} is non empty trivial V42(1) set
{{(P . s),(P . x)},{(P . s)}} is non empty set
[(P . x),(P . s)] is V26() set
{(P . x),(P . s)} is non empty set
{(P . x)} is non empty trivial V42(1) set
{{(P . x),(P . s)},{(P . x)}} is non empty set
P . 0 is set
P . (P . 0) is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
EqCl R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
a is Element of the carrier of S
(S,A,R) . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
the Sorts of A . s is non empty set
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
(S,A,R) . a is non empty Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
b is Relation-like Function-like set
[:( the Sorts of A . s),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . a):] is set
P is set
P is set
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
b . P is set
b . P is set
[(b . P),(b . P)] is V26() set
{(b . P),(b . P)} is non empty set
{(b . P)} is non empty trivial V42(1) set
{{(b . P),(b . P)},{(b . P)}} is non empty set
(S,A,R) . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued total V29( the Sorts of A . s, the Sorts of A . s) reflexive symmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
i is Element of the Sorts of A . s
s is Element of the Sorts of A . s
R . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
P is non empty Relation-like the Sorts of A . s -defined the Sorts of A . a -valued Function-like total V29( the Sorts of A . s, the Sorts of A . a) Element of bool [:( the Sorts of A . s),( the Sorts of A . a):]
P . i is Element of the Sorts of A . a
P . s is Element of the Sorts of A . a
S is non empty non void feasible ManySortedSign
A is non-empty (S) MSAlgebra over S
the carrier of S is non empty set
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
EqCl R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty set
A is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
s is non empty Relation-like S -defined Function-like total Relation-yielding ManySortedRelation of A,A
R is non empty Relation-like S -defined Function-like total Relation-yielding ManySortedRelation of A,A
a is set
A . a is set
[:(A . a),(A . a):] is Relation-like set
bool [:(A . a),(A . a):] is set
s . a is set
b is Relation-like A . a -defined A . a -valued Element of bool [:(A . a),(A . a):]
P is Element of S
A . P is non empty set
s . P is Relation-like A . P -defined A . P -valued Element of bool [:(A . P),(A . P):]
[:(A . P),(A . P):] is Relation-like set
bool [:(A . P),(A . P):] is set
R . P is Relation-like A . P -defined A . P -valued Element of bool [:(A . P),(A . P):]
P is set
P is set
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
a is non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding (S,A)
b is Element of the carrier of S
s . b is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
the Sorts of A . b is non empty set
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
a . b is non empty Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Function-like total V29( the Sorts of A . b, the Sorts of A . b) Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
P is set
P is set
[P,P] is V26() set
{P,P} is non empty set
{P} is non empty trivial V42(1) set
{{P,P},{P}} is non empty set
(a . b) . P is set
(a . b) . P is set
[((a . b) . P),((a . b) . P)] is V26() set
{((a . b) . P),((a . b) . P)} is non empty set
{((a . b) . P)} is non empty trivial V42(1) set
{{((a . b) . P),((a . b) . P)},{((a . b) . P)}} is non empty set
P is Element of the Sorts of A . b
(a . b) . P is Element of the Sorts of A . b
i is Element of the Sorts of A . b
(a . b) . i is Element of the Sorts of A . b
(S,A,R) . b is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
s is Element of the Sorts of A . b
x is Element of the Sorts of A . b
a is Element of the carrier of S
b is Element of the carrier of S
s . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
the Sorts of A . a is non empty set
[:( the Sorts of A . a),( the Sorts of A . a):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . a):] is set
s . b is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
the Sorts of A . b is non empty set
[:( the Sorts of A . b),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . b),( the Sorts of A . b):] is set
P is Relation-like Function-like set
[:( the Sorts of A . a),( the Sorts of A . b):] is Relation-like set
bool [:( the Sorts of A . a),( the Sorts of A . b):] is set
P is set
i is set
[P,i] is V26() set
{P,i} is non empty set
{P} is non empty trivial V42(1) set
{{P,i},{P}} is non empty set
P . P is set
P . i is set
[(P . P),(P . i)] is V26() set
{(P . P),(P . i)} is non empty set
{(P . P)} is non empty trivial V42(1) set
{{(P . P),(P . i)},{(P . P)}} is non empty set
(S,A,R) . a is Relation-like the Sorts of A . a -defined the Sorts of A . a -valued Element of bool [:( the Sorts of A . a),( the Sorts of A . a):]
s is Element of the Sorts of A . a
x is Element of the Sorts of A . a
(S,A,R) . b is Relation-like the Sorts of A . b -defined the Sorts of A . b -valued Element of bool [:( the Sorts of A . b),( the Sorts of A . b):]
P . s is set
P . x is set
P is non empty Relation-like the Sorts of A . a -defined the Sorts of A . b -valued Function-like total V29( the Sorts of A . a, the Sorts of A . b) Element of bool [:( the Sorts of A . a),( the Sorts of A . b):]
P . x is Element of the Sorts of A . b
P . s is Element of the Sorts of A . b
S is non empty set
A is non empty Relation-like non-empty non empty-yielding S -defined Function-like total set
R is non empty Relation-like S -defined Function-like total Relation-yielding ManySortedRelation of A,A
s is non empty Relation-like S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of A,A
a is Element of S
A . a is non empty set
R . a is Relation-like A . a -defined A . a -valued Element of bool [:(A . a),(A . a):]
[:(A . a),(A . a):] is Relation-like set
bool [:(A . a),(A . a):] is set
s . a is Relation-like A . a -defined A . a -valued Element of bool [:(A . a),(A . a):]
b is Element of A . a
P is Element of A . a
[b,P] is V26() set
{b,P} is non empty set
{b} is non empty trivial V42(1) set
{{b,P},{b}} is non empty set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like (S,A) (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
a is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like (S,A) (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
a is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
b is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like (S,A) (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
P is set
R . P is set
b . P is set
P is Element of the carrier of S
the Sorts of A . P is non empty set
R . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
[:( the Sorts of A . P),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . P):] is set
b . P is non empty Relation-like the Sorts of A . P -defined the Sorts of A . P -valued total V29( the Sorts of A . P, the Sorts of A . P) reflexive symmetric transitive Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
P is set
i is set
[P,i] is V26() set
{P,i} is non empty set
{P} is non empty trivial V42(1) set
{{P,i},{P}} is non empty set
(S,A,R) . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
s is Element of the Sorts of A . P
x is Element of the Sorts of A . P
P is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like (S,A) (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
P is set
b . P is set
P . P is set
P is Element of the carrier of S
the Sorts of A . P is non empty set
b . P is non empty Relation-like the Sorts of A . P -defined the Sorts of A . P -valued total V29( the Sorts of A . P, the Sorts of A . P) reflexive symmetric transitive Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
[:( the Sorts of A . P),( the Sorts of A . P):] is Relation-like set
bool [:( the Sorts of A . P),( the Sorts of A . P):] is set
P . P is non empty Relation-like the Sorts of A . P -defined the Sorts of A . P -valued total V29( the Sorts of A . P, the Sorts of A . P) reflexive symmetric transitive Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
i is set
s is set
[i,s] is V26() set
{i,s} is non empty set
{i} is non empty trivial V42(1) set
{{i,s},{i}} is non empty set
(S,A,R) . P is Relation-like the Sorts of A . P -defined the Sorts of A . P -valued Element of bool [:( the Sorts of A . P),( the Sorts of A . P):]
x is Element of the Sorts of A . P
y is Element of the Sorts of A . P
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
EqCl R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like (S,A) (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like (S,A) (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
s is Element of the carrier of S
the Sorts of A . s is non empty set
(S,A,R) . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued total V29( the Sorts of A . s, the Sorts of A . s) reflexive symmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
(S,A,R) . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
a is Element of the Sorts of A . s
b is Element of the Sorts of A . s
[a,b] is V26() set
{a,b} is non empty set
{a} is non empty trivial V42(1) set
{{a,b},{a}} is non empty set
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
P is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
P is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like (S,A) (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
i is set
R . i is set
P . i is set
s is Element of the carrier of S
the Sorts of A . s is non empty set
R . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
[:( the Sorts of A . s),( the Sorts of A . s):] is Relation-like set
bool [:( the Sorts of A . s),( the Sorts of A . s):] is set
P . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued total V29( the Sorts of A . s, the Sorts of A . s) reflexive symmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
x is set
y is set
[x,y] is V26() set
{x,y} is non empty set
{x} is non empty trivial V42(1) set
{{x,y},{x}} is non empty set
(S,A,R) . s is Relation-like the Sorts of A . s -defined the Sorts of A . s -valued Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
a is Element of the Sorts of A . s
b is Element of the Sorts of A . s
P . s is non empty Relation-like the Sorts of A . s -defined the Sorts of A . s -valued total V29( the Sorts of A . s, the Sorts of A . s) reflexive symmetric transitive Element of bool [:( the Sorts of A . s),( the Sorts of A . s):]
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty (S) MSAlgebra over S
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like (S,A) (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
(S,A,(S,A,R)) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like MSEquivalence-like (S,A) (S,A) (S,A) ManySortedRelation of the Sorts of A, the Sorts of A
EqCl (S,A,R) is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A