:: Armstrong's Axioms :: by William W. Armstrong , Yatsuka Nakamura and Piotr Rudnicki :: :: Received October 25, 2002 :: Copyright (c) 2002 Association of Mizar Users environ vocabularies ARMSTRNG, BOOLE, RELAT_1, RELAT_2, FINSET_1, FUNCT_1, FUNCT_4, CARD_3, PBOOLE, ZF_REFLE, MCART_1, ORDERS_1, SETFAM_1, INT_1, EQREL_1, WAYBEL_4, SUBSET_1, CANTOR_1, CARD_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, MARGREL1, MATRLIN, BINARITH, BINARI_3, ZF_LANG, MIDSP_3, POWER, EUCLID, FINSEQ_4, CONLAT_1, FINSUB_1, PARTFUN1, ARYTM; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, FINSUB_1, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, PARTFUN1, CARD_1, NUMBERS, FUNCT_4, FUNCT_1, ORDERS_2, MCART_1, EQREL_1, CARD_3, PBOOLE, STRUCT_0, WAYBEL_4, FINSEQ_1, PRE_CIRC, MARGREL1, FUNCT_2, FINSEQ_2, MATRLIN, BINARITH, BINARI_3, SERIES_1, EUCLID, XXREAL_0, NAT_1; constructors SETFAM_1, FINSUB_1, XXREAL_0, NAT_1, CARD_3, FINSEQOP, SERIES_1, BINARITH, PRE_CIRC, EUCLID, MATRLIN, WAYBEL_4, BINARI_3, BINOP_2; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, FRAENKEL, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, EQREL_1, MARGREL1, FINSEQ_2, CARD_3, PBOOLE, ORDERS_2, ALTCAT_1, MATRLIN, GOBRD13; requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM; definitions TARSKI, RELAT_2, YELLOW_0, MATRLIN, WAYBEL_4, FINSUB_1, FINSEQ_2, SUBSET_1, XBOOLEAN; theorems TARSKI, RELSET_1, ZFMISC_1, EQREL_1, MCART_1, RELAT_1, RELAT_2, XBOOLE_0, XBOOLE_1, ORDERS_2, STRUCT_0, ENUMSET1, BAGORDER, WAYBEL_4, POLYNOM1, 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, PBOOLE, FUNCT_2, MATRLIN, BINARITH, POWER, REAL_1, FUNCT_4, FINSUB_1, PARTFUN1, NUMBERS, XREAL_1, ORDERS_1, XXREAL_0, ORDINAL1, CARD_2; schemes FINSET_1, NAT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, XBOOLE_0, CLASSES1; begin Lm1: now let n be Element of NAT, X be non empty set, t be Tuple of n,X; len t = n by FINSEQ_2:109; 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: S is finite; A5: P[{}] by A2,SETFAM_1:def 10; A6: now let x be set, b be set such that A7: x in S and A8: b c= S and A9: P[b]; thus P[ b\/{x}] proof let sf be Subset-Family of X such that A10: sf = b\/{x}; reconsider sx = x as Subset of X by A7; reconsider fb = b as Subset-Family of X by A8,XBOOLE_1:1; reconsider fx = {x} as Subset-Family of X by A7,ZFMISC_1:37; A11: Intersect fb in B by A9; Intersect (fb\/fx) = Intersect fb /\ Intersect fx by MSSUBFAM:8 .= Intersect fb /\ sx by MSSUBFAM:9; hence Intersect sf in B by A1,A3,A7,A10,A11,FINSUB_1:def 2; end; end; P[S] from FINSET_1:sch 2(A4,A5,A6); hence Intersect S in B; end; registration cluster reflexive antisymmetric transitive non empty Relation; existence proof set R = {[{},{}]}; reconsider R as Relation; A1: field R = {{},{}} by RELAT_1:32 .= {{}} by ENUMSET1:69; take R; thus R is reflexive proof let x be set; assume x in field R; then x = {} by A1,TARSKI:def 1; hence [x,x] in R by TARSKI:def 1; end; thus R is antisymmetric proof let x, y be set; assume x in field R & y in field R & [x,y] in R & [y,x] in R; then x = {} & y = {} by A1,TARSKI:def 1; hence thesis; end; thus R is transitive proof let x, y, z be set; assume x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R; then x = {} & z = {} by A1,TARSKI:def 1; hence [x,z] in R by TARSKI:def 1; end; thus R is non empty; 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; assume A1: X <> {}; reconsider IR = R as Relation of field R by POLYNOM1:4; set S = RelStr(# field R, IR #); set CR = the carrier of S; set ir = the InternalRel of S; A2: CR is non empty by A1; A3: R is_antisymmetric_in field R by RELAT_2:def 12; A4: S is antisymmetric proof let x, y be Element of S; assume x <= y & y <= x; then [x,y] in ir & [y,x] in ir by ORDERS_2:def 9; hence x = y by A2,A3,RELAT_2:def 4; end; A5: R is_transitive_in field R by RELAT_2:def 16; S is transitive proof let x, y, z be Element of S; assume x <= y & y <= z; then [x,y] in ir & [y,z] in ir by ORDERS_2:def 9; then [x,z] in ir by A2,A5,RELAT_2:def 8; hence x <= z by ORDERS_2:def 9; end; then reconsider S as antisymmetric transitive non empty RelStr by A2,A4; reconsider Y = X as finite Subset of CR; consider x being Element of S such that A6: x in Y & x is_maximal_wrt Y, the InternalRel of S by A1,BAGORDER:7; reconsider x as Element of X by A6; take x; thus x in X by A6; given y being set such that A7: y in X & y <> x & [x, y] in R; thus thesis by A6,A7,WAYBEL_4:def 24; 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 set holds x in X1 iff x in X2 proof let x be set; hereby assume x in X1; then P[x] by A1; hence x in X2 by A2; end; assume x in X2; then P[x] by A2; hence thesis by A1; end; hence thesis by TARSKI:2; end; definition let X be set, R be Relation; func R Maximal_in X -> Subset of X means :Def1: for x being set holds x in it iff x is_maximal_wrt X, R; existence proof defpred P[set] means $1 is_maximal_wrt X, R; consider I being set such that A1: for x being set holds x in I iff x in X & P[x] from XBOOLE_0:sch 1; for x being set 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 set; thus x in I implies x is_maximal_wrt X, R by A1; assume A2: x is_maximal_wrt X, R; then x in X by WAYBEL_4:def 24; hence x in I by A1,A2; end; uniqueness proof defpred P[set] means $1 is_maximal_wrt X, R; 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; definition let x, X be set; pred x is_/\-irreducible_in X means :Def2: 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 set; assume x in irr; then consider z being Element of X such that A1: x = z & z is_/\-irreducible_in X; thus x in X by A1; end; then reconsider irr as Subset of X; take irr; let x be set; hereby assume x in irr; then consider z being Element of X such that A2: x = z & z is_/\-irreducible_in X; thus x is_/\-irreducible_in X by A2; end; assume A3: x is_/\-irreducible_in X; then x in X by Def2; hence x in irr by A3; 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 set; assume x1 in U(x); then ex xx being Element of X() st x1 = xx & x c= xx; hence x1 in X(); end; then reconsider Ux = U(x) as finite set; A5: ex k being Nat st R[k] proof take k = card Ux; reconsider x as Element of X() by A3; take x; thus Card U(x) = k; thus not P[x] 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 s is_/\-reducible_in X(); then consider z, y being set such that A10: z in X() & y in X() and A11: s = z /\ y and A12: s <> z & s <> y by Def2; A13: s c= z & s c= y by A11,XBOOLE_1:17; U(s) c= X() proof let x be set; assume x in U(s); then ex xx being Element of X() st x = xx & s c= xx; hence x in X(); end; then reconsider Us = U(s) as finite set; U(y) c= X() proof let x be set; assume x in U(y); then ex xx being Element of X() st x = xx & y c= xx; hence x in X(); end; then reconsider Uy = U(y) as finite set; U(z) c= X() proof let x be set; assume x in U(z); then ex xx being Element of X() st x = xx & z c= xx; hence x in X(); end; then reconsider Uz = U(z) as finite set; reconsider y, z as Element of X() by A10; A14: now assume s in Uz; then ex x being Element of X() st s = x & z c= x; hence contradiction by A12,A13,XBOOLE_0:def 10; end; now assume s in Uy; then ex x being Element of X() st s = x & y c= x; hence contradiction by A12,A13,XBOOLE_0:def 10; end; then A15: Uz <> Us & Uy <> Us by A14; A16: Uz c= Us proof let x be set; assume x in Uz; then consider xx being Element of X() such that A17: x = xx and A18: z c= xx; s c= xx by A13,A18,XBOOLE_1:1; hence x in Us by A17; end; Uy c= Us proof let x be set; 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 A13,A20,XBOOLE_1:1; hence x in Us by A19; end; then Uz c< Us & Uy c< Us by A15,A16,XBOOLE_0:def 8; then card Us > card Uz & card Us > card Uy by TREES_1:24; then P[z] & P[y] by A7,A8; hence contradiction by A2,A9,A11; 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 be set; assume A2: x is_/\-irreducible_in X; thus P[x] proof x in X by A2,Def2; then reconsider S = {x} as non empty Subset of X by ZFMISC_1:37; take S; thus x = meet S by SETFAM_1:11; let s be set; assume s in S; hence s is_/\-irreducible_in X by A2,TARSKI:def 1; end; end; A3: now let x, y be set such that x in X & y in X and A4: P[x] and A5: P[y]; 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 A4; consider Sy being non empty Subset of X such that A8: y = meet Sy and A9: for s being set st s in Sy holds s is_/\-irreducible_in X by A5; reconsider S = Sx\/Sy as non empty Subset of X; now take S; thus x /\ y = meet S by A6,A8,SETFAM_1:10; let s be set; assume A10: s in S; per cases by A10,XBOOLE_0:def 2; suppose s in Sx; hence s is_/\-irreducible_in X by A7; end; suppose s in Sy; hence s is_/\-irreducible_in X by A9; end; end; hence P[x /\ y]; end; for x being set st x in X holds P[x] from FinIntersect(A1,A3); hence thesis; end; definition let X be set, B be Subset-Family of X; attr B is (B1) means :Def4: 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) Subset-Family of X; existence proof set B = {X}; reconsider B as Subset-Family of X by ZFMISC_1:80; take B; X in B by TARSKI:def 1; hence B is (B1) by Def4; thus B is (B2) proof let a, b be set; assume a in B & b in B; then a = X & b = X by TARSKI:def 1; hence a/\b in B by 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; 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; 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; A7: S is finite; A8: P[{}]; A9: now let s, A be set such that A10: s in S and A c= S and A11: P[A]; per cases by A11; 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 A12: 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 A10,ZFMISC_1:37; A13: Intersect sf = meet sf by SETFAM_1:def 10; then A14: Intersect sf = s by SETFAM_1:11; per cases by A12; suppose A = {}; hence P[A\/{s}] by A4,A6,A10,A14; end; suppose A15: 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; A16: Intersect f = meet f by A15,SETFAM_1:def 10; A17: Intersect As = meet As by SETFAM_1:def 10 .= meet A /\ meet sf by A15,SETFAM_1:10; thus P[A\/{s}] proof per cases; suppose A18: Intersect As <> x; Intersect As in B by A1,A4,A10,A13,A14,A15,A16,A17, FINSUB_1:def 2; hence thesis by A18; end; suppose Intersect As = x; hence thesis by A4,A6,A10,A13,A14,A15,A16,A17; end; end; end; end; end; end; P[S] from FINSET_1:sch 2(A7,A8,A9); then consider f being Subset-Family of X such that A19: S = {} or S = f & Intersect f <> x by A2,Def2; thus thesis by A3,A5,A19,SETFAM_1:def 10; end; registration let X, D be non empty set, n be Element of NAT; cluster -> FinSequence-yielding Function of X, n-tuples_on D; coherence proof let f be Function of X, n-tuples_on D; let x be set; assume x in dom f; then reconsider fx = f.x as Element of n-tuples_on D by FUNCT_2:7; fx = f.x; hence f.x is FinSequence; end; end; registration let f be FinSequence-yielding Function, x be set; cluster f.x -> FinSequence-like; coherence proof per cases; suppose x in dom f; hence thesis by MATRLIN:def 1; end; suppose not x in dom f; hence thesis by FUNCT_1:def 4; end; end; end; definition :: cannot redefine from VALUAT for I need to use functions from :: BINARI* and they are on Tuple of 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 A4: i in Seg n; thus thesis by A2,A4,A3; end; uniqueness proof let it1, it2 be Element of n-tuples_on BOOLEAN such that A5: for i being set st i in Seg n holds it1.i = (p/.i) '&' (q/.i) and A6: for i being set st i in Seg n holds it2.i = (p/.i) '&' (q/.i); now A7: dom it1 = Seg n by Lm1; hence dom it1 = dom it2 by Lm1; let x be set; assume A8: x in dom it1; hence it1.x = (p/.x) '&' (q/.x) by A5,A7 .=it2.x by A6,A7,A8; end; hence it1 = it2 by FUNCT_1:9; end; commutativity; end; theorem Th5: for n being Element of NAT, p being Tuple of n, BOOLEAN holds (n-BinarySequence 0) '&' p = n-BinarySequence 0 proof let n be Element of NAT, p be Tuple of n, BOOLEAN; set B = n-BinarySequence 0; now let x be set; A1: dom (B '&' p) = Seg n by Lm1; hence dom (B '&' p) = dom B by Lm1; let x be set; assume A2: x in dom (B '&' p); A3: dom B = Seg n by Lm1; A4: B = 0*n by BINARI_3:26 .= n |-> 0 by EUCLID:def 4; then B.x = 0 by A1,A2,FUNCOP_1:13; then B/.x = FALSE by A1,A2,A3,PARTFUN1:def 8; hence (B '&' p).x = FALSE '&' (p/.x) by A1,A2,Def5 .= B.x by A1,A2,A4,FUNCOP_1:13; end; hence (n-BinarySequence 0) '&' p = (n-BinarySequence 0) by FUNCT_1:9; 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 (nB '&' p) = Seg n by Lm1; hence A2: dom (nB '&' p) = dom p by Lm1; let x be set; assume A3: x in dom (nB '&' p); then reconsider k=x as Element of NAT; A4: B = 0*n by BINARI_3:26 .= n |-> 0 by EUCLID:def 4; A5: dom B = Seg n by Lm1; B.x = 0 by A1,A3,A4,FUNCOP_1:13; then A6: B/.x = FALSE by A1,A3,A5,PARTFUN1:def 8; nB/.x = 'not' (B/.k) by A1,A3,BINARITH:def 4 .= TRUE by A6; hence (nB '&' p).x = TRUE '&' (p/.x) by A1,A3,Def5 .= p.x by A2,A3,PARTFUN1:def 8; end; hence 'not' (n-BinarySequence 0) '&' p = p by FUNCT_1:9; end; canceled; theorem Th8: 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; set B = n-BinarySequence 2 to_power i; deffunc B(Nat) = $1-BinarySequence 2 to_power i; defpred P[Nat] means i < $1 implies B($1).(i+1) = TRUE; A2: P[0]; A3: now let n be Element of NAT such that A4: P[n]; now assume i < n+1; then A5: i <= n by NAT_1:13; per cases by A5,REAL_1:def 5; suppose A6: n = 0; then A7: i = 0 by A5; 0*n = n |-> 0 by EUCLID:def 4; then dom 0*n =Seg n by FUNCOP_1:19; then A8: len 0*n = n by FINSEQ_1:def 3; dom <*TRUE*> =Seg 1 by FINSEQ_1:55; then A9: 1 in dom <*TRUE*> by FINSEQ_1:3; thus B(n+1).(i+1) = (0*n^<*TRUE*>).(i+1) by A6,A7,BINARI_3:29 .= <*TRUE*>.1 by A6,A7,A8,A9,FINSEQ_1:def 7 .= TRUE by FINSEQ_1:57; end; suppose A10: n > 0 & n = i; 0*n = n |-> 0 by EUCLID:def 4; then dom 0*n = Seg n by FUNCOP_1: 19; then A11: len 0*n = n by FINSEQ_1:def 3; dom <*TRUE*> = Seg 1 by FINSEQ_1:55; then A12: 1 in dom <*TRUE*> by FINSEQ_1:3; thus B(n+1).(i+1) = (0*n^<*TRUE*>).(i+1) by A10,BINARI_3:29 .= <*TRUE*>.1 by A10,A11,A12,FINSEQ_1:def 7 .= TRUE by FINSEQ_1:57; end; suppose A13: n > 0 & n > i; then reconsider n' = n as non empty Element of NAT; A14: 2 to_power i < 2 to_power n by A13,POWER:44; A15: 0+1 <= i+1 by XREAL_1:8; i+1 <= n by A13,NAT_1:13; then i+1 in Seg n by A15,FINSEQ_1:3; then A16: i+1 in dom B(n) by Lm1; thus B(n+1).(i+1) = (B(n')^<*FALSE*>).(i+1) by A14,BINARI_3:28 .= TRUE by A4,A13,A16,FINSEQ_1:def 7; end; end; hence P[n+1]; end; A17: for n being Element of NAT holds P[n] from NAT_1:sch 1(A2,A3); defpred P[Element of NAT] means i < $1 implies for j being Element of NAT st i+1 <=j & j <= $1 holds B($1).(j+1)= FALSE; A18: P[0]; A19: now let n be Element of NAT such that A20: P[n]; now assume A21: i < n+1; let j be Element of NAT such that A22: i+1 <=j & j <= n+1; A23: i <= n by A21,NAT_1:13; A24: 0+1 <= i+1 by XREAL_1:8; per cases by A23,REAL_1:def 5; suppose A25: n = 0; A26: dom B(n+1) = Seg (n+1) by Lm1; 1 <= j by A22,A24,XXREAL_0:2; then j = 1 by A22,A25,XXREAL_0:1; then not j+1 in dom B(n+1) by A25,A26,FINSEQ_1:3; hence B(n+1).(j+1) = FALSE by FUNCT_1:def 4; end; suppose A27: n > 0 & n = i; A28: dom B(n+1) = Seg (n+1) by Lm1; j+1 > n+1 by A22,A27,NAT_1:13; then not j+1 in dom B(n+1) by A28,FINSEQ_1:3; hence B(n+1).(j+1) = FALSE by FUNCT_1:def 4; end; suppose A29: n > 0 & n > i; then reconsider n' = n as non empty Element of NAT; A30: 2 to_power i < 2 to_power n by A29,POWER:44; thus B(n+1).(j+1) = FALSE proof j n+1 by A32,NAT_1:13; then not j+1 in dom B(n+1) by A33,FINSEQ_1:3; hence B(n+1).(j+1) = FALSE by FUNCT_1:def 4; end; suppose A34: j = n; dom B(n) = Seg n by Lm1; then A35: j = len B(n) by A34,FINSEQ_1:def 3; dom <*FALSE*> = Seg 1 by FINSEQ_1:55; then A36: 1 in dom <*FALSE*> by FINSEQ_1:3; thus B(n+1).(j+1) = (B(n')^<*FALSE*>).(j+1) by A30,BINARI_3:28 .= <*FALSE*>.1 by A35,A36,FINSEQ_1:def 7 .= FALSE by FINSEQ_1:57; end; suppose A37: j < n; A38: 1 <= j+1 by NAT_1:12; j+1 <= n by A37,NAT_1:13; then j+1 in Seg n by A38,FINSEQ_1:3; then A39: j+1 in dom B(n) by Lm1; thus B(n+1).(j+1) = (B(n')^<*FALSE*>).(j+1) by A30,BINARI_3:28 .= B(n).(j+1) by A39,FINSEQ_1:def 7 .= FALSE by A20,A22,A29,A37; end; end; end; end; hence P[n+1]; end; A40: for n being Element of NAT holds P[n] from NAT_1:sch 1(A18,A19); defpred P[Element of NAT] means i < $1 implies for j being Element of NAT st 1 <=j & j < i+1 holds B($1).j = FALSE; A41: P[0]; A42: now let n be Element of NAT such that A43: P[n]; now assume A44: i < n+1; let j be Element of NAT such that A45: 1 <=j & j < i+1; A46: i <= n by A44,NAT_1:13; per cases by A46,REAL_1:def 5; suppose n = 0; then 0 <= i & i <= 0 by A44,NAT_1:13; then i = 0; hence B(n+1).j = FALSE by A45; end; suppose A47: n > 0 & i < n; then reconsider n' = n as non empty Element of NAT; A48: dom B(n) = Seg n by Lm1; j <= i & i <= n by A44,A45,NAT_1:13; then j <= n by XXREAL_0:2; then A49: j in dom B(n) by A45,A48,FINSEQ_1:3; 2 to_power i < 2 to_power n by A47,POWER:44; hence B(n+1).j = (B(n')^<*FALSE*>).j by BINARI_3:28 .= B(n).j by A49,FINSEQ_1:def 7 .= FALSE by A43,A45,A47; end; suppose A50: n > 0 & i = n; then j <= n by A45,NAT_1:13; then A51: j in Seg n by A45,FINSEQ_1:3; A52: 0*n = n |-> 0 by EUCLID:def 4; then A53: j in dom 0*n by A51,FUNCOP_1:19; thus B(n+1).j = (0*n^<*TRUE*>).j by A50,BINARI_3:29 .= (0*n).j by A53,FINSEQ_1:def 7 .= FALSE by A51,A52,FUNCOP_1:13; end; end; hence P[n+1]; end; A54: for n being Element of NAT holds P[n] from NAT_1:sch 1(A41,A42); thus B.(i+1) = 1 by A1,A17; let j be Element of NAT such that A55: j in Seg n and A56: j<>i+1; A57: 1 <= j & j <= n by A55,FINSEQ_1:3; per cases by A56,A57,REAL_1:def 5; suppose j < i+1; hence B.j = 0 by A1,A54,A57; end; suppose A58: j > i+1 & j < n; then consider k being Nat such that A59: j = k+1 by NAT_1:6; reconsider k as Element of NAT by ORDINAL1:def 13; A60: i+1 <= k by A58,A59,NAT_1:13; k <= n by A58,A59,NAT_1:13; hence B.j = 0 by A1,A40,A59,A60; end; suppose A61: j > i+1 & j = n; then consider m being Nat such that A62: n = m+1 by NAT_1:6; reconsider m as Element of NAT by ORDINAL1:def 13; i < m by A61,A62,XREAL_1:8; then 2 to_power i < 2 to_power m by POWER:44; hence B.j = 0 by A61,A62,BINARI_3:27; 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 Dependency-set of X; existence proof {} c= X by XBOOLE_1:2; then reconsider R = {[{},{}]} as Relation of bool X by RELSET_1:8; take R; thus R is non empty; thus R is finite; end; end; definition let X be set; canceled; func Dependencies(X) -> Dependency-set of X equals [: bool X, bool X :]; coherence by RELSET_1:def 1; 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; correctness proof let x be Element of F; thus thesis; end; end; theorem Th9: 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 set such that A2: [a, b] = x by RELAT_1:def 1; reconsider a, b as Subset of X by A1,A2,ZFMISC_1:106; take a,b; thus x = [a,b] by A2; end; given a, b being Subset of X such that A3: x = [a,b]; thus x in Dependencies X by A3,ZFMISC_1:106; end; theorem Th10: 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 set such that A2: [a, b] = x by RELAT_1:def 1; reconsider a, b as Subset of X by A1,A2,ZFMISC_1:106; take a,b; thus x = [a,b] by A2; end; definition let R be DB-Rel, A, B be Subset of the Attributes of R; pred A >|> B, R means :Def8: 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 X = {[A,B] where A,B is Subset of the Attributes of R: A >|> B, R}; set at = the Attributes of R; X c= [:bool at, bool at:] proof let x be set; assume x in X; then consider A, B being Subset of at such that A1: x = [A, B] and A >|> B, R; thus x in [:bool at, bool at:] by A1,ZFMISC_1:def 2; end; hence thesis by RELSET_1:def 1; end; end; canceled; theorem Th12: 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] & a >|> b, D; A = a & B = b by A1,ZFMISC_1:33; hence A >|> B, D by A1; 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 :Def10: 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 Th13: :: 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 p <= q & q <= p; then p`1 c= q`1 & q`2 c= p`2 & q`1 c= p`1 & p`2 c= q`2 by Def10; then A1: p`1 = q`1 & p`2 = q`2 by XBOOLE_0:def 10; p = [p`1,p`2] & q = [q`1,q`2] by MCART_1:24; hence p = q by A1; end; theorem Th14: :: 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 p <= q & q <= r; then q`1 c= p`1 & p`2 c= q`2 & r`1 c= q`1 & q`2 c= r`2 by Def10; then r`1 c= p`1 & p`2 c= r`2 by XBOOLE_1:1; hence p <= r by Def10; end; definition let X be set, A, B be Subset of X; redefine func [A, B] -> Dependency of X; coherence by ZFMISC_1:def 2; end; theorem Th15: for X being set, A, B, A', B' being Subset of X holds [A,B] >= [A',B'] iff A c= A' & B' c= B proof let X be set, A, B, A', B' be Subset of X; [A,B]`1 = A & [A,B]`2 = B & [A',B']`1 = A' & [A',B']`2 = B' by MCART_1:def 1,def 2; hence [A,B] >= [A',B'] iff A c= A' & B' c= B by Def10; end; 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 set; assume x in Y; then consider E, F being Dependency of X such that A1: x = [E, F] and E <= F; thus thesis by A1,ZFMISC_1:def 2; end; hence thesis by RELSET_1:def 1; 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 Th17: for X being set holds dom Dependencies-Order X = [: bool X, bool X :] proof let X be set; now let x be set; thus x in dom Dependencies-Order X implies x in [: bool X, bool X :]; assume x in [: bool X, bool X :]; then reconsider x' = x as Dependency of X; [x', x'] in Dependencies-Order X; hence x in dom Dependencies-Order X by RELAT_1:def 4; end; hence dom Dependencies-Order X = [: bool X, bool X :] by TARSKI:2; end; theorem Th18: for X being set holds rng Dependencies-Order X = [: bool X, bool X :] proof let X be set; now let x be set; thus x in rng Dependencies-Order X implies x in [: bool X, bool X :]; assume x in [: bool X, bool X :]; then reconsider x' = x as Dependency of X; [x', x'] in Dependencies-Order X; hence x in rng Dependencies-Order X by RELAT_1:def 5; end; hence rng Dependencies-Order X = [: bool X, bool X :] by TARSKI:2; end; theorem Th19: 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 Th17 .= [: bool X, bool X :]\/[: bool X, bool X :] by Th18 .= [: bool X, bool X :]; end; registration let X be set; cluster Dependencies-Order X -> non empty; coherence by Th17,RELAT_1:60; cluster Dependencies-Order X -> total reflexive antisymmetric transitive; coherence proof set dox = Dependencies-Order X; set dx = Dependencies X; dx c= dom dox proof let x be set; assume x in dx; then reconsider x' = x as Element of dx; x' <= x'; then [x,x] in dox; hence thesis by RELAT_1:def 4; 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 4; dox is_reflexive_in dx proof let x be set; assume x in dx; then reconsider x' = x as Element of dx; x' <= x'; hence [x,x] in dox; end; hence dox is reflexive by A2,RELAT_2:def 9; dox is_antisymmetric_in dx proof let x, y be set; assume that x in dx & y in dx and A3: [x,y] in dox & [y,x] in dox; consider x', y' being Element of dx such that A4: [x,y]=[x',y'] & x' <= y' by A3; consider y'', x'' being Element of dx such that A5: [y,x]=[y'',x''] & y'' <= x'' by A3; x = x' & x = x'' & y = y' & y = y'' by A4,A5,ZFMISC_1:33; hence x = y by A4,A5,Th13; end; hence dox is antisymmetric by A2,RELAT_2:def 12; dox is_transitive_in dx proof let x, y, z be set; assume that x in dx & y in dx & z in dx and A6: [x,y] in dox & [y,z] in dox; consider x', y' being Element of dx such that A7: [x,y]=[x',y'] & x' <= y' by A6; consider y'', z' being Element of dx such that A8: [y,z]=[y'',z'] & y'' <= z' by A6; A9: x = x' & y = y' & y = y'' & z = z' by A7,A8,ZFMISC_1:33; then x' <= z' by A7,A8,Th14; hence [x,z] in dox by A9; end; hence dox is transitive by A2,RELAT_2:def 16; 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 : Def12: 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 Th20: 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 by RELAT_2:def 16; let A, B, C be Subset of X; assume A2: [A, B] in F & [B, C] in F; then A in field F & B in field F & C in field F by RELAT_1:30; hence [A, C] in F by A1,A2,RELAT_2:def 8; end; assume A3: 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 set such that A4: x in field F & y in field F & z in field F & [x,y] in F & [y,z] in F; field F c= bool X\/bool X by RELSET_1:19; then reconsider A = x, B = y, C = z as Subset of X by A4; [A, B] in F & [B, C] in F by A4; hence [x,z] in F by A3; end; definition let X be set, F be Dependency-set of X; attr F is (F3) means : Def13: for A, B, A', B' being Subset of X st [A, B] in F & [A, B] >= [A', B'] holds [A', B'] in F; attr F is (F4) means : Def14: for A, B, A', B' being Subset of X st [A, B] in F & [A', B'] in F holds [A\/A', B\/B'] in F; end; theorem Th21: for X being set holds Dependencies X is (F1) (F2) (F3) (F4) proof let X be set; set D = Dependencies X; D = nabla bool X by EQREL_1:def 1; then A1: field D = bool X by ORDERS_1:97; thus D is (F1) proof let A be Subset of X; thus [A, A] in D; end; thus D is (F2) proof let x, y, z be set; assume x in field D & y in field D & z in field D & [x,y] in D & [y,z] in D; hence [x,z] in D by A1,ZFMISC_1:def 2; end; thus D is (F3) proof let A, B, A', B' be Subset of X; thus thesis; end; thus D is (F4) proof let A, B, A', B' being Subset of X; thus thesis; end; end; registration let X be set; cluster (F1) (F2) (F3) (F4) non empty Dependency-set of X; existence proof take Dependencies X; thus thesis by Th21; end; end; definition let X be set, F be Dependency-set of X; attr F is full_family means : Def15: F is (F1) (F2) (F3) (F4); end; registration let X be set; cluster full_family Dependency-set of X; existence proof consider D being (F1) (F2) (F3) (F4) non empty Dependency-set of X; take D; thus thesis by Def15; 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 Full-family of X; existence proof consider D being (F1) (F2) (F3) (F4) non empty Dependency-set of X; reconsider D as Full-family of X by Def15; take D; thus thesis; end; cluster -> finite Dependency-set of X; coherence; end; registration let X be set; cluster full_family -> (F1) (F2) (F3) (F4) Dependency-set of X; coherence by Def15; cluster (F1) (F2) (F3) (F4) -> full_family Dependency-set of X; correctness by Def15; end; definition let X be set, F be Dependency-set of X; attr F is (DC3) means :Def16: 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) 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 such that A2: B c= A; A3: [A, A] in F by A1,Def12; [A, A] >= [A, B] by A2,Th15; hence [A, B] in F by A1,A3,Def13; end; cluster (DC3) (F2) -> (F1) (F3) Dependency-set of X; coherence proof let F be Dependency-set of X; assume A4: F is (DC3) (F2); thus F is (F1) proof let A be Subset of X; thus [A, A] in F by A4,Def16; end; let A, B, A', B' be Subset of X; assume A5: [A, B] in F; assume [A, B] >= [A', B']; then A c= A' & B' c= B by Th15; then [A', A] in F & [B, B'] in F by A4,Def16; then [A', B] in F & [B, B'] in F by A4,A5,Th20; hence [A', B'] in F by A4,Th20; end; end; registration let X be set; cluster (DC3) (F2) (F4) non empty Dependency-set of X; existence proof consider D being (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 Dependency-set of X; coherence by Def12; end; theorem Th25: :: 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: S is (DC3) proof let A, B being Subset of T such that A2: B c= A; A >|> B, D proof let f, g being Element of R such that A3: f|A = g|A; thus f|B = (f|A)|B by A2,RELAT_1:103 .= g|B by A2,A3,RELAT_1:103; end; hence [A, B] in S; end; A4: now let A, B, C being Subset of T; assume [A, B] in S & [B, C] in S; then A5: A >|> B, D & B >|> C, D by Th12; A >|> C, D proof let f, g being Element of R; assume f|A = g|A; then f|B = g|B by A5,Def8; hence f|C = g|C by A5,Def8; end; hence [A, C] in S; end; then A6: S is (F2) by Th20; hence S is (F1) by A1; thus S is (F2) by A4,Th20; thus S is (F3) by A1,A6; thus S is (F4) proof let A, B, A', B' being Subset of T; assume [A, B] in S & [A', B'] in S; then A7: A >|> B, D & A' >|> B', D by Th12; (A\/A') >|> (B\/B'), D proof let f, g be Element of R; assume A8: f|(A\/A') = g|(A\/A'); f|A=(f|(A\/A'))|A by RELAT_1:103,XBOOLE_1:7 .=g|A by A8,RELAT_1:103, XBOOLE_1:7; then A9: f|B = g|B by A7,Def8; f|A'=(f|(A\/A'))|A' by RELAT_1:103,XBOOLE_1:7 .=g|A' by A8,RELAT_1: 103,XBOOLE_1:7; then A10: f|B' = g|B' by A7,Def8; thus f|(B\/B')=f|B\/f|B' by RELAT_1:107 .= g|(B\/B') by A9,A10,RELAT_1:107; end; hence [A\/A', B\/B'] in S; 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 set; assume x in F; then ex A, B being Subset of X st x = [A, B] & (K c= A or B c= A); hence x in [:bool X, bool X:]; end; then reconsider F as Dependency-set of X by RELSET_1:def 1; F is full_family proof A1: now let A, B, C be Subset of X; assume A2: [A, B] in F & [B, C] in F; then consider a, b being Subset of X such that A3: [A, B] = [a, b] and A4: K c= a or b c= a; consider b1, c being Subset of X such that A5: [B, C] = [b1, c] and A6: K c= b1 or c c= b1 by A2; A7: A = a & B = b & B = b1 & C = c by A3,A5,ZFMISC_1:33; then K c= a or c c= a by A4,A6,XBOOLE_1:1; hence [A, C] in F by A7; end; then A8: F is (F2) by Th20; A9: F is (DC3) proof let A, B be Subset of X; assume B c= A; hence [A, B] in F; end; hence F is (F1) by A8; thus F is (F2) by A1,Th20; hence F is (F3) by A9; thus F is (F4) proof let A, B, A', B' be Subset of X; assume A10: [A, B] in F & [A', B'] in F; then consider a, b being Subset of X such that A11: [A, B] = [a, b] & (K c= a or b c= a); consider a', b' being Subset of X such that A12: [A', B'] = [a', b'] & (K c= a' or b' c= a') by A10; A = a & B = b & A' = a' & B' = b' by A11,A12,ZFMISC_1:33; then K c= A\/A' or B\/B' c= A\/A' by A11,A12,XBOOLE_1:10,13; hence [A\/A', B\/B'] in F; end; end; hence thesis; 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:4; 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 :Def18: [x, y] in Maximal_wrt F; end; theorem Th28: 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; 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; set DOX = Dependencies-Order X; A2: field DOX = [:bool X, bool X:] by Th19; S c= field DOX proof let a be set; assume a in S; then ex b be Element of FF st a = b & x <= b; hence a in field DOX by A2; end; then A3: S is finite Subset of field DOX by A2; 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,WAYBEL_4:def 24; then consider y being Element of FF such that A5: m = y & x <= y; consider a, b being Subset of X such that A6: m = [a, b] by A5,Th9; 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; m = e & y = f by A10,ZFMISC_1:33; then x <= y by A5,A11,Th14; then y in S; hence contradiction by A4,A8,A9,WAYBEL_4:def 24; end; hence [a,b] in Maximal_wrt F by A6,Def1; thus [a, b] >= x by A5,A6; end; theorem Th29: 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 A', B' being Subset of X st [A', B'] in F & (A <> A' or B <> B') & [A, B] <= [A', B'] 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 by Def18; then A2: [x, y] is_maximal_wrt F, DOX by Def1; thus [x, y] in F by A1; given x', y' being Subset of X such that A3: [x', y'] in F & (x <> x' or y <> y') & [x, y] <= [x',y']; A4: [x,y] <> [x',y'] by A3,ZFMISC_1:33; [[x,y],[x',y']] in DOX by A3; hence contradiction by A2,A3,A4,WAYBEL_4:def 24; end; assume A5: [x, y] in F & not ex x', y' being Subset of X st [x', y'] in F & (x <> x' or y <> y') & [x, y] <= [x',y']; [x,y] is_maximal_wrt F, DOX proof thus [x,y] in F by A5; given z being set such that A6: z in F & z <> [x,y] & [[x, y],z] in DOX; consider x',y' being set such that A7: z = [x',y'] & x' in bool X & y' in bool X by A6,RELSET_1:6; reconsider x', y' as Subset of X by A7; A8: x <> x' or y <> y' by A6,A7; consider e, f being Dependency of X such that A9: [[x, y],z] = [e, f] & e <= f by A6; e = [x,y] & f = z by A9,ZFMISC_1:33; hence contradiction by A5,A6,A7,A8,A9; end; then [x,y] in Maximal_wrt F by Def1; hence x ^|^ y, F by Def18; end; definition let X be set, M be Dependency-set of X; attr M is (M1) means : Def19: for A being Subset of X ex A', B' being Subset of X st [A', B'] >= [A, A] & [A', B'] in M; attr M is (M2) means : Def20: for A, B, A', B' being Subset of X st [A, B] in M & [A', B'] in M & [A, B] >= [A', B'] holds A = A' & B = B'; attr M is (M3) means : Def21: for A, B, A', B' being Subset of X st [A, B] in M & [A', B'] in M & A' c= B holds B' c= B; end; theorem Th30: :: 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 let A be Subset of X; A1: field DOX = [:bool X, bool X:] by Th19; defpred P[set] means ex y being Dependency of X st $1 = y & y >= [A,A]; consider MA being set such that A2: for x being set holds x in MA iff x in F & P[x] from XBOOLE_0:sch 1; [A, A] in F by Def16; then A3: MA <> {} by A2; MA c= F proof let x be set; assume x in MA; hence x in F by A2; end; then MA is finite Subset of field DOX by A1,XBOOLE_1:1; 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,WAYBEL_4:def 24; then x in F by A2; then consider A', B' being set such that A6: A' in bool X & B' in bool X & x = [A',B'] by ZFMISC_1:def 2; reconsider A', B' as Subset of X by A6; take A', B'; consider y being Dependency of X such that A7: x = y & y >= [A,A] by A2,A5; thus [A', B'] >= [A, A] by A6,A7; x is_maximal_wrt F, DOX proof thus x in F by A2,A5; given z being set such that A8: z in F & z <> x & [x, z] in DOX; consider e, f being Dependency of X such that A9: [x,z] = [e, f] & e <= f by A8; A10: x = e & z = f by A9,ZFMISC_1:33; then f >= [A,A] by A7,A9,Th14; then z in MA by A2,A8,A10; hence contradiction by A4,A8,WAYBEL_4:def 24; end; hence [A', B'] in Maximal_wrt F by A6,Def1; end; thus Maximal_wrt F is (M2) proof let A, B, A', B' be Subset of X such that A11: [A, B] in MEF & [A', B'] in MEF & [A, B] >= [A', B']; A12: [A', B'] is_maximal_wrt F, DOX by A11,Def1; assume not (A = A' & B = B'); then A13: [A, B] <> [A',B'] by ZFMISC_1:33; [[A',B'], [A, B]] in DOX by A11; hence contradiction by A11,A12,A13,WAYBEL_4:def 24; end; thus Maximal_wrt F is (M3) proof let A, B, A', B' be Subset of X; assume A14: [A, B] in MEF & [A', B'] in MEF & A' c= B; then [A',B'] >= [B,B'] by Th15; then A15: [ B, B'] in F by A14,Def13; A16: A\/A = A; A17: A ^|^ B, F by A14,Def18; [ A, B'] in F by A14,A15,Th20; then A18: [A, B\/B'] in F by A14,A16,Def14; B c= B\/B' by XBOOLE_1:7; then [A,B\/B'] >= [A,B] by Th15; then B\/B' = B by A17,A18,Th29; hence B' c= B by XBOOLE_1:11; end; end; theorem Th31: :: 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 A', B' being Subset of X st [A', B'] >= [A, B] & [A', B'] 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 A', B' being Subset of X st [A', B'] >= [A, B] & [A', B'] in M}; set DOX = Dependencies-Order X; A3: now let x be set; assume x in F; then consider a, b being Subset of X such that A4: x = [a,b] and A5: ex a', b' being Subset of X st [a', b'] >= [a, b] & [a', b'] in M by A2; consider a', b' being Subset of X such that A6: [a', b'] >= [a, b] & [a', b'] in M by A5; take a, b, a', b'; thus x = [a,b] & [a', b'] >= [a, b] & [a', b'] in M by A4,A6; end; A7: now let A, B be Subset of X; assume [A,B] in F; then consider a, b, a', b' being Subset of X such that A8: [A,B] = [a,b] and A9: [a', b'] >= [a, b] & [a', b'] in M by A3; take a', b'; thus [a', b'] >= [A, B] & [a', b'] in M by A8,A9; end; now let x be set; hereby assume A10: x in M; then consider a, b being Subset of X such that A11: x = [a,b] by Th10; x is_maximal_wrt F, DOX proof thus x in F by A2,A10,A11; given y being set such that A12: y in F & y <> x & [x, y] in DOX; consider e, f being Dependency of X such that A13: [x,y] = [e, f] & e <= f by A12; A14: x = e & y = f by A13,ZFMISC_1:33; consider c, d, c', d' being Subset of X such that A15: y = [c,d] and A16: [c',d'] >= [c,d] & [c',d'] in M by A3,A12; [c',d'] >= [a,b] by A11,A13,A14,A15,A16,Th14; then c' = a & d' = b by A1,A10,A11,A16,Def20; hence contradiction by A11,A12,A13,A14,A15,A16,Th13; end; hence x in Maximal_wrt F by Def1; end; assume A17: x in Maximal_wrt F; then A18: x in F & x is_maximal_wrt F, DOX by Def1; consider a,b,a',b' being Subset of X such that A19: x = [a,b] and A20: [a', b'] >= [a, b] & [a', b'] in M by A3,A17; A21: [a',b'] in F by A2,A20; assume A22: not x in M; [[a,b], [a',b']] in DOX by A20; hence contradiction by A18,A19,A20,A21,A22,WAYBEL_4:def 24; end; hence M = Maximal_wrt F by TARSKI:2; thus F is full_family proof thus F is (F1) proof let A be Subset of X; consider A', B' being Subset of X such that A23: [A', B'] >= [A, A] & [A', B'] in M by A1,Def19; thus [A, A] in F by A2,A23; end; now let A, B, C be Subset of X; assume A24: [A, B] in F & [B, C] in F; then consider A', B' being Subset of X such that A25: [A', B'] >= [A, B] & [A', B'] in M by A7; consider B1', C' being Subset of X such that A26: [B1', C'] >= [B, C] & [B1', C'] in M by A7,A24; B1' c= B & B c= B' by A25,A26,Th15; then B1' c= B' by XBOOLE_1:1; then A' c= A' & C' c= B' by A1,A25,A26,Def21; then A27: [A', B'] >= [A', C'] by Th15; A' c= A & C c= C' by A25,A26,Th15; then [A',C'] >= [A, C] by Th15; then [A',B'] >= [A, C] by A27,Th14; hence [A, C] in F by A2,A25; end; hence F is (F2) by Th20; thus F is (F3) proof let A, B, A', B' be Subset of X such that A28: [A, B] in F & [A, B] >= [A', B']; consider a',b' being Subset of X such that A29: [a', b'] >= [A, B] & [a', b'] in M by A7,A28; [a',b'] >= [A',B'] by A28,A29,Th14; hence [A', B'] in F by A2,A29; end; thus F is (F4) proof let A, B, A', B' be Subset of X such that A30: [A, B] in F & [A', B'] in F; consider A'', B'' being Subset of X such that A31: [A'', B''] >= [A\/A', A\/A'] & [A'', B''] in M by A1,Def19; A32: A'' c= A\/A' & A\/A' c= B'' by A31,Th15; consider a1, b1 being Subset of X such that A33: [a1, b1] >= [A, B] & [a1, b1] in M by A7,A30; A34: a1 c= A & B c= b1 by A33,Th15; then a1 c= A\/A' by XBOOLE_1:10; then a1 c= B'' by A32,XBOOLE_1:1; then b1 c= B'' by A1,A31,A33,Def21; then A35: B c= B'' by A34,XBOOLE_1:1; consider a1',b1' being Subset of X such that A36: [a1', b1'] >= [A', B'] & [a1', b1'] in M by A7,A30; A37: a1' c= A' & B' c= b1' by A36,Th15; then a1' c= A\/A' by XBOOLE_1:10; then a1' c= B'' by A32,XBOOLE_1:1; then b1' c= B'' by A1,A31,A36,Def21; then B' c= B'' by A37,XBOOLE_1:1; then B\/B' c= B''\/B'' by A35,XBOOLE_1:13; then [A'',B''] >= [A\/A',B\/B'] by A32,Th15; hence [A\/A',B\/B'] in F by A2,A31; end; end; let G being Full-family of X such that A38: M = Maximal_wrt G; now let x be set; hereby assume A39: x in G; then consider a, b being Subset of X such that A40: x = [a,b] by Th10; A41: field DOX = [:bool X, bool X:] by Th19; defpred P[set] means ex y being Dependency of X st $1 = y & y >= [a,b]; consider MA being set such that A42: for x being set holds x in MA iff x in G & P[x] from XBOOLE_0:sch 1; A43: MA <> {} by A39,A40,A42; MA c= G proof let x be set; assume x in MA; hence x in G by A42; end; then MA is finite Subset of field DOX by A41,XBOOLE_1:1; then consider m being Element of MA such that A44: m is_maximal_wrt MA, DOX by A43,Th2; A45: m in MA by A44,WAYBEL_4:def 24; m is_maximal_wrt G, DOX proof thus m in G by A42,A45; given y being set such that A46: y in G & y <> m & [m, y] in DOX; consider mm being Dependency of X such that A47: m = mm & mm >= [a,b] by A42,A45; consider e, f being Dependency of X such that A48: [m,y]=[e,f] & e <= f by A46; A49: m = e & y = f by A48,ZFMISC_1:33; then f >= [a,b] by A47,A48,Th14; then y in MA by A42,A46,A49; hence contradiction by A44,A46,WAYBEL_4:def 24; end; then A50: m in (DOX Maximal_in G) by Def1; consider y being Dependency of X such that A51: m = y & y >= [a,b] by A42,A45; m in G by A42,A45; then consider a', b' being Subset of X such that A52: m = [a',b'] by Th10; thus x in F by A2,A38,A40,A50,A51,A52; end; assume x in F; then consider a, b, a1, b1 being Subset of X such that A53: x = [a,b] and A54: [a1, b1] >= [a, b] & [a1, b1] in M by A3; thus x in G by A38,A53,A54,Def13; end; hence G = F 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 Th30; then ex A',B' being Subset of X st [A', B']>=[[#]X, [#]X]&[A', B'] in M by Def19; hence thesis; end; end; theorem Th32: :: 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; assume A1: F = { [A, B] where A, B is Subset of X : K c= A or B c= A }; A2: [#] X = X; set M = {[K, X]}\/{[A, A] where A is Subset of X : not K c= A}; A3: [K,X] in {[K,X]} by TARSKI:def 1; A4: {[K,X]} c= M by XBOOLE_1:7; A5: now let A be Subset of X; assume not K c= A; then A6: [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 A6; end; A7: now let A, B be Subset of X; assume A8: [A,B] in M; per cases by A8,XBOOLE_0:def 2; 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] & not K c= a; A = a & B = a by A9,ZFMISC_1:33; hence [A,B] = [K,X] or not K c= A & A = B by A9; end; end; M c= [:bool X, bool X:] proof let x be set; assume A10: x in M; per cases by A10,XBOOLE_0:def 2; suppose x in {[K, X]}; then x = [K,X] by TARSKI:def 1; hence thesis by A2,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; then reconsider M as Dependency-set of X by RELSET_1:def 1; A11: M is (M1) proof let A be Subset of X; per cases; suppose A12: K c= A; take A' = K, B' = [#]X; thus [A', B'] >= [A, A] by A12,Th15; thus [A', B'] in M by A3,A4; end; suppose A13: not K c= A; take A' = A, B' = A; thus [A', B'] >= [A, A]; thus [A', B'] in M by A5,A13; end; end; A14: M is (M2) proof let A, B, A', B' be Subset of X such that A15: [A, B] in M and A16: [A', B'] in M and A17: [A, B] >= [A', B']; A18: A c= A' & B' c= B by A17,Th15; per cases by A7,A15; suppose A19: [A,B] = [K,X]; thus A = A' & B = B' proof per cases by A7,A16; suppose [A',B'] = [K,X]; hence thesis by A19,ZFMISC_1:33; end; suppose not K c= A' & A' = B'; hence thesis by A18,A19,ZFMISC_1:33; end; end; end; suppose A20: not K c= A & A = B; thus A = A' & B = B' proof per cases by A7,A16; suppose [A',B'] = [K,X]; then A' = K & B' = X by ZFMISC_1:33; then B = X by A18,XBOOLE_0:def 10; hence thesis by A20; end; suppose not K c= A' & A' = B'; hence thesis by A18,A20,XBOOLE_0:def 10; end; end; end; end; A21: M is (M3) proof let A, B, A', B' be Subset of X such that A22: [A, B] in M and A23: [A', B'] in M and A24: A' c= B; per cases by A7,A22; suppose [A,B] = [K,X]; then A = K & B = X by ZFMISC_1:33; hence B' c= B; end; suppose A25: not K c= A & A = B; thus B' c= B proof per cases by A7,A23; suppose [A',B'] = [K,X]; hence thesis by A24,A25,ZFMISC_1:33; end; suppose not K c= A' & A' = B'; hence thesis by A24; end; end; end; end; set FF = {[A, B] where A, B is Subset of X : ex A', B' being Subset of X st [A', B'] >= [A, B] & [A', B'] in M}; FF c= [:bool X, bool X:] proof let x be set; assume x in FF; then consider A, B being Subset of X such that A26: x = [A,B] and ex A', B' being Subset of X st [A', B'] >= [A, B] & [A', B'] in M; thus thesis by A26; end; then reconsider FF as Dependency-set of X by RELSET_1:def 1; A27: M = Maximal_wrt FF by A11,A14,A21,Th31; now let x be set; hereby assume x in F; then consider A, B being Subset of X such that A28: x = [A,B] and A29: K c= A or B c= A by A1; A30: {[K,X]} c= M by XBOOLE_1:7; A31: [K,X] in {[K,X]} by TARSKI:def 1; A32: {[a, a] where a is Subset of X : not K c= a} c= M by XBOOLE_1:7; per cases; suppose K c= A; then [K,[#] X] >= [A,B] by Th15; hence x in FF by A28,A30,A31; end; suppose A33: not K c= A; then A34: [A,A] in {[a, a] where a is Subset of X : not K c= a}; [A,A] >= [A,B] by A29,A33,Th15; hence x in FF by A28,A32,A34; end; end; assume x in FF; then consider A, B being Subset of X such that A35: x = [A,B] and A36: ex A', B' being Subset of X st [A', B'] >= [A, B] & [A', B'] in M; consider A', B' being Subset of X such that A37: [A', B'] >= [A, B] & [A', B'] in M by A36; per cases by A37,XBOOLE_0:def 2; suppose [A',B'] in {[K, X]}; then [A',B'] = [K,X] by TARSKI:def 1; then A' = K & B' = X by ZFMISC_1:33; then K c= A & B c= X by A37,Th15; hence x in F by A1,A35; 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 A38: [A',B'] = [a,a] and not K c= a; A39: A' = a & B' = a by A38,ZFMISC_1:33; A' c= A & B c= B' by A37,Th15; then B c= A by A39,XBOOLE_1:1; hence x in F by A1,A35; end; end; hence {[K, X]}\/{[A, A] where A is Subset of X : not K c= A} = Maximal_wrt F by A27,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 set; assume x in SS; then consider B being Subset of X such that A1: x = B & ex A being Subset of X st A ^|^ B, F; thus thesis by A1; 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 set ss = {B where B is Subset of X: ex A being Subset of X st A ^|^ B, F }; defpred P[set,set] means ex a,b being set st $1 = [a,b] & $2 = [a,b]`2; A2: for x being set st x in F ex y being set st P[x,y] proof let x be set; assume x in F; then consider a, b being Subset of X such that A3: x = [a,b] by Th10; reconsider a, b as set; take b; take a, b; thus x = [a,b] & b = [a,b]`2 by A3,MCART_1:def 2; end; consider f being Function such that A4: dom f = F and A5: for x being set st x in F holds P[x,f.x] from CLASSES1:sch 1(A2); A6: rng f is finite by A4,FINSET_1:26; ss c= rng f proof let x be set; assume x in ss; then consider B being Subset of X such that A7: x = B and A8: ex A being Subset of X st A ^|^ B, F; consider A being Subset of X such that A9: A ^|^ B, F by A8; A10: [A, B] in Maximal_wrt F by A9,Def18; then consider a,b being set such that A11: [A,B] = [a,b] & f.[A,B] = [a,b]`2 by A5; f.[A,B] = B by A11,MCART_1:def 2; hence x in rng f by A4,A7,A10,FUNCT_1:12; end; hence saturated-subsets F is finite by A6; end; end; theorem Th33: 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 & A ^|^ B, F; thus x in saturated-subsets F by A4; end; theorem Th34: :: 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 Th30; then consider A', B' being Subset of X such that A2: [A',B'] >= [[#]X,[#]X] and A3: [A',B'] in Maximal_wrt F by Def19; A4: A' ^|^ B', F by A3,Def18; [#]X c= B' by A2,Th15; then [#]X = B' by XBOOLE_0:def 10; then X in ss by A4; hence ss is (B1) by Def4; thus ss is (B2) proof let a, b be set such that A5: a in ss and A6: b in ss; reconsider a' = a, b' = b as Subset of X by A5,A6; consider B1, A1 being Subset of X such that A7: a = B1 and A8: A1 ^|^ B1, F by A5,Th33; A9: [A1,B1] in Maximal_wrt F by A8,Def18; consider B2, A2 being Subset of X such that A10: b = B2 and A11: A2 ^|^ B2, F by A6,Th33; A12: [A2,B2] in Maximal_wrt F by A11,Def18; consider A', B' being Subset of X such that A13: [A',B'] >= [a'/\b',a'/\b'] and A14: [A',B'] in Maximal_wrt F by A1,Def19; A15: A' ^|^ B', F by A14,Def18; A16: A' c= a/\b & a/\b c= B' by A13,Th15; a/\b c= a by XBOOLE_1:17; then A17: A' c= B1 by A7,A16,XBOOLE_1:1; A18: Maximal_wrt F is (M3) by Th30; then A19: B' c= B1 by A9,A14,A17,Def21; a/\b c= b by XBOOLE_1:17; then A' c= B2 by A10,A16,XBOOLE_1:1; then B' c= B2 by A12,A14,A18,Def21; then B' c= a/\b by A7,A10,A19,XBOOLE_1:19; then B' = a/\b by A16, XBOOLE_0:def 10; hence a /\ b in ss by A15; 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 set; 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 x in [:bool X, bool X:]; end; hence F is Dependency-set of X by RELSET_1:def 1; end; end; theorem Th35: :: 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 set; thus x in F implies x in Dependencies X; assume x in Dependencies X; then consider x1, x2 being set such that A2: x1 in bool X & x2 in bool X & x = [x1, x2] by ZFMISC_1:def 2; for g being set st g in B & x1 c= g holds x2 c= g by A1; hence x in F by A2; end; then F = Dependencies X by TARSKI:2; then F is (F1) (F2) (F3) (F4) by Th21; hence thesis; end; suppose B is non empty; then reconsider B as non empty Subset-Family of X; A3: now let x,y be Subset of X, c be Element of B; assume that A4: [x, y] in F and A5: x c= c; consider a, b being Subset of X such that A6: [x,y] = [a,b] and A7: for c being set st c in B & a c= c holds b c= c by A4; x = a & y = b by A6,ZFMISC_1:33; hence y c= c by A5,A7; end; 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 [A, A] in F; end; now let a, b, c be Subset of X such that A8: [a, b] in F and A9: [b, c] in F; now let x be set; assume A10: x in B & a c= x; then b c= x by A3,A8; hence c c= x by A3,A9,A10; end; hence [a, c] in F; end; hence F is (F2) by Th20; thus F is (F3) proof let a, b, a', b' be Subset of X such that A11: [a, b] in F and A12: [a, b] >= [a', b']; A13: a c= a' & b' c= b by A12,Th15; now let c be set; assume A14: c in B & a' c= c; then a c= c by A13,XBOOLE_1:1; then b c= c by A3,A11,A14; hence b' c= c by A13,XBOOLE_1:1; end; hence [a',b'] in F; end; thus F is (F4) proof let a, b, a', b' be Subset of X such that A15: [a, b] in F and A16: [a', b'] in F; now let c be set; assume A17: c in B & a\/a' c= c; then a c= c & a' c= c by XBOOLE_1:11; then b c= c & b' c= c by A3,A15,A16,A17; hence b\/b' c= c by XBOOLE_1:8; end; hence [a\/a', b\/b'] in F; end; end; end; theorem Th36: :: 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; set ss = saturated-subsets F; reconsider F' = F as Full-family of X by Th35; set M = Maximal_wrt F'; A1: M is (M1) by Th30; let x be set; assume A2: x in B; then reconsider x' = x as Element of B; reconsider x'' = x as Subset of X by A2; consider a', b' being Subset of X such that A3: [a',b'] >= [x'',x''] and A4: [a', b'] in M by A1,Def19; A5: a' c= x'' & x'' c= b' by A3,Th15; [a',b'] in F by A4; then consider a, b being Subset of X such that A6: [a',b'] = [a,b] and A7: for c being set st c in B & a c= c holds b c= c; A8: a' = a & b' = b by A6,ZFMISC_1:33; then b c= x' by A2,A5,A7; then A9: b = x by A5,A8,XBOOLE_0:def 10; a ^|^ b, F by A4,A6,Def18; hence x in ss by A9; end; theorem Th37: :: 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; assume A1: B is (B1) (B2); set F = X deps_encl_by B; set ss = saturated-subsets F; reconsider F' = F as Full-family of X by Th35; set M = Maximal_wrt F'; A2: X in B by A1,Def4; reconsider B' = B as non empty set by A1,Def4; now let x be set; B c= ss by Th36; 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 Th33; [a,b] in M by A4,Def18; 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: a = aa & b = bb by A5,ZFMISC_1:33; set S = { b' where b' is Element of B': a c= b' }; A9: S c= bool X proof let x be set; assume x in S; then consider b' being Element of B' such that A10: x = b' & a c= b'; b' in B' & B c= bool X; hence x in bool X by A10; end; A12: X in S by A2; A13: S c= B proof let x be set; assume x in S; then consider b' being Element of B' such that A14: x = b' & a c= b'; thus x in B by A14; end; reconsider S as Subset-Family of X by A9; set mS = Intersect S; reconsider mS as Subset of X; A15: b c= mS proof let x be set; assume A16: x in b; now let Y be set; assume Y in S; then consider b' being Element of B' such that A17: Y = b' & a c= b'; b c= b' by A6,A7,A17; hence x in Y by A16,A17; end; then x in meet S by A12,SETFAM_1:def 1; hence x in mS by A12,SETFAM_1:def 10; end; now assume A18: b <> mS; now let c be set; assume c in B & a c= c; then c in S; then meet S c= c by SETFAM_1:4; hence mS c= c by A12,SETFAM_1:def 10; end; then A19: [a,mS] in F; [a,mS] >= [a,b] by A15,Th15; hence contradiction by A4,A18,A19,Th29; end; hence x in B by A1,A2,A3,A13,Th1; end; hence B = saturated-subsets F by TARSKI:2; let G be Full-family of X; assume A20: B = saturated-subsets G; set MG = Maximal_wrt G; A21: MG is (M1)(M3) by Th30; now let x be set; hereby assume x in G; then reconsider x1 = x as Element of G; reconsider x' = x1 as Dependency of X; consider a, b being Subset of X such that A22: x' = [a,b] by Th9; now let b' be set such that A23: b' in B' and A24: a c= b'; consider b1', a' being Subset of X such that A25: b' = b1' and A26: a' ^|^ b1', G by A20,A23,Th33; A27: [a',b'] in MG by A25,A26,Def18; consider a'', b'' being Subset of X such that A28: [a'',b''] in MG and A29: [a'', b''] >= x' by Th28; a'' c= a by A22,A29,Th15; then a'' c= b' by A24,XBOOLE_1:1; then A30: b'' c= b1' by A21,A25,A27,A28,Def21; b c= b'' by A22,A29,Th15; hence b c= b' by A25,A30,XBOOLE_1:1; end; hence x in F by A22; end; assume x in F; then consider a, b being Subset of X such that A31: x = [a,b] and A32: for c being set st c in B & a c= c holds b c= c; consider a', b' being Subset of X such that A33: [a', b'] >= [a,a] and A34: [a', b'] in MG by A21,Def19; A35: a' c= a & a c= b' by A33,Th15; a' ^|^ b', G by A34,Def18; then b' in B by A20; then b c= b' by A32,A35; then [a',b'] >= [a,b] by A35,Th15; hence x in G by A31,A34,Def13; end; hence G = F 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 set; 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 z in bool X; end; hence B is Subset-Family of X; end; end; theorem Th38: :: 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: X = [#]X; for x, y being Subset of X st [x, y] in F & x c= X holds y c= X; then X in B by A1; hence B is (B1) by Def4; let a, b be set such that A2: a in B and A3: b in B; consider a' being Subset of X such that A4: a' = a and A5: for x, y being Subset of X st [x, y] in F & x c= a' holds y c= a' by A2; consider b' being Subset of X such that A6: b' = b and A7: for x, y being Subset of X st [x, y] in F & x c= b' holds y c= b' by A3; reconsider ab = a' /\ b' as Subset of X; now let x, y be Subset of X such that A8: [x, y] in F and A9: x c= ab; x c= a' & x c= b' by A9,XBOOLE_1:18; then y c= a' & y c= b' by A5,A7,A8; hence y c= ab by XBOOLE_1:19; end; hence a /\ b in B by A4,A6; end; theorem Th39: :: 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 set; assume A1: x in F; then consider a, b being Subset of X such that A2: x = [a,b] by Th10; 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 c' being Subset of X st c' = c & for x, y being Subset of X st [x, y] in F & x c= c' holds y c= c' by A3; hence contradiction by A1,A2,A4,A5; end; hence x in H by A2; end; let G be Dependency-set of X such that A6: F c= G and A7: G is full_family; let z be set; assume z in H; then consider a, b being Subset of X such that A8: z = [a,b] and A9: for c being set st c in B & a c= c holds b c= c; B is (B1) (B2) by Th38; then A10: B = saturated-subsets H by Th37; set B' = saturated-subsets G; A11: B' is (B1) (B2) by A7,Th34; set GG = {[e, f] where e, f is Subset of X : for c being set st c in B' & e c= c holds f c= c}; GG = X deps_encl_by B'; then A12: GG = G by A7,A11,Th37; B' c= saturated-subsets H proof let d be set such that A13: d in B' 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 A10,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 B' & e c= c holds f c= c by A12; x = e & y = f by A18,ZFMISC_1:33; hence contradiction by A13,A16,A17,A19; end; then for c be set st c in B' & a c= c holds b c= c by A9,A10; hence z in G by A8,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 :Def25: 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 set; 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 x in bool X; end; then reconsider B as Subset-Family of X; set H = X deps_encl_by B; reconsider H as Full-family of X by Th35; take H; thus thesis by A1,Th39; end; correctness proof let it1, it2 be Full-family of X; assume F c= it1 & (for G being Dependency-set of X st F c=G&G is full_family holds it1 c=G) & F c= it2 & for G being Dependency-set of X st F c=G&G is full_family holds it2 c=G; then it1 c= it2 & it2 c= it1; hence it1 = it2 by XBOOLE_0:def 10; end; end; theorem Th40: :: 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 Th35; A1: F c= H by Th39; for G being Dependency-set of X st F c= G & G is full_family holds H c= G by Th39; hence thesis by A1,Def25; end; theorem Th41: :: 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}; set BB1 = {B where B is Subset of X : not K c= B}; thus BB is (B1) proof X in {X} by TARSKI:def 1; hence X in BB by A1,XBOOLE_0:def 2; end; thus BB is (B2) proof let a, b be set; assume A2: a in BB & b in BB; then reconsider a' =a, b' = b as Subset of X; per cases by A1,A2,XBOOLE_0:def 2; suppose a in {X} & b in {X}; then a = X & b = X by TARSKI:def 1; then a/\ b in {X} by TARSKI:def 1; hence a /\ b in BB by A1,XBOOLE_0:def 2; end; suppose A3: a in {X} & b in BB1; then a = X by TARSKI:def 1; then a'/\b' = b by XBOOLE_1:28; hence a /\ b in BB by A1,A3,XBOOLE_0:def 2; end; suppose A4: a in BB1 & b in {X}; then b = X by TARSKI:def 1; then a'/\b' = a by XBOOLE_1:28; hence a /\ b in BB by A1,A4,XBOOLE_0:def 2; 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 a'/\b' in BB1; hence a /\ b in BB by A1,XBOOLE_0:def 2; end; end; end; theorem :: Ex3a: :: use WWA3* to prove what is the saturated subset for the example 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; assume A1: F = { [A, B] where A, B is Subset of X : K c= A or B c= A }; set BB = {X}\/{B where B is Subset of X : not K c= B}; BB c= bool X proof let x be set; assume A2: x in BB; per cases by A2,XBOOLE_0:def 2; suppose A3: x in {X}; {X} c= bool X by ZFMISC_1:80; hence x in bool X by A3; 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 x in bool X; end; end; then reconsider BB' = BB as non empty Subset-Family of X; A4: BB' is (B1) by Th41; A5: BB' is (B2) by Th41; set G = {[a, b] where a,b is Subset of X : for c being set st c in BB' & a c= c holds b c= c}; A6: G = X deps_encl_by BB'; now let x be set; hereby assume x in F; then consider a, b being Subset of X such that A7: x = [a,b] and A8: K c= a or b c= a by A1; now let c be set such that A9: c in BB' and A10: a c= c; per cases by A8; suppose A11: K c= a; thus b c= c proof per cases by A9,XBOOLE_0:def 2; suppose c in {X}; then c = X by TARSKI:def 1; hence b c= c; 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 b c= c by A10,A11,XBOOLE_1:1; end; end; end; suppose b c= a; hence b c= c by A10,XBOOLE_1:1; end; end; hence x in G by A7; end; assume x in G; then consider a, b being Subset of X such that A12: x = [a,b] and A13: for c being set st c in BB' & 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 BB' by XBOOLE_0:def 2; hence b c= a by A13; end; hence x in F by A1,A12; end; then F = G by TARSKI:2; hence BB = saturated-subsets F by A4,A5,A6,Th37; end; theorem :: Ex3b: 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; assume A1: F = { [A, B] where A, B is Subset of X : K c= A or B c= A }; 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}; A2: M = Maximal_wrt F by A1,Th32; A3: [#]X = X; set ss = saturated-subsets F; now let x be set; hereby assume A4: x in BB; per cases by A4,XBOOLE_0:def 2; suppose x in {X}; then A5: x = X by TARSKI:def 1; [K,X] in {[K,X]} by TARSKI:def 1; then [K,X] in M by XBOOLE_0:def 2; then K ^|^ X, F by A2,Def18; hence x in ss by A3,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 2; then B ^|^ B, F by A2,Def18; 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 Th33; A10: [a,b] in M by A2,A9,Def18; per cases by A10,XBOOLE_0:def 2; suppose [a,b] in {[K,X]}; then [a,b] = [K,X] by TARSKI:def 1; then b = X by ZFMISC_1:33; then b in {X} by TARSKI:def 1; hence x in BB by A8,XBOOLE_0:def 2; 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: a = c & b = c by A11,ZFMISC_1:33; c in {B where B is Subset of X : not K c= B} by A12; hence x in BB by A8,A13,XBOOLE_0:def 2; end; end; hence BB = ss by TARSKI:2; end; definition let X, G be set, B be Subset-Family of X; pred G is_generator-set_of B means :Def26: 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 Th35; then A1: ssF is (B1) (B2) by Th34; thus G is_generator-set_of ssF proof thus A2: G c= ssF by Th36; set H = { Intersect S where S is Subset-Family of X: S c= G }; now let x be set; hereby assume x in ssF; then consider b', a' being Subset of X such that A3: x = b' and A4: a' ^|^ b', F by Th33; [a', b'] in Maximal_wrt F by A4,Def18; then [a',b'] in F; then consider a, b being Subset of X such that A5: [a, b] = [a', b'] and A6: for c being set st c in G & a c= c holds b c= c; A7: a = a' & b = b' by A5,ZFMISC_1:33; set C = {c where c is Subset of X: c in G & a c= c}; C c= bool X proof let x be set; assume x in C; then ex c being Subset of X st x = c & c in G & a c= c; hence x in bool X; end; then reconsider C as Subset-Family of X; set ic = Intersect C; now let z1 be set; assume z1 in C; then consider c being Subset of X such that A8: z1 = c & c in G & a c= c; thus b c= z1 by A6,A8; end; then A9: b c= Intersect C by MSSUBFAM:4; A10: C c= G proof let c be set; assume c in C; then ex cc being Subset of X st cc = c & cc in G & a c= cc; hence c in G; end; thus x in H proof per cases; suppose b = ic; hence thesis by A3,A7,A10; end; suppose A11: b <> ic; reconsider ic as Subset of X; now let c be set; assume c in G & a c= c; then c in C; hence ic c= c by MSSUBFAM:2; end; then A12: [a,ic] in F; [a,b] <= [a,ic] by A9,Th15; hence thesis by A4,A7,A11,A12,Th29; end; end; end; assume x in H; then consider S being Subset-Family of X such that A13: Intersect S = x and A14: S c= G; X in ssF by A1, Def4; hence x in ssF by A1,A2,A13,A14,Th1,XBOOLE_1:1; end; hence ssF = H by TARSKI:2; end; end; theorem Th45: :: 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 Th34; thus G is_generator-set_of G proof thus G c= G; set H = { Intersect S where S is Subset-Family of X: S c= G }; now let x be set; hereby set sx = {x}; assume A2: x in G; then A3: sx c= G by ZFMISC_1:37; reconsider sx as Subset-Family of X by A2,ZFMISC_1:37; A4: Intersect sx = meet sx by SETFAM_1:def 10; Intersect sx in H by A3; hence x in H by A4,SETFAM_1:11; end; assume x in H; then consider S being Subset-Family of X such that A5: Intersect S = x and A6: S c= G; X in G by A1,Def4; hence x in G by A1,A5,A6,Th1; end; hence G = H by TARSKI:2; end; thus F = X deps_encl_by G by A1,Th37; 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); then A2: X in B by Def4; 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 set; hereby assume x in B; then reconsider xx = x as Element of B; consider yz being non empty Subset of B such that A3: xx = meet yz and A4: 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; A5: Intersect yz = meet yz by SETFAM_1:def 10; yz c= G proof let x be set; assume x in yz; then x is_/\-irreducible_in B by A4; hence x in G by Def3; end; hence x in H by A3,A5; end; assume x in H; then consider S being Subset-Family of X such that A6: x = Intersect S and A7: S c= G; thus x in B by A1,A2,A6,A7,Th1,XBOOLE_1:1; end; hence B = H 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,Def26; A4: G c= B by A2,Def26; let x be set; assume A5: x in /\-IRR B; then x in B; then consider S being Subset-Family of X such that A6: x = Intersect S and A7: S c= G by A3; assume A9: not x in G\/{X}; then not x in G & not x in {X} by XBOOLE_0:def 2; then A10: not x in G & x <> X by TARSKI:def 1; A11: not x in S by A7,A9,XBOOLE_0:def 2; reconsider xx = x as Element of B by A5; xx is_/\-irreducible_in B by A5,Def3; hence contradiction by A1,A4,A6,A7,A10,A11,Th4,XBOOLE_1:1; end; begin :: 7. Justification of the axioms theorem :: WWA5: 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; consider G being Subset-Family of X such that G is_generator-set_of saturated-subsets F and A2: F = X deps_encl_by G by Th45; consider H being FinSequence such that A3: rng H = G and H is one-to-one by FINSEQ_4:73; reconsider H as FinSequence of G by A3,FINSEQ_1:def 4; reconsider D = X --> INT as non-empty ManySortedSet of X; A4: dom D = X by PBOOLE:def 3; A5: now set f = X --> 0; thus dom f = dom D by A4,FUNCOP_1:19; let x be set; assume A6: x in dom D; then f.x = 0 by A4,FUNCOP_1:13; then f.x in NAT; then f.x in INT by NUMBERS:17; hence f.x in D.x by A4,A6,FUNCOP_1:13; end; then A7: X --> 0 is Element of product D by CARD_3:def 5; per cases; suppose A8: G is empty; set R = {X-->0}; R c= product D proof let x be set; assume x in R; then x = X --> 0 by TARSKI:def 1; hence x in product D by A5,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 by FUNCOP_1:13; set Ds = Dependency-str BD; now let x be set; hereby assume x in F; then consider A, B being Subset of X such that A9: x = [A, B] and for g being set st g in G & A c= g holds B c= g by A2; 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 & g = X --> 0 by TARSKI:def 1; hence thesis; end; hence x in Ds by A9; end; assume x in Ds; then consider A, B being Subset of the Attributes of BD such that A10: x = [A,B] and A >|> B, BD; for g being set st g in G & A c= g holds B c= g by A8; hence x in F by A2,A10; end; hence F = Dependency-str BD by TARSKI:2; end; suppose A11: G is non empty; then reconsider n =len H as non empty Element of NAT by A3,CARD_2:59,RELAT_1:60; A12: dom H = Seg n by FINSEQ_1:def 3; 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); A13: 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); A14: 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 A15: x in H.i; reconsider b = FALSE as Element of BOOLEAN; take b; thus P[i,b] by A15; end; suppose A16: not x in H.i; reconsider b = TRUE as Element of BOOLEAN; take b; thus P[i,b] by A16; end; end; consider y being FinSequence of BOOLEAN such that A17: dom y = Seg n and A18: for i being Nat st i in Seg n holds P[i,y.i] from FINSEQ_1:sch 5(A14); A19: y in BOOLEAN* by FINSEQ_1:def 11; len y = n by A17,FINSEQ_1:def 3; then y in { s where s is Element of BOOLEAN*: len s = n } by A19; then reconsider y as Tuple of n, BOOLEAN; take y; thus R[x,y] by A18; end; consider M being Function of X, n-tuples_on BOOLEAN such that A20: for x being Element of X holds R[x,(M.x) qua Element of n-tuples_on BOOLEAN] from FUNCT_2:sch 3(A13); 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)) }; now set f = X --> 0; take i = 0; let x be Element of X; A21: (n-BinarySequence i) '&' (M.x) = n-BinarySequence i by Th5 .= 0*n by BINARI_3:26; thus f.x = 0 by FUNCOP_1:13 .= Absval ((n-BinarySequence i) '&' (M.x)) by A21,BINARI_3:7; end; then A22: X --> 0 in R by A7; R c= product D proof let x be set; 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)); hence thesis; end; then reconsider R as non empty Subset of product D by A22; 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 by FUNCOP_1:13; set Ds = Dependency-str BD; now let x be set; hereby assume x in F; then consider A, B being Subset of X such that A23: x = [A, B] and A24: for g being set st g in G & A c= g holds B c= g by A2; reconsider A' = A, B' = B as Subset of the Attributes of BD; A' >|> B', BD proof let f, g be Element of the Relationship of BD; assume A25: f|A' = g|A'; f in R; then consider Rf being Element of product D such that A26: f = Rf and A27: ex i being Element of NAT st for x being Element of X holds Rf.x = Absval ((n-BinarySequence i) '&' (M.x)); 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)); consider fi being Element of NAT such that A30: for x being Element of X holds Rf.x = Absval ((n-BinarySequence fi) '&' (M.x)) by A27; consider gi being Element of NAT such that A31: for x being Element of X holds Rg.x = Absval ((n-BinarySequence gi) '&' (M.x)) by A29; A32: dom g = dom D by A28,CARD_3:18 .= dom f by A26,CARD_3:18; now thus A33: dom (g|B) = dom f /\ B by A32,RELAT_1:90; let a be set such that A34: a in dom (g|B); A35: a in B by A33,A34,XBOOLE_0:def 3; reconsider x = a as Element of X by A33,A34; set nbf = n-BinarySequence fi; set nbg = n-BinarySequence gi; set nf = nbf '&' (M.x); set ng = nbg '&' (M.x); A36: dom (M.x) = Seg n by Lm1; A37: dom nf = Seg n by Lm1; reconsider Mx = M.x as Tuple of n, BOOLEAN; now thus dom nf = dom ng by A37,Lm1; let i be set; assume A38: i in dom nf; per cases; suppose A c= H.i; then A39: B c= H.i by A3,A12,A24,A37,A38,FUNCT_1:12; A40: Mx/.i = Mx.i by A36,A37,A38,PARTFUN1:def 8 .= 0 by A20,A35,A37,A38,A39; thus nf.i = (nbf/.i) '&' (Mx/.i) by A37,A38,Def5 .= (nbg/.i) '&' (Mx/.i) by A40 .= ng.i by A37,A38,Def5; end; suppose A41: not A c= H.i; thus nf.i = ng.i proof consider xx being set such that A42: xx in A and A43: not xx in H.i by A41,TARSKI:def 3; reconsider xx as Element of X by A42; reconsider Mxx = M.xx as Tuple of n, BOOLEAN; dom (M.xx) = Seg n by Lm1; then A44: Mxx/.i = Mxx.i by A37,A38,PARTFUN1:def 8 .= 1 by A20,A37,A38,A43; A45: f.xx = (g|A).xx by A25,A42,FUNCT_1:72 .= g.xx by A42,FUNCT_1:72; A46: f.xx = Absval (nbf '&' (M.xx)) by A26,A30; A47: g.xx = Absval ((nbg) '&' (M.xx)) by A28,A31; A48: nbf/.i = (nbf/.i) '&' (Mxx/.i) by A44 .= (nbf '&' (M.xx)).i by A37,A38,Def5 .= (nbg '&' (M.xx)).i by A45,A46,A47,BINARI_3:2 .= (nbg/.i) '&' (Mxx/.i) by A37,A38,Def5 .= nbg/.i by A44; thus nf.i = (nbf/.i) '&' (Mx/.i) by A37,A38,Def5 .= ng.i by A37,A38,A48,Def5; end; end; end; then nf = ng by FUNCT_1:9; then g.a = Absval ((n-BinarySequence fi) '&' (M.x)) by A28,A31 .= f.a by A26,A30; hence (g|B).a = f.a by A34,FUNCT_1:70; end; hence f|B' = g|B' by FUNCT_1:68; end; hence x in Ds by A23; end; assume x in Ds; then consider A, B being Subset of the Attributes of BD such that A49: x = [A, B] and A50: A >|> B, BD; now let gg be set such that A51: gg in G and A52: A c= gg and A53: not B c= gg; reconsider gg as Element of G by A51; consider bx being set such that A54: bx in B & not bx in gg by A53,TARSKI:def 3; reconsider bx as Element of X by A54; consider i being Nat such that A55: i in dom H and A56: H.i = gg by A3,A11,FINSEQ_2:11; A57: 1 <= i & i <= n by A12,A55,FINSEQ_1:3; i <> 0 by A12,A55,FINSEQ_1:3; then consider k being Nat such that A58: i = k+1 by NAT_1:6; reconsider k as Element of NAT by ORDINAL1:def 13; A59: k < n by A57,A58,NAT_1:13; deffunc F(Element of X) = Absval ((n-BinarySequence 0) '&' (M.$1)); consider f being Function of X, NAT such that A60: for x being Element of X holds f.x = F(x) from FUNCT_2:sch 4; deffunc F(Element of X) = Absval ((n-BinarySequence 2 to_power k) '&' (M.$1)); consider g being Function of X, NAT such that A61: for x being Element of X holds g.x = F(x) from FUNCT_2:sch 4; A62: dom f = dom D by A4,FUNCT_2:def 1; now let x be set; assume x in dom D; then reconsider x' = x as Element of X by PBOOLE:def 3; f.x = Absval ((n-BinarySequence 0) '&' (M.x')) by A60; then f.x in NAT; then f.x' in INT by NUMBERS:17; hence f.x in D.x by FUNCOP_1:13; end; then reconsider f as Element of product D by A62,CARD_3:def 5; A63: f in R by A60; A64: dom g = dom D by A4,FUNCT_2:def 1; now let x be set; assume x in dom D; then reconsider x' = x as Element of X by PBOOLE:def 3; g.x = Absval ((n-BinarySequence 2 to_power k) '&' (M.x')) by A61; then g.x in NAT; then g.x' in INT by NUMBERS:17; hence g.x in D.x by FUNCOP_1:13; end; then reconsider g as Element of product D by A64,CARD_3:def 5; A65: g in R by A61; now thus A66: dom (f|A) = dom g /\ A by A62,A64,RELAT_1:90; let x be set; assume A67: x in dom (f|A); then A68: x in A by A66,XBOOLE_0:def 3; reconsider a = x as Element of X by A66,A67; set bs0 = n-BinarySequence 0, bsi = n-BinarySequence 2 to_power k; A69: (f|A).a = f.a by A68,FUNCT_1:72 .= Absval (bs0 '&' (M.a)) by A60; A70: g.a = Absval (bsi '&' (M.a)) by A61; reconsider Ma = M.a as Tuple of n, BOOLEAN; set L = bs0 '&' (M.a), R = bsi '&' (M.a); now thus dom L = Seg n by Lm1 .= dom R by Lm1; let j be set; assume A71: j in dom L; then A72: j in Seg n by Lm1; reconsider nj = j as Element of NAT by A71; A73: bs0 = 0*n by BINARI_3:26 .= n |-> 0 by EUCLID:def 4; dom bs0 = Seg n by Lm1; then A74: bs0/.nj = bs0.nj by A72,PARTFUN1:def 8 .= 0 by A72,A73,FUNCOP_1:13; A75: L.j = (bs0/.nj) '&' (Ma/.nj) by A72,Def5 .= 0 by A74; per cases; suppose A76: i <> nj; dom bsi = Seg n by Lm1; then A77: bsi/.nj = bsi.nj by A72,PARTFUN1:def 8 .= FALSE by A58,A59,A72,A76,Th8; R.j = (bsi/.nj) '&' (Ma/.nj) by A72,Def5; hence L.j = R.j by A75,A77; end; suppose A78: i = nj; dom Ma = Seg n by Lm1; then A79: Ma/.nj = Ma.i by A72,A78,PARTFUN1:def 8 .= 0 by A20,A52,A56,A68,A72,A78; R.j = (bsi/.nj) '&' (Ma/.nj) by A72,Def5 .= 0 by A79; hence L.j = R.j by A75; end; end; hence (f|A).x = g.x by A69,A70,FUNCT_1:9; end; then f|A = g|A by FUNCT_1:68; then A80: f|B = g|B by A50,A63,A65,Def8; set bs0 = n-BinarySequence 0, bsi = n-BinarySequence 2 to_power k; A81: Absval (bs0 '&' (M.bx)) = f.bx by A60 .= (f|B).bx by A54,FUNCT_1:72 .= g.bx by A54,A80,FUNCT_1:72 .= Absval (bsi '&' (M.bx)) by A61; reconsider Mbx = M.bx as Tuple of n, BOOLEAN; dom Mbx = Seg n by Lm1; then A82: Mbx/.i = Mbx.i by A12,A55,PARTFUN1:def 8 .= 1 by A12,A20,A54,A55,A56; A83: bs0 = 0*n by BINARI_3:26 .= n |-> 0 by EUCLID:def 4; dom bs0 = Seg n by Lm1; then A84: bs0/.i = bs0.i by A12,A55,PARTFUN1:def 8 .= 0 by A12,A55,A83,FUNCOP_1:13; A85: (bs0 '&' (Mbx)).i = (bs0/.i) '&' (Mbx/.i) by A12,A55,Def5 .= bs0/.i by A82; A86: (bsi '&' (Mbx)).i = (bsi/.i) '&' (Mbx/.i) by A12,A55,Def5 .= bsi/.i by A82; dom bsi = Seg n by Lm1; then bsi/.i = bsi.i by A12,A55,PARTFUN1:def 8 .= 1 by A58,A59,Th8; hence contradiction by A81,A84,A85,A86,BINARI_3:2; end; hence x in F by A2,A49; end; hence F = Dependency-str BD by TARSKI:2; end; end; begin :: 8. Structure of the family of candidate keys Lm2: for X, F, BB being set st F = {[a, b] where a,b is Subset of X : for c being set st c in BB & a c= c holds b c= c} 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; x = a & y = b by A2,ZFMISC_1:33; hence for c being set st c in BB & x c= c holds y c= c by A3; end; assume for c being set st c in BB & x c= c holds y c= c; hence [x,y] in F 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 set; assume x in B; then ex A being Subset of X st x = A & [A, X] in Maximal_wrt F; hence x in bool X; 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 such that A1: F = { [A, B] where A, B is Subset of X : K c= A or B c= A }; A2: Maximal_wrt F = {[K, X]}\/{[A, A] where A is Subset of X : not K c= A} by A1,Th32; now let x be set; hereby assume x in candidate-keys F; then consider a being Subset of X such that A3: x = a and A4: [a,X] in Maximal_wrt F; per cases by A2,A4,XBOOLE_0:def 2; suppose [a,X] in {[K, X]}; then [a,X] = [K,X] by TARSKI:def 1; then a = K by ZFMISC_1:33; hence x in {K} by A3,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 A5: [a,X] = [A,A] and A6: not K c= A; a = A & X = A by A5,ZFMISC_1:33; hence x in {K} by A6; end; end; assume x in {K}; then A7: x = K by TARSKI:def 1; [K,X] in {[K,X]} by TARSKI:def 1; then [K,X] in Maximal_wrt F by A2,XBOOLE_0:def 2; hence x in candidate-keys F by A7; end; hence candidate-keys F = {K} 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 :Def28: 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 Th25; then saturated-subsets F is (B1) by Th34; then X in saturated-subsets F by Def4; then consider B, A be Subset of X such that A2: X = B & A ^|^ B, F by Th33; [A,X] in Maximal_wrt F by A2,Def18; then A in candidate-keys F; hence candidate-keys F is non empty; let k1, k2 be set such that A3: k1 in candidate-keys F and A4: k2 in candidate-keys F and A5: k1 c= k2; consider a1 being Subset of X such that A6: k1 = a1 and A7: [a1, X] in Maximal_wrt F by A3; consider a2 being Subset of X such that A8: k2 = a2 and A9: [a2, X] in Maximal_wrt F by A4; A10: Maximal_wrt F is (M2) by A1,Th30; [a1,[#]X] >= [a2,[#]X] by A5,A6,A8, Th15; hence k1 = k2 by A6,A7,A8,A9,A10,Def20; 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; assume A1: C is (C1); assume A2: C is (C2); set 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 set; 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 x in bool X; 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 Th35; take F; A3: [#]X = X; A4: now let x be set; assume A5: x in C; then reconsider x' = x as Subset of X; now let c be set; assume A6: c in BB & x' c= c; then ex b being Subset of X st c = b & for K being Subset of X st K in C holds not K c= b; hence X c= c by A5,A6; end; then [x',X] in F by A3; then consider a, b being Subset of X such that A7: [a,b] in Maximal_wrt F and A8: [a, b] >= [x',[#]X] by Th28; A9: a c= x' by A8,Th15; X c= b by A8,Th15; then A10: b = X by XBOOLE_0:def 10; assume A11: not [x,X] in Maximal_wrt F; now let K be Subset of X; assume A12: K in C; assume A13: K c= a; then K c= x' by A9,XBOOLE_1:1; then K = x' by A2,A5,A12,Def28; hence contradiction by A7,A9,A10,A11,A13,XBOOLE_0:def 10; end; then a in BB; then X c= a by A7,A10,Lm2; then X = a by XBOOLE_0:def 10; hence contradiction by A7,A9,A10,A11,XBOOLE_0:def 10; end; now let x be set; hereby assume A14: x in C; then [x,X] in Maximal_wrt F by A4; hence x in candidate-keys F by A14; end; assume x in candidate-keys F; then consider A being Subset of X such that A15: x = A and A16: [A, X] in Maximal_wrt F; A17: for c being set st c in BB holds c = X or not A c= c proof let c be set; assume that A18: c in BB and A19: not c = X; consider cb being Subset of X such that A20: c = cb and for K being Subset of X st K in C holds not K c= cb by A18; assume A c= c; then X c= c by A3,A16,A18,Lm2; hence contradiction by A19,A20,XBOOLE_0:def 10; end; assume A21: not x in C; now given K being Subset of X such that A22: K in C and A23: K c= A; A24: [K,X] in Maximal_wrt F by A4,A22; A25: A ^|^ X, F by A16,Def18; [K, [#]X] >= [A, [#]X] by A23,Th15; hence contradiction by A15,A21,A22,A24,A25,Th29; end; then A in BB; then X in BB by A17; then consider b being Subset of X such that A26: b = X and A27: for K being Subset of X st K in C holds not K c= b; not ex K being set st K in C by A26,A27; hence contradiction by A1,XBOOLE_0:def 1; end; hence C = candidate-keys F 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}; set F = X deps_encl_by B; B c= bool X proof let x be set; 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 x in bool X; end; then reconsider BB = B as Subset-Family of X; A4: [#]X = X; A5: now let x be set; assume A6: x in C; then reconsider x' = x as Subset of X; now let c be set; assume A7: c in BB & x' c= c; then 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; hence X c= c by A6,A7; end; then [x',X] in F by A4; then consider a, b being Subset of X such that A8: [a,b] in Maximal_wrt F and A9: [a, b] >= [x',[#]X] by Th28; A10: a c= x' by A9,Th15; X c= b by A9,Th15; 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= x' by A10,XBOOLE_1:1; then K = x' by A2,A6,A13,Def28; hence contradiction by A8,A10,A11,A12,A14,XBOOLE_0:def 10; end; then a in BB by A3; then X c= a by A8,A11,Lm2; then X = a by XBOOLE_0:def 10; hence contradiction by A8,A10,A11,A12,XBOOLE_0:def 10; end; now let x be set; hereby assume A15: x in C; then [x,X] in Maximal_wrt F by A5; 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; A18: for c being set st c in BB holds c = X or not A c= c proof let c be set; assume that A19: c in BB and A20: not c = X; consider cb being Subset of X such that A21: c = cb and for K being Subset of X st K in C holds not K c= cb by A3,A19; assume A c= c; then X c= c by A4,A17,A19,Lm2; hence contradiction by A20,A21,XBOOLE_0:def 10; end; assume A22: not x in C; now given K being Subset of X such that A23: K in C and A24: K c= A; A25: [K,X] in Maximal_wrt F by A5,A23; A26: A ^|^ X, F by A17,Def18; [K, [#]X] >= [A, [#]X] by A24,Th15; hence contradiction by A16,A22,A23,A25,A26,Th29; end; then A in BB by A3; then X in BB by A18; then consider b being Subset of X such that A27: b = X and A28: for K being Subset of X st K in C holds not K c= b by A3; not ex K being set st K in C by A27,A28; hence contradiction by A1,XBOOLE_0:def 1; end; hence C = candidate-keys F 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); set M = {L where L is Subset of X: for K being Subset of X st K in C holds L/\K <> {}}; 0 in {0} by TARSKI:def 1; then A3: 0 in M\/{0} by XBOOLE_0:def 2; reconsider M0 = M\/{0} as non empty set; reconsider D = X --> bool X as non-empty ManySortedSet of X; set R = { (X --> 0) +* (L --> L) where L is Subset of X : L in M0 }; A4: (X --> 0) +* ({}X --> {}X) in R by A3; R c= product D proof let x be set; 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 by FUNCOP_1:19; then A7: dom g = dom (X --> 0)\/L by FUNCT_4:def 1 .= X\/L by FUNCOP_1:19 .= X by XBOOLE_1:12; A8: dom D = X by PBOOLE:def 3; now let x be set such that A9: x in dom D; A10: D.x = bool X by A8,A9,FUNCOP_1:13; per cases; suppose A11: x in L; then g.x = (L --> L).x by A6,FUNCT_4:14 .= L by A11,FUNCOP_1:13; hence g.x in D.x by A10; end; suppose not x in L; then g.x = (X --> 0).x by A6,FUNCT_4:12 .= {}X by A8,A9,FUNCOP_1:13; hence g.x in D.x by A10; end; end; hence x in product D by A5,A7,A8,CARD_3:def 5; end; then reconsider R as non empty Subset of product D by A4; 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 }; A12: [#]X = X; :: And here WWA writes that the rest is "easy to show". Good luck. :: Interesting in showing C = ck we show C c= ck and then in order to show :: that ck c= C we use the fact that C c= ck. I do not understand why so. A13: now let x be set; assume A14: x in C; then reconsider A = x as Subset of X; reconsider AA = A, XA = X as Subset of the Attributes of DB by A12; now let f, g be Element of the Relationship of DB such that A15: f|A = g|A; f in R; then consider Lf being Subset of X such that A16: f = (X --> 0) +* (Lf --> Lf) and A17: Lf in M0; g in R; then consider Lg being Subset of X such that A18: g = (X --> 0) +* (Lg --> Lg) and A19: Lg in M0; A20: (Lf in M or Lf in {0}) & (Lg in M or Lg in {0}) by A17,A19,XBOOLE_0:def 2; A21: dom (Lg --> Lg) = Lg by FUNCOP_1:19; A22: dom (Lf --> Lf) = Lf by FUNCOP_1:19; per cases by A20,TARSKI:def 1; suppose Lf in M & Lg in M; then consider Lff being Subset of X such that A23: Lf = Lff and A24: for K being Subset of X st K in C holds Lff/\K <> {}; A25: Lf /\ A <> {} by A14,A23,A24; then consider a being set such that A26: a in Lf /\ A by XBOOLE_0:def 1; A27: a in Lf & a in A by A26,XBOOLE_0:def 3; then A28: (f|A).a = f.a by FUNCT_1:72 .= (Lf --> Lf).a by A16,A22,A27,FUNCT_4:14 .= Lf by A27,FUNCOP_1:13; A29: (g|A).a = g.a by A27,FUNCT_1:72; g.a = 0 or g.a = Lg proof per cases; suppose A30: a in Lg; then g.a = (Lg --> Lg).a by A18,A21,FUNCT_4:14; hence thesis by A30,FUNCOP_1:13; end; suppose not a in Lg; then g.a = (X --> 0).a by A18,A21,FUNCT_4:12; hence thesis by A26,FUNCOP_1:13; end; end; hence f|X = g|X by A15,A16,A18,A25,A28,A29; end; suppose A31: Lf in M & Lg = 0; then consider L being Subset of X such that A32: Lf = L and A33: for K being Subset of X st K in C holds L/\K <> {}; A34: Lf /\ A <> {} by A14,A32,A33; then consider a being set such that A35: a in Lf /\ A by XBOOLE_0:def 1; A36: a in A & a in Lf by A35,XBOOLE_0:def 3; A37: dom (Lg --> Lg) = {} by A31; A38: (g|A).a = g.a by A36,FUNCT_1:72 .= ((X --> 0) +* {}).a by A18,A37,RELAT_1:64 .= (X --> 0).a by FUNCT_4:22 .= {} by A35,FUNCOP_1:13; (f|A).a = f.a by A36,FUNCT_1:72 .= (Lf --> Lf).a by A16,A22,A36,FUNCT_4:14 .= Lf by A36,FUNCOP_1:13; hence f|X = g|X by A15,A34,A38; end; suppose A39: Lf = 0 & Lg in M; then consider L being Subset of X such that A40: Lg = L and A41: for K being Subset of X st K in C holds L/\K <> {}; A42: Lg /\ A <> {} by A14,A40,A41; then consider a being set such that A43: a in Lg /\ A by XBOOLE_0:def 1; A44: a in A & a in Lg by A43,XBOOLE_0:def 3; A45: dom (Lf --> Lf) = {} by A39; A46: (f|A).a = f.a by A44,FUNCT_1:72 .= ((X --> 0) +* {}).a by A16,A45,RELAT_1:64 .= (X --> 0).a by FUNCT_4:22 .= {} by A43,FUNCOP_1:13; (g|A).a = g.a by A44,FUNCT_1:72 .= (Lg --> Lg).a by A18,A21,A44,FUNCT_4:14 .= Lg by A44,FUNCOP_1:13; hence f|X = g|X by A15,A42,A46; end; suppose Lf = 0 & Lg = 0; hence f|X = g|X by A16,A18; end; end; then AA >|> XA, DB by Def8; then [A,X] in ds; then consider a, b being Subset of X such that A47: [a,b] in Maximal_wrt ds and A48: [a, b] >= [A,[#]X] by Th28; A49: a c= A & X c= b by A48,Th15; then A50: b = X by XBOOLE_0:def 10; [a,b] in ds by A47; then consider aa, XX being Subset of the Attributes of DB such that A51: [a,b] = [aa,XX] and A52: aa >|> XX, DB; A53: a = aa & b = XX by A51,ZFMISC_1:33; now assume A54: a <> A; set r0 = X --> 0; set r1 = (X --> 0) +* (a` --> a`); 0 in {0} by TARSKI:def 1; then 0 in M0 by XBOOLE_0:def 2; then A55: (X --> 0) +* ({}X --> {}X) in R; now let K be Subset of X; assume A56: K in C; assume a` /\ K = {}; then K misses a` by XBOOLE_0:def 7; then A57: K c= a by SUBSET_1:44; then K c= A by A49,XBOOLE_1:1; then K = A by A2,A14,A56,Def28; hence contradiction by A49,A54,A57,XBOOLE_0:def 10; end; then a` in M; then a` in M0 by XBOOLE_0:def 2; then A58: r1 in R; A59: dom (a` --> a`) = a` by FUNCOP_1:19; reconsider r0, r1 as Element of the Relationship of DB by A55,A58, FUNCT_4:22; now A60: dom (r0|a) = dom r0 /\ a by RELAT_1:90; A61: dom r0 = X by FUNCOP_1:19; dom r1 = dom (X --> 0)\/dom (a` --> a`) by FUNCT_4:def 1 .= X\/dom (a` --> a`) by FUNCOP_1:19 .= X\/a` by FUNCOP_1:19 .= X by XBOOLE_1:12; hence dom (r0|a) = dom r1 /\ a by A61,RELAT_1:90; let x be set; assume x in dom (r0|a); then A62: x in a by A60,XBOOLE_0:def 3; a misses a` by XBOOLE_1:79; then a /\ a` = {} by XBOOLE_0:def 7; then A63: not x in a` by A62,XBOOLE_0:def 3; thus (r0|a).x = (X --> 0).x by A62,FUNCT_1:72 .= r1.x by A59,A63,FUNCT_4:12; end; then A64: r0|a = r1|a by FUNCT_1:68; A65: now assume a` = {}; then a` c= a by XBOOLE_1:2; then a = X by A12,SUBSET_1:39; hence contradiction by A49,A54,XBOOLE_0:def 10; end; then consider y being set such that A66: y in a` by XBOOLE_0:def 1; A67: (r0|X).y = r0.y by A66,FUNCT_1:72 .= 0 by A66,FUNCOP_1:13; (r1|X).y = r1.y by A66,FUNCT_1:72 .= (a` --> a`).y by A59,A66,FUNCT_4:14 .= a` by A66,FUNCOP_1:13; hence contradiction by A50,A52,A53,A64,A65,A67,Def8; end; then [A,X] in Maximal_wrt ds by A47,A49,XBOOLE_0:def 10; hence x in ck; end; now let x be set; thus x in C implies x in ck by A13; assume x in ck; then consider A being Subset of X such that A68: x = A and A69: [A, X] in Maximal_wrt ds; A70: [A,X] in ds by A69; A71: now let K be set such that A72: K in C and A73: K c= A; K in ck by A13,A72; then consider B being Subset of X such that A74: K = B and A75: [B, X] in Maximal_wrt ds; reconsider AA = A, B, XA = X as Subset of the Attributes of DB by A12; assume A76: K <> A; A77: A ^|^ [#]X, ds by A69,Def18; [AA,XA] <= [B,XA] by A73,A74,Th15; hence contradiction by A74,A75,A76,A77,Th29; end; consider K being set such that A78: K in C by A1,XBOOLE_0:def 1; reconsider K as Subset of X by A78; assume A79: not x in C; then not K c= A by A68,A71,A78; then consider k being set such that A80: k in K & not k in A by TARSKI:def 3; set m = { a where a is Element of X: not a in A & ex K being set st K in C & a in K }; reconsider k as Element of X by A80; A81: k in m by A78,A80; then consider n being set such that A82: n in m; now let x be set; 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; then reconsider m as Subset of X by TARSKI:def 3; now let K be Subset of X such that A83: K in C; not K c= A by A68,A71,A79,A83; then consider k being set such that A84: k in K & not k in A by TARSKI:def 3; k in m by A83,A84; hence m/\K <> {} by A84,XBOOLE_0:def 3; end; then A85: m in M; set r0 = X --> 0, r1 = (X --> 0) +* (m --> m); 0 in {0} by TARSKI:def 1; then 0 in M0 by XBOOLE_0:def 2; then A86: (X --> 0) +* ({}X --> {}X) in R; m in M0 by A85,XBOOLE_0:def 2; then r1 in R; then reconsider r0, r1 as Element of the Relationship of DB by A86, FUNCT_4:22; A87: dom (m --> m) = m by FUNCOP_1:19; now A88: dom (r0|A) = dom r0 /\ A by RELAT_1:90; A89: dom r0 = X by FUNCOP_1:19; dom r1 = dom (X --> 0)\/dom (m --> m) by FUNCT_4:def 1 .= X\/dom (m --> m) by FUNCOP_1:19 .= X\/m by FUNCOP_1:19 .= X by XBOOLE_1:12; hence dom (r0|A) = dom r1 /\ A by A89,RELAT_1:90; let x be set such that A90: x in dom (r0|A); A91: x in A by A88,A90,XBOOLE_0:def 3; 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 A88,A90,XBOOLE_0:def 3; end; thus (r0|A).x = (X --> 0).x by A91,FUNCT_1:72 .= r1.x by A87,A92,FUNCT_4:12; end; then A93: r0|A = r1|A by FUNCT_1:68; consider aa, XX being Subset of the Attributes of DB such that A94: [A,X] = [aa,XX] and A95: aa >|> XX, DB by A70; A96: A = aa & X = XX by A94,ZFMISC_1:33; A97: m c= X; then A98: (r0|X).n = r0.n by A82,FUNCT_1:72 .= 0 by A82,A97,FUNCOP_1:13; (r1|X).n = r1.n by A82,FUNCT_1:72 .= (m --> m).n by A82,A87,FUNCT_4:14 .= m by A82,FUNCOP_1:13; hence contradiction by A81,A93,A95,A96,A98,Def8; end; hence C = candidate-keys Dependency-str DB by TARSKI:2; end; begin :: 9. Applications definition let X be set, F be Dependency-set of X; attr F is (DC4) means :Def29: for A, B, C being Subset of X st [A, B] in F & [A, C] in F holds [A, B\/C] in F; attr F is (DC5) means :Def30: for A, B, C, D being Subset of X st [A, B] in F & [B\/C, D] in F holds [A\/C, D] in F; attr F is (DC6) means :Def31: 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 [A, B] in F & [A, C] in F; then [A\/A, B\/C] in F by A4,Def14; hence [A, B\/C] in F; end; end; assume that A5: F is (DC1) and A6: F is (DC3) and A7: F is (DC4); thus F is (F1) by A5,A6; thus F is (F2) by A5; thus F is (F3) by A5,A6; let A, B, A', B' be Subset of X such that A8: [A, B] in F and A9: [A', B'] in F; A c= A\/A' & A' c= A\/A' by XBOOLE_1:7; then [A\/A', A] in F & [A\/A', A'] in F by A6,Def16; then [A\/A', B] in F & [A\/A', B'] in F by A5,A8,A9,Th20; hence [A\/A', B\/B'] in F by A7,Def29; 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,Def12; then [A\/C, B\/C] in F by A4,A5,Def14; hence [A\/C, D] in F by A2,A6,Th20; end; thus F is (DC6) proof let A, B, C be Subset of X such that A7: [A, B] in F; A8: F is (DC3) by A1,A3; A c= A\/C by XBOOLE_1:7; then [A\/C, A] in F by A8,Def16; hence [A\/C, B] in F by A2,A7,Th20; end; end; assume that A9: F is (DC2) and A10: F is (DC5) and A11: F is (DC6); thus F is (F1) by A9; A12: now let A, B, C be Subset of X such that A13: [A, B] in F and A14: [B, C] in F; [B\/A, C] in F by A11,A14,Def31; then [A\/A, C] in F by A10,A13, Def30; hence [A, C] in F; end; hence F is (F2) by Th20; thus F is (F3) proof let A, B, A', B' be Subset of X such that A15: [A, B] in F and A16: [A, B] >= [A', B']; A17: A c= A' & B' c= B by A16,Th15; then A' = A\/(A'\A) by XBOOLE_1:45; then A18: [A', B] in F by A11,A15,Def31; A19: [B', B'] in F by A9,Def12; B = B'\/(B\B') by A17,XBOOLE_1:45; then [ B, B'] in F by A11,A19, Def31; hence [A', B'] in F by A12,A18; end; let A, B, A', B' be Subset of X such that A20: [A, B] in F and A21: [A', B'] in F; [B\/B', B\/B'] in F by A9,Def12; then [A\/B', B\/B'] in F by A10,A20,Def30; hence [A\/A', B\/B'] in F by A10,A21,Def30; end; definition let X be set, F be Dependency-set of X; func charact_set F 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 Th57: 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 Th59: :: 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; A1: F c= G by Def25; 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 set; hereby assume A2: c in B; then c in bool A & not c in charact_set F by XBOOLE_0:def 4; then for x, y being Subset of A st [x,y] in F & x c= c holds y c= c; hence c in BB by A2; end; assume c in BB; then consider b being Subset of A such that A3: c = b and A4: 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 A4,Th57; hence c in B by A3,XBOOLE_0:def 4; end; then A5: B = BB by TARSKI:2; reconsider B as Subset-Family of A; 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 Th57; then A in B by XBOOLE_0:def 4; then A6: B is (B1) by Def4; A7: BB = enclosure_of F; then A8: B is (B2) by A5,Th38; 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}; A9: FF = A deps_encl_by B; then reconsider FF as Dependency-set of A; A10: FF is full_family by A9,Th35; F c= FF by A5,A7,A9,Th39; then A11: G c= FF by A10,Def25; A12: FF c= G by A1,A5,A7,A9,Th39; then A13: G = FF by A11,XBOOLE_0:def 10; hereby let X, Y be Subset of A; hereby assume A14: [X, Y] in G; let a be Subset of A such that A15: X c= a & not Y c= a; [X,Y] in FF by A11,A14; then consider a', b' being Subset of A such that A16: [a',b'] = [X,Y] and A17: for c being set st c in B & a' c= c holds b' c= c; A18: a' = X & b' = Y by A16,ZFMISC_1:33; assume not a in charact_set F; then a in B by XBOOLE_0:def 4; hence contradiction by A15,A17,A18; end; assume A19: 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 A20: c in B and A21: X c= c and A22: not Y c= c; reconsider c as Subset of A b