# Capturing Homomorphism-Closed Decidable Queries with Existential Rules

Camille Bourgaux1 David Carral2 Markus Krötzsch3 Sebastian Rudolph3 Michaël
Thomazo1 1 DI ENS, ENS, CNRS, PSL University & Inria, Paris, France
2 LIRMM, Inria, University of Montpellier, CNRS, Montpellier, France
3 Technische Universität Dresden, Dresden, Germany
{camille.bourgaux, david.carral<EMAIL_ADDRESS>
{markus.kroetzsch<EMAIL_ADDRESS>
###### Abstract

Existential rules are a very popular ontology-mediated query language for
which the chase represents a generic computational approach for query
answering. It is straightforward that existential rule queries exhibiting
chase termination are decidable and can only recognize properties that are
preserved under homomorphisms. In this paper, we show the converse: every
decidable query that is closed under homomorphism can be expressed by an
existential rule set for which the standard chase universally terminates.
Membership in this fragment is not decidable, but we show via a
diagonalisation argument that this is unavoidable.

##  1 Introduction

At the core of contemporary logic-based knowledge representation is the
concept of _querying_ data sources, often using elaborate query formalisms
that allow for taking background knowledge into account. The classical
decision problem related to such knowledge-aware querying is _Boolean query
entailment_. From an abstract point of view, a Boolean query identifies a
class of _databases_ $\mathcal{D}$ – those that satisfy the query, i.e., to
which the query “matches”. This view allows us to define and investigate
properties of (abstract) queries independently from the syntax used to specify
them. Such properties can be structural (morphisms, closure properties) or
computational (decidability, complexity).

A very popular querying formalism are _existential rules_ , also referred to
as _tuple-generating dependencies_. It is straightforward that the class of
databases satisfying some existential rule query is closed under homomorphisms
and recursively enumerable. Conversely, it was established that every
homomorphism-closed query that is recursively enumerable can be expressed
using existential rules (?). That is, plain existential rules already realize
their full potential; further syntactic extensions within these boundaries do
not enhance expressivity.

For questions related to automated deduction, however, a more restricted
requirement than recursive enumerability is of central interest: decidability.
Therefore, the crucial question we tackle in this paper is:

_Can we characterize an existential rules fragment capable of expressing every
decidable homomorphism-closed query?_

The generic computational paradigm for existential rules, the _chase_ (?), is
based on repetitive, forward-chaining rule application, starting from the
database. As this may cause the iterated introduction of new domain elements,
this procedure is not guaranteed to terminate – yet, termination is a crucial
criterion for decidability. The chase comes in several variants, mainly
differing in their (increasingly thorough) mechanisms to prevent unnecessary
rule applications: While the _Skolem_ chase (?) essentially just avoids
duplicate rule applications, the _standard_ (?) and the _core_ chase (?) check
for redundancy on a local and global level, respectively.

The class of existential rule sets with terminating111We always mean universal
termination, i.e., for every database. Skolem chase has already been weighed
and found wanting: it only comprises those queries that are already
expressible in plain Datalog – and hence can be evaluated in polynomial time
(?; ?; ?). For the standard-chase-terminating and the core-chase-terminating
existential rules classes, on the other hand, we only know that the former is
contained in the latter (?), but little more than that (?). In this paper, we
clarify the situation significantly by showing the following:

_Standard-chase-terminating existential rules capture the class of all
decidable homomorphism-closed queries._

Notably, this implies that standard-chase-terminating and core-chase-
terminating existential rule queries are equally expressive and no decidable
enhancement of this formalism that preserves homomorphism-closedness (e.g. by
allowing disjunction in rule heads) can be strictly more expressive.

As a downside, the existential rules fragment thus identified is not even
semi-decidable, but we show via a diagonalisation argument that this downside
is, in fact, unavoidable.

Additional proofs and details are given in the appendix.

##  2 Preliminaries

#### Rules

We consider first-order formulas over countably infinite sets $\mathsf{Vars}$
of variables and $\mathsf{Preds}$ of _predicates_ , where each
$\mathtt{p}\in\mathsf{Preds}$ has an arity $\mathit{Ar}(\mathtt{p})\geq 0$.
Lists of variables are denoted $\vec{x}=x_{1},\ldots,x_{k}$ and will be
treated like sets when order is not relevant. An _atom_ is an expression
$\mathtt{p}(\vec{x})$ with $\mathtt{p}\in\mathsf{Preds}$ and
$|\vec{x}|=\mathit{Ar}(\mathtt{p})$.

The fragment of _disjunctive existential rules_ consists of formulae of the
form:

$\displaystyle\forall\vec{x}.\Big{(}\beta[\vec{x}]$
$\displaystyle\to\bigvee\nolimits_{\\!\\!i=1}^{k}\exists\vec{y}_{i}.\eta_{i}[\vec{x}_{i},\vec{y}_{i}]\Big{)},$
(1)

where $\beta[\vec{x}]$ and $\eta_{i}[\vec{x}_{i},\vec{y}_{i}]$
($i=1,\ldots,k$) are conjunctions of atoms with variables $\vec{x}$ and
$\vec{x}_{i}\cup\vec{y}_{i}$, respectively. We call $\beta$ _body_ and
$\bigvee\nolimits_{i=1}^{k}\exists\vec{y}_{i}.\eta_{i}$ _head_. Bodies can be
empty (we then omit $\to$), but heads must be non-empty. We require that
$\vec{x}$ and $\vec{y_{i}}$ ($i=1,\ldots,k$) are mutually disjoint and that
$\vec{x}_{i}\subseteq\vec{x}$ for all $i=1,\ldots,k$. We single out the
fragment of _existential rules_ by disallowing disjunction, i.e. requiring
$k=1$, and _Datalog rules_ by disallowing existential quantifiers. We often
omit the universal quantifiers from rules and treat conjunctions of atoms as
sets of atoms.

#### Databases, Interpretations, and Entailment

The semantics of formulas is based on logical interpretations, which we define
as relational structures over a countably infinite set $\mathsf{Nulls}$ of
_nulls_. A _schema_ $\mathcal{S}$ is a finite set of predicates. An
_interpretation_ $\mathcal{I}$ over schema $\mathcal{S}$ is a set of
expressions $\mathtt{p}(\vec{n})$ with $\mathtt{p}\in\mathcal{S}$ and
$\vec{n}$ a list of nulls of length $\mathit{Ar}(\mathtt{p})$. We write
$\mathsf{Nulls}(\mathcal{I})$ for the set of nulls in $\mathcal{I}$. A
_database_ is a finite interpretation. See also the remarks on this notation
below.

A _homomorphism_ $h:\mathcal{I}_{1}\to\mathcal{I}_{2}$ between interpretations
$\mathcal{I}_{1}$ and $\mathcal{I}_{2}$ is a mapping $h$ from the nulls in
$\mathcal{I}_{1}$ to the nulls in $\mathcal{I}_{2}$, such that
$\mathtt{p}(\vec{n})\in\mathcal{I}_{1}$ implies
$\mathtt{p}(h(\vec{n}))\in\mathcal{I}_{2}$, where $h(\vec{n})$ denotes the
list of $h$-values over $\vec{n}$. We also write $h(\mathcal{I})$ for
$\\{\mathtt{p}(h(\vec{n}))\mid\mathtt{p}(\vec{n})\in\mathcal{I}\\}$.

A _substitution_ $\sigma$ is a mapping from variables to nulls, which we
extend to lists of variables and formulas as usual. A rule $\rho$ as in (1) is
_satisfied_ by interpretation $\mathcal{I}$ if every substitution
$\sigma:\vec{x}\to\mathsf{Nulls}$ with $\sigma(\beta)\subseteq\mathcal{I}$ can
be extended to a substitution
$\sigma^{\prime}:\vec{x}\cup\vec{y}_{i}\to\mathsf{Nulls}$ for some
$i\in\\{1,\ldots,k\\}$ such that
$\sigma^{\prime}(\eta_{i})\subseteq\mathcal{I}$. Otherwise, if
$\sigma(\beta)\subseteq\mathcal{I}$ but no extension $\sigma^{\prime}$ of
$\sigma$ verifies $\sigma^{\prime}(\eta_{i})\subseteq\mathcal{I}$ for some
$i\in\\{1,\ldots,k\\}$, then $\langle\rho,\sigma\rangle$ is _applicable_ to
$\mathcal{I}$.

$\mathcal{I}$ _satisfies_ a set $\Sigma$ of rules if it satisfies every rule
in $\Sigma$. An interpretation $\mathcal{J}$ is _satisfied_ by an
interpretation $\mathcal{I}$ if there is a homomorphism
$h:\mathcal{J}\to\mathcal{I}$. $\mathcal{I}$ is a _model_ of a rule/rule
set/interpretation/database $\mathcal{X}$ if $\mathcal{X}$ is satisfied by
$\mathcal{I}$, written $\mathcal{I}\models\mathcal{X}$. As usual, we also
write $\mathcal{X}\models\mathcal{Y}$ (“$\mathcal{X}$ entails $\mathcal{Y}$”)
if every model of $\mathcal{X}$ is a model of $\mathcal{Y}$, where
$\mathcal{X}$ and $\mathcal{Y}$ might be rules, rule sets, databases, or lists
of several such elements. Note that the semantics of a database $\mathcal{D}$
in this context corresponds to the semantics of a _Boolean conjunctive query_
$\exists\vec{x}.\bigwedge\\{\mathtt{p}(x_{n_{1}},\ldots,x_{n_{\ell}})\mid\mathtt{p}(n_{1},\ldots,n_{\ell})\in\mathcal{D}\\}$
– we will therefore not introduce such queries as a separate notion. Also note
that entailment and satisfaction between interpretations/databases coincide.

#### Abstract Queries, Expressivity, and Decidability

An _(abstract) query_ $\mathfrak{Q}$ over a schema $\mathcal{S}$ is a set of
databases over $\mathcal{S}$ that is _closed under isomorphism_ , i.e., such
that whenever $\mathcal{D}\in\mathfrak{Q}$ and $\mathcal{D}^{\prime}$ is
obtained from $\mathcal{D}$ by bijective renaming of nulls, then
$\mathcal{D}^{\prime}\in\mathfrak{Q}$. $\mathfrak{Q}$ is further _closed under
homomorphisms_ if, for all $\mathcal{D}\in\mathfrak{Q}$ and homomorphisms
$h:\mathcal{D}\to\mathcal{D}^{\prime}$, we have
$\mathcal{D}^{\prime}\in\mathfrak{Q}$.

######  Definition 1.

Let $\mathtt{Goal}$ be a nullary predicate. A query $\mathfrak{Q}$ over
$\mathcal{S}$ is _expressed by_ a set $\Sigma$ of rules if, for every database
$\mathcal{D}$ over $\mathcal{S}$, we have $\mathcal{D}\in\mathfrak{Q}$ if and
only if $\Sigma,\mathcal{D}\models\mathtt{Goal}$.

To discuss decidability of queries, we need to conceive databases as Turing
machine inputs over a fixed alphabet. A _serialisation_ for a schema
$\mathcal{S}$ is a word
$s\in(\\{0,1,\mathord{\parallel}\\}\cup\mathcal{S})^{*}$ of the form
$e_{1}\cdots e_{n}$ where $n\geq 0$ and
$e_{i}=\mathtt{p}_{i}\mathord{\parallel}w_{i1}\mathord{\parallel}\cdots\mathord{\parallel}w_{i\mathit{Ar}(\mathtt{p}_{i})}\mathord{\parallel}$
for $w_{ij}\in\\{0,1\\}^{+}$ and $\mathtt{p}_{i}\in\mathcal{S}$. Given $s$ of
this form and an injection $\eta:\\{0,1\\}^{+}\to\mathsf{Nulls}$, let
$\eta(s)$ denote the database
$\\{\mathtt{p}_{i}(\eta(w_{i1}),\ldots,\eta(w_{i\mathit{Ar}(\mathtt{p}_{i})}))\mid
1\leq i\leq n\\}$. Then $s$ _corresponds to_ a database $\mathcal{D}$ if
$\eta(s)$ is isomorphic to $\mathcal{D}$; note that this does not depend on
the choice of $\eta$.

A query $\mathfrak{Q}$ with schema $\mathcal{S}$ is _decidable_ if the set of
all serialisations for $\mathcal{S}$ that correspond to some
$\mathcal{D}\in\mathfrak{Q}$ is a decidable language.

#### Remarks on our Notation

Many works consider constants to appear in databases (not just nulls), but
complexity and expressivity is usually studied for queries that are closed
under isomorphisms, a.k.a.  _generic_ (?, Ch. 16), and nulls are more natural
there. One can admit finitely many exceptions (elements that must not be
renamed), but such “constants” can be simulated by marking them with dedicated
unary predicates.

Specifying logical interpretations as sets of “atoms” that may use nulls is a
notational convenience with some side effects: our interpretations cannot
contain elements that do not stand in any relation, but they can have an empty
domain. Both aspects do not change the notion of logical entailment _on the
formulas we consider_.

#### Universal Models and the Chase

Entailment of databases (corresponding to Boolean conjunctive queries) can be
decided by considering only a subset of all models. Given sets $\mathfrak{I}$
and $\mathfrak{K}$ of interpretations, $\mathfrak{I}$ is _universal_ for
$\mathfrak{K}$ if, for all $\mathcal{K}\in\mathfrak{K}$, there is
$\mathcal{I}\in\mathfrak{I}$ and a homomorphism $\mathcal{I}\to\mathcal{K}$.
Consider a rule set $\Sigma$ and database $\mathcal{D}$, and let
$\mathfrak{M}$ be the set of all models of $\Sigma,\mathcal{D}$. Then
$\mathfrak{I}$ is a _universal model set_ for $\Sigma$ and $\mathcal{D}$ if
$\mathfrak{I}\subseteq\mathfrak{M}$ and $\mathfrak{I}$ is universal for
$\mathfrak{M}$.

######  Fact 1.

If $\mathfrak{I}$ is a universal model set for $\Sigma$ and $\mathcal{D}$
then, for every database $\mathcal{C}$, we have
$\Sigma,\mathcal{D}\models\mathcal{C}$ iff $\mathcal{I}\models\mathcal{C}$ for
all $\mathcal{I}\in\mathfrak{I}$.

Universal model sets can be computed with the _chase_ algorithm. Here, we
consider a variation of the _standard_ (or _restricted_) chase for rules with
disjunction, introduced by (?).

######  Definition 2.

A _chase tree_ for a rule set $\Sigma$ and database $\mathcal{D}$ is a (finite
or infinite) tree where each node is labelled by a database, such that:

  1. 1.

The root is labelled with $\mathcal{D}$.

  2. 2.

For every node with label $\mathcal{E}$ that has $\ell$ children labelled
$\mathcal{C}_{1},\ldots,\mathcal{C}_{\ell}$, there is a rule $\rho\in\Sigma$
of the form (1) and a substitution $\sigma:\vec{x}\to\mathsf{Nulls}$ such that
(i) $\langle\rho,\sigma\rangle$ is applicable to $\mathcal{E}$, (ii) $\rho$
has $k=\ell$ head disjuncts, and (iii)
$\mathcal{C}_{i}=\mathcal{E}\cup\sigma_{i}(\eta_{i})$ where $\sigma_{i}$
extends $\sigma$ by mapping each variable $y\in\vec{y}_{i}$ to a fresh null.

  3. 3.

For each rule $\rho\in\Sigma$ and each substitution $\sigma$, there is $i\geq
1$ such that $\langle\rho,\sigma\rangle$ is not applicable to the label of any
node of depth $\geq i$.

The _result_ that corresponds to a chase tree is the set of all
interpretations that can be obtained as the union of all interpretations along
a path in the tree.

Condition (3) ensures fair, exhaustive rule application, but different orders
of application can lead to different chase trees, which can also have
different results. Nevertheless, every result is semantically correct in the
following sense:

######  Fact 2.

Every result of a chase on a rule set $\Sigma$ and database $\mathcal{D}$ is a
universal model set for $\Sigma$ and $\mathcal{D}$.

The pair $\langle\Sigma,\mathcal{D}\rangle$ is _chase-terminating_ if all its
chase trees are finite – by König’s Lemma, this is equivalent to all chase
results for $\langle\Sigma,\mathcal{D}\rangle$ containing only finite
interpretations; this corresponds to _all-strategy termination_. $\Sigma$ is
_chase-terminating_ if $\langle\Sigma,\mathcal{D}\rangle$ is chase-terminating
for every database $\mathcal{D}$; this corresponds to _universal termination_.

#### Turing Machines

We will use (deterministic) Turing machines (TM), denoted as a tuple
$M=\langle Q,\Gamma,\delta\rangle$, with states $Q$, tape alphabet $\Gamma$
with blank $\text{\textvisiblespace}\in\Gamma$, and transition function
$\delta$. $M$ has a distinguished initial state $q_{S}\in Q$, and accepting
and rejecting halting states $q_{A},q_{R}\in Q$. For all states $q\in
Q\setminus\\{q_{A},q_{R}\\}$ and tape symbols $a\in\Gamma$, there is exactly
one transition $(q,a)\mapsto(r,b,D)\in\delta$. We assume that TM tapes are
unbounded to the right but bounded to the left, and that TMs will never
attempt to move left on the first position of the tape (this is w.l.o.g.,
since one can modify any TM to insert a marker at the tape start to recognise
this case).

##  3 On the Expressivity of Disjunctive Rules

In this section, we show how to express a homomorphism-closed, decidable query
with a disjunctive rule set. This construction will be the basis for finding a
chase-terminating set of (deterministic) existential rules. Throughout this
section, $\mathfrak{Q}$ is a fixed but arbitrary homomorphism-closed query
over signature $\mathcal{S}$, and $M=\langle Q,\Gamma,\delta\rangle$ is a TM
that decides $\mathfrak{Q}$.

To express $\mathfrak{Q}$, we specify five rule sets
$\mathcal{R}_{1}\subseteq\mathcal{R}_{2}\subseteq\mathcal{R}_{3}\subseteq\mathcal{R}_{4}\subseteq\mathcal{R}_{5}$
(see Figures 1–6), which will be explained later. We want to show the
following result:

######  Theorem 3.

The set $\mathcal{R}_{5}$ of disjunctive existential rules expresses the query
$\mathfrak{Q}$.

To show this, we fix an arbitrary database $\mathcal{D}$ over $\mathcal{S}$.
Theorem 3 then follows from Fact 1 and the next lemma:

######  Lemma 4.

There is a universal model set $\mathfrak{M}$ of $\mathcal{R}_{5}$ and
$\mathcal{D}$ such that $\mathcal{D}\in\mathfrak{Q}$ iff
$\mathtt{Goal}\in\mathcal{I}$ for every $\mathcal{I}\in\mathfrak{M}$.

The universal model set $\mathfrak{M}$ is a complicated structure that we
describe step by step, by specifying five sets of interpretations –
$\mathfrak{I}_{1}$, $\mathfrak{I}_{2}$, $\mathfrak{I}_{3}$,
$\mathfrak{I}_{4}$, and $\mathfrak{I}_{5}$ –, such that (1) $\mathfrak{I}_{i}$
is a universal model set of $\mathcal{R}_{i},\mathcal{D}$ for each $1\leq
i\leq 5$, (2)
$|\mathfrak{I}_{1}|=|\mathfrak{I}_{2}|=|\mathfrak{I}_{3}|=|\mathfrak{I}_{4}|=|\mathfrak{I}_{5}|$,
and (3) for each $1\leq i<j\leq 5$ and each $\mathcal{I}\in\mathfrak{I}_{i}$,
there is exactly one $\mathcal{J}\in\mathfrak{I}_{j}$ with
$\mathcal{I}\subseteq\mathcal{J}$. Lemma 4 can then be shown using
$\mathfrak{M}=\mathfrak{I}_{5}$.

Before dwelling into the details of each rule set and universal model, we give
an overview of the construction: $\mathcal{R}_{1}$ constructs all possible
linear orders over the nulls in $\mathcal{D}$, as well as all possible
completions of $\mathcal{D}$ with facts built using these nulls;
$\mathcal{R}_{2}\setminus\mathcal{R}_{1}$ extracts successor relations from
the linear orders; $\mathcal{R}_{3}\setminus\mathcal{R}_{2}$ associates to
nulls representations of their positions in successor relations;
$\mathcal{R}_{4}\setminus\mathcal{R}_{3}$ encodes all initial TM
configurations corresponding to some linear order and completion, and
$\mathcal{R}_{5}\setminus\mathcal{R}_{4}$ simulates the run of the TM on these
configurations.

$\displaystyle\to\exists y.\mathtt{First}(y)\wedge\mathtt{DbDom}(y)$ (2)
$\displaystyle\to\exists z.\mathtt{Last}(z)\wedge\mathtt{DbDom}(z)$ (3)
$\displaystyle\mathtt{p}(\vec{x})$
$\displaystyle\textstyle\to\mathtt{In}_{\mathtt{p}}(\vec{x})\wedge\bigwedge_{x\in\vec{x}}\mathtt{DbDom}(x)$
(4) $\displaystyle\mathtt{DbDom}(x)$ $\displaystyle\to\mathtt{Eq}(x,x)$ (5)
$\displaystyle\mathtt{Eq}(x,y)$ $\displaystyle\to\mathtt{Eq}(y,x)$ (6)
$\displaystyle\mathtt{NEq}(x,y)$ $\displaystyle\to\mathtt{NEq}(y,x)$ (7)
$\displaystyle\mathtt{R}(\vec{x})\wedge\mathtt{Eq}(x_{i},y)$
$\displaystyle\to\mathtt{R}(\vec{x}_{x_{i}\mapsto y})$ (8)
$\displaystyle\mathtt{DbDom}(x)\wedge\mathtt{DbDom}(y)$
$\displaystyle\to\mathtt{Eq}(x,y)\vee\mathtt{NEq}(x,y)$ (9)
$\displaystyle\mathtt{LT}(x,y)\wedge\mathtt{LT}(y,z)$
$\displaystyle\to\mathtt{LT}(x,z)$ (10)
$\displaystyle\mathtt{First}(x)\wedge\mathtt{NEq}(x,y)$
$\displaystyle\to\mathtt{LT}(x,y)$ (11)
$\displaystyle\mathtt{NEq}(x,y)\wedge\mathtt{Last}(y)$
$\displaystyle\to\mathtt{LT}(x,y)$ (12) $\displaystyle\mathtt{NEq}(x,y)$
$\displaystyle\to\mathtt{LT}(x,y)\vee\mathtt{LT}(y,x)$ (13)
$\displaystyle\textstyle\bigwedge_{x\in\vec{x}}\mathtt{DbDom}(x)$
$\displaystyle\to\mathtt{In}_{\mathtt{p}}(\vec{x})\vee\mathtt{NIn}_{\mathtt{p}}(\vec{x})$
(14)
Figure 1: The rule set $\mathcal{R}_{1}$, where rules (4) and (14) are
instantiated for each $\mathtt{p}\in\mathcal{S}$, and rules (8) are
instantiated for each
$\mathtt{R}\in\\{\mathtt{First},\mathtt{Last},\mathtt{Eq},\mathtt{NEq},\mathtt{LT}\\}\cup\\{\mathtt{In}_{\mathtt{p}},\mathtt{NIn}_{\mathtt{p}}\mid\mathtt{p}\in\mathcal{S}\\}$
and $1\leq i\leq\mathit{Ar}(\mathtt{R})$, and $\vec{x}_{x_{i}\mapsto y}$
denotes $\vec{x}$ with $x_{i}$ replaced by $y$.
$\displaystyle\mathtt{First}(x)$ $\displaystyle\to\exists
u.\mathtt{Root}(u)\wedge\mathtt{Rep}(x,u)$ (15)
$\displaystyle\mathtt{Rep}(x,v)\wedge\mathtt{LT}(x,z)$
$\displaystyle\to\exists w.\mathtt{Chi}(v,w)\wedge\mathtt{Rep}(z,w)$ (16)
$\displaystyle\mathtt{Last}(x)\wedge\mathtt{Rep}(x,u)$
$\displaystyle\to\mathtt{Leaf}(u)$ (17)
$\displaystyle\mathtt{Rep}(x,u)\wedge\mathtt{Eq}(x,y)$
$\displaystyle\to\mathtt{Rep}(y,u)$ (18)
$\displaystyle\textstyle\mathtt{In}_{\mathtt{p}}(\vec{x})\wedge\bigwedge_{i=1}^{|\vec{x}|}$
$\displaystyle\mathtt{Rep}(x_{i},u_{i})\to\mathtt{In}_{\mathtt{p}}^{\prime}(\vec{u})$
(19)
$\displaystyle\textstyle\mathtt{NIn}_{\mathtt{p}}(\vec{x})\wedge\bigwedge_{i=1}^{|\vec{x}|}$
$\displaystyle\mathtt{Rep}(x_{i},u_{i})\to\mathtt{NIn}_{\mathtt{p}}^{\prime}(\vec{u})$
(20) Figure 2: The rule set $\mathcal{R}_{2}$ contains $\mathcal{R}_{1}$ (see
Figure 1) and all above rules, where (19) and (20) are instantiated for each
$\mathtt{p}\in\mathcal{S}$.  $\displaystyle\mathtt{Root}(u)$
$\displaystyle\to\exists
y_{1},y_{2}.\mathtt{Enc}(u,y_{1},y_{2})\wedge\mathtt{S}_{0}(y_{1})\wedge\mathtt{Nxt}(y_{1},y_{2})\wedge\mathtt{S}_{1}(y_{2})$
(21) $\displaystyle\mathtt{Enc}(u,y_{1},y_{\\_})\wedge\mathtt{Chi}(u,v)$
$\displaystyle\to\exists
z_{1},z_{\\_}.\mathtt{Enc}(v,z_{1},z_{\\_})\wedge\mathtt{Cpy}_{\\!+1}(y_{1},y_{\\_},z_{1},z_{\\_})$
(22)
$\displaystyle\mathtt{Cpy}_{\\!+1}(y_{1},y_{2},z_{1},z_{\\_})\wedge\mathtt{S}_{0}(y_{1})\wedge\mathtt{Nxt}(y_{1},y_{2})$
$\displaystyle\to\mathtt{S}_{1}(z_{1})\wedge\mathtt{Nxt}(z_{1},z_{\\_})\wedge\mathtt{S}_{1}(z_{\\_})$
(23)
$\displaystyle\mathtt{Cpy}_{\\!+1}(y_{1},y_{2},z_{1},z_{\\_})\wedge\mathtt{S}_{1}(y_{1})\wedge\mathtt{Nxt}(y_{1},y_{2})$
$\displaystyle\to\exists
z_{2}.\mathtt{S}_{0}(z_{1})\wedge\mathtt{Nxt}(z_{1},z_{2})\wedge\mathtt{S}_{0}(z_{2})\wedge\mathtt{Nxt}(z_{2},z_{\\_})\wedge\mathtt{S}_{1}(z_{\\_})$
(24)
$\displaystyle\\!\\!\mathtt{Cpy}_{\\!+1}(y_{1},y_{\\_},z_{1},z_{\\_})\wedge\mathtt{S}_{0}(y_{1})\wedge\mathtt{Nxt}(y_{1},y_{2})\wedge\mathtt{Nxt}(y_{2},y_{3})$
$\displaystyle\to\exists
z_{2}.\mathtt{Cpy}(y_{2},y_{\\_},z_{2},z_{\\_})\wedge\mathtt{S}_{1}(z_{1})\wedge\mathtt{Nxt}(z_{1},z_{2})$
(25)
$\displaystyle\\!\\!\mathtt{Cpy}_{\\!+1}(y_{1},y_{\\_},z_{1},z_{\\_})\wedge\mathtt{S}_{1}(y_{1})\wedge\mathtt{Nxt}(y_{1},y_{2})\wedge\mathtt{Nxt}(y_{2},y_{3})$
$\displaystyle\to\exists
z_{2}.\mathtt{Cpy}_{\\!+1}(y_{2},y_{\\_},z_{2},z_{\\_})\wedge\mathtt{S}_{0}(z_{1})\wedge\mathtt{Nxt}(z_{1},z_{2})$
(26)
$\displaystyle\mathtt{Cpy}(y_{1},y_{2},z_{1},z_{2})\wedge\mathtt{S}_{*}(y_{1})\wedge\mathtt{Nxt}(y_{1},y_{2})$
$\displaystyle\to\mathtt{S}_{*}(z_{1})\wedge\mathtt{Nxt}(z_{1},z_{2})\wedge\mathtt{S}_{1}(z_{2})$
(27)
$\displaystyle\mathtt{Cpy}(y_{1},y_{\\_},z_{1},z_{\\_})\wedge\mathtt{S}_{*}(y_{1})\wedge\mathtt{Nxt}(y_{1},y_{2})\wedge\mathtt{Nxt}(y_{2},y_{3})$
$\displaystyle\to\exists
z_{2}.\mathtt{Cpy}(y_{2},y_{\\_},z_{2},z_{\\_})\wedge\mathtt{S}_{*}(z_{1})\wedge\mathtt{Nxt}(z_{1},z_{2})$
(28)
Figure 3: The rule set $\mathcal{R}_{3}$ contains $\mathcal{R}_{2}$ (Figure 2)
and all of the above rules, where (27) and (28) are instantiated for each
$*\in\\{0,1\\}$.

####  $\mathbf{\mathcal{R}_{1}}$: Linear Order and Database Completion

$\mathcal{R}_{1}$ serves two distinct purposes: (1) predicates
$\mathtt{First}$, $\mathtt{Last}$, $\mathtt{Eq}$ (“$=$”), $\mathtt{NEq}$
(“$\neq$”), and $\mathtt{LT}$ (“$<$”) encode representations of possible
linear orders over nulls in $\mathcal{D}$ (collected in predicate
$\mathtt{DbDom}$); and (2) predicates $\mathtt{In}_{\mathtt{p}}$ and
$\mathtt{NIn}_{\mathtt{p}}$ for each $\mathtt{p}\in\mathcal{S}$ explicitly
encode positive and negative (absent) facts in $\mathcal{D}$. Both purposes
require disjunctive reasoning. Possible models include representations of
strict, total linear orders (1) and the exact database completion (2), but
also models for collapsed orders and inconsistent completions. The latter is
not problematic since we consider homomorphism-closed queries.

We define the interpretation set $\mathfrak{I}_{1}$ on the set
$\Delta=\mathsf{Nulls}(\mathcal{D})\cup\\{u_{\alpha},u_{\omega}\\}$, for fresh
nulls $u_{\alpha},u_{\omega}\notin\mathsf{Nulls}(\mathcal{D})$. A (partially
collapsed) linear order can be represented by an ordered partition
$\vec{T}=T_{1},\ldots,T_{k}$ ($k\geq 1$) of $\Delta$ where $u_{\alpha}\in
T_{1}$ and $u_{\omega}\in T_{k}$. Let $\mathit{Ords}$ be the set of all such
$\vec{T}$, and let $\mathit{Compls}(\vec{T})$ be the set of all
interpretations with nulls $\Delta$ that are set-minimal among the models of
$\mathcal{R}_{1}$ and $\mathcal{D}$, and that contain the database

$\displaystyle\\{$ $\displaystyle\mathtt{First}(u)\mid u\in
T_{1}\\}\cup\\{\mathtt{Last}(u)\mid u\in T_{k}\\}\cup{}$ $\displaystyle\\{$
$\displaystyle\mathtt{Eq}(t,u)\mid 1\leq i\leq k;t,u\in T_{i}\\}\cup{}$
$\displaystyle\\{$
$\displaystyle\mathtt{LT}(t,\\!u),\mathtt{NEq}(t,\\!u),\mathtt{NEq}(u,\\!t)\,{\mid}\,1\,{\leq}\,i\,{<}\,j\,{\leq}\,k;t\,{\in}\,T_{i};u\,{\in}\,T_{j}\\}.$

By minimality, each $\mathcal{I}\in\mathit{Compls}(\vec{T})$ contains exactly
one of
$\\{\mathtt{In}_{\mathtt{p}}(\vec{t}),\mathtt{NIn}_{\mathtt{p}}(\vec{t})\\}$
for every $\vec{t}\subseteq\Delta$ with $|\vec{t}|=\mathit{Ar}(\mathtt{p})$.

######  Lemma 5.

$\mathfrak{I}_{1}=\bigcup_{\vec{T}\in\mathit{Ords}}\mathit{Compls}(\vec{T})$
is a universal model set of $\mathcal{R}_{1}$ and $\mathcal{D}$.

###### Proof Sketch.

We can construct a chase tree for $\mathcal{R}_{1}$ and $\mathcal{D}$ that
prioritises the application of rules in the order of their appearance in
Figure 1. The result of that chase $\mathfrak{K}$ is a finite universal model
set (Fact 2) and we can show that every $\mathcal{K}\in\mathfrak{K}$ is
isomorphic to a unique $\mathcal{I}\in\mathfrak{I}_{1}$. ∎

Each set $\mathfrak{I}_{i}$ for some $2\leq i\leq 5$ is obtained as
$\mathfrak{I}_{i}=\\{\mathit{Int}_{i}(\mathcal{I})\mid\mathcal{I}\in\mathfrak{I}_{i-1}\\}$
for a function $\mathit{Int}_{i}$ as defined below. Every
$\mathcal{I}\in\mathfrak{I}_{i}$ with $1\leq i\leq 5$ contains a unique
interpretation $\mathit{Seed}(\mathcal{I})\in\mathfrak{I}_{1}$, and there is a
unique ordered partition $\mathit{Order}(\mathcal{I})\in\mathit{Ords}$ such
that
$\mathit{Seed}(\mathcal{I})\in\mathit{Compls}(\mathit{Order}(\mathcal{I}))$.

####  $\mathbf{\mathcal{R}_{2}}$: Representative Tree

The purpose of $\mathcal{R}_{2}$ is to extract successor relations from the
transitive linear order $\mathtt{LT}$. Given an ordered partition
$\mathit{Order}(\mathcal{I})=T_{1},\ldots,T_{k}$ of some model $\mathcal{I}$
of $\mathcal{R}_{1}$, $\mathcal{R}_{2}$ constructs a finite tree structure –
defined using predicates $\mathtt{Root}$, $\mathtt{Chi}$ (“child”), and
$\mathtt{Leaf}$ – where each path represents a sub-sequence
$T_{z_{1}},\ldots,T_{z_{p}}$ of $T_{1},\ldots,T_{k}$ with $z_{1}=1$ and
$z_{p}=k$. Unavoidably, some paths will skip some $T_{i}$, but it suffices for
our purposes if one path is complete. The elements of any set $T_{j}$ are
related to the tree nodes that represent $T_{j}$ by a predicate
$\mathtt{Rep}$. Moreover, nodes are related via predicates
$\mathtt{In}_{\mathtt{p}}^{\prime}$ and $\mathtt{NIn}_{\mathtt{p}}^{\prime}$
that reflect the relations for $\mathtt{In}_{\mathtt{p}}$ and
$\mathtt{NIn}_{\mathtt{p}}$ that hold between the represented elements (in the
database completion of the considered model $\mathcal{I}$ of
$\mathcal{R}_{1}$).

Given $\mathcal{I}$ with $|\mathit{Order}(\mathcal{I})|=k$ as above, let
$\mathbf{Z}$ be the set of all words $z_{1}\cdots
z_{p}\in\\{1,\ldots,k\\}^{*}$ such that $z_{1}=1$ and $z_{i}<z_{i+1}$ for all
$i\in\\{1,\ldots,p-1\\}$. Moreover, let $\mathit{end}(z_{1}\cdots
z_{p}):=z_{p}$. Using fresh nulls $\\{u_{w}\mid w\in\mathbf{Z}\\}$, we define
$\mathit{Tree}(\mathcal{I})$ to be the interpretation

$\displaystyle\\{\mathtt{Root}(u_{1})\\}\cup\\{\mathtt{Chi}(u_{w},u_{wz})\mid
wz\in\mathbf{Z},2\leq z\leq k\\}\cup{}$
$\displaystyle\\{\mathtt{Leaf}(u_{w})\mid
w\in\mathbf{Z};\mathit{end}(w)=k\\}\cup{}$
$\displaystyle\\{\mathtt{Rep}(x,u_{w})\mid w\in\mathbf{Z};x\in
T_{\mathit{end}(w)}\\}.$

Now $\mathit{Int}_{2}(\mathcal{I})$ is the least interpretation that contains
$\mathcal{I}$ and $\mathit{Tree}(\mathcal{I})$, and that further satisfies
rules (19) and (20). We can extend Lemma 5 as follows. The required universal
model set is obtained by any chase that prioritises rule (18).

######  Lemma 6.

$\mathfrak{I}_{2}=\\{\mathit{Int}_{2}(\mathcal{I})\mid\mathcal{I}\in\mathfrak{I}_{1}\\}$
is a universal model set of $\mathcal{R}_{2}$ and $\mathcal{D}$.

$\displaystyle\mathtt{Ld}_{\mathtt{p}}(u,t,\vec{v})\wedge\mathtt{In}_{\mathtt{p}}^{\prime}(\vec{v})$
$\displaystyle\to\textstyle\exists\vec{x},y.\mathtt{S}_{\mathtt{p}}(t)\wedge\mathtt{Nxt}(t,x_{1})\wedge\bigwedge_{i=1}^{|\vec{v}|}\mathtt{LdE}(v_{i},x_{i},x_{i+1})\wedge\mathtt{Nxt}(x_{|\vec{v}|+1},y)\wedge\mathtt{Rdy}_{\mathtt{p}}(u,y,\vec{v})$
(29)
$\displaystyle\mathtt{LdE}(v,x_{s},x_{e})\wedge\mathtt{Enc}(v,y_{1},y_{\\_})$
$\displaystyle\to\exists
z_{1},z_{\\_}.\mathtt{S}_{\mathord{\parallel}}(x_{s})\wedge\mathtt{Nxt}(x_{s},z_{1})\wedge\mathtt{Cpy}(y_{1},y_{\\_},z_{1},z_{\\_})\wedge\mathtt{Nxt}(z_{\\_},x_{e})\wedge\mathtt{S}_{\mathord{\parallel}}(x_{e})$
(30) Figure 4: The rule set $\mathcal{R}_{4}$ contains $\mathcal{R}_{3}$ (see
Figure 3), the rules from Figure 5, and the above rules instantiated for all
$\mathtt{p}\in\mathcal{S}$. $\displaystyle\mathtt{Leaf}(u)\to\exists
t.\mathtt{Ld}_{1}(u,$ $\displaystyle t,u)\wedge\mathtt{Hd}_{q_{S}}(t)$ (31)
$\displaystyle\mathtt{Ld}_{\ell}(u,t,\vec{v})$
$\displaystyle\to\mathtt{Ld}_{\mathtt{p}^{\ell}_{1}}(u,t,\vec{v})$ (32)
$\displaystyle\mathtt{Rdy}_{\mathtt{p}_{j}^{\ell}}(u,t,\vec{v})$
$\displaystyle\to\mathtt{Ld}_{\mathtt{p}_{j+1}^{\ell}}(u,t,\vec{v})$ (33)
$\displaystyle\mathtt{Rdy}_{\mathtt{p}_{{\bar{n}}}^{\ell}}(u,t,\vec{v})$
$\displaystyle\to\mathtt{Rdy}_{\ell}(u,t,\vec{v})$ (34)
$\displaystyle\begin{split}\textstyle\\!\\!\\!\mathtt{Rdy}_{\ell}(u,t,\vec{v})\wedge\bigwedge_{i=k+1}^{\ell}\mathtt{Root}&(v_{i})\wedge\mathtt{Chi}(w,v_{k})\\\
\to\mathtt{Ld}_{\ell}(u,t,&v_{1},{\scriptstyle\cdots},v_{k-1},w,u,{\scriptstyle\cdots},u)\\!\end{split}$
(35)
$\displaystyle\textstyle\\!\\!\\!\mathtt{Rdy}_{\ell}(u,t,\vec{v})\,{\wedge}\bigwedge_{i=1}^{\ell}\mathtt{Root}(v_{i})$
$\displaystyle\to\mathtt{Ld}_{\ell+1}(u,t,u,{\scriptstyle\cdots},u)\\!$ (36)
$\displaystyle\textstyle\\!\\!\\!\mathtt{Rdy}_{{\bar{m}}}(u,t,\vec{v})\,{\wedge}\bigwedge_{i=1}^{{\bar{m}}}\mathtt{Root}(v_{i})$
$\displaystyle\to\mathtt{S}_{\text{\textvisiblespace}}(t)\wedge\mathtt{End}(t)$
(37)
$\displaystyle\mathtt{Ld}_{\mathtt{p}}(u,t,\vec{v})\wedge\mathtt{NIn}_{\mathtt{p}}^{\prime}(\vec{v})$
$\displaystyle\to\mathtt{Rdy}_{\mathtt{p}}(u,t,\vec{v})$ (38) Figure 5: Some
rules of $\mathcal{R}_{4}$, to be instantiated for all $1\leq
j\leq{\bar{n}}-1$, $1\leq k\leq\ell\leq{\bar{m}}$, and
$\mathtt{p}\in\mathcal{S}$.

####  $\mathbf{\mathcal{R}_{3}}$: Position Binary Encodings

The purpose of $\mathcal{R}_{3}$ is to associate each node in the tree of
$\mathcal{R}_{2}$ with a binary encoding of its distance from the root (the
root starts with “distance” $2$ for technical reasons). Encodings start at the
least significant bit and always end in $1$ (i.e., have no leading $0$s). To
simplify upcoming steps, encodings take the form of little TM tapes,
represented by a $\mathtt{Nxt}$-connected chain of nulls with unary predicates
$\mathtt{S}_{0}$ and $\mathtt{S}_{1}$ encoding the symbol at each position.
Nodes $u$ relate to the first and last null $t_{s}$ and $t_{e}$ of their
“tape” through facts $\mathtt{Enc}(u,t_{s},t_{e})$. Facts
$\mathtt{Cpy}(a_{s},a_{e},b_{s},b_{e})$ are used to create a tape between
$b_{s}$ and $b_{e}$ that contains a copy of the information on the tape
between $a_{s}$ and $a_{e}$. Predicate $\mathtt{Cpy}_{\\!+1}$ is analogous,
but creates a representation of the successor of the number that is copied.

Consider a model $\mathcal{I}$ of $\mathcal{R}_{2}$ and define the set of
sequences $\mathbf{Z}$ as before. For $w\in\mathbf{Z}$ of length $|w|$, and
$b_{1}\cdots b_{\ell}$ the binary representation of $|w|+1$, let
$\mathit{EncPos}(w)$ be the database

$\displaystyle\\{$
$\displaystyle\mathtt{Enc}(u_{w},e_{w}^{1},e_{w}^{\ell})\\}\cup\\{\mathtt{S}_{b_{i}}(e_{w}^{i})\mid
1\leq i\leq\ell\\}\cup{}$ $\displaystyle\\{$
$\displaystyle\mathtt{Nxt}(e_{w}^{i-1},e_{w}^{i})\mid 2\leq i\leq\ell\\}.$

Let $\mathcal{J}=\mathcal{I}\cup\bigcup_{w\in\mathbf{Z}}\mathit{EncPos}(w)$.
We define $\mathit{Int}_{3}(\mathcal{I})$ as the smallest superset of
$\mathcal{J}$ that satisfies all rules in $\mathcal{R}_{3}$ while including
only the nulls in $\mathcal{J}$. $\mathit{Int}_{3}(\mathcal{I})$ extends
$\mathcal{J}$ only by missing $\mathtt{Cpy}$ and $\mathtt{Cpy}_{\\!+1}$
relations, which can be inferred by slightly rewritten rules. For example,
rule (22) is satisfied when applying the following rule to $\mathcal{J}$:

$\displaystyle\mathtt{Enc}(u,y_{1},y_{\\_})\wedge\mathtt{Chi}(u,v)$
$\displaystyle\wedge\mathtt{Enc}(v,z_{1},z_{\\_})$
$\displaystyle\to\mathtt{Cpy}_{\\!+1}(y_{1},y_{\\_},z_{1},z_{\\_}).$

All other rules can be rewritten analogously, since every existentially
quantified variable is used in unique ways with predicates other than
$\mathtt{Cpy}$ and $\mathtt{Cpy}_{\\!+1}$.

For every $\mathcal{I}\in\mathfrak{I}_{2}$, we show that
$\mathit{Int}_{3}(\mathcal{I})$ is isomorphic to a result of the chase on
$\mathcal{R}_{3}$ and $\mathcal{I}$. The next result then follows from Lemma
6.

######  Lemma 7.

$\mathfrak{I}_{3}=\\{\mathit{Int}_{3}(\mathcal{I})\mid\mathcal{I}\in\mathfrak{I}_{2}\\}$
is a universal model set of $\mathcal{R}_{3}$ and $\mathcal{D}$.

####  $\mathbf{\mathcal{R}_{4}}$: Initial TM Configuration

For each leaf in the tree of completions, $\mathcal{R}_{4}$ creates the
representation of an initial TM configuration. The tape is again represented
by a $\mathtt{Nxt}$-chain, using further unary predicates
$\mathtt{S}_{\mathord{\parallel}}$, $\mathtt{S}_{\text{\textvisiblespace}}$,
and $\mathtt{S}_{\mathtt{p}}$ (for all $\mathtt{p}\in\mathcal{S}$) for
additional tape symbols. $\mathtt{Hd}_{q_{S}}$ marks the TM’s starting
position and initial state $q_{S}$, and $\mathtt{End}$ the end of the tape.

Let ${\bar{m}}$ be the maximal arity of predicates in $\mathcal{S}$. We
require that there is some ${\bar{n}}>0$ such that $\mathcal{S}$ contains
exactly ${\bar{n}}$ predicates
$\mathtt{p}^{i}_{1},\ldots,\mathtt{p}^{i}_{\bar{n}}$ of arity $i$, for every
$1\leq i\leq{\bar{m}}$. This is without loss of generality, except for the
exclusion of nullary predicates. Our results do not depend on this
restriction, but it helps to simplify the presentation of our main ideas.

To serialise the data as a tape, we iterate over all predicate arities
$\ell=1,\ldots,{\bar{m}}$ and over all lists $\vec{v}$ of tree nodes with
length $\ell$. In this process, $\mathtt{Ld}_{\ell}(u,t,\vec{v})$ expresses
that, while encoding the leaf $u$, after constructing the tape until position
$t$, we continue serialising $\ell$-ary predicate data for arguments
$\vec{v}$. Analogously, $\mathtt{Rdy}_{\ell}(u,t,\vec{v})$ means that this was
completed at tape position $t$. Similar predicates $\mathtt{Ld}_{\mathtt{p}}$
and $\mathtt{Rdy}_{\mathtt{p}}$ are used to consider a specific predicate
$\mathtt{p}\in\mathcal{S}$ during this process. The rules in Figure 5 start
the serialisation (31), proceed over all predicates (32)–(34), iterate over
parameter vectors (35) and arities (36), and finally end the tape (37).

Absent facts do not need to be serialised (38), while present facts can be
treated by copying the encodings for each of their parameters (29) and (30).
In the latter, $\mathtt{LdE}$ states that a specific argument is serialised
between two given tape positions.

The resulting TM tapes serialise facts
$\mathtt{In}_{\mathtt{p}}^{\prime}(\vec{u})$ as introduced by
$\mathcal{R}_{2}$, i.e., where $\vec{u}$ are nodes in the representative tree.
Given a model $\mathcal{I}\in\mathfrak{I}_{3}$ with some
$\mathtt{Leaf}(u_{w})\in\mathcal{I}$, let $\mathit{branch}(u_{w})$ be the set
of all nodes $u_{w^{\prime}}$ on the branch of $u_{w}$, i.e. all nulls
$u_{w^{\prime}}$ where $w^{\prime}$ is a prefix of $w$. Elements of
$\mathit{branch}(u_{w})$ are totally ordered by setting $u_{w_{1}}\prec
u_{w_{2}}$ if $|w_{1}|>|w_{2}|$. Predicates are totally ordered by setting
$\mathtt{p}^{a}_{i}\prec\mathtt{p}^{b}_{j}$ if either $a<b$, or both $a=b$ and
$i<j$. We can then order facts as
$\mathtt{p}(\vec{u})\prec\mathtt{q}(\vec{v})$ if
$\vec{u},\vec{v}\subseteq\mathit{branch}(u_{w})$ and
$\langle\mathtt{p},\vec{u}\rangle$ is lexicographically before
$\langle\mathtt{q},\vec{v}\rangle$.

Now let
$\mathit{branchDb}(\mathcal{I},u_{w})=\\{\mathtt{p}(\vec{u})\mid\mathtt{In}_{\mathtt{p}}^{\prime}(\vec{u})\in\mathcal{I},\vec{u}\subseteq\mathit{branch}(u_{w})\\}$
denote the set of all facts on the branch with leaf $u_{w}$, and let
$\mathit{branchTape}(\mathcal{I},u_{w})$ denote the TM tape serialisation (as
defined in Section 2) of $\mathit{branchDb}(\mathcal{I},u_{w})$ according to
the total order $\prec$ and representing each node $u_{w}$ by the binary
representation of $|w|+1$ as before. Given
$S=\mathit{branchTape}(\mathcal{I},u_{w})$, let
$\mathit{startConf}(\mathcal{I},u_{w})$ be the following interpretation:

$\displaystyle\\{$
$\displaystyle\mathtt{Ld}_{1}(u_{w},t_{w}^{1},u_{w}),\mathtt{Hd}_{q_{S}}(t^{1}_{w}),\mathtt{End}(t_{w}^{|S|+1})\\}\cup{}$
$\displaystyle\\{$ $\displaystyle\mathtt{Nxt}(t_{w}^{j-1},t_{w}^{j})\mid 2\leq
j\leq|S|+1\\}\cup{}$ $\displaystyle\\{$
$\displaystyle\mathtt{S}_{a}(t_{w}^{j})\mid 1\leq
j\leq|S|,a=S[j]\\}\cup\\{\mathtt{S}_{\text{\textvisiblespace}}(t_{w}^{|S|+1})\\}.$

Let $\mathcal{J}$ be the extension of $\mathcal{I}$ with
$\mathit{startConf}(\mathcal{I},u_{w})$ for every
$\mathtt{Leaf}(u_{w})\in\mathcal{I}$. We define
$\mathit{Int}_{4}(\mathcal{I})$ to be the smallest superset of $\mathcal{J}$
that satisfies all rules in $\mathcal{R}_{4}$ while including only the nulls
in $\mathcal{J}$. As in the case of $\mathit{Int}_{3}$, the missing relations
can easily be inferred using the original rules or, for (29) and (30), with
simple rewritings thereof.

######  Lemma 8.

$\mathfrak{I}_{4}=\\{\mathit{Int}_{4}(\mathcal{I})\mid\mathcal{I}\in\mathfrak{I}_{3}\\}$
is a universal model set of $\mathcal{R}_{4}$ and $\mathcal{D}$.

$\displaystyle\mathtt{Hd}_{q_{A}}(x)$ $\displaystyle\to\mathtt{Goal}$ (39)
$\displaystyle\mathtt{Nxt}(x,y)$ $\displaystyle\to\mathtt{Nxt}^{\\!+}(x,y)$
(40) $\displaystyle\mathtt{Nxt}^{\\!+}(x,y)\wedge\mathtt{Nxt}^{\\!+}(y,z)$
$\displaystyle\to\mathtt{Nxt}^{\\!+}(x,z)$ (41)
$\displaystyle\mathtt{Nxt}(x,y)\wedge\mathtt{Stp}(x,z)\wedge\mathtt{Stp}(y,w)$
$\displaystyle\to\mathtt{Nxt}(z,w)$ (42)

$\displaystyle\\!\\!\\!\\!\mathtt{End}(x)\,{\wedge}\,\mathtt{Stp}(x,z)$
$\displaystyle\to\exists
v.\mathtt{Nxt}(z,v)\,{\wedge}\,\mathtt{S}_{\text{\textvisiblespace}}(v)\,{\wedge}\,\mathtt{End}(v)$
(43)

$\displaystyle\mathtt{Hd}_{q}(x)\wedge\mathtt{S}_{a}(x)$
$\displaystyle\to\exists z.\mathtt{Stp}(x,z)\,{\wedge}\,\mathtt{S}_{b}(z)$
(44)
$\displaystyle\\!\\!\mathtt{Hd}_{q}(x)\,{\wedge}\,\mathtt{Nxt}^{\\!+}(x,y)\,{\wedge}\,\mathtt{S}_{c}(y)$
$\displaystyle\to\exists z.\mathtt{Stp}(y,z)\,{\wedge}\,\mathtt{S}_{c}(z)$
(45)
$\displaystyle\\!\\!\mathtt{Hd}_{q}(x)\,{\wedge}\,\mathtt{Nxt}^{\\!+}(y,x)\,{\wedge}\,\mathtt{S}_{c}(y)$
$\displaystyle\to\exists z.\mathtt{Stp}(y,z)\,{\wedge}\,\mathtt{S}_{c}(z)$
(46)

$\displaystyle\mathtt{Hd}_{q}(x)\wedge\mathtt{S}_{a}(x)\wedge\mathtt{Stp}(x,z)\wedge\mathtt{Nxt}(z,w)$
$\displaystyle\to\mathtt{Hd}_{r}(w)$ (47)
$\displaystyle\mathtt{Hd}_{q}(x)\wedge\mathtt{S}_{a}(x)\wedge\mathtt{Stp}(x,z)\wedge\mathtt{Nxt}(w,z)$
$\displaystyle\to\mathtt{Hd}_{r}(w)$ (48)

Figure 6: The rule set $\mathcal{R}_{5}$ contains $\mathcal{R}_{4}$ (see
Figure 4) and the above rules, where we instantiate rules (44)–(46) for all
transitions $(q,a)\mapsto(r,b,X)\in\delta$ and $c\in\Gamma$; rule (47) for all
$(q,a)\mapsto(r,b,+1)\in\delta$; and rule (48) for all
$(q,a)\mapsto(r,b,-1)\in\delta$.

####  $\mathbf{\mathcal{R}_{5}}$: TM Run

The purpose of $\mathcal{R}_{5}$ is to simulate the run of the deterministic
TM $\langle Q,\Gamma,\delta\rangle$ on each of the initial tapes created by
$\mathcal{R}_{4}$. We continue to use predicate $\mathtt{Nxt}$ for
neighbouring tape cells (augmented with its transitive closure
$\mathtt{Nxt}^{\\!+}$), $\mathtt{S}_{b}$ to encode tape symbols $b\in\Gamma$,
and $\mathtt{Hd}_{q}$ to encode head position and current state $q\in Q$.
Predicate $\mathtt{Stp}$ connects tape cells in each configuration to the
corresponding tape cells in the next configuration (provided the TM performs
another step). The rules in Figure 6 are a standard TM encoding, with the
slight exception of rule (43), which adds a new blank tape cell in each step
(even if not used by the TM). Our rules use the assumptions on TMs in Section
2.

Consider some $\mathcal{I}\in\mathfrak{I}_{4}$. It is easy and only mildly
laborious to define interpretations $\mathit{Run}(u_{w})$ that represent all
successor configurations of the starting configuration
$\mathit{startConf}(\mathcal{I},u_{w})$, appropriately connected with
$\mathtt{Stp}$ and the transitive closure $\mathtt{Nxt}^{\\!+}$. Moreover, let
$\mathcal{J}$ be the extension of $\mathcal{I}$ with all $\mathtt{Nxt}^{\\!+}$
required to satisfy (40) and (41) (note that $\mathtt{Nxt}$ also occurs in
encodings from $\mathcal{R}_{3}$). We define $\mathit{Int}_{5}(\mathcal{I})$
as the union of $\mathcal{J}$ with the interpretations $\mathit{Run}(u_{w})$
for all $u_{w}$ with $\mathtt{Leaf}(u_{w})\in\mathcal{I}$.

######  Lemma 9.

$\mathfrak{I}_{5}=\\{\mathit{Int}_{5}(\mathcal{I})\mid\mathcal{I}\in\mathfrak{I}_{4}\\}$
is a universal model set of $\mathcal{R}_{5}$ and $\mathcal{D}$.

#### Proving Lemma 4

To complete the proof of Lemma 4, we set $\mathfrak{M}=\mathfrak{I}_{5}$. For
$\mathcal{I}\in\mathfrak{M}$, let
$\mathit{Db}(\mathcal{I})=\\{\mathtt{p}(\vec{t})\mid\mathtt{In}_{\mathtt{p}}(\vec{t})\in\mathcal{I}\\}$
denote the completed database created by $\mathcal{R}_{1}$. Due to rule (4) in
Figure 1, there is a homomorphism $\mathcal{D}\to\mathit{Db}(\mathcal{I})$.
Moreover, the representation tree constructed for $\mathcal{I}$ by
$\mathcal{R}_{2}$ has a branch that is maximal, i.e., has
$|\mathit{Order}(\mathcal{I})|$ nodes; this branch has a leaf $u_{w}$ with
$|w|=|\mathit{Order}(\mathcal{I})|$. We obtain a homomorphism
$\mathit{Db}(\mathcal{I})\to\mathit{branchDb}(\mathcal{I},u_{w})$. Lemma 4 now
follows from Lemma 9 and Lemmas 11 and 10 below.

######  Lemma 10.

If $\mathcal{D}\in\mathfrak{Q}$, then $\mathtt{Goal}\in\mathcal{I}$ for each
$\mathcal{I}\in\mathfrak{M}$.

###### Proof.

As shown above, there is a homomorphism
$\mathcal{D}\to\mathit{branchDb}(\mathcal{I},u_{w})$ for the node $u_{w}$
where $|w|=|\mathit{Order}(\mathcal{I})|$. Since $\mathfrak{Q}$ is closed
under homomorphisms, $\mathcal{D}\in\mathfrak{Q}$ implies
$\mathit{branchDb}(\mathcal{I},u_{w})\in\mathfrak{Q}$. By the correctness of
our TM simulation, we obtain $\mathtt{Goal}\in\mathcal{I}$. ∎

######  Lemma 11.

If $\mathcal{D}\notin\mathfrak{Q}$, then $\mathtt{Goal}\notin\mathcal{I}$ for
some $\mathcal{I}\in\mathfrak{M}$.

###### Proof.

Consider some $\mathcal{I}\in\mathfrak{M}$ such that
$\mathit{Db}(\mathcal{I})=\mathcal{D}$ and $\mathtt{NEq}(t,u)\in\mathcal{I}$
for each $t,u\in\mathsf{Nulls}(\mathcal{D})$ with $t\neq u$. Let $u_{w}$
denote the leaf node with $|w|=|\mathit{Order}(\mathcal{I})|$ as before. Then
$\mathit{branchDb}(\mathcal{I},u_{w})$ is isomorphic to
$\mathit{Db}(\mathcal{I})=\mathcal{D}$. By the correctness of our TM
simulation, $\mathtt{Goal}$ is not derived from this maximal branch. Moreover,
for all other leaf nodes $u_{v}$ with $\mathtt{Leaf}(u_{v})\in\mathcal{I}$,
there is a homomorphism
$\mathit{branchDb}(\mathcal{I},u_{v})\to\mathit{branchDb}(\mathcal{I},u_{w})$.
Since $\mathfrak{Q}$ is closed under homomorphisms, the TM does not accept any
such $\mathit{branchDb}(\mathcal{I},u_{v})$, so
$\mathtt{Goal}\notin\mathcal{I}$. ∎

##  4 Ensuring Chase Termination

While the rules in Section 3 are semantically correct, the disjunctive chase
may not terminate on them. Many known fragments of existential rules can
guarantee chase termination, including for expressive cases where termination
might be exponential (?), but they are not applicable to our case, since the
runtime of TMs that decide a query can in general not be bounded by any
elementary function. Indeed, we rely on the TM to stop “naturally”, by virtue
of being a decider. Nevertheless, our rules lead to infinite chase trees,
e.g., if the disjunctive guessing of $\mathtt{LT}$ leads to a cycle, which
enables rule (16) to create an infinite path in the representation tree. We
will now show that this can be avoided:

######  Theorem 12.

Every homomorphism-closed decidable query is expressed by a set of disjunctive
rules that is chase-terminating for all databases over the schema of the
query.

To show this, we refine and generalise the “emergency brake” technique of ?
(?), and re-formulate it as a general rule set transformation. This not only
yields a generic method that is of independent interest, but it also allows us
to address potential termination problems in our prior modelling.

######  Definition 3.

Consider a rule set $\Sigma$ and a nullary predicate $\mathtt{Halt}$ that does
not occur in $\Sigma$. For every predicate $\mathtt{p}$ in $\Sigma$, let
$\hat{\mathtt{p}}$ be a fresh predicate of the same arity, and, for any
formula $\psi$, let $\hat{\psi}$ be $\psi$ with all predicates $\mathtt{p}$
replaced by $\hat{\mathtt{p}}$. Now the set
$\mathit{brake}(\Sigma,\mathtt{Halt})$ consists of the following rules:

$\displaystyle\textstyle\to\exists v.\mathtt{Brake}(v)$ (49)
$\displaystyle\mathtt{Halt}\wedge\mathtt{Brake}(x)$
$\displaystyle\to\mathtt{Real}(x)$ (50)
$\displaystyle\textstyle\hat{\mathtt{p}}(\vec{x})\wedge\bigwedge_{x\in\vec{x}}\mathtt{Real}(x)$
$\displaystyle\to\mathtt{p}(\vec{x})\qquad\text{for all $\mathtt{p}$ in
$\Sigma$}$ (51)

For every rule
$\rho:\beta[\vec{x}]\to\bigvee_{i=1}^{k}\exists\vec{y}_{i}.\eta_{i}[\vec{x}_{i},\vec{y}_{i}]$:

$\displaystyle\begin{split}\beta[\vec{x}]\,{\wedge}\,\mathtt{Brake}(v)&\textstyle\to\bigvee_{i=1}^{k}\big{(}\mathtt{B}_{\rho}^{i}(\vec{x}_{i})\,{\wedge}\,\hat{\eta}_{i}[\vec{x_{i}},\vec{y}_{i}\mapsto
v]\,{\wedge}\\\
&\textstyle\phantom{{}\to\bigvee_{i=1}^{k}(}\bigwedge_{x\in\vec{x}_{i}}\mathtt{Real}(x)\big{)}\end{split}$
(52) $\displaystyle\mathtt{B}_{\rho}^{i}(\vec{x}_{i})$
$\displaystyle\textstyle\to\exists\vec{y}_{i}.\hat{\eta}_{i}[\vec{x_{i}},\vec{y_{i}}]\wedge\bigwedge_{y\in\vec{y}_{i}}\mathtt{Real}(y)$
(53)

where $\hat{\eta}_{i}[\vec{x_{i}},\vec{y}_{i}\mapsto v]$ is $\hat{\eta}_{i}$
with each variable $y\in\vec{y}_{i}$ replaced by $v$, and $\mathtt{Brake}$,
$\mathtt{Real}$, and all $\mathtt{B}_{\rho}^{i}$ are fresh predicates with
arities as indicated.

Note that $\mathit{brake}(\Sigma,\mathtt{Halt})$ does not define rules to
derive $\mathtt{Halt}$, and indeed the transformation largely preserves the
models of $\Sigma$ in the following sense:

######  Lemma 13.

Consider a rule set $\Sigma$ and database $\mathcal{D}$ over predicates that
occur in $\Sigma$. For every model $\mathcal{I}$ of
$\mathit{brake}(\Sigma,\mathtt{Halt})$ and $\mathcal{D}$, the set
$\mathcal{I}^{-}=\\{\mathtt{p}(\vec{n})\mid\mathtt{p}(\vec{n})\in\mathcal{I},\mathtt{p}\text{
occurs in }\Sigma\\}$ is a model of $\Sigma$ and $\mathcal{D}$, and every
model $\mathcal{J}$ of $\Sigma$ and $\mathcal{D}$ is of this form.

###### Proof.

Consider a rule $\rho\in\Sigma$ as in Definition 3, and let $\sigma$ be a
substitution such that $\sigma(\beta)\subseteq\mathcal{I}^{-}$. Then we can
apply rules (52), (53), and finally (51) to derive
$\sigma^{\prime}(\eta_{i})\subseteq\mathcal{I}^{-}$ for a suitable extension
$\sigma^{\prime}$ of $\sigma$. Hence $\mathcal{I}^{-}\models\Sigma$.

Conversely, let $\mathcal{J}\models\Sigma$. A model $\mathcal{I}$ of
$\mathit{brake}(\Sigma,\mathtt{Halt})$ can be found by adding, for each
matching body $\sigma(\beta)\subseteq\mathcal{J}$ of rule $\rho$, an atom
$\sigma(\mathtt{B}_{\rho}^{i}(\vec{x}_{i}))$ for some $i$ such that
$\sigma^{\prime}(\eta_{i})\subseteq\mathcal{J}$ for an extension
$\sigma^{\prime}$ of $\sigma$. To obtain the required model $\mathcal{I}$ of
$\mathit{brake}(\Sigma,\mathtt{Halt})$, it remains to add facts
$\mathtt{Brake}(b)$ for a fresh null $b$,
$\sigma(\hat{\eta}_{i}[\vec{x_{i}},\vec{y}_{i}\mapsto b])$ as in (52) for
every $\sigma(\mathtt{B}_{\rho}^{i}(\vec{x}_{i}))\in\mathcal{I}$, and
$\mathtt{Real}(n)$ for every $\mathtt{p}(\vec{n})\in\mathcal{J}$ and
$n\in\vec{n}$. ∎

For $\mathit{brake}(\Sigma,\mathtt{Halt})$ to be useful, we need to add rules
that can “pull the brake” by deriving $\mathtt{Halt}$. Doing so stops the
chase in the following sense:

######  Lemma 14.

Consider a rule set $\Sigma$, a database $\mathcal{D}$ over predicates that
occur in $\Sigma$, and a set $\Pi$ of rules of the form
$\beta\to\mathtt{Halt}$ where $\beta$ only uses predicates in $\Sigma$. If
$\mathcal{I}$ is the label of a node in a chase tree for $\Sigma\cup\Pi$ and
$\mathcal{D}$ such that $\mathtt{Halt}\in\mathcal{I}$, then the tree starting
at the node of $\mathcal{I}$ is finite.

###### Proof.

Since $\mathtt{Halt}\in\mathcal{I}$, there is a substitution $\sigma$ such
that $\langle\rho_{\eqref{rul_brake_halt}},\sigma\rangle$ is applicable (for
$\rho_{\eqref{rul_brake_halt}}$ in (50)). By fairness,
$\mathtt{Real}(\sigma(x))$ will be derived at some depth of the tree. From
this depth on, no rule of form (53) is applicable: given
$\mathtt{Real}(\sigma(x))$, the head of rules of form (52) already satisfies
the head of the rule (53) that could be applied to a newly derived atom for
$\mathtt{B}_{\rho}^{i}$. Rules other than (53) do not contain existential
quantifiers thus can only be applied a finite number of times before the chase
on this part of the tree terminates. ∎

If $\mathtt{Halt}$ is derived, the semantic correspondence of Lemma 13 is
weakened, but suffices to preserve entailments:

######  Lemma 15.

Consider $\Sigma$, $\mathcal{D}$, and $\Pi$ as in Lemma 14. For every model
$\mathcal{I}$ of $\mathit{brake}(\Sigma,\mathtt{Halt})\cup\Pi$ and
$\mathcal{D}$, $\mathcal{I}^{-}$ (as in Lemma 13) is a model of $\Sigma$ and
$\mathcal{D}$.

###### Proof.

This is immediate from Lemma 13 and the fact that every model of
$\mathit{brake}(\Sigma,\mathtt{Halt})\cup\Pi$ and $\mathcal{D}$ is also a
model of $\mathit{brake}(\Sigma,\mathtt{Halt})$ and $\mathcal{D}$. ∎

Having established the key properties of the emergency brake construction, we
can now apply it to show Theorem 12. Given the rule set $\mathcal{R}_{5}$ as
defined for a query $\mathfrak{Q}$ in Section 3, let $\mathcal{R}_{6}$ denote
the extension of $\mathit{brake}(\mathcal{R}_{5},\mathtt{Halt})$ with the
following rules:

$\displaystyle\mathtt{In}_{\mathtt{p}}(\vec{x})\wedge\mathtt{NIn}_{\mathtt{p}}(\vec{x})$
$\displaystyle\to\mathtt{Halt}$ (54) $\displaystyle\mathtt{LT}(x,x)$
$\displaystyle\to\mathtt{Halt}$ (55)
$\displaystyle\mathtt{Last}(x)\wedge\mathtt{LT}(x,y)$
$\displaystyle\to\mathtt{Halt}$ (56)
$\displaystyle\mathtt{LT}(x,y)\wedge\mathtt{First}(y)$
$\displaystyle\to\mathtt{Halt}$ (57)

######  Lemma 16.

$\mathcal{R}_{6}$ expresses the query $\mathfrak{Q}$.

###### Proof.

For a database $\mathcal{D}$ over $\mathcal{S}$, let $\mathfrak{M}$ be the
universal model set constructed in Section 3. If $\mathcal{D}\in\mathfrak{Q}$,
then $\mathcal{R}_{5},\mathcal{D}\models\mathtt{Goal}$ by Theorem 3. Then
$\mathcal{R}_{6},\mathcal{D}\models\mathtt{Goal}$ since any model of
$\mathcal{R}_{6}$ and $\mathcal{D}$ must contain $\mathtt{Goal}$ by Lemma 15.

Conversely, if $\mathcal{D}\notin\mathfrak{Q}$, then there is
$\mathcal{U}\in\mathfrak{M}$ with $\mathtt{Goal}\notin\mathcal{U}$. By Lemma
13, there is a model $\mathcal{I}$ of
$\mathit{brake}(\mathcal{R}_{5},\mathtt{Halt})$ with
$\mathcal{I}^{-}=\mathcal{U}$, and hence $\mathtt{Goal}\notin\mathcal{I}$. By
construction of $\mathfrak{M}$, none of the rules (54)–(57) applies to
$\mathcal{U}$, and hence $\mathcal{I}$ is also a model of $\mathcal{R}_{6}$,
i.e., $\mathcal{R}_{6},\mathcal{D}\not\models\mathtt{Goal}$. ∎

######  Lemma 17.

$\mathcal{R}_{6}$ is chase-terminating for all databases over the schema
$\mathcal{S}$ of the query $\mathfrak{Q}$.

###### Proof.

Consider a chase over $\mathcal{R}_{6}$ and input database $\mathcal{D}$.
Chase branches where $\mathtt{Halt}$ is eventually part of a node label
terminate by Lemma 14. Let $b$ denote any branch of the chase where
$\mathtt{Halt}$ is not derived, and let $\mathcal{I}$ be the union of all node
labels on that branch. We want to show that $\mathcal{I}$ (and hence $b$) is
finite.

By Lemma 13, $\mathcal{I}\models\mathcal{R}_{1}$. Moreover, since
$\mathtt{Halt}\notin\mathcal{I}$, rules (54)–(57) are not applicable to
$\mathcal{I}$. Both properties together suffice to show that the set
$\mathcal{I}_{\mathcal{R}_{1}}=\\{\mathtt{p}(\vec{n})\in\mathcal{I}\mid\mathtt{p}$
is a predicate in $\mathcal{R}_{1}\\}$ is an element of $\mathfrak{I}_{1}$
defined in Section 3.

Since the predicates in rule bodies of $\mathcal{R}_{1}$ do not occur in any
rule head in $\mathcal{R}_{5}\setminus\mathcal{R}_{1}$, we can assume without
loss of generality (and without affecting chase termination), that the
corresponding rules of
$\mathit{brake}(\mathcal{R}_{1},\mathtt{Halt})\subseteq\mathcal{R}_{6}$ have
been applied first. This shows that $\mathcal{I}$ is equal to the result of a
chase with non-disjunctive rules
$\mathcal{R}_{6}\setminus\mathit{brake}(\mathcal{R}_{1},\mathtt{Halt})$ on a
database $\mathcal{I}_{\mathcal{R}_{1}}\in\mathfrak{I}_{1}$. The claim follows
by noting that any such chase must terminate: this was shown in Section 3,
where we described a deterministic process of defining the elements in the
universal model set $\mathfrak{I}_{5}$ from those in $\mathfrak{I}_{1}$. Each
steps in this construction is fully determined and introduces isomorphic sets
of nulls irrespectively of the order of rule applications. The only exception
are application of rules (15), (16), and (18). For example, given facts
$\mathtt{First}(n_{1})$, $\mathtt{First}(n_{2})$, and
$\mathtt{Eq}(n_{1},n_{2})$, the standard model of Section 3 contains one fact
$\mathtt{Root}(u_{1})$ with $\mathtt{Rep}(n_{1},u_{1})$ and
$\mathtt{Rep}(n_{2},u_{1})$, which can be obtained using (15) (on $n_{1}$) and
(18). If we apply (15) to both $n_{1}$ and $n_{2}$ before applying (18), we
obtain two distinct $\mathtt{Root}(u_{1})$ and
$\mathtt{Root}(u_{1}^{\prime})$. Similar variations can occur with other tree
nodes if (16) is applied before (18). If is easy to see that this does not
endanger termination, but merely leads to several isomorphic paths in the
representation tree. ∎

Together, Lemmas 16 and 17 show Theorem 12.

##  5 Removing Disjunctions

$\displaystyle\rightarrow\exists
w.\mathtt{Init}(w)\wedge\mathtt{Done}(w)\wedge\mathtt{Empty}(w)$ (58)
$\displaystyle\mathtt{Done}(w)\wedge\mathtt{Init}(w)\wedge\mathtt{p}(\vec{x})$
$\displaystyle\rightarrow\exists
w^{\prime}.\mathtt{Ins_{\mathtt{p}}}(\vec{x},w,w^{\prime})\wedge\mathtt{Subs}(w^{\prime},w^{\prime})\wedge\mathtt{Init}(w^{\prime})$
(59)
$\displaystyle\textstyle\mathtt{Done}(w)\wedge\bigwedge_{\mathtt{p}(\vec{x})\in\beta}\mathtt{Ins_{\mathtt{p}}}(\vec{x},w,w)$
$\displaystyle\rightarrow\exists
w_{1}.\mathtt{Ins_{\mathtt{p}_{1}}}(\vec{x_{1}},w,w_{1})\wedge\mathtt{Subs}(w_{1},w_{1})$
(60)
$\displaystyle\textstyle\mathtt{Done}(w)\wedge\bigwedge_{\mathtt{p}(\vec{x})\in\beta}\mathtt{Ins_{\mathtt{p}}}(\vec{x},w,w)$
$\displaystyle\rightarrow\exists
w_{2}.\mathtt{Ins_{\mathtt{p}_{2}}}(\vec{x_{2}},w,w_{2})\wedge\mathtt{Subs}(w_{2},w_{2})$
(61)
$\displaystyle\mathtt{Ins_{\mathtt{p}}}(\vec{x},w_{0},w_{1})\wedge\mathtt{Subs}(w_{1},w_{2})$
$\displaystyle\rightarrow\mathtt{Ins_{\mathtt{p}}}(\vec{x},w_{2},w_{2})\wedge\mathtt{\mathtt{p}^{\prime}}(\vec{x},w_{2})\wedge\mathtt{Subs}(w_{0},w_{2})$
(62) $\displaystyle\mathtt{Empty}(w)\wedge\mathtt{Subs}(w,w^{\prime})$
$\displaystyle\rightarrow\mathtt{Done}(w^{\prime})$ (63) Figure 7: The rule
set $\Sigma^{\prime}_{1}$, where we instantiate (59) and (62) for all
$\mathtt{p}\in\mathsf{Preds}$ in $\Sigma_{1}\cup\Sigma_{2}$, and (60) and (61)
for all
$\beta\rightarrow\mathtt{p}_{1}(\vec{x_{1}})\vee\mathtt{p}_{2}(\vec{x_{2}})\in\Sigma_{1}$.
$\displaystyle\mathtt{Done}(w)\wedge\textstyle\bigwedge_{\mathtt{p}(\vec{x})\in\beta}\mathtt{\mathtt{p}^{\prime}}(\vec{x},w)$
$\displaystyle\textstyle\rightarrow\exists\vec{z}.\bigwedge_{\mathtt{q}(\vec{y})\in\eta}\mathtt{\mathtt{q}^{\prime}}(\vec{y},w)$
(64) Figure 8: The rule set $\Sigma^{\prime}_{2}$, where we instantiate (64)
for all $\beta\rightarrow\exists\vec{z}.\eta\in\Sigma_{2}$.
$\displaystyle\mathtt{\mathtt{Goal}^{\prime}}(w)$
$\displaystyle\to\mathtt{Acc}(w)$ (65)
$\displaystyle\begin{split}\mathtt{Ins_{\mathtt{p}_{1}}}(\vec{x}_{1},w,w_{1})\wedge\mathtt{Acc}(w_{1})\wedge{}\\\
\mathtt{Ins_{\mathtt{p}_{2}}}(\vec{x}_{2},w,w_{2})\wedge\mathtt{Acc}(w_{2})\wedge{}\\\
\textstyle\bigwedge_{\mathtt{p}(\vec{x})\in\beta}\mathtt{Ins_{\mathtt{p}}}(\vec{x},w,w)&\to\mathtt{Acc}(w)\end{split}$
(66) $\displaystyle\mathtt{Init}(w)\wedge\mathtt{Acc}(w)$
$\displaystyle\to\mathtt{Goal}$ (67) Figure 9: The rule set
$\Sigma^{\prime}_{3}$, where (66) is instantiated for all rules
$\beta\rightarrow\mathtt{p}_{1}(\vec{x_{1}})\vee\mathtt{p}_{2}(\vec{x_{2}})\in\Sigma_{1}$

Our main result is that any decidable homomorphism-closed query is expressible
by a chase-terminating existential rule set. To conclude the proof of this
statement, we remove the disjunction from the rule set $\mathcal{R}_{6}$ of
Section 4. We present this as a general technique of expressing disjunctive
Datalog using existential rules, which is also of independent interest.

For a rule set $\Sigma$, the _input schema_
$\mathcal{S}_{\mathsf{in}}(\Sigma)$ is the set of all predicates in $\Sigma$
that do not occur in any rule head. We focus on rule sets that can be split
into a disjunctive part and an existential part, such that it is admissible to
completely apply the disjunctive rules first, and the existential ones
afterwards:

######  Definition 4.

A _split_ of a set $\Sigma$ of disjunctive existential rules consists of a set
$\Sigma_{1}$ of disjunctive Datalog rules and a set $\Sigma_{2}$ of
existential rules, such that $\Sigma=\Sigma_{1}\cup\Sigma_{2}$ and:

> For every database $\mathcal{D}$ over $\mathcal{S}_{\mathsf{in}}(\Sigma)$,
> and for every chase result $\mathfrak{M}$ over
> $\langle\Sigma,\mathcal{D}\rangle$, there is a chase result
> $\mathfrak{M}_{1}$ over $\langle\Sigma_{1},\mathcal{D}\rangle$, such that
> $\mathfrak{M}=\\{\mathcal{C}_{\mathcal{I}}\mid\mathcal{I}\in\mathfrak{M}_{1}\\}$
> where each $\mathcal{C}_{\mathcal{I}}$ is the (unique) interpretation
> resulting from some chase over $\langle\Sigma_{2},\mathcal{I}\rangle$.

######  Lemma 18.

Consider a rule set $\Sigma$ with split $\langle\Sigma_{1},\Sigma_{2}\rangle$.
There is a set $\Sigma^{\prime}$ of existential rules, such that, for every
database $\mathcal{D}$ over $\mathcal{S}_{\mathsf{in}}(\Sigma)$, we have:

  1. 1.

$\mathcal{D},\Sigma\models\mathtt{Goal}$ iff
$\mathcal{D},\Sigma^{\prime}\models\mathtt{Goal}$, and

  2. 2.

if $\langle\Sigma_{2},\mathcal{D}_{2}\rangle$ is chase-terminating for every
database $\mathcal{D}_{2}$ over $\mathcal{S}_{\mathsf{in}}(\Sigma_{2})$, then
$\langle\Sigma^{\prime},\mathcal{D}\rangle$ is also chase-terminating.

To construct this set $\Sigma^{\prime}$, we assume w.l.o.g. that all
disjunctive rules have exactly two disjuncts in the head. We define
$\Sigma^{\prime}$ as the union of sets $\Sigma^{\prime}_{1}$,
$\Sigma^{\prime}_{2}$ and $\Sigma^{\prime}_{3}$ as shown in Figures 7, 8 and
9, which we explain below.

$\Sigma^{\prime}_{1}$ uses a technique for modelling sets with chase-
terminating existential rules (?, Fig. 2). We adapt this to sets of ground
atoms, called _worlds_ and denoted by variables $w$ in the figures. Facts
$\mathtt{Ins_{\mathtt{p}}}(\vec{t},w,w^{\prime})$ express that world
$w^{\prime}$ is obtained by adding $\mathtt{p}(\vec{t})$ to world $w$. In
particular, $\mathtt{Ins_{\mathtt{p}}}(\vec{t},w,w)$ states that
$\mathtt{p}(\vec{t})$ is in $w$, and we define
$\mathsf{world}(w)=\\{\mathtt{p}(\vec{a})\mid\mathtt{Ins_{\mathtt{p}}}(\vec{a},w,w)\in\mathcal{I}\\}$
for any interpretation $\mathcal{I}$. Worlds are created by adding database
facts (59) or by applying rules to existing worlds (60)–(61). Worlds
containing only database facts are marked with $\mathtt{Init}$. Predicate
$\mathtt{Subs}$ defines the subset relation on worlds. Rules (62)–(63) copy
all prior facts to a new world before marking it $\mathtt{Done}$.

######  Proposition 19.

$\Sigma^{\prime}_{1}$ is chase-terminating and for every $\mathcal{D}$ over
$\mathcal{S}_{\mathsf{in}}(\Sigma)$, the (unique) interpretation $\mathcal{I}$
resulting from some chase over $\Sigma^{\prime}_{1}$ and $\mathcal{D}$ is such
that:

  * •

if $\mathtt{p}(\vec{a})\in\mathcal{D}$ and $\mathtt{Done}(w)\in\mathcal{I}$,
there exists $w^{\prime}$ such that
$\mathtt{Ins_{\mathtt{p}}}(\vec{a},w,w^{\prime})\in\mathcal{I}$ and
$\mathsf{world}(w^{\prime})=\mathsf{world}(w)\cup\\{\mathtt{p}(\vec{a})\\}$;

  * •

if $\rho\in\Sigma_{1}$ is applicable to $\mathsf{world}(w)$, creating
$\mathtt{p}_{1}(\vec{a})$ or $\mathtt{p}_{2}(\vec{b})$, there exists $w_{1}$
and $w_{2}$ such that
$\\{\mathtt{Ins_{\mathtt{p}_{1}}}(\vec{a},w,w_{1}),\mathtt{Ins_{\mathtt{p}_{2}}}(\vec{b},w,w_{2})\\}\subseteq\mathcal{I}$,
$\mathsf{world}(w_{1})=\mathsf{world}(w)\cup\\{\mathtt{p}_{1}(\vec{a})\\}$ and
$\mathsf{world}(w_{2})=\mathsf{world}(w)\cup\\{\mathtt{p}_{2}(\vec{b})\\}$.

Note that we cannot distinguish worlds that are not containing all database
facts, and that some worlds may contain more facts than needed to satisfy all
disjunctive heads.

$\Sigma^{\prime}_{2}$ now simulates the application of rules from $\Sigma_{2}$
in any of the worlds. Computations relative to different worlds are
independent from each other. Finally, $\Sigma^{\prime}_{3}$ aggregates results
from all worlds: a world is accepting ($\mathtt{Acc}$) if either
$\mathtt{Goal}$ was derived locally (65) or it has two successor worlds for a
disjunctive rule that are both accepting (66). $\mathtt{Goal}$ is a
consequence if any initial world is accepting (67). This finishes the
construction of $\Sigma^{\prime}$ as the main ingredient for proving Lemma 18.

Finally, we can apply Lemma 18 to
$\mathcal{R}_{6}=\mathit{brake}(\mathcal{R}_{5},\mathtt{Halt})\cup\Pi$ from
Section 4, where $\Pi$ denotes rules (54)–(57). Intuitively, a possible split
is $\mathit{brake}(\mathcal{R}_{1},\mathtt{Halt})$ and
$\mathit{brake}(\mathcal{R}_{5}\setminus\mathcal{R}_{1},\mathtt{Halt})\cup\Pi$.
Formally, however, $\mathit{brake}(\mathcal{R}_{1},\mathtt{Halt})$ is not
disjunctive Datalog due to existential rules (2), (3), and (49). However, our
result easily extends to such rules with empty body: we can just add them to
$\Sigma_{1}^{\prime}$ and treat their inferences like facts from the initial
database. The other properties of Definition 4 are easy to verify. The fact
that both rule sets have some common rules, such as (50), is no concern.
Finally, it remains to argue termination for $\Sigma_{2}$ as required for item
(2) in Lemma 18. This is slightly stronger than Lemma 17 since we must also
consider databases that use some inferred predicates of $\mathcal{R}_{1}$.
However, the proof of Lemma 17 and the emergency brake technique in general
served the main purpose of safeguarding against problematic structures among
the inferred predicates of $\mathcal{R}_{1}$, and it is not hard to see that
this already showed what we require here. Combining all of our insights, we
finally obtain:

######  Theorem 20.

Chase-terminating existential rules capture the class of all decidable
homomorphism-closed queries.

##  6 Limitations of Semi-Decidable Languages

A _query language_ $\mathfrak{F}$ over a schema $\mathcal{S}$ is a function
from a set $L$ to $2^{\mathfrak{D}_{\mathcal{S}}}$, where
$\mathfrak{D}_{\mathcal{S}}$ is the set of all databases over schema
$\mathcal{S}$. We say that $\mathfrak{F}$ is _semi-decidable_ if membership to
$L$ is semi-decidable, and that its _query answering problem is decidable_ if
there exists a TM $M_{\mathfrak{F}}$ that takes as input some
$(l,\mathcal{D})\in(L\times\mathfrak{D}_{\mathcal{S}})$ and decides whether
$\mathcal{D}\in\mathfrak{F}(l)$.

The set of chase-terminating existential rule sets is a query language that is
not semi-decidable (?) and for which the query answering problem is decidable
(by running the chase). In fact, we show that one cannot find a semi-decidable
query language with similar properties.

######  Theorem 21.

There are no semi-decidable query languages that (i) express all decidable,
homomorphism-closed queries and (ii) for which query answering is decidable.

To show this result, we define a set $\mathcal{M}$ of TMs (cf. Definition 5),
show that $\mathcal{M}$ can be enumerated up to equivalence if there is a
semi-decidable language that satisfies (i) and (ii) above (cf. Lemma 22), and
finally prove that the consequence of this implication does not hold (cf.
Lemma 23).

######  Definition 5.

Consider the set $\mathcal{M}$ of all TMs $M$ such that: (i) The TM $M$ halts
on all inputs. (ii) If $M$ accepts some word $w$, then $w$ corresponds to a
database over schema $\\{\mathtt{ed}\\}$. (iii) Consider some words $w$ and
$v$ that correspond to some $\mathcal{D}$ and $\mathcal{E}$ in
$\mathfrak{D}_{\\{\mathtt{ed}\\}}$, respectively. If $M$ accepts $w$ and there
is a homomorphism $h:\mathcal{D}\to\mathcal{E}$, then $M$ accepts $v$.

Intuitively, $\mathcal{M}$ is the set of all deciders that solve homomorphism-
closed queries over databases in $\mathfrak{D}_{\\{\mathtt{ed}\\}}$.

######  Lemma 22.

If there is a semi-decidable query language $\mathfrak{F}$ that satisfies (i)
and (ii) in Theorem 21, then $\mathcal{M}$ is enumerable up to equivalence.

###### Proof.

If there is a language such as $\mathfrak{F}$, then there is an enumerator $P$
for $L$ that prints out a sequence $l_{1},\l_{2},\ldots$ and a decider
$M_{\mathfrak{F}}$ that can be used to check if
$\mathcal{D}\in\mathfrak{F}(l)$ for each
$(l,\mathcal{D})\in(L\times\mathfrak{D}_{\\{\mathtt{ed}\\}})$. For each $i\geq
1$, let $M_{i}$ be the TM that, on input $w$, performs the following
computation: if $w$ corresponds to a database
$\mathcal{D}\in\mathfrak{D}_{\\{\mathtt{ed}\\}}$ and $M_{\mathfrak{F}}$
accepts $(l_{i},\mathcal{D})$, then _accept_ ; otherwise, _reject_. By
modifying $P$ we can define an enumerator that prints out the sequence
$M_{1},M_{2},\ldots$, which contains $\mathcal{M}$ up to equivalence. ∎

######  Lemma 23.

The set $\mathcal{M}$ is not enumerable up to equivalence.

###### Proof Sketch.

Assume that there is an enumerator that outputs a sequence
$M_{1},M_{2},\ldots$ that includes $\mathcal{M}$ up to equivalence. We obtain
a contradiction by defining a sequence
$\mathcal{D}_{1},\mathcal{D}_{2},\ldots$ of databases and a TM
$M_{d}\in\mathcal{M}$ that diagonalises over $M_{1},M_{2},\ldots$ and
$\mathcal{D}_{1},\mathcal{D}_{2},\ldots$ Namely, for each $i\geq 1$, let
$\mathcal{D}_{i}=\\{\mathtt{ed}(u_{1},u_{2})$,
$\ldots,\mathtt{ed}(u_{p_{i+1}},u_{1})\\}$ where $p_{i+1}$ is the $(i+1)$-th
prime. Moreover, $M_{d}$ is the TM that, on input $w$, performs the
computation: (1) _Reject_ if $w$ does not correspond to some
$\mathcal{D}\in\mathfrak{D}_{\\{\mathtt{ed}\\}}$. (2) _Reject_ if
$\mathcal{D}$ can be hom-embedded into a path over $\mathtt{ed}$. (3) _Accept_
if $\mathtt{ed}(u,u)\in\mathcal{D}$ for some null $u$. (4) If there is some
$i\geq 1$ such that there are less nulls in $\mathcal{D}_{i}$ than in
$\mathcal{D}$, the TM $M_{i}$ accepts some serialisation that corresponds to
$\mathcal{D}_{i}$, and there is a homomorphism
$h:\mathcal{D}\to\mathcal{D}_{i}$; then _reject_. Otherwise, _accept_.∎

##  7 Discussion and Conclusion

In this paper, we have established a characterization of all decidable
homomorphism-closed Boolean queries. We showed that these are exactly the
chase-terminating existential rule queries, that is, queries that can be
expressed by a set of (non-disjunctive) existential rules for which the
standard chase universally terminates irrespective of the order of rule
applications (as long as it is fair).

By its nature, our result immediately shows that various extensions of our
framework do not increase its expressivity:

######  Theorem 24.

Chase-terminating existential rule queries have the same expressivity as

  1. 1.

existential rule queries with guaranteed existence of some finite chase tree
(for every database),

  2. 2.

existential rule queries for which the chase terminates according to some fair
strategy (such as datalog-first),

  3. 3.

core-chase-terminating existential rule queries,

  4. 4.

disjunctive chase-terminating existential rule queries.

###### Proof.

(3) Standard-chase termination implies core-chase termination. On the other
hand, core chase termination implies decidability and thus our result applies.
(1) and (2) Standard-chase termination implies these weaker form of
guarantees, which themselve imply core chase termination. (4) Obviously, every
(non-disjunctive) existential rule set is a special case of a disjunctive one
and for this special case, disjunctive chase termination coincides with
termination of the (non-disjunctive) standard chase. On the other hand,
disjunctive existential rule queries are also closed under homomorphisms, and
disjunctive universal chase termination obviously implies decidability. So our
result applies. ∎

However, the applicability of our result does not stop at (syntactic)
extensions of our framework, as it applies to arbitrary query languages and
querying formalisms of different types. In particular we would like to stress
the relationship to the very comprehensive existential rules fragment of
_bounded treewidth sets (bts) of rules_ (?) that is _not_ chase-terminating
and encompasses a plethora of well-known existential rule fragments with
decidable query entailment, including guarded (?), frontier-guarded (?), and
glut-guarded existential rules (?), as well as greedy bts (?):

######  Theorem 25.

Let $\Sigma$ be a bounded-treewidth set of rules and $Q$ a conjunctive query.
There is a chase-terminating set $\Sigma_{Q}$ of existential rules such that
$\mathcal{D},\Sigma\models Q$ iff
$\mathcal{D},\Sigma_{Q}\models\mathtt{Goal}$.

While possibly surprising, this is a straightforward consequence of
decidability of conjunctive query entailment from bts and of homomorphism-
closedness of existential rule queries in general. Note, however, that every
$Q$ would give rise to a different $\Sigma_{Q}$. In fact, asking for a
“uniform” chase-terminating existential rules set $\Sigma^{\prime}$ satisfying
$\mathcal{D},\Sigma^{\prime}\models Q$ iff $\mathcal{D},\Sigma\models Q$ would
change the game (?). Such a set will not exist in all cases.

While our result addresses many of the open questions regarding _expressivity_
of the terminating chase (?) an important avenue for future work is to
investigate potential differences when it comes to the corresponding
computational _complexities_. We deem it likely that not all of the discussed
chase variants give rise to worst-case optimal computations.

#### Acknowledgements

This work is partly supported by DFG in project number 389792660 (TRR 248,
Center for Perspicuous Systems), by BMBF in the Center for Scalable Data
Analytics and Artificial Intelligence (ScaDS.AI), by the Center for Advancing
Electronics Dresden (cfaed), by the ERC Consolidator Grant DeciGUT (project
number 771779), and by the ANR project CQFD (ANR-18-CE23-0003).

## References

  * Abiteboul, Hull, and Vianu 1995 Abiteboul, S.; Hull, R.; and Vianu, V.  1995\.  Foundations of Databases.  Addison-Wesley.
  * Baget et al. 2011a Baget, J.; Leclère, M.; Mugnier, M.; and Salvat, E.  2011a.  On rules with existential variables: Walking the decidability line.  Artif. Intell. 175(9-10):1620–1654.
  * Baget et al. 2011b Baget, J.; Mugnier, M.; Rudolph, S.; and Thomazo, M.  2011b.  Walking the complexity lines for generalized guarded existential rules.  In Walsh (?), 712–717.
  * 1984 Beeri, C., and Vardi, M. Y.  1984\.  A proof procedure for data dependencies.  J. ACM 31(4):718–741.
  * 2008 Calì, A.; Gottlob, G.; and Kifer, M.  2008\.  Taming the infinite chase: Query answering under expressive relational constraints.  In Brewka, G., and Lang, J., eds., Proc. 11th Int. Conf. on Knowledge Representation and Reasoning (KR’08), 70–80.  AAAI Press.
  * 2019 Carral, D.; Dragoste, I.; Krötzsch, M.; and Lewe, C.  2019\.  Chasing sets: How to use existential rules for expressive reasoning.  In Kraus, S., ed., Proc. 28th Int. Joint Conf. on Artificial Intelligence, IJCAI’19, 1624–1631.  ijcai.org.
  * 2017 Carral, D.; Dragoste, I.; and Krötzsch, M.  2017\.  Restricted chase (non)termination for existential rules with disjunctions.  In Sierra, C., ed., Proc. 26th Int. Joint Conf. on Artificial Intelligence, IJCAI’17, 922–928.  ijcai.org.
  * 2008 Deutsch, A.; Nash, A.; and Remmel, J. B.  2008\.  The chase revisited.  In Lenzerini, M., and Lembo, D., eds., Proc. 27th Symposium on Principles of Database Systems (PODS’08), 149–158.  ACM.
  * 2005 Fagin, R.; Kolaitis, P. G.; Miller, R. J.; and Popa, L.  2005\.  Data exchange: semantics and query answering.  Theoretical Computer Science 336(1):89–124.
  * 2018 Grahne, G., and Onet, A.  2018\.  Anatomy of the chase.  Fundam. Informaticae 157(3):221–270.
  * 2011 Krötzsch, M., and Rudolph, S.  2011\.  Extending decidable existential rules by joining acyclicity and guardedness.  In Walsh (?), 963–968.
  * 2019 Krötzsch, M.; Marx, M.; and Rudolph, S.  2019\.  The power of the terminating chase.  In Barceló, P., and Calautti, M., eds., Proc. 22nd Int. Conf. on Database Theory, ICDT’19, volume 127 of LIPIcs, 3:1–3:17.  Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
  * 2009 Marnette, B.  2009\.  Generalized schema-mappings: from termination to tractability.  In Paredaens, J., and Su, J., eds., Proc. 28th Symposium on Principles of Database Systems (PODS’09), 13–22.  ACM.
  * 2015 Rudolph, S., and Thomazo, M.  2015\.  Characterization of the expressivity of existential rule queries.  In Yang, Q., and Wooldridge, M., eds., Proc. 24th Int. Joint Conf. on Artificial Intelligence (IJCAI’15), 3193–3199.  AAAI Press.
  * 2011 Walsh, T., ed.  2011\.  Proc. 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI’11). AAAI Press/IJCAI.
  * 2015 Zhang, H.; Zhang, Y.; and You, J.  2015\.  Existential rule languages with finite chase: Complexity and expressiveness.  In Bonet, B., and Koenig, S., eds., Proc. 29th AAAI Conf. on Artificial Intelligence (AAAI’15).  AAAI Press.

##  Appendix A Proofs for Section 3

In this section, we prove the claims made in Section 3. In particular, besides
proving Lemmas 5, 6, 7, 8, 9, 10, and 11, we show Lemma 26 from which the next
claims (given in the order they occur in the section) follow.

  1. 1.

$|\mathfrak{I}_{1}|=|\mathfrak{I}_{2}|=|\mathfrak{I}_{3}|=|\mathfrak{I}_{4}|=|\mathfrak{I}_{5}|$.

  2. 2.

For each $1\leq i<j\leq 5$ and each $\mathcal{I}\in\mathfrak{I}_{i}$, there is
exactly one $\mathcal{J}\in\mathfrak{I}_{j}$ with
$\mathcal{I}\subseteq\mathcal{J}$.

  3. 3.

Every $\mathcal{I}\in\mathfrak{I}_{i}$ with $1\leq i\leq 5$ contains a unique
interpretation $\mathit{Seed}(\mathcal{I})\in\mathfrak{I}_{1}$, and there is a
unique ordered partition $\mathit{Order}(\mathcal{I})\in\mathit{Ords}$ such
that
$\mathit{Seed}(\mathcal{I})\in\mathit{Compls}(\mathit{Order}(\mathcal{I}))$.

Recall that
$\Delta=\mathsf{Nulls}(\mathcal{D})\cup\\{u_{\alpha},u_{\omega}\\}$. We will
call a $\mathcal{D}$-_order_ a database over schema
$\\{\mathtt{First},\mathtt{Last},\mathtt{LT},\mathtt{Eq},\mathtt{NEq}\\}$ and
nulls from $\Delta$, and a $\mathcal{D}$-_completion_ a database over schema
$\\{\mathtt{In}_{\mathtt{p}},\mathtt{NIn}_{\mathtt{p}}\mid\mathtt{p}\in\mathcal{S}\\}$
and nulls from $\Delta$. We say that a $\mathcal{D}$-completion is _complete_
if (i) it includes
$\\{\mathtt{In}_{\mathtt{p}}(\vec{t})\mid\mathtt{p}(\vec{t})\in\mathcal{D}\\}$
and (ii) for every $\mathtt{p}\in\mathcal{S}$ and tuple
$\vec{t}\subseteq\Delta$ of matching arity, it contains exactly one of
$\\{\mathtt{In}_{\mathtt{p}}(\vec{t}),\mathtt{NIn}_{\mathtt{p}}(\vec{t})\\}$.

######  Lemma 26.

There is a one-to-one correspondence between the interpretations in
$\mathfrak{I}_{i}$ ($1\leq i\leq 5$) and the pairs of the form
$(\vec{T},\mathcal{F}_{\mathcal{D}})$, where
$\vec{T}=T_{1},\ldots,T_{k}\in\mathit{Ords}$ is an ordered partition of
$\Delta$ with $u_{\alpha}\in T_{1}$ and $u_{\omega}\in T_{k}$, and
$\mathcal{F}_{\mathcal{D}}$ is a complete $\mathcal{D}$-completion. More
precisely:

  * •

An interpretation $\mathcal{I}\in\mathfrak{I}_{1}$ corresponds to a pair
$(\vec{T},\mathcal{F}_{\mathcal{D}})$ iff $\mathcal{I}$ is the union of the
following databases:

    * –

$\mathcal{D}\cup\\{\mathtt{DbDom}(t)\mid t\in\Delta\\}$,

    * –

the $\mathcal{D}$-order corresponding to $\vec{T}$: $\\{\mathtt{First}(t)\mid
t\in T_{1}\\}\cup\\{\mathtt{Last}(t)\mid t\in
T_{k}\\}\cup\\{\mathtt{Eq}(t,u)\mid 1\leq i\leq k;t,u\in
T_{i}\\}\cup\\{\mathtt{LT}(t,u),\mathtt{NEq}(t,u),\mathtt{NEq}(u,t)\mid 1\leq
i<j\leq k$, $t\in T_{i}$, $u\in T_{j}\\}$, and

    * –

$\mathcal{F}_{\mathcal{D}}$.

  * •

An interpretation $\mathcal{I}\in\mathfrak{I}_{i}$ ($2\leq i\leq 5$)
corresponds to $(\vec{T},\mathcal{F}_{\mathcal{D}})$ iff it includes some
$\mathcal{I}_{1}\in\mathfrak{I}_{1}$ that corresponds to
$(\vec{T},\mathcal{F}_{\mathcal{D}})$.

In particular, it follows that every $\mathcal{I}\in\mathfrak{I}_{i}$ with
$1\leq i\leq 5$ contains a unique interpretation
$\mathit{Seed}(\mathcal{I})\in\mathfrak{I}_{1}$, and there is a unique ordered
partition $\mathit{Order}(\mathcal{I})\in\mathit{Ords}$ such that
$\mathit{Seed}(\mathcal{I})\in\mathit{Compls}(\mathit{Order}(\mathcal{I}))$.

###### Proof.

The correspondence between interpretations in $\mathfrak{I}_{1}$ and pairs of
the form $(\vec{T},\mathcal{F}_{\mathcal{D}})$ is well defined because
$\mathfrak{I}_{1}=\bigcup_{\vec{T}\in\mathit{Ords}}\mathit{Compls}(\vec{T})$
where $\mathit{Compls}(\vec{T})$ is the set of all minimal models of
$\mathcal{R}_{1}$ and $\mathcal{D}$ that contain the $\mathcal{D}$-order
corresponding to $\vec{T}$. In particular, every
$\mathcal{I}\in\mathfrak{I}_{1}$ must include a complete
$\mathcal{D}$-completion to satisfy (14) and (4), and by minimality
$\mathcal{I}$ does not include any set of the form
$\\{\mathtt{In}_{\mathtt{p}}(\vec{t}),\mathtt{NIn}_{\mathtt{p}}(\vec{t})\\}$.
Moreover, by minimality, $\mathcal{I}$ does not contain any other atom over
predicates
$\\{\mathtt{First},\mathtt{Last},\mathtt{LT},\mathtt{Eq},\mathtt{NEq}\\}$.

Each $\mathfrak{I}_{i}$ ($2\leq i\leq 5$) is obtained from
$\mathfrak{I}_{i-1}$ by applying the function $\mathit{Int}_{i}$ to each of
its elements and by construction of $\mathit{Int}_{i}$,
$\mathcal{I}\subseteq\mathit{Int}_{i}(\mathcal{I})$ and
$\mathit{Int}_{i}(\mathcal{I})\setminus\mathcal{I}$ does not contain any atoms
on predicates from
$\mathcal{S}\cup\\{\mathtt{DbDom},\mathtt{First},\mathtt{Last},\mathtt{LT},\mathtt{Eq},\mathtt{NEq}\\}\cup\\{\mathtt{In}_{\mathtt{p}},\mathtt{NIn}_{\mathtt{p}}\mid\mathtt{p}\in\mathcal{S}\\}$.
Hence the one-to-one correspondence between elements of $\mathfrak{I}_{1}$ and
pairs of the form $(\vec{T},\mathcal{F}_{\mathcal{D}})$ is preserved when
applying $\mathit{Int}_{i}$ to elements of $\mathfrak{I}_{i-1}$ to obtain the
elements of $\mathfrak{I}_{i}$ for each $2\leq i\leq 5$. ∎

Lemma 5.
$\mathfrak{I}_{1}=\bigcup_{\vec{T}\in\mathit{Ords}}\mathit{Compls}(\vec{T})$
is a universal model set of $\mathcal{R}_{1}$ and $\mathcal{D}$.

###### Proof.

Let $\mathfrak{K}$ be the result of some chase tree for $\mathcal{R}_{1}$ and
$\mathcal{D}$ that prioritises the application of rules in the order of their
appearance in Figure 1. By Fact 2, $\mathfrak{K}$ is a universal model set for
$\mathcal{R}_{1}$ and $\mathcal{D}$ and we show that each
$\mathcal{K}\in\mathfrak{K}$ is isomorphic to a unique
$\mathcal{I}\in\mathfrak{I}_{1}$.

We use the one-to-one correspondence between the interpretations in
$\mathfrak{I}_{1}$ and the pairs of the form
$(\vec{T},\mathcal{F}_{\mathcal{D}})$ described in Lemma 26. Since
$\mathfrak{K}$ is a result of the chase on $\mathcal{R}_{1}$ and
$\mathcal{D}$, the domain of every $\mathcal{K}\in\mathfrak{K}$ contains all
nulls in $\mathsf{Nulls}(\mathcal{D})$ and exactly two fresh nulls introduced
to satisfy rules $\eqref{rul_createFirst}$ and $\eqref{rul_createLast}$,
respectively. We name them $u_{\alpha}$ and $u_{\omega}$ respectively, so that
$\Delta$ is the domain of $\mathcal{K}$, and define a one-to-one
correspondence between the interpretations in $\mathfrak{K}$ and the pairs of
the form $(\vec{T},\mathcal{F}_{\mathcal{D}})$ as in Lemma 26. This can be
done because of the following points:

  * •

Every $\mathcal{K}\in\mathfrak{K}$ includes $\mathcal{D}$ and does not contain
any other atom on predicates from $\mathcal{S}$ because such predicates do not
occur in rule heads.

  * •

Every $\mathcal{K}\in\mathfrak{K}$ includes $\\{\mathtt{DbDom}(t)\mid
t\in\Delta\\}$ and does not contain any other atom on predicate
$\mathtt{DbDom}$ (since there are no more nulls).

  * •

Every $\mathcal{K}\in\mathfrak{K}$ includes a $\mathcal{D}$-order
corresponding to some $\vec{T}\in\mathit{Ords}$ and does not contain any other
atom on predicates from
$\\{\mathtt{First},\mathtt{Last},\mathtt{LT},\mathtt{Eq},\mathtt{NEq}\\}$:

    * –

Let $\sim$ be the relation over $\Delta$ defined by $t\sim t^{\prime}$ iff
$\mathtt{Eq}(t,t^{\prime})\in\mathcal{K}$. This is an equivalence relation
because (i) $\\{\mathtt{DbDom}(t)\mid t\in\Delta\\}\subseteq\mathcal{K}$ and
$\mathcal{K}$ satisfies (5) (reflexivity); (ii) $\mathcal{K}$ satisfies (6)
(symmetry); and (iii) $\mathcal{K}$ satisfies (8) instantiated for
$\mathtt{R}=\mathtt{Eq}$ (transitivity). The equivalence classes form a
partition $T_{1},\dots,T_{k}$ of $\Delta$ such that $\\{\mathtt{Eq}(t,u)\mid
1\leq i\leq k;t,u\in T_{i}\\}\subseteq\mathcal{K}$.

    * –

For every $u,t\in\Delta$, $\mathcal{K}$ contains at least one of
$\\{\mathtt{Eq}(u,t),\mathtt{NEq}(u,t)\\}$ because it satisfies (9). Moreover,
$\mathcal{K}$ cannot contain both $\mathtt{Eq}(u,t)$ and $\mathtt{NEq}(u,t)$
because the rules (5), (6) and (8) have a higher priority than (9). Hence
$\\{\mathtt{NEq}(t,u),\mathtt{NEq}(u,t)\mid 1\leq i<j\leq k$, $t\in T_{i}$,
$u\in T_{j}\\}\subseteq\mathcal{K}$.

    * –

$\mathcal{K}$ includes $\\{\mathtt{First}(u)\mid u\sim u_{\alpha}\\}$ and
$\\{\mathtt{Last}(u)\mid u\sim u_{\omega}\\}$ by definition of
$u_{\alpha},u_{\omega}$ and because it satisfies (8). Assuming w.l.o.g. that
$T_{1}$ is the equivalence class of $u_{\alpha}$ and $T_{k}$ that of
$u_{\omega}$: $\\{\mathtt{First}(t)\mid t\in
T_{1}\\}\cup\\{\mathtt{Last}(t)\mid t\in T_{k}\\}\subseteq\mathcal{K}$.

    * –

$\mathcal{K}$ does not include any other atom over $\mathtt{First}$ or
$\mathtt{Last}$ because rules (2) and (3) are applied only once.

    * –

For every $u,t\in\Delta$ such that $\mathtt{NEq}(u,t)\in\mathcal{K}$,
$\mathcal{K}$ contains at least one of
$\\{\mathtt{LT}(u,t),\mathtt{LT}(t,u)\\}$ because it satisfies (13).

    * –

For every $u,t\in\Delta$, if $\mathtt{First}(u)\in\mathcal{K}$ (i.e. $u\sim
u_{\alpha}$) and $\mathtt{First}(t)\notin\mathcal{K}$ (i.e. $t\not\sim
u_{\alpha}$) then $\mathtt{LT}(u,t)\in\mathcal{K}$ because of (11).

    * –

For every $u,t\in\Delta$, if $\mathtt{Last}(u)\in\mathcal{K}$ (i.e. $u\sim
u_{\omega}$) and $\mathtt{Last}(t)\notin\mathcal{K}$ (i.e. $t\not\sim
u_{\omega}$) then $\mathtt{LT}(t,u)\in\mathcal{K}$ because of (12).

    * –

If $\mathtt{LT}(u,t)\in\mathcal{K}$ then
$\mathtt{LT}(u^{\prime},t^{\prime})\in\mathcal{K}$ for all $u^{\prime}\sim u$
and $t\sim t^{\prime}$ because $\mathcal{K}$ satisfies (8).

    * –

$\mathcal{K}$ contains the transitive closure of $\mathtt{LT}$ because it
satisfies (10).

    * –

Since the rules (11), (12), (5), (6), (8), and (10) have a higher priority
than (13), then $\mathcal{K}$ cannot contain both $\mathtt{LT}(u,t)$ and
$\mathtt{LT}(t,u)$.

    * –

Hence $T_{1},\dots,T_{k}$ can be ordered in a way such that
$\\{\mathtt{LT}(t,u)\mid 1\leq i<j\leq k$, $t\in T_{i}$, $u\in
T_{j}\\}\subseteq\mathcal{K}$ and the ordered partition corresponds to some
$\vec{T}\in\mathit{Ords}$ as required.

  * •

Every $\mathcal{K}\in\mathfrak{K}$ contains a complete
$\mathcal{D}$-completion $\mathcal{F}_{\mathcal{D}}$ and does not contain any
other atom on predicates from
$\\{\mathtt{In}_{\mathtt{p}},\mathtt{NIn}_{\mathtt{p}}\mid\mathtt{p}\in\mathcal{S}\\}$:

    * –

$\mathcal{K}$ includes
$\\{\mathtt{In}_{\mathtt{p}}(\vec{t})\mid\mathtt{p}(\vec{t})\in\mathcal{D}\\}$
because it satisfies (4).

    * –

For every $\mathtt{p}\in\mathcal{S}$ and tuple $\vec{t}\subseteq\Delta$ of
matching arity, $\mathcal{K}$ contains at least one of
$\\{\mathtt{In}_{\mathtt{p}}(\vec{t}),\mathtt{NIn}_{\mathtt{p}}(\vec{t})\\}$
because it satisfies (14). We show that it does not contain both. The rules of
the form (14) have the lowest priority and applying such a rule can only
trigger the application of some rules of the form (8), which themselves cannot
trigger the application of any rules but (8). Hence, (i) the application of
these rules in the chase tree happens after the construction of the
$\mathcal{D}$-order in $\mathcal{K}$, and (ii) when a rule of the form (14) is
applied and adds some $\mathtt{In}_{\mathtt{p}}(\vec{t})$ (resp.
$\mathtt{NIn}_{\mathtt{p}}(\vec{t})$), the exhaustive application of rules (8)
adds all $\mathtt{In}_{\mathtt{p}}(\vec{t}^{\prime})$ (resp.
$\mathtt{NIn}_{\mathtt{p}}(\vec{t}^{\prime})$) such that
$\vec{t}^{\prime}\sim\vec{t}$, where $\vec{t}^{\prime}\sim\vec{t}$ iff
$t_{i}\sim t^{\prime}_{i}$ for every $i$. Suppose for a contradiction that
there exists $\vec{u}$ such that
$\mathtt{In}_{\mathtt{p}}(\vec{u})\in\mathcal{K}$ and
$\mathtt{NIn}_{\mathtt{p}}(\vec{u})\in\mathcal{K}$. Since the rules (14) and
(8) are the only ones that have predicates from
$\\{\mathtt{In}_{\mathtt{p}},\mathtt{NIn}_{\mathtt{p}}\mid\mathtt{p}\in\mathcal{S}\\}$
in the head, it follows that there exist
$\mathtt{In}_{\mathtt{p}}(\vec{u}_{1})\in\mathcal{K}$ and
$\mathtt{NIn}_{\mathtt{p}}(\vec{u}_{2})\in\mathcal{K}$ that have both been
added by some application of (14) and are such that $\vec{u}_{1}\sim\vec{u}$
and $\vec{u}_{2}\sim\vec{u}$. Assume that
$\mathtt{In}_{\mathtt{p}}(\vec{u}_{1})$ was added first. Then by (ii)
$\mathtt{In}_{\mathtt{p}}(\vec{u}_{2})$ has been added before any new
application of (14), and the rule
$\bigwedge_{x\in\vec{x}}\mathtt{DbDom}(x)\to\mathtt{In}_{\mathtt{p}}(\vec{x})\vee\mathtt{NIn}_{\mathtt{p}}(\vec{x})$
with the substitution that maps $\vec{x}$ to $\vec{u}_{2}$ was already
satisfied, contradicting the introduction of
$\mathtt{NIn}_{\mathtt{p}}(\vec{u}_{2})$.

  * •

For every $(\vec{T},\mathcal{F}_{\mathcal{D}})$, there exists
$\mathcal{K}\in\mathfrak{K}$ that corresponds to
$(\vec{T},\mathcal{F}_{\mathcal{D}})$. The existence of $\mathcal{K}$ is
witnessed by the path of the chase tree such that for every vertex labelled
with $\mathcal{E}$ where a disjunctive rule (9), (13), or (14) is applied, the
path chooses the child labelled with
$\mathcal{C}_{i}=\mathcal{E}\cup\sigma_{i}(\eta_{i})$ where
$\sigma_{i}(\eta_{i})$ is included in $\mathcal{F}_{\mathcal{D}}$ or in the
$\mathcal{D}$-order corresponding to $\vec{T}$.

Hence, we can define a one-to-one correspondence between interpretations in
$\mathfrak{K}$ and interpretations in $\mathfrak{I}_{1}$ using the
corresponding pairs of the form $(\vec{T},\mathcal{F}_{\mathcal{D}})$. By
construction, every $\mathcal{K}\in\mathfrak{K}$ and
$\mathcal{I}\in\mathfrak{I}_{1}$ that are in correspondence are isomorphic
(note that since we choose to name the two fresh nulls $u_{\alpha}$ and
$u_{\omega}$, they are actually identical). ∎

######  Lemma 27.

Given some $\mathcal{I}\in\mathfrak{I}_{1}$, $\mathit{Int}_{2}(\mathcal{I})$
is isomorphic to the unique interpretation in a result of the chase over
$\mathcal{R}_{2}$ and $\mathcal{I}$.

###### Proof.

We will let $\mathit{Order}(\mathcal{F})=T_{1},\ldots,T_{k}$. The
interpretation $\mathit{Int}_{2}(\mathcal{I})$ is equal to:

$\displaystyle\mathcal{I}\cup\\{\mathtt{Root}(u_{1})\\}\cup\\{\mathtt{Chi}(u_{w},u_{wz})\mid
wz\in\mathbf{Z},2\leq z\leq k\\}\cup{}$
$\displaystyle\\{\mathtt{Leaf}(u_{w})\mid
w\in\mathbf{Z};\mathit{end}(w)=k\\}\cup\\{\mathtt{Rep}(x,u_{w})\mid
w\in\mathbf{Z};x\in T_{\mathit{end}(w)}\\}\cup{}$
$\displaystyle\\{\mathtt{In}_{\mathtt{p}}^{\prime}(u_{w_{1}},\dots,u_{w_{\mathit{Ar}(\mathtt{p})}})\mid\mathtt{In}_{\mathtt{p}}(t_{1},\dots,t_{\mathit{Ar}(\mathtt{p})})\in\mathcal{I};w_{i}\in\mathbf{Z};t_{i}\in
T_{\mathit{end}(w_{i})};1\leq i\leq\mathit{Ar}(\mathtt{p})\\}\cup{}$
$\displaystyle\\{\mathtt{NIn}_{\mathtt{p}}^{\prime}(u_{w_{1}},\dots,u_{w_{\mathit{Ar}(\mathtt{p})}})\mid\mathtt{NIn}_{\mathtt{p}}(t_{1},\dots,t_{\mathit{Ar}(\mathtt{p})})\in\mathcal{I};w_{i}\in\mathbf{Z};t_{i}\in
T_{\mathit{end}(w_{i})};1\leq i\leq\mathit{Ar}(\mathtt{p})\\}.$

We describe a chase over $\mathcal{R}_{2}$ and $\mathcal{I}$ that prioritises
rule (18) step by step (note that if we do not prioritise (18), we could get a
result which is not isomorphic to $\mathit{Int}_{2}(\mathcal{I})$). Instead of
constructing an isomorphism by giving for each fresh null introduced during
the chase its counterpart in $\mathit{Int}_{2}(\mathcal{I})$, we directly set
the the names of the fresh nulls so that the chase result coincides with
$\mathit{Int}_{2}(\mathcal{I})$. Note that no rule in Figure 1 is applicable
to $\mathcal{I}$ and that applying a rule in Figure 2 cannot make a rule in
Figure 1 applicable.

  * •

Apply $\langle\rho,\sigma\rangle$ with $\rho=\eqref{rul_RootCreation}$ and
$\sigma$ the substitution that maps $x$ to some $t\in T_{1}$ (recall that
$\\{\mathtt{First}(t)\mid t\in T_{1}\\}\subseteq\mathcal{I}$). This introduces
a fresh null that we call $u_{1}$, and adds $\mathtt{Root}(u_{1})$ and
$\mathtt{Rep}(t,u_{1})$.

  * •

Apply exhaustively (18): add $\mathtt{Rep}(t,u_{1})$ for all $t\in T_{1}$.

  * •

For $2\leq i\leq k$:

    * –

Choose one $t_{1}\in T_{1}$ and one $t_{i}\in T_{i}$ and apply
$\langle\rho,\sigma\rangle$ with $\rho=\eqref{rul_NextTreeRep}$ and $\sigma$
the substitution that maps $x$ to $t_{1}$, $v$ to $u_{1}$, and $z$ to $t_{i}$
(recall that the atoms on predicate $\mathtt{LT}$ in $\mathcal{I}$ are
$\\{\mathtt{LT}(t,u)\mid 1\leq j<j^{\prime}\leq k$, $t\in T_{j}$, $u\in
T_{j}^{\prime}\\}$). This introduces a fresh null that we call $u_{1\,i}$ and
adds $\mathtt{Chi}(u_{1},u_{1\,i})$, $\mathtt{Rep}(t_{i},u_{1\,i})$ (note that
this is the first fact of the form $\mathtt{Rep}(t_{i},x)$ with $t_{i}\in
T_{i}$ that we introduce).

    * –

Apply exhaustively (18): add $\mathtt{Rep}(t,u_{1\,i})$ for all $t\in T_{i}$.

  * •

Continue applying (16) and (18) exhaustively as done in the previous step,
introducing all nulls of the form $u_{w}$ with $w\in\mathbf{Z}$, and adding
facts $\\{\mathtt{Chi}(u_{w},u_{wz})\mid wz\in\mathbf{Z},2\leq z\leq k\\}$ and
$\\{\mathtt{Rep}(x,u_{w})\mid w\in\mathbf{Z};x\in T_{\mathit{end}(w)}\\}$.

  * •

Apply exhaustively (17) and add $\\{\mathtt{Leaf}(u_{w})\mid
w\in\mathbf{Z};\mathit{end}(w)=k\\}$ (recall that $\\{\mathtt{Last}(t)\mid
t\in T_{k}\\}\subseteq\mathcal{I}$).

  * •

Apply exhaustively (19): for all
$\mathtt{In}_{\mathtt{p}}(t_{1},\dots,t_{\mathit{Ar}(\mathtt{p})})\in\mathcal{I}$,
add all
$\mathtt{In}_{\mathtt{p}}^{\prime}(u_{w_{1}},\dots,u_{w_{\mathit{Ar}(\mathtt{p})}})$
where $t_{i}\in T_{\mathit{end}(w_{i})}$.

  * •

Apply exhaustively (20): for all
$\mathtt{NIn}_{\mathtt{p}}(t_{1},\dots,t_{\mathit{Ar}(\mathtt{p})})\in\mathcal{I}$,
add all
$\mathtt{NIn}_{\mathtt{p}}^{\prime}(u_{w_{1}},\dots,u_{w_{\mathit{Ar}(\mathtt{p})}})$
where $t_{i}\in T_{\mathit{end}(w_{i})}$. ∎

Lemma 6.
$\mathfrak{I}_{2}=\\{\mathit{Int}_{2}(\mathcal{I})\mid\mathcal{I}\in\mathfrak{I}_{1}\\}$
is a universal model set of $\mathcal{R}_{2}$ and $\mathcal{D}$.

###### Proof.

By Lemmas 5 and 27, $\mathfrak{I}_{2}$ only contains models of
$\mathcal{R}_{2}$ and $\mathcal{D}$. We show that for every model
$\mathcal{M}$ of $\mathcal{R}_{2}$ and $\mathcal{D}$, there exists
$\mathcal{I}_{2}\in\mathfrak{I}_{2}$ and a homomorphism
$\textit{h}_{2}:\mathcal{I}_{2}\to\mathcal{M}$.

  1. 1.

Let $\mathcal{M}$ be a model of $\mathcal{R}_{2}$ and $\mathcal{D}$.

  2. 2.

By Lemma 5: since $\mathcal{M}$ is a model of
$\mathcal{R}_{2}\supseteq\mathcal{R}_{1}$ and $\mathcal{D}$, there exist
$\mathcal{I}_{1}\in\mathfrak{I}_{1}$ and a homomorphism
$\textit{h}_{1}:\mathcal{I}_{1}\to\mathcal{M}$.

  3. 3.

By Lemma 27: since $\mathcal{I}_{1}\in\mathfrak{I}_{1}$, there exists a chase
over $\mathcal{R}_{2}$ and $\mathcal{I}_{1}$ such that the unique
interpretation $\mathcal{J}$ in its result is such that there exists an
isomorphism $\textit{g}_{2}:\mathit{Int}_{2}(\mathcal{I}_{1})\to\mathcal{J}$.

  4. 4.

By definition of $\mathcal{J}$, and since no rule from $\mathcal{R}_{1}$ is
applied in the chase of over $\mathcal{R}_{2}$ and $\mathcal{I}_{1}$ (see
proof of Lemma 27) and $\mathcal{R}_{2}\setminus\mathcal{R}_{1}$ contains no
disjunctive rules, it follows that $\mathcal{J}$ is a universal model of
$\mathcal{R}_{2}\setminus\mathcal{R}_{1}$ and $\mathcal{I}_{1}$.

  5. 5.

By (1), (2) and (4), there exists a homomorphism
$\textit{g}_{1}:\mathcal{J}\to\mathcal{M}$ that extends $\textit{h}_{1}$.

  6. 6.

Let $\mathcal{I}_{2}=\mathit{Int}_{2}(\mathcal{I}_{1})\in\mathfrak{I}_{2}$. By
(3) and (5), there is an homomorphism
$\textit{h}_{2}=\textit{g}_{2}\circ\textit{g}_{1}:\mathcal{I}_{2}\to\mathcal{M}$.
∎

In the next proofs, we will use the following notation. Given a chase tree
node labelled $\mathcal{C}_{i}=\mathcal{E}\cup\sigma_{i}(\eta_{i})$ and
obtained by applying some $\langle\rho,\sigma\rangle$ to its parent node
labelled by $\mathcal{E}$, then for each variable $y$ of $\rho$ not in the
domain of $\sigma$, we denote by $u_{\sigma,\rho,y}$ the fresh null such that
$\sigma_{i}(y)=u_{\sigma,\rho,y}$ where $\sigma_{i}$ is as introduced in
Definition 2.

######  Lemma 28.

Given some $\mathcal{I}\in\mathfrak{I}_{2}$, $\mathit{Int}_{3}(\mathcal{I})$
is well-defined and $\mathit{Int}_{3}(\mathcal{I})$ is isomorphic to the
unique interpretation in a result of the chase over $\mathcal{R}_{3}$ and
$\mathcal{I}$.

###### Proof.

We will let $\mathit{Order}(\mathcal{I})=T_{1},\ldots,T_{k}$. The
interpretation $\mathit{Int}_{3}(\mathcal{I})$ is equal to the union of the
following databases:

  1. 1.

$\mathcal{I}$.

  2. 2.

For each $w\in\mathbf{Z}$ of length $|w|$, with $b_{1}\cdots b_{\ell}$ the
binary representation of $|w|+1$, the database $\mathit{EncPos}(w)$:

$\\{\mathtt{Enc}(u_{w},e_{w}^{1},e_{w}^{\ell})\\}\cup\\{\mathtt{S}_{b_{i}}(e_{w}^{i})\mid
1\leq i\leq\ell\\}\cup{}\\{\mathtt{Nxt}(e_{w}^{i-1},e_{w}^{i})\mid 2\leq
i\leq\ell\\}.$

  3. 3.

For each $w\in\mathbf{Z}$ of length $|w|<k$, and $z\in\\{1,\dots,k\\}$ such
that $wz\in\mathbf{Z}$, with $b_{1}\cdots b_{\ell}$ the binary representation
of $|w|+2$ and $b^{\prime}_{1}\cdots b^{\prime}_{\ell^{\prime}}$ the binary
representation of $|w|+1$, the database $\mathit{CpyPlusOne}(w,wz)$ defined as
follows:

$\displaystyle\\{\mathtt{Cpy}_{\\!+1}(e^{i}_{w},e^{\ell^{\prime}}_{w},e^{j}_{wz},e^{\ell}_{wz})\mid$
$\displaystyle\qquad\qquad\text{ the number represented by }b_{j}\cdots
b_{\ell}\text{ is equal to the number represented by }b^{\prime}_{i}\cdots
b^{\prime}_{\ell^{\prime}}\text{ plus one}\\}$
$\displaystyle\cup\\{\mathtt{Cpy}(e^{i}_{w},e^{\ell^{\prime}}_{w},e^{i}_{wz},e^{\ell}_{wz})\mid
b_{i}\cdots b_{\ell}=b^{\prime}_{i}\cdots b^{\prime}_{\ell^{\prime}}\\}.$

We describe a (Datalog-first) chase over $\mathcal{R}_{3}$ and $\mathcal{I}$
step by step. We directly set the the names of the fresh nulls so that the
chase result coincides with $\mathit{Int}_{3}(\mathcal{I})$. Note that no rule
in Figures 1 or 2 is applicable to $\mathcal{I}$ and that applying a rule in
Figure 3 cannot make a rule in Figures 1 or 2 applicable.

  * •

Apply $\langle\rho,\sigma\rangle$ with $\rho=\eqref{rul_encRoot}$ and
$\sigma(u)=u_{1}$. This introduces two fresh nulls,
$u_{\sigma,\rho,y_{1}}=e_{1}^{1}$ and $u_{\sigma,\rho,y_{2}}=e_{1}^{2}$ and
adds $\mathtt{Enc}(u_{1},e_{1}^{1},e_{1}^{2})$, $\mathtt{S}_{0}(e_{1}^{1})$,
$\mathtt{Nxt}(e_{1}^{1},e_{1}^{2})$ and $\mathtt{S}_{1}(e_{1}^{2})$.

We show by induction on $p$ that for every $w\in\mathbf{Z}$ of length $|w|=p$
and $z\in\\{1,\dots,k\\}$ such that $wz\in\mathbf{Z}$, our chase sequence adds
$\mathit{EncPos}(wz)$, and $\mathit{CpyPlusOne}(w,wz)$.

_Case $p=1$._ In this case, $w=1$ and $z\in\\{2,\dots,k\\}$.

  * •

For $2\leq i\leq k$:

    * –

Apply $\langle\rho,\sigma\rangle$ with $\rho=\eqref{rul_encChild}$ and
$\sigma(u)=u_{1}$, $\sigma(y_{1})=e_{1}^{1}$, $\sigma(y_{\\_})=e_{1}^{2}$,
$\sigma(v)=u_{1\,i}$. This introduces two fresh nulls,
$u_{\sigma,\rho,z_{1}}=e_{1\,i}^{1}$ and
$u_{\sigma,\rho,z_{\\_}}=e_{1\,i}^{2}$ and adds
$\mathtt{Enc}(u_{1\,i},e_{1\,i}^{1},e_{1\,i}^{2})$ and
$\mathtt{Cpy}_{\\!+1}(e_{1}^{1},e_{1}^{2},e_{1\,i}^{1},e_{1\,i}^{2})$.

    * –

Apply (23): add $\mathtt{S}_{1}(e_{1\,i}^{1})$,
$\mathtt{Nxt}(e_{1\,i}^{1},e_{1\,i}^{2})$, $\mathtt{S}_{1}(e_{1\,i}^{2})$.

_Induction step:_ Assume that our chase sequence already added all required
facts for every $w^{\prime}\in\mathbf{Z}$ of length $|w^{\prime}|<p$, and
$z^{\prime}\in\\{1,\dots,k\\}$ such that $w^{\prime}z^{\prime}\in\mathbf{Z}$,
and consider $w\in\mathbf{Z}$ of length $|w|=p$, and $z\in\\{1,\dots,k\\}$
such that $wz\in\mathbf{Z}$. Let $b_{1}\cdots b_{\ell}$ the binary
representation of $p+2$ and $b^{\prime}_{1}\cdots b^{\prime}_{\ell^{\prime}}$
the binary representation of $p+1$.

  * •

By induction hypothesis, $\mathtt{Enc}(u_{w},e_{w}^{1},e_{w}^{\ell^{\prime}})$
was added by the chase sequence. Apply $\langle\rho,\sigma\rangle$ with
$\rho=\eqref{rul_encChild}$ and $\sigma(u)=u_{w}$, $\sigma(y_{1})=e_{w}^{1}$,
$\sigma(y_{\\_})=e_{w}^{\ell^{\prime}}$, $\sigma(v)=u_{wz}$. This introduces
two fresh nulls, $u_{\sigma,\rho,z_{1}}=e_{wz}^{1}$ and
$u_{\sigma,\rho,z_{\\_}}=e_{wz}^{\ell}$ and adds
$\mathtt{Enc}(u_{wz},e_{wz}^{1},e_{wz}^{\ell})$ and
$\mathtt{Cpy}_{\\!+1}(e_{w}^{1},e_{w}^{\ell^{\prime}},e_{wz}^{1},e_{wz}^{\ell})$.

  * •

By induction hypothesis, the chase sequence added
$\mathtt{S}_{b^{\prime}_{i}}(e_{w}^{i})$, $1\leq i\leq\ell^{\prime}$, and
$\mathtt{Nxt}(e_{w}^{i-1},e_{w}^{i})$, $2\leq i\leq\ell^{\prime}$. We
distinguish two cases, depending on the value of $b^{\prime}_{1}$.

(1) In the case where $b^{\prime}_{1}=0$, we have $\ell=\ell^{\prime}$ and
$b_{1}\cdots b_{\ell}=1b^{\prime}_{2}\cdots b^{\prime}_{\ell}$. Moreover, note
that $\ell>2$ (otherwise $b^{\prime}_{1}b^{\prime}_{2}=01$ and $p+1=2$).

    * –

Apply $\langle\rho,\sigma\rangle$ with $\rho=\eqref{rul_CpyPlusOneCell0Next}$
and $\sigma(y_{1})=e_{w}^{1}$, $\sigma(y_{\\_})=e_{w}^{\ell}$,
$\sigma(y_{2})=e_{w}^{2}$, $\sigma(y_{3})=e_{w}^{3}$,
$\sigma(z_{1})=e_{wz}^{1}$, $\sigma(z_{\\_})=e_{wz}^{\ell}$. This introduces a
fresh null, $u_{\sigma,\rho,z_{2}}=e_{wz}^{2}$, and adds the atoms
$\mathtt{Cpy}(e_{w}^{2},e_{w}^{\ell},e_{wz}^{2},e_{wz}^{\ell})$,
$\mathtt{S}_{1}(e_{wz}^{1})$, and $\mathtt{Nxt}(e_{wz}^{1},e_{wz}^{2})$.

    * –

While
$\mathtt{Cpy}(e_{w}^{\ell-1},e_{w}^{\ell},e_{wz}^{\ell-1},e_{wz}^{\ell})$ has
not been introduced, apply (28), introducing fresh nulls $e_{wz}^{i}$ for
$2<i<\ell$ and adding atoms
$\mathtt{Cpy}(e_{w}^{i},e_{w}^{\ell},e_{wz}^{i},e_{wz}^{\ell})$,
$\mathtt{S}_{b_{i-1}}(e_{wz}^{i-1})$, and
$\mathtt{Nxt}(e_{wz}^{i-1},e_{wz}^{i})$.

    * –

Apply (27) and add $\mathtt{S}_{b_{\ell-1}}(e_{wz}^{\ell-1})$,
$\mathtt{Nxt}(e_{wz}^{\ell-1},e_{wz}^{\ell})$,
$\mathtt{S}_{1}(e_{wz}^{\ell})$.

(2) In the case where $b^{\prime}_{1}=1$, we have $b_{1}=0$ and the number
represented by $b_{2}\cdots b_{\ell}$ is equal to the number represented by
$b^{\prime}_{2}\cdots b^{\prime}_{\ell^{\prime}}$ plus one.

    * –

While no atom of the form
$\mathtt{Cpy}(e_{w}^{j},e_{w}^{\ell^{\prime}},e_{wz}^{j},e_{wz}^{\ell})$ or
$\mathtt{Cpy}_{\\!+1}(e_{w}^{\ell^{\prime}-1},e_{w}^{\ell^{\prime}},e_{wz}^{\ell^{\prime}-1},e_{wz}^{\ell})$
have been introduced, and for $i$ starting from $2$ and growing by one at each
cycle, apply the applicable $\langle\rho,\sigma\rangle$ among:

      * *

$\rho=\eqref{rul_CpyPlusOneCell0Next}$ and $\sigma(y_{1})=e_{w}^{i-1}$,
$\sigma(y_{\\_})=e_{w}^{\ell^{\prime}}$, $\sigma(y_{2})=e_{w}^{i}$,
$\sigma(y_{3})=e_{w}^{i+1}$, $\sigma(z_{1})=e_{wz}^{i-1}$,
$\sigma(z_{\\_})=e_{wz}^{\ell}$. This introduces a fresh null,
$u_{\sigma,\rho,z_{2}}=e_{wz}^{i}$, and adds the atoms
$\mathtt{Cpy}(e_{w}^{i},e_{w}^{\ell^{\prime}},e_{wz}^{i},e_{wz}^{\ell})$,
$\mathtt{S}_{1}(e_{wz}^{i-1})=\mathtt{S}_{b_{i-1}}(e_{wz}^{i-1})$, and
$\mathtt{Nxt}(e_{wz}^{i-1},e_{wz}^{i})$.

      * *

$\rho=\eqref{rul_CpyPlusOneCell1Next}$ and $\sigma$ as above. This introduces
a fresh null, $u_{\sigma,\rho,z_{2}}=e_{wz}^{i}$, and adds the atoms
$\mathtt{Cpy}_{\\!+1}(e_{w}^{i},e_{w}^{\ell^{\prime}},e_{wz}^{i},e_{wz}^{\ell})$,
$\mathtt{S}_{0}(e_{wz}^{i-1})=\mathtt{S}_{b_{i-1}}(e_{wz}^{i-1})$, and
$\mathtt{Nxt}(e_{wz}^{i-1},e_{wz}^{i})$.

    * –

If an atom of the form
$\mathtt{Cpy}(e_{w}^{j},e_{w}^{\ell^{\prime}},e_{wz}^{j},e_{wz}^{\ell})$ is
introduced at some point (i.e. the applicable $\langle\rho,\sigma\rangle$ in
the previous step is such that $\rho=\eqref{rul_CpyPlusOneCell0Next}$), we use
a sequence of chase steps similar to the case $b^{\prime}_{1}=0$, and obtain
the required atoms.

    * –

Otherwise,
$\mathtt{Cpy}_{\\!+1}(e_{w}^{\ell^{\prime}-1},e_{w}^{\ell^{\prime}},e_{wz}^{\ell^{\prime}-1},e_{wz}^{\ell})$
is introduced at the end of the loop. Apply the applicable
$\langle\rho,\sigma\rangle$ among:

      * *

$\rho=\eqref{rul_CpyPlusOneCell0}$ and
$\sigma(y_{1})=e_{w}^{\ell^{\prime}-1}$,
$\sigma(y_{2})=e_{w}^{\ell^{\prime}}$,
$\sigma(z_{1})=e_{wz}^{\ell^{\prime}-1}$, $\sigma(z_{\\_})=e_{wz}^{\ell}$ with
$\ell^{\prime}=\ell$. This adds $\mathtt{S}_{1}(e_{wz}^{\ell-1})$,
$\mathtt{Nxt}(e_{wz}^{\ell-1},e_{wz}^{\ell})$, and
$\mathtt{S}_{1}(e_{wz}^{\ell})$.

      * *

$\rho=\eqref{rul_CpyPlusOneCell1}$ and $\sigma$ is as above but
$\ell=\ell^{\prime}+1$ so that
$\sigma(z_{1})=e_{wz}^{\ell^{\prime}-1}=e_{wz}^{\ell-2}$. This introduces a
new null $u_{\sigma,\rho,z_{2}}=e_{wz}^{\ell-1}$ and adds
$\mathtt{S}_{0}(e_{wz}^{\ell-2})$,
$\mathtt{Nxt}(e_{wz}^{\ell-2},e_{wz}^{\ell-1})$,
$\mathtt{S}_{0}(e_{wz}^{\ell-1})$,
$\mathtt{Nxt}(e_{wz}^{\ell-1},e_{wz}^{\ell})$ and
$\mathtt{S}_{1}(e_{wz}^{\ell})$.∎

Lemma 7.
$\mathfrak{I}_{3}=\\{\mathit{Int}_{3}(\mathcal{I})\mid\mathcal{I}\in\mathfrak{I}_{2}\\}$
is a universal model set of $\mathcal{R}_{3}$ and $\mathcal{D}$.

###### Proof.

Similar to the proof of Lemma 6, using Lemmas 6 and 28. ∎

######  Lemma 29.

Given some $\mathcal{I}\in\mathfrak{I}_{3}$, $\mathit{Int}_{4}(\mathcal{I})$
is well-defined and $\mathit{Int}_{4}(\mathcal{I})$ is isomorphic to the
unique interpretation in a result of the chase over $\mathcal{R}_{4}$ and
$\mathcal{I}$.

###### Proof.

Before giving the extension of $\mathit{Int}_{4}(\mathcal{I})$, we introduce
some notation. Consider some fact of the form
$\mathtt{Leaf}(u_{w})\in\mathcal{I}$ and let
$S=\mathit{branchTape}(\mathcal{I},u_{w})$. By construction, $S=e_{1}\cdots
e_{|\mathit{branchDb}(\mathcal{I},u_{w})|}$ where each $e_{i}$ corresponds to
the serialisation of some
$\mathtt{p}^{x}_{g}(u_{w_{1}},\dots,u_{w_{x}})\in\mathit{branchDb}(\mathcal{I},u_{w})$
and is of the form $\mathtt{p}^{x}_{g}\mathord{\parallel}b^{1}_{1}\cdots
b^{1}_{\ell_{1}}\mathord{\parallel}\cdots\mathord{\parallel}b^{x}_{1}\cdots
b^{x}_{\ell_{x}}\mathord{\parallel}$ where $b^{i}_{1}\cdots b^{i}_{\ell_{i}}$
is the binary representation of $|w_{i}|+1$. For every
$\mathtt{p}^{x}_{g}\in\mathcal{S}$ and
$u_{w_{1}},\dots,u_{w_{x}}\subseteq\mathit{branch}(u_{w})$, let
$j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})$ and
$j^{e}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})-1$ be the indexes
where the serialisation of $\mathtt{p}^{x}_{g}(u_{w_{1}},\dots,u_{w_{x}})$
starts and ends respectively if
$\mathtt{p}^{x}_{g}(u_{w_{1}},\dots,u_{w_{x}})\in\mathit{branchDb}(\mathcal{I},u_{w})$,
and otherwise
$j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})=j^{e}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})$
be the index where starts the serialisation of the first fact of
$\mathit{branchDb}(\mathcal{I},u_{w})$ that follows
$\mathtt{p}^{x}_{g}(u_{w_{1}},\dots,u_{w_{x}})$ according to $\prec$ (and
$|S|+1$ if there is no such fact). (Recall that $\prec$ is defined before
Lemma 8.) It is easy to verify that:

  * •

