REAL is V35() V36() V37() V41() set
NAT is V35() V36() V37() V38() V39() V40() V41() Element of bool REAL
bool REAL is non empty set
NAT is V35() V36() V37() V38() V39() V40() V41() set
bool NAT is non empty set
bool NAT is non empty set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is non empty set
K288() is non empty strict LattStr
the carrier of K288() is non empty set
K291() is V35() V36() V37() V38() V39() V40() Element of bool NAT
[:K291(),K291():] is set
[:[:K291(),K291():],K291():] is set
bool [:[:K291(),K291():],K291():] is non empty set
{} is set
the Function-like functional empty V35() V36() V37() V38() V39() V40() V41() finite V46() set is Function-like functional empty V35() V36() V37() V38() V39() V40() V41() finite V46() set
1 is non empty V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
0 is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
S is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
S + 1 is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
A is Relation-like Function-like FinSequence-like set
len A is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
dom A is V35() V36() V37() V38() V39() V40() Element of bool NAT
Seg (len A) is V35() V36() V37() V38() V39() V40() Element of bool NAT
Seg (len A) is V35() V36() V37() V38() V39() V40() Element of bool NAT
F1() is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
Seg F1() is V35() V36() V37() V38() V39() V40() Element of bool NAT
S is set
S is Relation-like Function-like set
dom S is set
A is Relation-like Function-like FinSequence-like set
dom A is V35() V36() V37() V38() V39() V40() Element of bool NAT
E is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
A . E is set
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (EqRelLatt S) is non empty set
[:S,S:] is set
bool [:S,S:] is non empty set
A is Element of the carrier of (EqRelLatt S)
E is Element of the carrier of (EqRelLatt S)
C is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
B is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
C /\ B is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
the L_meet of (EqRelLatt S) is Relation-like [: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] -defined the carrier of (EqRelLatt S) -valued Function-like V18([: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S)) Element of bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):]
[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] is non empty set
[:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
the L_meet of (EqRelLatt S) . (C,B) is set
A "/\" E is Element of the carrier of (EqRelLatt S)
A "/\" E is Element of the carrier of (EqRelLatt S)
the L_meet of (EqRelLatt S) is Relation-like [: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] -defined the carrier of (EqRelLatt S) -valued Function-like V18([: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S)) Element of bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):]
[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] is non empty set
[:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
the L_meet of (EqRelLatt S) . (C,B) is set
C /\ B is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (EqRelLatt S) is non empty set
nabla S is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
[:S,S:] is set
bool [:S,S:] is non empty set
E is Element of the carrier of (EqRelLatt S)
C is Element of the carrier of (EqRelLatt S)
E "\/" C is Element of the carrier of (EqRelLatt S)
C "\/" E is Element of the carrier of (EqRelLatt S)
the L_join of (EqRelLatt S) is Relation-like [: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] -defined the carrier of (EqRelLatt S) -valued Function-like V18([: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S)) Element of bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):]
[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] is non empty set
[:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
the L_join of (EqRelLatt S) . (E,C) is Element of the carrier of (EqRelLatt S)
B is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
(nabla S) "\/" B is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
(nabla S) \/ B is Relation-like S -defined S -valued Element of bool [:S,S:]
EqCl ((nabla S) \/ B) is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
EqCl (nabla S) is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
A is Element of the carrier of (EqRelLatt S)
id S is Relation-like S -defined S -valued Function-like one-to-one total V121() V123() V124() V128() Element of bool [:S,S:]
[:S,S:] is set
bool [:S,S:] is non empty set
E is Element of the carrier of (EqRelLatt S)
C is Element of the carrier of (EqRelLatt S)
E "/\" C is Element of the carrier of (EqRelLatt S)
C "/\" E is Element of the carrier of (EqRelLatt S)
the L_meet of (EqRelLatt S) is Relation-like [: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] -defined the carrier of (EqRelLatt S) -valued Function-like V18([: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S)) Element of bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):]
[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] is non empty set
[:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
the L_meet of (EqRelLatt S) . (E,C) is Element of the carrier of (EqRelLatt S)
B is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
(id S) /\ B is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
A is Element of the carrier of (EqRelLatt S)
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Bottom (EqRelLatt S) is Element of the carrier of (EqRelLatt S)
the carrier of (EqRelLatt S) is non empty set
id S is Relation-like S -defined S -valued Function-like one-to-one total V121() V123() V124() V128() Element of bool [:S,S:]
[:S,S:] is set
bool [:S,S:] is non empty set
E is Element of the carrier of (EqRelLatt S)
A is Element of the carrier of (EqRelLatt S)
A "/\" E is Element of the carrier of (EqRelLatt S)
the L_meet of (EqRelLatt S) is Relation-like [: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] -defined the carrier of (EqRelLatt S) -valued Function-like V18([: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S)) Element of bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):]
[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] is non empty set
[:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
the L_meet of (EqRelLatt S) . (A,E) is Element of the carrier of (EqRelLatt S)
C is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
(id S) /\ C is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
E "/\" A is Element of the carrier of (EqRelLatt S)
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
Top (EqRelLatt S) is Element of the carrier of (EqRelLatt S)
the carrier of (EqRelLatt S) is non empty set
nabla S is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
[:S,S:] is set
bool [:S,S:] is non empty set
E is Element of the carrier of (EqRelLatt S)
A is Element of the carrier of (EqRelLatt S)
A "\/" E is Element of the carrier of (EqRelLatt S)
the L_join of (EqRelLatt S) is Relation-like [: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] -defined the carrier of (EqRelLatt S) -valued Function-like V18([: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S)) Element of bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):]
[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):] is non empty set
[:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
bool [:[: the carrier of (EqRelLatt S), the carrier of (EqRelLatt S):], the carrier of (EqRelLatt S):] is non empty set
the L_join of (EqRelLatt S) . (A,E) is Element of the carrier of (EqRelLatt S)
C is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
(nabla S) "\/" C is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
(nabla S) \/ C is Relation-like S -defined S -valued Element of bool [:S,S:]
EqCl ((nabla S) \/ C) is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
EqCl (nabla S) is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
E "\/" A is Element of the carrier of (EqRelLatt S)
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
the carrier of (EqRelLatt S) is non empty set
bool the carrier of (EqRelLatt S) is non empty set
A is Element of bool the carrier of (EqRelLatt S)
Top (EqRelLatt S) is Element of the carrier of (EqRelLatt S)
E is Element of the carrier of (EqRelLatt S)
C is Element of the carrier of (EqRelLatt S)
C is Element of the carrier of (EqRelLatt S)
meet A is set
[:S,S:] is set
bool [:S,S:] is non empty Element of bool (bool [:S,S:])
bool [:S,S:] is non empty set
bool (bool [:S,S:]) is non empty set
C is set
B is set
C is Element of bool (bool [:S,S:])
meet C is Relation-like S -defined S -valued Element of bool [:S,S:]
B is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
V is Element of the carrier of (EqRelLatt S)
V is Element of the carrier of (EqRelLatt S)
V is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
V is Element of the carrier of (EqRelLatt S)
V is set
V is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
s2 is set
t is Element of the carrier of (EqRelLatt S)
t9 is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
V is Element of the carrier of (EqRelLatt S)
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded LattStr
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt S) is non empty set
bool the carrier of (EqRelLatt S) is non empty set
[:S,S:] is set
bool [:S,S:] is non empty set
A is Element of bool the carrier of (EqRelLatt S)
union A is set
E is set
C is set
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt S) is non empty set
bool the carrier of (EqRelLatt S) is non empty set
A is Element of bool the carrier of (EqRelLatt S)
union A is set
"\/" (A,(EqRelLatt S)) is Element of the carrier of (EqRelLatt S)
[:S,S:] is set
bool [:S,S:] is non empty set
C is set
B is set
d is Element of the carrier of (EqRelLatt S)
V is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
E is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt S) is non empty set
bool the carrier of (EqRelLatt S) is non empty set
[:S,S:] is set
bool [:S,S:] is non empty set
A is Element of bool the carrier of (EqRelLatt S)
union A is set
"\/" (A,(EqRelLatt S)) is Element of the carrier of (EqRelLatt S)
E is Relation-like S -defined S -valued Element of bool [:S,S:]
EqCl E is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
B is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
V is Element of the carrier of (EqRelLatt S)
V is set
V is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
d is Element of the carrier of (EqRelLatt S)
C is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
S is set
EqRelLatt S is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt S) is non empty set
bool the carrier of (EqRelLatt S) is non empty set
A is Element of bool the carrier of (EqRelLatt S)
union A is set
E is Relation-like set
E ~ is Relation-like set
C is set
B is set
[C,B] is set
{C,B} is finite set
{C} is finite set
{{C,B},{C}} is finite V46() set
d is set
[:S,S:] is set
bool [:S,S:] is non empty set
[B,C] is set
{B,C} is finite set
{B} is finite set
{{B,C},{B}} is finite V46() set
V is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
[B,C] is set
{B,C} is finite set
{B} is finite set
{{B,C},{B}} is finite V46() set
d is set
[:S,S:] is set
bool [:S,S:] is non empty set
V is Relation-like S -defined S -valued total V121() V123() V128() Element of bool [:S,S:]
S is set
A is set
[S,A] is set
{S,A} is finite set
{S} is finite set
{{S,A},{S}} is finite V46() set
E is set
EqRelLatt E is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt E) is non empty set
bool the carrier of (EqRelLatt E) is non empty set
C is Element of bool the carrier of (EqRelLatt E)
"\/" (C,(EqRelLatt E)) is Element of the carrier of (EqRelLatt E)
union C is set
B is non empty set
[:B,B:] is non empty set
bool [:B,B:] is non empty set
V is Relation-like B -defined B -valued Element of bool [:B,B:]
V ~ is Relation-like B -defined B -valued Element of bool [:B,B:]
V \/ (V ~) is Relation-like B -defined B -valued Element of bool [:B,B:]
d is Element of B
V is Element of B
[d,V] is Element of [:B,B:]
{d,V} is finite set
{d} is finite set
{{d,V},{d}} is finite V46() set
EqCl V is Relation-like B -defined B -valued total V121() V123() V128() Element of bool [:B,B:]
V is Relation-like Function-like FinSequence-like set
len V is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
V . 1 is set
V . (len V) is set
dom V is V35() V36() V37() V38() V39() V40() Element of bool NAT
0 + 1 is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
V is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
V . V is set
V + 1 is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
V . (V + 1) is set
[(V . V),(V . (V + 1))] is set
{(V . V),(V . (V + 1))} is finite set
{(V . V)} is finite set
{{(V . V),(V . (V + 1))},{(V . V)}} is finite V46() set
d is Element of B
V is Element of B
[d,V] is Element of [:B,B:]
{d,V} is finite set
{d} is finite set
{{d,V},{d}} is finite V46() set
EqCl V is Relation-like B -defined B -valued total V121() V123() V128() Element of bool [:B,B:]
V is Relation-like Function-like FinSequence-like set
len V is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
V . 1 is set
V . (len V) is set
V is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
dom V is V35() V36() V37() V38() V39() V40() Element of bool NAT
V + 1 is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
V . V is set
V . (V + 1) is set
[(V . V),(V . (V + 1))] is set
{(V . V),(V . (V + 1))} is finite set
{(V . V)} is finite set
{{(V . V),(V . (V + 1))},{(V . V)}} is finite V46() set
0 + 1 is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
CongrLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded M24( EqRelLatt the Sorts of A)
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (CongrLatt A) is non empty set
bool the carrier of (CongrLatt A) is non empty set
d is Element of bool the carrier of (CongrLatt A)
"/\" (d,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
the carrier of (EqRelLatt the Sorts of A) is non empty set
V is Relation-like the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
bool the carrier of (EqRelLatt the Sorts of A) is non empty set
[| the Sorts of A, the Sorts of A|] is Relation-like the carrier of S -defined Function-like non empty total set
Bool [| the Sorts of A, the Sorts of A|] is functional non empty with_common_domain set
bool (Bool [| the Sorts of A, the Sorts of A|]) is non empty set
V is Element of bool the carrier of (EqRelLatt the Sorts of A)
t is Function-like functional empty proper V35() V36() V37() V38() V39() V40() V41() finite V46() V114( CongrLatt A) final meet-closed join-closed Element of bool the carrier of (CongrLatt A)
Top (EqRelLatt the Sorts of A) is Element of the carrier of (EqRelLatt the Sorts of A)
t9 is Element of the carrier of (EqRelLatt the Sorts of A)
t9 is Element of the carrier of (EqRelLatt the Sorts of A)
the carrier' of S is non empty set
V is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
s2 is functional Element of bool (Bool [| the Sorts of A, the Sorts of A|])
|:s2:| is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of K196( the carrier of S,[| the Sorts of A, the Sorts of A|])
K196( the carrier of S,[| the Sorts of A, the Sorts of A|]) is Relation-like the carrier of S -defined Function-like non empty total set
meet |:s2:| is Relation-like the carrier of S -defined Function-like non empty total ManySortedSubset of [| the Sorts of A, the Sorts of A|]
a is Element of the carrier' of S
Args (a,A) is functional non empty Element of rng K302( the carrier of S, the Sorts of A)
K302( the carrier of S, the Sorts of A) is Relation-like K299( the carrier of S) -defined Function-like total set
K299( the carrier of S) is M25( the carrier of S)
rng K302( the carrier of S, the Sorts of A) is set
the_arity_of a is Relation-like NAT -defined the carrier of S -valued Function-like FinSequence-like M26( the carrier of S,K299( the carrier of S))
Result (a,A) is non empty Element of rng the Sorts of A
rng the Sorts of A is with_non-empty_elements set
Den (a,A) is Relation-like Args (a,A) -defined Result (a,A) -valued Function-like V18( Args (a,A), Result (a,A)) Element of bool [:(Args (a,A)),(Result (a,A)):]
[:(Args (a,A)),(Result (a,A)):] is non empty set
bool [:(Args (a,A)),(Result (a,A)):] is non empty set
the_result_sort_of a is Element of the carrier of S
V . (the_result_sort_of a) is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued non empty total V121() V123() V128() Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
the Sorts of A . (the_result_sort_of a) is non empty set
[:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):] is non empty set
bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):] is non empty set
b is Relation-like Function-like Element of Args (a,A)
dom b is set
f is Relation-like Function-like Element of Args (a,A)
(Den (a,A)) . b is Element of Result (a,A)
(Den (a,A)) . f is Element of Result (a,A)
[((Den (a,A)) . b),((Den (a,A)) . f)] is Element of [:(Result (a,A)),(Result (a,A)):]
[:(Result (a,A)),(Result (a,A)):] is non empty set
{((Den (a,A)) . b),((Den (a,A)) . f)} is finite set
{((Den (a,A)) . b)} is finite set
{{((Den (a,A)) . b),((Den (a,A)) . f)},{((Den (a,A)) . b)}} is finite V46() set
t is functional non empty Element of bool (Bool [| the Sorts of A, the Sorts of A|])
|:t:| is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total ManySortedSubset of K196( the carrier of S,[| the Sorts of A, the Sorts of A|])
g is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
j is V30() set
b . j is set
f . j is set
[(b . j),(f . j)] is set
{(b . j),(f . j)} is finite set
{(b . j)} is finite set
{{(b . j),(f . j)},{(b . j)}} is finite V46() set
(the_arity_of a) /. j is Element of the carrier of S
V . ((the_arity_of a) /. j) is Relation-like the Sorts of A . ((the_arity_of a) /. j) -defined the Sorts of A . ((the_arity_of a) /. j) -valued non empty total V121() V123() V128() Element of bool [:( the Sorts of A . ((the_arity_of a) /. j)),( the Sorts of A . ((the_arity_of a) /. j)):]
the Sorts of A . ((the_arity_of a) /. j) is non empty set
[:( the Sorts of A . ((the_arity_of a) /. j)),( the Sorts of A . ((the_arity_of a) /. j)):] is non empty set
bool [:( the Sorts of A . ((the_arity_of a) /. j)),( the Sorts of A . ((the_arity_of a) /. j)):] is non empty set
t9 is Relation-like the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
t9 . ((the_arity_of a) /. j) is Relation-like the Sorts of A . ((the_arity_of a) /. j) -defined the Sorts of A . ((the_arity_of a) /. j) -valued Element of bool [:( the Sorts of A . ((the_arity_of a) /. j)),( the Sorts of A . ((the_arity_of a) /. j)):]
g . ((the_arity_of a) /. j) is Relation-like the Sorts of A . ((the_arity_of a) /. j) -defined the Sorts of A . ((the_arity_of a) /. j) -valued non empty total V121() V123() V128() Element of bool [:( the Sorts of A . ((the_arity_of a) /. j)),( the Sorts of A . ((the_arity_of a) /. j)):]
g . (the_result_sort_of a) is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued non empty total V121() V123() V128() Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
|:s2:| . (the_result_sort_of a) is Element of bool (bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of a)))
[| the Sorts of A, the Sorts of A|] . (the_result_sort_of a) is set
bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of a)) is non empty set
bool (bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of a))) is non empty set
Bool [| the Sorts of A, the Sorts of A|] is functional non empty with_common_domain V153( the carrier of S,[| the Sorts of A, the Sorts of A|]) V154( the carrier of S,[| the Sorts of A, the Sorts of A|]) V155( the carrier of S,[| the Sorts of A, the Sorts of A|]) V156( the carrier of S,[| the Sorts of A, the Sorts of A|]) V157( the carrier of S,[| the Sorts of A, the Sorts of A|]) V158( the carrier of S,[| the Sorts of A, the Sorts of A|]) Element of bool (Bool [| the Sorts of A, the Sorts of A|])
{ (b1 . (the_result_sort_of a)) where b1 is Relation-like the carrier of S -defined Function-like non empty total Element of Bool [| the Sorts of A, the Sorts of A|] : b1 in d } is set
g is set
j is Relation-like the carrier of S -defined Function-like non empty total Element of Bool [| the Sorts of A, the Sorts of A|]
j . (the_result_sort_of a) is set
Z is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
Z . (the_result_sort_of a) is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued non empty total V121() V123() V128() Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
t9 . (the_result_sort_of a) is Relation-like the Sorts of A . (the_result_sort_of a) -defined the Sorts of A . (the_result_sort_of a) -valued Element of bool [:( the Sorts of A . (the_result_sort_of a)),( the Sorts of A . (the_result_sort_of a)):]
meet (|:s2:| . (the_result_sort_of a)) is Element of bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of a))
g is Element of bool (bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of a)))
Intersect g is Element of bool ([| the Sorts of A, the Sorts of A|] . (the_result_sort_of a))
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt the Sorts of A) is non empty set
E is Element of the carrier of (EqRelLatt the Sorts of A)
{ b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & E [= b1 ) } is set
"/\" ( { b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & E [= b1 ) } ,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
B is set
CongrLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded M24( EqRelLatt the Sorts of A)
the carrier of (CongrLatt A) is non empty set
d is Element of the carrier of (EqRelLatt the Sorts of A)
bool the carrier of (CongrLatt A) is non empty set
B is Element of bool the carrier of (CongrLatt A)
"/\" (B,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt the Sorts of A) is non empty set
bool the carrier of (EqRelLatt the Sorts of A) is non empty set
E is Element of bool the carrier of (EqRelLatt the Sorts of A)
{ b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & E is_less_than b1 ) } is set
"/\" ( { b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & E is_less_than b1 ) } ,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
B is set
CongrLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded M24( EqRelLatt the Sorts of A)
the carrier of (CongrLatt A) is non empty set
d is Element of the carrier of (EqRelLatt the Sorts of A)
bool the carrier of (CongrLatt A) is non empty set
B is Element of bool the carrier of (CongrLatt A)
"/\" (B,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt the Sorts of A) is non empty set
E is Element of the carrier of (EqRelLatt the Sorts of A)
(S,A,E) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
{ b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & E [= b1 ) } is set
"/\" ( { b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & E [= b1 ) } ,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
B is Element of the carrier of (EqRelLatt the Sorts of A)
d is Element of the carrier of (EqRelLatt the Sorts of A)
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt the Sorts of A) is non empty set
bool the carrier of (EqRelLatt the Sorts of A) is non empty set
E is Element of bool the carrier of (EqRelLatt the Sorts of A)
"\/" (E,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
(S,A,("\/" (E,(EqRelLatt the Sorts of A)))) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
{ b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & "\/" (E,(EqRelLatt the Sorts of A)) [= b1 ) } is set
"/\" ( { b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & "\/" (E,(EqRelLatt the Sorts of A)) [= b1 ) } ,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
(S,A,E) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
{ b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & E is_less_than b1 ) } is set
"/\" ( { b1 where b1 is Element of the carrier of (EqRelLatt the Sorts of A) : ( b1 is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A & E is_less_than b1 ) } ,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
d is set
V is Element of the carrier of (EqRelLatt the Sorts of A)
V is Element of the carrier of (EqRelLatt the Sorts of A)
d is set
V is Element of the carrier of (EqRelLatt the Sorts of A)
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
CongrLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded M24( EqRelLatt the Sorts of A)
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (CongrLatt A) is non empty set
bool the carrier of (CongrLatt A) is non empty set
E is Element of bool the carrier of (CongrLatt A)
"\/" (E,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
the carrier of (EqRelLatt the Sorts of A) is non empty set
C is Element of bool the carrier of (CongrLatt A)
"\/" (C,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
E \/ C is Element of bool the carrier of (CongrLatt A)
"\/" ((E \/ C),(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
B is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
d is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
B "\/" d is Relation-like the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
bool the carrier of (EqRelLatt the Sorts of A) is non empty set
V is Element of bool the carrier of (EqRelLatt the Sorts of A)
"\/" (V,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
V is Element of bool the carrier of (EqRelLatt the Sorts of A)
"\/" (V,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
{("\/" (V,(EqRelLatt the Sorts of A))),("\/" (V,(EqRelLatt the Sorts of A)))} is finite Element of bool the carrier of (EqRelLatt the Sorts of A)
{E,C} is finite Element of bool (bool the carrier of (CongrLatt A))
bool (bool the carrier of (CongrLatt A)) is non empty set
{ ("\/" (b1,(EqRelLatt the Sorts of A))) where b1 is Element of bool the carrier of (EqRelLatt the Sorts of A) : b1 in {E,C} } is set
V is set
V is set
s2 is Element of bool the carrier of (EqRelLatt the Sorts of A)
"\/" (s2,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
V is set
bool the carrier of (EqRelLatt the Sorts of A) is non empty Element of bool (bool the carrier of (EqRelLatt the Sorts of A))
bool (bool the carrier of (EqRelLatt the Sorts of A)) is non empty set
union {E,C} is Element of bool the carrier of (CongrLatt A)
"\/" ((union {E,C}),(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
"\/" ( { ("\/" (b1,(EqRelLatt the Sorts of A))) where b1 is Element of bool the carrier of (EqRelLatt the Sorts of A) : b1 in {E,C} } ,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
("\/" (V,(EqRelLatt the Sorts of A))) "\/" ("\/" (V,(EqRelLatt the Sorts of A))) is Element of the carrier of (EqRelLatt the Sorts of A)
the L_join of (EqRelLatt the Sorts of A) is Relation-like [: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):] -defined the carrier of (EqRelLatt the Sorts of A) -valued Function-like V18([: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):], the carrier of (EqRelLatt the Sorts of A)) Element of bool [:[: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):], the carrier of (EqRelLatt the Sorts of A):]
[: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):] is non empty set
[:[: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):], the carrier of (EqRelLatt the Sorts of A):] is non empty set
bool [:[: the carrier of (EqRelLatt the Sorts of A), the carrier of (EqRelLatt the Sorts of A):], the carrier of (EqRelLatt the Sorts of A):] is non empty set
the L_join of (EqRelLatt the Sorts of A) . (B,d) is set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
CongrLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded M24( EqRelLatt the Sorts of A)
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (CongrLatt A) is non empty set
bool the carrier of (CongrLatt A) is non empty set
the carrier of (EqRelLatt the Sorts of A) is non empty set
bool the carrier of (EqRelLatt the Sorts of A) is non empty set
E is Element of bool the carrier of (CongrLatt A)
"\/" (E,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
bool E is non empty set
{ ("\/" (b1,(EqRelLatt the Sorts of A))) where b1 is Element of bool the carrier of (EqRelLatt the Sorts of A) : b1 is finite Element of bool E } is set
"\/" ( { ("\/" (b1,(EqRelLatt the Sorts of A))) where b1 is Element of bool the carrier of (EqRelLatt the Sorts of A) : b1 is finite Element of bool E } ,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
{ b1 where b1 is Element of bool the carrier of (EqRelLatt the Sorts of A) : b1 is finite Element of bool E } is set
{ ("\/" (b1,(EqRelLatt the Sorts of A))) where b1 is Element of bool the carrier of (EqRelLatt the Sorts of A) : b1 in { b1 where b2 is Element of bool the carrier of (EqRelLatt the Sorts of A) : b1 is finite Element of bool E } } is set
V is set
V is Element of bool the carrier of (EqRelLatt the Sorts of A)
"\/" (V,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
union { b1 where b1 is Element of bool the carrier of (EqRelLatt the Sorts of A) : b1 is finite Element of bool E } is set
V is set
V is Element of the carrier of (CongrLatt A)
V is Element of the carrier of (EqRelLatt the Sorts of A)
{V} is finite Element of bool the carrier of (EqRelLatt the Sorts of A)
{V} is finite set
V is set
V is set
V is Element of bool the carrier of (EqRelLatt the Sorts of A)
V is set
bool the carrier of (EqRelLatt the Sorts of A) is non empty Element of bool (bool the carrier of (EqRelLatt the Sorts of A))
bool (bool the carrier of (EqRelLatt the Sorts of A)) is non empty set
V is Element of bool the carrier of (EqRelLatt the Sorts of A)
V is set
V is Element of bool the carrier of (EqRelLatt the Sorts of A)
"\/" (V,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
V is Element of bool the carrier of (EqRelLatt the Sorts of A)
S is non empty set
A is Relation-like S -defined Function-like non empty total set
E is Element of S
A . E is set
[:(A . E),(A . E):] is set
bool [:(A . E),(A . E):] is non empty set
C is Relation-like A . E -defined A . E -valued total V121() V123() V128() Element of bool [:(A . E),(A . E):]
B is Relation-like Function-like set
dom B is set
V is set
d is Relation-like S -defined Function-like non empty total set
d . V is set
A . V is set
[:(A . V),(A . V):] is set
bool [:(A . V),(A . V):] is non empty set
d is Relation-like S -defined Function-like non empty total set
d . V is set
A . V is set
nabla (A . V) is Relation-like A . V -defined A . V -valued total V121() V123() V128() Element of bool [:(A . V),(A . V):]
[:(A . V),(A . V):] is set
bool [:(A . V),(A . V):] is non empty set
d is Relation-like S -defined Function-like non empty total set
d is Relation-like S -defined Function-like non empty total set
V is set
A . V is set
[:(A . V),(A . V):] is set
bool [:(A . V),(A . V):] is non empty set
V is Relation-like S -defined Function-like non empty total ManySortedRelation of A,A
V . V is set
V is Relation-like A . V -defined A . V -valued Element of bool [:(A . V),(A . V):]
nabla (A . V) is Relation-like A . V -defined A . V -valued total V121() V123() V128() Element of bool [:(A . V),(A . V):]
V is Relation-like S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of A,A
V . E is Relation-like A . E -defined A . E -valued Element of bool [:(A . E),(A . E):]
V is Element of S
A . V is set
V . V is Relation-like A . V -defined A . V -valued Element of bool [:(A . V),(A . V):]
[:(A . V),(A . V):] is set
bool [:(A . V),(A . V):] is non empty set
nabla (A . V) is Relation-like A . V -defined A . V -valued total V121() V123() V128() Element of bool [:(A . V),(A . V):]
S is non empty set
A is Relation-like S -defined Function-like non empty total set
EqRelLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt A) is non empty set
bool the carrier of (EqRelLatt A) is non empty set
S is non empty set
A is Relation-like S -defined Function-like non empty total set
EqRelLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt A) is non empty set
bool the carrier of (EqRelLatt A) is non empty set
E is Element of S
C is Element of bool the carrier of (EqRelLatt A)
pi (C,E) is set
A . E is set
EqRelLatt (A . E) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt (A . E)) is non empty set
bool the carrier of (EqRelLatt (A . E)) is non empty set
B is set
d is Relation-like Function-like set
d . E is set
V is Relation-like S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of A,A
V . E is Relation-like A . E -defined A . E -valued Element of bool [:(A . E),(A . E):]
[:(A . E),(A . E):] is set
bool [:(A . E),(A . E):] is non empty set
B is Element of bool the carrier of (EqRelLatt (A . E))
d is set
V is Relation-like Function-like set
V . E is set
V is Relation-like S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of A,A
V . E is Relation-like A . E -defined A . E -valued Element of bool [:(A . E),(A . E):]
[:(A . E),(A . E):] is set
bool [:(A . E),(A . E):] is non empty set
V is Relation-like S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of A,A
V . E is Relation-like A . E -defined A . E -valued Element of bool [:(A . E),(A . E):]
[:(A . E),(A . E):] is set
bool [:(A . E),(A . E):] is non empty set
d is set
V is Relation-like S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of A,A
V . E is Relation-like A . E -defined A . E -valued Element of bool [:(A . E),(A . E):]
[:(A . E),(A . E):] is set
bool [:(A . E),(A . E):] is non empty set
d is set
V is Relation-like Function-like set
V . E is set
V is Relation-like S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of A,A
V . E is Relation-like A . E -defined A . E -valued Element of bool [:(A . E),(A . E):]
[:(A . E),(A . E):] is set
bool [:(A . E),(A . E):] is non empty set
V is Relation-like S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of A,A
V . E is Relation-like A . E -defined A . E -valued Element of bool [:(A . E),(A . E):]
[:(A . E),(A . E):] is set
bool [:(A . E),(A . E):] is non empty set
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt the Sorts of A) is non empty set
bool the carrier of (EqRelLatt the Sorts of A) is non empty set
E is Element of the carrier of S
the Sorts of A . E is non empty set
EqRelLatt ( the Sorts of A . E) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
V is Element of bool the carrier of (EqRelLatt the Sorts of A)
"\/" (V,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
( the carrier of S, the Sorts of A,E,V) is Element of bool the carrier of (EqRelLatt ( the Sorts of A . E))
the carrier of (EqRelLatt ( the Sorts of A . E)) is non empty set
bool the carrier of (EqRelLatt ( the Sorts of A . E)) is non empty set
"\/" (( the carrier of S, the Sorts of A,E,V),(EqRelLatt ( the Sorts of A . E))) is Element of the carrier of (EqRelLatt ( the Sorts of A . E))
V is Relation-like the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
V . E is Relation-like the Sorts of A . E -defined the Sorts of A . E -valued Element of bool [:( the Sorts of A . E),( the Sorts of A . E):]
[:( the Sorts of A . E),( the Sorts of A . E):] is non empty set
bool [:( the Sorts of A . E),( the Sorts of A . E):] is non empty set
V is Relation-like the Sorts of A . E -defined the Sorts of A . E -valued total V121() V123() V128() Element of bool [:( the Sorts of A . E),( the Sorts of A . E):]
t is Element of the carrier of (EqRelLatt ( the Sorts of A . E))
t9 is Relation-like the Sorts of A . E -defined the Sorts of A . E -valued total V121() V123() V128() Element of bool [:( the Sorts of A . E),( the Sorts of A . E):]
a is Relation-like the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
a . E is Relation-like the Sorts of A . E -defined the Sorts of A . E -valued Element of bool [:( the Sorts of A . E),( the Sorts of A . E):]
f is Element of the carrier of (EqRelLatt the Sorts of A)
g is Relation-like the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
g . E is Relation-like the Sorts of A . E -defined the Sorts of A . E -valued Element of bool [:( the Sorts of A . E),( the Sorts of A . E):]
j is Relation-like the Sorts of A . E -defined the Sorts of A . E -valued total V121() V123() V128() Element of bool [:( the Sorts of A . E),( the Sorts of A . E):]
Z is Element of the carrier of (EqRelLatt ( the Sorts of A . E))
Eq is set
the Sorts of A . Eq is set
[:( the Sorts of A . Eq),( the Sorts of A . Eq):] is set
bool [:( the Sorts of A . Eq),( the Sorts of A . Eq):] is non empty set
Eq is Element of the carrier of S
a . Eq is Relation-like the Sorts of A . Eq -defined the Sorts of A . Eq -valued Element of bool [:( the Sorts of A . Eq),( the Sorts of A . Eq):]
the Sorts of A . Eq is non empty set
[:( the Sorts of A . Eq),( the Sorts of A . Eq):] is non empty set
bool [:( the Sorts of A . Eq),( the Sorts of A . Eq):] is non empty set
g . Eq is Relation-like the Sorts of A . Eq -defined the Sorts of A . Eq -valued Element of bool [:( the Sorts of A . Eq),( the Sorts of A . Eq):]
g . Eq is set
a . Eq is set
a . Eq is set
nabla ( the Sorts of A . Eq) is Relation-like the Sorts of A . Eq -defined the Sorts of A . Eq -valued total V121() V123() V128() Element of bool [:( the Sorts of A . Eq),( the Sorts of A . Eq):]
Eq is Relation-like the Sorts of A . Eq -defined the Sorts of A . Eq -valued total V121() V123() V128() Element of bool [:( the Sorts of A . Eq),( the Sorts of A . Eq):]
Eq is Relation-like the Sorts of A . Eq -defined the Sorts of A . Eq -valued total V121() V123() V128() Element of bool [:( the Sorts of A . Eq),( the Sorts of A . Eq):]
Eq /\ Eq is Relation-like the Sorts of A . Eq -defined the Sorts of A . Eq -valued total V121() V123() V128() Element of bool [:( the Sorts of A . Eq),( the Sorts of A . Eq):]
g . Eq is set
b is Element of the carrier of (EqRelLatt the Sorts of A)
V is Element of the carrier of (EqRelLatt the Sorts of A)
s2 is Element of the carrier of (EqRelLatt ( the Sorts of A . E))
t is Element of the carrier of (EqRelLatt ( the Sorts of A . E))
a is Relation-like the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
a . E is Relation-like the Sorts of A . E -defined the Sorts of A . E -valued Element of bool [:( the Sorts of A . E),( the Sorts of A . E):]
b is Element of the carrier of (EqRelLatt the Sorts of A)
t9 is Relation-like the Sorts of A . E -defined the Sorts of A . E -valued total V121() V123() V128() Element of bool [:( the Sorts of A . E),( the Sorts of A . E):]
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
CongrLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded M24( EqRelLatt the Sorts of A)
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (CongrLatt A) is non empty set
bool the carrier of (CongrLatt A) is non empty set
E is Element of bool the carrier of (CongrLatt A)
"\/" (E,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
the carrier of (EqRelLatt the Sorts of A) is non empty set
bool the carrier of (EqRelLatt the Sorts of A) is non empty set
d is Element of bool the carrier of (EqRelLatt the Sorts of A)
"\/" (d,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
V is Relation-like the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
V is Relation-like the carrier of S -defined Function-like non empty total ManySortedRelation of the Sorts of A, the Sorts of A
V is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
V is Element of the carrier of S
s2 is Element of the carrier of S
V . V is Relation-like the Sorts of A . V -defined the Sorts of A . V -valued non empty total V121() V123() V128() Element of bool [:( the Sorts of A . V),( the Sorts of A . V):]
the Sorts of A . V is non empty set
[:( the Sorts of A . V),( the Sorts of A . V):] is non empty set
bool [:( the Sorts of A . V),( the Sorts of A . V):] is non empty set
V . s2 is Relation-like the Sorts of A . s2 -defined the Sorts of A . s2 -valued non empty total V121() V123() V128() Element of bool [:( the Sorts of A . s2),( the Sorts of A . s2):]
the Sorts of A . s2 is non empty set
[:( the Sorts of A . s2),( the Sorts of A . s2):] is non empty set
bool [:( the Sorts of A . s2),( the Sorts of A . s2):] is non empty set
t is Relation-like Function-like set
[:( the Sorts of A . V),( the Sorts of A . s2):] is non empty set
bool [:( the Sorts of A . V),( the Sorts of A . s2):] is non empty set
a is set
b is set
[a,b] is set
{a,b} is finite set
{a} is finite set
{{a,b},{a}} is finite V46() set
t . a is set
t . b is set
[(t . a),(t . b)] is set
{(t . a),(t . b)} is finite set
{(t . a)} is finite set
{{(t . a),(t . b)},{(t . a)}} is finite V46() set
t9 is Relation-like the Sorts of A . V -defined the Sorts of A . s2 -valued Function-like V18( the Sorts of A . V, the Sorts of A . s2) Element of bool [:( the Sorts of A . V),( the Sorts of A . s2):]
t9 . b is set
EqRelLatt ( the Sorts of A . V) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
( the carrier of S, the Sorts of A,V,d) is Element of bool the carrier of (EqRelLatt ( the Sorts of A . V))
the carrier of (EqRelLatt ( the Sorts of A . V)) is non empty set
bool the carrier of (EqRelLatt ( the Sorts of A . V)) is non empty set
"\/" (( the carrier of S, the Sorts of A,V,d),(EqRelLatt ( the Sorts of A . V))) is Element of the carrier of (EqRelLatt ( the Sorts of A . V))
union ( the carrier of S, the Sorts of A,V,d) is set
f is Relation-like Function-like FinSequence-like set
len f is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
f . 1 is set
f . (len f) is set
( the carrier of S, the Sorts of A,s2,d) is Element of bool the carrier of (EqRelLatt ( the Sorts of A . s2))
EqRelLatt ( the Sorts of A . s2) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
the carrier of (EqRelLatt ( the Sorts of A . s2)) is non empty set
bool the carrier of (EqRelLatt ( the Sorts of A . s2)) is non empty set
union ( the carrier of S, the Sorts of A,s2,d) is set
g is Relation-like Function-like FinSequence-like set
len g is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
dom g is V35() V36() V37() V38() V39() V40() Element of bool NAT
g . 1 is set
g . (len g) is set
Seg (len f) is V35() V36() V37() V38() V39() V40() Element of bool NAT
j is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
g . j is set
j + 1 is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
g . (j + 1) is set
[(g . j),(g . (j + 1))] is set
{(g . j),(g . (j + 1))} is finite set
{(g . j)} is finite set
{{(g . j),(g . (j + 1))},{(g . j)}} is finite V46() set
f . j is set
f . (j + 1) is set
[(f . j),(f . (j + 1))] is set
{(f . j),(f . (j + 1))} is finite set
{(f . j)} is finite set
{{(f . j),(f . (j + 1))},{(f . j)}} is finite V46() set
Z is set
Eq is Relation-like the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like ManySortedRelation of the Sorts of A, the Sorts of A
Eq . V is Relation-like the Sorts of A . V -defined the Sorts of A . V -valued Element of bool [:( the Sorts of A . V),( the Sorts of A . V):]
Eq is Relation-like the carrier of S -defined Function-like non empty total ManySortedRelation of the Sorts of A, the Sorts of A
Eq is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like ManySortedRelation of the Sorts of A, the Sorts of A
t . (f . j) is set
t . (f . (j + 1)) is set
[(t . (f . j)),(t . (f . (j + 1)))] is set
{(t . (f . j)),(t . (f . (j + 1)))} is finite set
{(t . (f . j))} is finite set
{{(t . (f . j)),(t . (f . (j + 1)))},{(t . (f . j))}} is finite V46() set
Eq is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like compatible invariant ManySortedRelation of the Sorts of A, the Sorts of A
Eq . s2 is Relation-like the Sorts of A . s2 -defined the Sorts of A . s2 -valued non empty total V121() V123() V128() Element of bool [:( the Sorts of A . s2),( the Sorts of A . s2):]
W is Relation-like the Sorts of A . s2 -defined the Sorts of A . s2 -valued non empty total V121() V123() V128() Element of bool [:( the Sorts of A . s2),( the Sorts of A . s2):]
W is set
t9 . a is set
"\/" (( the carrier of S, the Sorts of A,s2,d),(EqRelLatt ( the Sorts of A . s2))) is Element of the carrier of (EqRelLatt ( the Sorts of A . s2))
g is Relation-like Function-like FinSequence-like set
len g is V30() V31() ext-real V35() V36() V37() V38() V39() V40() Element of NAT
g . 1 is set
g . (len g) is set
V is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like compatible invariant ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
CongrLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded M24( EqRelLatt the Sorts of A)
the carrier of (CongrLatt A) is non empty set
bool the carrier of (CongrLatt A) is non empty set
B is Element of bool the carrier of (CongrLatt A)
"/\" (B,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
the carrier of (EqRelLatt the Sorts of A) is non empty set
d is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
CongrLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded M24( EqRelLatt the Sorts of A)
the carrier of (CongrLatt A) is non empty set
bool the carrier of (CongrLatt A) is non empty set
B is Element of bool the carrier of (CongrLatt A)
"\/" (B,(EqRelLatt the Sorts of A)) is Element of the carrier of (EqRelLatt the Sorts of A)
the carrier of (EqRelLatt the Sorts of A) is non empty set
d is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like ManySortedRelation of the Sorts of A, the Sorts of A
S is non empty non void feasible ManySortedSign
the carrier of S is non empty set
A is non-empty feasible MSAlgebra over S
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
EqRelLatt the Sorts of A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complete LattStr
CongrLatt A is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded M24( EqRelLatt the Sorts of A)