:: Armstrong's Axioms
::  by William W. Armstrong , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received October 25, 2002
:: Copyright (c) 2002-2021 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, EQREL_1, MARGREL1, FINSEQ_2,
      CARD_3, ORDERS_2, 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;