$j^{s}_{S}(\mathtt{p}^{1}_{1},u_{w})=1$.

  * •

If
$\mathtt{In}_{\mathtt{p}^{x}_{g}}^{\prime}(u_{w_{1}},\dots,u_{w_{x}})\notin\mathcal{I}$,
then
$j^{e}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})=j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})$.

  * •

If
$\mathtt{In}_{\mathtt{p}^{x}_{g}}^{\prime}(u_{w_{1}},\dots,u_{w_{x}})\in\mathcal{I}$,
then
$j^{e}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})=j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})+\Sigma_{i=1}^{x}\ell_{i}+x+2$,
where $\ell_{i}$ is the length of the binary encoding of $|w_{i}|+1$.

  * •

If $g<{\bar{n}}$, then
$j^{e}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})=j^{s}_{S}(\mathtt{p}^{x}_{g+1},u_{w_{1}},\dots,u_{w_{x}})$.

  * •

If $u_{w_{1}},\dots,u_{w_{x}}\neq u_{1},\dots,u_{1}$, then
$j^{e}_{S}(\mathtt{p}^{x}_{{\bar{n}}},u_{w_{1}},\dots,u_{w_{x}})=j^{s}_{S}(\mathtt{p}^{x}_{1},u_{w_{1}^{\prime}},\dots,u_{w_{x}^{\prime}})$,
where $u_{w^{\prime}_{1}},\dots,u_{w_{x}^{\prime}}$ comes right after
$u_{w_{1}},\dots,u_{w_{x}}$ in the lexicographic order according to $\prec$.

  * •

