:: MSUALG_8 semantic presentation

theorem Th1: :: MSUALG_8:1

for n being Nat
for p being FinSequence holds
( 1 <= n & n < len p iff ( n in dom p & n + 1 in dom p ) )

proof end;

scheme :: MSUALG_8:sch 1
NonUniqSeqEx{ F₁() -> Nat, P₁[ set , set ] } :

ex p being FinSequence st
( dom p = Seg F₁() & ( for k being Nat st k in Seg F₁() holds
P₁[k,p . k] ) )

provided

A1: for k being Nat st k in Seg F₁() holds
ex x being set st P₁[k,x]

proof end;

theorem Th2: :: MSUALG_8:2

for Y being set
for a, b being Element of (EqRelLatt Y)
for A, B being Equivalence_Relation of Y st a = A & b = B holds
( a [= b iff A c= B )

proof end;

registration

let Y be set ;
cluster EqRelLatt Y -> bounded ;
coherence

proof end;

end;

theorem :: MSUALG_8:3

for Y being set holds Bottom (EqRelLatt Y) = id Y

proof end;

theorem :: MSUALG_8:4

for Y being set holds Top (EqRelLatt Y) = nabla Y

proof end;

theorem Th5: :: MSUALG_8:5

for Y being set holds EqRelLatt Y is complete

proof end;

registration

let Y be set ;
cluster EqRelLatt Y -> bounded complete ;
coherence by Th5;

end;

theorem Th6: :: MSUALG_8:6

for Y being set
for X being Subset of (EqRelLatt Y) holds union X is Relation of Y

proof end;

theorem Th7: :: MSUALG_8:7

for Y being set
for X being Subset of (EqRelLatt Y) holds union X c= "\/" X

proof end;

theorem Th8: :: MSUALG_8:8

for Y being set
for X being Subset of (EqRelLatt Y)
for R being Relation of Y st R = union X holds
"\/" X = EqCl R

proof end;

theorem Th9: :: MSUALG_8:9

for Y being set
for X being Subset of (EqRelLatt Y)
for R being Relation st R = union X holds
R = R ~

proof end;

theorem Th10: :: MSUALG_8:10

for x, y, Y being set
for X being Subset of (EqRelLatt Y) st x in Y & y in Y holds
( [x,y] in "\/" X iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in union X ) ) )

proof end;

theorem Th11: :: MSUALG_8:11

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for B being Subset of (CongrLatt A) holds "/\" B,(EqRelLatt the Sorts of A) is MSCongruence of A

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let E be Element of (EqRelLatt the Sorts of A);
func CongrCl E -> MSCongruence of A equals :: MSUALG_8:def 1
"/\" { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A);
coherence

proof end;

end;

:: deftheorem defines CongrCl MSUALG_8:def 1 :

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let X be Subset of (EqRelLatt the Sorts of A);
func CongrCl X -> MSCongruence of A equals :: MSUALG_8:def 2
"/\" { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & X is_less_than x ) } ,(EqRelLatt the Sorts of A);
coherence

proof end;

end;

:: deftheorem defines CongrCl MSUALG_8:def 2 :

theorem :: MSUALG_8:12

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for C being Element of (EqRelLatt the Sorts of A) st C is MSCongruence of A holds
CongrCl C = C

proof end;

theorem :: MSUALG_8:13

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for X being Subset of (EqRelLatt the Sorts of A) holds CongrCl ("\/" X,(EqRelLatt the Sorts of A)) = CongrCl X

proof end;

theorem :: MSUALG_8:14

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for B1, B2 being Subset of (CongrLatt A)
for C1, C2 being MSCongruence of A st C1 = "\/" B1,(EqRelLatt the Sorts of A) & C2 = "\/" B2,(EqRelLatt the Sorts of A) holds
C1 "\/" C2 = "\/" (B1 \/ B2),(EqRelLatt the Sorts of A)

proof end;

theorem :: MSUALG_8:15

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for X being Subset of (CongrLatt A) holds "\/" X,(EqRelLatt the Sorts of A) = "\/" { ("\/" X0,(EqRelLatt the Sorts of A)) where X0 is Subset of (EqRelLatt the Sorts of A) : X0 is finite Subset of X } ,(EqRelLatt the Sorts of A)

proof end;

theorem Th16: :: MSUALG_8:16

for I being non empty set
for M being ManySortedSet of I
for i being Element of I
for e being Equivalence_Relation of M . i ex E being Equivalence_Relation of M st
( E . i = e & ( for j being Element of I st j <> i holds
E . j = nabla (M . j) ) )

proof end;

notation

let I be non empty set ;
let M be ManySortedSet of I;
let i be Element of I;
let X be Subset of (EqRelLatt M);
synonym EqRelSet X,i for pi M,I;

end;

definition

let I be non empty set ;
let M be ManySortedSet of I;
let i be Element of I;
let X be Subset of (EqRelLatt M);
:: original: EqRelSet
redefine func EqRelSet X,i -> Subset of (EqRelLatt (M . i)) means :Def3: :: MSUALG_8:def 3
for x being set holds
( x in it iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) );
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def3 defines EqRelSet MSUALG_8:def 3 :

theorem Th17: :: MSUALG_8:17

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for i being Element of S
for X being Subset of (EqRelLatt the Sorts of A)
for B being Equivalence_Relation of the Sorts of A st B = "\/" X holds
B . i = "\/" (EqRelSet X,i),(EqRelLatt (the Sorts of A . i))

proof end;

theorem Th18: :: MSUALG_8:18

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for X being Subset of (CongrLatt A) holds "\/" X,(EqRelLatt the Sorts of A) is MSCongruence of A

proof end;

theorem Th19: :: MSUALG_8:19

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S holds CongrLatt A is /\-inheriting

proof end;

theorem Th20: :: MSUALG_8:20

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S holds CongrLatt A is \/-inheriting

proof end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
cluster CongrLatt A -> /\-inheriting \/-inheriting ;
coherence by Th19, Th20;

end;