Database Reference
In-Depth Information
a linear order of length 2
n
. With every
c
-node
v
we associate the sequence of
a
's and
b
's
on the path leading from the root to
v
. This sequence is interpreted as a binary number (
a
read as 0,
b
read as 1), which is the position of
v
in the order. The auxiliary patterns take
the following form:
First
(
x
)=
ord
/
a
1
/
a
2
/
···
/
a
n
/
c
(
x
)
,
Last
(
x
)=
ord
/
b
1
/
b
2
/
···
/
b
n
/
c
(
x
)
,
n
//
a
i
/
b
i
+1
/
b
i
+2
/
Succ
(
x
,
y
)=
···
/
b
n
/
c
(
x
)
,
i
=1
/
a
n
/
c
(
y
)
,
b
i
/
a
i
+1
/
a
i
+2
/
···
//
a
i
/
b
i
+1
/
b
i
+2
/
n
−
1
/
b
n
−
1
a
n
/
c
(
x
)
,
b
n
/
c
(
y
)
,
Succ
3
(
x
,
y
,
z
)=
···
i
=1
/
a
n
/
c
(
z
)
b
i
/
a
i
+1
/
a
i
+2
/
···
∨
//
a
i
/
b
i
+1
/
b
i
+2
/
n
−
1
∨
···
/
b
n
/
c
(
x
)
,
i
=1
/
a
n
−
1
a
n
/
c
(
y
)
,
b
n
/
c
(
z
)
.
b
i
/
a
i
+1
/
a
i
+2
/
···
Each occurrence of
//
above can be replaced with a sequence of
/
and symbols, and
disjunction can be eliminated since we only use the auxiliary patterns on the source side.
To build the first configuration we copy the input word stored in the sequence of
zero
and
one
nodes with the head in the state
q
0
over the first cell,
r
First
(
x
)
,
First
(
y
)
/
s
,
q
0
(
u
)
,
s
(
v
)
−→
r
//
Cell
(
x
,
y
,
u
,
v
)
,
r
First
(
x
)
,
Succ
3
(
z
1
,
y
,
z
2
)
/
s
,
(
u
)
,
s
(
v
)
−→
r
//
Cell
(
x
,
y
,
u
,
v
)
,
⊥
r
First
(
x
)
,
Last
(
y
)
/
s
,
(
u
)
,
s
(
v
)
−→
⊥
r
//
Cell
(
x
,
y
,
u
,
v
)
,
where
s
ranges over
A
\{}
and by
Succ
3
(
z
1
,
y
,
z
2
)
/
s
we mean
Succ
3
(
z
1
,
y
,
z
2
) with
c
(
y
)
replaced with
c
(
y
)
/
s
.
To make sure we encode a correct accepting run, we add
r
Succ
(
x
0
,
x
1
)
,
Succ
3
(
y
1
,
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
∃
r
q
f
(
u
)
−→ ∃
x
∃
y
∃
vr
//
cell
(
x
,
y
,
u
,
v
)
.
We claim that the mapping we have just defined is absolutely consistent iff the answer to
n
-
UNIVERSALITY
is “yes”. Assume that the mapping is absolutely consistent. Every input
word
w
can be encoded in a source tree using distinct data values. An inductive argument
shows that a solution to such a tree encodes an accepting run of
M
on
w
.Conversely,if
the answer is “yes”, for each source tree
S
using distinct data values, a solution is obtained
