:: OSALG_2 semantic presentation

theorem Th1: :: OSALG_2:1

for R being non empty Poset
for X, Y being OrderSortedSet of R holds X /\ Y is OrderSortedSet of R

proof end;

theorem Th2: :: OSALG_2:2

for R being non empty Poset
for X, Y being OrderSortedSet of R holds X \/ Y is OrderSortedSet of R

proof end;

definition

let R be non empty Poset;
let M be OrderSortedSet of R;
mode OrderSortedSubset of M -> ManySortedSubset of M means :Def1: :: OSALG_2:def 1
it is OrderSortedSet of R;
existence

proof end;

end;

:: deftheorem Def1 defines OrderSortedSubset OSALG_2:def 1 :

registration

let R be non empty Poset;
let M be V3 OrderSortedSet of R;
cluster V3 OrderSortedSubset of M;
existence

proof end;

end;

definition

let S be OrderSortedSign;
let U0 be OSAlgebra of S;
mode OSSubset of U0 -> ManySortedSubset of the Sorts of U0 means :Def2: :: OSALG_2:def 2
it is OrderSortedSet of S;
existence

proof end;

end;

:: deftheorem Def2 defines OSSubset OSALG_2:def 2 :

registration

let S be OrderSortedSign;
cluster strict non-empty monotone MSAlgebra of S;
existence

proof end;

end;

registration

let S be OrderSortedSign;
let U0 be non-empty OSAlgebra of S;
cluster V3 OSSubset of U0;
existence

proof end;

end;

theorem Th3: :: OSALG_2:3

for S0 being non empty strict non void all-with_const_op ManySortedSign holds OSSign S0 is all-with_const_op

proof end;

registration

cluster strict all-with_const_op OverloadedRSSign ;
existence

proof end;

end;

theorem Th4: :: OSALG_2:4

for S being OrderSortedSign
for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0,the Charact of U0 #) is order-sorted

proof end;

registration

let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster order-sorted MSSubAlgebra of U0;
existence

proof end;

end;

definition

let S be OrderSortedSign;
let U0 be OSAlgebra of S;
mode OSSubAlgebra of U0 is order-sorted MSSubAlgebra of U0;

end;

registration

let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster strict MSSubAlgebra of U0;
existence

proof end;

end;

registration

let S be OrderSortedSign;
let U0 be non-empty OSAlgebra of S;
cluster strict non-empty MSSubAlgebra of U0;
existence

proof end;

end;

theorem Th5: :: OSALG_2:5

for S being OrderSortedSign
for U0 being OSAlgebra of S
for U1 being MSAlgebra of S holds
( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers U0,B ) ) ) )

proof end;

definition

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let s be SortSymbol of S1;
func OSConstants OU0,s -> Subset of (the Sorts of OU0 . s) equals :: OSALG_2:def 3
union { (Constants OU0,s2) where s2 is SortSymbol of S1 : s2 <= s } ;
coherence

proof end;

end;

:: deftheorem defines OSConstants OSALG_2:def 3 :

theorem :: OSALG_2:6

canceled;

theorem :: OSALG_2:7

canceled;

theorem :: OSALG_2:8

canceled;

theorem :: OSALG_2:9

canceled;

theorem :: OSALG_2:10

canceled;

theorem Th11: :: OSALG_2:11

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for s being SortSymbol of S1 holds Constants OU0,s c= OSConstants OU0,s

proof end;

definition

let S1 be OrderSortedSign;
let M be ManySortedSet of the carrier of S1;
func OSCl M -> OrderSortedSet of S1 means :Def4: :: OSALG_2:def 4
for s being SortSymbol of S1 holds it . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines OSCl OSALG_2:def 4 :

theorem Th12: :: OSALG_2:12

for S1 being OrderSortedSign
for M being ManySortedSet of the carrier of S1 holds M c= OSCl M

proof end;

theorem Th13: :: OSALG_2:13

for S1 being OrderSortedSign
for M being ManySortedSet of the carrier of S1
for A being OrderSortedSet of S1 st M c= A holds
OSCl M c= A

proof end;

theorem :: OSALG_2:14

for S being OrderSortedSign
for X being OrderSortedSet of S holds OSCl X = X

proof end;

definition

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
func OSConstants OU0 -> OSSubset of OU0 means :Def5: :: OSALG_2:def 5
for s being SortSymbol of S1 holds it . s = OSConstants OU0,s;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines OSConstants OSALG_2:def 5 :

