:: OSALG_4 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() V47() countable denumerable Element of bool REAL
bool REAL is non empty set

NAT is non empty V4() V5() V6() V47() countable denumerable set
bool NAT is non empty set
bool NAT is non empty set
{} is set

1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive V33() Element of NAT
{{},1} is set
2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive V33() Element of NAT
3 is non empty V4() V5() V6() V10() V11() V12() ext-real positive V33() Element of NAT
0 is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT

the carrier of S is non empty set

the carrier of S --> the Relation-like set is non empty Relation-like the carrier of S -defined {} -valued Function-like constant total V30( the carrier of S,{}) Element of bool [: the carrier of S,{}:]
{} is set
[: the carrier of S,{}:] is Relation-like set
bool [: the carrier of S,{}:] is non empty set
R is non empty Relation-like the carrier of S -defined Function-like total set
mc is Element of the carrier of S
qa is Element of the carrier of S
R . mc is set
R . qa is set

dom mc is non empty Element of bool the carrier of S
bool the carrier of S is non empty set
qa is set
mc . qa is set

the carrier of S is non empty set
U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total set

the carrier of S is non empty set
U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total set

the carrier of S --> R is non empty Relation-like the carrier of S -defined {R} -valued Function-like constant total V30( the carrier of S,{R}) Element of bool [: the carrier of S,{R}:]
{R} is set
[: the carrier of S,{R}:] is Relation-like set
bool [: the carrier of S,{R}:] is non empty set
qa is non empty Relation-like the carrier of S -defined Function-like total set
S1 is set
qa . S1 is set
U1 . S1 is set
U2 . S1 is set
[:(U1 . S1),(U2 . S1):] is Relation-like set
bool [:(U1 . S1),(U2 . S1):] is non empty set
S1O is Element of the carrier of S
sqa is Element of the carrier of S
U1 . S1O is set
U2 . S1O is set
qa . S1O is set
qa . sqa is set
s1 is set
s2 is set
[s1,s2] is set
{s1,s2} is set
{s1} is set
{{s1,s2},{s1}} is set
S1 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of U1,U2

the carrier of S is non empty set

the carrier of S is non empty set
U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of U1,U2
mc is Element of the carrier of S
qa is Element of the carrier of S
F . mc is set
F . qa is set
F . mc is Relation-like U1 . mc -defined U2 . mc -valued Element of bool [:(U1 . mc),(U2 . mc):]
U1 . mc is set
U2 . mc is set
[:(U1 . mc),(U2 . mc):] is Relation-like set
bool [:(U1 . mc),(U2 . mc):] is non empty set
F . qa is Relation-like U1 . qa -defined U2 . qa -valued Element of bool [:(U1 . qa),(U2 . qa):]
U1 . qa is set
U2 . qa is set
[:(U1 . qa),(U2 . qa):] is Relation-like set
bool [:(U1 . qa),(U2 . qa):] is non empty set
qh is set
S1 is set
[qh,S1] is set
{qh,S1} is set
{qh} is set
{{qh,S1},{qh}} is set

the carrier of S is non empty set
U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is non empty Relation-like the carrier of S -defined Function-like total set
F is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of U1,U2

the carrier of S is non empty set

the carrier of S is non empty set
U1 is order-sorted MSAlgebra over S
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set

the non empty Relation-like the carrier of S -defined Function-like total Relation-yielding order-sorted (S,U2,U2) ManySortedRelation of U2,U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding order-sorted (S,U2,U2) ManySortedRelation of U2,U2
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of U1, the Sorts of U1

the carrier of S is non empty set
U1 is order-sorted MSAlgebra over S
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set

dom U2 is set
F is non empty Relation-like the carrier of S -defined Function-like total set
R is set
F . R is set
the Sorts of U1 . R is set
[:( the Sorts of U1 . R),( the Sorts of U1 . R):] is Relation-like set
bool [:( the Sorts of U1 . R),( the Sorts of U1 . R):] is non empty set
id ( the Sorts of U1 . R) is Relation-like the Sorts of U1 . R -defined the Sorts of U1 . R -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of U1 . R),( the Sorts of U1 . R):]
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of U1, the Sorts of U1
mc is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of U1, the Sorts of U1
S1 is Element of the carrier of S
S1O is Element of the carrier of S
the Sorts of U1 . S1 is set
mc . S1 is Relation-like the Sorts of U1 . S1 -defined the Sorts of U1 . S1 -valued Element of bool [:( the Sorts of U1 . S1),( the Sorts of U1 . S1):]
[:( the Sorts of U1 . S1),( the Sorts of U1 . S1):] is Relation-like set
bool [:( the Sorts of U1 . S1),( the Sorts of U1 . S1):] is non empty set
mc . S1O is Relation-like the Sorts of U1 . S1O -defined the Sorts of U1 . S1O -valued Element of bool [:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):]
the Sorts of U1 . S1O is set
[:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):] is Relation-like set
bool [:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):] is non empty set
s2 is set
a1 is set
[s2,a1] is set
{s2,a1} is set
{s2} is set
{{s2,a1},{s2}} is set

qh . S1 is set
id (qh . S1) is Relation-like qh . S1 -defined qh . S1 -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:(qh . S1),(qh . S1):]
[:(qh . S1),(qh . S1):] is Relation-like set
bool [:(qh . S1),(qh . S1):] is non empty set
qh . S1O is set
id (qh . S1O) is Relation-like qh . S1O -defined qh . S1O -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:(qh . S1O),(qh . S1O):]
[:(qh . S1O),(qh . S1O):] is Relation-like set
bool [:(qh . S1O),(qh . S1O):] is non empty set
sqa is Element of the carrier of S
qh . sqa is set
s1 is Element of the carrier of S
qh . s1 is set
qh is set
the Sorts of U1 . qh is set
[:( the Sorts of U1 . qh),( the Sorts of U1 . qh):] is Relation-like set
bool [:( the Sorts of U1 . qh),( the Sorts of U1 . qh):] is non empty set
mc . qh is set
S1 is Relation-like the Sorts of U1 . qh -defined the Sorts of U1 . qh -valued Element of bool [:( the Sorts of U1 . qh),( the Sorts of U1 . qh):]
id ( the Sorts of U1 . qh) is Relation-like the Sorts of U1 . qh -defined the Sorts of U1 . qh -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of U1 . qh),( the Sorts of U1 . qh):]

