:: MSUALG_5 semantic presentation

theorem Th1: :: MSUALG_5:1

for X being set
for EqR1, EqR2, EqR3 being Equivalence_Relation of X holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)

proof end;

definition

let X be set ;
let R be Relation of X;
func EqCl R -> Equivalence_Relation of X means :Def1: :: MSUALG_5:def 1
( R c= it & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
it c= EqR2 ) );
existence by EQREL_1:20;
uniqueness

proof end;

end;

:: deftheorem Def1 defines EqCl MSUALG_5:def 1 :

theorem Th2: :: MSUALG_5:2

for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)

proof end;

theorem Th3: :: MSUALG_5:3

for X being set
for EqR1 being Equivalence_Relation of X holds EqCl EqR1 = EqR1

proof end;

theorem Th4: :: MSUALG_5:4

for X being set
for R1 being Relation of X holds (nabla X) \/ R1 = nabla X

proof end;

definition

let X be set ;
func EqRelLatt X -> strict Lattice means :: MSUALG_5:def 2
( the carrier of it = { x where x is Relation of X,X : x is Equivalence_Relation of X } & ( for x, y being Equivalence_Relation of X holds
( the L_meet of it . x,y = x /\ y & the L_join of it . x,y = x "\/" y ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines EqRelLatt MSUALG_5:def 2 :

registration

let I be set ;
let M be ManySortedSet of I;
cluster MSEquivalence_Relation-like ManySortedRelation of M,M;
existence

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
mode Equivalence_Relation of M is MSEquivalence_Relation-like ManySortedRelation of M;

end;

definition

let I be non empty set ;
let M be ManySortedSet of I;
let R be ManySortedRelation of M;
func EqCl R -> Equivalence_Relation of M means :Def3: :: MSUALG_5:def 3
for i being Element of I holds it . i = EqCl (R . i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines EqCl MSUALG_5:def 3 :

theorem :: MSUALG_5:5

for I being non empty set
for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqCl EqR = EqR

proof end;

definition

let I be non empty set ;
let M be ManySortedSet of I;
let EqR1, EqR2 be Equivalence_Relation of M;
func EqR1 "\/" EqR2 -> Equivalence_Relation of M means :Def4: :: MSUALG_5:def 4
ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & it = EqCl EqR3 );
existence

proof end;

uniqueness ;
commutativity ;

end;

:: deftheorem Def4 defines "\/" MSUALG_5:def 4 :

theorem Th6: :: MSUALG_5:6

for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 \/ EqR2 c= EqR1 "\/" EqR2

proof end;

theorem Th7: :: MSUALG_5:7

for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR1 "\/" EqR2 c= EqR

proof end;

theorem Th8: :: MSUALG_5:8

for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR3 being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR3 & ( for EqR being Equivalence_Relation of M st EqR1 \/ EqR2 c= EqR holds
EqR3 c= EqR ) holds
EqR3 = EqR1 "\/" EqR2

proof end;

theorem :: MSUALG_5:9

for I being non empty set
for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqR "\/" EqR = EqR

proof end;

theorem Th10: :: MSUALG_5:10

for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR3 being Equivalence_Relation of M holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)

proof end;

theorem Th11: :: MSUALG_5:11

for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1

proof end;

theorem Th12: :: MSUALG_5:12

for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, EqR being Equivalence_Relation of M st EqR = EqR1 /\ EqR2 holds
EqR1 "\/" EqR = EqR1

proof end;

theorem Th13: :: MSUALG_5:13

for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M

proof end;

definition

let I be non empty set ;
let M be ManySortedSet of I;
func EqRelLatt M -> strict Lattice means :Def5: :: MSUALG_5:def 5
( ( for x being set holds
( x in the carrier of it iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of it . x,y = x /\ y & the L_join of it . x,y = x "\/" y ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines EqRelLatt MSUALG_5:def 5 :

registration

let S be non empty ManySortedSign ;
let A be MSAlgebra of S;
cluster MSEquivalence-like -> MSEquivalence_Relation-like ManySortedRelation of the Sorts of A,the Sorts of A;
coherence by MSUALG_4:def 5;

end;

theorem Th14: :: MSUALG_5:14

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for x1, y1 being set
for a1, b1 being FinSequence st [x1,y1] in (C1 . ((the_arity_of o) /. ((len a1) + 1))) \/ (C2 . ((the_arity_of o) /. ((len a1) + 1))) holds
for x, y being Element of Args o,A st x = (a1 ^ <*x1*>) ^ b1 & y = (a1 ^ <*y1*>) ^ b1 holds
[((Den o,A) . x),((Den o,A) . y)] in (C1 . (the_result_sort_of o)) \/ (C2 . (the_result_sort_of o))

proof end;

theorem Th15: :: MSUALG_5:15

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x1, y1 being set
for n being Nat
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Nat st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den o,A) . ((a1 ^ <*x1*>) ^ b1)),((Den o,A) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args o,A st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den o,A) . x),((Den o,A) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)

proof end;

theorem Th16: :: MSUALG_5:16

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args o,A st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den o,A) . x),((Den o,A) . y)] in C . (the_result_sort_of o)

proof end;

theorem Th17: :: MSUALG_5:17

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for C1, C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A

proof end;

theorem Th18: :: MSUALG_5:18

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for C1, C2 being MSCongruence of A holds C1 /\ C2 is MSCongruence of A

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
func CongrLatt A -> strict SubLattice of EqRelLatt the Sorts of A means :Def6: :: MSUALG_5:def 6
for x being set holds
( x in the carrier of it iff x is MSCongruence of A );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines CongrLatt MSUALG_5:def 6 :

theorem Th19: :: MSUALG_5:19

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S holds id the Sorts of A is MSCongruence of A

proof end;

theorem Th20: :: MSUALG_5:20

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S holds [|the Sorts of A,the Sorts of A|] is MSCongruence of A

proof end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
cluster CongrLatt A -> strict bounded ;
coherence

proof end;

end;

theorem :: MSUALG_5:21

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S holds Bottom (CongrLatt A) = id the Sorts of A

proof end;

theorem :: MSUALG_5:22

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S holds Top (CongrLatt A) = [|the Sorts of A,the Sorts of A|]

proof end;