:: MSUALG_5 semantic presentation

theorem Th1: :: MSUALG_5:1

for b₁ being set
for b₂, b₃, b₄ being Equivalence_Relation of b₁ holds (b₂ "\/" b₃) "\/" b₄ = b₂ "\/" (b₃ "\/" b₄)

proof end;

definition

let c₁ be set ;
let c₂ be Relation of c₁;
func EqCl c₂ -> Equivalence_Relation of a₁ means :Def1: :: MSUALG_5:def 1
( a₂ c= a₃ & ( for b₁ being Equivalence_Relation of a₁ st a₂ c= b₁ holds
a₃ c= b₁ ) );
existence by EQREL_1:20;
uniqueness

proof end;

end;

:: deftheorem Def1 defines EqCl MSUALG_5:def 1 :

theorem Th2: :: MSUALG_5:2

for b₁ being set
for b₂, b₃ being Equivalence_Relation of b₁ holds b₂ "\/" b₃ = EqCl (b₂ \/ b₃)

proof end;

theorem Th3: :: MSUALG_5:3

for b₁ being set
for b₂ being Equivalence_Relation of b₁ holds EqCl b₂ = b₂

proof end;

theorem Th4: :: MSUALG_5:4

for b₁ being set
for b₂ being Relation of b₁ holds (nabla b₁) \/ b₂ = nabla b₁

proof end;

definition

