:: OSALG_2 semantic presentation

K152() is Element of K10(K148())

K148() is set

K10(K148()) is non empty set

K98() is set

K10(K98()) is non empty set

K10(K152()) is non empty set

{} is empty Relation-like non-empty empty-yielding K152() -defined Function-like one-to-one constant functional V31() V79() V80() V81() set

1 is non empty set

{{},1} is non empty set

2 is non empty set

3 is non empty set

S1 is non empty V99() V100() V101() RelStr

the carrier of S1 is non empty set

U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

U0 /\ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is Element of the carrier of S1

G1 is Element of the carrier of S1

B . L is set

B . G1 is set

U0 . L is set

U0 . G1 is set

B . L is set

B . G1 is set

(U0 /\ B) . L is set

(U0 . L) /\ (B . L) is set

(U0 /\ B) . G1 is set

(U0 . G1) /\ (B . G1) is set

S1 is non empty V99() V100() V101() RelStr

the carrier of S1 is non empty set

U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

U0 \/ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is Element of the carrier of S1

G1 is Element of the carrier of S1

B . L is set

B . G1 is set

U0 . L is set

U0 . G1 is set

B . L is set

B . G1 is set

(U0 \/ B) . L is set

(U0 . L) \/ (B . L) is set

(U0 \/ B) . G1 is set

(U0 . G1) \/ (B . G1) is set

S1 is non empty V99() V100() V101() RelStr

the carrier of S1 is non empty set

U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of U0

S1 is non empty V99() V100() V101() RelStr

the carrier of S1 is non empty set

U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of U0

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

{{}} is non empty functional set

the Relation-like Function-like Element of {{}} is Relation-like Function-like Element of {{}}

TrivialOSA (S1,{{}}, the Relation-like Function-like Element of {{}}) is strict non-empty order-sorted monotone MSAlgebra over S1

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is non-empty order-sorted MSAlgebra over S1

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

S1 is non empty non void V52() strict all-with_const_op ManySortedSign

OSSign S1 is non empty non void V52() V99() V100() V101() V148() strict order-sorted discernable op-discrete monotone V170() OverloadedRSSign

the carrier of (OSSign S1) is non empty set

U0 is Element of the carrier of (OSSign S1)

the carrier of S1 is non empty set

B is Element of the carrier of S1

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

B is Element of the carrier' of S1

the Arity of S1 . B is Relation-like K152() -defined Function-like V31() V79() V80() set

the ResultSort of S1 . B is set

the carrier' of (OSSign S1) is non empty set

