:: 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
proofend;

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

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] ) ) &amp; ( for y being set holds
( y in X2 iff P1[y] ) ) holds
X1 = X2
proofend;

definition
let X be set ;
let R be Relation;
funcR 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 )
proofend;
uniqueness
 for b1, b2 being Subset of X st ( for x being set holds
( x in b1 iff x is_maximal_wrt X,R ) ) &amp; ( for x being set holds
( x in b2 iff x is_maximal_wrt X,R ) ) holds
b1 = b2
proofend;
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 ;
predx is_/\-irreducible_in X means :Def2: :: ARMSTRNG:def 2
( x in X &amp; ( for z, y being set st z in X &amp; y in X &amp; x = z /\ y &amp; 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 &amp; ( for z, y being set st z in X &amp; y in X &amp; x = z /\ y &amp; 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 )
proofend;
uniqueness
 for b1, b2 being Subset of X st ( for x being set holds
( x in b1 iff x is_/\-irreducible_in X ) ) &amp; ( for x being set holds
( x in b2 iff x is_/\-irreducible_in X ) ) holds
b1 = b2
proofend;
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() &amp; y in F1() &amp; P1[x] &amp; P1[y] holds
P1[x /\ y]
proofend;

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 &amp; ( for s being set st s in A holds
s is_/\-irreducible_in X ) )
proofend;

definition
let X be set ;
let B be Subset-Family of X;
attrB 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) &amp; b1 is (B2) )
proofend;
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 &amp; x <> X holds
for S being finite Subset-Family of X st S c= B &amp; x = Intersect S holds
x in S
proofend;

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
proofend;
end;

registration
let f be FinSequence-yielding Function;
let x be set ;
clusterf . x ->  FinSequence-like ;
coherence
 f . x is FinSequence-like
proofend;
end;

definition
let n be Element of NAT ;
let p, q be Tuple of n, BOOLEAN ;
funcp '&amp;' q ->  Tuple of n, BOOLEAN  means :Def5: :: ARMSTRNG:def 5
 for i being set st i in Seg n holds
it . i = (p /. i) '&amp;' (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) '&amp;' (q /. i)
proofend;
uniqueness
 for b1, b2 being Tuple of n, BOOLEAN st ( for i being set st i in Seg n holds
b1 . i = (p /. i) '&amp;' (q /. i) ) &amp; ( for i being set st i in Seg n holds
b2 . i = (p /. i) '&amp;' (q /. i) ) holds
b1 = b2
proofend;
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) '&amp;' (q /. i) ) holds
for i being set st i in Seg n holds
b1 . i = (q /. i) '&amp;' (p /. i) ;
end;

:: deftheorem Def5 defines '&amp;' ARMSTRNG:def_5_:_
 for n being Element of NAT
for p, q, b4 being Tuple of n, BOOLEAN holds
( b4 = p '&amp;' q iff for i being set st i in Seg n holds
b4 . i = (p /. i) '&amp;' (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) '&amp;' p = n -BinarySequence 0
proofend;

theorem :: ARMSTRNG:6
for n being Element of NAT
for p being Tuple of n, BOOLEAN holds ('not' (n -BinarySequence 0)) '&amp;' p = p
proofend;

theorem Th7: :: ARMSTRNG:7
for n, i being Element of NAT st i < n holds
( (n -BinarySequence (2 to_power i)) . (i + 1) = 1 &amp; ( for j being Element of NAT st j in Seg n &amp; j <> i + 1 holds
(n -BinarySequence (2 to_power i)) . j = 0 ) )
proofend;

begin

definition
attrc1 is strict ;
struct DB-Rel  -> ;
aggrDB-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 &amp; b1 is finite )
proofend;
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;
proofend;
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] )
proofend;

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]
proofend;

definition
let R be DB-Rel ;
let A, B be Subset of the Attributes of R;
predA >|> 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
proofend;
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 )
proofend;

begin

definition
let X be set ;
let P, Q be Dependency of X;
predP >= Q means :Def9: :: ARMSTRNG:def 9
( P `1 c= Q `1 &amp; Q `2 c= P `2 );
reflexivity
 for P being Dependency of X holds
( P `1 c= P `1 &amp; 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 &amp; 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 &amp; Q <= P holds
P = Q
proofend;

theorem Th12: :: ARMSTRNG:12
for X being set
for P, Q, S being Dependency of X st P <= Q &amp; Q <= S holds
P <= S
proofend;

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 &amp; B9 c= B ) )
proofend;

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)
proofend;
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] &amp; P <= Q ) ) ;

theorem Th15: :: ARMSTRNG:15
for X being set holds dom (Dependencies-Order X) = [:(bool X),(bool X):]
proofend;

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