U1 is non-empty order-sorted MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set

dom U2 is set
F is non empty Relation-like the carrier of S -defined Function-like total set
R is set
F . R is set
the Sorts of U1 . R is set
[:( the Sorts of U1 . R),( the Sorts of U1 . R):] is Relation-like set
bool [:( the Sorts of U1 . R),( the Sorts of U1 . R):] is non empty set
id ( the Sorts of U1 . R) is Relation-like the Sorts of U1 . R -defined the Sorts of U1 . R -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of U1 . R),( the Sorts of U1 . R):]
R is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of U1, the Sorts of U1
mc is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding ManySortedRelation of the Sorts of U1, the Sorts of U1
qa is set
the Sorts of U1 . qa is set
[:( the Sorts of U1 . qa),( the Sorts of U1 . qa):] is Relation-like set
bool [:( the Sorts of U1 . qa),( the Sorts of U1 . qa):] is non empty set
mc . qa is set
qh is Relation-like the Sorts of U1 . qa -defined the Sorts of U1 . qa -valued Element of bool [:( the Sorts of U1 . qa),( the Sorts of U1 . qa):]
id ( the Sorts of U1 . qa) is Relation-like the Sorts of U1 . qa -defined the Sorts of U1 . qa -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of U1 . qa),( the Sorts of U1 . qa):]
qa is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like ManySortedRelation of the Sorts of U1, the Sorts of U1
S1O is Element of the carrier of S
sqa is Element of the carrier of S
the Sorts of U1 . S1O is non empty set
qa . S1O is Relation-like the Sorts of U1 . S1O -defined the Sorts of U1 . S1O -valued Element of bool [:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):]
[:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):] is non empty Relation-like set
bool [:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):] is non empty set
qa . sqa is Relation-like the Sorts of U1 . sqa -defined the Sorts of U1 . sqa -valued Element of bool [:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):]
the Sorts of U1 . sqa is non empty set
[:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):] is non empty Relation-like set
bool [:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):] is non empty set
a1 is set
x is set
[a1,x] is set
{a1,x} is set
{a1} is set
{{a1,x},{a1}} is set
qa . S1O is Relation-like the Sorts of U1 . S1O -defined the Sorts of U1 . S1O -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):]

S1 . S1O is set
id (S1 . S1O) is Relation-like S1 . S1O -defined S1 . S1O -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:(S1 . S1O),(S1 . S1O):]
[:(S1 . S1O),(S1 . S1O):] is Relation-like set
bool [:(S1 . S1O),(S1 . S1O):] is non empty set
qa . sqa is Relation-like the Sorts of U1 . sqa -defined the Sorts of U1 . sqa -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):]
S1 . sqa is set
id (S1 . sqa) is Relation-like S1 . sqa -defined S1 . sqa -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:(S1 . sqa),(S1 . sqa):]
[:(S1 . sqa),(S1 . sqa):] is Relation-like set
bool [:(S1 . sqa),(S1 . sqa):] is non empty set
s1 is Element of the carrier of S
S1 . s1 is set
s2 is Element of the carrier of S
S1 . s2 is set
S1 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like (S,U1)
the carrier' of S is non empty set
S1O is Element of the carrier' of S
Args (S1O,U1) is non empty functional Element of rng ( the Sorts of U1 #)
the Sorts of U1 # is non empty Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like total set
the carrier of S * is non empty functional FinSequence-membered M10( the carrier of S)
rng ( the Sorts of U1 #) is non empty with_non-empty_elements set

Result (S1O,U1) is non empty Element of rng the Sorts of U1
rng the Sorts of U1 is non empty with_non-empty_elements set
Den (S1O,U1) is Relation-like Args (S1O,U1) -defined Result (S1O,U1) -valued Function-like V30( Args (S1O,U1), Result (S1O,U1)) Element of bool [:(Args (S1O,U1)),(Result (S1O,U1)):]
[:(Args (S1O,U1)),(Result (S1O,U1)):] is non empty Relation-like set
bool [:(Args (S1O,U1)),(Result (S1O,U1)):] is non empty set
the_result_sort_of S1O is Element of the carrier of S
S1 . () is Relation-like the Sorts of U1 . () -defined the Sorts of U1 . () -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . ()),( the Sorts of U1 . ()):]
the Sorts of U1 . () is non empty set
[:( the Sorts of U1 . ()),( the Sorts of U1 . ()):] is non empty Relation-like set
bool [:( the Sorts of U1 . ()),( the Sorts of U1 . ()):] is non empty set
sqa is Relation-like Function-like Element of Args (S1O,U1)
dom sqa is set
s1 is Relation-like Function-like Element of Args (S1O,U1)
(Den (S1O,U1)) . sqa is Element of Result (S1O,U1)
(Den (S1O,U1)) . s1 is Element of Result (S1O,U1)
[((Den (S1O,U1)) . sqa),((Den (S1O,U1)) . s1)] is set
{((Den (S1O,U1)) . sqa),((Den (S1O,U1)) . s1)} is set
{((Den (S1O,U1)) . sqa)} is set
{{((Den (S1O,U1)) . sqa),((Den (S1O,U1)) . s1)},{((Den (S1O,U1)) . sqa)}} is set
dom (the_arity_of S1O) is countable Element of bool NAT
a1 is set
sqa . a1 is set
s1 . a1 is set
x is V4() V5() V6() V10() V11() V12() ext-real V33() set
(the_arity_of S1O) . x is set
rng (the_arity_of S1O) is Element of bool the carrier of S
bool the carrier of S is non empty set
S1 . ((the_arity_of S1O) . x) is set
the Sorts of U1 . ((the_arity_of S1O) . x) is set
id ( the Sorts of U1 . ((the_arity_of S1O) . x)) is Relation-like the Sorts of U1 . ((the_arity_of S1O) . x) -defined the Sorts of U1 . ((the_arity_of S1O) . x) -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of U1 . ((the_arity_of S1O) . x)),( the Sorts of U1 . ((the_arity_of S1O) . x)):]
[:( the Sorts of U1 . ((the_arity_of S1O) . x)),( the Sorts of U1 . ((the_arity_of S1O) . x)):] is Relation-like set
bool [:( the Sorts of U1 . ((the_arity_of S1O) . x)),( the Sorts of U1 . ((the_arity_of S1O) . x)):] is non empty set
(the_arity_of S1O) /. x is Element of the carrier of S
sqa . x is set
s1 . x is set
[(sqa . x),(s1 . x)] is set
{(sqa . x),(s1 . x)} is set
{(sqa . x)} is set
{{(sqa . x),(s1 . x)},{(sqa . x)}} is set
id ( the Sorts of U1 . ()) is non empty Relation-like the Sorts of U1 . () -defined the Sorts of U1 . () -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of U1 . ()),( the Sorts of U1 . ()):]
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like V30( the carrier' of S, the carrier of S) Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
dom the ResultSort of S is Element of bool the carrier' of S
bool the carrier' of S is non empty set
the ResultSort of S * the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like total set
dom ( the ResultSort of S * the Sorts of U1) is non empty Element of bool the carrier' of S
( the ResultSort of S * the Sorts of U1) . S1O is non empty set
the ResultSort of S . S1O is Element of the carrier of S
the Sorts of U1 . ( the ResultSort of S . S1O) is non empty set
dom s1 is set

the carrier of S is non empty set
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
the InternalRel of 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:]
{ [b1,b2] where b1, b2 is Element of the carrier of S : ( b1 in the carrier of S & b2 in the carrier of S & S1[b1,b2] ) } is set
U2 is set
F is Element of the carrier of S
R is Element of the carrier of S
[F,R] is set
{F,R} is set
{F} is set
{{F,R},{F}} is set

