:: MSUALG_5 semantic presentation

REAL is set
NAT is non empty V27() V28() V29() V50() V55() V56() Element of bool REAL
bool REAL is non empty set
COMPLEX is set
NAT is non empty V27() V28() V29() V50() V55() V56() set
bool NAT is non empty V50() set
[:NAT,NAT:] is Relation-like non empty V50() set
[:[:NAT,NAT:],NAT:] is Relation-like non empty V50() set
bool [:[:NAT,NAT:],NAT:] is non empty V50() set
Nat_Lattice is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of Nat_Lattice is non empty set
bool NAT is non empty V50() set
NATPLUS is non empty Element of bool NAT
[:NATPLUS,NATPLUS:] is Relation-like non empty set
[:[:NATPLUS,NATPLUS:],NATPLUS:] is Relation-like non empty set
bool [:[:NATPLUS,NATPLUS:],NATPLUS:] is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non negative V27() V28() V29() V31() V32() V33() V34() V35() reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive V50() V55() V57( {} ) FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
2 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
3 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg 1 is non empty trivial V50() V57(1) Element of bool NAT
{1} is non empty trivial V57(1) set
Seg 2 is non empty V50() V57(2) Element of bool NAT
{1,2} is non empty set
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non negative V27() V28() V29() V31() V32() V33() V34() V35() reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive V50() V55() V57( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
X is Relation-like Element of bool [:x,x:]
K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
X is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
X "\/" K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
X \/ K is Relation-like reflexive symmetric Element of bool [:x,x:]
(x,(X \/ K)) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
X is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
(x,X) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
x is set
[:x,x:] is Relation-like set
bool [:x,x:] is non empty set
{ b₁ where b₁ is Relation-like Element of bool [:x,x:] : b₁ is Relation-like total reflexive symmetric transitive Element of bool [:x,x:] } is set
id x is Relation-like x -defined x -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:x,x:]
K is non empty set
K is Element of K
a is Element of K
K \/ a is set
i is Relation-like Element of bool [:x,x:]
i9 is Relation-like Element of bool [:x,x:]
K9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K9 \/ a9 is Relation-like reflexive symmetric Element of bool [:x,x:]
i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i9 is Element of K
K2 is Element of K
y9 is Relation-like Element of bool [:x,x:]
a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
[:K,K:] is Relation-like non empty set
[:[:K,K:],K:] is Relation-like non empty set
bool [:[:K,K:],K:] is non empty set
K is Relation-like Function-like V18([:K,K:],K) Element of bool [:[:K,K:],K:]
a is Element of K
K9 is Element of K
a /\ K9 is set
i9 is Relation-like Element of bool [:x,x:]
K2 is Relation-like Element of bool [:x,x:]
a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a9 /\ i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K2 is Element of K
a is Relation-like Function-like V18([:K,K:],K) Element of bool [:[:K,K:],K:]
LattStr(# K,K,a #) is non empty strict LattStr
i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i9 is Element of K
K2 is Element of K
K . (i9,K2) is Element of K
[i9,K2] is set
K . [i9,K2] is set
a2 is Element of K
n is Relation-like Element of bool [:x,x:]
i9 \/ K2 is set
n is Element of K
a9 \/ i is Relation-like reflexive symmetric Element of bool [:x,x:]
n is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
L is Element of K
K . (a9,i) is set
[a9,i] is set
K . [a9,i] is set
y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a9 "\/" i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i is Element of K
i9 is Element of K
a9 is Element of K
n is Relation-like Element of bool [:x,x:]
L is Relation-like Element of bool [:x,x:]
L is Relation-like Element of bool [:x,x:]
K . (i,i9) is Element of K
[i,i9] is set
K . [i,i9] is set
K . (a9,(K . (i,i9))) is Element of K
[a9,(K . (i,i9))] is set
K . [a9,(K . (i,i9))] is set
a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a2 "\/" y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K . (a9,(a2 "\/" y9)) is set
[a9,(a2 "\/" y9)] is set
K . [a9,(a2 "\/" y9)] is set
K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K2 "\/" (a2 "\/" y9) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K2 "\/" a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
(K2 "\/" a2) "\/" y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K . ((K2 "\/" a2),i9) is set
[(K2 "\/" a2),i9] is set
K . [(K2 "\/" a2),i9] is set
K . (a9,i) is Element of K
[a9,i] is set
K . [a9,i] is set
K . ((K . (a9,i)),i9) is Element of K
[(K . (a9,i)),i9] is set
K . [(K . (a9,i)),i9] is set
K9 is non empty LattStr
the carrier of K9 is non empty set
a9 is Element of the carrier of K9
i is Element of the carrier of K9
i9 is Element of the carrier of K9
i "\/" i9 is Element of the carrier of K9
a9 "\/" (i "\/" i9) is Element of the carrier of K9
a9 "\/" i is Element of the carrier of K9
(a9 "\/" i) "\/" i9 is Element of the carrier of K9
the L_join of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]
[: the carrier of K9, the carrier of K9:] is Relation-like non empty set
[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set
bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is non empty set
the L_join of K9 . (a9,i) is Element of the carrier of K9
[a9,i] is set
the L_join of K9 . [a9,i] is set
the L_join of K9 . (a9,(i "\/" i9)) is Element of the carrier of K9
[a9,(i "\/" i9)] is set
the L_join of K9 . [a9,(i "\/" i9)] is set
K2 is Element of K
a2 is Element of K
y9 is Element of K
K . (a2,y9) is Element of K
[a2,y9] is set
K . [a2,y9] is set
K . (K2,(K . (a2,y9))) is Element of K
[K2,(K . (a2,y9))] is set
K . [K2,(K . (a2,y9))] is set
the L_join of K9 . (( the L_join of K9 . (a9,i)),i9) is Element of the carrier of K9
[( the L_join of K9 . (a9,i)),i9] is set
the L_join of K9 . [( the L_join of K9 . (a9,i)),i9] is set
i is Element of K
a9 is Element of K
a2 is Relation-like Element of bool [:x,x:]
y9 is Relation-like Element of bool [:x,x:]
K . (a9,i) is Element of K
[a9,i] is set
K . [a9,i] is set
K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K2 "\/" i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K . (i,a9) is Element of K
[i,a9] is set
K . [i,a9] is set
a9 is Element of the carrier of K9
i is Element of the carrier of K9
a9 "\/" i is Element of the carrier of K9
i "\/" a9 is Element of the carrier of K9
i9 is Element of K
K2 is Element of K
K . (i9,K2) is Element of K
[i9,K2] is set
K . [i9,K2] is set
the L_join of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]
[: the carrier of K9, the carrier of K9:] is Relation-like non empty set
[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set
bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is non empty set
the L_join of K9 . (i,a9) is Element of the carrier of K9
[i,a9] is set
the L_join of K9 . [i,a9] is set
i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i9 is Element of K
K2 is Element of K
a . (i9,K2) is Element of K
[i9,K2] is set
a . [i9,K2] is set
i9 /\ K2 is set
a . (a9,i) is set
[a9,i] is set
a . [a9,i] is set
a9 /\ i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i is Element of K
i9 is Element of K
a9 is Element of K
n is Relation-like Element of bool [:x,x:]
L is Relation-like Element of bool [:x,x:]
L is Relation-like Element of bool [:x,x:]
a . (i,i9) is Element of K
[i,i9] is set
a . [i,i9] is set
a . (a9,(a . (i,i9))) is Element of K
[a9,(a . (i,i9))] is set
a . [a9,(a . (i,i9))] is set
a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a2 /\ y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a . (a9,(a2 /\ y9)) is set
[a9,(a2 /\ y9)] is set
a . [a9,(a2 /\ y9)] is set
K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K2 /\ (a2 /\ y9) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K2 /\ a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
(K2 /\ a2) /\ y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a . ((K2 /\ a2),i9) is set
[(K2 /\ a2),i9] is set
a . [(K2 /\ a2),i9] is set
a . (a9,i) is Element of K
[a9,i] is set
a . [a9,i] is set
a . ((a . (a9,i)),i9) is Element of K
[(a . (a9,i)),i9] is set
a . [(a . (a9,i)),i9] is set
a9 is Element of the carrier of K9
i is Element of the carrier of K9
i9 is Element of the carrier of K9
i "/\" i9 is Element of the carrier of K9
a9 "/\" (i "/\" i9) is Element of the carrier of K9
a9 "/\" i is Element of the carrier of K9
(a9 "/\" i) "/\" i9 is Element of the carrier of K9
the L_meet of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]
[: the carrier of K9, the carrier of K9:] is Relation-like non empty set
[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set
bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is non empty set
the L_meet of K9 . (a9,i) is Element of the carrier of K9
[a9,i] is set
the L_meet of K9 . [a9,i] is set
the L_meet of K9 . (a9,(i "/\" i9)) is Element of the carrier of K9
[a9,(i "/\" i9)] is set
the L_meet of K9 . [a9,(i "/\" i9)] is set
K2 is Element of K
a2 is Element of K
y9 is Element of K
a . (a2,y9) is Element of K
[a2,y9] is set
a . [a2,y9] is set
a . (K2,(a . (a2,y9))) is Element of K
[K2,(a . (a2,y9))] is set
a . [K2,(a . (a2,y9))] is set
the L_meet of K9 . (( the L_meet of K9 . (a9,i)),i9) is Element of the carrier of K9
[( the L_meet of K9 . (a9,i)),i9] is set
the L_meet of K9 . [( the L_meet of K9 . (a9,i)),i9] is set
a9 is Element of the carrier of K9
i is Element of the carrier of K9
a9 "\/" i is Element of the carrier of K9
a9 "/\" (a9 "\/" i) is Element of the carrier of K9
i9 is Element of K
K2 is Element of K
K . (i9,K2) is Element of K
[i9,K2] is set
K . [i9,K2] is set
a . (i9,(K . (i9,K2))) is Element of K
[i9,(K . (i9,K2))] is set
a . [i9,(K . (i9,K2))] is set
n is Relation-like Element of bool [:x,x:]
L is Relation-like Element of bool [:x,x:]
a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a2 "\/" y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a2 /\ (a2 "\/" y9) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
the L_meet of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]
[: the carrier of K9, the carrier of K9:] is Relation-like non empty set
[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set
bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is non empty set
the L_meet of K9 . (a9,(a9 "\/" i)) is Element of the carrier of K9
[a9,(a9 "\/" i)] is set
the L_meet of K9 . [a9,(a9 "\/" i)] is set
i is Element of K
a9 is Element of K
a2 is Relation-like Element of bool [:x,x:]
y9 is Relation-like Element of bool [:x,x:]
a . (a9,i) is Element of K
[a9,i] is set
a . [a9,i] is set
K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K2 /\ i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a . (i,a9) is Element of K
[i,a9] is set
a . [i,a9] is set
a9 is Element of the carrier of K9
i is Element of the carrier of K9
a9 "/\" i is Element of the carrier of K9
i "/\" a9 is Element of the carrier of K9
i9 is Element of K
K2 is Element of K
a . (i9,K2) is Element of K
[i9,K2] is set
a . [i9,K2] is set
the L_meet of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]
[: the carrier of K9, the carrier of K9:] is Relation-like non empty set
[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set
bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is non empty set
the L_meet of K9 . (i,a9) is Element of the carrier of K9
[i,a9] is set
the L_meet of K9 . [i,a9] is set
a9 is Element of the carrier of K9
i is Element of the carrier of K9
a9 "/\" i is Element of the carrier of K9
(a9 "/\" i) "\/" i is Element of the carrier of K9
i9 is Element of K
K2 is Element of K
a . (i9,K2) is Element of K
[i9,K2] is set
a . [i9,K2] is set
K . ((a . (i9,K2)),K2) is Element of K
[(a . (i9,K2)),K2] is set
K . [(a . (i9,K2)),K2] is set
n is Relation-like Element of bool [:x,x:]
L is Relation-like Element of bool [:x,x:]
a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a2 /\ y9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
y9 "\/" (a2 /\ y9) is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
the L_join of K9 is Relation-like Function-like V18([: the carrier of K9, the carrier of K9:], the carrier of K9) Element of bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:]
[: the carrier of K9, the carrier of K9:] is Relation-like non empty set
[:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is Relation-like non empty set
bool [:[: the carrier of K9, the carrier of K9:], the carrier of K9:] is non empty set
the L_join of K9 . ((a9 "/\" i),i) is Element of the carrier of K9
[(a9 "/\" i),i] is set
the L_join of K9 . [(a9 "/\" i),i] is set
a9 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of a9 is non empty set
the L_meet of a9 is Relation-like Function-like V18([: the carrier of a9, the carrier of a9:], the carrier of a9) Element of bool [:[: the carrier of a9, the carrier of a9:], the carrier of a9:]
[: the carrier of a9, the carrier of a9:] is Relation-like non empty set
[:[: the carrier of a9, the carrier of a9:], the carrier of a9:] is Relation-like non empty set
bool [:[: the carrier of a9, the carrier of a9:], the carrier of a9:] is non empty set
the L_join of a9 is Relation-like Function-like V18([: the carrier of a9, the carrier of a9:], the carrier of a9) Element of bool [:[: the carrier of a9, the carrier of a9:], the carrier of a9:]
i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
the L_meet of a9 . (i,i9) is set
[i,i9] is set
the L_meet of a9 . [i,i9] is set
i /\ i9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
K2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
the L_join of a9 . (K2,a2) is set
[K2,a2] is set
the L_join of a9 . [K2,a2] is set
K2 "\/" a2 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
X is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of X is non empty set
the L_meet of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the L_join of X is Relation-like Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
K is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of K is non empty set
the L_meet of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the L_join of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
K is non empty set
K9 is Element of K
a is Element of K
i9 is Relation-like Element of bool [:x,x:]
K2 is Relation-like Element of bool [:x,x:]
the L_meet of X . (a,K9) is set
[a,K9] is set
the L_meet of X . [a,K9] is set
a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a9 /\ i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
the L_meet of K . (a,K9) is set
the L_meet of K . [a,K9] is set
K9 is Element of K
a is Element of K
i9 is Relation-like Element of bool [:x,x:]
K2 is Relation-like Element of bool [:x,x:]
the L_join of X . (a,K9) is set
[a,K9] is set
the L_join of X . [a,K9] is set
a9 is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
a9 "\/" i is Relation-like total reflexive symmetric transitive Element of bool [:x,x:]
the L_join of K . (a,K9) is set
the L_join of K . [a,K9] is set
x is set
X is Relation-like x -defined Function-like total set
K is Relation-like x -defined Function-like total set
K is set
K . K is set
X . K is set
[:(X . K),(X . K):] is Relation-like set
bool [:(X . K),(X . K):] is non empty set
id (X . K) is Relation-like X . K -defined X . K -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:(X . K),(X . K):]
K is Relation-like x -defined Function-like total V95() ManySortedRelation of X,X
a is set
X . a is set
[:(X . a),(X . a):] is Relation-like set
bool [:(X . a),(X . a):] is non empty set
K . a is set
K9 is Relation-like Element of bool [:(X . a),(X . a):]
id (X . a) is Relation-like X . a -defined X . a -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:(X . a),(X . a):]
x is set
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total set
a is set
K . a is set
X . a is set
[:(X . a),(X . a):] is Relation-like set
bool [:(X . a),(X . a):] is non empty set
K9 is Element of x
X . K9 is set
K . K9 is Relation-like Element of bool [:(X . K9),(X . K9):]
[:(X . K9),(X . K9):] is Relation-like set
bool [:(X . K9),(X . K9):] is non empty set
((X . K9),(K . K9)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . K9),(X . K9):]
a is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
K9 is set
X . K9 is set
[:(X . K9),(X . K9):] is Relation-like set
bool [:(X . K9),(X . K9):] is non empty set
a . K9 is set
a9 is Relation-like Element of bool [:(X . K9),(X . K9):]
i is Element of x
X . i is set
K . i is Relation-like Element of bool [:(X . i),(X . i):]
[:(X . i),(X . i):] is Relation-like set
bool [:(X . i),(X . i):] is non empty set
((X . i),(K . i)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . i),(X . i):]
K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a9 is Element of x
X . a9 is set
K9 . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]
[:(X . a9),(X . a9):] is Relation-like set
bool [:(X . a9),(X . a9):] is non empty set
K . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]
((X . a9),(K . a9)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . a9),(X . a9):]
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K9 is set
K . K9 is set
a9 is Element of x
X . a9 is set
K . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]
[:(X . a9),(X . a9):] is Relation-like set
bool [:(X . a9),(X . a9):] is non empty set
((X . a9),(K . a9)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . a9),(X . a9):]
a . K9 is set
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Element of x
X . K is set
[:(X . K),(X . K):] is Relation-like set
bool [:(X . K),(X . K):] is non empty set
K . K is Relation-like Element of bool [:(X . K),(X . K):]
a is Relation-like total reflexive symmetric transitive Element of bool [:(X . K),(X . K):]
((X . K),a) is Relation-like total reflexive symmetric transitive Element of bool [:(X . K),(X . K):]
((X . K),(K . K)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . K),(X . K):]
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K \/ K is Relation-like x -defined Function-like non empty total set
a is Relation-like x -defined Function-like non empty total set
K9 is set
a . K9 is set
X . K9 is set
[:(X . K9),(X . K9):] is Relation-like set
bool [:(X . K9),(X . K9):] is non empty set
(K \/ K) . K9 is set
a9 is Element of x
X . a9 is set
K . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]
[:(X . a9),(X . a9):] is Relation-like set
bool [:(X . a9),(X . a9):] is non empty set
K . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]
(K . a9) \/ (K . a9) is Relation-like Element of bool [:(X . a9),(X . a9):]
K9 is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
(x,X,K9) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a9 is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,a9) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
i is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,i) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
i is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K9 \/ a9 is Relation-like x -defined Function-like non empty total set
a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,i) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a9 \/ K9 is Relation-like x -defined Function-like non empty total set
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K \/ K is Relation-like x -defined Function-like non empty total set
(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
(x,X,a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K9 is set
a . K9 is set
a9 is Element of x
X . a9 is set
a . a9 is Relation-like Element of bool [:(X . a9),(X . a9):]
[:(X . a9),(X . a9):] is Relation-like set
bool [:(X . a9),(X . a9):] is non empty set
((X . a9),(a . a9)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . a9),(X . a9):]
(x,X,K,K) . K9 is set
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K \/ K is Relation-like x -defined Function-like non empty total set
(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
(x,X,a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a9 is set
i is Element of x
K9 . i is Relation-like Element of bool [:(X . i),(X . i):]
X . i is set
[:(X . i),(X . i):] is Relation-like set
bool [:(X . i),(X . i):] is non empty set
X . a9 is set
[:(X . a9),(X . a9):] is Relation-like set
bool [:(X . a9),(X . a9):] is non empty set
K9 . a9 is set
a . a9 is set
i9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . a9),(X . a9):]
a . i is Relation-like Element of bool [:(X . i),(X . i):]
((X . i),(a . i)) is Relation-like total reflexive symmetric transitive Element of bool [:(X . i),(X . i):]
(x,X,K,K) . a9 is set
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K \/ K is Relation-like x -defined Function-like non empty total set
(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K \/ K is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,(x,X,K,K),a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,K,a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,K,(x,X,K,a)) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K \/ a is Relation-like x -defined Function-like non empty total set
K \/ (x,X,K,a) is Relation-like x -defined Function-like non empty total set
K \/ K is Relation-like x -defined Function-like non empty total set
(x,X,K,K) \/ a is Relation-like x -defined Function-like non empty total set
K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K \/ K is Relation-like x -defined Function-like non empty total set
(x,X,K,K) \/ a is Relation-like x -defined Function-like non empty total set
K \/ a is Relation-like x -defined Function-like non empty total set
K \/ (x,X,K,a) is Relation-like x -defined Function-like non empty total set
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,K,K) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K /\ (x,X,K,K) is Relation-like x -defined Function-like non empty total set
K \/ K is Relation-like x -defined Function-like non empty total set
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K /\ K is Relation-like x -defined Function-like non empty total set
K \/ (K /\ K) is Relation-like x -defined Function-like non empty total set
a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,K,a) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
x is non empty set
X is Relation-like x -defined Function-like non empty total set
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K /\ K is Relation-like x -defined Function-like non empty total set
a is set
(K /\ K) . a is set
X . a is set
[:(X . a),(X . a):] is Relation-like set
bool [:(X . a),(X . a):] is non empty set
K . a is set
K . a is set
K9 is Relation-like Element of bool [:(X . a),(X . a):]
a9 is Relation-like Element of bool [:(X . a),(X . a):]
K9 /\ a9 is Relation-like Element of bool [:(X . a),(X . a):]
a is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
K9 is set
X . K9 is set
[:(X . K9),(X . K9):] is Relation-like set
bool [:(X . K9),(X . K9):] is non empty set
a . K9 is set
a9 is Relation-like Element of bool [:(X . K9),(X . K9):]
K . K9 is set
i is Relation-like Element of bool [:(X . K9),(X . K9):]
K . K9 is set
K2 is Relation-like Element of bool [:(X . K9),(X . K9):]
a2 is Relation-like total reflexive symmetric transitive Element of bool [:(X . K9),(X . K9):]
i9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . K9),(X . K9):]
a2 /\ i9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . K9),(X . K9):]
x is non empty set
X is Relation-like x -defined Function-like non empty total set
the Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is Relation-like x -defined Function-like non empty total set
product K is set
a is set
K9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
dom K is non empty Element of bool x
bool x is non empty set
a9 is set
K9 . a9 is set
K . a9 is set
i is Element of x
K9 . i is Relation-like Element of bool [:(X . i),(X . i):]
X . i is set
[:(X . i),(X . i):] is Relation-like set
bool [:(X . i),(X . i):] is non empty set
K . i is set
dom K9 is non empty Element of bool x
K9 is non empty set
a9 is Element of K9
i is Element of K9
i9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,i9,K2) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
y9 is Element of K9
n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
n \/ L is Relation-like x -defined Function-like non empty total set
[:K9,K9:] is Relation-like non empty set
[:[:K9,K9:],K9:] is Relation-like non empty set
bool [:[:K9,K9:],K9:] is non empty set
a9 is Relation-like Function-like V18([:K9,K9:],K9) Element of bool [:[:K9,K9:],K9:]
i is Element of K9
i9 is Element of K9
K2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K2 /\ a2 is Relation-like x -defined Function-like non empty total set
n is set
(K2 /\ a2) . n is set
X . n is set
[:(X . n),(X . n):] is Relation-like set
bool [:(X . n),(X . n):] is non empty set
L is Element of x
X . L is set
K2 . L is Relation-like Element of bool [:(X . L),(X . L):]
[:(X . L),(X . L):] is Relation-like set
bool [:(X . L),(X . L):] is non empty set
a2 . L is Relation-like Element of bool [:(X . L),(X . L):]
(K2 . L) /\ (a2 . L) is Relation-like Element of bool [:(X . L),(X . L):]
n is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
L is set
X . L is set
[:(X . L),(X . L):] is Relation-like set
bool [:(X . L),(X . L):] is non empty set
n . L is set
L is Relation-like Element of bool [:(X . L),(X . L):]
L is Element of x
K2 . L is Relation-like Element of bool [:(X . L),(X . L):]
X . L is set
[:(X . L),(X . L):] is Relation-like set
bool [:(X . L),(X . L):] is non empty set
a2 . L is Relation-like Element of bool [:(X . L),(X . L):]
c₁₇ is Relation-like Element of bool [:(X . L),(X . L):]
b9 is Relation-like Element of bool [:(X . L),(X . L):]
EQR is Relation-like total reflexive symmetric transitive Element of bool [:(X . L),(X . L):]
c9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . L),(X . L):]
EQR /\ c9 is Relation-like total reflexive symmetric transitive Element of bool [:(X . L),(X . L):]
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L is Element of K9
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
c₁₇ is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L /\ c₁₇ is Relation-like x -defined Function-like non empty total set
i is Relation-like Function-like V18([:K9,K9:],K9) Element of bool [:[:K9,K9:],K9:]
LattStr(# K9,a9,i #) is non empty strict LattStr
a2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K2 \/ a2 is Relation-like x -defined Function-like non empty total set
y9 is Element of K9
n is Element of K9
a9 . (y9,n) is Element of K9
[y9,n] is set
a9 . [y9,n] is set
a9 . (K2,a2) is set
[K2,a2] is set
a9 . [K2,a2] is set
(x,X,K2,a2) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L is Relation-like x -defined Function-like non empty total V95() ManySortedRelation of X,X
(x,X,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K2 is Element of K9
a2 is Element of K9
y9 is Element of K9
a9 . (a2,y9) is Element of K9
[a2,y9] is set
a9 . [a2,y9] is set
a9 . (K2,(a9 . (a2,y9))) is Element of K9
[K2,(a9 . (a2,y9))] is set
a9 . [K2,(a9 . (a2,y9))] is set
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,L,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a9 . (K2,(x,X,L,L)) is set
[K2,(x,X,L,L)] is set
a9 . [K2,(x,X,L,L)] is set
n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,n,(x,X,L,L)) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,n,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,(x,X,n,L),L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a9 . ((x,X,n,L),y9) is set
[(x,X,n,L),y9] is set
a9 . [(x,X,n,L),y9] is set
a9 . (K2,a2) is Element of K9
[K2,a2] is set
a9 . [K2,a2] is set
a9 . ((a9 . (K2,a2)),y9) is Element of K9
[(a9 . (K2,a2)),y9] is set
a9 . [(a9 . (K2,a2)),y9] is set
i9 is non empty LattStr
the carrier of i9 is non empty set
K2 is Element of the carrier of i9
a2 is Element of the carrier of i9
y9 is Element of the carrier of i9
a2 "\/" y9 is Element of the carrier of i9
K2 "\/" (a2 "\/" y9) is Element of the carrier of i9
K2 "\/" a2 is Element of the carrier of i9
(K2 "\/" a2) "\/" y9 is Element of the carrier of i9
the L_join of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]
[: the carrier of i9, the carrier of i9:] is Relation-like non empty set
[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set
bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is non empty set
the L_join of i9 . (K2,a2) is Element of the carrier of i9
[K2,a2] is set
the L_join of i9 . [K2,a2] is set
the L_join of i9 . (K2,(a2 "\/" y9)) is Element of the carrier of i9
[K2,(a2 "\/" y9)] is set
the L_join of i9 . [K2,(a2 "\/" y9)] is set
n is Element of K9
L is Element of K9
L is Element of K9
a9 . (L,L) is Element of K9
[L,L] is set
a9 . [L,L] is set
a9 . (n,(a9 . (L,L))) is Element of K9
[n,(a9 . (L,L))] is set
a9 . [n,(a9 . (L,L))] is set
the L_join of i9 . (( the L_join of i9 . (K2,a2)),y9) is Element of the carrier of i9
[( the L_join of i9 . (K2,a2)),y9] is set
the L_join of i9 . [( the L_join of i9 . (K2,a2)),y9] is set
a2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
n is Element of K9
y9 is Element of K9
i . (K2,a2) is set
[K2,a2] is set
i . [K2,a2] is set
K2 /\ a2 is Relation-like x -defined Function-like non empty total set
K2 is Element of K9
a2 is Element of K9
y9 is Element of K9
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L /\ L is Relation-like x -defined Function-like non empty total set
n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
n /\ L is Relation-like x -defined Function-like non empty total set
i . (a2,y9) is Element of K9
[a2,y9] is set
i . [a2,y9] is set
i . (K2,(i . (a2,y9))) is Element of K9
[K2,(i . (a2,y9))] is set
i . [K2,(i . (a2,y9))] is set
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
i . (K2,L) is set
[K2,L] is set
i . [K2,L] is set
n /\ (L /\ L) is Relation-like x -defined Function-like non empty total set
(n /\ L) /\ L is Relation-like x -defined Function-like non empty total set
c₁₇ is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
i . (c₁₇,y9) is set
[c₁₇,y9] is set
i . [c₁₇,y9] is set
i . (K2,a2) is Element of K9
[K2,a2] is set
i . [K2,a2] is set
i . ((i . (K2,a2)),y9) is Element of K9
[(i . (K2,a2)),y9] is set
i . [(i . (K2,a2)),y9] is set
K2 is Element of the carrier of i9
a2 is Element of the carrier of i9
y9 is Element of the carrier of i9
a2 "/\" y9 is Element of the carrier of i9
K2 "/\" (a2 "/\" y9) is Element of the carrier of i9
K2 "/\" a2 is Element of the carrier of i9
(K2 "/\" a2) "/\" y9 is Element of the carrier of i9
the L_meet of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]
[: the carrier of i9, the carrier of i9:] is Relation-like non empty set
[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set
bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is non empty set
the L_meet of i9 . (K2,a2) is Element of the carrier of i9
[K2,a2] is set
the L_meet of i9 . [K2,a2] is set
the L_meet of i9 . (K2,(a2 "/\" y9)) is Element of the carrier of i9
[K2,(a2 "/\" y9)] is set
the L_meet of i9 . [K2,(a2 "/\" y9)] is set
n is Element of K9
L is Element of K9
L is Element of K9
i . (L,L) is Element of K9
[L,L] is set
i . [L,L] is set
i . (n,(i . (L,L))) is Element of K9
[n,(i . (L,L))] is set
i . [n,(i . (L,L))] is set
the L_meet of i9 . (( the L_meet of i9 . (K2,a2)),y9) is Element of the carrier of i9
[( the L_meet of i9 . (K2,a2)),y9] is set
the L_meet of i9 . [( the L_meet of i9 . (K2,a2)),y9] is set
K2 is Element of K9
a2 is Element of K9
a9 . (K2,a2) is Element of K9
[K2,a2] is set
a9 . [K2,a2] is set
y9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,y9,n) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
a9 . (a2,K2) is Element of K9
[a2,K2] is set
a9 . [a2,K2] is set
K2 is Element of the carrier of i9
a2 is Element of the carrier of i9
K2 "\/" a2 is Element of the carrier of i9
a2 "\/" K2 is Element of the carrier of i9
y9 is Element of K9
n is Element of K9
a9 . (y9,n) is Element of K9
[y9,n] is set
a9 . [y9,n] is set
the L_join of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]
[: the carrier of i9, the carrier of i9:] is Relation-like non empty set
[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set
bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is non empty set
the L_join of i9 . (a2,K2) is Element of the carrier of i9
[a2,K2] is set
the L_join of i9 . [a2,K2] is set
K2 is Element of the carrier of i9
a2 is Element of the carrier of i9
K2 "/\" a2 is Element of the carrier of i9
(K2 "/\" a2) "\/" a2 is Element of the carrier of i9
y9 is Element of K9
n is Element of K9
i . (y9,n) is Element of K9
[y9,n] is set
i . [y9,n] is set
a9 . ((i . (y9,n)),n) is Element of K9
[(i . (y9,n)),n] is set
a9 . [(i . (y9,n)),n] is set
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L /\ L is Relation-like x -defined Function-like non empty total set
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,L,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
the L_join of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]
[: the carrier of i9, the carrier of i9:] is Relation-like non empty set
[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set
bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is non empty set
the L_join of i9 . ((K2 "/\" a2),a2) is Element of the carrier of i9
[(K2 "/\" a2),a2] is set
the L_join of i9 . [(K2 "/\" a2),a2] is set
K2 is Element of K9
a2 is Element of K9
i . (K2,a2) is Element of K9
[K2,a2] is set
i . [K2,a2] is set
n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
y9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
n /\ y9 is Relation-like x -defined Function-like non empty total set
i . (a2,K2) is Element of K9
[a2,K2] is set
i . [a2,K2] is set
K2 is Element of the carrier of i9
a2 is Element of the carrier of i9
K2 "/\" a2 is Element of the carrier of i9
a2 "/\" K2 is Element of the carrier of i9
y9 is Element of K9
n is Element of K9
i . (y9,n) is Element of K9
[y9,n] is set
i . [y9,n] is set
the L_meet of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]
[: the carrier of i9, the carrier of i9:] is Relation-like non empty set
[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set
bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is non empty set
the L_meet of i9 . (a2,K2) is Element of the carrier of i9
[a2,K2] is set
the L_meet of i9 . [a2,K2] is set
K2 is Element of the carrier of i9
a2 is Element of the carrier of i9
K2 "\/" a2 is Element of the carrier of i9
K2 "/\" (K2 "\/" a2) is Element of the carrier of i9
y9 is Element of K9
n is Element of K9
a9 . (y9,n) is Element of K9
[y9,n] is set
a9 . [y9,n] is set
i . (y9,(a9 . (y9,n))) is Element of K9
[y9,(a9 . (y9,n))] is set
i . [y9,(a9 . (y9,n))] is set
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
(x,X,L,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L /\ (x,X,L,L) is Relation-like x -defined Function-like non empty total set
the L_meet of i9 is Relation-like Function-like V18([: the carrier of i9, the carrier of i9:], the carrier of i9) Element of bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:]
[: the carrier of i9, the carrier of i9:] is Relation-like non empty set
[:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is Relation-like non empty set
bool [:[: the carrier of i9, the carrier of i9:], the carrier of i9:] is non empty set
the L_meet of i9 . (K2,(K2 "\/" a2)) is Element of the carrier of i9
[K2,(K2 "\/" a2)] is set
the L_meet of i9 . [K2,(K2 "\/" a2)] is set
K2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of K2 is non empty set
the L_meet of K2 is Relation-like Function-like V18([: the carrier of K2, the carrier of K2:], the carrier of K2) Element of bool [:[: the carrier of K2, the carrier of K2:], the carrier of K2:]
[: the carrier of K2, the carrier of K2:] is Relation-like non empty set
[:[: the carrier of K2, the carrier of K2:], the carrier of K2:] is Relation-like non empty set
bool [:[: the carrier of K2, the carrier of K2:], the carrier of K2:] is non empty set
the L_join of K2 is Relation-like Function-like V18([: the carrier of K2, the carrier of K2:], the carrier of K2) Element of bool [:[: the carrier of K2, the carrier of K2:], the carrier of K2:]
a2 is set
a2 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
y9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
the L_meet of K2 . (a2,y9) is set
[a2,y9] is set
the L_meet of K2 . [a2,y9] is set
a2 /\ y9 is Relation-like x -defined Function-like non empty total set
n is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
L is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
the L_join of K2 . (n,L) is set
[n,L] is set
the L_join of K2 . [n,L] is set
(x,X,n,L) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
K is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of K is non empty set
the L_meet of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the L_join of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
K is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of K is non empty set
the L_meet of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
the L_join of K is Relation-like Function-like V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
K9 is set
a is non empty set
K9 is Element of a
a9 is Element of a
the L_meet of K . (K9,a9) is set
[K9,a9] is set
the L_meet of K . [K9,a9] is set
i is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
i9 is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
i /\ i9 is Relation-like x -defined Function-like non empty total set
the L_meet of K . (K9,a9) is set
the L_meet of K . [K9,a9] is set
the L_join of K . (K9,a9) is set
the L_join of K . [K9,a9] is set
(x,X,i,i9) is Relation-like x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of X,X
the L_join of K . (K9,a9) is set
the L_join of K . [K9,a9] is set
x is non empty V71() ManySortedSign
the carrier of x is non empty set
X is MSAlgebra over x
the Sorts of X is Relation-like the carrier of x -defined Function-like non empty total set
K is Relation-like the carrier of x -defined Function-like non empty total V95() ManySortedRelation of the Sorts of X, the Sorts of X
x is non empty non void V71() ManySortedSign
the carrier' of x is non empty set
the carrier of x is non empty set
X is non-empty MSAlgebra over x
the Sorts of X is Relation-like non-empty non empty-yielding the carrier of x -defined Function-like non empty total set
K is Element of the carrier' of x
the_arity_of K is Relation-like NAT -defined the carrier of x -valued Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of x *
the carrier of x * is functional non empty FinSequence-membered M15( the carrier of x)
Args (K,X) is functional non empty Element of rng ( the Sorts of X #)
the Sorts of X # is Relation-like the carrier of x * -defined Function-like non empty total set
rng ( the Sorts of X #) is non empty set
Result (K,X) is non empty Element of rng the Sorts of X
rng the Sorts of X is non empty V38() set
Den (K,X) is Relation-like Function-like V18( Args (K,X), Result (K,X)) Element of bool [:(Args (K,X)),(Result (K,X)):]
[:(Args (K,X)),(Result (K,X)):] is Relation-like non empty set
bool [:(Args (K,X)),(Result (K,X)):] is non empty set
the_result_sort_of K is Element of the carrier of x
the Sorts of X . (the_result_sort_of K) is non empty set
K is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of X, the Sorts of X
a is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of X, the Sorts of X
K . (the_result_sort_of K) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):]
[:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):] is Relation-like non empty set
bool [:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):] is non empty set
a . (the_result_sort_of K) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):]
(K . (the_result_sort_of K)) \/ (a . (the_result_sort_of K)) is Relation-like reflexive symmetric Element of bool [:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):]
K9 is set
a9 is set
[K9,a9] is set
<*K9*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set
<*a9*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set
i is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len i is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len i) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(the_arity_of K) /. ((len i) + 1) is Element of the carrier of x
the Sorts of X . ((the_arity_of K) /. ((len i) + 1)) is non empty set
K . ((the_arity_of K) /. ((len i) + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):]
[:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):] is non empty set
a . ((the_arity_of K) /. ((len i) + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):]
(K . ((the_arity_of K) /. ((len i) + 1))) \/ (a . ((the_arity_of K) /. ((len i) + 1))) is Relation-like reflexive symmetric Element of bool [:( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))),( the Sorts of X . ((the_arity_of K) /. ((len i) + 1))):]
i ^ <*K9*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
i9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
(i ^ <*K9*>) ^ i9 is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
i ^ <*a9*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(i ^ <*a9*>) ^ i9 is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
K2 is Relation-like Function-like Element of Args (K,X)
a2 is Relation-like Function-like Element of Args (K,X)
(Den (K,X)) . K2 is Element of Result (K,X)
(Den (K,X)) . a2 is Element of Result (K,X)
[((Den (K,X)) . K2),((Den (K,X)) . a2)] is set
<*a9*> ^ i9 is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
i ^ (<*a9*> ^ i9) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
<*K9*> ^ i9 is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
i ^ (<*K9*> ^ i9) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
dom K2 is set
y9 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
K2 . y9 is set
a2 . y9 is set
[(K2 . y9),(a2 . y9)] is set
(the_arity_of K) /. y9 is Element of the carrier of x
K . ((the_arity_of K) /. y9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. y9)),( the Sorts of X . ((the_arity_of K) /. y9)):]
the Sorts of X . ((the_arity_of K) /. y9) is non empty set
[:( the Sorts of X . ((the_arity_of K) /. y9)),( the Sorts of X . ((the_arity_of K) /. y9)):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of K) /. y9)),( the Sorts of X . ((the_arity_of K) /. y9)):] is non empty set
dom (the_arity_of K) is Element of bool NAT
(the_arity_of K) * the Sorts of X is Relation-like non-empty NAT -defined dom (the_arity_of K) -defined Function-like total set
dom ((the_arity_of K) * the Sorts of X) is Element of bool NAT
n is non empty set
L is Relation-like non-empty non empty-yielding n -defined Function-like non empty total set
product L is non empty set
pi ((Args (K,X)),y9) is set
the Arity of x is Relation-like Function-like V18( the carrier' of x, the carrier of x * ) Element of bool [: the carrier' of x,( the carrier of x *):]
[: the carrier' of x,( the carrier of x *):] is Relation-like non empty set
bool [: the carrier' of x,( the carrier of x *):] is non empty set
the Arity of x * ( the Sorts of X #) is Relation-like Function-like set
( the Arity of x * ( the Sorts of X #)) . K is set
pi ((( the Arity of x * ( the Sorts of X #)) . K),y9) is set
the Arity of x . K is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of x *
( the Sorts of X #) . ( the Arity of x . K) is set
pi ((( the Sorts of X #) . ( the Arity of x . K)),y9) is set
( the Sorts of X #) . (the_arity_of K) is set
pi ((( the Sorts of X #) . (the_arity_of K)),y9) is set
product ((the_arity_of K) * the Sorts of X) is set
pi ((product ((the_arity_of K) * the Sorts of X)),y9) is set
((the_arity_of K) * the Sorts of X) . y9 is set
(the_arity_of K) . y9 is set
the Sorts of X . ((the_arity_of K) . y9) is set
dom (i ^ <*K9*>) is non empty Element of bool NAT
dom i9 is Element of bool NAT
len (i ^ <*K9