If $x<{\bar{m}}$, then
$j^{e}_{S}(\mathtt{p}^{x}_{{\bar{n}}},u_{1},\dots,u_{1})=j^{s}_{S}(\mathtt{p}^{x+1}_{1},u_{w},\dots,u_{w})$.

Note that $j^{e}_{S}(\mathtt{p}^{\bar{m}}_{\bar{n}},u_{1},\dots,u_{1})=|S|+1$
and that for every
$\mathtt{p}^{x}_{g}(u_{w_{1}},\dots,u_{w_{x}})\in\mathit{branchDb}(\mathcal{I},u_{w})$,
if $b^{i}_{1}\cdots b^{i}_{\ell_{i}}$ is the binary encoding of $|w_{i}|+1$
($1\leq i\leq x$), then :

  * •

$S[j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})]=\mathtt{p}^{x}_{g}$,

  * •

$S[j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})+1]=\mathord{\parallel}$,

  * •

and for $1\leq i\leq x$:

    * –

$S[j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})+i+\Sigma_{j=1}^{i-1}\ell_{j}+1]=b^{i}_{1}$,

    * –

$\dots$,

    * –

$S[j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})+i+\Sigma_{j=1}^{i-1}\ell_{j}+\ell_{i}]=b^{i}_{\ell_{i}}$,

    * –

