begin
theorem
canceled;
theorem Th2:
begin
:: deftheorem MSUALG_2:def 1 :
canceled;
:: deftheorem Def2 defines with_const_op MSUALG_2:def 2 :
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 ) );
:: deftheorem Def3 defines all-with_const_op MSUALG_2:def 3 :
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 );
:: deftheorem Def4 defines Constants MSUALG_2:def 4 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for s being SortSymbol of S
for b4 being Subset of ( the Sorts of U0 . s) holds
( ( the Sorts of U0 . s <> {} implies ( b4 = Constants (U0,s) iff ex A being non empty set st
( A = the Sorts of U0 . s & b4 = { 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 ( b4 = Constants (U0,s) iff b4 = {} ) ) );
:: deftheorem Def5 defines Constants MSUALG_2:def 5 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for b3 being MSSubset of U0 holds
( b3 = Constants U0 iff for s being SortSymbol of S holds b3 . s = Constants (U0,s) );
begin
:: deftheorem Def6 defines is_closed_on MSUALG_2:def 6 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 );
:: deftheorem Def7 defines opers_closed MSUALG_2:def 7 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 Th3:
:: deftheorem Def8 defines /. MSUALG_2:def 8 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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);
:: deftheorem Def9 defines Opers MSUALG_2:def 9 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0
for b4 being ManySortedFunction of (A #) * the Arity of S,A * the ResultSort of S holds
( b4 = Opers (U0,A) iff for o being OperSymbol of S holds b4 . o = o /. A );
theorem Th4:
theorem Th5:
:: deftheorem Def10 defines MSSubAlgebra MSUALG_2:def 10 :
for S being non empty non void ManySortedSign
for U0, b3 being MSAlgebra of S holds
( b3 is MSSubAlgebra of U0 iff ( the Sorts of b3 is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b3 holds
( B is opers_closed & the Charact of b3 = Opers (U0,B) ) ) ) );
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 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0
for b4 being set holds
( b4 = SubSort A iff for x being set holds
( x in b4 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 ) ) ) ) );
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 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for b3 being set holds
( b3 = SubSort U0 iff for x being set holds
( x in b3 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 ) ) ) );
:: deftheorem defines @ MSUALG_2:def 13 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for e being Element of SubSort U0 holds @ e = e;
theorem Th14:
theorem Th15:
:: deftheorem Def14 defines SubSort MSUALG_2:def 14 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0
for s being SortSymbol of S
for b5 being set holds
( b5 = SubSort (A,s) iff for x being set holds
( x in b5 iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) );
:: deftheorem Def15 defines MSSubSort MSUALG_2:def 15 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A, b4 being MSSubset of U0 holds
( b4 = MSSubSort A iff for s being SortSymbol of S holds b4 . s = meet (SubSort (A,s)) );
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
begin
:: deftheorem Def16 defines | MSUALG_2:def 16 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0 st A is opers_closed holds
U0 | A = MSAlgebra(# A,(Opers (U0,A)) #);
:: deftheorem Def17 defines /\ MSUALG_2:def 17 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for U1, U2 being MSSubAlgebra of U0
for b5 being strict MSSubAlgebra of U0 holds
( b5 = U1 /\ U2 iff ( the Sorts of b5 = the Sorts of U1 /\ the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b5 holds
( B is opers_closed & the Charact of b5 = Opers (U0,B) ) ) ) );
:: deftheorem Def18 defines GenMSAlg MSUALG_2:def 18 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubset of U0
for b4 being strict MSSubAlgebra of U0 holds
( b4 = GenMSAlg A iff ( A is MSSubset of b4 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b4 is MSSubAlgebra of U1 ) ) );
theorem Th22:
theorem Th23:
theorem Th24:
:: deftheorem Def19 defines "\/" MSUALG_2:def 19 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for U1, U2 being MSSubAlgebra of U0
for b5 being strict MSSubAlgebra of U0 holds
( b5 = U1 "\/" U2 iff for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b5 = GenMSAlg A );
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
begin
:: deftheorem Def20 defines MSSub MSUALG_2:def 20 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for b3 being set holds
( b3 = MSSub U0 iff for x being set holds
( x in b3 iff x is strict MSSubAlgebra of U0 ) );
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 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for b3 being BinOp of (MSSub U0) holds
( b3 = 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
b3 . (x,y) = U1 "\/" U2 );
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 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for b3 being BinOp of (MSSub U0) holds
( b3 = 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
b3 . (x,y) = U1 /\ U2 );
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
:: deftheorem defines MSSubAlLattice MSUALG_2:def 23 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S holds MSSubAlLattice U0 = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);
theorem Th34:
theorem
theorem Th36:
theorem
theorem
theorem
canceled;
theorem
theorem