begin
theorem
canceled;
theorem Th2:
begin
:: deftheorem MSUALG_2:def 1 :
canceled;
:: deftheorem Def2 defines with_const_op MSUALG_2:def 2 :
:: deftheorem Def3 defines all-with_const_op MSUALG_2:def 3 :
:: deftheorem Def4 defines Constants MSUALG_2:def 4 :
:: deftheorem Def5 defines Constants MSUALG_2:def 5 :
begin
:: deftheorem Def6 defines is_closed_on MSUALG_2:def 6 :
:: deftheorem Def7 defines opers_closed MSUALG_2:def 7 :
theorem Th3:
:: deftheorem Def8 defines /. MSUALG_2:def 8 :
:: deftheorem Def9 defines Opers MSUALG_2:def 9 :
theorem Th4:
theorem Th5:
:: 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
theorem
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
begin
:: 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
:: deftheorem Def12 defines SubSort MSUALG_2:def 12 :
:: deftheorem defines @ MSUALG_2:def 13 :
theorem Th14:
theorem Th15:
:: deftheorem Def14 defines SubSort MSUALG_2:def 14 :
:: deftheorem Def15 defines MSSubSort MSUALG_2:def 15 :
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
:: deftheorem Def16 defines | MSUALG_2:def 16 :
:: deftheorem Def17 defines /\ MSUALG_2:def 17 :
:: deftheorem Def18 defines GenMSAlg MSUALG_2:def 18 :
theorem Th22:
theorem Th23:
theorem Th24:
:: deftheorem Def19 defines "\/" MSUALG_2:def 19 :
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
begin
:: deftheorem Def20 defines MSSub MSUALG_2:def 20 :
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:
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
ex b1 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
b1 . x,y = U1 "\/" U2
uniqueness
for b1, b2 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
b1 . 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
b2 . x,y = U1 "\/" U2 ) holds
b1 = b2
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:
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
ex b1 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
b1 . x,y = U1 /\ U2
uniqueness
for b1, b2 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
b1 . 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
b2 . x,y = U1 /\ U2 ) holds
b1 = b2
end;
:: deftheorem Def22 defines MSAlg_meet MSUALG_2:def 22 :
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
:: deftheorem defines MSSubAlLattice MSUALG_2:def 23 :
theorem Th34:
theorem
theorem Th36:
theorem
theorem
theorem
canceled;
theorem
theorem