len mc is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
mc . 1 is set
mc . (len mc) is set
F is set
R is set
[F,R] is set
{F,R} is set
{F} is set
{{F,R},{F}} is set
mc is Element of the carrier of S
qa is Element of the carrier of S
[mc,qa] is set
{mc,qa} is set
{mc} is set
{{mc,qa},{mc}} is set

len qh is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
qh . 1 is set
qh . (len qh) is set

len mc is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
mc . 1 is set
mc . (len mc) is set
F is set
R is set
[F,R] is set
{F,R} is set
{F} is set
{{F,R},{F}} is set
U2 is Relation-like the carrier of S -defined the carrier of S -valued Element of bool [: the carrier of S, the carrier of S:]

len mc is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
mc . 1 is set
mc . (len mc) is set

len qa is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
qa . 1 is set
qa . (len qa) is set
qh is V4() V5() V6() V10() V11() V12() ext-real V33() set
qa . qh is set
qh - 1 is V11() V12() ext-real V33() set
qa . (qh - 1) is set
[(qa . qh),(qa . (qh - 1))] is set
{(qa . qh),(qa . (qh - 1))} is set
{(qa . qh)} is set
{{(qa . qh),(qa . (qh - 1))},{(qa . qh)}} is set
[(qa . (qh - 1)),(qa . qh)] is set
{(qa . (qh - 1)),(qa . qh)} is set
{(qa . (qh - 1))} is set
{{(qa . (qh - 1)),(qa . qh)},{(qa . (qh - 1))}} is set

(len mc) - qh is V11() V12() ext-real V33() set
((len mc) - qh) + 2 is V11() V12() ext-real V33() set
2 + 0 is V11() V12() ext-real V33() set
2 - 1 is V11() V12() ext-real V33() set
(len qa) - 0 is V11() V12() ext-real V33() set
S1O is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
(len mc) - (qh - 1) is V11() V12() ext-real V33() set
((len mc) - (qh - 1)) + 1 is V11() V12() ext-real V33() set
mc . (((len mc) - (qh - 1)) + 1) is set
mc . (((len mc) - qh) + 2) is set
(len mc) - 2 is V11() V12() ext-real V33() set
((len mc) - 2) + 2 is V11() V12() ext-real V33() set
sqa is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
sqa - 1 is V11() V12() ext-real V33() set
mc . (sqa - 1) is set
((len mc) - qh) + (2 - 1) is V11() V12() ext-real V33() set
mc . (((len mc) - qh) + (2 - 1)) is set
[R,F] is set
{R,F} is set
{R} is set
{{R,F},{R}} is set

len qa is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
qa . 1 is set
qa . (len qa) is set
F is set

rng <*F,F*> is non empty set
{F,F} is set
{F} is set

len mc is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
mc . 1 is set
mc . (len mc) is set
len <*F,F*> is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
qa is V4() V5() V6() V10() V11() V12() ext-real V33() set
mc . qa is set
qa - 1 is V11() V12() ext-real V33() set
mc . (qa - 1) is set
[(mc . qa),(mc . (qa - 1))] is set
{(mc . qa),(mc . (qa - 1))} is set
{(mc . qa)} is set
{{(mc . qa),(mc . (qa - 1))},{(mc . qa)}} is set
[(mc . (qa - 1)),(mc . qa)] is set
{(mc . (qa - 1)),(mc . qa)} is set
{(mc . (qa - 1))} is set
{{(mc . (qa - 1)),(mc . qa)},{(mc . (qa - 1))}} is set
<*F,F*> . 1 is set
<*F,F*> . 2 is set
[F,F] is set
{F,F} is set
{F} is set
{{F,F},{F}} is set

