Corollary 3.3 There is a domino system D such that the following is a NEXPTIME-hard problem:
Given an initial condition w = wo . . . w n_1 of length n . Does D tile the torus U(2 n +1 , 2 n +1 ) with initial condition w?

Proof. Let M be a (w.l.o.g. simple) non-deterministic TM with time- (and hence space-)
bound 2 n deciding an arbitrary NEXPTIME-complete language L ( M ) over the alphabet Σ .

Let D be the according domino system and trans the reduction from Theorem 3.2.

The function trans is a linear reduction from L ( M ) to the problem above: For v E Σ*
with | v | = n, it holds that v ∈ L ( M ) iff M accepts v in time and space 2 l v | iff D tiles U(2n+1, 2n+1) with initial condition trans(v).

n

## 3.2  Defining A Torus Of Exponential Size

Similar to proving undecidability by reduction of unbounded domino problems, where defining infinite grids is the key problem, defining a torus of exponential size is the key to obtaining a NExpTimE-completeness proof by reduction of bounded domino problems.

To be able to apply Corollary 3.3 to T C Box consistency for ACQI , we must characterise the torus Z 2 n x Z 2 n with a T C Box of polynomial size. To characterise this torus, we use 2n concepts X 0 , . . ,Xn-1 and Y 0 , . . ,Yn-1, where X i (resp., Y i ) codes the ith bit of the binary representation of the X-coordinate (resp., Y-coordinate) of an element a .

For an interpretation I and an element a ∈ ∆ X , we define pos ( a ) by

$$\begin{split}\text{\it pos}\,s\big{(}a\big{)}:=&\big{(}\,xpos\big{(}a\big{)},\,ypos\big{(}a\big{)}\big{)}:=\left(\sum_{i=0}^{n-1}x_{i}\cdot2^{i},\quad\sum_{i=0}^{n-1}y_{i}\cdot2^{i}\right)\,,\text{where}\\ x_{i}=&\begin{cases}0,&\text{if}a\not\in X_{i}^{\mathcal{I}}\\ 1,&\text{otherwise}\end{cases}\quad y_{i}=\begin{cases}0,&\text{if}a\not\in Y_{i}^{\mathcal{I}}\\ 1,&\text{otherwise}\end{cases}\,.\end{split}$$  $\bullet$\(\bullet
We use a well-known characterisation of binary addition (e.g. (Börger et al., 1997)) to relate the positions of the elements in the torus:
Lemma 3.4 Let x, x' be natural numbers with binary representations

$$x=\sum_{i=0}^{n-1}x_{i}\cdot2^{i}\quad{\mathrm{and}}\quad x^{\prime}=\sum_{i=0}^{n-1}x_{i}^{\prime}\cdot2^{i}\,.$$
$$\mathrm{Then}$$
Then x' = x + 1 (mod 2" = 1) -> (xk = 1 <> xk = 0) = 0) → ( x k  = x k ) ,
where the empty conjunction and disjunction are interpreted as true and false, respectively.