:: Subalgebras of a Order Sorted Algebra. {L}attice of Subalgebras
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-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 XBOOLE_0, ORDERS_2, OSALG_1, PBOOLE, SUBSET_1, XXREAL_0, FUNCT_1,
TARSKI, RELAT_1, MSUALG_1, MSUALG_2, SEQM_3, STRUCT_0, UNIALG_2, CARD_3,
ZFMISC_1, QC_LANG1, SETFAM_1, BINOP_1, LATTICES, EQREL_1, XXREAL_2,
OSALG_2, SETLIM_2;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, SETFAM_1, BINOP_1,
CARD_3, MBOOLEAN, PBOOLE, FINSEQ_2, STRUCT_0, LATTICES, MSUALG_1,
ORDERS_2, MSUALG_2, OSALG_1;
constructors SETFAM_1, MBOOLEAN, MSUALG_2, ORDERS_3, OSALG_1, RELSET_1,
CARD_3;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, MSUALG_1,
MSUALG_2, ORDERS_3, OSALG_1, FUNCT_1, RELAT_1, PBOOLE, FINSEQ_1;
requirements BOOLE, SUBSET;
definitions TARSKI, PBOOLE, LATTICES, OSALG_1, MSUALG_2;
equalities LATTICES, MSUALG_2;
expansions TARSKI, PBOOLE, LATTICES, MSUALG_2;
theorems TARSKI, XBOOLE_0, XBOOLE_1, FUNCT_1, PBOOLE, CARD_3, MSUALG_1,
FUNCT_2, ZFMISC_1, SETFAM_1, BINOP_1, LATTICES, RELAT_1, OSALG_1,
ORDERS_2, MSUALG_2, MBOOLEAN, PARTFUN1;
schemes XBOOLE_0, BINOP_1, FUNCT_1, XFAMILY;
begin :: Auxiliary facts about Order Sorted Sets.
reserve x for set,
R for non empty Poset;
:: should be clusters, but that requires redef of the operation
theorem Th1:
for X,Y being OrderSortedSet of R holds X (/\) Y is OrderSortedSet of R
proof
let X,Y be OrderSortedSet of R;
reconsider M = X (/\) Y as ManySortedSet of R;
M is order-sorted
proof
let s1,s2 be Element of R;
assume s1 <= s2;
then
A1: X.s1 c= X.s2 & Y.s1 c= Y.s2 by OSALG_1:def 16;
(X (/\) Y).s1 = X.s1 /\ Y.s1 & (X (/\) Y).s2 = X.s2 /\ Y.s2
by PBOOLE:def 5;
hence thesis by A1,XBOOLE_1:27;
end;
hence thesis;
end;
theorem Th2:
for X,Y being OrderSortedSet of R holds X (\/) Y is OrderSortedSet of R
proof
let X,Y be OrderSortedSet of R;
reconsider M = X (\/) Y as ManySortedSet of R;
M is order-sorted
proof
let s1,s2 be Element of R;
assume s1 <= s2;
then
A1: X.s1 c= X.s2 & Y.s1 c= Y.s2 by OSALG_1:def 16;
(X (\/) Y).s1 = X.s1 \/ Y.s1 & (X (\/) Y).s2 = X.s2 \/ Y.s2
by PBOOLE:def 4;
hence thesis by A1,XBOOLE_1:13;
end;
hence thesis;
end;
:: new and bad
definition
let R be non empty Poset, M be OrderSortedSet of R;
:: can be for ManySortedSet
mode OrderSortedSubset of M -> ManySortedSubset of M means
:Def1:
it is OrderSortedSet of R;
existence
proof
reconsider X=M as ManySortedSubset of M by PBOOLE:def 18;
take X;
thus thesis;
end;
end;
registration
let R be non empty Poset, M be non-empty OrderSortedSet of R;
cluster non-empty for OrderSortedSubset of M;
existence
proof
reconsider N= M as ManySortedSubset of M by PBOOLE:def 18;
reconsider N1 = N as OrderSortedSubset of M by Def1;
take N1;
thus thesis;
end;
end;
begin
::
:: Constants of an Order Sorted Algebra.
::
definition
let S be OrderSortedSign, U0 be OSAlgebra of S;
mode OSSubset of U0 -> ManySortedSubset of the Sorts of U0 means
:Def2:
it is OrderSortedSet of S;
existence
proof
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
take B;
thus thesis by OSALG_1:17;
end;
end;
:: very strange, the cluster in OSALG_1 should take care of this one
registration
let S be OrderSortedSign;
cluster monotone strict non-empty for OSAlgebra of S;
existence
proof
set z1 = the Element of {{}};
take TrivialOSA(S,{{}},z1);
thus thesis;
end;
end;
registration
let S be OrderSortedSign, U0 be non-empty OSAlgebra of S;
cluster non-empty for OSSubset of U0;
existence
proof
reconsider N= the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
then reconsider M = N as OSSubset of U0 by Def2;
take M;
thus thesis;
end;
end;
theorem Th3:
for S0 being non void all-with_const_op strict non empty
ManySortedSign holds OSSign S0 is all-with_const_op
proof
let S0 be non void all-with_const_op strict non empty ManySortedSign;
let s be Element of OSSign S0;
reconsider s1 =s as Element of S0 by OSALG_1:def 5;
s1 is with_const_op by MSUALG_2:def 2;
then consider o being Element of the carrier' of S0 such that
A1: (the Arity of S0).o = {} & (the ResultSort of S0).o = s1;
A2: o is Element of the carrier' of OSSign S0 by OSALG_1:def 5;
(the Arity of OSSign S0).o = {} & (the ResultSort of OSSign S0).o = s1
by A1,OSALG_1:def 5;
hence thesis by A2;
end;
registration
cluster all-with_const_op strict for OrderSortedSign;
existence
proof
set S0 = the non void all-with_const_op strict non empty ManySortedSign;
take OSSign S0;
thus thesis by Th3;
end;
end;
begin
::
:: Subalgebras of a Order Sorted Algebra.
::
theorem Th4:
for S being OrderSortedSign, U0 being OSAlgebra of S holds
MSAlgebra (#the Sorts of U0,the Charact of U0#) is order-sorted
proof
let S be OrderSortedSign, U0 be OSAlgebra of S;
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
hence thesis by OSALG_1:17;
end;
registration
let S be OrderSortedSign, U0 be OSAlgebra of S;
cluster order-sorted for MSSubAlgebra of U0;
existence
proof
reconsider U1 = MSAlgebra (#the Sorts of U0,the Charact of U0#) as strict
MSSubAlgebra of U0 by MSUALG_2:37;
take U1;
thus thesis by Th4;
end;
end;
definition
let S be OrderSortedSign, U0 be OSAlgebra of S;
mode OSSubAlgebra of U0 is order-sorted MSSubAlgebra of U0;
end;
registration
let S be OrderSortedSign, U0 be OSAlgebra of S;
cluster strict for OSSubAlgebra of U0;
existence
proof
reconsider U1 = MSAlgebra (#the Sorts of U0,the Charact of U0#) as
order-sorted MSSubAlgebra of U0 by Th4,MSUALG_2:37;
take U1;
thus thesis;
end;
end;
registration
let S be OrderSortedSign, U0 be non-empty OSAlgebra of S;
cluster non-empty strict for OSSubAlgebra of U0;
existence
proof
set U1 = MSAlgebra (#the Sorts of U0,the Charact of U0#);
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
then reconsider U1 as strict OSSubAlgebra of U0 by MSUALG_2:37,OSALG_1:17;
take U1;
thus thesis;
end;
end;
:: the equivalent def, maybe not needed
theorem Th5:
for S being OrderSortedSign for U0 being OSAlgebra of S for U1
being MSAlgebra over S holds U1 is OSSubAlgebra of U0 iff the Sorts of U1 is
OSSubset of U0 & for B be OSSubset of U0 st B = the Sorts of U1 holds B is
opers_closed & the Charact of U1 = Opers(U0,B)
proof
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
let U1 be MSAlgebra over S;
hereby
assume
A1: U1 is OSSubAlgebra of U0;
then the Sorts of U1 is OrderSortedSet of S & the Sorts of U1 is MSSubset
of U0 by MSUALG_2:def 9,OSALG_1:17;
hence the Sorts of U1 is OSSubset of U0 by Def2;
let B be OSSubset of U0;
assume B = the Sorts of U1;
hence B is opers_closed & the Charact of U1 = Opers(U0,B) by A1,
MSUALG_2:def 9;
end;
assume
A2: the Sorts of U1 is OSSubset of U0;
assume
A3: for B be OSSubset of U0 st B = the Sorts of U1 holds B is
opers_closed & the Charact of U1 = Opers(U0,B);
A4: U1 is MSSubAlgebra of U0
proof
thus the Sorts of U1 is MSSubset of U0 by A2;
let B be MSSubset of U0 such that
A5: B = the Sorts of U1;
reconsider B1=B as OSSubset of U0 by A2,A5;
B1 is opers_closed by A3,A5;
hence thesis by A3,A5;
end;
the Sorts of U1 is OrderSortedSet of S by A2,Def2;
hence thesis by A4,OSALG_1:17;
end;
reserve S1 for OrderSortedSign,
OU0 for OSAlgebra of S1;
reserve s,s1,s2,s3,s4 for SortSymbol of S1;
definition
let S1,OU0,s;
func OSConstants(OU0,s) -> Subset of (the Sorts of OU0).s equals
union {
Constants(OU0,s2) : s2 <= s};
coherence
proof
set Cs = {Constants(OU0,s2) : s2 <= s};
for X being set st X in Cs holds X c= (the Sorts of OU0).s
proof
let X be set;
assume X in Cs;
then consider s2 such that
A1: X = Constants(OU0,s2) and
A2: s2 <= s;
(the Sorts of OU0).s2 c= (the Sorts of OU0).s by A2,OSALG_1:def 17;
hence thesis by A1;
end;
hence thesis by ZFMISC_1:76;
end;
end;
:: maybe
:: theorem S1 is discrete implies OSConstants(OU0,s) = Constants(OU0,s);
theorem Th6:
Constants(OU0,s) c= OSConstants(OU0,s)
proof
Constants(OU0,s) in {Constants(OU0,s2) : s2 <= s};
hence thesis by ZFMISC_1:74;
end;
definition
let S1;
let M be ManySortedSet of the carrier of S1;
func OSCl M -> OrderSortedSet of S1 means
:Def4:
for s be SortSymbol of S1 holds it.s = union { M.s1: s1 <= s};
existence
proof
deffunc F(Element of S1) = union {M.s1: s1 <= $1};
consider f be Function such that
A1: dom f = the carrier of S1 & for d be Element of S1 holds f.d = F(d
) from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S1 by A1,PARTFUN1:def 2
,RELAT_1:def 18;
reconsider f1=f as ManySortedSet of S1;
f1 is order-sorted
proof
let r1,r2 be Element of S1;
assume
A2: r1 <= r2;
let x be object;
assume x in f1.r1;
then x in union {M.s2: s2 <= r1} by A1;
then consider y being set such that
A3: x in y & y in {M.s2: s2 <= r1} by TARSKI:def 4;
consider s3 such that
A4: y = M.s3 and
A5: s3 <= r1 by A3;
s3 <= r2 by A2,A5,ORDERS_2:3;
then y in {M.s2: s2 <= r2} by A4;
then x in union {M.s2: s2 <= r2} by A3,TARSKI:def 4;
hence thesis by A1;
end;
then reconsider f2 = f1 as OrderSortedSet of S1;
take f2;
thus thesis by A1;
end;
uniqueness
proof
let W1, W2 be OrderSortedSet of S1;
assume
A6: for s being SortSymbol of S1 holds W1.s = union { M.s1: s1 <= s};
assume
A7: for s being SortSymbol of S1 holds W2.s = union { M.s1: s1 <= s};
for s be object st s in the carrier of S1 holds W1.s = W2.s
proof
let s be object;
assume s in the carrier of S1;
then reconsider t = s as SortSymbol of S1;
W1.s = union { M.s1: s1 <= t} by A6
.= W2.s by A7;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th7:
for M being ManySortedSet of the carrier of S1 holds M c= OSCl M
proof
let M be ManySortedSet of the carrier of S1;
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
M.s in {M.s1: s1 <= s};
then M.s c= union { M.s1: s1 <= s} by ZFMISC_1:74;
hence thesis by Def4;
end;
theorem Th8:
for M being ManySortedSet of the carrier of S1, A being
OrderSortedSet of S1 holds M c= A implies OSCl M c= A
proof
let M be ManySortedSet of the carrier of S1, A be OrderSortedSet of S1;
assume
A1: M c= A;
assume not OSCl M c= A;
then consider i being object such that
A2: i in the carrier of S1 and
A3: not (OSCl M).i c= A.i;
reconsider s = i as SortSymbol of S1 by A2;
consider x being object such that
A4: x in (OSCl M).i and
A5: not x in A.i by A3;
(OSCl M).s = union { M.s2 : s2 <= s} by Def4;
then consider X1 being set such that
A6: x in X1 and
A7: X1 in { M.s2 : s2 <= s} by A4,TARSKI:def 4;
consider s1 being SortSymbol of S1 such that
A8: X1 = M.s1 and
A9: s1 <= s by A7;
M.s1 c= A.s1 by A1;
then
A10: x in A.s1 by A6,A8;
A.s1 c= A.s by A9,OSALG_1:def 16;
hence contradiction by A5,A10;
end;
theorem
for S being OrderSortedSign, X being OrderSortedSet of S holds OSCl X = X
proof
let S be OrderSortedSign, X be OrderSortedSet of S;
X c= OSCl X & OSCl X c= X by Th7,Th8;
hence thesis by PBOOLE:146;
end;
:: following should be rewritten to use OSCl Constants(OU0) instead;
:: maybe later
definition
let S1,OU0;
func OSConstants (OU0) -> OSSubset of OU0 means
:Def5:
for s be SortSymbol of S1 holds it.s = OSConstants(OU0,s);
existence
proof
deffunc F(Element of S1) = union {Constants(OU0,s1): s1 <= $1};
consider f be Function such that
A1: dom f = the carrier of S1 & for d be Element of S1 holds f.d = F(d
) from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S1 by A1,PARTFUN1:def 2
,RELAT_1:def 18;
f c= the Sorts of OU0
proof
let s be object;
assume s in the carrier of S1;
then reconsider s1 = s as SortSymbol of S1;
f.s1 = OSConstants(OU0,s1) by A1;
hence thesis;
end;
then reconsider f as MSSubset of OU0 by PBOOLE:def 18;
take f;
reconsider f1=f as ManySortedSet of S1;
f1 is order-sorted
proof
let r1,r2 be Element of S1;
assume
A2: r1 <= r2;
let x be object;
assume x in f1.r1;
then x in union {Constants(OU0,s2): s2 <= r1} by A1;
then consider y being set such that
A3: x in y & y in {Constants(OU0,s2): s2 <= r1} by TARSKI:def 4;
consider s3 such that
A4: y = Constants(OU0,s3) and
A5: s3 <= r1 by A3;
s3 <= r2 by A2,A5,ORDERS_2:3;
then y in {Constants(OU0,s2): s2 <= r2} by A4;
then x in union {Constants(OU0,s2): s2 <= r2} by A3,TARSKI:def 4;
hence thesis by A1;
end;
hence f is OSSubset of OU0 by Def2;
thus thesis by A1;
end;
uniqueness
proof
let W1, W2 be OSSubset of OU0;
assume that
A6: for s be SortSymbol of S1 holds W1.s = OSConstants(OU0,s) and
A7: for s be SortSymbol of S1 holds W2.s = OSConstants(OU0,s);
for s be object st s in the carrier of S1 holds W1.s = W2.s
proof
let s be object;
assume s in the carrier of S1;
then reconsider t = s as SortSymbol of S1;
W1.t = OSConstants(OU0,t) by A6;
hence thesis by A7;
end;
hence thesis;
end;
end;
theorem Th10:
Constants(OU0) c= OSConstants(OU0)
proof
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
(Constants(OU0)).s = Constants(OU0,s) & (OSConstants(OU0)).s =
OSConstants( OU0,s) by Def5,MSUALG_2:def 4;
hence thesis by Th6;
end;
theorem Th11:
for A being OSSubset of OU0 holds Constants(OU0) c= A implies
OSConstants(OU0) c= A
proof
let A be OSSubset of OU0;
assume
A1: Constants(OU0) c= A;
assume not OSConstants(OU0) c= A;
then consider i being object such that
A2: i in the carrier of S1 and
A3: not (OSConstants(OU0)).i c= A.i;
reconsider s = i as SortSymbol of S1 by A2;
consider x being object such that
A4: x in (OSConstants(OU0)).i and
A5: not x in A.i by A3;
(OSConstants(OU0)).s = OSConstants(OU0,s) by Def5
.= union {Constants(OU0,s2) : s2 <= s};
then consider X1 being set such that
A6: x in X1 and
A7: X1 in {Constants(OU0,s2) : s2 <= s} by A4,TARSKI:def 4;
consider s1 being SortSymbol of S1 such that
A8: X1 = Constants(OU0,s1) and
A9: s1 <= s by A7;
A10: (Constants(OU0)).s1 c= A.s1 by A1;
x in (Constants(OU0)).s1 by A6,A8,MSUALG_2:def 4;
then
A11: x in A.s1 by A10;
A is OrderSortedSet of S1 by Def2;
then A.s1 c= A.s by A9,OSALG_1:def 16;
hence contradiction by A5,A11;
end;
theorem
for A being OSSubset of OU0 holds OSConstants(OU0) = OSCl Constants( OU0)
proof
let A be OSSubset of OU0;
A1: now
let i be set;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
set c1 = { (Constants(OU0)).s1: s1 <= s}, c2 = { Constants(OU0,s1): s1 <=
s};
for x being object holds (x in c1 iff x in c2)
proof
let x be object;
hereby
assume x in c1;
then consider s1 such that
A2: x = (Constants(OU0)).s1 and
A3: s1 <= s;
x = Constants(OU0,s1) by A2,MSUALG_2:def 4;
hence x in c2 by A3;
end;
assume x in c2;
then consider s1 such that
A4: x = Constants(OU0,s1) and
A5: s1 <= s;
x = (Constants(OU0)).s1 by A4,MSUALG_2:def 4;
hence thesis by A5;
end;
then
A6: c1 = c2 by TARSKI:2;
(OSConstants(OU0)).s = OSConstants(OU0,s) by Def5
.= (OSCl Constants(OU0)).s by A6,Def4;
hence (OSConstants(OU0)).i = (OSCl Constants(OU0)).i;
end;
then
for i being object st i in the carrier of S1 holds (OSCl Constants(OU0)).i
c= (OSConstants(OU0)).i;
then
A7: OSCl Constants(OU0) c= OSConstants(OU0);
for i being object st i in the carrier of S1 holds (OSConstants(OU0)).i c=
(OSCl Constants(OU0)).i by A1;
then OSConstants(OU0) c= OSCl Constants(OU0);
hence thesis by A7,PBOOLE:146;
end;
theorem Th13:
for OU1 being OSSubAlgebra of OU0 holds OSConstants(OU0) is OSSubset of OU1
proof
let OU1 be OSSubAlgebra of OU0;
OSConstants(OU0) c= the Sorts of OU1
proof
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
Constants(OU0) is MSSubset of OU1 by MSUALG_2:10;
then
A1: Constants(OU0) c= (the Sorts of OU1) by PBOOLE:def 18;
A2: for s2,s3 st s2 <= s3 holds (Constants(OU0)).s2 c= (the Sorts of OU1). s3
proof
let s2,s3;
assume s2 <= s3;
then
A3: (the Sorts of OU1).s2 c= (the Sorts of OU1).s3 by OSALG_1:def 17;
(Constants(OU0)).s2 c= (the Sorts of OU1).s2 by A1;
hence thesis by A3;
end;
A4: for X being set st X in {Constants(OU0,s1): s1 <= s} holds X c= (the
Sorts of OU1).s
proof
let X be set;
assume X in {Constants(OU0,s1): s1 <= s};
then consider s4 such that
A5: X = Constants(OU0,s4) & s4 <= s;
Constants(OU0,s4) = (Constants(OU0)).s4 by MSUALG_2:def 4;
hence thesis by A2,A5;
end;
(OSConstants(OU0)).i = OSConstants(OU0,s) by Def5
.= union {Constants(OU0,s1): s1 <= s};
hence thesis by A4,ZFMISC_1:76;
end;
then
A6: OSConstants(OU0) is ManySortedSubset of the Sorts of OU1 by PBOOLE:def 18;
OSConstants(OU0) is OrderSortedSet of S1 by Def2;
hence thesis by A6,Def2;
end;
theorem
for S being all-with_const_op OrderSortedSign, OU0 being non-empty
OSAlgebra of S, OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants(OU0)
is non-empty OSSubset of OU1
proof
let S be all-with_const_op OrderSortedSign, OU0 be non-empty OSAlgebra of S,
OU1 be non-empty OSSubAlgebra of OU0;
Constants(OU0) c= OSConstants(OU0) by Th10;
hence thesis by Th13,PBOOLE:131;
end;
begin
::
:: Order Sorted Subsets of an Order Sorted Algebra.
::
:: this should be in MSUALG_2
theorem Th15:
for I being set for M being ManySortedSet of I for x being set
holds x is ManySortedSubset of M iff x in product bool M
proof
let I be set;
let M be ManySortedSet of I;
let x be set;
A1: I = dom bool M by PARTFUN1:def 2;
hereby
assume x is ManySortedSubset of M;
then reconsider x1 = x as ManySortedSubset of M;
A2: for i being object st i in dom bool M holds x1.i in (bool M).i
proof
let i be object such that
A3: i in dom bool M;
x1 c= M by PBOOLE:def 18;
then x1.i c= M.i by A1,A3;
then x1.i in bool (M.i);
hence thesis by A1,A3,MBOOLEAN:def 1;
end;
dom x1 = I by PARTFUN1:def 2
.= dom bool M by PARTFUN1:def 2;
hence x in product bool M by A2,CARD_3:def 5;
end;
assume x in product bool M;
then consider x1 being Function such that
A4: x = x1 and
A5: dom x1 = dom bool M and
A6: for i being object st i in dom bool M holds x1.i in (bool M).i
by CARD_3:def 5;
dom x1 = I by A5,PARTFUN1:def 2;
then reconsider x2 = x1 as ManySortedSet of I by PARTFUN1:def 2
,RELAT_1:def 18;
x2 c= M
proof
let i be object such that
A7: i in I;
x2.i in (bool M).i by A1,A6,A7;
then x2.i in bool (M.i) by A7,MBOOLEAN:def 1;
hence thesis;
end;
hence thesis by A4,PBOOLE:def 18;
end;
:: Fraenkel should be improved, to allow more than just Element type
definition
let R be non empty Poset, M be OrderSortedSet of R;
func OSbool(M) -> set means
for x being set holds x in it iff x is OrderSortedSubset of M;
existence
proof
defpred P[set] means $1 is OrderSortedSubset of M;
set f = product bool M;
consider X being set such that
A1: for y being set holds y in X iff y in f & P[y] from XFAMILY:sch 1;
take X;
let y be set;
thus y in X implies y is OrderSortedSubset of M by A1;
assume
A2: y is OrderSortedSubset of M;
then y in f by Th15;
hence thesis by A1,A2;
end;
uniqueness
proof
defpred P[set] means $1 is OrderSortedSubset of M;
thus for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (
for x being set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;
end;
end;
definition
let S be OrderSortedSign, U0 be OSAlgebra of S, A be OSSubset of U0;
func OSSubSort(A) -> set equals
{ x where x is Element of SubSort(A): x is
OrderSortedSet of S};
correctness;
end;
theorem Th16:
for A being OSSubset of OU0 holds OSSubSort(A) c= SubSort(A)
proof
let A be OSSubset of OU0;
let x be object;
assume x in OSSubSort(A);
then
ex y being Element of SubSort(A) st x = y & y is OrderSortedSet of S1;
hence thesis;
end;
theorem Th17:
for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort( A)
proof
let A be OSSubset of OU0;
reconsider X = the Sorts of OU0 as Element of SubSort(A) by MSUALG_2:38;
the Sorts of OU0 is OrderSortedSet of S1 by OSALG_1:17;
then
X in { x where x is Element of SubSort(A): x is OrderSortedSet of S1};
hence thesis;
end;
registration
let S1,OU0;
let A be OSSubset of OU0;
cluster OSSubSort(A) -> non empty;
coherence by Th17;
end;
definition
let S1,OU0;
func OSSubSort(OU0) -> set equals
{ x where x is Element of SubSort(OU0): x
is OrderSortedSet of S1};
correctness;
end;
theorem Th18:
for A being OSSubset of OU0 holds OSSubSort(A) c= OSSubSort(OU0)
proof
let A be OSSubset of OU0;
let x be object;
assume x in OSSubSort(A);
then consider x1 being Element of SubSort(A) such that
A1: x1 = x and
A2: x1 is OrderSortedSet of S1;
x1 in SubSort(A) & SubSort(A) c= SubSort(OU0) by MSUALG_2:39;
then reconsider x2 = x1 as Element of SubSort(OU0);
x2 in { y where y is Element of SubSort(OU0): y is OrderSortedSet of S1
} by A2;
hence thesis by A1;
end;
registration
let S1,OU0;
cluster OSSubSort(OU0) -> non empty;
coherence
proof
set A = the OSSubset of OU0;
OSSubSort(A) c= OSSubSort(OU0) by Th18;
hence thesis;
end;
end;
:: new-def for order-sorted
definition
let S1,OU0;
let e be Element of OSSubSort(OU0);
func @e -> OSSubset of OU0 equals
e;
coherence
proof
e in { x where x is Element of SubSort(OU0): x is OrderSortedSet of S1 };
then consider e1 being Element of SubSort(OU0) such that
A1: e = e1 and
A2: e1 is OrderSortedSet of S1;
reconsider e2 = @e1 as OSSubset of OU0 by A2,Def2;
e2 = e by A1;
hence thesis;
end;
end;
:: maybe do another definition of ossort, saying that it contains
:: Elements of subsort which are order-sorted (or ossubsets)
theorem Th19:
for A,B be OSSubset of OU0 holds B in OSSubSort(A) iff B is
opers_closed & OSConstants(OU0) c= B & A c= B
proof
let A, B be OSSubset of OU0;
thus B in OSSubSort(A) implies B is opers_closed & OSConstants(OU0) c= B & A
c= B
proof
assume B in OSSubSort(A);
then
A1: ex B1 being Element of SubSort(A) st B1 = B & B1 is OrderSortedSet of S1;
then Constants(OU0) c= B by MSUALG_2:13;
hence thesis by A1,Th11,MSUALG_2:13;
end;
assume that
A2: B is opers_closed and
A3: OSConstants(OU0) c= B and
A4: A c= B;
Constants(OU0) c= OSConstants(OU0) by Th10;
then Constants(OU0) c= B by A3,PBOOLE:13;
then
A5: B in SubSort(A) by A2,A4,MSUALG_2:13;
B is OrderSortedSet of S1 by Def2;
hence thesis by A5;
end;
theorem Th20:
for B be OSSubset of OU0 holds B in OSSubSort(OU0) iff B is opers_closed
proof
let B be OSSubset of OU0;
A1: B in SubSort(OU0) iff B is opers_closed by MSUALG_2:14;
thus B in OSSubSort(OU0) implies B is opers_closed
proof
assume B in OSSubSort(OU0);
then
ex B1 being Element of SubSort(OU0) st B1 = B & B1 is OrderSortedSet of S1;
hence thesis by MSUALG_2:14;
end;
assume
A2: B is opers_closed;
B is OrderSortedSet of S1 by Def2;
hence thesis by A1,A2;
end;
:: slices of members of OSsubsort
definition
let S1,OU0;
let A be OSSubset of OU0, s be Element of S1;
func OSSubSort(A,s) -> set means
:Def10:
for x be object holds x in it iff ex B
be OSSubset of OU0 st B in OSSubSort(A) & x = B.s;
existence
proof
defpred P[object] means
ex B be OSSubset of OU0 st B in OSSubSort(A) & $1 = B
.s;
set C =bool Union (the Sorts of OU0);
consider X be set such that
A1: for x be object holds x in X iff x in C & P[x] from XBOOLE_0:sch 1;
take X;
A2: C = bool union( rng(the Sorts of OU0)) by CARD_3:def 4;
for x be set holds x in X iff ex B be OSSubset of OU0 st B in
OSSubSort(A) & x = B.s
proof
dom (the Sorts of OU0) = the carrier of S1 by PARTFUN1:def 2;
then (the Sorts of OU0).s in rng (the Sorts of OU0) by FUNCT_1:def 3;
then
A3: (the Sorts of OU0).s c= union( rng (the Sorts of OU0)) by ZFMISC_1:74;
let x be set;
thus x in X implies ex B be OSSubset of OU0 st B in OSSubSort(A) & x = B
.s by A1;
given B be OSSubset of OU0 such that
A4: B in OSSubSort(A) and
A5: x = B.s;
B c= the Sorts of OU0 by PBOOLE:def 18;
then B.s c= (the Sorts of OU0).s;
then x c= union( rng (the Sorts of OU0)) by A5,A3;
hence thesis by A2,A1,A4,A5;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means
ex B be OSSubset of OU0 st B in OSSubSort(A) & $1 = B
.s;
thus for X1,X2 being set st (for x being object holds x in X1 iff P[x]) &
(
for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
theorem Th21:
for A being OSSubset of OU0, s1,s2 being SortSymbol of S1 holds
s1 <= s2 implies OSSubSort(A,s2) is_coarser_than OSSubSort(A,s1)
proof
let A be OSSubset of OU0, s1,s2 be SortSymbol of S1;
assume
A1: s1 <= s2;
for Y being set st Y in OSSubSort(A,s2) ex X being set st X in OSSubSort
(A,s1) & X c= Y
proof
let x be set;
assume x in OSSubSort(A,s2);
then consider B being OSSubset of OU0 such that
A2: B in OSSubSort(A) & x = B.s2 by Def10;
take B.s1;
B is OrderSortedSet of S1 by Def2;
hence thesis by A1,A2,Def10,OSALG_1:def 16;
end;
hence thesis by SETFAM_1:def 3;
end;
theorem Th22:
for A being OSSubset of OU0, s being SortSymbol of S1 holds
OSSubSort(A,s) c= SubSort(A,s)
proof
let A be OSSubset of OU0, s be SortSymbol of S1;
let x be object;
assume x in OSSubSort(A,s);
then
A1: ex B being OSSubset of OU0 st B in OSSubSort(A) & x = B.s by Def10;
OSSubSort(A) c= SubSort(A) by Th16;
hence thesis by A1,MSUALG_2:def 13;
end;
theorem Th23:
for A being OSSubset of OU0, s being SortSymbol of S1 holds (the
Sorts of OU0).s in OSSubSort(A,s)
proof
let A be OSSubset of OU0, s be SortSymbol of S1;
the Sorts of OU0 is ManySortedSubset of the Sorts of OU0 & the Sorts of
OU0 is OrderSortedSet of S1 by OSALG_1:17,PBOOLE:def 18;
then reconsider B = the Sorts of OU0 as OSSubset of OU0 by Def2;
the Sorts of OU0 in OSSubSort(A) by Th17;
then B.s in OSSubSort(A,s) by Def10;
hence thesis;
end;
registration
let S1,OU0;
let A be OSSubset of OU0, s be SortSymbol of S1;
cluster OSSubSort(A,s) -> non empty;
coherence by Th23;
end;
definition
let S1,OU0;
let A be OSSubset of OU0;
func OSMSubSort(A) -> OSSubset of OU0 means
:Def11:
for s be SortSymbol of S1 holds it.s = meet (OSSubSort(A,s));
existence
proof
deffunc F(Element of S1) = meet (OSSubSort(A,$1));
consider f be Function such that
A1: dom f = the carrier of S1 & for s be Element of S1 holds f.s = F(s
) from FUNCT_1:sch 4;
reconsider f as ManySortedSet of (the carrier of S1) by A1,PARTFUN1:def 2
,RELAT_1:def 18;
f c= the Sorts of OU0
proof
reconsider u0 = the Sorts of OU0 as MSSubset of OU0 by PBOOLE:def 18;
let x be object;
assume x in the carrier of S1;
then reconsider s = x as SortSymbol of S1;
A2: f.s = meet (OSSubSort(A,s)) by A1;
u0 is OrderSortedSet of S1 by OSALG_1:17;
then
A3: u0 is OSSubset of OU0 by Def2;
u0 in OSSubSort(A) by Th17;
then (the Sorts of OU0).s in (OSSubSort(A,s)) by A3,Def10;
hence thesis by A2,SETFAM_1:3;
end;
then reconsider f as MSSubset of OU0 by PBOOLE:def 18;
take f;
reconsider f1 = f as ManySortedSet of S1;
for s1,s2 being Element of S1 st s1 <= s2 holds f1.s1 c= f1.s2
proof
let s1,s2 be Element of S1;
assume s1 <= s2;
then
A4: meet OSSubSort(A,s1) c= meet OSSubSort(A,s2) by Th21,SETFAM_1:14;
f1.s1 = meet OSSubSort(A,s1) by A1;
hence thesis by A1,A4;
end;
then f is OrderSortedSet of S1 by OSALG_1:def 16;
hence thesis by A1,Def2;
end;
uniqueness
proof
let W1,W2 be OSSubset of OU0;
assume that
A5: for s be SortSymbol of S1 holds W1.s = meet (OSSubSort(A,s)) and
A6: for s be SortSymbol of S1 holds W2.s = meet (OSSubSort(A,s));
for s be object st s in (the carrier of S1) holds W1.s = W2.s
proof
let s be object;
assume s in (the carrier of S1);
then reconsider s as SortSymbol of S1;
W1.s = meet (OSSubSort(A,s)) by A5;
hence thesis by A6;
end;
hence thesis;
end;
end;
registration
let S1,OU0;
cluster opers_closed for OSSubset of OU0;
existence
proof
set x = the Element of OSSubSort(OU0);
x in { y where y is Element of SubSort(OU0): y is OrderSortedSet of S1 };
then consider x1 being Element of SubSort(OU0) such that
x = x1 and
A1: x1 is OrderSortedSet of S1;
reconsider x2 = x1 as MSSubset of OU0 by MSUALG_2:def 11;
reconsider x3 = x2 as OSSubset of OU0 by A1,Def2;
take x3;
thus thesis by MSUALG_2:def 11;
end;
end;
theorem Th24:
for A be OSSubset of OU0 holds OSConstants(OU0) (\/) A c= OSMSubSort(A)
proof
let A be OSSubset of OU0;
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
A1: for Z be set st Z in OSSubSort(A,s) holds (OSConstants(OU0) (\/) A).s c= Z
proof
let Z be set;
assume Z in OSSubSort(A,s);
then consider B be OSSubset of OU0 such that
A2: B in OSSubSort(A) and
A3: Z = B.s by Def10;
OSConstants(OU0) c= B & A c= B by A2,Th19;
then OSConstants(OU0) (\/) A c= B by PBOOLE:16;
hence thesis by A3;
end;
(OSMSubSort(A)).s = meet (OSSubSort(A,s)) by Def11;
hence thesis by A1,SETFAM_1:5;
end;
theorem
for A be OSSubset of OU0 st OSConstants(OU0) (\/) A is non-empty holds
OSMSubSort(A) is non-empty
proof
let A be OSSubset of OU0;
assume
A1: OSConstants(OU0) (\/) A is non-empty;
now
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
for Z be set st Z in OSSubSort(A,s) holds (OSConstants(OU0) (\/) A).s c= Z
proof
let Z be set;
assume Z in OSSubSort(A,s);
then consider B be OSSubset of OU0 such that
A2: B in OSSubSort(A) and
A3: Z = B.s by Def10;
OSConstants(OU0) c= B & A c= B by A2,Th19;
then OSConstants(OU0) (\/) A c= B by PBOOLE:16;
hence thesis by A3;
end;
then
A4: (OSConstants(OU0) (\/) A).s c= meet(OSSubSort(A,s)) by SETFAM_1:5;
ex x be object st x in (OSConstants(OU0) (\/) A).s by A1,XBOOLE_0:def 1;
hence (OSMSubSort(A)).i is non empty by A4,Def11;
end;
hence thesis;
end;
theorem Th26:
for o be OperSymbol of S1 for A be OSSubset of OU0 for B be
OSSubset of OU0 st B in OSSubSort(A) holds ((OSMSubSort A)# * (the Arity of S1)
).o c= (B# * (the Arity of S1)).o
proof
let o be OperSymbol of S1, A be OSSubset of OU0, B be OSSubset of OU0;
assume
A1: B in OSSubSort(A);
OSMSubSort (A) c= B
proof
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
(OSMSubSort A).s = meet (OSSubSort(A,s)) & B.s in (OSSubSort(A,s)) by A1
,Def10,Def11;
hence thesis by SETFAM_1:3;
end;
hence thesis by MSUALG_2:2;
end;
theorem Th27:
for o be OperSymbol of S1 for A be OSSubset of OU0 for B be
OSSubset of OU0 st B in OSSubSort(A) holds rng (Den(o,OU0)|(((OSMSubSort A)# *
(the Arity of S1)).o)) c= (B * (the ResultSort of S1)).o
proof
let o be OperSymbol of S1;
let A be OSSubset of OU0, B be OSSubset of OU0;
set m = ((OSMSubSort A)# * (the Arity of S1)).o, b = (B# * (the Arity of S1)
).o, d = Den(o,OU0);
assume
A1: B in OSSubSort(A);
then B is opers_closed by Th19;
then B is_closed_on o;
then
A2: rng (d|b) c= (B * (the ResultSort of S1)).o;
b /\ m = m by A1,Th26,XBOOLE_1:28;
then d|m = (d|b)|m by RELAT_1:71;
then rng (d|m) c= rng(d|b) by RELAT_1:70;
hence thesis by A2;
end;
theorem Th28:
for o be OperSymbol of S1 for A be OSSubset of OU0 holds rng ((
Den(o,OU0))|(((OSMSubSort A)# * (the Arity of S1)).o)) c= ((OSMSubSort A) * (
the ResultSort of S1)).o
proof
let o be OperSymbol of S1;
let A be OSSubset of OU0;
let x be object;
assume that
A1: x in rng ((Den(o,OU0))|(((OSMSubSort A)# * (the Arity of S1)).o)) and
A2: not x in ((OSMSubSort A) * (the ResultSort of S1)).o;
set r = the_result_sort_of o;
A3: r = (the ResultSort of S1).o & dom (the ResultSort of S1) = the carrier'
of S1 by FUNCT_2:def 1,MSUALG_1:def 2;
then ((OSMSubSort A) * (the ResultSort of S1)).o = (OSMSubSort A).r by
FUNCT_1:13
.= meet OSSubSort(A,r) by Def11;
then consider X be set such that
A4: X in OSSubSort(A,r) and
A5: not x in X by A2,SETFAM_1:def 1;
consider B be OSSubset of OU0 such that
A6: B in OSSubSort(A) and
A7: B.r = X by A4,Def10;
rng (Den(o,OU0)|(((OSMSubSort A)# * (the Arity of S1)).o)) c= (B * (the
ResultSort of S1)).o by A6,Th27;
then x in (B * (the ResultSort of S1)).o by A1;
hence contradiction by A3,A5,A7,FUNCT_1:13;
end;
theorem Th29:
for A be OSSubset of OU0 holds OSMSubSort(A) is opers_closed & A
c= OSMSubSort(A)
proof
let A be OSSubset of OU0;
thus OSMSubSort(A) is opers_closed
proof
let o1 be Element of the carrier' of S1;
reconsider o = o1 as OperSymbol of S1;
rng ((Den(o,OU0))|(((OSMSubSort A)# * (the Arity of S1)).o)) c= ((
OSMSubSort A) * (the ResultSort of S1)).o by Th28;
hence thesis;
end;
A c= OSConstants(OU0) (\/) A & OSConstants(OU0) (\/) A c= OSMSubSort(A)
by Th24,PBOOLE:14;
hence thesis by PBOOLE:13;
end;
registration
let S1,OU0;
let A be OSSubset of OU0;
cluster OSMSubSort(A) -> opers_closed;
coherence by Th29;
end;
begin :: Operations on Subalgebras of an Order Sorted Algebra.
registration
let S1,OU0;
let A be opers_closed OSSubset of OU0;
cluster OU0|A -> order-sorted;
coherence
proof
set M = MSAlgebra (#A, Opers(OU0,A) qua ManySortedFunction of (A# * the
Arity of S1),(A * the ResultSort of S1)#);
OU0|A = M & A is OrderSortedSet of S1 by Def2,MSUALG_2:def 15;
hence thesis by OSALG_1:17;
end;
end;
registration
let S1,OU0;
let OU1,OU2 be OSSubAlgebra of OU0;
cluster OU1 /\ OU2 -> order-sorted;
coherence
proof
reconsider M1 = (the Sorts of OU1), M2 = (the Sorts of OU2) as
OrderSortedSet of S1 by OSALG_1:17;
M1 (/\) M2 is OrderSortedSet of S1 by Th1;
then the Sorts of (OU1 /\ OU2) is OrderSortedSet of S1 by MSUALG_2:def 16;
hence thesis by OSALG_1:17;
end;
end;
:: generally, GenOSAlg can differ from GenMSAlg, example should be given
definition
let S1,OU0;
let A be OSSubset of OU0;
func GenOSAlg(A) -> strict OSSubAlgebra of OU0 means
:Def12:
A is OSSubset
of it & for OU1 be OSSubAlgebra of OU0 st A is OSSubset of OU1 holds it is
OSSubAlgebra of OU1;
existence
proof
set a = OSMSubSort(A);
reconsider u1 = OU0|a as strict OSSubAlgebra of OU0;
take u1;
A1: u1 = MSAlgebra (# a, Opers(OU0,a)qua ManySortedFunction of (a# * the
Arity of S1),(a * the ResultSort of S1)#) by MSUALG_2:def 15;
A2: A is OrderSortedSet of S1 by Def2;
A c= a by Th29;
then A is MSSubset of u1 by A1,PBOOLE:def 18;
hence A is OSSubset of u1 by A2,Def2;
let U2 be OSSubAlgebra of OU0;
reconsider B1 = the Sorts of U2 as MSSubset of OU0 by MSUALG_2:def 9;
B1 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B1 as OSSubset of OU0 by Def2;
assume A is OSSubset of U2;
then
A3: B is opers_closed & A c= B by MSUALG_2:def 9,PBOOLE:def 18;
OSConstants(OU0) is OSSubset of U2 by Th13;
then OSConstants(OU0) c= B by PBOOLE:def 18;
then
A4: B in OSSubSort(A) by A3,Th19;
the Sorts of u1 c= the Sorts of U2
proof
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
(the Sorts of u1).s = meet OSSubSort(A,s) & B.s in OSSubSort(A,s)
by A1,A4,Def10,Def11;
hence thesis by SETFAM_1:3;
end;
hence thesis by MSUALG_2:8;
end;
uniqueness
proof
let W1,W2 be strict OSSubAlgebra of OU0;
assume A is OSSubset of W1 & ( for U1 be OSSubAlgebra of OU0 st A is
OSSubset of U1 holds W1 is OSSubAlgebra of U1)& A is OSSubset of W2 & for U2 be
OSSubAlgebra of OU0 st A is OSSubset of U2 holds W2 is OSSubAlgebra of U2;
then W1 is strict OSSubAlgebra of W2 & W2 is strict OSSubAlgebra of W1;
hence thesis by MSUALG_2:7;
end;
end;
:: this should rather be a definition, but I want to keep
:: compatibility of the definition with MSUALG_2
theorem Th30:
for A be OSSubset of OU0 holds GenOSAlg(A) = OU0 | OSMSubSort(A)
& the Sorts of GenOSAlg(A) = OSMSubSort(A)
proof
let A be OSSubset of OU0;
set a = OSMSubSort(A);
reconsider u1 = OU0|a as strict OSSubAlgebra of OU0;
A1: u1 = MSAlgebra (# a, Opers(OU0,a)qua ManySortedFunction of (a# * the
Arity of S1),(a * the ResultSort of S1)#) by MSUALG_2:def 15;
A2: A c= a by Th29;
A3: A is OrderSortedSet of S1 by Def2;
A4: A is OSSubset of u1 & for OU1 be OSSubAlgebra of OU0 st A is OSSubset of
OU1 holds u1 is OSSubAlgebra of OU1
proof
A is MSSubset of u1 by A2,A1,PBOOLE:def 18;
hence A is OSSubset of u1 by A3,Def2;
let U2 be OSSubAlgebra of OU0;
reconsider B1 = the Sorts of U2 as MSSubset of OU0 by MSUALG_2:def 9;
B1 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B1 as OSSubset of OU0 by Def2;
assume A is OSSubset of U2;
then
A5: B is opers_closed & A c= B by MSUALG_2:def 9,PBOOLE:def 18;
OSConstants(OU0) is OSSubset of U2 by Th13;
then OSConstants(OU0) c= B by PBOOLE:def 18;
then
A6: B in OSSubSort(A) by A5,Th19;
the Sorts of u1 c= the Sorts of U2
proof
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
(the Sorts of u1).s = meet OSSubSort(A,s) & B.s in OSSubSort(A,s)
by A1,A6,Def10,Def11;
hence thesis by SETFAM_1:3;
end;
hence thesis by MSUALG_2:8;
end;
hence GenOSAlg(A) = OU0|a by Def12;
thus thesis by A1,A4,Def12;
end;
:: this could simplify some proofs in MSUALG_2, I need it anyway
theorem Th31:
for S be non void non empty ManySortedSign for U0 be MSAlgebra
over S for A be MSSubset of U0 holds GenMSAlg(A) = U0 | MSSubSort(A) & the
Sorts of GenMSAlg(A) = MSSubSort(A)
proof
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
set a = MSSubSort(A);
reconsider u1 = U0|a as strict MSSubAlgebra of U0;
A1: u1 = MSAlgebra (# a, Opers(U0,a)qua ManySortedFunction of (a# * the
Arity of S),(a * the ResultSort of S)#) by MSUALG_2:20,def 15;
A2: A c= a by MSUALG_2:20;
A3: A is MSSubset of u1 & for U1 be MSSubAlgebra of U0 st A is MSSubset of
U1 holds u1 is MSSubAlgebra of U1
proof
thus A is MSSubset of u1 by A2,A1,PBOOLE:def 18;
let U2 be MSSubAlgebra of U0;
reconsider B = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def 9;
Constants(U0) is MSSubset of U2 by MSUALG_2:10;
then
A4: Constants(U0) c= B by PBOOLE:def 18;
assume A is MSSubset of U2;
then B is opers_closed & A c= B by MSUALG_2:def 9,PBOOLE:def 18;
then
A5: B in SubSort(A) by A4,MSUALG_2:13;
the Sorts of u1 c= the Sorts of U2
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
(the Sorts of u1).s = meet SubSort(A,s) & B.s in SubSort(A,s) by A1,A5,
MSUALG_2:def 13,def 14;
hence thesis by SETFAM_1:3;
end;
hence thesis by MSUALG_2:8;
end;
hence GenMSAlg(A) = U0|a by MSUALG_2:def 17;
thus thesis by A1,A3,MSUALG_2:def 17;
end;
theorem Th32:
for A being OSSubset of OU0 holds the Sorts of GenMSAlg(A) c=
the Sorts of GenOSAlg(A)
proof
let A be OSSubset of OU0;
set GM = GenMSAlg(A), GO = GenOSAlg(A);
let i be object;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
the Sorts of GM = MSSubSort(A) by Th31;
then
A1: (the Sorts of GM).s = meet SubSort(A,s) by MSUALG_2:def 14;
the Sorts of GO = OSMSubSort(A) by Th30;
then (the Sorts of GO).s = meet OSSubSort(A,s) by Def11;
hence thesis by A1,Th22,SETFAM_1:6;
end;
theorem
for A being OSSubset of OU0 holds GenMSAlg(A) is MSSubAlgebra of
GenOSAlg(A) by Th32,MSUALG_2:8;
theorem Th34:
for OU0 being strict OSAlgebra of S1 for B being OSSubset of OU0
st B = the Sorts of OU0 holds GenOSAlg(B) = OU0
proof
let OU0 be strict OSAlgebra of S1;
let B be OSSubset of OU0;
assume B = the Sorts of OU0;
then
A1: GenMSAlg(B) = OU0 by MSUALG_2:21;
GenMSAlg(B) is strict MSSubAlgebra of GenOSAlg(B) by Th32,MSUALG_2:8;
hence thesis by A1,MSUALG_2:7;
end;
theorem Th35:
for OU1 being strict OSSubAlgebra of OU0, B being OSSubset of
OU0 st B = the Sorts of OU1 holds GenOSAlg(B) = OU1
proof
let OU1 be strict OSSubAlgebra of OU0;
let B be OSSubset of OU0;
set W = GenOSAlg(B);
assume
A1: B = the Sorts of OU1;
then
A2: B is MSSubset of OU1 by PBOOLE:def 18;
B is OSSubset of W by Def12;
then the Sorts of OU1 c= the Sorts of W by A1,PBOOLE:def 18;
then
A3: OU1 is strict MSSubAlgebra of W by MSUALG_2:8;
B is OrderSortedSet of S1 by Def2;
then B is OSSubset of OU1 by A2,Def2;
then W is strict OSSubAlgebra of OU1 by Def12;
hence thesis by A3,MSUALG_2:7;
end;
theorem Th36:
for U0 be non-empty OSAlgebra of S1, U1 be OSSubAlgebra of U0
holds GenOSAlg(OSConstants(U0)) /\ U1 = GenOSAlg(OSConstants(U0))
proof
let U0 be non-empty OSAlgebra of S1, U1 be OSSubAlgebra of U0;
set C = OSConstants(U0), G = GenOSAlg(C);
C is OSSubset of U1 by Th13;
then G is strict OSSubAlgebra of U1 by Def12;
then the Sorts of G is MSSubset of U1 by MSUALG_2:def 9;
then the Sorts of ( G /\ U1) = (the Sorts of G) (/\) (the Sorts of U1) & the
Sorts of G c= the Sorts of U1 by MSUALG_2:def 16,PBOOLE:def 18;
then the Sorts of ( G /\ U1) = the Sorts of G by PBOOLE:23;
hence thesis by MSUALG_2:9;
end;
definition
let S1;
let U0 be non-empty OSAlgebra of S1, U1,U2 be OSSubAlgebra of U0;
func U1 "\/"_os U2 -> strict OSSubAlgebra of U0 means
:Def13:
for A be
OSSubset of U0 st A = (the Sorts of U1) (\/) (the Sorts of U2) holds it =
GenOSAlg(A);
existence
proof
set B=(the Sorts of U1) (\/) (the Sorts of U2);
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 9;
then
A1: the Sorts of U2 c=the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 9;
then the Sorts of U1 c=the Sorts of U0 by PBOOLE:def 18;
then B c= the Sorts of U0 by A1,PBOOLE:16;
then reconsider B as MSSubset of U0 by PBOOLE:def 18;
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of
S1 by OSALG_1:17;
B = B1 (\/) B2;
then B is OrderSortedSet of S1 by Th2;
then reconsider B0 = B as OSSubset of U0 by Def2;
take GenOSAlg(B0);
thus thesis;
end;
uniqueness
proof
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of
S1 by OSALG_1:17;
set B=(the Sorts of U1) (\/) (the Sorts of U2);
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 9;
then
A2: the Sorts of U2 c=the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 9;
then the Sorts of U1 c=the Sorts of U0 by PBOOLE:def 18;
then B c= the Sorts of U0 by A2,PBOOLE:16;
then reconsider B as MSSubset of U0 by PBOOLE:def 18;
let W1,W2 be strict OSSubAlgebra of U0;
assume that
A3: for A be OSSubset of U0 st A = (the Sorts of U1) (\/) (the Sorts of
U2) holds W1 = GenOSAlg(A) and
A4: for A be OSSubset of U0 st A = (the Sorts of U1) (\/) (the Sorts of
U2) holds W2 = GenOSAlg(A);
B = B1 (\/) B2;
then B is OrderSortedSet of S1 by Th2;
then reconsider B0 = B as OSSubset of U0 by Def2;
W1 = GenOSAlg(B0) by A3;
hence thesis by A4;
end;
end;
theorem Th37:
for U0 be non-empty OSAlgebra of S1, U1 be OSSubAlgebra of U0, A
,B be OSSubset of U0 st B = A (\/) the Sorts of U1
holds GenOSAlg(A) "\/"_os U1 = GenOSAlg(B)
proof
let U0 be non-empty OSAlgebra of S1, U1 be OSSubAlgebra of U0, A,B be
OSSubset of U0;
assume
A1: B = A (\/) the Sorts of U1;
reconsider u1m = the Sorts of U1, am = the Sorts of GenOSAlg(A) as MSSubset
of U0 by MSUALG_2:def 9;
A2: the Sorts of U1 is OrderSortedSet of S1 & the Sorts of GenOSAlg(A) is
OrderSortedSet of S1 by OSALG_1:17;
then reconsider u1 = u1m, a = am as OSSubset of U0 by Def2;
a c= the Sorts of U0 & u1 c= the Sorts of U0 by PBOOLE:def 18;
then a (\/) u1 c= the Sorts of U0 by PBOOLE:16;
then reconsider b=a (\/) u1 as MSSubset of U0 by PBOOLE:def 18;
A3: a (\/) u1 is OrderSortedSet of S1 by A2,Th2;
then reconsider b as OSSubset of U0 by Def2;
A4: (GenOSAlg(A) "\/"_os U1) = GenOSAlg(b) by Def13;
then a (\/) u1 is OSSubset of (GenOSAlg(A)"\/"_os U1) by Def12;
then
A5: a (\/) u1 c=the Sorts of (GenOSAlg(A)"\/"_os U1) by PBOOLE:def 18;
A is OSSubset of GenOSAlg(A) by Def12;
then
A6: A c= the Sorts of GenOSAlg(A) by PBOOLE:def 18;
then A (\/) u1 c= a (\/) u1 by PBOOLE:20;
then B c=the Sorts of (GenOSAlg(A)"\/"_os U1) by A1,A5,PBOOLE:13;
then
A7: B is MSSubset of (GenOSAlg(A)"\/"_os U1) by PBOOLE:def 18;
A8: A is OrderSortedSet of S1 by Def2;
A9: the Sorts of (GenOSAlg(A) /\ GenOSAlg(B)) = (the Sorts of GenOSAlg(A))
(/\) (the Sorts of GenOSAlg(B)) by MSUALG_2:def 16;
B is OSSubset of GenOSAlg(B) by Def12;
then
A10: B c= the Sorts of GenOSAlg(B) by PBOOLE:def 18;
A c= B by A1,PBOOLE:14;
then A c= the Sorts of GenOSAlg(B) by A10,PBOOLE:13;
then A c= (the Sorts of GenOSAlg(A)) (/\) (the Sorts of GenOSAlg(B))
by A6,PBOOLE:17;
then A is MSSubset of (GenOSAlg(A) /\ GenOSAlg(B)) by A9,PBOOLE:def 18;
then A is OSSubset of (GenOSAlg(A) /\ GenOSAlg(B)) by A8,Def2;
then GenOSAlg(A) is OSSubAlgebra of (GenOSAlg(A) /\ GenOSAlg(B)) by Def12;
then a is MSSubset of (GenOSAlg(A) /\ GenOSAlg(B)) by MSUALG_2:def 9;
then
A11: a c= (the Sorts of GenOSAlg(A)) (/\) (the Sorts of GenOSAlg(B)) by A9,
PBOOLE:def 18;
(the Sorts of GenOSAlg(A)) (/\) (the Sorts of GenOSAlg(B)) c= a by PBOOLE:15;
then a= (the Sorts of GenOSAlg(A)) (/\) (the Sorts of GenOSAlg(B)) by A11,
PBOOLE:146;
then
A12: a c= the Sorts of GenOSAlg(B) by PBOOLE:15;
u1 c= B by A1,PBOOLE:14;
then u1 c= the Sorts of GenOSAlg(B) by A10,PBOOLE:13;
then b c= the Sorts of GenOSAlg(B) by A12,PBOOLE:16;
then b is MSSubset of GenOSAlg(B) by PBOOLE:def 18;
then b is OSSubset of GenOSAlg(B) by A3,Def2;
then
A13: GenOSAlg(b) is strict OSSubAlgebra of GenOSAlg(B) by Def12;
B is OrderSortedSet of S1 by Def2;
then B is OSSubset of (GenOSAlg(A)"\/"_os U1) by A7,Def2;
then GenOSAlg(B) is strict OSSubAlgebra of (GenOSAlg(A)"\/"_os U1) by Def12;
hence thesis by A4,A13,MSUALG_2:7;
end;
theorem Th38:
for U0 be non-empty OSAlgebra of S1, U1 be OSSubAlgebra of U0, B
be OSSubset of U0 st B = the Sorts of U0 holds GenOSAlg(B) "\/"_os U1 =
GenOSAlg(B)
proof
let U0 be non-empty OSAlgebra of S1, U1 be OSSubAlgebra of U0, B be OSSubset
of U0;
A1: the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 9;
assume B = the Sorts of U0;
then the Sorts of U1 c= B by A1,PBOOLE:def 18;
then B (\/) the Sorts of U1 = B by PBOOLE:22;
hence thesis by Th37;
end;
theorem Th39:
for U0 being non-empty OSAlgebra of S1, U1,U2 be OSSubAlgebra of
U0 holds U1 "\/"_os U2 = U2 "\/"_os U1
proof
let U0 be non-empty OSAlgebra of S1, U1,U2 be OSSubAlgebra of U0;
reconsider u1= the Sorts of U1, u2= the Sorts of U2 as MSSubset of U0 by
MSUALG_2:def 9;
u1 c= the Sorts of U0 & u2 c= the Sorts of U0 by PBOOLE:def 18;
then u1 (\/) u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A1 = u1 (\/) u2 as MSSubset of U0 by PBOOLE:def 18;
u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 by OSALG_1:17;
then A1 is OrderSortedSet of S1 by Th2;
then reconsider A = A1 as OSSubset of U0 by Def2;
U1 "\/"_os U2 = GenOSAlg(A) by Def13;
hence thesis by Def13;
end;
theorem Th40:
for U0 be non-empty OSAlgebra of S1, U1,U2 be strict
OSSubAlgebra of U0 holds U1 /\ (U1"\/"_os U2) = U1
proof
let U0 be non-empty OSAlgebra of S1, U1,U2 be strict OSSubAlgebra of U0;
reconsider u1= the Sorts of U1,u2 =the Sorts of U2 as MSSubset of U0 by
MSUALG_2:def 9;
reconsider u112=the Sorts of(U1 /\ (U1"\/"_os U2)) as MSSubset of U0 by
MSUALG_2:def 9;
A1: the Charact of (U1/\(U1"\/"_os U2))=Opers(U0,u112) by MSUALG_2:def 16;
u1 c= the Sorts of U0 & u2 c= the Sorts of U0 by PBOOLE:def 18;
then u1 (\/) u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A= u1 (\/) u2 as MSSubset of U0 by PBOOLE:def 18;
u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 by OSALG_1:17;
then A is OrderSortedSet of S1 by Th2;
then reconsider A as OSSubset of U0 by Def2;
A2: the Sorts of (U1 /\(U1"\/"_os U2))= (the Sorts of U1)(/\)(the Sorts of(U1
"\/"_os U2)) by MSUALG_2:def 16;
U1"\/"_os U2 = GenOSAlg(A) by Def13;
then A is OSSubset of U1"\/"_os U2 by Def12;
then
A3: A c= the Sorts of (U1 "\/"_os U2) by PBOOLE:def 18;
the Sorts of U1 c= A by PBOOLE:14;
then the Sorts of U1 c= the Sorts of (U1"\/"_os U2) by A3,PBOOLE:13;
then
A4: the Sorts of U1 c=the Sorts of (U1 /\(U1"\/"_os U2)) by A2,PBOOLE:17;
the Sorts of (U1 /\(U1"\/"_os U2)) c= the Sorts of U1 by A2,PBOOLE:15;
then the Sorts of (U1 /\(U1"\/"_os U2)) = the Sorts of U1 by A4,PBOOLE:146;
hence thesis by A1,MSUALG_2:def 9;
end;
theorem Th41:
for U0 be non-empty OSAlgebra of S1, U1,U2 be strict
OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2
proof
let U0 be non-empty OSAlgebra of S1, U1,U2 be strict OSSubAlgebra of U0;
reconsider u12= the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of
U0 by MSUALG_2:def 9;
A1: u12 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider u12, u2 as OSSubset of U0 by Def2;
u12 c= the Sorts of U0 & u2 c= the Sorts of U0 by PBOOLE:def 18;
then u12 (\/) u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A= u12 (\/) u2 as MSSubset of U0 by PBOOLE:def 18;
A is OrderSortedSet of S1 by A1,Th2;
then reconsider A= u12 (\/) u2 as OSSubset of U0 by Def2;
u12 = (the Sorts of U1) (/\) (the Sorts of U2) by MSUALG_2:def 16;
then u12 c= u2 by PBOOLE:15;
then
A2: A = u2 by PBOOLE:22;
(U1 /\ U2) "\/"_os U2 = GenOSAlg(A) by Def13;
hence thesis by A2,Th35;
end;
begin :: The Lattice of SubAlgebras of an Order Sorted Algebra.
:: ossub, ossubalgebra
definition
let S1,OU0;
func OSSub(OU0) -> set means
:Def14:
for x being object holds x in it iff x is strict OSSubAlgebra of OU0;
existence
proof
set X = the set of all GenOSAlg(@A) where A is Element of OSSubSort(OU0);
take X;
let x be object;
thus x in X implies x is strict OSSubAlgebra of OU0
proof
assume x in X;
then ex A be Element of OSSubSort(OU0) st x = GenOSAlg(@A);
hence thesis;
end;
assume x is strict OSSubAlgebra of OU0;
then reconsider a = x as strict OSSubAlgebra of OU0;
reconsider A = the Sorts of a as OSSubset of OU0 by Th5;
A is opers_closed by Th5;
then reconsider h = A as Element of OSSubSort(OU0) by Th20;
a = GenOSAlg(@h) by Th35;
hence thesis;
end;
uniqueness
proof
defpred P[object] means $1 is strict OSSubAlgebra of OU0;
thus for X1,X2 being set st
(for x being object holds x in X1 iff P[x]) & (
for x being object holds x in X2 iff P[x])
holds X1 = X2 from XBOOLE_0:sch 3;
end;
end;
theorem Th42:
OSSub(OU0) c= MSSub(OU0)
proof
let x be object;
assume x in OSSub(OU0);
then x is strict MSSubAlgebra of OU0 by Def14;
hence thesis by MSUALG_2:def 19;
end;
registration
let S be OrderSortedSign, U0 be OSAlgebra of S;
cluster OSSub(U0) -> non empty;
coherence
proof
set x = the strict OSSubAlgebra of U0;
x in OSSub U0 by Def14;
hence thesis;
end;
end;
definition
let S1,OU0;
redefine func OSSub(OU0) -> Subset of MSSub(OU0); :: redefines OSSub (OSALG_2, definition)
coherence by Th42;
end;
:: maybe show that e.g. for TrivialOSA(S,z,z1), OSSub(U0) is
:: proper subset of MSSub(U0), to have some counterexamples
definition
let S1;
let U0 be non-empty OSAlgebra of S1;
func OSAlg_join(U0) -> BinOp of (OSSub(U0)) means
:Def15:
for x,y be Element
of OSSub(U0) holds for U1,U2 be strict OSSubAlgebra of U0 st x = U1 & y = U2
holds it.(x,y) = U1 "\/"_os U2;
existence
proof
defpred P[(Element of OSSub(U0)),(Element of OSSub(U0)), set] means for U1
,U2 be strict OSSubAlgebra of U0 st $1=U1 & $2=U2 holds $3=U1 "\/"_os U2;
A1: for x,y being Element of OSSub(U0) ex z being Element of OSSub(U0) st
P[x,y,z]
proof
let x,y be Element of OSSub(U0);
reconsider U1=x, U2=y as strict OSSubAlgebra of U0 by Def14;
reconsider z =U1"\/"_os U2 as Element of OSSub(U0) by Def14;
take z;
thus thesis;
end;
consider o be BinOp of OSSub(U0) such that
A2: for a,b be Element of OSSub(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 (OSSub(U0));
assume that
A3: for x,y be Element of OSSub(U0) holds for U1,U2 be strict
OSSubAlgebra of U0 st x=U1 & y=U2 holds o1.(x,y)=U1 "\/"_os U2 and
A4: for x,y be Element of OSSub(U0) holds for U1,U2 be strict
OSSubAlgebra of U0 st x=U1 & y=U2 holds o2.(x,y) = U1 "\/"_os U2;
for x be Element of OSSub(U0) for y be Element of OSSub(U0) holds o1.(
x,y) = o2.(x,y)
proof
let x,y be Element of OSSub(U0);
reconsider U1=x,U2=y as strict OSSubAlgebra of U0 by Def14;
o1.(x,y) = U1"\/"_os U2 by A3;
hence thesis by A4;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let S1;
let U0 be non-empty OSAlgebra of S1;
func OSAlg_meet(U0) -> BinOp of (OSSub(U0)) means
:Def16:
for x,y be Element
of OSSub(U0) holds for U1,U2 be strict OSSubAlgebra of U0 st x = U1 & y = U2
holds it.(x,y) = U1 /\ U2;
existence
proof
defpred P[(Element of OSSub(U0)),(Element of OSSub(U0)), set] means for U1
,U2 be strict OSSubAlgebra of U0 st $1=U1 & $2=U2 holds $3=U1 /\ U2;
A1: for x,y being Element of OSSub(U0) ex z being Element of OSSub(U0) st
P[x,y,z]
proof
let x,y be Element of OSSub(U0);
reconsider U1=x, U2=y as strict OSSubAlgebra of U0 by Def14;
reconsider z =U1 /\ U2 as Element of OSSub(U0) by Def14;
take z;
thus thesis;
end;
consider o be BinOp of OSSub(U0) such that
A2: for a,b be Element of OSSub(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 OSSub(U0);
assume that
A3: for x,y be Element of OSSub(U0) holds for U1,U2 be strict
OSSubAlgebra of U0 st x=U1 & y=U2 holds o1.(x,y)=U1 /\ U2 and
A4: for x,y be Element of OSSub(U0) holds for U1,U2 be strict
OSSubAlgebra of U0 st x=U1 & y=U2 holds o2.(x,y) = U1 /\ U2;
for x be Element of OSSub(U0) for y be Element of OSSub(U0) holds o1.(
x,y) = o2.(x,y)
proof
let x,y be Element of OSSub(U0);
reconsider U1=x,U2=y as strict OSSubAlgebra 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 Th43:
for U0 being non-empty OSAlgebra of S1 for x,y being Element of
OSSub(U0) holds (OSAlg_meet(U0)).(x,y) = (MSAlg_meet(U0)).(x,y)
proof
let U0 be non-empty OSAlgebra of S1;
let x,y be Element of OSSub(U0);
x is strict OSSubAlgebra of U0 & y is strict OSSubAlgebra of U0 by Def14;
then consider U1,U2 being strict OSSubAlgebra of U0 such that
A1: x = U1 & y = U2;
(OSAlg_meet(U0)).(x,y) = U1 /\ U2 by A1,Def16
.= (MSAlg_meet(U0)).(x,y) by A1,MSUALG_2:def 21;
hence thesis;
end;
reserve U0 for non-empty OSAlgebra of S1;
theorem Th44:
OSAlg_join(U0) is commutative
proof
set o = OSAlg_join(U0);
for x,y be Element of OSSub(U0) holds o.(x,y)=o.(y,x)
proof
let x,y be Element of OSSub(U0);
reconsider U1=x,U2=y as strict OSSubAlgebra of U0 by Def14;
set B=(the Sorts of U1) (\/) (the Sorts of U2);
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 9;
then
A1: the Sorts of U2 c=the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 9;
then the Sorts of U1 c=the Sorts of U0 by PBOOLE:def 18;
then B c= the Sorts of U0 by A1,PBOOLE:16;
then
A2: B is MSSubset of U0 by PBOOLE:def 18;
the Sorts of U1 is OrderSortedSet of S1 & the Sorts of U2 is
OrderSortedSet of S1 by OSALG_1:17;
then B is OrderSortedSet of S1 by Th2;
then reconsider B as OSSubset of U0 by A2,Def2;
A3: U1 "\/"_os U2 = GenOSAlg(B) by Def13;
o.(x,y) = U1 "\/"_os U2 & o.(y,x) = U2 "\/"_os U1 by Def15;
hence thesis by A3,Def13;
end;
hence thesis by BINOP_1:def 2;
end;
theorem Th45:
OSAlg_join(U0) is associative
proof
set o = OSAlg_join(U0);
for x,y,z be Element of OSSub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
proof
let x,y,z be Element of OSSub(U0);
reconsider U1=x,U2=y,U3=z as strict OSSubAlgebra of U0 by Def14;
set B=(the Sorts of U1) (\/) ((the Sorts of U2) (\/) (the Sorts of U3));
A1: (the Sorts of U2) is OrderSortedSet of S1 by OSALG_1:17;
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 9;
then
A2: the Sorts of U2 c=the Sorts of U0 by PBOOLE:def 18;
the Sorts of U3 is MSSubset of U0 by MSUALG_2:def 9;
then the Sorts of U3 c=the Sorts of U0 by PBOOLE:def 18;
then
A3: (the Sorts of U2) (\/) (the Sorts of U3) c= the Sorts of U0
by A2,PBOOLE:16;
then reconsider
C1 =(the Sorts of U2) (\/) (the Sorts of U3) as MSSubset of U0 by
PBOOLE:def 18;
(the Sorts of U3) is OrderSortedSet of S1 by OSALG_1:17;
then
A4: (the Sorts of U2) (\/) (the Sorts of U3) is OrderSortedSet of S1 by A1,Th2;
then reconsider C = C1 as OSSubset of U0 by Def2;
A5: (the Sorts of U1) is OrderSortedSet of S1 by OSALG_1:17;
then
A6: B is OrderSortedSet of S1 by A4,Th2;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 9;
then
A7: the Sorts of U1 c=the Sorts of U0 by PBOOLE:def 18;
then (the Sorts of U1) (\/) (the Sorts of U2) c= the Sorts of U0 by A2,
PBOOLE:16;
then reconsider
D1=(the Sorts of U1) (\/) (the Sorts of U2) as MSSubset of U0 by
PBOOLE:def 18;
o.(y,z)=U2"\/"_os U3 by Def15;
then
A8: o.(x,o.(y,z)) = U1 "\/"_os (U2"\/"_os U3) by Def15;
(the Sorts of U1) (\/) (the Sorts of U2) is OrderSortedSet of S1
by A5,A1,Th2;
then reconsider D = D1 as OSSubset of U0 by Def2;
A9: o.(x,y)=U1"\/"_os U2 by Def15;
B c= the Sorts of U0 by A7,A3,PBOOLE:16;
then B is MSSubset of U0 by PBOOLE:def 18;
then reconsider B as OSSubset of U0 by A6,Def2;
A10: B= D (\/) (the Sorts of U3) by PBOOLE:28;
A11: (U1"\/"_os U2)"\/"_os U3 = GenOSAlg(D)"\/"_os U3 by Def13
.= GenOSAlg(B) by A10,Th37;
U1 "\/"_os (U2 "\/"_os U3) = U1 "\/"_os (GenOSAlg(C)) by Def13
.= (GenOSAlg(C)) "\/"_os U1 by Th39
.= GenOSAlg(B) by Th37;
hence thesis by A9,A8,A11,Def15;
end;
hence thesis by BINOP_1:def 3;
end;
theorem Th46:
OSAlg_meet(U0) is commutative
proof
set o = OSAlg_meet(U0);
set m = MSAlg_meet(U0);
A1: m is commutative by MSUALG_2:31;
for x,y be Element of OSSub(U0) holds o.(x,y)=o.(y,x)
proof
let x,y be Element of OSSub(U0);
o.(x,y) = m.(x,y) by Th43
.= m.(y,x) by A1,BINOP_1:def 2
.= o.(y,x) by Th43;
hence thesis;
end;
hence thesis by BINOP_1:def 2;
end;
theorem Th47:
OSAlg_meet(U0) is associative
proof
set o = OSAlg_meet(U0);
set m = MSAlg_meet(U0);
A1: m is associative by MSUALG_2:32;
for x,y,z be Element of OSSub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
proof
let x,y,z be Element of OSSub(U0);
A2: o.(x,y) = m.(x,y) by Th43;
o.(y,z) = m.(y,z) by Th43;
then o.(x,o.(y,z)) = m.(x,m.(y,z)) by Th43
.= m.(m.(x,y),z) by A1,BINOP_1:def 3
.= o.(o.(x,y),z) by A2,Th43;
hence thesis;
end;
hence thesis by BINOP_1:def 3;
end;
definition
let S1;
let U0 be non-empty OSAlgebra of S1;
func OSSubAlLattice(U0) -> strict Lattice equals
LattStr (# OSSub(U0),
OSAlg_join(U0), OSAlg_meet(U0) #);
coherence
proof
set L = LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #);
A1: for a,b,c being Element of L holds a"\/" (b"\/" c) = (a"\/" b)"\/" c
by Th45,BINOP_1:def 3;
A2: for a,b being Element of L holds a"/\"b = b"/\"a
by Th46,BINOP_1:def 2;
A3: 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 OSSub(U0);
(OSAlg_meet(U0)).(x,(OSAlg_join(U0)).(x,y))= x
proof
reconsider U1= x,U2=y as strict OSSubAlgebra of U0 by Def14;
(OSAlg_join(U0)).(x,y) = U1"\/"_os U2 by Def15;
hence (OSAlg_meet(U0)).(x,(OSAlg_join(U0)).(x,y)) = (U1 /\( U1"\/"_os
U2)) by Def16
.=x by Th40;
end;
hence thesis;
end;
A4: 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 OSSub(U0);
(OSAlg_join(U0)).((OSAlg_meet(U0)).(x,y),y)= y
proof
reconsider U1= x,U2=y as strict OSSubAlgebra of U0 by Def14;
(OSAlg_meet(U0)).(x,y) = U1 /\ U2 by Def16;
hence (OSAlg_join(U0)).((OSAlg_meet(U0)).(x,y),y) = ((U1 /\ U2)"\/"_os
U2) by Def15
.=y by Th41;
end;
hence thesis;
end;
A5: for a,b,c being Element of L holds a"/\"(b"/\"c) = (a"/\"b)"/\"c
by Th47,BINOP_1:def 3;
for a,b being Element of L holds (a "\/" b) = (b "\/" a)
by Th44,BINOP_1:def 2;
then L is strict join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A1,A4,A2,A5,A3;
hence thesis;
end;
end;
theorem Th48:
for U0 be non-empty OSAlgebra of S1 holds OSSubAlLattice(U0) is bounded
proof
let U0 be non-empty OSAlgebra of S1;
set L = OSSubAlLattice(U0);
thus L is lower-bounded
proof
set C = OSConstants(U0);
reconsider G = GenOSAlg(C) as Element of OSSub(U0) by Def14;
reconsider G1 = G as Element of L;
take G1;
let a be Element of L;
reconsider a1 = a as Element of OSSub(U0);
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "/\" a = GenOSAlg(C) /\ a2 by Def16
.= G1 by Th36;
hence thesis;
end;
thus L is upper-bounded
proof
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
the Sorts of U0 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B as OSSubset of U0 by Def2;
reconsider G = GenOSAlg(B) as Element of OSSub(U0) by Def14;
reconsider G1 = G as Element of L;
take G1;
let a be Element of L;
reconsider a1 = a as Element of OSSub(U0);
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1"\/" a = GenOSAlg(B)"\/"_os a2 by Def15
.= G1 by Th38;
hence thesis;
end;
end;
registration
let S1;
let U0 be non-empty OSAlgebra of S1;
cluster OSSubAlLattice(U0) -> bounded;
coherence by Th48;
end;
theorem
for U0 be non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice(U0))
= GenOSAlg(OSConstants(U0))
proof
let U0 be non-empty OSAlgebra of S1;
set C = OSConstants(U0);
reconsider G = GenOSAlg(C) as Element of OSSub(U0) by Def14;
set L = OSSubAlLattice(U0);
reconsider G1 = G as Element of L;
now
let a be Element of L;
reconsider a1 = a as Element of OSSub(U0);
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "/\" a = GenOSAlg(C) /\ a2 by Def16
.= G1 by Th36;
hence a "/\" G1 = G1;
end;
hence thesis by LATTICES:def 16;
end;
theorem Th50:
for U0 be non-empty OSAlgebra of S1, B be OSSubset of U0 st B =
the Sorts of U0 holds Top (OSSubAlLattice(U0)) = GenOSAlg(B)
proof
let U0 be non-empty OSAlgebra of S1, B be OSSubset of U0;
reconsider G = GenOSAlg(B) as Element of OSSub(U0) by Def14;
set L = OSSubAlLattice(U0);
reconsider G1 = G as Element of L;
assume
A1: B = the Sorts of U0;
now
let a be Element of L;
reconsider a1 = a as Element of OSSub(U0);
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1"\/" a = GenOSAlg(B)"\/"_os a2 by Def15
.= G1 by A1,Th38;
hence a "\/" G1 = G1;
end;
hence thesis by LATTICES:def 17;
end;
theorem
for U0 be strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice(
U0)) = U0
proof
let U0 be strict non-empty OSAlgebra of S1;
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
B is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = the Sorts of U0 as OSSubset of U0 by Def2;
thus Top (OSSubAlLattice(U0)) = GenOSAlg(B) by Th50
.= U0 by Th34;
end;