the Arity of (OSSign S1) is Relation-like the carrier' of (OSSign S1) -defined the carrier of (OSSign S1) * -valued Function-like V21( the carrier' of (OSSign S1), the carrier of (OSSign S1) * ) Element of K10(K11( the carrier' of (OSSign S1),( the carrier of (OSSign S1) *)))

the carrier of (OSSign S1) * is non empty functional V81() M12( the carrier of (OSSign S1))

K11( the carrier' of (OSSign S1),( the carrier of (OSSign S1) *)) is non empty Relation-like set

K10(K11( the carrier' of (OSSign S1),( the carrier of (OSSign S1) *))) is non empty set

the Arity of (OSSign S1) . B is Relation-like K152() -defined Function-like V31() V79() V80() set

the ResultSort of (OSSign S1) is Relation-like the carrier' of (OSSign S1) -defined the carrier of (OSSign S1) -valued Function-like V21( the carrier' of (OSSign S1), the carrier of (OSSign S1)) Element of K10(K11( the carrier' of (OSSign S1), the carrier of (OSSign S1)))

K11( the carrier' of (OSSign S1), the carrier of (OSSign S1)) is non empty Relation-like set

K10(K11( the carrier' of (OSSign S1), the carrier of (OSSign S1))) is non empty set

the ResultSort of (OSSign S1) . B is set

the non empty non void V52() strict all-with_const_op ManySortedSign is non empty non void V52() strict all-with_const_op ManySortedSign

OSSign the non empty non void V52() strict all-with_const_op ManySortedSign is non empty non void V52() V99() V100() V101() V148() strict order-sorted discernable op-discrete monotone V170() OverloadedRSSign

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is order-sorted MSAlgebra over S1

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the carrier of S1 is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of U0 #), the ResultSort of S1 * the Sorts of U0

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * the Sorts of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S1

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is order-sorted MSAlgebra over S1

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the carrier of S1 is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of U0 #), the ResultSort of S1 * the Sorts of U0

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * the Sorts of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S1

B is strict MSSubAlgebra of U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is order-sorted MSAlgebra over S1

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the carrier of S1 is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of U0 #), the ResultSort of S1 * the Sorts of U0

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * the Sorts of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict MSAlgebra over S1

B is order-sorted MSSubAlgebra of U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is non-empty order-sorted MSAlgebra over S1

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set

the carrier of S1 is non empty set

the Charact of U0 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of U0 #), the ResultSort of S1 * the Sorts of U0

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ( the Sorts of U0 #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is strict non-empty MSAlgebra over S1

B is strict order-sorted MSSubAlgebra of U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

the carrier' of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is MSAlgebra over S1

the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Charact of B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ( the Sorts of B #), the ResultSort of S1 * the Sorts of B

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

the Sorts of B # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ( the Sorts of B #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * the Sorts of B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

Opers (U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * (B #), the ResultSort of S1 * B

B # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * (B #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 * B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

Opers (U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * (B #), the ResultSort of S1 * B

B # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * (B #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 * B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is Element of the carrier of S1

{ (Constants (U0,b

union { (Constants (U0,b

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of U0 . B is set

K10(( the Sorts of U0 . B)) is non empty set

L is set

G1 is Element of the carrier of S1

Constants (U0,G1) is Element of K10(( the Sorts of U0 . G1))

the Sorts of U0 . G1 is set

K10(( the Sorts of U0 . G1)) is non empty set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is Element of the carrier of S1

Constants (U0,B) is Element of K10(( the Sorts of U0 . B))

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of U0 . B is set

K10(( the Sorts of U0 . B)) is non empty set

(S1,U0,B) is Element of K10(( the Sorts of U0 . B))

{ (Constants (U0,b

union { (Constants (U0,b

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

{ (U0 . b

union { (U0 . b

B is Relation-like Function-like set

dom B is set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

G1 is Element of the carrier of S1

a is Element of the carrier of S1

L . G1 is set

L . a is set

a1 is set

{ (U0 . b

union { (U0 . b

a2 is set

a2 is Element of the carrier of S1

U0 . a2 is set

{ (U0 . b

union { (U0 . b

G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

a is Element of the carrier of S1

G1 . a is set

{ (U0 . b

union { (U0 . b

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

L is set

B . L is set

B . L is set

G1 is Element of the carrier of S1

{ (U0 . b

union { (U0 . b

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

B is set

U0 . B is set

(S1,U0) . B is set

B is Element of the carrier of S1

U0 . B is set

{ (U0 . b

union { (U0 . b

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

B is set

(S1,U0) . B is set

B . B is set

G1 is set

L is Element of the carrier of S1

(S1,U0) . L is set

{ (U0 . b

union { (U0 . b

a is set

a1 is Element of the carrier of S1

U0 . a1 is set

B . a1 is set

B . L is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

{ (Constants (U0,b

union { (Constants (U0,b

B is Relation-like Function-like set

dom B is set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is set

B . L is set

the Sorts of U0 . L is set

G1 is Element of the carrier of S1

B . G1 is set

(S1,U0,G1) is Element of K10(( the Sorts of U0 . G1))

the Sorts of U0 . G1 is set

K10(( the Sorts of U0 . G1)) is non empty set

{ (Constants (U0,b

union { (Constants (U0,b

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

a is Element of the carrier of S1

a1 is Element of the carrier of S1

G1 . a is set

G1 . a1 is set

a2 is set

{ (Constants (U0,b

union { (Constants (U0,b

a2 is set

C1 is Element of the carrier of S1

Constants (U0,C1) is Element of K10(( the Sorts of U0 . C1))

the Sorts of U0 . C1 is set

K10(( the Sorts of U0 . C1)) is non empty set

{ (Constants (U0,b

union { (Constants (U0,b

a is Element of the carrier of S1

L . a is set

(S1,U0,a) is Element of K10(( the Sorts of U0 . a))

the Sorts of U0 . a is set

K10(( the Sorts of U0 . a)) is non empty set

{ (Constants (U0,b

union { (Constants (U0,b

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

L is set

B . L is set

B . L is set

G1 is Element of the carrier of S1

B . G1 is set

(S1,U0,G1) is Element of K10(( the Sorts of U0 . G1))

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of U0 . G1 is set

K10(( the Sorts of U0 . G1)) is non empty set

{ (Constants (U0,b

union { (Constants (U0,b

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is set

(Constants U0) . B is set

(S1,U0) . B is set

B is Element of the carrier of S1

(Constants U0) . B is set

Constants (U0,B) is Element of K10(( the Sorts of U0 . B))

the Sorts of U0 . B is set

K10(( the Sorts of U0 . B)) is non empty set

(S1,U0) . B is set

(S1,U0,B) is Element of K10(( the Sorts of U0 . B))

{ (Constants (U0,b

union { (Constants (U0,b

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is set

(S1,U0) . B is set

B . B is set

G1 is set

L is Element of the carrier of S1

(S1,U0) . L is set

(S1,U0,L) is Element of K10(( the Sorts of U0 . L))

the Sorts of U0 . L is set

K10(( the Sorts of U0 . L)) is non empty set

{ (Constants (U0,b

union { (Constants (U0,b

a is set

a1 is Element of the carrier of S1

Constants (U0,a1) is Element of K10(( the Sorts of U0 . a1))

the Sorts of U0 . a1 is set

K10(( the Sorts of U0 . a1)) is non empty set

(Constants U0) . a1 is set

B . a1 is set

B . L is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

(S1,(Constants U0)) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

B is set

L is Element of the carrier of S1

{ ((Constants U0) . b

{ (Constants (U0,b

a1 is set

a2 is Element of the carrier of S1

(Constants U0) . a2 is set

Constants (U0,a2) is Element of K10(( the Sorts of U0 . a2))

the Sorts of U0 . a2 is set

K10(( the Sorts of U0 . a2)) is non empty set

a2 is Element of the carrier of S1

Constants (U0,a2) is Element of K10(( the Sorts of U0 . a2))

the Sorts of U0 . a2 is set

K10(( the Sorts of U0 . a2)) is non empty set

(Constants U0) . a2 is set

(S1,U0) . L is set

(S1,U0,L) is Element of K10(( the Sorts of U0 . L))

the Sorts of U0 . L is set

K10(( the Sorts of U0 . L)) is non empty set

union { (Constants (U0,b

(S1,(Constants U0)) . L is set

(S1,U0) . B is set

(S1,(Constants U0)) . B is set

B is set

(S1,(Constants U0)) . B is set

(S1,U0) . B is set

B is set

(S1,U0) . B is set

(S1,(Constants U0)) . B is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is order-sorted MSSubAlgebra of U0

the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is set

(S1,U0) . B is set

the Sorts of B . B is set

Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

G1 is Element of the carrier of S1

(Constants U0) . G1 is set

a is Element of the carrier of S1

the Sorts of B . a is set

the Sorts of B . G1 is set

L is Element of the carrier of S1

{ (Constants (U0,b

the Sorts of B . L is set

G1 is set

a is Element of the carrier of S1

Constants (U0,a) is Element of K10(( the Sorts of U0 . a))

the Sorts of U0 . a is set

K10(( the Sorts of U0 . a)) is non empty set

(Constants U0) . a is set

(S1,U0,L) is Element of K10(( the Sorts of U0 . L))

the Sorts of U0 . L is set

K10(( the Sorts of U0 . L)) is non empty set

union { (Constants (U0,b

S1 is non empty non void V52() all-with_const_op V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is non-empty order-sorted MSAlgebra over S1

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is non-empty order-sorted MSSubAlgebra of U0

Constants U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set

S1 is set

U0 is Relation-like S1 -defined Function-like V17(S1) set

bool U0 is Relation-like S1 -defined Function-like V17(S1) set

product (bool U0) is set

B is set

dom (bool U0) is set

B is Relation-like S1 -defined Function-like V17(S1) ManySortedSubset of U0

L is set

B . L is set

(bool U0) . L is set

U0 . L is set

bool (U0 . L) is non empty Element of K10(K10((U0 . L)))

K10((U0 . L)) is non empty set

K10(K10((U0 . L))) is non empty set

dom B is set

B is Relation-like Function-like set

dom B is set

L is Relation-like S1 -defined Function-like V17(S1) set

G1 is set

L . G1 is set

U0 . G1 is set

(bool U0) . G1 is set

bool (U0 . G1) is non empty Element of K10(K10((U0 . G1)))

K10((U0 . G1)) is non empty set

K10(K10((U0 . G1))) is non empty set

S1 is non empty V99() V100() V101() RelStr

the carrier of S1 is non empty set

U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

bool U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

product (bool U0) is set

B is set

L is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

SubSort B is non empty set

{ b

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is set

SubSort B is non empty set

{ b

B is set

L is Element of SubSort B

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is set

SubSort B is non empty set

{ b

B is Element of SubSort B

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is set

SubSort B is non empty set

{ b

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is order-sorted MSAlgebra over S1

SubSort U0 is non empty set

the carrier of S1 is non empty set

{ b

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

(S1,U0) is set

SubSort U0 is non empty set

{ b

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

B is set

L is Element of SubSort B

G1 is Element of SubSort U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is order-sorted MSAlgebra over S1

(S1,U0) is set

SubSort U0 is non empty set

the carrier of S1 is non empty set

{ b

the non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0, the non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)) is non empty set

SubSort the non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0) is non empty set

{ b

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is order-sorted MSAlgebra over S1

(S1,U0) is non empty set

SubSort U0 is non empty set

the carrier of S1 is non empty set

{ b

B is Element of (S1,U0)

B is Element of SubSort U0

@ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is Element of SubSort B

L is Element of SubSort B

Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

(S1,U0) is non empty set

SubSort U0 is non empty set

{ b

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is Element of SubSort U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

B is Element of the carrier of S1

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

Union the Sorts of U0 is set

bool (Union the Sorts of U0) is non empty Element of K10(K10((Union the Sorts of U0)))

K10((Union the Sorts of U0)) is non empty set

K10(K10((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 K10(K10((union (rng the Sorts of U0))))

K10((union (rng the Sorts of U0))) is non empty set

K10(K10((union (rng the Sorts of U0)))) is non empty set

dom the Sorts of U0 is non empty set

the Sorts of U0 . B is set

a is set

a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

a1 . B is set

a is set

a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

a1 is set

a2 . B is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is Element of the carrier of S1

L is Element of the carrier of S1

(S1,U0,B,B) is set

(S1,U0,B,L) is set

G1 is set

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

a . L is set

a . B is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is Element of the carrier of S1

(S1,U0,B,B) is set

SubSort (B,B) is non empty set

L is set

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

G1 . B is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is Element of the carrier of S1

the Sorts of U0 . B is set

(S1,U0,B,B) is set

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

L . B is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is Element of the carrier of S1

(S1,U0,B,B) is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is Relation-like Function-like set

dom B is set

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

a is set

L . a is set

the Sorts of U0 . a is set

a1 is Element of the carrier of S1

L . a1 is set

(S1,U0,B,a1) is non empty set

meet (S1,U0,B,a1) is set

G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

the Sorts of U0 . a1 is set

G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

a1 is Element of the carrier of S1

a2 is Element of the carrier of S1

a . a1 is set

a . a2 is set

(S1,U0,B,a1) is non empty set

meet (S1,U0,B,a1) is set

(S1,U0,B,a2) is non empty set

meet (S1,U0,B,a2) is set

a1 is Element of the carrier of S1

G1 . a1 is set

(S1,U0,B,a1) is non empty set

meet (S1,U0,B,a1) is set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

G1 is set

B . G1 is set

L . G1 is set

a is Element of the carrier of S1

B . a is set

(S1,U0,B,a) is non empty set

meet (S1,U0,B,a) is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

(S1,U0) is non empty set

SubSort U0 is non empty set

{ b

the Element of (S1,U0) is Element of (S1,U0)

B is Element of SubSort U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0) \/ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is set

((S1,U0) \/ B) . B is set

(S1,U0,B) . B is set

L is Element of the carrier of S1

(S1,U0,B,L) is non empty set

((S1,U0) \/ B) . L is set

G1 is set

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

a . L is set

(S1,U0,B) . L is set

meet (S1,U0,B,L) is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0) \/ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is set

L is Element of the carrier of S1

(S1,U0,B,L) is non empty set

((S1,U0) \/ B) . L is set

G1 is set

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

a . L is set

meet (S1,U0,B,L) is set

(S1,U0,B) . B is set

G1 is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier' of S1 is non empty set

the carrier of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

U0 is order-sorted MSAlgebra over S1

B is Element of the carrier' of S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the Arity of S1 * ((S1,U0,B) #)) . B is set

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

L # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * (L #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the Arity of S1 * (L #)) . B is set

G1 is set

(S1,U0,B) . G1 is set

L . G1 is set

a is Element of the carrier of S1

(S1,U0,B) . a is set

(S1,U0,B,a) is non empty set

meet (S1,U0,B,a) is set

L . a is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier' of S1 is non empty set

the carrier of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

U0 is order-sorted MSAlgebra over S1

B is Element of the carrier' of S1

Den (B,U0) is Relation-like Args (B,U0) -defined Result (B,U0) -valued Function-like V21( Args (B,U0), Result (B,U0)) Element of K10(K11((Args (B,U0)),(Result (B,U0))))

Args (B,U0) is Element of rng ( the Sorts of U0 #)

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

rng ( the Sorts of U0 #) is non empty set

Result (B,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

K11((Args (B,U0)),(Result (B,U0))) is Relation-like set

K10(K11((Args (B,U0)),(Result (B,U0)))) is non empty set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the Arity of S1 * ((S1,U0,B) #)) . B is set

(Den (B,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . B) is Relation-like ( the Arity of S1 * ((S1,U0,B) #)) . B -defined Args (B,U0) -defined Result (B,U0) -valued Function-like set

rng ((Den (B,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . B)) is set

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

the ResultSort of S1 * L is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the ResultSort of S1 * L) . B is set

L # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * (L #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the Arity of S1 * (L #)) . B is set

(Den (B,U0)) | (( the Arity of S1 * (L #)) . B) is Relation-like ( the Arity of S1 * (L #)) . B -defined Args (B,U0) -defined Result (B,U0) -valued Function-like set

rng ((Den (B,U0)) | (( the Arity of S1 * (L #)) . B)) is set

(( the Arity of S1 * (L #)) . B) /\ (( the Arity of S1 * ((S1,U0,B) #)) . B) is set

((Den (B,U0)) | (( the Arity of S1 * (L #)) . B)) | (( the Arity of S1 * ((S1,U0,B) #)) . B) is Relation-like ( the Arity of S1 * ((S1,U0,B) #)) . B -defined Args (B,U0) -defined Result (B,U0) -valued Function-like set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier' of S1 is non empty set

the carrier of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

U0 is order-sorted MSAlgebra over S1

B is Element of the carrier' of S1

Den (B,U0) is Relation-like Args (B,U0) -defined Result (B,U0) -valued Function-like V21( Args (B,U0), Result (B,U0)) Element of K10(K11((Args (B,U0)),(Result (B,U0))))

Args (B,U0) is Element of rng ( the Sorts of U0 #)

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

rng ( the Sorts of U0 #) is non empty set

Result (B,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

K11((Args (B,U0)),(Result (B,U0))) is Relation-like set

K10(K11((Args (B,U0)),(Result (B,U0)))) is non empty set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the Arity of S1 * ((S1,U0,B) #)) . B is set

(Den (B,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . B) is Relation-like ( the Arity of S1 * ((S1,U0,B) #)) . B -defined Args (B,U0) -defined Result (B,U0) -valued Function-like set

rng ((Den (B,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . B)) is set

the ResultSort of S1 * (S1,U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the ResultSort of S1 * (S1,U0,B)) . B is set

L is set

the_result_sort_of B is Element of the carrier of S1

the ResultSort of S1 . B is set

dom the ResultSort of S1 is set

(S1,U0,B) . (the_result_sort_of B) is set

(S1,U0,B,(the_result_sort_of B)) is non empty set

meet (S1,U0,B,(the_result_sort_of B)) is set

a is set

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

a1 . (the_result_sort_of B) is set

the ResultSort of S1 * a1 is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the ResultSort of S1 * a1) . B is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

the carrier' of S1 is non empty set

B is Element of the carrier' of S1

L is Element of the carrier' of S1

Den (L,U0) is Relation-like Args (L,U0) -defined Result (L,U0) -valued Function-like V21( Args (L,U0), Result (L,U0)) Element of K10(K11((Args (L,U0)),(Result (L,U0))))

Args (L,U0) is Element of rng ( the Sorts of U0 #)

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of U0 # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

rng ( the Sorts of U0 #) is non empty set

Result (L,U0) is Element of rng the Sorts of U0

rng the Sorts of U0 is non empty set

K11((Args (L,U0)),(Result (L,U0))) is Relation-like set

K10(K11((Args (L,U0)),(Result (L,U0)))) is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the Arity of S1 * ((S1,U0,B) #)) . L is set

(Den (L,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . L) is Relation-like ( the Arity of S1 * ((S1,U0,B) #)) . L -defined Args (L,U0) -defined Result (L,U0) -valued Function-like set

rng ((Den (L,U0)) | (( the Arity of S1 * ((S1,U0,B) #)) . L)) is set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * (S1,U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

( the ResultSort of S1 * (S1,U0,B)) . L is set

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0) \/ B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is order-sorted MSAlgebra over S1

the carrier of S1 is non empty set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed (S1,U0)

U0 | B is strict MSSubAlgebra of U0

Opers (U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * (B #), the ResultSort of S1 * B

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

B # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * (B #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * B is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

MSAlgebra(# B,(Opers (U0,B)) #) is strict MSAlgebra over S1

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is order-sorted MSAlgebra over S1

B is order-sorted MSSubAlgebra of U0

B is order-sorted MSSubAlgebra of U0

B /\ B is strict MSSubAlgebra of U0

the carrier of S1 is non empty set

the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

L /\ G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of (B /\ B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed (S1,U0)

U0 | (S1,U0,B) is strict order-sorted MSSubAlgebra of U0

L is strict order-sorted MSSubAlgebra of U0

Opers (U0,(S1,U0,B)) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ((S1,U0,B) #), the ResultSort of S1 * (S1,U0,B)

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * (S1,U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

MSAlgebra(# (S1,U0,B),(Opers (U0,(S1,U0,B))) #) is strict MSAlgebra over S1

the Sorts of L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

G1 is order-sorted MSSubAlgebra of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

a2 is set

the Sorts of L . a2 is set

the Sorts of G1 . a2 is set

a2 is Element of the carrier of S1

the Sorts of L . a2 is set

(S1,U0,B,a2) is non empty set

meet (S1,U0,B,a2) is set

a1 . a2 is set

B is strict order-sorted MSSubAlgebra of U0

L is strict order-sorted MSSubAlgebra of U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is strict order-sorted MSSubAlgebra of U0

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed (S1,U0)

U0 | (S1,U0,B) is strict order-sorted MSSubAlgebra of U0

the Sorts of (S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is strict order-sorted MSSubAlgebra of U0

Opers (U0,(S1,U0,B)) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ((S1,U0,B) #), the ResultSort of S1 * (S1,U0,B)

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

(S1,U0,B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ((S1,U0,B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * (S1,U0,B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

MSAlgebra(# (S1,U0,B),(Opers (U0,(S1,U0,B))) #) is strict MSAlgebra over S1

the Sorts of L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

G1 is order-sorted MSSubAlgebra of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is non empty set

SubSort B is non empty set

{ b

a2 is set

the Sorts of L . a2 is set

the Sorts of G1 . a2 is set

a2 is Element of the carrier of S1

the Sorts of L . a2 is set

(S1,U0,B,a2) is non empty set

meet (S1,U0,B,a2) is set

a1 . a2 is set

S1 is non empty non void V52() ManySortedSign

the carrier of S1 is non empty set

U0 is MSAlgebra over S1

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

GenMSAlg B is strict MSSubAlgebra of U0

MSSubSort B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

U0 | (MSSubSort B) is strict MSSubAlgebra of U0

the Sorts of (GenMSAlg B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is strict MSSubAlgebra of U0

Opers (U0,(MSSubSort B)) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) V75() ManySortedFunction of the Arity of S1 * ((MSSubSort B) #), the ResultSort of S1 * (MSSubSort B)

the carrier' of S1 is non empty set

the Arity of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 * -valued Function-like V21( the carrier' of S1, the carrier of S1 * ) Element of K10(K11( the carrier' of S1,( the carrier of S1 *)))

the carrier of S1 * is non empty functional V81() M12( the carrier of S1)

K11( the carrier' of S1,( the carrier of S1 *)) is non empty Relation-like set

K10(K11( the carrier' of S1,( the carrier of S1 *))) is non empty set

(MSSubSort B) # is non empty Relation-like the carrier of S1 * -defined Function-like V17( the carrier of S1 * ) set

the Arity of S1 * ((MSSubSort B) #) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

the ResultSort of S1 is Relation-like the carrier' of S1 -defined the carrier of S1 -valued Function-like V21( the carrier' of S1, the carrier of S1) Element of K10(K11( the carrier' of S1, the carrier of S1))

K11( the carrier' of S1, the carrier of S1) is non empty Relation-like set

K10(K11( the carrier' of S1, the carrier of S1)) is non empty set

the ResultSort of S1 * (MSSubSort B) is non empty Relation-like the carrier' of S1 -defined Function-like V17( the carrier' of S1) set

MSAlgebra(# (MSSubSort B),(Opers (U0,(MSSubSort B))) #) is strict MSAlgebra over S1

the Sorts of L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

G1 is MSSubAlgebra of U0

the Sorts of G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

Constants U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

SubSort B 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 S1

the Sorts of L . a2 is set

SubSort (B,a2) is non empty set

meet (SubSort (B,a2)) is set

a . a2 is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

GenMSAlg B is strict MSSubAlgebra of U0

the Sorts of (GenMSAlg B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

(S1,U0,B) is strict order-sorted MSSubAlgebra of U0

the Sorts of (S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

G1 is set

the Sorts of (GenMSAlg B) . G1 is set

the Sorts of (S1,U0,B) . G1 is set

MSSubSort B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

a is Element of the carrier of S1

the Sorts of (GenMSAlg B) . a is set

SubSort (B,a) is non empty set

meet (SubSort (B,a)) is set

(S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed (S1,U0)

the Sorts of (S1,U0,B) . a is set

(S1,U0,B,a) is non empty set

meet (S1,U0,B,a) is set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

GenMSAlg B is strict MSSubAlgebra of U0

(S1,U0,B) is strict order-sorted MSSubAlgebra of U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is strict order-sorted MSAlgebra over S1

the Sorts of U0 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is strict order-sorted MSSubAlgebra of U0

GenMSAlg B is strict MSSubAlgebra of U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is order-sorted MSAlgebra over S1

B is strict order-sorted MSSubAlgebra of U0

the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,B) is strict order-sorted MSSubAlgebra of U0

the Sorts of (S1,U0,B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is non-empty order-sorted MSAlgebra over S1

(S1,U0) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

the carrier of S1 is non empty set

(S1,U0,(S1,U0)) is strict order-sorted MSSubAlgebra of U0

B is order-sorted MSSubAlgebra of U0

(S1,U0,(S1,U0)) /\ B is strict order-sorted MSSubAlgebra of U0

the Sorts of (S1,U0,(S1,U0)) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of ((S1,U0,(S1,U0)) /\ B) is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of (S1,U0,(S1,U0)) /\ the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

U0 is non-empty order-sorted MSAlgebra over S1

the carrier of S1 is non empty set

B is order-sorted MSSubAlgebra of U0

the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

B is order-sorted MSSubAlgebra of U0

the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of B \/ the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set

G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

a is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

a \/ a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,a2) is strict order-sorted MSSubAlgebra of U0

a2 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,a2) is strict order-sorted MSSubAlgebra of U0

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set

a2 is strict order-sorted MSSubAlgebra of U0

a2 is strict order-sorted MSSubAlgebra of U0

a1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) ManySortedSubset of the Sorts of U0

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) order-sorted set

L \/ G1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

C1 is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

(S1,U0,C1) is strict order-sorted MSSubAlgebra of U0

S1 is non empty non void V52() V99() V100() V101() order-sorted discernable OverloadedRSSign

the carrier of S1 is non empty set

U0 is non-empty order-sorted MSAlgebra over S1

B is order-sorted MSSubAlgebra of U0

the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

L is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) (S1,U0)

B \/ the Sorts of B is non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) set

(S1,U0,B) is strict order-sorted MSSubAlgebra of U0

(S1,U0,(S1,U0,B),B) is strict order-sorted MSSubAlgebra of U0

(S1,U0,L) is strict order-sorted MSSubAlgebra of U0

the Sorts of U0 is non empty Relation-like non-empty non empty-yielding the carrier of S1 -defined Function-like V17( the carrier of S1) set

the Sorts of (S1,U0,B) is non empty Relation-like the carrier of S1