:: 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*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
dom i is Element of bool NAT
i . y9 is set
dom <*K9*> is non empty trivial V57(1) Element of bool NAT
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len i) + L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len i) + L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len i) + 1) is non empty V50() V57((len i) + 1) Element of bool NAT
len <*a9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len i) + (len <*a9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len i) + (len <*a9*>)) is non empty V50() V57((len i) + (len <*a9*>)) Element of bool NAT
len (i ^ <*a9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len (i ^ <*a9*>)) is non empty V50() V57( len (i ^ <*a9*>)) Element of bool NAT
dom (i ^ <*a9*>) is non empty Element of bool NAT
(i ^ <*a9*>) . ((len i) + 1) is set
len <*K9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len i) + (len <*K9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len i) + (len <*K9*>)) is non empty V50() V57((len i) + (len <*K9*>)) Element of bool NAT
Seg (len (i ^ <*K9*>)) is non empty V50() V57( len (i ^ <*K9*>)) Element of bool NAT
(i ^ <*K9*>) . ((len i) + 1) is set
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (i ^ <*K9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (i ^ <*K9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*K9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len i) + (len <*K9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len i) + (len <*K9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len i) + 1) + L is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*a9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len i) + (len <*a9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len i) + (len <*a9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len (i ^ <*a9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (i ^ <*a9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
i9 . L is set
dom i is Element of bool NAT
dom <*K9*> is non empty trivial V57(1) Element of bool NAT
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len (i ^ <*K9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
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
a . ((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*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
dom i is Element of bool NAT
i . y9 is set
dom <*K9*> is non empty trivial V57(1) Element of bool NAT
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len i) + L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len i) + L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len i) + 1) is non empty V50() V57((len i) + 1) Element of bool NAT
len <*a9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len i) + (len <*a9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len i) + (len <*a9*>)) is non empty V50() V57((len i) + (len <*a9*>)) Element of bool NAT
len (i ^ <*a9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len (i ^ <*a9*>)) is non empty V50() V57( len (i ^ <*a9*>)) Element of bool NAT
dom (i ^ <*a9*>) is non empty Element of bool NAT
(i ^ <*a9*>) . ((len i) + 1) is set
len <*K9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len i) + (len <*K9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len i) + (len <*K9*>)) is non empty V50() V57((len i) + (len <*K9*>)) Element of bool NAT
Seg (len (i ^ <*K9*>)) is non empty V50() V57( len (i ^ <*K9*>)) Element of bool NAT
(i ^ <*K9*>) . ((len i) + 1) is set
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (i ^ <*K9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (i ^ <*K9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*K9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len i) + (len <*K9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len i) + (len <*K9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len i) + 1) + L is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*a9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len i) + (len <*a9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len i) + (len <*a9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len (i ^ <*a9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (i ^ <*a9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
i9 . L is set
dom i is Element of bool NAT
dom <*K9*> is non empty trivial V57(1) Element of bool NAT
L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len (i ^ <*K9*>)) + L is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
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)
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) 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
[:(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
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
( the carrier of x, the Sorts of X,K,a) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
K9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of X, the Sorts of X
K9 . (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) is non empty set
[:( 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
K \/ a is Relation-like the carrier of x -defined Function-like non empty total set
a9 is Relation-like the carrier of x -defined Function-like non empty total V95() ManySortedRelation of the Sorts of X, the Sorts of X
( the carrier of x, the Sorts of X,a9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-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)):]
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 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)):]
(( the Sorts of X . (the_result_sort_of K)),((K . (the_result_sort_of K)) \/ (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)):]
a9 . (the_result_sort_of K) is Relation-like 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)),(a9 . (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 carrier of x, the Sorts of X,K,a) . (the_result_sort_of K) is Relation-like Element of bool [:( the Sorts of X . (the_result_sort_of K)),( the Sorts of X . (the_result_sort_of K)):]
i is Relation-like the carrier of x -defined Function-like non empty total V95() ManySortedRelation of the Sorts of X, the Sorts of X
( the carrier of x, the Sorts of X,i) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
i9 is set
<*i9*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set
K2 is set
[i9,K2] is set
<*K2*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set
a2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
a2 + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(the_arity_of K) /. (a2 + 1) is Element of the carrier of x
K9 . ((the_arity_of K) /. (a2 + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):]
the Sorts of X . ((the_arity_of K) /. (a2 + 1)) is non empty set
[:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):] is non empty set
y9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len y9 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
n is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len n is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
dom y9 is Element of bool NAT
y9 ^ <*i9*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
L is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
(y9 ^ <*i9*>) ^ L is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(Den (K,X)) . ((y9 ^ <*i9*>) ^ L) is set
n ^ <*i9*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(n ^ <*i9*>) ^ L is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(Den (K,X)) . ((n ^ <*i9*>) ^ L) is set
[((Den (K,X)) . ((y9 ^ <*i9*>) ^ L)),((Den (K,X)) . ((n ^ <*i9*>) ^ L))] is set
n ^ <*K2*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(n ^ <*K2*>) ^ L is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(Den (K,X)) . ((n ^ <*K2*>) ^ L) is set
K . ((the_arity_of K) /. (a2 + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):]
a . ((the_arity_of K) /. (a2 + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):]
(K . ((the_arity_of K) /. (a2 + 1))) "\/" (a . ((the_arity_of K) /. (a2 + 1))) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):]
(K . ((the_arity_of K) /. (a2 + 1))) \/ (a . ((the_arity_of K) /. (a2 + 1))) is Relation-like reflexive symmetric Element of bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):]
(( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),((K . ((the_arity_of K) /. (a2 + 1))) \/ (a . ((the_arity_of K) /. (a2 + 1))))) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):]
i . ((the_arity_of K) /. (a2 + 1)) is Relation-like Element of bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):]
(( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),(i . ((the_arity_of K) /. (a2 + 1)))) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):]
( the carrier of x, the Sorts of X,K,a) . ((the_arity_of K) /. (a2 + 1)) is Relation-like Element of bool [:( the Sorts of X . ((the_arity_of K) /. (a2 + 1))),( the Sorts of X . ((the_arity_of K) /. (a2 + 1))):]
L is Relation-like Function-like Element of Args (K,X)
(Den (K,X)) . L is Element of Result (K,X)
[((Den (K,X)) . L),((Den (K,X)) . ((n ^ <*K2*>) ^ L))] is set
the ResultSort 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 ResultSort of x . K is Element of the carrier of x
the Sorts of X . ( the ResultSort of x . K) is non empty set
the ResultSort of x * the Sorts of X is Relation-like non-empty Function-like set
( the ResultSort of x * the Sorts of X) . K is set
c₁₇ is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len c₁₇ is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c₁₇ . 1 is set
c₁₇ . (len c₁₇) is set
b9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len b9 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
b9 . 1 is set
b9 . (len b9) is set
EQR is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len EQR is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
dom EQR is Element of bool NAT
Seg (len b9) is V50() V57( len b9) Element of bool NAT
dom L is set
len ((y9 ^ <*i9*>) ^ L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len ((y9 ^ <*i9*>) ^ L)) is non empty V50() V57( len ((y9 ^ <*i9*>) ^ L)) Element of bool NAT
<*i9*> ^ L is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
y9 ^ (<*i9*> ^ L) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
len (y9 ^ (<*i9*> ^ L)) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len (y9 ^ (<*i9*> ^ L))) is non empty V50() V57( len (y9 ^ (<*i9*> ^ L))) Element of bool NAT
len (<*i9*> ^ L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + (len (<*i9*> ^ L)) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len n) + (len (<*i9*> ^ L))) is non empty V50() V57((len n) + (len (<*i9*> ^ L))) Element of bool NAT
n ^ (<*i9*> ^ L) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
len (n ^ (<*i9*> ^ L)) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len (n ^ (<*i9*> ^ L))) is non empty V50() V57( len (n ^ (<*i9*> ^ L))) Element of bool NAT
len ((n ^ <*i9*>) ^ L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len ((n ^ <*i9*>) ^ L)) is non empty V50() V57( len ((n ^ <*i9*>) ^ L)) Element of bool NAT
dom ((n ^ <*i9*>) ^ L) is non empty Element of bool NAT
c₁₇ ^ EQR is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
c9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len c9 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c9 . 1 is set
c9 . (len c9) is set
(len c₁₇) + (len EQR) is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
dom c₁₇ is Element of bool NAT
EQR . (len EQR) is set
d is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len c₁₇) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
dom (the_arity_of K) is Element of bool NAT
len (the_arity_of K) is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len (the_arity_of K)) is V50() V57( len (the_arity_of K)) Element of bool NAT
e is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of 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
d1 is non empty set
d2 is Relation-like non-empty non empty-yielding d1 -defined Function-like non empty total set
product d2 is non empty set
pi ((Args (K,X)),e) 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),e) 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)),e) is set
( the Sorts of X #) . (the_arity_of K) is set
pi ((( the Sorts of X #) . (the_arity_of K)),e) is set
product ((the_arity_of K) * the Sorts of X) is set
pi ((product ((the_arity_of K) * the Sorts of X)),e) is set
((the_arity_of K) * the Sorts of X) . e is set
(the_arity_of K) . e is set
the Sorts of X . ((the_arity_of K) . e) is set
(the_arity_of K) /. e is Element of the carrier of x
the Sorts of X . ((the_arity_of K) /. e) is non empty set
L . e is set
d + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c9 . (d + 1) is set
c₁₇ . (d + 1) is set
c9 . d is set
c₁₇ . d is set
[(c9 . d),(c9 . (d + 1))] is set
Seg (len c₁₇) is V50() V57( len c₁₇) Element of bool NAT
e is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
e + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c9 . d is set
Seg (len EQR) is V50() V57( len EQR) Element of bool NAT
d + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c9 . (d + 1) is set
EQR . 1 is set
e is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
((n ^ <*i9*>) ^ L) . e is set
(the_arity_of K) /. e is Element of the carrier of x
the Sorts of X . ((the_arity_of K) /. e) is non empty set
dom (n ^ (<*i9*> ^ L)) is non empty Element of bool NAT
dom n is Element of bool NAT
Seg (len n) is V50() V57( len n) Element of bool NAT
y9 . e is set
n . e is set
[(y9 . e),(n . e)] is set
K9 . ((the_arity_of K) /. e) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. e)),( the Sorts of X . ((the_arity_of K) /. e)):]
[:( the Sorts of X . ((the_arity_of K) /. e)),( the Sorts of X . ((the_arity_of K) /. e)):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of K) /. e)),( the Sorts of X . ((the_arity_of K) /. e)):] is non empty set
(n ^ (<*i9*> ^ L)) . e is set
dom (<*i9*> ^ L) is non empty Element of bool NAT
d1 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len n) + d1 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
d1 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len n) + d1 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(n ^ (<*i9*> ^ L)) . e is set
(<*i9*> ^ L) . d1 is set
(y9 ^ (<*i9*> ^ L)) . e is set
L . e is set
dom n is Element of bool NAT
dom (<*i9*> ^ L) is non empty Element of bool NAT
field (a . (the_result_sort_of K)) is set
field (K . (the_result_sort_of K)) is set
field ((K . (the_result_sort_of K)) \/ (a . (the_result_sort_of K))) is set
( the Sorts of X . (the_result_sort_of K)) \/ ( the Sorts of X . (the_result_sort_of K)) is non empty set
e is Relation-like Function-like Element of Args (K,X)
(Den (K,X)) . e is Element of Result (K,X)
[(c9 . d),(c9 . (d + 1))] is set
d - (len c₁₇) is ext-real V34() V35() set
e is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
e + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len c9) - (len c₁₇) is ext-real V34() V35() set
d + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(d + 1) - (len c₁₇) is ext-real V34() V35() set
b9 . e is set
b9 . (e + 1) is set
[(b9 . e),(b9 . (e + 1))] is set
(d - (len c₁₇)) + 1 is ext-real V34() V35() set
b9 . ((d - (len c₁₇)) + 1) is set
b9 . ((d + 1) - (len c₁₇)) is set
<*(b9 . ((d + 1) - (len c₁₇)))*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set
n ^ <*(b9 . ((d + 1) - (len c₁₇)))*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) ^ L is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
dom ((n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) ^ L) is non empty Element of bool NAT
d1 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
((n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) ^ L) . d1 is set
(the_arity_of K) /. d1 is Element of the carrier of x
the Sorts of X . ((the_arity_of K) /. d1) is non empty set
dom (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) is non empty Element of bool NAT
dom L is Element of bool NAT
len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
dom n is Element of bool NAT
Seg (len n) is V50() V57( len n) Element of bool NAT
y9 . d1 is set
n . d1 is set
[(y9 . d1),(n . d1)] is set
K9 . ((the_arity_of K) /. d1) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. d1)),( the Sorts of X . ((the_arity_of K) /. d1)):]
[:( the Sorts of X . ((the_arity_of K) /. d1)),( the Sorts of X . ((the_arity_of K) /. d1)):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of K) /. d1)),( the Sorts of X . ((the_arity_of K) /. d1)):] is non empty set
<*(b9 . ((d + 1) - (len c₁₇)))*> ^ L is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
n ^ (<*(b9 . ((d + 1) - (len c₁₇)))*> ^ L) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(n ^ (<*(b9 . ((d + 1) - (len c₁₇)))*> ^ L)) . d1 is set
dom <*(b9 . ((d + 1) - (len c₁₇)))*> is non empty trivial V57(1) Element of bool NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len n) + d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len n) + d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len y9) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len n) + 1) is non empty V50() V57((len n) + 1) Element of bool NAT
len <*(b9 . ((d + 1) - (len c₁₇)))*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + (len <*(b9 . ((d + 1) - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len n) + (len <*(b9 . ((d + 1) - (len c₁₇)))*>)) is non empty V50() V57((len n) + (len <*(b9 . ((d + 1) - (len c₁₇)))*>)) Element of bool NAT
Seg (len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>)) is non empty V50() V57( len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>)) Element of bool NAT
(n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) . d1 is set
len (y9 ^ <*i9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*i9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len y9) + (len <*i9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*(b9 . ((d + 1) - (len c₁₇)))*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + (len <*(b9 . ((d + 1) - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (y9 ^ <*i9*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len (y9 ^ <*i9*>)) + (len L)) is non empty V50() V57((len (y9 ^ <*i9*>)) + (len L)) Element of bool NAT
((len y9) + (len <*i9*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (((len y9) + (len <*i9*>)) + (len L)) is non empty V50() V57(((len y9) + (len <*i9*>)) + (len L)) Element of bool NAT
((len n) + 1) + (len L) is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (((len n) + 1) + (len L)) is non empty V50() V57(((len n) + 1) + (len L)) Element of bool NAT
((len n) + (len <*(b9 . ((d + 1) - (len c₁₇)))*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (((len n) + (len <*(b9 . ((d + 1) - (len c₁₇)))*>)) + (len L)) is non empty V50() V57(((len n) + (len <*(b9 . ((d + 1) - (len c₁₇)))*>)) + (len L)) Element of bool NAT
(len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>)) + (len L)) is non empty V50() V57((len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>)) + (len L)) Element of bool NAT
len ((n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) ^ L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len ((n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) ^ L)) is non empty V50() V57( len ((n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) ^ L)) Element of bool NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>)) + d2 is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>)) + d2 is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
L . d2 is set
L . d1 is set
dom n is Element of bool NAT
dom <*(b9 . ((d + 1) - (len c₁₇)))*> is non empty trivial V57(1) Element of bool NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>)) + d2 is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
b9 . (d - (len c₁₇)) is set
<*(b9 . (d - (len c₁₇)))*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set
n ^ <*(b9 . (d - (len c₁₇)))*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(n ^ <*(b9 . (d - (len c₁₇)))*>) ^ L is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
dom ((n ^ <*(b9 . (d - (len c₁₇)))*>) ^ L) is non empty Element of bool NAT
d1 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
((n ^ <*(b9 . (d - (len c₁₇)))*>) ^ L) . d1 is set
(the_arity_of K) /. d1 is Element of the carrier of x
the Sorts of X . ((the_arity_of K) /. d1) is non empty set
dom (n ^ <*(b9 . (d - (len c₁₇)))*>) is non empty Element of bool NAT
dom L is Element of bool NAT
len (n ^ <*(b9 . (d - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
dom n is Element of bool NAT
Seg (len n) is V50() V57( len n) Element of bool NAT
y9 . d1 is set
n . d1 is set
[(y9 . d1),(n . d1)] is set
K9 . ((the_arity_of K) /. d1) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. d1)),( the Sorts of X . ((the_arity_of K) /. d1)):]
[:( the Sorts of X . ((the_arity_of K) /. d1)),( the Sorts of X . ((the_arity_of K) /. d1)):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of K) /. d1)),( the Sorts of X . ((the_arity_of K) /. d1)):] is non empty set
<*(b9 . (d - (len c₁₇)))*> ^ L is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
n ^ (<*(b9 . (d - (len c₁₇)))*> ^ L) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(n ^ (<*(b9 . (d - (len c₁₇)))*> ^ L)) . d1 is set
dom <*(b9 . (d - (len c₁₇)))*> is non empty trivial V57(1) Element of bool NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len n) + d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len n) + d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len y9) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len n) + 1) is non empty V50() V57((len n) + 1) Element of bool NAT
len <*(b9 . (d - (len c₁₇)))*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + (len <*(b9 . (d - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len n) + (len <*(b9 . (d - (len c₁₇)))*>)) is non empty V50() V57((len n) + (len <*(b9 . (d - (len c₁₇)))*>)) Element of bool NAT
Seg (len (n ^ <*(b9 . (d - (len c₁₇)))*>)) is non empty V50() V57( len (n ^ <*(b9 . (d - (len c₁₇)))*>)) Element of bool NAT
(n ^ <*(b9 . (d - (len c₁₇)))*>) . d1 is set
len (y9 ^ <*i9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*i9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len y9) + (len <*i9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*(b9 . (d - (len c₁₇)))*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + (len <*(b9 . (d - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (y9 ^ <*i9*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len (y9 ^ <*i9*>)) + (len L)) is non empty V50() V57((len (y9 ^ <*i9*>)) + (len L)) Element of bool NAT
((len y9) + (len <*i9*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (((len y9) + (len <*i9*>)) + (len L)) is non empty V50() V57(((len y9) + (len <*i9*>)) + (len L)) Element of bool NAT
((len n) + 1) + (len L) is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (((len n) + 1) + (len L)) is non empty V50() V57(((len n) + 1) + (len L)) Element of bool NAT
((len n) + (len <*(b9 . (d - (len c₁₇)))*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (((len n) + (len <*(b9 . (d - (len c₁₇)))*>)) + (len L)) is non empty V50() V57(((len n) + (len <*(b9 . (d - (len c₁₇)))*>)) + (len L)) Element of bool NAT
(len (n ^ <*(b9 . (d - (len c₁₇)))*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg ((len (n ^ <*(b9 . (d - (len c₁₇)))*>)) + (len L)) is non empty V50() V57((len (n ^ <*(b9 . (d - (len c₁₇)))*>)) + (len L)) Element of bool NAT
len ((n ^ <*(b9 . (d - (len c₁₇)))*>) ^ L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len ((n ^ <*(b9 . (d - (len c₁₇)))*>) ^ L)) is non empty V50() V57( len ((n ^ <*(b9 . (d - (len c₁₇)))*>) ^ L)) Element of bool NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (n ^ <*(b9 . (d - (len c₁₇)))*>)) + d2 is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (n ^ <*(b9 . (d - (len c₁₇)))*>)) + d2 is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
L . d2 is set
L . d1 is set
dom n is Element of bool NAT
dom <*(b9 . (d - (len c₁₇)))*> is non empty trivial V57(1) Element of bool NAT
d2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(len (n ^ <*(b9 . (d - (len c₁₇)))*>)) + d2 is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len ((n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) ^ L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (n ^ <*(b9 . ((d + 1) - (len c₁₇)))*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*(b9 . ((d + 1) - (len c₁₇)))*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + (len <*(b9 . ((d + 1) - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len n) + (len <*(b9 . ((d + 1) - (len c₁₇)))*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len n) + 1) + (len L) is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*i9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len y9) + (len <*i9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len y9) + (len <*i9*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len (y9 ^ <*i9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (y9 ^ <*i9*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len ((n ^ <*(b9 . (d - (len c₁₇)))*>) ^ L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len (n ^ <*(b9 . (d - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len (n ^ <*(b9 . (d - (len c₁₇)))*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*(b9 . (d - (len c₁₇)))*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len n) + (len <*(b9 . (d - (len c₁₇)))*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
((len n) + (len <*(b9 . (d - (len c₁₇)))*>)) + (len L) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c9 . d is set
EQR . (d - (len c₁₇)) is set
d1 is Relation-like Function-like Element of Args (K,X)
(Den (K,X)) . d1 is Element of Result (K,X)
[(b9 . (d - (len c₁₇))),(b9 . ((d + 1) - (len c₁₇)))] is set
c9 . (d + 1) is set
EQR . ((d + 1) - (len c₁₇)) is set
d2 is Relation-like Function-like Element of Args (K,X)
(Den (K,X)) . d2 is Element of Result (K,X)
[(c9 . d),(c9 . (d + 1))] is set
c9 . d is set
d + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c9 . (d + 1) is set
[(c9 . d),(c9 . (d + 1))] is set
c9 . d is set
d + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c9 . (d + 1) is set
[(c9 . d),(c9 . (d + 1))] is set
c9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len c9 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c9 . 1 is set
c9 . (len c9) is set
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
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
the carrier of x * is functional non empty FinSequence-membered M15( the carrier of x)
rng ( the Sorts of X #) is non empty set
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 *
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
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
K9 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
( the carrier of x, the Sorts of X,a,K9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
a9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of X, the Sorts of X
a9 . (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) is non empty set
[:( 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
i is Relation-like Function-like Element of Args (K,X)
dom i is set
i9 is Relation-like Function-like Element of Args (K,X)
(Den (K,X)) . i is Element of Result (K,X)
(Den (K,X)) . i9 is Element of Result (K,X)
[((Den (K,X)) . i),((Den (K,X)) . i9)] is set
K2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
K2 + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
a2 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len a2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
y9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len y9 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
n is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
a2 ^ n is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
dom a2 is Element of bool NAT
y9 ^ n is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
(Den (K,X)) . (y9 ^ n) is set
[((Den (K,X)) . i),((Den (K,X)) . (y9 ^ n))] is set
Seg (len a2) is V50() V57( len a2) Element of bool NAT
dom y9 is Element of bool NAT
L is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
L is set
<*L*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set
L ^ <*L*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
len L is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*L*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len L) + (len <*L*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len L) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
y9 . (K2 + 1) is set
(y9 ^ n) . (K2 + 1) is set
c₁₇ is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
b9 is set
<*b9*> is Relation-like NAT -defined Function-like constant non empty trivial V50() V57(1) FinSequence-like FinSubsequence-like set
c₁₇ ^ <*b9*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
len c₁₇ is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
len <*b9*> is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len c₁₇) + (len <*b9*>) is non empty ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
(len c₁₇) + 1 is non empty ext-real positive non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
dom c₁₇ is Element of bool NAT
Seg (len c₁₇) is V50() V57( len c₁₇) Element of bool NAT
dom L is Element of bool NAT
EQR is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
c₁₇ . EQR is set
L . EQR is set
[(c₁₇ . EQR),(L . EQR)] is set
(the_arity_of K) /. EQR is Element of the carrier of x
a9 . ((the_arity_of K) /. EQR) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. EQR)),( the Sorts of X . ((the_arity_of K) /. EQR)):]
the Sorts of X . ((the_arity_of K) /. EQR) is non empty set
[:( the Sorts of X . ((the_arity_of K) /. EQR)),( the Sorts of X . ((the_arity_of K) /. EQR)):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of K) /. EQR)),( the Sorts of X . ((the_arity_of K) /. EQR)):] is non empty set
i . EQR is set
a2 . EQR is set
(y9 ^ n) . EQR is set
y9 . EQR is set
(c₁₇ ^ <*b9*>) ^ n is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
<*b9*> ^ n is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
c₁₇ ^ (<*b9*> ^ n) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
L ^ <*b9*> is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
(L ^ <*b9*>) ^ n is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
L ^ (<*b9*> ^ n) is Relation-like NAT -defined Function-like non empty V50() FinSequence-like FinSubsequence-like set
EQR is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
i . EQR is set
((L ^ <*b9*>) ^ n) . EQR is set
[(i . EQR),(((L ^ <*b9*>) ^ n) . EQR)] is set
(the_arity_of K) /. EQR is Element of the carrier of x
a9 . ((the_arity_of K) /. EQR) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. EQR)),( the Sorts of X . ((the_arity_of K) /. EQR)):]
the Sorts of X . ((the_arity_of K) /. EQR) is non empty set
[:( the Sorts of X . ((the_arity_of K) /. EQR)),( the Sorts of X . ((the_arity_of K) /. EQR)):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of K) /. EQR)),( the Sorts of X . ((the_arity_of K) /. EQR)):] is non empty set
L . EQR is set
c₁₇ . EQR is set
a2 . (K2 + 1) is set
i . (K2 + 1) is set
[b9,L] is set
(the_arity_of K) /. (K2 + 1) is Element of the carrier of x
a9 . ((the_arity_of K) /. (K2 + 1)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of K) /. (K2 + 1))),( the Sorts of X . ((the_arity_of K) /. (K2 + 1))):]
the Sorts of X . ((the_arity_of K) /. (K2 + 1)) is non empty set
[:( the Sorts of X . ((the_arity_of K) /. (K2 + 1))),( the Sorts of X . ((the_arity_of K) /. (K2 + 1))):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of K) /. (K2 + 1))),( the Sorts of X . ((the_arity_of K) /. (K2 + 1))):] is non empty set
(Den (K,X)) . ((L ^ <*b9*>) ^ n) is set
[((Den (K,X)) . i),((Den (K,X)) . ((L ^ <*b9*>) ^ n))] is set
dom i9 is set
dom (the_arity_of K) is Element of bool NAT
len (the_arity_of K) is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len (the_arity_of K)) is V50() V57( len (the_arity_of K)) Element of bool NAT
a2 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len a2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len a2) is V50() V57( len a2) Element of bool NAT
dom a2 is Element of bool NAT
K2 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len K2 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len K2) is V50() V57( len K2) Element of bool NAT
dom K2 is Element of bool NAT
K2 ^ {} is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
a2 ^ {} is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
field (a9 . (the_result_sort_of K)) is set
the ResultSort 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 ResultSort of x . K is Element of the carrier of x
the Sorts of X . ( the ResultSort of x . K) is non empty set
the ResultSort of x * the Sorts of X is Relation-like non-empty Function-like set
( the ResultSort of x * the Sorts of X) . K is set
y9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len y9 is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
n is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
len n is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
L is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
y9 ^ L is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
dom y9 is Element of bool NAT
n ^ L is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
(Den (K,X)) . (n ^ L) is set
[((Den (K,X)) . i),((Den (K,X)) . (n ^ L))] is set
x is non empty non void V71() ManySortedSign
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 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 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
( the carrier of x, the Sorts of X,K,K) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-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 ManySortedRelation of the Sorts of X, the Sorts of X
K9 is Relation-like the carrier of x -defined Function-like non empty total V95() ManySortedRelation of the Sorts of X, the Sorts of X
the carrier' of x is non empty set
a9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of X, the Sorts of X
i is Element of the carrier' of x
Args (i,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
the carrier of x * is functional non empty FinSequence-membered M15( the carrier of x)
rng ( the Sorts of X #) is non empty set
i9 is Relation-like Function-like Element of Args (i,X)
dom i9 is set
K2 is Relation-like Function-like Element of Args (i,X)
the_arity_of i is Relation-like NAT -defined the carrier of x -valued Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of x *
Result (i,X) is non empty Element of rng the Sorts of X
rng the Sorts of X is non empty V38() set
Den (i,X) is Relation-like Function-like V18( Args (i,X), Result (i,X)) Element of bool [:(Args (i,X)),(Result (i,X)):]
[:(Args (i,X)),(Result (i,X)):] is Relation-like non empty set
bool [:(Args (i,X)),(Result (i,X)):] is non empty set
(Den (i,X)) . i9 is Element of Result (i,X)
(Den (i,X)) . K2 is Element of Result (i,X)
[((Den (i,X)) . i9),((Den (i,X)) . K2)] is set
the_result_sort_of i is Element of the carrier of x
a9 . (the_result_sort_of i) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of i)),( the Sorts of X . (the_result_sort_of i)):]
the Sorts of X . (the_result_sort_of i) is non empty set
[:( the Sorts of X . (the_result_sort_of i)),( the Sorts of X . (the_result_sort_of i)):] is Relation-like non empty set
bool [:( the Sorts of X . (the_result_sort_of i)),( the Sorts of X . (the_result_sort_of i)):] is non empty set
x is non empty non void V71() ManySortedSign
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 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 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 /\ K is Relation-like the carrier of x -defined Function-like non empty total set
a is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
K9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
a9 is Relation-like the carrier of x -defined Function-like non empty total V95() ManySortedRelation of the Sorts of X, the Sorts of X
the carrier' of x is non empty set
i is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of X, the Sorts of X
i9 is Element of the carrier' of x
Args (i9,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
the carrier of x * is functional non empty FinSequence-membered M15( the carrier of x)
rng ( the Sorts of X #) is non empty set
the_arity_of i9 is Relation-like NAT -defined the carrier of x -valued Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of x *
Result (i9,X) is non empty Element of rng the Sorts of X
rng the Sorts of X is non empty V38() set
Den (i9,X) is Relation-like Function-like V18( Args (i9,X), Result (i9,X)) Element of bool [:(Args (i9,X)),(Result (i9,X)):]
[:(Args (i9,X)),(Result (i9,X)):] is Relation-like non empty set
bool [:(Args (i9,X)),(Result (i9,X)):] is non empty set
the_result_sort_of i9 is Element of the carrier of x
i . (the_result_sort_of i9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of i9)),( the Sorts of X . (the_result_sort_of i9)):]
the Sorts of X . (the_result_sort_of i9) is non empty set
[:( the Sorts of X . (the_result_sort_of i9)),( the Sorts of X . (the_result_sort_of i9)):] is Relation-like non empty set
bool [:( the Sorts of X . (the_result_sort_of i9)),( the Sorts of X . (the_result_sort_of i9)):] is non empty set
K2 is Relation-like Function-like Element of Args (i9,X)
dom K2 is set
a2 is Relation-like Function-like Element of Args (i9,X)
(Den (i9,X)) . K2 is Element of Result (i9,X)
(Den (i9,X)) . a2 is Element of Result (i9,X)
[((Den (i9,X)) . K2),((Den (i9,X)) . a2)] 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 i9) /. y9 is Element of the carrier of x
K . ((the_arity_of i9) /. y9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):]
the Sorts of X . ((the_arity_of i9) /. y9) is non empty set
[:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):] is non empty set
i . ((the_arity_of i9) /. y9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):]
K . ((the_arity_of i9) /. y9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):]
(K . ((the_arity_of i9) /. y9)) /\ (K . ((the_arity_of i9) /. y9)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):]
K . (the_result_sort_of i9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of i9)),( the Sorts of X . (the_result_sort_of i9)):]
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 i9) /. y9 is Element of the carrier of x
K . ((the_arity_of i9) /. y9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):]
the Sorts of X . ((the_arity_of i9) /. y9) is non empty set
[:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):] is non empty set
i . ((the_arity_of i9) /. y9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):]
K . ((the_arity_of i9) /. y9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):]
(K . ((the_arity_of i9) /. y9)) /\ (K . ((the_arity_of i9) /. y9)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i9) /. y9)),( the Sorts of X . ((the_arity_of i9) /. y9)):]
K . (the_result_sort_of i9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of i9)),( the Sorts of X . (the_result_sort_of i9)):]
(K . (the_result_sort_of i9)) /\ (K . (the_result_sort_of i9)) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of i9)),( the Sorts of X . (the_result_sort_of i9)):]
x is non empty non void V71() ManySortedSign
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
( the carrier of x, the Sorts of X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of ( the carrier of x, the Sorts of X) is non empty set
the 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 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 set
product a is set
K9 is set
a9 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
i is set
dom a is non empty Element of bool the carrier of x
bool the carrier of x is non empty set
i9 is Element of the carrier of x
a9 . i9 is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . i9),( the Sorts of X . i9):]
the Sorts of X . i9 is non empty set
[:( the Sorts of X . i9),( the Sorts of X . i9):] is Relation-like non empty set
bool [:( the Sorts of X . i9),( the Sorts of X . i9):] is non empty set
a . i9 is set
a9 . i is set
a . i is set
dom a9 is non empty Element of bool the carrier of x
a9 is set
the L_join of ( the carrier of x, the Sorts of X) is Relation-like Function-like V18([: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):]
[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
[:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is non empty set
a9 is non empty set
the L_join of ( the carrier of x, the Sorts of X) || a9 is set
[:a9,a9:] is Relation-like non empty set
the L_join of ( the carrier of x, the Sorts of X) | [:a9,a9:] is Relation-like Function-like set
the L_meet of ( the carrier of x, the Sorts of X) is Relation-like Function-like V18([: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):]
the L_meet of ( the carrier of x, the Sorts of X) || a9 is set
the L_meet of ( the carrier of x, the Sorts of X) | [:a9,a9:] is Relation-like Function-like set
K2 is set
[:[:a9,a9:], the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
bool [:[:a9,a9:], the carrier of ( the carrier of x, the Sorts of X):] is non empty set
a2 is Relation-like Function-like V18([:a9,a9:], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[:a9,a9:], the carrier of ( the carrier of x, the Sorts of X):]
dom a2 is set
y9 is set
n is set
L is set
[n,L] is set
L 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
L 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
a2 . y9 is set
the L_meet of ( the carrier of x, the Sorts of X) . (n,L) is set
the L_meet of ( the carrier of x, the Sorts of X) . [n,L] is set
L /\ L is Relation-like the carrier of x -defined Function-like non empty total set
[:[:a9,a9:],a9:] is Relation-like non empty set
bool [:[:a9,a9:],a9:] is non empty set
K2 is Relation-like Function-like V18([:a9,a9:], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[:a9,a9:], the carrier of ( the carrier of x, the Sorts of X):]
dom K2 is set
n is set
L is set
L is set
[L,L] is set
c₁₇ 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
L 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
K2 . n is set
the L_join of ( the carrier of x, the Sorts of X) . (L,L) is set
the L_join of ( the carrier of x, the Sorts of X) . [L,L] is set
( the carrier of x, the Sorts of X,L,c₁₇) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
n is Relation-like Function-like V18([:a9,a9:],a9) Element of bool [:[:a9,a9:],a9:]
y9 is Relation-like Function-like V18([:a9,a9:],a9) Element of bool [:[:a9,a9:],a9:]
LattStr(# a9,n,y9 #) is non empty strict LattStr
L 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
L 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
n . (L,L) is set
[L,L] is set
n . [L,L] is set
( the carrier of x, the Sorts of X,L,L) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
y9 . (L,L) is set
y9 . [L,L] is set
L /\ L is Relation-like the carrier of x -defined Function-like non empty total set
the L_join of ( the carrier of x, the Sorts of X) . (L,L) is set
the L_join of ( the carrier of x, the Sorts of X) . [L,L] is set
the L_meet of ( the carrier of x, the Sorts of X) . (L,L) is set
the L_meet of ( the carrier of x, the Sorts of X) . [L,L] is set
L is Element of a9
L is Element of a9
n . (L,L) is Element of a9
[L,L] is set
n . [L,L] is set
c₁₇ 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
b9 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
( the carrier of x, the Sorts of X,c₁₇,b9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
n . (L,L) is Element of a9
[L,L] is set
n . [L,L] is set
L is non empty LattStr
the carrier of L is non empty set
L is Element of the carrier of L
L is Element of the carrier of L
L "\/" L is Element of the carrier of L
L "\/" L is Element of the carrier of L
n . (L,L) is set
[L,L] is set
n . [L,L] is set
the L_join of L is Relation-like Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (L,L) is Element of the carrier of L
[L,L] is set
the L_join of L . [L,L] is set
L is Element of a9
L is Element of a9
c₁₇ is Element of a9
EQR 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
c9 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
EQR /\ c9 is Relation-like the carrier of x -defined Function-like non empty total set
b9 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
b9 /\ EQR is Relation-like the carrier of x -defined Function-like non empty total set
y9 . (L,c₁₇) is Element of a9
[L,c₁₇] is set
y9 . [L,c₁₇] is set
y9 . (L,(y9 . (L,c₁₇))) is Element of a9
[L,(y9 . (L,c₁₇))] is set
y9 . [L,(y9 . (L,c₁₇))] is set
d 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
y9 . (L,d) is set
[L,d] is set
y9 . [L,d] is set
b9 /\ (EQR /\ c9) is Relation-like the carrier of x -defined Function-like non empty total set
(b9 /\ EQR) /\ c9 is Relation-like the carrier of x -defined Function-like non empty total set
e 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
y9 . (e,c₁₇) is set
[e,c₁₇] is set
y9 . [e,c₁₇] is set
y9 . (L,L) is Element of a9
[L,L] is set
y9 . [L,L] is set
y9 . ((y9 . (L,L)),c₁₇) is Element of a9
[(y9 . (L,L)),c₁₇] is set
y9 . [(y9 . (L,L)),c₁₇] is set
L is Element of the carrier of L
L is Element of the carrier of L
c₁₇ is Element of the carrier of L
L "/\" c₁₇ is Element of the carrier of L
L "/\" (L "/\" c₁₇) is Element of the carrier of L
L "/\" L is Element of the carrier of L
(L "/\" L) "/\" c₁₇ is Element of the carrier of L
the L_meet of L is Relation-like Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L,(L "/\" c₁₇)) is Element of the carrier of L
[L,(L "/\" c₁₇)] is set
the L_meet of L . [L,(L "/\" c₁₇)] is set
y9 . (L,c₁₇) is set
[L,c₁₇] is set
y9 . [L,c₁₇] is set
y9 . (L,(y9 . (L,c₁₇))) is set
[L,(y9 . (L,c₁₇))] is set
y9 . [L,(y9 . (L,c₁₇))] is set
the L_meet of L . (L,L) is Element of the carrier of L
[L,L] is set
the L_meet of L . [L,L] is set
the L_meet of L . (( the L_meet of L . (L,L)),c₁₇) is Element of the carrier of L
[( the L_meet of L . (L,L)),c₁₇] is set
the L_meet of L . [( the L_meet of L . (L,L)),c₁₇] is set
the L_meet of L . ((L "/\" L),c₁₇) is Element of the carrier of L
[(L "/\" L),c₁₇] is set
the L_meet of L . [(L "/\" L),c₁₇] is set
L is Element of a9
L is Element of a9
c₁₇ is Element of a9
EQR 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
c9 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
( the carrier of x, the Sorts of X,EQR,c9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
b9 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
( the carrier of x, the Sorts of X,b9,EQR) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
n . (L,c₁₇) is Element of a9
[L,c₁₇] is set
n . [L,c₁₇] is set
n . (L,(n . (L,c₁₇))) is Element of a9
[L,(n . (L,c₁₇))] is set
n . [L,(n . (L,c₁₇))] is set
d 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
n . (L,d) is set
[L,d] is set
n . [L,d] is set
( the carrier of x, the Sorts of X,b9,( the carrier of x, the Sorts of X,EQR,c9)) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
( the carrier of x, the Sorts of X,( the carrier of x, the Sorts of X,b9,EQR),c9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
e 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
n . (e,c₁₇) is set
[e,c₁₇] is set
n . [e,c₁₇] is set
n . (L,L) is Element of a9
[L,L] is set
n . [L,L] is set
n . ((n . (L,L)),c₁₇) is Element of a9
[(n . (L,L)),c₁₇] is set
n . [(n . (L,L)),c₁₇] is set
L is Element of the carrier of L
L is Element of the carrier of L
c₁₇ is Element of the carrier of L
L "\/" c₁₇ is Element of the carrier of L
L "\/" (L "\/" c₁₇) is Element of the carrier of L
L "\/" L is Element of the carrier of L
(L "\/" L) "\/" c₁₇ is Element of the carrier of L
the L_join of L is Relation-like Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . (L,(L "\/" c₁₇)) is Element of the carrier of L
[L,(L "\/" c₁₇)] is set
the L_join of L . [L,(L "\/" c₁₇)] is set
n . (L,c₁₇) is set
[L,c₁₇] is set
n . [L,c₁₇] is set
n . (L,(n . (L,c₁₇))) is set
[L,(n . (L,c₁₇))] is set
n . [L,(n . (L,c₁₇))] is set
the L_join of L . (L,L) is Element of the carrier of L
[L,L] is set
the L_join of L . [L,L] is set
the L_join of L . (( the L_join of L . (L,L)),c₁₇) is Element of the carrier of L
[( the L_join of L . (L,L)),c₁₇] is set
the L_join of L . [( the L_join of L . (L,L)),c₁₇] is set
the L_join of L . ((L "\/" L),c₁₇) is Element of the carrier of L
[(L "\/" L),c₁₇] is set
the L_join of L . [(L "\/" L),c₁₇] is set
L is Element of a9
L is Element of a9
y9 . (L,L) is Element of a9
[L,L] is set
y9 . [L,L] is set
b9 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
c₁₇ 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
b9 /\ c₁₇ is Relation-like the carrier of x -defined Function-like non empty total set
y9 . (L,L) is Element of a9
[L,L] is set
y9 . [L,L] is set
L is Element of the carrier of L
L is Element of the carrier of L
L "/\" L is Element of the carrier of L
L "/\" L is Element of the carrier of L
y9 . (L,L) is set
[L,L] is set
y9 . [L,L] is set
the L_meet of L is Relation-like Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L,L) is Element of the carrier of L
[L,L] is set
the L_meet of L . [L,L] is set
L is Element of the carrier of L
L is Element of the carrier of L
L "\/" L is Element of the carrier of L
L "/\" (L "\/" L) is Element of the carrier of L
n . (L,L) is set
[L,L] is set
n . [L,L] is set
y9 . (L,(n . (L,L))) is set
[L,(n . (L,L))] is set
y9 . [L,(n . (L,L))] is set
c₁₇ 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
b9 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
( the carrier of x, the Sorts of X,c₁₇,b9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
EQR 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
y9 . (L,EQR) is set
[L,EQR] is set
y9 . [L,EQR] is set
c₁₇ /\ ( the carrier of x, the Sorts of X,c₁₇,b9) is Relation-like the carrier of x -defined Function-like non empty total set
the L_meet of L is Relation-like Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_meet of L . (L,(L "\/" L)) is Element of the carrier of L
[L,(L "\/" L)] is set
the L_meet of L . [L,(L "\/" L)] is set
L is Element of the carrier of L
L is Element of the carrier of L
L "/\" L is Element of the carrier of L
(L "/\" L) "\/" L is Element of the carrier of L
y9 . (L,L) is set
[L,L] is set
y9 . [L,L] is set
n . ((y9 . (L,L)),L) is set
[(y9 . (L,L)),L] is set
n . [(y9 . (L,L)),L] is set
c₁₇ 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
b9 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
c₁₇ /\ b9 is Relation-like the carrier of x -defined Function-like non empty total set
n . ((c₁₇ /\ b9),b9) is set
[(c₁₇ /\ b9),b9] is set
n . [(c₁₇ /\ b9),b9] is set
EQR 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
( the carrier of x, the Sorts of X,EQR,b9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
the L_join of L is Relation-like Function-like V18([: the carrier of L, the carrier of L:], the carrier of L) Element of bool [:[: the carrier of L, the carrier of L:], the carrier of L:]
[: the carrier of L, the carrier of L:] is Relation-like non empty set
[:[: the carrier of L, the carrier of L:], the carrier of L:] is Relation-like non empty set
bool [:[: the carrier of L, the carrier of L:], the carrier of L:] is non empty set
the L_join of L . ((L "/\" L),L) is Element of the carrier of L
[(L "/\" L),L] is set
the L_join of L . [(L "/\" L),L] is set
L is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
L is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of ( the carrier of x, the Sorts of X)
the carrier of L is non empty set
c₁₇ is set
b9 is set
K is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of ( the carrier of x, the Sorts of X)
the carrier of K is non empty set
K is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of ( the carrier of x, the Sorts of X)
the carrier of K is non empty set
a is 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:]
[: 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 ( the carrier of x, the Sorts of X) is Relation-like Function-like V18([: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):]
the carrier of ( the carrier of x, the Sorts of X) is non empty set
[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
[:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is non empty set
the L_join of ( the carrier of x, the Sorts of X) || the carrier of K is set
[: the carrier of K, the carrier of K:] is Relation-like non empty set
the L_join of ( the carrier of x, the Sorts of X) | [: the carrier of K, the carrier of K:] is Relation-like Function-like 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:]
[:[: 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_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 L_meet of ( the carrier of x, the Sorts of X) is Relation-like Function-like V18([: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):]
the L_meet of ( the carrier of x, the Sorts of X) || the carrier of K is set
the L_meet of ( the carrier of x, the Sorts of X) | [: the carrier of K, the carrier of K:] is Relation-like Function-like 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:]
x is non empty non void V71() ManySortedSign
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
id the Sorts of X is Relation-like the carrier of x -defined Function-like non empty total V94() ManySortedFunction of the Sorts of X, the Sorts of X
K is set
(id the Sorts of X) . K is set
the Sorts of X . K is set
[:( the Sorts of X . K),( the Sorts of X . K):] is Relation-like set
bool [:( the Sorts of X . K),( the Sorts of X . K):] is non empty set
id ( the Sorts of X . K) is Relation-like the Sorts of X . K -defined the Sorts of X . K -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of X . K),( the Sorts of X . K):]
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
a is set
the Sorts of X . a is set
[:( the Sorts of X . a),( the Sorts of X . a):] is Relation-like set
bool [:( the Sorts of X . a),( the Sorts of X . a):] is non empty set
K . a is set
K9 is Relation-like Element of bool [:( the Sorts of X . a),( the Sorts of X . a):]
id ( the Sorts of X . a) is Relation-like the Sorts of X . a -defined the Sorts of X . a -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of X . a),( the Sorts of X . a):]
a is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
K9 is Relation-like the carrier of x -defined Function-like non empty total V95() ManySortedRelation of the Sorts of X, the Sorts of X
the carrier' of x is non empty set
a9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of X, the Sorts of X
i is Element of the carrier' of x
Args (i,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
the carrier of x * is functional non empty FinSequence-membered M15( the carrier of x)
rng ( the Sorts of X #) is non empty set
the_arity_of i is Relation-like NAT -defined the carrier of x -valued Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of x *
Result (i,X) is non empty Element of rng the Sorts of X
rng the Sorts of X is non empty V38() set
Den (i,X) is Relation-like Function-like V18( Args (i,X), Result (i,X)) Element of bool [:(Args (i,X)),(Result (i,X)):]
[:(Args (i,X)),(Result (i,X)):] is Relation-like non empty set
bool [:(Args (i,X)),(Result (i,X)):] is non empty set
the_result_sort_of i is Element of the carrier of x
a9 . (the_result_sort_of i) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of i)),( the Sorts of X . (the_result_sort_of i)):]
the Sorts of X . (the_result_sort_of i) is non empty set
[:( the Sorts of X . (the_result_sort_of i)),( the Sorts of X . (the_result_sort_of i)):] is Relation-like non empty set
bool [:( the Sorts of X . (the_result_sort_of i)),( the Sorts of X . (the_result_sort_of i)):] is non empty set
i9 is Relation-like Function-like Element of Args (i,X)
dom i9 is set
K2 is Relation-like Function-like Element of Args (i,X)
(Den (i,X)) . i9 is Element of Result (i,X)
(Den (i,X)) . K2 is Element of Result (i,X)
[((Den (i,X)) . i9),((Den (i,X)) . K2)] is set
dom K2 is set
dom (the_arity_of i) is Element of bool NAT
len (the_arity_of i) is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() Element of NAT
Seg (len (the_arity_of i)) is V50() V57( len (the_arity_of i)) Element of bool NAT
n is ext-real non negative V27() V28() V29() V33() V34() V35() V50() V55() set
(the_arity_of i) /. n is Element of the carrier of x
the Sorts of X . ((the_arity_of i) /. n) is non empty set
a9 . ((the_arity_of i) /. n) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i) /. n)),( the Sorts of X . ((the_arity_of i) /. n)):]
[:( the Sorts of X . ((the_arity_of i) /. n)),( the Sorts of X . ((the_arity_of i) /. n)):] is Relation-like non empty set
bool [:( the Sorts of X . ((the_arity_of i) /. n)),( the Sorts of X . ((the_arity_of i) /. n)):] is non empty set
id ( the Sorts of X . ((the_arity_of i) /. n)) is Relation-like the Sorts of X . ((the_arity_of i) /. n) -defined the Sorts of X . ((the_arity_of i) /. n) -valued Function-like one-to-one non empty total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of X . ((the_arity_of i) /. n)),( the Sorts of X . ((the_arity_of i) /. n)):]
i9 . n is set
K2 . n is set
[(i9 . n),(K2 . n)] is set
a2 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
a2 . n is set
y9 is Relation-like NAT -defined Function-like V50() FinSequence-like FinSubsequence-like set
y9 . n is set
the ResultSort 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 ResultSort of x * the Sorts of X is Relation-like non-empty Function-like set
( the ResultSort of x * the Sorts of X) . i is set
dom the ResultSort of x is set
the ResultSort of x . i is Element of the carrier of x
the Sorts of X . ( the ResultSort of x . i) is non empty set
id ( the Sorts of X . (the_result_sort_of i)) is Relation-like the Sorts of X . (the_result_sort_of i) -defined the Sorts of X . (the_result_sort_of i) -valued Function-like one-to-one non empty total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of i)),( the Sorts of X . (the_result_sort_of i)):]
x is non empty non void V71() ManySortedSign
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
[| the Sorts of X, the Sorts of X|] is Relation-like the carrier of x -defined Function-like non empty total set
K is set
[| the Sorts of X, the Sorts of X|] . K is set
the Sorts of X . K is set
[:( the Sorts of X . K),( the Sorts of X . K):] is Relation-like set
bool [:( the Sorts of X . K),( the Sorts of X . K):] is non empty 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
a is set
the Sorts of X . a is set
[:( the Sorts of X . a),( the Sorts of X . a):] is Relation-like set
bool [:( the Sorts of X . a),( the Sorts of X . a):] is non empty set
K . a is set
K9 is Relation-like Element of bool [:( the Sorts of X . a),( the Sorts of X . a):]
nabla ( the Sorts of X . a) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . a),( the Sorts of X . a):]
a is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
the carrier' of x is non empty set
K9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of X, the Sorts of X
a9 is Element of the carrier' of x
Args (a9,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
the carrier of x * is functional non empty FinSequence-membered M15( the carrier of x)
rng ( the Sorts of X #) is non empty set
the_arity_of a9 is Relation-like NAT -defined the carrier of x -valued Function-like V50() FinSequence-like FinSubsequence-like Element of the carrier of x *
Result (a9,X) is non empty Element of rng the Sorts of X
rng the Sorts of X is non empty V38() set
Den (a9,X) is Relation-like Function-like V18( Args (a9,X), Result (a9,X)) Element of bool [:(Args (a9,X)),(Result (a9,X)):]
[:(Args (a9,X)),(Result (a9,X)):] is Relation-like non empty set
bool [:(Args (a9,X)),(Result (a9,X)):] is non empty set
the_result_sort_of a9 is Element of the carrier of x
K9 . (the_result_sort_of a9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . (the_result_sort_of a9)),( the Sorts of X . (the_result_sort_of a9)):]
the Sorts of X . (the_result_sort_of a9) is non empty set
[:( the Sorts of X . (the_result_sort_of a9)),( the Sorts of X . (the_result_sort_of a9)):] is Relation-like non empty set
bool [:( the Sorts of X . (the_result_sort_of a9)),( the Sorts of X . (the_result_sort_of a9)):] is non empty set
i is Relation-like Function-like Element of Args (a9,X)
dom i is set
i9 is Relation-like Function-like Element of Args (a9,X)
(Den (a9,X)) . i is Element of Result (a9,X)
(Den (a9,X)) . i9 is Element of Result (a9,X)
[((Den (a9,X)) . i),((Den (a9,X)) . i9)] is set
the ResultSort 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
dom the ResultSort of x is set
the ResultSort of x * the Sorts of X is Relation-like non-empty Function-like set
( the ResultSort of x * the Sorts of X) . a9 is set
the ResultSort of x . a9 is Element of the carrier of x
the Sorts of X . ( the ResultSort of x . a9) is non empty set
x is non empty non void V71() ManySortedSign
X is non-empty MSAlgebra over x
(x,X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like SubLattice of ( the carrier of x, the Sorts of X)
the carrier of x is non empty set
the Sorts of X is Relation-like non-empty non empty-yielding the carrier of x -defined Function-like non empty total set
( the carrier of x, the Sorts of X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (x,X) is non empty set
[| the Sorts of X, the Sorts of X|] is Relation-like the carrier of x -defined Function-like non empty total set
the L_join of (x,X) is Relation-like Function-like V18([: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X)) Element of bool [:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):]
[: the carrier of (x,X), the carrier of (x,X):] is Relation-like non empty set
[:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):] is Relation-like non empty set
bool [:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):] is non empty set
the L_join of ( the carrier of x, the Sorts of X) is Relation-like Function-like V18([: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):]
the carrier of ( the carrier of x, the Sorts of X) is non empty set
[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
[:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is non empty set
the L_join of ( the carrier of x, the Sorts of X) || the carrier of (x,X) is set
the L_join of ( the carrier of x, the Sorts of X) | [: the carrier of (x,X), the carrier of (x,X):] is Relation-like Function-like 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
K is Element of the carrier of (x,X)
a is Element of the carrier of (x,X)
K "\/" a is Element of the carrier of (x,X)
a "\/" K is Element of the carrier of (x,X)
[K,a] is set
a9 is set
K9 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 \/ K9 is Relation-like the carrier of x -defined Function-like non empty total set
( the carrier of x, the Sorts of X,K,K9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
the Sorts of X . a9 is set
[:( the Sorts of X . a9),( the Sorts of X . a9):] is Relation-like set
bool [:( the Sorts of X . a9),( the Sorts of X . a9):] is non empty set
i is Element of the carrier of x
K . i is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
the Sorts of X . i is non empty set
[:( the Sorts of X . i),( the Sorts of X . i):] is Relation-like non empty set
bool [:( the Sorts of X . i),( the Sorts of X . i):] is non empty set
K9 . i is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
(K \/ K9) . a9 is set
K . a9 is set
K9 . a9 is set
(K . a9) \/ (K9 . a9) is set
nabla ( the Sorts of X . a9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . a9),( the Sorts of X . a9):]
K2 is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . a9),( the Sorts of X . a9):]
(nabla ( the Sorts of X . a9)) \/ K2 is Relation-like reflexive symmetric Element of bool [:( the Sorts of X . a9),( the Sorts of X . a9):]
( the carrier of x, the Sorts of X,K,K9) . a9 is set
i9 is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . a9),( the Sorts of X . a9):]
(( the Sorts of X . a9),i9) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . a9),( the Sorts of X . a9):]
a2 is Relation-like the carrier of x -defined Function-like non empty total V95() ManySortedRelation of the Sorts of X, the Sorts of X
( the carrier of x, the Sorts of X,a2) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
the L_join of (x,X) . (K,a) is Element of the carrier of (x,X)
the L_join of (x,X) . [K,a] is set
the L_join of ( the carrier of x, the Sorts of X) . (K,a) is set
the L_join of ( the carrier of x, the Sorts of X) . [K,a] is set
K is Element of the carrier of (x,X)
id the Sorts of X is Relation-like the carrier of x -defined Function-like non empty total V94() ManySortedFunction of the Sorts of X, the Sorts of X
the L_meet of (x,X) is Relation-like Function-like V18([: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X)) Element of bool [:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):]
[: the carrier of (x,X), the carrier of (x,X):] is Relation-like non empty set
[:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):] is Relation-like non empty set
bool [:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):] is non empty set
the L_meet of ( the carrier of x, the Sorts of X) is Relation-like Function-like V18([: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):]
the carrier of ( the carrier of x, the Sorts of X) is non empty set
[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
[:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is non empty set
the L_meet of ( the carrier of x, the Sorts of X) || the carrier of (x,X) is set
the L_meet of ( the carrier of x, the Sorts of X) | [: the carrier of (x,X), the carrier of (x,X):] is Relation-like Function-like 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
K is Element of the carrier of (x,X)
a is Element of the carrier of (x,X)
K "/\" a is Element of the carrier of (x,X)
a "/\" K is Element of the carrier of (x,X)
[K,a] is set
a9 is set
the Sorts of X . a9 is set
[:( the Sorts of X . a9),( the Sorts of X . a9):] is Relation-like set
bool [:( the Sorts of X . a9),( the Sorts of X . a9):] is non empty set
K9 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
i is Element of the carrier of x
K9 . i is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
the Sorts of X . i is non empty set
[:( the Sorts of X . i),( the Sorts of X . i):] is Relation-like non empty set
bool [:( the Sorts of X . i),( the Sorts of X . i):] is non empty set
K /\ K9 is Relation-like the carrier of x -defined Function-like non empty total set
(K /\ K9) . a9 is set
K . a9 is set
K9 . a9 is set
(K . a9) /\ (K9 . a9) is set
id ( the Sorts of X . a9) is Relation-like the Sorts of X . a9 -defined the Sorts of X . a9 -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of X . a9),( the Sorts of X . a9):]
i9 is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . a9),( the Sorts of X . a9):]
(id ( the Sorts of X . a9)) /\ i9 is Relation-like total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of X . a9),( the Sorts of X . a9):]
the L_meet of (x,X) . (K,a) is Element of the carrier of (x,X)
the L_meet of (x,X) . [K,a] is set
the L_meet of ( the carrier of x, the Sorts of X) . (K,a) is set
the L_meet of ( the carrier of x, the Sorts of X) . [K,a] is set
K is Element of the carrier of (x,X)
x is non empty non void V71() ManySortedSign
the carrier of x is non empty set
X is non-empty MSAlgebra over x
(x,X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded SubLattice of ( the carrier of x, the Sorts of X)
the Sorts of X is Relation-like non-empty non empty-yielding the carrier of x -defined Function-like non empty total set
( the carrier of x, the Sorts of X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Bottom (x,X) is Element of the carrier of (x,X)
the carrier of (x,X) is non empty set
id the Sorts of X is Relation-like the carrier of x -defined Function-like non empty total V94() ManySortedFunction of the Sorts of X, the Sorts of X
the L_meet of (x,X) is Relation-like Function-like V18([: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X)) Element of bool [:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):]
[: the carrier of (x,X), the carrier of (x,X):] is Relation-like non empty set
[:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):] is Relation-like non empty set
bool [:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):] is non empty set
the L_meet of ( the carrier of x, the Sorts of X) is Relation-like Function-like V18([: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):]
the carrier of ( the carrier of x, the Sorts of X) is non empty set
[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
[:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is non empty set
the L_meet of ( the carrier of x, the Sorts of X) || the carrier of (x,X) is set
the L_meet of ( the carrier of x, the Sorts of X) | [: the carrier of (x,X), the carrier of (x,X):] is Relation-like Function-like set
K is Element of the carrier of (x,X)
a is Element of the carrier of (x,X)
[K,a] is set
i is set
the Sorts of X . i is set
[:( the Sorts of X . i),( the Sorts of X . i):] is Relation-like set
bool [:( the Sorts of X . i),( the Sorts of X . i):] is non empty set
a9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
i9 is Element of the carrier of x
a9 . i9 is Relation-like Element of bool [:( the Sorts of X . i9),( the Sorts of X . i9):]
the Sorts of X . i9 is non empty set
[:( the Sorts of X . i9),( the Sorts of X . i9):] is Relation-like non empty set
bool [:( the Sorts of X . i9),( the Sorts of X . i9):] is non empty set
K9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
K9 /\ a9 is Relation-like the carrier of x -defined Function-like non empty total set
(K9 /\ a9) . i is set
K9 . i is set
a9 . i is set
(K9 . i) /\ (a9 . i) is set
id ( the Sorts of X . i) is Relation-like the Sorts of X . i -defined the Sorts of X . i -valued Function-like one-to-one total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
K2 is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
(id ( the Sorts of X . i)) /\ K2 is Relation-like total reflexive symmetric antisymmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
K "/\" a is Element of the carrier of (x,X)
the L_meet of (x,X) . (K,a) is Element of the carrier of (x,X)
the L_meet of (x,X) . [K,a] is set
the L_meet of ( the carrier of x, the Sorts of X) . (K,a) is set
the L_meet of ( the carrier of x, the Sorts of X) . [K,a] is set
a "/\" K is Element of the carrier of (x,X)
x is non empty non void V71() ManySortedSign
the carrier of x is non empty set
X is non-empty MSAlgebra over x
(x,X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded SubLattice of ( the carrier of x, the Sorts of X)
the Sorts of X is Relation-like non-empty non empty-yielding the carrier of x -defined Function-like non empty total set
( the carrier of x, the Sorts of X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
Top (x,X) is Element of the carrier of (x,X)
the carrier of (x,X) is non empty set
[| the Sorts of X, the Sorts of X|] is Relation-like the carrier of x -defined Function-like non empty total set
the L_join of (x,X) is Relation-like Function-like V18([: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X)) Element of bool [:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):]
[: the carrier of (x,X), the carrier of (x,X):] is Relation-like non empty set
[:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):] is Relation-like non empty set
bool [:[: the carrier of (x,X), the carrier of (x,X):], the carrier of (x,X):] is non empty set
the L_join of ( the carrier of x, the Sorts of X) is Relation-like Function-like V18([: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X)) Element of bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):]
the carrier of ( the carrier of x, the Sorts of X) is non empty set
[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
[:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is Relation-like non empty set
bool [:[: the carrier of ( the carrier of x, the Sorts of X), the carrier of ( the carrier of x, the Sorts of X):], the carrier of ( the carrier of x, the Sorts of X):] is non empty set
the L_join of ( the carrier of x, the Sorts of X) || the carrier of (x,X) is set
the L_join of ( the carrier of x, the Sorts of X) | [: the carrier of (x,X), the carrier of (x,X):] is Relation-like Function-like set
K is Element of the carrier of (x,X)
a is Element of the carrier of (x,X)
[K,a] is set
i is set
K9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
a9 is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
K9 \/ a9 is Relation-like the carrier of x -defined Function-like non empty total set
( the carrier of x, the Sorts of X,K9,a9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
the Sorts of X . i is set
[:( the Sorts of X . i),( the Sorts of X . i):] is Relation-like set
bool [:( the Sorts of X . i),( the Sorts of X . i):] is non empty set
i9 is Element of the carrier of x
K9 . i9 is Relation-like Element of bool [:( the Sorts of X . i9),( the Sorts of X . i9):]
the Sorts of X . i9 is non empty set
[:( the Sorts of X . i9),( the Sorts of X . i9):] is Relation-like non empty set
bool [:( the Sorts of X . i9),( the Sorts of X . i9):] is non empty set
a9 . i9 is Relation-like Element of bool [:( the Sorts of X . i9),( the Sorts of X . i9):]
(K9 \/ a9) . i is set
K9 . i is set
a9 . i is set
(K9 . i) \/ (a9 . i) is set
nabla ( the Sorts of X . i) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
a2 is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
(nabla ( the Sorts of X . i)) \/ a2 is Relation-like reflexive symmetric Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
( the carrier of x, the Sorts of X,K9,a9) . i is set
K2 is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
(( the Sorts of X . i),K2) is Relation-like total reflexive symmetric transitive Element of bool [:( the Sorts of X . i),( the Sorts of X . i):]
y9 is Relation-like the carrier of x -defined Function-like non empty total V95() ManySortedRelation of the Sorts of X, the Sorts of X
( the carrier of x, the Sorts of X,y9) is Relation-like the carrier of x -defined Function-like non empty total V95() MSEquivalence_Relation-like ManySortedRelation of the Sorts of X, the Sorts of X
K "\/" a is Element of the carrier of (x,X)
the L_join of (x,X) . (K,a) is Element of the carrier of (x,X)
the L_join of (x,X) . [K,a] is set
the L_join of ( the carrier of x, the Sorts of X) . (K,a) is set
the L_join of ( the carrier of x, the Sorts of X) . [K,a] is set
a "\/" K is Element of the carrier of (x,X)
x is set
X is set
(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
[: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
K is Relation-like Element of bool [:X,X:]