:: ARMSTRNG semantic presentation

Lm1: now

let n be Nat; :: thesis:
let X be non empty set ; :: thesis:
let t be Tuple of n,X; :: thesis:
len t = n by FINSEQ_2:109;
hence dom t = Seg n by FINSEQ_1:def 3; :: thesis:

end;

theorem Th1: :: ARMSTRNG:1

for B being set st B is (B2) holds
for X being set
for S being finite Subset-Family of X st X in B & S c= B holds
Intersect S in B

proof end;

registration

cluster non empty reflexive antisymmetric transitive set ;
existence

proof end;

end;

theorem Th2: :: ARMSTRNG:2

for R being non empty antisymmetric transitive Relation
for X being finite Subset of (field R) st X <> {} holds
ex x being Element of X st x is_maximal_wrt X,R

proof end;

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

for X1, X2 being Subset of F₁() st ( for y being set holds
( y in X1 iff P₁[y] ) ) & ( for y being set holds
( y in X2 iff P₁[y] ) ) holds
X1 = X2

proof end;

definition

let X be set ;
let R be Relation;
func R Maximal_in X -> Subset of X means :Def1: :: ARMSTRNG:def 1
for x being set holds
( x in it iff x is_maximal_wrt X,R );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Maximal_in ARMSTRNG:def 1 :

definition

let x, X be set ;
pred x is_/\-irreducible_in X means :Def2: :: ARMSTRNG:def 2
( x in X & ( for z, y being set st z in X & y in X & x = z /\ y & not x = z holds
x = y ) );

end;

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

notation

let x, X be set ;
antonym x is_/\-reducible_in X for x is_/\-irreducible_in X;

end;

definition

let X be non empty set ;
func /\-IRR X -> Subset of X means :Def3: :: ARMSTRNG:def 3
for x being set holds
( x in it iff x is_/\-irreducible_in X );
existence

proof end;

uniqueness

proof end;

end;

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

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

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

provided

A1: for x being set st x is_/\-irreducible_in F₁() holds
P₁[x] and
A2: for x, y being set st x in F₁() & y in F₁() & P₁[x] & P₁[y] holds
P₁[x /\ y]

proof end;

theorem Th3: :: ARMSTRNG:3

for X being non empty finite set
for x being Element of X ex A being non empty Subset of X st
( x = meet A & ( for s being set st s in A holds
s is_/\-irreducible_in X ) )

proof end;

definition

let X be set ;
let B be Subset-Family of X;
attr B is (B1) means :Def4: :: ARMSTRNG:def 4
X in B;

end;

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

notation

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

end;

registration

let X be set ;
cluster (B2) (B1) Element of bool (bool X);
existence

proof end;

end;

theorem Th4: :: ARMSTRNG:4

for X being set
for B being non empty Subset-Family of X st B is (B2) holds
for x being Element of B st x is_/\-irreducible_in B & x <> X holds
for S being finite Subset-Family of X st S c= B & x = Intersect S holds
x in S

proof end;

registration

let X, D be non empty set ;
let n be Nat;
cluster -> FinSequence-yielding Relation of X,n -tuples_on D;
coherence

proof end;

end;

registration

let f be FinSequence-yielding Function;
let x be set ;
cluster f . x -> FinSequence-like ;
coherence

proof end;

end;

definition

let n be Nat;
let p, q be Tuple of n,BOOLEAN ;
func p '&' q -> Tuple of n,BOOLEAN means :Def5: :: ARMSTRNG:def 5
for i being set st i in Seg n holds
it . i = (p /. i) '&' (q /. i);
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

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

theorem Th5: :: ARMSTRNG:5

for n being Nat
for p being Tuple of n,BOOLEAN holds (n -BinarySequence 0) '&' p = n -BinarySequence 0

proof end;

theorem :: ARMSTRNG:6

for n being Nat
for p being Tuple of n,BOOLEAN holds ('not' (n -BinarySequence 0)) '&' p = p

proof end;

theorem :: ARMSTRNG:7

canceled;

theorem Th8: :: ARMSTRNG:8

for n, i being Nat st i < n holds
( (n -BinarySequence (2 to_power i)) . (i + 1) = 1 & ( for j being Nat st j in Seg n & j <> i + 1 holds
(n -BinarySequence (2 to_power i)) . j = 0 ) )

proof end;

definition

attr c₁ 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 c₁;
sel Relationship c₁ -> Subset of (product the Domains of c₁);

end;

definition

