begin
theorem Th1:
theorem
theorem Th3:
theorem
canceled;
theorem
theorem Th6:
theorem Th7:
:: deftheorem Def1 defines "" EQUATION:def 1 :
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b4 being ManySortedSet of I holds
( b4 = F "" A iff for i being set st i in I holds
b4 . i = (F . i) " (A . i) );
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th14:
theorem Th15:
theorem
theorem
begin
theorem
canceled;
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
:: deftheorem Def2 defines SuperAlgebraSet EQUATION:def 2 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for B being MSSubAlgebra of A
for b4 being set holds
( b4 = SuperAlgebraSet B iff for x being set holds
( x in b4 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) );
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem
begin
:: deftheorem defines TermAlg EQUATION:def 3 :
for S being non empty non void ManySortedSign holds TermAlg S = FreeMSA ( the carrier of S --> NAT);
:: deftheorem defines Equations EQUATION:def 4 :
for S being non empty non void ManySortedSign holds Equations S = [| the Sorts of (TermAlg S), the Sorts of (TermAlg S)|];
theorem Th31:
theorem Th32:
:: deftheorem Def5 defines |= EQUATION:def 5 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for s being SortSymbol of S
for e being Element of (Equations S) . s holds
( A |= e iff for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds
(h . s) . (e `1) = (h . s) . (e `2) );
:: deftheorem Def6 defines |= EQUATION:def 6 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for E being EqualSet of S holds
( A |= E iff for s being SortSymbol of S
for e being Element of (Equations S) . s st e in E . s holds
A |= e );
theorem Th33:
theorem
theorem Th35:
theorem
theorem Th37:
theorem
Lm1:
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s
for I being non empty set
for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e
theorem Th39:
theorem