:: ARMSTRNG semantic presentation

E1: now

let c₁ be Nat;
let c₂ be non empty set ;
let c₃ be Tuple of c₁,c₂;
len c₃ = c₁ by FINSEQ_2:109;
hence dom c₃ = Seg c₁ by FINSEQ_1:def 3;

end;

theorem Th1: :: ARMSTRNG:1

for b₁ being set st b₁ is (B2) holds
for b₂ being set
for b₃ being finite Subset-Family of b₂ st b₂ in b₁ & b₃ c= b₁ holds
Intersect b₃ in b₁

proof end;

registration

cluster non empty reflexive antisymmetric transitive set ;
existence

proof end;

end;

theorem Th2: :: ARMSTRNG:2

for b₁ being non empty antisymmetric transitive Relation
for b₂ being finite Subset of (field b₁) st b₂ <> {} holds
ex b₃ being Element of b₂ st b₃ is_maximal_wrt b₂,b₁

proof end;

scheme :: ARMSTRNG:sch 1
s1{ F₁() -> set , P₁[ set ] } :

for b₁, b₂ being Subset of F₁() st ( for b₃ being set holds
( b₃ in b₁ iff P₁[b₃] ) ) & ( for b₃ being set holds
( b₃ in b₂ iff P₁[b₃] ) ) holds
b₁ = b₂

proof end;

definition

