begin
theorem Th1:
theorem Th2:
scheme
SubsetSEq{
F1()
-> set ,
P1[
set ] } :
for
X1,
X2 being
Subset of st ( for
y being
set holds
(
y in X1 iff
P1[
y] ) ) & ( for
y being
set holds
(
y in X2 iff
P1[
y] ) ) holds
X1 = X2
:: 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:
:: deftheorem Def4 defines (B1) ARMSTRNG:def 4 :
theorem Th4:
:: deftheorem Def5 defines '&' ARMSTRNG:def 5 :
theorem Th5:
theorem
theorem
canceled;
theorem Th8:
begin
begin
:: deftheorem ARMSTRNG:def 6 :
canceled;
:: deftheorem defines Dependencies ARMSTRNG:def 7 :
theorem Th9:
theorem Th10:
:: deftheorem Def8 defines >|> ARMSTRNG:def 8 :
:: deftheorem defines Dependency-str ARMSTRNG:def 9 :
theorem
canceled;
theorem Th12:
begin
:: deftheorem Def10 defines >= ARMSTRNG:def 10 :
theorem Th13:
theorem Th14:
theorem Th15:
for
X being
set for
A,
B,
A',
B' being
Subset of holds
(
[A,B] >= [A',B'] iff (
A c= A' &
B' c= B ) )
:: deftheorem defines Dependencies-Order ARMSTRNG:def 11 :
theorem
theorem Th17:
theorem Th18:
theorem Th19:
:: deftheorem Def12 defines (F1) ARMSTRNG:def 12 :
theorem Th20:
definition
let X be
set ;
let F be
Dependency-set of
X;
attr F is
(F3) means :
Def13:
for
A,
B,
A',
B' being
Subset of st
[A,B] in F &
[A,B] >= [A',B'] holds
[A',B'] in F;
attr F is
(F4) means :
Def14:
for
A,
B,
A',
B' being
Subset of 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:
:: deftheorem Def15 defines full_family ARMSTRNG:def 15 :
theorem
:: deftheorem Def16 defines (DC3) ARMSTRNG:def 16 :
theorem
theorem
theorem Th25:
theorem
begin
:: deftheorem defines Maximal_wrt ARMSTRNG:def 17 :
theorem
:: deftheorem Def18 defines ^|^ ARMSTRNG:def 18 :
theorem Th28:
theorem Th29:
definition
let X be
set ;
let M be
Dependency-set of
X;
attr M is
(M1) means :
Def19:
for
A being
Subset of ex
A',
B' being
Subset of st
(
[A',B'] >= [A,A] &
[A',B'] in M );
attr M is
(M2) means :
Def20:
for
A,
B,
A',
B' being
Subset of st
[A,B] in M &
[A',B'] in M &
[A,B] >= [A',B'] holds
(
A = A' &
B = B' );
attr M is
(M3) means :
Def21:
for
A,
B,
A',
B' being
Subset of 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:
theorem Th31:
theorem Th32:
begin
:: deftheorem defines saturated-subsets ARMSTRNG:def 22 :
theorem Th33:
theorem Th34:
:: deftheorem defines deps_encl_by ARMSTRNG:def 23 :
theorem Th35:
theorem Th36:
theorem Th37:
:: deftheorem defines enclosure_of ARMSTRNG:def 24 :
theorem Th38:
theorem Th39:
:: deftheorem Def25 defines Dependency-closure ARMSTRNG:def 25 :
theorem Th40:
theorem Th41:
theorem
theorem
:: deftheorem Def26 defines is_generator-set_of ARMSTRNG:def 26 :
theorem
theorem Th45:
theorem
theorem
begin
theorem
begin
Lm2:
for X, F, BB being set st F = { [a,b] where a, b is Subset of : for c being set st c in BB & a c= c holds
b c= c } holds
for x, y being Subset of 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
:: deftheorem Def28 defines without_proper_subsets ARMSTRNG:def 28 :
theorem
theorem
theorem
theorem
begin
definition
let X be
set ;
let F be
Dependency-set of
X;
attr F is
(DC4) means :
Def29:
for
A,
B,
C being
Subset of st
[A,B] in F &
[A,C] in F holds
[A,(B \/ C)] in F;
attr F is
(DC5) means :
Def30:
for
A,
B,
C,
D being
Subset of st
[A,B] in F &
[(B \/ C),D] in F holds
[(A \/ C),D] in F;
attr F is
(DC6) means :
Def31:
for
A,
B,
C being
Subset of 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
theorem
theorem
:: deftheorem defines charact_set ARMSTRNG:def 32 :
theorem Th57:
theorem
theorem Th59:
theorem
theorem Th61:
:: deftheorem Def33 defines is_p_i_w_ncv_of ARMSTRNG:def 33 :
theorem