Information Technology Reference
In-Depth Information
The case where (13) holds is analogous. Hence
s
(
y
)=
s
(
z
). This concludes
=
X
∗
ʸ
.
We have now concluded Step 3 of the outline of the proof. Next we show the last
part of the proof. That is, we show that
X
∗
can be constructed by quantifying
Q
1
x
1
...Q
m
x
m
in
A
,
b
,ʵ
(
c
|
the case of inclusion atom and thus the proof of (
))
A
over
{∅}
. For this, it suces to show the following claim.
be such that
Q
p
X
∗
Claim.
Let
a
∈
A
,
p
∈{
1
,...,m
}
=
∀
,and
s
∈
X
∗
{
{
.
Proof (Claim).
Let
a
,
p
and
s
be as in the assumption. Then
s
=
h
(
f
x
1
,...,x
p−
1
}
.Then
s
(
a/x
p
)
∈
x
1
,...,x
p
}
ⓦ
t
)
{
x
1
,...,x
p−
1
}
,
X
.Let
a
0
=
f
−
1
(
a
)and
a
1
=
f
−
1
for some
f
ʵ
(
a
). Note that
both
t
(
a
0
/x
p
)
{x
1
,...,x
p
}
and
t
(
a
1
/x
p
)
{x
1
,...,x
p
}
are in
X
{x
1
,...,x
p
}
since
Q
p
=
∀
.Let
t
0
,t
1
∈ X
extend
t
(
a
0
/x
p
)
{x
1
,...,x
p
}
and
t
(
a
1
/x
p
)
{
∈F
and
t
∈
ⓦ
x
1
,...,x
p
}
, respectively. It suces to show that either
h
(
f
ⓦ
t
0
)or
h
(
f
ⓦ
t
1
)
(which both are in
X
∗
)extend
s
(
a/x
p
).
Firstnotethatsince
t
0
{
x
1
,...,x
p−
1
}
=
t
1
{
x
1
,...,x
p−
1
}
=
t
{
x
1
,...,x
p−
1
}
we have by item 3 of the definition of mid that, for
i
≤
p
−
1, inequalities (14),
(15) and (16) are equivalent:
row(
t
0
(
x
i
))
<
mid(row(
t
0
(
x
)))
,
(14)
row(
t
1
(
x
i
))
<
mid(row(
t
1
(
x
)))
,
(15)
row(
t
(
x
i
))
<
mid(row(
t
(
x
)))
.
(16)
Since also
f
preserves the rows, we have by the definition of
h
that
h
(
f
ⓦ
t
0
),
h
(
f
t
) all agree in variables
x
1
,...,x
p−
1
. Note that also
ʵ
preserves
the rows, so have row(
a
0
)=row(
a
1
). Since then row(
t
0
(
x
i
)) = row(
t
1
(
x
i
)), for
i
ⓦ
t
1
)and
h
(
f
ⓦ
≤
p
, we have by item 3 of the definition of mid that
row(
t
0
(
x
p
))
<
mid(row(
t
0
(
x
))) iff row(
t
1
(
x
p
))
<
mid(row(
t
1
(
x
)))
.
Therefore, either
row(
t
0
(
x
p
))
<
mid(row(
t
0
(
x
))) or row(
t
1
(
x
p
))
>
mid(row(
t
1
(
x
)))
.
Then in the first case
h
(
f
ⓦ
t
0
)(
x
p
)=
f
ⓦ
t
0
(
x
p
)=
a
, and in the second case
X
∗
{
h
(
f
ⓦ
t
1
)(
x
p
)=
ʵ
ⓦ
f
ⓦ
t
1
(
x
p
)=
ʵ
ⓦ
ʵ
(
a
)=
a
. Hence
s
(
a/x
p
)
∈
x
1
,...,x
p
}
.
This concludes the proof of Claim.
We have now shown that
X
∗
can be constructed by quantifying
Q
1
x
1
...Q
m
x
m
in
A
over
{∅}
. Also previously we showed that (
A
,
b
,ʵ
(
c
))
|
=
X
∗
ʸ
. Therefore,
since
ˆ
=
Q
1
x
1
...Q
m
x
m
ʸ
, we obtain that (
A
,
b
,ʵ
(
c
))
|
=
ˆ
. Hence the as-
sumption that
ˆ
(
b
,
c
) defines
¬
[TC
x
,
y
E
DGE
k
](
b
,
c
) is false. Otherwise
A
|
=
¬
b
,
c
A
,
b
,
c
|
=
ˆ
from which (
A
,
b
,ʵ
(
c
|
=
ˆ
[TC
x
,
y
E
DGE
k
](
)wouldyield(
)
))
A
|
¬
b
,ʵ
(
c
follows. Therefore we would obtain
=
[TC
x
,
y
E
DGE
k
](
)) which contra-
A
|
¬
b
,ʵ
(
c
dicts the fact that
=
[TC
x
,
y
E
DGE
k
](
)) by Theorem 8. This concludes
the proof of Lemma 1.
