:: Armstrong's Axioms
:: by William W. Armstrong , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received October 25, 2002
:: Copyright (c) 2002-2011 Association of Mizar Users

begin

Lm1: now

let n be Element of NAT ; :: thesis: for X being non empty set
for t being Tuple of n,X holds dom t = Seg n
let X be non empty set ; :: thesis: for t being Tuple of n,X holds dom t = Seg n
let t be Tuple of n,X; :: thesis: dom t = Seg n
len t = n by CARD_1:def 13;
hence dom t = Seg n by FINSEQ_1:def 3; :: thesis: verum

end;

Lm2: now

let n be Element of NAT ; :: thesis: for X being non empty set
for t being Element of n -tuples_on X holds dom t = Seg n
let X be non empty set ; :: thesis: for t being Element of n -tuples_on X holds dom t = Seg n
let t be Element of n -tuples_on X; :: thesis: dom t = Seg n
len t = n by CARD_1:def 13;
hence dom t = Seg n by FINSEQ_1:def 3; :: thesis: verum

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 Relation-like reflexive antisymmetric transitive set ;
existence
ex b₁ being Relation st
( b₁ is reflexive & b₁ is antisymmetric & b₁ is (F2) & b₁ is (C1) )

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
ex b₁ being Subset of X st
for x being set holds
( x in b₁ iff x is_maximal_wrt X,R )

proof end;