theorem Th15: :: OSALG_2:15

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0

proof end;

theorem Th16: :: OSALG_2:16

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st Constants OU0 c= A holds
OSConstants OU0 c= A

proof end;

theorem :: OSALG_2:17

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)

proof end;

theorem Th18: :: OSALG_2:18

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1

proof end;

theorem :: OSALG_2:19

for S being all-with_const_op OrderSortedSign
for OU0 being non-empty OSAlgebra of S
for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V3 OSSubset of OU1

proof end;

theorem Th20: :: OSALG_2:20

for I being set
for M being ManySortedSet of I
for x being set holds
( x is ManySortedSubset of M iff x in product (bool M) )

proof end;

definition

let R be non empty Poset;
let M be OrderSortedSet of R;
func OSbool M -> set means :: OSALG_2:def 6
for x being set holds
( x in it iff x is OrderSortedSubset of M );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines OSbool OSALG_2:def 6 :

definition

let S be OrderSortedSign;
let U0 be OSAlgebra of S;
let A be OSSubset of U0;
func OSSubSort A -> set equals :: OSALG_2:def 7
{ x where x is Element of SubSort A : x is OrderSortedSet of S } ;
correctness ;

end;

:: deftheorem defines OSSubSort OSALG_2:def 7 :

theorem Th21: :: OSALG_2:21

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= SubSort A

proof end;

theorem Th22: :: OSALG_2:22

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A

proof end;

registration

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
cluster OSSubSort A -> non empty ;
coherence by Th22;

end;