let X be set ;
mode Subset-Relation of X is Relation of bool X;
mode Dependency-set of X is Relation of bool X;

end;

registration

let X be set ;
cluster non empty finite Relation of bool X, bool X;
existence

proof end;

end;

definition

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

end;

:: deftheorem ARMSTRNG:def 6 :

:: deftheorem defines Dependencies ARMSTRNG:def 7 :

definition

let X be set ;
mode Dependency of X is Element of Dependencies X;

end;

registration

let X be set ;
cluster Dependencies X -> non empty ;
coherence ;

end;

definition

let X be set ;
let F be non empty Dependency-set of X;
:: original: Element
redefine mode Element of F -> Dependency of X;
correctness

proof end;

end;

theorem Th9: :: ARMSTRNG:9

for X, x being set holds
( x in Dependencies X iff ex a, b being Subset of X st x = [a,b] )

proof end;

theorem Th10: :: ARMSTRNG:10

for X, x being set
for F being Dependency-set of X st x in F holds
ex a, b being Subset of X st x = [a,b]

proof end;

definition

let R be DB-Rel ;
let A, B be Subset of the Attributes of R;
pred A >|> B,R means :Def8: :: ARMSTRNG:def 8
for f, g being Element of the Relationship of R st f | A = g | A holds
f | B = g | B;

end;

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

notation

let R be DB-Rel ;
let A, B be Subset of the Attributes of R;
synonym A,B holds_in R for A >|> B,R;

end;

definition

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

proof end;

end;

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

theorem :: ARMSTRNG:11

canceled;

theorem Th12: :: ARMSTRNG:12

for R being DB-Rel
for A, B being Subset of the Attributes of R holds
( [A,B] in Dependency-str R iff A >|> B,R )

proof end;

definition

let X be set ;
let P, Q be Dependency of X;
pred P >= Q means :Def10: :: ARMSTRNG:def 10
( P `1 c= Q `1 & Q `2 c= P `2 );
reflexivity ;

end;

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

notation

let X be set ;
let P, Q be Dependency of X;
synonym Q <= P for P >= Q;
synonym P is_at_least_as_informative_as Q for P >= Q;

end;

theorem Th13: :: ARMSTRNG:13

for X being set
for P, Q being Dependency of X st P <= Q & Q <= P holds
P = Q

proof end;

theorem Th14: :: ARMSTRNG:14

for X being set
for P, Q, S being Dependency of X st P <= Q & Q <= S holds
P <= S

proof end;

definition