uniqueness
for b₁, b₂ being Subset of X st ( for x being set holds
( x in b₁ iff x is_maximal_wrt X,R ) ) & ( for x being set holds
( x in b₂ iff x is_maximal_wrt X,R ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Maximal_in ARMSTRNG:def 1 :
for X being set
for R being Relation
for b₃ being Subset of X holds
( b₃ = R Maximal_in X iff for x being set holds
( x in b₃ iff x is_maximal_wrt X,R ) );

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 :
for x, X being set holds
( x is_/\-irreducible_in X iff ( x in X & ( for z, y being set st z in X & y in X & x = z /\ y & not x = z holds
x = y ) ) );

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
ex b₁ being Subset of X st
for x being set holds
( x in b₁ iff x is_/\-irreducible_in X )

proof end;

uniqueness
for b₁, b₂ being Subset of X st ( for x being set holds
( x in b₁ iff x is_/\-irreducible_in X ) ) & ( for x being set holds
( x in b₂ iff x is_/\-irreducible_in X ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines /\-IRR ARMSTRNG:def 3 :
for X being non empty set
for b₂ being Subset of X holds
( b₂ = /\-IRR X iff for x being set holds
( x in b₂ iff x is_/\-irreducible_in X ) );

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 :
for X being set
for B being Subset-Family of X holds
( B is (B1) iff X in B );

notation

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

end;

registration

let X be set ;
cluster (B2) (B1) Element of bool (bool X);
existence
ex b₁ being Subset-Family of X st
( b₁ is (B1) & b₁ is (B2) )

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 Element of NAT ;
cluster Function-like V21(X,n -tuples_on D) -> FinSequence-yielding Element of bool [:X,(n -tuples_on D):];
coherence
for b₁ being Function of X,(n -tuples_on D) holds b₁ is FinSequence-yielding

proof end;

end;

registration

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

proof end;

end;

definition

let n be Element of 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
ex b₁ being Tuple of n, BOOLEAN st
for i being set st i in Seg n holds
b₁ . i = (p /. i) '&' (q /. i)

proof end;

uniqueness
for b₁, b₂ being Tuple of n, BOOLEAN st ( for i being set st i in Seg n holds
b₁ . i = (p /. i) '&' (q /. i) ) & ( for i being set st i in Seg n holds
b₂ . i = (p /. i) '&' (q /. i) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, p, q being Tuple of n, BOOLEAN st ( for i being set st i in Seg n holds
b₁ . i = (p /. i) '&' (q /. i) ) holds
for i being set st i in Seg n holds
b₁ . i = (q /. i) '&' (p /. i) ;

end;

:: deftheorem Def5 defines '&' ARMSTRNG:def 5 :
for n being Element of NAT
for p, q, b₄ being Tuple of n, BOOLEAN holds
( b₄ = p '&' q iff for i being set st i in Seg n holds
b₄ . i = (p /. i) '&' (q /. i) );

theorem Th5: :: ARMSTRNG:5

for n being Element of NAT
for p being Element of n -tuples_on BOOLEAN holds (n -BinarySequence 0) '&' p = n -BinarySequence 0

proof end;

theorem :: ARMSTRNG:6

for n being Element of 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 Element of NAT st i < n holds
( (n -BinarySequence (2 to_power i)) . (i + 1) = 1 & ( for j being Element of NAT st j in Seg n & j <> i + 1 holds
(n -BinarySequence (2 to_power i)) . j = 0 ) )

proof end;

begin

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

end;

begin

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 Relation-like bool X -defined bool X -valued finite Element of bool [:(bool X),(bool X):];
existence
ex b₁ being Dependency-set of X st
( b₁ is (C1) & b₁ is finite )

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
[:(bool X),(bool X):] is Dependency-set of X

proof end;

end;

:: deftheorem ARMSTRNG:def 6 :
canceled;

:: deftheorem defines Dependencies ARMSTRNG:def 7 :
for X being set holds Dependencies X = [:(bool X),(bool X):];

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
Dependencies X is (C1) ;

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
coherence
for b₁ being Element of F holds b₁ is Dependency of X;

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 :
for R being DB-Rel
for A, B being Subset of the Attributes of R holds
( A >|> B,R iff for f, g being Element of the Relationship of R st f | A = g | A holds
f | B = g | B );

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
{ [A,B] where A, B is Subset of the Attributes of R : A >|> B,R } is Dependency-set of the Attributes of R

proof end;

end;

:: deftheorem defines Dependency-str ARMSTRNG:def 9 :
for R being DB-Rel holds Dependency-str R = { [A,B] where A, B is Subset of the Attributes of R : A >|> B,R } ;

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;

begin

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
for P being Dependency of X holds
( P `1 c= P `1 & P `2 c= P `2 ) ;

end;

:: deftheorem Def10 defines >= ARMSTRNG:def 10 :
for X being set
for P, Q being Dependency of X holds
( P >= Q iff ( P `1 c= Q `1 & Q `2 c= P `2 ) );

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
[A,B] is Dependency of X by ZFMISC_1:def 2;

end;

theorem Th15: :: ARMSTRNG:15

for X being set
for A, B, A9, B9 being Subset of X holds
( [A,B] >= [A9,B9] iff ( A c= A9 & B9 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
{ [P,Q] where P, Q is Dependency of X : P <= Q } is Relation of (Dependencies X)

proof end;

end;

:: deftheorem defines Dependencies-Order ARMSTRNG:def 11 :
for X being set holds Dependencies-Order X = { [P,Q] where P, Q is Dependency of X : P <= Q } ;

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
Dependencies-Order X is (C1) by Th17, RELAT_1:60;
cluster Dependencies-Order X -> total reflexive antisymmetric transitive ;
coherence
( Dependencies-Order X is total & Dependencies-Order X is reflexive & Dependencies-Order X is antisymmetric & Dependencies-Order X is (F2) )

proof end;

end;

notation

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

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 :
for X being set
for F being Dependency-set of X holds
( F is (F1) iff for A being Subset of X holds [A,A] in F );

notation

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

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, A9, B9 being Subset of X st [A,B] in F & [A,B] >= [A9,B9] holds
[A9,B9] in F;
attr F is (F4) means :Def14: :: ARMSTRNG:def 14
for A, B, A9, B9 being Subset of X st [A,B] in F & [A9,B9] in F holds
[(A \/ A9),(B \/ B9)] in F;

end;

:: deftheorem Def13 defines (F3) ARMSTRNG:def 13 :
for X being set
for F being Dependency-set of X holds
( F is (F3) iff for A, B, A9, B9 being Subset of X st [A,B] in F & [A,B] >= [A9,B9] holds
[A9,B9] in F );

:: deftheorem Def14 defines (F4) ARMSTRNG:def 14 :
for X being set
for F being Dependency-set of X holds
( F is (F4) iff for A, B, A9, B9 being Subset of X st [A,B] in F & [A9,B9] in F holds
[(A \/ A9),(B \/ B9)] in F );

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 Relation-like bool X -defined bool X -valued (F2) (F1) (F3) (F4) Element of bool [:(bool X),(bool X):];
existence
ex b₁ being Dependency-set of X st
( b₁ is (F1) & b₁ is (F2) & b₁ is (F3) & b₁ is (F4) & b₁ is (C1) )

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 :
for X being set
for F being Dependency-set of X holds
( F is full_family iff ( F is (F1) & F is (F2) & F is (F3) & F is (F4) ) );

registration

let X be set ;
cluster Relation-like bool X -defined bool X -valued full_family Element of bool [:(bool X),(bool X):];
existence
ex b₁ being Dependency-set of X st b₁ is full_family

proof end;

end;

definition

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

end;

theorem :: ARMSTRNG:22

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

registration

let X be finite set ;
cluster Relation-like bool X -defined bool X -valued finite countable full_family Element of bool [:(bool X),(bool X):];
existence
ex b₁ being Full-family of X st b₁ is finite

proof end;

cluster -> finite Element of bool [:(bool X),(bool X):];
coherence
for b₁ being Dependency-set of X holds b₁ is finite ;

end;

registration

let X be set ;
cluster full_family -> (F2) (F1) (F3) (F4) Element of bool [:(bool X),(bool X):];
coherence
for b₁ being Dependency-set of X st b₁ is full_family holds
( b₁ is (F1) & b₁ is (F2) & b₁ is (F3) & b₁ is (F4) ) by Def15;
cluster (F2) (F1) (F3) (F4) -> full_family Element of bool [:(bool X),(bool X):];
correctness
coherence
for b₁ being Dependency-set of X st b₁ is (F1) & b₁ is (F2) & b₁ is (F3) & b₁ is (F4) holds
b₁ is full_family ;
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 :
for X being set
for F being Dependency-set of X holds
( F is (DC3) iff for A, B being Subset of X st B c= A holds
[A,B] in F );

registration

let X be set ;
cluster (F1) (F3) -> (DC3) Element of bool [:(bool X),(bool X):];
coherence
for b₁ being Dependency-set of X st b₁ is (F1) & b₁ is (F3) holds
b₁ is (DC3)

proof end;

cluster (F2) (DC3) -> (F1) (F3) Element of bool [:(bool X),(bool X):];
coherence
for b₁ being Dependency-set of X st b₁ is (DC3) & b₁ is (F2) holds
( b₁ is (F1) & b₁ is (F3) )

proof end;

end;

registration

let X be set ;
cluster non empty Relation-like bool X -defined bool X -valued (F2) (F4) (DC3) Element of bool [:(bool X),(bool X):];
existence
ex b₁ being Dependency-set of X st
( b₁ is (DC3) & b₁ is (F2) & b₁ is (F4) & b₁ is (C1) )

proof end;

end;

theorem :: 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) ) ;

theorem :: ARMSTRNG:24

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

registration

let X be set ;
cluster (F1) -> non empty Element of bool [:(bool X),(bool X):];
coherence
for b₁ being Dependency-set of X st b₁ is (F1) holds
b₁ is (C1) 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;

begin

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
(Dependencies-Order X) Maximal_in F is Dependency-set of X by RELSET_1:4;

end;

:: deftheorem defines Maximal_wrt ARMSTRNG:def 17 :
for X being set
for F being Dependency-set of X holds Maximal_wrt F = (Dependencies-Order X) Maximal_in F;

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 :
for X being set
for F being Dependency-set of X
for x, y being set holds
( x ^|^ y,F iff [x,y] in Maximal_wrt F );

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 A9, B9 being Subset of X holds
( not [A9,B9] in F or ( not A <> A9 & not B <> B9 ) or not [A,B] <= [A9,B9] ) ) ) )

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 A9, B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M );
attr M is (M2) means :Def20: :: ARMSTRNG:def 20
for A, B, A9, B9 being Subset of X st [A,B] in M & [A9,B9] in M & [A,B] >= [A9,B9] holds
( A = A9 & B = B9 );
attr M is (M3) means :Def21: :: ARMSTRNG:def 21
for A, B, A9, B9 being Subset of X st [A,B] in M & [A9,B9] in M & A9 c= B holds
B9 c= B;

end;

:: deftheorem Def19 defines (M1) ARMSTRNG:def 19 :
for X being set
for M being Dependency-set of X holds
( M is (M1) iff for A being Subset of X ex A9, B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M ) );