definition

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
func OSSubSort OU0 -> set equals :: OSALG_2:def 8
{ x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;
correctness ;

end;

:: deftheorem defines OSSubSort OSALG_2:def 8 :

theorem Th23: :: OSALG_2:23

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0

proof end;

registration

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
cluster OSSubSort OU0 -> non empty ;
coherence

proof end;

end;

definition

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let e be Element of OSSubSort OU0;
func @ e -> OSSubset of OU0 equals :: OSALG_2:def 9
e;
coherence

proof end;

end;

:: deftheorem defines @ OSALG_2:def 9 :

theorem Th24: :: OSALG_2:24

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A, B being OSSubset of OU0 holds
( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )

proof end;

theorem Th25: :: OSALG_2:25

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for B being OSSubset of OU0 holds
( B in OSSubSort OU0 iff B is opers_closed )

proof end;

definition

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
let s be Element of S1;
func OSSubSort A,s -> set means :Def10: :: OSALG_2:def 10
for x being set holds
( x in it iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines OSSubSort OSALG_2:def 10 :

theorem Th26: :: OSALG_2:26

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort A,s2 is_coarser_than OSSubSort A,s1

proof end;

theorem Th27: :: OSALG_2:27

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being SortSymbol of S1 holds OSSubSort A,s c= SubSort A,s

proof end;

theorem Th28: :: OSALG_2:28

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0
for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort A,s

proof end;

registration

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
let s be SortSymbol of S1;
cluster OSSubSort A,s -> non empty ;
coherence by Th28;

end;

definition

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
func OSMSubSort A -> OSSubset of OU0 means :Def11: :: OSALG_2:def 11
for s being SortSymbol of S1 holds it . s = meet (OSSubSort A,s);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines OSMSubSort OSALG_2:def 11 :

registration

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
cluster opers_closed OSSubset of OU0;
existence

proof end;

end;

theorem Th29: :: OSALG_2:29

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds (OSConstants OU0) \/ A c= OSMSubSort A

proof end;

theorem :: OSALG_2:30

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st (OSConstants OU0) \/ A is non-empty holds
OSMSubSort A is non-empty

proof end;

theorem Th31: :: OSALG_2:31

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
(((OSMSubSort A) # ) * the Arity of S1) . o c= ((B # ) * the Arity of S1) . o

proof end;

theorem Th32: :: OSALG_2:32

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A, B being OSSubset of OU0 st B in OSSubSort A holds
rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o

proof end;

theorem Th33: :: OSALG_2:33

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for o being OperSymbol of S1
for A being OSSubset of OU0 holds rng ((Den o,OU0) | ((((OSMSubSort A) # ) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o

proof end;

theorem Th34: :: OSALG_2:34

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( OSMSubSort A is opers_closed & A c= OSMSubSort A )

proof end;

registration

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
cluster OSMSubSort A -> opers_closed ;
coherence by Th34;

end;

registration

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be opers_closed OSSubset of OU0;
cluster OU0 | A -> order-sorted ;
coherence

proof end;

end;

registration

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let OU1, OU2 be OSSubAlgebra of OU0;
cluster OU1 /\ OU2 -> order-sorted ;
coherence

proof end;

end;

definition

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
canceled;
func GenOSAlg A -> strict OSSubAlgebra of OU0 means :Def13: :: OSALG_2:def 13
( A is OSSubset of it & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
it is OSSubAlgebra of OU1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem OSALG_2:def 12 :

:: deftheorem Def13 defines GenOSAlg OSALG_2:def 13 :

theorem Th35: :: OSALG_2:35

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )

proof end;

theorem Th36: :: OSALG_2:36

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 holds
( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )

proof end;

theorem Th37: :: OSALG_2:37

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)

proof end;

theorem Th38: :: OSALG_2:38

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds GenMSAlg A is MSSubAlgebra of GenOSAlg A

proof end;

theorem Th39: :: OSALG_2:39

for S1 being OrderSortedSign
for OU0 being strict OSAlgebra of S1
for B being OSSubset of OU0 st B = the Sorts of OU0 holds
GenOSAlg B = OU0

proof end;

theorem Th40: :: OSALG_2:40

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for OU1 being strict OSSubAlgebra of OU0
for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1

proof end;

theorem Th41: :: OSALG_2:41

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)

proof end;

definition

let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
let U1, U2 be OSSubAlgebra of U0;
func U1 "\/"_os U2 -> strict OSSubAlgebra of U0 means :Def14: :: OSALG_2:def 14
for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
it = GenOSAlg A;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines "\/"_os OSALG_2:def 14 :

theorem Th42: :: OSALG_2:42

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0
for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B

proof end;

theorem Th43: :: OSALG_2:43

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0
for B being OSSubset of U0 st B = the Sorts of U0 holds
(GenOSAlg B) "\/"_os U1 = GenOSAlg B

proof end;

theorem Th44: :: OSALG_2:44

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1

proof end;

theorem Th45: :: OSALG_2:45

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1

proof end;

theorem Th46: :: OSALG_2:46

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2

proof end;

definition

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
func OSSub OU0 -> set means :Def15: :: OSALG_2:def 15
for x being set holds
( x in it iff x is strict OSSubAlgebra of OU0 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines OSSub OSALG_2:def 15 :

theorem Th47: :: OSALG_2:47

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds OSSub OU0 c= MSSub OU0

proof end;

registration

let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster OSSub U0 -> non empty ;
coherence

proof end;

end;

definition

let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
:: original: OSSub
redefine func OSSub OU0 -> Subset of (MSSub OU0);
coherence by Th47;

end;

definition

let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
func OSAlg_join U0 -> BinOp of OSSub U0 means :Def16: :: OSALG_2:def 16
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
it . x,y = U1 "\/"_os U2;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines OSAlg_join OSALG_2:def 16 :

definition

let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
func OSAlg_meet U0 -> BinOp of OSSub U0 means :Def17: :: OSALG_2:def 17
for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
it . x,y = U1 /\ U2;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines OSAlg_meet OSALG_2:def 17 :

theorem Th48: :: OSALG_2:48

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . x,y = (MSAlg_meet U0) . x,y

proof end;

theorem Th49: :: OSALG_2:49

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative

proof end;

theorem Th50: :: OSALG_2:50

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative

proof end;

theorem Th51: :: OSALG_2:51

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative

proof end;

theorem Th52: :: OSALG_2:52

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative

proof end;

definition

let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
func OSSubAlLattice U0 -> strict Lattice equals :: OSALG_2:def 18
LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);
coherence

proof end;

end;

:: deftheorem defines OSSubAlLattice OSALG_2:def 18 :

theorem Th53: :: OSALG_2:53

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded

proof end;

registration

let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
cluster OSSubAlLattice U0 -> strict bounded ;
coherence by Th53;

end;

theorem :: OSALG_2:54

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)

proof end;

theorem Th55: :: OSALG_2:55

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for B being OSSubset of U0 st B = the Sorts of U0 holds
Top (OSSubAlLattice U0) = GenOSAlg B

proof end;

theorem :: OSALG_2:56

for S1 being OrderSortedSign
for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0

proof end;