:: Subalgebras of the Universal Algebra. Lattices of Subalgebras
:: by Ewa Burakowska
::
:: Received July 8, 1993
:: Copyright (c) 1993-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 NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_2, TARSKI, UNIALG_1, FUNCT_2,
PARTFUN1, RELAT_1, FINSEQ_1, FUNCOP_1, STRUCT_0, CQC_SIM1, FUNCT_1,
CARD_1, ZFMISC_1, SETFAM_1, EQREL_1, BINOP_1, LATTICES, UNIALG_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1,
STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, SETFAM_1, FUNCOP_1, PARTFUN1,
FINSEQ_2, LATTICES, BINOP_1, UNIALG_1, MARGREL1;
constructors SETFAM_1, BINOP_1, DOMAIN_1, FUNCOP_1, LATTICES, UNIALG_1,
MARGREL1, FINSEQ_2, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, PARTFUN1, FINSEQ_2, STRUCT_0,
LATTICES, UNIALG_1, ORDINAL1, FINSEQ_1, CARD_1, MARGREL1;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, XBOOLE_0, MARGREL1;
equalities SUBSET_1, FUNCOP_1;
expansions TARSKI, XBOOLE_0, MARGREL1;
theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, UNIALG_1, ZFMISC_1,
SETFAM_1, FUNCOP_1, BINOP_1, LATTICES, FINSEQ_3, RELAT_1, RELSET_1,
XBOOLE_0, XBOOLE_1, MARGREL1;
schemes FINSEQ_1, BINOP_1, XFAMILY;
begin
reserve U0,U1,U2,U3 for Universal_Algebra,
n for Nat,
x,y for set;
definition
let U1;
mode PFuncsDomHQN of U1 is PFuncsDomHQN of (the carrier of U1);
end;
definition
let U1 be UAStr;
mode PartFunc of U1 is PartFunc of (the carrier of U1)*,the carrier of U1;
end;
definition
let U1,U2;
pred U1,U2 are_similar means
signature (U1) = signature (U2);
symmetry;
reflexivity;
end;
theorem
U1,U2 are_similar implies len the charact of(U1) = len the charact of( U2)
proof
A1: len signature (U1) = len the charact of(U1) & len signature (U2) = len
the charact of(U2) by UNIALG_1:def 4;
assume U1,U2 are_similar;
hence thesis by A1;
end;
theorem
U1,U2 are_similar & U2,U3 are_similar implies U1,U3 are_similar;
theorem
rng the charact of(U0) is non empty Subset of PFuncs((the carrier of
U0)*,the carrier of U0) by FINSEQ_1:def 4,RELAT_1:41;
definition
let U0;
func Operations(U0) -> PFuncsDomHQN of U0 equals
rng the charact of(U0);
coherence
proof
reconsider A=rng the charact of(U0) as non empty set by RELAT_1:41;
now
let x be Element of A;
consider i being Nat such that
A1: i in dom(the charact of(U0)) and
A2: (the charact of(U0)).i = x by FINSEQ_2:10;
reconsider p = (the charact of U0).i as PartFunc of U0;
p is homogeneous quasi_total non empty by A1,FUNCT_1:def 9
,MARGREL1:def 24;
hence x is homogeneous quasi_total non empty PartFunc of U0 by A2;
end;
hence thesis by MARGREL1:def 26;
end;
end;
definition
let U1;
mode operation of U1 is Element of Operations(U1);
end;
reserve A for non empty Subset of U0,
o for operation of U0,
x1,y1 for FinSequence of A;
definition
let U0 be Universal_Algebra, A be Subset of U0, o be operation of U0;
pred A is_closed_on o means
for s being FinSequence of A st len s = arity o holds o.s in A;
end;
definition
let U0 be Universal_Algebra, A be Subset of U0;
attr A is opers_closed means
for o be operation of U0 holds A is_closed_on o;
end;
definition
let U0,A,o;
assume
A1: A is_closed_on o;
func o/.A ->homogeneous quasi_total non empty PartFunc of A*,A equals
:Def5:
o|((arity o)-tuples_on A);
coherence
proof
A2: (arity o)-tuples_on A c= (arity o)-tuples_on the carrier of U0
proof
let x be object;
assume x in (arity o)-tuples_on A;
then x in { s where s is Element of A* : len s =arity o} by
FINSEQ_2:def 4;
then consider s be Element of A* such that
A3: x = s and
A4: len s = arity o;
rng s c= A by FINSEQ_1:def 4;
then rng s c= the carrier of U0 by XBOOLE_1:1;
then reconsider s as FinSequence of the carrier of U0 by FINSEQ_1:def 4;
reconsider s as Element of (the carrier of U0)* by FINSEQ_1:def 11;
x=s by A3;
then
x in { s1 where s1 is Element of(the carrier of U0)*: len s1 =arity
o} by A4;
hence thesis by FINSEQ_2:def 4;
end;
A5: dom ( o|((arity o)-tuples_on A))= (dom o) /\ ((arity o)-tuples_on A)
by RELAT_1:61
.=((arity o)-tuples_on the carrier of U0) /\ ((arity o)-tuples_on A)
by MARGREL1:22
.=(arity o)-tuples_on A by A2,XBOOLE_1:28;
A6: rng (o|((arity o)-tuples_on A)) c= A
proof
let x be object;
assume x in rng( o|((arity o)-tuples_on A));
then consider y being object such that
A7: y in dom ( o|((arity o)-tuples_on A)) and
A8: x = (o|((arity o)-tuples_on A)).y by FUNCT_1:def 3;
y in { s where s is Element of A* : len s =arity o} by A5,A7,
FINSEQ_2:def 4;
then consider s be Element of A* such that
A9: y = s and
A10: len s = arity o;
(o|((arity o)-tuples_on A)).s = o.s by A7,A9,FUNCT_1:47;
hence thesis by A1,A8,A9,A10;
end;
(arity o)-tuples_on A in the set of all i-tuples_on A where i is Nat;
then (arity o)-tuples_on A c=
union the set of all i-tuples_on A where i is Nat by ZFMISC_1:74;
then dom ( o|((arity o)-tuples_on A)) c= A* by A5,FINSEQ_2:108;
then reconsider oa = o|((arity o)-tuples_on A) as PartFunc of A*,A by A6,
RELSET_1:4;
A11: oa is homogeneous
proof
let x1,y1 be FinSequence;
assume that
A12: x1 in dom oa and
A13: y1 in dom oa;
y1 in { s1 where s1 is Element of A* : len s1=arity o} by A5,A13,
FINSEQ_2:def 4;
then
A14: ex s1 be Element of A* st y1=s1 & len s1 = arity o;
x1 in { s where s is Element of A* : len s =arity o} by A5,A12,
FINSEQ_2:def 4;
then ex s be Element of A* st x1 = s & len s = arity o;
hence thesis by A14;
end;
oa is quasi_total
proof
let x1,y1;
assume that
A15: len x1 = len y1 and
A16: x1 in dom oa;
x1 in { s where s is Element of A* : len s =arity o} by A5,A16,
FINSEQ_2:def 4;
then ex s be Element of A* st x1 = s & len s = arity o;
then y1 is Element of (arity o)-tuples_on A by A15,FINSEQ_2:92;
hence thesis by A5;
end;
hence thesis by A5,A11;
end;
end;
definition
let U0,A;
func Opers(U0,A) -> PFuncFinSequence of A means
:Def6:
dom it = dom the
charact of(U0) & for n being set,o st n in dom it & o =(the charact of(U0)).n
holds it.n = o/.A;
existence
proof
defpred P[Nat,set] means for o st o =(the charact of(U0)).$1 holds $2 = o
/.A;
A1: for n being Nat st n in Seg len the charact of(U0) ex x being Element
of PFuncs(A*,A) st P[n,x]
proof
let n be Nat;
assume n in Seg len the charact of(U0);
then n in dom the charact of(U0) by FINSEQ_1:def 3;
then reconsider o1 =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
reconsider x = o1/.A as Element of PFuncs(A*,A) by PARTFUN1:45;
take x;
let o;
assume o = (the charact of(U0)).n;
hence thesis;
end;
consider p being FinSequence of PFuncs(A*,A) such that
A2: dom p = Seg len the charact of(U0) and
A3: for n being Nat st n in Seg len the charact of(U0) holds P[n,p.n]
from FINSEQ_1:sch 5(A1);
reconsider p as PFuncFinSequence of A;
take p;
thus dom p =dom the charact of(U0) by A2,FINSEQ_1:def 3;
let n be set,o;
assume n in dom p & o =(the charact of(U0)).n;
hence thesis by A2,A3;
end;
uniqueness
proof
let p1,p2 be PFuncFinSequence of A;
assume that
A4: dom p1 = dom the charact of(U0) and
A5: for n being set,o st n in dom p1 & o = (the charact of(U0)).n
holds p1.n = o/.A and
A6: dom p2 = dom the charact of(U0) and
A7: for n being set,o st n in dom p2 & o = (the charact of(U0)).n
holds p2.n = o/.A;
for n be Nat st n in dom the charact of(U0) holds p1.n = p2.n
proof
let n be Nat;
assume
A8: n in dom the charact of(U0);
then reconsider k =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
p1.n =k/.A by A4,A5,A8;
hence thesis by A6,A7,A8;
end;
hence thesis by A4,A6,FINSEQ_1:13;
end;
end;
theorem Th4:
for B being non empty Subset of U0 st B=the carrier of U0 holds B
is opers_closed & for o holds o/.B = o
proof
let B be non empty Subset of U0;
assume
A1: B=the carrier of U0;
A2: for o holds B is_closed_on o
proof
let o;
let s be FinSequence of B;
assume
A3: len s = arity o;
dom o = (arity o)-tuples_on B & s is Element of (len s)-tuples_on B by A1,
FINSEQ_2:92,MARGREL1:22;
then
A4: o.s in rng o by A3,FUNCT_1:def 3;
rng o c= B by A1,RELAT_1:def 19;
hence thesis by A4;
end;
for o holds o/.B = o
proof
let o;
dom o = (arity(o))-tuples_on B & o/.B =o|((arity(o))-tuples_on B) by A1,A2
,Def5,MARGREL1:22;
hence thesis by RELAT_1:68;
end;
hence thesis by A2;
end;
theorem
for U1 be Universal_Algebra, A be non empty Subset of U1, o be
operation of U1 st A is_closed_on o holds arity (o/.A) = arity o
proof
let U1 be Universal_Algebra, A be non empty Subset of U1, o be operation of
U1;
assume A is_closed_on o;
then o/.A =o|((arity o)-tuples_on A) by Def5;
then dom (o/.A) = dom o /\ ((arity o)-tuples_on A) by RELAT_1:61;
then
A1: dom (o/.A) = ((arity o)-tuples_on the carrier of U1) /\ ((arity o)
-tuples_on A) by MARGREL1:22
.= (arity o)-tuples_on A by MARGREL1:21;
dom (o/.A)=(arity (o/.A))-tuples_on A by MARGREL1:22;
hence thesis by A1,FINSEQ_2:110;
end;
definition
let U0;
mode SubAlgebra of U0 -> Universal_Algebra means
:Def7:
the carrier of it is
Subset of U0 & for B be non empty Subset of U0 st B=the carrier of it holds the
charact of it = Opers(U0,B) & B is opers_closed;
existence
proof
take U1=U0;
A1: for B be non empty Subset of U0 st B=the carrier of U0 holds the
charact of(U0) = Opers(U0,B) & B is opers_closed
proof
let B be non empty Subset of U0;
assume
A2: B =the carrier of U0;
A3: dom the charact of(U0) = dom Opers(U0,B) by Def6;
for n be Nat st n in dom the charact of(U0) holds (the charact of(U0
)).n = (Opers(U0,B)).n
proof
let n be Nat;
assume
A4: n in dom the charact of(U0);
then reconsider o =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
(Opers(U0,B)).n = o/.B by A3,A4,Def6;
hence thesis by A2,Th4;
end;
hence thesis by A2,A3,Th4,FINSEQ_1:13;
end;
the carrier of U1 c= the carrier of U1;
hence thesis by A1;
end;
end;
registration
let U0 be Universal_Algebra;
cluster strict for SubAlgebra of U0;
existence
proof
reconsider S = UAStr(#the carrier of U0,the charact of U0#) as strict
Universal_Algebra by UNIALG_1:def 1,def 2,def 3;
A1: the carrier of S c= the carrier of U0;
for B be non empty Subset of U0 st B=the carrier of S holds the
charact of(S) = Opers(U0,B) & B is opers_closed
proof
let B be non empty Subset of U0;
assume
A2: B=the carrier of S;
A3: now
let n be Nat;
assume
A4: n in dom the charact of (U0);
then reconsider o = (the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
n in dom Opers(U0,B) by A4,Def6;
hence Opers (U0,B).n = o/.B by Def6
.= (the charact of(U0)).n by A2,Th4;
end;
dom the charact of(U0)= dom Opers(U0,B) by Def6;
hence thesis by A2,A3,Th4,FINSEQ_1:13;
end;
then reconsider S as SubAlgebra of U0 by A1,Def7;
take S;
thus thesis;
end;
end;
theorem Th6:
for U0,U1 be Universal_Algebra, o0 be operation of U0, o1 be
operation of U1, n be Nat st U0 is SubAlgebra of U1 & n in dom the charact of(
U0) & o0 = (the charact of(U0)).n & o1 = (the charact of(U1)).n holds arity o0
= arity o1
proof
let U0,U1 be Universal_Algebra, o0 be operation of U0, o1 be operation of U1
,n;
assume that
A1: U0 is SubAlgebra of U1 and
A2: n in dom the charact of(U0) & o0 = (the charact of(U0)).n and
A3: o1 = (the charact of(U1)).n;
reconsider A =the carrier of U0 as non empty Subset of U1 by A1,Def7;
A is opers_closed by A1,Def7;
then
A4: A is_closed_on o1;
n in dom Opers(U1,A) & o0 = Opers(U1,A).n by A1,A2,Def7;
then o0 = o1/.A by A3,Def6;
then o0 = o1|((arity o1)-tuples_on A) by A4,Def5;
then dom o0 = dom o1 /\ ((arity o1)-tuples_on A) by RELAT_1:61;
then
A5: dom o0 = ((arity o1)-tuples_on the carrier of U1) /\ ((arity o1)
-tuples_on A) by MARGREL1:22
.= (arity o1)-tuples_on A by MARGREL1:21;
dom o0 =(arity o0)-tuples_on A by MARGREL1:22;
hence thesis by A5,FINSEQ_2:110;
end;
theorem Th7:
U0 is SubAlgebra of U1 implies dom the charact of(U0)=dom the charact of(U1)
proof
assume
A1: U0 is SubAlgebra of U1;
then reconsider A =the carrier of U0 as non empty Subset of U1 by Def7;
the charact of(U0) = Opers(U1,A) by A1,Def7;
hence thesis by Def6;
end;
theorem
U0 is SubAlgebra of U0
proof
A1: for B be non empty Subset of U0 st B=the carrier of U0 holds the charact
of(U0) = Opers(U0,B) & B is opers_closed
proof
let B be non empty Subset of U0;
assume
A2: B =the carrier of U0;
A3: dom the charact of(U0) = dom Opers(U0,B) by Def6;
for n be Nat st n in dom the charact of(U0) holds (the charact of(U0))
.n = (Opers(U0,B)).n
proof
let n be Nat;
assume
A4: n in dom the charact of(U0);
then reconsider o =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
(Opers(U0,B)).n = o/.B by A3,A4,Def6;
hence thesis by A2,Th4;
end;
hence thesis by A2,A3,Th4,FINSEQ_1:13;
end;
the carrier of U0 c= the carrier of U0;
hence thesis by A1,Def7;
end;
theorem
U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 implies U0 is
SubAlgebra of U2
proof
assume that
A1: U0 is SubAlgebra of U1 and
A2: U1 is SubAlgebra of U2;
A3: the carrier of U0 is Subset of U1 by A1,Def7;
reconsider B2 = the carrier of U1 as non empty Subset of U2 by A2,Def7;
A4: the charact of(U1) = Opers(U2,B2) by A2,Def7;
the carrier of U1 is Subset of U2 by A2,Def7;
hence the carrier of U0 is Subset of U2 by A3,XBOOLE_1:1;
let B be non empty Subset of U2;
assume
A5: B = the carrier of U0;
reconsider B1 = the carrier of U0 as non empty Subset of U1 by A1,Def7;
A6: the charact of(U0) = Opers(U1,B1) by A1,Def7;
A7: B2 is opers_closed by A2,Def7;
A8: dom the charact of(U1)= dom Opers(U2,B2) by A2,Def7
.= dom the charact of(U2) by Def6;
A9: B1 is opers_closed by A1,Def7;
A10: now
let o2 be operation of U2;
consider n being Nat such that
A11: n in dom the charact of(U2) and
A12: (the charact of(U2)).n = o2 by FINSEQ_2:10;
A13: dom the charact of(U2) = dom Opers(U2,B2) by Def6;
then reconsider o21 = (the charact of(U1)).n as operation of U1 by A4,A11,
FUNCT_1:def 3;
A14: dom o21 = (arity o21)-tuples_on (the carrier of U1) by MARGREL1:22;
A15: dom the charact of(U1) = dom Opers(U1,B1) by Def6;
then reconsider
o20 = (the charact of(U0)).n as operation of U0 by A6,A4,A11,A13,
FUNCT_1:def 3;
A16: dom o20 = (arity o20)-tuples_on (the carrier of U0) by MARGREL1:22;
A17: dom o2 = (arity o2)-tuples_on (the carrier of U2) & dom(o2 | ((arity
o2) -tuples_on B2)) = dom o2 /\ ((arity o2)-tuples_on B2)
by MARGREL1:22,RELAT_1:61;
A18: B2 is_closed_on o2 by A7;
A19: o21 = o2/.B2 by A4,A11,A12,A13,Def6;
then o21 = o2 | ((arity o2)-tuples_on B2) by A18,Def5;
then
A20: arity o2 = arity o21 by A14,A17,FINSEQ_2:110,MARGREL1:21;
A21: B1 is_closed_on o21 by A9;
A22: o20 = o21 /. B1 by A6,A4,A11,A13,A15,Def6;
then o20 = o21 | ((arity o21)-tuples_on B1) by A21,Def5;
then (arity o20)-tuples_on B1 = (arity o21)-tuples_on (the carrier of U1)
/\ (arity o21)-tuples_on B1 by A16,A14,RELAT_1:61;
then
A23: arity o20 = arity o21 by FINSEQ_2:110,MARGREL1:21;
now
let s be FinSequence of B;
reconsider s1 = s as Element of B1* by A5,FINSEQ_1:def 11;
reconsider s0 = s as Element of (the carrier of U0)* by A5,
FINSEQ_1:def 11;
A24: rng o20 c= B by A5,RELAT_1:def 19;
rng s c= B by FINSEQ_1:def 4;
then rng s c= B2 by A3,A5,XBOOLE_1:1;
then s is FinSequence of B2 by FINSEQ_1:def 4;
then reconsider s2 = s as Element of B2* by FINSEQ_1:def 11;
assume
A25: len s = arity o2;
then s2 in {w where w is Element of B2*: len w = arity o2};
then
A26: s2 in (arity o2)-tuples_on B2 by FINSEQ_2:def 4;
s0 in {w where w is Element of (the carrier of U0)*: len w = arity
o20 } by A23,A20,A25;
then s0 in (arity o20)-tuples_on (the carrier of U0) by FINSEQ_2:def 4;
then
A27: o20.s0 in rng o20 by A16,FUNCT_1:def 3;
s1 in {w where w is Element of B1*: len w = arity o21} by A20,A25;
then
A28: s1 in (arity o21)-tuples_on B1 by FINSEQ_2:def 4;
o20.s0 = (o21 | (arity o21)-tuples_on B1).s1 by A21,A22,Def5
.= o21.s1 by A28,FUNCT_1:49
.= (o2 | (arity o2)-tuples_on B2).s2 by A18,A19,Def5
.= o2.s by A26,FUNCT_1:49;
hence o2.s in B by A27,A24;
end;
hence B is_closed_on o2;
end;
A29: dom the charact of(U0) = dom Opers(U1,B1) by A1,Def7
.= dom the charact of(U1) by Def6;
A30: dom the charact of(U2)= dom Opers(U2,B) by Def6;
A31: B = B1 by A5;
now
let n be Nat;
assume
A32: n in dom Opers(U2,B);
then reconsider o2 = (the charact of(U2)).n as operation of U2 by A30,
FUNCT_1:def 3;
reconsider o21 = (the charact of(U1)).n as operation of U1 by A8,A30,A32,
FUNCT_1:def 3;
A33: B2 is_closed_on o2 by A7;
A34: B1 is_closed_on o21 by A9;
thus Opers(U2,B).n = o2/.B by A32,Def6
.=o2|((arity o2)-tuples_on B) by A10,Def5
.=o2|((arity o2)-tuples_on B2 /\ (arity o2)-tuples_on B)
by A31,MARGREL1:21
.=(o2|((arity o2)-tuples_on B2))|((arity o2)-tuples_on B)by RELAT_1:71
.=(o2/.B2)|((arity o2)-tuples_on B) by A33,Def5
.=o21|((arity o2)-tuples_on B) by A4,A8,A30,A32,Def6
.=o21|((arity o21)-tuples_on B1) by A2,A5,A8,A30,A32,Th6
.=o21/.B1 by A34,Def5
.= (the charact of(U0)).n by A6,A29,A8,A30,A32,Def6;
end;
hence the charact of(U0) = Opers(U2,B) by A29,A8,A30,FINSEQ_1:13;
thus thesis by A10;
end;
theorem Th10:
U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 implies U1 = U2
proof
assume that
A1: U1 is strict SubAlgebra of U2 and
A2: U2 is strict SubAlgebra of U1;
reconsider B = the carrier of U1 as non empty Subset of U2 by A1,Def7;
the carrier of U2 c= the carrier of U2;
then reconsider B1 = the carrier of U2 as non empty Subset of U2;
A3: dom Opers(U2,B1) = dom the charact of (U2) by Def6;
A4: for n being Nat st n in dom the charact of(U2) holds (the charact of(U2)
).n = (Opers(U2,B1)).n
proof
let n be Nat;
assume
A5: n in dom the charact of(U2);
then reconsider o =(the charact of(U2)).n as operation of U2 by
FUNCT_1:def 3;
(Opers(U2,B1)).n = o/.B1 by A3,A5,Def6
.= o by Th4;
hence thesis;
end;
the carrier of U2 is Subset of U1 by A2,Def7;
then
A6: B1 = B;
then the charact of(U1) = Opers(U2,B1) by A1,Def7;
hence thesis by A1,A2,A6,A3,A4,FINSEQ_1:13;
end;
theorem Th11:
for U1,U2 be SubAlgebra of U0 st the carrier of U1 c= the
carrier of U2 holds U1 is SubAlgebra of U2
proof
let U1,U2 be SubAlgebra of U0;
A1: dom the charact of(U1) = dom the charact of(U0) by Th7;
reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7;
assume
A2: the carrier of U1 c= the carrier of U2;
hence the carrier of U1 is Subset of U2;
let B be non empty Subset of U2;
assume
A3: B = the carrier of U1;
reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7;
A4: the charact of(U2) = Opers(U0,B2) by Def7;
A5: B2 is opers_closed by Def7;
A6: dom Opers(U2,B) = dom the charact of(U2) by Def6;
A7: dom the charact of(U2)= dom the charact of(U0) by Th7;
A8: B1 is opers_closed by Def7;
A9: B is opers_closed
proof
let o2 be operation of U2;
let s be FinSequence of B;
consider n being Nat such that
A10: n in dom the charact of(U2) and
A11: (the charact of(U2)).n = o2 by FINSEQ_2:10;
reconsider o0 = (the charact of(U0)).n as operation of U0 by A7,A10,
FUNCT_1:def 3;
A12: arity o2 = arity o0 by A10,A11,Th6;
rng s c= B by FINSEQ_1:def 4;
then
rng s c= B2 by XBOOLE_1:1;
then s is FinSequence of B2 by FINSEQ_1:def 4;
then reconsider s2 = s as Element of B2* by FINSEQ_1:def 11;
reconsider s1 = s as Element of B1* by A3,FINSEQ_1:def 11;
assume
A13: arity o2 = len s;
set tb2 = (arity o0)-tuples_on B2;
A14: B2 is_closed_on o0 by A5;
A15: o2 = o0/.B2 by A4,A10,A11,Def6
.= o0 | tb2 by A14,Def5;
A16: B1 is_closed_on o0 by A8;
tb2 = {w where w is Element of B2*: len w = arity o0} by FINSEQ_2:def 4;
then s2 in tb2 by A13,A12;
then o2.s = o0.s1 by A15,FUNCT_1:49;
hence thesis by A3,A13,A16,A12;
end;
A17: the charact of(U1) = Opers(U0,B1) by Def7;
now
let n be Nat;
assume
A18: n in dom the charact of(U0);
then reconsider o0 = (the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
reconsider o2 = (the charact of(U2)).n as operation of U2 by A7,A18,
FUNCT_1:def 3;
A19: o2 = o0/.B2 & arity o2 = arity o0 by A4,A7,A18,Def6,Th6;
A20: B is_closed_on o2 by A9;
A21: B2 is_closed_on o0 by A5;
A22: B1 is_closed_on o0 by A8;
thus (the charact of(U1)).n = o0/.B1 by A17,A1,A18,Def6
.= o0 | (arity o0)-tuples_on B1 by A22,Def5
.= o0 | (((arity o0)-tuples_on B2) /\ ((arity o0)-tuples_on B1)) by A2,
MARGREL1:21
.= (o0 | (arity o0)-tuples_on B2) | ((arity o0)-tuples_on B) by A3,
RELAT_1:71
.= (o0 /. B2) | ((arity o0)-tuples_on B) by A21,Def5
.= o2 /. B by A20,A19,Def5
.= Opers(U2,B).n by A7,A6,A18,Def6;
end;
hence the charact of(U1) = Opers(U2,B) by A1,A7,A6,FINSEQ_1:13;
thus thesis by A9;
end;
theorem Th12:
for U1,U2 be strict SubAlgebra of U0 st the carrier of U1 = the
carrier of U2 holds U1 = U2
proof
let U1,U2 be strict SubAlgebra of U0;
assume the carrier of U1 = the carrier of U2;
then U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 by Th11;
hence thesis by Th10;
end;
theorem
U1 is SubAlgebra of U2 implies U1,U2 are_similar
proof
set s1 = signature(U1), s2 = signature(U2);
set X = dom s1;
len s1 = len the charact of(U1) by UNIALG_1:def 4;
then
A1: dom s1 = dom the charact of(U1) by FINSEQ_3:29;
assume
A2: U1 is SubAlgebra of U2;
then reconsider A = the carrier of U1 as non empty Subset of U2 by Def7;
len s2 = len the charact of(U2) by UNIALG_1:def 4;
then
A3: dom s2 = dom the charact of(U2) by FINSEQ_3:29;
dom the charact of (U1)= dom Opers(U2,A) by A2,Def7;
then
A4: dom s1 = dom s2 by A1,A3,Def6;
the charact of(U1)=Opers(U2,A) by A2,Def7;
then
A5: dom s1 c= dom s2 by A1,A3,Def6;
for n being Nat st n in X holds s1.n = s2.n
proof
let n be Nat;
assume
A6: n in X;
then reconsider o1=(the charact of(U1)).n as operation of U1 by A1,
FUNCT_1:def 3;
reconsider o2=(the charact of U2).n as operation of U2 by A3,A4,A6,
FUNCT_1:def 3;
s1.n = arity(o1) & s2.n = arity(o2) by A5,A6,UNIALG_1:def 4;
hence thesis by A2,A1,A6,Th6;
end;
then s1 = s2 by A4,FINSEQ_1:13;
hence thesis;
end;
theorem Th14:
for A be non empty Subset of U0 holds UAStr (#A,Opers(U0,A)#) is
strict Universal_Algebra
proof
let A be non empty Subset of U0;
set C = UAStr(#A,Opers(U0,A)#);
A1: dom the charact of(C) = dom the charact of(U0) by Def6;
for n be object st n in dom the charact of(C) holds (the charact of C).n
is non empty
proof
let n be object;
assume
A2: n in dom the charact of(C);
then reconsider o = (the charact of U0).n as operation of U0 by A1,
FUNCT_1:def 3;
(the charact of C).n =o/.A by A2,Def6;
hence thesis;
end;
then
A3: the charact of(C) is non-empty by FUNCT_1:def 9;
for n be Nat ,h be PartFunc of C st n in dom the charact of(C) & h = (
the charact of C).n holds h is quasi_total
proof
let n;
let h be PartFunc of (the carrier of C)*,the carrier of C;
assume that
A4: n in dom the charact of(C) and
A5: h = (the charact of C).n;
reconsider o = (the charact of U0).n as operation of U0 by A1,A4,
FUNCT_1:def 3;
h =o/.A by A4,A5,Def6;
hence thesis;
end;
then
A6: the charact of C is quasi_total;
for n be Nat ,h be PartFunc of (the carrier of C)*,the carrier of C st n
in dom the charact of(C) & h = (the charact of C).n holds h is homogeneous
proof
let n;
let h be PartFunc of (the carrier of C)*,the carrier of C;
assume that
A7: n in dom the charact of(C) and
A8: h = (the charact of C).n;
reconsider o = (the charact of U0).n as operation of U0 by A1,A7,
FUNCT_1:def 3;
h =o/.A by A7,A8,Def6;
hence thesis;
end;
then
A9: the charact of (C) is homogeneous;
the charact of C <> {} by A1,RELAT_1:38,41;
hence thesis by A9,A6,A3,UNIALG_1:def 1,def 2,def 3;
end;
definition
let U0 be Universal_Algebra, A be non empty Subset of U0;
assume
A1: A is opers_closed;
func UniAlgSetClosed(A) -> strict SubAlgebra of U0 equals
:Def8:
UAStr (# A,
Opers(U0,A) #);
coherence
proof
reconsider C = UAStr(# A,Opers(U0,A) #) as strict Universal_Algebra by Th14
;
for B be non empty Subset of U0 st B =the carrier of C holds the
charact of(C) = Opers(U0,B) & B is opers_closed by A1;
hence thesis by Def7;
end;
end;
definition
let U0;
let U1,U2 be SubAlgebra of U0;
assume
A1: the carrier of U1 meets the carrier of U2;
func U1 /\ U2 -> strict SubAlgebra of U0 means
:Def9:
the carrier of it = (
the carrier of U1) /\ (the carrier of U2) & for B be non empty Subset of U0 st
B=the carrier of it holds the charact of(it) = Opers(U0,B) & B is opers_closed;
existence
proof
A2: (the carrier of U1) /\ (the carrier of U2)c= the carrier of U1 by
XBOOLE_1:17;
the carrier of U1 is Subset of U0 by Def7;
then reconsider C =(the carrier of U1) /\ (the carrier of U2) as non empty
Subset of U0 by A1,A2,XBOOLE_1:1;
set S =UAStr(#C,Opers(U0,C)#);
A3: (the carrier of U1) /\ (the carrier of U2)c= the carrier of U2 by
XBOOLE_1:17;
A4: now
let o be operation of U0;
now
set B1 =the carrier of U1, B2 =the carrier of U2;
let s be FinSequence of C;
reconsider s2=s as FinSequence of B2 by A3,FINSEQ_2:24;
reconsider s1=s as FinSequence of B1 by A2,FINSEQ_2:24;
assume
A5: len s =arity o;
reconsider B1 as non empty Subset of U0 by Def7;
reconsider B2 as non empty Subset of U0 by Def7;
B2 is opers_closed by Def7;
then B2 is_closed_on o;
then
A6: o.s2 in B2 by A5;
B1 is opers_closed by Def7;
then B1 is_closed_on o;
then o.s1 in B1 by A5;
hence o.s in C by A6,XBOOLE_0:def 4;
end;
hence C is_closed_on o;
end;
then
A7: for B be non empty Subset of U0 st B=the carrier of S holds the
charact of(S) = Opers(U0,B) & B is opers_closed;
reconsider S as Universal_Algebra by Th14;
reconsider S as strict SubAlgebra of U0 by A7,Def7;
take S;
thus thesis by A4;
end;
uniqueness
proof
the carrier of U1 is Subset of U0 & (the carrier of U1) /\ (the
carrier of U2)c=(the carrier of U1) by Def7,XBOOLE_1:17;
then reconsider C =(the carrier of U1) /\ (the carrier of U2) as non empty
Subset of U0 by A1,XBOOLE_1:1;
let W1,W2 be strict SubAlgebra of U0;
assume that
A8: the carrier of W1 = (the carrier of U1) /\ (the carrier of U2) &
for B1 be non empty Subset of U0 st B1=the carrier of W1 holds the charact of(
W1) = Opers (U0,B1) & B1 is opers_closed and
A9: the carrier of W2= (the carrier of U1) /\ (the carrier of U2) and
A10: for B2 be non empty Subset of U0 st B2=the carrier of W2 holds
the charact of(W2) = Opers(U0,B2) & B2 is opers_closed;
the charact of W2 = Opers(U0,C) by A9,A10;
hence thesis by A8,A9;
end;
end;
definition
let U0;
func Constants(U0) -> Subset of U0 equals
{ a where a is Element of U0: ex o
be operation of U0 st arity o=0 & a in rng o};
coherence
proof
set E = {a where a is Element of U0 : ex o be operation of U0 st arity o=0
& a in rng o};
E c= the carrier of U0
proof
let x be object;
assume x in E;
then
ex w be Element of U0 st w=x & ex o be operation of U0 st arity o=0 &
w in rng o;
hence thesis;
end;
hence thesis;
end;
end;
definition
let IT be Universal_Algebra;
attr IT is with_const_op means
:Def11:
ex o being operation of IT st arity o =0;
end;
registration
cluster with_const_op strict for Universal_Algebra;
existence
proof
set A = the non empty set;
set a = the Element of A;
reconsider w = <*>A .--> a as Element of PFuncs(A*,A) by MARGREL1:19;
set U0 = UAStr (# A, <*w*> #);
A1: the charact of U0 is quasi_total & the charact of U0 is homogeneous by
MARGREL1:20;
the charact of U0 is non-empty by MARGREL1:20;
then reconsider U0 as Universal_Algebra by A1,UNIALG_1:def 1,def 2,def 3;
take U0;
dom <*w*> ={1} & 1 in {1} by FINSEQ_1:2,38,TARSKI:def 1;
then reconsider o= (the charact of U0).1 as operation of U0 by
FUNCT_1:def 3;
A2: dom o = {<*>A} by FUNCOP_1:13;
A3: now
let x be FinSequence;
assume x in dom o;
then x = <*>A by A2,TARSKI:def 1;
hence len x = 0;
end;
<*>A in {<*>A} by TARSKI:def 1;
then arity o = 0 by A2,A3,MARGREL1:def 25;
hence thesis;
end;
end;
registration
let U0 be with_const_op Universal_Algebra;
cluster Constants(U0) -> non empty;
coherence
proof
consider o being operation of U0 such that
A1: arity o=0 by Def11;
dom o = 0-tuples_on the carrier of U0 by A1,MARGREL1:22
.={<*>the carrier of U0} by FINSEQ_2:94;
then <*>the carrier of U0 in dom o by TARSKI:def 1;
then
A2: o.(<*>the carrier of U0) in rng o by FUNCT_1:def 3;
rng o c= the carrier of U0 by RELAT_1:def 19;
then reconsider u = o.(<*>the carrier of U0) as Element of U0 by A2;
u in { a where a is Element of U0: ex o be operation of U0 st arity o=
0 & a in rng o} by A1,A2;
hence thesis;
end;
end;
theorem Th15:
for U0 be Universal_Algebra, U1 be SubAlgebra of U0 holds
Constants(U0) is Subset of U1
proof
let U0 be Universal_Algebra, U1 be SubAlgebra of U0;
set u1 = the carrier of U1;
Constants(U0) c= u1
proof
reconsider B =u1 as non empty Subset of U0 by Def7;
let x be object;
assume x in Constants(U0);
then consider a be Element of U0 such that
A1: a=x and
A2: ex o be operation of U0 st arity o=0 & a in rng o;
consider o0 be operation of U0 such that
A3: arity o0 = 0 and
A4: a in rng o0 by A2;
consider y be object such that
A5: y in dom o0 and
A6: a = o0.y by A4,FUNCT_1:def 3;
dom o0 = 0-tuples_on the carrier of U0 by A3,MARGREL1:22
.= {<*>the carrier of U0} by FINSEQ_2:94;
then y in {<*>B} by A5;
then y in 0-tuples_on B by FINSEQ_2:94;
then y in dom o0 /\ (arity o0)-tuples_on B by A3,A5,XBOOLE_0:def 4;
then
A7: y in dom (o0 | (arity o0)-tuples_on B) by RELAT_1:61;
consider n being Nat such that
A8: n in dom (the charact of U0) and
A9: (the charact of U0).n=o0 by FINSEQ_2:10;
A10: n in dom the charact of(U1) by A8,Th7;
then reconsider o1= (the charact of U1).n as operation of U1 by
FUNCT_1:def 3;
the charact of(U1) =Opers(U0,B) by Def7;
then
A11: o1=o0/.B by A9,A10,Def6;
B is opers_closed by Def7;
then
A12: B is_closed_on o0;
then y in dom (o0/.B) by A7,Def5;
then
A13: o1.y in rng o1 by A11,FUNCT_1:def 3;
A14: rng o1 c= the carrier of U1 by RELAT_1:def 19;
o1.y = (o0 | (arity o0)-tuples_on B).y by A11,A12,Def5
.= a by A6,A7,FUNCT_1:47;
hence thesis by A1,A13,A14;
end;
hence thesis;
end;
theorem
for U0 be with_const_op Universal_Algebra, U1 be SubAlgebra of U0
holds Constants(U0) is non empty Subset of U1 by Th15;
theorem Th17:
for U0 be with_const_op Universal_Algebra,U1,U2 be SubAlgebra of
U0 holds the carrier of U1 meets the carrier of U2
proof
let U0 be with_const_op Universal_Algebra, U1,U2 be SubAlgebra of U0;
set a = the Element of Constants(U0);
Constants(U0) is non empty Subset of U1 & Constants(U0) is non empty
Subset of U2 by Th15;
then
A1: Constants(U0) c= (the carrier of U1) /\ (the carrier of U2) by XBOOLE_1:19;
thus thesis by A1;
end;
definition
let U0 be Universal_Algebra, A be Subset of U0;
assume
A1: Constants(U0) <> {} or A <> {};
func GenUnivAlg(A) -> strict SubAlgebra of U0 means
:Def12:
A c= the carrier
of it & for U1 be SubAlgebra of U0 st A c= the carrier of U1 holds it is
SubAlgebra of U1;
existence
proof
defpred P[set] means A c= $1 & Constants(U0) c= $1 &
for B be non empty Subset of U0 st B =$1 holds B is opers_closed;
set C = bool(the carrier of U0);
consider X be set such that
A2: for x holds x in X iff x in C & P[x] from XFAMILY:sch 1;
set P = meet X;
the carrier of U0 in C & for B be non empty Subset of U0 st B = the
carrier of U0 holds B is opers_closed by Th4,ZFMISC_1:def 1;
then
A3: the carrier of U0 in X by A2;
A4: P c= the carrier of U0
by A3,SETFAM_1:def 1;
now
let x be set;
assume x in X;
then A c= x & Constants(U0) c= x by A2;
hence A \/ Constants(U0) c= x by XBOOLE_1:8;
end;
then
A5: A \/ Constants(U0) c= P by A3,SETFAM_1:5;
then reconsider P as non empty Subset of U0 by A1,A4;
take E = UniAlgSetClosed(P);
A6: P is opers_closed
proof
let o be operation of U0;
let s be FinSequence of P;
assume
A7: len s = arity o;
now
let a be set;
A8: rng s c= P by FINSEQ_1:def 4;
assume
A9: a in X;
then reconsider a0 = a as Subset of U0 by A2;
A c= a0 & Constants(U0) c= a0 by A2,A9;
then reconsider a0 as non empty Subset of U0 by A1;
P c= a0 by A9,SETFAM_1:3;
then rng s c= a0 by A8;
then reconsider s0 = s as FinSequence of a0 by FINSEQ_1:def 4;
a0 is opers_closed by A2,A9;
then a0 is_closed_on o;
then o.s0 in a0 by A7;
hence o.s in a;
end;
hence thesis by A3,SETFAM_1:def 1;
end;
then
A10: E = UAStr (# P, Opers(U0,P) #) by Def8;
A c= A \/ Constants(U0) by XBOOLE_1:7;
hence A c= the carrier of E by A5,A10;
let U1 be SubAlgebra of U0;
assume
A11: A c= the carrier of U1;
set u1 = the carrier of U1;
A12: Constants(U0) c= u1
proof
reconsider B =u1 as non empty Subset of U0 by Def7;
let x be object;
assume x in Constants(U0);
then consider a be Element of U0 such that
A13: a=x and
A14: ex o be operation of U0 st arity o=0 & a in rng o;
consider o0 be operation of U0 such that
A15: arity o0 = 0 and
A16: a in rng o0 by A14;
consider y be object such that
A17: y in dom o0 and
A18: a = o0.y by A16,FUNCT_1:def 3;
dom o0 = 0-tuples_on the carrier of U0 by A15,MARGREL1:22
.= {<*>the carrier of U0} by FINSEQ_2:94;
then y in {<*>B} by A17;
then y in 0-tuples_on B by FINSEQ_2:94;
then y in dom o0 /\ (arity o0)-tuples_on B by A15,A17,XBOOLE_0:def 4;
then
A19: y in dom (o0 | (arity o0)-tuples_on B) by RELAT_1:61;
consider n being Nat such that
A20: n in dom (the charact of(U0)) and
A21: (the charact of U0).n=o0 by FINSEQ_2:10;
A22: n in dom the charact of(U1) by A20,Th7;
then reconsider o1= (the charact of U1).n as operation of U1 by
FUNCT_1:def 3;
the charact of(U1) =Opers(U0,B) by Def7;
then
A23: o1=o0/.B by A21,A22,Def6;
B is opers_closed by Def7;
then
A24: B is_closed_on o0;
then y in dom (o0/.B) by A19,Def5;
then
A25: o1.y in rng o1 by A23,FUNCT_1:def 3;
A26: rng o1 c= the carrier of U1 by RELAT_1:def 19;
o1.y = (o0 | (arity o0)-tuples_on B).y by A23,A24,Def5
.= a by A18,A19,FUNCT_1:47;
hence thesis by A13,A25,A26;
end;
u1 is Subset of U0 & for B be non empty Subset of U0 st B = u1 holds
B is opers_closed by Def7;
then
A27: u1 in X by A2,A11,A12;
hence the carrier of E is Subset of U1 by A10,SETFAM_1:3;
let B be non empty Subset of U1;
assume
A28: B = the carrier of E;
reconsider u11 = u1 as non empty Subset of U0 by Def7;
A29: the charact of(U1) = Opers(U0,u11) by Def7;
A30: dom the charact of(U0) = dom Opers(U0,u11) by Def6;
A31: u11 is opers_closed by Def7;
A32: now
let o1 be operation of U1;
consider n being Nat such that
A33: n in dom the charact of(U1) and
A34: o1 = (the charact of U1).n by FINSEQ_2:10;
reconsider o0 = (the charact of U0).n as operation of U0 by A29,A30,A33,
FUNCT_1:def 3;
A35: arity o0 =arity o1 by A33,A34,Th6;
A36: u11 is_closed_on o0 by A31;
now
let s be FinSequence of B;
A37: P is_closed_on o0 by A6;
reconsider sE=s as Element of P* by A10,A28,FINSEQ_1:def 11;
s is FinSequence of u11 by FINSEQ_2:24;
then reconsider s1 =s as Element of u11* by FINSEQ_1:def 11;
A38: dom(o0|(arity o0)-tuples_on u11) = (dom o0) /\ (arity o0)
-tuples_on u11 by RELAT_1:61
.= (arity o0)-tuples_on (the carrier of U0) /\ (arity o0)
-tuples_on u11 by MARGREL1:22
.= (arity o0)-tuples_on u11 by MARGREL1:21;
assume
A39: len s = arity o1;
then s1 in{q where q is Element of u11*: len q = arity o0} by A35;
then
A40: s1 in dom(o0|(arity o0)-tuples_on u11) by A38,FINSEQ_2:def 4;
o1.s = (o0/.u11).s1 by A29,A33,A34,Def6
.= (o0|(arity o0)-tuples_on u11).s1 by A36,Def5
.= o0.sE by A40,FUNCT_1:47;
hence o1.s in B by A10,A28,A35,A39,A37;
end;
hence B is_closed_on o1;
end;
A41: dom Opers(U1,B) = dom the charact of(U1) by Def6;
A42: dom the charact of(U0) = dom Opers(U0,P) by Def6;
A43: P c= u1 by A27,SETFAM_1:3;
now
let n be Nat;
assume
A44: n in dom the charact of(U0);
then reconsider o0 = (the charact of U0).n as operation of U0 by
FUNCT_1:def 3;
reconsider o1 = (the charact of U1).n as operation of U1 by A29,A30,A44,
FUNCT_1:def 3;
A45: u11 is_closed_on o0 by A31;
A46: P is_closed_on o0 by A6;
thus (the charact of E).n = o0/.P by A10,A42,A44,Def6
.= o0|((arity o0)-tuples_on P) by A46,Def5
.= o0|((arity o0)-tuples_on u11 /\(arity o0)-tuples_on P)
by A43,MARGREL1:21
.= (o0|((arity o0)-tuples_on u11))|((arity o0)-tuples_on P) by
RELAT_1:71
.= (o0/.u11)|((arity o0)-tuples_on P) by A45,Def5
.= o1|((arity o0)-tuples_on P) by A29,A30,A44,Def6
.= o1|((arity o1)-tuples_on B) by A10,A28,A29,A30,A44,Th6
.= o1/.B by A32,Def5
.= Opers(U1,B).n by A29,A30,A41,A44,Def6;
end;
hence thesis by A10,A29,A42,A30,A32,A41,FINSEQ_1:13;
end;
uniqueness
proof
let W1,W2 be strict SubAlgebra of U0;
assume A c= the carrier of W1 & ( for U1 be SubAlgebra of U0 st A c= the
carrier of U1 holds W1 is SubAlgebra of U1)& A c= the carrier of W2 & for U2 be
SubAlgebra of U0 st A c= the carrier of U2 holds W2 is SubAlgebra of U2;
then W1 is strict SubAlgebra of W2 & W2 is strict SubAlgebra of W1;
hence thesis by Th10;
end;
end;
theorem
for U0 be strict Universal_Algebra holds GenUnivAlg([#](the carrier of
U0)) = U0
proof
let U0 be strict Universal_Algebra;
set W = GenUnivAlg([#](the carrier of U0));
reconsider B = the carrier of W as non empty Subset of U0 by Def7;
(the carrier of W) is Subset of U0 & the carrier of U0 c= the carrier of
W by Def7,Def12;
then
A1: the carrier of U0 = the carrier of W;
A2: dom the charact of(U0) = dom Opers(U0,B) by Def6;
A3: for n being Nat st n in dom the charact of(U0) holds (the charact of(U0)
).n = (Opers(U0,B)).n
proof
let n be Nat;
assume
A4: n in dom the charact of(U0);
then reconsider o =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
(Opers(U0,B)).n = o/.B by A2,A4,Def6;
hence thesis by A1,Th4;
end;
the charact of(W) = Opers(U0,B) by Def7;
hence thesis by A1,A2,A3,FINSEQ_1:13;
end;
theorem Th19:
for U0 be Universal_Algebra, U1 be strict SubAlgebra of U0, B be
non empty Subset of U0 st B = the carrier of U1 holds GenUnivAlg(B) = U1
proof
let U0 be Universal_Algebra,U1 be strict SubAlgebra of U0, B be non empty
Subset of U0;
set W = GenUnivAlg(B);
assume
A1: B = the carrier of U1;
then GenUnivAlg(B) is SubAlgebra of U1 by Def12;
then
A2: the carrier of W is non empty Subset of U1 by Def7;
the carrier of U1 c= the carrier of W by A1,Def12;
then the carrier of U1 = the carrier of W by A2;
hence thesis by Th12;
end;
definition
let U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0;
func U1 "\/" U2 -> strict SubAlgebra of U0 means
:Def13:
for A be non empty
Subset of U0 st A = (the carrier of U1) \/ (the carrier of U2) holds it =
GenUnivAlg(A);
existence
proof
reconsider B =(the carrier of U1) \/ (the carrier of U2) as non empty set;
the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0
by Def7;
then reconsider B as non empty Subset of U0 by XBOOLE_1:8;
take GenUnivAlg(B);
thus thesis;
end;
uniqueness
proof
reconsider B =(the carrier of U1) \/ (the carrier of U2) as non empty set;
let W1,W2 be strict SubAlgebra of U0;
assume that
A1: for A be non empty Subset of U0 st A = (the carrier of U1) \/ (the
carrier of U2) holds W1 = GenUnivAlg(A) and
A2: for A be non empty Subset of U0 st A = (the carrier of U1) \/ (the
carrier of U2) holds W2 = GenUnivAlg(A);
the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0
by Def7;
then reconsider B as non empty Subset of U0 by XBOOLE_1:8;
W1 = GenUnivAlg(B) by A1;
hence thesis by A2;
end;
end;
theorem Th20:
for U0 be Universal_Algebra, U1 be SubAlgebra of U0, A,B be
Subset of U0 st (A <> {} or Constants(U0) <> {}) & B = A \/ the carrier of U1
holds GenUnivAlg(A) "\/" U1 = GenUnivAlg(B)
proof
let U0 be Universal_Algebra, U1 be SubAlgebra of U0, A,B be Subset of U0;
reconsider u1 = the carrier of U1, a = the carrier of GenUnivAlg(A) as non
empty Subset of U0 by Def7;
assume that
A1: A <> {} or Constants(U0) <> {} and
A2: B = A \/ the carrier of U1;
A3: A c= the carrier of GenUnivAlg(A) by Def12;
A4: B c= the carrier of GenUnivAlg(B) by Def12;
A c=B by A2,XBOOLE_1:7;
then
A5: A c= the carrier of GenUnivAlg( B) by A4;
now
per cases by A1;
case
A <> {};
hence
(the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) <>
{} by A3,A5,XBOOLE_1:3,19;
end;
case
A6: Constants(U0) <> {};
Constants(U0) is Subset of GenUnivAlg(A) & Constants(U0) is Subset
of GenUnivAlg(B) by Th15;
hence
(the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) <>
{} by A6,XBOOLE_1:3,19;
end;
end;
then (the carrier of GenUnivAlg(A)) meets (the carrier of GenUnivAlg(B));
then
A7: the carrier of (GenUnivAlg(A) /\ GenUnivAlg(B)) = (the carrier of
GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) by Def9;
reconsider b=a \/ u1 as non empty Subset of U0;
A8: (the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) c= a
by XBOOLE_1:17;
A c= (the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B) )
by A3,A5,XBOOLE_1:19;
then GenUnivAlg(A) is SubAlgebra of (GenUnivAlg(A) /\ GenUnivAlg(B)) by A1,A7
,Def12;
then a is non empty Subset of (GenUnivAlg(A) /\ GenUnivAlg(B)) by Def7;
then a= (the carrier of GenUnivAlg(A)) /\ (the carrier of GenUnivAlg(B)) by
A7,A8;
then
A9: a c= the carrier of GenUnivAlg(B) by XBOOLE_1:17;
u1 c= B by A2,XBOOLE_1:7;
then u1 c= the carrier of GenUnivAlg(B) by A4;
then b c= the carrier of GenUnivAlg(B) by A9,XBOOLE_1:8;
then
A10: GenUnivAlg(b) is strict SubAlgebra of GenUnivAlg(B) by Def12;
A11: (GenUnivAlg(A) "\/" U1) = GenUnivAlg(b) by Def13;
then
A12: a \/ u1 c= the carrier of (GenUnivAlg(A)"\/"U1) by Def12;
A \/ u1 c= a \/ u1 by A3,XBOOLE_1:13;
then B c=the carrier of (GenUnivAlg(A)"\/"U1) by A2,A12;
then GenUnivAlg(B) is strict SubAlgebra of (GenUnivAlg(A)"\/"U1) by A2,Def12;
hence thesis by A11,A10,Th10;
end;
theorem Th21:
for U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0 holds U1
"\/" U2 = U2 "\/" U1
proof
let U0 be Universal_Algebra ,U1,U2 be SubAlgebra of U0;
reconsider u1=the carrier of U1,u2=the carrier of U2 as non empty Subset of
U0 by Def7;
reconsider A = u1 \/ u2 as non empty Subset of U0;
U1 "\/" U2 = GenUnivAlg(A) by Def13;
hence thesis by Def13;
end;
theorem Th22:
for U0 be with_const_op Universal_Algebra,U1,U2 be strict
SubAlgebra of U0 holds U1 /\ (U1"\/"U2) = U1
proof
let U0 be with_const_op Universal_Algebra, U1,U2 be strict SubAlgebra of U0;
reconsider u112=the carrier of(U1 /\ (U1"\/"U2)) as non empty Subset of U0
by Def7;
reconsider u1= the carrier of U1,u2 =the carrier of U2 as non empty Subset
of U0 by Def7;
reconsider A= u1 \/ u2 as non empty Subset of U0;
A1: the charact of (U1)= Opers(U0,u1) by Def7;
A2: dom Opers(U0,u1) = dom the charact of(U0) by Def6;
U1"\/"U2 = GenUnivAlg(A) by Def13;
then
A3: A c= the carrier of (U1 "\/" U2) by Def12;
A4: (the carrier of U1) meets (the carrier of (U1"\/"U2)) by Th17;
then
A5: the carrier of (U1 /\(U1"\/"U2))=(the carrier of U1)/\ (the carrier of(
U1 "\/" U2)) by Def9;
then
A6: the carrier of (U1 /\(U1"\/"U2)) c= the carrier of U1 by XBOOLE_1:17;
the carrier of U1 c= A by XBOOLE_1:7;
then the carrier of U1 c= the carrier of (U1"\/"U2) by A3;
then
A7: the carrier of U1 c=the carrier of (U1 /\(U1"\/"U2)) by A5,XBOOLE_1:19;
A8: dom Opers(U0,u112) = dom the charact of(U0) by Def6;
A9: for n being Nat st n in dom the charact of (U0) holds (the charact of
U1/\(U1"\/"U2)).n= (the charact of U1).n
proof
let n be Nat;
assume
A10: n in dom the charact of (U0);
then reconsider o0 = (the charact of U0).n as operation of U0 by
FUNCT_1:def 3;
thus (the charact of U1 /\ ( U1 "\/" U2)).n = Opers(U0,u112).n by A4,Def9
.= o0/.u112 by A8,A10,Def6
.=o0/.u1 by A7,A6,XBOOLE_0:def 10
.=Opers(U0,u1).n by A2,A10,Def6
.= (the charact of U1).n by Def7;
end;
the charact of (U1/\(U1"\/"U2)) = Opers(U0,u112) by A4,Def9;
then the charact of (U1/\(U1"\/"U2))= the charact of (U1) by A1,A8,A2,A9,
FINSEQ_1:13;
hence thesis by A7,A6,XBOOLE_0:def 10;
end;
theorem Th23:
for U0 be with_const_op Universal_Algebra,U1,U2 be strict
SubAlgebra of U0 holds (U1 /\ U2)"\/"U2 = U2
proof
let U0 be with_const_op Universal_Algebra, U1,U2 be strict SubAlgebra of U0;
reconsider u12= the carrier of (U1 /\ U2), u2 = the carrier of U2 as non
empty Subset of U0 by Def7;
reconsider A=u12 \/ u2 as non empty Subset of U0;
(the carrier of U1) meets (the carrier of U2) by Th17;
then u12 = (the carrier of U1) /\ (the carrier of U2) by Def9;
then
A1: u12 c= u2 by XBOOLE_1:17;
(U1 /\ U2)"\/"U2=GenUnivAlg(A) by Def13;
hence thesis by A1,Th19,XBOOLE_1:12;
end;
definition
let U0 be Universal_Algebra;
func Sub(U0) -> set means
:Def14:
for x being object holds x in it iff x is strict SubAlgebra of U0;
existence
proof
reconsider X = { GenUnivAlg(A) where A is Subset of U0: A is non empty} as
set;
take X;
let x be object;
thus x in X implies x is strict SubAlgebra of U0
proof
assume x in X;
then ex A be Subset of U0 st x = GenUnivAlg(A) & A is non empty;
hence thesis;
end;
assume x is strict SubAlgebra of U0;
then reconsider a = x as strict SubAlgebra of U0;
reconsider A = the carrier of a as non empty Subset of U0 by Def7;
a = GenUnivAlg(A) by Th19;
hence thesis;
end;
uniqueness
proof
let A,B be set;
assume that
A1: for x being object holds x in A iff x is strict SubAlgebra of U0 and
A2: for y being object holds y in B iff y is strict SubAlgebra of U0;
now
let x be object;
assume x in A;
then x is strict SubAlgebra of U0 by A1;
hence x in B by A2;
end;
hence A c= B;
let y be object;
assume y in B;
then y is strict SubAlgebra of U0 by A2;
hence thesis by A1;
end;
end;
registration
let U0 be Universal_Algebra;
cluster Sub(U0) -> non empty;
coherence
proof
set x = the strict SubAlgebra of U0;
x in Sub U0 by Def14;
hence thesis;
end;
end;
definition
let U0 be Universal_Algebra;
func UniAlg_join(U0) -> BinOp of Sub(U0) means
:Def15:
for x,y be Element of
Sub(U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds it.
(x,y) = U1 "\/" U2;
existence
proof
defpred P[(Element of Sub(U0)),(Element of Sub(U0)),Element of Sub(U0)]
means for U1,U2 be strict SubAlgebra of U0 st $1=U1 & $2=U2 holds $3=U1 "\/" U2
;
A1: for x,y being Element of Sub(U0) ex z being Element of Sub(U0) st P[x, y,z]
proof
let x,y be Element of Sub(U0);
reconsider U1=x, U2=y as strict SubAlgebra of U0 by Def14;
reconsider z =U1"\/"U2 as Element of Sub(U0) by Def14;
take z;
thus thesis;
end;
consider o be BinOp of Sub(U0) such that
A2: for a,b be Element of Sub(U0) holds P[a,b,o.(a,b)] from BINOP_1:
sch 3 (A1);
take o;
thus thesis by A2;
end;
uniqueness
proof
let o1,o2 be BinOp of (Sub(U0));
assume that
A3: for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra
of U0 st x=U1 & y=U2 holds o1.(x,y)=U1 "\/" U2 and
A4: for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra
of U0 st x=U1 & y=U2 holds o2.(x,y) = U1 "\/" U2;
for x be Element of Sub(U0) for y be Element of Sub(U0) holds o1.(x,y)
= o2.(x,y)
proof
let x,y be Element of Sub(U0);
reconsider U1=x,U2=y as strict SubAlgebra of U0 by Def14;
o1.(x,y) = U1"\/" U2 by A3;
hence thesis by A4;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let U0 be Universal_Algebra;
func UniAlg_meet(U0) -> BinOp of Sub(U0) means
:Def16:
for x,y be Element of
Sub(U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds it.
(x,y) = U1 /\ U2;
existence
proof
defpred P[(Element of Sub(U0)),(Element of Sub(U0)),Element of Sub(U0)]
means for U1,U2 be strict SubAlgebra of U0 st $1=U1 & $2=U2 holds $3=U1 /\ U2;
A1: for x,y being Element of Sub(U0) ex z being Element of Sub(U0) st P[x, y,z]
proof
let x,y be Element of Sub(U0);
reconsider U1=x, U2=y as strict SubAlgebra of U0 by Def14;
reconsider z =U1 /\ U2 as Element of Sub(U0) by Def14;
take z;
thus thesis;
end;
consider o be BinOp of Sub(U0) such that
A2: for a,b be Element of Sub(U0) holds P[a,b,o.(a,b)] from BINOP_1:
sch 3 (A1);
take o;
thus thesis by A2;
end;
uniqueness
proof
let o1,o2 be BinOp of (Sub(U0));
assume that
A3: for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra
of U0 st x=U1 & y=U2 holds o1.(x,y)=U1 /\ U2 and
A4: for x,y be Element of Sub(U0) holds for U1,U2 be strict SubAlgebra
of U0 st x=U1 & y=U2 holds o2.(x,y) = U1 /\ U2;
for x be Element of Sub(U0) for y be Element of Sub(U0) holds o1.(x,y)
= o2.(x,y)
proof
let x,y be Element of Sub(U0);
reconsider U1=x,U2=y as strict SubAlgebra of U0 by Def14;
o1.(x,y) = U1 /\ U2 by A3;
hence thesis by A4;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th24:
UniAlg_join(U0) is commutative
proof
set o = UniAlg_join(U0);
for x,y be Element of Sub(U0) holds o.(x,y)=o.(y,x)
proof
let x,y be Element of Sub(U0);
reconsider U1=x,U2=y as strict SubAlgebra of U0 by Def14;
reconsider B=(the carrier of U1) \/ (the carrier of U2) as non empty set;
the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0
by Def7;
then reconsider B as non empty Subset of U0 by XBOOLE_1:8;
A1: U1"\/" U2 = GenUnivAlg(B) by Def13;
o.(x,y) = U1 "\/" U2 & o.(y,x) = U2 "\/" U1 by Def15;
hence thesis by A1,Def13;
end;
hence thesis by BINOP_1:def 2;
end;
theorem Th25:
UniAlg_join(U0) is associative
proof
set o = UniAlg_join(U0);
for x,y,z be Element of Sub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
proof
let x,y,z be Element of Sub(U0);
reconsider U1=x,U2=y,U3=z as strict SubAlgebra of U0 by Def14;
reconsider B=(the carrier of U1) \/ ((the carrier of U2) \/ (the carrier
of U3)) as non empty set;
A1: o.(x,y)=U1"\/"U2 by Def15;
A2: the carrier of U2 is Subset of U0 by Def7;
A3: the carrier of U3 is Subset of U0 by Def7;
then reconsider
C = (the carrier of U2) \/ (the carrier of U3) as non empty
Subset of U0 by A2,XBOOLE_1:8;
A4: the carrier of U1 is Subset of U0 by Def7;
then reconsider D=(the carrier of U1) \/ (the carrier of U2) as non empty
Subset of U0 by A2,XBOOLE_1:8;
(the carrier of U2) \/ (the carrier of U3) c= the carrier of U0 by A2,A3,
XBOOLE_1:8;
then reconsider B as non empty Subset of U0 by A4,XBOOLE_1:8;
A5: B= D \/ (the carrier of U3) by XBOOLE_1:4;
A6: (U1"\/"U2)"\/"U3 = GenUnivAlg(D)"\/" U3 by Def13
.= GenUnivAlg(B) by A5,Th20;
o.(y,z)=U2"\/"U3 by Def15;
then
A7: o.(x,o.(y,z)) = U1 "\/" (U2"\/"U3) by Def15;
U1"\/" (U2"\/"U3) = U1 "\/"(GenUnivAlg(C)) by Def13
.=(GenUnivAlg(C)) "\/" U1 by Th21
.= GenUnivAlg(B) by Th20;
hence thesis by A1,A7,A6,Def15;
end;
hence thesis by BINOP_1:def 3;
end;
theorem Th26:
for U0 be with_const_op Universal_Algebra holds UniAlg_meet(U0)
is commutative
proof
let U0 be with_const_op Universal_Algebra;
set o = UniAlg_meet(U0);
for x,y be Element of Sub(U0) holds o.(x,y)=o.(y,x)
proof
let x,y be Element of Sub(U0);
reconsider U1=x,U2=y as strict SubAlgebra of U0 by Def14;
A1: o.(x,y) = U1 /\ U2 & o.(y,x) = U2 /\ U1 by Def16;
A2: (the carrier of U1) meets (the carrier of U2) by Th17;
then
the carrier of(U2 /\ U1) = (the carrier of U2) /\ (the carrier of U1)
& for B2 be non empty Subset of U0 st B2=the carrier of (U2/\U1) holds the
charact of (U2/\U1) = Opers(U0,B2) & B2 is opers_closed by Def9;
hence thesis by A1,A2,Def9;
end;
hence thesis by BINOP_1:def 2;
end;
theorem Th27:
for U0 be with_const_op Universal_Algebra holds UniAlg_meet(U0)
is associative
proof
let U0 be with_const_op Universal_Algebra;
set o = UniAlg_meet(U0);
for x,y,z be Element of Sub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
proof
let x,y,z be Element of Sub(U0);
reconsider U1=x,U2=y,U3=z as strict SubAlgebra of U0 by Def14;
reconsider u23 = U2 /\ U3,u12 =U1 /\ U2 as Element of Sub(U0) by Def14;
A1: o.(x,o.(y,z)) =o.(x,u23) by Def16
.= U1/\(U2 /\ U3) by Def16;
A2: o.(o.(x,y),z) = o.(u12,z) by Def16
.=(U1 /\ U2) /\ U3 by Def16;
(the carrier of U2) meets (the carrier of U3) by Th17;
then
A3: the carrier of(U2 /\ U3) = (the carrier of U2) /\ (the carrier of U3)
by Def9;
then
A4: (the carrier of U1) meets ((the carrier of U2)/\(the carrier of U3))
by Th17;
then
A5: for B be non empty Subset of U0 st B=the carrier of (U1/\(U2/\U3))
holds the charact of (U1/\(U2/\U3)) = Opers(U0,B) & B is opers_closed by A3
,Def9;
A6: the carrier of (U1 /\ (U2 /\ U3)) =(the carrier of U1) /\ ((the
carrier of U2)/\(the carrier of U3)) by A3,A4,Def9;
then reconsider
C =(the carrier of U1) /\ ((the carrier of U2)/\ (the carrier
of U3)) as non empty Subset of U0 by Def7;
A7: C =((the carrier of U1)/\(the carrier of U2)) /\ (the carrier of U3)
by XBOOLE_1:16;
(the carrier of U1) meets (the carrier of U2) by Th17;
then
A8: the carrier of (U1 /\ U2) = (the carrier of U1) /\ (the carrier of U2)
by Def9;
then
((the carrier of U1) /\ (the carrier of U2)) meets (the carrier of U3)
by Th17;
hence thesis by A1,A2,A8,A6,A5,A7,Def9;
end;
hence thesis by BINOP_1:def 3;
end;
definition
let U0 be with_const_op Universal_Algebra;
func UnSubAlLattice(U0) -> strict Lattice equals
LattStr (# Sub(U0),
UniAlg_join(U0), UniAlg_meet(U0) #);
coherence
proof
set L = LattStr (# Sub(U0), UniAlg_join(U0), UniAlg_meet(U0) #);
A1: 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 Sub(U0);
A2: UniAlg_join(U0) is associative by Th25;
thus a"\/"(b"\/"c) = (the L_join of L).(a,(b"\/"c)) by LATTICES:def 1
.= (UniAlg_join(U0)).(x,(UniAlg_join(U0)).(y,z)) by LATTICES:def 1
.=(the L_join of L).((the L_join of L).(a,b),c) by A2,BINOP_1:def 3
.=((the L_join of L).(a,b))"\/"c by LATTICES:def 1
.=(a"\/"b)"\/"c by LATTICES:def 1;
end;
A3: 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 Sub(U0);
A4: UniAlg_meet(U0) is commutative by Th26;
thus a"/\"b = (UniAlg_meet(U0)).(x,y) by LATTICES:def 2
.=(the L_meet of L).(b,a) by A4,BINOP_1:def 2
.=b"/\"a by LATTICES:def 2;
end;
A5: 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 Sub(U0);
A6: (UniAlg_meet(U0)).(x,(UniAlg_join(U0)).(x,y))= x
proof
reconsider U1= x,U2=y as strict SubAlgebra of U0 by Def14;
(UniAlg_join(U0)).(x,y) = U1"\/"U2 by Def15;
hence
(UniAlg_meet(U0)).(x,(UniAlg_join(U0)).(x,y)) = (U1 /\( U1"\/"U2)
) by Def16
.=x by Th22;
end;
thus a"/\"(a"\/"b) = (the L_meet of L).(a,(a"\/"b)) by LATTICES:def 2
.=a by A6,LATTICES:def 1;
end;
A7: 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 Sub(U0);
A8: (UniAlg_join(U0)).((UniAlg_meet(U0)).(x,y),y)= y
proof
reconsider U1= x,U2=y as strict SubAlgebra of U0 by Def14;
(UniAlg_meet(U0)).(x,y) = U1 /\ U2 by Def16;
hence
(UniAlg_join(U0)).((UniAlg_meet(U0)).(x,y),y) = ((U1 /\ U2)"\/"U2
) by Def15
.=y by Th23;
end;
thus (a"/\"b)"\/"b = (the L_join of L).((a"/\"b),b) by LATTICES:def 1
.=b by A8,LATTICES:def 2;
end;
A9: 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 Sub(U0);
A10: UniAlg_meet(U0) is associative by Th27;
thus a"/\"(b"/\"c) = (the L_meet of L).(a,(b"/\"c)) by LATTICES:def 2
.= (UniAlg_meet(U0)).(x,(UniAlg_meet(U0)).(y,z)) by LATTICES:def 2
.=(the L_meet of L).((the L_meet of L).(a,b),c) by A10,BINOP_1:def 3
.=((the L_meet of L).(a,b))"/\"c by LATTICES:def 2
.=(a"/\"b)"/\"c by LATTICES:def 2;
end;
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 Sub(U0);
A11: UniAlg_join(U0) is commutative by Th24;
thus a"\/"b = (UniAlg_join(U0)).(x,y) by LATTICES:def 1
.=(the L_join of L).(b,a) by A11,BINOP_1:def 2
.=b"\/"a by LATTICES:def 1;
end;
then L is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A1,A7,A3,A9,A5,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
hence thesis;
end;
end;