:: deftheorem Def20 defines (M2) ARMSTRNG:def 20 :
for X being set
for M being Dependency-set of X holds
( M is (M2) iff for A, B, A9, B9 being Subset of X st [A,B] in M & [A9,B9] in M & [A,B] >= [A9,B9] holds
( A = A9 & B = B9 ) );

:: deftheorem Def21 defines (M3) ARMSTRNG:def 21 :
for X being set
for M being Dependency-set of X holds
( M is (M3) iff for A, B, A9, B9 being Subset of X st [A,B] in M & [A9,B9] in M & A9 c= B holds
B9 c= B );

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 A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] 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 ;
coherence
Maximal_wrt F is (C1)

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;

begin

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
{ B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } is Subset-Family of X

proof end;

end;

:: deftheorem defines saturated-subsets ARMSTRNG:def 22 :
for X being set
for F being Dependency-set of X holds saturated-subsets F = { B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } ;

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
saturated-subsets F is finite

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
{ [a,b] where a, b is Subset of X : for c being set st c in B & a c= c holds
b c= c } is Dependency-set of X

proof end;

end;

:: deftheorem defines deps_encl_by ARMSTRNG:def 23 :
for X, B being set holds X deps_encl_by B = { [a,b] where a, b is Subset of X : for c being set st c in B & a c= c holds
b c= c } ;

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
{ 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 } is Subset-Family of X