$S[j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})+i+\Sigma_{j=1}^{i}\ell_{j}+1]=\mathord{\parallel}$.

Finally, let $J_{S}(u_{w^{\prime}})$ be the set of indexes of $S$ where starts
the sequence $\mathord{\parallel}b^{\prime}_{1}\cdots
b^{\prime}_{\ell^{\prime}}\mathord{\parallel}$ where $b^{\prime}_{1}\cdots
b^{\prime}_{\ell^{\prime}}$ is the binary representation of $|w^{\prime}|+1$.
The interpretation $\mathit{Int}_{4}(\mathcal{I})$ is equal to the union of
the following databases:

  1. 1.

$\mathcal{I}$;

  2. 2.

For every $\mathtt{Leaf}(u_{w})\in\mathcal{I}$ with serialisation
$S=\mathit{branchTape}(\mathcal{I},u_{w})$, the database
$\mathit{startConf}(\mathcal{I},u_{w})$:

$\displaystyle\\{\mathtt{Ld}_{1}(u_{w},t_{w}^{1},u_{w}),\mathtt{Hd}_{q_{S}}(t^{1}_{w}),\mathtt{End}(t_{w}^{|S|+1}),\mathtt{S}_{\text{\textvisiblespace}}(t_{w}^{|S|+1})\\}\cup{}$
$\displaystyle\\{\mathtt{Nxt}(t_{w}^{j-1},t_{w}^{j})\mid 2\leq
j\leq|S|+1\\}\cup\\{\mathtt{S}_{a}(t_{w}^{j})\mid 1\leq j\leq|S|,a=S[j]\\}.$

  3. 3.

