:: CLOSURE1 semantic presentation

scheme :: CLOSURE1:sch 1
MSSUBSET{ F₁() -> set , F₂() -> V3 ManySortedSet of F₁(), F₃() -> ManySortedSet of F₁(), P₁[ set ] } :

( ( for X being ManySortedSet of F₁() holds
( X in F₂() iff ( X in F₃() & P₁[X] ) ) ) implies F₂() c= F₃() )

proof end;

theorem Th1: :: CLOSURE1:1

for X being non empty set
for x, y being set st x c= y holds
{ t where t is Element of X : y c= t } c= { z where z is Element of X : x c= z }

proof end;

theorem :: CLOSURE1:2

for I being set
for M being ManySortedSet of I st ex A being ManySortedSet of I st A in M holds
M is non-empty

proof end;

definition

let I be set ;
let F be ManySortedFunction of I;
let A be ManySortedSet of I;
:: original: ..
redefine func F .. A -> ManySortedSet of I;
coherence

proof end;

end;

Lm1: now

let I be set ; :: thesis:
let A, B be V3 ManySortedSet of I; :: thesis:
let F be ManySortedFunction of A,B; :: thesis:
let X be Element of A; :: thesis:
thus F .. X is Element of B :: thesis:

proof

let i be set ; :: according to PBOOLE:def 17 :: thesis:
assume A1: i in I ; :: thesis:
A2: dom F = I by PBOOLE:def 3;
reconsider g = F . i as Function ;
A3: g is Function of A . i,B . i by A1, PBOOLE:def 18;
A4: A . i <> {} by A1, PBOOLE:def 16;
A5: B . i <> {} by A1, PBOOLE:def 16;
X . i is Element of A . i by A1, PBOOLE:def 17;
then g . (X . i) in B . i by A3, A4, A5, FUNCT_2:7;
hence (F .. X) . i is Element of B . i by A1, A2, PRALG_1:def 17; :: thesis:

end;

definition

let I be set ;
let A, B be V3 ManySortedSet of I;
let F be ManySortedFunction of A,B;
let X be Element of A;
:: original: ..
redefine func F .. X -> Element of B;
coherence by Lm1;

end;

theorem :: CLOSURE1:3

for I being set
for A, X being ManySortedSet of I
for B being V3 ManySortedSet of I
for F being ManySortedFunction of A,B st X in A holds
F .. X in B

proof end;

theorem Th4: :: CLOSURE1:4

for I being set
for F, G being ManySortedFunction of I
for A being ManySortedSet of I st A in doms G holds
F .. (G .. A) = (F ** G) .. A

proof end;

theorem :: CLOSURE1:5

for I being set
for F being ManySortedFunction of I st F is "1-1" holds
for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B

proof end;

theorem :: CLOSURE1:6

for I being set
for F being ManySortedFunction of I st doms F is non-empty & ( for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds
A = B ) holds
F is "1-1"

proof end;

theorem Th7: :: CLOSURE1:7

for I being set
for A, B being V3 ManySortedSet of I
for F, G being ManySortedFunction of A,B st ( for M being ManySortedSet of I st M in A holds
F .. M = G .. M ) holds
F = G

proof end;

registration

let I be set ;
let M be ManySortedSet of I;
cluster V4 locally-finite Element of bool M;
existence

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
mode MSSetOp of M is ManySortedFunction of bool M, bool M;

end;

definition

let I be set ;
let M be ManySortedSet of I;
let O be MSSetOp of M;
let X be Element of bool M;
:: original: ..
redefine func O .. X -> Element of bool M;
coherence by Lm1;

end;

definition

let I be set ;
let M be ManySortedSet of I;
let IT be MSSetOp of M;
canceled;
attr IT is reflexive means :Def2: :: CLOSURE1:def 2
for X being Element of bool M holds X c= IT .. X;
attr IT is monotonic means :Def3: :: CLOSURE1:def 3
for X, Y being Element of bool M st X c= Y holds
IT .. X c= IT .. Y;
attr IT is idempotent means :Def4: :: CLOSURE1:def 4
for X being Element of bool M holds IT .. X = IT .. (IT .. X);
attr IT is topological means :Def5: :: CLOSURE1:def 5
for X, Y being Element of bool M holds IT .. (X \/ Y) = (IT .. X) \/ (IT .. Y);

