

![0_image_0.png](0_image_0.png)

![0_image_1.png](0_image_1.png)

![0_image_2.png](0_image_2.png)

The TCBox Tn is dened in Figure 3. The 
on
ept C(0;0) is satised by all elements a of the domain for whi h pos(a) = (0; 0) holds. C(2n1;2n1) is a similar 
on
ept, whose instan es a satisfy pos(a) = (2n  1; 2n  1).

The on ept Dnorth is similar to Deast where the role north has been substituted for east and variables Xi and Yi have been swapped. The 
on
ept Deast (resp. Dnorth) enfor
es that, along the role east (resp. north), the value of xpos (resp. ypos) in reases by one while the value of ypos (resp. xpos) is un hanged. They are analogous to the formula in Lemma 3.4.

The following lemma is a onsequen e of the denition of pos and Lemma 3.4.

Lemma 3.5 Let I = (I; 
I

) be an interpretation, Deast; Dnorth dened as in Figure 3, and a; b 2 I.

$(a,b)\in\mathit{eat}^{\mathcal{I}}$ and $a\in D^{\mathcal{I}}_{\mathit{as}t}$ implies: $\mathit{xpos}(b)\equiv\mathit{xpos}(a)+1\pmod{2^{n}}$ $\mathit{ypos}(b)=\mathit{ypos}(a)$ $(a,b)\in\mathit{north}^{\mathcal{I}}$ and $a\in D^{\mathcal{I}}_{\mathit{nor}b}$ implies: $\mathit{xpos}(b)=\mathit{xpos}(a)$ $\mathit{ypos}(b)\equiv\mathit{ypos}(a)+1\pmod{2^{n}}$

The TCBox Tn denes a torus of exponential size in the following sense:
Lemma 3.6 Let Tn be the TCBox as dened in Figure 3. Let I = (I; 
I

) be a model of Tn. Then
(I; eastI; northI) = (U(2n; 2 n

); S1; S2) ;