:: by William W. Armstrong , Yatsuka Nakamura and Piotr Rudnicki

::

:: Received October 25, 2002

:: Copyright (c) 2002-2019 Association of Mizar Users

Lm1: now :: thesis: for n being Nat

for X being non empty set

for t being Tuple of n,X holds dom t = Seg n

for X being non empty set

for t being Tuple of n,X holds dom t = Seg n

let n be 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;
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

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

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

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

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

existence

ex b_{1} being Relation st

( b_{1} is reflexive & b_{1} is antisymmetric & b_{1} is transitive & not b_{1} is empty )

end;
ex b

( b

proof 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

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;

definition

let X be set ;

let R be Relation;

defpred S_{1}[ object ] means $1 is_maximal_wrt X,R;

ex b_{1} being Subset of X st

for x being object holds

( x in b_{1} iff x is_maximal_wrt X,R )

for b_{1}, b_{2} being Subset of X st ( for x being object holds

( x in b_{1} iff x is_maximal_wrt X,R ) ) & ( for x being object holds

( x in b_{2} iff x is_maximal_wrt X,R ) ) holds

b_{1} = b_{2}

end;
let R be Relation;

defpred S

func R Maximal_in X -> Subset of X means :Def1: :: ARMSTRNG:def 1

for x being object holds

( x in it iff x is_maximal_wrt X,R );

existence for x being object holds

( x in it iff x is_maximal_wrt X,R );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines Maximal_in ARMSTRNG:def 1 :

for X being set

for R being Relation

for b_{3} being Subset of X holds

( b_{3} = R Maximal_in X iff for x being object holds

( x in b_{3} iff x is_maximal_wrt X,R ) );

for X being set

for R being Relation

for b

( b

( x in b

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

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

definition

let X be non empty set ;

ex b_{1} being Subset of X st

for x being set holds

( x in b_{1} iff x is_/\-irreducible_in X )

for b_{1}, b_{2} being Subset of X st ( for x being set holds

( x in b_{1} iff x is_/\-irreducible_in X ) ) & ( for x being set holds

( x in b_{2} iff x is_/\-irreducible_in X ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff x is_/\-irreducible_in X );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

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

for X being non empty set

for b_{2} being Subset of X holds

( b_{2} = /\-IRR X iff for x being set holds

( x in b_{2} iff x is_/\-irreducible_in X ) );

for X being non empty set

for b

( b

( x in b

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

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

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

for X being set

for B being Subset-Family of X holds

( B is (B1) iff X in B );

for X being set

for B being Subset-Family of X holds

( B is (B1) iff X in B );

registration

let X be set ;

existence

ex b_{1} being Subset-Family of X st

( b_{1} is (B1) & b_{1} is (B2) )

end;
existence

ex b

( b

proof 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

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;

definition

let n be Element of NAT ;

let p, q be Tuple of n, BOOLEAN ;

ex b_{1} being Tuple of n, BOOLEAN st

for i being set st i in Seg n holds

b_{1} . i = (p /. i) '&' (q /. i)

for b_{1}, b_{2} being Tuple of n, BOOLEAN st ( for i being set st i in Seg n holds

b_{1} . i = (p /. i) '&' (q /. i) ) & ( for i being set st i in Seg n holds

b_{2} . i = (p /. i) '&' (q /. i) ) holds

b_{1} = b_{2}

for b_{1}, p, q being Tuple of n, BOOLEAN st ( for i being set st i in Seg n holds

b_{1} . i = (p /. i) '&' (q /. i) ) holds

for i being set st i in Seg n holds

b_{1} . i = (q /. i) '&' (p /. i)
;

end;
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 for i being set st i in Seg n holds

it . i = (p /. i) '&' (q /. i);

ex b

for i being set st i in Seg n holds

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

b

for i being set st i in Seg n holds

b

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

for n being Element of NAT

for p, q, b_{4} being Tuple of n, BOOLEAN holds

( b_{4} = p '&' q iff for i being set st i in Seg n holds

b_{4} . i = (p /. i) '&' (q /. i) );

for n being Element of NAT

for p, q, b

( b

b

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

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

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

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

definition

attr c_{1} is strict ;

struct DB-Rel -> ;

aggr DB-Rel(# Attributes, Domains, Relationship #) -> DB-Rel ;

sel Attributes c_{1} -> non empty finite set ;

sel Domains c_{1} -> V11() ManySortedSet of the Attributes of c_{1};

sel Relationship c_{1} -> Subset of (product the Domains of c_{1});

end;
struct DB-Rel -> ;

aggr DB-Rel(# Attributes, Domains, Relationship #) -> DB-Rel ;

sel Attributes c

sel Domains c

sel Relationship c

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;
mode Subset-Relation of X is Relation of (bool X);

mode Dependency-set of X is Relation of (bool X);

registration

let X be set ;

ex b_{1} being Dependency-set of X st

( not b_{1} is empty & b_{1} is finite )

end;
cluster non empty Relation-like bool X -defined bool X -valued finite for Element of bool [:(bool X),(bool X):];

existence ex b

( not b

proof end;

:: deftheorem defines Dependencies ARMSTRNG:def 6 :

for X being set holds Dependencies X = [:(bool X),(bool X):];

for X being set holds Dependencies X = [:(bool X),(bool X):];

registration
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_{1} being Element of F holds b_{1} is Dependency of X;

end;
let F be non empty Dependency-set of X;

:: original: Element

redefine mode Element of F -> Dependency of X;

correctness

coherence

for 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]

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;

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

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

definition

let R be DB-Rel ;

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

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

{ [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;

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

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 )

for A, B being Subset of the Attributes of R holds

( [A,B] in Dependency-str R iff A >|> B,R )

proof end;

definition

let X be set ;

let P, Q be Dependency of X;

reflexivity

for P being Dependency of X holds

( P `1 c= P `1 & P `2 c= P `2 ) ;

end;
let P, Q be Dependency of X;

reflexivity

for P being Dependency of X holds

( P `1 c= P `1 & P `2 c= P `2 ) ;

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

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

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

theorem :: ARMSTRNG:13

definition

let X be set ;

{ [P,Q] where P, Q is Dependency of X : P <= Q } is Relation of (Dependencies X)

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

{ [P,Q] where P, Q is Dependency of X : P <= Q } is Relation of (Dependencies X)

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

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

( x in Dependencies-Order X iff ex P, Q being Dependency of X st

( x = [P,Q] & P <= Q ) ) ;

registration

let X be set ;

coherence

Dependencies-Order X is (C1) by Th15, RELAT_1:38;

coherence

( Dependencies-Order X is total & Dependencies-Order X is reflexive & Dependencies-Order X is antisymmetric & Dependencies-Order X is (F2) )

end;
coherence

Dependencies-Order X is (C1) by Th15, RELAT_1:38;

coherence

( Dependencies-Order X is total & Dependencies-Order X is reflexive & Dependencies-Order X is antisymmetric & Dependencies-Order X is (F2) )

proof end;

notation

let X be set ;

let F be Dependency-set of X;

synonym (F2) F for transitive ;

synonym (DC1) F for transitive ;

end;
let F be Dependency-set of X;

synonym (F2) F for transitive ;

synonym (DC1) F for transitive ;

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

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

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 )

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;

end;
let F be Dependency-set of X;

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

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

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

( Dependencies X is (F1) & Dependencies X is (F2) & Dependencies X is (F3) & Dependencies X is (F4) )

proof end;

registration

let X be set ;

ex b_{1} being Dependency-set of X st

( b_{1} is (F1) & b_{1} is (F2) & b_{1} is (F3) & b_{1} is (F4) & not b_{1} is empty )

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

( b

proof end;

definition

let X be set ;

let F be Dependency-set of X;

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

( F is (F1) & F is (F2) & F is (F3) & F is (F4) );

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

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 ;

ex b_{1} being Dependency-set of X st b_{1} is full_family

end;
cluster Relation-like bool X -defined bool X -valued full_family for Element of bool [:(bool X),(bool X):];

existence ex b

proof end;

registration

let X be finite set ;

ex b_{1} being Full-family of X st b_{1} is finite

for b_{1} being Dependency-set of X holds b_{1} is finite
;

end;
cluster Relation-like bool X -defined bool X -valued finite countable full_family for Element of bool [:(bool X),(bool X):];

existence ex b

proof end;

coherence for b

registration

let X be set ;

coherence

for b_{1} being Dependency-set of X st b_{1} is full_family holds

( b_{1} is (F1) & b_{1} is (F2) & b_{1} is (F3) & b_{1} is (F4) )
;

correctness

coherence

for b_{1} being Dependency-set of X st b_{1} is (F1) & b_{1} is (F2) & b_{1} is (F3) & b_{1} is (F4) holds

b_{1} is full_family ;

;

end;
coherence

for b

( b

correctness

coherence

for b

b

;

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

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 ;

coherence

for b_{1} being Dependency-set of X st b_{1} is (F1) & b_{1} is (F3) holds

b_{1} is (DC3)

for b_{1} being Dependency-set of X st b_{1} is (DC3) & b_{1} is (F2) holds

( b_{1} is (F1) & b_{1} is (F3) )

end;
coherence

for b

b

proof end;

coherence for b

( b

proof end;

registration

let X be set ;

ex b_{1} being Dependency-set of X st

( b_{1} is (DC3) & b_{1} is (F2) & b_{1} is (F4) & not b_{1} is empty )

end;
cluster non empty Relation-like bool X -defined bool X -valued (F2) (F4) (DC3) for Element of bool [:(bool X),(bool X):];

existence ex b

( b

proof end;

theorem :: ARMSTRNG:21

theorem :: ARMSTRNG:22

registration

let X be set ;

coherence

for b_{1} being Dependency-set of X st b_{1} is (F1) holds

not b_{1} is empty
;

end;
coherence

for b

not b

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

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

proof end;

definition

let X be set ;

let F be Dependency-set of X;

(Dependencies-Order X) Maximal_in F is Dependency-set of X by RELSET_1:1;

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

(Dependencies-Order X) Maximal_in F is Dependency-set of X by RELSET_1:1;

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

for X being set

for F being Dependency-set of X holds Maximal_wrt F = (Dependencies-Order X) Maximal_in F;

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

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 )

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

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;

end;
let M be Dependency-set of X;

attr M is (M1) means :: 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 );

for A being Subset of X ex A9, B9 being Subset of X st

( [A9,B9] >= [A,A] & [A9,B9] in M );

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

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

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

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

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

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;

coherence

Maximal_wrt F is (C1)

end;
let F be Full-family of X;

coherence

Maximal_wrt F is (C1)

proof 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

for F being Dependency-set of X

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

{[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F

proof end;

definition

let X be set ;

let F be Dependency-set of X;

{ B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } is Subset-Family of X

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

{ B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } is Subset-Family of X

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

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;
let F be Dependency-set of X;

synonym closed_attribute_subset F for saturated-subsets F;

registration

let X be set ;

let F be finite Dependency-set of X;

coherence

saturated-subsets F is finite

end;
let F be finite Dependency-set of X;

coherence

saturated-subsets F is finite

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

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

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 ;

{ [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

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

{ [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;

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

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

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)

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

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;

{ 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

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

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

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

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

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

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;

ex b_{1} being Full-family of X st

( F c= b_{1} & ( for G being Dependency-set of X st F c= G & G is full_family holds

b_{1} c= G ) )

uniqueness

for b_{1}, b_{2} being Full-family of X st F c= b_{1} & ( for G being Dependency-set of X st F c= G & G is full_family holds

b_{1} c= G ) & F c= b_{2} & ( for G being Dependency-set of X st F c= G & G is full_family holds

b_{2} c= G ) holds

b_{1} = b_{2};

end;
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 ( F c= it & ( for G being Dependency-set of X st F c= G & G is full_family holds

it c= G ) );

ex b

( F c= b

b

proof end;

correctness uniqueness

for b

b

b

b

proof end;

:: deftheorem Def24 defines Dependency-closure ARMSTRNG:def 24 :

for X being non empty finite set

for F being Dependency-set of X

for b_{3} being Full-family of X holds

( b_{3} = Dependency-closure F iff ( F c= b_{3} & ( for G being Dependency-set of X st F c= G & G is full_family holds

b_{3} c= G ) ) );

for X being non empty finite set

for F being Dependency-set of X

for b

( b

b

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)

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

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

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

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;

end;
let B be Subset-Family of X;

pred G is_generator-set_of B means :: ARMSTRNG:def 25

( G c= B & B = { (Intersect S) where S is Subset-Family of X : S c= G } );

( G c= B & B = { (Intersect S) where S is Subset-Family of X : S c= G } );

:: deftheorem 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 } ) );

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)

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 )

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

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}

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;

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

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;

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;

{ A where A is Subset of X : [A,X] in Maximal_wrt F } is Subset-Family of X

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

{ A where A is Subset of X : [A,X] in Maximal_wrt F } is Subset-Family of X

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

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}

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;

definition

let X be set ;

end;
attr X is without_proper_subsets means :: ARMSTRNG:def 27

for x, y being set st x in X & y in X & x c= y holds

x = y;

for x, y being set st x in X & y in X & x c= y holds

x = y;

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

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

theorem :: ARMSTRNG:48

for R being DB-Rel holds

( candidate-keys (Dependency-str R) is (C1) & candidate-keys (Dependency-str R) is (C2) )

( 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

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)

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

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;

definition

let X be set ;

let F be Dependency-set of X;

end;
let F be Dependency-set of X;

attr F is (DC4) means :: 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;

for A, B, C being Subset of X st [A,B] in F & [A,C] in F holds

[A,(B \/ C)] in F;

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

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

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

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

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

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

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;

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

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 ;

;

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

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

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

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

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

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)

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;

end;
let F be Dependency-set of A;

pred K is_p_i_w_ncv_of F means :: 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 ) ) );

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

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

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 )

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;

:: they are the irreducible elements \ X