▷ $\psi_1 \stackrel{\text{def}}{=} \forall x \exists^{\le 1} y . \text{right}(x, y) \wedge \exists^{\le 1} y . \text{right}(y, x)$ states that **right** and $\text{right}^{-1}$ are partial functions, $\psi_2$ states that that **up** and $\text{up}^{-1}$ are partial functions,

▷ $\psi_3 \stackrel{\text{def}}{=} \forall x, y, z . \text{up}(x, y) \wedge \text{right}(x, z) \rightarrow \exists w . \text{up}(z, w) \wedge \text{right}(y, w)$ states that **right** and **up** commute, $\psi_4$ states that $\text{right}^{-1}$ and **up** commute, $\psi_5$ states that **right** and $\text{up}^{-1}$ commute and $\psi_6$ states that $\text{right}^{-1}$ and $\text{up}^{-1}$ commute,

▷ $\psi_7 \stackrel{\text{def}}{=} \forall x . \mathbf{S}(x) \leftrightarrow \neg \exists y . \mathbf{up}(y, x)$ states that south-labelled nodes are exactly the ones that do not have incoming **up** edges, and $\psi_8, \psi_9, \psi_{10}$ define the analogous property for the west, east, and north labels,

▷ $\psi_{11} \stackrel{\text{def}}{=} \forall x . \mathbf{I}(x) \leftrightarrow \neg (\mathbf{S}(x) \lor \mathbf{E}(x) \lor \mathbf{N}(x) \lor \mathbf{W}(x))$ states that internal nodes are exactly the ones not labelled by south, east, north or west,

▷ $\psi_{12} \stackrel{\text{def}}{=} \forall x . \mathbf{I}(x) \rightarrow \exists y . \mathbf{right}(x, y) \wedge \exists y . \mathbf{right}(y, x)$ states that internal nodes have exactly one outgoing and exactly one incoming **right** edge, $\psi_{13}$ states that internal nodes have exactly one outgoing and exactly one incoming **up** edge,

▷ $\phi_1 \stackrel{\text{def}}{=} \forall x . \bigvee_{i=1}^n \mathbf{T}_i(x)$ states that every coordinate holds at least one tile,

▷ $\phi_2 \stackrel{\text{def}}{=} \forall x . \bigwedge_{i \neq j} \neg \mathbf{T}_i(x) \lor \neg \mathbf{T}_j(x)$ states that every coordinate holds at most one tile,

▷ $\phi_3 \stackrel{\text{def}}{=} \forall x \forall y . \mathbf{right}(x, y) \rightarrow \bigvee_{(t_i, t_j) \in \mathcal{H}} \mathbf{T}_i(x) \wedge \mathbf{T}_j(y)$ states that tiles, that are next to each other horizontally, satisfy the horizontal matching constraint, and

▷ $\phi_4 \stackrel{\text{def}}{=} \forall x \forall y . \mathbf{up}(x, y) \rightarrow \bigvee_{(t_i, t_j) \in \mathcal{V}} \mathbf{T}_i(x) \wedge \mathbf{T}_j(y)$ states that tiles, that are next to each other vertically, satisfy the vertical matching constraint.

As usual, the formulæ $\exists^{\le 1} x . \varphi$ stand for $\exists x . \varphi \rightarrow \forall y . \varphi[x/y] \rightarrow y = x$. The proof will make use of the fact that $\phi$ encodes grids and non-standard models of grids, which are (disjoint unions of) grid-like structures. We will argue the following:

**Fact 5.2.** Each model of $\phi$ can be decomposed into (disjoint unions of) grids, cylinders, and toruses, where grids have S, E, W, N borders, cylinders have either S, N or E, W borders, and toruses do not have any borders and only consist of internal nodes.

*Proof.* We recall that we are only interested in finite models of first-order formulæ. We note that $\phi$ specifies that **up** and **right** are (partial) functions, and, hence, we will use functional notation in the following. We now fix a model $(U, \sigma)$ of $\phi$ – as usual, we require that $U \neq \emptyset$. We decompose $(U, \sigma)$ into its maximally connected components, connected via **up**, **right**. We choose a representative $u_C$, for each component $C$. We observe that either there are $j \le 0 \le i$ such that $\text{right}^j(u_C)$ is W-labelled and $\text{right}^i(u_C)$ is E-labelled, or $\text{right}^i(u_C) = u_C$, for some $i \ge 0$ (because the universe is finite and the functionality of **right** and $\text{right}^{-1}$ ensures that the only possible loop returns to $u_C$). An analogous statement holds for **up** as well as the N and S labels. We now call a component $C$ a *grid*, if $u_C$ reaches S, E, W, N via **up**, **right** and their inverses, a *cylinder* if $u_C$ reaches S, N or E, W via **up** and its inverse resp. **right** and its inverse, or a *torus*, otherwise. $\square$

We now justify the naming of these components:

**Fact 5.3.** Consider a grid component $C$ with representative $u_C$ such that $\text{right}^j(u_C)$ is W-labelled, $\text{right}^i(u_C)$ is E-labelled, $\text{up}^k(u_C)$ is S-labelled and $\text{up}^l(u_C)$ is N-labelled, for some $j \le 0 \le i$ and $k \le 0 \le l$. We claim that:

(1) the elements $\text{right}^a(\text{up}^b(u_C))$ exist, for all $j \le a \le i$ and all $k \le b \le l$,

(2) an element $\text{right}^a(\text{up}^b(u_C))$, for $j \le a \le i$ and $k \le b \le l$, is E-labelled iff $a = i$; analogous claims hold for the labels S, W, N,

(3) the elements $\text{right}^a(\text{up}^b(u_C))$ are internal nodes, for all $j < a < i$ and all $k < b < l$,
(4) the elements $\mathbf{right}^a(\mathbf{up}^b(u_C))$ are pairwise different, for all $j \le a \le i$ and all $k \le b \le l$,

(5) all elements of the component can be represented as $\mathbf{right}^a(\mathbf{up}^b(u_C))$, for some $j \le a \le i$ and $k \le b \le l$, and

(6) the component is isomorphic to a grid.

**Proof.** Items (1), (2) and (3) directly follow from the commutativity requirements. For (4), we consider some $j \le a_1, a_2 \le i$ and $k \le b_1, b_2 \le l$. We will show that $a_1 \ne a_2$ resp. $b_1 \ne b_2$ imply that $\mathbf{right}^{a_1}(\mathbf{up}^{b_1}(u_C)) \ne \mathbf{right}^{a_2}(\mathbf{up}^{b_2}(u_C))$. We will assume that $\mathbf{right}^{a_1}(\mathbf{up}^{b_1}(u_C)) = \mathbf{right}^{a_2}(\mathbf{up}^{b_2}(u_C))$ and derive a contradiction. Let us assume that $a_1 > a_2$ (the other cases are analogous). Then, we have $\mathbf{right}^{a_1+s}(\mathbf{up}^{b_1}(u_C)) = \mathbf{right}^{a_2+s}(\mathbf{up}^{b_2}(u_C))$ for $s = i - a_1 \ge 0$. However, $\mathbf{right}^{a_1+s}(\mathbf{up}^{b_1}(u_C))$ is E-labelled, while $\mathbf{right}^{a_2+s}(\mathbf{up}^{b_2}(u_C))$ is not, by (2), contradiction. For (5), we observe that every node reachable from $u_C$ connected via up, right and their inverses can be represented as $\mathbf{right}^a(\mathbf{up}^b(u_C))$, because of the commutativity requirements; further, we must have $j \le a \le i$ and $k \le b \le l$ because the S,E,W,N borders do not have outgoing edges. For (6), we observe that the component is isomorphic to the structure with domain $\{(x,y) \mid x,y \in [j,i], y \in [k,l]\}$, where right is interpreted as $\{((x,y),(x+1,y)) \mid x \in [j,i-1], y \in [k,l]\}$ and up as $\{((x,y),(x,y+1)) \mid x \in [j,i], y \in [k,l-1]\}$. $\square$

**Fact 5.4.** Consider a cylinder component $C$ with representative $u_C$ such that $\mathbf{right}^j(u_C)$ is W-labelled, $\mathbf{right}^i(u_C)$ is E-labelled, and $\mathbf{up}^k(u_C) = u_C$ for some $j \le 0 \le i$ and $k \le 0$, where $k$ is the smallest number with this property. (The properties stated below hold analogously for N,S cylinders). We claim that:

(1) the elements $\mathbf{right}^a(\mathbf{up}^b(u_C))$ exist, for all $j \le a \le i$ and all $0 \le b < k$,

(2) an element $\mathbf{right}^a(\mathbf{up}^b(u_C))$, for $j \le a \le i$ and $0 \le b < k$, is E-labelled iff $a = i$; an analogous claim holds for the label W,

(3) the elements $\mathbf{right}^a(\mathbf{up}^b(u_C))$ are internal nodes, for all $j < a < i$ and all $0 \le b < k$,

(4) all the elements $\mathbf{right}^a(\mathbf{up}^b(u_C))$ are pairwise different, for all $j \le a \le i$ and all $0 \le b < k$,

(5) all nodes of the component can be represented as $\mathbf{right}^a(\mathbf{up}^b(u_C))$, for some $j \le a \le i$ and $0 \le b < k$, and

(6) the component is isomorphic to a cylinder, i.e., a grid for which the north-border connects to south-border.

**Proof.** Items (1), (2) and (3) directly follow from the commutativity requirements. For (4), we consider some $j \le a_1, a_2 \le i$ and $0 \le b_1, b_2 < k$. We will show that $a_1 \ne a_2$ resp. $b_1 \ne b_2$ imply that $\mathbf{right}^{a_1}(\mathbf{up}^{b_1}(u_C)) \ne \mathbf{right}^{a_2}(\mathbf{up}^{b_2}(u_C))$. We will assume that $\mathbf{right}^{a_1}(\mathbf{up}^{b_1}(u_C)) = \mathbf{right}^{a_2}(\mathbf{up}^{b_2}(u_C))$ and derive a contradiction. Let us first assume that $a_1 > a_2$ (the case $a_1 < a_2$ is symmetric). Then, we have $\mathbf{right}^{a_1+s}(\mathbf{up}^{b_1}(u_C)) = \mathbf{right}^{a_2+s}(\mathbf{up}^{b_2}(u_C))$ for $s = i - a_1$. However, $\mathbf{right}^{a_1+s}(\mathbf{up}^{b_1}(u_C))$ is E-labelled, while $\mathbf{right}^{a_2+s}(\mathbf{up}^{b_2}(u_C))$ is not, by (2), contradiction. Now we assume $a_1 = a_2$ and $b_1 > b_2$ (the case $b_1 < b_2$ is symmetric). Then, $\mathbf{right}^{a_1}(\mathbf{up}^{b_1}(u_C)) = \mathbf{right}^{a_2}(\mathbf{up}^{b_2}(u_C))$ implies that $\mathbf{up}^{b_1-b_2}(u_C) = u_C$ with $0 \le b_1 - b_2 < k$. However, this contradicts that $k$ is the smallest number with this property. For (5), we observe that every node reachable from $u_C$ connected via up, right and their inverses can be represented as $\mathbf{right}^a(\mathbf{up}^b(u_C))$, because of the commutativity requirements; further, we can in fact choose $0 \le b < k$ because of commutativity and the assumption that $\mathbf{up}^k(u_C) = u_C$. Moreover, we must have $j \le a \le i$ because the E,W borders do not have outgoing edges. For (6), we observe that
the component is isomorphic to the structure with domain {((x, y) | x, y ∈ [j, i], y ∈ [k, l])}, where right is interpreted as {((x, y), (x + 1, y)) | x ∈ [j, i − 1], y ∈ [0, k − 1]} and up as {((x, y), (x, y + 1)) | x ∈ [j, i], y ∈ [0, k − 2]} ∪ {((x, k), (x, 1)) | x ∈ [j, i]}. □

**Fact 5.5.** Consider a torus component *C*, with representative *u*<sub>*C*</sub> such that *up*<sup>*k*</sup>(*u*<sub>*C*</sub>) = *u*<sub>*C*</sub> and *right*<sup>*l*</sup>(*u*<sub>*C*</sub>) = *u*<sub>*C*</sub> for some *k* ≤ 0 and *l* ≤ 0, where *k* and *l* are the smallest numbers with this property. We claim that:

(1) the elements $\mathbf{right}^a(\mathbf{up}^b(u_C))$, for all $0 \le a < k$ and all $0 \le b < l$,

(2) the elements $\mathbf{right}^a(\mathbf{up}^b(u_C))$ are internal nodes, for all $0 \le a < k$ and all $0 \le b < l$,

(3) all nodes of the component can be represented as $\mathbf{right}^a(\mathbf{up}^b(u_C))$, for some $0 \le a < k$ and $0 \le b < l$.

*Proof.* Items (1) and (2) directly follow from the commutativity requirements. For (3), we observe that every node reachable from $u_C$ connected via up, right and their inverses can be represented as some $\mathbf{right}^a(\mathbf{up}^b(u_C))$ because of the commutativity requirements; further, we can in fact choose $0 \le a < k$ and $0 \le b < l$ because of commutativity and the assumptions that $\mathbf{up}^k(u_C) = u_C$ and $\mathbf{right}^k(u_C) = u_C$. We note that the $\mathbf{right}^a(\mathbf{up}^b(u_C))$ are in general not pairwise different (e.g., we might have $\mathbf{right}^a(u_C) = \mathbf{up}^b(u_C)$ for some $0 \le a < k$ and $0 \le b < l$). However, in our below argument we do not need to distinguish whether all the elements $\mathbf{right}^a(\mathbf{up}^b(u_C))$ of a torus component are pairwise different. $\square$

The following claim reduces the treewidth boundedness problem for first-order logic to
the tiling problem for the first quadrant of the plane:

**Fact 5.6.** $\phi$ has models of unbounded treewidth iff there is a tiling of the upper-right quadrant of the plane.

*Proof.* “$\Leftarrow$” Let us assume that there is a tiling of the upper-right quadrant of the plane. Then, for every $n \in \mathbb{N}$, this tiling induces a square grid $G_n$ of size $n \times n$ with $G_n \models \phi$: simply take the tiles at positions $(x, y)$, with $x, y \in [1, n]$, from the tiling of the upper-right quadrant, and verify that in this way we obtain a model of the formula $\phi$.

“$\Rightarrow$” We now assume that $\phi$ has models of unbounded treewidth, i.e., for every $i \ge 1$ there is a finite model $(\mathcal{U}, \sigma)$ with $\mathrm{tw}((\mathcal{U}, \sigma)) \ge i$. If any model $(\mathcal{U}, \sigma)$ contains a torus component $C$, we immediately obtain a tiling of the upper-right quadrant by unrolling the torus: we define the tiling of the upper right quadrant by placing the tile of the element $\mathbf{right}^i(\mathbf{up}^j(u_C))$ at position $(i, j)$. It is then routine to verify that the subformula $\bigwedge_{j=1}^4 \phi_j$ of $\phi$ ensures that the matching requirements of a tiling are satisfied. Hence, we are left with the case that no model of $\phi$ contains a torus component.

We now observe that an $n \times m$ grid has treewidth $\min\{n, m\}$ and an $n \times m$ cylinder has treewidth $\min\{2n, m\}$ resp. $\min\{n, 2m\}$ for E, W resp. S, N cylinders. For the $n \times m$ grid, this follows from the $k$-cops and robber game, defined as follows. A position in the game is a pair $(\gamma, r)$, where $\gamma \subseteq [1..n] \times [1..m]$, $\mathrm{card}(\gamma) = k$ and $r \in [1..n] \times [1..m] \setminus \gamma$. The game can move from $(\gamma_i, r_i)$ to $(\gamma_{i+1}, r_{i+1})$ iff there exists a path between $r_i$ and $r_{i+1}$ in the restriction of the grid to $[1..n] \times [1..m] \setminus (\gamma_i \cap \gamma_{i+1})$. We say that $k$ cops catch the robber iff every sequence of moves in the game is finite. It is known that, if the treewidth of the graph is greater or equal to $k$, then $k+1$ cops catch the robber on a graph $G$ [ST93]. Since $\min\{n, m\} - 1$ cops do not catch the robber (which can always move to the intersection of a cop-free row and a cop-free column) it follows that the treewidth of the grid is greater than $\min\{n, m\} - 1$. At the same time, there exists a tree decomposition of width $\min\{n, m\}$. For the $n \times m$ N-S
cylinder (the case of the E-W cylinder is analogous), we need extra $n$ cops to prevent the robber escaping wrapping around the E-W axis, thus the treewidth is $\min\{2n, m\}$.

We now consider some $i \ge 0$ and some model $(U, \sigma)$ with $\mathrm{tw}((U, \sigma)) \ge 2i$ that does not contain torus components. Then, $N$ decomposes into grid components and cylinder components. Because of our assumption $\mathrm{tw}((U, \sigma)) \ge 2i$ there must be some component $C$ of $N$ with $\mathrm{tw}(C) \ge 2i$. Now, we can deduce that $C$ contains some square grid $M$ of size $i \times i$ as a substructure (this follows from $2i \le \min\{n, m\}$ for grids and from $2i \le \min\{n, 2m\}$ resp. $2i \le \min\{2n, m\}$ for cylinders). Hence, we can restrict our attention to models of $\phi$ that are square grids. Let $M_1, M_2, \dots$ be a sequence of models with $M_n \models \phi$, where each $M_n$ is a square grid of size $n \times n$. We are now going to construct a sequence of models $G_1, G_2, \dots$ such that each $G_n$ is a square grid of size $n$ with $G_n \models \phi$, and each $G_n$ is included in $G_{n+1}$, where we say a model $I$ of $\phi$ is included in a model $J$ of $\phi$ if $I$ resp. $J$ are square grids of size $n \times n$ resp. $m \times m$, and we have that $n \le m$ and all tiles at positions $(x, y)$, with $x, y \in [1, n]$, are the same in both models. We construct the sequence $G_1, G_2, \dots$ inductively, maintaining an infinite sequence of models $M_1^n, M_2^n, \dots$, for each $n \in \mathbb{N}$, such that $G_n$ is included in all $M_i^n$: Take $G_1$ to be a model that consists of a single tile, which appears infinitely often at position $(1, 1)$ in the models $M_1, M_2, \dots$; then we obtain the sequence $M_1^1, M_2^1, \dots$ as the restriction of $M_1, M_2, \dots$ to the models that include $G_1$. Assume we have already defined $G_n$. Choose some square grid $G_{n+1}$ of size $n+1$ that is included infinitely often in models of the sequence $M_1^n, M_2^n, \dots$ (note that such a square grid must exist by the pigeonhole principle); then obtain the sequence $M_1^{n+1}, M_2^{n+1}, \dots$ by restricting the sequence to the $M_1^n, M_2^n, \dots$ to the models that include $G_{n+1}$. With the sequence $G_1, G_2, \dots$ at hand we now obtain a tiling of the plane: For position $(i, j)$, with $i, j \in \mathbb{N}$, simply take the tile at this position in $G_{\max\{i,j\}}$. We now verify that the horizontal resp. vertical requirements of a tiling are satisfied. We verify only the horizontal requirement (the vertical one is symmetric). Consider tiles at positions $(i, j)$ and $(i+1, j)$. If $i \ne j$, then both tiles have been defined by $G_{\max\{i,j\}}$, and the matching requirement is satisfied because $G_{\max\{i,j\}}$ is a model of $\phi$. If $i = j$ then the tile at position $(i, i)$ is defined by $G_i$ and the tile at position $(i+1, i)$ is defined by $G_{i+1}$. Now we observe that the tile at position $(i, i)$ in $G_i$ is the same as the tile at position $(i, i)$ in $G_{i+1}$, because $G_i$ is included in $G_{i+1}$, and the matching requirement is satisfied because $G_{i+1}$ is a model of $\phi$. $\square$

This concludes the proof of the theorem. $\square$

## 6. CONCLUSIONS

We have presented a decision procedure for the treewidth boundedness problem in the context of SLR, a generalization of Separation Logic over relational signatures, interpreted over structures. This procedure allows to define the precise fragment of SLR in which every formula has a bound on the treewidth of its models. This fragment is the right candidate for the definition of a fragment of SLR with a decidable entailment problem. Another application is checking that each graph defined by a treewidth-bounded SLR formula satisfies MSO-definable properties such as, e.g., Hamiltonicity, or 3-Colorability.
REFERENCES

[ABIK22] Emma Ahrens, Marius Bozga, Radu Iosif, and Joost-Pieter Katoen. Reasoning about distributed reconfigurable systems. *Proc. ACM Program. Lang.*, 6(OOPSLA2):145–174, 2022. doi:10.1145/3563293.

[ABS00] Serge Abiteboul, Peter Buneman, and Dan Suciu. *Data on the Web: From Relations to Semistructured Data and XML*. Morgan Kaufmann, 2000.

[Acz77] Peter Aczel. An introduction to inductive definitions. In *Handbook of Mathematical Logic*, volume 90 of *Studies in Logic and the Foundations of Mathematics*, pages 739–782. Elsevier, 1977. doi:10.1016/S0049-237X(08)71120-0.

[BBI22a] Marius Bozga, Lucas Bueri, and Radu Iosif. Decision problems in a logic for reasoning about reconfigurable distributed systems. In *Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings*, volume 13385 of *Lecture Notes in Computer Science*, pages 691–711. Springer, 2022. doi:10.1007/978-3-031-10769-6\_40.

[BBI22b] Marius Bozga, Lucas Bueri, and Radu Iosif. On an invariance problem for parameterized concurrent systems. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, *33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland*, volume 243 of *LIPIcs*, pages 24:1–24:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.CONCUR.2022.24.

[BCO06] Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, *Formal Methods for Components and Objects*, pages 115–137, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.

[Ber66] Robert Berger. *The undecidability of the domino problem*. American Mathematical Soc., 1966.

[BFPG14] James Brotherston, Carsten Fuhs, Juan Antonio Navarro Pérez, and Nikos Gorogiannis. A decision procedure for satisfiability in separation logic with inductive predicates. In Thomas A. Henzinger and Dale Miller, editors, *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 25:1–25:10. ACM, 2014. doi:10.1145/2603088.2603091.

[Bod98] Hans L. Bodlaender. A partial k-arboretum of graphs with bounded treewidth. *Theor. Comput. Sci.*, 209(1-2):1–45, 1998. doi:10.1016/S0304-3975(97)00228-4.