len R is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
R . 1 is set
R . (len R) is set
dom U2 is Element of bool the carrier of S
bool the carrier of S is non empty set
field U2 is set
F is set
R is set
mc is set
[F,R] is set
{F,R} is set
{F} is set
{{F,R},{F}} is set
[R,mc] is set
{R,mc} is set
{R} is set
{{R,mc},{R}} is set

len qa is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
qa . 1 is set
qa . (len qa) is set

len qh is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
qh . 1 is set
qh . (len qh) is set

len qa is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
qa . 1 is set
qa . (len qa) is set

len qh is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
qh . 1 is set
qh . (len qh) is set

len S1 is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
S1 . 1 is set
S1 . (len S1) is set
(len qa) + (len qh) is V11() V12() ext-real V33() set
1 + 1 is V11() V12() ext-real V33() set

S1O is V4() V5() V6() V10() V11() V12() ext-real V33() set
S1 . S1O is set
S1O - 1 is V11() V12() ext-real V33() set
S1 . (S1O - 1) is set
[(S1 . S1O),(S1 . (S1O - 1))] is set
{(S1 . S1O),(S1 . (S1O - 1))} is set
{(S1 . S1O)} is set
{{(S1 . S1O),(S1 . (S1O - 1))},{(S1 . S1O)}} is set
[(S1 . (S1O - 1)),(S1 . S1O)] is set
{(S1 . (S1O - 1)),(S1 . S1O)} is set
{(S1 . (S1O - 1))} is set
{{(S1 . (S1O - 1)),(S1 . S1O)},{(S1 . (S1O - 1))}} is set
2 - 1 is V11() V12() ext-real V33() set
(len qa) + 1 is V11() V12() ext-real V33() set
(len S1) - 0 is V11() V12() ext-real V33() set
(len qa) - 0 is V11() V12() ext-real V33() set
sqa is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
qa . (S1O - 1) is set
qa . S1O is set
S1O - (len qa) is V11() V12() ext-real V33() set
((len qa) + 1) - 1 is V11() V12() ext-real V33() set
sqa is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
S1 . sqa is set
sqa - (len qa) is V11() V12() ext-real V33() set
qh . (sqa - (len qa)) is set
s1 is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
s1 - 1 is V11() V12() ext-real V33() set
qh . (s1 - 1) is set
qh . s1 is set
((len qa) + 1) - (len qa) is V11() V12() ext-real V33() set
[F,mc] is set
{F,mc} is set
{{F,mc},{F}} is set

len S1 is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
S1 . 1 is set
S1 . (len S1) is set
F is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
R is set
mc is set
[R,mc] is set
{R,mc} is set
{R} is set
{{R,mc},{R}} is set
qa is set
qh is set

len S1 is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
S1 . 1 is set
S1 . (len S1) is set
[qa,qh] is set
{qa,qh} is set
{qa} is set
{{qa,qh},{qa}} is set
U1 is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
U2 is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
F is set
R is set
[F,R] is set
{F,R} is set
{F} is set
{{F,R},{F}} is set

len mc is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
mc . 1 is set
mc . (len mc) is set

len mc is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
mc . 1 is set
mc . (len mc) is set

the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
U1 is Element of the carrier of S
U2 is Element of the carrier of S
[U1,U2] is set
{U1,U2} is set
{U1} is set
{{U1,U2},{U1}} is set
<*U1,U2*> is non empty Relation-like NAT -defined the carrier of S -valued Function-like V47() V54(2) FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S
len <*U1,U2*> is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
<*U1,U2*> . 1 is set
the InternalRel of 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:]
R is V4() V5() V6() V10() V11() V12() ext-real V33() set
<*U1,U2*> . R is set
R - 1 is V11() V12() ext-real V33() set
<*U1,U2*> . (R - 1) is set
[(<*U1,U2*> . R),(<*U1,U2*> . (R - 1))] is set
{(<*U1,U2*> . R),(<*U1,U2*> . (R - 1))} is set
{(<*U1,U2*> . R)} is set
{{(<*U1,U2*> . R),(<*U1,U2*> . (R - 1))},{(<*U1,U2*> . R)}} is set
[(<*U1,U2*> . (R - 1)),(<*U1,U2*> . R)] is set
{(<*U1,U2*> . (R - 1)),(<*U1,U2*> . R)} is set
{(<*U1,U2*> . (R - 1))} is set
{{(<*U1,U2*> . (R - 1)),(<*U1,U2*> . R)},{(<*U1,U2*> . (R - 1))}} is set
<*U1,U2*> . (len <*U1,U2*>) is set

the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
field (S) is set
R is Element of the carrier of S
[R,R] is set
{R,R} is set
{R} is set
{{R,R},{R}} is set
field (S) is set
R is Element of the carrier of S
mc is Element of the carrier of S
[R,mc] is set
{R,mc} is set
{R} is set
{{R,mc},{R}} is set
[mc,R] is set
{mc,R} is set
{mc} is set
{{mc,R},{mc}} is set

the carrier of S is non empty set
U1 is Element of the carrier of S
U2 is Element of the carrier of S
F is Element of the carrier of S
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
field (S) is set
[U1,U2] is set
{U1,U2} is set
{U1} is set
{{U1,U2},{U1}} is set
[U2,F] is set
{U2,F} is set
{U2} is set
{{U2,F},{U2}} is set
[U1,F] is set
{U1,F} is set
{{U1,F},{U1}} is set

the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
bool the carrier of S is non empty set
bool (bool the carrier of S) is non empty set

