:: by Ewa Burakowska

::

:: Received April 25, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

registration

let I be set ;

let X be ManySortedSet of I;

let Y be V8() ManySortedSet of I;

coherence

X \/ Y is non-empty

Y \/ X is non-empty ;

end;
let X be ManySortedSet of I;

let Y be V8() ManySortedSet of I;

coherence

X \/ Y is non-empty

proof end;

coherence Y \/ X is non-empty ;

theorem Th1: :: MSUALG_2:1

for I being non empty set

for X, Y being ManySortedSet of I

for i being Element of I * holds product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i))

for X, Y being ManySortedSet of I

for i being Element of I * holds product ((X /\ Y) * i) = (product (X * i)) /\ (product (Y * i))

proof end;

begin

definition

let S be non empty ManySortedSign ;

let U0 be MSAlgebra over S;

mode MSSubset of U0 is ManySortedSubset of the Sorts of U0;

end;
let U0 be MSAlgebra over S;

mode MSSubset of U0 is ManySortedSubset of the Sorts of U0;

definition

let S be non empty ManySortedSign ;

let IT be SortSymbol of S;

end;
let IT be SortSymbol of S;

attr IT is with_const_op means :Def1: :: MSUALG_2:def 1

ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = IT );

ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = IT );

:: deftheorem Def1 defines with_const_op MSUALG_2:def 1 :

for S being non empty ManySortedSign

for IT being SortSymbol of S holds

( IT is with_const_op iff ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = IT ) );

for S being non empty ManySortedSign

for IT being SortSymbol of S holds

( IT is with_const_op iff ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = IT ) );

definition

let IT be non empty ManySortedSign ;

end;
attr IT is all-with_const_op means :Def2: :: MSUALG_2:def 2

for s being SortSymbol of IT holds s is with_const_op ;

for s being SortSymbol of IT holds s is with_const_op ;

:: deftheorem Def2 defines all-with_const_op MSUALG_2:def 2 :

for IT being non empty ManySortedSign holds

( IT is all-with_const_op iff for s being SortSymbol of IT holds s is with_const_op );

for IT being non empty ManySortedSign holds

( IT is all-with_const_op iff for s being SortSymbol of IT holds s is with_const_op );

registration

let A be non empty set ;

let B be set ;

let a be Function of B,(A *);

let r be Function of B,A;

coherence

