:: CLOSURE3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let S be non empty 1-sorted ;
cluster 1-sorted(# the carrier of S #) -> non empty ;
coherence
not 1-sorted(# the carrier of S #) is empty by STRUCT_0:def 1;
end;

theorem Th1: :: CLOSURE3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for M, N being ManySortedSet of I holds M +* N = N
proof end;

theorem Th2: :: CLOSURE3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M, N being ManySortedSet of I
for F being SubsetFamily of M st N in F holds
meet |:F:| c=' N
proof end;

theorem Th3: :: CLOSURE3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra of S
for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
proof end;

definition
let I be set ;
let M be ManySortedSet of I;
let B, A be SubsetFamily of M;
pred A is_finer_than B means :Def1: :: CLOSURE3:def 1
for a being set st a in A holds
ex b being set st
( b in B & a c= b );
reflexivity
for A being SubsetFamily of M
for a being set st a in A holds
ex b being set st
( b in A & a c= b ) ;
pred B is_coarser_than A means :Def2: :: CLOSURE3:def 2
for b being set st b in B holds
ex a being set st
( a in A & a c= b );
reflexivity
for B being SubsetFamily of M
for b being set st b in B holds
ex a being set st
( a in B & a c= b ) ;
end;

:: deftheorem Def1 defines is_finer_than CLOSURE3:def 1 :
for I being set
for M being ManySortedSet of I
for B, A being SubsetFamily of M holds
( A is_finer_than B iff for a being set st a in A holds
ex b being set st
( b in B & a c= b ) );

:: deftheorem Def2 defines is_coarser_than CLOSURE3:def 2 :
for I being set
for M being ManySortedSet of I
for B, A being SubsetFamily of M holds
( B is_coarser_than A iff for b being set st b in B holds
ex a being set st
( a in A & a c= b ) );

theorem :: CLOSURE3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for A, B, C being SubsetFamily of M st A is_finer_than B & B is_finer_than C holds
A is_finer_than C
proof end;

theorem :: CLOSURE3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for A, B, C being SubsetFamily of M st A is_coarser_than B & B is_coarser_than C holds
A is_coarser_than C
proof end;

definition
let I be non empty set ;
let M be ManySortedSet of I;
func supp M -> set means :Def3: :: CLOSURE3:def 3
it = { x where x is Element of I : M . x <> {} } ;
correctness
existence
ex b1 being set st b1 = { x where x is Element of I : M . x <> {} } ;
uniqueness
for b1, b2 being set st b1 = { x where x is Element of I : M . x <> {} } & b2 = { x where x is Element of I : M . x <> {} } holds
b1 = b2;
;
end;

:: deftheorem Def3 defines supp CLOSURE3:def 3 :
for I being non empty set
for M being ManySortedSet of I
for b3 being set holds
( b3 = supp M iff b3 = { x where x is Element of I : M . x <> {} } );

theorem :: CLOSURE3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for M being V3 ManySortedSet of I holds M = ([0] I) +* (M | (supp M))
proof end;

theorem :: CLOSURE3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for M1, M2 being V3 ManySortedSet of I st supp M1 = supp M2 & M1 | (supp M1) = M2 | (supp M2) holds
M1 = M2
proof end;

theorem :: CLOSURE3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for M being ManySortedSet of I
for x being Element of I st not x in supp M holds
M . x = {}
proof end;

theorem Th9: :: CLOSURE3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set
for M being ManySortedSet of I
for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is locally-finite & supp a is finite & a c= x )
proof end;

definition
let I be set ;
let M be ManySortedSet of I;
let A be SubsetFamily of M;
func MSUnion A -> ManySortedSubset of M means :Def4: :: CLOSURE3:def 4
for i being set st i in I holds
it . i = union { (f . i) where f is Element of Bool M : f in A } ;
existence
ex b1 being ManySortedSubset of M st
for i being set st i in I holds
b1 . i = union { (f . i) where f is Element of Bool M : f in A }
proof end;
uniqueness
for b1, b2 being ManySortedSubset of M st ( for i being set st i in I holds
b1 . i = union { (f . i) where f is Element of Bool M : f in A } ) & ( for i being set st i in I holds
b2 . i = union { (f . i) where f is Element of Bool M : f in A } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines MSUnion CLOSURE3:def 4 :
for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M
for b4 being ManySortedSubset of M holds
( b4 = MSUnion A iff for i being set st i in I holds
b4 . i = union { (f . i) where f is Element of Bool M : f in A } );

definition
let I be set ;
let M be ManySortedSet of I;
let B be non empty SubsetFamily of M;
:: original: Element
redefine mode Element of B -> ManySortedSet of I;
coherence
for b1 being Element of B holds b1 is ManySortedSet of I
proof end;
end;

registration
let I be set ;
let M be ManySortedSet of I;
let A be empty SubsetFamily of M;
cluster MSUnion A -> V4 ;
coherence
MSUnion A is empty-yielding
proof end;
end;

theorem :: CLOSURE3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M holds MSUnion A = union |:A:|
proof end;

definition
let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original: \/
redefine func A \/ B -> SubsetFamily of M;
correctness
coherence
A \/ B is SubsetFamily of M;
by CLOSURE2:4;
end;

theorem :: CLOSURE3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
proof end;

theorem :: CLOSURE3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M st A c= B holds
MSUnion A c= MSUnion B
proof end;

definition
let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original: /\
redefine func A /\ B -> SubsetFamily of M;
correctness
coherence
A /\ B is SubsetFamily of M;
by CLOSURE2:5;
end;

theorem :: CLOSURE3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
proof end;

theorem :: CLOSURE3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being ManySortedSet of I
for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A
proof end;

definition
let I be non empty set ;
let M be ManySortedSet of I;
let S be SetOp of M;
attr S is algebraic means :: CLOSURE3:def 5
for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A = { (S . a) where a is Element of Bool M : ( a is locally-finite & supp a is finite & a c= x ) } & x = MSUnion A );
end;

:: deftheorem defines algebraic CLOSURE3:def 5 :
for I being non empty set
for M being ManySortedSet of I
for S being SetOp of M holds
( S is algebraic iff for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A = { (S . a) where a is Element of Bool M : ( a is locally-finite & supp a is finite & a c= x ) } & x = MSUnion A ) );