the carrier of S is non empty set
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
U1 is Element of (S)
U2 is set
Class ((S),U2) is Element of bool the carrier of S

the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
U1 is Element of the carrier of S
Class ((S),U1) is Element of bool the carrier of S
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S

the carrier of S is non empty set
U1 is Element of the carrier of S
U2 is Element of the carrier of S
(S,U1) is non empty Element of (S)
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
Class ((S),U1) is Element of bool the carrier of S
(S,U2) is non empty Element of (S)
Class ((S),U2) is Element of bool the carrier of S
[U1,U2] is set
{U1,U2} is set
{U1} is set
{{U1,U2},{U1}} is set

the carrier of S is non empty set
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is non empty Element of (S)
{ (U1 . b1) where b1 is Element of the carrier of S : b1 in U2 } is set
union { (U1 . b1) where b1 is Element of the carrier of S : b1 in U2 } is set

the carrier of S is non empty set
U1 is non empty Relation-like the carrier of S -defined Function-like total set
U2 is Element of the carrier of S
U1 . U2 is set
(S,U2) is non empty Element of (S)
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
Class ((S),U2) is Element of bool the carrier of S
(S,U1,(S,U2)) is set
{ (U1 . b1) where b1 is Element of the carrier of S : b1 in (S,U2) } is set
union { (U1 . b1) where b1 is Element of the carrier of S : b1 in (S,U2) } is set
F is set

the carrier of S is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
U1 is Element of the carrier of S
U2 is Element of the carrier of S
[U1,U2] is set
{U1,U2} is set
{U1} is set
{{U1,U2},{U1}} is set
the InternalRel of 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:]

len F is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
F . 1 is set
F . (len F) is set
R is V4() V5() V6() V10() V11() V12() ext-real V33() set
F . R is set
mc is V4() V5() V6() V10() V11() V12() ext-real V33() set
F . mc is set
1 + 1 is V11() V12() ext-real V33() set
(1 + 1) - 1 is V11() V12() ext-real V33() set
mc - 1 is V11() V12() ext-real V33() set
qa is V4() V5() V6() V10() V11() V12() ext-real V33() Element of NAT
F . qa is set

qh is Element of the carrier of S
[qh,U1] is set
{qh,U1} is set
{qh} is set
{{qh,U1},{qh}} is set
qh is Element of the carrier of S
[U1,qh] is set
{U1,qh} is set
{{U1,qh},{U1}} is set
qh is Element of the carrier of S
[qh,U1] is set
{qh,U1} is set
{qh} is set
{{qh,U1},{qh}} is set
[U1,qh] is set
{U1,qh} is set
{{U1,qh},{U1}} is set

the carrier of S is non empty set
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
U1 is non empty Element of (S)
U2 is set
Class ((S),U2) is Element of bool the carrier of S
F is Element of the carrier of S
{F} is set
R is set
[R,U2] is set
{R,U2} is set
{R} is set
{{R,U2},{R}} is set
mc is Element of the carrier of S

the carrier of S is non empty set
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
U1 is non empty Element of (S)
U2 is Element of the carrier of S
{U2} is set
F is Element of the carrier of S
R is Element of the carrier of S

S is non empty reflexive transitive antisymmetric () RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
U1 is non empty Element of (S)

bool is non empty set

