msualg_2.miz
begin
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 ::
MSUALG_2:1
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 be
object st y
in (
dom ((X
(/\) Y)
* i)) holds (g
. y)
in (((X
(/\) Y)
* i)
. y) by
CARD_3:def 5;
for y be
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 be
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 be
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 be
object st y
in (
dom (Y
* i)) holds (h
. y)
in ((Y
* i)
. y) by
CARD_3:def 5;
for y be
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
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;
::
MSUALG_2:def1
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;
::
MSUALG_2:def2
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;
::
MSUALG_2:def3
func
Constants (U0,s) ->
Subset of (the
Sorts of U0
. s) means
:
Def3: ex A be non
empty
set st A
= (the
Sorts of U0
. s) & it
= { a where a be
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 be
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 be
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;
::
MSUALG_2:def4
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 be non
empty
set st A
= (the
Sorts of U0
. s) & (
Constants (U0,s))
= { b where b be
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
definition
let S be non
void non
empty
ManySortedSign, U0 be
MSAlgebra over S, o be
OperSymbol of S, A be
MSSubset of U0;
::
MSUALG_2:def5
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;
::
MSUALG_2:def6
attr A is
opers_closed means for o be
OperSymbol of S holds A
is_closed_on o;
end
theorem ::
MSUALG_2:2
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 be
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;
::
MSUALG_2:def7
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;
::
MSUALG_2:def8
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 be
object st x
in the
carrier' of S holds ex y be
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 be
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 be
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 be
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 ::
MSUALG_2:3
Th3: for U0 be
MSAlgebra over S holds for B be
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 ::
MSUALG_2:4
Th4: for B be
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 be
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;
::
MSUALG_2:def9
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 be
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 be non
void non
empty
ManySortedSign, U0 be
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 be
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 ::
MSUALG_2:5
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,
RELAT_1:def 19;
hence (
rng ((
Den (o,U1))
| (((B
# )
* the
Arity of S)
. o)))
c= ((B
* the
ResultSort of S)
. o);
end;
for x be
object st x
in the
carrier' of S holds (f1
. x)
= (f2
. x) by
A1,
A2,
Th4;
hence thesis;
end;
theorem ::
MSUALG_2:6
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 be
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 ::
MSUALG_2:7
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 be
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 ::
MSUALG_2:8
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 be
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 ::
MSUALG_2:9
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 ::
MSUALG_2:10
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 be non
empty
set st A
= (the
Sorts of U0
. s) & (
Constants (U0,s))
= { b where b be
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 ::
MSUALG_2:11
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 ::
MSUALG_2:12
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
definition
let S be non
void non
empty
ManySortedSign, U0 be
MSAlgebra over S, A be
MSSubset of U0;
::
MSUALG_2:def10
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 be
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 be non
void non
empty
ManySortedSign, U0 be
MSAlgebra over S, A be
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;
::
MSUALG_2:def11
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 be
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
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);
::
MSUALG_2:def12
func
@ e ->
MSSubset of U0 equals e;
coherence by
Def11;
end
theorem ::
MSUALG_2:13
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 ::
MSUALG_2:14
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;
::
MSUALG_2:def13
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 be
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
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;
::
MSUALG_2:def14
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 ::
MSUALG_2:15
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 ::
MSUALG_2:16
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 ::
MSUALG_2:17
Th17: for A be
MSSubset of U0 holds 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 ::
MSUALG_2:18
Th18: for A be
MSSubset of U0 holds 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 ::
MSUALG_2:19
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 ::
MSUALG_2:20
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
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;
::
MSUALG_2:def15
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;
::
MSUALG_2:def16
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;
::
MSUALG_2:def17
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 ::
MSUALG_2:21
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 ::
MSUALG_2:22
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 ::
MSUALG_2:23
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;
::
MSUALG_2:def18
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 ::
MSUALG_2:24
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 ::
MSUALG_2:25
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 ::
MSUALG_2:26
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 ::
MSUALG_2:27
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 ::
MSUALG_2:28
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
definition
let S be non
void non
empty
ManySortedSign, U0 be
MSAlgebra over S;
::
MSUALG_2:def19
func
MSSub (U0) ->
set means
:
Def19: for x be
object holds x
in it iff x is
strict
MSSubAlgebra of U0;
existence
proof
reconsider X = the set of all (
GenMSAlg (
@ A)) where A be
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 be
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
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;
::
MSUALG_2:def20
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 be
Element of (
MSSub U0) holds ex z be
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) holds 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;
::
MSUALG_2:def21
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 be
Element of (
MSSub U0) holds ex z be
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) holds 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 ::
MSUALG_2:29
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 ::
MSUALG_2:30
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 ::
MSUALG_2:31
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 ::
MSUALG_2:32
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;
::
MSUALG_2:def22
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 be
Element of L holds (a
"\/" (b
"\/" c))
= ((a
"\/" b)
"\/" c) by
Th30,
BINOP_1:def 3;
A2: for a,b be
Element of L holds (a
"/\" b)
= (b
"/\" a) by
Th31,
BINOP_1:def 2;
A3: for a,b be
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 be
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 be
Element of L holds (a
"/\" (b
"/\" c))
= ((a
"/\" b)
"/\" c) by
Th32,
BINOP_1:def 3;
for a,b be
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 ::
MSUALG_2:33
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 ::
MSUALG_2:34
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 ::
MSUALG_2:35
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 ::
MSUALG_2:36
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 ::
MSUALG_2:37
for S be non
void non
empty
ManySortedSign, U0 be
MSAlgebra over S holds
MSAlgebra (# the
Sorts of U0, the
Charact of U0 #) is
MSSubAlgebra of U0 by
Lm1;
theorem ::
MSUALG_2:38
for S be non
void non
empty
ManySortedSign, U0 be
MSAlgebra over S, A be
MSSubset of U0 holds the
Sorts of U0
in (
SubSort A) by
Lm2;
theorem ::
MSUALG_2:39
for S be non
void non
empty
ManySortedSign, U0 be
MSAlgebra over S, A be
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;