:: MSUALG_2 semantic presentation

registration

let I be set ;
let X be ManySortedSet of I;
let Y be V6 ManySortedSet of I;
cluster X \/ Y -> V6 ;
coherence

proof end;

cluster Y \/ X -> V6 ;
coherence ;

end;

theorem :: MSUALG_2:1

canceled;

theorem Th2: :: MSUALG_2:2

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

proof end;

definition

let S be non empty ManySortedSign ;
let U0 be MSAlgebra of S;
mode MSSubset of U0 is ManySortedSubset of the Sorts of U0;

end;

definition

let S be non empty ManySortedSign ;
let IT be SortSymbol of S;
canceled;
attr IT is with_const_op means :Def2: :: MSUALG_2:def 2
ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = IT );

end;

:: deftheorem MSUALG_2:def 1 :

:: deftheorem Def2 defines with_const_op MSUALG_2:def 2 :

definition

let IT be non empty ManySortedSign ;
attr IT is all-with_const_op means :Def3: :: MSUALG_2:def 3
for s being SortSymbol of IT holds s is with_const_op;

end;

:: deftheorem Def3 defines all-with_const_op MSUALG_2:def 3 :

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;
cluster ManySortedSign(# A,B,a,r #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty strict non void all-with_const_op ManySortedSign ;
existence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let s be SortSymbol of S;
func Constants U0,s -> Subset of (the Sorts of U0 . s) means :Def4: :: MSUALG_2:def 4
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

proof end;

correctness ;

end;

:: deftheorem Def4 defines Constants MSUALG_2:def 4 :

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
func Constants U0 -> MSSubset of U0 means :Def5: :: MSUALG_2:def 5
for s being SortSymbol of S holds it . s = Constants U0,s;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Constants MSUALG_2:def 5 :

registration

let S be non empty non void all-with_const_op ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
let s be SortSymbol of S;
cluster Constants U0,s -> non empty ;
coherence

proof end;

end;

registration

let S be non empty non void all-with_const_op ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
cluster Constants U0 -> V6 ;
coherence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let o be OperSymbol of S;
let A be MSSubset of U0;
pred A is_closed_on o means :Def6: :: MSUALG_2:def 6
rng ((Den o,U0) | (((A # ) * the Arity of S) . o)) c= (A * the ResultSort of S) . o;

end;

:: deftheorem Def6 defines is_closed_on MSUALG_2:def 6 :

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
attr A is opers_closed means :Def7: :: MSUALG_2:def 7
for o being OperSymbol of S holds A is_closed_on o;

end;

:: deftheorem Def7 defines opers_closed MSUALG_2:def 7 :

theorem Th3: :: MSUALG_2:3

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra of 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 of 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 :Def8: :: MSUALG_2:def 8
(Den o,U0) | (((A # ) * the Arity of S) . o);
coherence

proof end;

end;

:: deftheorem Def8 defines /. MSUALG_2:def 8 :

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
func Opers U0,A -> ManySortedFunction of (A # ) * the Arity of S,A * the ResultSort of S means :Def9: :: MSUALG_2:def 9
for o being OperSymbol of S holds it . o = o /. A;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Opers MSUALG_2:def 9 :

theorem Th4: :: MSUALG_2:4

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 Th5: :: MSUALG_2:5

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 of S;
mode MSSubAlgebra of U0 -> MSAlgebra of S means :Def10: :: MSUALG_2:def 10
( 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

proof end;

end;

:: deftheorem Def10 defines MSSubAlgebra MSUALG_2:def 10 :

Lm1: for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 of S;
cluster strict MSSubAlgebra of U0;
existence

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
cluster MSAlgebra(# the Sorts of U0,the Charact of U0 #) -> non-empty ;
coherence by MSUALG_1:def 8;

end;

registration

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
cluster strict non-empty MSSubAlgebra of U0;
existence

proof end;

end;

theorem :: MSUALG_2:6

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S holds U0 is MSSubAlgebra of U0

proof end;

theorem :: MSUALG_2:7

for S being non empty non void ManySortedSign
for U0, U1, U2 being MSAlgebra of S st U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 holds
U0 is MSSubAlgebra of U2

proof end;

theorem Th8: :: MSUALG_2:8

for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S st U1 is strict MSSubAlgebra of U2 & U2 is strict MSSubAlgebra of U1 holds
U1 = U2

proof end;

theorem Th9: :: MSUALG_2:9

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 Th10: :: MSUALG_2:10

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for U1, U2 being strict MSSubAlgebra of U0 st the Sorts of U1 = the Sorts of U2 holds
U1 = U2

proof end;

theorem Th11: :: MSUALG_2:11

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for U1 being MSSubAlgebra of U0 holds Constants U0 is MSSubset of U1

proof end;

theorem :: MSUALG_2:12

for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1 being non-empty MSSubAlgebra of U0 holds Constants U0 is V6 MSSubset of U1 by Th11;

theorem :: MSUALG_2:13

for S being non empty non void all-with_const_op ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is non-empty

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
func SubSort A -> 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 & Constants U0 c= B & A c= B ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines SubSort MSUALG_2:def 11 :

Lm2: for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 of S;
let A be MSSubset of U0;
cluster SubSort A -> non empty ;
coherence by Lm2;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
func SubSort U0 -> set means :Def12: :: MSUALG_2:def 12
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines SubSort MSUALG_2:def 12 :

registration

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
cluster SubSort U0 -> non empty ;
coherence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let e be Element of SubSort U0;
func @ e -> MSSubset of U0 equals :: MSUALG_2:def 13
e;
coherence by Def12;

end;

:: deftheorem defines @ MSUALG_2:def 13 :

theorem Th14: :: MSUALG_2:14

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 Th15: :: MSUALG_2:15

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 of S;
let A be MSSubset of U0;
let s be SortSymbol of S;
func SubSort A,s -> set means :Def14: :: MSUALG_2:def 14
for x being set holds
( x in it iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines SubSort MSUALG_2:def 14 :

registration

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
let s be SortSymbol of S;
cluster SubSort A,s -> non empty ;
coherence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
func MSSubSort A -> MSSubset of U0 means :Def15: :: MSUALG_2:def 15
for s being SortSymbol of S holds it . s = meet (SubSort A,s);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines MSSubSort MSUALG_2:def 15 :

theorem Th16: :: MSUALG_2:16

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A

proof end;

theorem Th17: :: MSUALG_2:17

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 st (Constants U0) \/ A is non-empty holds
MSSubSort A is non-empty

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 of 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 Th19: :: MSUALG_2:19

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra of 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 Th20: :: MSUALG_2:20

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U0 being MSAlgebra of 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 Th21: :: MSUALG_2:21

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds
( MSSubSort A is opers_closed & A c= MSSubSort A )

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
assume A1: A is opers_closed ;
func U0 | A -> strict MSSubAlgebra of U0 equals :Def16: :: MSUALG_2:def 16
MSAlgebra(# A,(Opers U0,A) #);
coherence

proof end;

end;

:: deftheorem Def16 defines | MSUALG_2:def 16 :

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let U1, U2 be MSSubAlgebra of U0;
func U1 /\ U2 -> strict MSSubAlgebra of U0 means :Def17: :: MSUALG_2:def 17
( 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

proof end;

uniqueness by Th10;

end;

:: deftheorem Def17 defines /\ MSUALG_2:def 17 :

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
let A be MSSubset of U0;
func GenMSAlg A -> strict MSSubAlgebra of U0 means :Def18: :: MSUALG_2:def 18
( A is MSSubset of it & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
it is MSSubAlgebra of U1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines GenMSAlg MSUALG_2:def 18 :

registration

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
let A be V6 MSSubset of U0;
cluster GenMSAlg A -> strict non-empty ;
coherence

proof end;

end;

theorem Th22: :: MSUALG_2:22

for S being non empty non void ManySortedSign
for U0 being strict MSAlgebra of S
for B being MSSubset of U0 st B = the Sorts of U0 holds
GenMSAlg B = U0

proof end;

theorem Th23: :: MSUALG_2:23

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for U1 being strict MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = U1

proof end;

theorem Th24: :: MSUALG_2:24

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of 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 of S;
let U1, U2 be MSSubAlgebra of U0;
func U1 "\/" U2 -> strict MSSubAlgebra of U0 means :Def19: :: MSUALG_2:def 19
for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
it = GenMSAlg A;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines "\/" MSUALG_2:def 19 :

theorem Th25: :: MSUALG_2:25

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of 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 Th26: :: MSUALG_2:26

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of 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 Th27: :: MSUALG_2:27

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1

proof end;

theorem Th28: :: MSUALG_2:28

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being strict MSSubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1

proof end;

theorem Th29: :: MSUALG_2:29

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being strict MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
func MSSub U0 -> set means :Def20: :: MSUALG_2:def 20
for x being set holds
( x in it iff x is strict MSSubAlgebra of U0 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines MSSub MSUALG_2:def 20 :

registration

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of S;
cluster MSSub U0 -> non empty ;
coherence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
func MSAlg_join 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines MSAlg_join MSUALG_2:def 21 :

definition

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
func MSAlg_meet U0 -> BinOp of MSSub U0 means :Def22: :: MSUALG_2:def 22
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines MSAlg_meet MSUALG_2:def 22 :

theorem Th30: :: MSUALG_2:30

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSAlg_join U0 is commutative

proof end;

theorem Th31: :: MSUALG_2:31

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSAlg_join U0 is associative

proof end;

theorem Th32: :: MSUALG_2:32

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSAlg_meet U0 is commutative

proof end;

theorem Th33: :: MSUALG_2:33

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSAlg_meet U0 is associative

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
func MSSubAlLattice U0 -> strict Lattice equals :: MSUALG_2:def 23
LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);
coherence

proof end;

end;

:: deftheorem defines MSSubAlLattice MSUALG_2:def 23 :

theorem Th34: :: MSUALG_2:34

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSSubAlLattice U0 is bounded

proof end;

registration

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra of S;
cluster MSSubAlLattice U0 -> strict bounded ;
coherence by Th34;

end;

theorem :: MSUALG_2:35

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

proof end;

theorem Th36: :: MSUALG_2:36

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for B being MSSubset of U0 st B = the Sorts of U0 holds
Top (MSSubAlLattice U0) = GenMSAlg B

proof end;

theorem :: MSUALG_2:37

for S being non empty non void ManySortedSign
for U0 being strict non-empty MSAlgebra of S holds Top (MSSubAlLattice U0) = U0

proof end;

theorem :: MSUALG_2:38

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S holds MSAlgebra(# the Sorts of U0,the Charact of U0 #) is MSSubAlgebra of U0 by Lm1;

theorem :: MSUALG_2:39

canceled;

theorem :: MSUALG_2:40

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds the Sorts of U0 in SubSort A by Lm2;

theorem :: MSUALG_2:41

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds SubSort A c= SubSort U0

proof end;