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


begin

Lm1: now :: thesis: for n being Element of NAT
for X being non empty set
for t being Tuple of n,X holds dom t = Seg n
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 7;
hence dom t = Seg n by FINSEQ_1:def 3; :: thesis: verum
end;

Lm2: now :: thesis: for n being Element of NAT
for X being non empty set
for t being Element of n -tuples_on X holds dom t = Seg n
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 7;
hence dom t = Seg n by FINSEQ_1:def 3; :: thesis: verum
end;

theorem Th1: :: ARMSTRNG:1
for B being set st B is cap-closed 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 for set ;
existence
ex b1 being Relation st
( b1 is reflexive & b1 is antisymmetric & b1 is transitive & not b1 is empty )
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{ F1() -> set , P1[ set ] } :
for X1, X2 being Subset of F1() st ( for y being set holds
( y in X1 iff P1[y] ) ) & ( for y being set holds
( y in X2 iff P1[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 b1 being Subset of X st
for x being set holds
( x in b1 iff x is_maximal_wrt X,R )
proof end;
uniqueness
for b1, b2 being Subset of X st ( for x being set holds
( x in b1 iff x is_maximal_wrt X,R ) ) & ( for x being set holds
( x in b2 iff x is_maximal_wrt X,R ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Maximal_in ARMSTRNG:def 1 :
for X being set
for R being Relation
for b3 being Subset of X holds
( b3 = R Maximal_in X iff for x being set holds
( x in b3 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 b1 being Subset of X st
for x being set holds
( x in b1 iff x is_/\-irreducible_in X )
proof end;
uniqueness
for b1, b2 being Subset of X st ( for x being set holds
( x in b1 iff x is_/\-irreducible_in X ) ) & ( for x being set holds
( x in b2 iff x is_/\-irreducible_in X ) ) holds
b1 = b2
proof end;
end;

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

scheme :: ARMSTRNG:sch 2
FinIntersect{ F1() -> non empty finite set , P1[ set ] } :
for x being set st x in F1() holds
P1[x]
provided
A1: for x being set st x is_/\-irreducible_in F1() holds
P1[x] and
A2: for x, y being set st x in F1() & y in F1() & P1[x] & P1[y] holds
P1[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) for Element of bool (bool X);
existence
ex b1 being Subset-Family of X st
( b1 is (B1) & b1 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 cap-closed 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 V24(X,n -tuples_on D) -> FinSequence-yielding for Element of bool [:X,(n -tuples_on D):];
coherence
for b1 being Function of X,(n -tuples_on D) holds b1 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 b1 being Tuple of n, BOOLEAN st
for i being set st i in Seg n holds
b1 . i = (p /. i) '&' (q /. i)
proof end;
uniqueness
for b1, b2 being Tuple of n, BOOLEAN st ( for i being set st i in Seg n holds
b1 . i = (p /. i) '&' (q /. i) ) & ( for i being set st i in Seg n holds
b2 . i = (p /. i) '&' (q /. i) ) holds
b1 = b2
proof end;
commutativity
for b1, p, q being Tuple of n, BOOLEAN st ( for i being set st i in Seg n holds
b1 . i = (p /. i) '&' (q /. i) ) holds
for i being set st i in Seg n holds
b1 . i = (q /. i) '&' (p /. i) ;
end;

:: deftheorem Def5 defines '&' ARMSTRNG:def 5 :
for n being Element of NAT
for p, q, b4 being Tuple of n, BOOLEAN holds
( b4 = p '&' q iff for i being set st i in Seg n holds
b4 . 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 Th7: :: ARMSTRNG:7
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 c1 is strict ;
struct DB-Rel -> ;
aggr DB-Rel(# Attributes, Domains, Relationship #) -> DB-Rel ;
sel Attributes c1 -> non empty finite set ;
sel Domains c1 -> non-empty ManySortedSet of the Attributes of c1;
sel Relationship c1 -> Subset of (product the Domains of c1);
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 for Element of bool [:(bool X),(bool X):];
existence
ex b1 being Dependency-set of X st
( not b1 is empty & b1 is finite )
proof end;
end;

definition
let X be set ;
func Dependencies X -> Dependency-set of X equals :: ARMSTRNG:def 6
[:(bool X),(bool X):];
coherence
[:(bool X),(bool X):] is Dependency-set of X ;
end;

:: deftheorem defines Dependencies ARMSTRNG:def 6 :
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 b1 being Element of F holds b1 is Dependency of X;
proof end;
end;

theorem Th8: :: ARMSTRNG:8
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 Th9: :: ARMSTRNG:9
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 :Def7: :: ARMSTRNG:def 7
 for f, g being Element of the Relationship of R st f | A = g | A holds
f | B = g | B;
end;

:: deftheorem Def7 defines >|> ARMSTRNG:def 7 :
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 8
 { [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 8 :
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 Th10: :: ARMSTRNG:10
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 :Def9: :: ARMSTRNG:def 9
( 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 Def9 defines >= ARMSTRNG:def 9 :
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 Th11: :: ARMSTRNG:11
for X being set
for P, Q being Dependency of X st P <= Q & Q <= P holds
P = Q
proof end;

theorem Th12: :: ARMSTRNG:12
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 Th13: :: ARMSTRNG:13
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 10
 { [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 10 :
for X being set holds Dependencies-Order X = { [P,Q] where P, Q is Dependency of X : P <= Q } ;

theorem :: ARMSTRNG:14
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 Th15: :: ARMSTRNG:15
for X being set holds dom (Dependencies-Order X) = [:(bool X),(bool X):]
proof end;

theorem Th16: :: ARMSTRNG:16
for X being set holds rng (Dependencies-Order X) = [:(bool X),(bool X):]
proof end;

theorem Th17: :: ARMSTRNG:17
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 Th15, RELAT_1:38;
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 :Def11: :: ARMSTRNG:def 11
 for A being Subset of X holds [A,A] in F;
end;

:: deftheorem Def11 defines (F1) ARMSTRNG:def 11 :
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 Th18: :: ARMSTRNG:18
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 :Def12: :: ARMSTRNG:def 12
 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 :Def13: :: ARMSTRNG:def 13
 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 Def12 defines (F3) ARMSTRNG:def 12 :
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 Def13 defines (F4) ARMSTRNG:def 13 :
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 Th19: :: ARMSTRNG:19
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) for Element of bool [:(bool X),(bool X):];
existence
ex b1 being Dependency-set of X st
( b1 is (F1) & b1 is (F2) & b1 is (F3) & b1 is (F4) & not b1 is empty )
proof end;
end;

definition
let X be set ;
let F be Dependency-set of X;
attr F is full_family means :Def14: :: ARMSTRNG:def 14
( F is (F1) & F is (F2) & F is (F3) & F is (F4) );
end;

:: deftheorem Def14 defines full_family ARMSTRNG:def 14 :
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 for Element of bool [:(bool X),(bool X):];
existence
ex b1 being Dependency-set of X st b1 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:20
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 for Element of bool [:(bool X),(bool X):];
existence
ex b1 being Full-family of X st b1 is finite
proof end;
cluster -> finite for Element of bool [:(bool X),(bool X):];
coherence
for b1 being Dependency-set of X holds b1 is finite ;
end;

registration
let X be set ;
cluster full_family -> (F2) (F1) (F3) (F4) for Element of bool [:(bool X),(bool X):];
coherence
for b1 being Dependency-set of X st b1 is full_family holds
( b1 is (F1) & b1 is (F2) & b1 is (F3) & b1 is (F4) ) by Def14;
cluster (F2) (F1) (F3) (F4) -> full_family for Element of bool [:(bool X),(bool X):];
correctness
coherence
for b1 being Dependency-set of X st b1 is (F1) & b1 is (F2) & b1 is (F3) & b1 is (F4) holds
b1 is full_family ;
by Def14;
end;

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

:: deftheorem Def15 defines (DC3) ARMSTRNG:def 15 :
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) for Element of bool [:(bool X),(bool X):];
coherence
for b1 being Dependency-set of X st b1 is (F1) & b1 is (F3) holds
b1 is (DC3)
proof end;
cluster (F2) (DC3) -> (F1) (F3) for Element of bool [:(bool X),(bool X):];
coherence
for b1 being Dependency-set of X st b1 is (DC3) & b1 is (F2) holds
( b1 is (F1) & b1 is (F3) )
proof end;
end;

registration
let X be set ;
cluster non empty Relation-like bool X -defined bool X -valued (F2) (F4) (DC3) for Element of bool [:(bool X),(bool X):];
existence
ex b1 being Dependency-set of X st
( b1 is (DC3) & b1 is (F2) & b1 is (F4) & not b1 is empty )
proof end;
end;

theorem :: ARMSTRNG:21
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:22
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 for Element of bool [:(bool X),(bool X):];
coherence
for b1 being Dependency-set of X st b1 is (F1) holds
not b1 is empty by Def11;
end;

theorem Th23: :: ARMSTRNG:23
for R being DB-Rel holds Dependency-str R is full_family
proof end;

theorem :: ARMSTRNG:24
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 16
(Dependencies-Order X) Maximal_in F;
coherence
(Dependencies-Order X) Maximal_in F is Dependency-set of X by RELSET_1:1;
end;

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

theorem :: ARMSTRNG:25
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 :Def17: :: ARMSTRNG:def 17
[x,y] in Maximal_wrt F;
end;

:: deftheorem Def17 defines ^|^ ARMSTRNG:def 17 :
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 Th26: :: ARMSTRNG:26
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 Th27: :: ARMSTRNG:27
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 :Def18: :: ARMSTRNG:def 18
 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 :Def19: :: ARMSTRNG:def 19
 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 :Def20: :: ARMSTRNG:def 20
 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 Def18 defines (M1) ARMSTRNG:def 18 :
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 Def19 defines (M2) ARMSTRNG:def 19 :
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 Def20 defines (M3) ARMSTRNG:def 20 :
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 Th28: :: ARMSTRNG:28
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 Th29: :: ARMSTRNG:29
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 Th30: :: ARMSTRNG:30
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 21
 { 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 21 :
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 Th31: :: ARMSTRNG:31
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 Th32: :: ARMSTRNG:32
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 22
 { [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 22 :
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 Th33: :: ARMSTRNG:33
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 Th34: :: ARMSTRNG:34
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 Th35: :: ARMSTRNG:35
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 23
 { 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 23 :
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 Th36: :: ARMSTRNG:36
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 Th37: :: ARMSTRNG:37
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 :Def24: :: ARMSTRNG:def 24
( F c= it & ( for G being Dependency-set of X st F c= G & G is full_family holds
it c= G ) );
existence
ex b1 being Full-family of X st
( F c= b1 & ( for G being Dependency-set of X st F c= G & G is full_family holds
b1 c= G ) )
proof end;
correctness
uniqueness
for b1, b2 being Full-family of X st F c= b1 & ( for G being Dependency-set of X st F c= G & G is full_family holds
b1 c= G ) & F c= b2 & ( for G being Dependency-set of X st F c= G & G is full_family holds
b2 c= G ) holds
b1 = b2;
proof end;
end;

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

theorem Th38: :: ARMSTRNG:38
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 Th39: :: ARMSTRNG:39
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:40
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:41
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 :Def25: :: ARMSTRNG:def 25
( G c= B & B = { (Intersect S) where S is Subset-Family of X : S c= G } );
end;

:: deftheorem Def25 defines is_generator-set_of ARMSTRNG:def 25 :
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:42
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 Th43: :: ARMSTRNG:43
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;

:: WWA did not show what generators B are,
:: they are the irreducible elements \ X
theorem :: ARMSTRNG:44
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:45
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:46
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 26
 { 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 26 :
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:47
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 :Def27: :: ARMSTRNG:def 27
 for x, y being set st x in X & y in X & x c= y holds
x = y;
end;

:: deftheorem Def27 defines without_proper_subsets ARMSTRNG:def 27 :
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:48
for R being DB-Rel holds
( candidate-keys (Dependency-str R) is (C1) & candidate-keys (Dependency-str R) is (C2) )
proof end;

theorem :: ARMSTRNG:49
for X being finite set
for C being Subset-Family of X st C is (C1) & C is (C2) holds
ex F being Full-family of X st C = candidate-keys F
proof end;

theorem :: ARMSTRNG:50
for X being finite set
for C being Subset-Family of X
for B being set st C is (C1) & C is (C2) & 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:51
for X being non empty finite set
for C being Subset-Family of X st C is (C1) & C is (C2) 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 :Def28: :: ARMSTRNG:def 28
 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 :Def29: :: ARMSTRNG:def 29
 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 :Def30: :: ARMSTRNG:def 30
 for A, B, C being Subset of X st [A,B] in F holds
[(A \/ C),B] in F;
end;

:: deftheorem Def28 defines (DC4) ARMSTRNG:def 28 :
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 Def29 defines (DC5) ARMSTRNG:def 29 :
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 Def30 defines (DC6) ARMSTRNG:def 30 :
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:52
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:53
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 (DC1) & F is (DC3) & F is (DC4) ) )
proof end;

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 (DC2) & 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 31
 { 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 31 :
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 Th55: :: ARMSTRNG:55
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:56
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 Th57: :: ARMSTRNG:57
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:58
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 Th59: :: ARMSTRNG:59
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 :Def32: :: ARMSTRNG:def 32
( ( 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 Def32 defines is_p_i_w_ncv_of ARMSTRNG:def 32 :
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:60
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;