:: MSUALG_5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: MSUALG_5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Equivalence_Relation of X st
( R c= b1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b1 c= EqR2 ) )
by EQREL_1:20;
uniqueness
for b1, b2 being Equivalence_Relation of X st R c= b1 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b1 c= EqR2 ) & R c= b2 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b2 c= EqR2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines EqCl MSUALG_5:def 1 :
for X being set
for R being Relation of X
for b3 being Equivalence_Relation of X holds
( b3 = EqCl R iff ( R c= b3 & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
b3 c= EqR2 ) ) );

theorem Th2: :: MSUALG_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for EqR1 being Equivalence_Relation of X holds EqCl EqR1 = EqR1
proof end;

theorem Th4: :: MSUALG_5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being strict Lattice st
( the carrier of b1 = { 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 b1 . x,y = x /\ y & the L_join of b1 . x,y = x "\/" y ) ) )
proof end;
uniqueness
for b1, b2 being strict Lattice st the carrier of b1 = { 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 b1 . x,y = x /\ y & the L_join of b1 . x,y = x "\/" y ) ) & the carrier of b2 = { 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 b2 . x,y = x /\ y & the L_join of b2 . x,y = x "\/" y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines EqRelLatt MSUALG_5:def 2 :
for X being set
for b2 being strict Lattice holds
( b2 = EqRelLatt X iff ( the carrier of b2 = { 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 b2 . x,y = x /\ y & the L_join of b2 . x,y = x "\/" y ) ) ) );

registration
let I be set ;
let M be ManySortedSet of I;
cluster MSEquivalence_Relation-like ManySortedRelation of M,M;
existence
ex b1 being ManySortedRelation of M st b1 is MSEquivalence_Relation-like
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
ex b1 being Equivalence_Relation of M st
for i being Element of I holds b1 . i = EqCl (R . i)
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of M st ( for i being Element of I holds b1 . i = EqCl (R . i) ) & ( for i being Element of I holds b2 . i = EqCl (R . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines EqCl MSUALG_5:def 3 :
for I being non empty set
for M being ManySortedSet of I
for R being ManySortedRelation of M
for b4 being Equivalence_Relation of M holds
( b4 = EqCl R iff for i being Element of I holds b4 . i = EqCl (R . i) );

theorem :: MSUALG_5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Equivalence_Relation of M ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 )
proof end;
uniqueness
for b1, b2 being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 ) & ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b2 = EqCl EqR3 ) holds
b1 = b2
;
commutativity
for b1, EqR1, EqR2 being Equivalence_Relation of M st ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b1 = EqCl EqR3 ) holds
ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR2 \/ EqR1 & b1 = EqCl EqR3 )
;
end;

:: deftheorem Def4 defines "\/" MSUALG_5:def 4 :
for I being non empty set
for M being ManySortedSet of I
for EqR1, EqR2, b5 being Equivalence_Relation of M holds
( b5 = EqR1 "\/" EqR2 iff ex EqR3 being ManySortedRelation of M st
( EqR3 = EqR1 \/ EqR2 & b5 = EqCl EqR3 ) );

theorem Th6: :: MSUALG_5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being strict Lattice st
( ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . x,y = x /\ y & the L_join of b1 . x,y = x "\/" y ) ) )
proof end;
uniqueness
for b1, b2 being strict Lattice st ( for x being set holds
( x in the carrier of b1 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b1 . x,y = x /\ y & the L_join of b1 . x,y = x "\/" y ) ) & ( for x being set holds
( x in the carrier of b2 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b2 . x,y = x /\ y & the L_join of b2 . x,y = x "\/" y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines EqRelLatt MSUALG_5:def 5 :
for I being non empty set
for M being ManySortedSet of I
for b3 being strict Lattice holds
( b3 = EqRelLatt M iff ( ( for x being set holds
( x in the carrier of b3 iff x is Equivalence_Relation of M ) ) & ( for x, y being Equivalence_Relation of M holds
( the L_meet of b3 . x,y = x /\ y & the L_join of b3 . x,y = x "\/" y ) ) ) );

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
for b1 being ManySortedRelation of A st b1 is MSEquivalence-like holds
b1 is MSEquivalence_Relation-like
by MSUALG_4:def 5;
end;

theorem Th14: :: MSUALG_5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being strict SubLattice of EqRelLatt the Sorts of A st
for x being set holds
( x in the carrier of b1 iff x is MSCongruence of A )
proof end;
uniqueness
for b1, b2 being strict SubLattice of EqRelLatt the Sorts of A st ( for x being set holds
( x in the carrier of b1 iff x is MSCongruence of A ) ) & ( for x being set holds
( x in the carrier of b2 iff x is MSCongruence of A ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines CongrLatt MSUALG_5:def 6 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for b3 being strict SubLattice of EqRelLatt the Sorts of A holds
( b3 = CongrLatt A iff for x being set holds
( x in the carrier of b3 iff x is MSCongruence of A ) );

theorem Th19: :: MSUALG_5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
CongrLatt A is bounded
proof end;
end;

theorem :: MSUALG_5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;