proof end;

end;

:: deftheorem defines enclosure_of ARMSTRNG:def 24 :
for X being set
for F being Dependency-set of X holds enclosure_of F = { 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 } ;

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
ex b₁ being Full-family of X st
( F c= b₁ & ( for G being Dependency-set of X st F c= G & G is full_family holds
b₁ c= G ) )

proof end;

correctness
uniqueness
for b₁, b₂ being Full-family of X st F c= b₁ & ( for G being Dependency-set of X st F c= G & G is full_family holds
b₁ c= G ) & F c= b₂ & ( for G being Dependency-set of X st F c= G & G is full_family holds
b₂ c= G ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def25 defines Dependency-closure ARMSTRNG:def 25 :
for X being non empty finite set
for F being Dependency-set of X
for b₃ being Full-family of X holds
( b₃ = Dependency-closure F iff ( F c= b₃ & ( for G being Dependency-set of X st F c= G & G is full_family holds
b₃ c= G ) ) );

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 :
for X, G being set
for B being Subset-Family of X holds
( G is_generator-set_of B iff ( G c= B & B = { (Intersect S) where S is Subset-Family of X : S c= G } ) );

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;

begin

definition

let n be Element of NAT ;
let D be non empty set ;
mode Tuple of n,D is Element of n -tuples_on D;

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;

begin

Lm3: 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
{ A where A is Subset of X : [A,X] in Maximal_wrt F } is Subset-Family of X

proof end;

end;

:: deftheorem defines candidate-keys ARMSTRNG:def 27 :
for X being set
for F being Dependency-set of X holds candidate-keys F = { A where A is Subset of X : [A,X] in Maximal_wrt F } ;

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 ;

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 :
for X being set holds
( X is without_proper_subsets iff for x, y being set st x in X & y in X & x c= y holds
x = y );

notation

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

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;

begin

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 :
for X being set
for F being Dependency-set of X holds
( F is (DC4) iff for A, B, C being Subset of X st [A,B] in F & [A,C] in F holds
[A,(B \/ C)] in F );

:: deftheorem Def30 defines (DC5) ARMSTRNG:def 30 :
for X being set
for F being Dependency-set of X holds
( F is (DC5) iff 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 );

:: deftheorem Def31 defines (DC6) ARMSTRNG:def 31 :
for X being set
for F being Dependency-set of X holds
( F is (DC6) iff for A, B, C being Subset of X st [A,B] in F holds
[(A \/ C),B] in F );

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) ) ) ;

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
coherence
{ 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 ) } is set ;
;

end;

:: deftheorem defines charact_set ARMSTRNG:def 32 :
for X being set
for F being Dependency-set of X holds charact_set F = { 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 ) } ;

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 :
for A, K being set
for F being Dependency-set of A holds
( K is_p_i_w_ncv_of F iff ( ( 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 ) ) ) );

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;