:: MSUALG_2 semantic presentation

K168() is Element of bool K164()
K164() is set
bool K164() is non empty set
K101() is set
bool K101() is non empty set
bool K168() is non empty set
{} is empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set
the empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set is empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty set
2 is non empty set
3 is non empty set
product {} is set
{{}} is non empty functional set
S is set
U0 is Relation-like S -defined Function-like V17(S) set
A is Relation-like non-empty S -defined Function-like V17(S) set
U0 \/ A is Relation-like S -defined Function-like V17(S) set
x is set
(U0 \/ A) . x is set
U0 . x is set
A . x is set
(U0 . x) \/ (A . x) is set
A \/ U0 is Relation-like non-empty S -defined Function-like V17(S) set
S is non empty set
S * is non empty functional FinSequence-membered M12(S)
U0 is non empty Relation-like S -defined Function-like V17(S) set
A is non empty Relation-like S -defined Function-like V17(S) set
U0 /\ A is non empty Relation-like S -defined Function-like V17(S) set
x is Relation-like K168() -defined S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of S *
x * (U0 /\ A) is Relation-like K168() -defined Function-like set
product (x * (U0 /\ A)) is set
x * U0 is Relation-like K168() -defined Function-like set
product (x * U0) is set
x * A is Relation-like K168() -defined Function-like set
product (x * A) is set
(product (x * U0)) /\ (product (x * A)) is set
rng x is set
dom U0 is non empty set
dom (x * U0) is set
dom x is Element of bool K168()
dom (U0 /\ A) is non empty set
dom (x * (U0 /\ A)) is set
dom A is non empty set
dom (x * A) is set
L is set
G1 is Relation-like Function-like set
dom G1 is set
a is set
G1 . a is set
(x * A) . a is set
(x * (U0 /\ A)) . a is set
x . a is set
(U0 /\ A) . (x . a) is set
U0 . (x . a) is set
A . (x . a) is set
(U0 . (x . a)) /\ (A . (x . a)) is set
a is set
G1 . a is set
(x * U0) . a is set
(x * (U0 /\ A)) . a is set
x . a is set
(U0 /\ A) . (x . a) is set
U0 . (x . a) is set
A . (x . a) is set
(U0 . (x . a)) /\ (A . (x . a)) is set
L is set
G1 is Relation-like Function-like set
dom G1 is set
a is set
G1 . a is set
(x * (U0 /\ A)) . a is set
x . a is set
(x * U0) . a is set
U0 . (x . a) is set
(x * A) . a is set
a1 is Relation-like Function-like set
dom a1 is set
A . (x . a) is set
(U0 . (x . a)) /\ (A . (x . a)) is set
(U0 /\ A) . (x . a) is set
S is non empty V60() ManySortedSign
S is non empty V60() ManySortedSign
the carrier of S is non empty set
U0 is set
S is non empty set
S * is non empty functional FinSequence-membered M12(S)
[:U0,(S *):] is Relation-like set
bool [:U0,(S *):] is non empty set
[:U0,S:] is Relation-like set
bool [:U0,S:] is non empty set
A is Relation-like U0 -defined S * -valued Function-like V17(U0) quasi_total Element of bool [:U0,(S *):]
x is Relation-like U0 -defined S -valued Function-like V17(U0) quasi_total Element of bool [:U0,S:]
ManySortedSign(# S,U0,A,x #) is strict ManySortedSign
the set is set
{ the set } is non empty set
<*> { the set } is empty Relation-like non-empty empty-yielding K168() -defined { the set } -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of { the set }
{(<*> { the set })} is non empty functional set
A is Relation-like Function-like set
dom A is set
rng A is set
{ the set } * is non empty functional FinSequence-membered M12({ the set })
x is set
[:{ the set },({ the set } *):] is non empty Relation-like set
bool [:{ the set },({ the set } *):] is non empty set
L is Relation-like Function-like set
dom L is set
rng L is set
[:{ the set },{ the set }:] is non empty Relation-like set
bool [:{ the set },{ the set }:] is non empty set
x is non empty Relation-like { the set } -defined { the set } * -valued Function-like V17({ the set }) quasi_total Element of bool [:{ the set },({ the set } *):]
G1 is non empty Relation-like { the set } -defined { the set } -valued Function-like V17({ the set }) quasi_total Element of bool [:{ the set },{ the set }:]
ManySortedSign(# { the set },{ the set },x,G1 #) is non empty V60() strict ManySortedSign
the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) is non empty set
the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #) is set
a2 is Element of the carrier of ManySortedSign(# { the set },{ the set },x,G1 #)
a1 is Element of the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #)
the Arity of ManySortedSign(# { the set },{ the set },x,G1 #) is Relation-like the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #) -defined the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) * -valued Function-like V17( the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #)) quasi_total Element of bool [: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #),( the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) *):]
the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) * is non empty functional FinSequence-membered M12( the carrier of ManySortedSign(# { the set },{ the set },x,G1 #))
[: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #),( the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) *):] is Relation-like set
bool [: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #),( the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) *):] is non empty set
the Arity of ManySortedSign(# { the set },{ the set },x,G1 #) . a1 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like set
the ResultSort of ManySortedSign(# { the set },{ the set },x,G1 #) is Relation-like the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #) -defined the carrier of ManySortedSign(# { the set },{ the set },x,G1 #) -valued Function-like V17( the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #)) quasi_total Element of bool [: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #), the carrier of ManySortedSign(# { the set },{ the set },x,G1 #):]
[: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #), the carrier of ManySortedSign(# { the set },{ the set },x,G1 #):] is Relation-like set
bool [: the carrier' of ManySortedSign(# { the set },{ the set },x,G1 #), the carrier of ManySortedSign(# { the set },{ the set },x,G1 #):] is non empty set
the ResultSort of ManySortedSign(# { the set },{ the set },x,G1 #) . a1 is set
x . a1 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like set
rng x is non empty set
G1 . a1 is set
rng G1 is non empty set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is Element of the carrier of S
the Sorts of U0 . A is set
bool ( the Sorts of U0 . A) is non empty set
the carrier' of S is non empty set
the carrier of S * is non empty functional FinSequence-membered 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 Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
x is non empty set
{ b₁ where b₁ is Element of x : ex b₂ being Element of the carrier' of S st
( the Arity of S . b₂ = {} & the ResultSort of S . b₂ = A & b₁ in rng (Den (b₂,U0)) ) } is set
G1 is set
a is Element of the Sorts of U0 . A
a1 is Element of the carrier' of S
the Arity of S . a1 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . a1 is Element of the carrier of S
Den (a1,U0) is Relation-like Args (a1,U0) -defined Result (a1,U0) -valued Function-like quasi_total Element of bool [:(Args (a1,U0)),(Result (a1,U0)):]
Args (a1,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of U0 #) is non empty set
Result (a1,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (a1,U0)),(Result (a1,U0)):] is Relation-like set
bool [:(Args (a1,U0)),(Result (a1,U0)):] is non empty set
rng (Den (a1,U0)) is set
G1 is Element of bool ( the Sorts of U0 . A)
a1 is non empty set
a is Element of bool ( the Sorts of U0 . A)
{ b₁ where b₁ is Element of a1 : ex b₂ being Element of the carrier' of S st
( the Arity of S . b₂ = {} & the ResultSort of S . b₂ = A & b₁ in rng (Den (b₂,U0)) ) } is set
{} ( the Sorts of U0 . A) is empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool ( the Sorts of U0 . A)
a is non empty set
L is Element of bool ( the Sorts of U0 . A)
{ b₁ where b₁ is Element of a : ex b₂ being Element of the carrier' of S st
( the Arity of S . b₂ = {} & the ResultSort of S . b₂ = A & b₁ in rng (Den (b₂,U0)) ) } is set
a1 is non empty set
G1 is Element of bool ( the Sorts of U0 . A)
{ b₁ where b₁ is Element of a1 : ex b₂ being Element of the carrier' of S st
( the Arity of S . b₂ = {} & the ResultSort of S . b₂ = A & b₁ in rng (Den (b₂,U0)) ) } is set
a2 is Element of bool ( the Sorts of U0 . A)
u23 is Element of bool ( the Sorts of U0 . A)
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is Relation-like Function-like set
dom A is set
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is set
x . L is set
the Sorts of U0 . L is set
G1 is Element of the carrier of S
x . G1 is set
(S,U0,G1) is Element of bool ( the Sorts of U0 . G1)
the Sorts of U0 . G1 is set
bool ( the Sorts of U0 . G1) is non empty set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
G1 is Element of the carrier of S
L . G1 is set
(S,U0,G1) is Element of bool ( the Sorts of U0 . G1)
the Sorts of U0 . G1 is set
bool ( the Sorts of U0 . G1) 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 U0
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
L is set
A . L is set
x . L is set
G1 is Element of the carrier of S
A . G1 is set
(S,U0,G1) is Element of bool ( the Sorts of U0 . G1)
the Sorts of U0 . G1 is set
bool ( the Sorts of U0 . G1) is non empty set
S is non empty non void V60() () ManySortedSign
the carrier of S is non empty set
U0 is non-empty MSAlgebra over S
A is Element of the carrier of S
(S,U0,A) is Element of bool ( the Sorts of U0 . A)
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of U0 . A is non empty set
bool ( the Sorts of U0 . A) is non empty set
dom {} is empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool K168()
rng {} is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set
[:{},{}:] is Relation-like set
bool [:{},{}:] is non empty set
the carrier' of S is non empty set
the carrier of S * is non empty functional FinSequence-membered 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 Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
L is Element of the carrier' of S
the Arity of S . L is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . L is Element of the carrier of S
dom the Arity of S is non empty set
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
dom ( the Sorts of U0 #) is non empty set
rng the Arity of S is non empty set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
dom ( the Arity of S * ( the Sorts of U0 #)) is non empty set
Args (L,U0) is non empty Element of rng ( the Sorts of U0 #)
rng ( the Sorts of U0 #) is non empty set
( the Arity of S * ( the Sorts of U0 #)) . L is set
( the Sorts of U0 #) . ( the Arity of S . L) is set
the_arity_of L is Relation-like K168() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
( the Sorts of U0 #) . (the_arity_of L) is set
(the_arity_of L) * the Sorts of U0 is Relation-like non-empty K168() -defined Function-like set
product ((the_arity_of L) * the Sorts of U0) is set
x is empty Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional V17( {} ) quasi_total V34() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},{}:]
x * the Sorts of U0 is empty Relation-like non-empty empty-yielding K168() -defined {} -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set
product (x * the Sorts of U0) is set
Den (L,U0) is non empty Relation-like Args (L,U0) -defined Result (L,U0) -valued Function-like V17( Args (L,U0)) quasi_total Element of bool [:(Args (L,U0)),(Result (L,U0)):]
Result (L,U0) is non empty Element of rng the Sorts of U0
rng the Sorts of U0 is non empty with_non-empty_elements set
[:(Args (L,U0)),(Result (L,U0)):] is non empty Relation-like set
bool [:(Args (L,U0)),(Result (L,U0)):] is non empty set
rng (Den (L,U0)) is non empty set
dom (Den (L,U0)) is non empty set
(Den (L,U0)) . {} is set
dom the ResultSort of S is non empty set
dom the Sorts of U0 is non empty set
rng the ResultSort of S is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V17( the carrier' of S) set
dom ( the ResultSort of S * the Sorts of U0) is non empty set
( the ResultSort of S * the Sorts of U0) . L is non empty set
a is Element of the Sorts of U0 . A
a1 is non empty set
{ b₁ where b₁ is Element of a1 : ex b₂ being Element of the carrier' of S st
( the Arity of S . b₂ = {} & the ResultSort of S . b₂ = A & b₁ in rng (Den (b₂,U0)) ) } is set
S is non empty non void V60() () ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
A is set
x is Element of the carrier of S
(S,U0) . x is set
(S,U0,x) is non empty Element of bool ( the Sorts of U0 . x)
the Sorts of U0 . x is non empty set
bool ( the Sorts of U0 . x) is non empty set
(S,U0) . A is set
S is non empty non void V60() ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
U0 is Element of the carrier' of S
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * (x #)) . U0 is set
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * (L #)) . U0 is set
the Arity of S . U0 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
G1 is Relation-like K168() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
rng G1 is set
dom x is non empty set
G1 * x is Relation-like K168() -defined Function-like set
dom (G1 * x) is set
dom G1 is Element of bool K168()
G1 * L is Relation-like K168() -defined Function-like set
a is set
(G1 * x) . a is set
(G1 * L) . a is set
G1 . a is set
x . (G1 . a) is set
L . (G1 . a) is set
dom the Arity of S is non empty set
dom ( the Arity of S * (x #)) is non empty set
(x #) . G1 is set
product (G1 * x) is set
dom ( the Arity of S * (L #)) is non empty set
(L #) . G1 is set
product (G1 * L) is set
dom L is non empty set
dom (G1 * L) is set
S is non empty non void V60() ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is Element of the carrier' of S
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
Den (A,U0) is Relation-like Args (A,U0) -defined Result (A,U0) -valued Function-like quasi_total Element of bool [:(Args (A,U0)),(Result (A,U0)):]
Args (A,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # 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 FinSequence-membered M12( the carrier of S)
rng ( the Sorts of U0 #) is non empty set
Result (A,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (A,U0)),(Result (A,U0)):] is Relation-like set
bool [:(Args (A,U0)),(Result (A,U0)):] is non empty 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 Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * (x #)) . A is set
(Den (A,U0)) | (( the Arity of S * (x #)) . A) is Relation-like ( the Arity of S * (x #)) . A -defined Args (A,U0) -defined Result (A,U0) -valued Function-like set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * x) . A is set
[:(( the Arity of S * (x #)) . A),(( the ResultSort of S * x) . A):] is Relation-like set
bool [:(( the Arity of S * (x #)) . A),(( the ResultSort of S * x) . A):] is non empty set
dom the ResultSort of S is non empty set
rng ((Den (A,U0)) | (( the Arity of S * (x #)) . A)) is set
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
rng ((Den (A,U0)) | (( the Arity of S * (x #)) . A)) is set
the ResultSort of S . A is Element of the carrier of S
x . ( the ResultSort of S . A) is set
the Sorts of U0 . ( the ResultSort of S . A) is set
the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * the Sorts of U0) . A is set
dom (Den (A,U0)) is set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * ( the Sorts of U0 #)) . A is set
dom ((Den (A,U0)) | (( the Arity of S * (x #)) . A)) is set
(( the Arity of S * ( the Sorts of U0 #)) . A) /\ (( the Arity of S * (x #)) . A) is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 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 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 * is non empty functional FinSequence-membered M12( 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
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
G1 is set
a is Element of the carrier' of S
(S,U0,a,A) is Relation-like ( the Arity of S * (A #)) . a -defined ( the ResultSort of S * A) . a -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):]
( the Arity of S * (A #)) . a is set
( the ResultSort of S * A) . a is set
[:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is Relation-like set
bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is non empty set
a1 is Element of the carrier' of S
(S,U0,a1,A) is Relation-like ( the Arity of S * (A #)) . a1 -defined ( the ResultSort of S * A) . a1 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a1),(( the ResultSort of S * A) . a1):]
( the Arity of S * (A #)) . a1 is set
( the ResultSort of S * A) . a1 is set
[:(( the Arity of S * (A #)) . a1),(( the ResultSort of S * A) . a1):] is Relation-like set
bool [:(( the Arity of S * (A #)) . a1),(( the ResultSort of S * A) . a1):] is non empty set
G1 is Relation-like Function-like set
dom G1 is set
a is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
dom a is non empty set
a1 is set
a . a1 is set
a2 is Element of the carrier' of S
a . a2 is set
(S,U0,a2,A) is Relation-like ( the Arity of S * (A #)) . a2 -defined ( the ResultSort of S * A) . a2 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):]
( the Arity of S * (A #)) . a2 is set
( the ResultSort of S * A) . a2 is set
[:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):] is Relation-like set
bool [:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):] is non empty set
a1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() set
a2 is set
a1 . a2 is set
( the Arity of S * (A #)) . a2 is set
( the ResultSort of S * A) . a2 is set
[:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):] is Relation-like set
bool [:(( the Arity of S * (A #)) . a2),(( the ResultSort of S * A) . a2):] is non empty set
u23 is Element of the carrier' of S
a1 . u23 is set
(S,U0,u23,A) is Relation-like ( the Arity of S * (A #)) . u23 -defined ( the ResultSort of S * A) . u23 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):]
( the Arity of S * (A #)) . u23 is set
( the ResultSort of S * A) . u23 is set
[:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):] is Relation-like set
bool [:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):] is non empty set
a2 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A
u23 is Element of the carrier' of S
a2 . u23 is set
(S,U0,u23,A) is Relation-like ( the Arity of S * (A #)) . u23 -defined ( the ResultSort of S * A) . u23 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):]
( the Arity of S * (A #)) . u23 is set
( the ResultSort of S * A) . u23 is set
[:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):] is Relation-like set
bool [:(( the Arity of S * (A #)) . u23),(( the ResultSort of S * A) . u23):] is non empty set
x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A
L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A
G1 is set
x . G1 is set
L . G1 is set
a is Element of the carrier' of S
x . a is set
(S,U0,a,A) is Relation-like ( the Arity of S * (A #)) . a -defined ( the ResultSort of S * A) . a -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):]
( the Arity of S * (A #)) . a is set
( the ResultSort of S * A) . a is set
[:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is Relation-like set
bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is non empty set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x is Element of the carrier' of S
Result (x,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * A) . x is set
Den (x,U0) is Relation-like Args (x,U0) -defined Result (x,U0) -valued Function-like quasi_total Element of bool [:(Args (x,U0)),(Result (x,U0)):]
Args (x,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # 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 FinSequence-membered M12( the carrier of S)
rng ( the Sorts of U0 #) is non empty set
[:(Args (x,U0)),(Result (x,U0)):] is Relation-like set
bool [:(Args (x,U0)),(Result (x,U0)):] is non empty 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 Relation-like set
bool [: the carrier' of S,( 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 * ) set
the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * (A #)) . x is set
(Den (x,U0)) | (( the Arity of S * (A #)) . x) is Relation-like ( the Arity of S * (A #)) . x -defined Args (x,U0) -defined Result (x,U0) -valued Function-like set
rng ((Den (x,U0)) | (( the Arity of S * (A #)) . x)) is set
x is Element of the carrier' of S
(S,U0,x,A) is Relation-like ( the Arity of S * (A #)) . x -defined ( the ResultSort of S * A) . x -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . x),(( the ResultSort of S * A) . x):]
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 * is non empty functional FinSequence-membered M12( 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
A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * (A #)) . x is set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * A) . x is set
[:(( the Arity of S * (A #)) . x),(( the ResultSort of S * A) . x):] is Relation-like set
bool [:(( the Arity of S * (A #)) . x),(( the ResultSort of S * A) . x):] is non empty set
Den (x,U0) is Relation-like Args (x,U0) -defined Result (x,U0) -valued Function-like quasi_total Element of bool [:(Args (x,U0)),(Result (x,U0)):]
Args (x,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of U0 #) is non empty set
Result (x,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (x,U0)),(Result (x,U0)):] is Relation-like set
bool [:(Args (x,U0)),(Result (x,U0)):] is non empty set
(Den (x,U0)) | (( the Arity of S * (A #)) . x) is Relation-like ( the Arity of S * (A #)) . x -defined Args (x,U0) -defined Result (x,U0) -valued Function-like set
dom (Den (x,U0)) is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
the carrier' of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A
A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
G1 is set
the Charact of U0 . G1 is set
(S,U0,A) . G1 is set
a is Element of the carrier' of S
the Charact of U0 . a is set
Den (a,U0) is Relation-like Args (a,U0) -defined Result (a,U0) -valued Function-like quasi_total Element of bool [:(Args (a,U0)),(Result (a,U0)):]
Args (a,U0) is Element of rng ( the Sorts of U0 #)
rng ( the Sorts of U0 #) is non empty set
Result (a,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (a,U0)),(Result (a,U0)):] is Relation-like set
bool [:(Args (a,U0)),(Result (a,U0)):] is non empty set
(S,U0,A) . a is set
(S,U0,a,A) is Relation-like ( the Arity of S * (A #)) . a -defined ( the ResultSort of S * A) . a -valued Function-like quasi_total Element of bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):]
( the Arity of S * (A #)) . a is set
( the ResultSort of S * A) . a is set
[:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is Relation-like set
bool [:(( the Arity of S * (A #)) . a),(( the ResultSort of S * A) . a):] is non empty set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 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 set
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
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 * is non empty functional FinSequence-membered M12( 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
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,x) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (x #), the ResultSort of S * x
x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
a is set
the Charact of A . a is set
(S,U0,x) . a is set
a1 is Element of the carrier' of S
the Charact of A . a1 is set
Den (a1,A) is Relation-like Args (a1,A) -defined Result (a1,A) -valued Function-like quasi_total Element of bool [:(Args (a1,A)),(Result (a1,A)):]
Args (a1,A) is Element of rng ( the Sorts of A #)
rng ( the Sorts of A #) is non empty set
Result (a1,A) is Element of rng the Sorts of A
rng the Sorts of A is non empty set
[:(Args (a1,A)),(Result (a1,A)):] is Relation-like set
bool [:(Args (a1,A)),(Result (a1,A)):] is non empty set
(S,U0,x) . a1 is set
(S,U0,a1,x) is Relation-like ( the Arity of S * (x #)) . a1 -defined ( the ResultSort of S * x) . a1 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):]
( the Arity of S * (x #)) . a1 is set
( the ResultSort of S * x) . a1 is set
[:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):] is Relation-like set
bool [:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):] is non empty set
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
the Sorts of U0 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 set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S
A is strict MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,x) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (x #), the ResultSort of S * x
x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
a is set
the Charact of A . a is set
(S,U0,x) . a is set
a1 is Element of the carrier' of S
the Charact of A . a1 is set
Den (a1,U0) is Relation-like Args (a1,U0) -defined Result (a1,U0) -valued Function-like quasi_total Element of bool [:(Args (a1,U0)),(Result (a1,U0)):]
Args (a1,U0) is Element of rng ( the Sorts of U0 #)
rng ( the Sorts of U0 #) is non empty set
Result (a1,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (a1,U0)),(Result (a1,U0)):] is Relation-like set
bool [:(Args (a1,U0)),(Result (a1,U0)):] is non empty set
(S,U0,x) . a1 is set
(S,U0,a1,x) is Relation-like ( the Arity of S * (x #)) . a1 -defined ( the ResultSort of S * x) . a1 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):]
( the Arity of S * (x #)) . a1 is set
( the ResultSort of S * x) . a1 is set
[:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):] is Relation-like set
bool [:(( the Arity of S * (x #)) . a1),(( the ResultSort of S * x) . a1):] is non empty set
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
the Sorts of U0 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 set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the carrier of S is non empty set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the carrier of S is non empty set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict non-empty MSAlgebra over S
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
the Sorts of U0 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 set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of A, the Charact of A #) is strict MSAlgebra over S
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
(S,A,x) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (x #), the ResultSort of S * x
x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
a is Element of the carrier' of S
Den (a,A) is Relation-like Args (a,A) -defined Result (a,A) -valued Function-like quasi_total Element of bool [:(Args (a,A)),(Result (a,A)):]
Args (a,A) is Element of rng ( the Sorts of A #)
rng ( the Sorts of A #) is non empty set
Result (a,A) is Element of rng the Sorts of A
rng the Sorts of A is non empty set
[:(Args (a,A)),(Result (a,A)):] is Relation-like set
bool [:(Args (a,A)),(Result (a,A)):] is non empty set
( the Arity of S * (x #)) . a is set
(Den (a,A)) | (( the Arity of S * (x #)) . a) is Relation-like ( the Arity of S * (x #)) . a -defined Args (a,A) -defined Result (a,A) -valued Function-like set
rng ((Den (a,A)) | (( the Arity of S * (x #)) . a)) is set
rng (Den (a,A)) is set
( the ResultSort of S * x) . a is set
a is set
the Charact of U0 . a is set
(S,A,x) . a is set
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
A is MSAlgebra over S
x is MSAlgebra over S
the carrier of S is non empty set
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of x
the carrier' of S is non empty set
the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
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 * is non empty functional FinSequence-membered M12( 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
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
(S,x,G1) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (G1 #), the ResultSort of S * G1
G1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (G1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * G1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of x
(S,x,a1) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (a1 #), the ResultSort of S * a1
a1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (a1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * a1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
(S,A,L) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (L #), the ResultSort of S * L
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
u12 is Element of the carrier' of S
Den (u12,A) is Relation-like Args (u12,A) -defined Result (u12,A) -valued Function-like quasi_total Element of bool [:(Args (u12,A)),(Result (u12,A)):]
Args (u12,A) is Element of rng ( the Sorts of A #)
rng ( the Sorts of A #) is non empty set
Result (u12,A) is Element of rng the Sorts of A
rng the Sorts of A is non empty set
[:(Args (u12,A)),(Result (u12,A)):] is Relation-like set
bool [:(Args (u12,A)),(Result (u12,A)):] is non empty set
(S,x,G1) . u12 is set
(S,x,u12,G1) is Relation-like ( the Arity of S * (G1 #)) . u12 -defined ( the ResultSort of S * G1) . u12 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (G1 #)) . u12),(( the ResultSort of S * G1) . u12):]
( the Arity of S * (G1 #)) . u12 is set
( the ResultSort of S * G1) . u12 is set
[:(( the Arity of S * (G1 #)) . u12),(( the ResultSort of S * G1) . u12):] is Relation-like set
bool [:(( the Arity of S * (G1 #)) . u12),(( the ResultSort of S * G1) . u12):] is non empty set
Den (u12,x) is Relation-like Args (u12,x) -defined Result (u12,x) -valued Function-like quasi_total Element of bool [:(Args (u12,x)),(Result (u12,x)):]
Args (u12,x) is Element of rng ( the Sorts of x #)
the Sorts of x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of x #) is non empty set
Result (u12,x) is Element of rng the Sorts of x
rng the Sorts of x is non empty set
[:(Args (u12,x)),(Result (u12,x)):] is Relation-like set
bool [:(Args (u12,x)),(Result (u12,x)):] is non empty set
(Den (u12,x)) | (( the Arity of S * (G1 #)) . u12) is Relation-like ( the Arity of S * (G1 #)) . u12 -defined Args (u12,x) -defined Result (u12,x) -valued Function-like set
( the Arity of S * (L #)) . u12 is set
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
a # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (a #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * (a #)) . u12 is set
Den (u12,U0) is Relation-like Args (u12,U0) -defined Result (u12,U0) -valued Function-like quasi_total Element of bool [:(Args (u12,U0)),(Result (u12,U0)):]
Args (u12,U0) is Element of rng ( the Sorts of U0 #)
rng ( the Sorts of U0 #) is non empty set
Result (u12,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (u12,U0)),(Result (u12,U0)):] is Relation-like set
bool [:(Args (u12,U0)),(Result (u12,U0)):] is non empty set
(S,A,L) . u12 is set
(S,A,u12,L) is Relation-like ( the Arity of S * (L #)) . u12 -defined ( the ResultSort of S * L) . u12 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (L #)) . u12),(( the ResultSort of S * L) . u12):]
( the ResultSort of S * L) . u12 is set
[:(( the Arity of S * (L #)) . u12),(( the ResultSort of S * L) . u12):] is Relation-like set
bool [:(( the Arity of S * (L #)) . u12),(( the ResultSort of S * L) . u12):] is non empty set
((Den (u12,x)) | (( the Arity of S * (G1 #)) . u12)) | (( the Arity of S * (L #)) . u12) is Relation-like ( the Arity of S * (L #)) . u12 -defined ( the Arity of S * (G1 #)) . u12 -defined Result (u12,x) -valued Function-like set
(( the Arity of S * (G1 #)) . u12) /\ (( the Arity of S * (L #)) . u12) is set
(Den (u12,x)) | ((( the Arity of S * (G1 #)) . u12) /\ (( the Arity of S * (L #)) . u12)) is Relation-like (( the Arity of S * (G1 #)) . u12) /\ (( the Arity of S * (L #)) . u12) -defined Args (u12,x) -defined Result (u12,x) -valued Function-like set
(Den (u12,x)) | (( the Arity of S * (L #)) . u12) is Relation-like ( the Arity of S * (L #)) . u12 -defined Args (u12,x) -defined Result (u12,x) -valued Function-like set
rng ((Den (u12,x)) | (( the Arity of S * (L #)) . u12)) is set
( the ResultSort of S * the Sorts of U0) . u12 is set
u12 is set
the Charact of U0 . u12 is set
(S,x,a1) . u12 is set
C is Element of the carrier' of S
Den (C,A) is Relation-like Args (C,A) -defined Result (C,A) -valued Function-like quasi_total Element of bool [:(Args (C,A)),(Result (C,A)):]
Args (C,A) is Element of rng ( the Sorts of A #)
rng ( the Sorts of A #) is non empty set
Result (C,A) is Element of rng the Sorts of A
rng the Sorts of A is non empty set
[:(Args (C,A)),(Result (C,A)):] is Relation-like set
bool [:(Args (C,A)),(Result (C,A)):] is non empty set
(S,x,G1) . C is set
(S,x,C,G1) is Relation-like ( the Arity of S * (G1 #)) . C -defined ( the ResultSort of S * G1) . C -valued Function-like quasi_total Element of bool [:(( the Arity of S * (G1 #)) . C),(( the ResultSort of S * G1) . C):]
( the Arity of S * (G1 #)) . C is set
( the ResultSort of S * G1) . C is set
[:(( the Arity of S * (G1 #)) . C),(( the ResultSort of S * G1) . C):] is Relation-like set
bool [:(( the Arity of S * (G1 #)) . C),(( the ResultSort of S * G1) . C):] is non empty set
Den (C,x) is Relation-like Args (C,x) -defined Result (C,x) -valued Function-like quasi_total Element of bool [:(Args (C,x)),(Result (C,x)):]
Args (C,x) is Element of rng ( the Sorts of x #)
the Sorts of x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of x #) is non empty set
Result (C,x) is Element of rng the Sorts of x
rng the Sorts of x is non empty set
[:(Args (C,x)),(Result (C,x)):] is Relation-like set
bool [:(Args (C,x)),(Result (C,x)):] is non empty set
(Den (C,x)) | (( the Arity of S * (G1 #)) . C) is Relation-like ( the Arity of S * (G1 #)) . C -defined Args (C,x) -defined Result (C,x) -valued Function-like set
(S,A,C,L) is Relation-like ( the Arity of S * (L #)) . C -defined ( the ResultSort of S * L) . C -valued Function-like quasi_total Element of bool [:(( the Arity of S * (L #)) . C),(( the ResultSort of S * L) . C):]
( the Arity of S * (L #)) . C is set
( the ResultSort of S * L) . C is set
[:(( the Arity of S * (L #)) . C),(( the ResultSort of S * L) . C):] is Relation-like set
bool [:(( the Arity of S * (L #)) . C),(( the ResultSort of S * L) . C):] is non empty set
((Den (C,x)) | (( the Arity of S * (G1 #)) . C)) | (( the Arity of S * (L #)) . C) is Relation-like ( the Arity of S * (L #)) . C -defined ( the Arity of S * (G1 #)) . C -defined Result (C,x) -valued Function-like set
(( the Arity of S * (G1 #)) . C) /\ (( the Arity of S * (L #)) . C) is set
(Den (C,x)) | ((( the Arity of S * (G1 #)) . C) /\ (( the Arity of S * (L #)) . C)) is Relation-like (( the Arity of S * (G1 #)) . C) /\ (( the Arity of S * (L #)) . C) -defined Args (C,x) -defined Result (C,x) -valued Function-like set
( the Arity of S * (a1 #)) . C is set
(Den (C,x)) | (( the Arity of S * (a1 #)) . C) is Relation-like ( the Arity of S * (a1 #)) . C -defined Args (C,x) -defined Result (C,x) -valued Function-like set
(S,x,C,a1) is Relation-like ( the Arity of S * (a1 #)) . C -defined ( the ResultSort of S * a1) . C -valued Function-like quasi_total Element of bool [:(( the Arity of S * (a1 #)) . C),(( the ResultSort of S * a1) . C):]
( the ResultSort of S * a1) . C is set
[:(( the Arity of S * (a1 #)) . C),(( the ResultSort of S * a1) . C):] is Relation-like set
bool [:(( the Arity of S * (a1 #)) . C),(( the ResultSort of S * a1) . C):] is non empty set
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
the Sorts of U0 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 set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of A, the Charact of A #) is strict MSAlgebra over S
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
(S,A,x) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (x #), the ResultSort of S * x
x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,L) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (L #), the ResultSort of S * L
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
a1 is set
the Charact of U0 . a1 is set
(S,U0,L) . a1 is set
a2 is Element of the carrier' of S
Args (a2,A) is Element of rng ( the Sorts of A #)
rng ( the Sorts of A #) is non empty set
( the Arity of S * (L #)) . a2 is set
(S,A,a2,x) is Relation-like ( the Arity of S * (x #)) . a2 -defined ( the ResultSort of S * x) . a2 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (x #)) . a2),(( the ResultSort of S * x) . a2):]
( the Arity of S * (x #)) . a2 is set
( the ResultSort of S * x) . a2 is set
[:(( the Arity of S * (x #)) . a2),(( the ResultSort of S * x) . a2):] is Relation-like set
bool [:(( the Arity of S * (x #)) . a2),(( the ResultSort of S * x) . a2):] is non empty set
Den (a2,A) is Relation-like Args (a2,A) -defined Result (a2,A) -valued Function-like quasi_total Element of bool [:(Args (a2,A)),(Result (a2,A)):]
Result (a2,A) is Element of rng the Sorts of A
rng the Sorts of A is non empty set
[:(Args (a2,A)),(Result (a2,A)):] is Relation-like set
bool [:(Args (a2,A)),(Result (a2,A)):] is non empty set
(Den (a2,A)) | (( the Arity of S * (x #)) . a2) is Relation-like ( the Arity of S * (x #)) . a2 -defined Args (a2,A) -defined Result (a2,A) -valued Function-like set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
A is (S,U0)
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x is (S,U0)
the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of U0 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 set
the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
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 * is non empty functional FinSequence-membered M12( 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
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of x
(S,x,a) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (a #), the ResultSort of S * a
a # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (a #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * a is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,L) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (L #), the ResultSort of S * L
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the Charact of x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of x #), the ResultSort of S * the Sorts of x
the Sorts of x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
(S,U0,G1) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (G1 #), the ResultSort of S * G1
G1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (G1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * G1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
u23 is Element of the carrier' of S
Den (u23,x) is Relation-like Args (u23,x) -defined Result (u23,x) -valued Function-like quasi_total Element of bool [:(Args (u23,x)),(Result (u23,x)):]
Args (u23,x) is Element of rng ( the Sorts of x #)
rng ( the Sorts of x #) is non empty set
Result (u23,x) is Element of rng the Sorts of x
rng the Sorts of x is non empty set
[:(Args (u23,x)),(Result (u23,x)):] is Relation-like set
bool [:(Args (u23,x)),(Result (u23,x)):] is non empty set
(S,U0,G1) . u23 is set
(S,U0,u23,G1) is Relation-like ( the Arity of S * (G1 #)) . u23 -defined ( the ResultSort of S * G1) . u23 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (G1 #)) . u23),(( the ResultSort of S * G1) . u23):]
( the Arity of S * (G1 #)) . u23 is set
( the ResultSort of S * G1) . u23 is set
[:(( the Arity of S * (G1 #)) . u23),(( the ResultSort of S * G1) . u23):] is Relation-like set
bool [:(( the Arity of S * (G1 #)) . u23),(( the ResultSort of S * G1) . u23):] is non empty set
Den (u23,U0) is Relation-like Args (u23,U0) -defined Result (u23,U0) -valued Function-like quasi_total Element of bool [:(Args (u23,U0)),(Result (u23,U0)):]
Args (u23,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of U0 #) is non empty set
Result (u23,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (u23,U0)),(Result (u23,U0)):] is Relation-like set
bool [:(Args (u23,U0)),(Result (u23,U0)):] is non empty set
(Den (u23,U0)) | (( the Arity of S * (G1 #)) . u23) is Relation-like ( the Arity of S * (G1 #)) . u23 -defined Args (u23,U0) -defined Result (u23,U0) -valued Function-like set
Den (u23,A) is Relation-like Args (u23,A) -defined Result (u23,A) -valued Function-like quasi_total Element of bool [:(Args (u23,A)),(Result (u23,A)):]
Args (u23,A) is Element of rng ( the Sorts of A #)
rng ( the Sorts of A #) is non empty set
Result (u23,A) is Element of rng the Sorts of A
rng the Sorts of A is non empty set
[:(Args (u23,A)),(Result (u23,A)):] is Relation-like set
bool [:(Args (u23,A)),(Result (u23,A)):] is non empty set
(S,U0,L) . u23 is set
(S,U0,u23,L) is Relation-like ( the Arity of S * (L #)) . u23 -defined ( the ResultSort of S * L) . u23 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (L #)) . u23),(( the ResultSort of S * L) . u23):]
( the Arity of S * (L #)) . u23 is set
( the ResultSort of S * L) . u23 is set
[:(( the Arity of S * (L #)) . u23),(( the ResultSort of S * L) . u23):] is Relation-like set
bool [:(( the Arity of S * (L #)) . u23),(( the ResultSort of S * L) . u23):] is non empty set
(Den (u23,U0)) | (( the Arity of S * (L #)) . u23) is Relation-like ( the Arity of S * (L #)) . u23 -defined Args (u23,U0) -defined Result (u23,U0) -valued Function-like set
(( the Arity of S * (G1 #)) . u23) /\ (( the Arity of S * (L #)) . u23) is set
(Den (u23,U0)) | ((( the Arity of S * (G1 #)) . u23) /\ (( the Arity of S * (L #)) . u23)) is Relation-like (( the Arity of S * (G1 #)) . u23) /\ (( the Arity of S * (L #)) . u23) -defined Args (u23,U0) -defined Result (u23,U0) -valued Function-like set
(Den (u23,x)) | (( the Arity of S * (L #)) . u23) is Relation-like ( the Arity of S * (L #)) . u23 -defined Args (u23,x) -defined Result (u23,x) -valued Function-like set
rng ((Den (u23,x)) | (( the Arity of S * (L #)) . u23)) is set
( the ResultSort of S * the Sorts of A) . u23 is set
u23 is set
the Charact of A . u23 is set
(S,x,a) . u23 is set
u12 is Element of the carrier' of S
Den (u12,x) is Relation-like Args (u12,x) -defined Result (u12,x) -valued Function-like quasi_total Element of bool [:(Args (u12,x)),(Result (u12,x)):]
Args (u12,x) is Element of rng ( the Sorts of x #)
rng ( the Sorts of x #) is non empty set
Result (u12,x) is Element of rng the Sorts of x
rng the Sorts of x is non empty set
[:(Args (u12,x)),(Result (u12,x)):] is Relation-like set
bool [:(Args (u12,x)),(Result (u12,x)):] is non empty set
(S,U0,G1) . u12 is set
(S,U0,u12,G1) is Relation-like ( the Arity of S * (G1 #)) . u12 -defined ( the ResultSort of S * G1) . u12 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (G1 #)) . u12),(( the ResultSort of S * G1) . u12):]
( the Arity of S * (G1 #)) . u12 is set
( the ResultSort of S * G1) . u12 is set
[:(( the Arity of S * (G1 #)) . u12),(( the ResultSort of S * G1) . u12):] is Relation-like set
bool [:(( the Arity of S * (G1 #)) . u12),(( the ResultSort of S * G1) . u12):] is non empty set
Den (u12,U0) is Relation-like Args (u12,U0) -defined Result (u12,U0) -valued Function-like quasi_total Element of bool [:(Args (u12,U0)),(Result (u12,U0)):]
Args (u12,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of U0 #) is non empty set
Result (u12,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (u12,U0)),(Result (u12,U0)):] is Relation-like set
bool [:(Args (u12,U0)),(Result (u12,U0)):] is non empty set
(Den (u12,U0)) | (( the Arity of S * (G1 #)) . u12) is Relation-like ( the Arity of S * (G1 #)) . u12 -defined Args (u12,U0) -defined Result (u12,U0) -valued Function-like set
(S,U0,u12,L) is Relation-like ( the Arity of S * (L #)) . u12 -defined ( the ResultSort of S * L) . u12 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (L #)) . u12),(( the ResultSort of S * L) . u12):]
( the Arity of S * (L #)) . u12 is set
( the ResultSort of S * L) . u12 is set
[:(( the Arity of S * (L #)) . u12),(( the ResultSort of S * L) . u12):] is Relation-like set
bool [:(( the Arity of S * (L #)) . u12),(( the ResultSort of S * L) . u12):] is non empty set
(Den (u12,U0)) | (( the Arity of S * (L #)) . u12) is Relation-like ( the Arity of S * (L #)) . u12 -defined Args (u12,U0) -defined Result (u12,U0) -valued Function-like set
(( the Arity of S * (G1 #)) . u12) /\ (( the Arity of S * (L #)) . u12) is set
(Den (u12,U0)) | ((( the Arity of S * (G1 #)) . u12) /\ (( the Arity of S * (L #)) . u12)) is Relation-like (( the Arity of S * (G1 #)) . u12) /\ (( the Arity of S * (L #)) . u12) -defined Args (u12,U0) -defined Result (u12,U0) -valued Function-like set
(Den (u12,x)) | (( the Arity of S * (L #)) . u12) is Relation-like ( the Arity of S * (L #)) . u12 -defined Args (u12,x) -defined Result (u12,x) -valued Function-like set
(S,x,u12,a) is Relation-like ( the Arity of S * (a #)) . u12 -defined ( the ResultSort of S * a) . u12 -valued Function-like quasi_total Element of bool [:(( the Arity of S * (a #)) . u12),(( the ResultSort of S * a) . u12):]
( the Arity of S * (a #)) . u12 is set
( the ResultSort of S * a) . u12 is set
[:(( the Arity of S * (a #)) . u12),(( the ResultSort of S * a) . u12):] is Relation-like set
bool [:(( the Arity of S * (a #)) . u12),(( the ResultSort of S * a) . u12):] is non empty set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
A is (S,U0)
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x is (S,U0)
the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of A, the Charact of A #) is strict MSAlgebra over S
the Charact of x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of x #), the ResultSort of S * the Sorts of x
the Sorts of x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of x, the Charact of x #) is strict MSAlgebra over S
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is (S,U0)
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x is set
(S,U0) . x is set
the Sorts of A . x is set
G1 is set
L is Element of the carrier of S
the Sorts of U0 . L is set
(S,U0) . L is set
(S,U0,L) is Element of bool ( the Sorts of U0 . L)
bool ( the Sorts of U0 . L) is non empty set
L is Element of the carrier of S
the Sorts of U0 . L is set
(S,U0,L) is Element of bool ( the Sorts of U0 . L)
bool ( the Sorts of U0 . L) is non empty set
the carrier' of S is non empty set
the carrier of S * is non empty functional FinSequence-membered 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 Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
a1 is non empty set
{ b₁ where b₁ is Element of a1 : ex b₂ being Element of the carrier' of S st
( the Arity of S . b₂ = {} & the ResultSort of S . b₂ = L & b₁ in rng (Den (b₂,U0)) ) } is set
a1 is Element of the Sorts of U0 . L
a2 is Element of the carrier' of S
the Arity of S . a2 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . a2 is Element of the carrier of S
Den (a2,U0) is Relation-like Args (a2,U0) -defined Result (a2,U0) -valued Function-like quasi_total Element of bool [:(Args (a2,U0)),(Result (a2,U0)):]
Args (a2,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of U0 #) is non empty set
Result (a2,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (a2,U0)),(Result (a2,U0)):] is Relation-like set
bool [:(Args (a2,U0)),(Result (a2,U0)):] is non empty set
rng (Den (a2,U0)) is set
a2 is Element of the carrier' of S
the Arity of S . a2 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
the ResultSort of S . a2 is Element of the carrier of S
Den (a2,U0) is Relation-like Args (a2,U0) -defined Result (a2,U0) -valued Function-like quasi_total Element of bool [:(Args (a2,U0)),(Result (a2,U0)):]
Args (a2,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of U0 #) is non empty set
Result (a2,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (a2,U0)),(Result (a2,U0)):] is Relation-like set
bool [:(Args (a2,U0)),(Result (a2,U0)):] is non empty set
rng (Den (a2,U0)) is set
dom the Arity of S is non empty set
rng the Arity of S is non empty set
dom {} is empty Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool K168()
rng {} is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding K168() -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set
[:{},{}:] is Relation-like set
bool [:{},{}:] is non empty set
dom the ResultSort 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 U0
a # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
dom (a #) is non empty set
the Arity of S * (a #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
dom ( the Arity of S * (a #)) is non empty set
( the Arity of S * (a #)) . a2 is set
(a #) . ( the Arity of S . a2) is set
the_arity_of a2 is Relation-like K168() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
(a #) . (the_arity_of a2) is set
(the_arity_of a2) * a is Relation-like K168() -defined Function-like set
product ((the_arity_of a2) * a) is set
u23 is empty Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional V17( {} ) quasi_total V34() FinSequence-like FinSubsequence-like FinSequence-membered Element of bool [:{},{}:]
u23 * a is empty Relation-like non-empty empty-yielding K168() -defined {} -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set
product (u23 * a) is set
dom ( the Sorts of U0 #) is non empty set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
dom ( the Arity of S * ( the Sorts of U0 #)) is non empty set
(Den (a2,U0)) | (( the Arity of S * (a #)) . a2) is Relation-like ( the Arity of S * (a #)) . a2 -defined Args (a2,U0) -defined Result (a2,U0) -valued Function-like set
rng ((Den (a2,U0)) | (( the Arity of S * (a #)) . a2)) is set
the ResultSort of S * a is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * a) . a2 is set
dom (Den (a2,U0)) is set
( the Arity of S * ( the Sorts of U0 #)) . a2 is set
( the Sorts of U0 #) . ( the Arity of S . a2) is set
( the Sorts of U0 #) . (the_arity_of a2) is set
(the_arity_of a2) * the Sorts of U0 is Relation-like K168() -defined Function-like set
product ((the_arity_of a2) * the Sorts of U0) is set
u23 * the Sorts of U0 is empty Relation-like non-empty empty-yielding K168() -defined {} -defined Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered set
product (u23 * the Sorts of U0) is set
L is Element of the carrier of S
the Sorts of U0 . L is set
S is non empty non void V60() () ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
A is non-empty (S,U0)
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() () ManySortedSign
the carrier of S is non empty set
U0 is non-empty MSAlgebra over S
A is non-empty (S,U0)
the Sorts of A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
x is non-empty (S,U0)
the Sorts of x is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of A /\ the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0) is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0) /\ (S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is set
G1 is Element of the carrier of S
( the Sorts of A /\ the Sorts of x) . G1 is set
the Sorts of A . G1 is non empty set
the Sorts of x . G1 is non empty set
( the Sorts of A . G1) /\ ( the Sorts of x . G1) is set
(S,U0) . G1 is non empty set
( the Sorts of A /\ the Sorts of x) . L is set
a is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of bool (bool (Union the Sorts of U0))
bool (Union the Sorts of U0) is non empty set
bool (bool (Union the Sorts of U0)) is non empty set
Funcs ( the carrier of S,(bool (Union the Sorts of U0))) is non empty functional FUNCTION_DOMAIN of the carrier of S, bool (Union the Sorts of U0)
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x is set
L is set
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
a is set
x is set
L is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is set
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of bool (bool (Union the Sorts of U0))
bool (Union the Sorts of U0) is non empty set
bool (bool (Union the Sorts of U0)) is non empty set
Funcs ( the carrier of S,(bool (Union the Sorts of U0))) is non empty functional FUNCTION_DOMAIN of the carrier of S, bool (Union the Sorts of U0)
rng the Sorts of U0 is non empty set
union (rng the Sorts of U0) is set
dom the Sorts of U0 is non empty set
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of bool (bool (Union the Sorts of U0))
bool (Union the Sorts of U0) is non empty set
bool (bool (Union the Sorts of U0)) is non empty set
Funcs ( the carrier of S,(bool (Union the Sorts of U0))) is non empty functional FUNCTION_DOMAIN of the carrier of S, bool (Union the Sorts of U0)
A is set
x is set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
G1 is set
A is set
x is set
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
(S,U0) is set
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of bool (bool (Union the Sorts of U0))
bool (Union the Sorts of U0) is non empty set
bool (bool (Union the Sorts of U0)) is non empty set
Funcs ( the carrier of S,(bool (Union the Sorts of U0))) is non empty functional FUNCTION_DOMAIN of the carrier of S, bool (Union the Sorts of U0)
x is set
rng the Sorts of U0 is non empty set
union (rng the Sorts of U0) is set
dom the Sorts of U0 is non empty set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
L is non empty set
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
(S,U0) is non empty set
A is Element of (S,U0)
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty set
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of bool (bool (Union the Sorts of U0))
bool (Union the Sorts of U0) is non empty set
bool (bool (Union the Sorts of U0)) is non empty set
dom x is non empty set
dom the Sorts of U0 is non empty set
rng x is non empty set
union (rng x) is set
rng the Sorts of U0 is non empty set
union (rng the Sorts of U0) is set
G1 is set
a is set
a1 is set
x . a1 is set
the Sorts of U0 . a1 is set
bool (union (rng x)) is non empty Element of bool (bool (union (rng x)))
bool (union (rng x)) is non empty set
bool (bool (union (rng x))) is non empty set
bool (union (rng the Sorts of U0)) is non empty Element of bool (bool (union (rng the Sorts of U0)))
bool (union (rng the Sorts of U0)) is non empty set
bool (bool (union (rng the Sorts of U0))) is non empty set
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
Funcs ( the carrier of S,(bool (Union the Sorts of U0))) is non empty functional FUNCTION_DOMAIN of the carrier of S, bool (Union the Sorts of U0)
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0) 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 U0
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of bool (bool (Union the Sorts of U0))
bool (Union the Sorts of U0) is non empty set
bool (bool (Union the Sorts of U0)) is non empty set
dom A is non empty set
dom the Sorts of U0 is non empty set
rng A is non empty set
union (rng A) is set
rng the Sorts of U0 is non empty set
union (rng the Sorts of U0) is set
L is set
G1 is set
a is set
A . a is set
the Sorts of U0 . a is set
bool (union (rng A)) is non empty Element of bool (bool (union (rng A)))
bool (union (rng A)) is non empty set
bool (bool (union (rng A))) is non empty set
bool (union (rng the Sorts of U0)) is non empty Element of bool (bool (union (rng the Sorts of U0)))
bool (union (rng the Sorts of U0)) is non empty set
bool (bool (union (rng the Sorts of U0))) is non empty set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
Funcs ( the carrier of S,(bool (Union the Sorts of U0))) is non empty functional FUNCTION_DOMAIN of the carrier of S, bool (Union the Sorts of U0)
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty set
x is Element of the carrier of S
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of bool (bool (Union the Sorts of U0))
bool (Union the Sorts of U0) is non empty set
bool (bool (Union the Sorts of U0)) is non empty set
G1 is set
rng the Sorts of U0 is non empty set
union (rng the Sorts of U0) is set
bool (union (rng the Sorts of U0)) is non empty Element of bool (bool (union (rng the Sorts of U0)))
bool (union (rng the Sorts of U0)) is non empty set
bool (bool (union (rng the Sorts of U0))) is non empty set
dom the Sorts of U0 is non empty set
the Sorts of U0 . x is set
a is set
a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
a1 . x is set
a is set
a2 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
a1 is set
a2 . x is set
L is set
G1 is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x is Element of the carrier of S
(S,U0,A,x) is set
(S,U0,A) is non empty set
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of bool (bool (Union the Sorts of U0))
bool (Union the Sorts of U0) is non empty set
bool (bool (Union the Sorts of U0)) is non empty set
a is set
rng the Sorts of U0 is non empty set
union (rng the Sorts of U0) is set
bool (union (rng the Sorts of U0)) is non empty Element of bool (bool (union (rng the Sorts of U0)))
bool (union (rng the Sorts of U0)) is non empty set
bool (bool (union (rng the Sorts of U0))) is non empty set
dom the Sorts of U0 is non empty set
the Sorts of U0 . x is set
a1 is set
a2 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
a2 . x is set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the Sorts of U0 . x is set
a1 is non empty set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x is Relation-like Function-like set
dom x is set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a is set
L . a is set
the Sorts of U0 . a is set
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty set
a1 is Element of the carrier of S
the Sorts of U0 . a1 is set
(S,U0,A,a1) is non empty set
L . a1 is set
meet (S,U0,A,a1) is set
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
a is Element of the carrier of S
G1 . a is set
(S,U0,A,a) is non empty set
meet (S,U0,A,a) is set
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
G1 is set
x . G1 is set
L . G1 is set
a is Element of the carrier of S
x . a is set
(S,U0,A,a) is non empty set
meet (S,U0,A,a) is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0) \/ A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,A) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x is set
((S,U0) \/ A) . x is set
(S,U0,A) . x is set
L is Element of the carrier of S
(S,U0,A,L) is non empty set
((S,U0) \/ A) . L is set
G1 is set
(S,U0,A) 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 U0
a . L is set
(S,U0,A) . L is set
meet (S,U0,A,L) is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0) \/ A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,A) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x is set
L is Element of the carrier of S
(S,U0,A,L) is non empty set
((S,U0) \/ A) . L is set
G1 is set
(S,U0,A) 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 U0
a . L is set
meet (S,U0,A,L) is set
(S,U0,A) . x is set
G1 is set
S is non empty non void V60() ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
U0 is Element of the carrier' of S
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
(S,A,x) is non empty set
(S,A,x) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
(S,A,x) # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ((S,A,x) #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * ((S,A,x) #)) . U0 is set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * (L #)) . U0 is set
G1 is set
(S,A,x) . G1 is set
L . G1 is set
a is Element of the carrier of S
(S,A,x) . a is set
(S,A,x,a) is non empty set
meet (S,A,x,a) is set
L . a is set
S is non empty non void V60() ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
U0 is Element of the carrier' of S
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
Den (U0,A) is Relation-like Args (U0,A) -defined Result (U0,A) -valued Function-like quasi_total Element of bool [:(Args (U0,A)),(Result (U0,A)):]
Args (U0,A) is Element of rng ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of A #) is non empty set
Result (U0,A) is Element of rng the Sorts of A
rng the Sorts of A is non empty set
[:(Args (U0,A)),(Result (U0,A)):] is Relation-like set
bool [:(Args (U0,A)),(Result (U0,A)):] is non empty set
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
(S,A,x) is non empty set
(S,A,x) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
(S,A,x) # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ((S,A,x) #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * ((S,A,x) #)) . U0 is set
(Den (U0,A)) | (( the Arity of S * ((S,A,x) #)) . U0) is Relation-like ( the Arity of S * ((S,A,x) #)) . U0 -defined Args (U0,A) -defined Result (U0,A) -valued Function-like set
rng ((Den (U0,A)) | (( the Arity of S * ((S,A,x) #)) . U0)) is set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
the ResultSort of S * L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * L) . U0 is set
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * (L #)) . U0 is set
(( the Arity of S * (L #)) . U0) /\ (( the Arity of S * ((S,A,x) #)) . U0) is set
(Den (U0,A)) | (( the Arity of S * (L #)) . U0) is Relation-like ( the Arity of S * (L #)) . U0 -defined Args (U0,A) -defined Result (U0,A) -valued Function-like set
((Den (U0,A)) | (( the Arity of S * (L #)) . U0)) | (( the Arity of S * ((S,A,x) #)) . U0) is Relation-like ( the Arity of S * ((S,A,x) #)) . U0 -defined Args (U0,A) -defined Result (U0,A) -valued Function-like set
rng ((Den (U0,A)) | (( the Arity of S * (L #)) . U0)) is set
S is non empty non void V60() ManySortedSign
the carrier' of S is non empty set
the carrier of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
U0 is Element of the carrier' of S
A is MSAlgebra over S
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
Den (U0,A) is Relation-like Args (U0,A) -defined Result (U0,A) -valued Function-like quasi_total Element of bool [:(Args (U0,A)),(Result (U0,A)):]
Args (U0,A) is Element of rng ( the Sorts of A #)
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of A #) is non empty set
Result (U0,A) is Element of rng the Sorts of A
rng the Sorts of A is non empty set
[:(Args (U0,A)),(Result (U0,A)):] is Relation-like set
bool [:(Args (U0,A)),(Result (U0,A)):] is non empty set
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
(S,A,x) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
(S,A,x) # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ((S,A,x) #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * ((S,A,x) #)) . U0 is set
(Den (U0,A)) | (( the Arity of S * ((S,A,x) #)) . U0) is Relation-like ( the Arity of S * ((S,A,x) #)) . U0 -defined Args (U0,A) -defined Result (U0,A) -valued Function-like set
rng ((Den (U0,A)) | (( the Arity of S * ((S,A,x) #)) . U0)) is set
the ResultSort of S * (S,A,x) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * (S,A,x)) . U0 is set
L is set
the_result_sort_of U0 is Element of the carrier of S
the ResultSort of S . U0 is Element of the carrier of S
dom the ResultSort of S is non empty set
(S,A,x) . (the_result_sort_of U0) is set
(S,A,x,(the_result_sort_of U0)) is non empty set
meet (S,A,x,(the_result_sort_of U0)) is set
a is set
(S,A,x) is non empty set
a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of A
a1 . (the_result_sort_of U0) is set
the ResultSort of S * a1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * a1) . U0 is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the carrier' of S is non empty set
x is Element of the carrier' of S
Den (x,U0) is Relation-like Args (x,U0) -defined Result (x,U0) -valued Function-like quasi_total Element of bool [:(Args (x,U0)),(Result (x,U0)):]
Args (x,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # 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 FinSequence-membered M12( the carrier of S)
rng ( the Sorts of U0 #) is non empty set
Result (x,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (x,U0)),(Result (x,U0)):] is Relation-like set
bool [:(Args (x,U0)),(Result (x,U0)):] is non empty 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 Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is non empty set
(S,U0,A) # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ((S,U0,A) #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the Arity of S * ((S,U0,A) #)) . x is set
(Den (x,U0)) | (( the Arity of S * ((S,U0,A) #)) . x) is Relation-like ( the Arity of S * ((S,U0,A) #)) . x -defined Args (x,U0) -defined Result (x,U0) -valued Function-like set
rng ((Den (x,U0)) | (( the Arity of S * ((S,U0,A) #)) . x)) is set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * (S,U0,A) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * (S,U0,A)) . x is set
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0) \/ A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (A #), the ResultSort of S * A
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# A,(S,U0,A) #) is strict MSAlgebra over S
x is MSAlgebra over S
the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of x #), the ResultSort of S * the Sorts of x
the Sorts of x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,L) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (L #), the ResultSort of S * L
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
the carrier of S is non empty set
A is (S,U0)
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x is (S,U0)
the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of A /\ the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of U0 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 set
the Sorts of U0 /\ the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,L) is strict (S,U0)
G1 is strict (S,U0)
the Sorts of G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of G1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of G1 #), the ResultSort of S * the Sorts of G1
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 * is non empty functional FinSequence-membered M12( 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
the Sorts of G1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of G1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of G1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
a2 is Element of the carrier' of S
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
a # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (a #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
dom ( the Arity of S * (a #)) is non empty set
a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
a1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (a1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
dom ( the Arity of S * (a1 #)) is non empty set
Den (a2,U0) is Relation-like Args (a2,U0) -defined Result (a2,U0) -valued Function-like quasi_total Element of bool [:(Args (a2,U0)),(Result (a2,U0)):]
Args (a2,U0) is Element of rng ( the Sorts of U0 #)
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
rng ( the Sorts of U0 #) is non empty set
Result (a2,U0) is Element of rng the Sorts of U0
rng the Sorts of U0 is non empty set
[:(Args (a2,U0)),(Result (a2,U0)):] is Relation-like set
bool [:(Args (a2,U0)),(Result (a2,U0)):] is non empty set
( the Arity of S * (a1 #)) . a2 is set
(Den (a2,U0)) | (( the Arity of S * (a1 #)) . a2) is Relation-like ( the Arity of S * (a1 #)) . a2 -defined Args (a2,U0) -defined Result (a2,U0) -valued Function-like set
rng ((Den (a2,U0)) | (( the Arity of S * (a1 #)) . a2)) is set
the ResultSort of S * a1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * a1) . a2 is set
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
dom ( the Arity of S * (L #)) is non empty set
( the Arity of S * (L #)) . a2 is set
the Arity of S . a2 is Relation-like K168() -defined Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
(L #) . ( the Arity of S . a2) is set
the_arity_of a2 is Relation-like K168() -defined the carrier of S -valued Function-like V34() FinSequence-like FinSubsequence-like Element of the carrier of S *
(L #) . (the_arity_of a2) is set
a /\ a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(the_arity_of a2) * (a /\ a1) is Relation-like K168() -defined Function-like set
product ((the_arity_of a2) * (a /\ a1)) is set
(the_arity_of a2) * a is Relation-like K168() -defined Function-like set
product ((the_arity_of a2) * a) is set
(the_arity_of a2) * a1 is Relation-like K168() -defined Function-like set
product ((the_arity_of a2) * a1) is set
(product ((the_arity_of a2) * a)) /\ (product ((the_arity_of a2) * a1)) is set
(a #) . (the_arity_of a2) is set
((a #) . (the_arity_of a2)) /\ (product ((the_arity_of a2) * a1)) is set
(a1 #) . (the_arity_of a2) is set
((a #) . (the_arity_of a2)) /\ ((a1 #) . (the_arity_of a2)) is set
(a #) . ( the Arity of S . a2) is set
((a #) . ( the Arity of S . a2)) /\ ((a1 #) . (the_arity_of a2)) is set
(a1 #) . ( the Arity of S . a2) is set
((a #) . ( the Arity of S . a2)) /\ ((a1 #) . ( the Arity of S . a2)) is set
( the Arity of S * (a #)) . a2 is set
(( the Arity of S * (a #)) . a2) /\ ((a1 #) . ( the Arity of S . a2)) is set
(( the Arity of S * (a #)) . a2) /\ (( the Arity of S * (a1 #)) . a2) is set
(Den (a2,U0)) | (( the Arity of S * (L #)) . a2) is Relation-like ( the Arity of S * (L #)) . a2 -defined Args (a2,U0) -defined Result (a2,U0) -valued Function-like set
((Den (a2,U0)) | (( the Arity of S * (a1 #)) . a2)) | (( the Arity of S * (a #)) . a2) is Relation-like ( the Arity of S * (a #)) . a2 -defined Args (a2,U0) -defined Result (a2,U0) -valued Function-like set
rng ((Den (a2,U0)) | (( the Arity of S * (L #)) . a2)) is set
(Den (a2,U0)) | (( the Arity of S * (a #)) . a2) is Relation-like ( the Arity of S * (a #)) . a2 -defined Args (a2,U0) -defined Result (a2,U0) -valued Function-like set
rng ((Den (a2,U0)) | (( the Arity of S * (a #)) . a2)) is set
the ResultSort of S * a is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
( the ResultSort of S * a) . a2 is set
dom ( the ResultSort of S * a1) is non empty set
((Den (a2,U0)) | (( the Arity of S * (a #)) . a2)) | (( the Arity of S * (a1 #)) . a2) is Relation-like ( the Arity of S * (a1 #)) . a2 -defined Args (a2,U0) -defined Result (a2,U0) -valued Function-like set
(( the ResultSort of S * a) . a2) /\ (( the ResultSort of S * a1) . a2) is set
the ResultSort of S * L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
dom ( the ResultSort of S * L) is non empty set
dom ( the ResultSort of S * a) is non empty set
the ResultSort of S . a2 is Element of the carrier of S
a . ( the ResultSort of S . a2) is set
(a . ( the ResultSort of S . a2)) /\ (( the ResultSort of S * a1) . a2) is set
a1 . ( the ResultSort of S . a2) is set
(a . ( the ResultSort of S . a2)) /\ (a1 . ( the ResultSort of S . a2)) is set
the_result_sort_of a2 is Element of the carrier of S
a . (the_result_sort_of a2) is set
(a . (the_result_sort_of a2)) /\ (a1 . ( the ResultSort of S . a2)) is set
a1 . (the_result_sort_of a2) is set
(a . (the_result_sort_of a2)) /\ (a1 . (the_result_sort_of a2)) is set
L . (the_result_sort_of a2) is set
L . ( the ResultSort of S . a2) is set
( the ResultSort of S * L) . a2 is set
(S,U0,L) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (L #), the ResultSort of S * L
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# L,(S,U0,L) #) is strict MSAlgebra over S
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,a) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (a #), the ResultSort of S * a
a # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (a #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * a is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
L is strict (S,U0)
the Sorts of L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of L #), the ResultSort of S * the Sorts of L
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 * is non empty functional FinSequence-membered M12( 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
the Sorts of L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
G1 is strict (S,U0)
the Sorts of G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of G1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of G1 #), the ResultSort of S * the Sorts of G1
the Sorts of G1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of G1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of G1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,(S,U0,A)) is strict (S,U0)
L is strict (S,U0)
the Sorts of L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,(S,U0,A)) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ((S,U0,A) #), the ResultSort of S * (S,U0,A)
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
(S,U0,A) # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ((S,U0,A) #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * (S,U0,A) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# (S,U0,A),(S,U0,(S,U0,A)) #) is strict MSAlgebra over S
G1 is (S,U0)
the Sorts of G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty set
a1 is set
the Sorts of L . a1 is set
the Sorts of G1 . a1 is set
a2 is Element of the carrier of S
the Sorts of L . a2 is set
(S,U0,A,a2) is non empty set
meet (S,U0,A,a2) is set
a . a2 is set
x is strict (S,U0)
the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is strict (S,U0)
the Sorts of L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is non-empty MSAlgebra over S
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is strict (S,U0)
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0) \/ A is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,A) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,x) is strict (S,U0)
(S,U0,x) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (x #), the ResultSort of S * x
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * x is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# x,(S,U0,x) #) is strict MSAlgebra over S
L is strict non-empty (S,U0)
the Sorts of L is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
G1 is (S,U0)
the Sorts of G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty set
a1 is set
the Sorts of L . a1 is set
the Sorts of G1 . a1 is set
a2 is Element of the carrier of S
the Sorts of L . a2 is non empty set
(S,U0,A,a2) is non empty set
meet (S,U0,A,a2) is set
a . a2 is set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is strict (S,U0)
the Sorts of (S,U0,A) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of (S,U0,A) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of (S,U0,A) #), the ResultSort of S * the Sorts of (S,U0,A)
the Sorts of (S,U0,A) # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of (S,U0,A) #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of (S,U0,A) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,L) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (L #), the ResultSort of S * L
L # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (L #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * L is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is (S,U0)
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of A, the Charact of A #) is strict MSAlgebra over S
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,x) is strict (S,U0)
the Sorts of (S,U0,x) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,(S,U0)) is strict (S,U0)
A is (S,U0)
(S,U0,(S,U0,(S,U0)),A) is strict (S,U0)
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of (S,U0,(S,U0)) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of (S,U0,(S,U0,(S,U0)),A) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of (S,U0,(S,U0)) /\ the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
A is (S,U0)
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x is (S,U0)
the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of A \/ the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,G1) is strict (S,U0)
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,a) is strict (S,U0)
a is strict (S,U0)
a1 is strict (S,U0)
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,G1) is strict (S,U0)
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is non-empty MSAlgebra over S
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
A is (S,U0)
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
x \/ the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,x) is strict (S,U0)
(S,U0,(S,U0,x),A) is strict (S,U0)
(S,U0,L) is strict (S,U0)
the Sorts of (S,U0,x) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of (S,U0,L) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of (S,U0,x) /\ the Sorts of (S,U0,L) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,(S,U0,x),(S,U0,L)) is strict (S,U0)
the Sorts of (S,U0,(S,U0,x),(S,U0,L)) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
a \/ G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,a1) is strict (S,U0)
the Sorts of (S,U0,(S,U0,x),A) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x \/ G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is non-empty MSAlgebra over S
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
A is (S,U0)
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,x) is strict (S,U0)
(S,U0,(S,U0,x),A) is strict (S,U0)
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
x \/ the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
A is (S,U0)
x is (S,U0)
(S,U0,A,x) is strict (S,U0)
(S,U0,x,A) is strict (S,U0)
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
L \/ G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,a) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
A is (S,U0)
x is (S,U0)
(S,U0,A,x) is strict (S,U0)
(S,U0,A,(S,U0,A,x)) is strict (S,U0)
the Sorts of A 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 set
the Charact of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of A #), the ResultSort of S * the Sorts of A
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of A # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of A #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of A is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of A, the Charact of A #) is strict MSAlgebra over S
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of (S,U0,A,(S,U0,A,x)) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of (S,U0,A,x) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of A /\ the Sorts of (S,U0,A,x) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
L \/ G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,a) is strict (S,U0)
the Charact of (S,U0,A,(S,U0,A,x)) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of (S,U0,A,(S,U0,A,x)) #), the ResultSort of S * the Sorts of (S,U0,A,(S,U0,A,x))
the Sorts of (S,U0,A,(S,U0,A,x)) # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of (S,U0,A,(S,U0,A,x)) #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * the Sorts of (S,U0,A,(S,U0,A,x)) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,a1) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (a1 #), the ResultSort of S * a1
a1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (a1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * a1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
A is (S,U0)
x is (S,U0)
(S,U0,A,x) is strict (S,U0)
(S,U0,(S,U0,A,x),x) is strict (S,U0)
the Sorts of x 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 set
the Charact of x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of x #), the ResultSort of S * the Sorts of x
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of x # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of x #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of x is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of x, the Charact of x #) is strict MSAlgebra over S
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of (S,U0,A,x) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
L \/ G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of A /\ the Sorts of x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,a) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
(S,U0) is non empty set
{ (S,U0,(S,U0,b₁)) where b₁ is Element of (S,U0) : verum } is set
A is set
x is set
L is Element of (S,U0)
(S,U0,L) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,(S,U0,L)) is strict (S,U0)
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
L is strict (S,U0)
the Sorts of L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
a is Element of (S,U0)
(S,U0,a) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,(S,U0,a)) is strict (S,U0)
A is set
x is set
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
(S,U0) is set
the strict (S,U0) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty set
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
A is Element of (S,U0)
x is Element of (S,U0)
L is strict (S,U0)
G1 is strict (S,U0)
(S,U0,L,G1) is strict (S,U0)
a is Element of (S,U0)
a1 is strict (S,U0)
a2 is strict (S,U0)
(S,U0,a1,a2) is strict (S,U0)
A is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
x is Element of (S,U0)
G1 is strict (S,U0)
L is Element of (S,U0)
a is strict (S,U0)
A . (x,L) is Element of (S,U0)
(S,U0,G1,a) is strict (S,U0)
A is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
x is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
L is Element of (S,U0)
G1 is Element of (S,U0)
A . (L,G1) is Element of (S,U0)
x . (L,G1) is Element of (S,U0)
a is strict (S,U0)
a1 is strict (S,U0)
(S,U0,a,a1) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty set
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
A is Element of (S,U0)
x is Element of (S,U0)
L is strict (S,U0)
G1 is strict (S,U0)
(S,U0,L,G1) is strict (S,U0)
a is Element of (S,U0)
a1 is strict (S,U0)
a2 is strict (S,U0)
(S,U0,a1,a2) is strict (S,U0)
A is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
x is Element of (S,U0)
G1 is strict (S,U0)
L is Element of (S,U0)
a is strict (S,U0)
A . (x,L) is Element of (S,U0)
(S,U0,G1,a) is strict (S,U0)
A is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
x is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
L is Element of (S,U0)
G1 is Element of (S,U0)
A . (L,G1) is Element of (S,U0)
x . (L,G1) is Element of (S,U0)
a is strict (S,U0)
a1 is strict (S,U0)
(S,U0,a,a1) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
x is Element of (S,U0)
L is Element of (S,U0)
(S,U0) . (x,L) is Element of (S,U0)
(S,U0) . (L,x) is Element of (S,U0)
the carrier of S is non empty set
G1 is strict (S,U0)
the Sorts of G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a is strict (S,U0)
the Sorts of a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of G1 \/ the Sorts of a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,G1,a) is strict (S,U0)
a2 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,a2) is strict (S,U0)
(S,U0,a,G1) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
x is Element of (S,U0)
L is Element of (S,U0)
G1 is Element of (S,U0)
(S,U0) . (L,G1) is Element of (S,U0)
(S,U0) . (x,((S,U0) . (L,G1))) is Element of (S,U0)
(S,U0) . (x,L) is Element of (S,U0)
(S,U0) . (((S,U0) . (x,L)),G1) is Element of (S,U0)
the carrier of S is non empty set
a is strict (S,U0)
the Sorts of a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a1 is strict (S,U0)
the Sorts of a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
a2 is strict (S,U0)
the Sorts of a2 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a1 \/ the Sorts of a2 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a \/ ( the Sorts of a1 \/ the Sorts of a2) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,a,a1) is strict (S,U0)
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a \/ the Sorts of a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
B is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
C is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
C \/ the Sorts of a2 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,(S,U0,a,a1),a2) is strict (S,U0)
(S,U0,C) is strict (S,U0)
(S,U0,(S,U0,C),a2) is strict (S,U0)
(S,U0,B) is strict (S,U0)
(S,U0,a1,a2) is strict (S,U0)
(S,U0,a,(S,U0,a1,a2)) is strict (S,U0)
u12 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,u12) is strict (S,U0)
(S,U0,a,(S,U0,u12)) is strict (S,U0)
(S,U0,(S,U0,u12),a) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
x is Element of (S,U0)
L is Element of (S,U0)
(S,U0) . (x,L) is Element of (S,U0)
(S,U0) . (L,x) is Element of (S,U0)
the carrier of S is non empty set
a is strict (S,U0)
G1 is strict (S,U0)
(S,U0,a,G1) is strict (S,U0)
the Sorts of (S,U0,a,G1) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a /\ the Sorts of G1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the carrier' of S is non empty set
the Charact of (S,U0,a,G1) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of (S,U0,a,G1) #), the ResultSort of S * the Sorts of (S,U0,a,G1)
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 * is non empty functional FinSequence-membered M12( 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
the Sorts of (S,U0,a,G1) # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of (S,U0,a,G1) #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of (S,U0,a,G1) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,a1) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (a1 #), the ResultSort of S * a1
a1 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (a1 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * a1 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
(S,U0,G1,a) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
x is Element of (S,U0)
L is Element of (S,U0)
G1 is Element of (S,U0)
(S,U0) . (L,G1) is Element of (S,U0)
(S,U0) . (x,((S,U0) . (L,G1))) is Element of (S,U0)
(S,U0) . (x,L) is Element of (S,U0)
(S,U0) . (((S,U0) . (x,L)),G1) is Element of (S,U0)
a1 is strict (S,U0)
a2 is strict (S,U0)
(S,U0,a1,a2) is strict (S,U0)
a is strict (S,U0)
(S,U0,a,a1) is strict (S,U0)
the carrier of S is non empty set
the Sorts of (S,U0,a,a1) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a /\ the Sorts of a1 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,a,(S,U0,a1,a2)) is strict (S,U0)
the Sorts of (S,U0,a,(S,U0,a1,a2)) 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 set
the Charact of (S,U0,a,(S,U0,a1,a2)) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of (S,U0,a,(S,U0,a1,a2)) #), the ResultSort of S * the Sorts of (S,U0,a,(S,U0,a1,a2))
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 * is non empty functional FinSequence-membered M12( 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
the Sorts of (S,U0,a,(S,U0,a1,a2)) # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of (S,U0,a,(S,U0,a1,a2)) #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of (S,U0,a,(S,U0,a1,a2)) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
C is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,C) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * (C #), the ResultSort of S * C
C # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * (C #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
the ResultSort of S * C is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
u12 is Element of (S,U0)
(S,U0) . (u12,G1) is Element of (S,U0)
(S,U0,(S,U0,a,a1),a2) is strict (S,U0)
the Sorts of (S,U0,a1,a2) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a2 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a1 /\ the Sorts of a2 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
the Sorts of a /\ ( the Sorts of a1 /\ the Sorts of a2) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
u23 is Element of (S,U0)
(S,U0) . (x,u23) is Element of (S,U0)
C is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
( the Sorts of a /\ the Sorts of a1) /\ the Sorts of a2 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty strict LattStr
the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty set
x is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
G1 is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L "\/" G1 is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty Relation-like [: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] -defined the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #) -valued Function-like V17([: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]) quasi_total Element of bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]
[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
[:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty set
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) . (L,G1) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x "\/" (L "\/" G1) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) . (x,(L "\/" G1)) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x "\/" L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) . (x,L) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
(x "\/" L) "\/" G1 is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) . ((x "\/" L),G1) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x "/\" L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty Relation-like [: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] -defined the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #) -valued Function-like V17([: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]) quasi_total Element of bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]
[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
[:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty set
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) . (x,L) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L "/\" x is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) . (L,x) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x "\/" L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty Relation-like [: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] -defined the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #) -valued Function-like V17([: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]) quasi_total Element of bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]
[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
[:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty set
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) . (x,L) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x "/\" (x "\/" L) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty Relation-like [: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] -defined the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #) -valued Function-like V17([: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]) quasi_total Element of bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) . (x,(x "\/" L)) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
G1 is Element of (S,U0)
a is Element of (S,U0)
(S,U0) . (G1,a) is Element of (S,U0)
(S,U0) . (G1,((S,U0) . (G1,a))) is Element of (S,U0)
a1 is strict (S,U0)
a2 is strict (S,U0)
(S,U0,a1,a2) is strict (S,U0)
(S,U0,a1,(S,U0,a1,a2)) is strict (S,U0)
x is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x "/\" L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty Relation-like [: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] -defined the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #) -valued Function-like V17([: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]) quasi_total Element of bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]
[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
[:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty set
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) . (x,L) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
(x "/\" L) "\/" L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty Relation-like [: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] -defined the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #) -valued Function-like V17([: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]) quasi_total Element of bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) . ((x "/\" L),L) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
G1 is Element of (S,U0)
a is Element of (S,U0)
(S,U0) . (G1,a) is Element of (S,U0)
(S,U0) . (((S,U0) . (G1,a)),a) is Element of (S,U0)
a1 is strict (S,U0)
a2 is strict (S,U0)
(S,U0,a1,a2) is strict (S,U0)
(S,U0,(S,U0,a1,a2),a2) is strict (S,U0)
x is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
G1 is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L "/\" G1 is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty Relation-like [: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] -defined the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #) -valued Function-like V17([: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]) quasi_total Element of bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]
[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
[:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty set
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) . (L,G1) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x "/\" (L "/\" G1) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) . (x,(L "/\" G1)) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x "/\" L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) . (x,L) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
(x "/\" L) "/\" G1 is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_meet of LattStr(# (S,U0),(S,U0),(S,U0) #) . ((x "/\" L),G1) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
x "\/" L is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty Relation-like [: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] -defined the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #) -valued Function-like V17([: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]) quasi_total Element of bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):]
[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
[:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty Relation-like set
bool [:[: the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #), the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):], the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #):] is non empty set
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) . (x,L) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
L "\/" x is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
the L_join of LattStr(# (S,U0),(S,U0),(S,U0) #) . (L,x) is Element of the carrier of LattStr(# (S,U0),(S,U0),(S,U0) #)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty strict LattStr
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,(S,U0)) is strict (S,U0)
the carrier of (S,U0) is non empty set
L is Element of (S,U0)
G1 is Element of the carrier of (S,U0)
a is Element of the carrier of (S,U0)
G1 "/\" a is Element of the carrier of (S,U0)
the L_meet of (S,U0) is non empty Relation-like [: the carrier of (S,U0), the carrier of (S,U0):] -defined the carrier of (S,U0) -valued Function-like V17([: the carrier of (S,U0), the carrier of (S,U0):]) quasi_total Element of bool [:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):]
[: the carrier of (S,U0), the carrier of (S,U0):] is non empty Relation-like set
[:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):] is non empty Relation-like set
bool [:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):] is non empty set
the L_meet of (S,U0) . (G1,a) is Element of the carrier of (S,U0)
a "/\" G1 is Element of the carrier of (S,U0)
the L_meet of (S,U0) . (a,G1) is Element of the carrier of (S,U0)
a1 is Element of (S,U0)
G1 "/\" a is Element of the carrier of (S,U0)
a2 is strict (S,U0)
(S,U0,(S,U0,(S,U0)),a2) is strict (S,U0)
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
x is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,x) is strict (S,U0)
the carrier of (S,U0) is non empty set
L is Element of (S,U0)
G1 is Element of the carrier of (S,U0)
a is Element of the carrier of (S,U0)
G1 "\/" a is Element of the carrier of (S,U0)
the L_join of (S,U0) is non empty Relation-like [: the carrier of (S,U0), the carrier of (S,U0):] -defined the carrier of (S,U0) -valued Function-like V17([: the carrier of (S,U0), the carrier of (S,U0):]) quasi_total Element of bool [:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):]
[: the carrier of (S,U0), the carrier of (S,U0):] is non empty Relation-like set
[:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):] is non empty Relation-like set
bool [:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):] is non empty set
the L_join of (S,U0) . (G1,a) is Element of the carrier of (S,U0)
a "\/" G1 is Element of the carrier of (S,U0)
the L_join of (S,U0) . (a,G1) is Element of the carrier of (S,U0)
a1 is Element of (S,U0)
G1 "\/" a is Element of the carrier of (S,U0)
a2 is strict (S,U0)
(S,U0,(S,U0,x),a2) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty strict LattStr
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty strict LattStr
Bottom (S,U0) is Element of the carrier of (S,U0)
the carrier of (S,U0) is non empty set
(S,U0) is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
the carrier of S is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0,(S,U0)) is strict (S,U0)
x is Element of (S,U0)
a is Element of the carrier of (S,U0)
a1 is Element of (S,U0)
G1 is Element of the carrier of (S,U0)
G1 "/\" a is Element of the carrier of (S,U0)
the L_meet of (S,U0) is non empty Relation-like [: the carrier of (S,U0), the carrier of (S,U0):] -defined the carrier of (S,U0) -valued Function-like V17([: the carrier of (S,U0), the carrier of (S,U0):]) quasi_total Element of bool [:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):]
[: the carrier of (S,U0), the carrier of (S,U0):] is non empty Relation-like set
[:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):] is non empty Relation-like set
bool [:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):] is non empty set
the L_meet of (S,U0) . (G1,a) is Element of the carrier of (S,U0)
a2 is strict (S,U0)
(S,U0,(S,U0,(S,U0)),a2) is strict (S,U0)
a "/\" G1 is Element of the carrier of (S,U0)
the L_meet of (S,U0) . (a,G1) is Element of the carrier of (S,U0)
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is non-empty MSAlgebra over S
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty strict LattStr
Top (S,U0) is Element of the carrier of (S,U0)
the carrier of (S,U0) 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 U0
(S,U0,A) is strict (S,U0)
x is Element of (S,U0)
a is Element of the carrier of (S,U0)
a1 is Element of (S,U0)
G1 is Element of the carrier of (S,U0)
G1 "\/" a is Element of the carrier of (S,U0)
the L_join of (S,U0) is non empty Relation-like [: the carrier of (S,U0), the carrier of (S,U0):] -defined the carrier of (S,U0) -valued Function-like V17([: the carrier of (S,U0), the carrier of (S,U0):]) quasi_total Element of bool [:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):]
[: the carrier of (S,U0), the carrier of (S,U0):] is non empty Relation-like set
[:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):] is non empty Relation-like set
bool [:[: the carrier of (S,U0), the carrier of (S,U0):], the carrier of (S,U0):] is non empty set
the L_join of (S,U0) . (G1,a) is Element of the carrier of (S,U0)
a2 is strict (S,U0)
(S,U0,(S,U0,A),a2) is strict (S,U0)
a "\/" G1 is Element of the carrier of (S,U0)
the L_join of (S,U0) . (a,G1) is Element of the carrier of (S,U0)
S is non empty non void V60() ManySortedSign
U0 is non-empty MSAlgebra over S
(S,U0) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
(S,U0) is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
[:(S,U0),(S,U0):] is non empty Relation-like set
[:[:(S,U0),(S,U0):],(S,U0):] is non empty Relation-like set
bool [:[:(S,U0),(S,U0):],(S,U0):] is non empty set
(S,U0) is non empty Relation-like [:(S,U0),(S,U0):] -defined (S,U0) -valued Function-like V17([:(S,U0),(S,U0):]) quasi_total Element of bool [:[:(S,U0),(S,U0):],(S,U0):]
LattStr(# (S,U0),(S,U0),(S,U0) #) is non empty strict LattStr
Top (S,U0) is Element of the carrier of (S,U0)
the carrier of (S,U0) is non empty set
the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S -defined Function-like V17( the carrier of S) set
the carrier of S is non empty set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict non-empty MSAlgebra over S
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is strict (S,U0)
S is non empty non void V60() ManySortedSign
U0 is MSAlgebra over S
the Sorts of U0 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 set
the Charact of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) V83() ManySortedFunction of the Arity of S * ( the Sorts of U0 #), the ResultSort of S * the Sorts of U0
the carrier' of S is non empty 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 * is non empty functional FinSequence-membered M12( 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
the Sorts of U0 # is non empty Relation-like the carrier of S * -defined Function-like V17( the carrier of S * ) set
the Arity of S * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
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 Relation-like set
bool [: the carrier' of S, the carrier of S:] is non empty set
the ResultSort of S * the Sorts of U0 is non empty Relation-like the carrier' of S -defined Function-like V17( the carrier' of S) set
MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
A is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
(S,U0,A) is non empty set
S is non empty non void V60() ManySortedSign
the carrier of S is non empty set
U0 is MSAlgebra over S
the Sorts of U0 is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) set
(S,U0) 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 U0
(S,U0,A) is non empty set
x is set
L is non empty Relation-like the carrier of S -defined Function-like V17( the carrier of S) ManySortedSubset of the Sorts of U0
Union the Sorts of U0 is set
bool (Union the Sorts of U0) is non empty Element of bool (bool (Union the Sorts of U0))
bool (Union the Sorts of U0) is non empty set
bool (bool (Union the Sorts of U0)) is non empty set
Funcs ( the carrier of S,(bool (Union the Sorts of U0))) is non empty functional FUNCTION_DOMAIN of the carrier of S, bool (Union the Sorts of U0)