U1 is order-sorted MSAlgebra over S
the carrier of S is non empty set
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set
F is non empty directed Element of (S)
(S, the Sorts of U1,F) is set
{ ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in F } is set
union { ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in F } is set
[:(S, the Sorts of U1,F),(S, the Sorts of U1,F):] is Relation-like set
bool [:(S, the Sorts of U1,F),(S, the Sorts of U1,F):] is non empty set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like (S,U1)
R is set
mc is set
[R,mc] is set
{R,mc} is set
{R} is set
{{R,mc},{R}} is set
qa is Element of the carrier of S
U2 . qa is Relation-like the Sorts of U1 . qa -defined the Sorts of U1 . qa -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . qa),( the Sorts of U1 . qa):]
the Sorts of U1 . qa is set
[:( the Sorts of U1 . qa),( the Sorts of U1 . qa):] is Relation-like set
bool [:( the Sorts of U1 . qa),( the Sorts of U1 . qa):] is non empty set
qa is Element of the carrier of S
U2 . qa is Relation-like the Sorts of U1 . qa -defined the Sorts of U1 . qa -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . qa),( the Sorts of U1 . qa):]
the Sorts of U1 . qa is set
[:( the Sorts of U1 . qa),( the Sorts of U1 . qa):] is Relation-like set
bool [:( the Sorts of U1 . qa),( the Sorts of U1 . qa):] is non empty set
R is non empty set
{ [b1,b2] where b1, b2 is Element of R : S1[b1,b2] } is set
[:R,R:] is non empty Relation-like set
qa is set
qh is Element of R
S1 is Element of R
[qh,S1] is set
{qh,S1} is set
{qh} is set
{{qh,S1},{qh}} is set
S1O is Element of the carrier of S
U2 . S1O is Relation-like the Sorts of U1 . S1O -defined the Sorts of U1 . S1O -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):]
the Sorts of U1 . S1O is set
[:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):] is Relation-like set
bool [:( the Sorts of U1 . S1O),( the Sorts of U1 . S1O):] is non empty set
bool [:R,R:] is non empty set
qh is set
S1 is set
[qh,S1] is set
{qh,S1} is set
{qh} is set
{{qh,S1},{qh}} is set
qa is Relation-like R -defined R -valued Element of bool [:R,R:]
s1 is Element of R
s2 is Element of R
[s1,s2] is set
{s1,s2} is set
{s1} is set
{{s1,s2},{s1}} is set
a1 is Element of the carrier of S
U2 . a1 is Relation-like the Sorts of U1 . a1 -defined the Sorts of U1 . a1 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . a1),( the Sorts of U1 . a1):]
the Sorts of U1 . a1 is set
[:( the Sorts of U1 . a1),( the Sorts of U1 . a1):] is Relation-like set
bool [:( the Sorts of U1 . a1),( the Sorts of U1 . a1):] is non empty set
a1 is Element of the carrier of S
U2 . a1 is Relation-like the Sorts of U1 . a1 -defined the Sorts of U1 . a1 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . a1),( the Sorts of U1 . a1):]
the Sorts of U1 . a1 is set
[:( the Sorts of U1 . a1),( the Sorts of U1 . a1):] is Relation-like set
bool [:( the Sorts of U1 . a1),( the Sorts of U1 . a1):] is non empty set
field (U2 . a1) is set
[S1,qh] is set
{S1,qh} is set
{S1} is set
{{S1,qh},{S1}} is set
sqa is Element of R
S1O is Element of R
[sqa,S1O] is set
{sqa,S1O} is set
{sqa} is set
{{sqa,S1O},{sqa}} is set
qh is set
S1O is set
sqa is Element of the carrier of S
the Sorts of U1 . sqa is set
U2 . sqa is Relation-like the Sorts of U1 . sqa -defined the Sorts of U1 . sqa -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):]
[:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):] is Relation-like set
bool [:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):] is non empty set
field (U2 . sqa) is set
[qh,qh] is set
{qh,qh} is set
{qh} is set
{{qh,qh},{qh}} is set
S1 is Element of R
[S1,S1] is set
{S1,S1} is set
{S1} is set
{{S1,S1},{S1}} is set
dom qa is Element of bool R
bool R is non empty set
field qa is set
qh is set
S1 is set
S1O is set
[qh,S1] is set
{qh,S1} is set
{qh} is set
{{qh,S1},{qh}} is set
[S1,S1O] is set
{S1,S1O} is set
{S1} is set
{{S1,S1O},{S1}} is set
sqa is Element of R
s1 is Element of R
[sqa,s1] is set
{sqa,s1} is set
{sqa} is set
{{sqa,s1},{sqa}} is set
s2 is Element of R
a1 is Element of R
[s2,a1] is set
{s2,a1} is set
{s2} is set
{{s2,a1},{s2}} is set
x is Element of the carrier of S
U2 . x is Relation-like the Sorts of U1 . x -defined the Sorts of U1 . x -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . x),( the Sorts of U1 . x):]
the Sorts of U1 . x is set
[:( the Sorts of U1 . x),( the Sorts of U1 . x):] is Relation-like set
bool [:( the Sorts of U1 . x),( the Sorts of U1 . x):] is non empty set
x is Element of the carrier of S
U2 . x is Relation-like the Sorts of U1 . x -defined the Sorts of U1 . x -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . x),( the Sorts of U1 . x):]
the Sorts of U1 . x is set
[:( the Sorts of U1 . x),( the Sorts of U1 . x):] is Relation-like set
bool [:( the Sorts of U1 . x),( the Sorts of U1 . x):] is non empty set
x2 is Element of the carrier of S
U2 . x2 is Relation-like the Sorts of U1 . x2 -defined the Sorts of U1 . x2 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . x2),( the Sorts of U1 . x2):]
the Sorts of U1 . x2 is set
[:( the Sorts of U1 . x2),( the Sorts of U1 . x2):] is Relation-like set
bool [:( the Sorts of U1 . x2),( the Sorts of U1 . x2):] is non empty set
x2 is Element of the carrier of S
U2 . x2 is Relation-like the Sorts of U1 . x2 -defined the Sorts of U1 . x2 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . x2),( the Sorts of U1 . x2):]
the Sorts of U1 . x2 is set
[:( the Sorts of U1 . x2),( the Sorts of U1 . x2):] is Relation-like set
bool [:( the Sorts of U1 . x2),( the Sorts of U1 . x2):] is non empty set
s3 is Element of the carrier of S
s4 is Element of the carrier of S
x1 is Element of the carrier of S
U2 . x1 is Relation-like the Sorts of U1 . x1 -defined the Sorts of U1 . x1 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . x1),( the Sorts of U1 . x1):]
the Sorts of U1 . x1 is set
[:( the Sorts of U1 . x1),( the Sorts of U1 . x1):] is Relation-like set
bool [:( the Sorts of U1 . x1),( the Sorts of U1 . x1):] is non empty set
field (U2 . x1) is set
[sqa,a1] is set
{sqa,a1} is set
{{sqa,a1},{sqa}} is set
[qh,S1O] is set
{qh,S1O} is set
{{qh,S1O},{qh}} is set
qh is Relation-like (S, the Sorts of U1,F) -defined (S, the Sorts of U1,F) -valued total reflexive symmetric transitive Element of bool [:(S, the Sorts of U1,F),(S, the Sorts of U1,F):]
S1 is set
S1O is set
[S1,S1O] is set
{S1,S1O} is set
{S1} is set
{{S1,S1O},{S1}} is set
sqa is Element of R
s1 is Element of R
[sqa,s1] is set
{sqa,s1} is set
{sqa} is set
{{sqa,s1},{sqa}} is set
s2 is Element of the carrier of S
U2 . s2 is Relation-like the Sorts of U1 . s2 -defined the Sorts of U1 . s2 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . s2),( the Sorts of U1 . s2):]
the Sorts of U1 . s2 is set
[:( the Sorts of U1 . s2),( the Sorts of U1 . s2):] is Relation-like set
bool [:( the Sorts of U1 . s2),( the Sorts of U1 . s2):] is non empty set
sqa is Element of the carrier of S
U2 . sqa is Relation-like the Sorts of U1 . sqa -defined the Sorts of U1 . sqa -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):]
the Sorts of U1 . sqa is set
[:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):] is Relation-like set
bool [:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):] is non empty set
sqa is Element of the carrier of S
U2 . sqa is Relation-like the Sorts of U1 . sqa -defined the Sorts of U1 . sqa -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):]
the Sorts of U1 . sqa is set
[:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):] is Relation-like set
bool [:( the Sorts of U1 . sqa),( the Sorts of U1 . sqa):] is non empty set
s1 is Element of R
s2 is Element of R
[s1,s2] is set
{s1,s2} is set
{s1} is set
{{s1,s2},{s1}} is set
a1 is Element of the carrier of S
U2 . a1 is Relation-like the Sorts of U1 . a1 -defined the Sorts of U1 . a1 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . a1),( the Sorts of U1 . a1):]
the Sorts of U1 . a1 is set
[:( the Sorts of U1 . a1),( the Sorts of U1 . a1):] is Relation-like set
bool [:( the Sorts of U1 . a1),( the Sorts of U1 . a1):] is non empty set
S1 is set
S1O is set
[S1,S1O] is set
{S1,S1O} is set
{S1} is set
{{S1,S1O},{S1}} is set
s2 is Element of the carrier of S
sqa is set
s1 is set
[sqa,s1] is set
{sqa,s1} is set
{sqa} is set
{{sqa,s1},{sqa}} is set
U2 . s2 is Relation-like the Sorts of U1 . s2 -defined the Sorts of U1 . s2 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . s2),( the Sorts of U1 . s2):]
the Sorts of U1 . s2 is set
[:( the Sorts of U1 . s2),( the Sorts of U1 . s2):] is Relation-like set
bool [:( the Sorts of U1 . s2),( the Sorts of U1 . s2):] is non empty set
R is Relation-like (S, the Sorts of U1,F) -defined (S, the Sorts of U1,F) -valued total reflexive symmetric transitive Element of bool [:(S, the Sorts of U1,F),(S, the Sorts of U1,F):]
mc is Relation-like (S, the Sorts of U1,F) -defined (S, the Sorts of U1,F) -valued total reflexive symmetric transitive Element of bool [:(S, the Sorts of U1,F),(S, the Sorts of U1,F):]
qa is set
qh is set
[qa,qh] is set
{qa,qh} is set
{qa} is set
{{qa,qh},{qa}} is set
S1 is Element of the carrier of S
U2 . S1 is Relation-like the Sorts of U1 . S1 -defined the Sorts of U1 . S1 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . S1),( the Sorts of U1 . S1):]
the Sorts of U1 . S1 is set
[:( the Sorts of U1 . S1),( the Sorts of U1 . S1):] is Relation-like set
bool [:( the Sorts of U1 . S1),( the Sorts of U1 . S1):] is non empty set
S1 is Element of the carrier of S
U2 . S1 is Relation-like the Sorts of U1 . S1 -defined the Sorts of U1 . S1 -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . S1),( the Sorts of U1 . S1):]
the Sorts of U1 . S1 is set
[:( the Sorts of U1 . S1),( the Sorts of U1 . S1):] is Relation-like set
bool [:( the Sorts of U1 . S1),( the Sorts of U1 . S1):] is non empty set