For every $\mathtt{Leaf}(u_{w})\in\mathcal{I}$ with serialisation
$S=\mathit{branchTape}(\mathcal{I},u_{w})$, the database
$\mathit{loadS}(\mathcal{I},u_{w})$ defined as follows:

$\displaystyle\\{\mathtt{Ld}_{x}(u_{w},t^{j}_{w},u_{w_{1}},\dots,u_{w_{x}})\mid$
$\displaystyle 1\leq
x\leq{\bar{m}};u_{w_{i}}\in\mathit{branch}(u_{w});j=j^{s}_{S}(\mathtt{p}^{x}_{1},u_{w_{1}},\dots,u_{w_{x}})\\}$
$\displaystyle\cup\\{\mathtt{Rdy}_{x}(u_{w},t^{j}_{w},u_{w_{1}},\dots,u_{w_{x}})\mid$
$\displaystyle 1\leq
x\leq{\bar{m}};u_{w_{i}}\in\mathit{branch}(u_{w});j=j^{e}_{S}(\mathtt{p}^{x}_{\bar{n}},u_{w_{1}},\dots,u_{w_{x}})\\}$
$\displaystyle\cup\\{\mathtt{Ld}_{\mathtt{p}^{x}_{g}}(u_{w},t^{j}_{w},u_{w_{1}},\dots,u_{w_{x}})\mid$
$\displaystyle 1\leq g\leq{\bar{n}};1\leq
x\leq{\bar{m}};u_{w_{i}}\in\mathit{branch}(u_{w});j=j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})\\}$
$\displaystyle\cup\\{\mathtt{Rdy}_{\mathtt{p}^{x}_{g}}(u_{w},t^{j}_{w},u_{w_{1}},\dots,u_{w_{x}})\mid$
$\displaystyle 1\leq g\leq{\bar{n}};1\leq
x\leq{\bar{m}};u_{w_{i}}\in\mathit{branch}(u_{w});j=j^{e}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})\\}$
$\displaystyle\cup\\{\mathtt{LdE}(u_{w^{\prime}},t^{j+1}_{w},t^{j+\ell^{\prime}+2}_{w})\mid$
$\displaystyle u_{w^{\prime}}\in\mathit{branch}(u_{w});b_{1}^{\prime}\cdots
b_{\ell^{\prime}}^{\prime}\text{ bin. rep. of }|w^{\prime}|+1;j\in
J_{S}(u_{w^{\prime}})\\}$
$\displaystyle\cup\\{\mathtt{Cpy}(e_{w^{\prime}}^{r},e_{w^{\prime}}^{\ell^{\prime}},t^{j+r+1}_{w},t^{j+\ell^{\prime}+1}_{w})\mid$
$\displaystyle u_{w^{\prime}}\in\mathit{branch}(u_{w});b_{1}^{\prime}\cdots
b_{\ell^{\prime}}^{\prime}\text{ bin. rep. of }|w^{\prime}|+1;$
$\displaystyle\qquad 1\leq r\leq\ell^{\prime}-1;j-1\in
J_{S}(u_{w^{\prime}})\\}$

