:: Armstrong's Axioms
:: by William W. Armstrong , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received October 25, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem Th1: :: ARMSTRNG:1
theorem Th2: :: ARMSTRNG:2
:: deftheorem Def1 defines Maximal_in ARMSTRNG:def 1 :
:: deftheorem Def2 defines is_/\-irreducible_in ARMSTRNG:def 2 :
:: deftheorem Def3 defines /\-IRR ARMSTRNG:def 3 :
theorem Th3: :: ARMSTRNG:3
:: deftheorem Def4 defines (B1) ARMSTRNG:def 4 :
theorem Th4: :: ARMSTRNG:4
:: deftheorem Def5 defines '&' ARMSTRNG:def 5 :
theorem Th5: :: ARMSTRNG:5
theorem :: ARMSTRNG:6
theorem :: ARMSTRNG:7
canceled;
theorem Th8: :: ARMSTRNG:8
:: deftheorem ARMSTRNG:def 6 :
canceled;
:: deftheorem defines Dependencies ARMSTRNG:def 7 :
theorem Th9: :: ARMSTRNG:9
theorem Th10: :: ARMSTRNG:10
:: deftheorem Def8 defines >|> ARMSTRNG:def 8 :
:: deftheorem defines Dependency-str ARMSTRNG:def 9 :
theorem :: ARMSTRNG:11
canceled;
theorem Th12: :: ARMSTRNG:12
:: deftheorem Def10 defines >= ARMSTRNG:def 10 :
theorem Th13: :: ARMSTRNG:13
theorem Th14: :: ARMSTRNG:14
theorem Th15: :: ARMSTRNG:15
for
X being
set for
A,
B,
A',
B' being
Subset of
X holds
(
[A,B] >= [A',B'] iff (
A c= A' &
B' c= B ) )
:: deftheorem defines Dependencies-Order ARMSTRNG:def 11 :
theorem :: ARMSTRNG:16
theorem Th17: :: ARMSTRNG:17
theorem Th18: :: ARMSTRNG:18
theorem Th19: :: ARMSTRNG:19
:: deftheorem Def12 defines (F1) ARMSTRNG:def 12 :
theorem Th20: :: ARMSTRNG:20
definition
let X be
set ;
let F be
Dependency-set of
X;
attr F is
(F3) means :
Def13:
:: ARMSTRNG:def 13
for
A,
B,
A',
B' being
Subset of
X st
[A,B] in F &
[A,B] >= [A',B'] holds
[A',B'] in F;
attr F is
(F4) means :
Def14:
:: ARMSTRNG:def 14
for
A,
B,
A',
B' being
Subset of
X st
[A,B] in F &
[A',B'] in F holds
[(A \/ A'),(B \/ B')] in F;
end;
:: deftheorem Def13 defines (F3) ARMSTRNG:def 13 :
:: deftheorem Def14 defines (F4) ARMSTRNG:def 14 :
theorem Th21: :: ARMSTRNG:21
:: deftheorem Def15 defines full_family ARMSTRNG:def 15 :
theorem :: ARMSTRNG:22
:: deftheorem Def16 defines (DC3) ARMSTRNG:def 16 :
theorem :: ARMSTRNG:23
theorem :: ARMSTRNG:24
theorem Th25: :: ARMSTRNG:25
theorem :: ARMSTRNG:26
:: deftheorem defines Maximal_wrt ARMSTRNG:def 17 :
theorem :: ARMSTRNG:27
:: deftheorem Def18 defines ^|^ ARMSTRNG:def 18 :
theorem Th28: :: ARMSTRNG:28
theorem Th29: :: ARMSTRNG:29
definition
let X be
set ;
let M be
Dependency-set of
X;
attr M is
(M1) means :
Def19:
:: ARMSTRNG:def 19
for
A being
Subset of
X ex
A',
B' being
Subset of
X st
(
[A',B'] >= [A,A] &
[A',B'] in M );
attr M is
(M2) means :
Def20:
:: ARMSTRNG:def 20
for
A,
B,
A',
B' being
Subset of
X st
[A,B] in M &
[A',B'] in M &
[A,B] >= [A',B'] holds
(
A = A' &
B = B' );
attr M is
(M3) means :
Def21:
:: ARMSTRNG:def 21
for
A,
B,
A',
B' being
Subset of
X st
[A,B] in M &
[A',B'] in M &
A' c= B holds
B' c= B;
end;
:: deftheorem Def19 defines (M1) ARMSTRNG:def 19 :
:: deftheorem Def20 defines (M2) ARMSTRNG:def 20 :
:: deftheorem Def21 defines (M3) ARMSTRNG:def 21 :
theorem Th30: :: ARMSTRNG:30
theorem Th31: :: ARMSTRNG:31
theorem Th32: :: ARMSTRNG:32
:: deftheorem defines saturated-subsets ARMSTRNG:def 22 :
theorem Th33: :: ARMSTRNG:33
theorem Th34: :: ARMSTRNG:34
:: deftheorem defines deps_encl_by ARMSTRNG:def 23 :
theorem Th35: :: ARMSTRNG:35
theorem Th36: :: ARMSTRNG:36
theorem Th37: :: ARMSTRNG:37
:: deftheorem defines enclosure_of ARMSTRNG:def 24 :
theorem Th38: :: ARMSTRNG:38
theorem Th39: :: ARMSTRNG:39
:: deftheorem Def25 defines Dependency-closure ARMSTRNG:def 25 :
theorem Th40: :: ARMSTRNG:40
theorem Th41: :: ARMSTRNG:41
theorem :: ARMSTRNG:42
theorem :: ARMSTRNG:43
:: deftheorem Def26 defines is_generator-set_of ARMSTRNG:def 26 :
theorem :: ARMSTRNG:44
theorem Th45: :: ARMSTRNG:45
theorem :: ARMSTRNG:46
theorem :: ARMSTRNG:47
theorem :: ARMSTRNG:48
Lm2:
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 )
:: deftheorem defines candidate-keys ARMSTRNG:def 27 :
theorem :: ARMSTRNG:49
:: deftheorem Def28 defines without_proper_subsets ARMSTRNG:def 28 :
theorem :: ARMSTRNG:50
theorem :: ARMSTRNG:51
theorem :: ARMSTRNG:52
theorem :: ARMSTRNG:53
definition
let X be
set ;
let F be
Dependency-set of
X;
attr F is
(DC4) means :
Def29:
:: ARMSTRNG:def 29
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 :
Def30:
:: ARMSTRNG:def 30
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 :
Def31:
:: ARMSTRNG:def 31
for
A,
B,
C being
Subset of
X st
[A,B] in F holds
[(A \/ C),B] in F;
end;
:: deftheorem Def29 defines (DC4) ARMSTRNG:def 29 :
:: deftheorem Def30 defines (DC5) ARMSTRNG:def 30 :
:: deftheorem Def31 defines (DC6) ARMSTRNG:def 31 :
theorem :: ARMSTRNG:54
theorem :: ARMSTRNG:55
theorem :: ARMSTRNG:56
:: deftheorem defines charact_set ARMSTRNG:def 32 :
theorem Th57: :: ARMSTRNG:57
theorem :: ARMSTRNG:58
theorem Th59: :: ARMSTRNG:59
theorem :: ARMSTRNG:60
theorem Th61: :: ARMSTRNG:61
:: deftheorem Def33 defines is_p_i_w_ncv_of ARMSTRNG:def 33 :
theorem :: ARMSTRNG:62