U1 is order-sorted MSAlgebra over S
the carrier of S is non empty set
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set
F is Element of the carrier of S
(S,F) is non empty directed Element of (S)
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
Class ((S),F) is Element of bool the carrier of S
(S, the Sorts of U1,(S,F)) is set
{ ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in (S,F) } is set
union { ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in (S,F) } is set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like (S,U1)
(S,U1,U2,(S,F)) is Relation-like (S, the Sorts of U1,(S,F)) -defined (S, the Sorts of U1,(S,F)) -valued total reflexive symmetric transitive Element of bool [:(S, the Sorts of U1,(S,F)),(S, the Sorts of U1,(S,F)):]
[:(S, the Sorts of U1,(S,F)),(S, the Sorts of U1,(S,F)):] is Relation-like set
bool [:(S, the Sorts of U1,(S,F)),(S, the Sorts of U1,(S,F)):] is non empty set
Class (S,U1,U2,(S,F)) is with_non-empty_elements a_partition of (S, the Sorts of U1,(S,F))
bool (Class (S,U1,U2,(S,F))) is non empty set
the Sorts of U1 . F is set
qa is Element of bool (Class (S,U1,U2,(S,F)))
qh is set
S1 is set
Class ((S,U1,U2,(S,F)),S1) is Element of bool (S, the Sorts of U1,(S,F))
bool (S, the Sorts of U1,(S,F)) is non empty set
S1 is set
Class ((S,U1,U2,(S,F)),S1) is Element of bool (S, the Sorts of U1,(S,F))
bool (S, the Sorts of U1,(S,F)) is non empty set
bool (S, the Sorts of U1,(S,F)) is non empty set
bool (bool (S, the Sorts of U1,(S,F))) is non empty set
qa is non empty Element of bool (bool (S, the Sorts of U1,(S,F)))
{ b1 where b1 is Element of qa : S1[b1] } is set
S1 is set
S1O is Element of qa
sqa is set
Class ((S,U1,U2,(S,F)),sqa) is Element of bool (S, the Sorts of U1,(S,F))
S1 is Element of bool (Class (S,U1,U2,(S,F)))
S1O is set
sqa is Element of qa
s1 is set
Class ((S,U1,U2,(S,F)),s1) is Element of bool (S, the Sorts of U1,(S,F))
sqa is set
Class ((S,U1,U2,(S,F)),sqa) is Element of bool (S, the Sorts of U1,(S,F))
sqa is set
Class ((S,U1,U2,(S,F)),sqa) is Element of bool (S, the Sorts of U1,(S,F))
s1 is set
Class ((S,U1,U2,(S,F)),s1) is Element of bool (S, the Sorts of U1,(S,F))
S1O is set
s1 is set
sqa is set
Class ((S,U1,U2,(S,F)),s1) is Element of bool (S, the Sorts of U1,(S,F))
R is Element of bool (Class (S,U1,U2,(S,F)))
mc is Element of bool (Class (S,U1,U2,(S,F)))
qa is set
qh is set
Class ((S,U1,U2,(S,F)),qh) is Element of bool (S, the Sorts of U1,(S,F))
bool (S, the Sorts of U1,(S,F)) is non empty set
qh is set
Class ((S,U1,U2,(S,F)),qh) is Element of bool (S, the Sorts of U1,(S,F))
bool (S, the Sorts of U1,(S,F)) is non empty set