We describe a (Datalog-first) chase over $\mathcal{R}_{4}$ and $\mathcal{I}$
step by step. We directly set the the names of the fresh nulls so that the
chase result coincides with $\mathit{Int}_{4}(\mathcal{I})$. Note that no rule
in Figures 1, 2, or 3 is applicable to $\mathcal{I}$ but that applying rule
(30) may trigger the application of the “copy” rules (27) and (28) in Figure3.

For every $\mathtt{Leaf}(u_{w})\in\mathcal{I}$ with serialisation
$S=\mathit{branchTape}(\mathcal{I},u_{w})$:

  * •

Apply $\langle\rho,\sigma\rangle$ with $\rho=\eqref{rul_startTape}$ and
$\sigma$ that maps $u$ to $u_{w}$. This introduces a fresh null that we call
$t^{1}_{w}$ and adds atoms $\mathtt{Ld}_{1}(u_{w},t^{1}_{w},u_{w})$ and
$\mathtt{Hd}_{q_{S}}(t^{1}_{w})$. Note that
$j^{s}_{S}(\mathtt{p}^{1}_{1},u_{w})=1$ so that we have indeed added
$\mathtt{Ld}_{1}(u_{w},t^{j^{s}_{S}(\mathtt{p}^{1}_{1},u_{w})}_{w},u_{w})$.

  * •

