Database Reference
In-Depth Information
eliminated at the cost of multiplying dependencies. Formally, they are defined as:
First
(
x
)=
zero
bit
(
x
1
)
,
bit
(
x
2
)
,...,
bit
(
x
n
)
,
Last
(
x
)=
one
bit
(
x
1
)
,
bit
(
x
2
)
,...,
bit
(
x
n
)
,
i
−
1
n
bit
(
x
j
)
,
bit
(
y
j
)
,
zero
/
bit
(
x
i
)
Succ
(
x
,
y
)=
∧
one
/
bit
(
y
i
)
,
i
=1
j
=1
zero
/
bit
(
y
j
)
.
n
one
/
bit
(
x
j
)
∧
j
=
i
+1
Using the auxiliary patterns we ensure that the target tree encodes an accepting run of
M
. In the first configuration the tape is empty and the head state
q
0
is over the first cell,
r
[
First
(
x
)
,
First
(
y
)
,
q
0
(
u
)
,
(
v
)]
−→
r
//
cell
(
x
,
y
,
u
,
v
)
,
r
[
First
(
x
)
,
Succ
(
z
1
,
y
)
,
Succ
(
y
,
z
2
)
,
⊥
(
u
)
,
(
v
)]
−→
r
//
cell
(
x
,
y
,
u
,
v
)
,
(
u
)
,
(
v
)]
r
[
First
(
x
)
,
Last
(
y
)
,
⊥
−→
r
//
cell
(
x
,
y
,
u
,
v
)
.
Note that the valuations of
y
correspond to all numbers from 0 to 2
n
−
1, and thus the
content of each cell of the tape is specified.
The correctness of transitions is ensured by
r
Succ
(
x
0
,
x
1
)
,
Succ
(
y
1
,
y
2
)
,
Succ
(
y
2
,
y
3
)
−→
vr
/
tr
(
u
1
,
v
1
,
u
2
,
v
2
,...,
u
6
,
v
6
)
,
i
,
j
//
cell
(
x
i
,
y
j
,
u
3
i
+
j
,
v
3
i
+
j
)
.
−→ ∃
u
∃
≤
k
<
2
n
Again,
x
0
,
x
1
range over
k
,
k
+1 with 0
−
1, and
y
1
,
y
2
,
y
3
range over
,
+1
,
+2
<
2
n
with 0
2, which means that the evolution of each three consecutive cells is
checked for every step.
Finally, the machine needs to reach the accepting state (w.l.o.g. we assume that the
accepting state is looping),
r
q
f
(
u
)
≤
−
−→ ∃
x
∃
y
∃
vr
//
cell
(
x
,
y
,
u
,
v
)
.
Note that each occurrence of
//
above can be replaced with a sequence of and
/
symbols
of suitable length.
It is straightforward to verify that
M
has an accepting computation of length at most 2
n
if and only if
T
has a solution with respect to the mapping defined above.
