:: BIRKHOFF semantic presentation

NAT is non empty V34() V35() V36() Element of bool REAL

REAL is set

bool REAL is set

NAT is non empty V34() V35() V36() set

bool NAT is set

bool NAT is set

{} is empty V34() V35() V36() V38() V39() V40() set

1 is non empty set

{{},1} is non empty set

K274() is set

bool K274() is set

K275() is Element of bool K274()

K315() is non empty V118() L13()

the carrier of K315() is non empty set

K278( the carrier of K315()) is non empty M20( the carrier of K315())

K314(K315()) is Element of bool K278( the carrier of K315())

bool K278( the carrier of K315()) is set

[:K314(K315()),NAT:] is set

bool [:K314(K315()),NAT:] is set

[:NAT,K314(K315()):] is set

bool [:NAT,K314(K315()):] is set

[:NAT,NAT:] is set

[:[:NAT,NAT:],NAT:] is set

bool [:[:NAT,NAT:],NAT:] is set

K359() is non empty V73() L9()

the carrier of K359() is non empty set

K362() is Element of bool NAT

[:K362(),K362():] is set

[:[:K362(),K362():],K362():] is set

bool [:[:K362(),K362():],K362():] is set

product {} is set

{{}} is non empty set

XX is non empty non void V62() ManySortedSign

the carrier of XX is non empty set

I is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

E is non-empty MSAlgebra over XX

the Sorts of E is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

FreeMSA I is non-empty V126(XX) MSAlgebra over XX

the Sorts of (FreeMSA I) is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

FreeGen I is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) V125(XX, FreeMSA I) GeneratorSet of FreeMSA I

Reverse I is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen I,I

E is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of I, the Sorts of E

E ** (Reverse I) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E

K is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA I), the Sorts of E

K || (FreeGen I) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E

F is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA I), the Sorts of E

F || (FreeGen I) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen I, the Sorts of E

XX is non empty non void V62() ManySortedSign

the carrier of XX is non empty set

I is non-empty MSAlgebra over XX

the Sorts of I is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

E is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

E is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of E, the Sorts of I

rngs E is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

(XX,E,I,E) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of the Sorts of (FreeMSA E), the Sorts of I

FreeMSA E is non-empty V126(XX) MSAlgebra over XX

the Sorts of (FreeMSA E) is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

rngs (XX,E,I,E) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

Reverse E is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen E,E

FreeGen E is Relation-like non-empty non empty-yielding the carrier of XX -defined Function-like non empty V14( the carrier of XX) V125(XX, FreeMSA E) GeneratorSet of FreeMSA E

F is set

(rngs E) . F is set

(rngs (XX,E,I,E)) . F is set

B is set

A is Element of the carrier of XX

(FreeGen E) . A is non empty set

(Reverse E) . A is Relation-like (FreeGen E) . A -defined E . A -valued Function-like non empty V14((FreeGen E) . A) V18((FreeGen E) . A,E . A) Element of bool [:((FreeGen E) . A),(E . A):]

E . A is non empty set

[:((FreeGen E) . A),(E . A):] is set

bool [:((FreeGen E) . A),(E . A):] is set

dom ((Reverse E) . A) is Element of bool ((FreeGen E) . A)

bool ((FreeGen E) . A) is set

the Sorts of (FreeMSA E) . A is non empty set

the Sorts of I . A is non empty set

E . A is Relation-like E . A -defined the Sorts of I . A -valued Function-like non empty V14(E . A) V18(E . A, the Sorts of I . A) Element of bool [:(E . A),( the Sorts of I . A):]

[:(E . A),( the Sorts of I . A):] is set

bool [:(E . A),( the Sorts of I . A):] is set

rng (E . A) is non empty Element of bool ( the Sorts of I . A)

bool ( the Sorts of I . A) is set

dom (E . A) is Element of bool (E . A)

bool (E . A) is set

e is set

(E . A) . e is set

rngs (Reverse E) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) set

rng ((Reverse E) . A) is non empty Element of bool (E . A)

x is set

((Reverse E) . A) . x is set

(XX,E,I,E) . A is Relation-like the Sorts of (FreeMSA E) . A -defined the Sorts of I . A -valued Function-like non empty V14( the Sorts of (FreeMSA E) . A) V18( the Sorts of (FreeMSA E) . A, the Sorts of I . A) Element of bool [:( the Sorts of (FreeMSA E) . A),( the Sorts of I . A):]

