:: Lattice of Congruences in a Many Sorted Algebra
:: by Robert Milewski
::
:: Received January 11, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PBOOLE, RELAT_1, EQREL_1, TARSKI, XBOOLE_0, STRUCT_0,
LATTICES, FUNCT_1, SUBSET_1, BINOP_1, MSUALG_4, ZFMISC_1, CARD_3,
MSUALG_1, FINSEQ_1, MARGREL1, PARTFUN1, ARYTM_3, ORDINAL4, NAT_1,
XXREAL_0, CARD_1, RELAT_2, ARYTM_1, NAT_LAT, REALSET1, XXREAL_2,
MSUALG_5, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
REALSET1, ORDINAL1, NUMBERS, XCMPLX_0, FINSEQ_2, STRUCT_0, PARTFUN1,
FUNCT_2, RELSET_1, EQREL_1, BINOP_1, PBOOLE, MSUALG_1, MSUALG_3,
MSUALG_4, LATTICES, NAT_LAT, CARD_3, FINSEQ_1, NAT_1, XXREAL_0;
constructors BINOP_1, XXREAL_0, NAT_1, NAT_D, EQREL_1, REALSET1, NAT_LAT,
MSUALG_3, MSUALG_4, RELSET_1, PRALG_2, FUNCOP_1, FINSEQ_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, XREAL_0, NAT_1, FINSEQ_1,
EQREL_1, PBOOLE, STRUCT_0, LATTICES, NAT_LAT, PRALG_1, MSUALG_1,
MSUALG_3, MSUALG_4, ORDINAL1, CARD_1, RELAT_2;
requirements NUMERALS, REAL, BOOLE, SUBSET;
equalities BINOP_1, REALSET1, EQREL_1;
theorems BINOP_1, PBOOLE, MSUALG_4, EQREL_1, TARSKI, NAT_LAT, LATTICES,
RELAT_1, RELAT_2, FUNCT_2, CARD_3, ZFMISC_1, MSUALG_1, FUNCT_1, MSUALG_3,
FINSEQ_1, NAT_1, MSAFREE2, XBOOLE_0, XBOOLE_1, FINSEQ_3, XCMPLX_1,
ORDERS_1, XREAL_1, XXREAL_0, PARTFUN1, FINSEQ_2;
schemes PBOOLE, BINOP_1, NAT_1, FINSEQ_1, XBOOLE_0;
begin
:: MORE OF EQUIVALENCE RELATIONS
reserve I,X,x,d,i for set;
reserve M for ManySortedSet of I;
reserve EqR1,EqR2 for Equivalence_Relation of X;
definition
let X be set, R be Relation of X;
func EqCl R -> Equivalence_Relation of X means
:Def1:
R c= it & for EqR2 be
Equivalence_Relation of X st R c= EqR2 holds it c= EqR2;
existence by EQREL_1:12;
uniqueness
proof
let C1,C2 be Equivalence_Relation of X such that
A1: R c= C1 and
A2: for EqR2 be Equivalence_Relation of X st R c= EqR2 holds C1 c= EqR2 and
A3: R c= C2 and
A4: for EqR2 be Equivalence_Relation of X st R c= EqR2 holds C2 c= EqR2;
A5: C2 c= C1 by A1,A4;
C1 c= C2 by A2,A3;
hence C1 = C2 by A5,XBOOLE_0:def 10;
end;
end;
theorem Th1:
EqR1 "\/" EqR2 = EqCl (EqR1 \/ EqR2)
proof
A1: for EqR3 be Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR3 holds EqR1
"\/" EqR2 c= EqR3 by EQREL_1:def 2;
EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by EQREL_1:def 2;
hence thesis by A1,Def1;
end;
theorem Th2:
EqCl EqR1 = EqR1
proof
for EqR2 be Equivalence_Relation of X st EqR1 c= EqR2 holds EqR1 c= EqR2;
hence thesis by Def1;
end;
begin
:: LATTICE OF EQUIVALENCE RELATIONS ::
definition
let X be set;
func EqRelLatt X -> strict Lattice means
:Def2: 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
set B = {x where x is Relation of X,X : x is Equivalence_Relation of X};
id X in B;
then reconsider B as non empty set;
defpred Z[Element of B,Element of B,Element of B] means ( $1 \/ $2 c= $3 &
for x9 be Element of B st $1 \/ $2 c= x9 holds $3 c= x9 );
A1: for x,y being Element of B ex z being Element of B st Z[x,y,z]
proof
let x,y be Element of B;
y in B;
then
A2: ex y99 be Relation of X,X st y = y99 & y99 is Equivalence_Relation of X;
x in B;
then ex x99 be Relation of X,X st x = x99 & x99 is Equivalence_Relation
of X;
then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A2;
consider z being Equivalence_Relation of X such that
A3: x1 \/ y1 c= z and
A4: for x9 be Equivalence_Relation of X st x1 \/ y1 c= x9 holds z c=
x9 by EQREL_1:12;
z in B;
then reconsider z9 = z as Element of B;
take z9;
thus x \/ y c= z9 by A3;
hereby
let x9 be Element of B such that
A5: x \/ y c= x9;
x9 in B;
then ex x99 be Relation of X,X st x9 = x99 & x99 is
Equivalence_Relation of X;
then reconsider x19 = x9 as Equivalence_Relation of X;
x \/ y c= x19 by A5;
hence z9 c= x9 by A4;
end;
end;
consider B1 being BinOp of B such that
A6: for x,y being Element of B holds Z[x,y,B1.(x,y)] from BINOP_1:sch
3(A1);
defpred Z[Element of B,Element of B,Element of B] means $3 = $1 /\ $2;
A7: for x,y being Element of B ex z being Element of B st Z[x,y,z]
proof
let x,y be Element of B;
y in B;
then
A8: ex y1 being Relation of X,X st y = y1 & y1 is Equivalence_Relation of X;
x in B;
then ex x1 being Relation of X,X st x = x1 & x1 is Equivalence_Relation
of X;
then reconsider x9 = x, y9 = y as Equivalence_Relation of X by A8;
set z = x9 /\ y9;
z in B;
then reconsider z as Element of B;
take z;
thus thesis;
end;
consider B2 be BinOp of B such that
A9: for x,y being Element of B holds Z[x,y,B2.(x,y)] from BINOP_1:sch
3(A7);
reconsider L = LattStr (# B,B1,B2 #) as non empty LattStr;
A10: now
let x,y be Equivalence_Relation of X;
A11: y in B;
x in B;
then reconsider x1 = x, y1 = y as Element of B by A11;
reconsider B19 = B1.(x1,y1) as Element of B;
B19 in B;
then ex B199 be Relation of X,X st B19 = B199 & B199 is
Equivalence_Relation of X;
then reconsider B19 as Equivalence_Relation of X;
A12: for x9 be Element of B st x1 \/ y1 c= x9 holds B1.(x1,y1) c= x9 by A6;
A13: now
let x9 be Equivalence_Relation of X such that
A14: x \/ y c= x9;
x9 in B;
then reconsider x19 = x9 as Element of B;
x \/ y c= x19 by A14;
hence B1.(x,y) c= x9 by A12;
end;
x1 \/ y1 c= B1.(x1,y1) by A6;
then B19 = x "\/" y by A13,EQREL_1:def 2;
hence B1.(x,y) = x "\/" y;
end;
A15: now
let a,b,c be Element of B;
b in B;
then
A16: ex x2 be Relation of X,X st b = x2 & x2 is Equivalence_Relation of X;
c in B;
then
A17: ex x3 be Relation of X,X st c = x3 & x3 is Equivalence_Relation of X;
a in B;
then ex x1 be Relation of X,X st a = x1 & x1 is Equivalence_Relation of
X;
then reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by
A16,A17;
thus B1.(a,B1.(b,c)) = B1.(a,U2 "\/" U3) by A10
.= U1 "\/" (U2 "\/" U3) by A10
.= (U1 "\/" U2) "\/" U3 by EQREL_1:13
.= B1.(U1 "\/" U2,c) by A10
.= B1.(B1.(a,b),c) by A10;
end;
A18: for a,b,c being Element of L holds a"\/"(b"\/"c) = (a"\/"b)"\/"c
proof
let a,b,c be Element of L;
reconsider x=a,y=b,z=c as Element of B;
A19: (the L_join of L).(a,b) = a"\/"b by LATTICES:def 1;
thus a"\/"(b"\/"c) = (the L_join of L).(a,(b"\/"c)) by LATTICES:def 1
.=B1.(x,B1.(y,z)) by LATTICES:def 1
.= (the L_join of L).((the L_join of L).(a,b),c) by A15
.=(a"\/"b)"\/"c by A19,LATTICES:def 1;
end;
A20: now
let a,b be Element of B;
b in B;
then
A21: ex x2 be Relation of X,X st b = x2 & x2 is Equivalence_Relation of X;
a in B;
then ex x1 be Relation of X,X st a = x1 & x1 is Equivalence_Relation of
X;
then reconsider U1 = a, U2 = b as Equivalence_Relation of X by A21;
thus B1.(a,b) = U2 "\/" U1 by A10
.= B1.(b,a) by A10;
end;
A22: for a,b being Element of L holds a"\/"b = b"\/"a
proof
let a,b be Element of L;
reconsider x=a,y=b as Element of B;
thus a"\/"b = B1.(x,y) by LATTICES:def 1
.= (the L_join of L).(b,a) by A20
.=b"\/"a by LATTICES:def 1;
end;
A23: now
let x,y be Equivalence_Relation of X;
A24: y in B;
x in B;
then reconsider x9 = x, y9 = y as Element of B by A24;
B2.(x9,y9) = x9 /\ y9 by A9;
hence B2.(x,y) = x /\ y;
end;
A25: now
let a,b,c be Element of B;
b in B;
then
A26: ex x2 be Relation of X,X st b = x2 & x2 is Equivalence_Relation of X;
c in B;
then
A27: ex x3 be Relation of X,X st c = x3 & x3 is Equivalence_Relation of X;
a in B;
then ex x1 be Relation of X,X st a = x1 & x1 is Equivalence_Relation of
X;
then reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of X by
A26,A27;
thus B2.(a,B2.(b,c)) = B2.(a,U2 /\ U3) by A23
.= U1 /\ (U2 /\ U3) by A23
.= (U1 /\ U2) /\ U3 by XBOOLE_1:16
.= B2.(U1 /\ U2,c) by A23
.= B2.(B2.(a,b),c) by A23;
end;
A28: for a,b,c being Element of L holds a"/\"(b"/\"c) = (a"/\"b)"/\"c
proof
let a,b,c be Element of L;
reconsider x=a,y=b,z=c as Element of B;
A29: (the L_meet of L).(a,b) = a"/\"b by LATTICES:def 2;
thus a"/\"(b"/\"c) = (the L_meet of L).(a,(b"/\"c)) by LATTICES:def 2
.=B2.(x,B2.(y,z)) by LATTICES:def 2
.= (the L_meet of L).((the L_meet of L).(a,b),c) by A25
.=(a"/\"b)"/\"c by A29,LATTICES:def 2;
end;
A30: for a,b being Element of L holds a"/\"(a"\/"b)=a
proof
let a,b be Element of L;
reconsider x=a,y=b as Element of B;
A31: B2.(x,B1.(x,y))= x
proof
y in B;
then
A32: ex x2 be Relation of X,X st y = x2 & x2 is Equivalence_Relation of X;
x in B;
then ex x1 be Relation of X,X st x = x1 & x1 is Equivalence_Relation
of X;
then reconsider U1= x,U2=y as Equivalence_Relation of X by A32;
B1.(x,y) = U1 "\/" U2 by A10;
hence B2.(x,B1.(x,y)) = (U1 /\( U1 "\/" U2)) by A23
.= x by EQREL_1:16;
end;
thus a"/\"(a"\/"b) = (the L_meet of L).(a,(a"\/"b)) by LATTICES:def 2
.= a by A31,LATTICES:def 1;
end;
A33: now
let a,b be Element of B;
b in B;
then
A34: ex x2 be Relation of X,X st b = x2 & x2 is Equivalence_Relation of X;
a in B;
then ex x1 be Relation of X,X st a = x1 & x1 is Equivalence_Relation of
X;
then reconsider U1 = a, U2 = b as Equivalence_Relation of X by A34;
thus B2.(a,b) = U2 /\ U1 by A23
.= B2.(b,a) by A23;
end;
A35: for a,b being Element of L holds a"/\"b = b"/\"a
proof
let a,b be Element of L;
reconsider x=a,y=b as Element of B;
thus a"/\"b = B2.(x,y) by LATTICES:def 2
.= (the L_meet of L).(b,a) by A33
.=b"/\"a by LATTICES:def 2;
end;
for a,b being Element of L holds (a"/\"b)"\/"b = b
proof
let a,b be Element of L;
reconsider x=a,y=b as Element of B;
A36: B1.(B2.(x,y),y)= y
proof
y in B;
then
A37: ex x2 be Relation of X,X st y = x2 & x2 is Equivalence_Relation of X;
x in B;
then ex x1 be Relation of X,X st x = x1 & x1 is Equivalence_Relation
of X;
then reconsider U1 = x, U2 = y as Equivalence_Relation of X by A37;
B2.(x,y) = U1 /\ U2 by A23;
hence B1.(B2.(x,y),y) = (U2 "\/" (U1 /\ U2)) by A10
.= y by EQREL_1:17;
end;
thus (a"/\"b)"\/"b = (the L_join of L).((a"/\"b),b) by LATTICES:def 1
.= b by A36,LATTICES:def 2;
end;
then L is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A22,A18,A35,A28,A30,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
then reconsider L as strict Lattice;
take L;
thus the carrier of L = {x where x is Relation of X,X : x is
Equivalence_Relation of X};
thus thesis by A10,A23;
end;
uniqueness
proof
let P1,P2 be strict Lattice such that
A38: the carrier of P1 = {x where x is Relation of X,X : x is
Equivalence_Relation of X} and
A39: for x,y being Equivalence_Relation of X holds (the L_meet of P1).
(x,y) = x /\ y & (the L_join of P1).(x,y) = x "\/" y and
A40: the carrier of P2 = {x where x is Relation of X,X : x is
Equivalence_Relation of X} and
A41: for x,y being Equivalence_Relation of X holds (the L_meet of P2).
(x,y) = x /\ y & (the L_join of P2).(x,y) = x "\/" y;
reconsider Z = the carrier of P1 as non empty set;
now
let x,y be Element of Z;
y in Z;
then
A42: ex x3 be Relation of X,X st y = x3 & x3 is Equivalence_Relation of
X by A38;
x in Z;
then ex x2 be Relation of X,X st x = x2 & x2 is Equivalence_Relation of
X by A38;
then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A42;
thus (the L_meet of P1).(x,y) = x1 /\ y1 by A39
.= (the L_meet of P2).(x,y) by A41;
end;
then
A43: the L_meet of P1 = the L_meet of P2 by A38,A40,BINOP_1:2;
now
let x,y be Element of Z;
y in Z;
then
A44: ex x3 be Relation of X,X st y = x3 & x3 is Equivalence_Relation of
X by A38;
x in Z;
then ex x2 be Relation of X,X st x = x2 & x2 is Equivalence_Relation of
X by A38;
then reconsider x1 = x, y1 = y as Equivalence_Relation of X by A44;
thus (the L_join of P1).(x,y) = x1 "\/" y1 by A39
.= (the L_join of P2).(x,y) by A41;
end;
hence thesis by A38,A40,A43,BINOP_1:2;
end;
end;
begin
:: MANY SORTED EQUIVALENCE RELATIONS ::
registration
let I,M;
cluster MSEquivalence_Relation-like for ManySortedRelation of M;
existence
proof
deffunc F(object)=id (M.$1);
consider f be ManySortedSet of I such that
A1: for d being object st d in I holds f.d = F(d) from PBOOLE:sch 4;
for i be set st i in I holds f.i is Relation of M.i,M.i
proof
let i be set;
assume i in I;
then f.i = id (M.i) by A1;
hence thesis;
end;
then reconsider f as ManySortedRelation of M by MSUALG_4:def 1;
take f;
for i be object, R be Relation of M.i st i in I & f.i = R holds R is
Equivalence_Relation of M.i
proof
let i be object,R be Relation of M.i;
assume that
A2: i in I and
A3: f.i = R;
R = id (M.i) by A1,A2,A3;
hence thesis;
end;
hence thesis by MSUALG_4:def 2;
end;
end;
definition
let I,M;
mode Equivalence_Relation of M is MSEquivalence_Relation-like
ManySortedRelation of M;
end;
reserve I for non empty set;
reserve M for ManySortedSet of I;
reserve EqR,EqR1,EqR2,EqR3,EqR4 for Equivalence_Relation of M;
definition
let I be non empty set;
let M be ManySortedSet of I, R be ManySortedRelation of M;
func EqCl R -> Equivalence_Relation of M means
:Def3:
for i being Element of I holds it.i = EqCl(R.i);
existence
proof
deffunc F(Element of I) = EqCl(R.$1);
consider EqR be ManySortedSet of I such that
A1: for i being Element of I holds EqR.i = F(i) from PBOOLE:sch 5;
for i be set st i in I holds EqR.i is Relation of M.i
proof
let i be set;
assume i in I;
then reconsider i9 = i as Element of I;
EqR.i = EqCl(R.i9) by A1;
hence thesis;
end;
then reconsider EqR as ManySortedRelation of M by MSUALG_4:def 1;
for i be object, R be Relation of M.i st i in I & EqR.i = R holds R is
Equivalence_Relation of M.i
proof
let i be object;
let R1 be Relation of M.i;
assume that
A2: i in I and
A3: EqR.i = R1;
reconsider i9 = i as Element of I by A2;
R1 = EqCl(R.i9) by A1,A3;
hence thesis;
end;
then reconsider EqR as Equivalence_Relation of M by MSUALG_4:def 2;
take EqR;
thus thesis by A1;
end;
uniqueness
proof
let C1,C2 be Equivalence_Relation of M such that
A4: for i being Element of I holds C1.i = EqCl(R.i) and
A5: for i being Element of I holds C2.i = EqCl(R.i);
now
let i be object;
assume i in I;
then reconsider i1 = i as Element of I;
thus C1.i = EqCl(R.i1) by A4
.= C2.i by A5;
end;
hence C1 = C2 by PBOOLE:3;
end;
end;
theorem
EqCl EqR = EqR
proof
now
let i be Element of I;
reconsider ER = EqR.i as Equivalence_Relation of M.i by MSUALG_4:def 2;
thus EqR.i = EqCl ER by Th2
.= EqCl (EqR.i);
end;
hence thesis by Def3;
end;
begin
:: LATTICE OF MANY SORTED EQUIVALENCE RELATIONS ::
definition
let I be non empty set, M be ManySortedSet of I;
let EqR1,EqR2 be Equivalence_Relation of M;
func EqR1 "\/" EqR2 -> Equivalence_Relation of M means
:Def4:
ex EqR3 being
ManySortedRelation of M st EqR3 = EqR1 (\/) EqR2 & it = EqCl EqR3;
existence
proof
deffunc F(object) = (EqR1 (\/) EqR2).$1;
consider E be ManySortedSet of I such that
A1: for i being object st i in I holds E.i = F(i) from PBOOLE:sch 4;
for i be set st i in I holds E.i is Relation of M.i
proof
let i be set;
assume
A2: i in I;
then reconsider i9 = i as Element of I;
E.i = (EqR1 (\/) EqR2).i by A1,A2
.= EqR1.i9 \/ EqR2.i9 by PBOOLE:def 4;
hence thesis;
end;
then reconsider E as ManySortedRelation of M by MSUALG_4:def 1;
take EqCl E;
take E;
thus thesis by A1,PBOOLE:3;
end;
uniqueness;
commutativity;
end;
theorem Th4:
EqR1 (\/) EqR2 c= EqR1 "\/" EqR2
proof
consider EqR3 being ManySortedRelation of M such that
A1: EqR3 = EqR1 (\/) EqR2 and
A2: EqR1 "\/" EqR2 = EqCl EqR3 by Def4;
now
let i be object;
assume i in I;
then reconsider i9 = i as Element of I;
EqR3.i c= EqCl(EqR3.i9) by Def1;
hence EqR3.i c= (EqR1 "\/" EqR2).i by A2,Def3;
end;
hence thesis by A1,PBOOLE:def 2;
end;
theorem Th5:
for EqR be Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds
EqR1 "\/" EqR2 c= EqR
proof
consider EqR3 being ManySortedRelation of M such that
A1: EqR3 = EqR1 (\/) EqR2 and
A2: EqR1 "\/" EqR2 = EqCl EqR3 by Def4;
let EqR be Equivalence_Relation of M such that
A3: EqR1 (\/) EqR2 c= EqR;
now
let i be object;
assume
A4: i in I;
then reconsider i9 = i as Element of I;
EqR.i9 is Relation of M.i;
then reconsider E = EqR.i as Equivalence_Relation of M.i by MSUALG_4:def 2;
EqR3.i c= E by A3,A1,A4,PBOOLE:def 2;
then EqCl(EqR3.i9) c= E by Def1;
hence (EqR1 "\/" EqR2).i c= EqR.i by A2,Def3;
end;
hence thesis by PBOOLE:def 2;
end;
theorem Th6:
( EqR1 (\/) EqR2 c= EqR3 & for EqR be Equivalence_Relation of M st
EqR1 (\/) EqR2 c= EqR holds EqR3 c= EqR ) implies EqR3 = EqR1 "\/" EqR2
proof
assume that
A1: EqR1 (\/) EqR2 c= EqR3 and
A2: for EqR be Equivalence_Relation of M st EqR1 (\/) EqR2 c= EqR holds
EqR3 c= EqR;
A3: EqR1 "\/" EqR2 c= EqR3 by A1,Th5;
EqR3 c= EqR1 "\/" EqR2 by A2,Th4;
hence thesis by A3,PBOOLE:146;
end;
theorem
EqR "\/" EqR = EqR
proof
for EqR3 st EqR (\/) EqR c= EqR3 holds EqR c= EqR3;
hence thesis by Th6;
end;
theorem Th8:
(EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
proof
for EqR4 holds EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) implies (EqR1 "\/"
EqR2) "\/" EqR3 c= EqR4
proof
let EqR4;
A1: EqR2 (\/) EqR3 c= EqR2 "\/" EqR3 by Th4;
assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3);
then
A2: EqR1 (\/) (EqR2 "\/" EqR3) c= EqR4 by Th4;
EqR2 "\/" EqR3 c= EqR1 (\/) (EqR2 "\/" EqR3) by PBOOLE:14;
then EqR2 "\/" EqR3 c= EqR4 by A2,PBOOLE:13;
then
A3: EqR2 (\/) EqR3 c= EqR4 by A1,PBOOLE:13;
EqR2 c= EqR2 (\/) EqR3 by PBOOLE:14;
then
A4: EqR2 c= EqR4 by A3,PBOOLE:13;
EqR1 c= EqR1 (\/) (EqR2 "\/" EqR3) by PBOOLE:14;
then EqR1 c= EqR4 by A2,PBOOLE:13;
then EqR1 (\/) EqR2 c= EqR4 by A4,PBOOLE:16;
then
A5: EqR1 "\/" EqR2 c= EqR4 by Th5;
EqR3 c= EqR2 (\/) EqR3 by PBOOLE:14;
then EqR3 c= EqR4 by A3,PBOOLE:13;
then (EqR1 "\/" EqR2) (\/) EqR3 c= EqR4 by A5,PBOOLE:16;
hence thesis by Th5;
end;
then
A6: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3);
for EqR4 holds EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 implies EqR1 "\/" (EqR2
"\/" EqR3) c= EqR4
proof
let EqR4;
A7: EqR1 (\/) EqR2 c= EqR1 "\/" EqR2 by Th4;
assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3;
then
A8: (EqR1 "\/" EqR2) (\/) EqR3 c= EqR4 by Th4;
EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) (\/) EqR3 by PBOOLE:14;
then EqR1 "\/" EqR2 c= EqR4 by A8,PBOOLE:13;
then
A9: EqR1 (\/) EqR2 c= EqR4 by A7,PBOOLE:13;
EqR3 c= (EqR1 "\/" EqR2) (\/) EqR3 by PBOOLE:14;
then
A10: EqR3 c= EqR4 by A8,PBOOLE:13;
EqR2 c= EqR1 (\/) EqR2 by PBOOLE:14;
then EqR2 c= EqR4 by A9,PBOOLE:13;
then EqR2 (\/) EqR3 c= EqR4 by A10,PBOOLE:16;
then
A11: EqR2 "\/" EqR3 c= EqR4 by Th5;
EqR1 c= EqR1 (\/) EqR2 by PBOOLE:14;
then EqR1 c= EqR4 by A9,PBOOLE:13;
then EqR1 (\/) (EqR2 "\/" EqR3) c= EqR4 by A11,PBOOLE:16;
hence thesis by Th5;
end;
then EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3;
hence thesis by A6,PBOOLE:146;
end;
theorem Th9:
EqR1 (/\) (EqR1 "\/" EqR2) = EqR1
proof
A1: EqR1 (/\) (EqR1 "\/" EqR2) c= EqR1 by PBOOLE:15;
A2: EqR1 c= EqR1 (\/) EqR2 by PBOOLE:14;
EqR1 (\/) EqR2 c= EqR1 "\/" EqR2 by Th4;
then EqR1 c= EqR1 "\/" EqR2 by A2,PBOOLE:13;
then EqR1 c= EqR1 (/\) (EqR1 "\/" EqR2) by PBOOLE:17;
hence thesis by A1,PBOOLE:146;
end;
theorem Th10:
for EqR be Equivalence_Relation of M st EqR = EqR1 (/\) EqR2 holds
EqR1 "\/" EqR = EqR1
proof
A1: EqR1 = EqR1 (\/) (EqR1 (/\) EqR2) by PBOOLE:31;
A2: for EqR4 st EqR1 (\/) (EqR1 (/\) EqR2) c= EqR4 holds EqR1 c= EqR4
by PBOOLE:31;
let EqR be Equivalence_Relation of M;
assume EqR = EqR1 (/\) EqR2;
hence thesis by A1,A2,Th6;
end;
theorem Th11:
for EqR1,EqR2 be Equivalence_Relation of M holds EqR1 (/\) EqR2 is
Equivalence_Relation of M
proof
let EqR1,EqR2 be Equivalence_Relation of M;
for i be set st i in I holds (EqR1 (/\) EqR2).i is Relation of M.i,M.i
proof
let i be set;
assume
A1: i in I;
then reconsider U19 = EqR1.i as Relation of M.i,M.i by MSUALG_4:def 1;
reconsider U29 = EqR2.i as Relation of M.i,M.i by A1,MSUALG_4:def 1;
(EqR1 (/\) EqR2).i = U19 /\ U29 by A1,PBOOLE:def 5;
hence thesis;
end;
then reconsider U3 = EqR1 (/\) EqR2 as ManySortedRelation of M by
MSUALG_4:def 1;
for i be object, R be Relation of M.i st i in I & U3.i = R holds R is
Equivalence_Relation of M.i
proof
let i be object;
let R be Relation of M.i;
assume that
A2: i in I and
A3: U3.i = R;
reconsider U29 = EqR2.i as Relation of M.i by A2,MSUALG_4:def 1;
reconsider U29 as Equivalence_Relation of M.i by A2,MSUALG_4:def 2;
reconsider U19 = EqR1.i as Relation of M.i by A2,MSUALG_4:def 1;
reconsider U19 as Equivalence_Relation of M.i by A2,MSUALG_4:def 2;
U19 /\ U29 is Equivalence_Relation of M.i;
hence thesis by A2,A3,PBOOLE:def 5;
end;
hence thesis by MSUALG_4:def 2;
end;
definition
let I be non empty set;
let M be ManySortedSet of I;
func EqRelLatt M -> strict Lattice means
:Def5:
(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
set f = the Equivalence_Relation of M;
defpred P[object] means $1 is Equivalence_Relation of M;
deffunc F(Element of I)=bool [:M.$1,M.$1:];
consider M2 being ManySortedSet of I such that
A1: for i be Element of I holds M2.i = F(i) from PBOOLE:sch 5;
consider B be set such that
A2: for x being object holds x in B iff x in product M2 & P[x] from
XBOOLE_0:sch 1;
A3: for EqR be Equivalence_Relation of M holds EqR in product M2
proof
let EqR be Equivalence_Relation of M;
A4: for x be object st x in dom M2 holds EqR.x in M2.x
proof
let x be object;
assume x in dom M2;
then reconsider x9 = x as Element of I;
A5: EqR.x9 is Subset of [:M.x9,M.x9:];
M2.x9 = bool [:M.x9,M.x9:] by A1;
hence thesis by A5;
end;
dom EqR = I by PARTFUN1:def 2
.= dom M2 by PARTFUN1:def 2;
hence thesis by A4,CARD_3:9;
end;
then f in product M2;
then reconsider B as non empty set by A2;
defpred Z[Element of B,Element of B,Element of B] means (for x1,y1 be
Equivalence_Relation of M st x1 = $1 & y1 = $2 ex EqR3 being ManySortedRelation
of M st EqR3 = x1 (\/) y1 & $3 = EqCl EqR3);
A6: for x,y being Element of B ex z being Element of B st Z[x,y,z]
proof
let x,y be Element of B;
reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2;
set z = x9 "\/" y9;
z in product M2 by A3;
then reconsider z as Element of B by A2;
take z;
let x1,y1 be Equivalence_Relation of M;
assume that
A7: x1 = x and
A8: y1 = y;
thus thesis by A7,A8,Def4;
end;
consider B1 be BinOp of B such that
A9: for x,y being Element of B holds Z[x,y,B1.(x,y)] from BINOP_1:sch
3(A6 );
defpred Q[Element of B,Element of B,Element of B] means for x1,y1 be
Equivalence_Relation of M st x1 = $1 & y1 = $2 holds $3 = x1 (/\) y1;
A10: for x,y being Element of B ex z being Element of B st Q[x,y,z]
proof
let x,y be Element of B;
reconsider x9 = x, y9 = y as Equivalence_Relation of M by A2;
set z = x9 (/\) y9;
for i be set st i in I holds z.i is Relation of M.i
proof
let i be set;
assume i in I;
then reconsider i9 = i as Element of I;
z.i = x9.i9 /\ y9.i9 by PBOOLE:def 5;
hence thesis;
end;
then reconsider z as ManySortedRelation of M by MSUALG_4:def 1;
for i be object, R be Relation of M.i st i in I & z.i = R holds R is
Equivalence_Relation of M.i
proof
let i be object;
let R be Relation of M.i;
assume that
A11: i in I and
A12: z.i = R;
reconsider i9 = i as Element of I by A11;
reconsider x199 = x9.i9, y199 = y9.i9 as Relation of M.i;
reconsider x99 = x199, y99 = y199 as Equivalence_Relation of M.i by
MSUALG_4:def 2;
R = x99 /\ y99 by A12,PBOOLE:def 5;
hence thesis;
end;
then reconsider z as Equivalence_Relation of M by MSUALG_4:def 2;
z in product M2 by A3;
then reconsider z as Element of B by A2;
take z;
thus thesis;
end;
consider B2 be BinOp of B such that
A13: for x,y being Element of B holds Q[x,y,B2.(x,y)] from BINOP_1:sch
3(A10 );
reconsider L = LattStr (# B,B1,B2 #) as non empty LattStr;
A14: now
let x,y be Equivalence_Relation of M;
A15: y in product M2 by A3;
x in product M2 by A3;
then reconsider x9 = x, y9 = y as Element of B by A2,A15;
ex EqR3 being ManySortedRelation of M st EqR3 = x (\/) y & B1.(x9,
y9) = EqCl EqR3 by A9;
hence B1.(x,y) = x "\/" y by Def4;
end;
A16: now
let a,b,c be Element of B;
reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2;
thus B1.(a,B1.(b,c)) = B1.(a,U2 "\/" U3) by A14
.= U1 "\/" (U2 "\/" U3) by A14
.= (U1 "\/" U2) "\/" U3 by Th8
.= B1.(U1 "\/" U2,c) by A14
.= B1.(B1.(a,b),c) by A14;
end;
A17: for a,b,c being Element of L holds a"\/"(b"\/"c) = (a"\/"b) "\/"c
proof
let a,b,c be Element of L;
reconsider x=a,y=b,z=c as Element of B;
A18: (the L_join of L).(a,b) = a"\/"b by LATTICES:def 1;
thus a"\/"(b"\/"c) = (the L_join of L).(a,(b"\/"c)) by LATTICES:def 1
.=B1.(x,B1.(y,z)) by LATTICES:def 1
.= (the L_join of L).((the L_join of L).(a,b),c) by A16
.=(a"\/"b)"\/"c by A18,LATTICES:def 1;
end;
A19: now
let x,y be Equivalence_Relation of M;
A20: y in product M2 by A3;
x in product M2 by A3;
then reconsider x9 = x, y9 = y as Element of B by A2,A20;
A21: y9 = y;
x9 = x;
hence B2.(x,y) = x (/\) y by A13,A21;
end;
A22: now
let a,b,c be Element of B;
reconsider U1 = a, U2 = b, U3 = c as Equivalence_Relation of M by A2;
reconsider EQR1 = U2 (/\) U3 as Equivalence_Relation of M by Th11;
reconsider EQR2 = U1 (/\) U2 as Equivalence_Relation of M by Th11;
thus B2.(a,B2.(b,c)) = B2.(a,EQR1) by A19
.= U1 (/\) (U2 (/\) U3) by A19
.= (U1 (/\) U2) (/\) U3 by PBOOLE:29
.= B2.(EQR2,c) by A19
.= B2.(B2.(a,b),c) by A19;
end;
A23: for a,b,c being Element of L holds a"/\"(b"/\"c) = (a"/\"b) "/\"c
proof
let a,b,c be Element of L;
reconsider x=a,y=b,z=c as Element of B;
A24: (the L_meet of L).(a,b) = a"/\"b by LATTICES:def 2;
thus a"/\"(b"/\"c) = (the L_meet of L).(a,(b"/\"c)) by LATTICES:def 2
.=B2.(x,B2.(y,z)) by LATTICES:def 2
.= (the L_meet of L).((the L_meet of L).(a,b),c) by A22
.=(a"/\"b)"/\"c by A24,LATTICES:def 2;
end;
A25: now
let a,b be Element of B;
reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2;
thus B1.(a,b) = U1 "\/" U2 by A14
.= B1.(b,a) by A14;
end;
A26: for a,b being Element of L holds a"\/"b = b"\/"a
proof
let a,b be Element of L;
reconsider x=a,y=b as Element of B;
thus a"\/"b = B1.(x,y) by LATTICES:def 1
.= (the L_join of L).(b,a) by A25
.=b"\/"a by LATTICES:def 1;
end;
A27: for a,b being Element of L holds (a"/\"b)"\/"b = b
proof
let a,b be Element of L;
reconsider x=a,y=b as Element of B;
A28: B1.(B2.(x,y),y)= y
proof
reconsider U1 = x, U2 = y as Equivalence_Relation of M by A2;
reconsider EQR = U1 (/\) U2 as Equivalence_Relation of M by Th11;
B2.(x,y) = U1 (/\) U2 by A19;
hence B1.(B2.(x,y),y) = EQR "\/" U2 by A14
.= y by Th10;
end;
thus (a"/\"b)"\/"b = (the L_join of L).((a"/\"b),b) by LATTICES:def 1
.= b by A28,LATTICES:def 2;
end;
A29: now
let a,b be Element of B;
reconsider U1 = a, U2 = b as Equivalence_Relation of M by A2;
thus B2.(a,b) = U2 (/\) U1 by A19
.= B2.(b,a) by A19;
end;
A30: for a,b being Element of L holds a"/\"b = b"/\"a
proof
let a,b be Element of L;
reconsider x=a,y=b as Element of B;
thus a"/\"b = B2.(x,y) by LATTICES:def 2
.= (the L_meet of L).(b,a) by A29
.=b"/\"a by LATTICES:def 2;
end;
for a,b being Element of L holds a"/\"(a"\/"b)=a
proof
let a,b be Element of L;
reconsider x=a,y=b as Element of B;
A31: B2.(x,B1.(x,y))= x
proof
reconsider U1= x,U2=y as Equivalence_Relation of M by A2;
B1.(x,y) = U1 "\/" U2 by A14;
hence B2.(x,B1.(x,y)) = (U1 (/\)( U1 "\/" U2)) by A19
.= x by Th9;
end;
thus a"/\"(a"\/"b) = (the L_meet of L).(a,(a"\/"b)) by LATTICES:def 2
.= a by A31,LATTICES:def 1;
end;
then L is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A26,A17,A27,A30,A23,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
then reconsider L as strict Lattice;
take L;
thus for x being set holds x in the carrier of L iff x is
Equivalence_Relation of M
by A2,A3;
thus thesis by A14,A19;
end;
uniqueness
proof
let S1,S2 be strict Lattice such that
A32: for x being set holds x in the carrier of S1 iff x is
Equivalence_Relation of M and
A33: for x,y being Equivalence_Relation of M holds (the L_meet of S1).
(x,y) = x (/\) y & (the L_join of S1).(x,y) = x "\/" y and
A34: for x being set holds x in the carrier of S2 iff x is
Equivalence_Relation of M and
A35: for x,y being Equivalence_Relation of M holds (the L_meet of S2).
(x,y) = x (/\) y & (the L_join of S2).(x,y) = x "\/" y;
reconsider Z = the carrier of S1 as non empty set;
now
let x be object;
x is Equivalence_Relation of M iff x in the carrier of S2 by A34;
hence x in the carrier of S1 iff x in the carrier of S2 by A32;
end;
then
A36: the carrier of S1 = the carrier of S2 by TARSKI:2;
A37: now
let x,y be Element of Z;
reconsider x1 = x, y1 = y as Equivalence_Relation of M by A32;
thus (the L_meet of S1).(x,y) = x1 (/\) y1 by A33
.= (the L_meet of S2).(x,y) by A35;
thus (the L_join of S1).(x,y) = x1 "\/" y1 by A33
.= (the L_join of S2).(x,y) by A35;
end;
then the L_meet of S1 = the L_meet of S2 by A36,BINOP_1:2;
hence thesis by A36,A37,BINOP_1:2;
end;
end;
begin
:: LATTICE OF CONGRUENCES IN A MANY SORTED ALGEBRA ::
registration
let S be non empty ManySortedSign;
let A be MSAlgebra over S;
cluster MSEquivalence-like -> MSEquivalence_Relation-like for
ManySortedRelation
of A;
coherence by MSUALG_4:def 3;
end;
reserve S for non void non empty ManySortedSign;
reserve A for non-empty MSAlgebra over S;
theorem Th12:
for o be OperSymbol of S for C1,C2 being MSCongruence of A for
x1,y1 be set for a1,b1 be FinSequence holds [x1,y1] in C1.((the_arity_of o)/.(
len a1 + 1)) \/ C2.((the_arity_of o)/.(len a1 + 1)) implies for x,y be 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
let o be OperSymbol of S;
let C1,C2 be MSCongruence of A;
let x1,y1 be set;
let a1,b1 be FinSequence;
assume
A1: [x1,y1] in C1.((the_arity_of o)/.(len a1 + 1)) \/ C2.((the_arity_of
o)/.(len a1 + 1));
let x,y be Element of Args(o,A);
assume that
A2: x = (a1 ^ <*x1*> ^ b1) and
A3: y = (a1 ^ <*y1*> ^ b1);
A4: y = a1 ^ (<*y1*> ^ b1) by A3,FINSEQ_1:32;
A5: x = a1 ^ (<*x1*> ^ b1) by A2,FINSEQ_1:32;
now
per cases by A1,XBOOLE_0:def 3;
suppose
A6: [x1,y1] in C1.((the_arity_of o)/.(len a1 + 1));
for n be Nat st n in dom x holds [x.n,y.n] in C1.((the_arity_of o)/. n)
proof
let n be Nat;
assume
A7: n in dom x;
then reconsider dz = dom (the_arity_of o) as non empty set by
MSUALG_3:6;
A8: n in dom (the_arity_of o) by A7,MSUALG_3:6;
then
A9: n in dom ((the Sorts of A) * (the_arity_of o)) by PARTFUN1:def 2;
reconsider so = (the Sorts of A) * (the_arity_of o) as non-empty
ManySortedSet of dz;
A10: product so is non empty;
pi(Args(o,A),n) = pi(((the Sorts of A)# * the Arity of S).o,n) by
MSUALG_1:def 4
.= pi((the Sorts of A)# . ((the Arity of S).o),n) by FUNCT_2:15
.= pi((the Sorts of A)# . (the_arity_of o),n) by MSUALG_1:def 1
.= pi(product((the Sorts of A) * (the_arity_of o)),n) by
FINSEQ_2:def 5
.= ((the Sorts of A) * (the_arity_of o)).n by A9,A10,CARD_3:12
.= (the Sorts of A) . ((the_arity_of o).n) by A8,FUNCT_1:13
.= (the Sorts of A) . ((the_arity_of o)/.n) by A8,PARTFUN1:def 6;
then
A11: x.n in (the Sorts of A).((the_arity_of o)/.n) by CARD_3:def 6;
A12: n in dom (a1 ^ <*x1*>) or ex k be Nat st k in dom b1 & n = len (
a1 ^ <*x1*>) + k by A2,A7,FINSEQ_1:25;
now
per cases by A12,FINSEQ_1:25;
suppose
A13: n in dom a1;
then
A14: y.n = a1.n by A4,FINSEQ_1:def 7;
x.n = a1.n by A5,A13,FINSEQ_1:def 7;
hence thesis by A11,A14,EQREL_1:5;
end;
suppose
ex m be Nat st m in dom <*x1*> & n = len a1 + m;
then consider m be Nat such that
A15: m in dom <*x1*> and
A16: n = len a1 + m;
A17: m in Seg 1 by A15,FINSEQ_1:38;
then
A18: m = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A19: n in Seg (len a1 + 1) by A16,FINSEQ_1:4;
then n in Seg (len a1 + len <*y1*>) by FINSEQ_1:40;
then n in Seg len (a1 ^ <*y1*>) by FINSEQ_1:22;
then n in dom (a1 ^ <*y1*>) by FINSEQ_1:def 3;
then
A20: y.n = (a1 ^ <*y1*>).(len a1 + 1) by A3,A16,A18,FINSEQ_1:def 7
.= y1 by FINSEQ_1:42;
n in Seg (len a1 + len <*x1*>) by A19,FINSEQ_1:40;
then n in Seg len (a1 ^ <*x1*>) by FINSEQ_1:22;
then n in dom (a1 ^ <*x1*>) by FINSEQ_1:def 3;
then x.n = (a1 ^ <*x1*>).(len a1 + 1) by A2,A16,A18,FINSEQ_1:def 7
.= x1 by FINSEQ_1:42;
hence thesis by A6,A16,A17,A20,FINSEQ_1:2,TARSKI:def 1;
end;
suppose
ex k be Element of NAT st k in dom b1 & n = len (a1 ^ <* x1*>) + k;
then consider k be Element of NAT such that
A21: k in dom b1 and
A22: n = len (a1 ^ <*x1*>) + k;
n = len a1 + len <*x1*> + k by A22,FINSEQ_1:22;
then n = len a1 + 1 + k by FINSEQ_1:40;
then n = len a1 + len <*y1*> + k by FINSEQ_1:40;
then n = len (a1 ^ <*y1*>) + k by FINSEQ_1:22;
then
A23: y.n = b1.k by A3,A21,FINSEQ_1:def 7;
x.n = b1.k by A2,A21,A22,FINSEQ_1:def 7;
hence thesis by A11,A23,EQREL_1:5;
end;
end;
hence thesis;
end;
then [Den(o,A).x,Den(o,A).y] in C1.(the_result_sort_of o) by
MSUALG_4:def 4;
hence thesis by XBOOLE_0:def 3;
end;
suppose
A24: [x1,y1] in C2.((the_arity_of o)/.(len a1 + 1));
for n be Nat st n in dom x holds [x.n,y.n] in C2.((the_arity_of o) /.n)
proof
let n be Nat;
assume
A25: n in dom x;
then reconsider dz = dom (the_arity_of o) as non empty set by
MSUALG_3:6;
A26: n in dom (the_arity_of o) by A25,MSUALG_3:6;
then
A27: n in dom ((the Sorts of A) * (the_arity_of o)) by PARTFUN1:def 2;
reconsider so = (the Sorts of A) * (the_arity_of o) as non-empty
ManySortedSet of dz;
A28: product so is non empty;
pi(Args(o,A),n) = pi(((the Sorts of A)# * the Arity of S).o,n) by
MSUALG_1:def 4
.= pi((the Sorts of A)# . ((the Arity of S).o),n) by FUNCT_2:15
.= pi((the Sorts of A)# . (the_arity_of o),n) by MSUALG_1:def 1
.= pi(product((the Sorts of A) * (the_arity_of o)),n) by
FINSEQ_2:def 5
.= ((the Sorts of A) * (the_arity_of o)).n by A27,A28,CARD_3:12
.= (the Sorts of A) . ((the_arity_of o).n) by A26,FUNCT_1:13
.= (the Sorts of A) . ((the_arity_of o)/.n) by A26,PARTFUN1:def 6;
then
A29: x.n in (the Sorts of A).((the_arity_of o)/.n) by CARD_3:def 6;
A30: n in dom (a1 ^ <*x1*>) or ex k be Nat st k in dom b1 & n = len (
a1 ^ <*x1*>) + k by A2,A25,FINSEQ_1:25;
now
per cases by A30,FINSEQ_1:25;
suppose
A31: n in dom a1;
then
A32: y.n = a1.n by A4,FINSEQ_1:def 7;
x.n = a1.n by A5,A31,FINSEQ_1:def 7;
hence thesis by A29,A32,EQREL_1:5;
end;
suppose
ex m be Nat st m in dom <*x1*> & n = len a1 + m;
then consider m be Nat such that
A33: m in dom <*x1*> and
A34: n = len a1 + m;
A35: m in Seg 1 by A33,FINSEQ_1:38;
then
A36: m = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A37: n in Seg (len a1 + 1) by A34,FINSEQ_1:4;
then n in Seg (len a1 + len <*y1*>) by FINSEQ_1:40;
then n in Seg len (a1 ^ <*y1*>) by FINSEQ_1:22;
then n in dom (a1 ^ <*y1*>) by FINSEQ_1:def 3;
then
A38: y.n = (a1 ^ <*y1*>).(len a1 + 1) by A3,A34,A36,FINSEQ_1:def 7
.= y1 by FINSEQ_1:42;
n in Seg (len a1 + len <*x1*>) by A37,FINSEQ_1:40;
then n in Seg len (a1 ^ <*x1*>) by FINSEQ_1:22;
then n in dom (a1 ^ <*x1*>) by FINSEQ_1:def 3;
then x.n = (a1 ^ <*x1*>).(len a1 + 1) by A2,A34,A36,FINSEQ_1:def 7
.= x1 by FINSEQ_1:42;
hence thesis by A24,A34,A35,A38,FINSEQ_1:2,TARSKI:def 1;
end;
suppose
ex k be Element of NAT st k in dom b1 & n = len (a1 ^ <* x1*>) + k;
then consider k be Element of NAT such that
A39: k in dom b1 and
A40: n = len (a1 ^ <*x1*>) + k;
n = len a1 + len <*x1*> + k by A40,FINSEQ_1:22;
then n = len a1 + 1 + k by FINSEQ_1:40;
then n = len a1 + len <*y1*> + k by FINSEQ_1:40;
then n = len (a1 ^ <*y1*>) + k by FINSEQ_1:22;
then
A41: y.n = b1.k by A3,A39,FINSEQ_1:def 7;
x.n = b1.k by A2,A39,A40,FINSEQ_1:def 7;
hence thesis by A29,A41,EQREL_1:5;
end;
end;
hence thesis;
end;
then [Den(o,A).x,Den(o,A).y] in C2.(the_result_sort_of o) by
MSUALG_4:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
theorem Th13:
for o be OperSymbol of S for C1,C2 being MSCongruence of A for C
being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2
for x1,y1 be object
for n be Element of NAT for a1,a2,b1 being FinSequence st len a1 = n & len
a1 = len a2 & for k be Element of NAT st k in dom a1 holds [a1.k,a2.k] in C.((
the_arity_of o)/.k) holds ( [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))
implies for x be 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
let o be OperSymbol of S;
let C1,C2 be MSCongruence of A;
let C be MSEquivalence-like ManySortedRelation of A such that
A1: C = C1 "\/" C2;
consider C9 being ManySortedRelation of the Sorts of A such that
A2: C9 = C1 (\/) C2 and
A3: C1 "\/" C2 = EqCl C9 by Def4;
A4: C1.(the_result_sort_of o) "\/" C2.(the_result_sort_of o) = EqCl (C1.(
the_result_sort_of o) \/ C2.(the_result_sort_of o)) by Th1
.= EqCl (C9.(the_result_sort_of o)) by A2,PBOOLE:def 4
.= (C1 "\/" C2).(the_result_sort_of o) by A3,Def3;
consider D9 being ManySortedRelation of the Sorts of A such that
A5: D9 = C1 (\/) C2 and
A6: C1 "\/" C2 = EqCl D9 by Def4;
let x1,y1 be object;
let n be Element of NAT;
let a1,a2,b1 be FinSequence such that
A7: len a1 = n and
A8: len a1 = len a2 and
A9: for k be Element of NAT st k in dom a1 holds [a1.k,a2.k] in C.((
the_arity_of o)/.k);
A10: C1.((the_arity_of o)/.(n+1)) "\/" C2.((the_arity_of o)/.(n+1)) = EqCl (
C1.((the_arity_of o)/.(n+1)) \/ C2.((the_arity_of o)/.(n+1))) by Th1
.= EqCl (D9.((the_arity_of o)/.(n+1))) by A5,PBOOLE:def 4
.= (C1 "\/" C2).((the_arity_of o)/.(n+1)) by A6,Def3;
set y = a2 ^ <*y1*> ^ b1;
assume that
A11: [Den(o,A).(a1 ^ <*x1*> ^ b1),Den(o,A).(a2 ^ <*x1*> ^ b1)] in C.(
the_result_sort_of o) and
A12: [x1,y1] in C.((the_arity_of o)/.(n+1));
let x be Element of Args(o,A) such that
A13: x = a1 ^ <*x1*> ^ b1;
A14: (the Sorts of A).(the_result_sort_of o) = (the Sorts of A).((the
ResultSort of S).o) by MSUALG_1:def 2
.= ((the Sorts of A) * the ResultSort of S).o by FUNCT_2:15
.= Result(o,A) by MSUALG_1:def 5;
then Den(o,A).x in (the Sorts of A).(the_result_sort_of o);
then consider p be FinSequence such that
A15: 1 <= len p and
A16: Den(o,A).(a1 ^ <*x1*> ^ b1) = p.1 and
A17: Den(o,A).(a2 ^ <*x1*> ^ b1) = p.(len p) and
A18: for i be Nat st 1 <= i & i < len p holds [p.i,p.(i+1)]
in C1.(the_result_sort_of o) \/ C2.(the_result_sort_of o) by A1,A11,A13,A4,
EQREL_1:28;
x1 in (the Sorts of A).((the_arity_of o)/.(n+1)) by A12,ZFMISC_1:87;
then consider f be FinSequence such that
A19: 1 <= len f and
A20: x1 = f.1 and
A21: y1 = f.(len f) and
A22: for i be Nat st 1 <= i & i < len f holds [f.i,f.(i+1)]
in C1.((the_arity_of o)/.(n+1)) \/ C2.((the_arity_of o)/.(n+1)) by A1,A12,A10,
EQREL_1:28;
deffunc G(Nat)=Den(o,A).(a2 ^ <*f.$1*> ^ b1);
consider g be FinSequence such that
A23: len g = len f & for i be Nat st i in dom g holds g.i = G(i) from
FINSEQ_1:sch 2;
A24: dom g = Seg len f by A23,FINSEQ_1:def 3;
A25: dom x = Seg len (a1 ^ <*x1*> ^ b1) by A13,FINSEQ_1:def 3
.= Seg len (a1 ^ (<*x1*> ^ b1)) by FINSEQ_1:32
.= Seg (len a2 + len (<*x1*> ^ b1)) by A8,FINSEQ_1:22
.= Seg len (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:22
.= Seg len (a2 ^ <*x1*> ^ b1) by FINSEQ_1:32
.= dom (a2 ^ <*x1*> ^ b1) by FINSEQ_1:def 3;
ex q being FinSequence st 1 <= len q & Den(o,A).x = q.1 & Den(o,A).y =
q.(len q) & for i be Nat st 1 <= i & i < len q holds [q.i,q.(i+1)]
in C1.(the_result_sort_of o) \/ C2.(the_result_sort_of o)
proof
take q = p ^ g;
A26: len q = len p + len g by FINSEQ_1:22;
hence 1 <= len q by A15,NAT_1:12;
1 in dom p by A15,FINSEQ_3:25;
hence q.1 = Den(o,A).x by A13,A16,FINSEQ_1:def 7;
A27: len g in Seg len f by A19,A23,FINSEQ_1:1;
then len g in dom g by A23,FINSEQ_1:def 3;
hence q.(len q) = g.len g by A26,FINSEQ_1:def 7
.= Den(o,A).y by A21,A23,A24,A27;
A28: len p <> 0 by A15;
hereby
let i be Nat such that
A29: 1 <= i and
A30: i < len q;
A31: 1 <= i & i < len p or len p + 1 <= i & i < len q or i = len p
proof
assume that
A32: not (1 <= i & i < len p) and
A33: not (len p + 1 <= i & i < len q);
i <= len p by A30,A33,NAT_1:13;
hence thesis by A29,A32,XXREAL_0:1;
end;
A34: Seg len (a1 ^ <*x1*> ^ b1) = dom x by A13,FINSEQ_1:def 3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
A35: len (a2 ^ <*x1*> ^ b1) = len (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32
.= len a2 + len (<*x1*> ^ b1) by FINSEQ_1:22
.= len (a1 ^ (<*x1*> ^ b1)) by A8,FINSEQ_1:22
.= len (a1 ^ <*x1*> ^ b1) by FINSEQ_1:32
.= len the_arity_of o by A34,FINSEQ_1:6;
A36: now
let k be Element of NAT;
assume k in dom x;
then
A37: k in Seg len (the_arity_of o) by A25,A35,FINSEQ_1:def 3;
then
A38: k in dom (the_arity_of o) by FINSEQ_1:def 3;
then
A39: k in dom ((the Sorts of A) * (the_arity_of o)) by PARTFUN1:def 2;
reconsider dz = dom (the_arity_of o) as non empty set by A37,
FINSEQ_1:def 3;
reconsider so = (the Sorts of A) * (the_arity_of o) as non-empty
ManySortedSet of dz;
A40: product so is non empty;
pi(Args(o,A),k) = pi(((the Sorts of A)# * the Arity of S).o,k) by
MSUALG_1:def 4
.= pi((the Sorts of A)# . ((the Arity of S).o),k) by FUNCT_2:15
.= pi((the Sorts of A)# . (the_arity_of o),k) by MSUALG_1:def 1
.= pi(product((the Sorts of A) * (the_arity_of o)),k) by
FINSEQ_2:def 5
.= ((the Sorts of A) * (the_arity_of o)).k by A39,A40,CARD_3:12
.= (the Sorts of A) . ((the_arity_of o).k) by A38,FUNCT_1:13
.= (the Sorts of A) . ((the_arity_of o)/.k) by A38,PARTFUN1:def 6;
hence x.k in (the Sorts of A).((the_arity_of o)/.k) by CARD_3:def 6;
end;
A41: ex i1 being Nat st len p = i1 + 1 by A28,NAT_1:6;
now
per cases by A31;
suppose
A42: 1 <= i & i < len p;
then
A43: i+1 <= len p by NAT_1:13;
1 <= i+1 by A42,NAT_1:13;
then i+1 in dom p by A43,FINSEQ_3:25;
then
A44: q.(i+1) = p.(i+1) by FINSEQ_1:def 7;
i in dom p by A42,FINSEQ_3:25;
then q.i = p.i by FINSEQ_1:def 7;
hence [q.i,q.(i+1)] in C1.(the_result_sort_of o) \/ C2.(
the_result_sort_of o) by A18,A42,A44;
end;
suppose
A45: i = len p;
then i in Seg len p by A41,FINSEQ_1:4;
then i in dom p by FINSEQ_1:def 3;
then
A46: q.i = Den(o,A).(a2 ^ <*x1*> ^ b1) by A17,A45,FINSEQ_1:def 7;
A47: 1 in Seg len g by A19,A23,FINSEQ_1:1;
then 1 in dom g by FINSEQ_1:def 3;
then
A48: q.(i+1) = g.1 by A45,FINSEQ_1:def 7
.= Den(o,A).(a2 ^ <*x1*> ^ b1) by A20,A23,A24,A47;
for k be Nat st k in dom (a2 ^ <*x1*> ^ b1) holds (a2 ^ <*x1*>
^ b1).k in (the Sorts of A).((the_arity_of o)/.k)
proof
let k be Nat;
assume
A49: k in dom (a2 ^ <*x1*> ^ b1);
then
A50: k in dom (a2 ^ (<*x1*> ^ b1)) by FINSEQ_1:32;
now
per cases by A50,FINSEQ_1:25;
suppose
A51: k in dom a2;
then k in Seg len a2 by FINSEQ_1:def 3;
then k in dom a1 by A8,FINSEQ_1:def 3;
then
A52: [a1.k,a2.k] in C.((the_arity_of o)/.k) by A9;
(a2 ^ <*x1*> ^ b1).k = (a2 ^ (<*x1*> ^ b1)).k by FINSEQ_1:32
.= a2.k by A51,FINSEQ_1:def 7;
hence thesis by A52,ZFMISC_1:87;
end;
suppose
ex n1 be Nat st n1 in dom (<*x1*> ^ b1) & k = len a2 + n1;
then consider n1 be Nat such that
A53: n1 in dom (<*x1*> ^ b1) and
A54: k = len a2 + n1;
(a2 ^ <*x1*> ^ b1).k = (a2 ^ (<*x1*> ^ b1)).k by FINSEQ_1:32
.= (<*x1*> ^ b1).n1 by A53,A54,FINSEQ_1:def 7
.= (a1 ^ (<*x1*> ^ b1)).k by A8,A53,A54,FINSEQ_1:def 7
.= x.k by A13,FINSEQ_1:32;
hence thesis by A25,A36,A49;
end;
end;
hence thesis;
end;
then reconsider
de = (a2 ^ <*x1*> ^ b1) as Element of Args(o,A) by A35,MSAFREE2:5;
A55: field (C2.(the_result_sort_of o)) = (the Sorts of A).(
the_result_sort_of o) by EQREL_1:9;
field (C1.(the_result_sort_of o)) = (the Sorts of A).(
the_result_sort_of o) by EQREL_1:9;
then
field (C1.(the_result_sort_of o) \/ C2.( the_result_sort_of o))
= (the Sorts of A).(the_result_sort_of o) \/ (the Sorts of A).(
the_result_sort_of o) by A55,RELAT_1:18
.= (the Sorts of A).(the_result_sort_of o);
then
A56: C1.(the_result_sort_of o) \/ C2.(the_result_sort_of o)
is_reflexive_in (the Sorts of A).(the_result_sort_of o) by RELAT_2:def 9;
Den(o,A).de in (the Sorts of A).(the_result_sort_of o) by A14;
hence [q.i,q.(i+1)] in C1.(the_result_sort_of o) \/ C2.(
the_result_sort_of o) by A46,A48,A56,RELAT_2:def 1;
end;
suppose
A57: len p + 1 <= i & i < len q;
then len p < i by NAT_1:13;
then reconsider j = i - len p as Element of NAT by NAT_1:21;
A58: 1 <= j+1 by NAT_1:12;
len f = len q - len p by A23,A26,XCMPLX_1:26;
then
A59: j < len f by A57,XREAL_1:9;
then j+1 <= len f by NAT_1:13;
then j+1 in Seg len f by A58,FINSEQ_1:1;
then
A60: i + 1 - len p in Seg len f by XCMPLX_1:29;
A61: 1 <= j by A57,XREAL_1:19;
then
A62: [f.j,f.(j + 1)] in C1.((the_arity_of o)/.(n+1)) \/ C2.((
the_arity_of o)/.(n+1)) by A22,A59;
then
A63: f.(i - len p + 1) in (the Sorts of A).((the_arity_of o)/.(n+1)
) by ZFMISC_1:87;
A64: for k be Nat st k in dom (a2 ^ <*f.(i + 1 - len p)*> ^ b1)
holds (a2 ^ <*f.(i + 1 - len p)*> ^ b1).k in (the Sorts of A).((the_arity_of o)
/.k)
proof
let k be Nat;
assume
A65: k in dom (a2 ^ <*f.(i + 1 - len p)*> ^ b1);
then
A66: k in dom (a2 ^ <*f.(i + 1 - len p)*>) or ex n1 be Nat st n1
in dom b1 & k = len (a2 ^ <*f.(i + 1 - len p)*>) + n1 by FINSEQ_1:25;
now
per cases by A66,FINSEQ_1:25;
suppose
A67: k in dom a2;
then k in Seg len a2 by FINSEQ_1:def 3;
then k in dom a1 by A8,FINSEQ_1:def 3;
then
A68: [a1.k,a2.k] in C.((the_arity_of o)/.k) by A9;
(a2 ^ <*f.(i + 1 - len p)*> ^ b1).k = (a2 ^ (<*f.(i + 1
- len p)*> ^ b1)).k by FINSEQ_1:32
.= a2.k by A67,FINSEQ_1:def 7;
hence thesis by A68,ZFMISC_1:87;
end;
suppose
ex n2 be Nat st n2 in dom <*f.(i + 1 - len p)*> & k
= len a2 + n2;
then consider n2 be Nat such that
A69: n2 in dom <*f.(i + 1 - len p)*> and
A70: k = len a2 + n2;
n2 in Seg 1 by A69,FINSEQ_1:38;
then
A71: k = len a1 + 1 by A8,A70,FINSEQ_1:2,TARSKI:def 1;
then k in Seg (len a2 + 1) by A8,FINSEQ_1:4;
then k in Seg (len a2 + len <*f.(i + 1 - len p)*>) by
FINSEQ_1:40;
then k in Seg len (a2 ^ <*f.(i + 1 - len p)*>) by FINSEQ_1:22;
then k in dom (a2 ^ <*f.(i + 1 - len p)*>) by FINSEQ_1:def 3;
then (a2 ^ <*f.(i + 1 - len p)*> ^ b1).k = (a2 ^ <*f.(i + 1 -
len p)*>).k by FINSEQ_1:def 7
.= f.(i + 1 - len p) by A8,A71,FINSEQ_1:42;
hence thesis by A7,A63,A71,XCMPLX_1:29;
end;
suppose
A72: ex n1 be Element of NAT st n1 in dom b1 & k = len (
a2 ^ <*f.(i + 1 - len p)*>) + n1;
A73: len (a1 ^ <*x1*>) = len a1 + len <*x1*> by FINSEQ_1:22
.= len a2 + 1 by A8,FINSEQ_1:40
.= len a2 + len <*f.(i + 1 - len p)*> by FINSEQ_1:40
.= len (a2 ^ <*f.(i + 1 - len p)*>) by FINSEQ_1:22;
A74: dom x = Seg len (a1 ^ <*x1*> ^ b1) by A13,FINSEQ_1:def 3
.= Seg (len (a1 ^ <*x1*>) + len b1) by FINSEQ_1:22
.= Seg ((len a1 + len <*x1*>) + len b1) by FINSEQ_1:22
.= Seg ((len a2 + 1) + len b1) by A8,FINSEQ_1:40
.= Seg ((len a2 + len <*f.(i + 1 - len p)*>) + len b1) by
FINSEQ_1:40
.= Seg (len (a2 ^ <*f.(i + 1 - len p)*>) + len b1) by
FINSEQ_1:22
.= Seg len (a2 ^ <*f.(i + 1 - len p)*> ^ b1) by FINSEQ_1:22
.= dom (a2 ^ <*f.(i + 1 - len p)*> ^ b1) by FINSEQ_1:def 3;
consider n1 be Element of NAT such that
A75: n1 in dom b1 and
A76: k = len (a2 ^ <*f.(i + 1 - len p)*>) + n1 by A72;
(a2 ^ <*f.(i + 1 - len p)*> ^ b1).k = b1.n1 by A75,A76,
FINSEQ_1:def 7
.= x.k by A13,A75,A76,A73,FINSEQ_1:def 7;
hence thesis by A36,A65,A74;
end;
end;
hence thesis;
end;
A77: f.(i - len p) in (the Sorts of A).((the_arity_of o)/.( n+1)) by A62,
ZFMISC_1:87;
A78: for k be Nat st k in dom (a2 ^ <*f.(i - len p)*> ^ b1) holds (
a2 ^ <*f.(i - len p)*> ^ b1).k in (the Sorts of A).((the_arity_of o)/.k)
proof
let k be Nat;
assume
A79: k in dom (a2 ^ <*f.(i - len p)*> ^ b1);
then
A80: k in dom (a2 ^ <*f.(i - len p)*>) or ex n1 be Nat st n1 in
dom b1 & k = len (a2 ^ <*f.(i - len p)*>) + n1 by FINSEQ_1:25;
now
per cases by A80,FINSEQ_1:25;
suppose
A81: k in dom a2;
then k in Seg len a2 by FINSEQ_1:def 3;
then k in dom a1 by A8,FINSEQ_1:def 3;
then
A82: [a1.k,a2.k] in C.((the_arity_of o)/.k) by A9;
(a2 ^ <*f.(i - len p)*> ^ b1).k = (a2 ^ (<*f.(i - len p)
*> ^ b1)).k by FINSEQ_1:32
.= a2.k by A81,FINSEQ_1:def 7;
hence thesis by A82,ZFMISC_1:87;
end;
suppose
ex n2 be Nat st n2 in dom <*f.(i - len p)*> & k = len a2 + n2;
then consider n2 be Nat such that
A83: n2 in dom <*f.(i - len p)*> and
A84: k = len a2 + n2;
A85: n2 in Seg 1 by A83,FINSEQ_1:38;
then
A86: k = len a1 + 1 by A8,A84,FINSEQ_1:2,TARSKI:def 1;
then k in Seg (len a2 + 1) by A8,FINSEQ_1:4;
then k in Seg (len a2 + len <*f.(i - len p)*>) by FINSEQ_1:40;
then k in Seg len (a2 ^ <*f.(i - len p)*>) by FINSEQ_1:22;
then k in dom (a2 ^ <*f.(i - len p)*>) by FINSEQ_1:def 3;
then (a2 ^ <*f.(i - len p)*> ^ b1).k = (a2 ^ <*f.(i - len p)
*>).k by FINSEQ_1:def 7
.= f.(i - len p) by A8,A86,FINSEQ_1:42;
hence thesis by A7,A8,A77,A84,A85,FINSEQ_1:2,TARSKI:def 1;
end;
suppose
A87: ex n1 be Element of NAT st n1 in dom b1 & k = len (
a2 ^ <*f.(i - len p)*>) + n1;
A88: len (a1 ^ <*x1*>) = len a1 + len <*x1*> by FINSEQ_1:22
.= len a2 + 1 by A8,FINSEQ_1:40
.= len a2 + len <*f.(i - len p)*> by FINSEQ_1:40
.= len (a2 ^ <*f.(i - len p)*>) by FINSEQ_1:22;
A89: dom x = Seg len (a1 ^ <*x1*> ^ b1) by A13,FINSEQ_1:def 3
.= Seg (len (a1 ^ <*x1*>) + len b1) by FINSEQ_1:22
.= Seg ((len a1 + len <*x1*>) + len b1) by FINSEQ_1:22
.= Seg ((len a2 + 1) + len b1) by A8,FINSEQ_1:40
.= Seg ((len a2 + len <*f.(i - len p)*>) + len b1) by
FINSEQ_1:40
.= Seg (len (a2 ^ <*f.(i - len p)*>) + len b1) by FINSEQ_1:22
.= Seg len (a2 ^ <*f.(i - len p)*> ^ b1) by FINSEQ_1:22
.= dom (a2 ^ <*f.(i - len p)*> ^ b1) by FINSEQ_1:def 3;
consider n1 be Element of NAT such that
A90: n1 in dom b1 and
A91: k = len (a2 ^ <*f.(i - len p)*>) + n1 by A87;
(a2 ^ <*f.(i - len p)*> ^ b1).k = b1.n1 by A90,A91,
FINSEQ_1:def 7
.= x.k by A13,A90,A91,A88,FINSEQ_1:def 7;
hence thesis by A36,A79,A89;
end;
end;
hence thesis;
end;
A92: 1 <= j by A57,XREAL_1:19;
j <= len f by A23,A26,A57,XREAL_1:19;
then
A93: i - len p in Seg len f by A92,FINSEQ_1:1;
A94: Seg len (a1 ^ <*x1*> ^ b1) = dom x by A13,FINSEQ_1:def 3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
A95: len (a2 ^ <*f.(i + 1 - len p)*> ^ b1) = len (a2 ^ <*f.(i + 1 -
len p)*>) + len b1 by FINSEQ_1:22
.= len a2 + len <*f.(i + 1 - len p)*> + len b1 by FINSEQ_1:22
.= len a2 + 1 + len b1 by FINSEQ_1:40
.= len a1 + len <*x1*> + len b1 by A8,FINSEQ_1:40
.= len (a1 ^ <*x1*>) + len b1 by FINSEQ_1:22
.= len (a1 ^ <*x1*> ^ b1) by FINSEQ_1:22
.= len the_arity_of o by A94,FINSEQ_1:6;
len (a2 ^ <*f.(i - len p)*> ^ b1) = len (a2 ^ <*f.(i - len p)
*>) + len b1 by FINSEQ_1:22
.= len a2 + len <*f.(i - len p)*> + len b1 by FINSEQ_1:22
.= len a2 + 1 + len b1 by FINSEQ_1:40
.= len a1 + len <*x1*> + len b1 by A8,FINSEQ_1:40
.= len (a1 ^ <*x1*>) + len b1 by FINSEQ_1:22
.= len (a1 ^ <*x1*> ^ b1) by FINSEQ_1:22
.= len the_arity_of o by A94,FINSEQ_1:6;
then reconsider
d1 = a2 ^ <*f.(i - len p)*> ^ b1, d2 = a2 ^ <*f.(i + 1 -
len p)*> ^ b1 as Element of Args(o,A) by A78,A64,A95,MSAFREE2:5;
A96: q.i = g.(i - len p) by A26,A57,FINSEQ_1:23
.= Den(o,A).d1 by A23,A24,A93;
i + 1 - len p = i - len p + 1 by XCMPLX_1:29;
then
A97: [f.(i - len p),f.(i + 1 - len p)] in C1.((the_arity_of o)/.(n+
1)) \/ C2.((the_arity_of o)/.(n+1)) by A22,A61,A59;
A98: i+1 <= len q by A57,NAT_1:13;
len p + 1 <= i+1 by A57,NAT_1:12;
then q.(i+1) = g.(i + 1 - len p) by A26,A98,FINSEQ_1:23
.= Den(o,A).d2 by A23,A24,A60;
hence [q.i,q.(i+1)] in C1.(the_result_sort_of o) \/ C2.(
the_result_sort_of o) by A7,A8,A96,A97,Th12;
end;
end;
hence [q.i,q.(i+1)] in C1.(the_result_sort_of o) \/ C2.(
the_result_sort_of o);
end;
end;
hence thesis by A1,A4,A14,EQREL_1:28;
end;
theorem Th14:
for o be OperSymbol of S for C1,C2 being MSCongruence of A for C
being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 for x,y be
Element of Args(o,A) holds (( for n be Nat st n in dom x holds [x.n,y.n] in C.(
(the_arity_of o)/.n)) implies [Den(o,A).x,Den(o,A).y] in C.(the_result_sort_of
o))
proof
set b1 = {};
let o be OperSymbol of S;
let C1,C2 be MSCongruence of A;
let C be MSEquivalence-like ManySortedRelation of A such that
A1: C = C1 "\/" C2;
let x,y be Element of Args(o,A);
defpred P[Nat] means for a1,a2,b1 being FinSequence holds ((len
a1 = $1 & len a1 = len a2 & x = a1 ^ b1 & for n be Nat st n in dom a1 holds [x.
n,(a2 ^ b1).n] in C.((the_arity_of o)/.n)) implies [Den(o,A).x,Den(o,A).(a2 ^
b1)] in C.(the_result_sort_of o));
A2: for l be Nat st P[l] holds P[l+1]
proof
let l be Nat such that
A3: for a1,a2,b1 being FinSequence holds ((len a1 = l & len a1 = len
a2 & x = a1 ^ b1 & for n be Nat st n in dom a1 holds [x.n,(a2 ^ b1).n] in C.((
the_arity_of o)/.n)) implies [Den(o,A).x,Den(o,A).(a2 ^ b1)] in C.(
the_result_sort_of o));
let a1,a2,b1 be FinSequence;
assume that
A4: len a1 = l+1 and
A5: len a1 = len a2 and
A6: x = a1 ^ b1 and
A7: for n be Nat st n in dom a1 holds [x.n,(a2 ^ b1).n] in C.((
the_arity_of o)/.n);
A8: l+1 in Seg len a1 by A4,FINSEQ_1:4;
then
A9: l+1 in dom a2 by A5,FINSEQ_1:def 3;
set y = a2 ^ b1;
a2 <> {} by A4,A5;
then consider q2 be FinSequence, y1 be object such that
A10: a2 = q2 ^ <*y1*> by FINSEQ_1:46;
A11: l+1 = len q2 + len <*y1*> by A4,A5,A10,FINSEQ_1:22
.= len q2 + 1 by FINSEQ_1:40;
then
A12: y1 = a2.(l + 1) by A10,FINSEQ_1:42
.= y.(l + 1) by A9,FINSEQ_1:def 7;
a1 <> {} by A4;
then consider q1 be FinSequence, x1 be object such that
A13: a1 = q1 ^ <*x1*> by FINSEQ_1:46;
A14: l+1 = len q1 + len <*x1*> by A4,A13,FINSEQ_1:22
.= len q1 + 1 by FINSEQ_1:40;
then
A15: len q1 = len q2 by A11,XCMPLX_1:2;
A16: dom q1 = Seg len q1 by FINSEQ_1:def 3
.= dom q2 by A15,FINSEQ_1:def 3;
A17: for n be Element of NAT st n in dom q1 holds [q1.n,q2.n] in C.((
the_arity_of o)/.n)
proof
let n be Element of NAT;
len q1 <= len a1 by A4,A14,NAT_1:11;
then
A18: Seg len q1 c= Seg len a1 by FINSEQ_1:5;
assume
A19: n in dom q1;
then n in Seg len q1 by FINSEQ_1:def 3;
then n in Seg len a1 by A18;
then
A20: n in dom a1 by FINSEQ_1:def 3;
then
A21: x.n = a1.n by A6,FINSEQ_1:def 7
.= q1.n by A13,A19,FINSEQ_1:def 7;
dom a1 = Seg len a1 by FINSEQ_1:def 3
.= dom a2 by A5,FINSEQ_1:def 3;
then y.n = a2.n by A20,FINSEQ_1:def 7
.= q2.n by A10,A16,A19,FINSEQ_1:def 7;
hence thesis by A7,A20,A21;
end;
A22: l+1 in dom a1 by A8,FINSEQ_1:def 3;
A23: q1 ^ <*x1*> ^ b1 = q1 ^ (<*x1*> ^ b1) by FINSEQ_1:32;
A24: q2 ^ <*x1*> ^ b1 = q2 ^ (<*x1*> ^ b1) by FINSEQ_1:32;
A25: for n be Nat st n in dom q1 holds [x.n,(q2 ^ <*x1*> ^ b1).n] in C.((
the_arity_of o)/.n)
proof
let n be Nat;
assume
A26: n in dom q1;
then
A27: (q2 ^ <*x1*> ^ b1).n = q2.n by A16,A24,FINSEQ_1:def 7;
x.n = q1.n by A6,A13,A23,A26,FINSEQ_1:def 7;
hence thesis by A17,A26,A27;
end;
x1 = a1.(l + 1) by A13,A14,FINSEQ_1:42
.= x.(l + 1) by A6,A22,FINSEQ_1:def 7;
then
A28: [x1,y1] in C.((the_arity_of o)/.(l+1)) by A7,A22,A12;
len q1 = l by A14,XCMPLX_1:2;
then [Den(o,A).x,Den(o,A).(q2 ^ <*x1*> ^ b1)] in C.(the_result_sort_of o)
by A3,A6,A13,A15,A23,A24,A25;
hence thesis by A1,A6,A13,A10,A14,A15,A17,A28,Th13;
end;
A29: dom y = dom (the_arity_of o) by MSUALG_3:6
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
dom x = dom (the_arity_of o) by MSUALG_3:6
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
then reconsider a1 = x, a2 = y as FinSequence by A29,FINSEQ_1:def 2;
assume
A30: for n be Nat st n in dom x holds [x.n,y.n] in C.((the_arity_of o)/.n );
A31: Seg len a2 = dom a2 by FINSEQ_1:def 3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
Seg len a1 = dom a1 by FINSEQ_1:def 3
.= dom (the_arity_of o) by MSUALG_3:6
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
then
A32: len a1 = len a2 by A31,FINSEQ_1:6;
A33: x = a1 ^ b1 by FINSEQ_1:34;
A34: y = a2 ^ b1 by FINSEQ_1:34;
A35: P[ 0 ]
proof
field(C.(the_result_sort_of o)) = (the Sorts of A).(
the_result_sort_of o) by ORDERS_1:12;
then
A36: C.(the_result_sort_of o) is_reflexive_in (the Sorts of A).(
the_result_sort_of o) by RELAT_2:def 9;
A37: (the Sorts of A).(the_result_sort_of o) = (the Sorts of A).((the
ResultSort of S).o) by MSUALG_1:def 2
.= ((the Sorts of A) * the ResultSort of S).o by FUNCT_2:15
.= Result(o,A) by MSUALG_1:def 5;
let a1,a2,b1 be FinSequence;
assume that
A38: len a1 = 0 and
A39: len a1 = len a2 and
A40: x = a1 ^ b1 and
for n be Nat st n in dom a1 holds [x.n,(a2 ^ b1).n] in C.((
the_arity_of o)/.n);
A41: a1 = {} by A38;
a2 = {} by A38,A39;
hence thesis by A40,A41,A37,A36,RELAT_2:def 1;
end;
for l be Nat holds P[l] from NAT_1:sch 2(A35,A2);
hence thesis by A30,A32,A33,A34;
end;
theorem Th15:
for C1,C2 being MSCongruence of A holds C1 "\/" C2 is MSCongruence of A
proof
let C1,C2 be MSCongruence of A;
reconsider C = C1 "\/" C2 as MSEquivalence_Relation-like ManySortedRelation
of the Sorts of A;
reconsider C as ManySortedRelation of A;
reconsider C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
for o be OperSymbol of S, x,y be Element of Args(o,A) st (for n be 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) by Th14;
hence thesis by MSUALG_4:def 4;
end;
theorem Th16:
for C1,C2 being MSCongruence of A holds C1 (/\) C2 is MSCongruence of A
proof
let C1,C2 be MSCongruence of A;
reconsider C = C1 (/\) C2 as Equivalence_Relation of the Sorts of A by Th11;
reconsider C as MSEquivalence_Relation-like ManySortedRelation of the Sorts
of A;
reconsider C as ManySortedRelation of A;
reconsider C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
for o be OperSymbol of S, x,y be Element of Args(o,A) st (for n be 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
let o be OperSymbol of S;
let x,y be Element of Args(o,A) such that
A1: for n be Nat st n in dom x holds [x.n,y.n] in C.((the_arity_of o) /.n);
for n be Nat st n in dom x holds [x.n,y.n] in C1.((the_arity_of o)/.n)
proof
let n be Nat;
assume n in dom x;
then [x.n,y.n] in C.((the_arity_of o)/.n) by A1;
then
[x.n,y.n] in C1.((the_arity_of o)/.n) /\ C2.((the_arity_of o)/.n) by
PBOOLE:def 5;
hence thesis by XBOOLE_0:def 4;
end;
then
A2: [Den(o,A).x,Den(o,A).y] in C1.(the_result_sort_of o) by MSUALG_4:def 4;
for n be Nat st n in dom x holds [x.n,y.n] in C2.((the_arity_of o)/.n)
proof
let n be Nat;
assume n in dom x;
then [x.n,y.n] in C.((the_arity_of o)/.n) by A1;
then [x.n,y.n] in C1.((the_arity_of o)/.n) /\ C2.((the_arity_of o)/.n)
by PBOOLE:def 5;
hence thesis by XBOOLE_0:def 4;
end;
then
A3: [Den(o,A).x,Den(o,A).y] in C2.(the_result_sort_of o) by MSUALG_4:def 4;
C1.(the_result_sort_of o) /\ C2.(the_result_sort_of o) = C.(
the_result_sort_of o) by PBOOLE:def 5;
hence thesis by A2,A3,XBOOLE_0:def 4;
end;
hence thesis by MSUALG_4:def 4;
end;
definition
let S;
let A be non-empty MSAlgebra over S;
func CongrLatt A -> strict SubLattice of EqRelLatt the Sorts of A means
:
Def6: for
x being set holds x in the carrier of it iff x is MSCongruence of A;
existence
proof
set D = the carrier of EqRelLatt the Sorts of A;
set f = the MSCongruence of A;
defpred P[object] means $1 is MSCongruence of A;
deffunc F(Element of S) = bool [:(the Sorts of A).$1,(the Sorts of A).$1:];
consider M2 being ManySortedSet of (the carrier of S) such that
A1: for i be Element of (the carrier of S) holds M2.i =F(i) from
PBOOLE:sch 5;
consider B be set such that
A2: for x being object holds x in B iff x in product M2 & P[x] from
XBOOLE_0:sch 1;
A3: for C1 be MSCongruence of A holds C1 in product M2
proof
let C1 be MSCongruence of A;
A4: now
let x be object;
assume x in dom M2;
then reconsider x9 = x as Element of (the carrier of S);
A5: C1.x9 is Subset of [:(the Sorts of A).x9,(the Sorts of A).x9:];
M2.x9 = bool [:(the Sorts of A).x9,(the Sorts of A).x9:] by A1;
hence C1.x in M2.x by A5;
end;
dom C1 = the carrier of S by PARTFUN1:def 2
.= dom M2 by PARTFUN1:def 2;
hence thesis by A4,CARD_3:9;
end;
A6: for x being set holds x in B iff x is MSCongruence of A
by A2,A3;
then f in B;
then reconsider B as non empty set;
set B1 = (the L_join of (EqRelLatt the Sorts of A))||B;
set B2 = (the L_meet of (EqRelLatt the Sorts of A))||B;
now
let x be object;
assume x in B;
then x is MSCongruence of A by A6;
hence x in the carrier of EqRelLatt the Sorts of A by Def5;
end;
then
A7: B c= D by TARSKI:def 3;
then [:B,B:] c= [:D,D:] by ZFMISC_1:96;
then reconsider B1,B2 as Function of [:B,B:],D by FUNCT_2:32;
A8: dom B2 = [:B,B:] by FUNCT_2:def 1;
now
let x be object;
assume
A9: x in [:B,B:];
then consider x1,x2 be object such that
A10: x = [x1,x2] by RELAT_1:def 1;
A11: x2 in B by A9,A10,ZFMISC_1:87;
x1 in B by A9,A10,ZFMISC_1:87;
then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6,A11;
A12: x29 in B by A6;
x19 in B by A6;
then [x1,x2] in [:B,B:] by A12,ZFMISC_1:87;
then B2.x = (the L_meet of (EqRelLatt the Sorts of A)).(x1,x2) by A10,
FUNCT_1:49
.= x19 (/\) x29 by Def5;
then B2.x is MSCongruence of A by Th16;
hence B2.x in B by A6;
end;
then reconsider B2 as BinOp of B by A8,FUNCT_2:3;
A13: dom B1 = [:B,B:] by FUNCT_2:def 1;
now
let x be object;
assume
A14: x in [:B,B:];
then consider x1,x2 be object such that
A15: x = [x1,x2] by RELAT_1:def 1;
A16: x2 in B by A14,A15,ZFMISC_1:87;
x1 in B by A14,A15,ZFMISC_1:87;
then reconsider x19 = x1, x29 = x2 as MSCongruence of A by A6,A16;
A17: x29 in B by A6;
x19 in B by A6;
then [x1,x2] in [:B,B:] by A17,ZFMISC_1:87;
then B1.x = (the L_join of EqRelLatt the Sorts of A).(x1,x2) by A15,
FUNCT_1:49
.= x19 "\/" x29 by Def5;
then B1.x is MSCongruence of A by Th15;
hence B1.x in B by A6;
end;
then reconsider B1 as BinOp of B by A13,FUNCT_2:3;
reconsider L = LattStr (# B,B1,B2 #) as non empty LattStr;
A18: for a,b being MSCongruence of A holds B1.(a,b) = a "\/" b & B2.(a,b)
= a (/\) b
proof
let a,b be MSCongruence of A;
A19: b in B by A6;
a in B by A6;
then
A20: [a,b] in [:B,B:] by A19,ZFMISC_1:87;
hence B1.(a,b) = (the L_join of (EqRelLatt the Sorts of A)).(a,b) by
FUNCT_1:49
.= a "\/" b by Def5;
thus B2.(a,b) = (the L_meet of (EqRelLatt the Sorts of A)).(a,b) by A20,
FUNCT_1:49
.= a (/\) b by Def5;
end;
A21: now
let a,b be Element of B;
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
thus B1.(a,b) = a9 "\/" b9 by A18
.= B1.(b,a) by A18;
end;
A22: for a,b being Element of L holds a"\/"b = b"\/"a
proof
let a,b be Element of L;
thus a"\/"b = B1.(a,b) by LATTICES:def 1
.= (the L_join of L).(b,a) by A21
.= b"\/"a by LATTICES:def 1;
end;
A23: now
let a,b,c be Element of B;
reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;
reconsider e1 = b9 (/\) c9 as MSCongruence of A by Th16;
reconsider e2 = a9 (/\) b9 as MSCongruence of A by Th16;
thus B2.(a,B2.(b,c)) = B2.(a,e1) by A18
.= a9 (/\) (b9 (/\) c9) by A18
.= (a9 (/\) b9) (/\) c9 by PBOOLE:29
.= B2.(e2,c) by A18
.= B2.(B2.(a,b),c) by A18;
end;
A24: for a,b,c being Element of L holds a"/\"(b"/\"c) = (a"/\"b)"/\"c
proof
let a,b,c be Element of L;
thus a"/\"(b"/\"c) = (the L_meet of L).(a,(b"/\"c)) by LATTICES:def 2
.= B2.(a,B2.(b,c)) by LATTICES:def 2
.= (the L_meet of L).((the L_meet of L).(a,b),c) by A23
.= (the L_meet of L).(a"/\"b,c) by LATTICES:def 2
.= (a"/\"b)"/\"c by LATTICES:def 2;
end;
A25: now
let a,b,c be Element of B;
reconsider a9 = a, b9 = b, c9 = c as MSCongruence of A by A6;
reconsider d = b9 "\/" c9 as MSCongruence of A by Th15;
reconsider e = a9 "\/" b9 as MSCongruence of A by Th15;
thus B1.(a,B1.(b,c)) = B1.(a,d) by A18
.= a9 "\/" (b9 "\/" c9) by A18
.= (a9 "\/" b9) "\/" c9 by Th8
.= B1.(e,c) by A18
.= B1.(B1.(a,b),c) by A18;
end;
A26: for a,b,c being Element of L holds a"\/"(b"\/"c) = (a"\/"b)"\/"c
proof
let a,b,c be Element of L;
thus a"\/"(b"\/"c) = (the L_join of L).(a,(b"\/"c)) by LATTICES:def 1
.= B1.(a,B1.(b,c)) by LATTICES:def 1
.= (the L_join of L).((the L_join of L).(a,b),c) by A25
.= (the L_join of L).(a"\/"b,c) by LATTICES:def 1
.= (a"\/"b)"\/"c by LATTICES:def 1;
end;
A27: now
let a,b be Element of B;
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
thus B2.(a,b) = b9 (/\) a9 by A18
.= B2.(b,a) by A18;
end;
A28: for a,b being Element of L holds a"/\"b = b"/\"a
proof
let a,b be Element of L;
thus a"/\"b = B2.(a,b) by LATTICES:def 2
.= (the L_meet of L).(b,a) by A27
.= b"/\"a by LATTICES:def 2;
end;
A29: for a,b being Element of L holds a"/\"(a"\/"b)=a
proof
let a,b be Element of L;
A30: B2.(a,B1.(a,b))= a
proof
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
reconsider d = a9 "\/" b9 as MSCongruence of A by Th15;
thus B2.(a,B1.(a,b)) = B2.(a, d) by A18
.= (a9 (/\) ( a9 "\/" b9)) by A18
.= a by Th9;
end;
thus a"/\"(a"\/"b) = (the L_meet of L).(a,(a"\/"b)) by LATTICES:def 2
.= a by A30,LATTICES:def 1;
end;
for a,b being Element of L holds (a"/\"b)"\/"b = b
proof
let a,b be Element of L;
A31: B1.(B2.(a,b),b)= b
proof
reconsider a9 = a, b9 = b as MSCongruence of A by A6;
reconsider EQR = a9 (/\) b9 as MSCongruence of A by Th16;
thus B1.(B2.(a,b),b) = B1.(a9 (/\) b9,b9) by A18
.= EQR "\/" b9 by A18
.= b by Th10;
end;
thus (a"/\"b)"\/"b = (the L_join of L).((a"/\"b),b) by LATTICES:def 1
.= b by A31,LATTICES:def 2;
end;
then L is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A22,A26,A28,A24,A29,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
then reconsider L as Lattice;
reconsider L as strict SubLattice of EqRelLatt the Sorts of A by A7,
NAT_LAT:def 12;
take L;
thus thesis by A6;
end;
uniqueness
proof
let C1,C2 be strict SubLattice of EqRelLatt the Sorts of A such that
A32: for x being set holds x in the carrier of C1 iff x is
MSCongruence of A and
A33: for x being set holds x in the carrier of C2 iff x is MSCongruence of A;
A34: now
let x be object;
x in the carrier of C2 iff x is MSCongruence of A by A33;
hence x in the carrier of C1 iff x in the carrier of C2 by A32;
end;
then
A35: the carrier of C1 = the carrier of C2 by TARSKI:2;
then
A36: the L_join of C1 = (the L_join of EqRelLatt the Sorts of A)||the
carrier of C2 by NAT_LAT:def 12
.= the L_join of C2 by NAT_LAT:def 12;
the L_meet of C1 = (the L_meet of EqRelLatt the Sorts of A)||the
carrier of C2 by A35,NAT_LAT:def 12
.= the L_meet of C2 by NAT_LAT:def 12;
hence thesis by A34,A36,TARSKI:2;
end;
end;
theorem Th17:
id (the Sorts of A) is MSCongruence of A
proof
set J = id (the Sorts of A);
for i be set st i in the carrier of S holds J.i is Relation of (the
Sorts of A).i
proof
let i be set;
assume i in the carrier of S;
then J.i = id ((the Sorts of A).i) by MSUALG_3:def 1;
hence thesis;
end;
then reconsider J as ManySortedRelation of the Sorts of A by MSUALG_4:def 1;
for i be object, R be Relation of (the Sorts of A).i st i in the carrier of
S & J.i = R holds R is Equivalence_Relation of (the Sorts of A).i
proof
let i be object;
let R be Relation of (the Sorts of A).i;
assume that
A1: i in the carrier of S and
A2: J.i = R;
J.i = id ((the Sorts of A).i) by A1,MSUALG_3:def 1;
hence thesis by A2;
end;
then reconsider
J as MSEquivalence_Relation-like ManySortedRelation of the Sorts
of A by MSUALG_4:def 2;
reconsider J as ManySortedRelation of A;
reconsider J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
for o be OperSymbol of S, x,y be Element of Args(o,A) st (for n be Nat
st n in dom x holds [x.n,y.n] in J.((the_arity_of o)/.n)) holds [Den(o,A).x,Den
(o,A).y] in J.(the_result_sort_of o)
proof
let o be OperSymbol of S;
let x,y be Element of Args(o,A) such that
A3: for n be Nat st n in dom x holds [x.n,y.n] in J.((the_arity_of o) /.n);
A4: dom y = dom (the_arity_of o) by MSUALG_3:6
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
A5: dom x = dom (the_arity_of o) by MSUALG_3:6
.= Seg len (the_arity_of o) by FINSEQ_1:def 3;
then reconsider x9 = x, y9 = y as FinSequence by A4,FINSEQ_1:def 2;
now
let n be Nat such that
A6: n in dom x;
J.((the_arity_of o)/.n) = id ((the Sorts of A).((the_arity_of o)/.n
) ) by MSUALG_3:def 1;
then [x.n,y.n] in id ((the Sorts of A).((the_arity_of o)/.n)) by A3,A6;
hence x9.n = y9.n by RELAT_1:def 10;
end;
then
A7: x = y by A5,A4,FINSEQ_1:13;
Den(o,A).x in Result(o,A);
then
A8: Den(o,A).x in ((the Sorts of A) * the ResultSort of S).o by MSUALG_1:def 5;
o in the carrier' of S;
then o in dom (the ResultSort of S) by FUNCT_2:def 1;
then Den(o,A).x in (the Sorts of A).((the ResultSort of S).o) by A8,
FUNCT_1:13;
then
A9: Den(o,A).x in (the Sorts of A).(the_result_sort_of o) by MSUALG_1:def 2;
J.(the_result_sort_of o) = id ((the Sorts of A).(the_result_sort_of o
) ) by MSUALG_3:def 1;
hence thesis by A7,A9,RELAT_1:def 10;
end;
hence thesis by MSUALG_4:def 4;
end;
theorem Th18:
[|the Sorts of A,the Sorts of A|] is MSCongruence of A
proof
set J = [|the Sorts of A,the Sorts of A|];
for i be set st i in the carrier of S holds J.i is Relation of (the
Sorts of A).i
proof
let i be set;
assume i in the carrier of S;
then J.i c= [:(the Sorts of A).i,(the Sorts of A).i:] by PBOOLE:def 16;
hence thesis;
end;
then reconsider J as ManySortedRelation of the Sorts of A by MSUALG_4:def 1;
for i be object, R be Relation of (the Sorts of A).i st i in the carrier of
S & J.i = R holds R is Equivalence_Relation of (the Sorts of A).i
proof
let i be object;
let R be Relation of (the Sorts of A).i;
assume that
A1: i in the carrier of S and
A2: J.i = R;
J.i = nabla (the Sorts of A).i by A1,PBOOLE:def 16;
hence thesis by A2;
end;
then reconsider
J as MSEquivalence_Relation-like ManySortedRelation of the Sorts
of A by MSUALG_4:def 2;
reconsider J as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
for o be OperSymbol of S, x,y be Element of Args(o,A) st (for n be Nat
st n in dom x holds [x.n,y.n] in J.((the_arity_of o)/.n)) holds [Den(o,A).x,Den
(o,A).y] in J.(the_result_sort_of o)
proof
let o be OperSymbol of S;
let x,y be Element of Args(o,A) such that
for n be Nat st n in dom x holds [x.n,y.n] in J.((the_arity_of o)/.n);
o in the carrier' of S;
then
A3: o in dom (the ResultSort of S) by FUNCT_2:def 1;
Den(o,A).y in Result(o,A);
then Den(o,A).y in ((the Sorts of A) * the ResultSort of S).o by
MSUALG_1:def 5;
then Den(o,A).y in (the Sorts of A).((the ResultSort of S).o) by A3,
FUNCT_1:13;
then
A4: Den(o,A).y in (the Sorts of A).(the_result_sort_of o) by MSUALG_1:def 2;
Den(o,A).x in Result(o,A);
then Den(o,A).x in ((the Sorts of A) * the ResultSort of S).o by
MSUALG_1:def 5;
then Den(o,A).x in (the Sorts of A).((the ResultSort of S).o) by A3,
FUNCT_1:13;
then
A5: Den(o,A).x in (the Sorts of A).(the_result_sort_of o) by MSUALG_1:def 2;
J.(the_result_sort_of o) = [:(the Sorts of A).(the_result_sort_of o),
(the Sorts of A).(the_result_sort_of o):] by PBOOLE:def 16;
hence thesis by A5,A4,ZFMISC_1:87;
end;
hence thesis by MSUALG_4:def 4;
end;
registration
let S, A;
cluster CongrLatt A -> bounded;
coherence
proof
ex c being Element of CongrLatt A st for a being Element of CongrLatt
A holds c"\/"a = c & a"\/"c = c
proof
reconsider c9 = [|the Sorts of A,the Sorts of A|] as MSCongruence of A
by Th18;
A1: the L_join of CongrLatt A = (the L_join of EqRelLatt the Sorts of A)
||the carrier of CongrLatt A by NAT_LAT:def 12;
reconsider c = c9 as Element of CongrLatt A by Def6;
take c;
let a be Element of CongrLatt A;
A2: [c,a] in [:the carrier of CongrLatt A,the carrier of CongrLatt A:]
by ZFMISC_1:87;
reconsider a9 = a as MSCongruence of A by Def6;
A3: now
let i be object;
assume
A4: i in the carrier of S;
then reconsider i9 = i as Element of S;
A5: ex K1 be ManySortedRelation of the Sorts of A st K1 = c9 (\/) a9 &
c9 "\/" a9 = EqCl K1 by Def4;
reconsider K2 = c9.i9, a2 = a9.i9 as Equivalence_Relation of (the
Sorts of A).i;
(c9 (\/) a9).i = c9.i \/ a9.i by A4,PBOOLE:def 4
.= nabla (the Sorts of A).i \/ a2 by PBOOLE:def 16
.= nabla (the Sorts of A).i by EQREL_1:1
.= c9.i by A4,PBOOLE:def 16;
hence (c9 "\/" a9).i = EqCl K2 by A5,Def3
.= c9.i by Th2;
end;
thus c"\/"a = (the L_join of CongrLatt A).(c,a) by LATTICES:def 1
.= (the L_join of EqRelLatt the Sorts of A).(c,a) by A1,A2,FUNCT_1:49
.= c9 "\/" a9 by Def5
.= c by A3,PBOOLE:3;
hence thesis;
end;
then
A6: CongrLatt A is upper-bounded by LATTICES:def 14;
ex c being Element of CongrLatt A st for a being Element of CongrLatt
A holds c"/\"a = c & a"/\"c = c
proof
reconsider c9 = id (the Sorts of A) as MSCongruence of A by Th17;
A7: the L_meet of CongrLatt A = (the L_meet of EqRelLatt the Sorts of A)
||the carrier of CongrLatt A by NAT_LAT:def 12;
reconsider c = c9 as Element of CongrLatt A by Def6;
take c;
let a be Element of CongrLatt A;
A8: [c,a] in [:the carrier of CongrLatt A,the carrier of CongrLatt A:]
by ZFMISC_1:87;
reconsider a9 = a as MSCongruence of A by Def6;
A9: now
let i be object;
assume
A10: i in the carrier of S;
then reconsider i9 = i as Element of S;
reconsider a2 = a9.i9 as Equivalence_Relation of (the Sorts of A).i;
thus (c9 (/\) a9).i = c9.i /\ a9.i by A10,PBOOLE:def 5
.= id ((the Sorts of A).i) /\ a2 by MSUALG_3:def 1
.= id ((the Sorts of A).i) by EQREL_1:10
.= c9.i by A10,MSUALG_3:def 1;
end;
thus c"/\"a = (the L_meet of CongrLatt A).(c,a) by LATTICES:def 2
.= (the L_meet of EqRelLatt the Sorts of A).(c,a) by A7,A8,FUNCT_1:49
.= c9 (/\) a9 by Def5
.= c by A9,PBOOLE:3;
hence thesis;
end;
then CongrLatt A is lower-bounded by LATTICES:def 13;
hence thesis by A6;
end;
end;
theorem
Bottom CongrLatt A = id (the Sorts of A)
proof
set K = id (the Sorts of A);
K is MSCongruence of A by Th17;
then reconsider K as Element of CongrLatt A by Def6;
A1: the L_meet of CongrLatt A = (the L_meet of EqRelLatt the Sorts of A)||
the carrier of CongrLatt A by NAT_LAT:def 12;
now
let a be Element of CongrLatt A;
reconsider K9 = K, a9 = a as Equivalence_Relation of the Sorts of A by Def6
;
A2: [K,a] in [:the carrier of CongrLatt A,the carrier of CongrLatt A:] by
ZFMISC_1:87;
A3: now
let i be object;
assume
A4: i in the carrier of S;
then reconsider i9 = i as Element of S;
reconsider a2 = a9.i9 as Equivalence_Relation of (the Sorts of A).i by
MSUALG_4:def 2;
thus (K9 (/\) a9).i = K9.i /\ a9.i by A4,PBOOLE:def 5
.= id ((the Sorts of A).i) /\ a2 by MSUALG_3:def 1
.= id ((the Sorts of A).i) by EQREL_1:10
.= K9.i by A4,MSUALG_3:def 1;
end;
thus K "/\" a = (the L_meet of CongrLatt A).(K,a) by LATTICES:def 2
.= (the L_meet of EqRelLatt the Sorts of A).(K,a) by A1,A2,FUNCT_1:49
.= K9 (/\) a9 by Def5
.= K by A3,PBOOLE:3;
hence a "/\" K = K;
end;
hence thesis by LATTICES:def 16;
end;
theorem
Top CongrLatt A = [|the Sorts of A,the Sorts of A|]
proof
set K = [|the Sorts of A,the Sorts of A|];
K is MSCongruence of A by Th18;
then reconsider K as Element of CongrLatt A by Def6;
A1: the L_join of CongrLatt A = (the L_join of EqRelLatt the Sorts of A)||
the carrier of CongrLatt A by NAT_LAT:def 12;
now
let a be Element of CongrLatt A;
reconsider K9 = K, a9 = a as Equivalence_Relation of the Sorts of A by Def6
;
A2: [K,a] in [:the carrier of CongrLatt A,the carrier of CongrLatt A:] by
ZFMISC_1:87;
A3: now
let i be object;
assume
A4: i in the carrier of S;
then reconsider i9 = i as Element of S;
A5: ex K1 be ManySortedRelation of the Sorts of A st K1 = K9 (\/) a9 &
K9 "\/" a9 = EqCl K1 by Def4;
reconsider K2 = K9.i9, a2 = a9.i9 as Equivalence_Relation of (the Sorts
of A).i by MSUALG_4:def 2;
(K9 (\/) a9).i = K9.i \/ a9.i by A4,PBOOLE:def 4
.= nabla (the Sorts of A).i \/ a2 by PBOOLE:def 16
.= nabla (the Sorts of A).i by EQREL_1:1
.= K9.i by A4,PBOOLE:def 16;
hence (K9 "\/" a9).i = EqCl K2 by A5,Def3
.= K9.i by Th2;
end;
thus K "\/" a = (the L_join of CongrLatt A).(K,a) by LATTICES:def 1
.= (the L_join of EqRelLatt the Sorts of A).(K,a) by A1,A2,FUNCT_1:49
.= K9 "\/" a9 by Def5
.= K by A3,PBOOLE:3;
hence a "\/" K = K;
end;
hence thesis by LATTICES:def 17;
end;
:: from MSUALG_7, 2010.02.21, A.T
theorem
for X be set holds x in the carrier of EqRelLatt X iff x is
Equivalence_Relation of X
proof
let X be set;
A1: the carrier of EqRelLatt X = { x1 where x1 is Relation of X,X : x1 is
Equivalence_Relation of X } by Def2;
thus x in the carrier of EqRelLatt X implies x is Equivalence_Relation of X
proof
assume x in the carrier of EqRelLatt X;
then
ex x1 be Relation of X,X st x = x1 & x1 is Equivalence_Relation of X by A1;
hence thesis;
end;
thus thesis by A1;
end;