U1 is non-empty order-sorted MSAlgebra over S
the carrier of S is non empty set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like (S,U1)
F is Element of the carrier of S
(S,U1,U2,F) is Element of bool (Class (S,U1,U2,(S,F)))
the Sorts of U1 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like total set
(S,F) is non empty directed Element of (S)
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
Class ((S),F) is Element of bool the carrier of S
(S, the Sorts of U1,(S,F)) is set
{ ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in (S,F) } is set
union { ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in (S,F) } is set
(S,U1,U2,(S,F)) is Relation-like (S, the Sorts of U1,(S,F)) -defined (S, the Sorts of U1,(S,F)) -valued total reflexive symmetric transitive Element of bool [:(S, the Sorts of U1,(S,F)),(S, the Sorts of U1,(S,F)):]
[:(S, the Sorts of U1,(S,F)),(S, the Sorts of U1,(S,F)):] is Relation-like set
bool [:(S, the Sorts of U1,(S,F)),(S, the Sorts of U1,(S,F)):] is non empty set
Class (S,U1,U2,(S,F)) is with_non-empty_elements a_partition of (S, the Sorts of U1,(S,F))
bool (Class (S,U1,U2,(S,F))) is non empty set
the Sorts of U1 . F is non empty set
R is set
Class ((S,U1,U2,(S,F)),R) is Element of bool (S, the Sorts of U1,(S,F))
bool (S, the Sorts of U1,(S,F)) is non empty set

the carrier of S is non empty set
U1 is order-sorted MSAlgebra over S
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like (S,U1)
F is Element of the carrier of S
R is Element of the carrier of S
(S,U1,U2,F) is Element of bool (Class (S,U1,U2,(S,F)))
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set
(S,F) is non empty directed Element of (S)
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of S, the carrier of S:] is non empty Relation-like set
bool [: the carrier of S, the carrier of S:] is non empty set
Class (S) is non empty with_non-empty_elements a_partition of the carrier of S
Class ((S),F) is Element of bool the carrier of S
(S, the Sorts of U1,(S,F)) is set
{ ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in (S,F) } is set
union { ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in (S,F) } is set
(S,U1,U2,(S,F)) is Relation-like (S, the Sorts of U1,(S,F)) -defined (S, the Sorts of U1,(S,F)) -valued total reflexive symmetric transitive Element of bool [:(S, the Sorts of U1,(S,F)),(S, the Sorts of U1,(S,F)):]
[:(S, the Sorts of U1,(S,F)),(S, the Sorts of U1,(S,F)):] is Relation-like set
bool [:(S, the Sorts of U1,(S,F)),(S, the Sorts of U1,(S,F)):] is non empty set
Class (S,U1,U2,(S,F)) is with_non-empty_elements a_partition of (S, the Sorts of U1,(S,F))
bool (Class (S,U1,U2,(S,F))) is non empty set
(S,U1,U2,R) is Element of bool (Class (S,U1,U2,(S,R)))
(S,R) is non empty directed Element of (S)
Class ((S),R) is Element of bool the carrier of S
(S, the Sorts of U1,(S,R)) is set
{ ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in (S,R) } is set
union { ( the Sorts of U1 . b1) where b1 is Element of the carrier of S : b1 in (S,R) } is set
(S,U1,U2,(S,R)) is Relation-like (S, the Sorts of U1,(S,R)) -defined (S, the Sorts of U1,(S,R)) -valued total reflexive symmetric transitive Element of bool [:(S, the Sorts of U1,(S,R)),(S, the Sorts of U1,(S,R)):]
[:(S, the Sorts of U1,(S,R)),(S, the Sorts of U1,(S,R)):] is Relation-like set
bool [:(S, the Sorts of U1,(S,R)),(S, the Sorts of U1,(S,R)):] is non empty set
Class (S,U1,U2,(S,R)) is with_non-empty_elements a_partition of (S, the Sorts of U1,(S,R))
bool (Class (S,U1,U2,(S,R))) is non empty set
S1 is set
the Sorts of U1 . F is set

mc is Element of the carrier of S
qh . mc is set
qa is Element of the carrier of S
qh . qa is set
S1O is set
Class ((S,U1,U2,(S,F)),S1O) is Element of bool (S, the Sorts of U1,(S,F))
bool (S, the Sorts of U1,(S,F)) is non empty set

U1 is order-sorted MSAlgebra over S
the carrier of S is non empty set
U2 is non empty Relation-like the carrier of S -defined Function-like total Relation-yielding MSEquivalence-like (S,U1)
the Sorts of U1 is non empty Relation-like the carrier of S -defined Function-like total set

dom F is set
R is non empty Relation-like the carrier of S -defined Function-like total set
qa is Element of the carrier of S
qh is Element of the carrier of S
R . qa is set
R . qh is set
(S,U1,U2,qa) is Element of bool (Class (S,U1,U2,(S,qa)))
(S,qa) is non empty directed Element of (S)
bool the carrier of S is non empty set
(S) is non empty Element of bool (bool the carrier of S)
bool (bool the carrier of S) is non empty set
(S) is Relation-like the carrier of S -defined the carrier of S -valued total reflexive symmetric transitive Element of bool [: the carrier of S, the carrier of S:]
[: the carrier of