[:( the Sorts of (FreeMSA E) . A),( the Sorts of I . A):] is set

bool [:( the Sorts of (FreeMSA E) . A),( the Sorts of I . A):] is set

dom ((XX,E,I,E) . A) is Element of bool ( the Sorts of (FreeMSA E) . A)

bool ( the Sorts of (FreeMSA E) . A) is set

(E . A) * ((Reverse E) . A) is Relation-like (FreeGen E) . A -defined the Sorts of I . A -valued Function-like non empty V14((FreeGen E) . A) V18((FreeGen E) . A, the Sorts of I . A) Element of bool [:((FreeGen E) . A),( the Sorts of I . A):]

[:((FreeGen E) . A),( the Sorts of I . A):] is set

bool [:((FreeGen E) . A),( the Sorts of I . A):] is set

((E . A) * ((Reverse E) . A)) . x is set

E ** (Reverse E) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen E, the Sorts of I

(E ** (Reverse E)) . A is Relation-like (FreeGen E) . A -defined the Sorts of I . A -valued Function-like non empty V14((FreeGen E) . A) V18((FreeGen E) . A, the Sorts of I . A) Element of bool [:((FreeGen E) . A),( the Sorts of I . A):]

((E ** (Reverse E)) . A) . x is set

(XX,E,I,E) || (FreeGen E) is Relation-like the carrier of XX -defined Function-like non empty V14( the carrier of XX) Function-yielding Relation-yielding ManySortedFunction of FreeGen E, the Sorts of I

((XX,E,I,E) || (FreeGen E)) . A is Relation-like (FreeGen E) . A -defined the Sorts of I . A -valued Function-like non empty V14((FreeGen E) . A) V18((FreeGen E) . A, the Sorts of I . A) Element of bool [:((FreeGen E) . A),( the Sorts of I . A):]

(((XX,E,I,E) || (FreeGen E)) . A) . x is set

((XX,E,I,E) . A) | ((FreeGen E) . A) is Relation-like the Sorts of (FreeMSA E) . A -defined the Sorts of I . A -valued Function-like Element of bool [:( the Sorts of (FreeMSA E) . A),( the Sorts of I . A):]

(((XX,E,I,E) . A) | ((FreeGen E) . A)) . x is set

((XX,E,I,E) . A) . x is set

rng ((XX,E,I,E) . A) is non empty Element of bool ( the Sorts of I . A)

F

the carrier of F

F

the Sorts of F

the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

CongrLatt F

EqRelLatt the Sorts of F

