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

COMPLEX is 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

the empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V33() reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive V47() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding Relation-yielding Cardinal-yielding countable set is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V33() reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive V47() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding Relation-yielding Cardinal-yielding countable 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

S is non empty reflexive transitive antisymmetric RelStr

the carrier of S is non empty set

the Relation-like set is Relation-like set

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

{ the Relation-like set } is set

[: the carrier of S,{ the Relation-like set }:] is Relation-like set

bool [: the carrier of S,{ the Relation-like set }:] 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

mc is non empty Relation-like the carrier of S -defined Function-like total order-sorted 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

S is non empty reflexive transitive antisymmetric RelStr

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

S is non empty reflexive transitive antisymmetric RelStr

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

R is Relation-like 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

S is non empty reflexive transitive antisymmetric RelStr

the carrier of S is non empty set

S is non empty reflexive transitive antisymmetric RelStr

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

S is non empty reflexive transitive antisymmetric RelStr

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

S is non empty reflexive transitive antisymmetric RelStr

the carrier of S is non empty set

S is non empty non void V73() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign

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

U2 is non empty Relation-like the carrier of S -defined Function-like total order-sorted 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

S is non empty non void V73() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign

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

U2 is Relation-like Function-like 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 is non empty Relation-like the carrier of S -defined Function-like total order-sorted 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):]

S is non empty non void V73() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign

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

U2 is Relation-like Function-like 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 is non empty Relation-like the carrier of S -defined Function-like total order-sorted set

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

the_arity_of S1O is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable Element of the carrier of S *

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 . (the_result_sort_of S1O) is Relation-like the Sorts of U1 . (the_result_sort_of S1O) -defined the Sorts of U1 . (the_result_sort_of S1O) -valued total reflexive symmetric transitive Element of bool [:( the Sorts of U1 . (the_result_sort_of S1O)),( the Sorts of U1 . (the_result_sort_of S1O)):]

the Sorts of U1 . (the_result_sort_of S1O) is non empty set

[:( the Sorts of U1 . (the_result_sort_of S1O)),( the Sorts of U1 . (the_result_sort_of S1O)):] is non empty Relation-like set

bool [:( the Sorts of U1 . (the_result_sort_of S1O)),( the Sorts of U1 . (the_result_sort_of S1O)):] 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 . (the_result_sort_of S1O)) is non empty Relation-like the Sorts of U1 . (the_result_sort_of S1O) -defined the Sorts of U1 . (the_result_sort_of S1O) -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of U1 . (the_result_sort_of S1O)),( the Sorts of U1 . (the_result_sort_of S1O)):]

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

S is non empty non void V73() reflexive transitive antisymmetric order-sorted discernable OverloadedRSSign

S is non empty reflexive transitive antisymmetric RelStr

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

{ [b

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

mc is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of 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

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

qh is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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

qh . 1 is set

qh . (len qh) is set

mc is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of 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

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

mc is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of 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

Rev mc is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

qa is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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

dom mc is countable Element of bool NAT

(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

qa is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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

<*F,F*> is non empty Relation-like NAT -defined Function-like V47() V54(2) FinSequence-like FinSubsequence-like countable set

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

{F,F} is set

{F} is set

mc is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of 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 <*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

R is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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

qa is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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 Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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

qh . 1 is set

qh . (len qh) is set

qa is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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 Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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

qh . 1 is set

qh . (len qh) is set

qa ^ qh is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

S1 is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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

dom qa is countable Element of bool NAT

dom qh is countable Element of bool NAT

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

S1 is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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

S1 is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of S

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

mc is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of 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

mc is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of 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

S is non empty reflexive transitive antisymmetric RelStr

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

S is non empty reflexive transitive antisymmetric RelStr

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

S is non empty reflexive transitive antisymmetric RelStr

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

S is non empty reflexive transitive antisymmetric RelStr

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

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 Element of (S)

U2 is set

Class ((S),U2) is Element of bool the carrier of S

S is non empty reflexive transitive antisymmetric RelStr

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

S is non empty reflexive transitive antisymmetric RelStr

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

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 Relation-like the carrier of S -defined Function-like total set

U2 is non empty Element of (S)

{ (U1 . b

union { (U1 . b

S is non empty reflexive transitive antisymmetric RelStr

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 . b

union { (U1 . b

F is set

S is non empty reflexive transitive antisymmetric discrete RelStr

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

F is Relation-like NAT -defined the carrier of S -valued Function-like V47() FinSequence-like FinSubsequence-like countable FinSequence of 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

dom F is countable Element of bool NAT

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

S is non empty reflexive transitive antisymmetric discrete 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)

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

S is non empty reflexive transitive antisymmetric discrete 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)

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

the non empty reflexive transitive antisymmetric discrete RelStr is non empty reflexive transitive antisymmetric discrete RelStr

the non empty non void V73() reflexive transitive antisymmetric discrete order-sorted discernable OverloadedRSSign is non empty non void V73() reflexive transitive antisymmetric discrete order-sorted discernable OverloadedRSSign

S is non empty reflexive transitive antisymmetric RelStr

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)

[:{},{}:] is Relation-like set

bool [:{},{}:] is non empty set

S is non empty non void V73() reflexive transitive antisymmetric order-sorted discernable () OverloadedRSSign

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 . b

union { ( the Sorts of U1 . b

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

{ [b

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

S is non empty non void V73() reflexive transitive antisymmetric order-sorted discernable () OverloadedRSSign

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 . b

union { ( the Sorts of U1 . b

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)))

{ b

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

S is non empty non void V73() reflexive transitive antisymmetric order-sorted discernable () OverloadedRSSign

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 . b

union { ( the Sorts of U1 . b

(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

S is non empty non void V73() reflexive transitive antisymmetric order-sorted discernable () OverloadedRSSign

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 . b

union { ( the Sorts of U1 . b

(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 . b

union { ( the Sorts of U1 . b

(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

qh is non empty Relation-like the carrier of S -defined Function-like total order-sorted 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

S is non empty non void V73() reflexive transitive antisymmetric order-sorted discernable () OverloadedRSSign

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

F is Relation-like Function-like 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