Copyright (c) 2002 Association of Mizar Users
environ
vocabulary FUNCT_1, RELAT_1, PBOOLE, ZF_REFLE, BOOLE, CARD_3, AMI_1, MSUALG_1,
UNIALG_2, TDGROUP, QC_LANG1, PRALG_1, PROB_1, TARSKI, SETFAM_1, LATTICES,
BINOP_1, MSUALG_2, OSALG_1, ORDERS_1, SEQM_3, OSALG_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
SETFAM_1, LATTICES, BINOP_1, PROB_1, CARD_3, MBOOLEAN, PBOOLE, MSUALG_1,
ORDERS_1, MSUALG_2, YELLOW18, OSALG_1;
constructors MBOOLEAN, PROB_1, ORDERS_3, OSALG_1, YELLOW18, MSUALG_2;
clusters FUNCT_1, LATTICES, MSUALG_1, RELSET_1, STRUCT_0, RLSUB_2, SUBSET_1,
ORDERS_3, OSALG_1, MSUALG_2, MSAFREE, XBOOLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, PBOOLE, LATTICES, OSALG_1, MSUALG_2;
theorems TARSKI, XBOOLE_0, XBOOLE_1, FUNCT_1, RELSET_1, PBOOLE, CARD_3,
MSUALG_1, FUNCT_2, ZFMISC_1, SETFAM_1, BINOP_1, LATTICES, RELAT_1,
PROB_1, OSALG_1, ORDERS_1, MSUALG_2, MBOOLEAN;
schemes XBOOLE_0, BINOP_1, MSUALG_2;
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 A1: s1 <= s2;
A2: (X /\ Y).s1 = X.s1 /\ Y.s1 &
(X /\ Y).s2 = X.s2 /\ Y.s2 by PBOOLE:def 8;
X.s1 c= X.s2 & Y.s1 c= Y.s2 by A1,OSALG_1:def 18;
hence thesis by A2,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 A1: s1 <= s2;
A2: (X \/ Y).s1 = X.s1 \/ Y.s1 &
(X \/ Y).s2 = X.s2 \/ Y.s2 by PBOOLE:def 7;
X.s1 c= X.s2 & Y.s1 c= Y.s2 by A1,OSALG_1:def 18;
hence thesis by A2,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 MSUALG_2:def 1;
take X;
thus thesis;
end;
end;
definition let R be non empty Poset,
M be non-empty OrderSortedSet of R;
cluster non-empty OrderSortedSubset of M;
existence
proof
reconsider N= M as ManySortedSubset of M by MSUALG_2:def 1;
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 MSUALG_2:def 1;
take B;
thus B is OrderSortedSet of S by OSALG_1:17;
end;
end;
:: very strange, the cluster in OSALG_1 should take care of this one
definition let S be OrderSortedSign;
cluster monotone strict non-empty OSAlgebra of S;
existence
proof
consider z being non empty set;
consider z1 being Element of z;
take TrivialOSA(S,z,z1);
thus thesis;
end;
end;
definition
let S be OrderSortedSign,
U0 be non-empty OSAlgebra of S;
cluster non-empty OSSubset of U0;
existence
proof
A1: the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
reconsider N= the Sorts of U0 as MSSubset of U0 by MSUALG_2:def 1;
reconsider M = N as OSSubset of U0 by A1,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 6;
s1 is with_const_op by MSUALG_2:def 3;
then consider o being Element of the OperSymbols of S0 such that
A1: (the Arity of S0).o = {} & (the ResultSort of S0).o = s1
by MSUALG_2:def 2;
o is Element of the OperSymbols of OSSign S0 &
(the Arity of OSSign S0).o = {} &
(the ResultSort of OSSign S0).o = s1 by A1,OSALG_1:def 6;
hence s is with_const_op by MSUALG_2:def 2;
end;
definition
cluster all-with_const_op strict OrderSortedSign;
existence
proof consider S0 being
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;
set U1 = MSAlgebra (#the Sorts of U0,the Charact of U0#);
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
hence U1 is order-sorted by OSALG_1:17;
end;
definition let S be OrderSortedSign,
U0 be OSAlgebra of S; :: can't for ms!
cluster order-sorted MSSubAlgebra of U0;
existence
proof
reconsider U1 = MSAlgebra (#the Sorts of U0,the Charact of U0#)
as strict MSSubAlgebra of U0 by MSUALG_2:38;
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;
definition let S be OrderSortedSign,
U0 be OSAlgebra of S;
cluster strict 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:38;
take U1;
thus thesis;
end;
end;
definition let S be OrderSortedSign,
U0 be non-empty OSAlgebra of S;
cluster non-empty strict 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:38,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 A2: the Sorts of U1 is OrderSortedSet of S by OSALG_1:17;
the Sorts of U1 is MSSubset of U0 by A1,MSUALG_2:def 10;
hence the Sorts of U1 is OSSubset of U0
by A2,Def2;
let B be OSSubset of U0 such that A3: B = the Sorts of U1;
thus B is opers_closed & the Charact of U1 = Opers(U0,B)
by A1,A3,MSUALG_2:def 10;
end;
assume A4: the Sorts of U1 is OSSubset of U0;
then A5: the Sorts of U1 is OrderSortedSet of S by Def2;
assume A6:
for B be OSSubset of U0 st B = the Sorts of U1 holds
B is opers_closed & the Charact of U1 = Opers(U0,B);
U1 is MSSubAlgebra of U0
proof
thus the Sorts of U1 is MSSubset of U0 by A4;
let B be MSSubset of U0 such that A7: B = the Sorts of U1;
reconsider B1=B as OSSubset of U0 by A4,A7;
B1 is opers_closed & the Charact of U1 = Opers(U0,B1) by A6,A7;
hence thesis;
end;
hence thesis by A5,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
:Def3: 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 such that A1: X in Cs;
consider s2 such that A2: X = Constants(OU0,s2) & s2 <= s by A1;
(the Sorts of OU0).s2 c= (the Sorts of OU0).s
by A2,OSALG_1:def 19;
hence thesis by A2,XBOOLE_1:1;
end;
hence thesis by ZFMISC_1:94;
end;
end;
:: maybe
:: theorem S1 is discrete implies OSConstants(OU0,s) = Constants(OU0,s);
canceled 5;
theorem Th11:
Constants(OU0,s) c= OSConstants(OU0,s)
proof
Constants(OU0,s) in {Constants(OU0,s2) : s2 <= s};
then Constants(OU0,s) c= union {Constants(OU0,s2) : s2 <= s} by ZFMISC_1:92;
hence thesis by Def3;
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 LambdaB;
reconsider f as ManySortedSet of the carrier of S1 by A1,PBOOLE:def 3;
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 set such that A3: x in f1.r1;
x in union {M.s2: s2 <= r1} by A1,A3;
then consider y being set such that A4: x in y &
y in {M.s2: s2 <= r1} by TARSKI:def 4;
consider s3 such that A5: y = M.s3 &
s3 <= r1 by A4;
s3 <= r2 by A2,A5,ORDERS_1:26;
then y in {M.s2: s2 <= r2} by A5;
then x in union {M.s2: s2 <= r2} by A4,TARSKI:def 4;
hence x in f1.r2 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 set st s in the carrier of S1 holds W1.s = W2.s
proof let s be set;
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 by PBOOLE:3;
end;
end;
theorem Th12:
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 set;
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:92;
hence thesis by Def4;
end;
theorem Th13:
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 set such that A2:
i in the carrier of S1 and A3: not (OSCl M).i c= A.i by PBOOLE:def 5;
consider x being set such that A4: x in (OSCl M).i
and A5: not x in A.i by A3,TARSKI:def 3;
reconsider s = i as SortSymbol of S1 by A2;
(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;
A10: M.s1 c= A.s1 by A1,PBOOLE:def 5;
A11: A.s1 c= A.s by A9,OSALG_1:def 18;
x in A.s1 by A6,A8,A10;
hence contradiction by A5,A11;
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 Th12,Th13;
hence thesis by PBOOLE:def 13;
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 LambdaB;
reconsider f as ManySortedSet of the carrier of S1 by A1,PBOOLE:def 3;
f c= the Sorts of OU0
proof let s be set;
assume s in the carrier of S1;
then reconsider s1 = s as SortSymbol of S1;
f.s1 = union {Constants(OU0,s2): s2 <= s1} by A1
.= OSConstants(OU0,s1) by Def3;
hence thesis;
end;
then reconsider f as MSSubset of OU0 by MSUALG_2:def 1;
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 set such that A3: x in f1.r1;
x in union {Constants(OU0,s2): s2 <= r1} by A1,A3;
then consider y being set such that A4: x in y &
y in {Constants(OU0,s2): s2 <= r1} by TARSKI:def 4;
consider s3 such that A5: y = Constants(OU0,s3) &
s3 <= r1 by A4;
s3 <= r2 by A2,A5,ORDERS_1:26;
then y in {Constants(OU0,s2): s2 <= r2} by A5;
then x in union {Constants(OU0,s2): s2 <= r2} by A4,TARSKI:def 4;
hence x in f1.r2 by A1;
end;
hence f is OSSubset of OU0 by Def2;
thus for s being SortSymbol of S1 holds f.s = OSConstants(OU0,s)
proof let s be SortSymbol of S1;
f.s = union {Constants(OU0,s2): s2 <= s} by A1 .=
OSConstants(OU0,s) by Def3;
hence thesis;
end;
end;
uniqueness
proof let W1, W2 be OSSubset of OU0;
assume A6: (for s be SortSymbol of S1 holds
W1.s = OSConstants(OU0,s)) &
for s be SortSymbol of S1 holds W2.s = OSConstants(OU0,s);
for s be set st s in the carrier of S1 holds W1.s = W2.s
proof let s be set;
assume s in the carrier of S1;
then reconsider t = s as SortSymbol of S1;
W1.t = OSConstants(OU0,t) & W2.t = OSConstants(OU0,t) by A6;
hence thesis;
end;
hence thesis by PBOOLE:3;
end;
end;
theorem Th15:
Constants(OU0) c= OSConstants(OU0)
proof
let i be set;
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 5;
hence thesis by Th11;
end;
theorem Th16:
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;
A2: A is OrderSortedSet of S1 by Def2;
assume not OSConstants(OU0) c= A;
then consider i being set such that A3:
i in the carrier of S1 and A4: not (OSConstants(OU0)).i c= A.i
by PBOOLE:def 5;
consider x being set such that A5: x in (OSConstants(OU0)).i
and A6: not x in A.i by A4,TARSKI:def 3;
reconsider s = i as SortSymbol of S1 by A3;
(OSConstants(OU0)).s = OSConstants(OU0,s) by Def5 .=
union {Constants(OU0,s2) : s2 <= s} by Def3;
then consider X1 being set such that A7: x in X1 and
A8: X1 in {Constants(OU0,s2) : s2 <= s} by A5,TARSKI:def 4;
consider s1 being SortSymbol of S1 such that A9: X1 = Constants(OU0,s1)
and A10: s1 <= s by A8;
A11: (Constants(OU0)).s1 c= A.s1 by A1,PBOOLE:def 5;
A12: A.s1 c= A.s by A2,A10,OSALG_1:def 18;
x in (Constants(OU0)).s1 by A7,A9,MSUALG_2:def 5;
then x in A.s1 by A11;
hence contradiction by A6,A12;
end;
theorem
for A being OSSubset of OU0 holds
OSConstants(OU0) = OSCl Constants(OU0)
proof
let A be OSSubset of OU0;
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 set holds (x in c1 iff x in c2)
proof let x be set;
hereby assume x in c1;
then consider s1 such that A1: x = (Constants(OU0)).s1 & s1 <= s;
x = Constants(OU0,s1) & s1 <= s by A1,MSUALG_2:def 5;
hence x in c2;
end;
assume x in c2;
then consider s1 such that A2: x = Constants(OU0,s1) & s1 <= s;
x = (Constants(OU0)).s1 & s1 <= s by A2,MSUALG_2:def 5;
hence x in c1;
end;
then A3: c1 = c2 by TARSKI:2;
(OSConstants(OU0)).s = OSConstants(OU0,s) by Def5
.= union { (Constants(OU0)).s1: s1 <= s} by A3,Def3 .=
(OSCl Constants(OU0)).s by Def4;
hence (OSConstants(OU0)).i = (OSCl Constants(OU0)).i;
end;
then ( for i being set st i in the carrier of S1 holds
(OSConstants(OU0)).i c= (OSCl Constants(OU0)).i) &
for i being set st i in the carrier of S1 holds
(OSCl Constants(OU0)).i c= (OSConstants(OU0)).i;
then OSConstants(OU0) c= OSCl Constants(OU0) &
OSCl Constants(OU0) c= OSConstants(OU0) by PBOOLE:def 5;
hence thesis by PBOOLE:def 13;
end;
theorem Th18:
for OU1 being OSSubAlgebra of OU0 holds
OSConstants(OU0) is OSSubset of OU1
proof
let OU1 be OSSubAlgebra of OU0;
A1: OSConstants(OU0) is ManySortedSubset of the Sorts of OU1
proof
OSConstants(OU0) c= the Sorts of OU1
proof let i be set such that A2:
i in the carrier of S1;
reconsider s = i as SortSymbol of S1 by A2;
Constants(OU0) is MSSubset of OU1 by MSUALG_2:11;
then A3: Constants(OU0) c= (the Sorts of OU1) by MSUALG_2:def 1;
A4: for s2,s3 st s2 <= s3 holds
(Constants(OU0)).s2 c= (the Sorts of OU1).s3
proof let s2,s3;
assume s2 <= s3;
then A5: (the Sorts of OU1).s2 c= (the Sorts of OU1).s3
by OSALG_1:def 19;
(Constants(OU0)).s2 c= (the Sorts of OU1).s2 by A3,PBOOLE:def 5;
hence (Constants(OU0)).s2 c= (the Sorts of OU1).s3
by A5,XBOOLE_1:1;
end;
A6: 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 A7: X = Constants(OU0,s4) &
s4 <= s;
Constants(OU0,s4) = (Constants(OU0)).s4 by MSUALG_2:def 5;
hence thesis by A4,A7;
end;
(OSConstants(OU0)).i = OSConstants(OU0,s)
by Def5 .= union {Constants(OU0,s1): s1 <= s} by Def3;
hence (OSConstants(OU0)).i c= (the Sorts of OU1).i by A6,ZFMISC_1:94;
end;
hence thesis by MSUALG_2:def 1;
end;
OSConstants(OU0) is OrderSortedSet of S1 by Def2;
hence thesis by A1,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 Th15;
hence thesis by Th18,PBOOLE:143;
end;
begin
::
:: Order Sorted Subsets of an Order Sorted Algebra.
::
:: this should be in MSUALG_2
theorem Th20:
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 PBOOLE:def 3;
hereby
assume x is ManySortedSubset of M;
then reconsider x1 = x as ManySortedSubset of M;
A2: dom x1 = I by PBOOLE:def 3 .= dom bool M by PBOOLE:def 3;
for i being set st i in dom bool M holds x1.i in (bool M).i
proof
let i be set such that A3: i in dom bool M;
x1 c= M by MSUALG_2:def 1;
then x1.i c= M.i by A1,A3,PBOOLE:def 5;
then x1.i in bool (M.i);
hence x1.i in (bool M).i by A1,A3,MBOOLEAN:def 1;
end;
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 & dom x1 = dom bool M &
for i being set st i in dom bool M holds x1.i in (bool M).i
by CARD_3:def 5;
reconsider x2 = x1 as ManySortedSet of I by A1,A4,PBOOLE:def 3;
x2 c= M
proof
let i be set such that A5: i in I;
x2.i in (bool M).i by A1,A4,A5;
then x2.i in bool (M.i) by A5,MBOOLEAN:def 1;
hence x2.i c= M.i;
end;
hence thesis by A4,MSUALG_2:def 1;
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
set f = product bool M;
defpred P[set] means $1 is OrderSortedSubset of M;
consider X being set such that
A1: for y being set holds
y in X iff y in f & P[y] from Separation;
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 Th20;
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 SetEq;
end;
end;
definition let S be OrderSortedSign,
U0 be OSAlgebra of S,
A be OSSubset of U0;
func OSSubSort(A) -> set equals
:Def7: { x where x is Element of SubSort(A): x is OrderSortedSet of S};
correctness;
end;
theorem Th21:
for A being OSSubset of OU0 holds OSSubSort(A) c= SubSort(A)
proof
let A be OSSubset of OU0;
let x be set such that A1: x in OSSubSort(A);
x in { y where y is Element of SubSort(A): y is OrderSortedSet of S1}
by A1,Def7;
then consider y being Element of SubSort(A) such that A2: x = y &
y is OrderSortedSet of S1;
thus thesis by A2;
end;
theorem Th22:
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:40;
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 by Def7;
end;
definition let S1,OU0;
let A be OSSubset of OU0;
cluster OSSubSort(A) -> non empty;
coherence by Th22;
end;
definition let S1,OU0;
func OSSubSort(OU0) -> set equals :Def8:
{ x where x is Element of SubSort(OU0): x is OrderSortedSet of S1};
correctness;
end;
theorem Th23:
for A being OSSubset of OU0 holds OSSubSort(A) c= OSSubSort(OU0)
proof
let A be OSSubset of OU0;
let x be set such that A1: x in OSSubSort(A);
x in { y where y is Element of SubSort(A): y is OrderSortedSet of S1}
by A1,Def7;
then consider x1 being Element of SubSort(A) such that
A2: x1 = x and A3: x1 is OrderSortedSet of S1;
x1 in SubSort(A) & SubSort(A) c= SubSort(OU0) by MSUALG_2:41;
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 A3;
hence thesis by A2,Def8;
end;
definition let S1,OU0;
cluster OSSubSort(OU0) -> non empty;
coherence
proof
consider A being OSSubset of OU0;
the Sorts of OU0 in OSSubSort(A) &
OSSubSort(A) c= OSSubSort(OU0) by Th22,Th23;
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 :Def9:
e;
coherence
proof
e in OSSubSort(OU0);
then e in
{ x where x is Element of SubSort(OU0): x is OrderSortedSet of S1}
by Def8;
then consider e1 being Element of SubSort(OU0) such that A1:
e = e1 & e1 is OrderSortedSet of S1;
e1 = @e1 by MSUALG_2:def 13;
then reconsider e2 = @e1 as OSSubset of OU0 by A1,Def2;
e2 = e by A1,MSUALG_2:def 13;
hence thesis;
end;
end;
:: maybe do another definition of ossort, saying that it contains
:: Elements of subsort which are order-sorted (or ossubsets)
theorem Th24:
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;
A1: B is OrderSortedSet of S1 by Def2;
thus B in OSSubSort(A) implies
B is opers_closed & OSConstants(OU0) c= B & A c= B
proof assume B in OSSubSort(A);
then B in
{ x where x is Element of SubSort(A): x is OrderSortedSet of S1}
by Def7;
then consider B1 being Element of SubSort(A) such that
A2: B1 = B & B1 is OrderSortedSet of S1;
B is opers_closed & Constants(OU0) c= B & A c= B
by A2,MSUALG_2:14;
hence thesis by Th16;
end;
assume A3: B is opers_closed & OSConstants(OU0) c= B & A c= B;
Constants(OU0) c= OSConstants(OU0) by Th15;
then Constants(OU0) c= B by A3,PBOOLE:15;
then B in SubSort(A) by A3,MSUALG_2:14;
then B in
{ x where x is Element of SubSort(A): x is OrderSortedSet of S1} by A1;
hence thesis by Def7;
end;
theorem Th25:
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 is OrderSortedSet of S1 by Def2;
A2: B in SubSort(OU0) iff B is opers_closed by MSUALG_2:15;
A3: B in OSSubSort(OU0) iff B in
{ x where x is Element of SubSort(OU0): x is OrderSortedSet of S1}
by Def8;
thus B in OSSubSort(OU0) implies B is opers_closed
proof assume B in OSSubSort(OU0);
then consider B1 being Element of SubSort(OU0) such that A4:
B1 = B & B1 is OrderSortedSet of S1 by A3;
thus thesis by A4,MSUALG_2:15;
end;
assume B is opers_closed;
hence B in OSSubSort(OU0) by A1,A2,A3;
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 set holds
x in it iff ex B be OSSubset of OU0 st B in OSSubSort(A) & x = B.s;
existence
proof
set C =bool Union (the Sorts of OU0);
A1: C = bool union( rng(the Sorts of OU0)) by PROB_1:def 3;
defpred P[set] means ex B be OSSubset of OU0 st
B in OSSubSort(A) & $1 = B.s;
consider X be set such that
A2: for x be set holds
x in X iff x in C & P[x] from Separation;
A3: for x be set holds
x in X iff ex B be OSSubset of OU0 st B in OSSubSort(A) & x = B.s
proof let x be set;
thus x in X implies
ex B be OSSubset of OU0 st B in OSSubSort(A) & x = B.s by A2;
given B be OSSubset of OU0 such that
A4: B in OSSubSort(A) & x = B.s;
dom (the Sorts of OU0) = the carrier of S1 &
dom B = the carrier of S1 by PBOOLE:def 3;
then (the Sorts of OU0).s in rng (the Sorts of OU0) by FUNCT_1:def 5;
then A5: (the Sorts of OU0).s c= union( rng (the Sorts of OU0)) by
ZFMISC_1:92;
B c= the Sorts of OU0 by MSUALG_2:def 1;
then B.s c= (the Sorts of OU0).s by PBOOLE:def 5;
then x c= union( rng (the Sorts of OU0)) by A4,A5,XBOOLE_1:1;
hence thesis by A1,A2,A4;
end;
take X;
thus thesis by A3;
end;
uniqueness
proof
defpred P[set] 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 set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
end;
end;
theorem Th26:
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 such that A2: x in OSSubSort(A,s2);
consider B being OSSubset of OU0 such that A3:
B in OSSubSort(A) & x = B.s2 by A2,Def10;
A4: B is OrderSortedSet of S1 by Def2;
take B.s1;
thus thesis by A1,A3,A4,Def10,OSALG_1:def 18;
end;
hence thesis by SETFAM_1:def 3;
end;
theorem Th27:
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 set;
assume x in OSSubSort(A,s);
then consider B being OSSubset of OU0 such that A1:
B in OSSubSort(A) & x = B.s by Def10;
OSSubSort(A) c= SubSort(A) by Th21;
hence thesis by A1,MSUALG_2:def 14;
end;
theorem Th28:
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;
A1: the Sorts of OU0 in OSSubSort(A) by Th22;
the Sorts of OU0 is ManySortedSubset of the Sorts of OU0 &
the Sorts of OU0 is OrderSortedSet of S1
by MSUALG_2:def 1,OSALG_1:17;
then reconsider B = the Sorts of OU0 as OSSubset of OU0 by Def2;
B.s in OSSubSort(A,s) by A1,Def10;
hence thesis;
end;
definition let S1,OU0;
let A be OSSubset of OU0,
s be SortSymbol of S1;
cluster OSSubSort(A,s) -> non empty;
coherence by Th28;
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 LambdaB;
reconsider f as ManySortedSet of (the carrier of S1) by A1,PBOOLE:def 3;
f c= the Sorts of OU0
proof let x be set;
assume x in the carrier of S1;
then reconsider s = x as SortSymbol of S1;
A2: f.s = meet (OSSubSort(A,s)) by A1;
reconsider u0 = the Sorts of OU0 as MSSubset of OU0 by MSUALG_2:def 1;
u0 is OrderSortedSet of S1 by OSALG_1:17;
then A3: u0 is OSSubset of OU0 by Def2;
u0 in OSSubSort(A) by Th22;
then (the Sorts of OU0).s in (OSSubSort(A,s)) by A3,Def10;
hence thesis by A2,SETFAM_1:4;
end;
then reconsider f as MSSubset of OU0 by MSUALG_2:def 1;
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 A4: s1 <= s2;
reconsider s3 = s1, s4 = s2 as SortSymbol of S1;
OSSubSort(A,s4) is_coarser_than OSSubSort(A,s3) by A4,Th26;
then A5: meet OSSubSort(A,s1) c= meet OSSubSort(A,s2) by SETFAM_1:19;
f1.s1 = meet OSSubSort(A,s1) by A1;
hence f1.s1 c= f1.s2 by A1,A5;
end;
then f is OrderSortedSet of S1 by OSALG_1:def 18;
hence thesis by A1,Def2;
end;
uniqueness
proof let W1,W2 be OSSubset of OU0;
assume A6: (for s be SortSymbol of S1 holds W1.s = meet (OSSubSort(A,s))) &
(for s be SortSymbol of S1 holds W2.s = meet (OSSubSort(A,s)));
for s be set st s in (the carrier of S1) holds W1.s = W2.s
proof let s be set;
assume s in (the carrier of S1);
then reconsider s as SortSymbol of S1;
W1.s = meet (OSSubSort(A,s)) & W2.s = meet (OSSubSort(A,s)) by A6;
hence thesis;
end;
hence thesis by PBOOLE:3;
end;
end;
definition let S1,OU0;
canceled;
cluster opers_closed OSSubset of OU0;
existence
proof
consider x being Element of OSSubSort(OU0);
x in OSSubSort(OU0);
then x in
{ y where y is Element of SubSort(OU0): y is OrderSortedSet of S1}
by Def8;
then consider x1 being Element of SubSort(OU0) such that A1:
x = x1 & x1 is OrderSortedSet of S1;
reconsider x2 = x1 as MSSubset of OU0 by MSUALG_2:def 12;
A2: x2 is opers_closed by MSUALG_2:def 12;
reconsider x3 = x2 as OSSubset of OU0 by A1,Def2;
take x3;
thus thesis by A2;
end;
end;
theorem Th29:
for A be OSSubset of OU0 holds OSConstants(OU0) \/ A c= OSMSubSort(A)
proof let A be OSSubset of OU0;
let i be set; assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
A1: (OSMSubSort(A)).s = meet (OSSubSort(A,s)) by Def11;
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) & Z = B.s by Def10;
OSConstants(OU0) c= B & A c= B by A2,Th24;
then OSConstants(OU0) \/ A c= B by PBOOLE:18;
hence thesis by A2,PBOOLE:def 5;
end;
hence thesis by A1,SETFAM_1:6;
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 set; assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
A2: (OSConstants(OU0) \/ A).s is non empty by A1,PBOOLE:def 16;
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
A3: B in OSSubSort(A) & Z = B.s by Def10;
OSConstants(OU0) c= B & A c= B by A3,Th24;
then OSConstants(OU0) \/ A c= B by PBOOLE:18;
hence thesis by A3,PBOOLE:def 5;
end;
then A4: (OSConstants(OU0) \/ A).s c= meet(OSSubSort(A,s)) by SETFAM_1:6;
consider x be set such that A5: x in (OSConstants(OU0) \/
A).s by A2,XBOOLE_0:def 1;
thus (OSMSubSort(A)).i is non empty by A4,A5,Def11;
end;
hence thesis by PBOOLE:def 16;
end;
theorem Th31:
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 set;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
A2: (OSMSubSort A).s = meet (OSSubSort(A,s)) by Def11;
B.s in (OSSubSort(A,s)) by A1,Def10;
hence thesis by A2,SETFAM_1:4;
end;
hence thesis by MSUALG_2:3;
end;
theorem Th32:
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 m c= b by Th31;
then b /\ m = m by XBOOLE_1:28;
then d|m = (d|b)|m by RELAT_1:100;
then A2: rng (d|m) c= rng(d|b) by FUNCT_1:76;
B is opers_closed by A1,Th24;
then B is_closed_on o by MSUALG_2:def 7;
then rng (d|b) c= (B * (the ResultSort of S1)).o by MSUALG_2:def 6;
hence thesis by A2,XBOOLE_1:1;
end;
theorem Th33:
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 set; 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 by MSUALG_1:def 7;
A4: dom (the ResultSort of S1) = the OperSymbols of S1 &
rng (the ResultSort of S1) c= the carrier of S1 by FUNCT_2:def 1,RELSET_1:12;
then ((OSMSubSort A) * (the ResultSort of S1)).o = (OSMSubSort A).r
by A3,FUNCT_1:23
.= meet OSSubSort(A,r) by Def11;
then consider X be set such that
A5: X in OSSubSort(A,r) & not x in X by A2,SETFAM_1:def 1;
consider B be OSSubset of OU0 such that
A6: B in OSSubSort(A) & B.r = X by A5,Def10;
rng (Den(o,OU0)|(((OSMSubSort A)# * (the Arity of S1)).o)) c=
(B * (the ResultSort of S1)).o by A6,Th32;
then x in (B * (the ResultSort of S1)).o by A1;
hence contradiction by A3,A4,A5,A6,FUNCT_1:23;
end;
theorem Th34:
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 OperSymbols 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 Th33;
hence thesis by MSUALG_2:def 6;
end;
A1: A c= OSConstants(OU0) \/ A by PBOOLE:16;
OSConstants(OU0) \/ A c= OSMSubSort(A) by Th29;
hence thesis by A1,PBOOLE:15;
end;
definition
let S1,OU0;
let A be OSSubset of OU0;
cluster OSMSubSort(A) -> opers_closed;
coherence by Th34;
end;
begin :: Operations on Subalgebras of an Order Sorted Algebra.
definition 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)#);
A1: OU0|A = M by MSUALG_2:def 16;
A is OrderSortedSet of S1 by Def2;
hence thesis by A1,OSALG_1:17;
end;
end;
definition 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 17;
hence OU1 /\ OU2 is order-sorted 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 :Def13:
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
A1: A is OrderSortedSet of S1 by Def2;
set a = OSMSubSort(A);
A2: a is opers_closed & A c= a by Th34;
reconsider u1 = OU0|a as strict OSSubAlgebra of OU0;
take u1;
A3: u1 = MSAlgebra (# a, Opers(OU0,a)qua ManySortedFunction of
(a# * the Arity of S1),(a * the ResultSort of S1)#)
by MSUALG_2:def 16;
then A is MSSubset of u1 by A2,MSUALG_2:def 1;
hence A is OSSubset of u1 by A1,Def2;
let U2 be OSSubAlgebra of OU0;
reconsider B1 = the Sorts of U2 as MSSubset of OU0
by MSUALG_2:def 10;
B1 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B1 as OSSubset of OU0 by Def2;
A4: B is opers_closed by MSUALG_2:def 10;
assume A is OSSubset of U2;
then A5: A c= B by MSUALG_2:def 1;
OSConstants(OU0) is OSSubset of U2 by Th18;
then OSConstants(OU0) c= B by MSUALG_2:def 1;
then A6: B in OSSubSort(A) by A4,A5,Th24;
the Sorts of u1 c= the Sorts of U2
proof let i be set;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
A7: (the Sorts of u1).s = meet OSSubSort(A,s)
by A3,Def11;
B.s in OSSubSort(A,s) by A6,Def10;
hence thesis by A7,SETFAM_1:4;
end;
hence u1 is OSSubAlgebra of U2 by MSUALG_2:9;
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:8;
end;
end;
:: this should rather be a definition, but I want to keep
:: compatibility of the definition with MSUALG_2
theorem Th35:
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;
A1: A is OrderSortedSet of S1 by Def2;
set a = OSMSubSort(A);
A2: a is opers_closed & A c= a by Th34;
reconsider u1 = OU0|a as strict OSSubAlgebra of OU0;
A3: u1 = MSAlgebra (# a, Opers(OU0,a)qua ManySortedFunction of
(a# * the Arity of S1),(a * the ResultSort of S1)#)
by MSUALG_2:def 16;
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,A3,MSUALG_2:def 1;
hence A is OSSubset of u1 by A1,Def2;
let U2 be OSSubAlgebra of OU0;
reconsider B1 = the Sorts of U2 as MSSubset of OU0
by MSUALG_2:def 10;
B1 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B1 as OSSubset of OU0 by Def2;
A5: B is opers_closed by MSUALG_2:def 10;
assume A is OSSubset of U2;
then A6: A c= B by MSUALG_2:def 1;
OSConstants(OU0) is OSSubset of U2 by Th18;
then OSConstants(OU0) c= B by MSUALG_2:def 1;
then A7: B in OSSubSort(A) by A5,A6,Th24;
the Sorts of u1 c= the Sorts of U2
proof let i be set;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
A8: (the Sorts of u1).s = meet OSSubSort(A,s)
by A3,Def11;
B.s in OSSubSort(A,s) by A7,Def10;
hence thesis by A8,SETFAM_1:4;
end;
hence u1 is OSSubAlgebra of U2 by MSUALG_2:9;
end;
hence GenOSAlg(A) = OU0|a by Def13;
thus thesis by A3,A4,Def13;
end;
:: this could simplify some proofs in MSUALG_2, I need it anyway
theorem Th36:
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);
A1: a is opers_closed & A c= a by MSUALG_2:21;
reconsider u1 = U0|a as strict MSSubAlgebra of U0;
A2: u1 = MSAlgebra (# a, Opers(U0,a)qua ManySortedFunction of
(a# * the Arity of S),(a * the ResultSort of S)#)
by A1,MSUALG_2:def 16;
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 A1,A2,MSUALG_2:def 1;
let U2 be MSSubAlgebra of U0;
reconsider B = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def 10;
A4: B is opers_closed by MSUALG_2:def 10;
assume A is MSSubset of U2;
then A5: A c= B by MSUALG_2:def 1;
Constants(U0) is MSSubset of U2 by MSUALG_2:11;
then Constants(U0) c= B by MSUALG_2:def 1;
then A6: B in SubSort(A) by A4,A5,MSUALG_2:14;
the Sorts of u1 c= the Sorts of U2
proof let i be set;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A7: (the Sorts of u1).s = meet SubSort(A,s)
by A2,MSUALG_2:def 15;
B.s in SubSort(A,s) by A6,MSUALG_2:def 14;
hence thesis by A7,SETFAM_1:4;
end;
hence u1 is MSSubAlgebra of U2 by MSUALG_2:9;
end;
hence GenMSAlg(A) = U0|a by MSUALG_2:def 18;
thus thesis by A2,A3,MSUALG_2:def 18;
end;
theorem Th37:
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);
A1: the Sorts of GM = MSSubSort(A) &
the Sorts of GO = OSMSubSort(A) by Th35,Th36;
let i be set;
assume i in the carrier of S1;
then reconsider s = i as SortSymbol of S1;
A2: (the Sorts of GO).s = meet OSSubSort(A,s)
by A1,Def11;
A3: (the Sorts of GM).s = meet SubSort(A,s)
by A1,MSUALG_2:def 15;
OSSubSort(A,s) c= SubSort(A,s) by Th27;
hence (the Sorts of GM).i c= (the Sorts of GO).i by A2,A3,SETFAM_1:7;
end;
theorem Th38:
for A being OSSubset of OU0 holds
GenMSAlg(A) is MSSubAlgebra of GenOSAlg(A)
proof
let A be OSSubset of OU0;
the Sorts of GenMSAlg(A) c= the Sorts of GenOSAlg(A) by Th37;
hence thesis by MSUALG_2:9;
end;
theorem Th39:
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:22;
GenMSAlg(B) is strict MSSubAlgebra of GenOSAlg(B) by Th38;
hence thesis by A1,MSUALG_2:8;
end;
theorem Th40:
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;
A1: B is OrderSortedSet of S1 by Def2;
assume A2: B = the Sorts of OU1;
then B is MSSubset of OU1 by MSUALG_2:def 1;
then A3: B is OSSubset of OU1 by A1,Def2;
set W = GenOSAlg(B);
A4: B is OSSubset of W by Def13;
A5: W is strict OSSubAlgebra of OU1 by A3,Def13;
the Sorts of OU1 c= the Sorts of W by A2,A4,MSUALG_2:def 1;
then OU1 is strict MSSubAlgebra of W by MSUALG_2:9;
hence thesis by A5,MSUALG_2:8;
end;
theorem Th41:
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);
A1: the Sorts of ( G /\ U1) = (the Sorts of G) /\ (the Sorts of U1)
by MSUALG_2:def 17;
C is OSSubset of U1 by Th18;
then G is strict OSSubAlgebra of U1 by Def13;
then the Sorts of G is MSSubset of U1 & the Sorts of G
is OrderSortedSet of S1 by MSUALG_2:def 10,OSALG_1:17;
then the Sorts of G c= the Sorts of U1 by MSUALG_2:def 1;
then the Sorts of ( G /\ U1) = the Sorts of G by A1,PBOOLE:25;
hence thesis by MSUALG_2:10;
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 :Def14:
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 U1 is MSSubset of U0 &
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 10;
then the Sorts of U1 c=the Sorts of U0 &
the Sorts of U2 c=the Sorts of U0 by MSUALG_2:def 1;
then B c= the Sorts of U0 by PBOOLE:18;
then reconsider B as MSSubset of U0 by MSUALG_2:def 1;
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 let W1,W2 be strict OSSubAlgebra of U0;
assume A1:(for A be OSSubset of U0 st
A = (the Sorts of U1) \/ (the Sorts of U2) holds W1 = GenOSAlg(A)) &
( for A be OSSubset of U0 st
A = (the Sorts of U1) \/ (the Sorts of U2) holds W2 = GenOSAlg(A));
set B=(the Sorts of U1) \/ (the Sorts of U2);
the Sorts of U1 is MSSubset of U0 &
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 10;
then the Sorts of U1 c=the Sorts of U0 &
the Sorts of U2 c=the Sorts of U0 by MSUALG_2:def 1;
then B c= the Sorts of U0 by PBOOLE:18;
then reconsider B as MSSubset of U0 by MSUALG_2:def 1;
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;
W1 = GenOSAlg(B0) & W2 = GenOSAlg(B0) by A1;
hence thesis;
end;
end;
theorem Th42:
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;
A1: A is OrderSortedSet of S1 & B is OrderSortedSet of S1
by Def2;
assume A2: B = A \/ the Sorts of U1;
A is OSSubset of GenOSAlg(A) by Def13;
then A3:A c= the Sorts of GenOSAlg(A) by MSUALG_2:def 1;
reconsider u1m = the Sorts of U1, am = the Sorts of GenOSAlg(A)
as MSSubset of U0 by MSUALG_2:def 10;
A4: 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 MSUALG_2:def 1;
then a \/ u1 c= the Sorts of U0 by PBOOLE:18;
then reconsider b=a \/ u1 as MSSubset of U0 by MSUALG_2:def 1;
A5: a \/ u1 is OrderSortedSet of S1 by A4,Th2;
then reconsider b as OSSubset of U0 by Def2;
A6: (GenOSAlg(A) "\/"_os U1) = GenOSAlg(b) by Def14;
then a \/ u1 is OSSubset of (GenOSAlg(A)"\/"_os U1) by Def13;
then A7: a \/ u1 c=the Sorts of (GenOSAlg(A)"\/"_os U1) by MSUALG_2:def 1;
A \/ u1 c= a \/ u1 by A3,PBOOLE:22;
then B c=the Sorts of (GenOSAlg(A)"\/"_os U1) by A2,A7,PBOOLE:15;
then B is MSSubset of (GenOSAlg(A)"\/"_os U1) by MSUALG_2:def 1;
then B is OSSubset of (GenOSAlg(A)"\/"_os U1) by A1,Def2;
then A8:GenOSAlg(B) is strict OSSubAlgebra of (GenOSAlg(A)"\/"_os U1)
by Def13;
B is OSSubset of GenOSAlg(B) & u1 c= B & A c= B by A2,Def13,PBOOLE:16;
then B c= the Sorts of GenOSAlg(B) & u1 c= B & A c= B by MSUALG_2:def 1;
then A9: u1 c= the Sorts of GenOSAlg(B) & A c= the Sorts of GenOSAlg(B)
by PBOOLE:15;
then A10: A c= (the Sorts of GenOSAlg(A)) /\ (the Sorts of GenOSAlg(B))
by A3,PBOOLE:19;
A11:the Sorts of (GenOSAlg(A) /\ GenOSAlg(B)) =
(the Sorts of GenOSAlg(A)) /\
(the Sorts of GenOSAlg(B)) by MSUALG_2:def 17;
then A is MSSubset of (GenOSAlg(A) /\ GenOSAlg(B)) by A10,MSUALG_2:def 1;
then A is OSSubset of (GenOSAlg(A) /\ GenOSAlg(B)) by A1,Def2;
then GenOSAlg(A) is OSSubAlgebra of (GenOSAlg(A) /\ GenOSAlg(B)) by Def13;
then a is MSSubset of (GenOSAlg(A) /\ GenOSAlg(B)) by MSUALG_2:def 10;
then A12:a c= (the Sorts of GenOSAlg(A)) /\ (the Sorts of GenOSAlg(B))
by A11,MSUALG_2:def 1;
(the Sorts of GenOSAlg(A)) /\ (the Sorts of GenOSAlg(B)) c= a
by PBOOLE:17;
then a= (the Sorts of GenOSAlg(A)) /\ (the Sorts of GenOSAlg(B))
by A12,PBOOLE:def 13;
then a c= the Sorts of GenOSAlg(B) by PBOOLE:17;
then b c= the Sorts of GenOSAlg(B) by A9,PBOOLE:18;
then b is MSSubset of GenOSAlg(B) by MSUALG_2:def 1;
then b is OSSubset of GenOSAlg(B) by A5,Def2;
then GenOSAlg(b) is strict OSSubAlgebra of GenOSAlg(B) by Def13;
hence thesis by A6,A8,MSUALG_2:8;
end;
theorem Th43:
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;
assume A1: B = the Sorts of U0;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 10;
then the Sorts of U1 c= B by A1,MSUALG_2:def 1;
then B \/ the Sorts of U1 = B by PBOOLE:24;
hence thesis by Th42;
end;
theorem Th44:
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 10;
A1:
u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 by OSALG_1:17;
u1 c= the Sorts of U0 & u2 c= the Sorts of U0 by MSUALG_2:def 1;
then u1 \/ u2 c= the Sorts of U0 by PBOOLE:18;
then reconsider A1 = u1 \/ u2 as MSSubset of U0 by MSUALG_2:def 1;
A1 is OrderSortedSet of S1 by A1,Th2;
then reconsider A = A1 as OSSubset of U0 by Def2;
U1 "\/"_os U2 = GenOSAlg(A) by Def14;
hence thesis by Def14;
end;
theorem Th45:
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 10;
A1: u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1
by OSALG_1:17;
u1 c= the Sorts of U0 & u2 c= the Sorts of U0 by MSUALG_2:def 1;
then u1 \/ u2 c= the Sorts of U0 by PBOOLE:18;
then reconsider A= u1 \/ u2 as MSSubset of U0 by MSUALG_2:def 1;
A is OrderSortedSet of S1 by A1,Th2;
then reconsider A as OSSubset of U0 by Def2;
U1"\/"_os U2 = GenOSAlg(A) by Def14;
then A is OSSubset of U1"\/"_os U2 by Def13;
then A2:A c= the Sorts of (U1 "\/"_os U2) by MSUALG_2:def 1;
the Sorts of U1 c= A by PBOOLE:16;
then A3: the Sorts of U1 c= the Sorts of (U1"\/"_os U2) by A2,PBOOLE:15;
A4:the Sorts of (U1 /\(U1"\/"_os U2))=
(the Sorts of U1)/\(the Sorts of(U1"\/"_os U2)) by MSUALG_2:def 17;
then A5:the Sorts of U1 c=the Sorts of (U1 /\(U1"\/"_os U2))
by A3,PBOOLE:19;
the Sorts of (U1 /\(U1"\/"_os U2)) c= the Sorts of U1 by A4,PBOOLE:17;
then A6:the Sorts of (U1 /\(U1"\/"_os U2)) = the Sorts of U1 by A5,PBOOLE:def
13;
reconsider u112=the Sorts of(U1 /\ (U1"\/"_os U2)) as MSSubset of U0
by MSUALG_2:def 10;
u112 is opers_closed & the Charact of (U1/\(U1"\/"_os
U2))=Opers(U0,u112) by MSUALG_2:def 17;
hence thesis by A6,MSUALG_2:def 10;
end;
theorem Th46:
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 10;
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 MSUALG_2:def 1;
then u12 \/ u2 c= the Sorts of U0 by PBOOLE:18;
then reconsider A= u12 \/ u2 as MSSubset of U0 by MSUALG_2:def 1;
A is OrderSortedSet of S1 by A1,Th2;
then reconsider A= u12 \/ u2 as OSSubset of U0 by Def2;
A2:(U1 /\ U2) "\/"_os U2 = GenOSAlg(A) by Def14;
u12 = (the Sorts of U1) /\ (the Sorts of U2) by MSUALG_2:def 17;
then u12 c= u2 by PBOOLE:17;
then A = u2 by PBOOLE:24;
hence thesis by A2,Th40;
end;
begin :: The Lattice of SubAlgebras of an Order Sorted Algebra.
:: ossub, ossubalgebra
definition let S1,OU0;
func OSSub(OU0) -> set means :Def15:
for x holds x in it iff x is strict OSSubAlgebra of OU0;
existence
proof
set X = {GenOSAlg(@A) where A is Element of OSSubSort(OU0):
not contradiction};
take X;
let x;
thus x in X implies x is strict OSSubAlgebra of OU0
proof assume x in X;
then consider A be Element of OSSubSort(OU0) such that
A1: x = GenOSAlg(@A);
thus thesis by A1;
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 Th25;
@h =A by Def9;
then a = GenOSAlg(@h) by Th40;
hence x in X;
end;
uniqueness
proof
defpred P[set] means $1 is strict OSSubAlgebra of OU0;
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 SetEq;
end;
end;
theorem Th47:
OSSub(OU0) c= MSSub(OU0)
proof
let x be set such that A1: x in OSSub(OU0);
x is strict MSSubAlgebra of OU0 by A1,Def15;
hence thesis by MSUALG_2:def 20;
end;
definition let S be OrderSortedSign,
U0 be OSAlgebra of S;
cluster OSSub(U0) -> non empty;
coherence
proof
consider x being strict OSSubAlgebra of U0;
x in OSSub U0 by Def15;
hence thesis;
end;
end;
definition let S1,OU0;
redefine func OSSub(OU0) -> Subset of MSSub(OU0);
coherence by Th47;
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 :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 "\/"_os U2;
existence
proof
defpred P[(Element of OSSub(U0)),(Element of OSSub(U0)),
Element of OSSub(U0)] 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 Def15;
reconsider z =U1"\/"_os U2 as Element of OSSub(U0)
by Def15;
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 BinOpEx(A1);
take o;
thus thesis by A2;
end;
uniqueness
proof let o1,o2 be BinOp of (OSSub(U0));
assume 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)
& (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 Def15;
o1.(x,y) = U1"\/"_os U2 & o2.(x,y) = U1"\/"_os U2 by A3;
hence thesis;
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 :Def17:
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)),
Element of OSSub(U0)] 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 Def15;
reconsider z =U1 /\ U2 as Element of OSSub(U0) by Def15;
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 BinOpEx(A1);
take o;
thus thesis by A2;
end;
uniqueness
proof let o1,o2 be BinOp of OSSub(U0);
assume 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)
& (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 Def15;
o1.(x,y) = U1 /\ U2 & o2.(x,y) = U1 /\ U2 by A3;
hence thesis;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem Th48:
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 Def15;
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,Def17 .=
(MSAlg_meet(U0)).(x,y) by A1,MSUALG_2:def 22;
hence thesis;
end;
reserve U0 for non-empty OSAlgebra of S1;
theorem Th49:
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 Def15;
A1:o.(x,y) = U1 "\/"_os U2 & o.(y,x) = U2 "\/"_os U1 by Def16;
set B=(the Sorts of U1) \/ (the Sorts of U2);
the Sorts of U1 is OrderSortedSet of S1 &
the Sorts of U2 is OrderSortedSet of S1 by OSALG_1:17;
then A2: B is OrderSortedSet of S1 by Th2;
the Sorts of U1 is MSSubset of U0 &
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 10;
then the Sorts of U1 c=the Sorts of U0 &
the Sorts of U2 c=the Sorts of U0 by MSUALG_2:def 1;
then B c= the Sorts of U0 by PBOOLE:18;
then B is MSSubset of U0 by MSUALG_2:def 1;
then reconsider B as OSSubset of U0 by A2,Def2;
U1 "\/"_os U2 = GenOSAlg(B) & U2 "\/"_os U1 = GenOSAlg(B)
by Def14;
hence thesis by A1;
end;
hence thesis by BINOP_1:def 2;
end;
theorem Th50:
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 Def15;
o.(y,z)=U2"\/"_os U3 & o.(x,y)=U1"\/"_os U2 by Def16;
then A1:o.(x,o.(y,z)) = U1 "\/"_os (U2"\/"_os U3) &
o.(o.(x,y),z) = (U1"\/"_os U2)"\/"_os U3 by Def16;
set B=(the Sorts of U1) \/ ((the Sorts of U2) \/ (the Sorts of U3));
A2: (the Sorts of U1) is OrderSortedSet of S1 & (the Sorts of U2) is
OrderSortedSet of S1 & (the Sorts of U3) is OrderSortedSet of S1
by OSALG_1:17; then A3:
(the Sorts of U1) \/ (the Sorts of U2) is OrderSortedSet of S1 &
(the Sorts of U2) \/ (the Sorts of U3) is OrderSortedSet of S1
by Th2;
then A4: B is OrderSortedSet of S1 by A2,Th2;
the Sorts of U1 is MSSubset of U0 & the Sorts of U2 is MSSubset of U0 &
the Sorts of U3 is MSSubset of U0 by MSUALG_2:def 10;
then A5:the Sorts of U1 c=the Sorts of U0 &
the Sorts of U2 c=the Sorts of U0 &
the Sorts of U3 c=the Sorts of U0 by MSUALG_2:def 1;
then A6:(the Sorts of U2) \/ (the Sorts of U3) c= the Sorts of U0
by PBOOLE:18;
A7:(the Sorts of U1) \/ (the Sorts of U2) c= the Sorts of U0
by A5,PBOOLE:18;
reconsider C1 =(the Sorts of U2) \/ (the Sorts of U3)
as MSSubset of U0 by A6,MSUALG_2:def 1;
reconsider C = C1 as OSSubset of U0 by A3,Def2;
reconsider D1=(the Sorts of U1) \/ (the Sorts of U2)
as MSSubset of U0 by A7,MSUALG_2:def 1;
reconsider D = D1 as OSSubset of U0 by A3,Def2;
B c= the Sorts of U0 by A5,A6,PBOOLE:18;
then B is MSSubset of U0 by MSUALG_2:def 1;
then reconsider B as OSSubset of U0 by A4,Def2;
A8:U1 "\/"_os (U2 "\/"_os U3) = U1 "\/"_os (GenOSAlg(C))
by Def14 .= (GenOSAlg(C)) "\/"_os U1 by Th44
.= GenOSAlg(B) by Th42;
A9:B= D \/ (the Sorts of U3) by PBOOLE:34;
(U1"\/"_os U2)"\/"_os U3 = GenOSAlg(D)"\/"_os U3 by Def14
.= GenOSAlg(B) by A9,Th42;
hence thesis by A1,A8;
end;
hence thesis by BINOP_1:def 3;
end;
theorem Th51:
OSAlg_meet(U0) is commutative
proof
set o = OSAlg_meet(U0);
set m = MSAlg_meet(U0);
A1: m is commutative by MSUALG_2:32;
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 Th48 .= m.(y,x) by A1,BINOP_1:def 2
.= o.(y,x) by Th48;
hence thesis;
end;
hence thesis by BINOP_1:def 2;
end;
theorem Th52:
OSAlg_meet(U0) is associative
proof
set o = OSAlg_meet(U0);
set m = MSAlg_meet(U0);
A1: m is associative by MSUALG_2:33;
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.(y,z) = m.(y,z) & o.(x,y) = m.(x,y) by Th48;
then o.(x,o.(y,z)) = m.(x,m.(y,z))
by Th48 .= m.(m.(x,y),z)
by A1,BINOP_1:def 3 .= o.(o.(x,y),z) by A2,Th48;
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 :Def18:
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 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 OSSub(U0);
A2:OSAlg_join(U0) is commutative by Th49;
thus a"\/" b =(OSAlg_join(U0)).(x,y) by LATTICES:def 1
.= (the L_join of L).(b,a) by A2,BINOP_1:def 2
.=b"\/" a by LATTICES:def 1;
end;
A3: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 OSSub(U0);
A4:OSAlg_join(U0) is associative by Th50;
thus a"\/" (b"\/" c) = (the L_join of L).(a,(b"\/" c))
by LATTICES:def 1
.=(OSAlg_join(U0)).(x,(OSAlg_join(U0)).(y,z)) by LATTICES:def 1
.= (the L_join of L).((the L_join of L).(a,b),c) by A4,BINOP_1:def 3
.=((the L_join of L).(a,b))"\/" c by LATTICES:def 1
.=(a"\/" b)"\/" c by LATTICES:def 1;
end;
A5: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);
A6:(OSAlg_join(U0)).((OSAlg_meet(U0)).(x,y),y)= y
proof
reconsider U1= x,U2=y as strict OSSubAlgebra of U0
by Def15;
(OSAlg_meet(U0)).(x,y) = U1 /\ U2 by Def17;
hence (OSAlg_join(U0)).((OSAlg_meet(U0)).(x,y),y)
= ((U1 /\ U2)"\/"_os U2) by Def16
.=y by Th46;
end;
thus (a"/\"b)"\/" b = (the L_join of L).((a"/\"b),b)
by LATTICES:def 1
.= b by A6,LATTICES:def 2;
end;
A7: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 OSSub(U0);
A8:OSAlg_meet(U0) is commutative by Th51;
thus a"/\"b =(OSAlg_meet(U0)).(x,y) by LATTICES:def 2
.= (the L_meet of L).(b,a) by A8,BINOP_1:def 2
.=b"/\"a by 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 OSSub(U0);
A10:OSAlg_meet(U0) is associative by Th52;
thus a"/\"(b"/\"c) = (the L_meet of L).(a,(b"/\"c)) by LATTICES:def 2
.=(OSAlg_meet(U0)).(x,(OSAlg_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"/\"(a"\/" b)=a
proof let a,b be Element of L;
reconsider x=a,y=b as Element of OSSub(U0);
A11:(OSAlg_meet(U0)).(x,(OSAlg_join(U0)).(x,y))= x
proof
reconsider U1= x,U2=y as strict OSSubAlgebra of U0 by Def15;
(OSAlg_join(U0)).(x,y) = U1"\/"_os U2 by Def16;
hence (OSAlg_meet(U0)).(x,(OSAlg_join(U0)).(x,y))
= (U1 /\( U1"\/"_os U2)) by Def17
.=x by Th45;
end;
thus a"/\"(a"\/" b) = (the L_meet of L).(a,(a"\/" b)) by LATTICES:def 2
.= a by A11,LATTICES:def 1;
end;
then L is strict join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing
by A1,A3,A5,A7,A9,LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
hence L is strict Lattice by LATTICES:def 10;
end;
end;
theorem Th53:
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);
A1: L = LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #)
by Def18;
thus L is lower-bounded
proof
set C = OSConstants(U0);
reconsider G = GenOSAlg(C) as Element of OSSub(U0) by Def15;
reconsider G1 = G as Element of L by A1;
take G1;
let a be Element of L;
reconsider a1 = a as Element of OSSub(U0) by A1;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def15;
thus G1 "/\" a =(OSAlg_meet(U0)).(G,a1) by A1,LATTICES:def 2
.= GenOSAlg(C) /\ a2 by Def17
.= G1 by Th41;
hence thesis;
end;
thus L is upper-bounded
proof
A2: the Sorts of U0 is OrderSortedSet of S1 by OSALG_1:17;
reconsider B = the Sorts of U0 as MSSubset of U0
by MSUALG_2:def 1;
reconsider B as OSSubset of U0 by A2,Def2;
reconsider G = GenOSAlg(B) as Element of OSSub(U0) by Def15;
reconsider G1 = G as Element of L by A1;
take G1;
let a be Element of L;
reconsider a1 = a as Element of OSSub(U0) by A1;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def15;
thus G1"\/" a =(OSAlg_join(U0)).(G1,a) by A1,LATTICES:def 1
.= GenOSAlg(B)"\/"_os a2 by Def16
.= G1 by Th43;
hence thesis;
end;
end;
definition let S1;
let U0 be non-empty OSAlgebra of S1;
cluster OSSubAlLattice(U0) -> bounded;
coherence by Th53;
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 L = OSSubAlLattice(U0);
A1: L = LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #)
by Def18;
set C = OSConstants(U0);
reconsider G = GenOSAlg(C) as Element of OSSub(U0) by Def15;
reconsider G1 = G as Element of L by A1;
now
let a be Element of L;
reconsider a1 = a as Element of OSSub(U0) by A1;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def15;
thus G1 "/\" a =(OSAlg_meet(U0)).(G,a1) by A1,LATTICES:def 2
.= GenOSAlg(C) /\ a2 by Def17
.= G1 by Th41;
hence a "/\" G1 = G1;
end;
hence thesis by LATTICES:def 16;
end;
theorem Th55:
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;
assume A1: B = the Sorts of U0;
set L = OSSubAlLattice(U0);
A2: L = LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #)
by Def18;
reconsider G = GenOSAlg(B) as Element of OSSub(U0) by Def15;
reconsider G1 = G as Element of L by A2;
now
let a be Element of L;
reconsider a1 = a as Element of OSSub(U0) by A2;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def15;
thus G1"\/" a =(OSAlg_join(U0)).(G1,a) by A2,LATTICES:def 1
.= GenOSAlg(B)"\/"_os a2 by Def16
.= G1 by A1,Th43;
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 MSUALG_2:def 1;
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 Th55
.= U0 by Th39;
end;