:: CLOSURE3 semantic presentation

K164() is Element of bool K160()
K160() is set
bool K160() is non empty set
K137() is set
bool K137() is non empty set
bool K164() is non empty set
K161() is set
K162() is set
K163() is set
2 is non empty set
{} is empty Function-like functional finite V45() V87() set
the empty Function-like functional finite V45() V87() set is empty Function-like functional finite V45() V87() set
1 is non empty set
3 is non empty set
K165() is empty Function-like functional finite V45() V87() Element of K164()
S is non empty 1-sorted
the carrier of S is non empty set
1-sorted(# the carrier of S #) is strict 1-sorted
S is non empty set
MA is non empty Relation-like S -defined Function-like V17(S) set
I is non empty Relation-like S -defined Function-like V17(S) set
MA +* I is Relation-like Function-like set
dom MA is set
dom I is set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is Relation-like S -defined Function-like V17(S) set
SS is functional Element of bool (Bool MA)
|:SS:| is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool MA
bool MA is Relation-like S -defined Function-like V17(S) set
meet |:SS:| is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
S is non empty non void V62() ManySortedSign
the carrier of S is non empty set
MA is strict non-empty MSAlgebra over S
the Sorts of MA is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
Bool the Sorts of MA is non empty functional with_common_domain set
bool (Bool the Sorts of MA) is non empty set
SubSort MA is set
I is functional Element of bool (Bool the Sorts of MA)
|:I:| is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of MA
bool the Sorts of MA is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet |:I:| is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA
SS is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of MA
[[0]] the carrier of S is non empty Relation-like non non-empty empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the carrier of S --> {} is non empty Relation-like the carrier of S -defined {{}} -valued Function-like V17( the carrier of S) quasi_total Element of bool [: the carrier of S,{{}}:]
{{}} is non empty finite V45() set
[: the carrier of S,{{}}:] is non empty set
bool [: the carrier of S,{{}}:] is non empty set
the carrier' of S is non empty set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA
y is Element of the carrier' of S
the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is non empty set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S . y is Element of the carrier of S
the_result_sort_of y is Element of the carrier of S
dom the ResultSort of S is set
Result (y,MA) is non empty Element of rng the Sorts of MA
rng the Sorts of MA is with_non-empty_elements set
the ResultSort of S * A is Relation-like Function-like set
( the ResultSort of S * A) . y is set
A . (the_result_sort_of y) is set
Args (y,MA) is non empty Element of rng ( the Sorts of MA #)
the Sorts of MA # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the carrier of S * is non empty functional V87() M12( the carrier of S)
rng ( the Sorts of MA #) is set
Den (y,MA) is non empty Relation-like Args (y,MA) -defined Result (y,MA) -valued Function-like V17( Args (y,MA)) quasi_total Element of bool [:(Args (y,MA)),(Result (y,MA)):]
[:(Args (y,MA)),(Result (y,MA)):] is non empty set
bool [:(Args (y,MA)),(Result (y,MA)):] is non empty set
A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the_arity_of y is Relation-like K164() -defined the carrier of S -valued Function-like finite V85() V86() Element of the carrier of S *
(A #) . (the_arity_of y) is set
(Den (y,MA)) | ((A #) . (the_arity_of y)) is Relation-like Args (y,MA) -defined Result (y,MA) -valued Function-like Element of bool [:(Args (y,MA)),(Result (y,MA)):]
rng ((Den (y,MA)) | ((A #) . (the_arity_of y))) is set
the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]
[: the carrier' of S,( the carrier of S *):] is non empty set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
the Arity of S . y is Relation-like K164() -defined Function-like finite V85() V86() Element of the carrier of S *
dom the Arity of S is set
the Arity of S * (A #) is Relation-like Function-like set
( the Arity of S * (A #)) . y is set
the carrier' of S is non empty set
x is Element of the carrier' of S
the_result_sort_of x is Element of the carrier of S
the ResultSort of S is non empty Relation-like the carrier' of S -defined the carrier of S -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is non empty set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S . x is Element of the carrier of S
dom the ResultSort of S is set
the carrier of S * is non empty functional V87() M12( the carrier of S)
the Arity of S is non empty Relation-like the carrier' of S -defined the carrier of S * -valued Function-like V17( the carrier' of S) quasi_total Element of bool [: the carrier' of S,( the carrier of S *):]
[: the carrier' of S,( the carrier of S *):] is non empty set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
the Arity of S . x is Relation-like K164() -defined Function-like finite V85() V86() Element of the carrier of S *
the_arity_of x is Relation-like K164() -defined the carrier of S -valued Function-like finite V85() V86() Element of the carrier of S *
dom the Arity of S is set
SS # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (SS #) is Relation-like Function-like set
( the Arity of S * (SS #)) . x is set
(SS #) . (the_arity_of x) is set
Result (x,MA) is non empty Element of rng the Sorts of MA
rng the Sorts of MA is with_non-empty_elements set
the ResultSort of S * the Sorts of MA is Relation-like Function-like set
( the ResultSort of S * the Sorts of MA) . x is set
the Sorts of MA . (the_result_sort_of x) is non empty set
Args (x,MA) is non empty Element of rng ( the Sorts of MA #)
the Sorts of MA # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of MA #) is set
Den (x,MA) is non empty Relation-like Args (x,MA) -defined Result (x,MA) -valued Function-like V17( Args (x,MA)) quasi_total Element of bool [:(Args (x,MA)),(Result (x,MA)):]
[:(Args (x,MA)),(Result (x,MA)):] is non empty set
bool [:(Args (x,MA)),(Result (x,MA)):] is non empty set
(Den (x,MA)) | ((SS #) . (the_arity_of x)) is Relation-like Args (x,MA) -defined Result (x,MA) -valued Function-like Element of bool [:(Args (x,MA)),(Result (x,MA)):]
rng ((Den (x,MA)) | ((SS #) . (the_arity_of x))) is set
SS . (the_result_sort_of x) is set
bool ( the Sorts of MA . (the_result_sort_of x)) is non empty set
bool (bool ( the Sorts of MA . (the_result_sort_of x))) is non empty set
|:I:| . (the_result_sort_of x) is Element of bool (bool ( the Sorts of MA . (the_result_sort_of x)))
A is Element of bool (bool ( the Sorts of MA . (the_result_sort_of x)))
Intersect A is Element of bool ( the Sorts of MA . (the_result_sort_of x))
y is set
dom ((Den (x,MA)) | ((SS #) . (the_arity_of x))) is set
z is set
((Den (x,MA)) | ((SS #) . (the_arity_of x))) . z is set
Bool the Sorts of MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool the Sorts of MA)
{ (b₁ . (the_result_sort_of x)) where b₁ is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) Element of Bool the Sorts of MA : b₁ in I } is set
i is set
SS9 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) Element of Bool the Sorts of MA
SS9 . (the_result_sort_of x) is set
SS9 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA
SS9 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (SS9 #) is Relation-like Function-like set
( the Arity of S * (SS9 #)) . x is set
(Den (x,MA)) | (( the Arity of S * (SS9 #)) . x) is Relation-like Args (x,MA) -defined Result (x,MA) -valued Function-like Element of bool [:(Args (x,MA)),(Result (x,MA)):]
rng ((Den (x,MA)) | (( the Arity of S * (SS9 #)) . x)) is set
the ResultSort of S * SS9 is Relation-like Function-like set
( the ResultSort of S * SS9) . x is set
(Den (x,MA)) | (( the Arity of S * (SS #)) . x) is Relation-like Args (x,MA) -defined Result (x,MA) -valued Function-like Element of bool [:(Args (x,MA)),(Result (x,MA)):]
dom ((Den (x,MA)) | (( the Arity of S * (SS #)) . x)) is set
dom ((Den (x,MA)) | (( the Arity of S * (SS9 #)) . x)) is set
(Den (x,MA)) . z is set
((Den (x,MA)) | (( the Arity of S * (SS9 #)) . x)) . z is set
SS9 . ( the ResultSort of S . x) is set
SS9 . (the_result_sort_of x) is set
the ResultSort of S * SS is Relation-like Function-like set
( the ResultSort of S * SS) . x is set
MA is set
S is set
I is set
SS is set
M is set
x is set
S is non empty set
MA is non empty Relation-like S -defined Function-like V17(S) set
{ b₁ where b₁ is Element of S : not MA . b₁ = {} } is set
support MA is set
SS is set
dom MA is set
MA . SS is set
SS is set
M is Element of S
MA . M is set
S is non empty set
MA is non empty Relation-like S -defined Function-like V17(S) set
support MA is set
{ b₁ where b₁ is Element of S : not MA . b₁ = {} } is set
I is set
SS is set
S is non empty set
[[0]] S is non empty Relation-like non non-empty empty-yielding S -defined Function-like V17(S) set
S --> {} is non empty Relation-like S -defined {{}} -valued Function-like V17(S) quasi_total Element of bool [:S,{{}}:]
{{}} is non empty finite V45() set
[:S,{{}}:] is non empty set
bool [:S,{{}}:] is non empty set
MA is non empty Relation-like non-empty non empty-yielding S -defined Function-like V17(S) set
(S,MA) is set
{ b₁ where b₁ is Element of S : not MA . b₁ = {} } is set
MA | (S,MA) is Relation-like Function-like set
([[0]] S) +* (MA | (S,MA)) is Relation-like Function-like set
SS is set
MA . SS is set
dom MA is set
S is non empty set
MA is non empty Relation-like non-empty non empty-yielding S -defined Function-like V17(S) set
(S,MA) is set
{ b₁ where b₁ is Element of S : not MA . b₁ = {} } is set
MA | (S,MA) is Relation-like Function-like set
I is non empty Relation-like non-empty non empty-yielding S -defined Function-like V17(S) set
(S,I) is set
{ b₁ where b₁ is Element of S : not I . b₁ = {} } is set
I | (S,I) is Relation-like Function-like set
dom MA is set
dom I is set
SS is set
MA . SS is set
I . SS is set
dom (I | (S,I)) is set
(dom I) /\ (S,I) is set
dom (MA | (S,MA)) is set
(dom MA) /\ (S,MA) is set
(I | (S,I)) . SS is set
S is non empty set
MA is non empty Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
SS is Element of S
I . SS is set
M is set
{SS} is non empty finite set
{M} is non empty finite set
{SS} --> {M} is non empty Relation-like {SS} -defined {{M}} -valued Function-like V17({SS}) quasi_total finite Element of bool [:{SS},{{M}}:]
{{M}} is non empty finite V45() set
[:{SS},{{M}}:] is non empty finite set
bool [:{SS},{{M}}:] is non empty finite V45() set
[[0]] S is non empty Relation-like non non-empty empty-yielding S -defined Function-like V17(S) set
S --> {} is non empty Relation-like S -defined {{}} -valued Function-like V17(S) quasi_total Element of bool [:S,{{}}:]
{{}} is non empty finite V45() set
[:S,{{}}:] is non empty set
bool [:S,{{}}:] is non empty set
([[0]] S) +* ({SS} --> {M}) is Relation-like Function-like set
dom ({SS} --> {M}) is finite set
({SS} --> {M}) . SS is set
(([[0]] S) +* ({SS} --> {M})) . SS is set
dom (([[0]] S) +* ({SS} --> {M})) is set
dom ([[0]] S) is set
(dom ([[0]] S)) \/ (dom ({SS} --> {M})) is set
S \/ {SS} is non empty set
A is non empty Relation-like S -defined Function-like V17(S) set
y is set
A . y is set
MA . y is set
i is set
z is non empty Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
z . y is set
(S --> {}) . y is set
y is non empty Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
z is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
i is set
z . i is set
I . i is set
SS9 is set
(S --> {}) . i is set
{ b₁ where b₁ is Element of S : not z . b₁ = {} } is set
i is set
SS9 is Element of S
z . SS9 is set
SS9 is Element of S
dom z is set
z . SS9 is set
(S --> {}) . SS9 is finite Element of {{}}
SS9 is Element of S
z . SS9 is set
i is set
SS9 is Element of S
z . SS9 is set
z . SS is set
(S,z) is set
i is set
z . i is set
(S --> {}) . i is set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
I is functional Element of bool (Bool MA)
{ (b₁ . a₁) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . a₁) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
SS is set
{ (b₁ . SS) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . SS) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
SS is Relation-like Function-like set
dom SS is set
M is Relation-like S -defined Function-like V17(S) set
x is set
M . x is set
MA . x is set
A is set
{ (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
A is set
y is Relation-like S -defined Function-like V17(S) Element of Bool MA
y . x is set
z is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
z . x is set
x is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
A is set
x . A is set
{ (b₁ . A) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . A) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
SS is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
M is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
x is set
SS . x is set
M . x is set
{ (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is empty proper Function-like functional finite V45() V87() Element of bool (Bool MA)
(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
SS is set
(S,MA,I) . SS is set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
{ (b₁ . SS) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . SS) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
x is set
A is set
A is Relation-like S -defined Function-like V17(S) Element of Bool MA
A . SS is set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is functional Element of bool (Bool MA)
(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
|:I:| is Relation-like S -defined Function-like V17(S) ManySortedSubset of bool MA
bool MA is Relation-like S -defined Function-like V17(S) set
union |:I:| is Relation-like S -defined Function-like V17(S) set
M is Relation-like S -defined Function-like V17(S) set
x is set
(S,MA,I) . x is set
M . x is set
|:I:| . x is set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
{ (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union (|:I:| . x) is set
M is Relation-like S -defined Function-like V17(S) set
x is set
(S,MA,I) . x is set
M . x is set
[[0]] S is Relation-like empty-yielding S -defined Function-like V17(S) set
S --> {} is Relation-like S -defined {{}} -valued Function-like V17(S) quasi_total Element of bool [:S,{{}}:]
{{}} is non empty finite V45() set
[:S,{{}}:] is set
bool [:S,{{}}:] is non empty set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is functional Element of bool (Bool MA)
SS is functional Element of bool (Bool MA)
I \/ SS is set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is functional Element of bool (Bool MA)
SS is functional Element of bool (Bool MA)
(S,MA,I,SS) is functional Element of bool (Bool MA)
(S,MA,(S,MA,I,SS)) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,SS) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,I) \/ (S,MA,SS) is Relation-like S -defined Function-like V17(S) set
M is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
A is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
y is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
x is Relation-like S -defined Function-like V17(S) set
A is Relation-like S -defined Function-like V17(S) set
z is Relation-like S -defined Function-like V17(S) set
A \/ z is Relation-like S -defined Function-like V17(S) set
i is set
x . i is set
(A \/ z) . i is set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
{ (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in (S,MA,I,SS) } is set
union { (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in (S,MA,I,SS) } is set
A . i is set
z . i is set
(A . i) \/ (z . i) is set
SS9 is set
{ (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
SS9 is set
v is Relation-like S -defined Function-like V17(S) Element of Bool MA
v . i is set
{ (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
union { (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
SS9 is set
v is Relation-like S -defined Function-like V17(S) Element of Bool MA
v . i is set
{ (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
{ (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
union { (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
{ (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
{ (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
union { (b₁ . i) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
SS9 is set
SS9 is set
v is Relation-like S -defined Function-like V17(S) Element of Bool MA
v . i is set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is functional Element of bool (Bool MA)
SS is functional Element of bool (Bool MA)
(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,SS) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
M is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
A is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
x is Relation-like S -defined Function-like V17(S) set
A is Relation-like S -defined Function-like V17(S) set
y is set
x . y is set
A . y is set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
{ (b₁ . y) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . y) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
z is set
i is set
{ (b₁ . y) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
SS9 is Relation-like S -defined Function-like V17(S) Element of Bool MA
SS9 . y is set
union { (b₁ . y) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is functional Element of bool (Bool MA)
SS is functional Element of bool (Bool MA)
I /\ SS is set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is functional Element of bool (Bool MA)
SS is functional Element of bool (Bool MA)
(S,MA,I,SS) is functional Element of bool (Bool MA)
(S,MA,(S,MA,I,SS)) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,I) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,SS) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,I) /\ (S,MA,SS) is Relation-like S -defined Function-like V17(S) set
M is Relation-like S -defined Function-like V17(S) set
x is Relation-like S -defined Function-like V17(S) set
A is Relation-like S -defined Function-like V17(S) set
x /\ A is Relation-like S -defined Function-like V17(S) set
A is set
M . A is set
(x /\ A) . A is set
x . A is set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
{ (b₁ . A) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
union { (b₁ . A) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in I } is set
A . A is set
{ (b₁ . A) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
union { (b₁ . A) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
{ (b₁ . A) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in (S,MA,I,SS) } is set
union { (b₁ . A) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in (S,MA,I,SS) } is set
y is set
z is set
i is Relation-like S -defined Function-like V17(S) Element of Bool MA
i . A is set
(x . A) /\ (A . A) is set
S is set
MA is Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
I is set
{ (S,MA,b₁) where b₁ is functional Element of bool (Bool MA) : b₁ in I } is set
union I is set
M is functional Element of bool (Bool MA)
SS is functional Element of bool (Bool MA)
(S,MA,M) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,SS) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
x is set
(S,MA,M) . x is set
(S,MA,SS) . x is set
A is set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
{ (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in M } is set
union { (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in M } is set
A is set
y is Relation-like S -defined Function-like V17(S) Element of Bool MA
y . x is set
z is functional Element of bool (Bool MA)
(S,MA,z) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,z) . x is set
{ (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in z } is set
union { (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in z } is set
i is set
SS9 is Relation-like S -defined Function-like V17(S) Element of Bool MA
SS9 . x is set
{ (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in union I } is set
union { (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in union I } is set
A is set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
{ (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
union { (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in SS } is set
A is set
y is Relation-like S -defined Function-like V17(S) Element of Bool MA
y . x is set
z is set
i is functional Element of bool (Bool MA)
{ (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in i } is set
union { (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in i } is set
(S,MA,i) is Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
(S,MA,i) . x is set
SS9 is set
{ (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in M } is set
union { (b₁ . x) where b₁ is Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in M } is set
S is non empty set
MA is non empty Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
[:(Bool MA),(Bool MA):] is non empty set
bool [:(Bool MA),(Bool MA):] is non empty set
S is non empty set
MA is non empty Relation-like S -defined Function-like V17(S) set
Bool MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool MA)
Bool MA is non empty functional with_common_domain set
bool (Bool MA) is non empty set
[:(Bool MA),(Bool MA):] is non empty set
bool [:(Bool MA),(Bool MA):] is non empty set
id (Bool MA) is non empty Relation-like Bool MA -defined Bool MA -valued Function-like one-to-one V17( Bool MA) quasi_total Element of bool [:(Bool MA),(Bool MA):]
I is non empty Relation-like Bool MA -defined Bool MA -valued Function-like V17( Bool MA) quasi_total Element of bool [:(Bool MA),(Bool MA):]
SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
I . SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
{ (I . b₁) where b₁ is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA : ( b₁ is finite-yielding & (S,b₁) is finite & b₁ c= SS ) } is set
x is set
A is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
I . A is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
(S,A) is set
{ b₁ where b₁ is Element of S : not A . b₁ = {} } is set
x is functional Element of bool (Bool MA)
(S,MA,x) is non empty Relation-like S -defined Function-like V17(S) ManySortedSubset of MA
A is Element of S
SS . A is set
(S,MA,x) . A is set
A is set
y is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
y . A is set
(S,y) is set
{ b₁ where b₁ is Element of S : not y . b₁ = {} } is set
I . y is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
{ (b₁ . A) where b₁ is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in x } is set
union { (b₁ . A) where b₁ is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in x } is set
A is set
{ (b₁ . A) where b₁ is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in x } is set
union { (b₁ . A) where b₁ is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA : b₁ in x } is set
y is set
z is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
z . A is set
i is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
I . i is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
(S,i) is set
{ b₁ where b₁ is Element of S : not i . b₁ = {} } is set
SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
I . SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
M is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
I . SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
I . M is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
I . SS is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
I . (I . SS) is non empty Relation-like S -defined Function-like V17(S) Element of Bool MA
S is non empty 1-sorted
S is non empty non void V62() ManySortedSign
the carrier of S is non empty set
1-sorted(# the carrier of S #) is strict non empty 1-sorted
MA is non-empty MSAlgebra over S
the Sorts of MA is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
SubSort MA is set
the carrier of 1-sorted(# the carrier of S #) is non empty set
Bool the Sorts of MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool the Sorts of MA)
Bool the Sorts of MA is non empty functional with_common_domain set
bool (Bool the Sorts of MA) is non empty set
SS is set
I is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set
Bool I is non empty functional with_common_domain set
bool (Bool I) is non empty set
SS is functional Element of bool (Bool I)
ClosureStr(# I,SS #) is strict ClosureStr over 1-sorted(# the carrier of S #)
the Sorts of ClosureStr(# I,SS #) is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set
the Family of ClosureStr(# I,SS #) is functional Element of bool (Bool the Sorts of ClosureStr(# I,SS #))
Bool the Sorts of ClosureStr(# I,SS #) is non empty functional with_common_domain set
bool (Bool the Sorts of ClosureStr(# I,SS #)) is non empty set
I is strict ClosureStr over 1-sorted(# the carrier of S #)
the Sorts of I is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set
the carrier of 1-sorted(# the carrier of S #) is non empty set
the Family of I is functional Element of bool (Bool the Sorts of I)
Bool the Sorts of I is non empty functional with_common_domain set
bool (Bool the Sorts of I) is non empty set
SS is strict ClosureStr over 1-sorted(# the carrier of S #)
the Sorts of SS is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set
the Family of SS is functional Element of bool (Bool the Sorts of SS)
Bool the Sorts of SS is non empty functional with_common_domain set
bool (Bool the Sorts of SS) is non empty set
S is non empty non void V62() ManySortedSign
the carrier of S is non empty set
MA is strict non-empty MSAlgebra over S
SubSort MA is set
the Sorts of MA is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
Bool the Sorts of MA is non empty functional with_common_domain set
bool (Bool the Sorts of MA) is non empty set
Bool the Sorts of MA is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool the Sorts of MA)
I is set
I is functional Element of bool (Bool the Sorts of MA)
Union the Sorts of MA is set
bool (Union the Sorts of MA) is non empty Element of bool (bool (Union the Sorts of MA))
bool (Union the Sorts of MA) is non empty set
bool (bool (Union the Sorts of MA)) is non empty set
x is functional Element of bool (Bool the Sorts of MA)
|:x:| is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of bool the Sorts of MA
bool the Sorts of MA is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
meet |:x:| is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA
dom (meet |:x:|) is set
rng (meet |:x:|) is set
A is set
y is set
(meet |:x:|) . y is set
dom the Sorts of MA is set
the Sorts of MA . y is set
rng the Sorts of MA is with_non-empty_elements set
union (rng the Sorts of MA) is set
bool ( the Sorts of MA . y) is non empty set
bool (bool ( the Sorts of MA . y)) is non empty set
|:x:| . y is set
z is Element of bool (bool ( the Sorts of MA . y))
Intersect z is Element of bool ( the Sorts of MA . y)
bool (union (rng the Sorts of MA)) is non empty Element of bool (bool (union (rng the Sorts of MA)))
bool (union (rng the Sorts of MA)) is non empty set
bool (bool (union (rng the Sorts of MA))) is non empty set
Funcs ( the carrier of S,(bool (Union the Sorts of MA))) is non empty functional FUNCTION_DOMAIN of the carrier of S, bool (Union the Sorts of MA)
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA
y is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of MA
S is non empty non void V62() ManySortedSign
the carrier of S is non empty set
1-sorted(# the carrier of S #) is strict non empty 1-sorted
MA is strict non-empty MSAlgebra over S
(S,MA) is strict ClosureStr over 1-sorted(# the carrier of S #)
the Sorts of MA is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
Bool the Sorts of MA is non empty functional with_common_domain set
bool (Bool the Sorts of MA) is non empty set
SubSort MA is set
the Family of (S,MA) is functional Element of bool (Bool the Sorts of (S,MA))
the carrier of 1-sorted(# the carrier of S #) is non empty set
the Sorts of (S,MA) is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set
Bool the Sorts of (S,MA) is non empty functional with_common_domain set
bool (Bool the Sorts of (S,MA)) is non empty set
I is non empty functional multiplicative absolutely-multiplicative properly-upper-bound Element of bool (Bool the Sorts of MA)
S is non empty non void V62() ManySortedSign
the carrier of S is non empty set
1-sorted(# the carrier of S #) is strict non empty 1-sorted
MA is strict non-empty MSAlgebra over S
(S,MA) is strict multiplicative absolutely-multiplicative properly-upper-bound ClosureStr over 1-sorted(# the carrier of S #)
ClSys->ClOp (S,MA) is non empty Relation-like Bool the Sorts of (S,MA) -defined Bool the Sorts of (S,MA) -valued Function-like V17( Bool the Sorts of (S,MA)) quasi_total reflexive monotonic idempotent Element of bool [:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):]
the carrier of 1-sorted(# the carrier of S #) is non empty set
the Sorts of (S,MA) is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) set
Bool the Sorts of (S,MA) is non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound Element of bool (Bool the Sorts of (S,MA))
Bool the Sorts of (S,MA) is non empty functional with_common_domain set
bool (Bool the Sorts of (S,MA)) is non empty set
[:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):] is non empty set
bool [:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):] is non empty set
x is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
(ClSys->ClOp (S,MA)) . x is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
{ ((ClSys->ClOp (S,MA)) . b₁) where b₁ is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA) : ( b₁ is finite-yielding & ( the carrier of 1-sorted(# the carrier of S #),b₁) is finite & b₁ c= x ) } is set
A is set
z is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
(ClSys->ClOp (S,MA)) . z is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
( the carrier of 1-sorted(# the carrier of S #),z) is set
{ b₁ where b₁ is Element of the carrier of 1-sorted(# the carrier of S #) : not z . b₁ = {} } is set
y is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
A is functional Element of bool (Bool the Sorts of (S,MA))
( the carrier of 1-sorted(# the carrier of S #), the Sorts of (S,MA),A) is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) ManySortedSubset of the Sorts of (S,MA)
y is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
z is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
i is Element of the carrier of S
y . i is set
z . i is set
SS9 is set
v is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
v . i is set
( the carrier of 1-sorted(# the carrier of S #),v) is set
{ b₁ where b₁ is Element of the carrier of 1-sorted(# the carrier of S #) : not v . b₁ = {} } is set
SS9 is non empty Relation-like Bool the Sorts of (S,MA) -defined Bool the Sorts of (S,MA) -valued Function-like V17( Bool the Sorts of (S,MA)) quasi_total reflexive Element of bool [:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):]
SS9 . v is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
(SS9 . v) . i is set
(ClSys->ClOp (S,MA)) . v is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
{ (b₁ . i) where b₁ is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA) : b₁ in A } is set
union { (b₁ . i) where b₁ is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA) : b₁ in A } is set
v is set
{ (b₁ . i) where b₁ is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA) : b₁ in A } is set
union { (b₁ . i) where b₁ is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA) : b₁ in A } is set
Y is set
ff is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
ff . i is set
a is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
(ClSys->ClOp (S,MA)) . a is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
( the carrier of 1-sorted(# the carrier of S #),a) is set
{ b₁ where b₁ is Element of the carrier of 1-sorted(# the carrier of S #) : not a . b₁ = {} } is set
SS9 is non empty Relation-like Bool the Sorts of (S,MA) -defined Bool the Sorts of (S,MA) -valued Function-like V17( Bool the Sorts of (S,MA)) quasi_total monotonic Element of bool [:(Bool the Sorts of (S,MA)),(Bool the Sorts of (S,MA)):]
SS9 . a is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
SS9 . x is non empty Relation-like the carrier of 1-sorted(# the carrier of S #) -defined Function-like V17( the carrier of 1-sorted(# the carrier of S #)) Element of Bool the Sorts of (S,MA)
x . i is set