theorem Th17: :: ARMSTRNG:17
for X being set holds field (Dependencies-Order X) = [:(bool X),(bool X):]
proofend;

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 &amp; Dependencies-Order X is reflexive &amp; Dependencies-Order X is antisymmetric &amp; Dependencies-Order X is (F2) )
proofend;
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;
attrF 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 &amp; [B,C] in F holds
[A,C] in F )
proofend;

definition
let X be set ;
let F be Dependency-set of X;
attrF is (F3)  means :Def12: :: ARMSTRNG:def 12
 for A, B, A9, B9 being Subset of X st [A,B] in F &amp; [A,B] >= [A9,B9] holds
[A9,B9] in F;
attrF is (F4)  means :Def13: :: ARMSTRNG:def 13
 for A, B, A9, B9 being Subset of X st [A,B] in F &amp; [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 &amp; [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 &amp; [A9,B9] in F holds
[(A \/ A9),(B \/ B9)] in F );

theorem Th19: :: ARMSTRNG:19
for X being set holds
( Dependencies X is (F1) &amp; Dependencies X is (F2) &amp; Dependencies X is (F3) &amp; Dependencies X is (F4) )
proofend;

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) &amp; b1 is (F2) &amp; b1 is (F3) &amp; b1 is (F4) &amp; not b1 is empty )
proofend;
end;

definition
let X be set ;
let F be Dependency-set of X;
attrF is full_family  means :Def14: :: ARMSTRNG:def 14
( F is (F1) &amp; F is (F2) &amp; F is (F3) &amp; 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) &amp; F is (F2) &amp; F is (F3) &amp; 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
proofend;
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
proofend;
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) &amp; b1 is (F2) &amp; b1 is (F3) &amp; 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) &amp; b1 is (F2) &amp; b1 is (F3) &amp; b1 is (F4) holds
b1 is full_family ;
by Def14;
end;

definition
let X be set ;
let F be Dependency-set of X;
attrF 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) &amp; b1 is (F3) holds
b1 is (DC3)
proofend;
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) &amp; b1 is (F2) holds
( b1 is (F1) &amp; b1 is (F3) )
proofend;
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) &amp; b1 is (F2) &amp; b1 is (F4) &amp; not b1 is empty )
proofend;
end;

theorem :: ARMSTRNG:21
for X being set
for F being Dependency-set of X st F is (DC3) &amp; F is (F2) holds
( F is (F1) &amp; F is (F3) ) ;

theorem :: ARMSTRNG:22
for X being set
for F being Dependency-set of X st F is (F1) &amp; 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
proofend;

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

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 ;
predx ^|^ 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 &amp; [A,B] >= P )
proofend;

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

definition
let X be set ;
let M be Dependency-set of X;
attrM 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] &amp; [A9,B9] in M );
attrM is (M2)  means :Def19: :: ARMSTRNG:def 19
 for A, B, A9, B9 being Subset of X st [A,B] in M &amp; [A9,B9] in M &amp; [A,B] >= [A9,B9] holds
( A = A9 &amp; B = B9 );
attrM is (M3)  means :Def20: :: ARMSTRNG:def 20
 for A, B, A9, B9 being Subset of X st [A,B] in M &amp; [A9,B9] in M &amp; 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] &amp; [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 &amp; [A9,B9] in M &amp; [A,B] >= [A9,B9] holds
( A = A9 &amp; 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 &amp; [A9,B9] in M &amp; 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) &amp; Maximal_wrt F is (M2) &amp; Maximal_wrt F is (M3) )
proofend;

theorem Th29: :: ARMSTRNG:29
for X being finite set
for M, F being Dependency-set of X st M is (M1) &amp; M is (M2) &amp; M is (M3) &amp; F =  {  [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] &amp; [A9,B9] in M )  }  holds
( M = Maximal_wrt F &amp; F is full_family &amp; ( for G being Full-family of X st M = Maximal_wrt G holds
G = F ) )
proofend;

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

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
proofend;
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
proofend;
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 &amp; A ^|^ B,F ) )
proofend;

theorem Th32: :: ARMSTRNG:32
for X being non empty finite set
for F being Full-family of X holds
( saturated-subsets F is (B1) &amp; saturated-subsets F is (B2) )
proofend;

definition
let X, B be set ;
funcX 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 &amp; 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 &amp; a c= c holds
b c= c  }  is Dependency-set of X
proofend;
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 &amp; 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
proofend;

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

