:: MSUALG_8 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_8:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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{ F1() -> Nat, P1[ set , set ] } :
ex p being FinSequence st
( dom p = Seg F1() & ( for k being Nat st k in Seg F1() holds
P1[k,p . k] ) )
provided
A1: for k being Nat st k in Seg F1() holds
ex x being set st P1[k,x]
proof end;

theorem Th2: :: MSUALG_8:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
EqRelLatt Y is bounded
proof end;
end;

theorem :: MSUALG_8:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set holds Bottom (EqRelLatt Y) = id Y
proof end;

theorem :: MSUALG_8:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set holds Top (EqRelLatt Y) = nabla Y
proof end;

theorem Th5: :: MSUALG_8:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set holds EqRelLatt Y is complete
proof end;

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

theorem Th6: :: MSUALG_8:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for X being Subset of (EqRelLatt Y) holds union X c= "\/" X
proof end;

theorem Th8: :: MSUALG_8:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  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 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
"/\" { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A) is MSCongruence of A
proof end;
end;

:: deftheorem defines CongrCl MSUALG_8:def 1 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for E being Element of (EqRelLatt the Sorts of A) holds CongrCl E = "/\" { x where x is Element of (EqRelLatt the Sorts of A) : ( x is MSCongruence of A & E [= x ) } ,(EqRelLatt the Sorts of A);

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
"/\" { 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) is MSCongruence of A
proof end;
end;

:: deftheorem defines CongrCl MSUALG_8:def 2 :
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 = "/\" { 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);

theorem :: MSUALG_8:12  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 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  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 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  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 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  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 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  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 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
EqRelSet , is Subset of (EqRelLatt (M . i))
proof end;
compatibility
for b1 being Subset of (EqRelLatt (M . i)) holds
( b1 = EqRelSet , iff for x being set holds
( x in b1 iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) )
proof end;
end;

:: deftheorem Def3 defines EqRelSet MSUALG_8:def 3 :
for I being non empty set
for M being ManySortedSet of I
for i being Element of I
for X being Subset of (EqRelLatt M)
for b5 being Subset of (EqRelLatt (M . i)) holds
( b5 = EqRelSet X,i iff for x being set holds
( x in b5 iff ex Eq being Equivalence_Relation of M st
( x = Eq . i & Eq in X ) ) );

theorem Th17: :: MSUALG_8: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 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  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 X being Subset of (CongrLatt A) holds "\/" X,(EqRelLatt the Sorts of A) is MSCongruence of A
proof end;

theorem Th19: :: MSUALG_8: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 CongrLatt A is /\-inheriting
proof end;

theorem Th20: :: MSUALG_8: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 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
( CongrLatt A is /\-inheriting & CongrLatt A is \/-inheriting )
by Th19, Th20;
end;