let c₁ be set ;
let c₂ be Relation;
func c₂ Maximal_in c₁ -> Subset of a₁ means :Def1: :: ARMSTRNG:def 1
for b₁ being set holds
( b₁ in a₃ iff b₁ is_maximal_wrt a₁,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Maximal_in ARMSTRNG:def 1 :

definition

let c₁, c₂ be set ;
pred c₁ is_/\-irreducible_in c₂ means :Def2: :: ARMSTRNG:def 2
( a₁ in a₂ & ( for b₁, b₂ being set st b₁ in a₂ & b₂ in a₂ & a₁ = b₁ /\ b₂ & not a₁ = b₁ holds
a₁ = b₂ ) );

end;

:: deftheorem Def2 defines is_/\-irreducible_in ARMSTRNG:def 2 :

notation

let c₁, c₂ be set ;
antonym c₁ is_/\-reducible_in c₂ for c₁ is_/\-irreducible_in c₂;

end;

definition

let c₁ be non empty set ;
func /\-IRR c₁ -> Subset of a₁ means :Def3: :: ARMSTRNG:def 3
for b₁ being set holds
( b₁ in a₂ iff b₁ is_/\-irreducible_in a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines /\-IRR ARMSTRNG:def 3 :

scheme :: ARMSTRNG:sch 2
s2{ F₁() -> non empty finite set , P₁[ set ] } :

for b₁ being set st b₁ in F₁() holds
P₁[b₁]

provided

E7: for b₁ being set st b₁ is_/\-irreducible_in F₁() holds
P₁[b₁] and
E8: for b₁, b₂ being set st b₁ in F₁() & b₂ in F₁() & P₁[b₁] & P₁[b₂] holds
P₁[b₁ /\ b₂]

proof end;

theorem Th3: :: ARMSTRNG:3

for b₁ being non empty finite set
for b₂ being Element of b₁ ex b₃ being non empty Subset of b₁ st
( b₂ = meet b₃ & ( for b₄ being set st b₄ in b₃ holds
b₄ is_/\-irreducible_in b₁ ) )

proof end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
attr a₂ is (B1) means :Def4: :: ARMSTRNG:def 4
a₁ in a₂;

end;

:: deftheorem Def4 defines (B1) ARMSTRNG:def 4 :

notation

let c₁ be set ;
synonym (B2) c₁ for cap-closed c₁;

end;

registration

let c₁ be set ;
cluster (B2) (B1) Element of bool (bool a₁);
existence

proof end;

end;

theorem Th4: :: ARMSTRNG:4

for b₁ being set
for b₂ being non empty Subset-Family of b₁ st b₂ is (B2) holds
for b₃ being Element of b₂ st b₃ is_/\-irreducible_in b₂ & b₃ <> b₁ holds
for b₄ being finite Subset-Family of b₁ st b₄ c= b₂ & b₃ = Intersect b₄ holds
b₃ in b₄

proof end;

registration

let c₁, c₂ be non empty set ;
let c₃ be Nat;
cluster -> FinSequence-yielding Relation of a₁,a₃ -tuples_on a₂;
coherence

proof end;

end;

registration

let c₁ be FinSequence-yielding Function;
let c₂ be set ;
cluster a₁ . a₂ -> FinSequence-like ;
coherence

proof end;

end;

definition

let c₁ be Nat;
let c₂, c₃ be Tuple of c₁,BOOLEAN ;
func c₂ '&' c₃ -> Tuple of a₁,BOOLEAN means :Def5: :: ARMSTRNG:def 5
for b₁ being set st b₁ in Seg a₁ holds
a₄ . b₁ = (a₂ /. b₁) '&' (a₃ /. b₁);
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def5 defines '&' ARMSTRNG:def 5 :

theorem Th5: :: ARMSTRNG:5

for b₁ being Nat
for b₂ being Tuple of b₁,BOOLEAN holds (b₁ -BinarySequence 0) '&' b₂ = b₁ -BinarySequence 0

proof end;

theorem Th6: :: ARMSTRNG:6

for b₁ being Nat
for b₂ being Tuple of b₁,BOOLEAN holds ('not' (b₁ -BinarySequence 0)) '&' b₂ = b₂

proof end;

theorem Th7: :: ARMSTRNG:7

canceled;

theorem Th8: :: ARMSTRNG:8

for b₁, b₂ being Nat st b₂ < b₁ holds
( (b₁ -BinarySequence (2 to_power b₂)) . (b₂ + 1) = 1 & ( for b₃ being Nat st b₃ in Seg b₁ & b₃ <> b₂ + 1 holds
(b₁ -BinarySequence (2 to_power b₂)) . b₃ = 0 ) )

proof end;

definition

attr a₁ is strict;
struct DB-Rel -> ;
aggr DB-Rel(# Attributes, Domains, Relationship #) -> DB-Rel ;
sel Attributes c₁ -> non empty finite set ;
sel Domains c₁ -> V2 ManySortedSet of the Attributes of a₁;
sel Relationship c₁ -> Subset of (product the Domains of a₁);

end;

definition

let c₁ be set ;
mode Subset-Relation of a₁ is Relation of bool a₁;
mode Dependency-set of a₁ is Relation of bool a₁;

end;

registration

let c₁ be set ;
cluster non empty finite Relation of bool a₁, bool a₁;
existence

proof end;

end;

definition

let c₁ be set ;
canceled;
func Dependencies c₁ -> Dependency-set of a₁ equals :: ARMSTRNG:def 7
[:(bool a₁),(bool a₁):];
coherence by RELSET_1:def 1;

end;

:: deftheorem Def6 ARMSTRNG:def 6 :

:: deftheorem Def7 defines Dependencies ARMSTRNG:def 7 :

definition

let c₁ be set ;
mode Dependency of a₁ is Element of Dependencies a₁;

end;

registration

let c₁ be set ;
cluster Dependencies a₁ -> non empty ;
coherence ;

end;

definition

let c₁ be set ;
let c₂ be non empty Dependency-set of c₁;
redefine mode Element as Element of c₂ -> Dependency of a₁;
correctness

proof end;

end;

theorem Th9: :: ARMSTRNG:9

for b₁, b₂ being set holds
( b₂ in Dependencies b₁ iff ex b₃, b₄ being Subset of b₁ st b₂ = [b₃,b₄] )

proof end;

theorem Th10: :: ARMSTRNG:10

for b₁, b₂ being set
for b₃ being Dependency-set of b₁ st b₂ in b₃ holds
ex b₄, b₅ being Subset of b₁ st b₂ = [b₄,b₅]

proof end;

definition

let c₁ be DB-Rel ;
let c₂, c₃ be Subset of the Attributes of c₁;
pred c₂ >|> c₃,c₁ means :Def8: :: ARMSTRNG:def 8
for b₁, b₂ being Element of the Relationship of a₁ st b₁ | a₂ = b₂ | a₂ holds
b₁ | a₃ = b₂ | a₃;

end;

:: deftheorem Def8 defines >|> ARMSTRNG:def 8 :

notation

let c₁ be DB-Rel ;
let c₂, c₃ be Subset of the Attributes of c₁;
synonym c₂,c₃ holds_in c₁ for c₂ >|> c₃,c₁;

end;

definition

let c₁ be DB-Rel ;
func Dependency-str c₁ -> Dependency-set of the Attributes of a₁ equals :: ARMSTRNG:def 9
{ [b₁,b₂] where B is Subset of the Attributes of a₁, B is Subset of the Attributes of a₁ : b₁ >|> b₂,a₁ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines Dependency-str ARMSTRNG:def 9 :

theorem Th11: :: ARMSTRNG:11

canceled;

theorem Th12: :: ARMSTRNG:12

for b₁ being DB-Rel
for b₂, b₃ being Subset of the Attributes of b₁ holds
( [b₂,b₃] in Dependency-str b₁ iff b₂ >|> b₃,b₁ )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be Dependency of c₁;
pred c₂ >= c₃ means :Def10: :: ARMSTRNG:def 10
( a₂ `1 c= a₃ `1 & a₃ `2 c= a₂ `2 );
reflexivity ;

end;

:: deftheorem Def10 defines >= ARMSTRNG:def 10 :

notation

let c₁ be set ;
let c₂, c₃ be Dependency of c₁;
synonym c₃ <= c₂ for c₂ >= c₃;
synonym c₂ is_at_least_as_informative_as c₃ for c₂ >= c₃;

end;

theorem Th13: :: ARMSTRNG:13

for b₁ being set
for b₂, b₃ being Dependency of b₁ st b₂ <= b₃ & b₃ <= b₂ holds
b₂ = b₃

proof end;

theorem Th14: :: ARMSTRNG:14

for b₁ being set
for b₂, b₃, b₄ being Dependency of b₁ st b₂ <= b₃ & b₃ <= b₄ holds
b₂ <= b₄

proof end;

definition

let c₁ be set ;
let c₂, c₃ be Subset of c₁;
redefine func [ as [c₂,c₃] -> Dependency of a₁;
coherence by ZFMISC_1:def 2;

end;

theorem Th15: :: ARMSTRNG:15

for b₁ being set
for b₂, b₃, b₄, b₅ being Subset of b₁ holds
( [b₂,b₃] >= [b₄,b₅] iff ( b₂ c= b₄ & b₅ c= b₃ ) )

proof end;

definition

let c₁ be set ;
func Dependencies-Order c₁ -> Relation of Dependencies a₁ equals :: ARMSTRNG:def 11
{ [b₁,b₂] where B is Dependency of a₁, B is Dependency of a₁ : b₁ <= b₂ } ;
coherence

proof end;

end;

:: deftheorem Def11 defines Dependencies-Order ARMSTRNG:def 11 :

theorem Th16: :: ARMSTRNG:16

for b₁, b₂ being set holds
( b₂ in Dependencies-Order b₁ iff ex b₃, b₄ being Dependency of b₁ st
( b₂ = [b₃,b₄] & b₃ <= b₄ ) ) ;

theorem Th17: :: ARMSTRNG:17

for b₁ being set holds dom (Dependencies-Order b₁) = [:(bool b₁),(bool b₁):]

proof end;

theorem Th18: :: ARMSTRNG:18

for b₁ being set holds rng (Dependencies-Order b₁) = [:(bool b₁),(bool b₁):]

proof end;

theorem Th19: :: ARMSTRNG:19

for b₁ being set holds field (Dependencies-Order b₁) = [:(bool b₁),(bool b₁):]

proof end;

registration

let c₁ be set ;
cluster Dependencies-Order a₁ -> non empty ;
coherence by Th17, RELAT_1:60;
cluster Dependencies-Order a₁ -> reflexive antisymmetric transitive total ;
coherence

proof end;

end;

notation

let c₁ be set ;
let c₂ be Dependency-set of c₁;
synonym (F2) c₂ for transitive c₁;
synonym (DC1) c₂ for transitive c₁;

end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
attr a₂ is (F1) means :Def12: :: ARMSTRNG:def 12
for b₁ being Subset of a₁ holds [b₁,b₁] in a₂;

end;

:: deftheorem Def12 defines (F1) ARMSTRNG:def 12 :

notation

let c₁ be set ;
let c₂ be Dependency-set of c₁;
synonym (DC2) c₂ for (F1) c₂;

end;

theorem Th20: :: ARMSTRNG:20

for b₁ being set
for b₂ being Dependency-set of b₁ holds
( b₂ is (F2) iff for b₃, b₄, b₅ being Subset of b₁ st [b₃,b₄] in b₂ & [b₄,b₅] in b₂ holds
[b₃,b₅] in b₂ )

proof end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
attr a₂ is (F3) means :Def13: :: ARMSTRNG:def 13
for b₁, b₂, b₃, b₄ being Subset of a₁ st [b₁,b₂] in a₂ & [b₁,b₂] >= [b₃,b₄] holds
[b₃,b₄] in a₂;
attr a₂ is (F4) means :Def14: :: ARMSTRNG:def 14
for b₁, b₂, b₃, b₄ being Subset of a₁ st [b₁,b₂] in a₂ & [b₃,b₄] in a₂ holds
[(b₁ \/ b₃),(b₂ \/ b₄)] in a₂;

end;

:: deftheorem Def13 defines (F3) ARMSTRNG:def 13 :

:: deftheorem Def14 defines (F4) ARMSTRNG:def 14 :

theorem Th21: :: ARMSTRNG:21

for b₁ being set holds
( Dependencies b₁ is (F1) & Dependencies b₁ is (F2) & Dependencies b₁ is (F3) & Dependencies b₁ is (F4) )

proof end;

registration

let c₁ be set ;
cluster non empty (F2) (F1) (F3) (F4) Relation of bool a₁, bool a₁;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
attr a₂ is full_family means :Def15: :: ARMSTRNG:def 15
( a₂ is (F1) & a₂ is (F2) & a₂ is (F3) & a₂ is (F4) );

end;

:: deftheorem Def15 defines full_family ARMSTRNG:def 15 :

registration

let c₁ be set ;
cluster full_family Relation of bool a₁, bool a₁;
existence

proof end;

end;

definition

let c₁ be set ;
mode Full-family of a₁ is full_family Dependency-set of a₁;

end;

theorem Th22: :: ARMSTRNG:22

for b₁ being finite set
for b₂ being Dependency-set of b₁ holds b₂ is finite

proof end;

registration

let c₁ be finite set ;
cluster finite Relation of bool a₁, bool a₁;
existence

proof end;

cluster -> finite Relation of bool a₁, bool a₁;
coherence by Th22;

end;

registration

let c₁ be set ;
cluster full_family -> (F2) (F1) (F3) (F4) Relation of bool a₁, bool a₁;
coherence by Def15;
cluster (F2) (F1) (F3) (F4) -> full_family Relation of bool a₁, bool a₁;
correctness by Def15;

end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
attr a₂ is (DC3) means :Def16: :: ARMSTRNG:def 16
for b₁, b₂ being Subset of a₁ st b₂ c= b₁ holds
[b₁,b₂] in a₂;

end;

:: deftheorem Def16 defines (DC3) ARMSTRNG:def 16 :

registration

let c₁ be set ;
cluster (F1) (F3) -> (DC3) Relation of bool a₁, bool a₁;
coherence

proof end;

cluster (F2) (DC3) -> (F1) (F3) Relation of bool a₁, bool a₁;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster non empty (F2) (F1) (F3) (F4) full_family (DC3) Relation of bool a₁, bool a₁;
existence

proof end;

end;

theorem Th23: :: ARMSTRNG:23

for b₁ being set
for b₂ being Dependency-set of b₁ st b₂ is (DC3) & b₂ is (F2) holds
( b₂ is (F1) & b₂ is (F3) )

proof end;

theorem Th24: :: ARMSTRNG:24

for b₁ being set
for b₂ being Dependency-set of b₁ st b₂ is (F1) & b₂ is (F3) holds
b₂ is (DC3)

proof end;

registration

let c₁ be set ;
cluster (F1) -> non empty Relation of bool a₁, bool a₁;
coherence by Def12;

end;

theorem Th25: :: ARMSTRNG:25

for b₁ being DB-Rel holds Dependency-str b₁ is full_family

proof end;

theorem Th26: :: ARMSTRNG:26

for b₁ being set
for b₂ being Subset of b₁ holds { [b₃,b₄] where B is Subset of b₁, B is Subset of b₁ : ( b₂ c= b₃ or b₄ c= b₃ ) } is Full-family of b₁

proof end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
func Maximal_wrt c₂ -> Dependency-set of a₁ equals :: ARMSTRNG:def 17
(Dependencies-Order a₁) Maximal_in a₂;
coherence by RELSET_1:4;

end;

:: deftheorem Def17 defines Maximal_wrt ARMSTRNG:def 17 :

theorem Th27: :: ARMSTRNG:27

for b₁ being set
for b₂ being Dependency-set of b₁ holds Maximal_wrt b₂ c= b₂ ;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
let c₃, c₄ be set ;
pred c₃ ^|^ c₄,c₂ means :Def18: :: ARMSTRNG:def 18
[a₃,a₄] in Maximal_wrt a₂;

end;

:: deftheorem Def18 defines ^|^ ARMSTRNG:def 18 :

theorem Th28: :: ARMSTRNG:28

for b₁ being finite set
for b₂ being Dependency of b₁
for b₃ being Dependency-set of b₁ st b₂ in b₃ holds
ex b₄, b₅ being Subset of b₁ st
( [b₄,b₅] in Maximal_wrt b₃ & [b₄,b₅] >= b₂ )

proof end;

theorem Th29: :: ARMSTRNG:29

for b₁ being set
for b₂ being Dependency-set of b₁
for b₃, b₄ being Subset of b₁ holds
( b₃ ^|^ b₄,b₂ iff ( [b₃,b₄] in b₂ & ( for b₅, b₆ being Subset of b₁ holds
( not [b₅,b₆] in b₂ or ( not b₃ <> b₅ & not b₄ <> b₆ ) or not [b₃,b₄] <= [b₅,b₆] ) ) ) )

proof end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
attr a₂ is (M1) means :Def19: :: ARMSTRNG:def 19
for b₁ being Subset of a₁ ex b₂, b₃ being Subset of a₁ st
( [b₂,b₃] >= [b₁,b₁] & [b₂,b₃] in a₂ );
attr a₂ is (M2) means :Def20: :: ARMSTRNG:def 20
for b₁, b₂, b₃, b₄ being Subset of a₁ st [b₁,b₂] in a₂ & [b₃,b₄] in a₂ & [b₁,b₂] >= [b₃,b₄] holds
( b₁ = b₃ & b₂ = b₄ );
attr a₂ is (M3) means :Def21: :: ARMSTRNG:def 21
for b₁, b₂, b₃, b₄ being Subset of a₁ st [b₁,b₂] in a₂ & [b₃,b₄] in a₂ & b₃ c= b₂ holds
b₄ c= b₂;

end;

:: deftheorem Def19 defines (M1) ARMSTRNG:def 19 :

:: deftheorem Def20 defines (M2) ARMSTRNG:def 20 :

:: deftheorem Def21 defines (M3) ARMSTRNG:def 21 :

theorem Th30: :: ARMSTRNG:30

for b₁ being non empty finite set
for b₂ being Full-family of b₁ holds
( Maximal_wrt b₂ is (M1) & Maximal_wrt b₂ is (M2) & Maximal_wrt b₂ is (M3) )

proof end;

theorem Th31: :: ARMSTRNG:31

for b₁ being finite set
for b₂, b₃ being Dependency-set of b₁ st b₂ is (M1) & b₂ is (M2) & b₂ is (M3) & b₃ = { [b₄,b₅] where B is Subset of b₁, B is Subset of b₁ : ex b₁, b₂ being Subset of b₁ st
( [b₆,b₇] >= [b₄,b₅] & [b₆,b₇] in b₂ ) } holds
( b₂ = Maximal_wrt b₃ & b₃ is full_family & ( for b₄ being Full-family of b₁ st b₂ = Maximal_wrt b₄ holds
b₄ = b₃ ) )

proof end;

registration

let c₁ be non empty finite set ;
let c₂ be Full-family of c₁;
cluster Maximal_wrt a₂ -> non empty finite ;
coherence

proof end;

end;

theorem Th32: :: ARMSTRNG:32

for b₁ being finite set
for b₂ being Dependency-set of b₁
for b₃ being Subset of b₁ st b₂ = { [b₄,b₅] where B is Subset of b₁, B is Subset of b₁ : ( b₃ c= b₄ or b₅ c= b₄ ) } holds
{[b₃,b₁]} \/ { [b₄,b₄] where B is Subset of b₁ : not b₃ c= b₄ } = Maximal_wrt b₂

proof end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
func saturated-subsets c₂ -> Subset-Family of a₁ equals :: ARMSTRNG:def 22
{ b₁ where B is Subset of a₁ : ex b₁ being Subset of a₁ st b₂ ^|^ b₁,a₂ } ;
coherence

proof end;

end;

:: deftheorem Def22 defines saturated-subsets ARMSTRNG:def 22 :

notation

let c₁ be set ;
let c₂ be Dependency-set of c₁;
synonym closed_attribute_subset c₂ for saturated-subsets c₂;

end;

registration

let c₁ be set ;
let c₂ be finite Dependency-set of c₁;
cluster saturated-subsets a₂ -> finite ;
coherence

proof end;

end;

theorem Th33: :: ARMSTRNG:33

for b₁, b₂ being set
for b₃ being Dependency-set of b₁ holds
( b₂ in saturated-subsets b₃ iff ex b₄, b₅ being Subset of b₁ st
( b₂ = b₄ & b₅ ^|^ b₄,b₃ ) )

proof end;

theorem Th34: :: ARMSTRNG:34

for b₁ being non empty finite set
for b₂ being Full-family of b₁ holds
( saturated-subsets b₂ is (B1) & saturated-subsets b₂ is (B2) )

proof end;

definition

let c₁, c₂ be set ;
func c₁ deps_encl_by c₂ -> Dependency-set of a₁ equals :: ARMSTRNG:def 23
{ [b₁,b₂] where B is Subset of a₁, B is Subset of a₁ : for b₁ being set st b₃ in a₂ & b₁ c= b₃ holds
b₂ c= b₃ } ;
coherence

proof end;

end;

:: deftheorem Def23 defines deps_encl_by ARMSTRNG:def 23 :

theorem Th35: :: ARMSTRNG:35

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃ being Dependency-set of b₁ holds b₁ deps_encl_by b₂ is full_family

proof end;

theorem Th36: :: ARMSTRNG:36

for b₁ being non empty finite set
for b₂ being Subset-Family of b₁ holds b₂ c= saturated-subsets (b₁ deps_encl_by b₂)

proof end;

theorem Th37: :: ARMSTRNG:37

for b₁ being non empty finite set
for b₂ being Subset-Family of b₁ st b₂ is (B1) & b₂ is (B2) holds
( b₂ = saturated-subsets (b₁ deps_encl_by b₂) & ( for b₃ being Full-family of b₁ st b₂ = saturated-subsets b₃ holds
b₃ = b₁ deps_encl_by b₂ ) )

proof end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
func enclosure_of c₂ -> Subset-Family of a₁ equals :: ARMSTRNG:def 24
{ b₁ where B is Subset of a₁ : for b₁, b₂ being Subset of a₁ st [b₂,b₃] in a₂ & b₂ c= b₁ holds
b₃ c= b₁ } ;
coherence

proof end;

end;

:: deftheorem Def24 defines enclosure_of ARMSTRNG:def 24 :

theorem Th38: :: ARMSTRNG:38

for b₁ being non empty finite set
for b₂ being Dependency-set of b₁ holds
( enclosure_of b₂ is (B1) & enclosure_of b₂ is (B2) )

proof end;

theorem Th39: :: ARMSTRNG:39

for b₁ being non empty finite set
for b₂ being Dependency-set of b₁ holds
( b₂ c= b₁ deps_encl_by (enclosure_of b₂) & ( for b₃ being Dependency-set of b₁ st b₂ c= b₃ & b₃ is full_family holds
b₁ deps_encl_by (enclosure_of b₂) c= b₃ ) )

proof end;

definition

let c₁ be non empty finite set ;
let c₂ be Dependency-set of c₁;
func Dependency-closure c₂ -> Full-family of a₁ means :Def25: :: ARMSTRNG:def 25
( a₂ c= a₃ & ( for b₁ being Dependency-set of a₁ st a₂ c= b₁ & b₁ is full_family holds
a₃ c= b₁ ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def25 defines Dependency-closure ARMSTRNG:def 25 :

theorem Th40: :: ARMSTRNG:40

for b₁ being non empty finite set
for b₂ being Dependency-set of b₁ holds Dependency-closure b₂ = b₁ deps_encl_by (enclosure_of b₂)

proof end;

theorem Th41: :: ARMSTRNG:41

for b₁ being set
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ st b₃ = {b₁} \/ { b₄ where B is Subset of b₁ : not b₂ c= b₄ } holds
( b₃ is (B1) & b₃ is (B2) )

proof end;

theorem Th42: :: ARMSTRNG:42

for b₁ being non empty finite set
for b₂ being Dependency-set of b₁
for b₃ being Subset of b₁ st b₂ = { [b₄,b₅] where B is Subset of b₁, B is Subset of b₁ : ( b₃ c= b₄ or b₅ c= b₄ ) } holds
{b₁} \/ { b₄ where B is Subset of b₁ : not b₃ c= b₄ } = saturated-subsets b₂

proof end;

theorem Th43: :: ARMSTRNG:43

for b₁ being finite set
for b₂ being Dependency-set of b₁
for b₃ being Subset of b₁ st b₂ = { [b₄,b₅] where B is Subset of b₁, B is Subset of b₁ : ( b₃ c= b₄ or b₅ c= b₄ ) } holds
{b₁} \/ { b₄ where B is Subset of b₁ : not b₃ c= b₄ } = saturated-subsets b₂

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Subset-Family of c₁;
pred c₂ is_generator-set_of c₃ means :Def26: :: ARMSTRNG:def 26
( a₂ c= a₃ & a₃ = { (Intersect b₁) where B is Subset-Family of a₁ : b₁ c= a₂ } );

end;

:: deftheorem Def26 defines is_generator-set_of ARMSTRNG:def 26 :

theorem Th44: :: ARMSTRNG:44

for b₁ being non empty finite set
for b₂ being Subset-Family of b₁ holds b₂ is_generator-set_of saturated-subsets (b₁ deps_encl_by b₂)

proof end;

theorem Th45: :: ARMSTRNG:45

for b₁ being non empty finite set
for b₂ being Full-family of b₁ ex b₃ being Subset-Family of b₁ st
( b₃ is_generator-set_of saturated-subsets b₂ & b₂ = b₁ deps_encl_by b₃ )

proof end;

theorem Th46: :: ARMSTRNG:46

for b₁ being set
for b₂ being non empty finite Subset-Family of b₁ st b₂ is (B1) & b₂ is (B2) holds
/\-IRR b₂ is_generator-set_of b₂

proof end;

theorem Th47: :: ARMSTRNG:47

for b₁, b₂ being set
for b₃ being non empty finite Subset-Family of b₁ st b₃ is (B1) & b₃ is (B2) & b₂ is_generator-set_of b₃ holds
/\-IRR b₃ c= b₂ \/ {b₁}

proof end;

theorem Th48: :: ARMSTRNG:48

for b₁ being non empty finite set
for b₂ being Full-family of b₁ ex b₃ being DB-Rel st
( the Attributes of b₃ = b₁ & ( for b₄ being Element of b₁ holds the Domains of b₃ . b₄ = INT ) & b₂ = Dependency-str b₃ )

proof end;

Lemma56: for b₁, b₂, b₃ being set st b₂ = { [b₄,b₅] where B is Subset of b₁, B is Subset of b₁ : for b₁ being set st b₆ in b₃ & b₄ c= b₆ holds
b₅ c= b₆ } holds
for b₄, b₅ being Subset of b₁ holds
( [b₄,b₅] in b₂ iff for b₆ being set st b₆ in b₃ & b₄ c= b₆ holds
b₅ c= b₆ )

proof end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
func candidate-keys c₂ -> Subset-Family of a₁ equals :: ARMSTRNG:def 27
{ b₁ where B is Subset of a₁ : [b₁,a₁] in Maximal_wrt a₂ } ;
coherence

proof end;

end;

:: deftheorem Def27 defines candidate-keys ARMSTRNG:def 27 :

theorem Th49: :: ARMSTRNG:49

for b₁ being finite set
for b₂ being Dependency-set of b₁
for b₃ being Subset of b₁ st b₂ = { [b₄,b₅] where B is Subset of b₁, B is Subset of b₁ : ( b₃ c= b₄ or b₅ c= b₄ ) } holds
candidate-keys b₂ = {b₃}

proof end;

notation

let c₁ be set ;
antonym (C1) c₁ for empty c₁;

end;

definition

let c₁ be set ;
attr a₁ is without_proper_subsets means :Def28: :: ARMSTRNG:def 28
for b₁, b₂ being set st b₁ in a₁ & b₂ in a₁ & b₁ c= b₂ holds
b₁ = b₂;

end;

:: deftheorem Def28 defines without_proper_subsets ARMSTRNG:def 28 :

notation

let c₁ be set ;
synonym (C2) c₁ for without_proper_subsets c₁;

end;

theorem Th50: :: ARMSTRNG:50

for b₁ being DB-Rel holds
( candidate-keys (Dependency-str b₁) is (C1) & candidate-keys (Dependency-str b₁) is without_proper_subsets )

proof end;

theorem Th51: :: ARMSTRNG:51

for b₁ being finite set
for b₂ being Subset-Family of b₁ st b₂ is (C1) & b₂ is without_proper_subsets holds
ex b₃ being Full-family of b₁ st b₂ = candidate-keys b₃

proof end;

theorem Th52: :: ARMSTRNG:52

for b₁ being finite set
for b₂ being Subset-Family of b₁
for b₃ being set st b₂ is (C1) & b₂ is without_proper_subsets & b₃ = { b₄ where B is Subset of b₁ : for b₁ being Subset of b₁ st b₅ in b₂ holds
not b₅ c= b₄ } holds
b₂ = candidate-keys (b₁ deps_encl_by b₃)

proof end;

theorem Th53: :: ARMSTRNG:53

for b₁ being non empty finite set
for b₂ being Subset-Family of b₁ st b₂ is (C1) & b₂ is without_proper_subsets holds
ex b₃ being DB-Rel st
( the Attributes of b₃ = b₁ & b₂ = candidate-keys (Dependency-str b₃) )

proof end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
attr a₂ is (DC4) means :Def29: :: ARMSTRNG:def 29
for b₁, b₂, b₃ being Subset of a₁ st [b₁,b₂] in a₂ & [b₁,b₃] in a₂ holds
[b₁,(b₂ \/ b₃)] in a₂;
attr a₂ is (DC5) means :Def30: :: ARMSTRNG:def 30
for b₁, b₂, b₃, b₄ being Subset of a₁ st [b₁,b₂] in a₂ & [(b₂ \/ b₃),b₄] in a₂ holds
[(b₁ \/ b₃),b₄] in a₂;
attr a₂ is (DC6) means :Def31: :: ARMSTRNG:def 31
for b₁, b₂, b₃ being Subset of a₁ st [b₁,b₂] in a₂ holds
[(b₁ \/ b₃),b₂] in a₂;

end;

:: deftheorem Def29 defines (DC4) ARMSTRNG:def 29 :

:: deftheorem Def30 defines (DC5) ARMSTRNG:def 30 :

:: deftheorem Def31 defines (DC6) ARMSTRNG:def 31 :

theorem Th54: :: ARMSTRNG:54

for b₁ being set
for b₂ being Dependency-set of b₁ holds
( b₂ is (F1) & b₂ is (F2) & b₂ is (F3) & b₂ is (F4) iff ( b₂ is (F2) & b₂ is (DC3) & b₂ is (F4) ) ) by Th23, Th24;

theorem Th55: :: ARMSTRNG:55

for b₁ being set
for b₂ being Dependency-set of b₁ holds
( b₂ is (F1) & b₂ is (F2) & b₂ is (F3) & b₂ is (F4) iff ( b₂ is (F2) & b₂ is (DC3) & b₂ is (DC4) ) )

proof end;

theorem Th56: :: ARMSTRNG:56

for b₁ being set
for b₂ being Dependency-set of b₁ holds
( b₂ is (F1) & b₂ is (F2) & b₂ is (F3) & b₂ is (F4) iff ( b₂ is (F1) & b₂ is (DC5) & b₂ is (DC6) ) )

proof end;

definition

let c₁ be set ;
let c₂ be Dependency-set of c₁;
func charact_set c₂ -> set equals :: ARMSTRNG:def 32
{ b₁ where B is Subset of a₁ : ex b₁, b₂ being Subset of a₁ st
( [b₂,b₃] in a₂ & b₂ c= b₁ & not b₃ c= b₁ ) } ;
correctness ;

end;

:: deftheorem Def32 defines charact_set ARMSTRNG:def 32 :

theorem Th57: :: ARMSTRNG:57

for b₁, b₂ being set
for b₃ being Dependency-set of b₁ st b₂ in charact_set b₃ holds
( b₂ is Subset of b₁ & ex b₄, b₅ being Subset of b₁ st
( [b₄,b₅] in b₃ & b₄ c= b₂ & not b₅ c= b₂ ) )

proof end;

theorem Th58: :: ARMSTRNG:58

for b₁ being set
for b₂ being Subset of b₁
for b₃ being Dependency-set of b₁ st ex b₄, b₅ being Subset of b₁ st
( [b₄,b₅] in b₃ & b₄ c= b₂ & not b₅ c= b₂ ) holds
b₂ in charact_set b₃ ;

theorem Th59: :: ARMSTRNG:59

for b₁ being non empty finite set
for b₂ being Dependency-set of b₁ holds
( ( for b₃, b₄ being Subset of b₁ holds
( [b₃,b₄] in Dependency-closure b₂ iff for b₅ being Subset of b₁ st b₃ c= b₅ & not b₄ c= b₅ holds
b₅ in charact_set b₂ ) ) & saturated-subsets (Dependency-closure b₂) = (bool b₁) \ (charact_set b₂) )

proof end;

theorem Th60: :: ARMSTRNG:60

for b₁ being non empty finite set
for b₂, b₃ being Dependency-set of b₁ st charact_set b₂ = charact_set b₃ holds
Dependency-closure b₂ = Dependency-closure b₃

proof end;

theorem Th61: :: ARMSTRNG:61

for b₁ being non empty finite set
for b₂ being Dependency-set of b₁ holds charact_set b₂ = charact_set (Dependency-closure b₂)

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Dependency-set of c₁;
pred c₂ is_p_i_w_ncv_of c₃ means :Def33: :: ARMSTRNG:def 33
( ( for b₁ being Subset of a₁ st a₂ c= b₁ & b₁ <> a₁ holds
b₁ in charact_set a₃ ) & ( for b₁ being set st b₁ c< a₂ holds
ex b₂ being Subset of a₁ st
( b₁ c= b₂ & b₂ <> a₁ & not b₂ in charact_set a₃ ) ) );

end;

:: deftheorem Def33 defines is_p_i_w_ncv_of ARMSTRNG:def 33 :

theorem Th62: :: ARMSTRNG:62

for b₁ being non empty finite set
for b₂ being Dependency-set of b₁
for b₃ being Subset of b₁ holds
( b₃ in candidate-keys (Dependency-closure b₂) iff b₃ is_p_i_w_ncv_of b₂ )

proof end;