end;

:: deftheorem CLOSURE1:def 1 :

:: deftheorem Def2 defines reflexive CLOSURE1:def 2 :

:: deftheorem Def3 defines monotonic CLOSURE1:def 3 :

:: deftheorem Def4 defines idempotent CLOSURE1:def 4 :

:: deftheorem Def5 defines topological CLOSURE1:def 5 :

theorem Th8: :: CLOSURE1:8

for I being set
for M being V3 ManySortedSet of I
for X being Element of M holds X = (id M) .. X

proof end;

theorem Th9: :: CLOSURE1:9

for I being set
for M being V3 ManySortedSet of I
for X, Y being Element of M st X c= Y holds
(id M) .. X c= (id M) .. Y

proof end;

theorem Th10: :: CLOSURE1:10

for I being set
for M being V3 ManySortedSet of I
for X, Y being Element of M st X \/ Y is Element of M holds
(id M) .. (X \/ Y) = ((id M) .. X) \/ ((id M) .. Y)

proof end;

theorem :: CLOSURE1:11

for I being set
for M being ManySortedSet of I
for X being Element of bool M
for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds
ex Y being locally-finite Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )

proof end;

registration

let I be set ;
let M be ManySortedSet of I;
cluster reflexive monotonic idempotent topological ManySortedFunction of bool M, bool M;
existence

proof end;

end;

theorem :: CLOSURE1:12

for I being set
for A being ManySortedSet of I holds id (bool A) is reflexive MSSetOp of A

proof end;

theorem :: CLOSURE1:13

for I being set
for A being ManySortedSet of I holds id (bool A) is monotonic MSSetOp of A

proof end;

theorem :: CLOSURE1:14

for I being set
for A being ManySortedSet of I holds id (bool A) is idempotent MSSetOp of A

proof end;

theorem :: CLOSURE1:15

for I being set
for A being ManySortedSet of I holds id (bool A) is topological MSSetOp of A

proof end;

theorem :: CLOSURE1:16

for I being set
for M being ManySortedSet of I
for P being MSSetOp of M
for E being Element of bool M st E = M & P is reflexive holds
E = P .. E

proof end;

theorem :: CLOSURE1:17

for I being set
for M being ManySortedSet of I
for P being MSSetOp of M st P is reflexive & ( for X being Element of bool M holds P .. X c= X ) holds
P is idempotent

proof end;

theorem :: CLOSURE1:18

for I being set
for M being ManySortedSet of I
for P being MSSetOp of M
for E, T being Element of bool M st P is monotonic holds
P .. (E /\ T) c= (P .. E) /\ (P .. T)

proof end;

registration

let I be set ;
let M be ManySortedSet of I;
cluster topological -> monotonic ManySortedFunction of bool M, bool M;
coherence

proof end;

end;

theorem :: CLOSURE1:19

for I being set
for M being ManySortedSet of I
for P being MSSetOp of M
for E, T being Element of bool M st P is topological holds
(P .. E) \ (P .. T) c= P .. (E \ T)

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
let R, P be MSSetOp of M;
:: original: **
redefine func P ** R -> MSSetOp of M;
coherence

proof end;

end;

theorem :: CLOSURE1:20

for I being set
for M being ManySortedSet of I
for P, R being MSSetOp of M st P is reflexive & R is reflexive holds
P ** R is reflexive

proof end;

theorem :: CLOSURE1:21

for I being set
for M being ManySortedSet of I
for P, R being MSSetOp of M st P is monotonic & R is monotonic holds
P ** R is monotonic

proof end;

theorem :: CLOSURE1:22

for I being set
for M being ManySortedSet of I
for P, R being MSSetOp of M st P is idempotent & R is idempotent & P ** R = R ** P holds
P ** R is idempotent

proof end;

theorem :: CLOSURE1:23