Let $\mathit{branch}(u_{w})=\\{u_{w_{1}},\dots,u_{w_{p}}\\}$ with
$u_{w}=u_{w_{1}}\prec\dots\prec u_{w_{p}}=u_{1}$ (i.e.
$|w|=|w_{1}|>\dots>|w_{p}|=1$). For $1\leq i\leq p$:

    * –

Apply (32) to
$\mathtt{Ld}_{1}(u_{w},t^{j^{s}_{S}(\mathtt{p}^{1}_{1},u_{w_{i}})}_{w},u_{w_{i}})$
and add
$\mathtt{Ld}_{\mathtt{p}^{1}_{1}}(u_{w},t^{j^{s}_{S}(\mathtt{p}^{1}_{1},u_{w_{i}})}_{w},u_{w_{i}})$.

    * –

For $1\leq g\leq{\bar{n}}$ and $j=j^{s}_{S}(\mathtt{p}^{1}_{g},u_{w_{i}})$:

      * *

If $\mathtt{NIn}_{\mathtt{p}^{1}_{g}}^{\prime}(u_{w_{i}})\in\mathcal{I}$,
apply $\eqref{rul_copyNotInPred}$ and add
$\mathtt{Rdy}_{\mathtt{p}^{1}_{g}}(u_{w},t^{j}_{w},u_{w_{i}})$. Note that
$j=j^{s}_{S}(\mathtt{p}^{1}_{g},u_{w_{i}})=j^{e}_{S}(\mathtt{p}^{1}_{g},u_{w_{i}})$.

      * *

Else, $\mathtt{In}_{\mathtt{p}^{1}_{g}}^{\prime}(u_{w_{i}})\in\mathcal{I}$:
apply $\langle\rho,\sigma\rangle$ with $\rho$ the instantiation of
$\eqref{rul_loadAllFacts}$ for $\mathtt{p}^{1}_{g}$, and $\sigma(u)=u_{w}$,
$\sigma(t)=t^{j}_{w}$ and $\sigma(v)=u_{w_{i}}$. This introduces three fresh
nulls $u_{\rho,\sigma,x_{1}}=t^{j+1}_{w}$,
$u_{\rho,\sigma,x_{2}}=t^{j+\ell_{i}+2}_{w}$ and
$u_{\rho,\sigma,y}=t^{j+\ell_{i}+3}_{w}$, where $b_{1}^{i}\cdots
b_{\ell_{i}}^{i}$ is the binary representation of $|w_{i}|+1$. This adds atoms
$\mathtt{S}_{\mathtt{p}^{1}_{g}}(t^{j}_{w})$,
$\mathtt{Nxt}(t^{j}_{w},t^{j+1}_{w})$,
$\mathtt{LdE}(u_{w_{i}},t^{j+1}_{w},t^{j+\ell_{i}+2}_{w})$,
$\mathtt{Nxt}(t^{j+\ell_{i}+2}_{w},t^{j+\ell_{i}+3}_{w})$ and
$\mathtt{Rdy}_{\mathtt{p}^{1}_{g}}(u_{w},t^{j+\ell_{i}+3}_{w},u_{w_{i}})$.
Note that
$j+\ell_{i}+3=j^{s}_{S}(\mathtt{p}^{1}_{g},u_{w_{i}})+\ell_{i}+3=j^{e}_{S}(\mathtt{p}^{1}_{g},u_{w_{i}})$.

      * *

If $g<{\bar{n}}$: Apply (33) and add
$\mathtt{Ld}_{\mathtt{p}_{g+1}^{1}}(u_{w},t^{j^{\prime}}_{w},u_{w_{i}})$ with
$j^{\prime}=j$ if
$\mathtt{NIn}_{\mathtt{p}^{1}_{g}}^{\prime}(u_{w_{i}})\in\mathcal{I}$,
$j^{\prime}=j+\ell_{i}+3$ otherwise. Note that
$j^{\prime}=j^{e}_{S}(\mathtt{p}^{1}_{g},u_{w_{i}})=j^{s}_{S}(\mathtt{p}^{1}_{g+1},u_{w_{i}})$,
independently of whether
$\mathtt{In}_{\mathtt{p}^{1}_{g}}^{\prime}(u_{w_{i}})$ is in $\mathcal{I}$.

    * –

Apply (34) and add
$\mathtt{Rdy}_{1}(u_{w},t^{j^{e}_{S}(\mathtt{p}^{1}_{\bar{n}},u_{w_{i}})}_{w},u_{w_{i}})$.

    * –

If $i<p$ (i.e. $u_{w_{i}}\neq u_{1}$): Apply the instantiation of (35)
$\mathtt{Rdy}_{1}(u,t,v)\wedge\mathtt{Chi}(w,v)\to\mathtt{Ld}_{1}(u,t,w)$ and
add $\mathtt{Ld}_{1}(u_{w},t^{j^{\prime}}_{w},u_{w_{i+1}})$ with
$j^{\prime}=j^{e}_{S}(\mathtt{p}^{1}_{\bar{n}},u_{w_{i}})=j^{s}_{S}(\mathtt{p}^{1}_{1},u_{w_{i+1}})$.
Recall that $u_{w_{i+1}}$ comes right after $u_{w_{i}}$ in the lexicographic
order according to $\prec$.

  * •

At the end of the above loop, we obtain an atom
$\mathtt{Rdy}_{1}(u_{w},t^{j^{e}_{S}(\mathtt{p}^{1}_{\bar{n}},u_{1})}_{w},u_{1})$.
Apply the instantiation of (36)
$\mathtt{Rdy}_{1}(u,t,v)\wedge\mathtt{Root}(v)\to\mathtt{Ld}_{2}(u,t,u,u)$ and
add
$\mathtt{Ld}_{2}(u_{w},t^{j^{e}_{S}(\mathtt{p}^{1}_{\bar{n}},u_{1})},u_{w},u_{w})$.
Note that
$j^{e}_{S}(\mathtt{p}^{1}_{\bar{n}},u_{1})=j^{s}_{S}(\mathtt{p}^{2}_{1},u_{w},u_{w})$.

  * •

Repeat the process, so that we obtain the atoms of the following form for
$2\leq x\leq{\bar{m}}$ and
$u_{w_{1}},\dots,u_{w_{x}}\in\mathit{branch}(u_{w})$:

    * –

