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