let c₁ be set ;
func EqRelLatt c₁ -> strict Lattice means :: MSUALG_5:def 2
( the carrier of a₂ = { b₁ where B is Relation of a₁,a₁ : b₁ is Equivalence_Relation of a₁ } & ( for b₁, b₂ being Equivalence_Relation of a₁ holds
( the L_meet of a₂ . b₁,b₂ = b₁ /\ b₂ & the L_join of a₂ . b₁,b₂ = b₁ "\/" b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines EqRelLatt MSUALG_5:def 2 :

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster MSEquivalence_Relation-like ManySortedRelation of a₂,a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
mode Equivalence_Relation of a₂ is MSEquivalence_Relation-like ManySortedRelation of a₂;

end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedSet of c₁;
let c₃ be ManySortedRelation of c₂;
func EqCl c₃ -> Equivalence_Relation of a₂ means :Def3: :: MSUALG_5:def 3
for b₁ being Element of a₁ holds a₄ . b₁ = EqCl (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines EqCl MSUALG_5:def 3 :

theorem Th5: :: MSUALG_5:5

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃ being Equivalence_Relation of b₂ holds EqCl b₃ = b₃

proof end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedSet of c₁;
let c₃, c₄ be Equivalence_Relation of c₂;
func c₃ "\/" c₄ -> Equivalence_Relation of a₂ means :Def4: :: MSUALG_5:def 4
ex b₁ being ManySortedRelation of a₂ st
( b₁ = a₃ \/ a₄ & a₅ = EqCl b₁ );
existence

proof end;

uniqueness ;
commutativity ;

end;

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

theorem Th6: :: MSUALG_5:6

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being Equivalence_Relation of b₂ holds b₃ \/ b₄ c= b₃ "\/" b₄

proof end;

theorem Th7: :: MSUALG_5:7

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃, b₄, b₅ being Equivalence_Relation of b₂ st b₃ \/ b₄ c= b₅ holds
b₃ "\/" b₄ c= b₅

proof end;

theorem Th8: :: MSUALG_5:8

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃, b₄, b₅ being Equivalence_Relation of b₂ st b₃ \/ b₄ c= b₅ & ( for b₆ being Equivalence_Relation of b₂ st b₃ \/ b₄ c= b₆ holds
b₅ c= b₆ ) holds
b₅ = b₃ "\/" b₄

proof end;

theorem Th9: :: MSUALG_5:9

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃ being Equivalence_Relation of b₂ holds b₃ "\/" b₃ = b₃

proof end;

theorem Th10: :: MSUALG_5:10

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃, b₄, b₅ being Equivalence_Relation of b₂ holds (b₃ "\/" b₄) "\/" b₅ = b₃ "\/" (b₄ "\/" b₅)

proof end;

theorem Th11: :: MSUALG_5:11

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being Equivalence_Relation of b₂ holds b₃ /\ (b₃ "\/" b₄) = b₃

proof end;

theorem Th12: :: MSUALG_5:12

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃, b₄, b₅ being Equivalence_Relation of b₂ st b₅ = b₃ /\ b₄ holds
b₃ "\/" b₅ = b₃

proof end;

theorem Th13: :: MSUALG_5:13

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being Equivalence_Relation of b₂ holds b₃ /\ b₄ is Equivalence_Relation of b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedSet of c₁;
func EqRelLatt c₂ -> strict Lattice means :Def5: :: MSUALG_5:def 5
( ( for b₁ being set holds
( b₁ in the carrier of a₃ iff b₁ is Equivalence_Relation of a₂ ) ) & ( for b₁, b₂ being Equivalence_Relation of a₂ holds
( the L_meet of a₃ . b₁,b₂ = b₁ /\ b₂ & the L_join of a₃ . b₁,b₂ = b₁ "\/" b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines EqRelLatt MSUALG_5:def 5 :

registration

let c₁ be non empty ManySortedSign ;
let c₂ be MSAlgebra of c₁;
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 b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄, b₅ being MSCongruence of b₂
for b₆, b₇ being set
for b₈, b₉ being FinSequence st [b₆,b₇] in (b₄ . ((the_arity_of b₃) /. ((len b₈) + 1))) \/ (b₅ . ((the_arity_of b₃) /. ((len b₈) + 1))) holds
for b₁₀, b₁₁ being Element of Args b₃,b₂ st b₁₀ = (b₈ ^ <*b₆*>) ^ b₉ & b₁₁ = (b₈ ^ <*b₇*>) ^ b₉ holds
[((Den b₃,b₂) . b₁₀),((Den b₃,b₂) . b₁₁)] in (b₄ . (the_result_sort_of b₃)) \/ (b₅ . (the_result_sort_of b₃))

proof end;

theorem Th15: :: MSUALG_5:15

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄, b₅ being MSCongruence of b₂
for b₆ being MSEquivalence-like ManySortedRelation of b₂ st b₆ = b₄ "\/" b₅ holds
for b₇, b₈ being set
for b₉ being Nat
for b₁₀, b₁₁, b₁₂ being FinSequence st len b₁₀ = b₉ & len b₁₀ = len b₁₁ & ( for b₁₃ being Nat st b₁₃ in dom b₁₀ holds
[(b₁₀ . b₁₃),(b₁₁ . b₁₃)] in b₆ . ((the_arity_of b₃) /. b₁₃) ) & [((Den b₃,b₂) . ((b₁₀ ^ <*b₇*>) ^ b₁₂)),((Den b₃,b₂) . ((b₁₁ ^ <*b₇*>) ^ b₁₂))] in b₆ . (the_result_sort_of b₃) & [b₇,b₈] in b₆ . ((the_arity_of b₃) /. (b₉ + 1)) holds
for b₁₃ being Element of Args b₃,b₂ st b₁₃ = (b₁₀ ^ <*b₇*>) ^ b₁₂ holds
[((Den b₃,b₂) . b₁₃),((Den b₃,b₂) . ((b₁₁ ^ <*b₈*>) ^ b₁₂))] in b₆ . (the_result_sort_of b₃)

proof end;

theorem Th16: :: MSUALG_5:16

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄, b₅ being MSCongruence of b₂
for b₆ being MSEquivalence-like ManySortedRelation of b₂ st b₆ = b₄ "\/" b₅ holds
for b₇, b₈ being Element of Args b₃,b₂ st ( for b₉ being Nat st b₉ in dom b₇ holds
[(b₇ . b₉),(b₈ . b₉)] in b₆ . ((the_arity_of b₃) /. b₉) ) holds
[((Den b₃,b₂) . b₇),((Den b₃,b₂) . b₈)] in b₆ . (the_result_sort_of b₃)

proof end;

theorem Th17: :: MSUALG_5:17

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being MSCongruence of b₂ holds b₃ "\/" b₄ is MSCongruence of b₂

proof end;

theorem Th18: :: MSUALG_5:18

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being MSCongruence of b₂ holds b₃ /\ b₄ is MSCongruence of b₂

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func CongrLatt c₂ -> strict SubLattice of EqRelLatt the Sorts of a₂ means :Def6: :: MSUALG_5:def 6
for b₁ being set holds
( b₁ in the carrier of a₃ iff b₁ 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 b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds id the Sorts of b₂ is MSCongruence of b₂

proof end;

theorem Th20: :: MSUALG_5:20

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds [|the Sorts of b₂,the Sorts of b₂|] is MSCongruence of b₂

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster CongrLatt a₂ -> strict bounded ;
coherence

proof end;

end;

theorem Th21: :: MSUALG_5:21

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds Bottom (CongrLatt b₂) = id the Sorts of b₂

proof end;

theorem Th22: :: MSUALG_5:22

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

proof end;