for I being set
for M being ManySortedSet of I
for P, R being MSSetOp of M st P is topological & R is topological holds
P ** R is topological

proof end;

Lm2: now

let I be set ; :: thesis:
let M be ManySortedSet of I; :: thesis:
let i be set ; :: thesis:
let a be ManySortedSet of I; :: thesis:
let b be Element of bool (M . i); :: thesis:
assume that
i in I and
A1: a = ([0] I) +* (i .--> b) ; :: thesis:
[0] I c= M by MBOOLEAN:5;
then A2: [0] I in bool M by MBOOLEAN:1;
A3: dom (i .--> b) = {i} by CQC_LANG:5;
thus a in bool M :: thesis:

proof

let j be set ; :: according to PBOOLE:def 4 :: thesis:
assume A4: j in I ; :: thesis:
i in {i} by TARSKI:def 1;
then A5: a . i = (i .--> b) . i by A1, A3, FUNCT_4:14
.= b by CQC_LANG:6 ;

now

per cases ;

case A6: j = i ; :: thesis:

then b in bool (M . j) ;
hence a . j in (bool M) . j by A4, A5, A6, MBOOLEAN:def 1; :: thesis:

end;

case j <> i ; :: thesis:

then not j in dom (i .--> b) by A3, TARSKI:def 1;
then a . j = ([0] I) . j by A1, FUNCT_4:12;
hence a . j in (bool M) . j by A2, A4, PBOOLE:def 4; :: thesis:

end;

hence a . j in (bool M) . j ; :: thesis:

end;

theorem Th24: :: CLOSURE1:24

for i, I being set
for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is reflexive & i in I & f = P . i holds
for x being Element of bool (M . i) holds x c= f . x

proof end;

theorem Th25: :: CLOSURE1:25

for i, I being set
for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds
for x, y being Element of bool (M . i) st x c= y holds
f . x c= f . y

proof end;

theorem Th26: :: CLOSURE1:26

for i, I being set
for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds
for x being Element of bool (M . i) holds f . x = f . (f . x)

proof end;

theorem :: CLOSURE1:27

for i, I being set
for M being ManySortedSet of I
for f being Function
for P being MSSetOp of M st P is topological & i in I & f = P . i holds
for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)

proof end;

definition

