:: MSUALG_8 semantic presentation

theorem Th1: :: MSUALG_8:1

for b₁ being Nat
for b₂ being FinSequence holds
( 1 <= b₁ & b₁ < len b₂ iff ( b₁ in dom b₂ & b₁ + 1 in dom b₂ ) )

proof end;

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

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

provided

E2: for b₁ being Nat st b₁ in Seg F₁() holds
ex b₂ being set st P₁[b₁,b₂]

proof end;

theorem Th2: :: MSUALG_8:2

for b₁ being set
for b₂, b₃ being Element of (EqRelLatt b₁)
for b₄, b₅ being Equivalence_Relation of b₁ st b₂ = b₄ & b₃ = b₅ holds
( b₂ [= b₃ iff b₄ c= b₅ )

proof end;

registration

let c₁ be set ;
cluster EqRelLatt a₁ -> bounded ;
coherence

proof end;

end;

theorem Th3: :: MSUALG_8:3

for b₁ being set holds Bottom (EqRelLatt b₁) = id b₁

proof end;

theorem Th4: :: MSUALG_8:4

for b₁ being set holds Top (EqRelLatt b₁) = nabla b₁

proof end;

theorem Th5: :: MSUALG_8:5

for b₁ being set holds EqRelLatt b₁ is complete

proof end;

registration

let c₁ be set ;
cluster EqRelLatt a₁ -> bounded complete ;
coherence by Th5;

end;

theorem Th6: :: MSUALG_8:6

for b₁ being set
for b₂ being Subset of (EqRelLatt b₁) holds union b₂ is Relation of b₁

proof end;

theorem Th7: :: MSUALG_8:7

for b₁ being set
for b₂ being Subset of (EqRelLatt b₁) holds union b₂ c= "\/" b₂

proof end;

theorem Th8: :: MSUALG_8:8

for b₁ being set
for b₂ being Subset of (EqRelLatt b₁)
for b₃ being Relation of b₁ st b₃ = union b₂ holds
"\/" b₂ = EqCl b₃

proof end;

theorem Th9: :: MSUALG_8:9

for b₁ being set
for b₂ being Subset of (EqRelLatt b₁)
for b₃ being Relation st b₃ = union b₂ holds
b₃ = b₃ ~

proof end;

theorem Th10: :: MSUALG_8:10

for b₁, b₂, b₃ being set
for b₄ being Subset of (EqRelLatt b₃) st b₁ in b₃ & b₂ in b₃ holds
( [b₁,b₂] in "\/" b₄ iff ex b₅ being FinSequence st
( 1 <= len b₅ & b₁ = b₅ . 1 & b₂ = b₅ . (len b₅) & ( for b₆ being Nat st 1 <= b₆ & b₆ < len b₅ holds
[(b₅ . b₆),(b₅ . (b₆ + 1))] in union b₄ ) ) )

proof end;

theorem Th11: :: MSUALG_8:11

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Subset of (CongrLatt b₂) holds "/\" b₃,(EqRelLatt the Sorts of b₂) is MSCongruence of b₂

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be Element of (EqRelLatt the Sorts of c₂);
func CongrCl c₃ -> MSCongruence of a₂ equals :: MSUALG_8:def 1
"/\" { b₁ where B is Element of (EqRelLatt the Sorts of a₂) : ( b₁ is MSCongruence of a₂ & a₃ [= b₁ ) } ,(EqRelLatt the Sorts of a₂);
coherence

proof end;

end;

:: deftheorem Def1 defines CongrCl MSUALG_8:def 1 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be Subset of (EqRelLatt the Sorts of c₂);
func CongrCl c₃ -> MSCongruence of a₂ equals :: MSUALG_8:def 2
"/\" { b₁ where B is Element of (EqRelLatt the Sorts of a₂) : ( b₁ is MSCongruence of a₂ & a₃ is_less_than b₁ ) } ,(EqRelLatt the Sorts of a₂);
coherence

proof end;

end;

:: deftheorem Def2 defines CongrCl MSUALG_8:def 2 :

theorem Th12: :: MSUALG_8:12

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Element of (EqRelLatt the Sorts of b₂) st b₃ is MSCongruence of b₂ holds
CongrCl b₃ = b₃

proof end;

theorem Th13: :: MSUALG_8:13

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Subset of (EqRelLatt the Sorts of b₂) holds CongrCl ("\/" b₃,(EqRelLatt the Sorts of b₂)) = CongrCl b₃

proof end;

theorem Th14: :: MSUALG_8:14

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being Subset of (CongrLatt b₂)
for b₅, b₆ being MSCongruence of b₂ st b₅ = "\/" b₃,(EqRelLatt the Sorts of b₂) & b₆ = "\/" b₄,(EqRelLatt the Sorts of b₂) holds
b₅ "\/" b₆ = "\/" (b₃ \/ b₄),(EqRelLatt the Sorts of b₂)

proof end;

theorem Th15: :: MSUALG_8:15

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Subset of (CongrLatt b₂) holds "\/" b₃,(EqRelLatt the Sorts of b₂) = "\/" { ("\/" b₄,(EqRelLatt the Sorts of b₂)) where B is Subset of (EqRelLatt the Sorts of b₂) : b₄ is finite Subset of b₃ } ,(EqRelLatt the Sorts of b₂)

proof end;

theorem Th16: :: MSUALG_8:16

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃ being Element of b₁
for b₄ being Equivalence_Relation of b₂ . b₃ ex b₅ being Equivalence_Relation of b₂ st
( b₅ . b₃ = b₄ & ( for b₆ being Element of b₁ st b₆ <> b₃ holds
b₅ . b₆ = nabla (b₂ . b₆) ) )

proof end;

notation

let c₁ be non empty set ;
let c₂ be ManySortedSet of c₁;
let c₃ be Element of c₁;
let c₄ be Subset of (EqRelLatt c₂);
synonym EqRelSet c₄,c₃ for pi c₂,c₁;

end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedSet of c₁;
let c₃ be Element of c₁;
let c₄ be Subset of (EqRelLatt c₂);
redefine func EqRelSet as EqRelSet c₄,c₃ -> Subset of (EqRelLatt (a₂ . a₃)) means :Def3: :: MSUALG_8:def 3
for b₁ being set holds
( b₁ in a₅ iff ex b₂ being Equivalence_Relation of a₂ st
( b₁ = b₂ . a₃ & b₂ in a₄ ) );
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def3 defines EqRelSet MSUALG_8:def 3 :

theorem Th17: :: MSUALG_8:17

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Element of b₁
for b₄ being Subset of (EqRelLatt the Sorts of b₂)
for b₅ being Equivalence_Relation of the Sorts of b₂ st b₅ = "\/" b₄ holds
b₅ . b₃ = "\/" (EqRelSet b₄,b₃),(EqRelLatt (the Sorts of b₂ . b₃))

proof end;

theorem Th18: :: MSUALG_8:18

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being Subset of (CongrLatt b₂) holds "\/" b₃,(EqRelLatt the Sorts of b₂) is MSCongruence of b₂

proof end;

theorem Th19: :: MSUALG_8:19

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds CongrLatt b₂ is /\-inheriting

proof end;

theorem Th20: :: MSUALG_8:20

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds CongrLatt b₂ is \/-inheriting

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster CongrLatt a₂ -> /\-inheriting \/-inheriting ;
coherence by Th19, Th20;

end;