the carrier of (CongrLatt F

{ b

( b

the carrier of F

{{{}}} is non empty set

[: the carrier of F

bool [: the carrier of F

K is Relation-like the carrier of F

{K} is Relation-like the carrier of F

F is set

product the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

OPS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

the carrier' of F

the Arity of F

K171( the carrier of F

[: the carrier' of F

bool [: the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

[: the carrier' of F

bool [: the carrier' of F

the ResultSort of F

MSAlgebra(# (SORTS the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

the Sorts of (product the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

the Sorts of (product the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

A is Element of the carrier of F

Carrier ( the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

product (Carrier ( the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

( the carrier of F

{K} . F is set

[| the Sorts of F

F is Relation-like the carrier of F

QuotMSAlg (F

Class F is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact F is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class F),(QuotCharact F) #) is strict MSAlgebra over F

the Sorts of (QuotMSAlg (F

{ the Sorts of F

Trivial_Algebra F

A is set

the Relation-like {} -defined Function-like V14( {} ) MSAlgebra-Family of {} ,F

A is set

B is Element of the carrier of (CongrLatt F

e is Relation-like the carrier of F

QuotMSAlg (F

Class e is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact e is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class e),(QuotCharact e) #) is strict MSAlgebra over F

the carrier of (EqRelLatt the Sorts of F

A is set

Bool [| the Sorts of F

bool (Bool [| the Sorts of F

A is non empty Element of bool (Bool [| the Sorts of F

|:A:| is Relation-like non-empty non empty-yielding the carrier of F

K109( the carrier of F

meet |:A:| is Relation-like the carrier of F

e is Relation-like the carrier of F

x is set

the Sorts of F

[:( the Sorts of F

bool [:( the Sorts of F

e . x is set

h is Relation-like the Sorts of F

{ b

bool the carrier of (CongrLatt F

x is Relation-like the carrier of F

h is Relation-like the carrier of F

QuotMSAlg (F

Class h is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact h is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class h),(QuotCharact h) #) is strict MSAlgebra over F

t2 is strict non-empty MSAlgebra over F

the Sorts of t2 is Relation-like non-empty non empty-yielding the carrier of F

MSNat_Hom (F

the Sorts of (QuotMSAlg (F

e is Relation-like the carrier of F

fi is set

x is Relation-like the carrier of F

QuotMSAlg (F

Class x is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact x is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class x),(QuotCharact x) #) is strict MSAlgebra over F

FofI1 is set

FofI1 is set

fi is Relation-like A -defined Function-like non empty V14(A) set

x is set

fi . x is set

FofI1 is Relation-like the carrier of F

QuotMSAlg (F

Class FofI1 is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact FofI1 is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class FofI1),(QuotCharact FofI1) #) is strict MSAlgebra over F

x is Relation-like A -defined Function-like non empty V14(A) MSAlgebra-Family of A,F

FofI1 is Relation-like the carrier of F

x . FofI1 is non-empty MSAlgebra over F

the Sorts of (x . FofI1) is Relation-like non-empty non empty-yielding the carrier of F

FofI1 is Relation-like the carrier of F

QuotMSAlg (F

Class FofI1 is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact FofI1 is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class FofI1),(QuotCharact FofI1) #) is strict MSAlgebra over F

MSNat_Hom (F

the Sorts of (QuotMSAlg (F

XX is Relation-like the carrier of F

FofI1 is Relation-like A -defined Function-like non empty V14(A) set

FofI1 is Relation-like the carrier of F

x . FofI1 is non-empty MSAlgebra over F

the Sorts of (x . FofI1) is Relation-like non-empty non empty-yielding the carrier of F

FofI1 . FofI1 is set

H is Relation-like the carrier of F

FofI1 is set

dom FofI1 is set

FofI1 . FofI1 is set

dom FofI1 is Element of bool A

bool A is set

H is Relation-like the carrier of F

x . H is non-empty MSAlgebra over F

the Sorts of (x . H) is Relation-like non-empty non empty-yielding the carrier of F

FofI1 . H is set

XX is Relation-like the carrier of F

product x is non-empty MSAlgebra over F

SORTS x is Relation-like the carrier of F

OPS x is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (SORTS x),(OPS x) #) is strict MSAlgebra over F

the Sorts of (product x) is Relation-like non-empty non empty-yielding the carrier of F

FofI1 is Relation-like A -defined Function-like non empty V14(A) Function-yielding Relation-yielding set

H is Relation-like the carrier of F

XX is set

B is Element of the carrier of F

[| the Sorts of F

bool ([| the Sorts of F

bool (bool ([| the Sorts of F

|:A:| . B is non empty Element of bool (bool ([| the Sorts of F

(meet |:A:|) . B is set

G is Element of bool (bool ([| the Sorts of F

Intersect G is Element of bool ([| the Sorts of F

Bool [| the Sorts of F

{ (b

the Sorts of F

MSCng H is Relation-like the carrier of F

(MSCng H) . B is Relation-like the Sorts of F

[:( the Sorts of F

bool [:( the Sorts of F

h . B is Relation-like the Sorts of F

C is set

H is set

[C,H] is V15() set

{C,H} is non empty set

{C} is non empty set

{{C,H},{C}} is non empty set

MSCng (H,B) is Relation-like the Sorts of F

K is set

t1 is Relation-like the carrier of F

t1 . B is set

F1 is Relation-like the carrier of F

x . F1 is non-empty MSAlgebra over F

the Sorts of (x . F1) is Relation-like non-empty non empty-yielding the carrier of F

FofI1 . F1 is Relation-like Function-like set

F1 is Relation-like the carrier of F

F1 . B is Relation-like the Sorts of F

the Sorts of (x . F1) . B is non empty set

[:( the Sorts of F

bool [:( the Sorts of F

(F1 . B) . C is set

proj (x,F1) is Relation-like the carrier of F

(proj (x,F1)) ** H is Relation-like the carrier of F

((proj (x,F1)) ** H) . B is Relation-like the Sorts of F

(((proj (x,F1)) ** H) . B) . C is set

the Sorts of (product x) . B is non empty set

H . B is Relation-like the Sorts of F

[:( the Sorts of F

bool [:( the Sorts of F

(proj (x,F1)) . B is Relation-like the Sorts of (product x) . B -defined the Sorts of (x . F1) . B -valued Function-like non empty V14( the Sorts of (product x) . B) V18( the Sorts of (product x) . B, the Sorts of (x . F1) . B) Element of bool [:( the Sorts of (product x) . B),( the Sorts of (x . F1) . B):]

[:( the Sorts of (product x) . B),( the Sorts of (x . F1) . B):] is set

bool [:( the Sorts of (product x) . B),( the Sorts of (x . F1) . B):] is set

((proj (x,F1)) . B) * (H . B) is Relation-like the Sorts of F

(((proj (x,F1)) . B) * (H . B)) . C is set

(H . B) . C is set

((proj (x,F1)) . B) . ((H . B) . C) is set

(H . B) . H is set

((proj (x,F1)) . B) . ((H . B) . H) is set

(((proj (x,F1)) . B) * (H . B)) . H is set

(((proj (x,F1)) ** H) . B) . H is set

(F1 . B) . H is set

c

MSNat_Hom (F

QuotMSAlg (F

Class c

QuotCharact c

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class c

the Sorts of (QuotMSAlg (F

Carrier (x,B) is Relation-like A -defined Function-like non empty V14(A) set

H . B is Relation-like the Sorts of F

the Sorts of (product x) . B is non empty set

[:( the Sorts of F

bool [:( the Sorts of F

(H . B) . C is set

(H . B) . H is set

K is Relation-like the carrier of F

proj ((Carrier (x,B)),K) is Relation-like Function-like set

(proj ((Carrier (x,B)),K)) . ((H . B) . C) is set

(proj ((Carrier (x,B)),K)) . ((H . B) . H) is set

x . K is non-empty MSAlgebra over F

the Sorts of (x . K) is Relation-like non-empty non empty-yielding the carrier of F

FofI1 . K is Relation-like Function-like set

F1 is Relation-like the carrier of F

t1 is Relation-like the carrier of F

t1 . B is Relation-like the Sorts of F

proj (x,K) is Relation-like the carrier of F

(proj (x,K)) . B is Relation-like the Sorts of (product x) . B -defined the Sorts of (x . K) . B -valued Function-like non empty V14( the Sorts of (product x) . B) V18( the Sorts of (product x) . B, the Sorts of (x . K) . B) Element of bool [:( the Sorts of (product x) . B),( the Sorts of (x . K) . B):]

the Sorts of (x . K) . B is non empty set

[:( the Sorts of (product x) . B),( the Sorts of (x . K) . B):] is set

bool [:( the Sorts of (product x) . B),( the Sorts of (x . K) . B):] is set

((proj (x,K)) . B) . ((H . B) . C) is set

((proj (x,K)) . B) * (H . B) is Relation-like the Sorts of F

[:( the Sorts of F

bool [:( the Sorts of F

(((proj (x,K)) . B) * (H . B)) . C is set

(proj (x,K)) ** H is Relation-like the carrier of F

((proj (x,K)) ** H) . B is Relation-like the Sorts of F

(((proj (x,K)) ** H) . B) . C is set

F1 . B is Relation-like the Sorts of F

(F1 . B) . C is set

(F1 . B) . H is set

(((proj (x,K)) ** H) . B) . H is set

(((proj (x,K)) . B) * (H . B)) . H is set

((proj (x,K)) . B) . ((H . B) . H) is set

F1 is Relation-like the carrier of F

MSNat_Hom (F

QuotMSAlg (F

Class F1 is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact F1 is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class F1),(QuotCharact F1) #) is strict MSAlgebra over F

the Sorts of (QuotMSAlg (F

product (Carrier (x,B)) is set

(MSCng H) . XX is set

h . XX is set

QuotMSAlg (F

Class (MSCng H) is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact (MSCng H) is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class (MSCng H)),(QuotCharact (MSCng H)) #) is strict MSAlgebra over F

MSHomQuot H is Relation-like the carrier of F

the Sorts of (QuotMSAlg (F

Image (MSHomQuot H) is strict non-empty MSSubAlgebra of product x

XX is strict non-empty MSSubAlgebra of product x

B is set

x . B is set

G is Relation-like the carrier of F

x . G is non-empty MSAlgebra over F

C is Relation-like the carrier of F

QuotMSAlg (F

Class C is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact C is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class C),(QuotCharact C) #) is strict MSAlgebra over F

H is Element of the carrier of (CongrLatt F

K is Relation-like the carrier of F

QuotMSAlg (F

Class K is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact K is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class K),(QuotCharact K) #) is strict MSAlgebra over F

B is non-empty MSAlgebra over F

the Sorts of B is Relation-like non-empty non empty-yielding the carrier of F

G is Relation-like the carrier of F

MSCng G is Relation-like the carrier of F

QuotMSAlg (F

Class (MSCng G) is Relation-like non-empty non empty-yielding the carrier of F

QuotCharact (MSCng G) is Relation-like the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

MSAlgebra(# (Class (MSCng G)),(QuotCharact (MSCng G)) #) is strict MSAlgebra over F

MSHomQuot G is Relation-like the carrier of F

the Sorts of (QuotMSAlg (F

Image (MSHomQuot G) is strict non-empty MSSubAlgebra of B

C is strict non-empty MSSubAlgebra of B

H is Relation-like the carrier of F

H ** e is Relation-like the carrier of F

K is Relation-like the carrier of F

K ** e is Relation-like the carrier of F

F

the carrier of F

F

XX is non-empty MSAlgebra over F

I is strict non-empty MSSubAlgebra of XX

XX is set

I is Relation-like XX -defined Function-like V14(XX) MSAlgebra-Family of XX,F

product I is non-empty MSAlgebra over F

SORTS I is Relation-like the carrier of F

OPS I is Relation-like the carrier' of F

the carrier' of F

the Arity of F

K171( the carrier of F

[: the carrier' of F

bool [: the carrier' of F

K174( the carrier of F

the Arity of F

the ResultSort of F

[: the carrier' of F

bool [: the carrier' of F

the ResultSort of F

MSAlgebra(# (SORTS I),(OPS I) #) is strict MSAlgebra over F

FreeMSA F

Reverse F

FreeGen F

I is non-empty MSAlgebra over F

E is non-empty MSAlgebra over F

the Sorts of (FreeMSA F

I is strict non-empty MSAlgebra over F

the Sorts of I is Relation-like non-empty non empty-yielding the carrier of F

E is Relation-like the carrier of F

(Reverse F

E || (FreeGen F

(E || (FreeGen F

E is Relation-like the carrier of F

K is non-empty MSAlgebra over F

the Sorts of K is Relation-like non-empty non empty-yielding the carrier of F

F is Relation-like the carrier of F

F ** (Reverse F

A is Relation-like the carrier of F

A || (FreeGen F

B is Relation-like the carrier of F

B ** E is Relation-like the carrier of F

B ** E is Relation-like the carrier of F

B ** (E || (FreeGen F

rngs (Reverse F

E ** (Reverse F

((Reverse F

(E || (FreeGen F

id (FreeGen F

(E || (FreeGen F

(B ** E) ** (Reverse F

e is Relation-like the carrier of F

e ** E is Relation-like the carrier of F

((E || (FreeGen F

e ** (((E || (FreeGen F

B ** ((E || (FreeGen F

(B ** ((E || (FreeGen F

B ** (((E || (FreeGen F

e ** ((E || (FreeGen F

B ** ((E || (FreeGen F

e ** ((E || (FreeGen F

B ** ((E || (FreeGen F

e ** (E || (FreeGen F

e ** E is Relation-like the carrier of F

(e ** E) || (FreeGen F

(B ** E) || (FreeGen F

F

the carrier of F

the carrier of F

{NAT} is non empty set

[: the carrier of F

bool [: the carrier of F

F

the Sorts of F

F

the Sorts of F

F

F

(F

FreeMSA ( the carrier of F

the Sorts of (FreeMSA ( the carrier of F

(F

XX is Relation-like the carrier of F

XX ** F

XX ** (F

I is Relation-like non-empty non empty-yielding the carrier of F

FreeMSA I is non-empty V126(F

E is Relation-like the carrier of F

(F

the Sorts of (FreeMSA I) is Relation-like non-empty non empty-yielding the carrier of F

FreeGen I is Relation-like non-empty non empty-yielding the carrier of F

(F

Reverse I is Relation-like the carrier of F

F

F

XX ** (F

FreeGen ( the carrier of F

(F

XX ** ((F

(XX ** (F

F

the carrier of F

the carrier of F

{NAT} is non empty set

[: the carrier of F

bool [: the carrier of F

F

the Sorts of F

TermAlg F

the carrier of F

[: the carrier of F

bool [: the carrier of F

FreeMSA ( the carrier of F

the Sorts of (TermAlg F

F

the Sorts of (TermAlg F

FreeMSA ( the carrier of F

the Sorts of (FreeMSA ( the carrier of F

F

(F

(F

the Sorts of (FreeMSA ( the carrier of F

the Sorts of F

[:( the Sorts of (FreeMSA ( the carrier of F

bool [:( the Sorts of (FreeMSA ( the carrier of F

F

((F

F

((F

F

Equations F

[| the Sorts of (TermAlg F

(Equations F

{F

{F

{{F

E is non-empty MSAlgebra over F

the Sorts of E is Relation-like non-empty non empty-yielding the carrier of F

E is Relation-like the carrier of F

E . F

the Sorts of E . F

[:( the Sorts of (TermAlg F

bool [:( the Sorts of (TermAlg F

(F

(E . F

(F

(E . F

I is Relation-like non-empty non empty-yielding the carrier of F

FreeMSA I is non-empty V126(F

the Sorts of (FreeMSA I) is Relation-like non-empty non empty-yielding the carrier of F

FreeGen I is Relation-like non-empty non empty-yielding the carrier of F

Reverse I is Relation-like the carrier of F

(Reverse I) "" is Relation-like the carrier of F

K is Relation-like the carrier of F

K || (FreeGen I) is Relation-like the carrier of F

(K || (FreeGen I)) ** ((Reverse I) "") is Relation-like the carrier of F

(F

XX is Relation-like the carrier of F

B is non-empty MSAlgebra over F

the Sorts of B is Relation-like non-empty non empty-yielding the carrier of F

e is Relation-like the carrier of F

A is Relation-like the carrier of F

(F

(F

B is Relation-like the carrier of F

B ** (F

(F

the Sorts of (FreeMSA I) . F

[:( the Sorts of (FreeMSA I) . F

bool [:( the Sorts of (FreeMSA I) . F

((F

B . F

[:( the Sorts of F

bool [:( the Sorts of F

(B . F

[:( the Sorts of (FreeMSA ( the carrier of F

bool [:( the Sorts of (FreeMSA ( the carrier of F

((B . F

(B . F

((B . F

((F

rngs (Reverse I) is Relation-like the carrier of F

(F

((K || (FreeGen I)) ** ((Reverse I) "")) ** (Reverse I) is Relation-like the carrier of F

((Reverse I) "") ** (Reverse I) is Relation-like the carrier of F

(K || (FreeGen I)) ** (((Reverse I) "") ** (Reverse I)) is Relation-like the carrier of F

id (FreeGen I) is Relation-like the carrier of F

(K || (FreeGen I)) ** (id (FreeGen I)) is Relation-like the carrier of F

[F

[F

(E . F

(E . F

[F

(E . F

F

the carrier of F

F

F

the Sorts of F

F

F

I is set

(F

F

the Sorts of F

[:(F

bool [:(F

F

E is Relation-like F

E .: (F

bool ( the Sorts of F

E is non empty set

dom E is Element of bool (F

bool (F

I is set

(F

the Sorts of F

F

[:(F

bool [:(F

F

E is Relation-like F

E .: (F

bool ( the Sorts of F

I is Relation-like non-empty non empty-yielding the carrier of F

GenMSAlg I is strict non-empty MSSubAlgebra of F

the Sorts of (GenMSAlg I) is Relation-like non-empty non empty-yielding the carrier of F

E is set

the Sorts of (GenMSAlg I) . E is set

F

E is set

the Sorts of F

F

doms F

rngs F

E is Relation-like the carrier of F

K is Relation-like the carrier of F

K ** F

id the Sorts of (GenMSAlg I) is Relation-like the carrier of F

F is Relation-like the carrier of F

F ** E is Relation-like the carrier of F

A is Relation-like the carrier of F

A ** F

F ** K is Relation-like the carrier of F

(F ** K) ** F

B is Relation-like the carrier of F

id the Sorts of F

(id the Sorts of F

F .:.: the Sorts of (GenMSAlg I) is Relation-like the carrier of F

F

the carrier of F

the carrier of F

{NAT} is non empty set

[: the carrier of F

bool [: the carrier of F

F

the Sorts of F

F

FreeMSA ( the carrier of F

(F

the Sorts of (FreeMSA ( the carrier of F