let S be 1-sorted ;
attr c₂ is strict;
struct MSClosureStr of S -> many-sorted of S;
aggr MSClosureStr(# Sorts, Family #) -> MSClosureStr of S;
sel Family c₂ -> MSSubsetFamily of the Sorts of c₂;

end;

definition

let S be 1-sorted ;
let IT be MSClosureStr of S;
attr IT is additive means :Def6: :: CLOSURE1:def 6
the Family of IT is additive;
attr IT is absolutely-additive means :Def7: :: CLOSURE1:def 7
the Family of IT is absolutely-additive;
attr IT is multiplicative means :Def8: :: CLOSURE1:def 8
the Family of IT is multiplicative;
attr IT is absolutely-multiplicative means :Def9: :: CLOSURE1:def 9
the Family of IT is absolutely-multiplicative;
attr IT is properly-upper-bound means :Def10: :: CLOSURE1:def 10
the Family of IT is properly-upper-bound;
attr IT is properly-lower-bound means :Def11: :: CLOSURE1:def 11
the Family of IT is properly-lower-bound;

end;

:: deftheorem Def6 defines additive CLOSURE1:def 6 :

:: deftheorem Def7 defines absolutely-additive CLOSURE1:def 7 :

:: deftheorem Def8 defines multiplicative CLOSURE1:def 8 :

:: deftheorem Def9 defines absolutely-multiplicative CLOSURE1:def 9 :

:: deftheorem Def10 defines properly-upper-bound CLOSURE1:def 10 :

:: deftheorem Def11 defines properly-lower-bound CLOSURE1:def 11 :

definition

let S be 1-sorted ;
let MS be many-sorted of S;
func MSFull MS -> MSClosureStr of S equals :: CLOSURE1:def 12
MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #);
correctness ;

end;

:: deftheorem defines MSFull CLOSURE1:def 12 :

registration

let S be 1-sorted ;
let MS be many-sorted of S;
cluster MSFull MS -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
coherence

proof end;

end;

registration

let S be 1-sorted ;
let MS be non-empty many-sorted of S;
cluster MSFull MS -> non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;
coherence by MSUALG_1:def 8;

end;

registration

let S be 1-sorted ;
cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSClosureStr of S;
existence

proof end;

end;

registration

let S be 1-sorted ;
let CS be additive MSClosureStr of S;
cluster the Family of CS -> additive ;
coherence by Def6;

end;

registration

let S be 1-sorted ;
let CS be absolutely-additive MSClosureStr of S;
cluster the Family of CS -> absolutely-additive ;
coherence by Def7;

end;

registration

let S be 1-sorted ;
let CS be multiplicative MSClosureStr of S;
cluster the Family of CS -> multiplicative ;
coherence by Def8;

end;

registration

let S be 1-sorted ;
let CS be absolutely-multiplicative MSClosureStr of S;
cluster the Family of CS -> absolutely-multiplicative ;
coherence by Def9;

end;

registration

let S be 1-sorted ;
let CS be properly-upper-bound MSClosureStr of S;
cluster the Family of CS -> properly-upper-bound ;
coherence by Def10;

end;

registration

let S be 1-sorted ;
let CS be properly-lower-bound MSClosureStr of S;
cluster the Family of CS -> properly-lower-bound ;
coherence by Def11;

end;

registration

let S be 1-sorted ;
let M be V3 ManySortedSet of the carrier of S;
let F be MSSubsetFamily of M;
cluster MSClosureStr(# M,F #) -> non-empty ;
coherence

proof end;

end;

registration

let S be 1-sorted ;
let MS be many-sorted of S;
let F be additive MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr(# the Sorts of MS,F #) -> additive ;
coherence by Def6;

end;

registration

let S be 1-sorted ;
let MS be many-sorted of S;
let F be absolutely-additive MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr(# the Sorts of MS,F #) -> additive absolutely-additive ;
coherence by Def7;

end;

registration

let S be 1-sorted ;
let MS be many-sorted of S;
let F be multiplicative MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr(# the Sorts of MS,F #) -> multiplicative ;
coherence by Def8;

end;

registration

let S be 1-sorted ;
let MS be many-sorted of S;
let F be absolutely-multiplicative MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr(# the Sorts of MS,F #) -> multiplicative absolutely-multiplicative ;
coherence by Def9;

end;

registration

let S be 1-sorted ;
let MS be many-sorted of S;
let F be properly-upper-bound MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr(# the Sorts of MS,F #) -> properly-upper-bound ;
coherence by Def10;

end;

registration

let S be 1-sorted ;
let MS be many-sorted of S;
let F be properly-lower-bound MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr(# the Sorts of MS,F #) -> properly-lower-bound ;
coherence by Def11;

end;

registration

let S be 1-sorted ;
cluster absolutely-additive -> additive MSClosureStr of S;
coherence

proof end;

end;

registration

let S be 1-sorted ;
cluster absolutely-multiplicative -> multiplicative MSClosureStr of S;
coherence

proof end;

end;

registration

let S be 1-sorted ;
cluster absolutely-multiplicative -> properly-upper-bound MSClosureStr of S;
coherence

proof end;

end;

registration

let S be 1-sorted ;
cluster absolutely-additive -> properly-lower-bound MSClosureStr of S;
coherence

proof end;

end;

definition

let S be 1-sorted ;
mode MSClosureSystem of S is absolutely-multiplicative MSClosureStr of S;

end;

definition

let I be set ;
let M be ManySortedSet of I;
mode MSClosureOperator of M is reflexive monotonic idempotent MSSetOp of M;

end;

definition

let I be set ;
let M be ManySortedSet of I;
let F be ManySortedFunction of M,M;
func MSFixPoints F -> ManySortedSubset of M means :Def13: :: CLOSURE1:def 13
for x, i being set st i in I holds
( x in it . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines MSFixPoints CLOSURE1:def 13 :

registration

let I be set ;
let M be V4 ManySortedSet of I;
let F be ManySortedFunction of M,M;
cluster MSFixPoints F -> V4 ;
coherence

proof end;

end;

theorem Th28: :: CLOSURE1:28

for I being set
for M, A being ManySortedSet of I
for F being ManySortedFunction of M,M holds
( ( A in M & F .. A = A ) iff A in MSFixPoints F )

proof end;

theorem :: CLOSURE1:29

for I being set
for A being ManySortedSet of I holds MSFixPoints (id A) = A

proof end;

theorem Th30: :: CLOSURE1:30

for S being 1-sorted
for A being ManySortedSet of the carrier of S
for J being reflexive monotonic MSSetOp of A
for D being MSSubsetFamily of A st D = MSFixPoints J holds
MSClosureStr(# A,D #) is MSClosureSystem of S

proof end;

theorem Th31: :: CLOSURE1:31

for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for X being Element of bool M ex SF being V3 MSSubsetFamily of M st
for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) )

proof end;

theorem Th32: :: CLOSURE1:32

for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for X being Element of bool M
for SF being V3 MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
for i being set
for Di being non empty set st i in I & Di = D . i holds
SF . i = { z where z is Element of Di : X . i c= z }

proof end;

theorem Th33: :: CLOSURE1:33

for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M ex J being MSSetOp of M st
for X being Element of bool M
for SF being V3 MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF

proof end;

theorem Th34: :: CLOSURE1:34

for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for A being Element of bool M
for J being MSSetOp of M st A in D & ( for X being Element of bool M
for SF being V3 MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J .. A = A

proof end;

theorem :: CLOSURE1:35

for I being set
for M being ManySortedSet of I
for D being absolutely-multiplicative MSSubsetFamily of M
for A being Element of bool M
for J being MSSetOp of M st J .. A = A & ( for X being Element of bool M
for SF being V3 MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
A in D

proof end;

theorem Th36: :: CLOSURE1:36

for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for J being MSSetOp of M st ( for X being Element of bool M
for SF being V3 MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
( J is reflexive & J is monotonic )

proof end;

theorem Th37: :: CLOSURE1:37

for I being set
for M being ManySortedSet of I
for D being absolutely-multiplicative MSSubsetFamily of M
for J being MSSetOp of M st ( for X being Element of bool M
for SF being V3 MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is idempotent

proof end;

theorem :: CLOSURE1:38

for S being 1-sorted
for D being MSClosureSystem of S
for J being MSSetOp of the Sorts of D st ( for X being Element of bool the Sorts of D
for SF being V3 MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is MSClosureOperator of the Sorts of D by Th36, Th37;

definition

let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
func ClOp->ClSys C -> MSClosureSystem of S means :Def14: :: CLOSURE1:def 14
ex D being MSSubsetFamily of A st
( D = MSFixPoints C & it = MSClosureStr(# A,D #) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def14 defines ClOp->ClSys CLOSURE1:def 14 :

registration

let S be 1-sorted ;
let A be ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
cluster ClOp->ClSys C -> strict ;
coherence

proof end;

end;

registration

let S be 1-sorted ;
let A be V3 ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
cluster ClOp->ClSys C -> non-empty strict ;
coherence

proof end;

end;

definition

let S be 1-sorted ;
let D be MSClosureSystem of S;
func ClSys->ClOp D -> MSClosureOperator of the Sorts of D means :Def15: :: CLOSURE1:def 15
for X being Element of bool the Sorts of D
for SF being V3 MSSubsetFamily of the Sorts of D st ( for Y being ManySortedSet of the carrier of S holds
( Y in SF iff ( Y in the Family of D & X c= Y ) ) ) holds
it .. X = meet SF;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines ClSys->ClOp CLOSURE1:def 15 :

theorem :: CLOSURE1:39

for S being 1-sorted
for A being ManySortedSet of the carrier of S
for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J

proof end;

theorem :: CLOSURE1:40

for S being 1-sorted
for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D,the Family of D #)

proof end;