let X be set ;
let A, B be Subset of X;
:: original: [
redefine func [A,B] -> Dependency of X;
coherence by ZFMISC_1:def 2;

end;

theorem Th15: :: ARMSTRNG:15

for X being set
for A, B, A', B' being Subset of X holds
( [A,B] >= [A',B'] iff ( A c= A' & B' c= B ) )

proof end;

definition

let X be set ;
func Dependencies-Order X -> Relation of Dependencies X equals :: ARMSTRNG:def 11
{ [P,Q] where P, Q is Dependency of X : P <= Q } ;
coherence

proof end;

end;

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

theorem :: ARMSTRNG:16

for X, x being set holds
( x in Dependencies-Order X iff ex P, Q being Dependency of X st
( x = [P,Q] & P <= Q ) ) ;

theorem Th17: :: ARMSTRNG:17

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

proof end;

theorem Th18: :: ARMSTRNG:18

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

proof end;

theorem Th19: :: ARMSTRNG:19

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

proof end;

registration

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

proof end;

end;

notation

let X be set ;
let F be Dependency-set of X;
synonym (F2) F for transitive X;
synonym (DC1) F for transitive X;

end;

definition

let X be set ;
let F be Dependency-set of X;
attr F is (F1) means :Def12: :: ARMSTRNG:def 12
for A being Subset of X holds [A,A] in F;

end;

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

notation

let X be set ;
let F be Dependency-set of X;
synonym (DC2) F for (F1) F;

end;

theorem Th20: :: ARMSTRNG:20

for X being set
for F being Dependency-set of X holds
( F is (F2) iff for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in F )

proof end;

definition

let X be set ;
let F be Dependency-set of X;
attr F is (F3) means :Def13: :: ARMSTRNG:def 13
for A, B, A', B' being Subset of X st [A,B] in F & [A,B] >= [A',B'] holds
[A',B'] in F;
attr F is (F4) means :Def14: :: ARMSTRNG:def 14
for A, B, A', B' being Subset of X st [A,B] in F & [A',B'] in F holds
[(A \/ A'),(B \/ B')] in F;

end;

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

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

theorem Th21: :: ARMSTRNG:21

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

proof end;

registration

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

proof end;

end;

definition

let X be set ;
let F be Dependency-set of X;
attr F is full_family means :Def15: :: ARMSTRNG:def 15
( F is (F1) & F is (F2) & F is (F3) & F is (F4) );

end;

:: deftheorem Def15 defines full_family ARMSTRNG:def 15 :

registration

let X be set ;
cluster full_family Relation of bool X, bool X;
existence

proof end;

end;

definition

let X be set ;
mode Full-family of X is full_family Dependency-set of X;

end;

theorem Th22: :: ARMSTRNG:22

for X being finite set
for F being Dependency-set of X holds F is finite

proof end;

registration

let X be finite set ;
cluster finite Relation of bool X, bool X;
existence

proof end;

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

end;

registration

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

end;

definition

let X be set ;
let F be Dependency-set of X;
attr F is (DC3) means :Def16: :: ARMSTRNG:def 16
for A, B being Subset of X st B c= A holds
[A,B] in F;

end;

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

registration

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

proof end;

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

proof end;

end;

registration

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

proof end;

end;

theorem Th23: :: ARMSTRNG:23

for X being set
for F being Dependency-set of X st F is (DC3) & F is (F2) holds
( F is (F1) & F is (F3) )

proof end;

theorem Th24: :: ARMSTRNG:24

for X being set
for F being Dependency-set of X st F is (F1) & F is (F3) holds
F is (DC3)

proof end;

registration

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

end;

theorem Th25: :: ARMSTRNG:25

for R being DB-Rel holds Dependency-str R is full_family

proof end;

theorem :: ARMSTRNG:26

for X being set
for K being Subset of X holds { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } is Full-family of X

proof end;

definition

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

end;

:: deftheorem defines Maximal_wrt ARMSTRNG:def 17 :

theorem :: ARMSTRNG:27

for X being set
for F being Dependency-set of X holds Maximal_wrt F c= F ;

definition

let X be set ;
let F be Dependency-set of X;
let x, y be set ;
pred x ^|^ y,F means :Def18: :: ARMSTRNG:def 18
[x,y] in Maximal_wrt F;

end;

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

theorem Th28: :: ARMSTRNG:28

for X being finite set
for P being Dependency of X
for F being Dependency-set of X st P in F holds
ex A, B being Subset of X st
( [A,B] in Maximal_wrt F & [A,B] >= P )

proof end;

theorem Th29: :: ARMSTRNG:29

for X being set
for F being Dependency-set of X
for A, B being Subset of X holds
( A ^|^ B,F iff ( [A,B] in F & ( for A', B' being Subset of X holds
( not [A',B'] in F or ( not A <> A' & not B <> B' ) or not [A,B] <= [A',B'] ) ) ) )

proof end;

definition

let X be set ;
let M be Dependency-set of X;
attr M is (M1) means :Def19: :: ARMSTRNG:def 19
for A being Subset of X ex A', B' being Subset of X st
( [A',B'] >= [A,A] & [A',B'] in M );
attr M is (M2) means :Def20: :: ARMSTRNG:def 20
for A, B, A', B' being Subset of X st [A,B] in M & [A',B'] in M & [A,B] >= [A',B'] holds
( A = A' & B = B' );
attr M is (M3) means :Def21: :: ARMSTRNG:def 21
for A, B, A', B' being Subset of X st [A,B] in M & [A',B'] in M & A' 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 X being non empty finite set
for F being Full-family of X holds
( Maximal_wrt F is (M1) & Maximal_wrt F is (M2) & Maximal_wrt F is (M3) )

proof end;

theorem Th31: :: ARMSTRNG:31

for X being finite set
for M, F being Dependency-set of X st M is (M1) & M is (M2) & M is (M3) & F = { [A,B] where A, B is Subset of X : ex A', B' being Subset of X st
( [A',B'] >= [A,B] & [A',B'] in M ) } holds
( M = Maximal_wrt F & F is full_family & ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )

proof end;

registration

let X be non empty finite set ;
let F be Full-family of X;
cluster Maximal_wrt F -> non empty finite ;
coherence

proof end;

end;

theorem Th32: :: ARMSTRNG:32

for X being finite set
for F being Dependency-set of X
for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
{[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F

proof end;

definition

let X be set ;
let F be Dependency-set of X;
func saturated-subsets F -> Subset-Family of X equals :: ARMSTRNG:def 22
{ B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } ;
coherence

proof end;

end;

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

notation

let X be set ;
let F be Dependency-set of X;
synonym closed_attribute_subset F for saturated-subsets F;

end;

registration

let X be set ;
let F be finite Dependency-set of X;
cluster saturated-subsets F -> finite ;
coherence

proof end;

end;

theorem Th33: :: ARMSTRNG:33

for X, x being set
for F being Dependency-set of X holds
( x in saturated-subsets F iff ex B, A being Subset of X st
( x = B & A ^|^ B,F ) )

proof end;

theorem Th34: :: ARMSTRNG:34

for X being non empty finite set
for F being Full-family of X holds
( saturated-subsets F is (B1) & saturated-subsets F is (B2) )

proof end;

definition

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

proof end;

end;

:: deftheorem defines deps_encl_by ARMSTRNG:def 23 :

theorem Th35: :: ARMSTRNG:35

for X being set
for B being Subset-Family of X
for F being Dependency-set of X holds X deps_encl_by B is full_family

proof end;

theorem Th36: :: ARMSTRNG:36

for X being non empty finite set
for B being Subset-Family of X holds B c= saturated-subsets (X deps_encl_by B)

proof end;

theorem Th37: :: ARMSTRNG:37

for X being non empty finite set
for B being Subset-Family of X st B is (B1) & B is (B2) holds
( B = saturated-subsets (X deps_encl_by B) & ( for G being Full-family of X st B = saturated-subsets G holds
G = X deps_encl_by B ) )

proof end;

definition

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

proof end;

end;

:: deftheorem defines enclosure_of ARMSTRNG:def 24 :

theorem Th38: :: ARMSTRNG:38

for X being non empty finite set
for F being Dependency-set of X holds
( enclosure_of F is (B1) & enclosure_of F is (B2) )

proof end;

theorem Th39: :: ARMSTRNG:39

for X being non empty finite set
for F being Dependency-set of X holds
( F c= X deps_encl_by (enclosure_of F) & ( for G being Dependency-set of X st F c= G & G is full_family holds
X deps_encl_by (enclosure_of F) c= G ) )

proof end;

definition

let X be non empty finite set ;
let F be Dependency-set of X;
func Dependency-closure F -> Full-family of X means :Def25: :: ARMSTRNG:def 25
( F c= it & ( for G being Dependency-set of X st F c= G & G is full_family holds
it c= G ) );
existence

proof end;

correctness

proof end;

end;

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

theorem Th40: :: ARMSTRNG:40

for X being non empty finite set
for F being Dependency-set of X holds Dependency-closure F = X deps_encl_by (enclosure_of F)

proof end;

theorem Th41: :: ARMSTRNG:41

for X being set
for K being Subset of X
for B being Subset-Family of X st B = {X} \/ { A where A is Subset of X : not K c= A } holds
( B is (B1) & B is (B2) )

proof end;

theorem :: ARMSTRNG:42

for X being non empty finite set
for F being Dependency-set of X
for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
{X} \/ { B where B is Subset of X : not K c= B } = saturated-subsets F

proof end;

theorem :: ARMSTRNG:43

for X being finite set
for F being Dependency-set of X
for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
{X} \/ { B where B is Subset of X : not K c= B } = saturated-subsets F

proof end;

definition

let X, G be set ;
let B be Subset-Family of X;
pred G is_generator-set_of B means :Def26: :: ARMSTRNG:def 26
( G c= B & B = { (Intersect S) where S is Subset-Family of X : S c= G } );

end;

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

theorem :: ARMSTRNG:44

for X being non empty finite set
for G being Subset-Family of X holds G is_generator-set_of saturated-subsets (X deps_encl_by G)

proof end;

theorem Th45: :: ARMSTRNG:45

for X being non empty finite set
for F being Full-family of X ex G being Subset-Family of X st
( G is_generator-set_of saturated-subsets F & F = X deps_encl_by G )

proof end;

theorem :: ARMSTRNG:46

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

proof end;

theorem :: ARMSTRNG:47

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

proof end;

theorem :: ARMSTRNG:48

for X being non empty finite set
for F being Full-family of X ex R being DB-Rel st
( the Attributes of R = X & ( for a being Element of X holds the Domains of R . a = INT ) & F = Dependency-str R )

proof end;

Lm2: for X, F, BB being set st F = { [a,b] where a, b is Subset of X : for c being set st c in BB & a c= c holds
b c= c } holds
for x, y being Subset of X holds
( [x,y] in F iff for c being set st c in BB & x c= c holds
y c= c )

proof end;

definition

let X be set ;
let F be Dependency-set of X;
func candidate-keys F -> Subset-Family of X equals :: ARMSTRNG:def 27
{ A where A is Subset of X : [A,X] in Maximal_wrt F } ;
coherence

proof end;

end;

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

theorem :: ARMSTRNG:49

for X being finite set
for F being Dependency-set of X
for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
candidate-keys F = {K}

proof end;

notation

let X be set ;
antonym (C1) X for empty X;

end;

definition

let X be set ;
attr X is without_proper_subsets means :Def28: :: ARMSTRNG:def 28
for x, y being set st x in X & y in X & x c= y holds
x = y;

end;

:: deftheorem Def28 defines without_proper_subsets ARMSTRNG:def 28 :

notation

let X be set ;
synonym (C2) X for without_proper_subsets X;

end;

theorem :: ARMSTRNG:50

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

proof end;

theorem :: ARMSTRNG:51

for X being finite set
for C being Subset-Family of X st C is (C1) & C is without_proper_subsets holds
ex F being Full-family of X st C = candidate-keys F

proof end;

theorem :: ARMSTRNG:52

for X being finite set
for C being Subset-Family of X
for B being set st C is (C1) & C is without_proper_subsets & B = { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } holds
C = candidate-keys (X deps_encl_by B)

proof end;

theorem :: ARMSTRNG:53

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

proof end;

definition

let X be set ;
let F be Dependency-set of X;
attr F is (DC4) means :Def29: :: ARMSTRNG:def 29
for A, B, C being Subset of X st [A,B] in F & [A,C] in F holds
[A,(B \/ C)] in F;
attr F is (DC5) means :Def30: :: ARMSTRNG:def 30
for A, B, C, D being Subset of X st [A,B] in F & [(B \/ C),D] in F holds
[(A \/ C),D] in F;
attr F is (DC6) means :Def31: :: ARMSTRNG:def 31
for A, B, C being Subset of X st [A,B] in F holds
[(A \/ C),B] in F;

end;

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

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

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

theorem :: ARMSTRNG:54

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

theorem :: ARMSTRNG:55

for X being set
for F being Dependency-set of X holds
( F is (F1) & F is (F2) & F is (F3) & F is (F4) iff ( F is (F2) & F is (DC3) & F is (DC4) ) )

proof end;

theorem :: ARMSTRNG:56

for X being set
for F being Dependency-set of X holds
( F is (F1) & F is (F2) & F is (F3) & F is (F4) iff ( F is (F1) & F is (DC5) & F is (DC6) ) )

proof end;

definition

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

end;

:: deftheorem defines charact_set ARMSTRNG:def 32 :

theorem Th57: :: ARMSTRNG:57

for X, A being set
for F being Dependency-set of X st A in charact_set F holds
( A is Subset of X & ex a, b being Subset of X st
( [a,b] in F & a c= A & not b c= A ) )

proof end;

theorem :: ARMSTRNG:58

for X being set
for A being Subset of X
for F being Dependency-set of X st ex a, b being Subset of X st
( [a,b] in F & a c= A & not b c= A ) holds
A in charact_set F ;

theorem Th59: :: ARMSTRNG:59

for X being non empty finite set
for F being Dependency-set of X holds
( ( for A, B being Subset of X holds
( [A,B] in Dependency-closure F iff for a being Subset of X st A c= a & not B c= a holds
a in charact_set F ) ) & saturated-subsets (Dependency-closure F) = (bool X) \ (charact_set F) )

proof end;

theorem :: ARMSTRNG:60

for X being non empty finite set
for F, G being Dependency-set of X st charact_set F = charact_set G holds
Dependency-closure F = Dependency-closure G

proof end;

theorem Th61: :: ARMSTRNG:61

for X being non empty finite set
for F being Dependency-set of X holds charact_set F = charact_set (Dependency-closure F)

proof end;

definition

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

end;

:: deftheorem Def33 defines is_p_i_w_ncv_of ARMSTRNG:def 33 :

theorem :: ARMSTRNG:62

for X being non empty finite set
for F being Dependency-set of X
for K being Subset of X holds
( K in candidate-keys (Dependency-closure F) iff K is_p_i_w_ncv_of F )

proof end;