not ManySortedSign(# A,B,a,r #) is empty ;

end;
let B be set ;

let a be Function of B,(A *);

let r be Function of B,A;

coherence

not ManySortedSign(# A,B,a,r #) is empty ;

registration

existence

ex b_{1} being non empty ManySortedSign st

( not b_{1} is void & b_{1} is all-with_const_op & b_{1} is strict )

end;
ex b

( not b

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let s be SortSymbol of S;

( ( the Sorts of U0 . s <> {} implies ex b_{1} being Subset of ( the Sorts of U0 . s) ex A being non empty set st

( A = the Sorts of U0 . s & b_{1} = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) & ( not the Sorts of U0 . s <> {} implies ex b_{1} being Subset of ( the Sorts of U0 . s) st b_{1} = {} ) )

consistency

for b_{1} being Subset of ( the Sorts of U0 . s) holds verum;

uniqueness

for b_{1}, b_{2} being Subset of ( the Sorts of U0 . s) holds

( ( the Sorts of U0 . s <> {} & ex A being non empty set st

( A = the Sorts of U0 . s & b_{1} = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) & ex A being non empty set st

( A = the Sorts of U0 . s & b_{2} = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) implies b_{1} = b_{2} ) & ( not the Sorts of U0 . s <> {} & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) );

;

end;
let U0 be MSAlgebra over S;

let s be SortSymbol of S;

func Constants (U0,s) -> Subset of ( the Sorts of U0 . s) means :Def3: :: MSUALG_2:def 3

ex A being non empty set st

( A = the Sorts of U0 . s & it = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) if the Sorts of U0 . s <> {}

otherwise it = {} ;

existence ex A being non empty set st

( A = the Sorts of U0 . s & it = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) if the Sorts of U0 . s <> {}

otherwise it = {} ;

( ( the Sorts of U0 . s <> {} implies ex b

( A = the Sorts of U0 . s & b

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) & ( not the Sorts of U0 . s <> {} implies ex b

proof end;

correctness consistency

for b

uniqueness

for b

( ( the Sorts of U0 . s <> {} & ex A being non empty set st

( A = the Sorts of U0 . s & b

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) & ex A being non empty set st

( A = the Sorts of U0 . s & b

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) implies b

;

:: deftheorem Def3 defines Constants MSUALG_2:def 3 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for s being SortSymbol of S

for b_{4} being Subset of ( the Sorts of U0 . s) holds

( ( the Sorts of U0 . s <> {} implies ( b_{4} = Constants (U0,s) iff ex A being non empty set st

( A = the Sorts of U0 . s & b_{4} = { a where a is Element of A : ex o being OperSymbol of S st

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) ) & ( not the Sorts of U0 . s <> {} implies ( b_{4} = Constants (U0,s) iff b_{4} = {} ) ) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for s being SortSymbol of S

for b

( ( the Sorts of U0 . s <> {} implies ( b

( A = the Sorts of U0 . s & b

( the Arity of S . o = {} & the ResultSort of S . o = s & a in rng (Den (o,U0)) ) } ) ) ) & ( not the Sorts of U0 . s <> {} implies ( b

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

ex b_{1} being MSSubset of U0 st

for s being SortSymbol of S holds b_{1} . s = Constants (U0,s)

for b_{1}, b_{2} being MSSubset of U0 st ( for s being SortSymbol of S holds b_{1} . s = Constants (U0,s) ) & ( for s being SortSymbol of S holds b_{2} . s = Constants (U0,s) ) holds

b_{1} = b_{2}

end;
let U0 be MSAlgebra over S;

func Constants U0 -> MSSubset of U0 means :Def4: :: MSUALG_2:def 4

for s being SortSymbol of S holds it . s = Constants (U0,s);

existence for s being SortSymbol of S holds it . s = Constants (U0,s);

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines Constants MSUALG_2:def 4 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for b_{3} being MSSubset of U0 holds

( b_{3} = Constants U0 iff for s being SortSymbol of S holds b_{3} . s = Constants (U0,s) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for b

( b

registration

let S be non empty non void all-with_const_op ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

let s be SortSymbol of S;

coherence

not Constants (U0,s) is empty

end;
let U0 be non-empty MSAlgebra over S;

let s be SortSymbol of S;

coherence

not Constants (U0,s) is empty

proof end;

registration

let S be non empty non void all-with_const_op ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

coherence

Constants U0 is non-empty

end;
let U0 be non-empty MSAlgebra over S;

coherence

Constants U0 is non-empty

proof end;

begin

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let o be OperSymbol of S;

let A be MSSubset of U0;

end;
let U0 be MSAlgebra over S;

let o be OperSymbol of S;

let A be MSSubset of U0;

pred A is_closed_on o means :Def5: :: MSUALG_2:def 5

rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o;

rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o;

:: deftheorem Def5 defines is_closed_on MSUALG_2:def 5 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for o being OperSymbol of S

for A being MSSubset of U0 holds

( A is_closed_on o iff rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for o being OperSymbol of S

for A being MSSubset of U0 holds

( A is_closed_on o iff rng ((Den (o,U0)) | (((A #) * the Arity of S) . o)) c= (A * the ResultSort of S) . o );

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let A be MSSubset of U0;

end;
let U0 be MSAlgebra over S;

let A be MSSubset of U0;

attr A is opers_closed means :Def6: :: MSUALG_2:def 6

for o being OperSymbol of S holds A is_closed_on o;

for o being OperSymbol of S holds A is_closed_on o;

:: deftheorem Def6 defines opers_closed MSUALG_2:def 6 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds

( A is opers_closed iff for o being OperSymbol of S holds A is_closed_on o );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds

( A is opers_closed iff for o being OperSymbol of S holds A is_closed_on o );

theorem Th2: :: MSUALG_2:2

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for U0 being MSAlgebra over S

for B0, B1 being MSSubset of U0 st B0 c= B1 holds

((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o

for o being OperSymbol of S

for U0 being MSAlgebra over S

for B0, B1 being MSSubset of U0 st B0 c= B1 holds

((B0 #) * the Arity of S) . o c= ((B1 #) * the Arity of S) . o

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let o be OperSymbol of S;

let A be MSSubset of U0;

assume A1: A is_closed_on o ;

(Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)

end;
let U0 be MSAlgebra over S;

let o be OperSymbol of S;

let A be MSSubset of U0;

assume A1: A is_closed_on o ;

func o /. A -> Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o) equals :Def7: :: MSUALG_2:def 7

(Den (o,U0)) | (((A #) * the Arity of S) . o);

coherence (Den (o,U0)) | (((A #) * the Arity of S) . o);

(Den (o,U0)) | (((A #) * the Arity of S) . o) is Function of (((A #) * the Arity of S) . o),((A * the ResultSort of S) . o)

proof end;

:: deftheorem Def7 defines /. MSUALG_2:def 7 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for o being OperSymbol of S

for A being MSSubset of U0 st A is_closed_on o holds

o /. A = (Den (o,U0)) | (((A #) * the Arity of S) . o);

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for o being OperSymbol of S

for A being MSSubset of U0 st A is_closed_on o holds

o /. A = (Den (o,U0)) | (((A #) * the Arity of S) . o);

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let A be MSSubset of U0;

ex b_{1} being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st

for o being OperSymbol of S holds b_{1} . o = o /. A

for b_{1}, b_{2} being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S st ( for o being OperSymbol of S holds b_{1} . o = o /. A ) & ( for o being OperSymbol of S holds b_{2} . o = o /. A ) holds

b_{1} = b_{2}

end;
let U0 be MSAlgebra over S;

let A be MSSubset of U0;

func Opers (U0,A) -> ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S means :Def8: :: MSUALG_2:def 8

for o being OperSymbol of S holds it . o = o /. A;

existence for o being OperSymbol of S holds it . o = o /. A;

ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines Opers MSUALG_2:def 8 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0

for b_{4} being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S holds

( b_{4} = Opers (U0,A) iff for o being OperSymbol of S holds b_{4} . o = o /. A );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0

for b

( b

theorem Th3: :: MSUALG_2:3

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )

for U0 being MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )

proof end;

theorem Th4: :: MSUALG_2:4

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

Opers (U0,B) = the Charact of U0

for U0 being MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

Opers (U0,B) = the Charact of U0

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

ex b_{1} being MSAlgebra over S st

( the Sorts of b_{1} is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b_{1} holds

( B is opers_closed & the Charact of b_{1} = Opers (U0,B) ) ) )

end;
let U0 be MSAlgebra over S;

mode MSSubAlgebra of U0 -> MSAlgebra over S means :Def9: :: MSUALG_2:def 9

( the Sorts of it is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of it holds

( B is opers_closed & the Charact of it = Opers (U0,B) ) ) );

existence ( the Sorts of it is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of it holds

( B is opers_closed & the Charact of it = Opers (U0,B) ) ) );

ex b

( the Sorts of b

( B is opers_closed & the Charact of b

proof end;

:: deftheorem Def9 defines MSSubAlgebra MSUALG_2:def 9 :

for S being non empty non void ManySortedSign

for U0, b_{3} being MSAlgebra over S holds

( b_{3} is MSSubAlgebra of U0 iff ( the Sorts of b_{3} is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b_{3} holds

( B is opers_closed & the Charact of b_{3} = Opers (U0,B) ) ) ) );

for S being non empty non void ManySortedSign

for U0, b

( b

( B is opers_closed & the Charact of b

Lm1: for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0

proof end;

registration

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

existence

ex b_{1} being MSSubAlgebra of U0 st b_{1} is strict

end;
let U0 be MSAlgebra over S;

existence

ex b

proof end;

registration

let S be non empty non void ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

coherence

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is non-empty by MSUALG_1:def 3;

end;
let U0 be non-empty MSAlgebra over S;

coherence

MSAlgebra(# the Sorts of U0, the Charact of U0 #) is non-empty by MSUALG_1:def 3;

registration

let S be non empty non void ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

existence

ex b_{1} being MSSubAlgebra of U0 st

( b_{1} is non-empty & b_{1} is strict )

end;
let U0 be non-empty MSAlgebra over S;

existence

ex b

( b

proof end;

theorem :: MSUALG_2:5

for S being non empty non void ManySortedSign

for U0, U1 being MSAlgebra over S st MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) holds

U0 is MSSubAlgebra of U1

for U0, U1 being MSAlgebra over S st MSAlgebra(# the Sorts of U0, the Charact of U0 #) = MSAlgebra(# the Sorts of U1, the Charact of U1 #) holds

U0 is MSSubAlgebra of U1

proof end;

theorem :: MSUALG_2:6

for S being non empty non void ManySortedSign

for U0, U1, U2 being MSAlgebra over S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds

U0 is MSSubAlgebra of U2

for U0, U1, U2 being MSAlgebra over S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds

U0 is MSSubAlgebra of U2

proof end;

theorem Th7: :: MSUALG_2:7

for S being non empty non void ManySortedSign

for U1, U2 being MSAlgebra over S st U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 holds

MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

for U1, U2 being MSAlgebra over S st U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 holds

MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

proof end;

theorem Th8: :: MSUALG_2:8

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds

U1 is MSSubAlgebra of U2

for U0 being MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts of U2 holds

U1 is MSSubAlgebra of U2

proof end;

theorem Th9: :: MSUALG_2:9

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds

MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

for U0 being MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds

MSAlgebra(# the Sorts of U1, the Charact of U1 #) = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

proof end;

theorem Th10: :: MSUALG_2:10

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1

for U0 being MSAlgebra over S

for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1

proof end;

theorem :: MSUALG_2:11

for S being non empty non void all-with_const_op ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1 being non-empty MSSubAlgebra of U0 holds Constants U0 is V8() MSSubset of U1 by Th10;

for U0 being non-empty MSAlgebra over S

for U1 being non-empty MSSubAlgebra of U0 holds Constants U0 is V8() MSSubset of U1 by Th10;

theorem :: MSUALG_2:12

for S being non empty non void all-with_const_op ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is V8()

for U0 being non-empty MSAlgebra over S

for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is V8()

proof end;

begin

::

:: Many Sorted Subsets of a Many Sorted Algebra.

::

:: Many Sorted Subsets of a Many Sorted Algebra.

::

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let A be MSSubset of U0;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) holds

b_{1} = b_{2}

end;
let U0 be MSAlgebra over S;

let A be MSSubset of U0;

func SubSort A -> set means :Def10: :: MSUALG_2:def 10

for x being set holds

( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) );

existence for x being set holds

( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) );

ex b

for x being set holds

( x in b

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) )

proof end;

uniqueness for b

( x in b

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) & ( for x being set holds

( x in b

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) ) holds

b

proof end;

:: deftheorem Def10 defines SubSort MSUALG_2:def 10 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0

for b_{4} being set holds

( b_{4} = SubSort A iff for x being set holds

( x in b_{4} iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0

for b

( b

( x in b

( B is opers_closed & Constants U0 c= B & A c= B ) ) ) ) );

Lm2: for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds the Sorts of U0 in SubSort A

proof end;

registration

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let A be MSSubset of U0;

coherence

not SubSort A is empty by Lm2;

end;
let U0 be MSAlgebra over S;

let A be MSSubset of U0;

coherence

not SubSort A is empty by Lm2;

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

B is opers_closed ) ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

B is opers_closed ) ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

B is opers_closed ) ) ) ) holds

b_{1} = b_{2}

end;
let U0 be MSAlgebra over S;

func SubSort U0 -> set means :Def11: :: MSUALG_2:def 11

for x being set holds

( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

B is opers_closed ) ) );

existence for x being set holds

( x in it iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

B is opers_closed ) ) );

ex b

for x being set holds

( x in b

B is opers_closed ) ) )

proof end;

uniqueness for b

( x in b

B is opers_closed ) ) ) ) & ( for x being set holds

( x in b

B is opers_closed ) ) ) ) holds

b

proof end;

:: deftheorem Def11 defines SubSort MSUALG_2:def 11 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for b_{3} being set holds

( b_{3} = SubSort U0 iff for x being set holds

( x in b_{3} iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds

B is opers_closed ) ) ) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for b

( b

( x in b

B is opers_closed ) ) ) );

registration

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

coherence

not SubSort U0 is empty

end;
let U0 be MSAlgebra over S;

coherence

not SubSort U0 is empty

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let e be Element of SubSort U0;

coherence

e is MSSubset of U0 by Def11;

end;
let U0 be MSAlgebra over S;

let e be Element of SubSort U0;

coherence

e is MSSubset of U0 by Def11;

:: deftheorem defines @ MSUALG_2:def 12 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for e being Element of SubSort U0 holds @ e = e;

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for e being Element of SubSort U0 holds @ e = e;

theorem Th13: :: MSUALG_2:13

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A, B being MSSubset of U0 holds

( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )

for U0 being MSAlgebra over S

for A, B being MSSubset of U0 holds

( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )

proof end;

theorem Th14: :: MSUALG_2:14

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for B being MSSubset of U0 holds

( B in SubSort U0 iff B is opers_closed )

for U0 being MSAlgebra over S

for B being MSSubset of U0 holds

( B in SubSort U0 iff B is opers_closed )

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let A be MSSubset of U0;

let s be SortSymbol of S;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) ) ) & ( for x being set holds

( x in b_{2} iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) ) ) holds

b_{1} = b_{2}

end;
let U0 be MSAlgebra over S;

let A be MSSubset of U0;

let s be SortSymbol of S;

func SubSort (A,s) -> set means :Def13: :: MSUALG_2:def 13

for x being set holds

( x in it iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) );

existence for x being set holds

( x in it iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) );

ex b

for x being set holds

( x in b

( B in SubSort A & x = B . s ) )

proof end;

uniqueness for b

( x in b

( B in SubSort A & x = B . s ) ) ) & ( for x being set holds

( x in b

( B in SubSort A & x = B . s ) ) ) holds

b

proof end;

:: deftheorem Def13 defines SubSort MSUALG_2:def 13 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0

for s being SortSymbol of S

for b_{5} being set holds

( b_{5} = SubSort (A,s) iff for x being set holds

( x in b_{5} iff ex B being MSSubset of U0 st

( B in SubSort A & x = B . s ) ) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0

for s being SortSymbol of S

for b

( b

( x in b

( B in SubSort A & x = B . s ) ) );

registration

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let A be MSSubset of U0;

let s be SortSymbol of S;

coherence

not SubSort (A,s) is empty

end;
let U0 be MSAlgebra over S;

let A be MSSubset of U0;

let s be SortSymbol of S;

coherence

not SubSort (A,s) is empty

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let A be MSSubset of U0;

ex b_{1} being MSSubset of U0 st

for s being SortSymbol of S holds b_{1} . s = meet (SubSort (A,s))

for b_{1}, b_{2} being MSSubset of U0 st ( for s being SortSymbol of S holds b_{1} . s = meet (SubSort (A,s)) ) & ( for s being SortSymbol of S holds b_{2} . s = meet (SubSort (A,s)) ) holds

b_{1} = b_{2}

end;
let U0 be MSAlgebra over S;

let A be MSSubset of U0;

func MSSubSort A -> MSSubset of U0 means :Def14: :: MSUALG_2:def 14

for s being SortSymbol of S holds it . s = meet (SubSort (A,s));

existence for s being SortSymbol of S holds it . s = meet (SubSort (A,s));

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines MSSubSort MSUALG_2:def 14 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A, b_{4} being MSSubset of U0 holds

( b_{4} = MSSubSort A iff for s being SortSymbol of S holds b_{4} . s = meet (SubSort (A,s)) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A, b

( b

theorem Th15: :: MSUALG_2:15

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A

proof end;

theorem Th16: :: MSUALG_2:16

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 st (Constants U0) \/ A is V8() holds

MSSubSort A is V8()

for U0 being MSAlgebra over S

for A being MSSubset of U0 st (Constants U0) \/ A is V8() holds

MSSubSort A is V8()

proof end;

theorem Th17: :: MSUALG_2:17

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for U0 being MSAlgebra over S

for A, B being MSSubset of U0 st B in SubSort A holds

(((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o

for o being OperSymbol of S

for U0 being MSAlgebra over S

for A, B being MSSubset of U0 st B in SubSort A holds

(((MSSubSort A) #) * the Arity of S) . o c= ((B #) * the Arity of S) . o

proof end;

theorem Th18: :: MSUALG_2:18

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for U0 being MSAlgebra over S

for A, B being MSSubset of U0 st B in SubSort A holds

rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o

for o being OperSymbol of S

for U0 being MSAlgebra over S

for A, B being MSSubset of U0 st B in SubSort A holds

rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o

proof end;

theorem Th19: :: MSUALG_2:19

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o

for o being OperSymbol of S

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds rng ((Den (o,U0)) | ((((MSSubSort A) #) * the Arity of S) . o)) c= ((MSSubSort A) * the ResultSort of S) . o

proof end;

theorem Th20: :: MSUALG_2:20

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds

( MSSubSort A is opers_closed & A c= MSSubSort A )

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds

( MSSubSort A is opers_closed & A c= MSSubSort A )

proof end;

begin

::

:: Operations on Subalgebras of a Many Sorted Algebra.

::

:: Operations on Subalgebras of a Many Sorted Algebra.

::

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let A be MSSubset of U0;

assume A1: A is opers_closed ;

MSAlgebra(# A,(Opers (U0,A)) #) is strict MSSubAlgebra of U0

end;
let U0 be MSAlgebra over S;

let A be MSSubset of U0;

assume A1: A is opers_closed ;

func U0 | A -> strict MSSubAlgebra of U0 equals :Def15: :: MSUALG_2:def 15

MSAlgebra(# A,(Opers (U0,A)) #);

coherence MSAlgebra(# A,(Opers (U0,A)) #);

MSAlgebra(# A,(Opers (U0,A)) #) is strict MSSubAlgebra of U0

proof end;

:: deftheorem Def15 defines | MSUALG_2:def 15 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 st A is opers_closed holds

U0 | A = MSAlgebra(# A,(Opers (U0,A)) #);

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 st A is opers_closed holds

U0 | A = MSAlgebra(# A,(Opers (U0,A)) #);

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let U1, U2 be MSSubAlgebra of U0;

ex b_{1} being strict MSSubAlgebra of U0 st

( the Sorts of b_{1} = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b_{1} holds

( B is opers_closed & the Charact of b_{1} = Opers (U0,B) ) ) )

for b_{1}, b_{2} being strict MSSubAlgebra of U0 st the Sorts of b_{1} = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b_{1} holds

( B is opers_closed & the Charact of b_{1} = Opers (U0,B) ) ) & the Sorts of b_{2} = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b_{2} holds

( B is opers_closed & the Charact of b_{2} = Opers (U0,B) ) ) holds

b_{1} = b_{2}
by Th9;

end;
let U0 be MSAlgebra over S;

let U1, U2 be MSSubAlgebra of U0;

func U1 /\ U2 -> strict MSSubAlgebra of U0 means :Def16: :: MSUALG_2:def 16

( the Sorts of it = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of it holds

( B is opers_closed & the Charact of it = Opers (U0,B) ) ) );

existence ( the Sorts of it = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of it holds

( B is opers_closed & the Charact of it = Opers (U0,B) ) ) );

ex b

( the Sorts of b

( B is opers_closed & the Charact of b

proof end;

uniqueness for b

( B is opers_closed & the Charact of b

( B is opers_closed & the Charact of b

b

:: deftheorem Def16 defines /\ MSUALG_2:def 16 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0

for b_{5} being strict MSSubAlgebra of U0 holds

( b_{5} = U1 /\ U2 iff ( the Sorts of b_{5} = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b_{5} holds

( B is opers_closed & the Charact of b_{5} = Opers (U0,B) ) ) ) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0

for b

( b

( B is opers_closed & the Charact of b

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

let A be MSSubset of U0;

ex b_{1} being strict MSSubAlgebra of U0 st

( A is MSSubset of b_{1} & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds

b_{1} is MSSubAlgebra of U1 ) )

for b_{1}, b_{2} being strict MSSubAlgebra of U0 st A is MSSubset of b_{1} & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds

b_{1} is MSSubAlgebra of U1 ) & A is MSSubset of b_{2} & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds

b_{2} is MSSubAlgebra of U1 ) holds

b_{1} = b_{2}

end;
let U0 be MSAlgebra over S;

let A be MSSubset of U0;

func GenMSAlg A -> strict MSSubAlgebra of U0 means :Def17: :: MSUALG_2:def 17

( A is MSSubset of it & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds

it is MSSubAlgebra of U1 ) );

existence ( A is MSSubset of it & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds

it is MSSubAlgebra of U1 ) );

ex b

( A is MSSubset of b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def17 defines GenMSAlg MSUALG_2:def 17 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0

for b_{4} being strict MSSubAlgebra of U0 holds

( b_{4} = GenMSAlg A iff ( A is MSSubset of b_{4} & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds

b_{4} is MSSubAlgebra of U1 ) ) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0

for b

( b

b

registration

let S be non empty non void ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

let A be V8() MSSubset of U0;

coherence

GenMSAlg A is non-empty

end;
let U0 be non-empty MSAlgebra over S;

let A be V8() MSSubset of U0;

coherence

GenMSAlg A is non-empty

proof end;

theorem Th21: :: MSUALG_2:21

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

for U0 being MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

proof end;

theorem Th22: :: MSUALG_2:22

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for U1 being MSSubAlgebra of U0

for B being MSSubset of U0 st B = the Sorts of U1 holds

GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

for U0 being MSAlgebra over S

for U1 being MSSubAlgebra of U0

for B being MSSubset of U0 st B = the Sorts of U1 holds

GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

proof end;

theorem Th23: :: MSUALG_2:23

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)

for U0 being non-empty MSAlgebra over S

for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

let U1, U2 be MSSubAlgebra of U0;

ex b_{1} being strict MSSubAlgebra of U0 st

for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds

b_{1} = GenMSAlg A

for b_{1}, b_{2} being strict MSSubAlgebra of U0 st ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds

b_{1} = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds

b_{2} = GenMSAlg A ) holds

b_{1} = b_{2}

end;
let U0 be non-empty MSAlgebra over S;

let U1, U2 be MSSubAlgebra of U0;

func U1 "\/" U2 -> strict MSSubAlgebra of U0 means :Def18: :: MSUALG_2:def 18

for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds

it = GenMSAlg A;

existence for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds

it = GenMSAlg A;

ex b

for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def18 defines "\/" MSUALG_2:def 18 :

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0

for b_{5} being strict MSSubAlgebra of U0 holds

( b_{5} = U1 "\/" U2 iff for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds

b_{5} = GenMSAlg A );

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0

for b

( b

b

theorem Th24: :: MSUALG_2:24

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1 being MSSubAlgebra of U0

for A, B being MSSubset of U0 st B = A \/ the Sorts of U1 holds

(GenMSAlg A) "\/" U1 = GenMSAlg B

for U0 being non-empty MSAlgebra over S

for U1 being MSSubAlgebra of U0

for A, B being MSSubset of U0 st B = A \/ the Sorts of U1 holds

(GenMSAlg A) "\/" U1 = GenMSAlg B

proof end;

theorem Th25: :: MSUALG_2:25

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1 being MSSubAlgebra of U0

for B being MSSubset of U0 st B = the Sorts of U0 holds

(GenMSAlg B) "\/" U1 = GenMSAlg B

for U0 being non-empty MSAlgebra over S

for U1 being MSSubAlgebra of U0

for B being MSSubset of U0 st B = the Sorts of U0 holds

(GenMSAlg B) "\/" U1 = GenMSAlg B

proof end;

theorem Th26: :: MSUALG_2:26

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1

for U0 being non-empty MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1

proof end;

theorem Th27: :: MSUALG_2:27

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

for U0 being non-empty MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

proof end;

theorem Th28: :: MSUALG_2:28

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

for U0 being non-empty MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

proof end;

begin

::

:: The Lattice of SubAlgebras of a Many Sorted Algebra.

::

:: The Lattice of SubAlgebras of a Many Sorted Algebra.

::

definition

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is strict MSSubAlgebra of U0 )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is strict MSSubAlgebra of U0 ) ) & ( for x being set holds

( x in b_{2} iff x is strict MSSubAlgebra of U0 ) ) holds

b_{1} = b_{2}

end;
let U0 be MSAlgebra over S;

func MSSub U0 -> set means :Def19: :: MSUALG_2:def 19

for x being set holds

( x in it iff x is strict MSSubAlgebra of U0 );

existence for x being set holds

( x in it iff x is strict MSSubAlgebra of U0 );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def19 defines MSSub MSUALG_2:def 19 :

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for b_{3} being set holds

( b_{3} = MSSub U0 iff for x being set holds

( x in b_{3} iff x is strict MSSubAlgebra of U0 ) );

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for b

( b

( x in b

registration

let S be non empty non void ManySortedSign ;

let U0 be MSAlgebra over S;

coherence

not MSSub U0 is empty

end;
let U0 be MSAlgebra over S;

coherence

not MSSub U0 is empty

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

ex b_{1} being BinOp of (MSSub U0) st

for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 "\/" U2

for b_{1}, b_{2} being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 "\/" U2 ) & ( for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{2} . (x,y) = U1 "\/" U2 ) holds

b_{1} = b_{2}

end;
let U0 be non-empty MSAlgebra over S;

func MSAlg_join U0 -> BinOp of (MSSub U0) means :Def20: :: MSUALG_2:def 20

for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 "\/" U2;

existence for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 "\/" U2;

ex b

for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b

proof end;

uniqueness for b

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b

b

proof end;

:: deftheorem Def20 defines MSAlg_join MSUALG_2:def 20 :

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for b_{3} being BinOp of (MSSub U0) holds

( b_{3} = MSAlg_join U0 iff for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{3} . (x,y) = U1 "\/" U2 );

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for b

( b

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b

definition

let S be non empty non void ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

ex b_{1} being BinOp of (MSSub U0) st

for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 /\ U2

for b_{1}, b_{2} being BinOp of (MSSub U0) st ( for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 /\ U2 ) & ( for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{2} . (x,y) = U1 /\ U2 ) holds

b_{1} = b_{2}

end;
let U0 be non-empty MSAlgebra over S;

func MSAlg_meet U0 -> BinOp of (MSSub U0) means :Def21: :: MSUALG_2:def 21

for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 /\ U2;

existence for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 /\ U2;

ex b

for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b

proof end;

uniqueness for b

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b

b

proof end;

:: deftheorem Def21 defines MSAlg_meet MSUALG_2:def 21 :

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for b_{3} being BinOp of (MSSub U0) holds

( b_{3} = MSAlg_meet U0 iff for x, y being Element of MSSub U0

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{3} . (x,y) = U1 /\ U2 );

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for b

( b

for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds

b

theorem Th29: :: MSUALG_2:29

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is commutative

for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is commutative

proof end;

theorem Th30: :: MSUALG_2:30

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is associative

for U0 being non-empty MSAlgebra over S holds MSAlg_join U0 is associative

proof end;

theorem Th31: :: MSUALG_2:31

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is commutative

for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is commutative

proof end;

theorem Th32: :: MSUALG_2:32

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is associative

for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is associative

proof end;

definition

let S be non empty non void ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice

end;
let U0 be non-empty MSAlgebra over S;

func MSSubAlLattice U0 -> strict Lattice equals :: MSUALG_2:def 22

LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);

coherence LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);

LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice

proof end;

:: deftheorem defines MSSubAlLattice MSUALG_2:def 22 :

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);

theorem Th33: :: MSUALG_2:33

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 is bounded

for U0 being non-empty MSAlgebra over S holds MSSubAlLattice U0 is bounded

proof end;

registration

let S be non empty non void ManySortedSign ;

let U0 be non-empty MSAlgebra over S;

coherence

MSSubAlLattice U0 is bounded by Th33;

end;
let U0 be non-empty MSAlgebra over S;

coherence

MSSubAlLattice U0 is bounded by Th33;

theorem :: MSUALG_2:34

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S holds Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0)

for U0 being non-empty MSAlgebra over S holds Bottom (MSSubAlLattice U0) = GenMSAlg (Constants U0)

proof end;

theorem Th35: :: MSUALG_2:35

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

Top (MSSubAlLattice U0) = GenMSAlg B

for U0 being non-empty MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

Top (MSSubAlLattice U0) = GenMSAlg B

proof end;

theorem :: MSUALG_2:36

for S being non empty non void ManySortedSign

for U0 being non-empty MSAlgebra over S holds Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

for U0 being non-empty MSAlgebra over S holds Top (MSSubAlLattice U0) = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

proof end;

theorem :: MSUALG_2:37

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1;

for U0 being MSAlgebra over S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1;

theorem :: MSUALG_2:38

theorem :: MSUALG_2:39

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds SubSort A c= SubSort U0

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds SubSort A c= SubSort U0

proof end;

:: Subalgebras of a Many Sorted Algebra.

::