theorem Th35: :: ARMSTRNG:35
for X being non empty finite set
for B being Subset-Family of X st B is (B1) &amp; B is (B2) holds
( B = saturated-subsets (X deps_encl_by B) &amp; ( for G being Full-family of X st B = saturated-subsets G holds
G = X deps_encl_by B ) )
proofend;

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 &amp; 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 &amp; A c= b holds
B c= b  }  is Subset-Family of X
proofend;
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 &amp; 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) &amp; enclosure_of F is (B2) )
proofend;

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) &amp; ( for G being Dependency-set of X st F c= G &amp; G is full_family holds
X deps_encl_by (enclosure_of F) c= G ) )
proofend;

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 &amp; ( for G being Dependency-set of X st F c= G &amp; G is full_family holds
it c= G ) );
existence
 ex b1 being Full-family of X st
( F c= b1 &amp; ( for G being Dependency-set of X st F c= G &amp; G is full_family holds
b1 c= G ) )
proofend;
correctness
uniqueness
for b1, b2 being Full-family of X st F c= b1 &amp; ( for G being Dependency-set of X st F c= G &amp; G is full_family holds
b1 c= G ) &amp; F c= b2 &amp; ( for G being Dependency-set of X st F c= G &amp; G is full_family holds
b2 c= G ) holds
b1 = b2;
proofend;
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 &amp; ( for G being Dependency-set of X st F c= G &amp; 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)
proofend;

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) &amp; B is (B2) )
proofend;

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

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

definition
let X, G be set ;
let B be Subset-Family of X;
predG is_generator-set_of B means :Def25: :: ARMSTRNG:def 25
( G c= B &amp; 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 &amp; 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)
proofend;

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 &amp; F = X deps_encl_by G )
proofend;

:: 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) &amp; B is (B2) holds
/\-IRR B is_generator-set_of B
proofend;

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

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 &amp; ( for a being Element of X holds the Domains of R . a = INT ) &amp; F = Dependency-str R )
proofend;

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 &amp; 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 &amp; x c= c holds
y c= c )
proofend;

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
proofend;
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}
proofend;

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

definition
let X be set ;
attrX is without_proper_subsets  means :Def27: :: ARMSTRNG:def 27
 for x, y being set st x in X &amp; y in X &amp; 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 &amp; y in X &amp; 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) &amp; candidate-keys (Dependency-str R) is (C2) )
proofend;

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

theorem :: ARMSTRNG:50
for X being finite set
for C being Subset-Family of X
for B being set st C is (C1) &amp; C is (C2) &amp; 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)
proofend;

theorem :: ARMSTRNG:51
for X being non empty finite set
for C being Subset-Family of X st C is (C1) &amp; C is (C2) holds
ex R being DB-Rel st
( the Attributes of R = X &amp; C = candidate-keys (Dependency-str R) )
proofend;

begin

definition
let X be set ;
let F be Dependency-set of X;
attrF is (DC4)  means :Def28: :: ARMSTRNG:def 28
 for A, B, C being Subset of X st [A,B] in F &amp; [A,C] in F holds
[A,(B \/ C)] in F;
attrF is (DC5)  means :Def29: :: ARMSTRNG:def 29
 for A, B, C, D being Subset of X st [A,B] in F &amp; [(B \/ C),D] in F holds
[(A \/ C),D] in F;
attrF 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 &amp; [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 &amp; [(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) &amp; F is (F2) &amp; F is (F3) &amp; F is (F4) iff ( F is (F2) &amp; F is (DC3) &amp; F is (F4) ) ) ;

theorem :: ARMSTRNG:53
for X being set
for F being Dependency-set of X holds
( F is (F1) &amp; F is (F2) &amp; F is (F3) &amp; F is (F4) iff ( F is (DC1) &amp; F is (DC3) &amp; F is (DC4) ) )
proofend;

theorem :: ARMSTRNG:54
for X being set
for F being Dependency-set of X holds
( F is (F1) &amp; F is (F2) &amp; F is (F3) &amp; F is (F4) iff ( F is (DC2) &amp; F is (DC5) &amp; F is (DC6) ) )
proofend;

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 &amp; a c= A &amp; 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 &amp; a c= A &amp; 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 &amp; a c= A &amp; 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 &amp; ex a, b being Subset of X st
( [a,b] in F &amp; a c= A &amp; not b c= A ) )
proofend;

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 &amp; a c= A &amp; 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 &amp; not B c= a holds
a in charact_set F ) ) &amp; saturated-subsets (Dependency-closure F) = (bool X) \ (charact_set F) )
proofend;

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

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

definition
let A, K be set ;
let F be Dependency-set of A;
predK is_p_i_w_ncv_of F means :Def32: :: ARMSTRNG:def 32
( ( for a being Subset of A st K c= a &amp; a <> A holds
a in charact_set F ) &amp; ( for k being set st k c< K holds
ex a being Subset of A st
( k c= a &amp; a <> A &amp; 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 &amp; a <> A holds
a in charact_set F ) &amp; ( for k being set st k c< K holds
ex a being Subset of A st
( k c= a &amp; a <> A &amp; 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 )
proofend;