[CDNQ12] Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. *Science of Computer Programming*, 77(9):1006–1036, 2012. The Programming Languages track at the 24th ACM Symposium on Applied Computing (SAC'09). doi:10.1016/j.scico.2010.07.004.

[CDOY11] Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. *J. ACM*, 58(6), December 2011. doi:10.1145/2049697.2049700.

[CE12] Bruno Courcelle and Joost Engelfriet. *Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach*. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2012. doi:10.1017/CBO9780511977619.

[CGG02] Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. A Spatial Logic for Querying Graphs. In Peter Widmayer, Francisco Triguero Ruiz, Rafael Morales Bueno, Matthew Hennessy, Stephan Eidenbenz, and Ricardo Conejo, editors, *Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP'02)*, volume 2380 of *Lecture Notes in Computer Science*, pages 597–610. Springer, July 2002.

[CHO+11] Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, and James Worrell. Tractable reasoning in a fragment of separation logic. In Joost-Pieter Katoen and Barbara König, editors, *CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings*, volume 6901 of *Lecture Notes in Computer Science*, pages 235–249. Springer, 2011. doi:10.1007/978-3-642-23217-6\_16.

[Cou90] Bruno Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. *Information and Computation*, 85(1):12–75, 1990. doi:10.1016/0890-5401(90)90043-H.

[COY07] Cristiano Calcagno, Peter W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In *22nd IEEE Symposium on Logic in Computer Science (LICS 2007)*, 10-12 July 2007,
Wroclaw, Poland, Proceedings, pages 366–378. IEEE Computer Society, 2007. doi:10.1109/LICS. 2007.30.

[DNM08] Pierpaolo Degano, Rocco De Nicola, and José Meseguer, editors. *Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday*, volume 5065 of *Lecture Notes in Computer Science*. Springer, 2008. doi:10.1007/978-3-540-68679-8.

[DPJ08] Dino Distefano and Matthew J. Parkinson. J.Star: towards practical verification for java. In *Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications*, OOPSLA '08, page 213–226, New York, NY, USA, 2008. Association for Computing Machinery. doi:10.1145/1449764.1449782.

[EF95] Heinz-Dieter Ebbinghaus and Jörg Flum. *Finite model theory*. Perspectives in Mathematical Logic. Springer, 1995.

[EIP21a] Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Decidable entailments in separation logic with inductive definitions: Beyond establishment. In Christel Baier and Jean Goubault-Larrecq, editors, *29th EACSL Annual Conference on Computer Science Logic (CSL 2021)*, volume 183 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 20:1–20:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl–Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CSL.2021.20.

[EIP21b] Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Unifying decidable entailments in separation logic with inductive definitions. In André Platzer and Geoff Sutcliffe, editors, *Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings*, volume 12699 of *Lecture Notes in Computer Science*, pages 183–199. Springer, 2021. doi:10.1007/978-3-030-79876-5\_11.

[EIP22] Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules. *Inf. Process. Lett.*, 173:106169, 2022. doi:10.1016/J.IPL.2021.106169.

[FG06] Jörg Flum and Martin Grohe. *Parameterized Complexity Theory*. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2006. doi:10.1007/3-540-29953-X.

[IO01] Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Chris Hankin and Dave Schmidt, editors, *Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001*, pages 14–26. ACM, 2001.

[IRS13] Radu Iosif, Adam Rogalewicz, and Jirí Simácek. The tree width of separation logic with recursive definitions. In Maria Paola Bonacina, editor, *Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings*, volume 7898 of *Lecture Notes in Computer Science*, pages 21–38. Springer, 2013. doi:10.1007/978-3-642-38574-2\_2.

[IZ23] Radu Iosif and Florian Zuleger. Expressiveness results for an inductive logic of separated relations. In Guillermo A. Pérez and Jean-François Raskin, editors, *34th International Conference on Concurrency Theory (CONCUR 2023)*, volume 279 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 20:1–20:20, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.CONCUR.2023.20.

[JKM$^{+}$17] Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger. Unified reasoning about robustness properties of symbolic-heap separation logic. In Hongseok Yang, editor, *Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings*, volume 10201 of *Lecture Notes in Computer Science*, pages 611–638. Springer, 2017. doi:10.1007/978-3-662-54434-1\_23.

[JM82] Neil D. Jones and Steven S. Muchnick. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In *Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '82*, page 66–74, New York, NY, USA, 1982. Association for Computing Machinery. doi:10.1145/582153.582161.

[KR04] Viktor Kuncak and Martin Rinard. Generalized records and spatial conjunction in role logic. In *Static Analysis*, pages 361–376, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.

[KZ20] Jens Katelaan and Florian Zuleger. Beyond symbolic heaps: Deciding separation logic with inductive definitions. In Elvira Albert and Laura Kovács, editors, *LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain*, 2020. doi:10.1007/978-3-662-54434-1\_24.
May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 390-408. EasyChair, 2020.
doi:10.29007/vkmj.

[LL23] Quang Loc Le and Xuan-Bach Dinh Le. An efficient cyclic entailment procedure in a fragment of separation logic. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 477-497. Springer, 2023. doi:10.1007/978-3-031-30829-1\_23.

[Rey02] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74. IEEE Computer Society, 2002. doi:10.1109/LICS.2002.1029817.

[See91] D. Seese. The structure of the models of decidable monadic theories of graphs. Annals of Pure and Applied Logic, 53(2):169-195, 1991. doi:10.1016/0168-0072(91)90054-P.

[ST93] P.D. Seymour and R. Thomas. Graph searching and a min-max theorem for tree-width. Journal of Combinatorial Theory, Series B, 58(1):22-33, 1993. doi:10.1006/jctb.1993.1027.

[vD94] Dirk van Dalen. Logic and structure (3. ed.). Universitext. Springer, 1994.

APPENDIX A. PROOFS FROM SECTION 2

A.1. **Proof of Lemma 2.9.** Without loss of generality, we consider that $\Delta$ is equality-free (Lemma 2.6). We propose a construction using an idea of Brotherston et al [BFPG14], that characterizes the satisfiability of a predicate by an abstraction consisting of tuples of parameters occurring in the interpretation of relation symbols. A similar abstraction has been used to check satisfiability of SLR formulæ [BBI22a].

**Definition A.1.** A base $\sigma^{\sharp}$ is a mapping $\sigma^{\sharp} : \mathbb{R} \to \text{mpow}(\mathbb{V}^{+})$ of relation symbols $r$ into multisets of tuples of variables of length $\#r$ each. A base is satisfiable iff $\sigma^{\sharp}(r)$ is a set, for all $r \in \mathbb{R}$. Given a set of variables $X \subseteq \mathbb{V}$, let $\text{SatBase}(X)$ denote the set of satisfiable bases whose images contain only variables from $X$ and let $\text{SatBase}^{\text{def}} = \text{SatBase}(\mathbb{V})$.

We consider three partial operations on $\text{SatBase}$. First, the composition is $\sigma_1^{\sharp} \otimes \sigma_2^{\sharp} \stackrel{\text{def}}{=} \sigma_1^{\sharp} \cup \sigma_2^{\sharp}$ if $\sigma_1^{\sharp} \cup \sigma_2^{\sharp}$ is satisfiable, and undefined, otherwise. Second, the substitution $\sigma^{\sharp}[x_1/y_1, \dots, x_n/y_n]$ replaces simultaneously each occurrence of $x_j$ by $y_j$ in $\sigma^{\sharp}$, for all $j \in [1..n]$. Third, given a set $X \subseteq \mathbb{V}$ of variables, the projection is:

$$ \sigma^{\sharp}|_{X} \stackrel{\text{def}}{=} \lambda r . \{ \langle x_1, \dots, x_n \rangle \in \sigma^{\sharp}(r) \mid x_1, \dots, x_n \in X \} $$

Finally, for a qpf formula $\phi$, we define:

$$ \text{Base}(\phi) \stackrel{\text{def}}{=} \lambda r . \{ \langle x_1, \dots, x_n \rangle \mid r(x_1, \dots, x_n) \text{ occurs in } \phi \} $$

The predicates $\mathbf{B}^{\sigma^{\sharp}}$ of the SID $\overline{\Delta}$ are obtained by annotating each predicate $\mathbf{B}$ that occurs in $\Delta$ with a satisfiable base $\sigma^{\sharp}$. The arity of each predicate $\mathbf{B}^{\sigma^{\sharp}}$ is the arity of $\mathbf{B}$. Then $\overline{\Delta}$ contains the rules:

$$ \mathbf{B}_{0}^{\sigma_{0}^{\sharp}}(x_{1}, \dots, x_{\#\mathbf{B}_{0}}) \leftarrow \exists y_{1} \dots \exists y_{m} . \psi * \mathbf{B}_{i}^{\sigma_{i}^{\sharp}}(z_{i,1}, \dots, z_{i, \#\mathbf{B}_{i}}) $$

where $\mathbf{B}_0(x_1, \dots, x_{\#\mathbf{B}_0}) \leftarrow \exists y_1 \dots \exists y_m . \psi * \mathbf{B}_{i}^{\sigma_{i}^{\ell}}(z_{i,1}, \dots, z_{i, \#\mathbf{B}_{i}})$ is a rule of $\Delta$, $\psi$ is the largest qpf formula from its right-hand side and, moreover, the following condition holds:

$$ \sigma_0^{\sharp} = (\text{Base}(\psi) \otimes \bigotimes_{i=1}^{\ell} \sigma_i^{\sharp}[x_1/z_{i,1}, \dots, x_{\#\mathbf{B}_i}/z_{i,\#\mathbf{B}_i}]) |_{\{x_1, \dots, x_{\#\mathbf{B}_0}\}} $$
In addition, $\bar{\Delta}$ contains a rule $A \leftarrow A^{\sigma^{\#}}$, for each satisfiable base $\sigma^{\#} \in \text{SatBase}$. Note that $\bar{\Delta}$ is finite, because $\Delta$ and $\text{SatBase}$ are finite. We now prove the points from the statement of Lemma 2.9:

"$\bar{\Delta}$ is all-satisfiable for A" We prove the following, more general, fact:

**Fact A.2.** For each predicate $B^{\sigma^{\#}}$ that occurs in $\bar{\Delta}$, each predicate-free formula $\phi$ such that $B^{\sigma^{\#}} \Rightarrow_{\bar{\Delta}}^{*} \phi$ and each injective store $s$ over $\{x_1, \dots, x_{\#B}\}$, there exists a structure $S = (U, \sigma)$ such that $S \models^{\#} \phi$ and, for all $r \in \mathbb{R}$ and tuples of variables $\langle x_{j_1}, \dots, x_{j_{\#r}} \rangle$ with $j_k \in [1..\#B]$ for all $k \in [1..\#r]$, we have $\langle x_{j_1}, \dots, x_{j_{\#r}} \rangle \in \sigma^{\#}(r)$ if and only if $\langle s(x_{j_1}), \dots, s(x_{j_{\#r}}) \rangle \in \sigma(r)$.

*Proof.* We proceed by induction on the length of the unfolding $B^{\sigma^{\#}} \Rightarrow_{\bar{\Delta}}^{*} \phi$. The first step of the unfolding uses a rule:

$$B^{\sigma^{\#}}(x_1, \dots, x_{\#B}) \leftarrow \exists y_1 \dots \exists y_m . \psi * \mathbf{\ast}^{\ell}_{i=1} B_i^{\sigma^{\#}}(z_{i,1}, \dots, z_{i,\#B_i})$$

and for all $i \in [1..\ell]$, we have $B_i^{\sigma^{\#}} \Rightarrow_{\bar{\Delta}}^{*} \phi_i$, such that

$$\phi = \exists y_1 \dots \exists y_m . \psi * \mathbf{\ast}^{\ell}_{i=1} \phi_i[x_1/z_{i,1}, \dots, x_{\#B_i}/z_{i,\#B_i}]$$

modulo a reordering of atoms. Let $s'$ be an injective store that extends $s$ over $\{y_1, \dots, y_m\}$. For all $i \in [1..\ell]$, we define $s_i$ over $\{x_1, \dots, x_{\#B_i}\}$ by $s_i(x_j) \stackrel{\text{def}}{=} s'(z_{i,j})$ for all $j \in [1..\#B_i]$. By the inductive hypothesis applied to the unfolding $B_i^{\sigma^{\#}} \Rightarrow_{\bar{\Delta}}^{*} \phi_i$, there exists a structure $S_i = (U_i, \sigma_i)$ such that $S_i \models^{\#i} \phi_i$ and $\langle x_{j_1}, \dots, x_{j_{\#r}} \rangle \in \sigma_i^{\#}(r)$ if and only if $\langle s_i(x_{j_1}), \dots, s_i(x_{j_{\#r}}) \rangle \in \sigma_i(r)$. We can furthermore assume for all $i_1 \neq i_2 \in [1..\ell]$ that $\text{supp}(\sigma_{i_1}) \cap \text{supp}(\sigma_{i_2}) = \{s'(x_1), \dots, s'(x_{\#B}), s'(y_1), \dots, s'(y_m)\}$. Since $\psi$ is equality-free, there exists a structure $S_{\psi}$ such that $S_{\psi} \models^{\#} \psi$, and $\text{Base}(\psi)$ is a satisfiable base. We then prove that the structure $S = (U, \sigma) \stackrel{\text{def}}{=} S_{\psi} \bullet S_1 \bullet \dots \bullet S_{\ell}$ is defined and meets the requirements from the statement:

▷ Let $r \in \mathbb{R}$, and suppose, for a contradiction, that there exists a tuple $\langle u_1, \dots, u_{\#r} \rangle \in \sigma_{i_1}(r) \cap \sigma_{i_2}(r)$ for $i_1 \neq i_2 \in [1..\ell]$. From the induction hypothesis and because $s'$ is injective, there exists $\langle z_1, \dots, z_{\#r} \rangle \in \sigma_{i_1}^{\#}[x_1/z_{i_1,1}, \dots, x_{\#B_{i_1}}/z_{i_1,\#B_{i_1}}](r) \cap \sigma_{i_2}^{\#}[x_1/z_{i_2,1}, \dots, x_{\#B_{i_2}}/z_{i_2,\#B_{i_2}}](r)$ with $s'(z_k) = u_k$ for all $k \in [1..\#r]$. This contradicts that the following base composition:

$$\sigma_{i_1}^{\#}[x_1/z_{i_1,1}, \dots, x_{\#B_{i_1}}/z_{i_1,\#B_{i_1}}] \otimes \sigma_{i_2}^{\#}[x_1/z_{i_2,1}, \dots, x_{\#B_{i_2}}/z_{i_2,\#B_{i_2}}]$$

is defined. However, this must be the case, for the above derivation rule to exist in $\bar{\Delta}$. Therefore, the composition $S_1 \bullet \dots \bullet S_{\ell}$ is defined. The same type of argument can be used if the tuple occurs in the intersection between the interpretation of a relation symbol in $S_{\psi}$ and $S_i$, for some $i \in [1..\ell]$, thus the composition $S_{\psi} \bullet S_1 \bullet \dots \bullet S_{\ell}$ is defined.

▷ $S_{\psi} \bullet S_1 \bullet \dots \bullet S_{\ell} \models^{\#} \psi * \mathbf{\ast}^{\ell}_{i=1} B_i^{\sigma^{\#}}(z_{i,1}, \dots, z_{i,\#B_i})$ by construction, thus $S \models^{\#} \phi$.

▷ Let $r \in \mathbb{R}$ and $j_k \in [1..\#B]$ for all $k \in [1..\#r]$. We omit relations that occur in $\psi$ since this is a simple case. Then $\langle x_{j_1}, \dots, x_{j_{\#r}} \rangle \in \sigma^{\#}(r)$ if and only if $\langle x_{j'_1}, \dots, x_{j'_{\#r}} \rangle \in \sigma^{\#}(r)$ for some $i \in [1..\ell]$ and $x_{j_k} = z_{i,j'_k}$ for all $k \in [1..\#r]$, if and only if $\langle s_i(x_{j'_1}), \dots, s_i(x_{j'_{\#r}}) \rangle \in \sigma_i(r)$ by induction hypothesis, if and only if $\langle s(x_{j_1}), \dots, s(x_{j_{\#r}}) \rangle \in \sigma(r)$. $\square$

By taking any injective store $s$ over $\{x_1, \dots, x_{\#A}\}$, for every predicate-free formula $\phi$ such that $A^{\sigma^{\#}} \Rightarrow_{\bar{\Delta}}^{*} \phi$, we find a structure $S$ such that $S \models^{\#} \phi$, by Fact A.2. Therefore, $\bar{\Delta}$ is all-satisfiable for A.
"[[A]]<sub>Δ</sub> = [[A]]<sub>Δ</sub>" The inclusion [[A]]<sub>Δ</sub> ⊆ [[A]]<sub>Δ</sub> is immediate by simply removing the base annotations from any derivation run on Δ. For the converse, we prove the following fact:

**Fact A.3.** For every predicate B of Δ, for every structure S ∈ [[B]]<sub>Δ</sub> and store s such that S |=<sup>s</sup> B(x<sub>1</sub>, ..., x<sub>#B</sub>), there exists a satisfiable base σ<sup>‡</sup>, such that S |=<sup>s</sup> Bσ<sup>‡</sup>(x<sub>1</sub>, ..., x<sub>#B</sub>), and ⟨x<sub>j<sub>1</sub></sub>, ..., x<sub>j<sub>#r</sub></sub>⟩ ∈ σ<sup>‡</sup>(r) if and only if ⟨s(x<sub>j<sub>1</sub></sub>), ..., s(x<sub>j<sub>#r</sub></sub>)⟩ ∈ σ(r) for all r ∈ ℝ and j<sub>k</sub> ∈ [1..#B] for all k ∈ [1..#r].

*Proof.* Let $S \in [[B]]_{\Delta}$ and $\mathfrak{s}$ be such that $S \models^s B(x_1, \dots, x_{\#B})$. The proof is by induction on the derivation of $S \models^s B(x_1, \dots, x_{\#B})$. Assume that the first step of this derivation uses a rule $B(x_1, \dots, x_{\#B}) \leftarrow \exists y_1 \dots \exists y_m \cdot \psi * \mathbf{\ast}_{i=1}^{\ell} B_i(z_{i,1}, \dots, z_{i, \#B_i})$. Then, one can split $S = S_{\psi} \bullet S_1 \bullet \dots \bullet S_{\ell}$, such that $S_{\psi} \models^{s'} \psi$ and $S_i \models^{s_i} B_i(x_1, \dots, x_{\#B_i})$, where $\mathfrak{s}'$ extends $\mathfrak{s}_0$ and $\mathfrak{s}_i(x_j) = \mathfrak{s}'(z_{i,j})$ for all $i \in [1..\ell]$ and $j \in [1..\#B_i]$. By the induction hypothesis, for each $i \in [1..\ell]$, there exists a satisfiable base $\sigma_i^{\ddagger}$, such that $S_i \models^{s_i} B_i^{\sigma_i^{\ddagger}}(x_1, \dots, x_{\#B_i})$, and $\langle x_{j_1}, \dots, x_{j_{\#r}} \rangle \in \sigma_i^{\ddagger}(r)$ if and only if $\langle \mathfrak{s}(x_{j_1}), \dots, \mathfrak{s}(x_{j_{\#r}}) \rangle \in \sigma(r)$. We consider:

$$ \sigma^{\ddagger} \stackrel{\text{def}}{=} \left( \text{Base}(\psi) \otimes \bigotimes_{i=1}^{\ell} \sigma_i^{\ddagger} [x_1/z_{i,1}, \dots, x_{\#B_i}/z_{i,\#B_i}] \right) \downarrow_{\{x_1, \dots, x_{\#B}\}} $$

and prove that $\sigma^{\ddagger}$ is properly defined above:

▷ $\psi$ is satisfiable, thus so is $\text{Base}(\psi) = \sigma_{\psi}^{\ddagger}$. Projections over base pairs do not change the satisfiability, nor substitutions because $\Delta$ is equality-free.

▷ We check the satisfiability of the composition in the definition of $\sigma^{\ddagger}$. Suppose, for a contradiction, that there exists a tuple $\langle z_1, \dots, z_{\#r} \rangle \in \sigma_{\psi}^{\ddagger}(r) \cap \sigma_i^{\ddagger}[x_1/z_{i,1}, \dots, x_{\#B_i}/z_{i,\#B_i}](r)$ for some $i \in [1..\ell]$ and $z_k \in \{x_1, \dots, x_{\#B}, y_1, \dots, y_m\}$ for all $k \in [1..\#r]$. Then there exist $j_1, \dots, j_{\#r} \in [1..\#B_i]$ such that $\langle x_{j_1}, \dots, x_{j_{\#r}} \rangle \in \sigma_i^{\ddagger}(r)$ and $\mathfrak{s}_i(x_{j_k}) = \mathfrak{s}'(z_k)$ for all $k \in [1..\#r]$. Thus we obtain $\langle \mathfrak{s}'(z_1), \dots, \mathfrak{s}'(z_{\#r}) \rangle \in \sigma_{\psi}(r) \cap \sigma_i(r)$, which contradicts the composition $S_{\psi} \bullet S_i$. A similar argument ensures that no collisions occur between $S_{i_1}$ and $S_{i_2}$, for any $i_1 \neq i_2 \in [1..\ell]$.

The last part of Fact A.3 is similar to the proof of Fact A.2. □

Therefore, any model S of [[A]]<sub>Δ</sub> is a model of [[A<sup>σ<sup>‡</sup></sup>]]<sub>Δ</sub> with an appropriate base σ<sup>‡</sup>. The upper bound on predNo(Δ) is obtained by noticing that, for each predicate symbol A that occurs in Δ, we introduce at most relNo(Δ) · #A<sup>maxRelArity(Δ)</sup> ≤ relNo(Δ) · maxVars(Δ)<sup>maxRelArity(Δ)</sup> new predicate symbols. □

**A.2.** **Proof of Lemma 2.10.** The proof follows a generic guideline. First, recall that for any set of structures S we have

$$ \text{tw}(S) = \max_{S \in S} \text{tw}(S) = \max_{S \in S} \min\{\text{wd}(T) \mid T \text{ is a tree decomposition of } S\}. $$

Therefore, in order to prove an inequality of the form $\text{tw}([\phi^{\exists}]) \le \text{tw}([\psi^{\exists}]) + k$ for $\phi, \psi$ two qpf formulæ, we make use of the alternating max and min by proving the following:

for every structure S and store s such that S |=<sup>s</sup> φ
there exists a structure S' and a store s' such that S' |=<sup>s'</sup> ψ and
for every tree decomposition T' of S' there exists a tree decomposition T of S such that wd(T) ≤ wd(T') + k.
(1) The first point is immediate since $[(\phi * \mathbf{s}_{i=1}^k x_0 = x_i)^{\exists}] \subseteq [\phi^{\exists}]$.

(2) Since $[(\phi * \mathbf{s}_{i=1}^k x_0 \neq x_i)^{\exists}] \subseteq [\phi^{\exists}]$, we obtain immediately $\mathrm{tw}([[(\phi * \mathbf{s}_{i=1}^k x_0 \neq x_i)^{\exists}]]) \le \mathrm{tw}([\phi^{\exists}])$. For the reverse inequality, recall that $\phi * \mathbf{s}_{i=1}^k x_0 \neq x_i$ is satisfiable. Then $\phi$ must also be satisfiable, so let $S = (U, \sigma)$ be a model and $\mathfrak{s}$ a store such that $S \models^{\mathfrak{s}} \phi$. We distinguish two cases:

▷ if $\mathfrak{s}(x_0) \neq \mathfrak{s}(x_i)$ for all $i \in [1..k]$ then let $S' = S$, $\mathfrak{s}' = \mathfrak{s}$ hence $S' \models^{\mathfrak{s}'} \phi * \mathbf{s}_{i=1}^k x_0 \neq x_i$ and $\mathrm{tw}(S) = \mathrm{tw}(S')$.

▷ if $\mathfrak{s}(x_0) = \mathfrak{s}(x_i)$ for some $i \in [1..k]$ then let us consider a new fresh element $e \in U$ and define a new store $\mathfrak{s}'$ by $\mathfrak{s}'(y) \stackrel{\mathrm{def}}{=} e$ if $y \approx_{\phi} x_0$, and $\mathfrak{s}'(y) \stackrel{\mathrm{def}}{=} \mathfrak{s}(y)$ otherwise. We define the $S' = (U \cup \{e\}, \sigma')$ as follows. For every $\mathbf{r} \in \mathbb{R}$, for every tuple $\langle u_1, \dots, u_{\#\mathbf{r}} \rangle \in \sigma(\mathbf{r})$, there exists a unique relation atom $\mathbf{r}(y_1, \dots, y_{\#\mathbf{r}})$ occurring in $\phi$ such that $\mathfrak{s}(y_j) = u_j$ for all $j \in [1..\#\mathbf{r}]$. Then, add the tuple $(\mathfrak{s}'(y_1), \dots, \mathfrak{s}'(y_{\#\mathbf{r}}))$ to $\sigma'(\mathbf{r})$. By construction $S' \models^{\mathfrak{s}'} \phi * \mathbf{s}_{i=1}^k x_0 \neq x_i$. Let $T'$ be a tree decomposition of $S'$. We define $T$ by removing the element $e$ from $T'$ and adding $\mathfrak{s}(x_0)$ in every node of $T'$. $T$ is a tree decomposition of $S$ of width at most $\mathrm{wd}(T') + 1$. Therefore $\mathrm{wd}(T) \le \mathrm{wd}(T') + 1$, hence the result.

In both cases we obtain the expected result $\mathrm{tw}([\phi^{\exists}]) \le \mathrm{tw}([[(\phi * \mathbf{s}_{i=1}^k x_0 \neq x_i)^{\exists}]]) + 1$.

(3) We prove $\mathrm{tw}([[(\phi * \mathbf{r}(x_1, \dots, x_k))^{\exists}]] \le \mathrm{tw}([\phi^{\exists}]) + k$. Let $S = (U, \sigma)$ and $\mathfrak{s}$ such that $S \models^{\mathfrak{s}} \phi * \mathbf{r}(x_1, \dots, x_k)$. We define $S' = (U, \sigma')$ from $S$ by removing the tuple $\langle \mathfrak{s}(x_1), \dots, \mathfrak{s}(x_k) \rangle$ from $\sigma(\mathbf{r})$. Let $T'$ be a tree decomposition of $S'$. We define $T$ by adding the elements $\mathfrak{s}(x_1), \dots, \mathfrak{s}(x_k)$ to every node in $T'$. This construction does not break connectedness of the subtree of $T$ containing any element, $T$ still contains a node with all elements of any relation in $\sigma'$, and moreover (since $T'$ is not empty) $T$ contains a node (in fact all nodes) with elements $\mathfrak{s}(x_1), \dots, \mathfrak{s}(x_k)$ simultaneously. Therefore $T$ is a tree decomposition of $S$ of width at most $\mathrm{wd}(T') + k$.

We now prove that $\mathrm{tw}([\phi^{\exists}]) \le \mathrm{tw}([[(\phi * \mathbf{r}(x_1, \dots, x_k))^{\exists}]]) + 1$. Recall $\phi * \mathbf{r}(x_1, \dots, x_k)$ is satisfiable from the hypothesis. Let $S = (U, \sigma) \models^{\mathfrak{s}} \phi$, and we distinguish two cases:

▷ If $\langle \mathfrak{s}(x_1), \dots, \mathfrak{s}(x_k) \rangle \notin \sigma(\mathbf{r})$, then consider $\mathfrak{s}' = \mathfrak{s}$ and $S'$ obtained by adding the above tuple to $\sigma(\mathbf{r})$. Then $S' \models^{\mathfrak{s}'} \phi * \mathbf{r}(x_1, \dots, x_k)$ and for any tree decomposition $T'$ of $S'$ we have $T = T'$ is also a tree decomposition for $S$ hence ensuring $\mathrm{wd}(T) = \mathrm{wd}(T')$.

▷ If $\langle \mathfrak{s}(x_1), \dots, \mathfrak{s}(x_k) \rangle \in \sigma(\mathbf{r})$ then, because $\phi * \mathbf{r}(x_1, \dots, x_k)$ is satisfiable, there must exist variables $x'_1, \dots, x'_k$ and $j \in [1..k]$ such that $\mathbf{r}(x'_1, \dots, x'_k)$ occurs in $\phi$, $\mathfrak{s}(x_i) = \mathfrak{s}(x'_i)$, for every $i \in [1..k]$, and moreover $x_j \not\approx_{\phi} x'_j$. Let us consider a new fresh element $e \in U$ and define a new store $\mathfrak{s}'$ by $\mathfrak{s}'(y) = e$ if $y \approx_{\phi} x'_j$, and $\mathfrak{s}'(y) = \mathfrak{s}(y)$ otherwise. Let $S' = (U \cup \{e\}, \sigma')$ defined as follows. For every $\mathbf{r}' \in \mathbb{R}$, for every tuple $\langle u_1, \dots, u_{\#\mathbf{r}'} \rangle \in \sigma(\mathbf{r}')$, there exists a unique relation atom $\mathbf{r}'(y_1, \dots, y_{\#\mathbf{r}'})$ occurring in $\phi$ such that $\mathfrak{s}(y_j) = u_j$ for all $j \in [1..\#\mathbf{r}']$. Then, add the tuple $(\mathfrak{s}'(y_1), \dots, \mathfrak{s}'(y_{\#\mathbf{r}'}))$ to $\sigma'(\mathbf{r})$. Finally, add the tuple $\langle \mathfrak{s}'(x_1), \dots, \mathfrak{s}'(x_k) \rangle$ to $\sigma'(\mathbf{r})$. By construction $S' \models^{\mathfrak{s}'} \phi * \mathbf{r}(x_1, \dots, x_k)$. Let $T'$ be a tree decomposition of $S'$. We define $T$ by removing the element $e$ from $T'$ and adding $\mathfrak{s}(x'_j)$ in every node of $T'$. $T$ is a tree decomposition of $S$ of width at most $\mathrm{wd}(T') + 1$, that is, $\mathrm{wd}(T) \le \mathrm{wd}(T') + 1$.

In both cases we obtain the expected result, that is, $\mathrm{tw}([\phi^{\exists}]) \le \mathrm{tw}([[(\phi * \mathbf{r}(x_1, \dots, x_k))^{\exists}]]) + 1$.
(4) Similar to point (3), it generalizes the (right) inequality from formulæ consisting of a single relation atom to formulæ consisting of arbitrarily many relation atoms. $\square$
### A.3. Proof of Lemma 2.11.
Note that $fv(\eta) \subseteq F \subseteq fv(\phi)$ and henceforth, $fv(\phi * \eta) = fv(\phi)$. We follow a similar strategy as in the proof of Lemma 2.10. Consider a structure $S = (U, \sigma)$ and a store $s$, such that $S \models^s \phi * \eta$. We build a store $s'$ and a structure $S'$ such that $S' \models^{s'} \phi * \psi$ and $tw(S) \le tw(S') + card(F)$. First, consider a store $s''$, that is canonical for $\psi$ (Definition 3.1), and a structure $S'' = (U'', \sigma'')$, such that $S'' \models^{s''} \psi$. Such store and structure exist, because $\psi$ is satisfiable. Assume without loss of generality that $S''$ and $S$ are disjoint structures, that is, $s''(fv(\psi)) \cap s(fv(\phi)) = \emptyset$. Second, we define the store $s'$, as follows:

$$ s'(y) \stackrel{\text{def}}{=} \begin{cases} s''(y) & \text{if } y \in fv(\psi) \\ s''(y') & \text{if } y \in fv(\phi) \setminus fv(\psi) \text{ and there exists } y' \in F \text{ such that } y \approx_{\phi} y' \\ s(y) & \text{otherwise} \end{cases} $$

Note that the definition of $s'$ is consistent. In particular, for any $y \in fv(\phi) \setminus fv(\psi)$ there exists at most one variable $y' \in F$, such that $y \approx_{\phi} y'$, because otherwise, the hypothesis $x \not\approx_{\phi} y$ for all $x, y \in F$ would not hold. We build now the structure $S' = (U', \sigma')$ where $U' \stackrel{\text{def}}{=} U \cup U''$ and $\sigma'(r)$ is defined for every relation symbol $r \in \mathbb{R}$ as follows:

* add each tuple $\langle u_1, \dots, u_{\#r} \rangle \in \sigma''(r)$ to $\sigma'(r)$,

* for every tuple $\langle u_1, \dots, u_{\#r} \rangle \in \sigma(r)$, there exists a unique relation atom $r(y_1, \dots, y_{\#r})$ occurring in $\phi$, such that $s(y_i) = u_i$ for all $i \in [1..\#r]$; we add the tuple $\langle s'(y_1), \dots, s'(y_{\#r}) \rangle$ to $\sigma'(r)$.

* nothing else belongs to $\sigma'(r)$.

This construction guarantees that $S' \models^s \phi * \psi$. Equality and disequality atoms in $\phi * \psi$ are satisfied, by the definition of $s'$. With regard to relation atoms, notice that no tuple is added twice to $\sigma'(r)$ in the definition above. That is, if some $\langle s'(y_1), \dots, s'(y_{\#r}) \rangle$ obtained from $\sigma(r)$ exists also in $\sigma''(r)$, then $\phi * \psi$ would not be satisfiable. Let $T'$ be a tree decomposition of $S'$. We define a tree decomposition $T$ by:

* removing $\{s'(y) | y \in fv(\psi)\}$ from every bag of $T'$,

* adding $\{s(y) | y \in F\}$ to every bag of $T'$.

The result is a tree decomposition $T$ of $S$ of width $wd(T) \le wd(T') + card(F)$. Since the choice of $T'$ was arbitrary, we obtain $tw(S) \le tw(S') + card(F)$. Since the choice of $S$ was arbitrary, we obtain $tw(\llbracket (\phi * \eta)^3 \rrbracket) \le tw(\llbracket (\phi * \psi)^3 \rrbracket) + card(F)$. $\square$

## APPENDIX B. PROOFS FROM SECTION 3

### B.1. Proof of Lemma 3.24.
(1) “EF\*(split($S$)) $\subseteq$ split(EF\*(S))” By induction on the derivation of $S \in \text{EF\*(split}(S))$ from split($S$).

**Base case:** Let $S \in \text{split}(S)$. We have:

$$ \exists S' \in S. S \in \text{split}(S') \Rightarrow \exists S' \in \text{EF}^*(S). S \in \text{split}(S') \Rightarrow S \in \text{split}(\text{EF}^*(S)) $$

**Induction step:** Assume $S = (S_1 \bullet S_2)_{\approx}$ for some $S_1, S_2 \in \text{EF}^*(\text{split}(S))$ and $\approx$ satisfying the conditions of Definition 3.11 for external fusion of $S_1$ and $S_2$. Moreover, assume the induction hypothesis $S_1, S_2 \in \text{split}(\text{EF}^*(S))$. Then

$$ \begin{align*} S_1, S_2 \in \text{split}(\text{EF}^*(S)), S = (S_1 \bullet S_2)_{\approx} &\Rightarrow \\ (\exists S'_1, S'_2 \in \text{EF}^*(S). S_1 \sqsubseteq^{mc} S'_1, S_2 \sqsubseteq^{mc} S'_2), S = (S_1 \bullet S_2)_{\approx} &\Rightarrow \\ \exists S'_1, S'_2 \in \text{EF}^*(S). (\exists \approx'. S \sqsubseteq^{mc} (S'_1 \bullet S'_2)_{\approx'}) &\Rightarrow \end{align*} $$
$$ \exists S' \in \mathbf{EF}^*(S). S \sqsubseteq^{mc} S' \Rightarrow S \in \mathbf{split}(\mathbf{EF}^*(S)) $$

In the above, the equivalence $\approx'$ is taken as the extension by equality of $\approx$ and henceforth it satisfies the conditions of Definition 3.11 for external fusion of $S'_1, S'_2$.

"split(\mathbf{EF}^*(S)) \subseteq \mathbf{EF}^*(\mathbf{split}(S))" By induction on the derivation of $S' \in \mathbf{EF}^*(S)$ from $S$.

**Base case:** Let $S \in \mathbf{split}(S')$ for some $S' \in S$. We have:

$$ S \in \mathbf{split}(S') \Rightarrow S \in \mathbf{EF}^*(\mathbf{split}(S')) \Rightarrow S \in \mathbf{EF}^*(\mathbf{split}(S)) $$

**Induction step:** Assume $S \in \mathbf{split}(S')$ for some $S' = (S'_1 \bullet S'_2)_{\approx'}$ for some $S'_1, S'_2 \in \mathbf{EF}^*(S)$ and equivalence $\approx'$ satisfying the conditions of Definition 3.11 for external fusion of $S'_1, S'_2$.

Assume the induction hypothesis, that is, $\mathbf{split}(S'_1), \mathbf{split}(S'_2) \subseteq \mathbf{EF}^*(\mathbf{split}(S))$. Then:

$$ \mathbf{split}(S'_1), \mathbf{split}(S'_2) \subseteq \mathbf{EF}^*(\mathbf{split}(S)), S' = (S'_1 \bullet S'_2)_{\approx'}, S \in \mathbf{split}(S') \Rightarrow \\ \mathbf{split}(S'_1), \mathbf{split}(S'_2) \subseteq \mathbf{EF}^*(\mathbf{split}(S)), S' = (S'_1 \bullet S'_2)_{\approx'}, S \sqsubseteq^{mc} S' $$

We distinguish two sub-cases:

* $S$ is a maximally connected substructure of $S'_1$ (the case of $S'_2$ is symmetric) not affected by the external fusion defined by $\approx'$:

$$ \mathbf{split}(S'_1) \subseteq \mathbf{EF}^*(\mathbf{split}(S)), (\exists S_1. S_1 \sqsubseteq^{mc} S'_1, S = S_1) \Rightarrow \\ \mathbf{split}(S'_1) \subseteq \mathbf{EF}^*(\mathbf{split}(S)), S \in \mathbf{split}(S'_1) \Rightarrow S \in \mathbf{EF}^*(\mathbf{split}(S)) $$

* $S$ is a connected structure including several maximally connected substructures, at least one from each $S'_i$, for $i = 1, 2$:

$$ \mathbf{split}(S'_1), \mathbf{split}(S'_2) \subseteq \mathbf{EF}^*(\mathbf{split}(S)), \\ \exists k_1 \geq 1. \exists S_{1,1} \dots \exists S_{1,k_1}. S_{1,i} \sqsubseteq^{mc} S'_1 \text{ for all } i \in [1..k_1], \\ \exists k_2 \geq 1. \exists S_{2,1} \dots \exists S_{2,k_2}. S_{2,j} \sqsubseteq^{mc} S'_2 \text{ for all } j \in [1..k_2], \\ (\exists \approx . S = (S_{1,1} \bullet \dots \bullet S_{1,k_1} \bullet S_{2,1} \bullet \dots \bullet S_{2,k_2})_{\approx}), S \text{ connected} \Rightarrow \\ \mathbf{split}(S'_1), \mathbf{split}(S'_2) \subseteq \mathbf{EF}^*(\mathbf{split}(S)), \\ \exists k_1 \geq 1. \exists S_{1,1} \dots \exists S_{1,k_1}. S_{1,i} \in \mathbf{split}(S'_1) \text{ for all } i \in [1..k_1], \\ \exists k_2 \geq 1. \exists S_{2,1} \dots \exists S_{2,k_2}. S_{2,j} \in \mathbf{split}(S'_2) \text{ for all } j \in [1..k_2], \\ (\exists \approx . S = (S_{1,1} \bullet \dots \bullet S_{1,k_1} \bullet S_{2,1} \bullet \dots \bullet S_{2,k_2})_{\approx}), S \text{ connected} \Rightarrow \\ \exists k_1 \geq 1. \exists S_{1,1} \dots \exists S_{1,k_1}. S_{1,i} \in \mathbf{EF}^*(\mathbf{split}(S)) \text{ for all } i \in [1..k_1], \\ \exists k_2 \geq 1. \exists S_{2,1} \dots \exists S_{2,k_2}. S_{2,j} \in \mathbf{EF}^*(\mathbf{split}(S)) \text{ for all } j \in [1..k_2], \\ (\exists \approx . S = (S_{1,1} \bullet \dots \bullet S_{1,k_1} \bullet S_{2,1} \bullet \dots \bullet S_{2,k_2})_{\approx}), S \text{ connected} \Rightarrow S \in \mathbf{EF}^*(\mathbf{split}(S)) $$

In the above, the equivalence $\approx$ is the restriction of $\approx'$ to the substructures included in the composition. As $\approx'$ is conforming for external fusion of $S'_1, S'_2$ and since the resulting structure $S$ is connected, it is always possible to obtain $S$ as a sequence of external fusions conforming to Definition 3.11 from the respective substructures.

(2) "IEF*(split(S)) ⊆ split(IEF*(S))" By induction on the derivation of $S \in \mathbf{IEF}^*(\mathbf{split}(S))$ from split(S). The induction proceeds as for (1), with one additional case in the induction step.

**Induction step:** Let $S = (S_1)_{\approx}$ for some $S_1 \in \mathbf{IEF}^*(\mathbf{split}(S))$ and equivalence relation $\approx$ conforming to internal fusion of $S_1$. Moreover, assume the induction hypothesis $S_1 \in$
split(IEF*(S)). Then

$$
\begin{align*}
S_1 \in \operatorname{split}(\operatorname{IEF}^*(S)), S = (S_1)_{/\approx} &\Rightarrow \\
(\exists S'_1 \in \operatorname{IEF}^*(S). S_1 \sqsubseteq^{mc} S'_1), S = (S_1)_{/\approx} &\Rightarrow \\
\exists S'_1 \in \operatorname{IEF}^*(S). (\exists \approx' . S \sqsubseteq^{mc} (S'_1)_{/\approx'}) &\Rightarrow \\
\exists S' \in \operatorname{IEF}^*(S), S \sqsubseteq^{mc} S' &\Rightarrow S \in \operatorname{split}(\operatorname{IEF}^*(S))
\end{align*}
$$

In the above, the equivalence $\approx'$ is taken as the extension by equality of $\approx$ and hence conforming for internal fusion of structure $S'_1$.

"split(IEF*(S)) ⊆ IEF*(split(S))" By induction on the derivation of $S' \in IEF^*(S)$ from S.
The induction proceeds as for (1), with one additional case in the induction step.

Induction step: Let $S \in \mathbf{split}(S')$ for some $S' = (S'_1)_{/\approx'}$ for some $S'_1 \in \mathbf{IEF}^*(S)$ and equivalence $\approx'$ conforming for internal fusion of $S'_1$. Moreover, assume the induction hypothesis $\mathbf{split}(S'_1) \subseteq \mathbf{IEF}^*(\mathbf{split}(S))$. Then

$$
\begin{align*}
\mathbf{split}(S'_1) \subseteq \mathbf{IEF}^*(\mathbf{split}(S)), S' = (S'_1)_{/\approx'}, S \in \mathbf{split}(S') &\Rightarrow \\
\mathbf{split}(S'_1) \subseteq \mathbf{IEF}^*(\mathbf{split}(S)), S' = (S'_1)_{/\approx'}, S \sqsubseteq^{mc} S' &\Rightarrow \\
\mathbf{split}(S'_1) \subseteq \mathbf{IEF}^*(\mathbf{split}(S)), & \\
\exists k \ge 1. \exists S_{1,1} \dots \exists S_{1,k}. S_{1,i} \sqsubseteq^{mc} S'_1 \text{ for all } i \in [1..k], & \\
(\exists \approx . S = (S_{1,1} \bullet \dots \bullet S_{1,k})_{/\approx}, \text{ S connected}) &\Rightarrow \\
\mathbf{split}(S'_1) \subseteq \mathbf{IEF}^*(\mathbf{split}(S)), & \\
\exists k \ge 1. \exists S_{1,1} \dots \exists S_{1,k}. S_{1,i} \in \mathbf{split}(S'_1) \text{ for all } i \in [1..k], & \\
(\exists \approx . S = (S_{1,1} \bullet \dots \bullet S_{1,k})_{/\approx}, \text{ S connected}) &\Rightarrow \\
\exists k \ge 1. \exists S_{1,1} \dots \exists S_{1,k}. S_{1,i} \in \mathbf{IEF}^*(\mathbf{split}(S)) \text{ for all } i \in [1..k], & \\
(\exists \approx . S = (S_{1,1} \bullet \dots \bullet S_{1,k})_{/\approx}, \text{ S connected}) &\Rightarrow S \in \mathbf{IEF}^*(\mathbf{split}(S))
\end{align*}
$$

In the above, the equivalence $\approx$ is taken as the restriction of $\approx'$ to the maximal connected substructures included in the construction of connected S. Henceforth, $\approx$ is conforming for internal fusion as well. As the resulting structure S is connected, it is always possible to construct it in $IEF^*(\mathbf{split}(S))$ i.e., first by using external fusion conforming to Definition 3.11 to connect all the included substructures and second, by using internal fusion to further restrict the result if needed. $\square$

B.2. **Proof of Lemma 3.31.** “$\mathbf{split}(\llbracket \Delta \rrbracket_A^c) \subseteq \llbracket \Gamma \rrbracket_P^c$” We prove first the following fact:

**Fact B.1.** Let $B_0(x_1, \dots, x_{\#B_0}) \Rightarrow^*_{\Delta} \exists y_1 \dots \exists y_n \cdot \phi$ be a complete $\Delta$-unfolding, where $\phi$ is a qpf formula, $s$ a store injective over $\{x_1, \dots, x_{\#B_0}\} \cup \{y_1, \dots, y_n\}$, $S = (U, \sigma)$ a structure such that $S \models^s \phi$ and $S' = (U', \sigma')$ a structure, such that $S' \sqsubseteq^{mc} S$ and $\text{supp}(\sigma') \cap \{s(x_1), \dots, s(x_{\#B_0})\} \neq \emptyset$. Then, there exist a nonempty set $J_0 \subseteq [1..\#B_0]$, equivalence relation $\xi_0 \subseteq J_0 \times J_0$ and complete $\Gamma$-unfolding $B_0(x_1, \dots, x_{\#B_0})/\xi_0 \Rightarrow^*_{\Gamma} \exists y_1 \dots \exists y_n \cdot \phi'$, where $\phi'$ is a qpf formula, such that $S' \models^s \phi'$.

*Proof.* By induction on the length of the $\Delta$-unfolding. Assume the first rule in this unfolding to be of the form (3.1), for a qpf formula $\psi_0$. Then, there exist:

▷ unfoldings $B_i(x_1, \dots, x_{\#B_i}) \Rightarrow^*_{\Delta} \exists y_{j_{i,1}} \dots \exists y_{j_{i,k_i}} \cdot \phi_i$, where $y_{j_{i,1}}, \dots, y_{j_{i,k_i}} \in \{y_1, \dots, y_n\}$ and $\phi_i$ are qpf formulæ, for all $i \in [1..\ell]$, and
▷ structures $S_0 = (U_0, \sigma_0), \dots, S_\ell = (U_\ell, \sigma_\ell)$, such that $S_0 \bullet \dots \bullet S_\ell = S$, $S_0 \models^s \psi_0$ and $S_i \models^s \phi_i \theta_i$, where $\theta_i \stackrel{\text{def}}{=} [x_1/z_{i,1}, \dots, x_{\#B_i}/z_{i,\#B_i}]$, for all $i \in [1..\ell]$.

Since $S' \sqsubseteq^{mc} S_0 \bullet \dots \bullet S_\ell$ is a maximally connected structure, there must exist structures $S'_0 = (U_0, \sigma'_0)$, $S'_{i_1} = (U_{i_1}, \sigma'_{i_1})$, \dots, $S'_{i_k} = (U_{i_k}, \sigma'_{i_k})$, for $i_1, \dots, i_k \in [1..\ell]$, such that:

▷ $S' = S'_0 \bullet S'_{i_1} \bullet \dots \bullet S'_{i_k}$,

▷ $\text{supp}(\sigma'_{i_h}) \cap \{\mathfrak{s}(z_{i_h,1}), \dots, \mathfrak{s}(z_{i_m,\#B_{i_h}})\} \neq \emptyset$ and $S'_{i_h} \sqsubseteq^{mc} S_{i_h}$, for all $h \in [1..k]$,

▷ $\text{supp}(\sigma') \cap \{\mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,\#B_i})\} = \emptyset$, for all $i \in [1..\ell] \setminus \{i_1, \dots, i_k\}$.

Since $S_{i_h} \models^s \phi_{i_h} \theta_{i_h}$, we have $S_{i_h} \models^{s\circ\theta_{i_h}^{-1}} \phi_{i_h}$, for all $h \in [1..k]$. By the inductive hypothesis, there exist nonempty sets $J_{i_1} \subseteq [1..\#B_{i_1}]$, \dots, $J_{i_k} \subseteq [1..\#B_{i_k}]$, equivalence relations $\xi_{i_1} \subseteq J_{i_1} \times J_{i_1}, \dots, \xi_{i_k} \subseteq J_{i_k} \times J_{i_k}$ and complete $\Gamma$-unfoldings:

$$ \mathbf{B}_{i_h}(x_1, \dots, x_{\#\mathbf{B}_{i_h}})/\xi_{i_h} \Rightarrow_{\Gamma}^{*} \exists y_{j_{i_h,1}} \dots \exists y_{j_{i_h,k_{i_h}}} \cdot \phi'_{i_h} $$

such that $S'_{i_h} \models^{s\circ\theta_{i_h}^{-1}} \phi'_{i_h}$, for all $h \in [1..k]$. Then, we define:

▷ sets $\bar{J}_{i_h} \stackrel{\text{def}}{=} [1..\#B_i] \setminus J_{i_h}$, for all $h \in [1..k]$,

▷ qpf formulæ $\psi'_0$ and $\psi''_0$ satisfying points (1) and (2) from the construction of $\Gamma$,

▷ an equivalence relation $\Xi \stackrel{\text{def}}{=} (\text{conn}(\psi'_0) \cup \bigcup_{h=1}^k \xi_{i_h} (\mathbf{B}_{i_h} (z_{i_h,1}, \dots, z_{i_h,\#B_{i_h}})))^\perp$.

We argue that the construction of the formulæ $\psi'_0$ and $\psi''_0$ is effective. There are no (dis-) equalities in $\Delta$, i.e., $\psi'_0$ consists of relation atoms only. Each atom $\alpha$ of $\psi'_0$, such that $\text{fv}(\alpha) \cap \text{fv}_{\bar{J}_{i_h}} (\mathbf{B}_{i_h} (z_{i_h,1}, \dots, z_{i_h,\#B_{i_h}})) \neq \emptyset$, for some $h \in [1..k]$, is added to $\psi'_0$. Moreover, each atom $\alpha$ of $\psi'_0$, such that $\text{fv}(\alpha) \cap \text{fv}_{\bar{J}_{i_h}} (\mathbf{B}_{i_h} (z_{i_h,1}, \dots, z_{i_h,\#B_{i_h}})) = \emptyset$, for all $h \in [1..k]$ is added to $\psi''_0$. Note that, each atom can only be added either to $\psi'_0$ or $\psi''_0$ but not to both, because $S'_{i_h} \sqsubseteq^{mc} S_{i_h}$ and $S'_{i_h} \models^s \phi'_{i_h}$ imply that no further element can be added to $S'_{i_h}$, for all $h \in [1..k]$. The rest of the atoms $\alpha$ from $\psi'_0$, i.e., such that $\text{fv}(\alpha) \cap \text{fv}_{\bar{J}_{i_h}} (\mathbf{B}_{i_h} (z_{i_h,1}, \dots, z_{i_h,\#B_{i_h}})) = \emptyset$ and $\text{fv}(\alpha) \cap \text{fv}_{\bar{J}_{i_h}} (\mathbf{B}_{i_h} (z_{i_h,1}, \dots, z_{i_h,\#B_{i_h}})) = \emptyset$, for all $h \in [1..k]$, are split between $\psi'_0$ and $\psi''_0$, by repeating the following steps until a fixpoint is reached:

▷ if $\text{fv}(\alpha) \cap \text{fv}(\psi'_0) \neq \emptyset$, then update $\psi'_0$ as $\psi'_0 * \alpha$,

▷ else, update $\psi''_0$ as $\psi''_0 * \alpha$.

By construction, we obtain that $\text{fv}(\psi'_0) \cap \text{fv}(\psi''_0) = \emptyset$, as required at point (1).

Let $J_0 \stackrel{\text{def}}{=} \{j \in [1..\#B_0] \mid \mathfrak{s}(x_j) \in \text{supp}(\sigma')\}$. Note that $J_0 \neq \emptyset$ because $\text{supp}(\sigma') \cap \{\mathfrak{s}(x_1), \dots, \mathfrak{s}(x_{\#B_0})\} \neq \emptyset$. We define the equivalence relation $\xi_0 \subseteq J_0 \times J_0$ as follows:

$$ (i, j) \in \xi_0 \iff (x_i, x_j) \in \Xi $$

Moreover, one can show that $S'_0 \models^s \psi'_0$, by the construction of $\psi'_0$ and $\psi''_0$, hence $\xi_0$ satisfies the conditions (4)–(7) from the definition of $\Gamma$, hence $\Gamma$ contains a rule of the form (3.2), with qpf formula $\psi'_0$. Since $S' \models^s \psi'_0 * \mathbf{S}^k_{h=1} \phi'_{i_h} \theta_h$ and $\phi' = \psi'_0 * \mathbf{S}^k_{h=1} \phi'_{i_h} \theta_h$ modulo a reordering of atoms, we obtain that $S' \models^s \phi'$.

The proof is completed as follows. Let $S' \in \text{split}([\mathbf{A}]^c_\Delta)$ be a maximally connected substructure of a canonical model $S \in [\mathbf{A}]^c_\Delta$. Then, there exists a complete $\Delta$-unfolding $A \Rightarrow^* \Delta \exists y_1 \dots \exists y_m \cdot \bar{\phi}$ and a store $\mathfrak{s}$, injective over $y_1, \dots, y_m$, such that $S \models^s \bar{\phi}$. Because $S'$ is connected, there exists a unique (i) predicate atom $B_0(z_1, \dots, z_{\#B_0})$, (ii) subformula $\phi$ of $\bar{\phi}$ and (iii) structure $S'' \sqsubseteq S$, such that $B_0(z_1, \dots, z_{\#B_0}) \Rightarrow^* \Delta \exists y_{i_1} \dots \exists y_{i_n} \cdot \phi$ is a complete unfolding, $\text{supp}(S'') \cap \{\mathfrak{s}(z_1), \dots, \mathfrak{s}(z_{\#B_0})\} = \emptyset$, $S'' \models^s \phi$ and $S' \sqsubseteq^{mc} S''$. Without losing generality, we assume that the above is the smallest $\Delta$-unfolding with these properties
and assume that the first rule of the Δ-unfolding is of the form (3.1), with a qpf formula $\psi$. Then, because $S'$ is connected, the right-hand side of this rule contains zero or more predicate atoms $B_{i_h}(z_{i_h,1}, \dots, z_{i_h, \#B_{i_h}})$, for $i_h \in \{i_1, \dots, i_k\} \subseteq [1..\ell]$, such that $\text{supp}(\sigma') \cap \{\mathfrak{s}(z_{i_h,1}), \dots, \mathfrak{s}(z_{i_h, \#B_{i_h}})\} \neq \emptyset$. Accordingly, we decompose $S'' = S_0'' \bullet \dots \bullet S_k''$ such that $S_0'' \models^s \psi_0$ and $S_h'' \models^s \phi_h$, where $B_{i_h}(z_{i_h,1}, \dots, z_{i_h, \#B_{i_h}}) \stackrel{*}{\Rightarrow}_{\Delta} \exists y_{j_{h,1}} \dots \exists y_{j_{h,m_h}}$. $\phi_h$ are complete unfoldings, for all $h \in [1..k]$. This decomposition of $S''$ induces a decomposition of $S' \subseteq^m S''$ as $S_0' \bullet \dots \bullet S_k' = S'$ such that $S_h' \subseteq^m S_h''$ and $\text{supp}(\sigma_h') \cap \{\mathfrak{s}(z_{i_h,1}), \dots, \mathfrak{s}(z_{i_h, \#B_{i_h}})\} \neq \emptyset$, for all $h \in [1..k]$. Applying Fact B.1, we find nonempty subsets $J_h \subseteq [1..\#B_{i_h}]$, equivalence relations $\xi_h \subseteq J_h \times J_h$ and complete $\Gamma$-unfoldings $B_{i_h}(z_{i_h,1}, \dots, z_{i_h, \#B_{i_h}})/\xi_h \stackrel{*}{\Rightarrow}_{\Gamma} \exists y_{p_{h,1}} \dots \exists y_{p_{h,n_h}}$. $\phi_h'$, such that $S_h' \models^s \phi_h'$, for all $h \in [1..k]$. We define the sets $\bar{J}_h = [1..\#B_{i_h}] \setminus J_h$ and the formulæ $\psi_0'$ and $\psi_0''$ such that conditions (1) and (2) are met. Let $\Xi \stackrel{\text{def}}{=} (\text{conn}(\psi_0') \cup \bigcup_{h=1}^k \xi_{i_h}(B_{i_h}(z_{i_h,1}, \dots, z_{i_h, \#B_{i_h}})))^c$ be an equivalence relation. Since $S'$ is connected, we argue that $\Xi$ has a single equivalence class. Moreover, $(z, z) \notin \Xi$, for all $z \in \{z_1, \dots, z_{\#B_0}\}$, since $\text{supp}(S'') \cap \{\mathfrak{s}(z_1), \dots, \mathfrak{s}(z_{\#B_0})\} = \emptyset$ and $\mathfrak{s}$ is injective. Then, by definition, $\Gamma$ contains a rule of the form (3.3). This rule and the complete unfoldings $B_{i_h}(z_{i_h,1}, \dots, z_{i_h, \#B_{i_h}}) \stackrel{*}{\Rightarrow}_{\Gamma} \exists y_{j_{h,1}} \dots \exists y_{j_{h,m_h}}$. $\phi_h'$, for all $h \in [1..k]$, are composed to make up a complete $\Gamma$-unfolding $\mathbf{P} \stackrel{\Gamma}{\Rightarrow} \exists y_{q_1} \dots \exists y_{q_r}$. $\psi_0' * \mathbf{P}^k \stackrel{*}{\Rightarrow} \phi_h'$, such that $S' \models^s \psi_0' * \mathbf{P}^k \stackrel{*}{\Rightarrow} \phi_h'$. Since $y_{q_1}, \dots, y_{q_r} \in \{y_1, \dots, y_m\}$ and $\mathfrak{s}$ is injective over $y_1, \dots, y_m$, we obtain that $S' \in [\mathbf{P}]^c_{\Gamma}$.

"$[\Gamma]^c_{\mathbf{P}} \subseteq \text{split}([\Delta]^c_{\mathbf{A}})$" We prove first two related facts. First, let $B_0(x_1, \dots, x_{\#B_0})/\xi_0 \stackrel{*}{\Rightarrow}_{\Gamma} \exists y_1 \dots \exists y_n$. $\phi$ be a complete $\Gamma$-unfolding, where $\phi$ is a qpf formula, $J_0 \subseteq [1..\#B_0]$ a nonempty set and $\xi_0 \subseteq J_0 \times J_0$ an equivalence relation, $\mathfrak{s}$ be a store injective over $\{x_1, \dots, x_{\#B_0}\} \cup \{y_1, \dots, y_n\}$ and $\mathbf{S} = (\mathbf{U}, \sigma)$ be a structure such that $\mathbf{S} \models^s \phi$. Given an equivalence class $I \subseteq J_0$ of $\xi_0$, we define the structure:

$\text{reach}^s_I(I) \stackrel{\text{def}}{=} (\mathbf{U}, \lambda\mathbf{r} . \{\langle u_1, \dots, u_{\#\mathbf{r}} \rangle \in \sigma(\mathbf{r}) \mid \forall j \in [1..\#\mathbf{r}] \exists i \in I . \mathfrak{s}(x_i) \text{ connected to } u_j \text{ in } \mathbf{S}\})$

**Fact B.2.** $\text{reach}^s_I(I) \subseteq^m \mathbf{S}$.

*Proof.* By induction on the length of the $\Gamma$-unfolding. Assume that the first rule of the unfolding is of the form (3.2), with a qpf formula $\psi_0$. Then, there exist nonempty sets $J_{i_h} \subseteq [1..\#B_{i_h}]$ and equivalence relations $\xi_{i_h} \subseteq J_{i_h} \times J_{i_h}$, for some $i_1, \dots, i_k \in [1..\ell]$ and all $h \in [1..k]$ and an equivalence relation $\Xi \subseteq (\{x_1, \dots, x_{\#B_0}\} \cup \{y_1, \dots, y_m\}) \times (\{x_1, \dots, x_{\#B_0}\} \cup \{y_1, \dots, y_m\})$, that satisfy points (1)–(7) from the definition of $\Gamma$. By point (7), $\{x_i \mid i \in I\}$ is an equivalence class of $\Xi|_{\{x_1, \dots, x_{\#B_0}\}}$ and let $X \subseteq \text{fv}(\psi_0') \cup \bigcup_{h=1}^k \{z_{i_h,1}, \dots, z_{i_h, \#B_{i_h}}\}$ be the unique equivalence class of $\Xi$ that contains it. For each $h \in [1..k]$, let $I_h \subseteq [1..\#B_{i_h}]$ be the equivalence class of $\xi_{i_h}$ used to define $X$ (3).

Let $B_{i_h}(x_1, \dots, x_{\#B_{i_h}}) \stackrel{*}{\Rightarrow}_{\Gamma} \exists y_{j_{h,1}} \dots \exists y_{j_{h,m_h}}$. $\phi_h$ be complete $\Gamma$-unfoldings, such that $\phi = \psi_0' * \mathbf{P}^k \stackrel{*}{\Rightarrow} \phi_h \theta_h$, where $\theta_h \stackrel{\text{def}}{=} [x_1/z_{i_h,1}, \dots, x_{\#B_{i_h}}/z_{i_h, \#B_{i_h}}]$, for each $h \in [1..k]$. Since $\mathbf{S} \models^s \phi$, there exist structures $\mathbf{S}_0 = (\mathbf{U}_0, \sigma_0), \dots, \mathbf{S}_k = (\mathbf{U}_k, \sigma_k)$ such that $\mathbf{S}_0 \models^s \psi_0'$ and $\mathbf{S}_h \models^s \phi_h \theta_h$, or equivalently, $\mathbf{S}_h \models^{s\circ\theta_h^{-1}} \phi_h$ for all $h \in [1..k]$. By the inductive hypothesis, we have $\text{reach}_{\mathbf{S}_h}^{s\circ\theta_h^{-1}}(I_h) \subseteq^m \mathbf{S}_h$, for all $h \in [1..k]$. Since $X$ is an equivalence class of $\Xi$, by point (3) of the definition of $\Gamma$, we obtain that $\text{reach}_{\mathbf{S}_h}^s(I) \subseteq^m \mathbf{S}$. $\square$

Second, let $B_0(x_1, \dots, x_{\#B_0}) \stackrel{*}{\Rightarrow}_{\Delta} \exists y_1 \dots \exists y_m$. $\phi'$ be the complete $\Delta$-unfolding obtained by replacing each rule of the form (3.2) with its corresponding rule (3.1) in the above
Γ-unfolding, such that $\phi'$ is a qpf formula and $y_1, \dots, y_n \in \{y_1, \dots, y_m\}$. Note that the latter can be assumed w.l.o.g., if necessary, by a renaming of the quantified variables.

**Fact B.3.** There exists a store $\mathfrak{s}'$, that is injective over $y_1, \dots, y_m$ and agrees with $\mathfrak{s}$ over $y_1, \dots, y_n$, and a structure $\mathfrak{S}' = (\mathcal{U}, \sigma')$, such that $\mathfrak{S}' \models^{\mathfrak{s}'} \phi'$ and $\mathrm{reach}_{\mathfrak{S}}^{\mathfrak{s}}(I) \sqsubseteq^{\mathrm{mc}} \mathfrak{S}'$, for each equivalence class $I \subseteq J_0$ of $\xi_0$.

*Proof.* The store $\mathfrak{s}'$ is defined as:

$\triangleright \mathfrak{s}'(y_i) = \mathfrak{s}(y_i)$, for each $i \in [1..n]$,

$\triangleright \mathfrak{s}'(y_i)$ is chosen from $\mathcal{U} \setminus \{\mathfrak{s}(y_1), \dots, \mathfrak{s}(y_n)\}$ such that, moreover, $\mathfrak{s}'(y_i) \neq \mathfrak{s}'(y_j)$, for all $n+1 \le i < j \le m$.

Note that $\mathfrak{s}'$ can be built, because $\mathcal{U}$ is infinite. Because of the assumption that each predicate defined by a rule from $\Delta$ occurs on some complete $\Delta$-unfolding of $\mathcal{A}$, there exists a complete $\Delta$-unfolding:

$$ \mathcal{A} \Rightarrow_{\Delta} \dots \Rightarrow_{\Delta} \mathcal{B}_0(z_1, \dots, z_{\#\mathcal{B}_0}) * \phi'' \Rightarrow_{\Delta} (\exists y_1 \dots \exists y_m \cdot \phi') [x_1/z_1, \dots, x_{\#\mathcal{B}_0}/z_{\#\mathcal{B}_0}] * \phi'' $$

where $\phi''$ is a predicate-free formula, possibly containing existential quantifiers. Since every complete $\Delta$-unfolding of $\mathcal{A}$ yields a satisfiable formula, there exists a store $\mathfrak{s}''$ that agrees with $\mathfrak{s}' \circ [z_1/x_1, \dots, z_{\#\mathcal{B}_0}/x_{\#\mathcal{B}_0}]$ over $y_1, \dots, y_m$ and a structure $\mathfrak{S}'$, such that:

$$ \mathfrak{S}'' \models^{\mathfrak{s}''} (\exists y_1 \dots \exists y_m \cdot \phi') [x_1/z_1, \dots, x_{\#\mathcal{B}_0}/z_{\#\mathcal{B}_0}] * \phi'' $$

Note that, in the above construction, we have taken $\mathfrak{s}''$ to agree with $\mathfrak{s}'$ over $y_1, \dots, y_m$. This is possible because there are no (dis-)equalities in $\Delta$ and the set of models of a qpf formula is closed under isomorphism-preserving renaming of elements.

Let $\mathfrak{S}'$ and $\mathfrak{S}'''$ be structures such that $\mathfrak{S}'' = \mathfrak{S}' \bullet \mathfrak{S}''$, $\mathfrak{S}' \models^{\mathfrak{s}''} \phi'[x_1/z_1, \dots, x_{\#\mathcal{B}_0}/z_{\#\mathcal{B}_0}]$, or equivalently $\mathfrak{S}' \models^{\mathfrak{s}'} \phi'$, and $\mathfrak{S}''' \models^{\mathfrak{s}''} \phi''$. By induction on the length of the $\Delta$-unfolding, relying on by point (1) of the definition of $\Gamma$, one can prove that $\phi' = \phi * \bar{\phi}$, where $\bar{\phi}$ is a qpf formula, such that $\mathrm{fv}(\phi) \cap \mathrm{fv}(\bar{\phi}) = \emptyset$. Since $\mathfrak{S}' \models^{\mathfrak{s}'} \phi'$, there exists a structure $\bar{\mathcal{S}} = (\mathcal{U}, \bar{\sigma})$, such that $\mathfrak{S}' = \mathcal{S} \bullet \bar{\mathcal{S}}$. Moreover, since $\mathfrak{s}'$ is injective over $y_1, \dots, y_m$, by construction, we obtain $\mathrm{supp}(\sigma) \cap \mathrm{supp}(\bar{\sigma}) = \emptyset$. Let $I \subseteq J_0$ be an equivalence class of $\xi_0$. By Fact B.2, we have $\mathrm{reach}_{\mathfrak{S}}^{\mathfrak{s}}(I) \sqsubseteq^{\mathrm{mc}} \mathfrak{S}$. Since $\mathfrak{S}' = \mathcal{S} \bullet \bar{\mathcal{S}}$ and $\mathrm{supp}(\sigma) \cap \mathrm{supp}(\bar{\sigma}) = \emptyset$, we obtain $\mathrm{reach}_{\mathfrak{S}}^{\mathfrak{s}}(I) \sqsubseteq^{\mathrm{mc}} \mathfrak{S}'$. $\square$

The proof is completed as follows. Let $\mathcal{S} \in [\mathbb{P}]_{\Gamma}^c$ be a canonical $\Gamma$-model of $\mathcal{P}$, i.e., there exists a complete $\Gamma$-unfolding $\mathcal{P} \Rightarrow_{\Gamma}^* \exists y_1 \dots \exists y_n \cdot \phi$, where $\phi$ is a qpf formula, and a store $\mathfrak{s}$ injective over $y_1, \dots, y_n$ such that $\mathcal{S} \models^{\mathfrak{s}} \phi$. By the definition of $\Gamma$, the first rule of this unfolding is of the form (3.3), with a qpf formula $\psi_0$. Then there exist $\Gamma$-unfoldings $\mathcal{B}_i(x_1, \dots, x_{\#\mathcal{B}_i}) / \xi_i \Rightarrow_{\Gamma}^* \exists y_{j_{i,1}} \dots \exists y_{j_{i,m_i}} \cdot \phi_i$, for some sets $J_i \subseteq [1..\#\mathcal{B}_i]$ and equivalence relations $\xi_i \subseteq J_i \times J_i$, for $i \in [1..\ell]$, such that:

$$ \phi = \psi_0 * \mathfrak{s}^*_{i \in [1..\ell], J_i \neq \emptyset} \phi_i \theta_i $$

where $\theta_i \stackrel{\mathrm{def}}{=} [x_1/z_{i,1}, \dots, x_{\#\mathcal{B}_i}/z_{i,\#\mathcal{B}_i}]$, $i \in [1..\ell]$. Let $\{i_1, \dots, i_k\} \stackrel{\mathrm{def}}{=} \{i \in [1..\ell] \mid J_i \neq \emptyset\}$. Then, there exist structures $\mathcal{S}_0 \bullet \dots \bullet \mathcal{S}_k = \mathcal{S}$, such that $\mathcal{S}_0 \models^{\mathfrak{s}} \psi_0$ and $\mathcal{S}_j \models^{\mathfrak{s}} \phi_{i_j} \theta_{i_j}$, for $i \in [1..\ell]$. By the definition of $\Gamma$, there exists a complete $\Delta$-unfolding:

$$ \begin{align*} \mathcal{B}_0(x_1, \dots, x_{\#\mathcal{B}_0}) &\Rightarrow_{\Delta} \exists y_1 \dots \exists y_m \cdot \psi_0' * \mathfrak{s}^*_{i=1} \mathcal{B}_i(z_{i,1}, \dots, z_{i,\#\mathcal{B}_i}) \Rightarrow_{\Delta} \dots \\ &\Rightarrow_{\Delta}^* \exists y_1 \dots \exists y_p \cdot \psi_0' * \mathfrak{s}^k_{j=1} \phi'_{i_j} \theta_{i_j} * \eta \end{align*} $$
for qpf formulæ $\psi'_0, \phi'_{i_1}, \dots, \phi'_{i_k}$ and predicate-free formula $\eta$. Consider the equivalence relation $\Xi$ over $\{x_1, \dots, x_{\#B_0}\} \cup \{y_1, \dots, y_m\}$ defined as:

$$ \Xi \stackrel{\text{def}}{=} (\text{conn}(\psi_0) \cup \bigcup_{j=1}^k \xi_{ij} (\mathbf{B}_{ij}(z_{ij,1}, \dots, z_{ij,\#\mathbf{B}_{ij}})))^= $$

By point (8), $\Xi$ has a single equivalence class $X$ such that:

$$ \triangleright X \cap \{x_1, \dots, x_{\#B_0}\} = \emptyset, $$

the sets $I_j \stackrel{\text{def}}{=} \{h \in [1..\#B_{ij}] | z_{ij,h} \in X\}$ are unions of equivalence classes of $\xi_{ij}$, namely $I_j = I_{j,1} \uplus \dots \uplus I_{j,q_j}$, where $I_{j,h}$ are equivalence classes of $\xi_i$, for all $j \in [1..k]$.

By Fact B.3, there exist a store $\mathfrak{s}'$, that is injective over $y_1, \dots, y_p$ and agrees with $\mathfrak{s}$ over $y_1, \dots, y_n$, and structures $S'_0, \dots, S'_k$, such that $S'_j \models^{\mathfrak{s}'} \phi_j$ and reach$\mathfrak{s}'_j(I_{j,h}) \sqsubseteq^{\text{mc}} S'_j$, for all $j \in [1..k]$ and $h \in [1..q_j]$. We argue that $S_j = \bullet_{h=1}^{q_j} \text{reach}_{\mathfrak{s}'_j}(I_{j,h}) \sqsubseteq^{\text{mc}} S'_j$. Moreover, since $\mathfrak{s}'$ is injective over $y_1, \dots, y_n$, one can build a structure $S'_0$, such that $S'_0 \models^{\mathfrak{s}'} \psi'_0$. We define $S' \stackrel{\text{def}}{=} S'_0 \bullet \bullet_{j=1}^k S'_j$. Thus, we have $S \sqsubseteq^{\text{mc}} S'$ and we are left with showing that $S'$ can be embedded in a canonical $\Delta$-model of $A$.

By the assumption that each predicate defined by $\Delta$ occurs on some complete $\Delta$-unfolding of $A$, there exists another complete $\Delta$-unfolding:

$$ \begin{align*} A &\Rightarrow_{\Delta} \dots \Rightarrow_{\Delta} \mathbf{B}_0(z_{0,1}, \dots, z_{0,\#\mathbf{B}_0}) * \zeta \\ &\Rightarrow_{\Delta} (\exists y_1 \dots \exists y_p . \psi_0 * \mathfrak{s}^\ell_{i=1} \mathbf{B}_i(z_{i,1}, \dots, z_{i,\#\mathbf{B}_i}) [x_1/z_{0,1}, \dots, x_{\#\mathbf{B}_0}/z_{0,\#\mathbf{B}_0}] * \zeta \\ &\Rightarrow_{\Delta} \dots \Rightarrow_{\Delta} (\exists y_1 \dots \exists y_n . \psi'_0 * \mathfrak{s}^k_{i=1} \phi'_i \theta_i * \eta) [x_1/z_{0,1}, \dots, x_{\#\mathbf{B}_0}/z_{0,\#\mathbf{B}_0}] * \zeta \end{align*} $$

for some predicate-free formula $\zeta \stackrel{\text{def}}{=} \exists y_{n+1} \dots \exists y_p . \eta$, for some variables $y_{n+1}, \dots, y_p$, such that $\{y_{n+1}, \dots, y_p\} \cap \{y_1, \dots, y_n\} = \emptyset$ and a qpf formula $\eta$. Since this latter $\Delta$-unfolding yields a satisfiable formula, there exists a structure $S''$ and a store $\mathfrak{s}''$, injective over $y_1, \dots, y_p$, that agrees with $\mathfrak{s}'$ over $y_1, \dots, y_n$, such that $S'' \models^{\mathfrak{s}''} \eta$. Then, $S' \bullet S'' \in [[A]]^c_\Delta$ and, since $S \sqsubseteq^{\text{mc}} S'$, we obtain $S \sqsubseteq^{\text{mc}} S' \bullet S''$, leading to $S \in \text{split}([A]^c_\Delta)$. $\square$

B.3. **Proof of Lemma 3.32.** Without loss of generality, we can consider that $\Gamma$ is equality-free (Lemma 2.6) and all-satisfiable for $P$ (Lemma 2.9).

”($[P]^c_\Gamma \sqsubseteq \pi_3([P]^k_\Gamma)$” We prove the following, more general, property:

Let $\mathbf{B}_0(x_1, \dots, x_{\#\mathbf{B}_0}) \Rightarrow^*_{\Gamma} \exists y_1 \dots \exists y_n . \phi$ be a complete $\Gamma$-unfolding such that $\phi$ is a qpf formula, $\mathfrak{s}$ be a store injective over $\{x_1, \dots, x_{\#\mathbf{B}_0}\} \cup \{y_1, \dots, y_n\}$, $S = (U, \sigma)$ be a structure such that $S \models^5 \phi$ and $D \subseteq \text{supp}(\sigma) \setminus \{\mathfrak{s}(x_1), \dots, \mathfrak{s}(x_{\#\mathbf{B}_0})\}$ be a set such that $\text{card}(D) \le k$. Then there exists $\langle \{x_1, \dots, x_{\#\mathbf{B}_0}\}, c, M \rangle \in \langle \mathbf{B}_0 \rangle_\Gamma^k$ such that $C_S(\mathfrak{s}(x_i)) = c(x_i)$, for all $i \in [1..\#\mathbf{B}_0]$ and $M = \{C_S(u) | u \in D\}$.

The proof is by induction on the length of the complete $\Gamma$-unfolding. Assume w.l.o.g. that the first rule applied in the unfolding is of the form (3.1), with a qpf formula $\psi_0$. Then, there exist structures $S_0 = (U_0, \sigma_0), \dots, S_\ell = (U_\ell, \sigma_\ell)$, such that:

$$ \triangleright S = S_0 \bullet \dots \bullet S_\ell, $$

$$ \triangleright S_0 \models^5 \psi_0, $$

there exists a complete $\Gamma$-unfolding $\mathbf{B}_i(z_{i,1}, \dots, z_{i,\#\mathbf{B}_i}) \Rightarrow^*_{\Gamma} \exists y_{j_{i,1}} \dots \exists y_{j_{i,k_i}} . \phi_i$, where $j_{i,1}, \dots, j_{i,k_i} \in [1..n]$ and $\phi_i$ is a subformula of $\phi$, such that $S_i \models^5 \phi_i$, and the indices $j_{i,m}$ are pairwise distinct, for all $m \in [1..k_i]$, for all $i \in [1..l]$.
Let $\mathfrak{s}_i$ be the store such that $\mathfrak{s}_i(x_j) = \mathfrak{s}(z_{i,j})$ for all $j \in [1..\#\mathbb{B}_i]$ and $\mathfrak{s}_i$ agrees with $\mathfrak{s}$ everywhere else, for all $i \in [1..\ell]$. Then, there exists a complete $\Gamma$-unfolding:

$$ \mathbb{B}_i(x_1, \dots, x_{\#\mathbb{B}_i}) \Rightarrow_{\Gamma}^{*} (\exists y_{j_{i,1}} \dots \exists y_{j_{i,k_i}} \cdot \phi_i)[z_{i,1}/x_1, \dots, z_{i,\#\mathbb{B}_i}/x_{\#\mathbb{B}_i}] = \exists y_{j_{i,1}} \dots \exists y_{j_{i,k_i}} \cdot \psi_i $$

such that $S_i \models^{\mathfrak{s}_i} \psi_i$, where $\psi_i$ is a qpf formula, for all $i \in [1..\ell]$. We define the sets:

$$ D_0 \stackrel{\text{def}}{=} D \cap (\text{supp}(\sigma_0) \cup \bigcup_{i=1}^{\ell} \{\mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,\#\mathbb{B}_i})\}) \\ D_i \stackrel{\text{def}}{=} (\text{supp}(\sigma_i) \cap D) \setminus \{\mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,\#\mathbb{B}_i})\}, \text{ for each } i \in [1..\ell] $$

and prove the following fact:

**Fact B.4.** $D = D_0 \uplus D_1 \uplus \dots \uplus D_\ell$

*Proof.* The sets $D_0, \dots, D_\ell$ are pairwise disjoint, since:

$$ D_0 \subseteq \text{supp}(\sigma_0) \cup \bigcup_{i=1}^{\ell} \{\mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,\#\mathbb{B}_i})\} \\ D_i \subseteq \text{supp}(\sigma_i) \setminus \{\mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,\#\mathbb{B}_i})\}, \text{ for all } i \in [1..\ell] $$

and, moreover for all $1 \le i < j \le \ell$:

$$ \triangleright (\text{supp}(\sigma_0) \cup \bigcup_{i=1}^{\ell} \{\mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,\#\mathbb{B}_i})\}) \cap \text{supp}(\sigma_i) \subseteq \{\mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,\#\mathbb{B}_i})\} $$

$$ \triangleright \text{supp}(\sigma_i) \cap \text{supp}(\sigma_j) \subseteq \{\mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,\#\mathbb{B}_i})\} \cap \{\mathfrak{s}(z_{j,1}), \dots, \mathfrak{s}(z_{j,\#\mathbb{B}_i})\} $$

because $\mathfrak{s}$ is injective over $y_1, \dots, y_n$. “$\supseteq$” We have $D_0 \uplus D_1 \uplus \dots \uplus D_\ell \subseteq D$ because $D_i \subseteq D$, for all $i \in [0..\ell]$. “$\subseteq$” Let $u \in D$ be an element. By the choice of $D$, we have $u \in \text{supp}(\sigma) \setminus \{\mathfrak{s}(x_1), \dots, \mathfrak{s}(x_{\#\mathbb{B}})\}$. Since $S = S_0 \bullet \dots \bullet S_\ell$, we have $\text{supp}(\sigma) = \bigcup_{i=0}^\ell \text{supp}(\sigma_i)$, hence $u \in \text{supp}(\sigma_i)$, for some $i \in [0..\ell]$. If $u \in D_0$ we are done. Otherwise, $u \notin D_0$, hence $u \notin \text{supp}(\sigma_0)$ and $u \in \text{supp}(\sigma_i)$, for some $i \in [1..\ell]$. Moreover, $u \notin \{\mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,\#\mathbb{B}_i})\}$, for all $j \in [1..\ell]$, hence $u \in D_i$. $\square$

Back to the proof, since $\text{card}(D_i) \le \text{card}(D) \le k$, for all $i \in [1..\ell]$, by the inductive hypothesis, there exist $\langle\{x_1, \dots, x_{\#\mathbb{B}_i}\}, c_i, M_i\rangle \in \langle\mathbb{B}_i\rangle_\Gamma^k$, for $i \in [1..\ell]$, such that:

$$ \triangleright C_S(\mathfrak{s}_i(x_j)) = c(x_j), \text{ for all } j \in [1..\#\mathbb{B}_i], $$

$$ \triangleright M_i = \{C_{S_i}(u) \mid u \in D_i\}. $$

Let $\langle\text{fv}(\psi_0), c_0, \emptyset\rangle \stackrel{\text{def}}{=} \gamma(\psi_0)$ be a color triple. Since $S_0 \models^{\mathfrak{s}} \psi_0$, we have $C_{S_0}(\mathfrak{s}(x_j)) = c(x_j)$, for all $j \in [1..\#\mathbb{B}_0]$. By definition, there exists a constraint of the form (3.4) for the above rule (3.1). We prove that the $\bullet^{\#k}$-composition from the right-hand side of the constraint is defined. Suppose, for a contradiction, that $c_i(x) \cap c_j(x) \ne \emptyset$, for some $x \in \{z_{i,1}, \dots, z_{i,\#\mathbb{B}_i}\} \cap \{z_{j,1}, \dots, z_{j,\#\mathbb{B}_j}\}$ and $1 \le i < j \le \ell$. Then $C_{S_i}(x) \cap C_{S_j}(x) \ne \emptyset$, contradicting the fact that $S_i \bullet S_j$ is defined. The same reasoning applies if $c_0(x) \cap c_i(x) \ne \emptyset$, for some $x \in \text{fv}(\psi) \cap \{z_{i,1}, \dots, z_{i,\#\mathbb{B}_i}\}$ and $i \in [1..\ell]$. Then, there exists a color triple:

$$ \langle X', c', M' \rangle \in \langle \text{fv}(\psi_0), c_0, \emptyset \rangle \bullet^{\#k} \bullet^{\#k} \underset{i \in [1..\ell]}{\cup} \{ \langle x_1, \dots, x_{\#\mathbb{B}_i} \rangle, c_i, M_i \rangle [x_1/z_{i,1}, \dots, x_{\#\mathbb{B}_i}/z_{i,\#\mathbb{B}_i}] $$

W.l.o.g. we can choose the tuple such that $M' = M_1 \cup \dots \cup M_\ell$. This choice is possible since $\text{card}(M') = \sum_{i=1}^\ell \text{card}(M_i) = \sum_{i=1}^\ell \text{card}(D_i) \le \text{card}(D) \le k$. Let $\langle X, c, M \rangle \in \langle X', c', M' \rangle |_{\{x_1, \dots, x_{\#\mathbb{B}_0}\}}^{\#k}$ be such that $M = M' \cup \{C_{S_0}(u) \mid u \in D_0\}$. This choice is possible, since $\text{card}(M) \le \sum_{i=0}^\ell \text{card}(D_i) \le k$. We prove the points of the statement:

Let $i \in [1..\#\mathbb{B}_0]$ be an index. By the definition of the $\bullet^{\#k}$-composition, we have:

$$ C_S(\mathfrak{s}(x_i)) = C_{S_0 \bullet \dots \bullet S_\ell}(\mathfrak{s}(x_i)) = \bigcup_{j=0}^{\ell} C_{S_j}(\mathfrak{s}(x_i)) = \bigsqcup_{j=0}^{\ell} c_j(x_i) = c'(x_i) = c(x_i) $$

$$ \triangleright M = \bigcup_{i=0}^{\ell} \{C_{S_i}(u) \mid u \in D_i\} = \{C_{S_0} \bullet \dots \bullet C_{S_\ell}(u) \mid u \in \bigsqcup_{i=0}^{\ell} D_i\} = \{C_S(u) \mid u \in D\} $$
"$\pi_3(\langle\mathbf{P}\rangle_{\Gamma}^{\sharp k}) \subseteq (\llbracket \mathbf{P} \rrbracket_{\Gamma}^{c})^{\sharp k}$" We prove the following, more general, property:

Let $\langle\{x_1, \dots, x_{\#B_0}\}, c, M\rangle \in \langle B_0\rangle_{\Gamma}^{\sharp k}$ be a color triple. Then there exists a complete $\Gamma$-unfolding $B_0(x_1, \dots, x_{\#B_0}) \Rightarrow_{\Gamma}^{*} \exists y_1 \dots \exists y_n$. $\phi$, whose steps belong to a complete $\Gamma$-unfolding of $\mathbf{P}$, such that $\phi$ is a qpf formula, a store $\mathfrak{s}$ injective over $\{x_1, \dots, x_{\#B_0}\} \cup \{y_1, \dots, y_n\}$, a structure $S = (U, \sigma)$ such that $S = \mathfrak{s}$ and $D \subseteq \text{supp}(\sigma) \setminus \{\mathfrak{s}(x_1), \dots, \mathfrak{s}(x_{\#B_0})\}$, $\text{card}(D) \le k$, such that $C_S(\mathfrak{s}(x_i)) = c(x_i)$, for all $i \in [1..\#B_0]$ and $M = \{C_S(u) | u \in D\}$.

The proof is by induction on the length of the finite fixpoint iteration that produced $\langle\{x_1, \dots, x_{\#B_0}\}, c, M\rangle$. Assume that the last step of the iteration corresponds to a constraint of the form (3.4), with a qpf formula $\psi_0$. By definition, there exists a rule of the form (3.1) in $\Gamma$, with the same qpf formula $\psi_0$. Then $\psi_0$ is satisfiable, because each $\Gamma$-unfolding of $\mathbf{P}$ yields a satisfiable formula. Then there exists a color triple:

$$ \langle X', c', M' \rangle \in \gamma(\psi_0) \bullet^{\sharp k} \bullet^{\sharp k} \mathbf{1}_{i \in [1..\ell]} \langle B_i \rangle_{\Gamma}^{\sharp k} [x_1/z_{i,1}, \dots, x_{\#B_i}/z_{i,\#B_i}] $$

such that

$$ \langle\{x_1, \dots, x_{\#B_0}\}, c, M\rangle \in \langle X', c', M' \rangle_{\{x_1, \dots, x_{\#B_0}\}}^{\sharp k} \\ M \subseteq M' \cup \{c'(x) \mid x \in X' \setminus \{x_1, \dots, x_{\#B_0}\}\} $$

Then, there exist

$$ \langle \text{fv}(\psi_0), c_0, \emptyset \rangle \stackrel{\text{def}}{=} \gamma(\psi_0) \\ \langle \{z_{i,1}, \dots, z_{i,\#B_i}\}, c'_i, M_i \rangle \in \langle B_i \rangle_{\Gamma}^{\sharp k} [x_1/z_{i,1}, \dots, x_{\#B_i}/z_{i,\#B_i}], \text{ for all } i \in [1..\ell] $$

such that

$$ \langle X', c', M' \rangle \in \langle \text{fv}(\psi_0), c_0, \emptyset \rangle \bullet^{\sharp k} \bullet^{\sharp k} \mathbf{1}_{i \in [1..\ell]} \langle \{z_{i,1}, \dots, z_{i,\#B_i}\}, c'_i, M_i \rangle $$

Hence, there exist $\langle\{x_1, \dots, x_{\#B_i}\}, c_i, M_i\rangle \in \langle B_i\rangle_{\Gamma}^{\sharp k}$ such that $c'_i = c_i \circ [x_1/z_{i,1}, \dots, x_{\#B_i}/z_{i,\#B_i}]$, for all $i \in [1..\ell]$. By the inductive hypothesis, for all $i \in [1..\ell]$, there exist:

▷ a complete unfolding $B_i(x_1, \dots, x_{\#B_i}) \Rightarrow_{\Gamma}^{*} \exists y_{j_{i,1}} \dots \exists y_{j_{i,k_i}}$. $\psi_i$ such that $\psi_i$ is a qpf formula. By applying an $\alpha$-renaming, if necessary, we assume w.l.o.g. that the variables $y_{j_{i,1}} \dots y_{j_{i,k_i}}$ are pairwise distinct and, moreover, distinct from $x_1, \dots, x_{\#B_i}$.

▷ a store $\mathfrak{s}_i$ that is injective over $\{x_1, \dots, x_{\#B_i}\} \cup \{y_{j_{i,1}}, \dots, y_{j_{i,k_i}}\}$. We assume w.l.o.g. that $\mathfrak{s}_i(x_j) = \mathfrak{s}_k(x_m)$ iff $z_{i,j}$ and $z_{k,m}$ are the same variable in the rule (3.1), for all $1 \le i < k \le \ell$, $j \in [1..\#B_i]$ and $m \in [1..\#B_k]$. Note that this assumption does not contradict the fact that $\mathfrak{s}_i$ is injective over $\{x_1, \dots, x_{\#B_i}\} \cup \{y_{j_{i,1}}, \dots, y_{j_{i,k_i}}\}$.

▷ a structure $S_i = (U_i, \sigma_i)$ such that $S_i = \mathfrak{s}_i \psi_i$. We assume w.l.o.g. that $\text{supp}(\sigma_i) \cap \text{supp}(\sigma_j) \subseteq \{\mathfrak{s}_i(x_1), \dots, \mathfrak{s}_i(x_{\#B_i})\} \cap \{\mathfrak{s}_j(x_1), \dots, \mathfrak{s}_j(x_{\#B_j})\}$. Note that this is possible by the assumption that $\Gamma$ is equality-free.

▷ a set $D_i \subseteq \text{supp}(\sigma_i) \setminus \{\mathfrak{s}_i(x_1), \dots, \mathfrak{s}_i(x_{\#B_i})\}$, such that $\text{card}(D_i) \le k$, $C_{S_i}(\mathfrak{s}_i(x_j)) = c_i(x_j)$, for all $j \in [1..\#B_i]$ and $M_i = \{C_{S_i}(u) | u \in D_i\}$.

We prove the points of the statement. Let $\theta_i$ be the substitution $[x_1/z_{i,1}, \dots, x_{\#B_i}/z_{i,\#B_i}]$, for each $i \in [1..\ell]$, where $B_i(z_{i,1}, \dots, z_{i,\#B_i})$ is a predicate atom that occurs on the right-hand side of the rule (3.1). A complete $\Gamma$-unfolding $B_0(x_1, \dots, x_{\#B_0}) \Rightarrow_{\Gamma}^{*} \exists y_1 \dots \exists y_n$. $\psi$ is built from the rule (3.1) above, with qpf formula $\psi_0$, followed by $B_i(x_1, \dots, x_{\#B_i}) \theta_i \Rightarrow_{\Gamma}^{*} \exists y_{j_{i,1}} \dots \exists y_{j_{i,k_i}}$. $\psi_i \theta_i$, for all $i \in [1..\ell]$. Hence $\psi = \psi_0 * \mathfrak{s}'_i \psi_i \theta_i$ modulo a reordering of atoms. Let $\mathfrak{s}'_i \stackrel{\text{def}}{=} \mathfrak{s}_i \circ \theta_i$ and define the store $\mathfrak{s}$ as follows:

▷ $\mathfrak{s}(z) \stackrel{\text{def}}{=} \mathfrak{s}'_i(z)$, for each each $z \in \text{fv}(\psi_i \theta_i)$,
▷ $\mathfrak{s}(z) \notin \bigcup_{i=1}^{\ell} \mathfrak{s}'_i(\mathrm{fv}(\psi_i\theta_i))$, for each variable $z \in \mathrm{fv}(\psi_0) \setminus \bigcup_{i=1}^{\ell} \mathrm{fv}(\psi_i\theta_i)$ such that, moreover, $\mathfrak{s}$ is injective over $\mathrm{fv}(\psi_0)$. Note that this is possible because we assumed $\Gamma$ to be equality-free.

Then, we consider a structure $S_0 = (U_0, \sigma_0)$ such that:

▷ $S_0 \models^s \psi_0$, and

▷ $\mathrm{supp}(\sigma_0) \cap \mathrm{supp}(\sigma_i) \subseteq \mathfrak{s}(\mathrm{fv}(\psi_0)) \cap \mathfrak{s}(\mathrm{fv}(\psi_i\theta_i))$, for all $i \in [1..\ell]$.

Since $\psi_0$ is satisfiable, such a structure exists and we can consider w.l.o.g. that it satisfies the above conditions, because $\Gamma$ is equality-free. It is easy to check that the structures $S_0, \dots, S_\ell$ are pairwise locally disjoint, hence $S = (U, \sigma) \stackrel{\mathrm{def}}{=} S_0 \bullet \dots \bullet S_\ell$ is defined. Moreover, we have $S \models^s \psi$, because $\psi = \psi_0 * \ast_{i=1}^\ell \psi_i\theta_i$, $S_0 \models^s \psi_0$ and $S_i \models^s \psi_i\theta_i$, for all $i \in [1..\ell]$. Further, for all $j \in [1..\#B_0]$, we have:

$$C_S(\mathfrak{s}(x_j)) = C_{S_0 \bullet \dots \bullet S_\ell}(\mathfrak{s}(x_i)) = \bigcup_{i=0}^{\ell} c_i(x_j) = c'(x_j) = c(x_j)$$

We consider the set $D \stackrel{\mathrm{def}}{=} \{u \in \mathrm{supp}(\sigma) \mid C_S(u) \in M\}$. Suppose, for a contradiction, that $\mathfrak{s}(x_i) \in D$, for some $i \in [1..\#B_0]$. Then $C_S(\mathfrak{s}(x_i)) \in M$, hence $c(x_i) \in M$. Since $M \subseteq M' \cup \{c'(x) \mid x \in X' \setminus \{x_1, \dots, x_{\#B_0}\}\}$, we must have $c(x_i) \in M' \subseteq \bigcup_{j=1}^\ell M_j$ and let $j \in [1..\ell]$ be such that $c(x_i) \in M_j = \{C_{S_j} \mid u \in D_j\}$, by the inductive hypothesis. Then there exists $k \in [1..\#B_j]$ such that $c(x_i) = c_j(x_k) = C_{S_i}(\mathfrak{s}_j(x_k))$, thus $\mathfrak{s}_j(x_k) \in D_j \subseteq \mathrm{supp}(\sigma_j) \setminus \{\mathfrak{s}_j(x_1), \dots, \mathfrak{s}_j(x_{\#B_j})\}$, contradiction. We obtained $D \subseteq \mathrm{supp}(\sigma) \setminus \{\mathfrak{s}(x_1), \dots, \mathfrak{s}(x_{\#B_0})\}$ and are left with proving that $M = \{C_S(u) \mid u \in D\}$. “$\supseteq$” Immediate, by the definition of $D$. “$\subseteq$” Let $C \in M$ be a color. Then either one of the following holds:

▷ $C = \{r \in \mathbb{R} \mid r(z, \dots, z) \text{ occurs in } \psi_0\} \cup \bigcup_{i=1}^{\ell} c_i(z)$, for some $z \in \mathrm{fv}(\psi_0)$: in this case, $C = C_S(\mathfrak{s}(z))$ and $\mathfrak{s}(z) \in \mathrm{supp}(\sigma)$, hence $\mathfrak{s}(z) \in D$.

▷ $C \in M_i$, for some $i \in [1..\ell]$: in this case, $C = C_S(u) = C_{S_i}(u)$, for some $u \in D_i$, by the inductive hypothesis. Then $u \in \mathrm{supp}(\sigma_i) \subseteq \mathrm{supp}(\sigma)$, hence $u \in D$. $\square$

## APPENDIX C. PROOFS FROM SECTION 4

**C.1. Proof of Lemma 4.7.** Assume w.l.o.g. that $\mathcal{A}$ is rooted and let $\mathfrak{G}_\mathcal{A} = (\mathcal{N}, \mathcal{E}, S_0)$ be the SCC graph of $\mathcal{A}$. By Definition 4.5, $\mathfrak{G}_\mathcal{A}$ is a tree and, moreover, $S_0 = \{\iota\}$, because $\mathcal{A}$ is rooted. Let $\Lambda : \mathcal{N} \cup \delta \to \{1, \infty\}$ be the labeling from Definition 4.5. For every SCC $S \in \mathcal{N} \setminus \{S_0\}$, let entry($S$) be the unique state $q$ such that $\{q\} = \tau^\bullet \cap S$, where $\{\tau\} = \bullet S$, by point (1) of Definition 4.5, and entry($S_0$) $\stackrel{\mathrm{def}}{=} \iota$. Moreover, each linear SCC $S \in \mathcal{N}$ such that $\Lambda(S) = 1$ has a unique transition $\tau$, such that $S^\bullet = \{\tau\}$, by point (2a) of Definition 4.5. We prove first an invariant of 1-labeled linear SCCs:

**Fact C.1.** Let $p \in \mathrm{dom}(\theta)$ be a position, such that $\theta(p) \in S$, for a linear SCC $S \in \mathcal{N}$, such that $\Lambda(S) = 1$. Then there exists a descendant $p' \in \mathrm{dom}(\theta)$ of $p$, such that $\theta(p') = s_0$, $t(p') = \beta$ and $\theta(p'i) = s_i$, for all $i \in [1..k]$, where $S^\bullet = \{s_0 \stackrel{\beta}{\to} (s_1, \dots, s_k)\}$.

*Proof.* Suppose, for a contradiction, that $s_0 \stackrel{\beta}{\to} (s_1, \dots, s_k)$ never occurs below $p$ in $\theta$. Then every transition that occurs at some position below $p$ in $\theta$ must be from $\bullet S^\bullet$. This, however, cannot be the case for a transition $\theta(p') \stackrel{t(p')}{\to} ()$, such that $p' \in \mathrm{fr}(\theta)$. Since, moreover, $\theta$ is an accepting run, such a transition must occur on the frontier of $\theta$. $\square$

The following facts prove the existence and uniqueness of a position labeled with the entry state of each 1-labeled linear SCC:
**Fact C.2.** For each SCC $S \in \mathcal{N}$, such that $\Lambda(S) = 1$, there exists a position $p \in \text{dom}(\theta)$, such that $\theta(p) = \text{entry}(S)$.

*Proof.* Because $\mathfrak{G}_A$ is a tree with root $S_0$, we have that $S$ is reachable from $S_0$ in $\mathfrak{G}_A$ by a path of pairs from $\mathcal{E}$. The proof goes by induction on the length $n \ge 0$ of this path. For the base case $n = 0$ (i.e., $S = S_0$) we take $p = \epsilon$. For the inductive step, let $S'$ be the parent of $S$ in $\mathfrak{G}_A$. By points (1) and (2c) of Definition 4.5, $\bullet S = \{\tau\}$ for some $\tau \in S'^{\bullet} \cap \delta^1$, such that $\{\text{entry}(S)\} = \tau^{\bullet} \cap S$. By the inductive hypothesis, there exists a position $p' \in \text{dom}(\theta)$, such that $\theta(p') = \text{entry}(S')$. By Fact C.1, there exists a descendant $p$ of $p'$, such that $\theta(p) = \text{entry}(S)$. $\square$

**Fact C.3.** For each SCC $S \in \mathcal{N}$, such that $\Lambda(S) = 1$, there exists at most one position $p \in \text{dom}(\theta)$, such that $\theta(p) = \text{entry}(S)$.

*Proof.* Suppose, for a contradiction, that there exist two positions $p_1, p_2 \in \text{dom}(\theta)$, such that $\theta(p_1) = \theta(p_2) = \text{entry}(S)$. By induction of the length of $p_i$, we prove the existence of a sequence $S_{i,k_i}, \tau_{i,k_i}, \dots, S_{i,1}, \tau_{i,1}, S_{i,0} = S_0$ such that $\theta(p_i) \in S_{i,k_i}$, $\bullet S_{i,j} = \tau_{i,j}$ and $\{\tau_{i,j}\} = S_{i,j-1}^{\bullet}$, for all $j \in [1..k_i]$ and $i = 1, 2$. Since $p_1 \neq p_2$, there exists an SCC $S_{1,j_1} = S_{2,j_2}$ that violates condition (1) of Definition 4.5. $\square$

Let $\tau : q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell)$ be a transition, such that $\Lambda(\tau) = 1$. By point (2b) of Definition 4.5, we have $\tau \in S^{\bullet}$ for some linear SCC $S \in \mathcal{N}$, such that $\Lambda(S) = 1$. By Fact C.2 and Fact C.3, there exists a unique position $p \in \text{dom}(\theta)$, such that $\theta(p) = \text{entry}(S)$. By Fact C.1, there exists a position $p' \in \text{dom}(\theta)$, such that $\theta(p') = q_0$, $t(p') = \alpha$ and $\theta(p'i) = q_i$, for all $i \in [1..\ell]$. Suppose, for a contradiction, that this position is not unique, hence there exists another position $p'' \in \text{dom}(\theta)$, such that $\theta(p'') = q_0$, $t(p'') = \alpha$ and $\theta(p''i) = q_i$, for all $i \in [1..\ell]$. Since $\theta(p') = \theta(p'') = q_0 \in S$, there exists a transition $\tau'$ with $\text{card}(\tau'^{\bullet} \cap S) \ge 2$, in contradiction with the fact that $S$ is linear. This concludes the proof. $\square$

**C.2.** *Proof of Lemma 4.8.* Let us consider the SCC graph $\mathfrak{G}_A = (\mathcal{N}, \mathcal{E}, S_0)$ and the mapping $\Lambda : \mathcal{N} \cup \delta \to \{1, \infty\}$ with the properties stated in Definition 4.5 and let $q \in \bullet(\delta^\infty)$ be a state. W.l.o.g., we consider that $\mathcal{L}(A) \neq \emptyset$ and that $A$ is trim. Then $q$ is reachable from $S_0 = \{\iota\}$, i.e., there exists a partial run $\theta_1$ on $A$ and a position $p_1$ such that $\theta_1(\epsilon) = \iota$ and $\theta_1(p_1) = q$. Let $p_2$ be the longest strict prefix of $p_1$ such that the transition $\tau : \theta_1(p_2) \xrightarrow{a} \langle\theta_1(p_21), \dots, \theta_1(p_2\ell)\rangle$ is in $\delta^1$ for some $a \in A$ and index $\ell$. This position $p_2$ exists, by Definition 4.5, because $S_0 = \{\iota\}$ is linear, $\Lambda(S_0) = 1$ by condition (2c), $\text{card}(S_0^{\bullet}) = 1$ by condition (2a), and the only transition $\tau_0 \in \{\iota\}^{\bullet}$ is in $\delta^1$ by condition (2b). This shows that $\iota \notin \bullet\delta^\infty$ hence $q \neq \iota$ and $\tau_0$ is a transition in $\delta^1$ on the path from $\iota$ to $q$ in $\theta_1$, with $\tau$ being the last one.

We decompose $p_1 = p_2rp_3$ for some index $r \in [1..\ell]$ and position $p_3$ and define the partial run $\theta_2$ as $\theta_2(\epsilon) \stackrel{\text{def}}{=} \theta_1(p_2r)$ and, for each $u \in \mathbb{N}^*$ and $i \in \mathbb{N}$ such that $p_2ru_i \in \text{dom}(\theta_1)$ and $p_2ru$ is a strict prefix of $p_1$, by $\theta_2(u_i) \stackrel{\text{def}}{=} \theta_1(p_2ru)$. Then $\theta_2$ starts from the state $q_0 \stackrel{\text{def}}{=} \theta_1(p_2r) \in \tau^{\bullet}$ and $p_3 \in \text{fr}(\theta_2)$ gives the state $\theta_2(p_3) = q$. Let $S \in \mathcal{N}$ be the SCC in $\mathfrak{G}_A$ such that $q_0 \in S$. Then $\Lambda(\tau) = 1$ and $\tau \in \bullet S$ (hence $\bullet S = \{\tau\}$ by condition (1) of Definition 4.5), thus $\Lambda(S) = 1$ by condition (2c) of Definition 4.5.

We distinguish three cases (see Figure 15 for an illustration):

▷ If $S$ is not linear, there exists a transition $\tau' \in \bullet S^{\bullet}$ such that $\text{card}(\tau'^{\bullet} \cap S) \ge 2$. Let $q' \stackrel{\text{def}}{=} \tau'$ and $q'', q'''$ be the states such that $\{\!\{q'', q'''\}\} \subseteq \tau'^{\bullet} \cap S$. Since $q_0, q', q'', q''' \in S$, we can
construct a partial run $\theta_3 \in \mathcal{R}_{q_0}^{\infty}(\mathcal{A})$ with transitions taken from $\bullet S^\bullet$, which reaches $q'$ from $q_0$, then applies $\tau'$ and reaches $q_0$ from both $q''$ and $q'''$. This gives $\theta_3(p_4) = \theta_3(p_5) = q_0$, for two distinct positions $p_4, p_5 \in \text{fr}(\theta_3)$. We define $\theta_0 \in \mathcal{R}_{q_0}^{\infty}(\mathcal{A})$ as the partial run with domain $\text{dom}(\theta_3) \cup \{p_5u \mid u \in \text{dom}(\theta_2)\}$, that extends $\theta_3$ by $\theta_0(p_5u) \stackrel{\text{def}}{=} \theta_2(u)$, for all $u \in \text{dom}(\theta_2)$. Then $\theta_0$ satisfies point 1 of the lemma because $\theta_0(p_4) = q_0$ and $\theta_0(p_5p_3) = q$, with $p_4 \neq p_5p_3 \in \text{fr}(\theta_0)$.

▷ If $S$ is linear and $q \notin S$, there exists a unique position $p_6$ and a transition:

$$ \tau' : \theta_2(p_6) \stackrel{\alpha}{\rightarrow} \langle \theta_2(p_61), \dots, \theta_2(p_6k) \rangle \in \delta^{\infty} $$

for some alphabet symbol $\alpha \in \mathcal{A}$ and some index $k \in \mathbb{N}$, such that $\theta_2(p_6) \in S$. Moreover, there exists an index $r \in [1..k]$ such that $\theta_2(p_6r) \notin S$ and $p_6r$ is a prefix of $p_3$. Then $\Lambda(\tau') = \infty$ and, by condition (2b) of Definition 4.5, we have $\tau' \notin S^\bullet$, hence $\tau' \in \bullet S^\bullet$ and $q' \stackrel{\text{def}}{=} \theta_2(p_6r') \in S$ for another index $r' \in [1..k] \setminus \{r\}$. Then there exists a partial run $\theta_4 \in \mathcal{R}_{q_0}^{\infty}(\mathcal{A})$ such that $\theta_4(p_7) = q_0$ for some position $p_7 \in \text{fr}(\theta_4)$. We define the partial run $\theta_0 \in \mathcal{R}_{q_0}^{\infty}(\mathcal{A})$ with domain $\text{dom}(\theta_2) \cup \{p_6r'u \mid u \in \text{dom}(\theta_4)\}$, by extending $\theta_2$ with $\theta_0(p_6r'u) \stackrel{\text{def}}{=} \theta_4(u)$, for all $u \in \text{dom}(\theta_4)$. Then $\theta_0$ satisfies point 1 of the lemma because $\theta_0(p_6r'p_7) = q_0$ and $\theta_0(p_3) = q$, with $p_6r'p_7 \neq p_3 \in \text{fr}(\theta_0)$.

▷ If $S$ is linear and $q \in S$, let $\theta \in \mathcal{R}_{q_0}^{\infty}(\mathcal{A})$ be a partial run. Then $S^\bullet$ contains only one transition in $\delta^1$, thus for every position $u \in \text{dom}(\theta) \setminus \text{fr}(\theta)$, such that $\theta(u) \in S$, the transition $\theta(u) \stackrel{\alpha}{\rightarrow} \langle \theta(u1), \dots, \theta(uk) \rangle$ belongs to $\bullet S^\bullet$. Then, there exists an index $i \in [1..k]$ such that $\theta(\text{ui}) \in S$, and we can find a path in $\theta$ which stays in $S$ and reaches the frontier, that is $q' \stackrel{\text{def}}{=} \theta(p_8) \in S$, for some $p_8 \in \text{fr}(\theta)$. Hence, there exists a partial run $\theta_5 \in \mathcal{R}_{q_0}^{\infty}(\mathcal{A})$ such that $\theta_5(p_9) = q_0$, for some position $p_9 \in \text{fr}(\theta_5)$. We now can extend $\theta$ to some partial run $\theta' \in \mathcal{R}_{q_0}^{\infty}(\mathcal{A})$ with domain $\text{dom}(\theta) \cup \{p_8u \mid u \in \text{dom}(\theta_5)\}$, as $\theta'(p_8u) \stackrel{\text{def}}{=} \theta_5(u)$ for all $u \in \text{dom}(\theta_5)$. The partial run $\theta'$ satisfies point 2 of the lemma, because $\theta'(p_8p_9) = q_0$, with $p_8p_9 \in \text{fr}(\theta')$. $\square$

<figure><img src="image_24.png" /><figcaption>Figure 15: The cases from the proof of Lemma 4.8</figcaption></figure>
### C.3. Proof of Lemma 4.9.
We assume w.l.o.g. that $\mathcal{A} = (\mathcal{A}, \mathcal{Q}, \iota, \delta)$ is rooted. Let $\mathfrak{G}_\mathcal{A} = (\mathcal{N}, \mathcal{E})$ be the SCC graph of $\mathcal{A}$, where $\mathcal{N} = \{S_1, \dots, S_M\}$ is a topological ordering of the SCCs i.e., if $(S_i, S_j) \in \mathcal{E}$ then $i < j$, for all $i, j \in [1..M]$. For each $i = 1, \dots, M$, we iterate the following transformation of $\mathcal{A}$:

* $\text{let } S_i \stackrel{\text{def}}{=} \bigcup_{(S_i, S_j) \in \mathcal{E}^*} S_j$ be the set of states from any SCC reachable from $S_i$ in $\mathfrak{G}_\mathcal{A}$,

* $\text{let } k_i \stackrel{\text{def}}{=} \sum_{\tau \in \bullet S_i} \text{card}(\tau \bullet \cap S_i)$ be the number of edges of $\mathfrak{G}_\mathcal{A}$ incoming to $S_i$,

* create $k_i$ copies of the transitions $q_0 \xrightarrow{a} (q_1, \dots, q_\ell) \in \delta$ such that $\{q_0, q_{i_1}, \dots, q_{i_j}\} = \{q_0, \dots, q_\ell\} \cap S_i$ i.e., add a transition $(q_0, h) \xrightarrow{a} (q_1, \dots, (q_{i_1}, h), \dots, (q_{i_j}, h), \dots, q_\ell)$ for each $h \in [1..k_i]$,

* connect these new transitions to the rest of the automaton by adequately changing the states $q \in \tau \bullet \cap S_i$ for $\tau \in \bullet S_i$ to their corresponding copies $(q, h)$, for all $h \in [1..k_i]$.

It is easy to check that the resulting automaton fulfills condition (1) of Definition 4.5 and has the same language as $\mathcal{A}$, using Lemma 4.4. We can thus assume w.l.o.g. in the following that $\mathfrak{G}_\mathcal{A} = (\mathcal{N}, \mathcal{E}, S_1)$ is a tree and let $S_1, \dots, S_N$ be a topological ordering of its nodes. We associate a variable $x_i$ (resp. $y_\tau$) ranging over $\{0, 1, \infty\}$ with each SCC $S_i \in \mathcal{N}$ (resp. transition $\tau \in \delta$). Initially, the values of these variables are all zero. We iterate over the finite sequence $S_1, \dots, S_N$ as follows. For each $i \in [1..N]$, we perform the following assignments in this order:

(i) let $x_i \stackrel{\text{def}}{=} \begin{cases} 1, & \text{if } i=1 \\ \sum_{\tau \in \bullet S_i} y_\tau \cdot \text{card}(\tau \bullet \cap S_i), & \text{otherwise} \end{cases}$

(ii) for each $\tau \in \bullet S_i \bullet$, let $y_\tau \stackrel{\text{def}}{=} \begin{cases} \infty, & \text{if } x_i > 0 \\ 0, & \text{otherwise} \end{cases}$

(iii) if $x_i \in \{0, \infty\}$ or $S_i$ is nonlinear, for each $\tau \in S_i \bullet$, let $y_\tau \stackrel{\text{def}}{=} \begin{cases} \infty, & \text{if } x_i > 0 \\ 0, & \text{otherwise} \end{cases}$

(iv) else (i.e., $x_i = 1$ and $S_i$ is linear) choose for all $\{y_\tau\}_{\tau \in S_i \bullet}$ some values from $\{0, 1\}$, such that $x_i = \sum_{\tau \in S_i \bullet} y_\tau$.

Since, for each SCC $S_i \in \mathcal{N}$, there is at most one transition $\tau \in \bullet S_i$ and $\text{card}(\tau \bullet \cap S_i) \le 1$, each variable $x_i$ is assigned either 0, 1 or $\infty$ at (i). Note that no variable is assigned twice in the above iteration sequence, because every $x_i$ is assigned exactly once, every $y_\tau$, for $\tau \in \bullet S_i$ is assigned before $x_i$ and every $y_\tau$, for $\tau \in \bullet S_i \bullet \cup S_i \bullet$ is assigned after $x_i$. Furthermore, we have $\bullet S_i \bullet \cap \bullet S_j \bullet = \emptyset$ and $S_i \bullet \cap S_j \bullet = \emptyset$, for all $1 \le i < j \le N$, so that each $y_\tau$, for $\tau \in \bullet S_i \bullet \cup S_i \bullet$, is assigned exactly once. Moreover, since the choice at (iv) is finite, there are finitely many outcomes of the above nondeterministic iteration, say $(\mathbf{x}_1, \mathbf{y}_1), \dots, (\mathbf{x}_\ell, \mathbf{y}_\ell)$, where $\mathbf{x}_i = \langle \bar{x}_{i,j} \rangle_{j \in [1..N]}$ and $\mathbf{y}_i = \langle \bar{y}_{i,\tau} \rangle_{\tau \in \delta}$. For each $i \in [1..\ell]$, we define the automaton $\mathcal{A}_i = (\mathcal{A}, \mathcal{Q}_i, \iota, \delta_i)$, where $\mathcal{Q}_i \stackrel{\text{def}}{=} \bigcup\{S_j \mid \bar{x}_{i,j} > 0, j \in [1..N]\}$ and $\delta_i \stackrel{\text{def}}{=} \{\tau \in \delta \mid \bar{y}_{i,\tau} > 0\}$. We are left with proving the following facts:

**Fact C.4.** Each automaton $\mathcal{A}_i$ is choice-free, for $i \in [1..N]$.

*Proof.* We prove below the points of Definition 4.5:

(1) Let $S_{j_0}$ be an SCC of $\mathcal{A}$, such that $\bar{x}_{i,j_0} > 0$ i.e., $S_{j_0}$ is a vertex in the SCC graph $\mathfrak{G}_{\mathcal{A}_i}$. Since the variable $x_{j_0}$ received its value $\bar{x}_{i,j_0}$ at (i), either $j_0 = 1$ (in which case $\bar{x}_{i,j_0} = 1$) or there exists an incoming transition $\tau \in \bullet S_{j_0}$ such that $\bar{y}_{i,\tau} > 0$. Let $S_{j_1}$, for some $j_1 < j_0$ be the SCC such that $\bullet \tau \in S_{j_1}$. Then $\bar{x}_{i,j_1} > 0$. Repeating the same argument for $j_1$, we discover a maximal finite sequence $j_0, \dots, j_k$ such that $(S_{j_{i+1}}, S_{j_i}) \in \mathcal{E}$, for all $i \in [0..k-1]$. Moreover, it must be the case that $j_k = 1$, or else the sequence could be extended, contradicting its
maximality. Since $\mathfrak{G}_A$ is a tree, the path from $S_1$ to $S_{j_0}$ must be unique and, since the choice of $S_{j_0}$ was arbitrary, $\mathfrak{G}_{A_i} = (\mathcal{N}_i, \mathcal{E}_i, S_1)$ is a tree as well. The second point from condition (1) holds already for $\mathfrak{G}_A$, hence it must hold for $\mathfrak{G}_{A_i}$.

(2) The mapping $\Lambda_i : \mathcal{N}_i \cup \delta_i \to \{1, \infty\}$ is defined as $\Lambda_i(S_j) = \bar{x}_{i,j}$ for each $S_j \in \mathcal{N}_i$ and $\Lambda_i(\tau) = \bar{y}_{i,\tau}$ for each $\tau \in \delta_i$. We check that $\Lambda_i$ verifies the conditions (2) from Definition 4.5:

(2a) if $S_j \in \mathcal{N}_i$ is linear and $\bar{x}_{i,j} = 1$ then the choice at step (iv) was $\bar{y}_{i,\tau} = 1$, for exactly one transition $\tau \in S_j$.

(2b) $\bar{y}_{i,\tau} = 1$ iff the value of $y_\tau$ was set at step (iv) and $\tau \in S_j$ is the unique outgoing transition for which a nonzero value was assigned to $y_\tau$, for a linear SCC $S_j$ with $\bar{x}_{i,j} = 1$.

(2c) $\bar{x}_{i,j} = 1$ iff the value of $x_j$ was set at step (i) and either $j = 1$ or for all but one transitions $\tau \in \mathcal{S}_j$ we have $\bar{y}_{i,\tau} = 1$. $\square$

**Fact C.5.** $\mathcal{L}(\mathcal{A}) = \bigcup_{i=1}^{\ell} \mathcal{L}(\mathcal{A}_i)$.

*Proof.* “$\supseteq$” Since $\delta_i \subseteq \delta$, we have $\mathcal{L}(\mathcal{A}_i) \subseteq \mathcal{L}(\mathcal{A})$, for all $i \in [1..\ell]$.

“$\subseteq$” Let $t \in \mathcal{L}(\mathcal{A})$ and $\theta$ be an accepting run of $\mathcal{A}$ over $t$. We show that there exists an iteration (i)-(iv) leading to the values $(\mathbf{x}_i, \mathbf{y}_i)$ such that, for each transition $\tau$ occurring on $\theta$ at some position $p \in \text{dom}(\theta)$ i.e., $\theta(p) = \bullet\tau$, we have:

▷ $\bar{x}_{i,j} > 0$, where $S_j$ is the unique SCC of $\mathcal{A}$ such that $\bullet\tau \in S_j$, and

▷ $\bar{y}_{i,\tau} > 0$.

By the second point above we obtain that $\theta$ is an accepting run of $\mathcal{A}_i$. The proof is by reverse induction on the size of the subtree of $\theta$ rooted at $p$.

**Base case:** If $p = \epsilon$, the variable $x_1$ is always assigned the value 1 at step (i). We chose the values for all $\{y_{\tau'}\}_{\tau' \in S_1} \bullet$, such that $y_\tau$ is assigned 1 and $y_{\tau'}$ is assigned 0, for all $\tau' \in S_1 \bullet \setminus \{\tau\}$ at step (iv).

**Induction step:** If $p \in \text{dom}(\theta) \setminus \{\epsilon\}$, since $j \neq 1$, by the inductive hypothesis, the variable $y_{\tau'}$ is assigned non-zero values, for at least one $\tau' \in \mathcal{S}_j$, thus we assign $x_j$ the value $\sum_{\tau' \in \mathcal{S}_j} y_{\tau'} \cdot \text{card}(\tau \bullet \cap S_j) > 0$ at step (i). If $\tau \in \mathcal{S}_j \bullet$, then $y_\tau$ is assigned $\infty$ at step (ii). Otherwise, it must be the case that $\tau \in \mathcal{S}_j \bullet$ and we distinguish two cases. If $S_j$ is nonlinear, then $y_\tau$ is assigned $\infty$ at (iii). Else, $S_j$ is linear and we can chose the value 1 for $y_\tau$ at step (iv), because $x_j$ has been already assigned to 1. $\square$

Let $i \in [1..\ell]$. We prove the upper bound on $\text{card}(\delta_i^1)$, as follows. Since the SCC graph of $\mathcal{A}_i$ is a tree, the number of 1-transitions in $\mathcal{A}_i$ equals the number of SCCs in $\mathcal{A}_i$. Due to the expansion of the first step of the proof, we have $\text{card}(\delta_i^1) \leq \max\{\rho(a) \mid a \in \mathcal{A}\}^s \leq \max\{\rho(a) \mid a \in \mathcal{A}\}^{\text{card}(\mathcal{Q})}$, where $s \leq \text{card}(\mathcal{Q})$ denotes the number of SCCs in $\mathcal{A}$. $\square$

**C.4.** **Proof of Lemma 4.13.** (1) For the first part, we prove the two directions of the following equivalence: for all structures $S$ and predicates $B$ of arity $n$, there exists a store $\mathfrak{s}$ such that $S \models_{\Delta}^{\mathfrak{s}} B(x_1, \dots, x_n)$ iff there exists a tree $t \in \mathcal{L}_{q_B}(\mathcal{A}_{\Delta,A})$ and a store $\bar{\mathfrak{s}}$ such that $S \models_{\bar{\Delta}}^{\bar{\mathfrak{s}}} \Theta(t)$ and $\bar{\mathfrak{s}}(x_j^{[\ell]}) = \mathfrak{s}(x_j)$ for all $j \in [1..n]$.

“⇒” We proceed by induction on the definition of $S \models_{\Delta}^{\mathfrak{s}} B(x_1, \dots, x_n)$. Then $\Delta$ contains a rule $\rho$ of the form $B(x_1, \dots, x_n) \leftarrow \exists y_1 \dots \exists y_m \cdot \psi * \mathcal{N}_{i=1}^{\ell} B_i(z_{i,1}, \dots, z_{i,n_i})$ and we can decompose the structure $S = S_0 \bullet \dots \bullet S_\ell$, such that $S_0 \models_{\bar{\Delta}}^{\mathfrak{s}'} \psi$ and $S_i \models_{\Delta}^{\mathfrak{s}'} B_i(z_{i,1}, \dots, z_{i,n_i})$ for all $i \in [1..\ell]$, for a store $\mathfrak{s}'$ that agrees with $\mathfrak{s}$ over $\{x_1, \dots, x_n\}$. For all $i \in [1..\ell]$, we consider a store $\mathfrak{s}_i$ such that $\mathfrak{s}_i(x_j) = \mathfrak{s}'(z_{i,j})$, for all $j \in [1..n_i]$. We have $S_i \models_{\Delta}^{\mathfrak{s}_i} B_i(x_1, \dots, x_{n_i})$
and, by induction hypothesis, there exists a tree $t_i \in \mathcal{L}_{q_{\mathbb{B}_i}}(\mathcal{A}_{\Delta,\mathcal{A}})$ and a store $\bar{s}_i$ such that
$S_i \models^{\bar{s}_i} \Theta(t_i)$ and $\bar{s}_i(x_j^{[\epsilon]}) = s_i(x_j)$ for all $j \in [1..n_i]$. Let $\bar{s}$ be a store such that:

▷ $\bar{s}(x_j^{[\epsilon]}) = s(x_j)$, for all $j \in [1..n]$,

▷ $\bar{s}(y_j^{[\epsilon]}) = s'(y_j)$ for all $j \in [1..m]$,

▷ $\bar{s}(z^{[\ell p]}) \stackrel{\text{def}}{=} \bar{s}_i(z^{[p]})$, for all $i \in [1..\ell]$ and $z^{[p]} \in \text{fv}(\Theta(t_i))$.

Note that $\bar{s}$ is well defined because $\bar{s}_i(z^{[p]}) = \bar{s}_j(z^{[p]}) = s'(z^{[p]})$, for all $z^{[p]} \in \text{fv}(\Theta(t_i)) \cap \text{fv}(\Theta(t_j))$. We have $S_i \models^{\bar{s}} \Theta(t_i)^{[i]}$ for all $i \in [1..\ell]$ and $S_0 \models^{\bar{s}} \alpha_\rho$, thus $S \models^{\bar{s}} \Theta(t)$ where $t$ is the tree consisting of a root labelled by $\alpha_\rho$ and $\ell$ children $t_i$ for $i \in [1..\ell]$. Since $t \in \mathcal{L}_{q_B}(\mathcal{A}_{\Delta,\mathcal{A}})$ and $\bar{s}(x_j^{[\epsilon]}) = s(x_j)$, for all $j \in [1..n_0]$, by definition, we obtain the result.

“<” The reverse implication is proven by induction on the structure of the tree $t \in \mathcal{L}_{q_B}(\mathcal{A}_{\Delta,\mathcal{A}})$ such that $S \models^{\bar{s}} \Theta(t)$. Since $t \in \mathcal{L}_{q_B}(\mathcal{A}_{\Delta,\mathcal{A}})$, there is a transition $q_B \xrightarrow{t(\epsilon)} (q_{B1}, \dots, q_{B_\ell}) \in \delta_\Delta$ such that $t(\epsilon) = \alpha_\rho$ for some rule $\rho$ of the form above and $t|_i \in \mathcal{L}_{q_{B_i}}(\mathcal{A}_{\Delta,\mathcal{A}})$ for all $i \in [1..\ell]$. Meanwhile $S \models^{\bar{s}} t(\epsilon) * \ast_{i=1}^\ell \Theta(t|_i)^{[i]}$, thus we can decompose the structure as $S = S_0 \bullet \dots \bullet S_\ell$, such that $S_0 \models^{\bar{s}} \alpha_\rho$ and $S_i \models^{\bar{s}} \Theta(t|_i)^{[i]} * \ast_{j=1}^{n_i} z_{i,j}^{[\epsilon]} = x_j^{[i]}$ for all $i \in [1..\ell]$. Note that the additional equalities from $\alpha_\rho$ are necessary to remember the links between the variables from $\rho$. Let $\bar{s}_i$ be a store, such that $\bar{s}_i(z^{[p]}) = \bar{s}(z^{[\ell p]})$, for all $z^{[p]} \in \text{fv}(\Theta(t_i))$ and all $i \in [1..\ell]$. By the inductive hypothesis on $t|_i$, there exists a store $s_i$ such that $S_i \models^{\bar{s}_i} B_i(x_1, \dots, x_{n_i})$ and $s_i(x_j) = \bar{s}_i(x_j^{[\epsilon]})$, for all $j \in [1..n_i]$. We consider a store $s'$ such that $s'(x_j) = \bar{s}(x_j^{[\epsilon]})$, for all $j \in [1..n]$ and $s'(y_j) = \bar{s}(y_j^{[\epsilon]})$, for all $j \in [1..m]$. For all $i \in [1..\ell]$ and $j \in [1..n_i]$ we have $s_i(x_j) = \bar{s}_i(x_j^{[\epsilon]}) = \bar{s}(x_j^{[i]}) = \bar{s}(z_{i,j}^{[\epsilon]}) = s'(z_{i,j})$, because $z_{i,j}^{[\epsilon]} = x_j^{[i]}$ holds for $\bar{s}$ in the empty structure. Therefore $S_i \models^{\bar{s}'} \Delta B_i(z_{i,1}, \dots, z_{i,n_i})$, for all $i \in [1..\ell]$. Moreover $S_0 \models^{\bar{s}'} \psi$, and by composing the structures and using $\rho$, we obtain $S \models^{\bar{s}'} \Delta B(x_1, \dots, x_n)$.

(2) To show $[\mathcal{A}] = [\mathcal{A}_t]_{\Delta_A}$ we prove the following equivalence: for all structures $S$ and states $q_0 \in \mathcal{Q}$, there exists a tree $t \in \mathcal{L}_{q_0}(\mathcal{A})$ and a store $\bar{s}$ such that $S \models^{\bar{s}} \Theta(t)$ iff there exists a store $s$ such that $S \models^{\bar{s}}_{\Delta_A} A_{q_0}(x_1, \dots, x_{\#q_0})$ and $\bar{s}(x_j) = \bar{s}(x_j^{[\epsilon]})$, for all $j \in [1..\#q_0]$.

“⇒” We reason by induction on the structure of the tree $t \in \mathcal{L}_{q_0}(\mathcal{A})$, such that $S \models^{\bar{s}} \Theta(t)$. Since $t \in \mathcal{L}_{q_0}(\mathcal{A})$, there is a transition $q_0 \xrightarrow{t(\epsilon)} (q_1, \dots, q_\ell) \in \delta$ such that $t|_i \in \mathcal{L}_{q_i}(\mathcal{A})$, for all $i \in [1..\ell]$. Meanwhile $S \models^{\bar{s}} t(\epsilon) * \ast_{i=1}^\ell \Theta(t|_i)^{[i]}$ thus, we can decompose the structure $S = S_0 \bullet \dots \bullet S_\ell$, such that $S_0 \models^{\bar{s}} t(\epsilon)$ and $S_i \models^{\bar{s}} \Theta(t|_i)^{[i]}$. Let $\bar{s}_i$ be a store, such that $\bar{s}_i(z^{[p]}) = \bar{s}(z^{[\ell p]})$, for all $z^{[p]} \in \text{fv}(\Theta(t_i))$ and all $i \in [1..\ell]$. By the inductive hypothesis on $t|_i$, there exists a store $s_i$ such that $S_i \models^{\bar{s}_i}_{\Delta_A} A_{q_i}(x_1, \dots, x_{\#q_i})$ and $s_i(x_j) = \bar{s}_i(x_j^{[\epsilon]})$ for all $j \in [1..\#q_i]$. We consider a store $s'$, such that $s'(x_j) = \bar{s}(x_j^{[\epsilon]})$, for all $j \in [1..\#q_0]$, $s'(x_j^{[i]}) = s_i(x_j)$, for all $i \in [1..\ell]$ and all $j \in [1..\#q_i]$, and $s'(z) = \bar{s}(z)$, for all other variables $z \in \text{fv}(t(\epsilon))$. Then $S_i \models^{\bar{s}'}_{\Delta_A} A_{q_i}(x_1^{[i]}, \dots, x_{\#q_i}^{[i]})$ and $S_0 \models^{\bar{s}'} t(\epsilon)[x_1^{[\epsilon]}/x_1, \dots, x_{\#q_0}^{[\epsilon]}/x_{\#q_0}]$ thus, by composing the structures, we obtain $S \models^{\bar{s}'}_{\Delta_A} A_{q_0}(x_1, \dots, x_{\#q_0})$.

“<” The reverse is shown by induction on the definition of $S \models^{\bar{s}}_{\Delta_A} A_{q_0}(x_1, \dots, x_{\#q_0})$. Then there exists a rule in $\Delta_A$ of the form (4.1) and we can decompose the structure $S = S_0 \bullet \dots \bullet S_\ell$ such that $S_0 \models^{\bar{s}'} \alpha[x_1^{[\epsilon]}/x_1, \dots, x_{\#q_0}^{[\epsilon]}/x_{\#q_0}]$ and $S_i \models^{\bar{s}'}_{\Delta_A} A_{q_i}(x_1^{[i]}, \dots, x_{\#q_i}^{[i]})$, for all $i \in [1..\ell]$, where $\bar{s}'$ is a store that agrees with $s$ over $\{x_1, \dots, x_{\#q_i}\}$. For all $i \in [1..\ell]$, we consider a store $s_i$ such that $s_i(x_j) = s'(x_j^{[i]})$. We have $S_i \models^{\bar{s}_i}_{\Delta_A} A_{q_i}(x_1, \dots, x_{\#q_0})$ and, by the inductive hypothesis, there exists a tree $t_i \in \mathcal{L}_{q_i}(\mathcal{A})$ and a store $\bar{s}_i$ such that $\sigma_i \models^{\bar{s}_i} \Theta(t_i)$ and $\bar{s}_i(x_j^{[\epsilon]}) = s_i(x_j)$, for all $j \in [1..\#q_i]$. Let $\bar{s}$ be a store such that:
▷ $\bar{s}(x_j^{[\epsilon]}) \stackrel{\text{def}}{=} s(x_j)$, for all $j \in [1..\#q_0]$,

▷ $\bar{s}(y_j^{[\epsilon]}) \stackrel{\text{def}}{=} s'(y_j^{[\epsilon]})$, for all $j \in [1..m]$,

▷ $\bar{s}(z^{[\ell p]}) \stackrel{\text{def}}{=} \bar{s}_i(z^{[p]})$, for all $i \in [1..\ell]$ and all $z^{[p]} \in \text{fv}(\Theta(t_i))$.

Note that $\bar{s}$ is well defined because $\bar{s}_i(z^{[p]}) = \bar{s}_j(z^{[p]}) = s'(z^{[p]})$, for all $z^{[p]} \in \text{fv}(\Theta(t_i)) \cap \text{fv}(\Theta(t_j))$. We have $S_i \models^{\bar{s}} \Theta(t_i)^{[i]}$, for all $i \in [1..\ell]$ and $S_0 \models^{\bar{s}} \alpha$, thus $S \models^{\bar{s}} \Theta(t)$, where $t$ is the tree consisting of a root labelled by $\alpha$ and children $t_i$, for $i \in [1..\ell]$. Since $t \in \mathcal{L}_{q_0}(\mathcal{A})$ and $\bar{s}(x_j^{[\epsilon]}) = s(x_j)$ for all $j \in [1..\#q_0]$ by definition, we obtain the result.

To show $[[\mathcal{A}]'] \subseteq [[\mathcal{A}_t]]'_{\Delta_A}$, let $(S, \mathfrak{d}) \in [[\mathcal{A}]']^c$, where $S = (U, \sigma)$ is a structure and $\mathfrak{d} \subseteq U \times U$ is a symmetric relation. Then there exists a tree $t \in \mathcal{L}(\mathcal{A})$ and a store $\mathfrak{s}$ canonical for $\Theta(t)$, such that $S \models^{\mathfrak{s}} \Theta(t)$ and, for each $(u, v) \in \mathfrak{d}$, there exist variables $x \in \mathfrak{s}^{-1}(u)$ and $y \in \mathfrak{s}^{-1}(v)$ such that the disequality $x \neq y$ occurs in $\Theta(t)$. Let $\theta$ be the accepting run of $\mathcal{A}$ over $t$. By a depth-first traversal of $\theta$, we build a complete unfolding $A_t \Rightarrow_{\Delta_A}^* \Theta(t)^{\exists}$. Since $S \models^{\mathfrak{s}} \Theta(t)$, we obtain $(S, \mathfrak{d}) \in [[\mathcal{A}_t]]'_{\Delta_A}$, by Definition 3.1. Conversely, to show $[[\mathcal{A}]'] \supseteq [[\mathcal{A}_t]]'_{\Delta_A}$, let $(S, \mathfrak{d}) \in [[\mathcal{A}_t]]'_{\Delta_A}$, where $S = (U, \sigma)$ is a structure and $\mathfrak{d} \subseteq U \times U$ is a symmetric relation. Then, there exists a complete unfolding $A_t \Rightarrow_{\Delta_A}^* \exists x_1 \dots \exists x_n$, $\psi$, where $\psi$ is a qpf formula, and a store $\mathfrak{s}$ canonical for $\psi$, such that $S \models^{\mathfrak{s}} \psi$ and, for all $(u, v) \in \mathfrak{d}$ there exist variables $x \in \mathfrak{s}^{-1}(u)$ and $y \in \mathfrak{s}^{-1}(v)$, such that the disequality $x \neq y$ occurs in $\psi$. By induction on the length of the unfolding, one can build an accepting run $\theta$ of $\mathcal{A}$, that recognizes a tree $t \in \mathcal{L}(\mathcal{A})$, such that $\Theta(t)$ differs from $\psi$ by an $\alpha$-renaming and permutation of atoms via commutativity and associativity of the separating conjunction. Hence $(S, \mathfrak{d}) \in [[\Theta(t)^{\exists}]]'$, thus $(S, \mathfrak{d}) \in [[\mathcal{A}]']$. $\square$

**C.5.** *Proof of Lemma 4.23.* (1) Let $t' \in \mathcal{L}(A_{\Delta,A}^I)$ be a tree. Since $A_{\Delta,A}^I$ was obtained from $A_{\Delta,A}$ by removing relation and disequality atoms from the labels of its 1-transitions, there exists a tree $t \in \mathcal{L}(A_{\Delta,A})$, such that $\text{dom}(t) = \text{dom}(t')$ and $\Theta(t) = \Theta(t') * \ast_{i=1}^n r_i(z_{i,1}, \dots, z_{i,k_i}) * \ast_{j=1}^m y_{j,1} \neq y_{j,2}$ modulo reordering of atoms, for some relation symbols $r_i$ and variables $z_{i,1}, \dots, z_{i,k_i}$, $y_{j,1}, y_{j,2}$. By Lemma 4.13, $\Theta(t)$ is satisfiable, hence there exists a structure $(U, \sigma)$ and a store $\mathfrak{s}$, such that $(U, \sigma) \models^{\mathfrak{s}} \Theta(t)$. We define the interpretation $\sigma'(r) = \sigma(r) \setminus \{\langle \mathfrak{s}(z_{i,1}), \dots, \mathfrak{s}(z_{i,k_i}) \rangle \mid i \in [1..n], r_i = r\}$, for all $r \in \mathbb{R}$. It is easy to check that $(U, \sigma') \models^{\mathfrak{s}} \Theta(t')$, hence $\Theta(t')$ is satisfiable. Since the choice of $t'$ was arbitrary, we obtain that $A_{\Delta,A}^I$ is all-satisfiable.

(2) Let $t' \in \mathcal{L}(A_{\Delta,A}^I)$ be a tree. By the construction of $A_{\Delta,A}^I$ from $A_{\Delta,A}$, there exists a tree $t \in \mathcal{L}(A_{\Delta,A})$, such that $\text{dom}(t) = \text{dom}(t')$ and $\Theta(t) = \Theta(t') * \ast_{i=1}^n r_i(z_{i,1}, \dots, z_{i,k_i}) * \ast_{j=1}^m y_{j,1} \neq y_{j,2}$ modulo reordering of atoms, for some relation symbols $r_i$ and variables $z_{i,1}, \dots, z_{i,k_i}$, $y_{j,1}, y_{j,2}$. Let $Y = \bigcup_{j=1}^m \{y_{j,1}, y_{j,2}\}$ be the set of variables occurring in disequality atoms. By Lemma 4.7, each 1-transition of $A_{\Delta,A}$ occurs exactly once in each accepting run, hence $n \le \text{card}(\delta_\Delta^1) \cdot \text{maxRelAtoms}(\Delta)$, $\text{card}(Y) \le \text{card}(\delta_\Delta^1) \cdot \text{maxVars}(\Delta)$. By Lemma 2.10 (2, 3), $\text{tw}(\Theta(t')^\exists) \le \text{tw}(\Theta(t)^\exists) + n + \text{card}(Y) \le \text{tw}(\Theta(t)^\exists) + \text{card}(\delta_\Delta^1) \cdot (\text{maxRelAtoms}(\Delta) + \text{maxVars}(\Delta))$. Since the choice of $t'$ was arbitrary, we obtain that $[[A_{\Delta,A}^I]]$ is treewidth bounded, more precisely $\text{tw}([A_{\Delta,A}^I]) \le \text{tw}([A_{\Delta,A}]) + \text{card}(\delta_\Delta^1) \cdot (\text{maxRelAtoms}(\Delta) + \text{maxVars}(\Delta))$.

(3) Let $t \in \mathcal{L}(A_{\Delta,A})$ be a tree. By the construction of $A_{\Delta,A}^I$ from $A_{\Delta,A}$, there exists a tree $t' \in \mathcal{L}(A_{\Delta,A}^I)$, such that $\text{dom}(t') = \text{dom}(t)$ and $\Theta(t) = \Theta(t') * \ast_{i=1}^n r_i(z_{i,1}, \dots, z_{i,k_i}) * \ast_{j=1}^m y_{j,1} \neq y_{j,2}$ modulo reordering of atoms, for some relation symbols $r_i$ and variables $z_{i,1}, \dots, z_{i,k_i}$, $y_{j,1}, y_{j,2}$. Let $Y = \bigcup_{i=1}^n \{z_{i,1}, \dots, z_{i,k_i}\}$ be the set of variables occurring in relation atoms.
By Lemma 4.7, each 1-transition of $\mathcal{A}_{\Delta,A}$ occurs exactly once in each accepting run, hence $\text{card}(Y) \le \text{card}(\delta_{\Delta}^1) \cdot \text{maxVars}(\Delta)$. By Lemma 2.10 (4) $\text{tw}(\Theta(t)^{\exists}) \le \text{tw}(\Theta(t')^{\exists}) + \text{card}(Y) \le \text{tw}(\Theta(t')^{\exists}) + \text{card}(\delta_{\Delta}^1) \cdot \text{maxVars}(\Delta)$. Since the choice of $t$ was arbitrary, we obtain that $[[\mathcal{A}_{\Delta,A}]]$ is treewidth bounded, more precisely $\text{tw}([[]\mathcal{A}_{\Delta,A}]) \le \text{tw}([[]\mathcal{A}_{\Delta,A}^I]) + \text{card}(\delta_{\Delta}^1) \cdot \text{maxVars}(\Delta)$. $\square$

**C.6.** *Proof of Lemma 4.25.* (1) Let $t' \in \mathcal{L}(\mathcal{A}_{\Delta,A}^{II})$ be a tree. Since $\mathcal{A}_{\Delta,A}^{II}$ was obtained from $\mathcal{A}_{\Delta,A}^I$ by removing equality atoms from the labels of its 1-transitions (2), there exists a tree $t \in \mathcal{L}(\mathcal{A}_{\Delta,A}^I)$, such that $\text{dom}(t) = \text{dom}(t')$ and $\Theta(t) = \Theta(t') * \psi$ where $\psi$ is a conjunction of equality atoms. By Lemma 4.23 (1), $\Theta(t)$ is satisfiable, hence there exists a structure $S$ and a store $s$ such that $S \models^{\mathfrak{s}} \Theta(t)$. We immediately obtain $S \models^{\mathfrak{s}} \Theta(t')$, hence $\Theta(t')$ is satisfiable. Since the choice of $t'$ was arbitrary, we obtain that $\mathcal{A}_{\Delta,A}^{II}$ is all-satisfiable.
(2) Let $t' \in \mathcal{L}(\mathcal{A}_{\Delta,A}^{II})$ be a tree and $\theta'$ be an accepting run over $t'$. We shall build a tree $t \in \mathcal{L}(\mathcal{A}_{\Delta,A}^I)$ related to $t'$ and $\theta'$ and show that $\text{tw}([[]\Theta(t')^{\exists}]) \le \text{tw}([[]\Theta(t)^{\exists}]) + K$, where $K$ is constant that does not depend on the choice of $t'$. The idea of the construction of $t$ from $t'$ is to add resets before and after each 1-transition in the run $\theta'$, so that the equalities removed by the transformation from $\delta_{\Delta}^I$ to $\delta_{\Delta}^{II}$ can be added back, without changing the set of models of $\Theta(t')^{\exists}$. To avoid unnecessary complications, we consider each 1-transition separately (recall that there are finitely many 1-transitions in $\mathcal{A}_{\Delta,A}^{II}$).

We refer to Figure 16 for an illustration of this construction. For a given position $p \in \text{dom}(t')$ such that $\theta'(p) \xrightarrow{t'(p)} (\theta'(p1), \dots, \theta'(p\ell)) \in (\delta_{\Delta}^{II})^1$, we separate the run $\theta'$ into a context $\theta_{p \leftarrow \theta(p)}^{\text{init}}$, before the 1-transition, and $\ell \stackrel{\text{def}}{=} \rho(t'(p))$ runs $\theta_1, \dots, \theta_\ell$, after the 1-transition, i.e., $\theta_{p \leftarrow \theta(p)}^{\text{init}}(r) \stackrel{\text{def}}{=} \theta'(r)$ for every $r \in \text{dom}(t')$ that is not a suffix of $p$, and $\theta_i(r) \stackrel{\text{def}}{=} \theta'(pir)$ for every $i \in [1..\ell]$ and position $r$ with $pir \in \text{dom}(t')$.

<figure><img src="image_25.png" /><figcaption>Figure 16: Construction of $t$ from $t'$ (Lemma 4.25)</figcaption></figure>

Then, we build $t$ and the associated run $\theta$ by combining successive partial runs:

* start $\theta$ with $\theta_{p \leftarrow \theta(p)}^{\text{init}}$, i.e., no change from $\theta'$ above position $p$,

* add a $\theta'(p)$-reset $\theta_{u \leftarrow \theta'(p)} \in \mathcal{R}_{\theta'(p)}^{\infty}(\mathcal{A}_{\Delta,A}^I)$ at position $p$; such a reset exists by Lemma 4.18 because $\theta'(p) \in \mathcal{R}_{\theta'(p)}^{\infty}((\delta_{\Delta}^{II})^1) \cap \mathcal{R}_{\theta'(p)}^{\infty}((\delta_{\Delta}^{II})^\infty)$, since $\theta'(p)$ belong to a non-trivial SCC,
▷ pursue at position *pu* with the transition $\theta'(p) \xrightarrow{\alpha_p} (\theta'(p1), \dots, \theta'(p\ell)) \in (\delta_\Delta^I)^1$ corresponding to the original 1-transition from $\mathcal{A}_{\Delta,A}^I$, after adding back the equalities removed by the transformation,

▷ for every $i \in [1..\ell]$, introduce at position *pui* a $\theta'(pi)$-reset $\theta_{v_i \leftarrow \theta'(pi)} \in \mathcal{R}_{\theta'(pi)}^\infty(\mathcal{A}_{\Delta,A}^{II})$; such a reset exists by Lemma 4.18 since $\theta'(pi) \in ((\delta_\Delta^{II})^1)^\bullet \cap ((\delta_\Delta^{II})^\infty)$ is a pivot state,

▷ continue with $\theta_i$ at position $puiv_i$, for every $i \in [1..\ell]$.

**Fact C.6.** $\mathrm{tw}([\Theta(t')^3]) \le \mathrm{tw}([\Theta(t)^3]) + K_1$, where $K_1 \le \mathrm{maxVars}(\Delta)$ is the maximal number of $i$-variables, $i \in \mathbb{N} \cup \{\epsilon\}$, in any 1-transition of $\mathcal{A}_{\Delta,A}^{II}$.

*Proof.* Let $\phi \stackrel{\mathrm{def}}{=} *_{p}$ not a prefix of $r$ $t'(r)^{[r]} * *_{pir \in \mathrm{dom}(t')} t'(pir)^{[puiv_i r]}$, which corresponds to the characteristic formula $\Theta(t')$ without the 1-transition at position $p$, and with the new position labels in $t$. Now $\Theta(t) = \phi * \psi$ where $\psi$ is the separating conjunction of all $t(pr)^{[pr]}$ with $pr \in \mathrm{dom}(t)$ and $uiv_i$ not the prefix of $r$ for any $i \in [1..\ell]$ (position $pr$ is either the start of the 1-transition or part of one of the reset contexts). Let $F \stackrel{\mathrm{def}}{=} \mathrm{fv}(\phi) \cap \mathrm{fv}(\psi)$ and $\eta \stackrel{\mathrm{def}}{=} *\{x=y \mid x, y \in V_f, x \approx_\psi y\}$. Then, $F$ contains the variables at the extremity of the added part from $t'$ to $t$, i.e., $F = \{x_k^{[p]} \mid k \in [1..\#t(p)]\} \cup \{x_j^{[puiv_i]} \mid i \in [1..\ell], j \in [1..\#t(pui)]\}$. These variables exactly correspond to the parameters appearing in the 1-transition at position $p$ of $t'$, i.e., $F = \{x_k^{[p]} \mid k \in [1..\#t'(p)]\} \cup \{x_j^{[pi]} \mid i \in [1..\ell], j \in [1..\#t'(pi)]\}$, hence $\mathrm{card}(F) \le K_1 \le \mathrm{maxVars}(\Delta)$. By Definition 4.11 (2), $\phi$ does not induce equalities between variables of $F$. On the other hand, $\psi$ only induces equalities between persistent variables of $F$, thanks to the introduced reset paths. These equalities $\eta$ correspond exactly to those occurring in $t'(p)$, thus $\phi * \eta$ is equal to $\Theta(t')$, modulo a renaming of the variables. Now $\phi * \psi$ is satisfiable (since $\mathcal{A}_{\Delta,A}^I$ is all-satisfiable), thus by Lemma 2.11, we obtain $\mathrm{tw}([\Theta(t')^3]) = \mathrm{tw}([\phi * \eta]^3) \le \mathrm{tw}([\phi * \psi]^3]) + K_1 = \mathrm{tw}([\Theta(t)^3]) + K_1$. $\square$

After doing this transformation ($t'$ to $t$) for all 1-transitions, the final tree $t$ satisfies $t \in \mathcal{L}(\mathcal{A}_{\Delta,A}^I)$ since all the added transitions (1-transition or reset) appear in $\delta_\Delta^I$. With the inequality at each step (Fact C.6) and since each 1-transition of $\delta_\Delta^{II}$ occurs exactly once in the initial tree $t'$ (Lemma 4.7), we get $\mathrm{tw}([\Theta(t')^3]) \le \mathrm{tw}([\Theta(t)^3]) + K$, where $K = \mathrm{card}((\delta_\Delta^{II})^1) \cdot K_1 \le \mathrm{card}((\delta_\Delta^{II})^1) \cdot \mathrm{maxVars}(\Delta)$. As $t'$ has been chosen arbitrary and $\mathrm{card}((\delta_\Delta^{II})^1) = \mathrm{card}((\delta_\Delta^I)^1)$, we conclude that $\mathrm{tw}([\mathcal{A}_{\Delta,A}^{II}]) \le \mathrm{tw}([\mathcal{A}_{\Delta,A}^I]) + \mathrm{card}((\delta_\Delta^I)^1) \cdot \mathrm{maxVars}(\Delta)$.

(3) Let $t \in \mathcal{L}(\mathcal{A}_{\Delta,A}^I)$. By the construction of $\mathcal{A}_{\Delta,A}^{II}$ from $\mathcal{A}_{\Delta,A}^I$, there exists a tree $t' \in \mathcal{L}(\mathcal{A}_{\Delta,A}^{II})$ such that $\mathrm{dom}(t) = \mathrm{dom}(t')$ and $\Theta(t) = \Theta(t') * \psi$ where $\psi$ is a conjunction of equalities. $\Theta(t')$ is a qpf formula thus by Lemma 2.10 (1), we get $\mathrm{tw}([\Theta(t')^3]) = \mathrm{tw}([\Theta(t') * \psi]^3]) \le \mathrm{tw}([\Theta(t')^3])$. As $t$ has been chosen arbitrary, we obtain that $\mathrm{tw}([\mathcal{A}_{\Delta,A}^I]) \le \mathrm{tw}([\mathcal{A}_{\Delta,A}^{II}])$.

**C.7.** *Proof of Lemma 4.28.* (1) By Lemma 4.27, $\mathcal{L}(\widetilde{\mathcal{A}}_{\Delta,A}^{II}) = \mathcal{L}(\mathcal{A}_{\Delta,A}^{II})$, hence $\widetilde{\mathcal{A}}_{\Delta,A}^{II}$ is all-satisfiable, because $\mathcal{A}_{\Delta,A}^{II}$ is all-satisfiable, by Lemma 4.25 (1). Since $\widetilde{\mathcal{B}}_i$ is obtained by removing zero or more transitions from $\widetilde{\mathcal{A}}_{\Delta,A}^{II}$, we have $\mathcal{L}(\widetilde{\mathcal{B}}_i) \subseteq \mathcal{L}(\widetilde{\mathcal{A}}_{\Delta,A}^{II})$, hence $\mathcal{B}_i$ is all-satisfiable.
Let $\tilde{\delta}^1$ be any of the sets $\tilde{\delta}_1^1, \dots, \tilde{\delta}_m^1$. We prove that $\tilde{B} \stackrel{\text{def}}{=} (\Sigma, \tilde{Q}_{\Delta}^I, (q_A, \emptyset), \tilde{\delta}^1 \uplus \tilde{\delta}^{\infty})$ is choice-free. To this end, we define the following labeling of transitions:

$$ \Lambda(\tau) \stackrel{\text{def}}{=} \begin{cases} 1 & \text{if } \tau \in \tilde{\delta}^1 \\ \infty & \text{if } \tau \in \tilde{\delta}^{\infty} \end{cases} $$

Let $h : \tilde{Q}_{\Delta}^I \to Q_{\Delta}^I$ be the function defined as $h((q, a)) \stackrel{\text{def}}{=} q$, for all $(q, a) \in \tilde{Q}_{\Delta}^I$. For each SCC $\tilde{S}$ of $\tilde{B}$, we have $h(\tilde{S}) \subseteq S$, for an SCC $S$ of $A_{\Delta,A}^{II}$, by the definitions of $\tilde{A}_{\Delta,A}^{II}$ and $\tilde{B}$. Since $A_{\Delta,A}^{II}$ is choice-free, by Lemma 4.25 (1), we can extend the labeling $\Lambda$ to the SCCs of $\tilde{B}$, as follows:

$$ \Lambda(\tilde{S}) \stackrel{\text{def}}{=} \begin{cases} 1 & \text{if } h(\tilde{S}) \subseteq S, \text{ for some 1-SCC } S \text{ of } A_{\Delta,A}^{II} \\ \infty & \text{if } h(\tilde{S}) \subseteq S, \text{ for some } \infty\text{-SCC } S \text{ of } A_{\Delta,A}^{II} \end{cases} $$

We prove first the following fact:

**Fact C.7.** Let $\tilde{S}$ be an SCC of $\tilde{B}$, such that $\Lambda(\tilde{S}) = 1$. Then $h(\tilde{S})$ is a 1-SCC of $A_{\Delta,A}^{II}$. Moreover, $h(\tilde{S})$ is linear if $\tilde{S}$ is linear.

*Proof.* By the definition of $\Lambda$, we have that $h(\tilde{S}) \subseteq S$, for a 1-SCC of $A_{\Delta,A}^{II}$, hence, for the first point, it suffices to prove that $h(\tilde{S}) = S$. Suppose, for a contradiction, that there exists a state $q \in S \setminus h(\tilde{S})$. Let $q' \in h(\tilde{S})$ be a state. Since $S$ is an SCC of $A_{\Delta,A}^{II}$, we have $q \rightsquigarrow q'$ $\rightsquigarrow q$ in $A_{\Delta,A}^{II}$. Since $q' \in h(\tilde{S})$, there exists an injective partial mapping $a' : [1..\#q'] \to [1..M]$ such that $(q', a') \in \tilde{S}$. By the construction of $\tilde{A}_{\Delta,A}^{II}$, we obtain $(q', a') \rightsquigarrow (q, a)$ in $\tilde{A}_{\Delta,A}^{II}$, for some injective partial mapping $a : [1..\#q] \to [1..M]$. To show a contradiction, we prove that $(q, a) \rightsquigarrow (q', a')$ in $\tilde{A}_{\Delta,A}^{II}$, hence $q' \in h(\tilde{S})$. By the construction of $\tilde{A}_{\Delta,A}^{II}$, there exist injective partial mappings $a_1, a_2, \dots : [1..\#q'] \to [1..M]$, such that $(q, a) \rightsquigarrow (q', a_1) \rightsquigarrow (q', a_2) \rightsquigarrow \dots$. Because the underlying transitions of $A_{\Delta,A}^{II}$ along this path are $\infty$-transitions, the mappings $a_1, a_2, \dots$ are undefined everywhere except for $\mathfrak{P}_{A_{\Delta,A}^{II}}(q')$, where they are defined. Because these transitions are from $\bullet S \bullet$, each of these mappings can be obtained from the previous one by composition with a permutation over $\mathfrak{P}_{A_{\Delta,A}^{II}}(q')$. Since all such permutations can be enumerated in this was, this leads to $(q', a'_1) \rightsquigarrow (q', a')$ in $\tilde{A}_{\Delta,A}^{II}$, i.e., contradiction.

For the second point, suppose, for a contradiction, that $h(\tilde{S})$ is not linear. Then, there exists a transition $q_0 \stackrel{\alpha}{\to} (q_1, \dots, q_\ell)$ such that $q_0, q_i, q_j \in h(\tilde{S})$, for some indices $1 \le i < j \le \ell$. Since $h(\tilde{S})$ is a connected component of $A_{\Delta,A}^{II}$, we have $q_i \rightsquigarrow q_0$ and $q_j \rightsquigarrow q_0$ in $A_{\Delta,A}^{II}$. Let $a_0, \dots, a_\ell$ be injective partial mappings, such that $(q_0, a_0) \stackrel{\alpha}{\to} ((q_1, a_1), \dots, (q_\ell, a_\ell))$ is a transition of $\tilde{B}$. By the above argument, we obtain $(q_i, a_i) \rightsquigarrow (q_0, a_0)$ and $(q_j, a_j) \rightsquigarrow (q_0, a_0)$, hence $\tilde{S}$ is non-linear, contradiction. $\square$

Back to the main proof, we check the points of Definition 4.5 below:

(1) The SCC graph of $\tilde{B}$ is a tree, by the choice of the set $\tilde{\delta}^1$ corresponding to $\tilde{B}$. Moreover, each non-root SCC of $\tilde{B}$ is entered by exactly one branch, since this is already the case for the choice-free automaton $A_{\Delta,A}^{II}$.
(2a) Let $\tilde{S}$ be a linear SCC of $\tilde{\mathcal{B}}$, such that $\Lambda(\tilde{S}) = 1$. By Fact C.7, $h(\tilde{S})$ is a linear 1-SCC of $\mathcal{A}_{\Delta,A}^{II}$, hence $\text{card}(h(\tilde{S})^\bullet) = 1$. Then, we obtain $\text{card}(\tilde{S}^\bullet) = 1$.

(2b) Let $\tilde{\tau} = (q_0, a_0) \stackrel{\alpha}{\to} ((q_1, a_1), \dots, (q_\ell, a_\ell))$ be a transition of $\tilde{\mathcal{B}}$. Then $\Lambda(\tilde{\tau}) = 1$ iff $\tilde{\tau} \in \tilde{\delta}^1$, by the definition of $\Lambda$. “⇒” Assume that $\tilde{\tau} \in \tilde{\delta}^1$. Then, the underlying transition $\tau = q_0 \stackrel{\alpha}{\to} (q_1, \dots, q_\ell)$ is a 1-transition of $\mathcal{A}_{\Delta,A}^{II}$. Since $\mathcal{A}_{\Delta,A}^{II}$ is choice-free, we have that $\tau \in S^\bullet$, for some linear 1-SCC $S$ of $\mathcal{A}_{\Delta,A}^{II}$. Let $\tilde{S}$ be an SCC of $\tilde{\mathcal{B}}$ such that $h(\tilde{S}) \subseteq S$. Then $\Lambda(\tilde{S}) = 1$, by the definition of $\Lambda$. Suppose, for a contradiction that $\tilde{S}$ is non-linear. Then, $h(\tilde{S})$ is non-linear, hence $S$ is non-linear, contradiction. Finally, $\tilde{\tau} \in \tilde{S}^\bullet$ follows from $\tau \in S^\bullet$. “<” Assume that $\tilde{\tau} \in \tilde{S}^\bullet$, for a linear SCC $\tilde{S}$ of $\tilde{\mathcal{B}}$, such that $\Lambda(\tilde{S}) = 1$. Then $h(\tilde{S})$ is a linear 1-SCC of $\mathcal{A}_{\Delta,A}^{II}$, by Fact C.7. Moreover, $\tau \in h(\tilde{S})^\bullet$, where $\tau$ is the underlying transition of $\tilde{\tau}$ from $\mathcal{A}_{\Delta,A}^{II}$. Hence $\tau$ is a 1-transition of $\mathcal{A}_{\Delta,A}^{II}$ and $\tilde{\tau} \in \tilde{\delta}^1$, by the choice of $\tilde{\delta}^1$.

(2c) By Fact C.7, $\Lambda(\tilde{S}) = 1$ iff $h(\tilde{S})$ is a 1-SCC of $\mathcal{A}_{\Delta,A}^{II}$, for each SCC $\tilde{S}$ of $\tilde{\mathcal{B}}$. “⇒” Assume that $h(\tilde{S})$ is a 1-SCC of $\mathcal{A}_{\Delta,A}^{II}$. Since $\mathcal{A}_{\Delta,A}^{II}$ is choice-free, then $h(\tilde{S})$ is the root of the SCC tree of $\mathcal{A}_{\Delta,A}^{II}$ or $\tilde{S} = \{\tilde{\tau}\}$, for some transition $\tilde{\tau}$ of $\tilde{\mathcal{B}}$, such that $\Lambda(\tilde{\tau}) = 1$. In the first case, $h(\tilde{S})$ has no incoming transition, hence $\tilde{S}$ is the root of the SCC tree of $\tilde{\mathcal{B}}$. In the second case, $\tilde{h}(\tilde{S}) = \{\tilde{\tau}\}$, for a 1-transition $\tilde{\tau}$ of $\mathcal{A}_{\Delta,A}^{II}$. Then, $\tilde{S} = \{\tilde{\tau}\}$, for a transition $\tilde{\tau}$, such that $\Lambda(\tilde{\tau}) = 1$, by the definition of $\Lambda$. “<” If $h(\tilde{S})$ is the root of the SCC tree of $\mathcal{A}_{\Delta,A}^{II}$, then $\tilde{S}$ has no incoming transitions, hence it is the root of the SCC tree of $\tilde{\mathcal{B}}$. If $\tilde{h}(\tilde{S}) = \{\tilde{\tau}\}$, for a 1-transition $\tilde{\tau}$ of $\mathcal{A}_{\Delta,A}^{II}$, we obtain $\tilde{S} = \{\tilde{\tau}\}$, for a transition $\tilde{\tau}$ of $\tilde{\mathcal{B}}$, such that $\Lambda(\tilde{\tau}) = 1$, by the definition of $\Lambda$.

(2) Since $\mathcal{L}(\tilde{\mathcal{B}}_i) \subseteq \mathcal{L}(\mathcal{A}_{\Delta,A}^{II})$, for each $i \in [1..m]$, we have $\bigcup_{i=1}^m \mathcal{L}(\tilde{\mathcal{B}}_i) \subseteq \mathcal{L}(\mathcal{A}_{\Delta,A}^{II})$. By the definition of $\tilde{\mathcal{B}}_1, \dots, \tilde{\mathcal{B}}_m$, for each accepting run $\theta$ of $\tilde{\mathcal{A}}_{\Delta,A}^{II}$, there exists $i \in [1..m]$, such that $\theta$ is an accepting run of $\tilde{\mathcal{B}}_i$, thus $\mathcal{L}(\mathcal{A}_{\Delta,A}^{II}) \subseteq \bigcup_{i=1}^m \mathcal{L}(\tilde{\mathcal{B}}_i)$. $\square$

### C.8. Proof of Lemma 4.29.
First, we prove the following fact:

**Fact C.8.** Let $t \in \mathcal{L}(\tilde{\mathcal{B}})$ be a tree, $\theta$ be an accepting run of $\tilde{\mathcal{B}}$ over $t$ and $p \in \text{dom}(t)$ be a position such that $\theta(p) = (q, a)$. Then, $x_i^{[p]} \approx_{\Theta(t)} y_{a(i)}^{[r_i]}$, for each $i \in \text{dom}(a)$, such that $r_i$ is the unique position where a variable $y_{a(i)}^{[\epsilon]} \in \mathcal{Y}$ occurs in $\Theta(t)$.

*Proof.* By induction on the structure of $t$. $\square$

<figure><img src="image_26.png" /></figure>

(1) Let $\bar{t} \in \mathcal{L}(\bar{\mathcal{B}})$ be a tree. By the construction of $\bar{\mathcal{B}}$, the accepting run $\bar{\theta}$ of $\bar{\mathcal{B}}$ over $\bar{t}$ can be transformed into an accepting run $\theta$ of $\bar{\mathcal{B}}$ over a tree $t$, such that $\text{dom}(t) = \text{dom}(\bar{t})$, by changing the labels $\bar{\alpha}$ back to the original labels $\alpha$. Since $\bar{\mathcal{B}}$ is all-satisfiable, by Lemma 4.28 (1), the formula $\Theta(t)$ is satisfiable, and let $(\mathcal{U}, \sigma)$ be a structure and $\mathcal{s}$ be a store such that $(\mathcal{U}, \sigma) \models^s \Theta(t)$. However, $\Theta(\bar{t})$ is obtained from $\Theta(t)$ by removing several (dis-)equalities from the labels of 1-transitions and by changing each relation atom $\mathfrak{r}(z_1^{[p]}, \dots, z_{\#\mathfrak{r}}^{[p]})$ into a relation atom $\mathfrak{r}_g(\zeta_\tau(z_{i_1}^{[p]}), \dots, \zeta_\tau(z_{i_k}^{[p]}))$, according to the construction of $\bar{\mathcal{B}}$. Suppose, for a contradiction, that there exist two distinct positions $p_1, p_2 \in \text{dom}(\bar{t})$ such that the relation atoms $\mathfrak{r}_g(\zeta_{\tau_1}(z_{i_1}^{[p_1]}), \dots, \zeta_{\tau_1}(z_{i_k}^{[p_1]}))$ and $\mathfrak{r}_g(\zeta_{\tau_2}(z_{i_1}^{[p_2]}), \dots, \zeta_{\tau_2}(z_{i_k}^{[p_2]}))$ occur in $\Theta(\bar{t})$ and $\zeta_{\tau_1}(z_{i_j}^{[p_1]}) \approx_{\Theta(\bar{t})} \zeta_{\tau_2}(z_{i_j}^{[p_2]})$, for all $j \in [1..k]$. Then, there exist relation atoms $\mathfrak{r}(z_1^{[p_1]}, \dots, z_{\#\mathfrak{r}}^{[p_1]})$
and $\mathbf{r}(z_1^{[p_1]}, \dots, z_{\#\mathbf{r}}^{[p_\mathbf{r}]})$ that occur in $\Theta(t)$, such that $i_1, \dots, i_k \in [1..\#\mathbf{r}]$ and, by Fact C.8 and properties of the renaming, we obtain that $z_j^{[p_1]} \approx_{\Theta(t)} z_j^{[p_2]}$, for all $j \in [1..\#\mathbf{r}]$. This however contradicts the satisfiability of $\Theta(t)$, hence such relation atoms cannot occur in $\Theta(\tilde{t})$. Similarly, we obtain a contradiction if we suppose a disequality atom $\zeta_\tau(x) \neq \zeta_\tau(y)$ occurs in $\Theta(\tilde{t})$ and $\zeta_\tau(x) \approx_{\Theta(\tilde{t})} \zeta_\tau(y)$. Then, $\Theta(\tilde{t})$ is satisfiable and, since the choice of $\tilde{t}$ was arbitrary, $\tilde{B}$ is all-satisfiable.

(2) Let $\tilde{S} = (U, \tilde{\sigma}) \in [[\tilde{B}]]$ be a structure. Then, there exists a tree $\tilde{t} \in \mathcal{L}(\tilde{B})$ and a store $\tilde{s}$ such that $\tilde{S} \models^{\tilde{\delta}} \Theta(\tilde{t})$. Let $\tilde{t}$ be the tree obtained from $\tilde{t}$ by replacing back each label $\tilde{\alpha}$ with the original label $\alpha$, according to the construction of $\tilde{B}$ from $\tilde{B}$. Note that $\mathrm{dom}(\tilde{t}) = \mathrm{dom}(\tilde{t})$ and let $\tilde{\theta}, \tilde{\theta}'$ be two related accepting runs of $\tilde{B}$, $\tilde{B}$ over $\tilde{t}, \tilde{t}'$ respectively. We define a store $\tilde{s}$ over $\mathrm{fv}(\Theta(\tilde{t}))$ as follows. Let $p$ be an arbitrary position in $\mathrm{dom}(\tilde{t})$. Let $(q_0, a_0) \to^{\alpha} ((q_1, a_1), \dots, (q_\ell, a_\ell))$ be the transition taken at $p$ in the run $\tilde{\theta}$. Let $\zeta_\tau$ be the renaming of variables as defined in the transformation. The store $\tilde{s}$ is then defined by:

$$ \begin{array}{l@{\qquad}l} \triangleright \tilde{s}(y_i^{[p]}) & \begin{cases} \tilde{s}(y_i^{[p]}) & \text{if } \tau \notin \tilde{\delta}^1 \\ u_i & \text{if } \tau \in \tilde{\delta}^1 \text{ for some distinct values } u_i \notin \tilde{s}(\mathrm{fv}(\Theta(\tilde{t}))), i \in [1..M] \end{cases} \\ \triangleright \tilde{s}(x_i^{[p]}) & \begin{cases} \tilde{s}(x_j^{[p]}) & \text{if } i \notin \mathrm{dom}(a_0) \text{ and } \zeta_\tau(x_i^{[\epsilon]}) = x_j^{[\epsilon]} \\ u_{a_0(i)} & \text{if } i \in \mathrm{dom}(a_0) \end{cases} \end{array} $$

That is, the store $\tilde{s}$ allocates fresh distinct values for all the persistent variables and re-uses the already given values for the non-persistent ones in $\tilde{s}$, while taking into account their renaming by $\zeta_\tau$. We now consider the structure $\tilde{S} = (U, \tilde{\sigma})$, where $\tilde{\sigma}$ is the interpretation that assigns to each relation symbol $\mathbf{r}$ the set of tuples $\langle \tilde{s}(\xi_1), \dots, \tilde{s}(\xi_{\#\mathbf{r}}) \rangle$ for every relation atom $\mathbf{r}(\xi_1, \dots, \xi_{\#\mathbf{r}})$ in $\Theta(\tilde{t})$. We can now check that $(U, \tilde{\sigma}) \models^{\tilde{\delta}} \Theta(\tilde{t})$. Any two tuples from $\tilde{\sigma}(\mathbf{r})$ defined as above are necessarily distinct, unless the corresponding tuples restricted to non-persistent variables from $\tilde{\sigma}(r_g)$ are not distinct. Similarly, equalities on disequality atoms on non-persistent variables only hold in $\Theta(\tilde{t})$ as they already hold in the renamed form in $\Theta(\tilde{t})$. Finally, equalities and disequalities in $\Theta(\tilde{t})$ involving persistent variables hold by the construction of $\tilde{s}$. But now, every tree decomposition of $\tilde{S}$ is a tree decomposition for $\tilde{S}$. Hence, $\mathrm{tw}(\tilde{S}) \le \mathrm{tw}(\tilde{S})$ and consequently, since the choice of $\tilde{S}$ was arbitrary we have $\mathrm{tw}([\tilde{B}]) \le \mathrm{tw}([\tilde{B}])$.

(3) Let $\tilde{S} = (U, \tilde{\sigma}) \in [[\tilde{B}]]$ be a structure. Then, there exists a tree $\tilde{t} \in \mathcal{L}(\tilde{B})$ and a store $\tilde{s}$, such that $\tilde{S} \models^{\tilde{\delta}} \Theta(\tilde{t})$. Let $\tilde{t} \in \mathcal{L}(\tilde{B})$ be the tree obtained by changing each label $\tilde{\alpha}$ of $\tilde{t}$ into $\tilde{\alpha}$, according to the construction of $\tilde{B}$. We consider the structure $\tilde{S} \stackrel{\mathrm{def}}{=} (U, \tilde{\sigma})$, where $\tilde{\sigma}$ interprets each relation symbol $r_g$ by the set of tuples $\langle \tilde{s}(\zeta_\tau(z_{i_1}^{[p]})), \dots, \tilde{s}(\zeta_\tau(z_{i_k}^{[p]})) \rangle$, such that $r_g(\zeta_\tau(z_{i_1}^{[p]}), \dots, \zeta_\tau(z_{i_k}^{[p]}))$ occurs in $\Theta(\tilde{t})$. Let $\tilde{T}$ be a tree decomposition of $\tilde{S}$. We consider the tree decomposition $\tilde{T}$ obtained by adding the values $\tilde{s}(y_i^{[r_i]})$, where $r_i$ is the unique position where a $\epsilon$-variable $y_i^{[\epsilon]} \in \mathcal{Y}$ occurs in $\Theta(\tilde{t})$, to the label of each node in $\tilde{T}$. Then, $\tilde{T}$ is a tree decomposition of $\tilde{S}$ and moreover $\mathrm{wd}(\tilde{T}) \le \mathrm{wd}(\tilde{T}) + M$. Since the choice of $\tilde{T}$ was arbitrary we obtain $\mathrm{tw}(\tilde{S}) \le \mathrm{tw}(\tilde{S}) + M$. Consequently, since the choice of $\tilde{S}$ was arbitrary and $M \le \mathrm{card}(\tilde{\delta}^1) \cdot \mathrm{maxVars}(\Delta)$, we obtain that $\mathrm{tw}([\tilde{B}]) \le \mathrm{tw}([\tilde{B}]) + \mathrm{card}(\tilde{\delta}^1) \cdot \mathrm{maxVars}(\Delta). \square$
C.9. **Proof of Lemma 4.32.** By hypothesis, $\bar{B}$ has no persistent variables and since the relabeling of 1-transitions introduces no existential quantifiers, then $\mathcal{B}$ has no persistent variables either.

(1) Let $t \in \mathcal{L}(\bar{B})$ be a tree and let $\theta$ be an accepting run of $\bar{B}$ over $t$. Let us consider the run $\theta'$ of $\bar{B}$ obtained by replacing with $\text{emp}$ the labels of the 1-transitions $\tau^{\text{exp}} : q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell) \in \delta^1$. We then define the run $\theta''$ of $\bar{B}$ by replacing each occurrence of a 1-transition $\tau : q_0 \xrightarrow{\text{emp}} (q_1, \dots, q_\ell)$ in $\theta'$ by the partial run $\theta_\tau$ constructed by extending $\tau$ with the resets used in the definition of the transformation, namely:

▷ a pre- $q_0$-reset $\theta_{p_0 \leftarrow q_0}^0 \in \mathcal{R}_{q_0}^{\infty}(\bar{B})$ if $q_0 \in \bullet(\delta^{\infty})$ and,

▷ a post- $q_i$-reset $\theta_{p_i \leftarrow q_i}^i \in \mathcal{R}_{q_i}^{\infty}(\bar{B})$ for each $i \in [1..\ell]$ such that $q_i \in \bullet(\delta^{\infty})$.

<figure><img src="image_27.png" /><figcaption>Figure 17: Expansion of 1-transitions</figcaption></figure>

The relation between $\tau$ from $\theta_\tau$ is illustrated in Figure 17 (a,b). Note that the resets exist according to Lemma 4.18. Then, it is easy to check that $\theta''$ is indeed a run of $\bar{B}$. Let $t'' \in \mathcal{L}(\bar{B})$ be the tree accepted by $\theta''$. Since $\bar{B}$ is all-satisfiable, there exists a store $s$ and a structure $S''$ such that $S'' \models^s \Theta(t'')$. Now, by the definition of $\mathcal{B}$, the label $\alpha$ of each transition $\tau^{\text{exp}} : q_0 \xrightarrow{\alpha} (q_1, \dots, q_\ell) \in \delta^1$ is actually $\omega_0 * \mathbf{\ast}_{j=1}^\ell \omega_j$, where:

$$ \omega_0 = \mathbf{\ast}_{i_1, \dots, i_k \in [1..\#q_0]} \Omega_{t_0}^{\epsilon/\epsilon}(x_{i_1}, \dots, x_{i_k}) $$

$$ \omega_j = \mathbf{\ast}_{i_1, \dots, i_k \in [1..\#q_j]} \Omega_{t_j}^{p_j/j}(x_{i_1}, \dots, x_{i_k}), \text{ for } j \in [1..\ell] $$

and $t_0, t_1, \dots, t_\ell$ are the $\Sigma$-labelled trees of the corresponding resets, respectively $\theta_0, \theta_1, \dots, \theta_\ell$. This construction is illustrated in Figure 17(c). Hence, there exists a substructure $S \sqsubseteq S''$ such that $S \models^s \Theta(t)$. Actually, $S$ is simply obtained from $S''$ by removing all but the tuples introduced by the relation atoms of $\omega_0, \dots, \omega_\ell$, defined along the partial runs $\theta_\tau$ of $\theta''$. Since the choice of $t$ was arbitrary, $\mathcal{B}$ is all-satisfiable.

(2) Let $t' \in \mathcal{L}(\bar{B})$ be a tree. Let $t \in \mathcal{L}(\bar{B})$ be the tree obtained by $t'$ be removing relational atoms from the labels of 1-transitions, that is, reversing the transformation. As both $\mathcal{B}$ and $\bar{B}$ are all-satisfiable, the characteristic formulæ $\Theta(t')$ and $\Theta(t)$ are satisfiable. They differ, moreover, only by finitely many relational atoms. Henceforth, by using Lemma 2.10 (4), we obtain that the difference between the treewidth of their models is bounded by the number of free variables occurring on these atoms, that is, at most $\text{card}(\bar{\delta}^1) \cdot \text{maxVars}(\Delta)$. Then $\text{tw}([\Theta(t')^\exists]) \le \text{tw}([\Theta(t)^\exists]) + \text{card}(\bar{\delta}^1) \cdot \text{maxVars}(\Delta)$ and as the choice of $t'$ was arbitrary, we obtain $\text{tw}([\mathcal{B}]) \le \text{tw}([\bar{B}]) + \text{card}(\bar{\delta}^1) \cdot \text{maxVars}(\Delta)$.

(3) Let $t \in \mathcal{L}(\bar{B})$ be a tree. Let $t' \in \mathcal{L}(\bar{B})$ be the tree obtained from $t$ by replacing the $\text{emp}$-labels of 1-transitions by their corresponding formulæ according to the transformation.
As both $\bar{\mathcal{B}}$ and $\mathcal{B}$ are all-satisfiable, the characteristic formulæ $\Theta(t)$ and $\Theta(t')$ are satisfiable. These formulæ differ only by a finite number of relation atoms, that is, the ones inserted in the labels of the modified 1-transitions. Henceforth, by Lemma 2.10 (3), we obtain that the difference between the treewidth of their models is bounded by the number $K$ of these relation atoms. As the choice of $t$ was arbitrary, we obtain that $\mathrm{tw}(\bar{\mathcal{B}}) \le \mathrm{tw}(\mathcal{B}) + K$.

We can further obtain an upper bound on $K$ as follows. First, note that for a relation symbol $r \in \mathbb{R}$ and $m$ distinct variables there exists at most distinct $m^{|r|}$ relation atoms. Note that, in our context $m \le \max\mathrm{Vars}(\Delta)$ and $|r| \le \max\mathrm{RelArity}(\Delta)$. Second, such atoms could be added for every 1-transition, for every one of its states $q_i$. That is, overall we obtain
$$ K \le \mathrm{card}(\bar{\delta}^1) \cdot (1 + \max\mathrm{PredAtoms}(\Delta)) \cdot \mathrm{relNo}(\Delta) \cdot \max\mathrm{Vars}(\Delta)^{\max\mathrm{RelArity}(\Delta)} \quad \square $$