:: Armstrong's Axioms
:: by William W. Armstrong , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received October 25, 2002
:: Copyright (c) 2002-2026 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;
definitions TARSKI, RELAT_2, YELLOW_0, WAYBEL_4, FINSUB_1;
equalities FINSEQ_2, SUBSET_1, XBOOLEAN;
expansions TARSKI, RELAT_2, WAYBEL_4, FINSUB_1;
theorems TARSKI, RELSET_1, ZFMISC_1, EQREL_1, MCART_1, RELAT_1, RELAT_2,
XBOOLE_0, XBOOLE_1, ORDERS_2, ENUMSET1, FINSET_1, SUBSET_1, SETFAM_1,
MSSUBFAM, TREES_1, FUNCT_1, FINSEQ_4, FINSEQ_1, FINSEQ_2, FUNCOP_1,
CARD_3, BINARI_3, NAT_1, EUCLID, FUNCT_2, BINARITH, POWER, FUNCT_4,
PARTFUN1, NUMBERS, XREAL_1, ORDERS_1, XXREAL_0, ORDINAL1, PRE_POLY,
CARD_1, XTUPLE_0, BAGORDER;
schemes FINSET_1, NAT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, XBOOLE_0, CLASSES1;
begin
Lm1: now
let n be Nat, X be non empty set, t be Tuple of n, X;
len t = n by CARD_1:def 7;
hence dom t = Seg n by FINSEQ_1:def 3;
end;
Lm2: now
let n be Element of NAT, X be non empty set,
t be Element of n-tuples_on X;
len t = n by CARD_1:def 7;
hence dom t = Seg n by FINSEQ_1:def 3;
end;
theorem Th1:
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
proof
let B be set;
assume
A1: B is cap-closed;
let X be set, S be finite Subset-Family of X such that
A2: X in B and
A3: S c= B;
defpred P[set] means for sf being Subset-Family of X st sf = $1 holds
Intersect sf in B;
A4: now
let x be set, b be set such that
A5: x in S and
A6: b c= S and
A7: P[b];
thus P[ b\/{x}]
proof
reconsider fx = {x} as Subset-Family of X by A5,ZFMISC_1:31;
reconsider fb = b as Subset-Family of X by A6,XBOOLE_1:1;
reconsider sx = x as Subset of X by A5;
A8: Intersect (fb\/fx) = Intersect fb /\ Intersect fx by MSSUBFAM:8
.= Intersect fb /\ sx by MSSUBFAM:9;
A9: Intersect fb in B by A7;
let sf be Subset-Family of X;
assume sf = b\/{x};
hence thesis by A1,A3,A5,A9,A8;
end;
end;
A10: S is finite;
A11: P[{}] by A2,SETFAM_1:def 9;
P[S] from FINSET_1:sch 2(A10,A11,A4);
hence thesis;
end;
registration
cluster reflexive antisymmetric transitive non empty for Relation;
existence
proof
set R = {[{},{}]};
reconsider R as Relation;
take R;
A1: field R = {{},{}} by RELAT_1:17
.= {{}} by ENUMSET1:29;
thus R is reflexive
proof
let x be object;
assume x in field R;
then x = {} by A1,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
thus R is antisymmetric
proof
let x, y be object;
assume that
A2: x in field R and
A3: y in field R and
[x,y] in R and
[y,x] in R;
x = {} by A1,A2,TARSKI:def 1;
hence thesis by A1,A3,TARSKI:def 1;
end;
thus R is transitive
proof
let x, y, z be object;
assume that
A4: x in field R and
y in field R and
A5: z in field R and
[x,y] in R and
[y,z] in R;
A6: z = {} by A1,A5,TARSKI:def 1;
x = {} by A1,A4,TARSKI:def 1;
hence thesis by A6,TARSKI:def 1;
end;
thus thesis;
end;
end;
theorem Th2:
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
proof
let R be antisymmetric transitive non empty Relation, X being finite Subset
of field R;
reconsider IR = R as Relation of field R by PRE_POLY:18;
set S = RelStr(# field R, IR #);
set CR = the carrier of S;
set ir = the InternalRel of S;
A1: CR is non empty;
A2: R is_transitive_in field R by RELAT_2:def 16;
A3: S is transitive
proof
let x, y, z be Element of S;
assume that
A4: x <= y and
A5: y <= z;
A6: [y,z] in ir by A5,ORDERS_2:def 5;
[x,y] in ir by A4,ORDERS_2:def 5;
then [x,z] in ir by A1,A2,A6;
hence thesis by ORDERS_2:def 5;
end;
A7: R is_antisymmetric_in field R by RELAT_2:def 12;
S is antisymmetric
proof
let x, y be Element of S;
assume that
A8: x <= y and
A9: y <= x;
A10: [y,x] in ir by A9,ORDERS_2:def 5;
[x,y] in ir by A8,ORDERS_2:def 5;
hence thesis by A1,A7,A10;
end;
then reconsider S as antisymmetric transitive non empty RelStr by A3;
reconsider Y = X as finite Subset of CR;
assume X <> {};
then consider x being Element of S such that
A11: x in Y and
A12: x is_maximal_wrt Y, the InternalRel of S by BAGORDER:6;
reconsider x as Element of X by A11;
take x;
thus x in X by A11;
given y being set such that
A13: y in X and
A14: y <> x and
A15: [x, y] in R;
thus thesis by A12,A13,A14,A15;
end;
scheme
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 proof
let X1,X2 being Subset of X() such that
A1: for y being set holds y in X1 iff P[y] and
A2: for y being set holds y in X2 iff P[y];
for x being object holds x in X1 iff x in X2 by A1,A2;
hence thesis by TARSKI:2;
end;
definition
let X be set, R be Relation;
defpred P[object] means $1 is_maximal_wrt X, R;
func R Maximal_in X -> Subset of X means
:Def1:
for x being object holds x in it iff x is_maximal_wrt X, R;
existence
proof
consider I being set such that
A1: for x being object holds x in I iff x in X & P[x] from XBOOLE_0:sch 1;
for x being object st x in I holds x in X by A1;
then reconsider I as Subset of X by TARSKI:def 3;
take I;
let x be object;
thus x in I implies x is_maximal_wrt X, R by A1;
assume
A2: x is_maximal_wrt X, R;
thus thesis by A1,A2;
end;
uniqueness
proof
let X1,X2 be Subset of X;
assume
(for y being object holds y in X1 iff P[y]) &
(for y being object holds y in X2 iff P[y]);
then for y being object holds y in X1 iff y in X2;
hence X1 = X2 by TARSKI:2;
end;
end;
definition
let x, X be set;
pred x is_/\-irreducible_in X means
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
:Def3:
for x being set holds x in it iff x is_/\-irreducible_in X;
existence
proof
set irr = {z where z is Element of X : z is_/\-irreducible_in X };
irr c= X
proof
let x be object;
assume x in irr;
then ex z being Element of X st x = z & z is_/\-irreducible_in X;
hence thesis;
end;
then reconsider irr as Subset of X;
take irr;
let x be set;
hereby
assume x in irr;
then ex z being Element of X st x = z & z is_/\-irreducible_in X;
hence x is_/\-irreducible_in X;
end;
assume
A1: x is_/\-irreducible_in X;
thus thesis by A1;
end;
uniqueness
proof
defpred P[set] means $1 is_/\-irreducible_in X;
thus 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 from SubsetSEq;
end;
end;
scheme
FinIntersect {X() -> non empty finite set, P[set]} : for x being set st x in
X() holds P[x]
provided
A1: for x being set st x is_/\-irreducible_in X() holds P[x] and
A2: for x, y being set st x in X() & y in X() & P[x] & P[y] holds P[x /\ y]
proof
deffunc U(set) = {x where x is Element of X(): $1 c= x};
given x being set such that
A3: x in X() and
A4: not P[x];
defpred R[Nat] means ex s being Element of X() st card U(s) = $1 & not P[s];
U(x) c= X()
proof
let x1 be object;
assume x1 in U(x);
then ex xx being Element of X() st x1 = xx & x c= xx;
hence thesis;
end;
then reconsider Ux = U(x) as finite set;
A5: ex k being Nat st R[k]
proof
reconsider x as Element of X() by A3;
take k = card Ux;
take x;
thus card U(x) = k;
thus thesis by A4;
end;
consider k being Nat such that
A6: R[k] and
A7: for n being Nat st R[n] holds k <= n from NAT_1:sch 5(A5);
consider s being Element of X() such that
A8: card U(s) = k and
A9: not P[s] by A6;
per cases;
suppose
s is_/\-irreducible_in X();
hence contradiction by A1,A9;
end;
suppose
A10: s is_/\-reducible_in X();
U(s) c= X()
proof
let x be object;
assume x in U(s);
then ex xx being Element of X() st x = xx & s c= xx;
hence thesis;
end;
then reconsider Us = U(s) as finite set;
consider z, y being set such that
A11: z in X() and
A12: y in X() and
A13: s = z /\ y and
A14: s <> z and
A15: s <> y by A10;
A16: s c= y by A13,XBOOLE_1:17;
U(z) c= X()
proof
let x be object;
assume x in U(z);
then ex xx being Element of X() st x = xx & z c= xx;
hence thesis;
end;
then reconsider Uz = U(z) as finite set;
U(y) c= X()
proof
let x be object;
assume x in U(y);
then ex xx being Element of X() st x = xx & y c= xx;
hence thesis;
end;
then reconsider Uy = U(y) as finite set;
A17: s c= z by A13,XBOOLE_1:17;
reconsider y, z as Element of X() by A11,A12;
A18: Uy c= Us
proof
let x be object;
assume x in Uy;
then consider xx being Element of X() such that
A19: x = xx and
A20: y c= xx;
s c= xx by A16,A20;
hence thesis by A19;
end;
now
assume s in Uy;
then ex x being Element of X() st s = x & y c= x;
hence contradiction by A15,A16,XBOOLE_0:def 10;
end;
then Uy <> Us;
then Uy c< Us by A18,XBOOLE_0:def 8;
then card Us > card Uy by TREES_1:6;
then
A21: P[y] by A7,A8;
A22: Uz c= Us
proof
let x be object;
assume x in Uz;
then consider xx being Element of X() such that
A23: x = xx and
A24: z c= xx;
s c= xx by A17,A24;
hence thesis by A23;
end;
now
assume s in Uz;
then ex x being Element of X() st s = x & z c= x;
hence contradiction by A14,A17,XBOOLE_0:def 10;
end;
then Uz <> Us;
then Uz c< Us by A22,XBOOLE_0:def 8;
then card Us > card Uz by TREES_1:6;
then P[z] by A7,A8;
hence contradiction by A2,A9,A13,A21;
end;
end;
theorem Th3:
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
proof
let X be non empty finite set, x be Element of X;
defpred P[set] means ex S being non empty Subset of X st $1 = meet S & for s
being set st s in S holds s is_/\-irreducible_in X;
A1: now
let x, y be set such that
x in X and
y in X and
A2: P[x] and
A3: P[y];
consider Sy being non empty Subset of X such that
A4: y = meet Sy and
A5: for s being set st s in Sy holds s is_/\-irreducible_in X by A3;
consider Sx being non empty Subset of X such that
A6: x = meet Sx and
A7: for s being set st s in Sx holds s is_/\-irreducible_in X by A2;
reconsider S = Sx\/Sy as non empty Subset of X;
now
take S;
thus x /\ y = meet S by A6,A4,SETFAM_1:9;
let s be set;
assume
A8: s in S;
per cases by A8,XBOOLE_0:def 3;
suppose
s in Sx;
hence s is_/\-irreducible_in X by A7;
end;
suppose
s in Sy;
hence s is_/\-irreducible_in X by A5;
end;
end;
hence P[x /\ y];
end;
A9: now
let x be set;
assume
A10: x is_/\-irreducible_in X;
thus P[x]
proof
x in X by A10;
then reconsider S = {x} as non empty Subset of X by ZFMISC_1:31;
take S;
thus x = meet S by SETFAM_1:10;
let s be set;
assume s in S;
hence thesis by A10,TARSKI:def 1;
end;
end;
for x being set st x in X holds P[x] from FinIntersect(A9,A1);
hence thesis;
end;
definition
let X be set, B be Subset-Family of X;
attr B is (B1) means
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;
existence
proof
set B = {X};
reconsider B as Subset-Family of X by ZFMISC_1:68;
take B;
X in B by TARSKI:def 1;
hence B is (B1);
thus B is (B2)
proof
let a, b be set;
assume that
A1: a in B and
A2: b in B;
A3: b = X by A2,TARSKI:def 1;
a = X by A1,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
end;
end;
theorem Th4:
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
proof
let X be set, B be non empty Subset-Family of X such that
A1: B is (B2);
let x be Element of B such that
A2: x is_/\-irreducible_in B and
A3: x <> X;
defpred P[set] means (ex a, b being Element of B st x <> a & x <> b & x = a
/\ b) or ex f being Subset-Family of X st $1 = {} or $1 <> {} & $1 = f &
Intersect f <> x & Intersect f in B;
let S be finite Subset-Family of X such that
A4: S c= B and
A5: x = Intersect S and
A6: not x in S;
A7: now
let s, A be set such that
A8: s in S and
A c= S and
A9: P[A];
per cases by A9;
suppose
ex a, b being Element of B st x <> a & x <> b & x = a /\ b;
hence P[A\/{s}];
end;
suppose
ex f being Subset-Family of X st A = {} or A = f & Intersect f
<> x & Intersect f in B;
then consider f being Subset-Family of X such that
A10: A = {} or A <> {} & A = f & Intersect f <> x & Intersect f in B;
thus P[A\/{s}]
proof
reconsider sf = {s} as Subset-Family of X by A8,ZFMISC_1:31;
A11: Intersect sf = meet sf by SETFAM_1:def 9;
then
A12: Intersect sf = s by SETFAM_1:10;
per cases by A10;
suppose
A = {};
hence thesis by A4,A6,A8,A12;
end;
suppose
A13: A <> {} & A = f & Intersect f <> x & Intersect f in B;
then reconsider As = A\/sf as non empty Subset-Family of X by
XBOOLE_1:8;
A14: Intersect As = meet As by SETFAM_1:def 9
.= meet A /\ meet sf by A13,SETFAM_1:9;
A15: Intersect f = meet f by A13,SETFAM_1:def 9;
thus P[A\/{s}]
proof
per cases;
suppose
A16: Intersect As <> x;
Intersect As in B by A1,A4,A8,A11,A12,A13,A15,A14;
hence thesis by A16;
end;
suppose
Intersect As = x;
hence thesis by A4,A6,A8,A11,A12,A13,A15,A14;
end;
end;
end;
end;
end;
end;
A17: P[{}];
A18: S is finite;
P[S] from FINSET_1:sch 2(A18,A17,A7);
hence thesis by A2,A3,A5,SETFAM_1:def 9;
end;
definition
let n be Element of NAT, p, q be Tuple of n, BOOLEAN;
func p '&' q -> Tuple of n, BOOLEAN means
:Def5:
for i being set st i in Seg n holds it.i = (p/.i) '&' (q/.i);
existence
proof
deffunc F(set) = (p/.$1) '&' (q/.$1);
consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j being Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
z in BOOLEAN* by FINSEQ_1:def 11;
then z in n-tuples_on BOOLEAN by A1;
then reconsider z as Element of n-tuples_on BOOLEAN;
take z;
let i be set;
assume i in Seg n;
hence thesis by A2,A3;
end;
uniqueness
proof
let it1, it2 be Tuple of n, BOOLEAN such that
A4: for i being set st i in Seg n holds it1.i = (p/.i) '&' (q/.i) and
A5: for i being set st i in Seg n holds it2.i = (p/.i) '&' (q/.i);
now
A6: dom it1 = Seg n by Lm1;
hence dom it1 = dom it2 by Lm1;
let x be object;
assume
A7: x in dom it1;
hence it1.x = (p/.x) '&' (q/.x) by A4,A6
.=it2.x by A5,A6,A7;
end;
hence thesis by FUNCT_1:2;
end;
commutativity;
end;
theorem Th5:
for n being Element of NAT, p being Element of n-tuples_on BOOLEAN holds (n
-BinarySequence 0) '&' p = n-BinarySequence 0
proof
let n be Element of NAT, p be Element of n-tuples_on BOOLEAN;
set B = n-BinarySequence 0;
now
let x be object;
A1: dom B = Seg n by Lm1;
A2: dom (B '&' p) = Seg n by Lm1;
hence dom (B '&' p) = dom B by Lm1;
let x be object;
assume
A3: x in dom (B '&' p);
A4: B = 0*n by BINARI_3:25
.= n |-> 0 by EUCLID:def 4;
then B.x = 0;
then B/.x = FALSE by A2,A3,A1,PARTFUN1:def 6;
hence (B '&' p).x = FALSE '&' (p/.x) by A2,A3,Def5
.= B.x by A4;
end;
hence thesis by FUNCT_1:2;
end;
theorem
for n being Element of NAT, p being Tuple of n, BOOLEAN holds 'not' (n
-BinarySequence 0) '&' p = p
proof
let n be Element of NAT, p be Tuple of n, BOOLEAN;
set B = n-BinarySequence 0;
set nB = 'not' B;
now
let x be set;
A1: dom B = Seg n by Lm1;
A2: dom (nB '&' p) = Seg n by Lm1;
hence
A3: dom (nB '&' p) = dom p by Lm1;
let x be object;
assume
A4: x in dom (nB '&' p);
then reconsider k=x as Element of NAT;
B = 0*n by BINARI_3:25
.= n |-> 0 by EUCLID:def 4;
then B.x = 0;
then
A5: B/.x = FALSE by A2,A4,A1,PARTFUN1:def 6;
nB/.x = 'not' (B/.k) by A2,A4,BINARITH:def 1
.= TRUE by A5;
hence (nB '&' p).x = TRUE '&' (p/.x) by A2,A4,Def5
.= p.x by A3,A4,PARTFUN1:def 6;
end;
hence thesis by FUNCT_1:2;
end;
theorem Th7:
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
proof
let n, i be Element of NAT;
assume
A1: i < n;
deffunc B(Nat) = $1-BinarySequence 2 to_power i;
set B = n-BinarySequence 2 to_power i;
defpred P[Nat] means i < $1 implies B($1).(i+1) = TRUE;
A2: now
let n be Nat such that
A3: P[n];
now
assume
A4: i < n+1;
then
A5: i <= n by NAT_1:13;
A6: n in NAT by ORDINAL1:def 12;
per cases by A5,XXREAL_0:1;
suppose
A7: n = 0;
0*n = n |-> 0 by EUCLID:def 4;
then dom 0*n =Seg n;
then
A8: len 0*n = n by FINSEQ_1:def 3,A6;
dom <*TRUE*> =Seg 1 by FINSEQ_1:38;
then
A9: 1 in dom <*TRUE*> by FINSEQ_1:1;
A10: i = 0 by A4,A7,NAT_1:13;
hence B(n+1).(i+1) = (0*n^<*TRUE*>).(i+1) by A7,BINARI_3:28
.= <*TRUE*>.1 by A7,A10,A8,A9,FINSEQ_1:def 7
.= TRUE by FINSEQ_1:40;
end;
suppose
A11: n > 0 & n = i;
0*n = n |-> 0 by EUCLID:def 4;
then dom 0*n = Seg n;
then
A12: len 0*n = n by FINSEQ_1:def 3,A6;
dom <*TRUE*> = Seg 1 by FINSEQ_1:38;
then
A13: 1 in dom <*TRUE*> by FINSEQ_1:1;
thus B(n+1).(i+1) = (0*n^<*TRUE*>).(i+1) by A11,BINARI_3:28
.= <*TRUE*>.1 by A11,A12,A13,FINSEQ_1:def 7
.= TRUE by FINSEQ_1:40;
end;
suppose
A14: n > 0 & n > i;
then reconsider n9 = n as non zero Nat;
A15: 0+1 <= i+1 by XREAL_1:6;
i+1 <= n by A14,NAT_1:13;
then i+1 in Seg n by A15,FINSEQ_1:1;
then
A16: i+1 in dom B(n) by Lm1;
2 to_power i < 2 to_power n by A14,POWER:39;
hence B(n+1).(i+1) = (B(n9)^<*FALSE*>).(i+1) by BINARI_3:27
.= TRUE by A3,A14,A16,FINSEQ_1:def 7;
end;
end;
hence P[n+1];
end;
A17: P[ 0 ];
for n being Nat holds P[n] from NAT_1:sch 2(A17,A2);
hence B.(i+1) = 1 by A1;
defpred P[Nat] means
i < $1 implies for j being Element of NAT st
i+1 <=j & j <= $1 holds B($1).(j+1)= FALSE;
let j be Element of NAT such that
A18: j in Seg n and
A19: j<>i+1;
A20: 1 <= j by A18,FINSEQ_1:1;
A21: now
let n be Nat such that
A22: P[n];
now
assume i < n+1;
then
A23: i <= n by NAT_1:13;
A24: 0+1 <= i+1 by XREAL_1:6;
let j be Element of NAT such that
A25: i+1 <=j and
A26: j <= n+1;
per cases by A23,XXREAL_0:1;
suppose
A27: n = 0;
1 <= j by A25,A24,XXREAL_0:2;
then
A28: j = 1 by A26,A27,XXREAL_0:1;
dom B(n+1) = Seg (n+1) by Lm1;
then not j+1 in dom B(n+1) by A27,A28,FINSEQ_1:1;
hence B(n+1).(j+1) = FALSE by FUNCT_1:def 2;
end;
suppose
A29: n > 0 & n = i;
A30: dom B(n+1) = Seg (n+1) by Lm1;
j+1 > n+1 by A25,A29,NAT_1:13;
then not j+1 in dom B(n+1) by A30,FINSEQ_1:1;
hence B(n+1).(j+1) = FALSE by FUNCT_1:def 2;
end;
suppose
A31: n > 0 & n > i;
then reconsider n9 = n as non zero Nat;
A32: 2 to_power i < 2 to_power n by A31,POWER:39;
thus B(n+1).(j+1) = FALSE
proof
j<n+1 or j=n+1 by A26,XXREAL_0:1;
then
A33: j <= n or j = n+1 by NAT_1:13;
per cases by A33,XXREAL_0:1;
suppose
j = n+1;
then
A34: j+1 > n+1 by NAT_1:13;
dom B(n+1) = Seg (n+1) by Lm1;
then not j+1 in dom B(n+1) by A34,FINSEQ_1:1;
hence thesis by FUNCT_1:def 2;
end;
suppose
A35: j = n;
dom B(n) = Seg n by Lm1;
then
A36: j = len B(n) by A35,FINSEQ_1:def 3;
dom <*FALSE*> = Seg 1 by FINSEQ_1:38;
then
A37: 1 in dom <*FALSE*> by FINSEQ_1:1;
thus B(n+1).(j+1) = (B(n9)^<*FALSE*>).(j+1) by A32,BINARI_3:27
.= <*FALSE*>.1 by A36,A37,FINSEQ_1:def 7
.= FALSE by FINSEQ_1:40;
end;
suppose
A38: j < n;
A39: 1 <= j+1 by NAT_1:12;
j+1 <= n by A38,NAT_1:13;
then j+1 in Seg n by A39,FINSEQ_1:1;
then
A40: j+1 in dom B(n) by Lm1;
thus B(n+1).(j+1) = (B(n9)^<*FALSE*>).(j+1) by A32,BINARI_3:27
.= B(n).(j+1) by A40,FINSEQ_1:def 7
.= FALSE by A22,A25,A31,A38;
end;
end;
end;
end;
hence P[n+1];
end;
A41: P[ 0 ];
A42: for n being Nat holds P[n] from NAT_1:sch 2(A41,A21);
defpred P[Nat] means
i < $1 implies for j being Element of NAT st
1 <=j & j < i+1 holds B($1).j = FALSE;
A43: now
let n be Nat such that
A44: P[n];
now
assume
A45: i < n+1;
then
A46: i <= n by NAT_1:13;
let j be Element of NAT such that
A47: 1 <=j and
A48: j < i+1;
per cases by A46,XXREAL_0:1;
suppose
n = 0;
then i = 0 by A45,NAT_1:13;
hence B(n+1).j = FALSE by A47,A48;
end;
suppose
A49: n > 0 & i < n;
then reconsider n9 = n as non zero Nat;
A50: dom B(n) = Seg n by Lm1;
A51: i <= n by A45,NAT_1:13;
j <= i by A48,NAT_1:13;
then j <= n by A51,XXREAL_0:2;
then
A52: j in dom B(n) by A47,A50,FINSEQ_1:1;
2 to_power i < 2 to_power n by A49,POWER:39;
hence B(n+1).j = (B(n9)^<*FALSE*>).j by BINARI_3:27
.= B(n).j by A52,FINSEQ_1:def 7
.= FALSE by A44,A47,A48,A49;
end;
suppose
A53: n > 0 & i = n;
then j <= n by A48,NAT_1:13;
then
A54: j in Seg n by A47,FINSEQ_1:1;
A55: 0*n = n |-> 0 by EUCLID:def 4;
then
A56: j in dom 0*n by A54;
thus B(n+1).j = (0*n^<*TRUE*>).j by A53,BINARI_3:28
.= (0*n).j by A56,FINSEQ_1:def 7
.= FALSE by A55;
end;
end;
hence P[n+1];
end;
A57: P[ 0 ];
A58: for n being Nat holds P[n] from NAT_1:sch 2(A57,A43);
A59: j <= n by A18,FINSEQ_1:1;
per cases by A19,A59,XXREAL_0:1;
suppose
j < i+1;
hence thesis by A1,A58,A20;
end;
suppose
A60: j > i+1 & j < n;
then consider k being Nat such that
A61: j = k+1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
A62: k <= n by A60,A61,NAT_1:13;
i+1 <= k by A60,A61,NAT_1:13;
hence thesis by A1,A42,A61,A62;
end;
suppose
A63: j > i+1 & j = n;
then consider m being Nat such that
A64: n = m+1 by NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
i < m by A63,A64,XREAL_1:6;
then 2 to_power i < 2 to_power m by POWER:39;
hence thesis by A63,A64,BINARI_3:26;
end;
end;
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;
existence
proof
{} c= X;
then reconsider R = {[{},{}]} as Relation of bool X by RELSET_1:3;
take R;
thus R is non empty;
thus thesis;
end;
end;
definition
let X be set;
func Dependencies(X) -> Dependency-set of X equals
[: bool X, bool X :];
coherence;
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;
coherence;
end;
definition
let X be set, F be non empty Dependency-set of X;
redefine mode Element of F -> Dependency of X; :: redefines Element (SUBSET_1, definition)
correctness
proof
let x be Element of F;
thus thesis;
end;
end;
theorem Th8:
for X, x being set holds x in Dependencies X iff ex a, b being
Subset of X st x = [a,b]
proof
let X be set, x be set;
hereby
assume
A1: x in Dependencies X;
then consider a, b being object such that
A2: [a, b] = x by RELAT_1:def 1;
reconsider a, b as Subset of X by A1,A2,ZFMISC_1:87;
take a,b;
thus x = [a,b] by A2;
end;
given a, b being Subset of X such that
A3: x = [a,b];
thus thesis by A3,ZFMISC_1:87;
end;
theorem Th9:
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]
proof
let X, x be set, M be Dependency-set of X;
assume
A1: x in M;
then consider a, b being object such that
A2: [a, b] = x by RELAT_1:def 1;
reconsider a, b as Subset of X by A1,A2,ZFMISC_1:87;
take a,b;
thus thesis by A2;
end;
definition
let R be DB-Rel, A, B be Subset of the Attributes of R;
pred A >|> B, R means
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
{ [A,
B] where A, B is Subset of the Attributes of R: A >|> B, R };
coherence
proof
set att = the Attributes of R;
set X = {[A,B] where A,B is Subset of the Attributes of R: A >|> B, R};
X c= [:bool att, bool att:]
proof
let x be object;
assume x in X;
then ex A, B being Subset of att st x = [A, B] & A >|> B, R;
hence thesis by ZFMISC_1:def 2;
end;
hence thesis;
end;
end;
theorem Th10:
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
proof
let D be DB-Rel, A, B be Subset of the Attributes of D;
set S = Dependency-str D;
hereby
assume [A, B] in S;
then consider a, b being Subset of the Attributes of D such that
A1: [A, B] = [a, b] and
A2: a >|> b, D;
A = a by A1,XTUPLE_0:1;
hence A >|> B, D by A1,A2,XTUPLE_0:1;
end;
thus thesis;
end;
begin :: 4. Full families of dependencies
definition
let X be set, P, Q be Dependency of X;
pred P >= Q means
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 Th11: :: antisymmetry
for X being set, P, Q being Dependency of X st P <= Q & Q <= P holds P = Q
proof
let X be set, p, q be Dependency of X;
assume that
A1: p <= q and
A2: q <= p;
A3: q`1 c= p`1 by A1;
A4: p`2 c= q`2 by A1;
q`2 c= p`2 by A2;
then
A5: p`2 = q`2 by A4,XBOOLE_0:def 10;
p`1 c= q`1 by A2;
then
A6: p`1 = q`1 by A3,XBOOLE_0:def 10;
p = [p`1,p`2] by MCART_1:22;
hence thesis by A6,A5,MCART_1:22;
end;
theorem Th12: :: transitivity
for X being set, P, Q, S being Dependency of X st P <= Q & Q <=
S holds P <= S
proof
let X be set, p, q, r be Dependency of X;
assume that
A1: p <= q and
A2: q <= r;
A3: q`2 c= r`2 by A2;
p`2 c= q`2 by A1;
then
A4: p`2 c= r`2 by A3;
A5: r`1 c= q`1 by A2;
q`1 c= p`1 by A1;
then r`1 c= p`1 by A5;
hence thesis by A4;
end;
definition
let X be set, A, B be Subset of X;
redefine func [A, B] -> Dependency of X; :: redefines [ (TARSKI, definition)
coherence by ZFMISC_1:def 2;
end;
theorem
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
{ [P, Q]
where P, Q is Dependency of X : P <= Q };
coherence
proof
set Y = { [E, F] where E, F is Dependency of X : E <= F };
Y c= [: Dependencies X, Dependencies X :]
proof
let x be object;
assume x in Y;
then ex E, F being Dependency of X st x = [E, F] & E <= F;
hence thesis by ZFMISC_1:def 2;
end;
hence thesis;
end;
end;
theorem
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 Th15:
for X being set holds dom Dependencies-Order X = [: bool X, bool X :]
proof
let X be set;
now
let x be object;
thus x in dom Dependencies-Order X implies x in [: bool X, bool X :];
assume x in [: bool X, bool X :];
then reconsider x9 = x as Dependency of X;
[x9, x9] in Dependencies-Order X;
hence x in dom Dependencies-Order X by XTUPLE_0:def 12;
end;
hence thesis by TARSKI:2;
end;
theorem Th16:
for X being set holds rng Dependencies-Order X = [: bool X, bool X :]
proof
let X be set;
now
let x be object;
thus x in rng Dependencies-Order X implies x in [: bool X, bool X :];
assume x in [: bool X, bool X :];
then reconsider x9 = x as Dependency of X;
[x9, x9] in Dependencies-Order X;
hence x in rng Dependencies-Order X by XTUPLE_0:def 13;
end;
hence thesis by TARSKI:2;
end;
theorem Th17:
for X being set holds field Dependencies-Order X = [: bool X, bool X :]
proof
let X be set;
thus field Dependencies-Order X = dom Dependencies-Order X\/rng
Dependencies-Order X by RELAT_1:def 6
.= [: bool X, bool X :]\/rng Dependencies-Order X by Th15
.= [: bool X, bool X :]\/[: bool X, bool X :] by Th16
.= [: bool X, bool X :];
end;
registration
let X be set;
cluster Dependencies-Order X -> non empty;
coherence by Th15,RELAT_1:38;
cluster Dependencies-Order X -> total reflexive antisymmetric transitive;
coherence
proof
set dx = Dependencies X;
set dox = Dependencies-Order X;
dx c= dom dox
proof
let x be object;
assume x in dx;
then reconsider x9 = x as Element of dx;
x9 <= x9;
then [x,x] in dox;
hence thesis by XTUPLE_0:def 12;
end;
then
A1: dom dox = dx by XBOOLE_0:def 10;
then
A2: field dox = dx \/ rng dox by RELAT_1:def 6
.= dx by XBOOLE_1:12;
thus dox is total by A1,PARTFUN1:def 2;
dox is_reflexive_in dx;
hence dox is reflexive by A2;
dox is_antisymmetric_in dx
proof
let x, y be object;
assume that
x in dx and
y in dx and
A3: [x,y] in dox and
A4: [y,x] in dox;
consider x9, y9 being Element of dx such that
A5: [x,y]=[x9,y9] and
A6: x9 <= y9 by A3;
A7: y = y9 by A5,XTUPLE_0:1;
consider y99, x99 being Element of dx such that
A8: [y,x]=[y99,x99] and
A9: y99 <= x99 by A4;
A10: x = x99 by A8,XTUPLE_0:1;
A11: y = y99 by A8,XTUPLE_0:1;
x = x9 by A5,XTUPLE_0:1;
hence thesis by A6,A9,A10,A7,A11,Th11;
end;
hence dox is antisymmetric by A2;
dox is_transitive_in dx
proof
let x, y, z be object;
assume that
x in dx and
y in dx and
z in dx and
A12: [x,y] in dox and
A13: [y,z] in dox;
consider x9, y9 being Element of dx such that
A14: [x,y]=[x9,y9] and
A15: x9 <= y9 by A12;
A16: x = x9 by A14,XTUPLE_0:1;
consider y99, z9 being Element of dx such that
A17: [y,z]=[y99,z9] and
A18: y99 <= z9 by A13;
A19: y = y99 by A17,XTUPLE_0:1;
A20: z = z9 by A17,XTUPLE_0:1;
y = y9 by A14,XTUPLE_0:1;
then x9 <= z9 by A15,A18,A19,Th12;
hence thesis by A16,A20;
end;
hence thesis by A2;
end;
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
: Def11:
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 Th18:
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
proof
let X be set, F be Dependency-set of X;
hereby
assume F is (F2);
then
A1: F is_transitive_in field F;
let A, B, C be Subset of X;
assume that
A2: [A, B] in F and
A3: [B, C] in F;
A4: B in field F by A2,RELAT_1:15;
A5: C in field F by A3,RELAT_1:15;
A in field F by A2,RELAT_1:15;
hence [A, C] in F by A1,A2,A3,A4,A5;
end;
assume
A6: for A,B,C being Subset of X st [A, B] in F & [B, C] in F holds [A, C
] in F;
let x, y, z be object such that
A7: x in field F and
A8: y in field F and
A9: z in field F and
A10: [x,y] in F and
A11: [y,z] in F;
field F c= bool X\/bool X by RELSET_1:8;
then reconsider A = x, B = y, C = z as Subset of X by A7,A8,A9;
A12: [B, C] in F by A11;
[A, B] in F by A10;
hence thesis by A6,A12;
end;
definition
let X be set, F be Dependency-set of X;
attr F is (F3) means
: Def12:
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
: Def13:
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 Th19:
for X being set holds Dependencies X is (F1) (F2) (F3) (F4)
proof
let X be set;
set D = Dependencies X;
thus D is (F1);
D = nabla bool X by EQREL_1:def 1;
then
A1: field D = bool X by ORDERS_1:12;
thus D is (F2)
proof
let x, y, z be object;
assume that
A2: x in field D and
y in field D and
A3: z in field D and
[x,y] in D and
[y,z] in D;
thus thesis by A1,A2,A3,ZFMISC_1:def 2;
end;
thus D is (F3);
thus D is (F4);
end;
registration
let X be set;
cluster (F1) (F2) (F3) (F4) non empty for Dependency-set of X;
existence
proof
take Dependencies X;
thus thesis by Th19;
end;
end;
definition
let X be set, F be Dependency-set of X;
attr F is full_family means
: Def14:
F is (F1) (F2) (F3) (F4);
end;
registration
let X be set;
cluster full_family for Dependency-set of X;
existence
proof
set D = the (F1) (F2) (F3) (F4) non empty Dependency-set of X;
take D;
thus thesis;
end;
end;
definition
let X be set;
mode Full-family of X is full_family Dependency-set of X;
end;
theorem
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;
existence
proof
set D = the (F1) (F2) (F3) (F4) non empty Dependency-set of X;
reconsider D as Full-family of X by Def14;
take D;
thus thesis;
end;
cluster -> finite for Dependency-set of X;
coherence;
end;
registration
let X be set;
cluster full_family -> (F1) (F2) (F3) (F4) for Dependency-set of X;
coherence;
cluster (F1) (F2) (F3) (F4) -> full_family for Dependency-set of X;
correctness;
end;
definition
let X be set, F be Dependency-set of X;
attr F is (DC3) means
:Def15:
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;
coherence
proof
let F be Dependency-set of X;
assume
A1: F is (F1) (F3);
let A, B being Subset of X;
assume B c= A;
then
A2: [A, A] >= [A, B];
thus thesis by A1,A2;
end;
cluster (DC3) (F2) -> (F1) (F3) for Dependency-set of X;
coherence
proof
let F be Dependency-set of X;
assume
A3: F is (DC3) (F2);
thus F is (F1)
by A3;
let A, B, A9, B9 be Subset of X;
assume
A4: [A, B] in F;
assume
A5: [A, B] >= [A9, B9];
then A c= A9;
then [A9, A] in F by A3;
then
A6: [A9, B] in F by A3,A4,Th18;
B9 c= B by A5;
then [B, B9] in F by A3;
hence thesis by A3,A6,Th18;
end;
end;
registration
let X be set;
cluster (DC3) (F2) (F4) non empty for Dependency-set of X;
existence
proof
set D = the (F1) (F3) (F2) (F4) non empty Dependency-set of X;
take D;
thus thesis;
end;
end;
theorem :: 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 :: 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;
coherence;
end;
theorem Th23: :: WWA1:
for R being DB-Rel holds Dependency-str R is full_family
proof
let D be DB-Rel;
set S = Dependency-str D;
set T = the Attributes of D, R = the Relationship of D;
A1: now
let A, B, C being Subset of T;
assume that
A2: [A, B] in S and
A3: [B, C] in S;
A4: B >|> C, D by A3,Th10;
A5: A >|> B, D by A2,Th10;
A >|> C, D
proof
let f, g being Element of R;
assume f|A = g|A;
then f|B = g|B by A5;
hence thesis by A4;
end;
hence [A, C] in S;
end;
then
A6: S is (F2) by Th18;
A7: S is (DC3)
proof
let A, B being Subset of T such that
A8: B c= A;
A >|> B, D
proof
let f, g being Element of R such that
A9: f|A = g|A;
thus f|B = (f|A)|B by A8,RELAT_1:74
.= g|B by A8,A9,RELAT_1:74;
end;
hence thesis;
end;
hence S is (F1);
thus S is (F2) by A1,Th18;
thus S is (F3) by A7,A6;
thus S is (F4)
proof
let A, B, A9, B9 being Subset of T;
assume that
A10: [A, B] in S and
A11: [A9, B9] in S;
A12: A9 >|> B9, D by A11,Th10;
A13: A >|> B, D by A10,Th10;
(A\/A9) >|> (B\/B9), D
proof
let f, g be Element of R;
assume
A14: f|(A\/A9) = g|(A\/A9);
f|A9=(f|(A\/A9))|A9 by RELAT_1:74,XBOOLE_1:7
.=g|A9 by A14,RELAT_1:74,XBOOLE_1:7;
then
A15: f|B9 = g|B9 by A12;
f|A=(f|(A\/A9))|A by RELAT_1:74,XBOOLE_1:7
.=g|A by A14,RELAT_1:74,XBOOLE_1:7;
then
A16: f|B = g|B by A13;
thus f|(B\/B9)=f|B\/f|B9 by RELAT_1:78
.= g|(B\/B9) by A16,A15,RELAT_1:78;
end;
hence thesis;
end;
end;
theorem :: 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
proof
let X be set, K be Subset of X;
set F = { [A, B] where A, B is Subset of X : K c= A or B c= A };
F c= [:bool X, bool X:]
proof
let x be object;
assume x in F;
then ex A, B being Subset of X st x = [A, B] & (K c= A or B c= A);
hence thesis;
end;
then reconsider F as Dependency-set of X;
A1: F is (F4)
proof
let A, B, A9, B9 be Subset of X;
assume that
A2: [A, B] in F and
A3: [A9, B9] in F;
consider a, b being Subset of X such that
A4: [A, B] = [a, b] and
A5: K c= a or b c= a by A2;
A6: B = b by A4,XTUPLE_0:1;
consider a9, b9 being Subset of X such that
A7: [A9, B9] = [a9, b9] and
A8: K c= a9 or b9 c= a9 by A3;
A9: A9 = a9 by A7,XTUPLE_0:1;
A10: B9 = b9 by A7,XTUPLE_0:1;
A = a by A4,XTUPLE_0:1;
then K c= A\/A9 or B\/B9 c= A\/A9 by A5,A8,A6,A9,A10,XBOOLE_1:10,13;
hence thesis;
end;
now
let A, B, C be Subset of X;
assume that
A11: [A, B] in F and
A12: [B, C] in F;
consider a, b being Subset of X such that
A13: [A, B] = [a, b] and
A14: K c= a or b c= a by A11;
A15: A = a by A13,XTUPLE_0:1;
consider b1, c being Subset of X such that
A16: [B, C] = [b1, c] and
A17: K c= b1 or c c= b1 by A12;
A18: B = b1 by A16,XTUPLE_0:1;
A19: C = c by A16,XTUPLE_0:1;
B = b by A13,XTUPLE_0:1;
then K c= a or c c= a by A14,A17,A18;
hence [A, C] in F by A15,A19;
end;
then
A20: F is (F2) by Th18;
F is (DC3);
hence thesis by A20,A1;
end;
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
Dependencies-Order X
Maximal_in F;
coherence by RELSET_1:1;
end;
theorem
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
[x, y] in Maximal_wrt F;
end;
theorem Th26:
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
proof
let X be finite set,x be Dependency of X,F be Dependency-set of X;
set DOX = Dependencies-Order X;
assume
A1: x in F;
then reconsider FF= F as non empty Dependency-set of X;
reconsider S = { y where y is Element of FF: x <= y } as set;
A2: field DOX = [:bool X, bool X:] by Th17;
A3: S c= field DOX
proof
let a be object;
assume a in S;
then ex b be Element of FF st a = b & x <= b;
hence thesis by A2;
end;
x in S by A1;
then consider m being Element of S such that
A4: m is_maximal_wrt S, DOX by A3,Th2;
m in S by A4;
then
A5: ex y being Element of FF st m = y & x <= y;
then consider a, b being Subset of X such that
A6: m = [a, b] by Th8;
take a, b;
m is_maximal_wrt F, DOX
proof
thus m in F by A5;
given y being set such that
A7: y in F and
A8: y <> m and
A9: [m, y] in DOX;
consider e, f being Dependency of X such that
A10: [m, y] = [e, f] and
A11: e <= f by A9;
reconsider y as Element of FF by A7;
A12: y = f by A10,XTUPLE_0:1;
m = e by A10,XTUPLE_0:1;
then x <= y by A5,A11,A12,Th12;
then y in S;
hence contradiction by A4,A8,A9;
end;
hence [a,b] in Maximal_wrt F by A6,Def1;
thus thesis by A5,A6;
end;
theorem Th27:
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]
proof
let X be set, F be Dependency-set of X, x, y be Subset of X;
set DOX = Dependencies-Order X;
hereby
assume x ^|^ y, F;
then
A1: [x, y] in Maximal_wrt F;
hence [x, y] in F;
A2: [x, y] is_maximal_wrt F, DOX by A1,Def1;
given x9, y9 being Subset of X such that
A3: [x9, y9] in F and
A4: x <> x9 or y <> y9 and
A5: [x, y] <= [x9,y9];
A6: [[x,y],[x9,y9]] in DOX by A5;
[x,y] <> [x9,y9] by A4,XTUPLE_0:1;
hence contradiction by A2,A3,A6;
end;
assume that
A7: [x, y] in F and
A8: not ex x9, y9 being Subset of X st [x9, y9] in F & (x <> x9 or y <>
y9) & [x, y] <= [x9,y9];
[x,y] is_maximal_wrt F, DOX
proof
thus [x,y] in F by A7;
given z being set such that
A9: z in F and
A10: z <> [x,y] and
A11: [[x, y],z] in DOX;
consider x9,y9 being object such that
A12: z = [x9,y9] and
A13: x9 in bool X and
A14: y9 in bool X by A9,RELSET_1:2;
consider e, f being Dependency of X such that
A15: [[x, y],z] = [e, f] and
A16: e <= f by A11;
A17: e = [x,y] by A15,XTUPLE_0:1;
A18: f = z by A15,XTUPLE_0:1;
reconsider x9, y9 as Subset of X by A13,A14;
x <> x9 or y <> y9 by A10,A12;
hence contradiction by A8,A9,A12,A13,A14,A16,A17,A18;
end;
then [x,y] in Maximal_wrt F by Def1;
hence thesis;
end;
definition
let X be set, M be Dependency-set of X;
attr M is (M1) means
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
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
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 Th28: :: WWA2:
for X being finite non empty set, F being Full-family of X holds
Maximal_wrt F is (M1) (M2) (M3)
proof
let X be finite non empty set, F be full_family Dependency-set of X;
set DOX = Dependencies-Order X;
set MEF = Maximal_wrt F;
thus Maximal_wrt F is (M1)
proof
A1: field DOX = [:bool X, bool X:] by Th17;
let A be Subset of X;
defpred P[object] means
ex y being Dependency of X st $1 = y & y >= [A,A];
consider MA being set such that
A2: for x being object holds x in MA iff x in F & P[x] from XBOOLE_0:sch
1;
MA c= F
by A2;
then
A3: MA is finite Subset of field DOX by A1,XBOOLE_1:1;
[A, A] in F by Def15;
then MA <> {} by A2;
then consider x being Element of MA such that
A4: x is_maximal_wrt MA, DOX by A3,Th2;
A5: x in MA by A4;
then x in F by A2;
then consider A9, B9 being object such that
A6: A9 in bool X and
A7: B9 in bool X and
A8: x = [A9,B9] by ZFMISC_1:def 2;
reconsider A9, B9 as Subset of X by A6,A7;
take A9, B9;
A9: ex y being Dependency of X st x = y & y >= [A,A] by A2,A5;
hence [A9, B9] >= [A, A] by A8;
x is_maximal_wrt F, DOX
proof
thus x in F by A2,A5;
given z being set such that
A10: z in F and
A11: z <> x and
A12: [x, z] in DOX;
consider e, f being Dependency of X such that
A13: [x,z] = [e, f] and
A14: e <= f by A12;
x = e by A13,XTUPLE_0:1;
then
A15: f >= [A,A] by A9,A14,Th12;
z = f by A13,XTUPLE_0:1;
then z in MA by A2,A10,A15;
hence contradiction by A4,A11,A12;
end;
hence thesis by A8,Def1;
end;
thus Maximal_wrt F is (M2)
proof
let A, B, A9, B9 be Subset of X such that
A16: [A, B] in MEF and
A17: [A9, B9] in MEF and
A18: [A, B] >= [A9, B9];
A19: [[A9,B9], [A, B]] in DOX by A18;
assume not (A = A9 & B = B9);
then
A20: [A, B] <> [A9,B9] by XTUPLE_0:1;
[A9, B9] is_maximal_wrt F, DOX by A17,Def1;
hence contradiction by A16,A20,A19;
end;
thus Maximal_wrt F is (M3)
proof
let A, B, A9, B9 be Subset of X;
assume that
A21: [A, B] in MEF and
A22: [A9, B9] in MEF and
A23: A9 c= B;
A24: A ^|^ B, F by A21;
[A9,B9] >= [B,B9] by A23;
then [ B, B9] in F by A22,Def12;
then
A25: [ A, B9] in F by A21,Th18;
B c= B\/B9 by XBOOLE_1:7;
then
A26: [A,B\/B9] >= [A,B];
A\/A = A;
then [A, B\/B9] in F by A21,A25,Def13;
then B\/B9 = B by A24,A26,Th27;
hence thesis by XBOOLE_1:11;
end;
end;
theorem Th29: :: 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
proof
let X be finite set, M be Dependency-set of X, F be Dependency-set of X;
assume that
A1: M is (M1) (M2) (M3) and
A2: 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};
A3: F is (F1)
proof
let A be Subset of X;
ex A9, B9 being Subset of X st [A9, B9] >= [A, A] & [A9, B9] in M
by A1;
hence thesis by A2;
end;
A4: now
let x be set;
assume x in F;
then consider a, b being Subset of X such that
A5: x = [a,b] and
A6: ex a9, b9 being Subset of X st [a9, b9] >= [a, b] & [a9, b9] in M by A2;
consider a9, b9 being Subset of X such that
A7: [a9, b9] >= [a, b] and
A8: [a9, b9] in M by A6;
take a, b, a9, b9;
thus x = [a,b] & [a9, b9] >= [a, b] & [a9, b9] in M by A5,A7,A8;
end;
A9: now
let A, B be Subset of X;
assume [A,B] in F;
then consider a, b, a9, b9 being Subset of X such that
A10: [A,B] = [a,b] and
A11: [a9, b9] >= [a, b] and
A12: [a9, b9] in M by A4;
take a9, b9;
thus [a9, b9] >= [A, B] & [a9, b9] in M by A10,A11,A12;
end;
now
let A, B, C be Subset of X;
assume that
A13: [A, B] in F and
A14: [B, C] in F;
consider A9, B9 being Subset of X such that
A15: [A9, B9] >= [A, B] and
A16: [A9, B9] in M by A9,A13;
consider B19, C9 being Subset of X such that
A17: [B19, C9] >= [B, C] and
A18: [B19, C9] in M by A9,A14;
A19: B19 c= B by A17;
B c= B9 by A15;
then B19 c= B9 by A19;
then C9 c= B9 by A1,A16,A18;
then
A20: [A9, B9] >= [A9, C9];
A21: C c= C9 by A17;
A9 c= A by A15;
then [A9,C9] >= [A, C] by A21;
then [A9,B9] >= [A, C] by A20,Th12;
hence [A, C] in F by A2,A16;
end;
then
A22: F is (F2) by Th18;
A23: F is (F4)
proof
let A, B, A9, B9 be Subset of X such that
A24: [A, B] in F and
A25: [A9, B9] in F;
consider a1, b1 being Subset of X such that
A26: [a1, b1] >= [A, B] and
A27: [a1, b1] in M by A9,A24;
A28: B c= b1 by A26;
consider a19,b19 being Subset of X such that
A29: [a19, b19] >= [A9, B9] and
A30: [a19, b19] in M by A9,A25;
A31: B9 c= b19 by A29;
consider A99, B99 being Subset of X such that
A32: [A99, B99] >= [A\/A9, A\/A9] and
A33: [A99, B99] in M by A1;
A34: A\/A9 c= B99 by A32;
a19 c= A9 by A29;
then a19 c= A\/A9 by XBOOLE_1:10;
then a19 c= B99 by A34;
then b19 c= B99 by A1,A33,A30;
then
A35: B9 c= B99 by A31;
a1 c= A by A26;
then a1 c= A\/A9 by XBOOLE_1:10;
then a1 c= B99 by A34;
then b1 c= B99 by A1,A33,A27;
then B c= B99 by A28;
then
A36: B\/B9 c= B99\/B99 by A35,XBOOLE_1:13;
A99 c= A\/A9 by A32;
then [A99,B99] >= [A\/A9,B\/B9] by A36;
hence thesis by A2,A33;
end;
set DOX = Dependencies-Order X;
now
let x be object;
hereby
assume
A37: x in M;
then consider a, b being Subset of X such that
A38: x = [a,b] by Th9;
x is_maximal_wrt F, DOX
proof
thus x in F by A2,A37,A38;
given y being set such that
A39: y in F and
A40: y <> x and
A41: [x, y] in DOX;
consider e, f being Dependency of X such that
A42: [x,y] = [e, f] and
A43: e <= f by A41;
A44: y = f by A42,XTUPLE_0:1;
consider c, d, c9, d9 being Subset of X such that
A45: y = [c,d] and
A46: [c9,d9] >= [c,d] and
A47: [c9,d9] in M by A4,A39;
A48: x = e by A42,XTUPLE_0:1;
then
A49: [c9,d9] >= [a,b] by A38,A43,A44,A45,A46,Th12;
then
A50: d9 = b by A1,A37,A38,A47;
c9 = a by A1,A37,A38,A47,A49;
hence contradiction by A38,A40,A43,A48,A44,A45,A46,A50,Th11;
end;
hence x in Maximal_wrt F by Def1;
end;
assume
A51: x in Maximal_wrt F;
then
A52: x is_maximal_wrt F, DOX by Def1;
assume
A53: not x in M;
consider a,b,a9,b9 being Subset of X such that
A54: x = [a,b] and
A55: [a9, b9] >= [a, b] and
A56: [a9, b9] in M by A4,A51;
A57: [[a,b], [a9,b9]] in DOX by A55;
[a9,b9] in F by A2,A56;
hence contradiction by A52,A54,A56,A53,A57;
end;
hence M = Maximal_wrt F by TARSKI:2;
F is (F3)
proof
let A, B, A9, B9 be Subset of X such that
A58: [A, B] in F and
A59: [A, B] >= [A9, B9];
consider a9,b9 being Subset of X such that
A60: [a9, b9] >= [A, B] and
A61: [a9, b9] in M by A9,A58;
[a9,b9] >= [A9,B9] by A59,A60,Th12;
hence thesis by A2,A61;
end;
hence F is full_family by A3,A22,A23;
let G being Full-family of X such that
A62: M = Maximal_wrt G;
now
let x be object;
hereby
A63: field DOX = [:bool X, bool X:] by Th17;
assume
A64: x in G;
then consider a, b being Subset of X such that
A65: x = [a,b] by Th9;
defpred P[object] means
ex y being Dependency of X st $1 = y & y >= [a,b];
consider MA being set such that
A66: for x being object holds x in MA iff x in G & P[x] from XBOOLE_0:
sch 1;
MA c= G
by A66;
then
A67: MA is finite Subset of field DOX by A63,XBOOLE_1:1;
MA <> {} by A64,A65,A66;
then consider m being Element of MA such that
A68: m is_maximal_wrt MA, DOX by A67,Th2;
A69: m in MA by A68;
then m in G by A66;
then
A70: ex a9, b9 being Subset of X st m = [a9,b9] by Th9;
m is_maximal_wrt G, DOX
proof
A71: ex mm being Dependency of X st m = mm & mm >= [a,b] by A66,A69;
thus m in G by A66,A69;
given y being set such that
A72: y in G and
A73: y <> m and
A74: [m, y] in DOX;
consider e, f being Dependency of X such that
A75: [m,y]=[e,f] and
A76: e <= f by A74;
A77: y = f by A75,XTUPLE_0:1;
m = e by A75,XTUPLE_0:1;
then f >= [a,b] by A71,A76,Th12;
then y in MA by A66,A72,A77;
hence contradiction by A68,A73,A74;
end;
then
A78: m in (DOX Maximal_in G) by Def1;
ex y being Dependency of X st m = y & y >= [a,b] by A66,A69;
hence x in F by A2,A62,A65,A78,A70;
end;
assume x in F;
then ex a, b, a1, b1 being Subset of X st x = [a,b] & [a1, b1 ] >= [a,
b] & [a1, b1] in M by A4;
hence x in G by A62,Def12;
end;
hence thesis by TARSKI:2;
end;
registration
let X be non empty finite set, F be Full-family of X;
cluster Maximal_wrt F -> non empty;
coherence
proof
set M = Maximal_wrt F;
M is (M1) by Th28;
then
ex A9,B9 being Subset of X st [A9, B9]>=[[#]X, [#]X]&[A9, B9] in M;
hence thesis;
end;
end;
theorem Th30: :: 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
proof
let X be finite set, F be Dependency-set of X, K be Subset of X;
set M = {[K, X]}\/{[A, A] where A is Subset of X : not K c= A};
A1: {[K,X]} c= M by XBOOLE_1:7;
A2: now
let A be Subset of X;
assume not K c= A;
then
A3: [A,A] in {[a, a] where a is Subset of X : not K c= a};
{[a, a] where a is Subset of X : not K c= a} c= M by XBOOLE_1:7;
hence [A,A] in M by A3;
end;
A4: [#] X = X;
A5: M c= [:bool X, bool X:]
proof
let x be object;
assume
A6: x in M;
per cases by A6,XBOOLE_0:def 3;
suppose
x in {[K, X]};
then x = [K,X] by TARSKI:def 1;
hence thesis by A4,ZFMISC_1:def 2;
end;
suppose
x in {[A, A] where A is Subset of X : not K c= A};
then ex A being Subset of X st x = [A,A] & not K c= A;
hence thesis;
end;
end;
A7: now
let A, B be Subset of X;
assume
A8: [A,B] in M;
per cases by A8,XBOOLE_0:def 3;
suppose
[A,B] in {[K, X]};
hence [A,B] = [K,X] or not K c= A & A = B by TARSKI:def 1;
end;
suppose
[A,B] in {[a, a] where a is Subset of X : not K c= a};
then consider a being Subset of X such that
A9: [A,B] = [a,a] and
A10: not K c= a;
A = a by A9,XTUPLE_0:1;
hence [A,B] = [K,X] or not K c= A & A = B by A9,A10,XTUPLE_0:1;
end;
end;
reconsider M as Dependency-set of X by A5;
set FF = {[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};
A11: FF c= [:bool X, bool X:]
proof
let x be object;
assume x in FF;
then ex A, B being Subset of X st x = [A,B] & ex A9, B9 being Subset of
X st [A9, B9] >= [A, B] & [A9, B9] in M;
hence thesis;
end;
A12: M is (M2)
proof
let A, B, A9, B9 be Subset of X such that
A13: [A, B] in M and
A14: [A9, B9] in M and
A15: [A, B] >= [A9, B9];
A16: A c= A9 by A15;
A17: B9 c= B by A15;
per cases by A7,A13;
suppose
A18: [A,B] = [K,X];
thus A = A9 & B = B9
proof
per cases by A7,A14;
suppose
[A9,B9] = [K,X];
hence thesis by A18,XTUPLE_0:1;
end;
suppose
not K c= A9 & A9 = B9;
hence thesis by A16,A18,XTUPLE_0:1;
end;
end;
end;
suppose
A19: not K c= A & A = B;
thus A = A9 & B = B9
proof
per cases by A7,A14;
suppose
[A9,B9] = [K,X];
then B9 = X by XTUPLE_0:1;
then B = X by A17,XBOOLE_0:def 10;
hence thesis by A19;
end;
suppose
not K c= A9 & A9 = B9;
hence thesis by A16,A17,A19,XBOOLE_0:def 10;
end;
end;
end;
end;
reconsider FF as Dependency-set of X by A11;
assume
A20: F = { [A, B] where A, B is Subset of X : K c= A or B c= A };
A21: now
let x be object;
hereby
A22: {[a, a] where a is Subset of X : not K c= a} c= M by XBOOLE_1:7;
A23: [K,X] in {[K,X]} by TARSKI:def 1;
A24: {[K,X]} c= M by XBOOLE_1:7;
assume x in F;
then consider A, B being Subset of X such that
A25: x = [A,B] and
A26: K c= A or B c= A by A20;
per cases;
suppose
K c= A;
then [K,[#] X] >= [A,B];
hence x in FF by A25,A24,A23;
end;
suppose
A27: not K c= A;
then
A28: [A,A] in {[a, a] where a is Subset of X : not K c= a};
[A,A] >= [A,B] by A26,A27;
hence x in FF by A25,A22,A28;
end;
end;
assume x in FF;
then consider A, B being Subset of X such that
A29: x = [A,B] and
A30: ex A9, B9 being Subset of X st [A9, B9] >= [A, B] & [A9, B9] in M;
consider A9, B9 being Subset of X such that
A31: [A9, B9] >= [A, B] and
A32: [A9, B9] in M by A30;
per cases by A32,XBOOLE_0:def 3;
suppose
[A9,B9] in {[K, X]};
then [A9,B9] = [K,X] by TARSKI:def 1;
then A9 = K by XTUPLE_0:1;
then K c= A by A31;
hence x in F by A20,A29;
end;
suppose
[A9,B9] in {[a, a] where a is Subset of X : not K c= a};
then consider a being Subset of X such that
A33: [A9,B9] = [a,a] and
not K c= a;
A34: A9 = a by A33,XTUPLE_0:1;
A35: B9 = a by A33,XTUPLE_0:1;
A36: B c= B9 by A31;
A9 c= A by A31;
then B c= A by A34,A35,A36;
hence x in F by A20,A29;
end;
end;
A37: M is (M3)
proof
let A, B, A9, B9 be Subset of X such that
A38: [A, B] in M and
A39: [A9, B9] in M and
A40: A9 c= B;
per cases by A7,A38;
suppose
[A,B] = [K,X];
then B = X by XTUPLE_0:1;
hence thesis;
end;
suppose
A41: not K c= A & A = B;
thus B9 c= B
proof
per cases by A7,A39;
suppose
[A9,B9] = [K,X];
hence thesis by A40,A41,XTUPLE_0:1;
end;
suppose
not K c= A9 & A9 = B9;
hence thesis by A40;
end;
end;
end;
end;
A42: [K,X] in {[K,X]} by TARSKI:def 1;
M is (M1)
proof
let A be Subset of X;
per cases;
suppose
A43: K c= A;
take A9 = K, B9 = [#]X;
thus [A9, B9] >= [A, A] by A43;
thus thesis by A42,A1;
end;
suppose
A44: not K c= A;
take A9 = A, B9 = A;
thus [A9, B9] >= [A, A];
thus thesis by A2,A44;
end;
end;
then M = Maximal_wrt FF by A12,A37,Th29;
hence thesis by A21,TARSKI:2;
end;
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
{ B where B is Subset
of X: ex A being Subset of X st A ^|^ B, F };
coherence
proof
set SS = {B where B is Subset of X: ex A being Subset of X st A ^|^B,F};
SS c= bool X
proof
let x be object;
assume x in SS;
then
ex B being Subset of X st x = B & ex A being Subset of X st A ^|^ B, F;
hence thesis;
end;
hence thesis;
end;
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;
coherence
proof
defpred P[object,object] means
ex a,b being object st $1 = [a,b] & $2 = [a,b]`2;
:: projekcja ??? !!!
set ss = {B where B is Subset of X: ex A being Subset of X st A ^|^ B, F };
A1: for x being object st x in F ex y being object st P[x,y]
proof
let x be object;
assume x in F;
then consider a, b being Subset of X such that
A2: x = [a,b] by Th9;
reconsider a, b as set;
take b;
take a, b;
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = F and
A4: for x being object st x in F holds P[x,f.x] from CLASSES1:sch 1(A1);
A5: ss c= rng f
proof
let x be object;
assume x in ss;
then consider B being Subset of X such that
A6: x = B and
A7: ex A being Subset of X st A ^|^ B, F;
consider A being Subset of X such that
A8: A ^|^ B, F by A7;
A9: [A, B] in Maximal_wrt F by A8;
then
A10: ex a,b being object st [A,B] = [a,b] & f.[A,B] = [a,b]`2 by A4;
f.[A,B] = B by A10;
hence thesis by A3,A6,A9,FUNCT_1:3;
end;
rng f is finite by A3,FINSET_1:8;
hence thesis by A5;
end;
end;
theorem Th31:
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
proof
let X, x be set, F be Dependency-set of X;
hereby
assume x in saturated-subsets F;
then consider B being Subset of X such that
A1: x = B and
A2: ex A being Subset of X st A^|^B,F;
consider A being Subset of X such that
A3: A^|^B,F by A2;
take B, A;
thus x = B & A^|^B,F by A1,A3;
end;
given B, A being Subset of X such that
A4: x = B and
A5: A ^|^ B, F;
thus thesis by A4,A5;
end;
theorem Th32: :: WWA3:
for X being finite non empty set, F being Full-family of X holds
saturated-subsets F is (B1) (B2)
proof
let X be finite non empty set, F be Full-family of X;
set ss = saturated-subsets F;
A1: Maximal_wrt F is (M1) by Th28;
then consider A9, B9 being Subset of X such that
A2: [A9,B9] >= [[#]X,[#]X] and
A3: [A9,B9] in Maximal_wrt F;
[#]X c= B9 by A2;
then
A4: [#]X = B9 by XBOOLE_0:def 10;
A9 ^|^ B9, F by A3;
then X in ss by A4;
hence ss is (B1);
thus ss is (B2)
proof
let a, b be set such that
A5: a in ss and
A6: b in ss;
reconsider a9 = a, b9 = b as Subset of X by A5,A6;
A7: Maximal_wrt F is (M3) by Th28;
consider B2, A2 being Subset of X such that
A8: b = B2 and
A9: A2 ^|^ B2, F by A6,Th31;
A10: [A2,B2] in Maximal_wrt F by A9;
consider B1, A1 being Subset of X such that
A11: a = B1 and
A12: A1 ^|^ B1, F by A5,Th31;
A13: [A1,B1] in Maximal_wrt F by A12;
consider A9, B9 being Subset of X such that
A14: [A9,B9] >= [a9/\b9,a9/\b9] and
A15: [A9,B9] in Maximal_wrt F by A1;
A16: A9 c= a/\b by A14;
a/\b c= b by XBOOLE_1:17;
then A9 c= B2 by A8,A16;
then
A17: B9 c= B2 by A10,A15,A7;
A18: a/\b c= B9 by A14;
a/\b c= a by XBOOLE_1:17;
then A9 c= B1 by A11,A16;
then B9 c= B1 by A13,A15,A7;
then B9 c= a/\b by A11,A8,A17,XBOOLE_1:19;
then
A19: B9 = a/\b by A18,XBOOLE_0:def 10;
A9 ^|^ B9, F by A15;
hence thesis by A19;
end;
end;
definition
let X be set, B be set;
func X deps_encl_by B -> Dependency-set of X equals
{ [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
proof
set F = {[a, b] where a,b is Subset of X : for c being set st c in B & a
c= c holds b c= c};
F c= [:bool X, bool X:]
proof
let x be object;
assume x in F;
then
ex a, b being Subset of X st x = [a,b] & for c being set st c in B &
a c= c holds b c= c;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th33: :: 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
proof
let X be set, B be Subset-Family of X, F be Dependency-set of X;
set F = X deps_encl_by B;
per cases;
suppose
A1: B is empty;
now
let x be object;
thus x in F implies x in Dependencies X;
assume x in Dependencies X;
then consider x1, x2 being object such that
A2: x1 in bool X and
A3: x2 in bool X and
A4: x = [x1, x2] by ZFMISC_1:def 2;
reconsider x1,x2 as set by TARSKI:1;
for g being set st g in B & x1 c= g holds x2 c= g by A1;
hence x in F by A2,A3,A4;
end;
then F = Dependencies X by TARSKI:2;
then F is (F1) (F2) (F3) (F4) by Th19;
hence thesis;
end;
suppose
B is non empty;
then reconsider B as non empty Subset-Family of X;
thus F is (F1)
proof
let A be Subset of X;
for c being set st c in B & A c= c holds A c= c;
hence thesis;
end;
A5: now
let x,y be Subset of X, c be Element of B;
assume that
A6: [x, y] in F and
A7: x c= c;
consider a, b being Subset of X such that
A8: [x,y] = [a,b] and
A9: for c being set st c in B & a c= c holds b c= c by A6;
A10: y = b by A8,XTUPLE_0:1;
x = a by A8,XTUPLE_0:1;
hence y c= c by A7,A9,A10;
end;
now
let a, b, c be Subset of X such that
A11: [a, b] in F and
A12: [b, c] in F;
now
let x be set;
assume that
A13: x in B and
A14: a c= x;
b c= x by A5,A11,A13,A14;
hence c c= x by A5,A12,A13;
end;
hence [a, c] in F;
end;
hence F is (F2) by Th18;
thus F is (F3)
proof
let a, b, a9, b9 be Subset of X such that
A15: [a, b] in F and
A16: [a, b] >= [a9, b9];
A17: b9 c= b by A16;
A18: a c= a9 by A16;
now
let c be set;
assume that
A19: c in B and
A20: a9 c= c;
a c= c by A18,A20;
then b c= c by A5,A15,A19;
hence b9 c= c by A17;
end;
hence thesis;
end;
thus F is (F4)
proof
let a, b, a9, b9 be Subset of X such that
A21: [a, b] in F and
A22: [a9, b9] in F;
now
let c be set;
assume that
A23: c in B and
A24: a\/a9 c= c;
a9 c= c by A24,XBOOLE_1:11;
then
A25: b9 c= c by A5,A22,A23;
a c= c by A24,XBOOLE_1:11;
then b c= c by A5,A21,A23;
hence b\/b9 c= c by A25,XBOOLE_1:8;
end;
hence thesis;
end;
end;
end;
theorem Th34: :: 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)
proof
let X be finite non empty set, B be Subset-Family of X;
set F = X deps_encl_by B;
reconsider F9 = F as Full-family of X by Th33;
set M = Maximal_wrt F9;
let x be object;
assume
A1: x in B;
then reconsider x9 = x as Element of B;
reconsider x99 = x as Subset of X by A1;
M is (M1) by Th28;
then consider a9, b9 being Subset of X such that
A2: [a9,b9] >= [x99,x99] and
A3: [a9, b9] in M;
A4: a9 c= x99 by A2;
[a9,b9] in F by A3;
then consider a, b being Subset of X such that
A5: [a9,b9] = [a,b] and
A6: for c being set st c in B & a c= c holds b c= c;
A7: a ^|^ b, F by A3,A5;
a9 = a by A5,XTUPLE_0:1;
then
A8: b c= x9 by A1,A4,A6;
A9: b9 = b by A5,XTUPLE_0:1;
x99 c= b9 by A2;
then b = x by A9,A8,XBOOLE_0:def 10;
hence thesis by A7;
end;
theorem Th35: :: 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
proof
let X be finite non empty set, B be Subset-Family of X;
set F = X deps_encl_by B;
reconsider F9 = F as Full-family of X by Th33;
set ss = saturated-subsets F;
set M = Maximal_wrt F9;
assume
A1: B is (B1) (B2);
then reconsider B9 = B as non empty set;
A2: X in B by A1;
now
let x be object;
B c= ss by Th34;
hence x in B implies x in ss;
assume x in ss;
then consider b, a being Subset of X such that
A3: x = b and
A4: a ^|^ b, F by Th31;
[a,b] in M by A4;
then [a,b] in F;
then consider aa, bb being Subset of X such that
A5: [a, b] = [aa, bb] and
A6: for c being set st c in B & aa c= c holds bb c= c;
A7: b = bb by A5,XTUPLE_0:1;
set S = { b9 where b9 is Element of B9: a c= b9 };
A8: S c= bool X
proof
let x be object;
assume x in S;
then consider b9 being Element of B9 such that
A9: x = b9 and
a c= b9;
b9 in B9;
hence thesis by A9;
end;
A10: S c= B
proof
let x be object;
assume x in S;
then ex b9 being Element of B9 st x = b9 & a c= b9;
hence thesis;
end;
A11: X in S by A2;
reconsider S as Subset-Family of X by A8;
set mS = Intersect S;
reconsider mS as Subset of X;
A12: a = aa by A5,XTUPLE_0:1;
A13: b c= mS
proof
let x be object;
assume
A14: x in b;
now
let Y be set;
assume Y in S;
then consider b9 being Element of B9 such that
A15: Y = b9 and
A16: a c= b9;
b c= b9 by A6,A12,A7,A16;
hence x in Y by A14,A15;
end;
then x in meet S by A11,SETFAM_1:def 1;
hence thesis by A11,SETFAM_1:def 9;
end;
now
now
let c be set;
assume that
A17: c in B and
A18: a c= c;
c in S by A17,A18;
then meet S c= c by SETFAM_1:3;
hence mS c= c by A11,SETFAM_1:def 9;
end;
then
A19: [a,mS] in F;
assume
A20: b <> mS;
[a,mS] >= [a,b] by A13;
hence contradiction by A4,A20,A19,Th27;
end;
hence x in B by A1,A3,A10,Th1;
end;
hence B = saturated-subsets F by TARSKI:2;
let G be Full-family of X;
assume
A21: B = saturated-subsets G;
set MG = Maximal_wrt G;
A22: MG is (M1)(M3) by Th28;
now
let x be object;
hereby
assume x in G;
then reconsider x1 = x as Element of G;
reconsider x9 = x1 as Dependency of X;
consider a, b being Subset of X such that
A23: x9 = [a,b] by Th8;
now
consider a99, b99 being Subset of X such that
A24: [a99,b99] in MG and
A25: [a99, b99] >= x9 by Th26;
A26: b c= b99 by A23,A25;
let b9 be set such that
A27: b9 in B9 and
A28: a c= b9;
consider b19, a9 being Subset of X such that
A29: b9 = b19 and
A30: a9 ^|^ b19, G by A21,A27,Th31;
a99 c= a by A23,A25;
then
A31: a99 c= b9 by A28;
[a9,b9] in MG by A29,A30;
then b99 c= b19 by A22,A29,A24,A31;
hence b c= b9 by A29,A26;
end;
hence x in F by A23;
end;
assume x in F;
then consider a, b being Subset of X such that
A32: x = [a,b] and
A33: for c being set st c in B & a c= c holds b c= c;
consider a9, b9 being Subset of X such that
A34: [a9, b9] >= [a,a] and
A35: [a9, b9] in MG by A22;
A36: a9 c= a by A34;
a9 ^|^ b9, G by A35;
then
A37: b9 in B by A21;
a c= b9 by A34;
then b c= b9 by A33,A37;
then [a9,b9] >= [a,b] by A36;
hence x in G by A32,A35,Def12;
end;
hence thesis by TARSKI:2;
end;
definition
let X be set, F be Dependency-set of X;
func enclosure_of F -> Subset-Family of X equals
{ 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
proof
set B = { b where b is Subset of X : for x, y being Subset of X st [x, y]
in F & x c= b holds y c= b};
B c= bool X
proof
let z be object;
assume z in B;
then
ex b being Subset of X st z = b & for x, y being Subset of X st [x,
y] in F & x c= b holds y c= b;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th36: :: WWA3c:
for X being finite non empty set, F being Dependency-set of X
holds enclosure_of F is (B1) (B2)
proof
let X be finite non empty set, F be Dependency-set of X;
set B = enclosure_of F;
A1: for x, y being Subset of X st [x, y] in F & x c= X holds y c= X;
X = [#]X;
then X in B by A1;
hence B is (B1);
let a, b be set such that
A2: a in B and
A3: b in B;
consider b9 being Subset of X such that
A4: b9 = b and
A5: for x, y being Subset of X st [x, y] in F & x c= b9 holds y c= b9 by A3;
consider a9 being Subset of X such that
A6: a9 = a and
A7: for x, y being Subset of X st [x, y] in F & x c= a9 holds y c= a9 by A2;
reconsider ab = a9 /\ b9 as Subset of X;
now
let x, y be Subset of X such that
A8: [x, y] in F and
A9: x c= ab;
A10: y c= b9 by A5,A8,A9,XBOOLE_1:18;
y c= a9 by A7,A8,A9,XBOOLE_1:18;
hence y c= ab by A10,XBOOLE_1:19;
end;
hence thesis by A6,A4;
end;
theorem Th37: :: 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
proof
let X be finite non empty set, F be Dependency-set of X;
set B = enclosure_of F;
set H = X deps_encl_by B;
thus F c= H
proof
let x be object;
assume
A1: x in F;
then consider a, b being Subset of X such that
A2: x = [a,b] by Th9;
now
let c be set such that
A3: c in B and
A4: a c= c and
A5: not b c= c;
reconsider c as Subset of X by A3;
ex c9 being Subset of X st c9 = c & for x, y being Subset of X st [x
, y] in F & x c= c9 holds y c= c9 by A3;
hence contradiction by A1,A2,A4,A5;
end;
hence thesis by A2;
end;
let G be Dependency-set of X such that
A6: F c= G and
A7: G is full_family;
set B9 = saturated-subsets G;
let z be object;
set GG = {[e, f] where e, f is Subset of X : for c being set st c in B9 & e
c= c holds f c= c};
A8: GG = X deps_encl_by B9;
B is (B1) (B2) by Th36;
then
A9: B = saturated-subsets H by Th35;
assume z in H;
then consider a, b being Subset of X such that
A10: z = [a,b] and
A11: for c being set st c in B & a c= c holds b c= c;
B9 is (B1) (B2) by A7,Th32;
then
A12: GG = G by A7,A8,Th35;
B9 c= saturated-subsets H
proof
let d be object such that
A13: d in B9 and
A14: not d in saturated-subsets H;
reconsider d as Subset of X by A13;
consider x, y being Subset of X such that
A15: [x, y] in F and
A16: x c= d and
A17: not y c= d by A9,A14;
[x,y] in G by A6,A15;
then consider e, f being Subset of X such that
A18: [x,y] = [e,f] and
A19: for c being set st c in B9 & e c= c holds f c= c by A12;
A20: y = f by A18,XTUPLE_0:1;
x = e by A18,XTUPLE_0:1;
hence contradiction by A13,A16,A17,A19,A20;
end;
then for c be set st c in B9 & a c= c holds b c= c by A11,A9;
hence thesis by A10,A12;
end;
definition
let X be finite non empty set, F be Dependency-set of X;
func Dependency-closure F -> Full-family of X means
:Def24:
F c= it & for G
being Dependency-set of X st F c= G & G is full_family holds it c= G;
existence
proof
set B = {c where c is Subset of X : for x, y being Subset of X st [x, y]
in F & x c= c holds y c= c};
A1: B = enclosure_of F;
B c= bool X
proof
let x be object;
assume x in B;
then
ex c being Subset of X st x = c & for x, y being Subset of X st [x,
y] in F & x c= c holds y c= c;
hence thesis;
end;
then reconsider B as Subset-Family of X;
set H = X deps_encl_by B;
reconsider H as Full-family of X by Th33;
take H;
thus thesis by A1,Th37;
end;
correctness
proof
let it1, it2 be Full-family of X;
assume that
A2: F c= it1 and
A3: for G being Dependency-set of X st F c=G&G is full_family holds it1 c=G and
A4: F c= it2 and
A5: for G being Dependency-set of X st F c=G&G is full_family holds it2 c=G;
A6: it2 c= it1 by A2,A5;
it1 c= it2 by A3,A4;
hence it1 = it2 by A6,XBOOLE_0:def 10;
end;
end;
theorem Th38: :: 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
proof
let X be finite non empty set, F be Dependency-set of X;
set B = enclosure_of F;
set H = X deps_encl_by B;
reconsider H as Full-family of X by Th33;
A1: for G being Dependency-set of X st F c= G & G is full_family holds H c=
G by Th37;
F c= H by Th37;
hence thesis by A1,Def24;
end;
theorem Th39: :: 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)
proof
let X be set, K be Subset of X, BB be Subset-Family of X such that
A1: BB = {X}\/{B where B is Subset of X : not K c= B};
X in {X} by TARSKI:def 1;
then X in BB by A1,XBOOLE_0:def 3;
hence BB is (B1);
set BB1 = {B where B is Subset of X : not K c= B};
thus BB is (B2)
proof
let a, b be set;
assume that
A2: a in BB and
A3: b in BB;
reconsider a9 =a, b9 = b as Subset of X by A2,A3;
per cases by A1,A2,A3,XBOOLE_0:def 3;
suppose
A4: a in {X} & b in {X};
then
A5: b = X by TARSKI:def 1;
a = X by A4,TARSKI:def 1;
then a/\ b in {X} by A5,TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 3;
end;
suppose
A6: a in {X} & b in BB1;
then a = X by TARSKI:def 1;
then a9/\b9 = b by XBOOLE_1:28;
hence thesis by A1,A6,XBOOLE_0:def 3;
end;
suppose
A7: a in BB1 & b in {X};
then b = X by TARSKI:def 1;
then a9/\b9 = a by XBOOLE_1:28;
hence thesis by A1,A7,XBOOLE_0:def 3;
end;
suppose
a in BB1 & b in BB1;
then ex B1 being Subset of X st b = B1 & not K c= B1;
then not K c= a/\b by XBOOLE_1:18;
then a9/\b9 in BB1;
hence thesis by A1,XBOOLE_0:def 3;
end;
end;
end;
theorem :: 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
proof
let X be finite non empty set, F be Dependency-set of X, K being Subset of X;
set BB = {X}\/{B where B is Subset of X : not K c= B};
BB c= bool X
proof
let x be object;
assume
A1: x in BB;
per cases by A1,XBOOLE_0:def 3;
suppose
A2: x in {X};
{X} c= bool X by ZFMISC_1:68;
hence thesis by A2;
end;
suppose
x in {B where B is Subset of X : not K c= B};
then ex B being Subset of X st x = B & not K c= B;
hence thesis;
end;
end;
then reconsider BB9 = BB as non empty Subset-Family of X;
set G = {[a, b] where a,b is Subset of X : for c being set st c in BB9 & a
c= c holds b c= c};
A3: G = X deps_encl_by BB9;
A4: BB9 is (B2) by Th39;
assume
A5: F = { [A, B] where A, B is Subset of X : K c= A or B c= A };
now
let x be object;
hereby
assume x in F;
then consider a, b being Subset of X such that
A6: x = [a,b] and
A7: K c= a or b c= a by A5;
now
let c be set such that
A8: c in BB9 and
A9: a c= c;
per cases by A7;
suppose
A10: K c= a;
thus b c= c
proof
per cases by A8,XBOOLE_0:def 3;
suppose
c in {X};
then c = X by TARSKI:def 1;
hence thesis;
end;
suppose
c in {B where B is Subset of X : not K c= B};
then ex B being Subset of X st c = B & not K c= B;
hence thesis by A9,A10;
end;
end;
end;
suppose
b c= a;
hence b c= c by A9;
end;
end;
hence x in G by A6;
end;
assume x in G;
then consider a, b being Subset of X such that
A11: x = [a,b] and
A12: for c being set st c in BB9 & a c= c holds b c= c;
now
assume not K c= a;
then a in {B where B is Subset of X : not K c= B };
then a in BB9 by XBOOLE_0:def 3;
hence b c= a by A12;
end;
hence x in F by A5,A11;
end;
then
A13: F = G by TARSKI:2;
BB9 is (B1) by Th39;
hence thesis by A4,A3,A13,Th35;
end;
theorem
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
proof
let X be finite set, F be Dependency-set of X, K being Subset of X;
set BB = {X}\/{B where B is Subset of X : not K c= B};
set M = {[K, X]}\/{[A, A] where A is Subset of X : not K c= A};
set ss = saturated-subsets F;
assume F = { [A, B] where A, B is Subset of X : K c= A or B c= A };
then
A1: M = Maximal_wrt F by Th30;
A2: [#]X = X;
now
let x be object;
hereby
assume
A3: x in BB;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: x in {X};
[K,X] in {[K,X]} by TARSKI:def 1;
then [K,X] in M by XBOOLE_0:def 3;
then
A5: K ^|^ X, F by A1;
x = X by A4,TARSKI:def 1;
hence x in ss by A2,A5;
end;
suppose
x in {B where B is Subset of X : not K c= B};
then consider B being Subset of X such that
A6: x = B and
A7: not K c= B;
[B,B] in {[A, A] where A is Subset of X : not K c= A} by A7;
then [B,B] in M by XBOOLE_0:def 3;
then B ^|^ B, F by A1;
hence x in ss by A6;
end;
end;
assume x in ss;
then consider b, a being Subset of X such that
A8: x = b and
A9: a ^|^ b, F by Th31;
A10: [a,b] in M by A1,A9;
per cases by A10,XBOOLE_0:def 3;
suppose
[a,b] in {[K,X]};
then [a,b] = [K,X] by TARSKI:def 1;
then b = X by XTUPLE_0:1;
then b in {X} by TARSKI:def 1;
hence x in BB by A8,XBOOLE_0:def 3;
end;
suppose
[a,b] in {[A, A] where A is Subset of X : not K c= A};
then consider c being Subset of X such that
A11: [a,b] = [c,c] and
A12: not K c= c;
A13: c in {B where B is Subset of X : not K c= B} by A12;
b = c by A11,XTUPLE_0:1;
hence x in BB by A8,A13,XBOOLE_0:def 3;
end;
end;
hence thesis by TARSKI:2;
end;
definition
let X, G be set, B be Subset-Family of X;
pred G is_generator-set_of B means
G c= B & B = { Intersect S where S is Subset-Family of X: S c= G };
end;
theorem :: 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)
proof
let X be finite non empty set, G be Subset-Family of X;
set F = X deps_encl_by G;
set ssF = saturated-subsets F;
F is full_family by Th33;
then
A1: ssF is (B1) (B2) by Th32;
thus G is_generator-set_of ssF
proof
set H = { Intersect S where S is Subset-Family of X: S c= G };
thus
A2: G c= ssF by Th34;
now
let x be object;
hereby
assume x in ssF;
then consider b9, a9 being Subset of X such that
A3: x = b9 and
A4: a9 ^|^ b9, F by Th31;
[a9, b9] in Maximal_wrt F by A4;
then [a9,b9] in F;
then consider a, b being Subset of X such that
A5: [a, b] = [a9, b9] and
A6: for c being set st c in G & a c= c holds b c= c;
set C = {c where c is Subset of X: c in G & a c= c};
C c= bool X
proof
let x be object;
assume x in C;
then ex c being Subset of X st x = c & c in G & a c= c;
hence thesis;
end;
then reconsider C as Subset-Family of X;
now
let z1 be set;
assume z1 in C;
then ex c being Subset of X st z1 = c & c in G & a c= c;
hence b c= z1 by A6;
end;
then
A7: b c= Intersect C by MSSUBFAM:4;
set ic = Intersect C;
A8: b = b9 by A5,XTUPLE_0:1;
A9: C c= G
proof
let c be object;
assume c in C;
then ex cc being Subset of X st cc = c & cc in G & a c= cc;
hence thesis;
end;
thus x in H
proof
per cases;
suppose
b = ic;
hence thesis by A3,A8,A9;
end;
suppose
A10: b <> ic;
reconsider ic as Subset of X;
now
let c be set;
assume that
A11: c in G and
A12: a c= c;
c in C by A11,A12;
hence ic c= c by MSSUBFAM:2;
end;
then
A13: [a,ic] in F;
[a,b] <= [a,ic] by A7;
hence thesis by A4,A5,A8,A10,A13,Th27;
end;
end;
end;
assume x in H;
then
A14: ex S being Subset-Family of X st Intersect S = x & S c= G;
thus x in ssF by A1,A2,A14,Th1,XBOOLE_1:1;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th43: :: 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
proof
let X be finite non empty set, F be Full-family of X;
set G = saturated-subsets F;
take G;
A1: G is (B1) (B2) by Th32;
thus G is_generator-set_of G
proof
set H = { Intersect S where S is Subset-Family of X: S c= G };
thus G c= G;
now
let x be object;
hereby
reconsider xx=x as set by TARSKI:1;
set sx = {xx};
assume
A2: x in G;
then
A3: sx c= G by ZFMISC_1:31;
reconsider sx as Subset-Family of X by A2,ZFMISC_1:31;
A4: Intersect sx = meet sx by SETFAM_1:def 9;
Intersect sx in H by A3;
hence x in H by A4,SETFAM_1:10;
end;
assume x in H;
then
A5: ex S being Subset-Family of X st Intersect S = x & S c= G;
thus x in G by A1,A5,Th1;
end;
hence thesis by TARSKI:2;
end;
thus thesis by A1,Th35;
end;
:: WWA did not show what generators B are,
:: they are the irreducible elements \ X
theorem
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
proof
let X be set, B be non empty finite Subset-Family of X;
assume
A1: B is (B1) (B2);
set G = /\-IRR B;
set H = {Intersect S where S is Subset-Family of X:S c= G};
thus G c= B;
now
let x be object;
hereby
assume x in B;
then reconsider xx = x as Element of B;
consider yz being non empty Subset of B such that
A2: xx = meet yz and
A3: for s being set st s in yz holds s is_/\-irreducible_in B by Th3;
reconsider yz as non empty Subset-Family of X by XBOOLE_1:1;
A4: yz c= G
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in yz;
then xx is_/\-irreducible_in B by A3;
hence thesis by Def3;
end;
Intersect yz = meet yz by SETFAM_1:def 9;
hence x in H by A2,A4;
end;
assume x in H;
then ex S being Subset-Family of X st x = Intersect S & S c= G;
hence x in B by A1,Th1,XBOOLE_1:1;
end;
hence thesis by TARSKI:2;
end;
theorem
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}
proof
let X, G be set, B be non empty finite Subset-Family of X such that
A1: B is (B1) (B2) and
A2: G is_generator-set_of B;
A3: B = { Intersect S where S is Subset-Family of X: S c= G } by A2;
A4: G c= B by A2;
let x be object;
assume
A5: x in /\-IRR B;
then reconsider xx = x as Element of B;
A6: xx is_/\-irreducible_in B by A5,Def3;
assume
A7: not x in G\/{X};
then not x in {X} by XBOOLE_0:def 3;
then
A8: x <> X by TARSKI:def 1;
x in B by A5;
then consider S being Subset-Family of X such that
A9: x = Intersect S and
A10: S c= G by A3;
not x in S by A10,A7,XBOOLE_0:def 3;
hence contradiction by A1,A4,A9,A10,A8,A6,Th4,XBOOLE_1:1;
end;
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
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
proof
let X be non empty finite set, F be Full-family of X;
reconsider D = X --> INT as non-empty ManySortedSet of X;
consider G being Subset-Family of X such that
G is_generator-set_of saturated-subsets F and
A1: F = X deps_encl_by G by Th43;
consider H being FinSequence such that
A2: rng H = G and
H is one-to-one by FINSEQ_4:58;
A4: now
set f = X --> 0;
thus dom f = dom D;
let x be object;
assume
A5: x in dom D;
then f.x = 0 by FUNCOP_1:7;
then f.x in NAT;
then f.x in INT by NUMBERS:17;
hence f.x in D.x by A5,FUNCOP_1:7;
end;
then
A6: X --> 0 is Element of product D by CARD_3:def 5;
reconsider H as FinSequence of G by A2,FINSEQ_1:def 4;
per cases;
suppose
A7: G is empty;
set R = {X-->0};
R c= product D
proof
let x be object;
assume x in R;
then x = X --> 0 by TARSKI:def 1;
hence thesis by A4,CARD_3:def 5;
end;
then reconsider R as non empty Subset of product D;
set BD = DB-Rel (# X, D, R #);
take BD;
thus the Attributes of BD = X & for a being Element of X holds (the
Domains of BD).a = INT;
set Ds = Dependency-str BD;
now
let x be object;
hereby
assume x in F;
then consider A, B being Subset of X such that
A8: x = [A, B] and
for g being set st g in G & A c= g holds B c= g by A1;
reconsider A, B as Subset of the Attributes of BD;
A >|> B, BD
proof
let f, g be Element of the Relationship of BD;
f = X --> 0 by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
hence x in Ds by A8;
end;
assume x in Ds;
then consider A, B being Subset of the Attributes of BD such that
A9: x = [A,B] and
A >|> B, BD;
for g being set st g in G & A c= g holds B c= g by A7;
hence x in F by A1,A9;
end;
hence thesis by TARSKI:2;
end;
suppose
A10: G is non empty;
then H is non empty by A2;
then reconsider n =len H as non zero Element of NAT;
defpred R[set,Element of n-tuples_on BOOLEAN ] means
for i being Element
of NAT st i in Seg n holds ($1 in H.i implies ($2).i = 0) & (not $1 in H.i
implies ($2).i = 1);
A11: now
let x be Element of X;
defpred P[set,set] means (x in H.$1 implies $2 = 0) & (not x in H.$1
implies $2 = 1);
A12: for i being Nat st i in Seg n ex x being Element of BOOLEAN st P[i, x]
proof
let i be Nat;
assume i in Seg n;
per cases;
suppose
A13: x in H.i;
reconsider b = FALSE as Element of BOOLEAN;
take b;
thus thesis by A13;
end;
suppose
A14: not x in H.i;
reconsider b = TRUE as Element of BOOLEAN;
take b;
thus thesis by A14;
end;
end;
consider y being FinSequence of BOOLEAN such that
A15: dom y = Seg n and
A16: for i being Nat st i in Seg n holds P[i,y.i] from FINSEQ_1:sch
5(A12 );
A17: y in BOOLEAN* by FINSEQ_1:def 11;
len y = n by A15,FINSEQ_1:def 3;
then y in { s where s is Element of BOOLEAN*: len s = n } by A17;
then reconsider y as Element of n-tuples_on BOOLEAN;
take y;
thus R[x,y] by A16;
end;
consider M being Function of X, n-tuples_on BOOLEAN such that
A18: for x being Element of X holds R[x,(M.x) qua Element of n
-tuples_on BOOLEAN] from FUNCT_2:sch 3(A11);
set R = {f where f is Element of product D : ex i being Element of NAT st
for x being Element of X holds f.x = Absval ((n-BinarySequence i)
'&' (M.x qua Element of n-tuples_on BOOLEAN)) };
A19: R c= product D
proof
let x be object;
assume x in R;
then ex f being Element of product D st x = f & ex i being Element of
NAT st for x being Element of X holds f.x = Absval ((n-BinarySequence i) '&' (M
.x qua Element of n-tuples_on BOOLEAN));
hence thesis;
end;
now
take i = 0;
set f = X --> 0;
let x be Element of X;
A20: (n-BinarySequence i) '&' (M.x qua Element of n-tuples_on BOOLEAN)
= n-BinarySequence i by Th5
.= 0*n by BINARI_3:25;
thus f.x = 0
.= Absval ((n-BinarySequence i) '&' (M.x
qua Element of n-tuples_on BOOLEAN)) by A20,BINARI_3:6;
end;
then X --> 0 in R by A6;
then reconsider R as non empty Subset of product D by A19;
set BD = DB-Rel (# X, D, R #);
take BD;
thus the Attributes of BD = X & for a being Element of X holds (the
Domains of BD).a = INT;
set Ds = Dependency-str BD;
A21: dom H = Seg n by FINSEQ_1:def 3;
now
let x be object;
hereby
assume x in F;
then consider A, B being Subset of X such that
A22: x = [A, B] and
A23: for g being set st g in G & A c= g holds B c= g by A1;
reconsider A9 = A, B9 = B as Subset of the Attributes of BD;
A9 >|> B9, BD
proof
let f, g be Element of the Relationship of BD;
assume
A24: f|A9 = g|A9;
f in R;
then consider Rf being Element of product D such that
A25: f = Rf and
A26: ex i being Element of NAT st for x being Element of X holds
Rf.x = Absval ((n-BinarySequence i) '&' (M.x
qua Element of n-tuples_on BOOLEAN));
consider fi being Element of NAT such that
A27: for x being Element of X holds Rf.x = Absval ((n
-BinarySequence fi) '&' (M.x qua Element of n-tuples_on BOOLEAN))
by A26;
g in R;
then consider Rg being Element of product D such that
A28: g = Rg and
A29: ex i being Element of NAT st for x being Element of X holds
Rg.x = Absval ((n-BinarySequence i) '&' (M.x
qua Element of n-tuples_on BOOLEAN));
consider gi being Element of NAT such that
A30: for x being Element of X holds Rg.x = Absval ((n
-BinarySequence gi) '&' (M.x
qua Element of n-tuples_on BOOLEAN)) by A29;
A31: dom g = dom D by A28,CARD_3:9
.= dom f by A25,CARD_3:9;
now
set nbg = n-BinarySequence gi;
set nbf = n-BinarySequence fi;
thus
A32: dom (g|B) = dom f /\ B by A31,RELAT_1:61;
let a be object such that
A33: a in dom (g|B);
reconsider x = a as Element of X by A32,A33;
reconsider Mx = M.x as Tuple of n, BOOLEAN;
set ng = nbg '&' (M.x qua Element of n-tuples_on BOOLEAN);
set nf = nbf '&' (M.x qua Element of n-tuples_on BOOLEAN);
A34: dom (M.x qua Element of n-tuples_on BOOLEAN) = Seg n by Lm2;
A35: dom nf = Seg n by Lm1;
A36: a in B by A32,A33,XBOOLE_0:def 4;
now
thus dom nf = dom ng by A35,Lm1;
let i be object;
assume
A37: i in dom nf;
per cases;
suppose
A c= H.i;
then
A38: B c= H.i by A2,A21,A23,A35,A37,FUNCT_1:3;
A39: Mx/.i = Mx.i by A34,A35,A37,PARTFUN1:def 6
.= 0 by A18,A36,A35,A37,A38;
thus nf.i = (nbf/.i) '&' (Mx/.i) by A35,A37,Def5
.= (nbg/.i) '&' (Mx/.i) by A39
.= ng.i by A35,A37,Def5;
end;
suppose
A40: not A c= H.i;
thus nf.i = ng.i
proof
consider xx being object such that
A41: xx in A and
A42: not xx in H.i by A40;
reconsider xx as Element of X by A41;
A43: f.xx = (g|A).xx by A24,A41,FUNCT_1:49
.= g.xx by A41,FUNCT_1:49;
reconsider Mxx = M.xx as Tuple of n, BOOLEAN;
A44: f.xx = Absval (nbf '&' (M.xx
qua Element of n-tuples_on BOOLEAN)) by A25,A27;
A45: g.xx = Absval ((nbg) '&' (M.xx
qua Element of n-tuples_on BOOLEAN)) by A28,A30;
dom (M.xx
qua Element of n-tuples_on BOOLEAN) = Seg n by Lm2;
then
A46: Mxx/.i = Mxx.i by A35,A37,PARTFUN1:def 6
.= 1 by A18,A35,A37,A42;
then
A47: nbf/.i = (nbf/.i) '&' (Mxx/.i) .= (nbf '&' (M.xx
qua Element of n-tuples_on BOOLEAN)).i by A35,A37,Def5
.= (nbg '&' (M.xx
qua Element of n-tuples_on BOOLEAN)).i
by A43,A44,A45,BINARI_3:2
.= (nbg/.i) '&' (Mxx/.i) by A35,A37,Def5
.= nbg/.i by A46;
thus nf.i = (nbf/.i) '&' (Mx/.i) by A35,A37,Def5
.= ng.i by A35,A37,A47,Def5;
end;
end;
end;
then nf = ng by FUNCT_1:2;
then g.a = Absval ((n-BinarySequence fi) '&' (M.x
qua Element of n-tuples_on BOOLEAN)) by A28,A30
.= f.a by A25,A27;
hence (g|B).a = f.a by A33,FUNCT_1:47;
end;
hence thesis by FUNCT_1:46;
end;
hence x in Ds by A22;
end;
assume x in Ds;
then consider A, B being Subset of the Attributes of BD such that
A48: x = [A, B] and
A49: A >|> B, BD;
now
deffunc F(Element of X) = Absval ((n-BinarySequence 0) '&' (M.$1
qua Element of n-tuples_on BOOLEAN));
let gg be set such that
A50: gg in G and
A51: A c= gg and
A52: not B c= gg;
reconsider gg as Element of G by A50;
consider f being Function of X, NAT such that
A53: for x being Element of X holds f.x = F(x) from FUNCT_2:sch 4;
A54: now
let x be object;
assume x in dom D;
then reconsider x9 = x as Element of X;
f.x9 in INT by NUMBERS:17;
hence f.x in D.x;
end;
A55: dom f = dom D by FUNCT_2:def 1;
then reconsider f as Element of product D by A54,CARD_3:def 5;
consider i being Nat such that
A56: i in dom H and
A57: H.i = gg by A2,A10,FINSEQ_2:10;
i <> 0 by A21,A56,FINSEQ_1:1;
then consider k being Nat such that
A58: i = k+1 by NAT_1:6;
consider bx being object such that
A59: bx in B and
A60: not bx in gg by A52;
reconsider bx as Element of X by A59;
reconsider Mbx = M.bx as Tuple of n, BOOLEAN;
A61: f in R by A53;
dom Mbx = Seg n by Lm1;
then
A62: Mbx/.i = Mbx.i by A21,A56,PARTFUN1:def 6
.= 1 by A21,A18,A60,A56,A57;
reconsider k as Element of NAT by ORDINAL1:def 12;
deffunc F(Element of X) = Absval ((n-BinarySequence 2 to_power k) '&'
(M.$1 qua Element of n-tuples_on BOOLEAN));
consider g being Function of X, NAT such that
A63: for x being Element of X holds g.x = F(x) from FUNCT_2:sch 4;
A64: now
let x be object;
assume x in dom D;
then reconsider x9 = x as Element of X;
g.x9 in INT by NUMBERS:17;
hence g.x in D.x;
end;
A65: dom g = dom D by FUNCT_2:def 1;
then reconsider g as Element of product D by A64,CARD_3:def 5;
i <= n by A21,A56,FINSEQ_1:1;
then
A66: k < n by A58,NAT_1:13;
now
thus
A67: dom (f|A) = dom g /\ A by A55,A65,RELAT_1:61;
let x be object;
assume
A68: x in dom (f|A);
then reconsider a = x as Element of X by A67;
set bs0 = n-BinarySequence 0, bsi = n-BinarySequence 2 to_power k;
A69: g.a = Absval (bsi '&' (M.a
qua Element of n-tuples_on BOOLEAN)) by A63;
set L = bs0 '&' (M.a
qua Element of n-tuples_on BOOLEAN), R = bsi '&' (M.a
qua Element of n-tuples_on BOOLEAN);
reconsider Ma = M.a as Tuple of n, BOOLEAN;
A70: x in A by A68;
A71: now
thus dom L = Seg n by Lm1
.= dom R by Lm1;
let j be object;
A72: bs0 = 0*n by BINARI_3:25
.= n |-> 0 by EUCLID:def 4;
assume
A73: j in dom L;
then reconsider nj = j as Element of NAT;
A74: j in Seg n by A73,Lm1;
dom bs0 = Seg n by Lm1;
then
A75: bs0/.nj = bs0.nj by A74,PARTFUN1:def 6
.= 0 by A72;
A76: L.j = (bs0/.nj) '&' (Ma/.nj) by A74,Def5
.= 0 by A75;
per cases;
suppose
A77: i <> nj;
dom bsi = Seg n by Lm1;
then
A78: bsi/.nj = bsi.nj by A74,PARTFUN1:def 6
.= FALSE by A58,A66,A74,A77,Th7;
R.j = (bsi/.nj) '&' (Ma/.nj) by A74,Def5;
hence L.j = R.j by A76,A78;
end;
suppose
A79: i = nj;
dom Ma = Seg n by Lm1;
then
A80: Ma/.nj = Ma.i by A74,A79,PARTFUN1:def 6
.= 0 by A18,A51,A57,A70,A74,A79;
R.j = (bsi/.nj) '&' (Ma/.nj) by A74,Def5
.= 0 by A80;
hence L.j = R.j by A76;
end;
end;
(f|A).a = f.a by A68,FUNCT_1:49
.= Absval (bs0 '&' (M.a
qua Element of n-tuples_on BOOLEAN)) by A53;
hence (f|A).x = g.x by A69,A71,FUNCT_1:2;
end;
then
A81: f|A = g|A by FUNCT_1:46;
set bs0 = n-BinarySequence 0, bsi = n-BinarySequence 2 to_power k;
A82: bs0 = 0*n by BINARI_3:25
.= n |-> 0 by EUCLID:def 4;
dom bs0 = Seg n by Lm1;
then
A83: bs0/.i = bs0.i by A21,A56,PARTFUN1:def 6
.= 0 by A82;
dom bsi = Seg n by Lm1;
then
A84: bsi/.i = bsi.i by A21,A56,PARTFUN1:def 6
.= 1 by A58,A66,Th7;
A85: (bsi '&' (Mbx)).i = (bsi/.i) '&' (Mbx/.i) by A21,A56,Def5
.= bsi/.i by A62;
A86: (bs0 '&' (Mbx)).i = (bs0/.i) '&' (Mbx/.i) by A21,A56,Def5
.= bs0/.i by A62;
g in R by A63;
then
A87: f|B = g|B by A49,A61,A81;
Absval (bs0 '&' (M.bx
qua Element of n-tuples_on BOOLEAN)) = f.bx by A53
.= (f|B).bx by A59,FUNCT_1:49
.= g.bx by A59,A87,FUNCT_1:49
.= Absval (bsi '&' (M.bx
qua Element of n-tuples_on BOOLEAN)) by A63;
hence contradiction by A83,A86,A85,A84,BINARI_3:2;
end;
hence x in F by A1,A48;
end;
hence thesis by TARSKI:2;
end;
end;
begin :: 8. Structure of the family of candidate keys
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} 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
let X, F, BB be set;
assume
A1: 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};
let x, y be Subset of X;
hereby
assume [x,y] in F;
then consider a, b being Subset of X such that
A2: [x,y] = [a, b] and
A3: for c being set st c in BB & a c= c holds b c= c by A1;
A4: y = b by A2,XTUPLE_0:1;
x = a by A2,XTUPLE_0:1;
hence for c being set st c in BB & x c= c holds y c= c by A3,A4;
end;
assume for c being set st c in BB & x c= c holds y c= c;
hence thesis by A1;
end;
definition
let X be set, F be Dependency-set of X;
func candidate-keys F -> Subset-Family of X equals
{ A where A is Subset of
X: [A, X] in Maximal_wrt F };
coherence
proof
set B = {A where A is Subset of X : [A, X] in Maximal_wrt F};
B c= bool X
proof
let x be object;
assume x in B;
then ex A being Subset of X st x = A & [A, X] in Maximal_wrt F;
hence thesis;
end;
hence thesis;
end;
end;
theorem :: 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}
proof
let X be finite set, F be Dependency-set of X, K be Subset of X;
assume F = { [A, B] where A, B is Subset of X : K c= A or B c= A };
then
A1: Maximal_wrt F = {[K, X]}\/{[A, A] where A is Subset of X : not K c= A}
by Th30;
now
let x be object;
hereby
assume x in candidate-keys F;
then consider a being Subset of X such that
A2: x = a and
A3: [a,X] in Maximal_wrt F;
per cases by A1,A3,XBOOLE_0:def 3;
suppose
[a,X] in {[K, X]};
then [a,X] = [K,X] by TARSKI:def 1;
then a = K by XTUPLE_0:1;
hence x in {K} by A2,TARSKI:def 1;
end;
suppose
[a,X] in {[A, A] where A is Subset of X : not K c= A};
then consider A being Subset of X such that
A4: [a,X] = [A,A] and
A5: not K c= A;
X = A by A4,XTUPLE_0:1;
hence x in {K} by A5;
end;
end;
assume x in {K};
then
A6: x = K by TARSKI:def 1;
[K,X] in {[K,X]} by TARSKI:def 1;
then [K,X] in Maximal_wrt F by A1,XBOOLE_0:def 3;
hence x in candidate-keys F by A6;
end;
hence thesis by TARSKI:2;
end;
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
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 :: WWA6:
for R being DB-Rel holds candidate-keys Dependency-str R is (C1) (C2)
proof
let D be DB-Rel;
set F = Dependency-str D;
set X = the Attributes of D;
A1: F is full_family by Th23;
then
A2: Maximal_wrt F is (M2) by Th28;
saturated-subsets F is (B1) by A1,Th32;
then X in saturated-subsets F;
then consider B, A be Subset of X such that
A3: X = B and
A4: A ^|^ B, F by Th31;
[A,X] in Maximal_wrt F by A3,A4;
then A in candidate-keys F;
hence candidate-keys F is non empty;
let k1, k2 be set such that
A5: k1 in candidate-keys F and
A6: k2 in candidate-keys F and
A7: k1 c= k2;
consider a2 being Subset of X such that
A8: k2 = a2 and
A9: [a2, X] in Maximal_wrt F by A6;
consider a1 being Subset of X such that
A10: k1 = a1 and
A11: [a1, X] in Maximal_wrt F by A5;
[a1,[#]X] >= [a2,[#]X] by A7,A10,A8;
hence thesis by A10,A11,A8,A9,A2;
end;
theorem :: 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
proof
let X be finite set, C be Subset-Family of X;
set B = {b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b};
A1: [#]X = X;
B c= bool X
proof
let x be object;
assume x in B;
then ex b being Subset of X st x = b & for K being Subset of X st K in C
holds not K c= b;
hence thesis;
end;
then reconsider BB = B as Subset-Family of X;
set 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};
F = X deps_encl_by BB;
then reconsider F as Full-family of X by Th33;
assume
A2: C is (C1);
assume
A3: C is (C2);
A4: now
let x be set;
assume
A5: x in C;
then reconsider x9 = x as Subset of X;
now
let c be set;
assume that
A6: c in BB and
A7: x9 c= c;
ex b being Subset of X st c = b & for K being Subset of X st K in C
holds not K c= b by A6;
hence X c= c by A5,A7;
end;
then [x9,X] in F by A1;
then consider a, b being Subset of X such that
A8: [a,b] in Maximal_wrt F and
A9: [a, b] >= [x9,[#]X] by Th26;
A10: a c= x9 by A9;
X c= b by A9;
then
A11: b = X by XBOOLE_0:def 10;
assume
A12: not [x,X] in Maximal_wrt F;
now
let K be Subset of X;
assume
A13: K in C;
assume
A14: K c= a;
then K c= x9 by A10;
then K = x9 by A3,A5,A13;
hence contradiction by A8,A10,A11,A12,A14,XBOOLE_0:def 10;
end;
then a in BB;
then X c= a by A8,A11,Lm3;
then X = a by XBOOLE_0:def 10;
hence contradiction by A8,A10,A11,A12,XBOOLE_0:def 10;
end;
take F;
now
let x be object;
hereby
assume
A15: x in C;
then [x,X] in Maximal_wrt F by A4;
hence x in candidate-keys F by A15;
end;
assume x in candidate-keys F;
then consider A being Subset of X such that
A16: x = A and
A17: [A, X] in Maximal_wrt F;
assume
A18: not x in C;
now
A19: A ^|^ X, F by A17;
given K being Subset of X such that
A20: K in C and
A21: K c= A;
A22: [K, [#]X] >= [A, [#]X] by A21;
[K,X] in Maximal_wrt F by A4,A20;
hence contradiction by A16,A18,A20,A19,A22,Th27;
end;
then
A23: A in BB;
for c being set st c in BB holds c = X or not A c= c
proof
let c be set;
assume that
A24: c in BB and
A25: not c = X;
assume A c= c;
then X c= c by A1,A17,A24,Lm3;
hence contradiction by A24,A25,XBOOLE_0:def 10;
end;
then X in BB by A23;
then
ex b being Subset of X st b = X & for K being Subset of X st K in C
holds not K c= b;
then not ex K being object st K in C;
hence contradiction by A2,XBOOLE_0:def 1;
end;
hence thesis by TARSKI:2;
end;
theorem :: 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)
proof
let X be finite set, C be Subset-Family of X, B be set such that
A1: C is (C1) and
A2: C is (C2) and
A3: B = {b where b is Subset of X : for K being Subset of X st K in C
holds not K c= b};
B c= bool X
proof
let x be object;
assume x in B;
then ex b being Subset of X st x = b & for K being Subset of X st K in C
holds not K c= b by A3;
hence thesis;
end;
then reconsider BB = B as Subset-Family of X;
set F = X deps_encl_by B;
A4: [#]X = X;
A5: now
let x be set;
assume
A6: x in C;
then reconsider x9 = x as Subset of X;
now
let c be set;
assume that
A7: c in BB and
A8: x9 c= c;
ex b being Subset of X st c = b & for K being Subset of X st K in C
holds not K c= b by A3,A7;
hence X c= c by A6,A8;
end;
then [x9,X] in F by A4;
then consider a, b being Subset of X such that
A9: [a,b] in Maximal_wrt F and
A10: [a, b] >= [x9,[#]X] by Th26;
A11: a c= x9 by A10;
X c= b by A10;
then
A12: b = X by XBOOLE_0:def 10;
assume
A13: not [x,X] in Maximal_wrt F;
now
let K be Subset of X;
assume
A14: K in C;
assume
A15: K c= a;
then K c= x9 by A11;
then K = x9 by A2,A6,A14;
hence contradiction by A9,A11,A12,A13,A15,XBOOLE_0:def 10;
end;
then a in BB by A3;
then X c= a by A9,A12,Lm3;
then X = a by XBOOLE_0:def 10;
hence contradiction by A9,A11,A12,A13,XBOOLE_0:def 10;
end;
now
let x be object;
hereby
assume
A16: x in C;
then [x,X] in Maximal_wrt F by A5;
hence x in candidate-keys F by A16;
end;
assume x in candidate-keys F;
then consider A being Subset of X such that
A17: x = A and
A18: [A, X] in Maximal_wrt F;
assume
A19: not x in C;
now
A20: A ^|^ X, F by A18;
given K being Subset of X such that
A21: K in C and
A22: K c= A;
A23: [K, [#]X] >= [A, [#]X] by A22;
[K,X] in Maximal_wrt F by A5,A21;
hence contradiction by A17,A19,A21,A20,A23,Th27;
end;
then
A24: A in BB by A3;
for c being set st c in BB holds c = X or not A c= c
proof
let c be set;
assume that
A25: c in BB and
A26: not c = X;
assume A c= c;
then X c= c by A4,A18,A25,Lm3;
hence contradiction by A25,A26,XBOOLE_0:def 10;
end;
then X in BB by A24;
then
ex b being Subset of X st b = X & for K being Subset of X st K in C
holds not K c= b by A3;
then not ex K being object st K in C;
hence contradiction by A1,XBOOLE_0:def 1;
end;
hence thesis by TARSKI:2;
end;
theorem :: 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
proof
let X be non empty finite set, C be Subset-Family of X such that
A1: C is (C1) and
A2: C is (C2);
reconsider D = X --> bool X as non-empty ManySortedSet of X;
set M = {L where L is Subset of X: for K being Subset of X st K in C holds L
/\K <> {}};
reconsider M0 = M\/{0} as non empty set;
set R = { (X --> 0) +* (L --> L) where L is Subset of X : L in M0 };
A3: R c= product D
proof
let x be object;
assume x in R;
then consider L being Subset of X such that
A5: x = (X --> 0) +* (L --> L) and
L in M0;
set g = (X --> 0) +* (L --> L);
A6: dom (L --> L) = L;
A7: now
let x be object such that
A8: x in dom D;
A9: D.x = bool X by A8,FUNCOP_1:7;
per cases;
suppose
A10: x in L;
then g.x = (L --> L).x by A6,FUNCT_4:13
.= L by A10,FUNCOP_1:7;
hence g.x in D.x by A9;
end;
suppose
not x in L;
then g.x = (X --> 0).x by A6,FUNCT_4:11
.= {}X;
hence g.x in D.x by A9;
end;
end;
dom g = dom (X --> 0)\/L by A6,FUNCT_4:def 1
.= X\/L
.= X by XBOOLE_1:12;
hence thesis by A5,A7,CARD_3:def 5;
end;
0 in {0} by TARSKI:def 1;
then 0 in M\/{0} by XBOOLE_0:def 3;
then (X --> 0) +* ({}X --> {}X) in R;
then reconsider R as non empty Subset of product D by A3;
take DB = DB-Rel(# X, D, R #);
thus the Attributes of DB = X;
set ds = Dependency-str DB;
set ck = { A where A is Subset of X : [A, X] in Maximal_wrt ds };
A11: [#]X = X;
A12: now
let x be set;
assume
A13: x in C;
then reconsider A = x as Subset of X;
reconsider AA = A, XA = X as Subset of the Attributes of DB by A11;
now
let f, g be Element of the Relationship of DB such that
A14: f|A = g|A;
f in R;
then consider Lf being Subset of X such that
A15: f = (X --> 0) +* (Lf --> Lf) and
A16: Lf in M0;
A17: Lf in M or Lf in {0} by A16,XBOOLE_0:def 3;
A18: dom (Lf --> Lf) = Lf;
g in R;
then consider Lg being Subset of X such that
A19: g = (X --> 0) +* (Lg --> Lg) and
A20: Lg in M0;
A21: Lg in M or Lg in {0} by A20,XBOOLE_0:def 3;
A22: dom (Lg --> Lg) = Lg;
per cases by A17,A21,TARSKI:def 1;
suppose
Lf in M & Lg in M;
then ex Lff being Subset of X st Lf = Lff & for K being Subset of X
st K in C holds Lff/\K <> {};
then
A23: Lf /\ A <> {} by A13;
then consider a being object such that
A24: a in Lf /\ A by XBOOLE_0:def 1;
A25: g.a = 0 or g.a = Lg
proof
per cases;
suppose
A26: a in Lg;
then g.a = (Lg --> Lg).a by A19,A22,FUNCT_4:13;
hence thesis by A26,FUNCOP_1:7;
end;
suppose
not a in Lg;
then g.a = (X --> 0).a by A19,A22,FUNCT_4:11;
hence thesis;
end;
end;
A27: a in Lf by A24,XBOOLE_0:def 4;
A28: a in A by A24,XBOOLE_0:def 4;
then
A29: (g|A).a = g.a by FUNCT_1:49;
(f|A).a = f.a by A28,FUNCT_1:49
.= (Lf --> Lf).a by A15,A18,A27,FUNCT_4:13
.= Lf by A27,FUNCOP_1:7;
hence f|X = g|X by A14,A15,A19,A23,A29,A25;
end;
suppose
A30: Lf in M & Lg = 0;
then
ex L being Subset of X st Lf = L & for K being Subset of X st K
in C holds L/\K <> {};
then
A31: Lf /\ A <> {} by A13;
then consider a being object such that
A32: a in Lf /\ A by XBOOLE_0:def 1;
A33: a in A by A32,XBOOLE_0:def 4;
then
A34: (g|A).a = g.a by FUNCT_1:49
.= ((X --> 0) +* {}).a by A19,A30
.= (X --> 0).a
.= {};
A35: a in Lf by A32,XBOOLE_0:def 4;
(f|A).a = f.a by A33,FUNCT_1:49
.= (Lf --> Lf).a by A15,A18,A35,FUNCT_4:13
.= Lf by A35,FUNCOP_1:7;
hence f|X = g|X by A14,A31,A34;
end;
suppose
A36: Lf = 0 & Lg in M;
then
ex L being Subset of X st Lg = L & for K being Subset of X st K
in C holds L/\K <> {};
then
A37: Lg /\ A <> {} by A13;
then consider a being object such that
A38: a in Lg /\ A by XBOOLE_0:def 1;
A39: a in A by A38,XBOOLE_0:def 4;
then
A40: (f|A).a = f.a by FUNCT_1:49
.= ((X --> 0) +* {}).a by A15,A36
.= (X --> 0).a
.= {};
A41: a in Lg by A38,XBOOLE_0:def 4;
(g|A).a = g.a by A39,FUNCT_1:49
.= (Lg --> Lg).a by A19,A22,A41,FUNCT_4:13
.= Lg by A41,FUNCOP_1:7;
hence f|X = g|X by A14,A37,A40;
end;
suppose
Lf = 0 & Lg = 0;
hence f|X = g|X by A15,A19;
end;
end;
then AA >|> XA, DB;
then [A,X] in ds;
then consider a, b being Subset of X such that
A42: [a,b] in Maximal_wrt ds and
A43: [a, b] >= [A,[#]X] by Th26;
A44: a c= A by A43;
[a,b] in ds by A42;
then consider aa, XX being Subset of the Attributes of DB such that
A45: [a,b] = [aa,XX] and
A46: aa >|> XX, DB;
A47: a = aa by A45,XTUPLE_0:1;
A48: b = XX by A45,XTUPLE_0:1;
A49: X c= b by A43;
then
A50: b = X by XBOOLE_0:def 10;
now
set r1 = (X --> 0) +* (a` --> a`);
set r0 = X --> 0;
assume
A51: a <> A;
A52: now
assume a` = {};
then a` c= a;
then a = X by A11,SUBSET_1:19;
hence contradiction by A44,A51,XBOOLE_0:def 10;
end;
then consider y being object such that
A53: y in a` by XBOOLE_0:def 1;
now
let K be Subset of X;
assume
A54: K in C;
assume a` /\ K = {};
then K misses a` by XBOOLE_0:def 7;
then
A55: K c= a by SUBSET_1:24;
then K c= A by A44;
then K = A by A2,A13,A54;
hence contradiction by A44,A51,A55,XBOOLE_0:def 10;
end;
then a` in M;
then a` in M0 by XBOOLE_0:def 3;
then
A56: r1 in R;
0 in {0} by TARSKI:def 1;
then 0 in M0 by XBOOLE_0:def 3;
then (X --> 0) +* ({}X --> {}X) in R;
then (X --> 0) +* {} in R;
then reconsider r0, r1 as Element of the Relationship of DB
by A56;
A57: (r0|X).y = r0.y
.= 0;
A58: dom (a` --> a`) = a`;
now
A59: dom r1 = dom (X --> 0)\/dom (a` --> a`) by FUNCT_4:def 1
.= X\/dom (a` --> a`)
.= X\/a`
.= X by XBOOLE_1:12;
dom r0 = X;
hence dom (r0|a) = dom r1 /\ a by A59,RELAT_1:61;
let x be object;
assume
A60: x in dom (r0|a);
dom (r0|a) = dom r0 /\ a by RELAT_1:61;
then
A61: x in a by A60,XBOOLE_0:def 4;
a misses a` by XBOOLE_1:79;
then a /\ a` = {} by XBOOLE_0:def 7;
then
A62: not x in a` by A61,XBOOLE_0:def 4;
thus (r0|a).x = (X --> 0).x by A61,FUNCT_1:49
.= r1.x by A58,A62,FUNCT_4:11;
end;
then
A63: r0|a = r1|a by FUNCT_1:46;
(r1|X).y = r1.y by A53,FUNCT_1:49
.= (a` --> a`).y by A58,A53,FUNCT_4:13
.= a` by A53,FUNCOP_1:7;
hence contradiction by A50,A46,A47,A48,A63,A52,A57;
end;
then [A,X] in Maximal_wrt ds by A42,A49,XBOOLE_0:def 10;
hence x in ck;
end;
now
let x be object;
thus x in C implies x in ck by A12;
assume x in ck;
then consider A being Subset of X such that
A64: x = A and
A65: [A, X] in Maximal_wrt ds;
[A,X] in ds by A65;
then consider aa, XX being Subset of the Attributes of DB such that
A66: [A,X] = [aa,XX] and
A67: aa >|> XX, DB;
A68: X = XX by A66,XTUPLE_0:1;
A69: now
A70: A ^|^ [#]X, ds by A65;
let K be set such that
A71: K in C and
A72: K c= A;
K in ck by A12,A71;
then consider B being Subset of X such that
A73: K = B and
A74: [B, X] in Maximal_wrt ds;
assume
A75: K <> A;
reconsider AA = A, B, XA = X as Subset of the Attributes of DB by A11;
[AA,XA] <= [B,XA] by A72,A73;
hence contradiction by A73,A74,A75,A70,Th27;
end;
set m = { a where a is Element of X: not a in A & ex K being set st K in C
& a in K };
A76: now
let x be object;
assume x in m;
then ex a being Element of X st x = a & not a in A & ex K being set st
K in C & a in K;
hence x in X;
end;
consider K being object such that
A77: K in C by A1,XBOOLE_0:def 1;
reconsider K as Subset of X by A77;
A78: A = aa by A66,XTUPLE_0:1;
assume
A79: not x in C;
then not K c= A by A64,A69,A77;
then consider k being object such that
A80: k in K and
A81: not k in A;
reconsider k as Element of X by A80;
A82: k in m by A77,A80,A81;
then consider n being object such that
A83: n in m;
reconsider m as Subset of X by A76,TARSKI:def 3;
set r0 = X --> 0, r1 = (X --> 0) +* (m --> m);
now
let K be Subset of X such that
A84: K in C;
not K c= A by A64,A69,A79,A84;
then consider k being object such that
A85: k in K and
A86: not k in A;
k in m by A84,A85,A86;
hence m/\K <> {} by A85,XBOOLE_0:def 4;
end;
then m in M;
then m in M0 by XBOOLE_0:def 3;
then
A87: r1 in R;
0 in {0} by TARSKI:def 1;
then 0 in M0 by XBOOLE_0:def 3;
then (X --> 0) +* ({}X --> {}X) in R;
then (X --> 0) +* {} in R;
then reconsider r0, r1 as Element of the Relationship of DB
by A87;
A88: dom (m --> m) = m;
now
A89: dom r1 = dom (X --> 0)\/dom (m --> m) by FUNCT_4:def 1
.= X\/dom (m --> m)
.= X\/m
.= X by XBOOLE_1:12;
dom r0 = X;
hence dom (r0|A) = dom r1 /\ A by A89,RELAT_1:61;
A90: dom (r0|A) = dom r0 /\ A by RELAT_1:61;
let x be object such that
A91: x in dom (r0|A);
A92: now
assume x in m;
then ex a being Element of X st x = a & not a in A & ex K being set
st K in C & a in K;
hence contradiction by A90,A91,XBOOLE_0:def 4;
end;
x in A by A90,A91,XBOOLE_0:def 4;
hence (r0|A).x = (X --> 0).x by FUNCT_1:49
.= r1.x by A88,A92,FUNCT_4:11;
end;
then
A93: r0|A = r1|A by FUNCT_1:46;
A94: (r1|X).n = r1.n by A83,FUNCT_1:49
.= (m --> m).n by A83,A88,FUNCT_4:13
.= m by A83,FUNCOP_1:7;
(r0|X).n = r0.n
.= 0;
hence contradiction by A82,A93,A67,A78,A68,A94;
end;
hence thesis by TARSKI:2;
end;
begin :: 9. Applications
definition
let X be set, F be Dependency-set of X;
attr F is (DC4) means
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
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
for A, B, C being Subset of X st [A, B] in F holds [A\/C, B] in F;
end;
theorem :: 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 :: APP1:
for X being set, F being Dependency-set of X holds F is (F1) (F2) (F3)
(F4) iff F is (DC1) (DC3) (DC4)
proof
let X be set, F be Dependency-set of X;
hereby
assume that
A1: F is (F1) and
A2: F is (F2) and
A3: F is (F3) and
A4: F is (F4);
thus F is (DC1) by A2;
thus F is (DC3) by A1,A3;
thus F is (DC4)
proof
let A, B, C be Subset of X;
assume that
A5: [A, B] in F and
A6: [A, C] in F;
[A\/A, B\/C] in F by A4,A5,A6;
hence thesis;
end;
end;
assume that
A7: F is (DC1) and
A8: F is (DC3) and
A9: F is (DC4);
thus F is (F1) by A8;
thus F is (F2) by A7;
thus F is (F3) by A7,A8;
let A, B, A9, B9 be Subset of X such that
A10: [A, B] in F and
A11: [A9, B9] in F;
A9 c= A\/A9 by XBOOLE_1:7;
then [A\/A9, A9] in F by A8;
then
A12: [A\/A9, B9] in F by A7,A11,Th18;
A c= A\/A9 by XBOOLE_1:7;
then [A\/A9, A] in F by A8;
then [A\/A9, B] in F by A7,A10,Th18;
hence thesis by A9,A12;
end;
theorem :: APP2:
for X being set, F being Dependency-set of X holds F is (F1) (F2) (F3)
(F4) iff F is (DC2) (DC5) (DC6)
proof
let X be set, F be Dependency-set of X;
hereby
assume that
A1: F is (F1) and
A2: F is (F2) and
A3: F is (F3) and
A4: F is (F4);
thus F is (DC2) by A1;
thus F is (DC5)
proof
let A, B, C, D be Subset of X such that
A5: [A, B] in F and
A6: [B\/C, D] in F;
[C, C] in F by A1;
then [A\/C, B\/C] in F by A4,A5;
hence thesis by A2,A6,Th18;
end;
thus F is (DC6)
proof
let A, B, C be Subset of X such that
A7: [A, B] in F;
A c= A\/C by XBOOLE_1:7;
then [A\/C, A] in F by A1,A3,Def15;
hence thesis by A2,A7,Th18;
end;
end;
assume that
A8: F is (DC2) and
A9: F is (DC5) and
A10: F is (DC6);
thus F is (F1) by A8;
A11: now
let A, B, C be Subset of X such that
A12: [A, B] in F and
A13: [B, C] in F;
[B\/A, C] in F by A10,A13;
then [A\/A, C] in F by A9,A12;
hence [A, C] in F;
end;
hence F is (F2) by Th18;
thus F is (F3)
proof
let A, B, A9, B9 be Subset of X such that
A14: [A, B] in F and
A15: [A, B] >= [A9, B9];
A c= A9 by A15;
then A9 = A\/(A9\A) by XBOOLE_1:45;
then
A16: [A9, B] in F by A10,A14;
B9 c= B by A15;
then
A17: B = B9\/(B\B9) by XBOOLE_1:45;
[B9, B9] in F by A8;
then [ B, B9] in F by A10,A17;
hence thesis by A11,A16;
end;
let A, B, A9, B9 be Subset of X such that
A18: [A, B] in F and
A19: [A9, B9] in F;
[B\/B9, B\/B9] in F by A8;
then [A\/B9, B\/B9] in F by A9,A18;
hence thesis by A9,A19;
end;
definition
let X be set, F be Dependency-set of X;
func charact_set F -> set equals
{ 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;
end;
theorem Th55:
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
proof
let X, A be set, F be Dependency-set of X;
assume A in charact_set F;
then
ex Y being Subset of X st A = Y & ex a, b being Subset of X st [a, b] in
F & a c= Y & not b c= Y;
hence thesis;
end;
theorem
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 Th57: :: 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
proof
let A be finite non empty set, F be Dependency-set of A;
set G = Dependency-closure F;
set B = (bool A) \ charact_set F;
set BB = {b where b is Subset of A : for x, y being Subset of A st [x, y] in
F & x c= b holds y c= b};
now
let c be object;
reconsider cc = c as set by TARSKI:1;
hereby
assume
A1: c in B;
then not c in charact_set F by XBOOLE_0:def 5;
then
for x, y being Subset of A st [x,y] in F & x c= cc holds y c= cc by A1;
hence c in BB by A1;
end;
assume c in BB;
then consider b being Subset of A such that
A2: c = b and
A3: for x, y being Subset of A st [x,y] in F & x c= b holds y c= b;
not b in charact_set F by A3,Th55;
hence c in B by A2,XBOOLE_0:def 5;
end;
then
A4: B = BB by TARSKI:2;
reconsider B as Subset-Family of A;
A5: BB = enclosure_of F;
then
A6: B is (B2) by A4,Th36;
set FF = {[a, b] where a, b is Subset of A : for c being set st c in B & a
c= c holds b c= c};
A7: FF = A deps_encl_by B;
then reconsider FF as Dependency-set of A;
F c= G by Def24;
then
A8: FF c= G by A4,A5,A7,Th37;
A9: FF is full_family by A7,Th33;
F c= FF by A4,A5,A7,Th37;
then
A10: G c= FF by A9,Def24;
hereby
let X, Y be Subset of A;
hereby
assume [X, Y] in G;
then [X,Y] in FF by A10;
then consider a9, b9 being Subset of A such that
A11: [a9,b9] = [X,Y] and
A12: for c being set st c in B & a9 c= c holds b9 c= c;
A13: b9 = Y by A11,XTUPLE_0:1;
let a be Subset of A such that
A14: X c= a and
A15: not Y c= a;
assume not a in charact_set F;
then
A16: a in B by XBOOLE_0:def 5;
a9 = X by A11,XTUPLE_0:1;
hence contradiction by A14,A15,A12,A13,A16;
end;
assume
A17: for a being Subset of A st X c= a & not Y c= a holds a in charact_set F;
now
let c be set such that
A18: c in B and
A19: X c= c and
A20: not Y c= c;
reconsider c as Subset of A by A18;
not c in charact_set F by A18,XBOOLE_0:def 5;
hence contradiction by A17,A19,A20;
end;
then [X,Y] in FF;
hence [X, Y] in G by A8;
end;
for x, y be Subset of A st [x, y] in F & x c= A holds y c= A;
then not [#]A in charact_set F by Th55;
then A in B by XBOOLE_0:def 5;
then
A21: B is (B1);
G = FF by A10,A8,XBOOLE_0:def 10;
hence thesis by A21,A6,A7,Th35;
end;
theorem :: 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
proof
let A be finite non empty set, F, G be Dependency-set of A such that
A1: charact_set F = charact_set G;
set DCF = Dependency-closure F, DCG = Dependency-closure G;
now
let x be object;
hereby
assume
A2: x in DCF;
then consider a, b being Subset of A such that
A3: x = [a,b] by Th9;
for c be Subset of A st a c= c & not b c= c holds c in charact_set G
by A1,A2,A3,Th57;
hence x in DCG by A3,Th57;
end;
assume
A4: x in DCG;
then consider a, b being Subset of A such that
A5: x = [a,b] by Th9;
for c be Subset of A st a c= c & not b c= c holds c in charact_set F
by A1,A4,A5,Th57;
hence x in DCF by A5,Th57;
end;
hence thesis by TARSKI:2;
end;
theorem Th59:
for X being non empty finite set, F being Dependency-set of X
holds charact_set F = charact_set (Dependency-closure F)
proof
let X be non empty finite set, F be Dependency-set of X;
set dcF = Dependency-closure F;
now
set B = {c where c is Subset of X : for x, y being Subset of X st [x, y]
in F & x c= c holds y c= c};
let A be object;
reconsider AA=A as set by TARSKI:1;
hereby
A1: F c= dcF by Def24;
assume
A2: A in charact_set F;
then
A3: A is Subset of X by Th55;
ex x, y being Subset of X st [x, y] in F & x c= AA & not y c= AA
by A2,Th55;
hence A in charact_set dcF by A1,A3;
end;
assume
A4: A in charact_set dcF;
then consider x, y being Subset of X such that
A5: [x, y] in dcF and
A6: x c= AA and
A7: not y c= AA by Th55;
A8: A is Subset of X by A4,Th55;
assume not A in charact_set F;
then for x, y being Subset of X st [x, y] in F & x c= AA holds y c= AA
by A8;
then
A9: A in B by A8;
B = enclosure_of F;
then Dependency-closure F = X deps_encl_by B by Th38;
then consider a, b being Subset of X such that
A10: [x, y] = [a,b] and
A11: for c being set st c in B & a c= c holds b c= c by A5;
A12: y = b by A10,XTUPLE_0:1;
x = a by A10,XTUPLE_0:1;
hence contradiction by A6,A7,A11,A12,A9;
end;
hence thesis by TARSKI:2;
end;
definition
let A be set, K be set, F be Dependency-set of A;
pred K is_p_i_w_ncv_of F means
( 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 :: 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
proof
let X be finite non empty set, F be Dependency-set of X, K be Subset of X;
set dcF = Dependency-closure F;
set S = {P where P is Subset of X : [K, P] in dcF };
S c= bool X
proof
let x be object;
assume x in S;
then ex P being Subset of X st x = P & [K, P] in dcF;
hence thesis;
end;
then reconsider S as Subset-Family of X;
set ck = candidate-keys dcF;
set B = {c where c is Subset of X : for x, y being Subset of X st [x, y] in
F & x c= c holds y c= c};
[K, K] in dcF by Def11;
then K in S;
then consider m being set such that
A1: m in S and
A2: for B being set st B in S holds m c= B implies B = m by FINSET_1:6;
B = enclosure_of F;
then
A3: dcF = X deps_encl_by B by Th38;
hereby
assume K in ck;
then consider A being Subset of X such that
A4: K = A and
A5: [A, X] in Maximal_wrt dcF;
A6: A ^|^ X, dcF by A5;
[A, [#]X] in dcF by A5;
then consider a, b being Subset of X such that
A7: [A,X] = [a,b] and
A8: for c being set st c in B & a c= c holds b c= c by A3;
A9: X = b by A7,XTUPLE_0:1;
A10: A = a by A7,XTUPLE_0:1;
thus K is_p_i_w_ncv_of F
proof
hereby
let z be Subset of X such that
A11: K c= z and
A12: z <> X and
A13: not z in charact_set F;
for x, y being Subset of X st [x,y]in F & x c=z holds y c=z by A13;
then z in B;
then X c= z by A4,A8,A10,A9,A11;
hence contradiction by A12,XBOOLE_0:def 10;
end;
let k be set;
assume
A14: k c< K;
then k c= A by A4,XBOOLE_0:def 8;
then reconsider k as Subset of X by XBOOLE_1:1;
set S = {P where P is Subset of X : [k, P] in dcF };
S c= bool X
proof
let x be object;
assume x in S;
then ex P being Subset of X st x = P & [k, P] in dcF;
hence thesis;
end;
then reconsider S as Subset-Family of X;
[k, k] in dcF by Def11;
then k in S;
then consider m being set such that
A15: m in S and
A16: for B being set st B in S holds m c= B implies B =m by FINSET_1:6;
consider P being Subset of X such that
A17: m = P and
A18: [k, P] in dcF by A15;
[k, k] in dcF by Def11;
then
A19: [k\/k, k\/P] in dcF by A18,Def13;
assume
A20: not thesis;
A21: [k, [#]X] in dcF
proof
per cases;
suppose
k\/P = X;
hence thesis by A19;
end;
suppose
k\/P <> X;
then k\/P in charact_set F by A20,XBOOLE_1:7;
then k\/P in charact_set dcF by Th59;
then consider x, y being Subset of X such that
A22: [x, y] in dcF and
A23: x c= k\/P and
A24: not y c= k\/P by Th55;
[k\/P, k\/P] in dcF by Def11;
then [x\/(k\/P), y\/(k\/P)] in dcF by A22,Def13;
then [k\/P, y\/(k\/P)] in dcF by A23,XBOOLE_1:12;
then [k, y\/(k\/P)] in dcF by A19,Th18;
then
A25: y\/(k\/P) in S;
P c= k\/P by XBOOLE_1:7;
then P = (y\/(k\/P)) by A16,A17,A25,XBOOLE_1:10;
hence thesis by A24,XBOOLE_1:7,10;
end;
end;
k c= K by A14,XBOOLE_0:def 8;
then [K,[#]X] <= [k,[#]X];
hence contradiction by A4,A6,A14,A21,Th27;
end;
end;
consider P being Subset of X such that
A26: m = P and
A27: [K, P] in dcF by A1;
[K, K] in dcF by Def11;
then
A28: [K\/K, K\/P] in dcF by A27,Def13;
assume
A29: K is_p_i_w_ncv_of F;
A30: K c= K\/P by XBOOLE_1:7;
A31: [K, [#]X] in dcF
proof
per cases;
suppose
K\/P = X;
hence thesis by A28;
end;
suppose
K\/P <> X;
then K\/P in charact_set F by A29,A30;
then K\/P in charact_set dcF by Th59;
then consider x, y being Subset of X such that
A32: [x, y] in dcF and
A33: x c= K\/P and
A34: not y c= K\/P by Th55;
[K\/P, K\/P] in dcF by Def11;
then [x\/(K\/P), y\/(K\/P)] in dcF by A32,Def13;
then [K\/P, y\/(K\/P)] in dcF by A33,XBOOLE_1:12;
then [K, y\/(K\/P)] in dcF by A28,Th18;
then
A35: y\/(K\/P) in S;
P c= K\/P by XBOOLE_1:7;
then P = (y\/(K\/P)) by A2,A26,A35,XBOOLE_1:10;
hence thesis by A34,XBOOLE_1:7,10;
end;
end;
now
let x9, y9 be Subset of X such that
A36: [x9, y9] in dcF and
A37: K <> x9 or X <> y9 and
A38: [K, [#]X] <= [x9,y9];
A39: X c= y9 by A38;
x9 c= K by A38;
then x9 c< K by A37,A39,XBOOLE_0:def 8,def 10;
then consider a being Subset of X such that
A40: x9 c= a and
A41: a <> X and
A42: not a in charact_set F by A29;
X = y9 by A39,XBOOLE_0:def 10;
then
A43: not y9 c= a by A41,XBOOLE_0:def 10;
not a in charact_set dcF by A42,Th59;
hence contradiction by A36,A40,A43;
end;
then K ^|^ X, dcF by A31,Th27;
then [K,X] in Maximal_wrt dcF;
hence thesis;
end;