:: Armstrong's Axioms
:: by William W. Armstrong , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received October 25, 2002
:: Copyright (c) 2002-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, FINSEQ_2, FINSEQ_1, RELAT_1,
FINSUB_1, FINSET_1, SETFAM_1, TARSKI, RELAT_2, WAYBEL_4, ORDERS_2,
STRUCT_0, XXREAL_0, NAT_1, CARD_1, PRE_POLY, FUNCT_1, MARGREL1, XBOOLEAN,
PARTFUN1, BINARI_3, EUCLID, ARYTM_3, POWER, ORDINAL4, PBOOLE, CARD_3,
ZFMISC_1, MCART_1, EQREL_1, FUNCOP_1, BINARITH, FUNCT_4, ARMSTRNG,
XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, FINSET_1,
FINSUB_1, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, PARTFUN1, CARD_1,
ORDINAL1, NUMBERS, FUNCT_4, FUNCT_1, ORDERS_2, MCART_1, EQREL_1, CARD_3,
PBOOLE, XCMPLX_0, STRUCT_0, WAYBEL_4, FINSEQ_1, FUNCOP_1, MARGREL1,
FINSEQ_2, BINARITH, BINARI_3, SERIES_1, EUCLID, XXREAL_0, NAT_1,
PRE_POLY, FUNCT_2;
constructors SETFAM_1, XXREAL_0, FINSEQOP, SERIES_1, BINARITH, EUCLID,
MATRLIN, WAYBEL_4, BINARI_3, RELSET_1, XTUPLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, EQREL_1, MARGREL1,
FINSEQ_2, CARD_3, ORDERS_2, PRE_POLY, CARD_1, RELSET_1, STRUCT_0,
FUNCT_4, XTUPLE_0;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin
theorem :: ARMSTRNG:1
for B being set st B is cap-closed for X being set, S being
finite Subset-Family of X st X in B & S c= B holds Intersect S in B;
registration
cluster reflexive antisymmetric transitive non empty for Relation;
end;
theorem :: ARMSTRNG:2
for R being antisymmetric transitive non empty Relation, X being
finite Subset of field R st X <> {} ex x being Element of X st x is_maximal_wrt
X, R;
scheme :: ARMSTRNG:sch 1
SubsetSEq { X() -> set, P[set] }: for X1,X2 being Subset of X() st (for y
being set holds y in X1 iff P[y]) & (for y being set holds y in X2 iff P[y])
holds X1 = X2;
definition
let X be set, R be Relation;
func R Maximal_in X -> Subset of X means
:: ARMSTRNG:def 1
for x being object holds x in it iff x is_maximal_wrt X, R;
end;
definition
let x, X be set;
pred x is_/\-irreducible_in X means
:: ARMSTRNG:def 2
x in X & for z, y being set st z
in X & y in X & x = z /\ y holds x = z or x = y;
end;
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
:: ARMSTRNG:def 3
for x being set holds x in it iff x is_/\-irreducible_in X;
end;
scheme :: ARMSTRNG:sch 2
FinIntersect {X() -> non empty finite set, P[set]} : for x being set st x in
X() holds P[x]
provided
for x being set st x is_/\-irreducible_in X() holds P[x] and
for x, y being set st x in X() & y in X() & P[x] & P[y] holds P[x /\ y];
theorem :: ARMSTRNG:3
for X being non empty finite set, 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;
definition
let X be set, B be Subset-Family of X;
attr B is (B1) means
:: ARMSTRNG:def 4
X in B;
end;
notation
let B be set;
synonym B is (B2) for B is cap-closed;
end;
registration
let X be set;
cluster (B1) (B2) for Subset-Family of X;
end;
theorem :: ARMSTRNG:4
for X being set, B being non empty Subset-Family of X st B is
cap-closed for x being Element of B st x is_/\-irreducible_in B & x <> X for S
being finite Subset-Family of X st S c= B & x = Intersect S holds x in S;
definition
let n be Element of NAT, p, q be Tuple of n, BOOLEAN;
func p '&' q -> Tuple of n, BOOLEAN means
:: ARMSTRNG:def 5
for i being set st i in Seg n holds it.i = (p/.i) '&' (q/.i);
commutativity;
end;
theorem :: ARMSTRNG:5
for n being Element of NAT, p being Element of n-tuples_on BOOLEAN holds (n
-BinarySequence 0) '&' p = n-BinarySequence 0;
theorem :: ARMSTRNG:6
for n being Element of NAT, p being Tuple of n, BOOLEAN holds 'not' (n
-BinarySequence 0) '&' p = p;
theorem :: 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;
begin :: 2. The relational model of data
definition
struct DB-Rel (# Attributes -> finite non empty set, Domains -> non-empty
ManySortedSet of the Attributes, Relationship -> Subset of product the Domains
#);
end;
begin :: 3. Dependency structures
definition
let X be set;
mode Subset-Relation of X is Relation of bool X;
mode Dependency-set of X is Relation of bool X;
end;
registration
let X be set;
cluster non empty finite for Dependency-set of X;
end;
definition
let X be set;
func Dependencies(X) -> Dependency-set of X equals
:: ARMSTRNG:def 6
[: bool X, bool X :];
end;
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;
end;
definition
let X be set, F be non empty Dependency-set of X;
redefine mode Element of F -> Dependency of X;
end;
theorem :: ARMSTRNG:8
for X, x being set holds x in Dependencies X iff ex a, b being
Subset of X st x = [a,b];
theorem :: ARMSTRNG:9
for X, x being set, F being Dependency-set of X holds x in F
implies ex a, b being Subset of X st x = [a,b];
definition
let R be DB-Rel, A, B be Subset of the Attributes of R;
pred A >|> B, R means
:: ARMSTRNG:def 7
for f, g being Element of the Relationship of R st f|A = g|A holds f|B = g|B;
end;
notation
let R be DB-Rel, 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 };
end;
theorem :: ARMSTRNG:10
for R being DB-Rel, A, B being Subset of the Attributes of R
holds [A, B] in Dependency-str R iff A >|> B, R;
begin :: 4. Full families of dependencies
definition
let X be set, P, Q be Dependency of X;
pred P >= Q means
:: ARMSTRNG:def 9
P`1 c= Q`1 & Q`2 c= P`2;
reflexivity;
end;
notation
let X be set, 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 :: ARMSTRNG:11 :: antisymmetry
for X being set, P, Q being Dependency of X st P <= Q & Q <= P holds P = Q;
theorem :: ARMSTRNG:12 :: transitivity
for X being set, P, Q, S being Dependency of X st P <= Q & Q <=
S holds P <= S;
definition
let X be set, A, B be Subset of X;
redefine func [A, B] -> Dependency of X;
end;
theorem :: ARMSTRNG:13
for X being set, A, B, A9, B9 being Subset of X holds [A,B] >= [
A9,B9] iff A c= A9 & B9 c= B;
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 };
end;
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 :: ARMSTRNG:15
for X being set holds dom Dependencies-Order X = [: bool X, bool X :];
theorem :: ARMSTRNG:16
for X being set holds rng Dependencies-Order X = [: bool X, bool X :];
theorem :: ARMSTRNG:17
for X being set holds field Dependencies-Order X = [: bool X, bool X :];
registration
let X be set;
cluster Dependencies-Order X -> non empty;
cluster Dependencies-Order X -> total reflexive antisymmetric transitive;
end;
notation
let X be set, F be Dependency-set of X;
synonym F is (F2) for F is transitive;
synonym F is (DC1) for F is transitive;
end;
definition
let X be set, F be Dependency-set of X;
attr F is (F1) means
:: ARMSTRNG:def 11
for A being Subset of X holds [A, A] in F;
end;
notation
let X be set, F be Dependency-set of X;
synonym F is (DC2) for F is (F1);
end;
theorem :: ARMSTRNG:18
for X being set, 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;
definition
let X be set, F be Dependency-set of X;
attr F is (F3) means
:: 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
:: 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;
theorem :: ARMSTRNG:19
for X being set holds Dependencies X is (F1) (F2) (F3) (F4);
registration
let X be set;
cluster (F1) (F2) (F3) (F4) non empty for Dependency-set of X;
end;
definition
let X be set, F be Dependency-set of X;
attr F is full_family means
:: ARMSTRNG:def 14
F is (F1) (F2) (F3) (F4);
end;
registration
let X be set;
cluster full_family for Dependency-set of X;
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, F being Dependency-set of X holds F is finite;
registration
let X be finite set;
cluster finite for Full-family of X;
cluster -> finite for Dependency-set of X;
end;
registration
let X be set;
cluster full_family -> (F1) (F2) (F3) (F4) for Dependency-set of X;
cluster (F1) (F2) (F3) (F4) -> full_family for Dependency-set of X;
end;
definition
let X be set, F be Dependency-set of X;
attr F is (DC3) means
:: ARMSTRNG:def 15
for A, B being Subset of X st B c= A holds [A, B] in F;
end;
registration
let X be set;
cluster (F1) (F3) -> (DC3) for Dependency-set of X;
cluster (DC3) (F2) -> (F1) (F3) for Dependency-set of X;
end;
registration
let X be set;
cluster (DC3) (F2) (F4) non empty for Dependency-set of X;
end;
theorem :: ARMSTRNG:21 :: F13_2_1_3:
for X being set, F being Dependency-set of X st F is (DC3) (F2) holds
F is (F1) (F3);
theorem :: ARMSTRNG:22 :: F1_3_13:
for X being set, F being Dependency-set of X st F is (F1) (F3) holds F
is (DC3);
registration
let X be set;
cluster (F1) -> non empty for Dependency-set of X;
end;
theorem :: ARMSTRNG:23 :: WWA1:
for R being DB-Rel holds Dependency-str R is full_family;
theorem :: ARMSTRNG:24 :: Ex1:
for X being set, 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;
begin :: 5. Maximal elements of full families
definition
let X be set, F be Dependency-set of X;
func Maximal_wrt F -> Dependency-set of X equals
:: ARMSTRNG:def 16
Dependencies-Order X
Maximal_in F;
end;
theorem :: ARMSTRNG:25
for X being set, F being Dependency-set of X holds Maximal_wrt F c= F;
definition
let X be set, F be Dependency-set of X, x, y be set;
pred x ^|^ y, F means
:: ARMSTRNG:def 17
[x, y] in Maximal_wrt F;
end;
theorem :: ARMSTRNG:26
for X being finite set, P being Dependency of X, F being
Dependency-set of X st P in F ex A, B being Subset of X st [A, B] in
Maximal_wrt F & [A, B] >= P;
theorem :: ARMSTRNG:27
for X being set, F being Dependency-set of X, A, B being Subset
of X holds A ^|^ B, F iff [A, B] in F & not ex A9, B9 being Subset of X st [A9,
B9] in F & (A <> A9 or B <> B9) & [A, B] <= [A9, B9];
definition
let X be set, 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;
attr M is (M2) means
:: 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
:: 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;
theorem :: ARMSTRNG:28 :: WWA2:
for X being finite non empty set, F being Full-family of X holds
Maximal_wrt F is (M1) (M2) (M3);
theorem :: ARMSTRNG:29 :: WWA2a check this proof, WWA is sketchy
for X being finite set, M, F being Dependency-set of X st M is
(M1) (M2) (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;
registration
let X be non empty finite set, F be Full-family of X;
cluster Maximal_wrt F -> non empty;
end;
theorem :: ARMSTRNG:30 :: Ex2:
for X being finite set, F being Dependency-set of X, 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;
begin :: 6. Saturated subsets of Attributes
definition
let X be set, 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 };
end;
notation
let X be set, F be Dependency-set of X;
synonym closed_attribute_subset F for saturated-subsets F;
end;
registration
let X be set, F be finite Dependency-set of X;
cluster saturated-subsets F -> finite;
end;
theorem :: ARMSTRNG:31
for X, x being set, 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;
theorem :: ARMSTRNG:32 :: WWA3:
for X being finite non empty set, F being Full-family of X holds
saturated-subsets F is (B1) (B2);
definition
let X be set, 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};
end;
theorem :: ARMSTRNG:33 :: WWA3_0:
for X being set, B being Subset-Family of X, F being
Dependency-set of X holds X deps_encl_by B is full_family;
theorem :: ARMSTRNG:34 :: WWA3_00:
for X being finite non empty set, B being Subset-Family of X
holds B c= saturated-subsets (X deps_encl_by B);
theorem :: ARMSTRNG:35 :: WWA3a:
for X being finite non empty set, B being Subset-Family of X st
B is (B1) (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;
definition
let X be set, 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 };
end;
theorem :: ARMSTRNG:36 :: WWA3c:
for X being finite non empty set, F being Dependency-set of X
holds enclosure_of F is (B1) (B2);
theorem :: ARMSTRNG:37 :: WWA3b
:: Added for proving WWA7 where it is referenced but never
:: stated. This characterizes the smallest full family
:: containing a given dependency set
for X being finite non empty set, 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;
definition
let X be finite non empty set, F be Dependency-set of X;
func Dependency-closure F -> Full-family of X means
:: 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;
end;
theorem :: ARMSTRNG:38 :: WWA3d:
for X being finite non empty set, F being Dependency-set of X
holds Dependency-closure F = X deps_encl_by enclosure_of F;
theorem :: ARMSTRNG:39 :: Ex3:
for X being set, K being Subset of X, B being Subset-Family of X
st B = {X}\/{A where A is Subset of X : not K c= A} holds B is (B1) (B2);
theorem :: ARMSTRNG:40 :: Ex3a:
for X being finite non empty set, F being Dependency-set of X, 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;
theorem :: ARMSTRNG:41
for X being finite set, F being Dependency-set of X, 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;
definition
let X, G be set, 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 };
end;
theorem :: ARMSTRNG:42 :: WWA4b:
for X be finite non empty set, G being Subset-Family of X holds G
is_generator-set_of saturated-subsets (X deps_encl_by G);
theorem :: ARMSTRNG:43 :: WWA4a:
for X being finite non empty set, 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;
:: WWA did not show what generators B are,
:: they are the irreducible elements \ X
theorem :: ARMSTRNG:44
for X being set, B being non empty finite Subset-Family of X st B is
(B1) (B2) holds /\-IRR B is_generator-set_of B;
theorem :: ARMSTRNG:45
for X, G being set, B being non empty finite Subset-Family of X st B
is (B1) (B2) & G is_generator-set_of B holds /\-IRR B c= G\/{X};
begin :: 7. Justification of the axioms
definition let n be Element of NAT, 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, 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;
begin
definition
let X be set, 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 };
end;
theorem :: ARMSTRNG:47 :: Ex8:
for X being finite set, F being Dependency-set of X, 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};
notation
let X be set;
antonym X is (C1) for X is empty;
end;
definition
let X be set;
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;
end;
notation
let X be set;
synonym X is (C2) for X is without_proper_subsets;
end;
theorem :: ARMSTRNG:48 :: WWA6:
for R being DB-Rel holds candidate-keys Dependency-str R is (C1) (C2);
theorem :: ARMSTRNG:49 :: WWA6a:
for X being finite set, C being Subset-Family of X st C is (C1) (C2)
ex F being Full-family of X st C = candidate-keys F;
theorem :: ARMSTRNG:50 :: WWA6a A more reasonable version
for X being finite set, C being Subset-Family of X, B being set st C
is (C1) (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);
theorem :: ARMSTRNG:51 :: WWA6a proof II
for X being non empty finite set, C being Subset-Family of X st C is
(C1) (C2) ex R being DB-Rel st the Attributes of R = X & C = candidate-keys
Dependency-str R;
begin :: 9. Applications
definition
let X be set, 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;
attr F is (DC5) means
:: 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
:: ARMSTRNG:def 30
for A, B, C being Subset of X st [A, B] in F holds [A\/C, B] in F;
end;
theorem :: ARMSTRNG:52 :: APP0:
for X being set, F being Dependency-set of X holds F is (F1) (F2) (F3)
(F4) iff F is (F2) (DC3) (F4);
theorem :: ARMSTRNG:53 :: APP1:
for X being set, F being Dependency-set of X holds F is (F1) (F2) (F3)
(F4) iff F is (DC1) (DC3) (DC4);
theorem :: ARMSTRNG:54 :: APP2:
for X being set, F being Dependency-set of X holds F is (F1) (F2) (F3)
(F4) iff F is (DC2) (DC5) (DC6);
definition
let X be set, 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 };
end;
theorem :: ARMSTRNG:55
for X, A being set, 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;
theorem :: ARMSTRNG:56
for X being set, A being Subset of X, 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 :: ARMSTRNG:57 :: WWA7:
for X being finite non empty set, 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;
theorem :: ARMSTRNG:58 :: WWACorA: :: Bill: Is this the right translation
for X being finite non empty set, F, G being Dependency-set of X st
charact_set F = charact_set G holds Dependency-closure F = Dependency-closure G
;
theorem :: ARMSTRNG:59
for X being non empty finite set, F being Dependency-set of X
holds charact_set F = charact_set (Dependency-closure F);
definition
let A be set, K be set, 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 ex a being
Subset of A st k c= a & a <> A & not a in charact_set F;
end;
theorem :: ARMSTRNG:60 :: WWACorB:
for X being finite non empty set, F being Dependency-set of X, K being
Subset of X holds K in candidate-keys Dependency-closure F iff K
is_p_i_w_ncv_of F;