:: Subalgebras of a Many Sorted Algebra. Lattice of Subalgebras
:: by Ewa Burakowska
::
:: Received April 25, 1994
:: Copyright (c) 1994-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 PBOOLE, RELAT_1, XBOOLE_0, FUNCT_1, SUBSET_1, CARD_3, TARSKI,
STRUCT_0, MSUALG_1, UNIALG_2, FINSEQ_1, MARGREL1, PARTFUN1, FUNCT_2,
ZFMISC_1, QC_LANG1, SETFAM_1, EQREL_1, BINOP_1, LATTICES, XXREAL_2,
MSUALG_2, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
FUNCT_2, FINSEQ_1, SETFAM_1, FINSEQ_2, LATTICES, BINOP_1, CARD_3, PBOOLE,
MSUALG_1;
constructors SETFAM_1, BINOP_1, CARD_3, LATTICES, MSUALG_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, STRUCT_0,
LATTICES, MSUALG_1, FINSEQ_1, FUNCT_2, PARTFUN1, RELSET_1;
requirements BOOLE, SUBSET;
definitions TARSKI, PBOOLE, LATTICES, XBOOLE_0;
equalities LATTICES;
expansions TARSKI, PBOOLE, LATTICES;
theorems TARSKI, FUNCT_1, FINSEQ_1, PBOOLE, CARD_3, MSUALG_1, FUNCT_2,
ZFMISC_1, SETFAM_1, BINOP_1, LATTICES, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, FUNCOP_1, PARTFUN1, FINSEQ_2;
schemes CLASSES1, BINOP_1, FUNCT_1, XBOOLE_0;
begin
::
:: Auxiliary facts about Many Sorted Sets.
::
reserve x,y for object;
registration
let I be set, X be ManySortedSet of I, Y be non-empty ManySortedSet of I;
cluster X (\/) Y -> non-empty;
coherence
proof
let i be object;
assume
A1: i in I;
then (X (\/) Y).i = X.i \/ Y.i by PBOOLE:def 4;
hence thesis by A1;
end;
cluster Y (\/) X -> non-empty;
coherence;
end;
theorem Th1:
for I be non empty set, X, Y be ManySortedSet of I, i be Element
of I* holds product ((X (/\) Y)*i) = product(X * i) /\ product(Y * i)
proof
let I be non empty set, X, Y be ManySortedSet of I, i be Element of I*;
A1: rng i c= I by FINSEQ_1:def 4;
dom X = I by PARTFUN1:def 2;
then
A2: dom (X *i) = dom i by A1,RELAT_1:27;
dom(X (/\) Y) = I by PARTFUN1:def 2;
then
A3: dom((X (/\) Y)*i) = dom i by A1,RELAT_1:27;
dom Y =I by PARTFUN1:def 2;
then
A4: dom (Y *i)= dom i by A1,RELAT_1:27;
thus product ((X (/\) Y)*i) c= product(X * i) /\ product(Y * i)
proof
let x be object;
assume x in product((X (/\) Y) * i);
then consider g be Function such that
A5: x = g & dom g = dom ((X (/\) Y)*i) and
A6: for y being object st y in dom ((X (/\) Y)*i)
holds g.y in ((X (/\) Y)*i).y
by CARD_3:def 5;
for y being object st y in dom( Y*i) holds g.y in (Y *i).y
proof
let y be object;
assume
A7: y in dom(Y *i);
then g.y in ((X (/\) Y)*i).y by A4,A3,A6;
then
A8: g.y in (X (/\) Y).(i.y) by A4,A3,A7,FUNCT_1:12;
i.y in rng i by A4,A7,FUNCT_1:def 3;
then g.y in X.(i.y) /\ Y.(i.y) by A1,A8,PBOOLE:def 5;
then g.y in Y.(i.y) by XBOOLE_0:def 4;
hence thesis by A7,FUNCT_1:12;
end;
then
A9: x in product(Y *i) by A4,A3,A5,CARD_3:def 5;
for y being object st y in dom( X*i) holds g.y in (X *i).y
proof
let y be object;
assume
A10: y in dom(X *i);
then g.y in ((X (/\) Y)*i).y by A2,A3,A6;
then
A11: g.y in (X (/\) Y).(i.y) by A2,A3,A10,FUNCT_1:12;
i.y in rng i by A2,A10,FUNCT_1:def 3;
then g.y in X.(i.y) /\ Y.(i.y) by A1,A11,PBOOLE:def 5;
then g.y in X.(i.y) by XBOOLE_0:def 4;
hence thesis by A10,FUNCT_1:12;
end;
then x in product(X *i) by A2,A3,A5,CARD_3:def 5;
hence thesis by A9,XBOOLE_0:def 4;
end;
let x be object;
assume
A12: x in (product(X * i) /\ product(Y * i));
then x in product(X * i) by XBOOLE_0:def 4;
then consider g be Function such that
A13: x = g and
A14: dom g = dom (X *i) and
A15: for y being object st y in dom (X *i) holds g.y in (X *i).y
by CARD_3:def 5;
x in product(Y * i) by A12,XBOOLE_0:def 4;
then
A16: ex h be Function st x = h & dom h = dom (Y *i) &
for y being object st y in dom (Y *i
) holds h.y in (Y *i).y by CARD_3:def 5;
for y being object st y in dom((X (/\) Y)*i)
holds g.y in ((X (/\) Y) *i).y
proof
let y be object;
assume
A17: y in dom((X (/\) Y)*i);
then
A18: i.y in rng i by A3,FUNCT_1:def 3;
g.y in (X *i).y by A2,A3,A15,A17;
then
A19: g.y in X.(i.y) by A2,A3,A17,FUNCT_1:12;
g.y in (Y *i).y by A4,A3,A13,A16,A17;
then g.y in Y.(i.y) by A4,A3,A17,FUNCT_1:12;
then g.y in (X.(i.y) /\ Y.(i.y)) by A19,XBOOLE_0:def 4;
then g.y in (X (/\) Y).(i.y) by A1,A18,PBOOLE:def 5;
hence thesis by A17,FUNCT_1:12;
end;
hence thesis by A2,A3,A13,A14,CARD_3:def 5;
end;
begin
::
:: Constants of a Many Sorted Algebra.
::
reserve S for non void non empty ManySortedSign,
o for OperSymbol of S,
U0,U1, U2 for MSAlgebra over S;
definition
let S be non empty ManySortedSign, U0 be MSAlgebra over S;
mode MSSubset of U0 is ManySortedSubset of the Sorts of U0;
end;
definition
let S be non empty ManySortedSign;
let IT be SortSymbol of S;
attr IT is with_const_op means
ex o be OperSymbol of S st (the Arity
of S).o = {} & (the ResultSort of S).o = IT;
end;
definition
let IT be non empty ManySortedSign;
attr IT is all-with_const_op means
:Def2:
for s be SortSymbol of IT holds s is with_const_op;
end;
registration
let A be non empty set, B be set, a be Function of B,A*, r be Function of B,
A;
cluster ManySortedSign(#A,B,a,r#) -> non empty;
coherence;
end;
registration
cluster non void all-with_const_op strict for non empty ManySortedSign;
existence
proof
set x = the set;
set C = {x};
consider a be Function such that
A1: dom a = C and
A2: rng a = {<*>C} by FUNCT_1:5;
rng a c= C*
proof
let y be object;
assume y in rng a;
then y = <*>C by A2,TARSKI:def 1;
hence thesis by FINSEQ_1:def 11;
end;
then reconsider a as Function of C,C* by A1,FUNCT_2:def 1,RELSET_1:4;
consider r be Function such that
A3: dom r = C and
A4: rng r = {x} by FUNCT_1:5;
reconsider r as Function of C,C by A3,A4,FUNCT_2:def 1,RELSET_1:4;
set M = ManySortedSign (#C,C,a,r#);
take M;
thus M is non void;
for s be SortSymbol of M holds s is with_const_op
proof
reconsider o = x as OperSymbol of M by TARSKI:def 1;
let s be SortSymbol of M;
take o;
a.o in rng a by A1,FUNCT_1:def 3;
hence (the Arity of M).o = {} by A2,TARSKI:def 1;
s=x & r.o in rng r by A3,FUNCT_1:def 3,TARSKI:def 1;
hence thesis by A4,TARSKI:def 1;
end;
hence M is all-with_const_op;
thus thesis;
end;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, s be
SortSymbol of S;
func Constants(U0,s) -> Subset of (the Sorts of U0).s means
:Def3:
ex A
being non empty set st A =(the Sorts of U0).s & it = { a where a is Element of
A: ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).
o = s & a in rng Den(o,U0)} if (the Sorts of U0).s <> {} otherwise it = {};
existence
proof
hereby
assume (the Sorts of U0).s <> {};
then reconsider A = (the Sorts of U0).s as non empty set;
set E = {a where a is Element of A : ex o be OperSymbol of S st (the
Arity of S).o={} & (the ResultSort of S).o = s & a in rng Den(o,U0)};
E c= A
proof
let x be object;
assume x in E;
then
ex w be Element of (the Sorts of U0).s st w=x & ex o be OperSymbol
of S st (the Arity of S).o={} & (the ResultSort of S).o = s & w in rng Den(o,U0
);
hence thesis;
end;
then reconsider E as Subset of (the Sorts of U0).s;
take E,A;
thus A =(the Sorts of U0).s & E = { a where a is Element of A : ex o be
OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = s & a in
rng Den(o,U0)};
end;
assume (the Sorts of U0).s = {};
take {}((the Sorts of U0).s);
thus thesis;
end;
correctness;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
func Constants (U0) -> MSSubset of U0 means
:Def4:
for s be SortSymbol of S holds it.s = Constants(U0,s);
existence
proof
deffunc G(SortSymbol of S) = Constants(U0,$1);
consider f be Function such that
A1: dom f = the carrier of S & for d be SortSymbol of S holds f.d = G(
d) from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
f c= the Sorts of U0
proof
let s be object;
assume s in the carrier of S;
then reconsider s1 = s as SortSymbol of S;
f.s1 = Constants(U0,s1) by A1;
hence thesis;
end;
then reconsider f as MSSubset of U0 by PBOOLE:def 18;
take f;
thus thesis by A1;
end;
uniqueness
proof
let W1, W2 be MSSubset of U0;
assume that
A2: for s be SortSymbol of S holds W1.s = Constants(U0,s) and
A3: for s be SortSymbol of S holds W2.s = Constants(U0,s);
for s be object st s in the carrier of S holds W1.s = W2.s
proof
let s be object;
assume s in the carrier of S;
then reconsider t = s as SortSymbol of S;
W1.t = Constants(U0,t) by A2;
hence thesis by A3;
end;
hence thesis;
end;
end;
registration
let S be all-with_const_op non void non empty ManySortedSign, U0 be
non-empty MSAlgebra over S, s be SortSymbol of S;
cluster Constants(U0,s) -> non empty;
coherence
proof
dom {} = {} & rng {} = {};
then reconsider a = {} as Function of {},{} by FUNCT_2:1;
s is with_const_op by Def2;
then consider o be OperSymbol of S such that
A1: (the Arity of S).o = {} and
A2: (the ResultSort of S).o = s;
A3: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1;
then dom ((the Sorts of U0)# qua ManySortedSet of(the carrier of S)*) = (
the carrier of S)* & (the Arity of S).o in rng (the Arity of S) by
FUNCT_1:def 3,PARTFUN1:def 2;
then
A4: o in dom ((the Sorts of U0)# * the Arity of S) by A3,FUNCT_1:11;
Args(o,U0) = ((the Sorts of U0)# * the Arity of S).o by MSUALG_1:def 4
.= (the Sorts of U0)# . ((the Arity of S).o) by A4,FUNCT_1:12
.= (the Sorts of U0)# . (the_arity_of o) by MSUALG_1:def 1
.= product ((the Sorts of U0) * (the_arity_of o)) by FINSEQ_2:def 5
.= product ((the Sorts of U0) * a) by A1,MSUALG_1:def 1
.= {{}} by CARD_3:10;
then
A5: {} in Args(o,U0) by TARSKI:def 1;
set f = Den(o,U0);
A6: rng f c= Result(o,U0) by RELAT_1:def 19;
dom f = Args (o,U0) by FUNCT_2:def 1;
then
A7: f.{} in rng f by A5,FUNCT_1:def 3;
A8: dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
then
dom (the Sorts of U0) = the carrier of S & (the ResultSort of S).o in
rng ( the ResultSort of S) by FUNCT_1:def 3,PARTFUN1:def 2;
then
A9: o in dom ((the Sorts of U0) * the ResultSort of S) by A8,FUNCT_1:11;
Result(o,U0) = ((the Sorts of U0) * the ResultSort of S).o by
MSUALG_1:def 5
.= (the Sorts of U0).s by A2,A9,FUNCT_1:12;
then reconsider a = f.{} as Element of (the Sorts of U0).s by A6,A7;
ex A being non empty set st A =(the Sorts of U0).s & Constants(U0,s)
= { b where b is Element of A : ex o be OperSymbol of S st (the Arity of S).o =
{} & (the ResultSort of S).o = s & b in rng Den(o,U0)} by Def3;
then a in Constants (U0,s) by A1,A2,A7;
hence thesis;
end;
end;
registration
let S be non void all-with_const_op non empty ManySortedSign, U0 be
non-empty MSAlgebra over S;
cluster Constants(U0) -> non-empty;
coherence
proof
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
(Constants(U0)).s = Constants(U0,s) by Def4;
hence (Constants(U0)).i is non empty;
end;
hence thesis;
end;
end;
begin
::
:: Subalgebras of a Many Sorted Algebra.
::
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be
OperSymbol of S, A be MSSubset of U0;
pred A is_closed_on o means
rng ((Den(o,U0))|((A# * the Arity of S).o )) c= (A * the ResultSort of S).o;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
attr A is opers_closed means
for o be OperSymbol of S holds A is_closed_on o;
end;
theorem Th2:
for S be non void non empty ManySortedSign, o be OperSymbol of S,
U0 be MSAlgebra over S, B0, B1 be MSSubset of U0 st B0 c= B1 holds ((B0# * the
Arity of S).o) c= ((B1# * the Arity of S).o)
proof
let S be non void non empty ManySortedSign, o be OperSymbol of S, U0 be
MSAlgebra over S, B0, B1 be MSSubset of U0;
reconsider a = (the Arity of S).o as Element of (the carrier of S)*;
A1: rng a c= the carrier of S by FINSEQ_1:def 4;
A2: dom B0 = the carrier of S by PARTFUN1:def 2;
then
A3: dom (B0 * a) = dom a by A1,RELAT_1:27;
assume
A4: B0 c= B1;
A5: for x being object st x in dom (B0 * a) holds (B0*a).x c= (B1 * a).x
proof
let x be object;
assume
A6: x in dom (B0 * a);
then a.x in rng a by A3,FUNCT_1:def 3;
then B0.(a.x) c= B1.(a.x) by A4,A1;
then (B0*a).x c= B1.(a.x) by A3,A6,FUNCT_1:13;
hence thesis by A3,A6,FUNCT_1:13;
end;
A7: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1;
then dom (B0# * the Arity of S) = dom (the Arity of S) by PARTFUN1:def 2;
then (B0# * the Arity of S).o = B0#.a by A7,FUNCT_1:12;
then
A8: (B0# * the Arity of S).o = product (B0 * a) by FINSEQ_2:def 5;
dom (B1# * the Arity of S) = dom (the Arity of S) by A7,PARTFUN1:def 2;
then (B1# * the Arity of S).o = B1#.a by A7,FUNCT_1:12;
then
A9: (B1# * the Arity of S).o = product (B1 * a) by FINSEQ_2:def 5;
dom B1 = the carrier of S by PARTFUN1:def 2;
then dom (B1 * a) = dom a by A1,RELAT_1:27;
hence thesis by A8,A9,A2,A1,A5,CARD_3:27,RELAT_1:27;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be
OperSymbol of S, A be MSSubset of U0;
assume
A1: A is_closed_on o;
func o/.A ->Function of (A# * the Arity of S).o, (A * the ResultSort of S).o
equals
:Def7:
(Den(o,U0)) | ((A# * the Arity of S).o);
coherence
proof
set f = (Den(o,U0)) | ((A# * the Arity of S).o), B = the Sorts of U0;
A2: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
per cases;
suppose
A3: (A * the ResultSort of S).o = {};
rng f c= (A * the ResultSort of S).o by A1;
then
A4: f = {} by A3;
now
per cases;
suppose
(A# * the Arity of S).o = {};
hence thesis by A4,RELSET_1:12;
end;
suppose
(A# * the Arity of S).o <> {};
thus thesis by A3,A4,FUNCT_2:def 1,RELSET_1:12;
end;
end;
hence thesis;
end;
suppose
A5: (A * the ResultSort of S).o <> {};
reconsider B0 = B as MSSubset of U0 by PBOOLE:def 18;
A6: A c= B0 by PBOOLE:def 18;
A7: rng f c= (A * the ResultSort of S).o by A1;
A c= B by PBOOLE:def 18;
then A.((the ResultSort of S).o) c= B.((the ResultSort of S).o);
then B.((the ResultSort of S).o) <> {} by A2,A5,FUNCT_1:13;
then (B * the ResultSort of S).o <> {} by A2,FUNCT_1:13;
then Result(o,U0) <> {} by MSUALG_1:def 5;
then dom Den(o,U0) = Args(o,U0) by FUNCT_2:def 1
.= (B# * the Arity of S).o by MSUALG_1:def 4;
then dom f = ((B# * the Arity of S).o) /\ ((A# * the Arity of S).o) by
RELAT_1:61
.= (A# * the Arity of S).o by A6,Th2,XBOOLE_1:28;
hence thesis by A7,FUNCT_2:2;
end;
end;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
func Opers(U0,A) -> ManySortedFunction of (A# * the Arity of S),(A * the
ResultSort of S) means
:Def8:
for o be OperSymbol of S holds it.o = o/.A;
existence
proof
set B= A# * the Arity of S, C= A * the ResultSort of S;
defpred P[object,object] means
for o be OperSymbol of S st o = $1 holds $2=o/.A;
A1: for x being object st x in the carrier' of S ex y being object st P[x,y]
proof
let x be object;
assume x in the carrier' of S;
then reconsider o=x as OperSymbol of S;
take o/.A;
thus thesis;
end;
consider f be Function such that
A2: dom f = the carrier' of S &
for x being object st x in the carrier' of S holds
P[x,f.x] from CLASSES1:sch 1(A1);
reconsider f as ManySortedSet of the carrier' of S by A2,PARTFUN1:def 2
,RELAT_1:def 18;
for x being object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then reconsider o=x as OperSymbol of S by A2;
f.o = o/.A by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of the carrier' of S by
FUNCOP_1:def 6;
for x st x in the carrier' of S holds f.x is Function of B.x,C.x
proof
let x;
assume x in the carrier' of S;
then reconsider o=x as OperSymbol of S;
f.o = o/.A by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of B,C by PBOOLE:def 15;
take f;
let o be OperSymbol of S;
thus thesis by A2;
end;
uniqueness
proof
let f1, f2 be ManySortedFunction of (A# * the Arity of S),(A * the
ResultSort of S);
assume that
A3: for o be OperSymbol of S holds f1.o = o/.A and
A4: for o be OperSymbol of S holds f2.o = o/.A;
for x being object st x in (the carrier' of S) holds f1.x = f2.x
proof
let x be object;
assume x in (the carrier' of S);
then reconsider o1 = x as OperSymbol of S;
f1.o1 = o1/.A by A3;
hence thesis by A4;
end;
hence thesis;
end;
end;
theorem Th3:
for U0 being MSAlgebra over S for B being MSSubset of U0 st B=the
Sorts of U0 holds B is opers_closed & for o holds o/.B = Den(o,U0)
proof
let U0 be MSAlgebra over S;
let B be MSSubset of U0;
assume
A1: B=the Sorts of U0;
thus
A2: B is opers_closed
proof
let o;
Result (o,U0) = (B* the ResultSort of S).o by A1,MSUALG_1:def 5;
hence rng ((Den(o,U0))|((B# * the Arity of S).o)) c= (B * the ResultSort
of S).o by RELAT_1:def 19;
end;
let o;
B is_closed_on o by A2;
then
A3: o/.B = (Den(o,U0))|((B# * the Arity of S).o) by Def7;
per cases;
suppose
(B * the ResultSort of S).o = {};
then Result(o,U0) = {} by A1,MSUALG_1:def 5;
then Den(o,U0) = {};
hence thesis by A3;
end;
suppose
(B * the ResultSort of S).o <> {};
Args(o,U0) = (B# * the Arity of S).o by A1,MSUALG_1:def 4;
hence thesis by A3;
end;
end;
theorem Th4:
for B being MSSubset of U0 st B=the Sorts of U0 holds Opers(U0,B)
= the Charact of U0
proof
let B be MSSubset of U0;
set f1 = the Charact of U0, f2 = Opers(U0,B);
assume
A1: B=the Sorts of U0;
for x being object st x in (the carrier' of S) holds f1.x = f2.x
proof
let x be object;
assume x in (the carrier' of S);
then reconsider o1 = x as OperSymbol of S;
f1.o1 = Den(o1,U0) & f2.o1 = o1/.B by Def8,MSUALG_1:def 6;
hence thesis by A1,Th3;
end;
hence thesis;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
mode MSSubAlgebra of U0 -> MSAlgebra over S means
:Def9:
the Sorts of it is
MSSubset of U0 & for B be MSSubset of U0 st B = the Sorts of it holds B is
opers_closed & the Charact of it = Opers(U0,B);
existence
proof
take U1 = U0;
thus the Sorts of U1 is MSSubset of U0 by PBOOLE:def 18;
let B be MSSubset of U0;
set f1 = the Charact of U1, f2 = Opers(U0,B);
assume
A1: B=the Sorts of U1;
hence B is opers_closed by Th3;
for x being object st x in (the carrier' of S) holds f1.x = f2.x
proof
let x be object;
assume x in (the carrier' of S);
then reconsider o1 = x as OperSymbol of S;
f1.o1 = Den(o1,U1) & f2.o1 = o1/.B by Def8,MSUALG_1:def 6;
hence thesis by A1,Th3;
end;
hence thesis;
end;
end;
Lm1: for S being non void non empty ManySortedSign, U0 being MSAlgebra over S
holds MSAlgebra (#the Sorts of U0,the Charact of U0#) is MSSubAlgebra of U0
proof
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
reconsider A = MSAlgebra (#the Sorts of U0,the Charact of U0#) as strict
MSAlgebra over S;
now
thus the Sorts of A is MSSubset of U0 by PBOOLE:def 18;
let B be MSSubset of U0;
set f1 = the Charact of A, f2 = Opers(U0,B);
assume
A1: B=the Sorts of A;
hence B is opers_closed by Th3;
for x being object st x in (the carrier' of S) holds f1.x = f2.x
proof
let x be object;
assume x in (the carrier' of S);
then reconsider o1 = x as Element of the carrier' of S;
f1.o1 = Den(o1,U0) & f2.o1 = o1/.B by Def8,MSUALG_1:def 6;
hence thesis by A1,Th3;
end;
hence the Charact of A = Opers(U0,B);
end;
hence thesis by Def9;
end;
registration
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
cluster strict for MSSubAlgebra of U0;
existence
proof
MSAlgebra (#the Sorts of U0,the Charact of U0#) is MSSubAlgebra of U0
by Lm1;
hence thesis;
end;
end;
registration
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
cluster MSAlgebra (#the Sorts of U0,the Charact of U0#) -> non-empty;
coherence by MSUALG_1:def 3;
end;
registration
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
cluster non-empty strict for MSSubAlgebra of U0;
existence
proof
MSAlgebra (#the Sorts of U0,the Charact of U0#) is MSSubAlgebra of U0
by Lm1;
hence thesis;
end;
end;
theorem
the MSAlgebra of U0 = the MSAlgebra of U1 implies U0 is MSSubAlgebra of U1
proof assume
A1: the MSAlgebra of U0 = the MSAlgebra of U1;
hence the Sorts of U0 is MSSubset of U1 by PBOOLE:def 18;
let B be MSSubset of U1;
set f1 = the Charact of U0, f2 = Opers(U1,B);
assume
A2: B=the Sorts of U0;
thus
B is opers_closed
proof let o be OperSymbol of S;
(Den(o,U1))|((B#*the Arity of S).o) c= Den(o,U1) by RELAT_1:59; then
rng((Den(o,U1))|((B#*the Arity of S).o)) c= rng Den(o,U1) & rng Den(o,U1)
c= Result(o,U1) & Result(o,U1) = (B*the ResultSort of S).o
by A1,A2,MSUALG_1:def 5,RELAT_1:11,def 19;
hence rng ((Den(o,U1))|((B#*the Arity of S).o)) c=
(B*the ResultSort of S).o;
end;
for x being object st x in (the carrier' of S) holds f1.x = f2.x
by A1,A2,Th4;
hence thesis;
end;
theorem
U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 implies U0 is
MSSubAlgebra of U2
proof
assume that
A1: U0 is MSSubAlgebra of U1 and
A2: U1 is MSSubAlgebra of U2;
reconsider B0 = the Sorts of U0 as MSSubset of U1 by A1,Def9;
A3: B0 is opers_closed by A1,Def9;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by A2,Def9;
A4: B1 is opers_closed by A2,Def9;
reconsider B19= B1 as MSSubset of U1 by PBOOLE:def 18;
A5: the Charact of U1 = Opers (U2,B1) by A2,Def9;
the Sorts of U0 is MSSubset of U1 by A1,Def9;
then
A6: the Sorts of U0 c= the Sorts of U1 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U2 by A2,Def9;
then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def 18;
then the Sorts of U0 c= the Sorts of U2 by A6,PBOOLE:13;
hence the Sorts of U0 is MSSubset of U2 by PBOOLE:def 18;
let B be MSSubset of U2;
set O = the Charact of U0, P = Opers(U2,B);
A7: the Charact of U0 = Opers (U1,B0) by A1,Def9;
assume
A8: B = the Sorts of U0;
A9: for o be OperSymbol of S holds B is_closed_on o
proof
let o be OperSymbol of S;
A10: B0 is_closed_on o by A3;
A11: B1 is_closed_on o by A4;
A12: Den(o,U1) = Opers(U2,B1).o by A5,MSUALG_1:def 6
.= o/.B1 by Def8
.= (Den(o,U2))|((B1# * the Arity of S).o) by A11,Def7;
A13: ((B0# * the Arity of S).o) c= ((B19# * the Arity of S).o) by A6,Th2;
Den(o,U0) = Opers(U1,B0).o by A7,MSUALG_1:def 6
.= o/.B0 by Def8
.= ((Den(o,U2))|((B1# * the Arity of S).o))|((B0# * the Arity of S).o)
by A10,A12,Def7
.= (Den(o,U2))|(((B1# * the Arity of S).o)/\((B0# * the Arity of S).o)
) by RELAT_1:71
.= (Den(o,U2))|((B0# * the Arity of S).o) by A13,XBOOLE_1:28;
then rng ((Den(o,U2))|((B0# * the Arity of S).o)) c= Result(o,U0) by
RELAT_1:def 19;
then rng ((Den(o,U2))|((B0# * the Arity of S).o)) c= ((the Sorts of U0) *
the ResultSort of S).o by MSUALG_1:def 5;
hence thesis by A8;
end;
hence B is opers_closed;
for x being object st x in the carrier' of S holds O.x =P.x
proof
let x be object;
assume x in the carrier' of S;
then reconsider o = x as OperSymbol of S;
A14: B0 is_closed_on o by A3;
A15: B1 is_closed_on o by A4;
A16: Den(o,U1) = Opers(U2,B1).o by A5,MSUALG_1:def 6
.= o/.B1 by Def8
.= (Den(o,U2))|((B1# * the Arity of S).o) by A15,Def7;
thus O.x = o/.B0 by A7,Def8
.= ((Den(o,U2))|((B1# * the Arity of S).o))|((B0# * the Arity of S).o)
by A14,A16,Def7
.= (Den(o,U2))|(((B1# * the Arity of S).o)/\((B0# * the Arity of S).o)
) by RELAT_1:71
.= (Den(o,U2))|((B# * the Arity of S).o) by A6,A8,Th2,XBOOLE_1:28
.= o/.B by A9,Def7
.= P.x by Def8;
end;
hence thesis;
end;
theorem Th7:
U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1
implies the MSAlgebra of U1 = the MSAlgebra of U2
proof
assume that
A1: U1 is MSSubAlgebra of U2 and
A2: U2 is MSSubAlgebra of U1;
the Sorts of U2 is MSSubset of U1 by A2,Def9;
then
A3: the Sorts of U2 c= the Sorts of U1 by PBOOLE:def 18;
reconsider B1 = the Sorts of U1 as MSSubset of U2 by A1,Def9;
A4: the Charact of U1 = Opers(U2,B1) by A1,Def9;
reconsider B2 = the Sorts of U2 as MSSubset of U1 by A2,Def9;
A5: the Charact of U2 = Opers(U1,B2) by A2,Def9;
the Sorts of U1 is MSSubset of U2 by A1,Def9;
then the Sorts of U1 c= the Sorts of U2 by PBOOLE:def 18;
then
A6: the Sorts of U1 = the Sorts of U2 by A3,PBOOLE:146;
set O = the Charact of U1, P = Opers(U1,B2);
A7: B1 is opers_closed by A1,Def9;
for x being object st x in the carrier' of S holds O.x = P.x
proof
let x be object;
assume x in the carrier' of S;
then reconsider o = x as OperSymbol of S;
A8: Args(o,U2) = (B2# * the Arity of S).o by MSUALG_1:def 4;
A9: B1 is_closed_on o by A7;
thus O.x = o/.B1 by A4,Def8
.= (Den(o,U2))|((B1# * the Arity of S).o) by A9,Def7
.= Den(o,U2) by A6,A8
.= P.x by A5,MSUALG_1:def 6;
end;
hence thesis by A6,A5,PBOOLE:3;
end;
theorem Th8:
for U1,U2 be MSSubAlgebra of U0 st the Sorts of U1 c= the Sorts
of U2 holds U1 is MSSubAlgebra of U2
proof
let U1, U2 be MSSubAlgebra of U0;
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as MSSubset of U0 by
Def9;
assume
A1: the Sorts of U1 c= the Sorts of U2;
hence the Sorts of U1 is MSSubset of U2 by PBOOLE:def 18;
let B be MSSubset of U2;
A2: B1 is opers_closed by Def9;
set O = the Charact of U1, P = Opers(U2,B);
A3: the Charact of U1 = Opers(U0,B1) by Def9;
A4: B2 is opers_closed by Def9;
A5: the Charact of U2 = Opers(U0,B2) by Def9;
assume
A6: B = the Sorts of U1;
A7: for o be OperSymbol of S holds B is_closed_on o
proof
let o be OperSymbol of S;
A8: B1 is_closed_on o by A2;
A9: B2 is_closed_on o by A4;
A10: Den(o,U2) = Opers(U0,B2).o by A5,MSUALG_1:def 6
.= o/.B2 by Def8
.= (Den(o,U0))|((B2# * the Arity of S).o) by A9,Def7;
Den(o,U1) = Opers(U0,B1).o by A3,MSUALG_1:def 6
.= o/.B1 by Def8
.= (Den(o,U0))|((B1# * the Arity of S).o) by A8,Def7
.= (Den(o,U0))|(((B2# * the Arity of S).o) /\ ((B1# * the Arity of S).
o)) by A1,Th2,XBOOLE_1:28
.= (Den(o,U2))|((B1# * the Arity of S).o) by A10,RELAT_1:71;
then rng ((Den(o,U2))|((B1# * the Arity of S).o)) c= Result(o,U1) by
RELAT_1:def 19;
then rng ((Den(o,U2))|((B1# * the Arity of S).o)) c= ((the Sorts of U1) *
the ResultSort of S).o by MSUALG_1:def 5;
hence thesis by A6;
end;
hence B is opers_closed;
for x being object st x in the carrier' of S holds O.x =P.x
proof
let x be object;
assume x in the carrier' of S;
then reconsider o = x as OperSymbol of S;
A11: B1 is_closed_on o by A2;
A12: B2 is_closed_on o by A4;
A13: Den(o,U2) = Opers(U0,B2).o by A5,MSUALG_1:def 6
.= o/.B2 by Def8
.= (Den(o,U0))|((B2# * the Arity of S).o) by A12,Def7;
thus O.x = o/.B1 by A3,Def8
.= (Den(o,U0))|((B1# * the Arity of S).o) by A11,Def7
.= (Den(o,U0))|(((B2# * the Arity of S).o) /\ ((B1# * the Arity of S).
o)) by A1,Th2,XBOOLE_1:28
.= (Den(o,U2))|((B1# * the Arity of S).o) by A13,RELAT_1:71
.= o/.B by A6,A7,Def7
.= P.x by Def8;
end;
hence thesis;
end;
theorem Th9:
for U1,U2 be MSSubAlgebra of U0 st the Sorts of U1 = the
Sorts of U2 holds the MSAlgebra of U1 = the MSAlgebra of U2
proof
let U1,U2 be MSSubAlgebra of U0;
assume the Sorts of U1 = the Sorts of U2;
then U1 is MSSubAlgebra of U2 & U2 is MSSubAlgebra of U1 by Th8;
hence thesis by Th7;
end;
theorem Th10:
for S be non void non empty ManySortedSign, U0 be MSAlgebra over
S, U1 be MSSubAlgebra of U0 holds Constants(U0) is MSSubset of U1
proof
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, U1 be
MSSubAlgebra of U0;
Constants(U0) c= the Sorts of U1
proof
let x be object;
assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
thus (Constants(U0)).x c= (the Sorts of U1).x
proof
let y be object;
per cases;
suppose
A1: (the Sorts of U0).s = {};
(Constants(U0)).s = Constants(U0,s) by Def4
.= {} by A1;
hence thesis;
end;
suppose
(the Sorts of U0).s <> {};
then
A2: ex A being non empty set st A =(the Sorts of U0).s & Constants(U0,
s) = { b where b is Element of A : ex o be OperSymbol of S st (the Arity of S).
o = {} & (the ResultSort of S).o = s & b in rng Den(o,U0)} by Def3;
reconsider u1=the Sorts of U1 as MSSubset of U0 by Def9;
assume
A3: y in (Constants(U0)).x;
(Constants(U0)).x = Constants(U0,s) by Def4;
then consider b be Element of (the Sorts of U0).s such that
A4: b=y and
A5: ex o be OperSymbol of S st (the Arity of S).o={} & (the
ResultSort of S).o = s & b in rng Den(o,U0) by A3,A2;
consider o be OperSymbol of S such that
A6: (the Arity of S).o = {} and
A7: (the ResultSort of S).o = s and
A8: b in rng Den(o,U0) by A5;
A9: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1;
then
A10: (the Arity of S).o in rng (the Arity of S) by FUNCT_1:def 3;
dom {} = {} & rng {} = {};
then reconsider a = {} as Function of {},{} by FUNCT_2:1;
A11: dom (the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
dom (u1# qua ManySortedSet of(the carrier of S)* ) = (the carrier
of S) * by PARTFUN1:def 2;
then o in dom (u1# * the Arity of S) by A9,A10,FUNCT_1:11;
then
A12: (u1# * the Arity of S).o = u1# . ((the Arity of S).o) by FUNCT_1:12
.= u1# . (the_arity_of o) by MSUALG_1:def 1
.= product (u1 * (the_arity_of o)) by FINSEQ_2:def 5
.= product (u1 * a) by A6,MSUALG_1:def 1
.= {{}} by CARD_3:10;
dom ((the Sorts of U0)# qua ManySortedSet of(the carrier of S)*)
= (the carrier of S)* by PARTFUN1:def 2;
then
A13: o in dom ((the Sorts of U0)# * the Arity of S) by A9,A10,FUNCT_1:11;
u1 is opers_closed by Def9;
then u1 is_closed_on o;
then
A14: rng ((Den(o,U0))|((u1# * the Arity of S).o)) c=(u1*the ResultSort
of S).o;
rng Den(o,U0) c= Result(o,U0) by RELAT_1:def 19;
then dom (Den (o,U0)) = Args(o,U0) by A8,FUNCT_2:def 1
.= ((the Sorts of U0)# * the Arity of S).o by MSUALG_1:def 4
.= (the Sorts of U0)# . ((the Arity of S).o) by A13,FUNCT_1:12
.= (the Sorts of U0)# . (the_arity_of o) by MSUALG_1:def 1
.= product ((the Sorts of U0) * (the_arity_of o)) by FINSEQ_2:def 5
.= product ((the Sorts of U0) * a) by A6,MSUALG_1:def 1
.= {{}} by CARD_3:10;
then (Den(o,U0))|((u1# * the Arity of S).o) =(Den(o,U0)) by A12;
then b in (u1*the ResultSort of S).o by A8,A14;
hence thesis by A4,A7,A11,FUNCT_1:13;
end;
end;
end;
hence thesis by PBOOLE:def 18;
end;
theorem
for S be non void all-with_const_op non empty ManySortedSign, U0 be
non-empty MSAlgebra over S, U1 be non-empty MSSubAlgebra of U0 holds Constants(
U0) is non-empty MSSubset of U1 by Th10;
theorem
for S be non void all-with_const_op non empty ManySortedSign, U0 be
non-empty MSAlgebra over S, U1,U2 be non-empty MSSubAlgebra of U0 holds (the
Sorts of U1) (/\) (the Sorts of U2) is non-empty
proof
let S be non void all-with_const_op non empty ManySortedSign, U0 be
non-empty MSAlgebra over S, U1,U2 be non-empty MSSubAlgebra of U0;
Constants(U0) is non-empty MSSubset of U2 by Th10;
then
A1: Constants(U0)c=the Sorts of U2 by PBOOLE:def 18;
Constants(U0) is non-empty MSSubset of U1 by Th10;
then Constants(U0)c=the Sorts of U1 by PBOOLE:def 18;
then
A2: (Constants(U0)) (/\) (Constants(U0))
c= (the Sorts of U1) (/\) (the Sorts of U2) by A1,PBOOLE:21;
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
((the Sorts of U1) (/\) (the Sorts of U2)).s = ((the Sorts of U1).s) /\
((the Sorts of U2).s) by PBOOLE:def 5;
then
A3: (Constants (U0)).s c= ((the Sorts of U1).s) /\ ((the Sorts of U2). s)
by A2;
ex a be object st a in (Constants(U0)).s by XBOOLE_0:def 1;
hence ((the Sorts of U1) (/\) (the Sorts of U2)).i is non empty by A3,
PBOOLE:def 5;
end;
hence thesis;
end;
begin
::
:: Many Sorted Subsets of a Many Sorted Algebra.
::
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
func SubSort(A) -> set means
:Def10:
for x be object holds x in it iff x in
Funcs(the carrier of S, bool (Union (the Sorts of U0))) & x is MSSubset of U0 &
for B be MSSubset of U0 st B = x holds B is opers_closed & Constants(U0) c= B &
A c= B;
existence
proof
defpred P[object] means
$1 is MSSubset of U0 & for B be MSSubset of U0 st B =
$1 holds B is opers_closed & Constants(U0) c= B & A c= B;
consider X be set such that
A1: for x be object holds x in X iff x in Funcs(the carrier of S, bool (
Union (the Sorts of U0))) & P[x] from XBOOLE_0:sch 1;
take X;
thus thesis by A1;
end;
uniqueness
proof
defpred P[object] means
$1 in Funcs(the carrier of S, bool (Union (the Sorts
of U0))) & $1 is MSSubset of U0 & for B be MSSubset of U0 st B = $1 holds B is
opers_closed & Constants(U0) c= B & A c= B;
for X1,X2 being set st
(for x be object holds x in X1 iff P[x]) & (for x
be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
hence thesis;
end;
end;
Lm2: for S being non void non empty ManySortedSign, U0 being MSAlgebra over S,
A being MSSubset of U0 holds the Sorts of U0 in SubSort(A)
proof
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
set f = Funcs(the carrier of S, bool (Union (the Sorts of U0)));
(Union (the Sorts of U0)) = union rng(the Sorts of U0) by CARD_3:def 4;
then
dom (the Sorts of U0) = the carrier of S & rng(the Sorts of U0) c= bool(
Union (the Sorts of U0)) by PARTFUN1:def 2,ZFMISC_1:82;
then
A1: the Sorts of U0 in f by FUNCT_2:def 2;
the Sorts of U0 is MSSubset of U0 & for B be MSSubset of U0 st B = the
Sorts of U0 holds B is opers_closed & Constants(U0) c= B & A c= B by Th3,
PBOOLE:def 18;
hence thesis by A1,Def10;
end;
registration
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
cluster SubSort(A) -> non empty;
coherence by Lm2;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
func SubSort(U0) -> set means
:Def11:
for x be object holds x in it iff x in
Funcs(the carrier of S, bool Union the Sorts of U0) & x is MSSubset of U0 & for
B be MSSubset of U0 st B = x holds B is opers_closed;
existence
proof
defpred P[object] means
$1 is MSSubset of U0 & for B be MSSubset of U0 st B =
$1 holds B is opers_closed;
consider X be set such that
A1: for x be object holds x in X iff x in Funcs(the carrier of S, bool
Union the Sorts of U0) & P[x] from XBOOLE_0:sch 1;
take X;
thus thesis by A1;
end;
uniqueness
proof
defpred P[object] means
$1 in Funcs(the carrier of S, bool Union the Sorts of
U0) & $1 is MSSubset of U0 & for B be MSSubset of U0 st B = $1 holds B is
opers_closed;
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;
hence thesis;
end;
end;
registration
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
cluster SubSort(U0) -> non empty;
coherence
proof
set f = Funcs(the carrier of S, bool (Union (the Sorts of U0)));
defpred P[object] means
$1 is MSSubset of U0 & for B be MSSubset of U0 st B =
$1 holds B is opers_closed;
consider X be set such that
A1: for x be object holds x in X iff x in Funcs(the carrier of S, bool (
Union (the Sorts of U0))) & P[x] from XBOOLE_0:sch 1;
(Union (the Sorts of U0)) = union rng(the Sorts of U0) by CARD_3:def 4;
then dom (the Sorts of U0) = the carrier of S & rng(the Sorts of U0) c=
bool( Union (the Sorts of U0)) by PARTFUN1:def 2,ZFMISC_1:82;
then
A2: the Sorts of U0 in f by FUNCT_2:def 2;
the Sorts of U0 is MSSubset of U0 & for B be MSSubset of U0 st B = the
Sorts of U0 holds B is opers_closed by Th3,PBOOLE:def 18;
then reconsider X as non empty set by A1,A2;
SubSort U0 = X by A1,Def11;
hence thesis;
end;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, e be
Element of SubSort(U0);
func @e -> MSSubset of U0 equals
e;
coherence by Def11;
end;
theorem Th13:
for A,B be MSSubset of U0 holds B in SubSort(A) iff B is
opers_closed & Constants(U0) c= B & A c= B
proof
let A, B be MSSubset of U0;
set C = bool (Union (the Sorts of U0));
A1: dom B = the carrier of S by PARTFUN1:def 2;
A2: dom (the Sorts of U0) = the carrier of S by PARTFUN1:def 2;
union rng B c= union(rng(the Sorts of U0))
proof
let x be object;
assume x in union rng B;
then consider Y be set such that
A3: x in Y and
A4: Y in rng B by TARSKI:def 4;
consider y be object such that
A5: y in dom B and
A6: B.y = Y by A4,FUNCT_1:def 3;
A7: (the Sorts of U0).y in rng(the Sorts of U0) by A1,A2,A5,FUNCT_1:def 3;
B c= the Sorts of U0 by PBOOLE:def 18;
then B.y c= (the Sorts of U0).y by A1,A5;
hence thesis by A3,A6,A7,TARSKI:def 4;
end;
then bool union rng B c= bool union(rng(the Sorts of U0)) by ZFMISC_1:67;
then
A8: bool union rng B c= C by CARD_3:def 4;
thus B in SubSort(A) implies B is opers_closed & Constants(U0) c= B & A c= B
by Def10;
assume B is opers_closed & Constants(U0) c= B & A c= B;
then
A9: for C be MSSubset of U0 st C = B holds C is opers_closed & Constants(U0
) c= C & A c= C;
rng B c= bool union rng B by ZFMISC_1:82;
then rng B c= C by A8;
then B in Funcs(the carrier of S, C) by A1,FUNCT_2:def 2;
hence thesis by A9,Def10;
end;
theorem Th14:
for B be MSSubset of U0 holds B in SubSort(U0) iff B is opers_closed
proof
let B be MSSubset of U0;
set C = bool (Union (the Sorts of U0));
A1: dom B = the carrier of S by PARTFUN1:def 2;
A2: dom (the Sorts of U0) = the carrier of S by PARTFUN1:def 2;
union rng B c= union(rng(the Sorts of U0))
proof
let x be object;
assume x in union rng B;
then consider Y be set such that
A3: x in Y and
A4: Y in rng B by TARSKI:def 4;
consider y be object such that
A5: y in dom B and
A6: B.y = Y by A4,FUNCT_1:def 3;
A7: (the Sorts of U0).y in rng(the Sorts of U0) by A1,A2,A5,FUNCT_1:def 3;
B c= the Sorts of U0 by PBOOLE:def 18;
then B.y c= (the Sorts of U0).y by A1,A5;
hence thesis by A3,A6,A7,TARSKI:def 4;
end;
then bool union rng B c= bool union(rng(the Sorts of U0)) by ZFMISC_1:67;
then
A8: bool union rng B c= C by CARD_3:def 4;
thus B in SubSort(U0) implies B is opers_closed by Def11;
assume B is opers_closed;
then
A9: for C be MSSubset of U0 st C = B holds C is opers_closed;
rng B c= bool union rng B by ZFMISC_1:82;
then rng B c= C by A8;
then B in Funcs(the carrier of S, C) by A1,FUNCT_2:def 2;
hence thesis by A9,Def11;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0, s be SortSymbol of S;
func SubSort(A,s) -> set means
:Def13:
for x be object holds x in it iff ex B
be MSSubset of U0 st B in SubSort(A) & x = B.s;
existence
proof
defpred P[object] means
ex B be MSSubset of U0 st B in SubSort(A) & $1 = B.s;
set C =bool Union (the Sorts of U0);
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 U0)) by CARD_3:def 4;
for x be set holds x in X iff ex B be MSSubset of U0 st B in SubSort(A
) & x = B.s
proof
dom (the Sorts of U0) = the carrier of S by PARTFUN1:def 2;
then (the Sorts of U0).s in rng (the Sorts of U0) by FUNCT_1:def 3;
then
A3: (the Sorts of U0).s c= union( rng (the Sorts of U0)) by ZFMISC_1:74;
let x be set;
thus x in X implies ex B be MSSubset of U0 st B in SubSort(A) & x = B.s
by A1;
given B be MSSubset of U0 such that
A4: B in SubSort(A) and
A5: x = B.s;
B c= the Sorts of U0 by PBOOLE:def 18;
then B.s c= (the Sorts of U0).s;
then x c= union( rng (the Sorts of U0)) by A5,A3;
hence thesis by A1,A2,A4,A5;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means
ex B be MSSubset of U0 st B in SubSort(A) & $1 = B.s;
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;
hence thesis;
end;
end;
registration
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0, s be SortSymbol of S;
cluster SubSort(A,s) -> non empty;
coherence
proof
reconsider u0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
defpred P[object] means
ex B be MSSubset of U0 st B in SubSort(A) & $1 = B.s;
set C =bool Union (the Sorts of U0);
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;
A2: C = bool union( rng(the Sorts of U0)) by CARD_3:def 4;
A3: for x be object
holds x in X iff ex B be MSSubset of U0 st B in SubSort A & x = B.s
proof
dom (the Sorts of U0) = the carrier of S by PARTFUN1:def 2;
then (the Sorts of U0).s in rng (the Sorts of U0) by FUNCT_1:def 3;
then
A4: (the Sorts of U0).s c= union( rng (the Sorts of U0)) by ZFMISC_1:74;
let x be object;
thus x in X implies ex B be MSSubset of U0 st B in SubSort(A) & x = B.s
by A1;
given B be MSSubset of U0 such that
A5: B in SubSort(A) and
A6: x = B.s;
reconsider x as set by TARSKI:1;
B c= the Sorts of U0 by PBOOLE:def 18;
then B.s c= (the Sorts of U0).s;
then x c= union( rng (the Sorts of U0)) by A6,A4;
hence thesis by A1,A2,A5,A6;
end;
A7: A c= u0 & Constants(U0)c= u0 by PBOOLE:def 18;
u0 is opers_closed by Th3;
then u0 in SubSort(A) by A7,Th13;
then (the Sorts of U0).s in X by A3;
then reconsider X as non empty set;
X = SubSort(A,s) by A3,Def13;
hence thesis;
end;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
func MSSubSort(A) -> MSSubset of U0 means
:Def14:
for s be SortSymbol of S holds it.s = meet (SubSort(A,s));
existence
proof
deffunc F(SortSymbol of S) = meet (SubSort(A,$1));
consider f be Function such that
A1: dom f = the carrier of S & for s be SortSymbol of S holds f.s = F(
s) from FUNCT_1:sch 4;
reconsider f as ManySortedSet of (the carrier of S) by A1,PARTFUN1:def 2
,RELAT_1:def 18;
f c= the Sorts of U0
proof
reconsider u0 = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
let x be object;
A2: A c= u0 & Constants(U0)c= u0 by PBOOLE:def 18;
assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
u0 is opers_closed by Th3;
then u0 in SubSort(A) by A2,Th13;
then
A3: (the Sorts of U0).s in (SubSort(A,s)) by Def13;
f.s = meet (SubSort(A,s)) by A1;
hence thesis by A3,SETFAM_1:3;
end;
then reconsider f as MSSubset of U0 by PBOOLE:def 18;
take f;
thus thesis by A1;
end;
uniqueness
proof
let W1,W2 be MSSubset of U0;
assume that
A4: for s be SortSymbol of S holds W1.s = meet (SubSort(A,s)) and
A5: for s be SortSymbol of S holds W2.s = meet (SubSort(A,s));
for s be object st s in (the carrier of S) holds W1.s = W2.s
proof
let s be object;
assume s in (the carrier of S);
then reconsider s as SortSymbol of S;
W1.s = meet (SubSort(A,s)) by A4;
hence thesis by A5;
end;
hence thesis;
end;
end;
theorem Th15:
for A be MSSubset of U0 holds Constants(U0) (\/) A c= MSSubSort(A)
proof
let A be MSSubset of U0;
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A1: for Z be set st Z in SubSort(A,s) holds (Constants(U0) (\/) A).s c= Z
proof
let Z be set;
assume Z in SubSort(A,s);
then consider B be MSSubset of U0 such that
A2: B in SubSort(A) and
A3: Z = B.s by Def13;
Constants(U0) c= B & A c= B by A2,Th13;
then Constants(U0) (\/) A c= B by PBOOLE:16;
hence thesis by A3;
end;
(MSSubSort(A)).s = meet (SubSort(A,s)) by Def14;
hence thesis by A1,SETFAM_1:5;
end;
theorem Th16:
for A be MSSubset of U0 st Constants(U0) (\/) A is non-empty holds
MSSubSort(A) is non-empty
proof
let A be MSSubset of U0;
assume
A1: Constants(U0) (\/) A is non-empty;
now
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
for Z be set st Z in SubSort(A,s) holds (Constants(U0) (\/) A).s c= Z
proof
let Z be set;
assume Z in SubSort(A,s);
then consider B be MSSubset of U0 such that
A2: B in SubSort(A) and
A3: Z = B.s by Def13;
Constants(U0) c= B & A c= B by A2,Th13;
then Constants(U0) (\/) A c= B by PBOOLE:16;
hence thesis by A3;
end;
then
A4: (Constants(U0) (\/) A).s c= meet(SubSort(A,s)) by SETFAM_1:5;
ex x be object st x in (Constants(U0) (\/) A).s by A1,XBOOLE_0:def 1;
hence (MSSubSort(A)).i is non empty by A4,Def14;
end;
hence thesis;
end;
theorem Th17:
for A be MSSubset of U0 for B be MSSubset of U0 st B in SubSort(
A) holds ((MSSubSort A)# * (the Arity of S)).o c= (B# * (the Arity of S)).o
proof
let A be MSSubset of U0, B be MSSubset of U0;
assume
A1: B in SubSort(A);
MSSubSort (A) c= B
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
(MSSubSort A).s = meet (SubSort(A,s)) & B.s in (SubSort(A,s)) by A1,Def13
,Def14;
hence thesis by SETFAM_1:3;
end;
hence thesis by Th2;
end;
theorem Th18:
for A be MSSubset of U0 for B be MSSubset of U0 st B in SubSort(
A) holds rng (Den(o,U0)|(((MSSubSort A)# * (the Arity of S)).o)) c= (B * (the
ResultSort of S)).o
proof
let A be MSSubset of U0, B be MSSubset of U0;
set m = ((MSSubSort A)# * (the Arity of S)).o, b = (B# * (the Arity of S)).o
, d = Den(o,U0);
assume
A1: B in SubSort(A);
then b /\ m = m by Th17,XBOOLE_1:28;
then d|m = (d|b)|m by RELAT_1:71;
then
A2: rng (d|m) c= rng(d|b) by RELAT_1:70;
B is opers_closed by A1,Th13;
then B is_closed_on o;
then rng (d|b) c= (B * (the ResultSort of S)).o;
hence thesis by A2;
end;
theorem Th19:
for A be MSSubset of U0 holds rng ((Den(o,U0))|(((MSSubSort A)#
* (the Arity of S)).o)) c= ((MSSubSort A) * (the ResultSort of S)).o
proof
let A be MSSubset of U0;
let x be object;
assume that
A1: x in rng ((Den(o,U0))|(((MSSubSort A)# * (the Arity of S)).o)) and
A2: not x in ((MSSubSort A) * (the ResultSort of S)).o;
set r = the_result_sort_of o;
A3: r = (the ResultSort of S).o & dom (the ResultSort of S) = the carrier'
of S by FUNCT_2:def 1,MSUALG_1:def 2;
then ((MSSubSort A) * (the ResultSort of S)).o = (MSSubSort A).r by
FUNCT_1:13
.= meet SubSort(A,r) by Def14;
then consider X be set such that
A4: X in SubSort(A,r) and
A5: not x in X by A2,SETFAM_1:def 1;
consider B be MSSubset of U0 such that
A6: B in SubSort(A) and
A7: B.r = X by A4,Def13;
rng (Den(o,U0)|(((MSSubSort A)# * (the Arity of S)).o)) c= (B * (the
ResultSort of S)).o by A6,Th18;
then x in (B * (the ResultSort of S)).o by A1;
hence contradiction by A3,A5,A7,FUNCT_1:13;
end;
theorem Th20:
for A be MSSubset of U0 holds MSSubSort(A) is opers_closed & A
c= MSSubSort(A)
proof
let A be MSSubset of U0;
thus MSSubSort(A) is opers_closed
proof
let o be OperSymbol of S;
rng ((Den(o,U0))|(((MSSubSort A)# * (the Arity of S)).o)) c= ((
MSSubSort A) * (the ResultSort of S)).o by Th19;
hence thesis;
end;
A c= Constants(U0) (\/) A & Constants(U0) (\/) A c= MSSubSort(A) by Th15,
PBOOLE:14;
hence thesis by PBOOLE:13;
end;
begin
::
:: Operations on Subalgebras of a Many Sorted Algebra.
::
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
assume
A1: A is opers_closed;
func U0|A -> strict MSSubAlgebra of U0 equals
:Def15:
MSAlgebra (#A, Opers(
U0,A) qua ManySortedFunction of (A# * the Arity of S),(A * the ResultSort of S)
#);
coherence
proof
reconsider E = MSAlgebra (#A, Opers(U0,A) qua ManySortedFunction of (A# *
the Arity of S),(A * the ResultSort of S)#) as MSAlgebra over S;
for B be MSSubset of U0 st B = the Sorts of E holds B is opers_closed
& the Charact of E = Opers(U0,B) by A1;
hence thesis by Def9;
end;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, U1,U2 be
MSSubAlgebra of U0;
func U1 /\ U2 -> strict MSSubAlgebra of U0 means
:Def16:
the Sorts of it = (the Sorts of U1) (/\) (the Sorts of U2) &
for B be MSSubset of U0 st B=the Sorts of it
holds B is opers_closed & the Charact of it = Opers(U0,B);
existence
proof
the Sorts of U2 is MSSubset of U0 by Def9;
then
A1: the Sorts of U2 c=the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by Def9;
then 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) (/\) (the Sorts of U0) by A1,PBOOLE:21;
then reconsider
A = (the Sorts of U1) (/\) (the Sorts of U2) as MSSubset of U0 by
PBOOLE:def 18;
reconsider E = U0|A as strict MSSubAlgebra of U0;
take E;
A is opers_closed
proof
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0
by Def9;
let o be OperSymbol of S;
A2: dom (u1 # * the Arity of S) = the carrier' of S by PARTFUN1:def 2;
A3: dom (u2 # * the Arity of S) = the carrier' of S by PARTFUN1:def 2;
u2 is opers_closed by Def9;
then u2 is_closed_on o;
then
A4: rng ((Den(o,U0))|((u2# * the Arity of S).o))c= (u2*the ResultSort
of S). o;
dom (A# * the Arity of S) = the carrier' of S by PARTFUN1:def 2;
then
A5: (A# * the Arity of S).o = (A# qua ManySortedSet of (the carrier of
S)*).((the Arity of S).o) by FUNCT_1:12
.= (A# qua ManySortedSet of (the carrier of S)*).(the_arity_of o) by
MSUALG_1:def 1
.= product ((u1 (/\) u2) * (the_arity_of o)) by FINSEQ_2:def 5
.= product(u1 *(the_arity_of o)) /\ product(u2 *(the_arity_of o)) by
Th1
.= (u1 # qua ManySortedSet of (the carrier of S)*).(the_arity_of o)
/\ product(u2 *(the_arity_of o)) by FINSEQ_2:def 5
.= (u1 # qua ManySortedSet of (the carrier of S)*).(the_arity_of o)
/\ (u2 # qua ManySortedSet of (the carrier of S)*).(the_arity_of o) by
FINSEQ_2:def 5
.= (u1 # qua ManySortedSet of (the carrier of S)*).((the Arity of S)
.o) /\ (u2 # qua ManySortedSet of (the carrier of S)*).(the_arity_of o) by
MSUALG_1:def 1
.= (u1 # qua ManySortedSet of (the carrier of S)*).((the Arity of S)
.o) /\ (u2 # qua ManySortedSet of (the carrier of S)*).((the Arity of S).o) by
MSUALG_1:def 1
.= (u1# *(the Arity of S)).o /\ (u2 # qua ManySortedSet of (the
carrier of S)*).((the Arity of S).o) by A2,FUNCT_1:12
.= (u1# *(the Arity of S)).o /\ (u2# *(the Arity of S)).o by A3,
FUNCT_1:12;
then Den(o,U0)|((A# * the Arity of S).o) = ((Den(o,U0))| ((u2# *(the
Arity of S)).o))|((u1# *(the Arity of S)).o) by RELAT_1:71;
then rng ((Den(o,U0))|((A# *(the Arity of S)).o)) c= rng (Den(o,U0)| ((
u2# *(the Arity of S)).o)) by RELAT_1:70;
then
A6: rng ((Den(o,U0))|((A# *(the Arity of S)).o)) c= (u2*the ResultSort
of S).o by A4;
u1 is opers_closed by Def9;
then u1 is_closed_on o;
then
A7: rng((Den(o,U0))|((u1#*the Arity of S).o))c=(u1*the ResultSort of S)
.o;
A8: dom (u2 * the ResultSort of S)=the carrier' of S by PARTFUN1:def 2;
Den(o,U0)|((A# * the Arity of S).o) = ( (Den(o,U0)) | ((u1# *(the
Arity of S)) .o)) | ( (u2# *(the Arity of S)) . o) by A5,RELAT_1:71;
then rng ( (Den(o,U0)) | ((A# *(the Arity of S)).o)) c= rng (Den(o,U0)|
((u1# *(the Arity of S)).o)) by RELAT_1:70;
then rng ((Den(o,U0))|((A# *(the Arity of S)).o)) c= (u1*the ResultSort
of S).o by A7;
then
A9: rng ((Den(o,U0))|((A# *(the Arity of S)).o)) c= ((u1*the ResultSort
of S).o)/\((u2*the ResultSort of S).o) by A6,XBOOLE_1:19;
A10: dom (A * the ResultSort of S) = the carrier' of S by PARTFUN1:def 2;
dom (u1 * the ResultSort of S) = the carrier' of S by PARTFUN1:def 2;
then ((u1*the ResultSort of S).o)/\((u2*the ResultSort of S).o) = u1.((
the ResultSort of S).o)/\ ((u2*the ResultSort of S).o) by FUNCT_1:12
.= u1.((the ResultSort of S).o)/\ u2.((the ResultSort of S).o) by A8,
FUNCT_1:12
.= u1.(the_result_sort_of o) /\ u2.((the ResultSort of S).o) by
MSUALG_1:def 2
.= u1.(the_result_sort_of o) /\ u2.(the_result_sort_of o) by
MSUALG_1:def 2
.= A.(the_result_sort_of o) by PBOOLE:def 5
.= A.((the ResultSort of S).o) by MSUALG_1:def 2
.= (A*the ResultSort of S).o by A10,FUNCT_1:12;
hence thesis by A9;
end;
then U0|A=MSAlgebra (#A, Opers(U0,A) qua ManySortedFunction of (A# * the
Arity of S),(A * the ResultSort of S)#) by Def15;
hence the Sorts of E = (the Sorts of U1) (/\) (the Sorts of U2);
thus thesis by Def9;
end;
uniqueness by Th9;
end;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
func GenMSAlg(A) -> strict MSSubAlgebra of U0 means
:Def17:
A is MSSubset of
it & for U1 be MSSubAlgebra of U0 st A is MSSubset of U1 holds it is
MSSubAlgebra of U1;
existence
proof
set a = MSSubSort(A);
reconsider u1 = U0|a as strict MSSubAlgebra of U0;
take u1;
A1: u1 = MSAlgebra (# a, Opers(U0,a)qua ManySortedFunction of (a# * the
Arity of S),(a * the ResultSort of S)#) by Def15,Th20;
A c= a by Th20;
hence A is MSSubset of u1 by A1,PBOOLE:def 18;
let U2 be MSSubAlgebra of U0;
reconsider B = the Sorts of U2 as MSSubset of U0 by Def9;
assume A is MSSubset of U2;
then
A2: A c= B by PBOOLE:def 18;
Constants(U0) is MSSubset of U2 by Th10;
then
A3: Constants(U0) c= B by PBOOLE:def 18;
B is opers_closed by Def9;
then
A4: B in SubSort(A) by A2,A3,Th13;
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,A4
,Def13,Def14;
hence thesis by SETFAM_1:3;
end;
hence thesis by Th8;
end;
uniqueness
proof
let W1,W2 be strict MSSubAlgebra of U0;
assume A is MSSubset of W1 & ( for U1 be MSSubAlgebra of U0 st A is
MSSubset of U1 holds W1 is MSSubAlgebra of U1)& A is MSSubset of W2 & for U2 be
MSSubAlgebra of U0 st A is MSSubset of U2 holds W2 is MSSubAlgebra of U2;
then W1 is strict MSSubAlgebra of W2 & W2 is strict MSSubAlgebra of W1;
hence thesis by Th7;
end;
end;
registration
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, A be non-empty MSSubset of U0;
cluster GenMSAlg(A) -> non-empty;
coherence
proof
Constants(U0) (\/) A is non-empty;
then reconsider a = MSSubSort(A) as non-empty MSSubset of U0 by Th16;
U0|a = MSAlgebra (#a, Opers(U0,a) qua ManySortedFunction of (a# * the
Arity of S),(a * the ResultSort of S)#) by Def15,Th20;
then reconsider u1 = U0|a as strict non-empty MSSubAlgebra of U0 by
MSUALG_1:def 3;
A1: A c= a by Th20;
now
A2: u1 = MSAlgebra (# a, Opers(U0,a)qua ManySortedFunction of (a# * the
Arity of S),(a * the ResultSort of S)#) by Def15,Th20;
hence A is MSSubset of u1 by A1,PBOOLE:def 18;
let U2 be MSSubAlgebra of U0;
reconsider B = the Sorts of U2 as MSSubset of U0 by Def9;
assume A is MSSubset of U2;
then
A3: A c= B by PBOOLE:def 18;
Constants(U0) is MSSubset of U2 by Th10;
then
A4: Constants(U0) c= B by PBOOLE:def 18;
B is opers_closed by Def9;
then
A5: B in SubSort(A) by A3,A4,Th13;
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 A2,A5
,Def13,Def14;
hence thesis by SETFAM_1:3;
end;
hence u1 is MSSubAlgebra of U2 by Th8;
end;
hence thesis by Def17;
end;
end;
theorem Th21:
for S be non void non empty ManySortedSign, U0 be
MSAlgebra over S, B be MSSubset of U0 st B = the Sorts of U0 holds GenMSAlg(B)
= the MSAlgebra of U0
proof
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, B
be MSSubset of U0;
set W = GenMSAlg(B);
reconsider B1 = the Sorts of W as MSSubset of U0 by Def9;
A1: the Charact of W = Opers(U0,B1) by Def9;
assume B = the Sorts of U0;
then the Sorts of U0 is MSSubset of W by Def17;
then
A2: the Sorts of U0 c= the Sorts of W by PBOOLE:def 18;
(the Sorts of W) is MSSubset of U0 by Def9;
then the Sorts of W c= the Sorts of U0 by PBOOLE:def 18;
then the Sorts of U0 = the Sorts of W by A2,PBOOLE:146;
hence thesis by A1,Th4;
end;
theorem Th22:
for S be non void non empty ManySortedSign, U0 be MSAlgebra over
S, U1 be MSSubAlgebra of U0, B be MSSubset of U0 st B = the Sorts of U1
holds GenMSAlg(B) = the MSAlgebra of U1
proof
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, U1 be
MSSubAlgebra of U0, B be MSSubset of U0;
assume
A1: B = the Sorts of U1;
set W = GenMSAlg(B);
B is MSSubset of W by Def17;
then the Sorts of U1 c= the Sorts of W by A1,PBOOLE:def 18;
then
A2: U1 is MSSubAlgebra of W by Th8;
B is MSSubset of U1 by A1,PBOOLE:def 18;
then W is MSSubAlgebra of U1 by Def17;
hence thesis by A2,Th7;
end;
theorem Th23:
for S be non void non empty ManySortedSign, U0 be non-empty
MSAlgebra over S, U1 be MSSubAlgebra of U0 holds GenMSAlg(Constants(U0)) /\ U1
= GenMSAlg(Constants(U0))
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, U1 be MSSubAlgebra of U0;
set C = Constants(U0), G = GenMSAlg(C);
C is MSSubset of U1 by Th10;
then G is strict MSSubAlgebra of U1 by Def17;
then the Sorts of G is MSSubset of U1 by Def9;
then
A1: the Sorts of G c= the Sorts of U1 by PBOOLE:def 18;
the Sorts of (G /\ U1) = (the Sorts of G) (/\) (the Sorts of U1) by Def16;
then the Sorts of (G /\ U1) = the Sorts of G by A1,PBOOLE:23;
hence thesis by Th9;
end;
definition
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, U1,U2 be MSSubAlgebra of U0;
func U1 "\/" U2 -> strict MSSubAlgebra of U0 means
:Def18:
for A be MSSubset of U0 st A = (the Sorts of U1) (\/) (the Sorts of U2)
holds it = GenMSAlg(A);
existence
proof
set B=(the Sorts of U1) (\/) (the Sorts of U2);
the Sorts of U2 is MSSubset of U0 by Def9;
then
A1: the Sorts of U2 c=the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by Def9;
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;
take GenMSAlg(B);
thus thesis;
end;
uniqueness
proof
set B=(the Sorts of U1) (\/) (the Sorts of U2);
the Sorts of U2 is MSSubset of U0 by Def9;
then
A2: the Sorts of U2 c=the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by Def9;
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 MSSubAlgebra of U0;
assume that
A3: for A be MSSubset of U0 st A = (the Sorts of U1) (\/) (the Sorts of
U2) holds W1 = GenMSAlg(A) and
A4: for A be MSSubset of U0 st A = (the Sorts of U1) (\/) (the Sorts of
U2) holds W2 = GenMSAlg(A);
W1 = GenMSAlg(B) by A3;
hence thesis by A4;
end;
end;
theorem Th24:
for S be non void non empty ManySortedSign,U0 be non-empty
MSAlgebra over S, U1 be MSSubAlgebra of U0, A,B be MSSubset of U0
st B = A (\/) the Sorts of U1 holds GenMSAlg(A) "\/" U1 = GenMSAlg(B)
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, U1 be MSSubAlgebra of U0, A,B be MSSubset of U0;
reconsider u1 = the Sorts of U1, a = the Sorts of GenMSAlg(A) as MSSubset of
U0 by Def9;
A1: (the Sorts of GenMSAlg(A)) (/\) (the Sorts of GenMSAlg(B)) c= a
by PBOOLE:15;
A2: the Sorts of (GenMSAlg(A) /\ GenMSAlg(B))
= (the Sorts of GenMSAlg(A)) (/\) (the Sorts of GenMSAlg(B)) by Def16;
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: (GenMSAlg(A) "\/" U1) = GenMSAlg(b) by Def18;
then a (\/) u1 is MSSubset of (GenMSAlg(A)"\/"U1) by Def17;
then
A4: a (\/) u1 c=the Sorts of (GenMSAlg(A)"\/"U1) by PBOOLE:def 18;
A is MSSubset of GenMSAlg(A) by Def17;
then
A5: A c= the Sorts of GenMSAlg(A) by PBOOLE:def 18;
B is MSSubset of GenMSAlg(B) by Def17;
then
A6: B c= the Sorts of GenMSAlg(B) by PBOOLE:def 18;
assume
A7: B = A (\/) the Sorts of U1;
then A c= B by PBOOLE:14;
then A c= the Sorts of GenMSAlg(B) by A6,PBOOLE:13;
then A c= (the Sorts of GenMSAlg(A)) (/\) (the Sorts of GenMSAlg(B))
by A5,PBOOLE:17;
then A is MSSubset of (GenMSAlg(A) /\ GenMSAlg(B)) by A2,PBOOLE:def 18;
then GenMSAlg(A) is MSSubAlgebra of (GenMSAlg(A) /\ GenMSAlg(B)) by Def17;
then a is MSSubset of (GenMSAlg(A) /\ GenMSAlg(B)) by Def9;
then a c= (the Sorts of GenMSAlg(A)) (/\) (the Sorts of GenMSAlg(B))
by A2,PBOOLE:def 18;
then a= (the Sorts of GenMSAlg(A)) (/\) (the Sorts of GenMSAlg(B))
by A1,PBOOLE:146;
then
A8: a c= the Sorts of GenMSAlg(B) by PBOOLE:15;
u1 c= B by A7,PBOOLE:14;
then u1 c= the Sorts of GenMSAlg(B) by A6,PBOOLE:13;
then b c= the Sorts of GenMSAlg(B) by A8,PBOOLE:16;
then b is MSSubset of GenMSAlg(B) by PBOOLE:def 18;
then
A9: GenMSAlg(b) is strict MSSubAlgebra of GenMSAlg(B) by Def17;
A (\/) u1 c= a (\/) u1 by A5,PBOOLE:20;
then B c=the Sorts of (GenMSAlg(A)"\/"U1) by A7,A4,PBOOLE:13;
then B is MSSubset of (GenMSAlg(A)"\/"U1) by PBOOLE:def 18;
then GenMSAlg(B) is strict MSSubAlgebra of (GenMSAlg(A)"\/"U1) by Def17;
hence thesis by A3,A9,Th7;
end;
theorem Th25:
for S be non void non empty ManySortedSign, U0 be non-empty
MSAlgebra over S, U1 be MSSubAlgebra of U0, B be MSSubset of U0 st B = the
Sorts of U0 holds GenMSAlg(B) "\/" U1 = GenMSAlg(B)
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, U1 be MSSubAlgebra of U0, B be MSSubset of U0;
assume
A1: B = the Sorts of U0;
the Sorts of U1 is MSSubset of U0 by Def9;
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 Th24;
end;
theorem Th26:
for S be non void non empty ManySortedSign,U0 be non-empty
MSAlgebra over S, U1,U2 be MSSubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, U1,U2 be MSSubAlgebra of U0;
reconsider u1= the Sorts of U1, u2= the Sorts of U2 as MSSubset of U0 by Def9
;
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 "\/" U2 = GenMSAlg(A) by Def18;
hence thesis by Def18;
end;
theorem Th27:
for S be non void non empty ManySortedSign, U0 be non-empty
MSAlgebra over S, U1,U2 be MSSubAlgebra of U0 holds U1 /\ (U1"\/"U2) =
the MSAlgebra of U1
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, U1,U2 be MSSubAlgebra of U0;
reconsider u1= the Sorts of U1,u2 =the Sorts of U2 as MSSubset of U0 by Def9;
A1: the Sorts of (U1 /\(U1"\/"U2))
=(the Sorts of U1) (/\) (the Sorts of(U1"\/"U2)) by Def16;
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"\/"U2 = GenMSAlg(A) by Def18;
then A is MSSubset of U1"\/"U2 by Def17;
then
A2: A c= the Sorts of (U1 "\/" U2) by PBOOLE:def 18;
the Sorts of U1 c= A by PBOOLE:14;
then the Sorts of U1 c= the Sorts of (U1"\/"U2) by A2,PBOOLE:13;
then
A3: the Sorts of U1 c=the Sorts of (U1 /\(U1"\/"U2)) by A1,PBOOLE:17;
reconsider u112=the Sorts of(U1 /\ (U1"\/"U2)) as MSSubset of U0 by Def9;
A4: the Charact of (U1/\(U1"\/" U2))=Opers(U0,u112) by Def16;
the Sorts of (U1 /\(U1"\/"U2)) c= the Sorts of U1 by A1,PBOOLE:15;
then the Sorts of (U1 /\(U1"\/"U2)) = the Sorts of U1 by A3,PBOOLE:146;
hence thesis by A4,Def9;
end;
theorem Th28:
for S be non void non empty ManySortedSign, U0 be non-empty
MSAlgebra over S, U1,U2 be MSSubAlgebra of U0 holds (U1 /\ U2)"\/"U2 =
the MSAlgebra of U2
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, U1,U2 be MSSubAlgebra of U0;
reconsider u12= the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of
U0 by Def9;
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;
u12 = (the Sorts of U1) (/\) (the Sorts of U2) by Def16;
then u12 c= u2 by PBOOLE:15;
then
A1: A = u2 by PBOOLE:22;
(U1 /\ U2)"\/"U2=GenMSAlg(A) by Def18;
hence thesis by A1,Th22;
end;
begin
::
:: The Lattice of SubAlgebras of a Many Sorted Algebra.
::
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
func MSSub(U0) -> set means
:Def19:
for x being object holds x in it iff x is strict MSSubAlgebra of U0;
existence
proof
reconsider X = the set of all
GenMSAlg(@A) where A is Element of SubSort(U0) as set;
take X;
let x be object;
thus x in X implies x is strict MSSubAlgebra of U0
proof
assume x in X;
then ex A be Element of SubSort(U0) st x = GenMSAlg(@A);
hence thesis;
end;
assume x is strict MSSubAlgebra of U0;
then reconsider a = x as strict MSSubAlgebra of U0;
reconsider A = the Sorts of a as MSSubset of U0 by Def9;
A is opers_closed by Def9;
then reconsider h = A as Element of SubSort(U0) by Th14;
a = GenMSAlg(@h) by Th22;
hence thesis;
end;
uniqueness
proof
defpred P[object] means $1 is strict MSSubAlgebra of U0;
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;
hence thesis;
end;
end;
registration
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
cluster MSSub(U0) -> non empty;
coherence
proof
set x = the strict MSSubAlgebra of U0;
x in MSSub U0 by Def19;
hence thesis;
end;
end;
definition
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
func MSAlg_join(U0) -> BinOp of (MSSub(U0)) means
:Def20:
for x,y be Element
of MSSub(U0) holds for U1,U2 be strict MSSubAlgebra of U0 st x = U1 & y = U2
holds it.(x,y) = U1 "\/" U2;
existence
proof
defpred P[(Element of MSSub(U0)),(Element of MSSub(U0)), Element of MSSub(
U0)] means for U1,U2 be strict MSSubAlgebra of U0 st $1=U1 & $2=U2 holds $3=U1
"\/" U2;
A1: for x,y being Element of MSSub(U0) ex z being Element of MSSub(U0) st
P[x,y,z]
proof
let x,y be Element of MSSub(U0);
reconsider U1=x, U2=y as strict MSSubAlgebra of U0 by Def19;
reconsider z =U1"\/"U2 as Element of MSSub(U0) by Def19;
take z;
thus thesis;
end;
consider o be BinOp of MSSub(U0) such that
A2: for a,b be Element of MSSub(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 (MSSub(U0));
assume that
A3: for x,y be Element of MSSub(U0) holds for U1,U2 be strict
MSSubAlgebra of U0 st x=U1 & y=U2 holds o1.(x,y)=U1 "\/" U2 and
A4: for x,y be Element of MSSub(U0) holds for U1,U2 be strict
MSSubAlgebra of U0 st x=U1 & y=U2 holds o2.(x,y) = U1 "\/" U2;
for x be Element of MSSub(U0) for y be Element of MSSub(U0) holds o1.(
x,y) = o2.(x,y)
proof
let x,y be Element of MSSub(U0);
reconsider U1=x,U2=y as strict MSSubAlgebra of U0 by Def19;
o1.(x,y) = U1"\/" U2 by A3;
hence thesis by A4;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
func MSAlg_meet(U0) -> BinOp of (MSSub(U0)) means
:Def21:
for x,y be Element
of MSSub(U0) holds for U1,U2 be strict MSSubAlgebra of U0 st x = U1 & y = U2
holds it.(x,y) = U1 /\ U2;
existence
proof
defpred P[(Element of MSSub(U0)),(Element of MSSub(U0)), Element of MSSub(
U0)] means for U1,U2 be strict MSSubAlgebra of U0 st $1=U1 & $2=U2 holds $3=U1
/\ U2;
A1: for x,y being Element of MSSub(U0) ex z being Element of MSSub(U0) st
P[x,y,z]
proof
let x,y be Element of MSSub(U0);
reconsider U1=x, U2=y as strict MSSubAlgebra of U0 by Def19;
reconsider z =U1 /\ U2 as Element of MSSub(U0) by Def19;
take z;
thus thesis;
end;
consider o be BinOp of MSSub(U0) such that
A2: for a,b be Element of MSSub(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 MSSub(U0);
assume that
A3: for x,y be Element of MSSub(U0) holds for U1,U2 be strict
MSSubAlgebra of U0 st x=U1 & y=U2 holds o1.(x,y)=U1 /\ U2 and
A4: for x,y be Element of MSSub(U0) holds for U1,U2 be strict
MSSubAlgebra of U0 st x=U1 & y=U2 holds o2.(x,y) = U1 /\ U2;
for x be Element of MSSub(U0) for y be Element of MSSub(U0) holds o1.(
x,y) = o2.(x,y)
proof
let x,y be Element of MSSub(U0);
reconsider U1=x,U2=y as strict MSSubAlgebra of U0 by Def19;
o1.(x,y) = U1 /\ U2 by A3;
hence thesis by A4;
end;
hence thesis by BINOP_1:2;
end;
end;
reserve U0 for non-empty MSAlgebra over S;
theorem Th29:
MSAlg_join(U0) is commutative
proof
set o = MSAlg_join(U0);
for x,y be Element of MSSub(U0) holds o.(x,y)=o.(y,x)
proof
let x,y be Element of MSSub(U0);
reconsider U1=x,U2=y as strict MSSubAlgebra of U0 by Def19;
set B=(the Sorts of U1) (\/) (the Sorts of U2);
the Sorts of U2 is MSSubset of U0 by Def9;
then
A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by Def9;
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;
A2: U1"\/" U2 = GenMSAlg(B) by Def18;
o.(x,y) = U1 "\/" U2 & o.(y,x) = U2 "\/" U1 by Def20;
hence thesis by A2,Def18;
end;
hence thesis by BINOP_1:def 2;
end;
theorem Th30:
MSAlg_join(U0) is associative
proof
set o = MSAlg_join(U0);
for x,y,z be Element of MSSub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
proof
let x,y,z be Element of MSSub(U0);
reconsider U1=x,U2=y,U3=z as strict MSSubAlgebra of U0 by Def19;
set B=(the Sorts of U1) (\/) ((the Sorts of U2) (\/) (the Sorts of U3));
A1: o.(x,y)=U1"\/"U2 by Def20;
the Sorts of U2 is MSSubset of U0 by Def9;
then
A2: the Sorts of U2 c=the Sorts of U0 by PBOOLE:def 18;
the Sorts of U3 is MSSubset of U0 by Def9;
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
C =(the Sorts of U2) (\/) (the Sorts of U3) as MSSubset of U0 by
PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by Def9;
then
A4: the Sorts of U1 c=the Sorts of U0 by PBOOLE:def 18;
then
A5: B c= the Sorts of U0 by A3,PBOOLE:16;
(the Sorts of U1) (\/) (the Sorts of U2) c= the Sorts of U0 by A4,A2,
PBOOLE:16;
then reconsider D = (the Sorts of U1) (\/) (the Sorts of U2)
as MSSubset of U0 by PBOOLE:def 18;
reconsider B as MSSubset of U0 by A5,PBOOLE:def 18;
A6: B= D (\/) (the Sorts of U3) by PBOOLE:28;
A7: (U1"\/"U2)"\/"U3 = GenMSAlg(D)"\/" U3 by Def18
.= GenMSAlg(B) by A6,Th24;
o.(y,z)=U2"\/"U3 by Def20;
then
A8: o.(x,o.(y,z)) = U1 "\/" (U2"\/"U3) by Def20;
U1"\/" (U2"\/"U3) = U1 "\/"(GenMSAlg(C)) by Def18
.=(GenMSAlg(C)) "\/" U1 by Th26
.= GenMSAlg(B) by Th24;
hence thesis by A1,A8,A7,Def20;
end;
hence thesis by BINOP_1:def 3;
end;
theorem Th31:
for S be non void non empty ManySortedSign, U0 be non-empty
MSAlgebra over S holds MSAlg_meet(U0) is commutative
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
set o = MSAlg_meet(U0);
for x,y be Element of MSSub(U0) holds o.(x,y)=o.(y,x)
proof
let x,y be Element of MSSub(U0);
reconsider U1=x,U2=y as strict MSSubAlgebra of U0 by Def19;
A1: the Sorts of(U2 /\ U1) = (the Sorts of U2) (/\) (the Sorts of U1) &
for B2 be MSSubset of U0 st B2=the Sorts of (U2/\U1)
holds B2 is opers_closed & the Charact of (U2/\U1) = Opers(U0,B2) by Def16;
o.(x,y) = U1 /\ U2 & o.(y,x) = U2 /\ U1 by Def21;
hence thesis by A1,Def16;
end;
hence thesis by BINOP_1:def 2;
end;
theorem Th32:
for S be non void non empty ManySortedSign, U0 be non-empty
MSAlgebra over S holds MSAlg_meet(U0) is associative
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
set o = MSAlg_meet(U0);
for x,y,z be Element of MSSub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
proof
let x,y,z be Element of MSSub(U0);
reconsider U1=x,U2=y,U3=z as strict MSSubAlgebra of U0 by Def19;
reconsider u23 = U2 /\ U3,u12 =U1 /\ U2 as Element of MSSub(U0) by Def19;
A1: the Sorts of (U1/\U2)=(the Sorts of U1) (/\) (the Sorts of U2) & for B
be MSSubset of U0 st B=the Sorts of (U1/\(U2/\U3)) holds B is opers_closed &
the Charact of (U1/\(U2/\U3)) = Opers(U0,B) by Def16;
A2: o.(o.(x,y),z) = o.(u12,z) by Def21
.=(U1 /\ U2) /\ U3 by Def21;
the Sorts of(U2 /\ U3) = (the Sorts of U2) (/\) (the Sorts of U3) by Def16;
then
A3: the Sorts of (U1 /\ (U2 /\ U3)) =(the Sorts of U1) (/\) ((the Sorts of
U2) (/\)(the Sorts of U3)) by Def16;
then reconsider
C = (the Sorts of U1) (/\) ((the Sorts of U2)(/\)(the Sorts of U3))
as MSSubset of U0 by Def9;
A4: o.(x,o.(y,z)) =o.(x,u23) by Def21
.= U1/\(U2 /\ U3) by Def21;
C =((the Sorts of U1)(/\)(the Sorts of U2)) (/\) (the Sorts of U3)
by PBOOLE:29;
hence thesis by A4,A2,A3,A1,Def16;
end;
hence thesis by BINOP_1:def 3;
end;
definition
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
func MSSubAlLattice(U0) -> strict Lattice equals
LattStr (# MSSub(U0),
MSAlg_join(U0), MSAlg_meet(U0) #);
coherence
proof
set L = LattStr (# MSSub(U0), MSAlg_join(U0), MSAlg_meet(U0) #);
A1: for a,b,c being Element of L holds a"\/"(b"\/"c) = (a"\/"b)"\/"c
by Th30,BINOP_1:def 3;
A2: for a,b being Element of L holds a"/\"b = b"/\"a
by Th31,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 MSSub(U0);
(MSAlg_meet(U0)).(x,(MSAlg_join(U0)).(x,y))= x
proof
reconsider U1= x,U2=y as strict MSSubAlgebra of U0 by Def19;
(MSAlg_join(U0)).(x,y) = U1"\/"U2 by Def20;
hence (MSAlg_meet(U0)).(x,(MSAlg_join(U0)).(x,y)) = (U1 /\( U1"\/"U2))
by Def21
.=x by Th27;
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 MSSub(U0);
(MSAlg_join(U0)).((MSAlg_meet(U0)).(x,y),y)= y
proof
reconsider U1= x,U2=y as strict MSSubAlgebra of U0 by Def19;
(MSAlg_meet(U0)).(x,y) = U1 /\ U2 by Def21;
hence (MSAlg_join(U0)).((MSAlg_meet(U0)).(x,y),y) = ((U1 /\ U2)"\/"U2)
by Def20
.=y by Th28;
end;
hence thesis;
end;
A5: for a,b,c being Element of L holds a"/\"(b"/\"c) = (a"/\"b)"/\"c
by Th32,BINOP_1:def 3;
for a,b being Element of L holds a"\/"b = b"\/"a
by Th29,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 Th33:
for S be non void non empty ManySortedSign, U0 be non-empty
MSAlgebra over S holds MSSubAlLattice(U0) is bounded
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
set L = MSSubAlLattice(U0);
thus L is lower-bounded
proof
set C = Constants(U0);
reconsider G = GenMSAlg(C) as Element of MSSub(U0) by Def19;
reconsider G1 = G as Element of L;
take G1;
let a be Element of L;
reconsider a1 = a as Element of MSSub(U0);
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1 "/\" a = GenMSAlg(C) /\ a2 by Def21
.= G1 by Th23;
hence thesis;
end;
thus L is upper-bounded
proof
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
reconsider G = GenMSAlg(B) as Element of MSSub(U0) by Def19;
reconsider G1 = G as Element of L;
take G1;
let a be Element of L;
reconsider a1 = a as Element of MSSub(U0);
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1"\/"a = GenMSAlg(B)"\/"a2 by Def20
.= G1 by Th25;
hence thesis;
end;
end;
registration
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
cluster MSSubAlLattice(U0) -> bounded;
coherence by Th33;
end;
theorem
for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra
over S holds Bottom (MSSubAlLattice(U0)) = GenMSAlg(Constants(U0))
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S;
set C = Constants(U0);
reconsider G = GenMSAlg(C) as Element of MSSub(U0) by Def19;
set L = MSSubAlLattice(U0);
reconsider G1 = G as Element of L;
now
let a be Element of L;
reconsider a1 = a as Element of MSSub(U0);
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1 "/\" a = GenMSAlg(C) /\ a2 by Def21
.= G1 by Th23;
hence a "/\" G1 = G1;
end;
hence thesis by LATTICES:def 16;
end;
theorem Th35:
for S be non void non empty ManySortedSign, U0 be non-empty
MSAlgebra over S, B be MSSubset of U0 st B = the Sorts of U0 holds Top (
MSSubAlLattice(U0)) = GenMSAlg(B)
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, B be MSSubset of U0;
reconsider G = GenMSAlg(B) as Element of MSSub(U0) by Def19;
set L = MSSubAlLattice(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 MSSub(U0);
reconsider a2 = a1 as strict MSSubAlgebra of U0 by Def19;
thus G1"\/"a = GenMSAlg(B)"\/"a2 by Def20
.= G1 by A1,Th25;
hence a "\/" G1 = G1;
end;
hence thesis by LATTICES:def 17;
end;
theorem
for S be non void non empty ManySortedSign, U0 be non-empty
MSAlgebra over S holds Top (MSSubAlLattice(U0)) = the MSAlgebra of U0
proof
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra
over S;
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
thus Top (MSSubAlLattice(U0)) = GenMSAlg(B) by Th35
.= the MSAlgebra of U0 by Th21;
end;
theorem
for S being non void non empty ManySortedSign, U0 being MSAlgebra over
S holds MSAlgebra (#the Sorts of U0,the Charact of U0#) is MSSubAlgebra of U0
by Lm1;
theorem
for S being non void non empty ManySortedSign, U0 being MSAlgebra over
S, A being MSSubset of U0 holds the Sorts of U0 in SubSort(A) by Lm2;
theorem
for S being non void non empty ManySortedSign, U0 being MSAlgebra over
S, A being MSSubset of U0 holds SubSort(A) c= SubSort(U0)
proof
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, A be
MSSubset of U0;
let x be object such that
A1: x in SubSort(A);
A2: for B be MSSubset of U0 st B = x holds B is opers_closed by A1,Def10;
x in Funcs(the carrier of S, bool (Union (the Sorts of U0))) & x is
MSSubset of U0 by A1,Def10;
hence thesis by A2,Def11;
end;