:: MSUALG_8 semantic presentation

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

F

Seg F

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|])

{ (b

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)

{ b

"/\" ( { b

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)

{ b

"/\" ( { b

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

{ b

"/\" ( { b

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

{ b

"/\" ( { b

(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

{ b

"/\" ( { b

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

{ ("\/" (b

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)

"\/" ( { ("\/" (b

("\/" (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

{ ("\/" (b

"\/" ( { ("\/" (b

{ b

{ ("\/" (b

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 { b

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)