registration
let I be non empty set ;
let M be ManySortedSet of I;
cluster reflexive monotonic idempotent algebraic M4( Bool M, Bool M);
existence
ex b1 being SetOp of M st
( b1 is algebraic & b1 is reflexive & b1 is monotonic & b1 is idempotent )
proof end;
end;

definition
let S be non empty 1-sorted ;
let IT be ClosureSystem of S;
attr IT is algebraic means :: CLOSURE3:def 6
 ClSys->ClOp IT is algebraic;
end;

:: deftheorem defines algebraic CLOSURE3:def 6 :
for S being non empty 1-sorted
for IT being ClosureSystem of S holds
( IT is algebraic iff ClSys->ClOp IT is algebraic );

definition
let S be non empty non void ManySortedSign ;
let MA be non-empty MSAlgebra of S;
func SubAlgCl MA -> strict ClosureStr of 1-sorted(# the carrier of S #) means :Def7: :: CLOSURE3:def 7
( the Sorts of it = the Sorts of MA & the Family of it = SubSort MA );
existence
ex b1 being strict ClosureStr of 1-sorted(# the carrier of S #) st
( the Sorts of b1 = the Sorts of MA & the Family of b1 = SubSort MA )
proof end;
uniqueness
for b1, b2 being strict ClosureStr of 1-sorted(# the carrier of S #) st the Sorts of b1 = the Sorts of MA & the Family of b1 = SubSort MA & the Sorts of b2 = the Sorts of MA & the Family of b2 = SubSort MA holds
b1 = b2 ;
end;

:: deftheorem Def7 defines SubAlgCl CLOSURE3:def 7 :
for S being non empty non void ManySortedSign
for MA being non-empty MSAlgebra of S
for b3 being strict ClosureStr of 1-sorted(# the carrier of S #) holds
( b3 = SubAlgCl MA iff ( the Sorts of b3 = the Sorts of MA & the Family of b3 = SubSort MA ) );

theorem :: CLOSURE3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th16: :: CLOSURE3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra of S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA
proof end;

registration
let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra of S;
cluster SubAlgCl MA -> strict absolutely-multiplicative ;
coherence
SubAlgCl MA is absolutely-multiplicative
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra of S;
cluster SubAlgCl MA -> strict absolutely-multiplicative algebraic ;
coherence
SubAlgCl MA is algebraic
proof end;
end;