let X be non empty finite set ; for 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 )
let F be 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 )
reconsider D = X --> INT as V11() ManySortedSet of X ;
consider G being Subset-Family of X such that
G is_generator-set_of saturated-subsets F
and
A1:
F = X deps_encl_by G
by Th43;
consider H being FinSequence such that
A2:
rng H = G
and
H is one-to-one
by FINSEQ_4:58;
then A6:
X --> 0 is Element of product D
by CARD_3:def 5;
reconsider H = H as FinSequence of G by A2, FINSEQ_1:def 4;
per cases
( G is empty or not G is empty )
;
suppose A7:
G is
empty
;
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 )set R =
{(X --> 0)};
{(X --> 0)} c= product D
then reconsider R =
{(X --> 0)} as non
empty Subset of
(product D) ;
set BD =
DB-Rel(#
X,
D,
R #);
take
DB-Rel(#
X,
D,
R #)
;
( the Attributes of DB-Rel(# X,D,R #) = X & ( for a being Element of X holds the Domains of DB-Rel(# X,D,R #) . a = INT ) & F = Dependency-str DB-Rel(# X,D,R #) )thus
( the
Attributes of
DB-Rel(#
X,
D,
R #)
= X & ( for
a being
Element of
X holds the
Domains of
DB-Rel(#
X,
D,
R #)
. a = INT ) )
;
F = Dependency-str DB-Rel(# X,D,R #)set Ds =
Dependency-str DB-Rel(#
X,
D,
R #);
now for x being object holds
( ( x in F implies x in Dependency-str DB-Rel(# X,D,R #) ) & ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F ) )let x be
object ;
( ( x in F implies x in Dependency-str DB-Rel(# X,D,R #) ) & ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F ) )hereby ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F )
assume
x in F
;
x in Dependency-str DB-Rel(# X,D,R #)then consider A,
B being
Subset of
X such that A8:
x = [A,B]
and
for
g being
set st
g in G &
A c= g holds
B c= g
by A1;
reconsider A =
A,
B =
B as
Subset of the
Attributes of
DB-Rel(#
X,
D,
R #) ;
A >|> B,
DB-Rel(#
X,
D,
R #)
hence
x in Dependency-str DB-Rel(#
X,
D,
R #)
by A8;
verum
end; assume
x in Dependency-str DB-Rel(#
X,
D,
R #)
;
x in Fthen consider A,
B being
Subset of the
Attributes of
DB-Rel(#
X,
D,
R #)
such that A9:
x = [A,B]
and
A >|> B,
DB-Rel(#
X,
D,
R #)
;
for
g being
set st
g in G &
A c= g holds
B c= g
by A7;
hence
x in F
by A1, A9;
verum end; hence
F = Dependency-str DB-Rel(#
X,
D,
R #)
by TARSKI:2;
verum end; suppose A10:
not
G is
empty
;
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 )then
not
H is
empty
by A2;
then reconsider n =
len H as non
zero Element of
NAT ;
defpred S1[
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 ) );
consider M being
Function of
X,
(n -tuples_on BOOLEAN) such that A18:
for
x being
Element of
X holds
S1[
x,
M . x]
from FUNCT_2:sch 3(A11);
set R =
{ f where f is Element of product D : ex i being Element of NAT st
for x being Element of X holds f . x = Absval ((n -BinarySequence i) '&' (M . x)) } ;
A19:
{ 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)) } c= product D
then
X --> 0 in { 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)) }
by A6;
then reconsider 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)) } as non
empty Subset of
(product D) by A19;
set BD =
DB-Rel(#
X,
D,
R #);
take
DB-Rel(#
X,
D,
R #)
;
( the Attributes of DB-Rel(# X,D,R #) = X & ( for a being Element of X holds the Domains of DB-Rel(# X,D,R #) . a = INT ) & F = Dependency-str DB-Rel(# X,D,R #) )thus
( the
Attributes of
DB-Rel(#
X,
D,
R #)
= X & ( for
a being
Element of
X holds the
Domains of
DB-Rel(#
X,
D,
R #)
. a = INT ) )
;
F = Dependency-str DB-Rel(# X,D,R #)set Ds =
Dependency-str DB-Rel(#
X,
D,
R #);
A21:
dom H = Seg n
by FINSEQ_1:def 3;
now for x being object holds
( ( x in F implies x in Dependency-str DB-Rel(# X,D,R #) ) & ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F ) )let x be
object ;
( ( x in F implies x in Dependency-str DB-Rel(# X,D,R #) ) & ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F ) )hereby ( x in Dependency-str DB-Rel(# X,D,R #) implies x in F )
assume
x in F
;
x in Dependency-str DB-Rel(# X,D,R #)then consider A,
B being
Subset of
X such that A22:
x = [A,B]
and A23:
for
g being
set st
g in G &
A c= g holds
B c= g
by A1;
reconsider A9 =
A,
B9 =
B as
Subset of the
Attributes of
DB-Rel(#
X,
D,
R #) ;
A9 >|> B9,
DB-Rel(#
X,
D,
R #)
proof
let f,
g be
Element of the
Relationship of
DB-Rel(#
X,
D,
R #);
ARMSTRNG:def 7 ( f | A9 = g | A9 implies f | B9 = g | B9 )
assume A24:
f | A9 = g | A9
;
f | B9 = g | B9
f in R
;
then consider Rf being
Element of
product D such that A25:
f = Rf
and A26:
ex
i being
Element of
NAT st
for
x being
Element of
X holds
Rf . x = Absval ((n -BinarySequence i) '&' (M . x))
;
consider fi being
Element of
NAT such that A27:
for
x being
Element of
X holds
Rf . x = Absval ((n -BinarySequence fi) '&' (M . x))
by A26;
g in R
;
then consider Rg being
Element of
product D such that A28:
g = Rg
and A29:
ex
i being
Element of
NAT st
for
x being
Element of
X holds
Rg . x = Absval ((n -BinarySequence i) '&' (M . x))
;
consider gi being
Element of
NAT such that A30:
for
x being
Element of
X holds
Rg . x = Absval ((n -BinarySequence gi) '&' (M . x))
by A29;
A31:
dom g =
dom D
by A28, CARD_3:9
.=
dom f
by A25, CARD_3:9
;
now ( dom (g | B) = (dom f) /\ B & ( for a being object st a in dom (g | B) holds
(g | B) . a = f . a ) )set nbg =
n -BinarySequence gi;
set nbf =
n -BinarySequence fi;
thus A32:
dom (g | B) = (dom f) /\ B
by A31, RELAT_1:61;
for a being object st a in dom (g | B) holds
(g | B) . a = f . alet a be
object ;
( a in dom (g | B) implies (g | B) . a = f . a )assume A33:
a in dom (g | B)
;
(g | B) . a = f . areconsider x =
a as
Element of
X by A32, A33;
reconsider Mx =
M . x as
Tuple of
n,
BOOLEAN ;
set ng =
(n -BinarySequence gi) '&' (M . x);
set nf =
(n -BinarySequence fi) '&' (M . x);
A34:
dom (M . x) = Seg n
by Lm2;
A35:
dom ((n -BinarySequence fi) '&' (M . x)) = Seg n
by Lm1;
A36:
a in B
by A32, A33, XBOOLE_0:def 4;
now ( dom ((n -BinarySequence fi) '&' (M . x)) = dom ((n -BinarySequence gi) '&' (M . x)) & ( for i being object st i in dom ((n -BinarySequence fi) '&' (M . x)) holds
((n -BinarySequence fi) '&' (M . x)) . i = ((n -BinarySequence gi) '&' (M . x)) . i ) )thus
dom ((n -BinarySequence fi) '&' (M . x)) = dom ((n -BinarySequence gi) '&' (M . x))
by A35, Lm1;
for i being object st i in dom ((n -BinarySequence fi) '&' (M . x)) holds
((n -BinarySequence fi) '&' (M . x)) . b2 = ((n -BinarySequence gi) '&' (M . x)) . b2let i be
object ;
( i in dom ((n -BinarySequence fi) '&' (M . x)) implies ((n -BinarySequence fi) '&' (M . x)) . b1 = ((n -BinarySequence gi) '&' (M . x)) . b1 )assume A37:
i in dom ((n -BinarySequence fi) '&' (M . x))
;
((n -BinarySequence fi) '&' (M . x)) . b1 = ((n -BinarySequence gi) '&' (M . x)) . b1per cases
( A c= H . i or not A c= H . i )
;
suppose
A c= H . i
;
((n -BinarySequence fi) '&' (M . x)) . b1 = ((n -BinarySequence gi) '&' (M . x)) . b1then A38:
B c= H . i
by A2, A21, A23, A35, A37, FUNCT_1:3;
A39:
Mx /. i =
Mx . i
by A34, A35, A37, PARTFUN1:def 6
.=
0
by A18, A36, A35, A37, A38
;
thus ((n -BinarySequence fi) '&' (M . x)) . i =
((n -BinarySequence fi) /. i) '&' (Mx /. i)
by A35, A37, Def5
.=
((n -BinarySequence gi) /. i) '&' (Mx /. i)
by A39
.=
((n -BinarySequence gi) '&' (M . x)) . i
by A35, A37, Def5
;
verum end; suppose A40:
not
A c= H . i
;
((n -BinarySequence fi) '&' (M . x)) . b1 = ((n -BinarySequence gi) '&' (M . x)) . b1thus
((n -BinarySequence fi) '&' (M . x)) . i = ((n -BinarySequence gi) '&' (M . x)) . i
verumproof
consider xx being
object such that A41:
xx in A
and A42:
not
xx in H . i
by A40;
reconsider xx =
xx as
Element of
X by A41;
A43:
f . xx =
(g | A) . xx
by A24, A41, FUNCT_1:49
.=
g . xx
by A41, FUNCT_1:49
;
reconsider Mxx =
M . xx as
Tuple of
n,
BOOLEAN ;
A44:
f . xx = Absval ((n -BinarySequence fi) '&' (M . xx))
by A25, A27;
A45:
g . xx = Absval ((n -BinarySequence gi) '&' (M . xx))
by A28, A30;
dom (M . xx) = Seg n
by Lm2;
then A46:
Mxx /. i =
Mxx . i
by A35, A37, PARTFUN1:def 6
.=
1
by A18, A35, A37, A42
;
then A47:
(n -BinarySequence fi) /. i =
((n -BinarySequence fi) /. i) '&' (Mxx /. i)
.=
((n -BinarySequence fi) '&' (M . xx)) . i
by A35, A37, Def5
.=
((n -BinarySequence gi) '&' (M . xx)) . i
by A43, A44, A45, BINARI_3:2
.=
((n -BinarySequence gi) /. i) '&' (Mxx /. i)
by A35, A37, Def5
.=
(n -BinarySequence gi) /. i
by A46
;
thus ((n -BinarySequence fi) '&' (M . x)) . i =
((n -BinarySequence fi) /. i) '&' (Mx /. i)
by A35, A37, Def5
.=
((n -BinarySequence gi) '&' (M . x)) . i
by A35, A37, A47, Def5
;
verum
end; end; end; end; then
(n -BinarySequence fi) '&' (M . x) = (n -BinarySequence gi) '&' (M . x)
by FUNCT_1:2;
then g . a =
Absval ((n -BinarySequence fi) '&' (M . x))
by A28, A30
.=
f . a
by A25, A27
;
hence
(g | B) . a = f . a
by A33, FUNCT_1:47;
verum end;
hence
f | B9 = g | B9
by FUNCT_1:46;
verum
end; hence
x in Dependency-str DB-Rel(#
X,
D,
R #)
by A22;
verum
end; assume
x in Dependency-str DB-Rel(#
X,
D,
R #)
;
x in Fthen consider A,
B being
Subset of the
Attributes of
DB-Rel(#
X,
D,
R #)
such that A48:
x = [A,B]
and A49:
A >|> B,
DB-Rel(#
X,
D,
R #)
;
now for gg being set st gg in G & A c= gg holds
B c= ggdeffunc H1(
Element of
X)
-> Element of
NAT =
Absval ((n -BinarySequence 0) '&' (M . $1));
let gg be
set ;
( gg in G & A c= gg implies B c= gg )assume that A50:
gg in G
and A51:
A c= gg
and A52:
not
B c= gg
;
contradictionreconsider gg =
gg as
Element of
G by A50;
consider f being
Function of
X,
NAT such that A53:
for
x being
Element of
X holds
f . x = H1(
x)
from FUNCT_2:sch 4();
A55:
dom f = dom D
by FUNCT_2:def 1;
then reconsider f =
f as
Element of
product D by A54, CARD_3:def 5;
consider i being
Nat such that A56:
i in dom H
and A57:
H . i = gg
by A2, A10, FINSEQ_2:10;
i <> 0
by A21, A56, FINSEQ_1:1;
then consider k being
Nat such that A58:
i = k + 1
by NAT_1:6;
consider bx being
object such that A59:
bx in B
and A60:
not
bx in gg
by A52;
reconsider bx =
bx as
Element of
X by A59;
reconsider Mbx =
M . bx as
Tuple of
n,
BOOLEAN ;
A61:
f in R
by A53;
dom Mbx = Seg n
by Lm1;
then A62:
Mbx /. i =
Mbx . i
by A21, A56, PARTFUN1:def 6
.=
1
by A21, A18, A60, A56, A57
;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
deffunc H2(
Element of
X)
-> Element of
NAT =
Absval ((n -BinarySequence (2 to_power k)) '&' (M . $1));
consider g being
Function of
X,
NAT such that A63:
for
x being
Element of
X holds
g . x = H2(
x)
from FUNCT_2:sch 4();
A65:
dom g = dom D
by FUNCT_2:def 1;
then reconsider g =
g as
Element of
product D by A64, CARD_3:def 5;
i <= n
by A21, A56, FINSEQ_1:1;
then A66:
k < n
by A58, NAT_1:13;
then A81:
f | A = g | A
by FUNCT_1:46;
set bs0 =
n -BinarySequence 0;
set bsi =
n -BinarySequence (2 to_power k);
A82:
n -BinarySequence 0 =
0* n
by BINARI_3:25
.=
n |-> 0
by EUCLID:def 4
;
dom (n -BinarySequence 0) = Seg n
by Lm1;
then A83:
(n -BinarySequence 0) /. i =
(n -BinarySequence 0) . i
by A21, A56, PARTFUN1:def 6
.=
0
by A82
;
dom (n -BinarySequence (2 to_power k)) = Seg n
by Lm1;
then A84:
(n -BinarySequence (2 to_power k)) /. i =
(n -BinarySequence (2 to_power k)) . i
by A21, A56, PARTFUN1:def 6
.=
1
by A58, A66, Th7
;
A85:
((n -BinarySequence (2 to_power k)) '&' Mbx) . i =
((n -BinarySequence (2 to_power k)) /. i) '&' (Mbx /. i)
by A21, A56, Def5
.=
(n -BinarySequence (2 to_power k)) /. i
by A62
;
A86:
((n -BinarySequence 0) '&' Mbx) . i =
((n -BinarySequence 0) /. i) '&' (Mbx /. i)
by A21, A56, Def5
.=
(n -BinarySequence 0) /. i
by A62
;
g in R
by A63;
then A87:
f | B = g | B
by A49, A61, A81;
Absval ((n -BinarySequence 0) '&' (M . bx)) =
f . bx
by A53
.=
(f | B) . bx
by A59, FUNCT_1:49
.=
g . bx
by A59, A87, FUNCT_1:49
.=
Absval ((n -BinarySequence (2 to_power k)) '&' (M . bx))
by A63
;
hence
contradiction
by A83, A86, A85, A84, BINARI_3:2;
verum end; hence
x in F
by A1, A48;
verum end; hence
F = Dependency-str DB-Rel(#
X,
D,
R #)
by TARSKI:2;
verum end; end;