$\mathtt{Ld}_{x}(u_{w},t^{j}_{w},u_{w_{1}},\dots,u_{w_{x}})$ where
$j=j^{s}_{S}(\mathtt{p}^{x}_{1},u_{w_{1}},\dots,u_{w_{x}})$;

    * –

$\mathtt{Rdy}_{x}(u_{w},t^{j}_{w},u_{w_{1}},\dots,u_{w_{x}})$ where
$j=j^{e}_{S}(\mathtt{p}^{x}_{\bar{n}},u_{w_{1}},\dots,u_{w_{x}})$;

    * –

for $1\leq g\leq{\bar{n}}$:

      * *

$\mathtt{Ld}_{\mathtt{p}^{x}_{g}}(u_{w},t^{j}_{w},u_{w_{1}},\dots,u_{w_{x}})$
where $j=j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})$;

      * *

$\mathtt{Rdy}_{\mathtt{p}^{x}_{g}}(u_{w},t^{j}_{w},u_{w_{1}},\dots,u_{w_{x}})$
where $j=j^{e}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})$;

      * *

for
$\mathtt{In}_{\mathtt{p}^{x}_{g}}^{\prime}(u_{w_{1}},\dots,u_{w_{x}})\in\mathcal{I}$
and $j=j^{s}_{S}(\mathtt{p}^{x}_{g},u_{w_{1}},\dots,u_{w_{x}})$:

        * ·

$\mathtt{S}_{\mathtt{p}^{x}_{g}}(t^{j}_{w})$,

        * ·

$\mathtt{Nxt}(t^{j}_{w},t^{j+1}_{w}),\dots,\mathtt{Nxt}(t^{j+\Sigma_{l=1}^{x}\ell_{l}+x+1}_{w},t^{j+\Sigma_{l=1}^{x}\ell_{l}+x+2}_{w})$,

        * ·

$\mathtt{LdE}(u_{w_{1}},t^{j+1}_{w},t^{j+\ell_{1}+2}_{w}),\dots,\mathtt{LdE}(u_{w_{x}},t^{j+\Sigma_{l=1}^{x-1}\ell_{l}+x}_{w},t^{j+\Sigma_{l=1}^{x}\ell_{l}+x+1}_{w})$.

  * •

We have obtained an atom
$\mathtt{Rdy}_{{\bar{m}}}(u_{w},t^{j}_{w},u_{1},\dots,u_{1})$ with
$j=j^{e}_{S}({\bar{m}},u_{1},\dots,u_{1})=|S|+1$. Apply (37) and add
$\mathtt{S}_{\text{\textvisiblespace}}(t^{|S|+1}_{w})$ and
$\mathtt{End}(t^{|S|+1}_{w})$.

  * •

For all $u_{w_{i}}\in\mathit{branch}(u_{w})$ and atoms of the form
$\mathtt{LdE}(u_{w_{i}},t^{j+1}_{w},t^{j+\ell_{i}+2}_{w})$:

    * –

Apply $\langle\rho,\sigma\rangle$ with $\rho=\eqref{rul_encodeFact}$ and
$\sigma(v)=u_{w_{i}}$, $\sigma(x_{s})=t^{j+1}_{w}$,
$\sigma(x_{e})=t^{j+\ell_{i}+2}_{w}$, $\sigma(y_{1})=e_{w_{i}}^{1}$ and
$\sigma(y_{\\_})=e_{w_{i}}^{\ell_{i}}$ where $b_{1}^{i}\cdots
b_{\ell_{i}}^{i}$ is the binary representation of $|w_{i}|+1$. This introduces
two fresh nulls $u_{\rho,\sigma,z_{1}}=t^{j+2}_{w}$ and
$u_{\rho,\sigma,z_{\\_}}=t^{j+\ell_{i}+1}_{w}$ and adds the atoms:
$\mathtt{S}_{\mathord{\parallel}}(t^{j+1}_{w})$,
$\mathtt{Nxt}(t^{j+1}_{w},t^{j+2}_{w})$,
$\mathtt{Cpy}(e_{w_{i}}^{1},e_{w_{i}}^{\ell_{i}},t^{j+2}_{w},t^{j+\ell_{i}+1}_{w})$,
$\mathtt{Nxt}(t^{j+\ell_{i}+1}_{w},t^{j+\ell_{i}+2}_{w})$ and
$\mathtt{S}_{\mathord{\parallel}}(t^{j+\ell_{i}+2}_{w})$.

    * –

Apply exhaustively rules (27) and (28). This process introduces nulls
$t^{j+3},\dots,t^{j+\ell_{i}}$ and adds the following atoms (cf. proof of
Lemma 28):

      * *

$\mathtt{S}_{b^{i}_{1}}(t^{j+2}_{w}),\dots,\mathtt{S}_{b^{i}_{\ell_{i}}}(t^{j+\ell_{i}+1}_{w})$,

      * *

$\mathtt{Nxt}(t^{j+2}_{w},t^{j+3}_{w}),\dots,\mathtt{Nxt}(t^{j+\ell_{i}}_{w},t^{j+\ell_{i}+1}_{w})$

      * *

$\mathtt{Cpy}(e_{w_{i}}^{2},e_{w_{i}}^{\ell_{i}},t^{j+3}_{w},t^{j+\ell_{i}+1}_{w})$,
$\dots$,
$\mathtt{Cpy}(e_{w_{i}}^{\ell_{i}-1},e_{w_{i}}^{\ell_{i}},t^{j+\ell_{i}}_{w},t^{j+\ell_{i}+1}_{w})$.

At this point, for every null $u_{w}$ such that
$\mathtt{Leaf}(u_{w})\in\mathcal{I}$, we have added
$\mathit{startConf}(\mathcal{I},u_{w})$ and
$\mathit{loadS}(\mathcal{I},u_{w})$ and no rule is applicable. ∎

Lemma 8.
$\mathfrak{I}_{4}=\\{\mathit{Int}_{4}(\mathcal{I})\mid\mathcal{I}\in\mathfrak{I}_{3}\\}$
is a universal model set of $\mathcal{R}_{4}$ and $\mathcal{D}$.

###### Proof.

Similar to the proof of Lemma 7, using Lemmas 7 and 29. ∎

Before proving Lemma 9, we introduce some notation about TM runs. A
_configuration_ for a TM $M=\langle Q,\Gamma,\delta\rangle$ is a finite
sequence $\smash{\vec{C}}=C_{1},\ldots,C_{k}$ where $C_{i}=\\{q,a\\}$ for some
$i\leq k$, $q\in Q$, and $a\in\Gamma$, while for each $j\neq i$,
$C_{j}=\\{a_{j}\\}$ for some $a_{j}\in\Gamma$. The _successor configuration_
of $\smash{\vec{C}}$ under $M$, denoted $M(\smash{\vec{C}})$, is the
configuration
$\smash{\vec{C}}^{\prime}=C^{\prime}_{1},\ldots,C^{\prime}_{k+1}$ satisfying,
assuming $\delta(q,a)=(q^{\prime},a^{\prime},l)$,

$C^{\prime}_{j}\cap\Gamma=\left\\{\begin{array}[]{ll}\\{a^{\prime}\\}&\text{
if }j=i,\\\ \\{\text{\textvisiblespace}\\}&\text{ if }j=k+1,\\\
C_{j}\cap\Gamma&\text{ otherwise,}\end{array}\right.$

while $C^{\prime}_{j}\cap Q=\\{q^{\prime}\\}$ if $j=\max(1,i+l)$, otherwise
$\emptyset$. For a word $\vec{\gamma}=\gamma_{1},\ldots,\gamma_{k}$, let
$\mathit{StConf}(M,\vec{\gamma})$ denote the sequence
$\\{q_{S},\gamma_{1}\\}$, $\\{\gamma_{2}\\}$,
$\ldots,\\{\gamma_{k}\\},\\{\text{\textvisiblespace}\\}$. Let
$\mathit{Comp}(M,\vec{\gamma})=\smash{\vec{C}}_{1},\smash{\vec{C}}_{2},\ldots$
be the (possibly finite) configuration sequence satisfying
$\smash{\vec{C}}_{1}=\mathit{StConf}(M,\vec{\gamma})$ as well as
$\smash{\vec{C}}_{i+1}=M(\smash{\vec{C}}_{i})$, whenever defined (otherwise –
and only then – the sequence ends at $i$). Note that $M$ halts on
$\vec{\gamma}$ if $\mathit{Comp}(M,\vec{\gamma})$ is finite, and accepts
$\vec{\gamma}$ if the last configuration in $\mathit{Comp}(M,\vec{\gamma})$
features $q_{A}$.

######  Lemma 30.

Given some $\mathcal{I}\in\mathfrak{I}_{4}$, $\mathit{Int}_{5}(\mathcal{I})$
is isomorphic to the unique interpretation in a result of the chase over
$\mathcal{R}_{5}$ and $\mathcal{I}$.

###### Proof.

The interpretation $\mathit{Int}_{5}(\mathcal{I})$ is equal to the union of
the following interpretations:

  1. 1.

$\mathcal{I}$;

  2. 2.

For each $w\in\mathbf{Z}$ with $b_{1}\cdots b_{\ell}$ the binary
representation of $|w|+1$: $\\{\mathtt{Nxt}^{\\!+}(e_{w}^{i},e_{w}^{j})\mid
1\leq i<j\leq\ell\\}$.

  3. 3.

For each $u_{w}\in\mathsf{Nulls}(\mathcal{I})$ with
$S=\mathit{branchTape}(\mathcal{I},u_{w})$,
$\mathit{Comp}(M,S)=\smash{\vec{C}}_{1},\ldots,\smash{\vec{C}}_{\ell}$, and
$\smash{\vec{C}}_{i}=C_{i,1},\ldots,C_{i,|S|+i}$ for each $1\leq i\leq\ell$,
the database $\mathit{Run}(u_{w})$ defined as follows:

$\displaystyle\\{$ $\displaystyle\mathtt{Nxt}^{\\!+}(t_{w}^{i},t_{w}^{j})\mid
1\leq i<j\leq|S|+1\\}\cup~{}$ $\displaystyle\\{$
$\displaystyle\mathtt{End}(t_{w}^{i,|S|+i})\mid 2\leq i\leq\ell\\}\cup~{}$
$\displaystyle\\{$ $\displaystyle\mathtt{Nxt}(t_{w}^{i,j-1},t_{w}^{i,j})\mid
2\leq i\leq\ell,2\leq j\leq|S|+i\\}\cup~{}$ $\displaystyle\\{$
$\displaystyle\mathtt{Nxt}^{\\!+}(t_{w}^{i,j},t_{w}^{i,j^{\prime}})\mid 1\leq
i\leq\ell,1\leq j<j^{\prime}\leq|S|+i\\}\cup~{}$ $\displaystyle\\{$
$\displaystyle\mathtt{Stp}(t_{w}^{i-1,j},t_{w}^{i,j})\mid 3\leq
i\leq\ell,1\leq j\leq|S|+i-1\\}\cup~{}$ $\displaystyle\\{$
$\displaystyle\mathtt{S}_{a}(t_{w}^{i,j})\mid 2\leq i\leq\ell,1\leq
j\leq|S|+i,a\in C_{i,j}\cap\Gamma\\}\cup~{}$ $\displaystyle\\{$
$\displaystyle\mathtt{Hd}_{q}(t_{w}^{i,j})\mid 2\leq i\leq\ell,1\leq
j\leq|S|+i,q\in C_{i,j}\cap Q\\}\cup~{}$ $\displaystyle\\{$
$\displaystyle\mathtt{Goal}\mid 1\leq j\leq|S|+\ell,q_{A}\in C_{\ell,j}\\};$

We describe a (Datalog-first) chase over $\mathcal{R}_{5}$ and $\mathcal{I}$
step by step. We directly set the the names of the fresh nulls so that the
chase result coincides with $\mathit{Int}_{5}(\mathcal{I})$. Note that no rule
in Figures 1, 2, 3, 4, or 5 is applicable to $\mathcal{I}$ and that applying a
rule in Figure 6 cannot make a rule in Figures 1, 2, 3, 4, or 5 applicable.

We first apply exhaustively (40) and (41) which compute a transitive closure
on the atoms of the form $\mathtt{Nxt}(e_{w}^{i},e_{w}^{j})$ and
$\mathtt{Nxt}(t^{i}_{w},t^{j}_{w})$ in $\mathcal{I}$. This adds the atoms
$\\{\mathtt{Nxt}^{\\!+}(e_{w}^{i},e_{w}^{j})\mid 1\leq i<j\leq\ell\\}$
described in point (2) and $\\{\mathtt{Nxt}^{\\!+}(t_{w}^{i},t_{w}^{j})\mid
1\leq i<j\leq|S|+1\\}$ of the first line in point (3).

For every null $u_{w}$ such that $\mathtt{Leaf}(u_{w})\in\mathcal{I}$,
$S=\mathit{branchTape}(\mathcal{I},u_{w})$ and
$\mathit{Comp}(M,S)=\smash{\vec{C}}_{1},\ldots,\smash{\vec{C}}_{\ell}$, we
show by induction that for every $2\leq i\leq\ell$ the following atoms belong
to the chase result:

  * •

$\mathtt{End}(t^{i,|S|+i}_{w})$,

  * •

$\mathtt{Nxt}(t^{i,j-1}_{w},t^{i,j}_{w})$ for $2\leq j\leq|S|+i$,

  * •

$\mathtt{Nxt}^{\\!+}(t^{i,j}_{w},t^{i,j^{\prime}}_{w})$ for $1\leq
j<j^{\prime}\leq|S|+i$,

  * •

$\mathtt{Stp}(t_{w}^{i-1,j},t_{w}^{i,j})$ for $1\leq j\leq|S|+i-1$,

  * •

$\mathtt{S}_{a}(t^{i,j}_{w})$ for $1\leq j\leq|S|+i,a\in C_{i,j}\cap\Gamma$,

  * •

$\mathtt{Hd}_{q}(t^{i,j}_{w})$ for $1\leq j\leq|S|+i,q\in C_{i,j}\cap Q$.

_Base case $i=2$._ Recall that for every $\mathtt{Leaf}(u_{w})\in\mathcal{I}$
with serialisation $S=\mathit{branchTape}(\mathcal{I},u_{w})$, $\mathcal{I}$
includes:

$\displaystyle\\{\mathtt{Ld}_{1}(u_{w},t_{w}^{1},u_{w}),\mathtt{Hd}_{q_{S}}(t^{1}_{w}),\mathtt{End}(t_{w}^{|S|+1}),\mathtt{S}_{\text{\textvisiblespace}}(t_{w}^{|S|+1})\\}\cup\\{\mathtt{Nxt}(t_{w}^{j-1},t_{w}^{j})\mid
2\leq j\leq|S|+1\\}\cup{}$ $\displaystyle\\{\mathtt{S}_{a}(t_{w}^{j})\mid
1\leq j\leq|S|,a=S[j]\\}.$

Moreover $\smash{\vec{C}}_{1}=\mathit{StConf}(M,S)=\\{q_{S},S[1]\\}$,
$\\{S[2]\\}$, $\ldots,\\{S[|S|]\\},\\{\text{\textvisiblespace}\\}$. Let
$(q_{S},S[1])\mapsto(r,b,+1)\in\delta$ (recall that we assume that the TM will
never attempt to move left on the first position of the tape). By definition,
we have $C_{2,1}\cap\Gamma=\\{b\\}$,
$C_{2,j}\cap\Gamma=C_{1,j}\cap\Gamma=\\{S[j]\\}$ for every $1<j\leq|S|+1$, and
$C_{2,2}\cap Q=\\{r\\}$.

  * •

For every $1<j\leq|S|+1$, let $a\in C_{1,j}\cap\Gamma=C_{2,j}\cap\Gamma$.

    * –

Apply $\langle\rho,\sigma\rangle$ with $\rho$ the instantiation of (45) for
transition $(q_{S},S[1])\mapsto(r,b,+1)$ and tape symbol $S[j]$, and
$\sigma(x)=t^{1}_{w}$, $\sigma(y)=t^{j}_{w}$. This introduces a fresh null
$u_{\rho,\sigma,z}=t^{2,j}_{w}$ and adds $\mathtt{Stp}(t^{j}_{w},t^{2,j}_{w})$
and $\mathtt{S}_{S[j]}(t^{2,j}_{w})$.

  * •

Apply $\langle\rho,\sigma\rangle$ with $\rho$ the instantiation of
$\eqref{rul_tm_new_symb}$ for $(q_{S},S[1])\mapsto(r,b,+X)$ and
$\sigma(x)=t^{1}_{w}$ . This introduces a fresh null
$u_{\rho,\sigma,z}=t^{2,1}_{w}$ and adds $\mathtt{Stp}(t^{1}_{w},t^{2,1}_{w})$
and $\mathtt{S}_{b}(t^{2,1}_{w})$.

  * •

Apply $\langle\rho,\sigma\rangle$ with $\rho=\eqref{rul_tm_add_mem}$ with
$\sigma(x)=t^{|S|+1}_{w}$ and $\sigma(z)=t^{2,|S|+1}_{w}$. This introduces a
fresh null $u_{\rho,\sigma,v}=t^{2,|S|+2}_{w}$ and adds
$\mathtt{Nxt}(t^{2,|S|+1}_{w},t^{2,|S|+2}_{w})$,
$\mathtt{S}_{\text{\textvisiblespace}}(t^{2,|S|+2}_{w})$ and
$\mathtt{End}(t^{2,|S|+2}_{w})$.

  * •

Apply exhaustively (42), adding all atoms
$\mathtt{Nxt}(t^{2,j-1}_{w},t^{2,j}_{w})$ for $2\leq j\leq|S|+2$.

  * •

Apply exhaustively (40) and (41), adding all atoms
$\mathtt{Nxt}^{\\!+}(t^{2,j}_{w},t^{2,j^{\prime}}_{w})$ for $1\leq
j<j^{\prime}\leq|S|+2$.

  * •

Apply (47) and add $\mathtt{Hd}_{r}(t^{2,2}_{w})$.

_Induction step:_ Assume the property is true for some $2\leq i<\ell$ and let
$j_{0}$ be the unique $C_{i,j_{0}}$ such that $C_{i,j_{0}}\cap
Q\neq\emptyset$, $\\{q_{0}\\}=C_{i,j_{0}}\cap Q$,
$\\{a_{0}\\}=C_{i,j_{0}}\cap\Gamma$, and
$(q_{0},a_{0})\mapsto(r,b,+X)\in\delta$. By definition, we have
$C_{i+1,j_{0}}\cap\Gamma=\\{b\\}$, $C_{i+1,j}\cap\Gamma=C_{i,j}\cap\Gamma$ for
every $j\neq j_{0}$, and $C_{i+1,j_{0}+X}\cap Q=\\{r\\}$.

  * •

For every $j>j_{0}$ (resp. $j<j_{0}$), let $a\in
C_{i,j}\cap\Gamma=C_{i+1,j}\cap\Gamma$.

    * –

Apply $\langle\rho,\sigma\rangle$ with $\rho$ the instantiation of
$\eqref{rul_tm_right_mem}$ (resp. (46)) for transition
$(q_{0},a_{0})\mapsto(r,b,+X)$ and tape symbol $a$, and
$\sigma(x)=t^{i,j_{0}}_{w}$, $\sigma(y)=t^{i,j}_{w}$. This introduces a fresh
null $u_{\rho,\sigma,z}=t^{i+1,j}_{w}$ and adds
$\mathtt{Stp}(t^{i,j}_{w},t^{i+1,j}_{w})$ and $\mathtt{S}_{a}(t^{i+1,j}_{w})$.

  * •

Apply $\langle\rho,\sigma\rangle$ with $\rho$ the instantiation of
$\eqref{rul_tm_new_symb}$ for $(q_{0},a_{0})\mapsto(r,b,+X)$ and
$\sigma(x)=t^{i,j_{0}}_{w}$ . This introduces a fresh null
$u_{\rho,\sigma,z}=t^{i+1,j_{0}}_{w}$ and adds
$\mathtt{Stp}(t^{i,j_{0}}_{w},t^{i+1,j_{0}}_{w})$ and
$\mathtt{S}_{b}(t^{i+1,j_{0}}_{w})$.

  * •

Apply $\langle\rho,\sigma\rangle$ with $\rho=\eqref{rul_tm_add_mem}$ with
$\sigma(x)=t^{i,|S|+i}_{w}$ and $\sigma(z)=t^{i+1,|S|+i}_{w}$. This introduces
a fresh null $u_{\rho,\sigma,v}=t^{i+1,|S|+i+1}_{w}$ and adds
$\mathtt{Nxt}(t^{i+1,|S|+i}_{w},t^{i+1,|S|+i+1}_{w})$,
$\mathtt{S}_{\text{\textvisiblespace}}(t^{i+1,|S|+i+1}_{w})$ and
$\mathtt{End}(t^{i+1,|S|+i+1}_{w})$.

  * •

Apply exhaustively (42), adding all atoms
$\mathtt{Nxt}(t^{i+1,j-1}_{w},t^{i+1,j}_{w})$ for $2\leq j\leq|S|+i+1$.

  * •

Apply exhaustively (40) and (41), adding all atoms
$\mathtt{Nxt}^{\\!+}(t^{i+1,j}_{w},t^{i+1,j^{\prime}}_{w})$ for $1\leq
j<j^{\prime}\leq|S|+i+1$.

  * •

If $X=+1$, apply (47) and add $\mathtt{Hd}_{r}(t^{i+1,j_{0}+X}_{w})$.

  * •

If $X=-1$, then $j_{0}>1$ (since the TM never attempts to move left on the
first position of the tape): apply (48) and add
$\mathtt{Hd}_{r}(t^{i+1,j_{0}+X}_{w})$.

We have shown that all atoms of $\mathit{Run}(u_{w})$ but $\mathtt{Goal}$
belong to the chase result. Finally, for every null $u_{w}$ such that
$\mathtt{Leaf}(u_{w})\in\mathcal{I}$,
$S=\mathit{branchTape}(\mathcal{I},u_{w})$ and
$\mathit{Comp}(M,S)=\smash{\vec{C}}_{1},\ldots,\smash{\vec{C}}_{\ell}$, if
there exists $j$ such that
$\mathtt{Hd}_{q_{A}}(t^{\ell,j}_{w})\in\mathit{Run}(u_{w})$, apply (39) and
add $\mathtt{Goal}$. ∎

Lemma 9.
$\mathfrak{I}_{5}=\\{\mathit{Int}_{5}(\mathcal{I})\mid\mathcal{I}\in\mathfrak{I}_{4}\\}$