$\rightarrow$-compatible $\mathfrak{R}$-model of $\phi_{i}$, which entails
that $u\rightarrow_{\phi}^{*}v$ since by definition
$\rightarrow_{\phi_{i}}\subseteq\rightarrow_{\phi}$, contradicting our
assumption. Otherwise, let $j$ be the smallest index in
$\ell_{1},\dots,\ell_{m-1}$ such that
$\ell_{j}\not\in\mathit{dom}(\mathfrak{h}_{1})$. Since
$\ell_{j}\in\mathit{dom}(\mathfrak{h})$ (as
$\ell_{j}\rightarrow_{\lambda}\ell_{j+1}$) we deduce that
$\ell_{j}\in\mathit{dom}(\mathfrak{h}_{2})\subseteq\mathit{ref}(\mathfrak{h}_{2})$,
and $\ell_{j}\in\mathit{ref}(\mathfrak{h}_{1})$. Since $U_{1}\cap
U_{2}=\emptyset$, we get $\ell_{j}=\mathfrak{s}(\mathcal{V}(\phi_{i}))$, for
some $i=1,2$. Thus $\ell_{j}=\mathfrak{s}(u^{\prime})$ with
$u^{\prime}\in\mathcal{V}(\phi)$. Since $u\not\rightarrow_{\phi}^{*}v$, we
have by transitivity either $u\not\rightarrow_{\phi}^{*}u^{\prime}$ or
$u^{\prime}\not\rightarrow_{\phi}^{*}v$, which contradicts the minimality of
$m$ (one of the sequences $\ell_{1},\dots,\ell_{j}$ or
$\ell_{j},\dots,\ell_{m}$ satisfies the conditions above and has a length
strictly less than $m+1$).

###### Lemma 4.38

All anti-axioms admit counter-models.

###### Proof 4.39

Consider an anti-axiom
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$, with the
same notations as in Definition 4.34. Let $\mathfrak{s}$ be an injective store
such that $\mathfrak{U}_{\mathtt{loc}}\setminus\mathfrak{s}(\mathcal{V})$ is
infinite, such a store always exists since $\mathfrak{U}_{\mathtt{loc}}$ is
infinite. First assume that $\phi\not=\mathit{emp}$. In this case $\phi$
necessarily contains at least one spatial atom $\alpha$, hence at least one
variable $x=\mathit{root}(\alpha)$ of sort $\mathtt{loc}$. Since
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ is not an
axiom, $\phi$ is heap-satisfiable, thus by Lemma 4.36 (applied with
$U\overset{\text{\tiny\it
def}}{=}\mathfrak{U}_{\mathtt{loc}}\setminus\mathfrak{s}(\mathcal{V})$),
$\phi\curlywedge\xi$ admits a $\rightarrow$-compatible model
$(\mathfrak{s},\mathfrak{h})$, such that $\mathit{dom}(\mathfrak{h})\subseteq
U\cup\mathfrak{s}(\mathit{alloc}(\phi))$. Since
$U\cap\mathfrak{s}(\mathcal{V})=\emptyset$, we have, for all
$u\in\mathcal{V}$,
$\mathfrak{s}(u)\in\mathit{dom}(\mathfrak{h})\iff\mathfrak{s}(u)\in\mathfrak{s}(\mathit{alloc}(\phi))$.
Since $\mathfrak{s}$ is injective, we deduce that

$\mathfrak{s}(u)\in\mathit{dom}(\mathfrak{h})\iff
u\in\mathit{alloc}(\phi)\quad(\dagger).$

Note that if $\phi=\mathit{emp}$, then the structure
$(\mathfrak{s},\mathfrak{h})$ with $\mathfrak{h}=\emptyset$ also satisfies
$(\dagger)$, since $\rightarrow_{\mathfrak{h}}$, $\rightarrow_{\phi}$,
$\mathit{dom}(\mathfrak{h})$ and $\mathit{alloc}(\phi)$ are all empty in this
case.

We show that $(\mathfrak{s},\mathfrak{h})$ is a counter-model of
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$. Since
$\mathfrak{s}$ is injective, in particular $\mathfrak{s}$ must be injective on
$V$, because otherwise $V$ would contain two occurrences of the same variable,
hence $\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ would
be an axiom, contradicting Definition 4.34. If $V$ contains a variable $y$
such that $\mathfrak{s}(y)\in\mathit{dom}(\mathfrak{h})$ then $(\dagger)$
entails that $y\in\mathit{alloc}(\phi)$, which is impossible since
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ would then
be an axiom. We prove that
$(\mathfrak{s},\mathfrak{h})\not\models_{\mathfrak{R}}\psi\curlywedge\zeta$ by
considering each case from Definition 4.34 separately.

  1. 1.

If $\mathit{alloc}(\psi)\setminus\mathit{alloc}(\phi)$ contains a variable
$y$, then by $(\dagger)$ we have
$\mathfrak{s}(y)\not\in\mathit{dom}(\mathfrak{h})$, which by Lemma 4.2 entails
that $(\mathfrak{s},\mathfrak{h})\not\models_{\mathfrak{R}}\psi$.

  2. 2.

If $\psi=\mathit{emp}$ and $\phi\not=\mathit{emp}$, then $\phi$ contains at
least one atom, hence $\mathit{alloc}(\phi)\not=\emptyset$. By Lemma 4.2,
$\mathfrak{s}(\mathit{alloc}(\phi))\subseteq\mathit{dom}(\mathfrak{h})$, thus
$\mathfrak{h}\not=\emptyset$ and
$(\mathfrak{s},\mathfrak{h})\not\models_{\mathfrak{R}}\psi\curlywedge\zeta$.

  3. 3.

Assume that there exists a variable
$x^{\prime}\in\mathit{alloc}(\phi)\setminus\mathit{alloc}(\psi)$ such that
$y\not\rightarrow_{\phi}x^{\prime}$, for all ${y\in\mathit{alloc}(\psi)}$, and
that $(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\psi$. By Lemma 4.2 we
have
$\mathfrak{s}(x^{\prime})\in\mathit{dom}(\mathfrak{h})\subseteq\mathit{ref}(\mathfrak{h})$,
thus by Proposition 4.9 there exists $y\in\mathit{alloc}(\psi)$ such that
$\mathfrak{s}(y)\rightarrow_{\mathfrak{h}}^{*}\mathfrak{s}(x)$. Since
$(\mathfrak{s},\mathfrak{h})$ is a $\rightarrow$-compatible model of $\phi$
necessarily $y\rightarrow_{\phi}^{*}x^{\prime}$, which contradicts the above
assumption.

For the remaining cases, we will apply Lemma 4.36 to obtain a heap, using a
variable $x$ that is in $V\cap(\mathcal{V}(\phi)\setminus\mathcal{V}(\psi))$
(for Condition 4) or in
$\mathcal{V}_{\mathtt{loc}}(\phi)\setminus(\mathcal{V}(\psi)\cup\mathit{alloc}(\phi))$
(for Condition 5). Note that by Lemma 4.36 this entails in particular that
$\mathfrak{s}(x)\in\mathit{ref}(\mathfrak{h})$.

  1. 4.

Assume that $x\in V\cap\mathcal{V}(\phi)$ and $x\not\in\mathcal{V}(\psi)$.
Then $\mathfrak{s}(x)\in\mathit{ref}(\mathfrak{h})$ and since $x\in V$ we get
${\mathfrak{s}(x)\not\in\mathit{dom}(\mathfrak{h})}$. By Lemma 4.11, if
$(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\psi$ then we have
$\mathfrak{s}(x)\in\mathfrak{s}(\mathcal{V}(\psi))$, and
$x\in\mathcal{V}(\psi)$ since $\mathfrak{s}$ is injective. Thus we get a
contradiction.

  2. 5.

Assume that $x\in\mathcal{V}_{\mathtt{loc}}(\phi)$,
$x\not\in\mathcal{V}(\psi)$ and $x\not\in\mathit{alloc}(\phi)$. By
$(\dagger)$, we deduce that
$\mathfrak{s}(x)\not\in\mathit{dom}(\mathfrak{h})$. Assume that
$(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\psi$. Since
$x\not\in\mathcal{V}(\psi)$ and $\mathfrak{s}$ is injective, we get
$\mathfrak{s}(x)\not\in\mathfrak{s}(\mathcal{V}(\psi))$. By Lemma 4.11, we
deduce that $\mathfrak{s}(x)\not\in\mathit{ref}(\mathfrak{h})$, a
contradiction.

###  4.5 Proof Trees

A proof tree is a (possibly infinite) tree with nodes labeled by sequents,
such that if a node labeled by ${\cal S}$ has successors labeled by ${\cal
S}_{1},\dots,{\cal S}_{n}$ then there exists a rule instance of the form
$\frac{{\cal S}_{1}\dots\cal S_{n}}{{\cal S}}$. We will usually identify the
nodes in a proof tree with the sequents labeling them. A path from ${\cal S}$
to ${\cal S}^{\prime}$ in a proof tree is a finite sequence ${\cal
S}_{0},\dots,{\cal S}_{n}$ such that ${\cal S}={\cal S}_{0}$, ${\cal
S}_{n}={\cal S}^{\prime}$ and for all $i=1,\dots,n$, ${\cal S}_{i}$ is a
successor of ${\cal S}_{i-1}$. A proof tree is fully expanded if all its
leaves are axioms. It is rational if it contains a finite number of subtrees,
up to a renaming of variables. Note that rational trees may be infinite, but
they can be represented finitely. A sequent ${\cal S}^{\prime}$ is a
descendant of a sequent ${\cal S}$ if there exists a proof tree with a path
from ${\cal S}$ to ${\cal S}^{\prime}$.

###### Example 4.40

Let $\mathfrak{R}$ be the following set of rules, where
$\mathtt{a},\mathtt{b}$ denote constant symbols and $u$ is a variable of the
same sort as $\mathtt{b}$:

$p(x,y)$ | $\Leftarrow$ | $x\mapsto(\mathtt{a},y,z)*p(z,y)$
---|---|---
$p(x,y)$ | $\Leftarrow$ | $x\mapsto(\mathtt{b})$
$r(x)$ | $\Leftarrow$ | $x\mapsto(\mathtt{a},y,z)*r(z)$
$r(x)$ | $\Leftarrow$ | $x\mapsto(u)$

The sequent $p(x,y)\vdash_{\mathfrak{R}}^{\emptyset}r(x)$ admits the following
rational proof tree (the sequent $p(z,y)\vdash_{\mathfrak{R}}^{\emptyset}r(z)$
is identical to the conclusion up to a renaming):

axiom
$x\mapsto(\mathtt{a},y,z)\vdash_{\mathfrak{R}}^{\\{z\\}}x\mapsto(\mathtt{a},y,z)$
$p(z,y)\vdash_{\mathfrak{R}}^{\emptyset}r(z)$ V
$p(z,y)\vdash_{\mathfrak{R}}^{\\{x\\}}r(z)$ S
$x\mapsto(\mathtt{a},y,z)*p(z,y)\vdash_{\mathfrak{R}}^{\emptyset}x\mapsto(\mathtt{a},y,z)*r(z)$
I $x\mapsto(\mathtt{a},y,z)*p(z,y)\vdash_{\mathfrak{R}}^{\emptyset}r(x)$ axiom
$x\mapsto(\mathtt{b})\vdash_{\mathfrak{R}}^{\emptyset}x\mapsto(\mathtt{b})$ I
$x\mapsto(\mathtt{b})\vdash_{\mathfrak{R}}^{\emptyset}r(x)$ U
$p(x,y)\vdash_{\mathfrak{R}}^{\emptyset}r(x)$

###### Remark 4.41

Note that, since infinite proof trees are allowed, the fact that each rule is
sound does not imply that the procedure itself is sound, i.e., that the root
of every fully expanded proof tree is valid. The latter property holds only
for the strategy introduced in the next section, see Theorem 5.21.

###  4.6 The Strategy

In this section, we introduce a strategy to restrict the application of the
inference rules, which will ensure both the soundness and efficiency of the
proof procedure. To this purpose, we define a set of variables ${\cal
V}^{\dagger}({\cal S})$ which denotes the variables occurring at non-root
positions on the right-hand side of the considered sequent, but not in the set
of non-allocated variables $V$. As we shall see, the strategy will handle the
sequents in different ways depending on the number of such variables. Recall
that $\mathit{width}(\mathfrak{R})$ denotes the maximal arity of the predicate
symbols and tuples occurring in $\mathfrak{R}$.

###### Definition 4.42

For every sequent ${\cal S}=\lambda\vdash_{\mathfrak{R}}^{V}\gamma$, we denote
by ${\cal V}^{\dagger}({\cal S})$ the set
$\mathcal{V}_{\mathtt{loc}}(\gamma)\setminus(V\cup\mathit{alloc}(\gamma))$. A
sequent ${\cal S}$ is narrow if it is equality-free and $\mathit{card}({\cal
V}^{\dagger}({\cal S}))\leq\mathit{width}(\mathfrak{R})$.

Note that in particular, if $\gamma$ is a spatial atom, then ${\cal S}$ is
necessarily narrow since in this case we must have
$\mathit{card}(\mathcal{V}(\gamma))\leq\mathit{ar}_{\mathit{max}}(\mathfrak{R})\leq\mathit{width}(\mathfrak{R})$.
The inference rules are applied with the following strategy:

###### Definition 4.43

We assume a selection function is given, mapping every nonempty finite set of
expressions (i.e., formulas or rule applications) $S$ to an element of $S$;
this element is said to be selected in $S$. A proof tree is admissible if all
the rule applications occurring in it fulfill the following conditions (see
Figure 1 for the notations):

  1. 1.

No rule is applied on an axiom or an an anti-axiom, and no rule is applied if
one of the premises is an anti-axiom.

  2. 2.

I is applied only if $\zeta=\top$ and $\psi=\mathit{emp}$.

  3. 3.

U is applied only if $\gamma$ is of one of the forms
$q(x_{1},\bm{y})\curlywedge\top$ or $x_{1}\mapsto\bm{y}\curlywedge\top$, where
$x_{1}$ is the first component of the vector $\bm{t}$ (as defined in the
rule).

  4. 4.

C is applied only if $\gamma$ is of the form $\psi\curlywedge\top$,
$x\in\mathit{alloc}(\phi)$,
$y\in\mathcal{V}(\gamma)\setminus(\mathit{alloc}(\phi)\cup V)$, $\psi$ is a
predicate atom and $x\not\approx y$ does not already occur in $\xi$.

  5. 5.

S is applied only if $\xi_{1}=\xi_{2}$, $\zeta_{1}=\zeta_{2}=\top$, and
$\psi_{1}$ is selected in the set of atoms in $\psi_{1}*\psi_{2}$.
Furthermore, if the conclusion is not narrow, then the rule is applied only if
the left-premise is valid (this will be tested by applying the decision
procedure recursively).

  6. 6.

The rules are applied with the following priority (meaning that no rule can be
applied if a rule with a higher priority is also applicable):

$\text{{\color[rgb]{0,0,1} {\tt W}}}\ >\text{{\color[rgb]{0,0,1} {\tt V}}}\
>\text{{\color[rgb]{0,0,1} {\tt R}}}\ >\text{{\color[rgb]{0,0,1} {\tt E}}}\
>\text{{\color[rgb]{0,0,1} {\tt S}}}\ >\text{{\color[rgb]{0,0,1} {\tt U}}}\
>\text{{\color[rgb]{0,0,1} {\tt C}}}\ >\text{{\color[rgb]{0,0,1} {\tt I}}}.$

  7. 7.

For all the rules other than  S, and for all applications of  S on a sequent
that is not narrow, if several applications of the rule are possible and all
fulfill the conditions above, then only the one that is selected in the set of
possible rule applications can be applied.

From now on, we assume that all the considered proof trees are admissible (the
soundness222The soundness of each individual rule, as stated by Lemmata 4.26
and 4.29, does not depend on Definition 4.43, but the global soundness of the
procedure, as stated in Theorem 5.21 holds only for admissible proof trees.
and completeness proofs below, as well as the complexity analysis hold with
this requirement). No assumption is made on the selection function, for
instance one may assume that $\psi_{1}$ is the leftmost atom in
$\psi_{1}*\psi_{2}$ (i.e., the atoms are ordered according to the order in
which they occur in the formula) and that the first detected rule application
is applied, except for  S if the conclusion is narrow.

Many of the conditions in Definition 4.43 are quite natural, and simply aim at
pruning the search space by avoiding irrelevant rule applications. For
instance, applying a rule on an axiom or on an anti-axiom is clearly useless.
The priority order is chosen in such a way that the rules with the minimal
branching factor are applied first, postponing the most computationally costly
rules. Similarly, the rules operating on spatial atoms ( I or  U) are
postponed until all pure formulas have been handled. The unfolding of the
atoms on the left-hand side of a sequent (Rule  U) is postponed until the
right-hand side has been fully decomposed (using rule  S), yielding a unique
spatial atom. This permits to guide the choice of the atom to be unfolded on
the left-hand side: we only unfold the atom with the same root as the one on
the right-hand side. Rule  C may cause a costly explosion if applied blindly,
thus the application conditions are carefully designed. They are meant to
ensure that the rule application is really useful, in the sense that it
permits further applications of rule  I. Condition 7 in Definition 4.43 is
meant to ensure that the considered rules are applied with a “don’t care”
strategy, meaning that if several rule applications are possible then one of
them (the selected one) is chosen arbitrarily and the others are ignored. This
is justified by the fact that these rules are invertible, hence exploring all
possibilities is useless. Such a strategy is crucial for proving that the
procedure runs in polynomial time. In contrast, if the conclusion of  S is
narrow, then the rule must applied with a “don’t know” indeterminism, i.e.,
all possible applications must be considered. This is necessary for
completeness, due to the fact that the rule is not invertible in this case. Of
course, all these possible rule applications must be taken into account for
the complexity analysis. In other words, one must cope with two different
kinds of branching: an “and-branching” due to the fact that a given rule may
have several premises, and an “or-branching” due to the fact that there may be
several ways of applying a given rule on a given sequent. By Condition 7, the
latter branching occurs only when the rule  S is applied on a narrow sequent;
in all other cases, only the selected rule application can be considered hence
there is no or-branching.

The requirement that $\psi_{1}$ must be selected in Condition 5 ensures that
only one decomposition $\psi_{1}*\psi_{2}$ can be considered for the right-
hand side of a given sequent. This avoids for instance the exponential blow-up
that would occur if the same decomposition was performed in different orders.
Note that, to check whether the left premise is valid in Condition 5, it is
necessary to recursively invoke the proof procedure. As we shall see below,
this is feasible because this premise and all its descendants are necessarily
narrow:

###### Proposition 4.44

Let ${\cal S}_{1}$ be an equality-free sequent. For every successor ${\cal
S}_{2}$ of ${\cal S}_{1}$, the relation ${\cal V}^{\dagger}({\cal
S}_{2})\subseteq{\cal V}^{\dagger}({\cal S}_{1})$ holds. Consequently, if a
sequent is narrow then all its descendants are narrow.

###### Proof 4.45

Let ${\cal S}_{i}=\lambda_{i}\vdash_{\mathfrak{R}}^{V_{i}}\gamma_{i}$ for
$i=1,2$. Assume for the sake of contradiction that ${\cal V}^{\dagger}({\cal
S}_{2})\setminus{\cal V}^{\dagger}({\cal S}_{1})$ contains a variable $u$. By
definition, $u\in\mathcal{V}(\gamma_{2})$ and
$u\not\in\mathit{alloc}(\gamma_{2})\cup V_{2}$. First assume that
$u\not\in\mathcal{V}(\gamma_{1})$, i.e., that $u$ was introduced by the
application of an inference rule to ${\cal S}_{1}$. By Proposition 4.23 (4),
the only rule that can introduce new variables to the right-hand side of a
sequent is  I. Indeed, since we assume that all inferences are admissible, by
Condition 4 of Definition 4.43,  C must replace a variable $x$ by a variable
$y$ occurring in $\mathcal{V}(\gamma_{1})$. Rule  I replaces a predicate atom
$p(x,\bm{z})$ that occurs in $\gamma_{1}$ by a formula of the form
$\gamma_{1}^{\prime}\sigma$, where
$p(x,\bm{z})\Leftarrow_{\mathfrak{R}}\gamma_{1}^{\prime}\curlywedge\zeta^{\prime}$.
Since the rules in $\mathfrak{R}$ are $\mathtt{P}$-rules, by Condition 2 of
Definition 2.9, all the variables occurring in $\gamma_{1}^{\prime}\sigma$ but
not in $p(x,\bm{z})$ must occur as roots in $\gamma_{1}^{\prime}\sigma$. This
entails that
$\mathcal{V}(\gamma_{2})\setminus\mathcal{V}(\gamma_{1})\subseteq\mathit{alloc}(\gamma_{2})$,
which contradicts the fact that $u\not\in\mathit{alloc}(\gamma_{2})\cup V$. We
deduce that $u\in\mathcal{V}(\gamma_{1})$.

Assume that $u\in V_{1}$. Since $u\notin V_{2}$, the inference rule applied to
${\cal S}_{1}$ must have deleted a variable from $V_{1}$. The only rules that
can delete variables from $V_{1}$ are  V and  C by Proposition 4.23 (2). Rule
V applies only on a variable $x\not\in\mathcal{V}(\gamma_{1})$, thus we cannot
have $x=u$. If Rule  C is applied and replaces a variable $x$ by $y$, then $x$
cannot occur in ${\cal S}_{2}$, hence $u\not=x$. Thus we must have $u\not\in
V_{1}$.

Finally assume that $u\in\mathit{alloc}(\gamma_{1})$. Since
$u\notin\mathit{alloc}(\gamma_{2})$, the inference rule applied to ${\cal
S}_{1}$ must have deleted a variable from $\mathit{alloc}(\gamma_{1})$. The
only rules that can delete variables from $\mathit{alloc}(\gamma_{1})$ are  S
and  C by Proposition 4.23 (3). Again, if rule  C replaces a variable $x$ by
$y$, then $x$ cannot occur in ${\cal S}_{2}$, hence $u\not=x$. Now, consider
rule  S and let ${\cal S}_{2}^{\prime}\overset{\text{\tiny\it
def}}{=}\lambda_{2}^{\prime}\vdash_{\mathfrak{R}}^{V_{2}^{\prime}}\gamma_{2}^{\prime}$
be the other premise of the rule. Since $u\in\mathit{alloc}(\gamma_{1})$ and
${\cal S}_{1}$ is not an anti-axiom, we must have
$u\in\mathit{alloc}(\lambda_{1})$, which entails by definition of the rule
that $u\in\mathit{alloc}(\lambda_{2})\cup V_{2}$ and
$u\in\mathit{alloc}(\lambda_{2}^{\prime})\cup V_{2}^{\prime}$. Still by
definition of rule  S, if a variable is the root of a spatial atom occurring
on the right-hand side of the conclusion $\gamma_{1}$, then this spatial atom
must occur on the right-hand side of one of the premises $\gamma_{2}$ or
$\gamma_{2}^{\prime}$. This entails that
$u\in\mathit{alloc}(\gamma_{2})\cup\mathit{alloc}(\gamma_{2}^{\prime})$.
Furthermore, we must have
$\mathit{alloc}(\lambda_{2})\cap\mathit{alloc}(\lambda_{2}^{\prime})=\emptyset$
because otherwise ${\cal S}_{1}$ would contain two atoms with the same root,
hence would be an axiom. Since $u\not\in V_{2}$ we deduce that
$u\in\mathit{alloc}(\lambda_{2})$, and that $u\in V_{2}^{\prime}$. If
$u\not\in\mathit{alloc}(\gamma_{2})$ then necessarily
$u\in\mathit{alloc}(\gamma_{2}^{\prime})$. Since ${\cal S}_{2}^{\prime}$ is
not an anti-axiom we deduce that $u\in\mathit{alloc}(\lambda_{2}^{\prime})$,
which entails that ${\cal S}_{2}^{\prime}$ is an axiom since
$\mathit{alloc}(\lambda_{2}^{\prime})\cap V_{2}^{\prime}\not=\emptyset$, a
contradiction.

The second part of the proposition follows by an immediate induction, using
the fact that no rule can introduce any equality in its premises.

We call auxiliary successors the sequents whose validity must be tested to
check whether rule  S is applicable or not, according to Definition 4.43:

###### Definition 4.46

A sequent ${\cal S}$ is an auxiliary successor of a sequent ${\cal
S}^{\prime}$ if:

  * •

${\cal S}$ is not an anti-axiom and is not narrow,

  * •

${\cal S}^{\prime}$ is not an axiom,

  * •

${\cal S}^{\prime}$ and ${\cal S}$ are of the form
$\phi^{\prime}\curlywedge\xi\vdash_{\mathfrak{R}}^{V^{\prime}}\psi^{\prime}\curlywedge\top$
and
$(\phi^{\prime}*\phi)\curlywedge\xi\vdash_{\mathfrak{R}}^{V}(\psi^{\prime}*\psi)\curlywedge\top$
respectively, where $\psi^{\prime}$ is a spatial atom, and
$V^{\prime}=V\cup\mathit{alloc}(\phi)$.

If the sequent ${\cal S}$ in Definition 4.46 is valid, then it is the left
premise of an application of  S on ${\cal S}^{\prime}$. The following
proposition gives an upper-bound on the number of auxiliary successors.

###### Proposition 4.47

Assume that $\mathit{ar}_{\mathit{max}}(\mathfrak{R})\leq\kappa$ (i.e., that
the maximal arity of the predicates is bounded by $\kappa$). Then every
sequent ${\cal S}$ has at most $2^{\kappa}$ auxiliary successors, and each of
these auxiliary successors can be computed in polynomial time.

###### Proof 4.48

If ${\cal S}$ admits an auxiliary successor, then ${\cal S}$ is necessarily of
the form $\phi\wedge\xi\vdash_{\mathfrak{R}}^{V}\psi_{1}*\psi_{2}$ where
$\psi_{1}$ is the selected predicate atom in $\psi_{1}*\psi_{2}$ according to
Definition 4.43. To get an auxiliary successor of ${\cal S}$, one has to
decompose $\phi$ into $\phi_{1}*\phi_{2}$, in such a way that the obtained
premises ${\cal
S}_{i}=\phi_{i}\curlywedge\xi\vdash_{\mathfrak{R}}^{V_{i}}\psi_{i}$ (with
$V_{i}=V\cup\mathit{alloc}(\phi_{3-i})$) are not anti-axioms. For each atom
$\alpha$ in $\phi$ such that $\mathit{root}(\alpha)\in\mathcal{V}(\psi_{1})$,
we first choose whether $\alpha$ occurs in $\phi_{1}$ or $\phi_{2}$. There is
at most one such atom for each variable, because otherwise $\phi$ would be
heap-unsatisfiable and ${\cal S}$ would be an axiom, and $\psi_{1}$ contains
at most $\kappa$ variables, thus there are at most $2^{\kappa}$ possible
choices.

We show that, once this choice is performed, the decomposition
$\phi=\phi_{1}*\phi_{2}$ is also fixed. We denote by $E$ the set of variables
$\mathcal{V}(\psi_{1})\setminus\mathit{alloc}(\phi_{1})$. Let $\alpha$ be a
predicate atom with root $x$ in $\phi$, and let $y_{0}$ be the root of
$\psi_{1}$. If $x=y_{0}$ then necessarily $\alpha$ occurs in $\phi_{1}$, since
otherwise $x\in V_{1}$ and ${\cal S}_{1}$ would be an anti-axiom. If for all
paths
$y_{0}\rightarrow_{\phi}y_{1}\rightarrow_{\phi}\dots\rightarrow_{\phi}y_{n}\rightarrow_{\phi}x$,
there exists $i=1,\dots,n$ such that $y_{i}\in E$, then necessarily
$y\not\rightarrow_{\phi_{1}}^{*}x$ and thus $\alpha$ cannot occur in
$\phi_{1}$, as otherwise ${\cal S}_{1}$ would be an anti-axiom. We finally
show that for every atom $\alpha^{\prime}$ in $\phi$ with root $x^{\prime}$,
if there exists a path
$y_{0}\rightarrow_{\phi}y_{1}\rightarrow_{\phi}\dots\rightarrow_{\phi}y_{n}\rightarrow_{\phi}x^{\prime}$
such that $\\{y_{1},\dots,y_{n},x^{\prime}\\}\cap E=\emptyset$, then
$\alpha^{\prime}$ occurs in $\phi_{1}$ (thus, in particular, $\alpha$ occurs
in $\phi_{1}$ if the previous conditions are not satisfied, since $x\not\in
E$, as $x\not\in\mathcal{V}(\psi_{1})$). We assume, w.l.o.g., that the
considered path is the minimal one not satisfying the property, so that the
atoms with roots $y_{0},\dots,y_{n}$ all occur in $\phi_{1}$. This entails
that $y_{0}\rightarrow_{\phi_{1}}^{*}x^{\prime}$. If
$x^{\prime}\not\in\mathcal{V}(\psi_{1})$ then $\alpha$ must occur in
$\phi_{1}$, otherwise ${\cal S}_{1}$ would be an anti-axiom, because we would
have $x^{\prime}\in V_{1}$, as $x^{\prime}\in\mathit{alloc}(\phi_{2})$.
Otherwise, since $x^{\prime}\not\in E$, we have
$x^{\prime}\in\mathit{alloc}(\phi_{2})$, by definition of $E$.

##  5 Properties of the Proof Procedure

###  5.1 Soundness

We prove that the proof procedure is sound, in the sense that the root of
every fully expanded proof tree fulfilling the conditions of Definition 4.43
is valid. As infinite proof trees are allowed, this does not follow from the
fact that all the rules are sound. We show that every infinite branch contains
infinitely many applications of the rule  S. As we shall see, this is
sufficient to ensure that no counter-model exists, since otherwise the size of
the smallest counter-model would be decreasing indefinitely along some
infinite branch. We recall that the rules are meant to be applied bottom-up: a
rule is applicable on some sequent ${\cal S}$ if it admits an instance with
conclusion ${\cal S}$, yielding some premises ${\cal S}_{1},\dots,{\cal
S}_{n}$. We focus on sequents on which rule  I is applied (which we call
I-reducible), and we establish some useful properties.

###### Definition 5.1

A sequent is  I-reducible if rule  I can be applied on it; this entails that
no other rule is applicable, as all other rules have priority over  I. A
sequent ${\cal S}$ is quasi- I-reducible if it is of the form
$(x\mapsto\bm{y}*\phi)\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\top$,
where $\xi$ is a conjunction of disequations, $\psi$ is a predicate atom with
root $x$, and ${\cal S}$ is not an axiom. If ${\cal S}$ is quasi- I-reducible
then we denote by ${\cal V}_{\mapsto}({\cal S})$ the set of variables
occurring in $\bm{y}$.

Note that the definition of ${\cal V}_{\mapsto}({\cal S})$ is unambiguous
because the left-hand side of ${\cal S}$ cannot contain more than one points-
to atom with root $x=\mathit{root}(\psi)$, otherwise it would be heap-
unsatisfiable and ${\cal S}$ would be an axiom. It is easy to check that every
I-reducible sequent is quasi- I-reducible (see Definition 4.43, Condition 2).
The converse does not hold in general, because rules  W,  V or  C may be
applicable on the considered sequent, and they have priority over  I. We
observe that the application of  I is necessarily interleaved with that of  S:

###### Lemma 5.2

Every path in a proof tree between two distinct  I-reducible sequents contains
an application of rule  S.

###### Proof 5.3

Let ${\cal S}_{1}$ be an  I-reducible sequent and assume that ${\cal S}_{2}$
is a descendant of ${\cal S}_{1}$. By definition, the only rule that applies
on ${\cal S}_{1}$ is  I, yielding a sequent ${\cal S}_{1}^{\prime}$. Since the
rules in $\mathfrak{R}$ are $\mathtt{P}$-rules, necessarily the right-hand
side of ${\cal S}_{1}^{\prime}$ contains exactly one points-to atom. Since
${\cal S}_{2}$ is  I-reducible,  I applies on ${\cal S}_{2}$, which entails
that no points-to atom can occur on the right-hand side of ${\cal S}_{2}$
(since  I applies only when the right-hand side is a predicate atom). The only
rule that can remove a points-to atom from the right-hand side of a sequent is
S, thus  S necessarily applies along the path from ${\cal S}_{1}$ to ${\cal
S}_{2}$.

To analyze the termination behavior of the rules, we define a new set of
variables ${\cal V}^{\star}({\cal S})$, which is similar to ${\cal
V}^{\dagger}({\cal S})$: it contains variables that occur on the right-hand
side of the considered sequent but are not allocated on the left-hand side,
and that do not occur either in the set of non-allocated variables $V$.

###### Definition 5.4

For every sequent ${\cal S}=\lambda\vdash_{\mathfrak{R}}^{V}\gamma$, we denote
by ${\cal V}^{\star}({\cal S})$ the set
$\mathcal{V}_{\mathtt{loc}}(\gamma)\setminus(V\cup\mathit{alloc}(\lambda))$.

Note that, since the considered inferences are admissible, if rule  C applies
on variables $x,y$ (with the notations of the rule), then necessarily
$y\in{\cal V}^{\star}({\cal S})$ and $x\in\mathcal{V}(\lambda)$ (see Condition
4 in Definition 4.43). The next proposition states that the rules (except
possibly  R) cannot add new variables in the set ${\cal V}^{\star}({\cal S})$.

###### Proposition 5.5

Let ${\cal S}_{1}$ be a sequent containing no equality. For every successor
${\cal S}_{2}$ of ${\cal S}_{1}$, we have ${\cal V}^{\star}({\cal
S}_{2})\subseteq{\cal V}^{\star}({\cal S}_{1})$.

###### Proof 5.6

The proof is similar to that of Proposition 4.44. Let ${\cal
S}_{i}=\lambda_{i}\vdash_{\mathfrak{R}}^{V_{i}}\gamma_{i}$ (for $i=1,2$).
Assume for the sake of contradiction that $v\in{\cal V}^{\star}({\cal
S}_{2})\setminus{\cal V}^{\star}({\cal S}_{1})$. By definition of ${\cal
V}^{\star}({\cal S}_{i})$, $v$ is of sort $\mathtt{loc}$,
$v\in\mathcal{V}(\gamma_{2})$, $v\not\in\mathit{alloc}(\lambda_{2})\cup
V_{2}$, and either $v\not\in\mathcal{V}(\gamma_{1})$ or
$v\in\mathit{alloc}(\gamma_{1})\cup V_{1}$. First assume that
$v\not\in\mathcal{V}(\gamma_{1})$. Since ${\cal S}_{1}$ contains no equality
and $v\notin{\cal V}^{\star}({\cal S}_{1})$, by Proposition 4.23 (4), the only
rule that can introduce new variables to the right-hand side of a sequent is
I. If Rule  I is applied, then we must have $v=y_{i}\sigma$ for some
$i=1,\dots,n$, with the notations used in the definition of the rule. Since
all the rules in $\mathfrak{R}$ are $\mathtt{P}$-rules, $\gamma_{2}$
necessarily contains an atom with root $v$ and
$v\in\mathit{alloc}(\gamma_{2}$). Since $v\not\in\mathit{alloc}(\lambda_{2})$,
this entails by Definition 4.34 (1) that ${\cal S}_{2}$ is an anti-axiom,
which contradicts Condition 1 in Definition 4.43. Thus we necessarily have
$v\in\mathcal{V}(\gamma_{1})$. Now assume that
$v\in\mathit{alloc}(\gamma_{1})\cup V_{1}$. Then by Proposition 4.23 (7), the
only rule that can remove a variable $v$ from $\mathit{alloc}(\gamma_{1})\cup
V_{1}$ is  C, setting $x=v$. However,  C replaces $x$ by another variable in
the entire sequent, hence we have $x\not\in\mathcal{V}(\gamma_{2})$, thus $x$
cannot be $v$.

We show (Lemma 5.19) that the rules terminate in polynomial time if  I is not
applied. To this purpose we prove that both the depth of the proof tree and
the number of branches are polynomial. We first introduce the following
definition:

###### Definition 5.7

A path ${\cal S}_{0},\dots,{\cal S}_{n}$ in a proof tree from ${\cal S}$ to
${\cal S}^{\prime}$ is  I-free if there is no application of the rule  I on
${\cal S}_{0},\dots,{\cal S}_{n-1}$. A descendant ${\cal S}^{\prime}$ of
${\cal S}$ is called  I-free if the path from ${\cal S}$ to ${\cal
S}^{\prime}$ is  I-free.

The first goal is thus to prove that the length of all  I-free paths is
bounded. Then we will derive a bound on the total number of  I-free
descendants. To this purpose, we analyze the rules that can be applied on
quasi- I-reducible sequents, and derive a number of easy but useful technical
results.

###### Proposition 5.8

If a sequent ${\cal S}$ is quasi- I-reducible then the only rules that can be
applied on ${\cal S}$ are  I,  W,  C, or  V. Moreover, for every  I-free
descendant ${\cal S}^{\prime}$ of ${\cal S}$, the sequent ${\cal S}^{\prime}$
is quasi- I-reducible and ${\cal V}_{\mapsto}({\cal S})\cap\mathcal{V}({\cal
S}^{\prime})\subseteq{\cal V}_{\mapsto}({\cal S}^{\prime})$.

###### Proof 5.9

The proof is by an inspection of the different rules. Note that if  U applies
on
$(x\mapsto\bm{y}*\phi)\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\top$
(with the notations of Definition 5.1), then, by Definition 4.43 (Condition
3), $\phi$ must contain an atom with the same root as $\mathit{root}(\psi)=x$,
hence $(x\mapsto\bm{y}*\phi)$ is heap-unsatisfiable and the sequent is an
axiom. For the second part, it is clear that the only rule among  W,  C or  V
that can delete a variable $x$ from ${\cal V}_{\mapsto}({\cal S})$ is  C, and
this rule entirely removes $x$ from the sequent.

###### Proposition 5.10

The premises of  U are quasi- I-reducible.

###### Proof 5.11

We use the notations of the rule. By Definition 4.43 (Condition 3), $\gamma$
is a predicate atom with the same root as $p(\bm{t})$ and $\xi$ is a
conjunction of disequations. Since the rules in $\mathfrak{R}$ are
$\mathtt{P}$-rules, every formula $\phi_{i}$ contains a points-to atom with
root $\mathit{root}(p(\bm{t}))=\mathit{root}(\gamma)$. Thus the premises of  U
are necessarily quasi- I-reducible.

###### Corollary 5.12

There is at most one application of  U along a path containing no  I-reducible
sequent.

###### Proof 5.13

The result follows immediately from Propositions 5.8 and 5.10.

We eventually derive (Lemma 5.15) the result concerning the length of the
I-free paths. To this aim we first introduce a new notation:

###### Definition 5.14

For every sequent ${\cal S}=\lambda\vdash_{\mathfrak{R}}^{V}\gamma$, we denote
by $\mathtt{NbDisEq}({\cal S})$ the number of disequations $x\not\approx y$
not occurring in $\lambda$ such that $x,y\in\mathcal{V}({\cal S})$.

###### Lemma 5.15

The length of every  I-free path from ${\cal S}$ is at most $O(|{\cal
S}|^{2})$.

###### Proof 5.16

By Corollary 5.12, an  I-free path contains at most one application of  U.
Rule  R applies at most $\mathit{card}(\mathcal{V}({\cal S})^{2})$ times, with
highest priority, yielding an equality-free sequent, and afterward  R can no
longer be applied, since no inference rules introduce any equality to a
sequent. Thus it is sufficient to prove the result for  I-free paths
containing no application of rules  R or  U. Let ${\cal S}_{1},\dots,{\cal
S}_{n}$ be a path with no application of  R,  U or  I, where ${\cal
S}_{1}={\cal S}$. Let ${\cal
S}_{i}=\phi_{i}\curlywedge\xi_{i}\vdash_{\mathfrak{R}}^{V_{i}}\psi_{i}\curlywedge\zeta_{i}$.
An inspection of the rules shows that we have $5\cdot\mathtt{NbDisEq}({\cal
S}_{i})+|{\cal S}_{i}|>5\cdot\mathtt{NbDisEq}({\cal S}_{i+1})+|{\cal
S}_{i+1}|$, for all $i=1,\dots,n$. Indeed, none of the considered rules can
add new variables to ${\cal S}_{i}$ by Proposition 4.23 (4) and Condition 4 of
Definition 4.43, all the rules (except possibly  C) decrease $|{\cal S}_{i}|$
and  W cannot remove disequations between variables occurring in predicate
atoms. Rule  C may add a disequation $x\not\approx y$ in ${\cal S}_{i+1}$
(increasing the size by $4=|*x\not\approx y|$), but simultaneously removes the
disequation $x\not\approx y$ from $\mathtt{NbDisEq}({\cal S}_{i+1})$. Then the
proof follows from the fact that $5\cdot\mathtt{NbDisEq}({\cal S}_{1})+|{\cal
S}_{1}|=O(|{\cal S}_{1}|^{2})$.

To derive the result about the total number of  I-free descendants, knowing
the length of the paths is of course not sufficient: it is also necessary to
estimate the number of such paths, which depends in particular on the number
of applications of rule  C. To this purpose, we prove the following result:

###### Lemma 5.17

Let ${\cal S}$ be a sequent, with $\mathit{card}({\cal V}^{\star}({\cal
S}))=\kappa$. The recursive application of  C on ${\cal S}$ yields at most
$\kappa\cdot\mathtt{NbDisEq}({\cal S})^{\kappa}$ different branches.

###### Proof 5.18

The proof is by induction on the pair $(\kappa,\mathtt{NbDisEq}({\cal S}))$.
By definition, every application of  C on ${\cal S}$ yields two sequents
${\cal S}_{1}$ and ${\cal S}_{2}$, where ${\cal S}_{1}$ is obtained from
${\cal S}$ by replacing a variable $x$ by $y$ and ${\cal S}_{2}$ is obtained
by adding the disequation $x\not\approx y$. By the application condition of
the rule (Definition 4.43, Condition 4) necessarily $y\in{\cal
V}^{\star}({\cal S})$. Since $x$ is replaced by $y$ and $x$ is the root of an
atom from the left-hand side of ${\cal S}$, we must have $y\not\in{\cal
V}^{\star}({\cal S}_{1})$, thus $\mathit{card}({\cal V}^{\star}({\cal
S}_{1}))=\kappa-1$. Now $\mathtt{NbDisEq}({\cal
S}_{1})\leq\mathtt{NbDisEq}({\cal S})$, $\mathtt{NbDisEq}({\cal
S}_{2})=\mathtt{NbDisEq}({\cal S})-1$ (since by Definition 4.43, Condition 4,
$x,y\in\mathcal{V}({\cal S})$ and $x\not\approx y$ does not occur in ${\cal
S}$) and ${\cal V}^{\star}({\cal S}_{2})={\cal V}^{\star}({\cal S})$, hence
$\mathit{card}({\cal V}^{\star}({\cal S}_{2}))=\kappa$. By the induction
hypothesis, the application of  C generates at most
$(\kappa-1)\cdot\mathtt{NbDisEq}({\cal
S}_{1})^{\kappa-1}\leq\kappa\cdot\mathtt{NbDisEq}({\cal S})^{\kappa-1}$
branches on ${\cal S}_{1}$ and $\kappa\cdot(\mathtt{NbDisEq}({\cal
S})-1)^{\kappa}\leq\kappa\cdot\mathtt{NbDisEq}({\cal
S})^{\kappa-1}\cdot(\mathtt{NbDisEq}({\cal
S})-1)=\kappa\cdot\mathtt{NbDisEq}({\cal
S})^{\kappa}-\kappa\cdot\mathtt{NbDisEq}({\cal S})^{\kappa-1}$ branches on
${\cal S}_{2}$. Thus the total number of branches is at most
$\kappa\cdot\mathtt{NbDisEq}({\cal S})^{\kappa}$.

###### Lemma 5.19

Assume that $\mathit{width}(\mathfrak{R})\leq\kappa$, for some fixed
$\kappa\in{\mathbb{N}}$ (i.e., that both the maximal arity of the symbols and
the number of record fields are bounded by $\kappa$). The number of  I-free
descendants of any sequent ${\cal S}$ is polynomial w.r.t. $|{\cal
S}|+|\mathfrak{R}|$ (but it is exponential w.r.t. $\kappa$).

###### Proof 5.20

By Lemma 5.15, it is sufficient to prove that the total number of paths
occurring in a proof tree with no application of  I is polynomial w.r.t.
$|{\cal S}|+|\mathfrak{R}|$.

The rules  R,  W,  V,  E apply with the highest priority and yield only one
branch, yielding a (unique) sequent
$\phi\curlywedge\xi\vdash\psi\curlywedge\zeta$. If $\zeta\not=\top$, then by
Definition 4.43, no other rule can be applied because these other rules apply
only when the right-hand side is of the form $\psi\curlywedge\top$. Otherwise,
the rule  S may apply (possibly several times), and eventually transforms the
sequent into sequents
$\phi_{i}\curlywedge\xi_{i}\vdash_{\mathfrak{R}}^{V_{i}}\psi_{i}\curlywedge\top$,
where each $\psi_{i}$ is a predicate atom,
$\phi=\scaleobj{1.5}{*}_{i=1}^{n}\phi_{i}$ and
$\psi=\scaleobj{1.5}{*}_{i=1}^{n}\psi_{i}$ (we may have $\xi_{i}\not=\xi$
since the rule may interleaved with applications of rule  W).

If the considered sequent is not narrow, then by definition of the strategy
(Condition 7 in Definition 4.43), there is at most one application of rule  S;
indeed, if several rule applications are possible then only the one that is
selected is considered. We thus obtain at most $|{\cal S}|$ branches, each
ending with a narrow sequent (because $\psi_{i}$ is a predicate atom, thus
$\phi_{i}\curlywedge\xi_{i}\vdash_{\mathfrak{R}}^{V_{i}}\psi_{i}$ is
necessarily narrow).

Now assume that ${\cal S}$ is narrow and let $x_{i}$ be the root of
$\psi_{i}$. We have $\mathit{alloc}(\psi_{i})=\\{x_{i}\\}$, because $\psi_{i}$
is a predicate atom. Since
$\phi_{i}*\xi_{i}\vdash_{\mathfrak{R}}^{V_{i}}\psi_{i}$ is not an axiom, we
have $x_{i}\in\mathit{alloc}(\phi_{i})$. By definition of rule  S, this
entails that $x_{i}\in V_{j}$, for all $j\in\\{1,\dots,i-1,i+1,\dots,n\\}$.
For  S to be applied, it is only necessary to choose how to decompose the
formula $\phi$ into $\scaleobj{1.5}{*}_{i=1}^{n}\phi_{i}$. To this aim, we
only have to associate each atom in $\phi$ with a formula $\phi_{i}$, hence to
associate each variable $y\in\mathit{alloc}(\phi)$ (that are by definition the
roots of the spatial atoms in $\phi$) to an index $i=1,\dots,n$. By
definition, the variable $x_{i}$ must be associated with index $i$, as
otherwise we would have $x_{i}\not\in\mathit{alloc}(\phi_{i})$ and the premise
$\phi_{i}*\xi_{i}\vdash_{\mathfrak{R}}^{V_{i}}\psi_{i}$ would be an anti-
axiom. We then arbitrarily choose the image of each variable occurring in
${\cal V}^{\dagger}({\cal S})$. Afterward, the image of the other variables
are fixed inductively as follows. Let $y\in\mathit{alloc}(\phi)$ and assume
that $y\not\in{\cal V}^{\dagger}({\cal S})\cup\\{x_{1},\dots,x_{n}\\}$. If $y$
occurs in some atom with root $y^{\prime}$ in $\phi$ and $y^{\prime}$ has
already been associated with $i$, then we also associate $y$ with $i$. For the
sake of contradiction, assume that $y$ is associated with an index $j\not=i$.
By definition of rule  S, this entails that $y\in V_{i}$, and since
$\phi_{i}*\xi_{i}\vdash_{\mathfrak{R}}^{V_{i}}\psi_{i}$ is not an anti-axiom,
we deduce that $y\in\mathcal{V}(\psi_{i})$, hence
$y\in\mathcal{V}(\psi)\setminus(\mathit{alloc}(\psi)\cup V)={\cal
V}^{\dagger}({\cal S})$, which contradicts our assumption (we cannot have
$y\in V$ since ${\cal S}$ would then be an axiom). Note that, for all
variables $y\in\mathit{alloc}(\phi)\setminus\\{x_{1},\dots,x_{n}\\}$, we have
$x_{i}\rightarrow_{\phi}^{*}y$, for some $i=1,\dots,n$, because otherwise
${\cal S}$ would be an anti-axiom. Hence all such variables $y$ must be
eventually associated with some indice $i=1,\dots,n$. Since ${\cal S}$ is
narrow, $\mathit{card}({\cal V}^{\dagger}({\cal S}))\leq\kappa$. Consequently,
there exist at most $|{\cal S}|^{\kappa}$ possible applications of rule  S,
each yielding $n\leq|{\cal S}|$ branches. We thus get a total of at most
$|{\cal S}|^{\kappa+1}$ branches.

Afterwards, rule  U applies, yielding at most $|\mathfrak{R}|$ premises in
each branch. Then  C applies on each leaf sequent ${\cal S}^{\prime}$, and by
Lemma 5.17 we get at most $|\mathfrak{R}|\cdot\mathtt{NbDisEq}({\cal
S}^{\prime})^{\kappa}$ branches. The variables in ${\cal S}^{\prime}$ either
occur in ${\cal S}$ or are introduced by the rule  U. Since each application
of  U introduces at most $\mathit{record}_{\mathit{max}}(\mathfrak{R})$
variables, we get $\mathtt{NbDisEq}({\cal S}^{\prime})\leq(|{\cal
S}|+\mathit{record}_{\mathit{max}}(\mathfrak{R}))^{2}$.

We derive the main result of this section:

###### Theorem 5.21

The root sequent of every (possibly infinite) fully expanded proof tree is
valid.

###### Proof 5.22

Let ${\cal S}$ be a non-valid sequent, with a counter-model
$(\mathfrak{s},\mathfrak{h})$. By Lemma 4.32, ${\cal S}$ is not an axiom,
hence by definition of a fully expanded proof tree, it admits successors. By
Lemmata 4.26 and 4.29, one of these successors must be non-valid and must
admit a counter-model $(\mathfrak{s},\mathfrak{h}^{\prime})$, with
$\mathit{card}(\mathfrak{h}^{\prime})\leq\mathit{card}(\mathfrak{h})$, and if
the rule that applies on ${\cal S}$ is  S, then
$\mathit{card}(\mathfrak{h}^{\prime})<\mathit{card}(\mathfrak{h})$. Starting
from the root of the tree, we thus obtain (if this root is not valid) an
infinite path ${\cal S}_{0},\dots,{\cal S}_{n},\dots,$ such that all the
${\cal S}_{i}$ admit a counter-model $(\mathfrak{s}_{i},\mathfrak{h}_{i})$,
$\mathit{card}(\mathfrak{h}_{i+1})\leq\mathit{card}(\mathfrak{h}_{i})$ and if
S is applies on ${\cal S}_{i}$ then
$\mathit{card}(\mathfrak{h}_{i+1})<\mathit{card}(\mathfrak{h}_{i})$. Since
$\mathit{card}(\mathfrak{h})$ is finite this entails that there exists $i\geq
0$ such that rule  S does not apply on ${\cal S}_{j}$, for all $j\geq i$. By
Lemma 5.2, this entails that there exists $k$ such that  I does not apply on
${\cal S}_{j}$, for all $j\geq k$. Thus ${\cal S}_{k}$ admits an infinite
number of  I-free descendants, which contradicts Lemma 5.19.

###  5.2 Completeness

We now establish completeness, i.e., we prove that every valid sequent admits
a fully expanded tree. To this aim, we prove that for every valid sequent,
there exists a rule application yielding valid premises. Lemma 5.32 handles
the case of rule  S, and Lemma 5.34 handles all the other rules. We begin by
establishing several preliminary results. First, we note that the truth value
of a formula in a structure is not dependent on the names of the locations:
these locations can be freely renamed, provided the relations between the
variables are preserved, and provided allocated locations are not mapped to
the same image. This result will be useful to construct copies of models when
needed in forthcoming proofs. More formally, we introduce a notion of a
$\mathfrak{U}$-mapping and state some conditions ensuring that the application
of such $\mathfrak{U}$-mappings on a structure preserves the truth value of a
formula.

###### Definition 5.23

A $\mathfrak{U}$-mapping is a function $\nu$ mapping every element of
$\mathfrak{U}_{\mathtt{s}}$ to an element of $\mathfrak{U}_{{\mathtt{s}}}$.
Let $\mathfrak{h}$ be a heap. If $\nu$ is injective on
$\mathit{dom}(\mathfrak{h})$, then we denote by $\nu(\mathfrak{h})$ the heap
with domain $\nu(\mathit{dom}(\mathfrak{h}))$, such that for all
$\ell_{0}\in\mathit{dom}(\mathfrak{h})$, with
$\mathfrak{h}(\ell_{0})=(\ell_{1},\dots,\ell_{n})$, we have
$\nu(\mathfrak{h})(\nu(\ell_{0}))=(\nu(\ell_{1}),\dots,\nu(\ell_{n}))$.

###### Lemma 5.24

Let $\lambda$ be a symbolic heap, let $(\mathfrak{s},\mathfrak{h})$ be an
$\mathfrak{R}$-model of $\lambda$ and let $\nu$ be a $\mathfrak{U}$-mapping
that is injective on
$\mathfrak{s}(\mathcal{V}(\lambda))\cup\mathit{dom}(\mathfrak{h})$. Then
$(\nu\circ\mathfrak{s},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\lambda$.

###### Proof 5.25

The proof is by induction on the satisfiability relation. The result is
established also for spatial formulas and pure formulas.

  * •

If $\lambda$ is an equation $x\approx y$, then
$\mathfrak{s}(x)=\mathfrak{s}(y)$, hence
$\nu(\mathfrak{s}(x))=\nu(\mathfrak{s}(y))$ and
$(\nu\circ\mathfrak{s},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\lambda$.

  * •

If $\lambda$ is a disequation $x\not\approx y$, then
$\mathfrak{s}(x)\not=\mathfrak{s}(y)$, and since $\nu$ is injective on
$\mathfrak{s}(\mathcal{V}(\lambda))$ we get
$\nu(\mathfrak{s}(x))\not=\nu(\mathfrak{s}(y))$ and
$(\nu\circ\mathfrak{s},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\lambda$.

  * •

If $\lambda=y_{0}\mapsto(y_{1},\dots,y_{n})$ then we must have
$\mathfrak{h}=\\{(\mathfrak{s}(y_{0}),\dots,\mathfrak{s}(y_{n}))\\}$, which
entails that $\nu(\mathfrak{h})$ is
${\\{(\nu(\mathfrak{s}(y_{0})),\dots,\nu(\mathfrak{s}(y_{n})))\\}}$ and that
$(\nu\circ\mathfrak{s},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\lambda$.

  * •

If $\lambda=\phi\curlywedge\xi$ (or $\lambda=\phi\wedge\xi$) then we have
$(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\phi$ and
$(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\xi$. By the induction
hypothesis, we get
$(\nu\circ\mathfrak{s},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\phi$ and
$(\nu\circ\mathfrak{s},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\xi$, thus
$(\nu\circ\mathfrak{s},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\lambda$.

  * •

If $\lambda=\phi_{1}*\phi_{2}$ then there exists disjoint heaps
$\mathfrak{h}_{i}$ (for $i=1,2$) such that
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$ and
$(\mathfrak{s},\mathfrak{h}_{i})\models_{\mathfrak{R}}\phi_{i}$. Since
$\mathfrak{s}(\mathcal{V}(\phi_{i}))\cup\mathit{dom}(\mathfrak{h}_{i})\subseteq\mathfrak{s}(\mathcal{V}(\lambda))\cup\mathit{dom}(\mathfrak{h})$,
by the induction hypothesis we have
$(\nu\circ\mathfrak{s},\nu(\mathfrak{h}_{i}))\models_{\mathfrak{R}}\phi_{i}$
(for $i=1,2$). But $\nu(\mathfrak{h}_{1})$ and $\nu(\mathfrak{h}_{2})$ must be
disjoint since
$\mathit{dom}(\mathfrak{h}_{1})\cap\mathit{dom}(\mathfrak{h}_{2})=\emptyset$
and $\nu$ is injective, therefore
$(\nu\circ\mathfrak{s},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\lambda$.

  * •

If $\lambda$ is a predicate atom, then we have
$\lambda\Leftarrow_{\mathfrak{R}}\gamma$ and
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{\mathfrak{R}}\gamma$, for some
associate $\mathfrak{s}^{\prime}$ of $\mathfrak{s}$ w.r.t.
$\mathcal{V}(\gamma)\setminus\mathcal{V}(\lambda)$. Since the rules in
$\mathfrak{R}$ are $\mathtt{P}$-rules, for all variables
$x\in\mathcal{V}(\gamma)\setminus\mathcal{V}(\lambda)$, we have
$x\in\mathit{alloc}(\gamma)$ thus
$\mathfrak{s}^{\prime}(x)\in\mathit{dom}(\mathfrak{h})$ by Lemma 4.2. This
entails that $\nu$ is injective on
$\mathfrak{s}^{\prime}(\mathcal{V}(\gamma))\cup\mathit{dom}(\mathfrak{h})$,
and by the induction hypothesis we get
$(\nu\circ\mathfrak{s}^{\prime},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\xi$.
Moreover, it is clear that $\nu(\mathfrak{s}^{\prime})$ is an associate of
$\nu(\mathfrak{s})$ w.r.t. $\mathcal{V}(\gamma)\setminus\mathcal{V}(\lambda)$,
thus $(\nu\circ\mathfrak{s},\nu(\mathfrak{h}))\models_{\mathfrak{R}}\lambda$.

This result entails that for every set $U$ that is sufficiently large,
counter-models may always be renamed, so that all locations occur in $U$:

###### Corollary 5.26

Let $U$ be an infinite subset of $\mathfrak{U}_{{\mathtt{s}}}$. Any non-valid
and equality-free sequent $\lambda\vdash_{\mathfrak{R}}^{V}\gamma$ admits a
counter-model $(\mathfrak{s},\mathfrak{h})$ such that
$\mathit{dom}(\mathfrak{h})\cup\mathfrak{s}(\mathcal{V}_{\mathtt{loc}})\subseteq
U$.

###### Proof 5.27

It suffices to consider any counter-model of $\gamma$ and apply a bijective
$\mathfrak{U}$-mapping (or any $\mathfrak{U}$-mapping that is injective on
$\mathfrak{s}(\mathcal{V}(\lambda))\cup\mathit{dom}(\mathfrak{h})$) that maps
all locations $\ell\in\mathfrak{U}_{\mathtt{loc}}$ to an element in $U$.

The first step toward establishing completeness is to show that rule  S always
applies (on a valid sequent) if the right-hand side of the sequent contains
several spatial formulas (assuming that the rules of higher priority do not
apply). This is essential because the strategy in Definition 4.43 forbids the
application of the other rules in this case. The difficulty is that, of
course,  S cannot be applied arbitrarily: we are required to obtain valid
premises. To this purpose we show that the heap decomposition of the left-hand
side ($\phi_{1}*\phi_{2}$) matches that of the right-hand side
($\psi_{1}*\psi_{2}$). This will be proven thanks to the next lemma.
Intuitively, this lemmas states that, under some additional conditions, if a
structure $(\mathfrak{s},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})$ validates a
formula $\phi_{1}*\phi_{2}$, then we may deduce that each structure
$(\mathfrak{s},\mathfrak{h}_{i})$ validates $\phi_{i}$, when all the variables
allocated by $\phi_{i}$ are in the domain of $\mathfrak{h}_{i}$.

###### Lemma 5.28

Let $\phi_{i},\psi_{i}$ (for $i=1,2$) be spatial formulas, with
$\mathit{alloc}(\psi_{1}*\psi_{2})\subseteq\mathit{alloc}(\phi_{1}*\phi_{2})$.
Let $\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ be disjoint heaps such that
$(\mathfrak{s},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})\models_{\mathfrak{R}}\phi_{1}*\phi_{2}$
and $(\mathfrak{s},\mathfrak{h}_{i})\models_{\mathfrak{R}}\psi_{i}$, for
$i=1,2$. If
$(\mathit{dom}(\mathfrak{h}_{1})\cup\mathit{dom}(\mathfrak{h}_{2}))\cap\mathfrak{s}(\mathcal{V})\subseteq\mathfrak{s}(\mathit{alloc}(\phi_{1}*\phi_{2}))$
and
$\mathfrak{s}(\mathit{alloc}(\phi_{i}))\subseteq\mathit{dom}(\mathfrak{h}_{i})$
for $i=1,2$, then
$(\mathfrak{s},\mathfrak{h}_{i})\models_{\mathfrak{R}}\phi_{i}$, for $i=1,2$.

###### Proof 5.29

By definition, since
$(\mathfrak{s},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})\models_{\mathfrak{R}}\phi_{1}*\phi_{2}$,
there exist disjoint heaps
$\widehat{\mathfrak{h}}_{1},\widehat{\mathfrak{h}}_{2}$ such that
$(\mathfrak{s},\widehat{\mathfrak{h}}_{i})\models_{\mathfrak{R}}\phi_{i}$, for
all $i=1,2$, and
$\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}=\widehat{\mathfrak{h}}_{1}\uplus\widehat{\mathfrak{h}}_{2}$.
We prove that $\widehat{\mathfrak{h}}_{i}=\mathfrak{h}_{i}$ for $i=1,2$. Since
$\widehat{\mathfrak{h}}_{1}\uplus\widehat{\mathfrak{h}}_{2}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$
and $\widehat{\mathfrak{h}}_{1}$ and $\widehat{\mathfrak{h}}_{2}$ are
disjoint, it is sufficient to prove that
$\mathit{dom}(\mathfrak{h}_{i})\subseteq\mathit{dom}(\widehat{\mathfrak{h}}_{i})$,
for $i=1,2$. By symmetry, we prove the result for $i=1$. Assume, for the sake
of contradiction, that $\ell\in\mathit{dom}(\mathfrak{h}_{1})$ and
$\ell\not\in\mathit{dom}(\widehat{\mathfrak{h}}_{1})$. By Proposition 4.9,
since $(\mathfrak{s},\mathfrak{h}_{1})\models_{\mathfrak{R}}\psi_{1}$ and
$\ell\in\mathit{dom}(\mathfrak{h}_{1})\subseteq\mathit{ref}(\mathfrak{h}_{1})$,
there exists $y\in\mathit{alloc}(\psi_{1})$ such that
$\mathfrak{s}(y)\rightarrow_{\mathfrak{h}_{1}}^{*}\ell$, thus there is a
sequence of locations $\ell_{0},\dots,\ell_{n}$ with
$\ell_{0}=\mathfrak{s}(y)$, $\ell=\ell_{n}$ and
$\ell_{i}\rightarrow_{\mathfrak{h}_{1}}\ell_{i+1}$, for all $i=0,\dots,n-1$.
Let $k$ be the smallest index such that
$\ell_{k}\not\in\mathit{dom}(\widehat{\mathfrak{h}}_{1})$. Note that
$\ell_{i}\in\mathit{dom}(\mathfrak{h}_{1})$, for all $i\leq k$ and that
$y\in\mathit{alloc}(\phi_{1})$. Indeed,
$y\in\mathit{alloc}(\psi_{1})\subseteq\mathit{alloc}(\phi_{1})\cup\mathit{alloc}(\phi_{2})$
by the hypothesis of the lemma, and if $y\in\mathit{alloc}(\phi_{2})$, then we
get (again by the hypothesis of the lemma)
$\mathfrak{s}(y)\in\mathit{dom}(\mathfrak{h}_{2})$, which contradicts the fact
that $\ell_{0}=\mathfrak{s}(y)\in\mathit{dom}(\mathfrak{h}_{1})$, as
$\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ are disjoint. By Lemma 4.2, we
deduce that
$\ell_{0}=\mathfrak{s}(y)\in\mathit{dom}(\widehat{\mathfrak{h}}_{1})$ since
$y\in\mathit{alloc}(\phi_{1})$ and
$(\mathfrak{s},\widehat{\mathfrak{h}}_{1})\models_{\mathfrak{R}}\phi_{1}$.
Thus $k>0$, and necessarily
$\ell_{k}\in\mathit{ref}(\widehat{\mathfrak{h}}_{1})$ (since
$\ell_{k-1}\in\mathit{dom}(\widehat{\mathfrak{h}}_{1})$, by minimality of
$k$). We deduce that
$\ell_{k}\in\mathit{ref}(\widehat{\mathfrak{h}}_{1})\setminus\mathit{dom}(\widehat{\mathfrak{h}}_{1})$.
By Lemma 4.11, this entails that $\ell_{k}=\mathfrak{s}(x)$ for some
$x\in\mathcal{V}(\phi_{1})$, as
$(\mathfrak{s},\widehat{\mathfrak{h}}_{1})\models\phi_{1}$. By the hypothesis
of the lemma, we may assume that $x\in\mathit{alloc}(\phi_{1}*\phi_{2})$,
since $\ell_{k}\in\mathit{dom}(\mathfrak{h}_{1})$ and
$(\mathit{dom}(\mathfrak{h}_{1})\cup\mathit{dom}(\mathfrak{h}_{2}))\cap\mathfrak{s}(\mathcal{V})\subseteq\mathfrak{s}(\mathit{alloc}(\phi_{1}*\phi_{2}))$.
However, we cannot have $x\in\mathit{alloc}(\phi_{1})$ because otherwise we
would have $\mathfrak{s}(x)\in\mathit{dom}(\widehat{\mathfrak{h}}_{1})$ by
Lemma 4.2, as
$(\mathfrak{s},\widehat{\mathfrak{h}}_{1})\models_{\mathfrak{R}}\phi_{1}$. We
cannot have $x\in\mathit{alloc}(\phi_{2})$ either, since otherwise we would
have $\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{2})$, as
$\mathfrak{s}(\mathit{alloc}(\phi_{2}))\subseteq\mathit{dom}(\mathfrak{h}_{2})$
by the hypothesis of the lemma, hence
$\mathfrak{s}(x)\not\in\mathit{dom}(\mathfrak{h}_{1})$ because
$\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ are disjoint. Thus we obtain a
contradiction.

We then derive the result about rule  S. The main issue is that we have to
take into account the fact that the strategy “blocks” some applications of  S,
if the sequent is not narrow (see Condition 5 in Definition 4.43). We show
that blocked applications do not yield valid premises. To illustrate the
difficulties that arise when applying  S, we provide the examples below. The
first one illustrates the importance of the fact that each predicate allocates
at most one parameter.

###### Example 5.30

Consider the sequent $p(x,y)\vdash_{\mathfrak{R}}^{\emptyset}q(x,y)*r(y)$,
with the rules:

$p(x,y)$ | $\Leftarrow$ | $x\mapsto(y)*p^{\prime}(y)$ |  | $q(x,y)$ | $\Leftarrow$ | $x\mapsto(y)$
---|---|---|---|---|---|---
$p^{\prime}(y)$ | $\Leftarrow$ | $y\mapsto()$ |  | $r(y)$ | $\Leftarrow$ | $y\mapsto()$

Note that the rules of $p$ are not $\mathtt{P}$-rules, as both $x$ and $y$ are
allocated by $p(x,y)$. Here, although the sequent is indeed valid, no
application of  S yields valid premises: to show that the sequent is valid,
one has first to unfold $p(x,y)$ once, before applying  S. In our context,
such a situation cannot arise as each predicate atom allocates only one of its
parameters, namely its root. As we shall see, this entails that every
decomposition of the right-hand side of the sequent necessarily corresponds to
some (purely syntactic) decomposition of the left-hand side.

The next example illustrates the importance of determinism.

###### Example 5.31

Consider the sequent ${\cal
S}:p(x,y)*q(y)*p(z,y)\vdash_{\mathfrak{R}}^{\emptyset}p^{\prime}(x,y)*q^{\prime}(z,y)$,
with the rules:

$p(x,y)$ | $\Leftarrow$ | $x\mapsto(y)$ | $q(y)$ | $\Leftarrow$ | $y\mapsto(z)*q(z)$
---|---|---|---|---|---
$q(y)$ | $\Leftarrow$ | $y\mapsto()$ | $q(y)$ | $\Leftarrow$ | $y\mapsto(y)$
$p^{\prime}(x,y)$ | $\Leftarrow$ | $x\mapsto(z)*p^{\prime}(z,y)$ | $q^{\prime}(x,y)$ | $\Leftarrow$ | $x\mapsto(z)*q^{\prime}(z,y)$
$p^{\prime}(x,y)$ | $\Leftarrow$ | $x\mapsto(y)$ | $q^{\prime}(x,y)$ | $\Leftarrow$ | $x\mapsto(y)$
$p^{\prime}(x,y)$ | $\Leftarrow$ | $x\mapsto()$ | $q^{\prime}(x,y)$ | $\Leftarrow$ | $x\mapsto(x)$

Intuitively, $q(y)$ denotes a list starting at $y$ and ending either with an
empty tuple or with a loop on its last element, whereas $p^{\prime}(x,y)$
(resp. $q^{\prime}(x,y)$) denotes a list starting at $x$ and ending either
with $y$ or with an empty tuple (resp. with a loop on the last element). These
rules are not deterministic (for instance there is an overlap between the
rules $p^{\prime}(x,y)\Leftarrow x\mapsto(z)*p^{\prime}(z,y)$ and
$p^{\prime}(x,y)\Leftarrow x\mapsto(y)$). Although the sequent ${\cal S}$ is
valid, there is no application of  S that yields valid premises. Indeed, none
of the sequents $p(x,y)*q(y)\vdash_{\mathfrak{R}}^{\emptyset}p^{\prime}(x,y)$,
or $q(y)*p(z,y)\vdash_{\mathfrak{R}}^{\emptyset}q^{\prime}(z,y)$ are valid.
Here  S cannot be applied before the entire list $q(y)$ is unfolded, as the
decision to group $q(y)$ with $p(x,y)$ or $p(y,z)$ cannot be made before the
last cell in $q(y)$ is known. This would yield an infinite proof tree (with
infinitely many branches). The fact that the rules are deterministic prevents
such a behavior to occur.

###### Lemma 5.32

Let ${\cal
S}:\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}(\psi_{1}*\psi_{2})\curlywedge\top$
be a valid sequent where $\psi_{i}\not=\mathit{emp}$ for $i=1,2$ and $\xi$ is
a conjunction of disequations. If ${\cal S}$ is not an axiom, then there
exists an application of  S with conclusion ${\cal S}$ for which all the
premises are valid.

###### Proof 5.33

To prove that  S applies on ${\cal S}$, it is necessary to show that $\phi$ is
of the form $\phi_{1}*\phi_{2}$. However $\phi_{i}$ cannot be chosen
arbitrarily, since the premises have to be valid. To construct $\phi_{i}$, we
shall construct a model of $\phi$ of a particular form, get a decomposition of
the heap of this model from the formula $\psi_{1}*\psi_{2}$ on the right-hand
side of the sequent, and use this decomposition to compute suitable formulas
$\phi_{1}$ and $\phi_{2}$. We first notice that, since ${\cal S}$ is not an
axiom, $\phi$ must be heap-satisfiable. Furthermore, since ${\cal S}$ is
valid, it cannot be an anti-axiom by Lemma 4.38, thus
$\mathit{alloc}(\psi_{i})\subseteq\mathit{alloc}(\phi)$ for $i=1,2$. Since
$\psi_{i}\not=\mathit{emp}$, this entails that $\mathit{alloc}(\phi)$ is not
empty. Let $U_{1},U_{2}$ be disjoint infinite subsets of
$\mathfrak{U}_{\mathtt{loc}}$ and let $\mathfrak{s}$ be an injective store
such that $\mathfrak{s}(\mathcal{V})\cap U_{i}=\emptyset$, for $i=1,2$. Note
that such $U_{1},U_{2}$ and $\mathfrak{s}$ exist since
$\mathfrak{U}_{{\mathtt{s}}}$ is infinite, for all
${\mathtt{s}}\in\mathfrak{S}$. By Lemma 4.36 applied with $U=U_{1}$ and with
any variable $x\in\mathit{alloc}(\phi)$, there exists an $\mathfrak{R}$-model
$(\mathfrak{s},\mathfrak{h})$ of $\phi$ such that
$\mathit{dom}(\mathfrak{h})\subseteq
U_{1}\cup\mathfrak{s}(\mathit{alloc}(\phi))$. Since $\mathfrak{s}$ is
injective and $\xi$ is a conjunction of disequations, necessarily
$\mathfrak{s}\models\xi$ (observe that $\xi$ contains no disequation of the
form $u\not\approx u$ as otherwise ${\cal S}$ would be an axiom). If there
exists $x\in V$ such that $\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h})$, then
since $\mathit{dom}(\mathfrak{h})\subseteq
U_{1}\cup\mathfrak{s}(\mathit{alloc}(\phi))$ and
$\mathfrak{s}(\mathcal{V})\cap U_{1}=\emptyset$, there must exist
$x^{\prime}\in\mathit{alloc}(\phi)$ such that
$\mathfrak{s}(x)=\mathfrak{s}(x^{\prime})$. Since $\mathfrak{s}$ is injective,
necessarily $x=x^{\prime}$, which entails that ${\cal S}$ is an axiom,
contradicting the hypotheses of the lemma. We deduce that
$\mathfrak{s}(V)\cap\mathit{dom}(\mathfrak{h})=\emptyset$. Since
$\mathfrak{s}$ is injective, it is injective on $V$, as otherwise $V$ would
contain two occurrences of the same variable and ${\cal S}$ would be an axiom.
Because ${\cal S}$ is valid, we deduce that
$(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}(\psi_{1}*\psi_{2})$, hence
there exist disjoint heaps $\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ such that
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$ and
$(\mathfrak{s},\mathfrak{h}_{i})\models_{\mathfrak{R}}\psi_{i}$, for $i=1,2$.
Let $\phi_{i}$ be the separating conjunction of all the spatial atoms $\alpha$
occurring in $\phi$ such that
$\mathfrak{s}(\mathit{alloc}(\alpha))\subseteq\mathit{dom}(\mathfrak{h}_{i})$.
By Lemma 4.2,
$\mathfrak{s}(\mathit{alloc}(\phi))\subseteq\mathit{dom}(\mathfrak{h})=\mathit{dom}(\mathfrak{h}_{1})\cup\mathit{dom}(\mathfrak{h}_{2})$,
hence every atom $\alpha$ occurs in either $\phi_{1}$ or $\phi_{2}$, and since
$\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ are disjoint, no atom $\alpha$ can
occur both in $\phi_{1}$ and $\phi_{2}$. Therefore, $\phi=\phi_{1}*\phi_{2}$.

We now prove that
$(\mathfrak{s},\mathfrak{h}_{i})\models_{\mathfrak{R}}\phi_{i}$ for $i=1,2$.
To this aim we use Lemma 5.28, thus we verify that all the hypotheses of the
lemma are satisfied. Since $\mathit{dom}(\mathfrak{h})\subseteq
U_{1}\cup\mathfrak{s}(\mathit{alloc}(\phi))$ and
$U_{1}\cap\mathfrak{s}(\mathcal{V})=\emptyset$, we have
$\mathit{dom}(\mathfrak{h})\cap\mathfrak{s}(\mathcal{V})\subseteq\mathfrak{s}(\mathit{alloc}(\phi))$,
i.e.
$(\mathit{dom}(\mathfrak{h}_{1})\cup\mathit{dom}(\mathfrak{h}_{2}))\cap\mathfrak{s}(\mathcal{V})=\mathfrak{s}(\mathit{alloc}(\phi_{1}*\phi_{2}))$.
Furthermore,
$\mathfrak{s}(\mathit{alloc}(\phi_{i}))\subseteq\mathit{dom}(\mathfrak{h}_{i})$
for $i=1,2$ by definition of $\phi_{i}$,
$(\mathfrak{s},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})=(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\phi=\phi_{1}*\phi_{2}$,
$(\mathfrak{s},\mathfrak{h}_{i})\models_{\mathfrak{R}}\psi_{i}$ (for all
$i=1,2$) and
$\mathit{alloc}(\psi_{1}*\psi_{2})\subseteq\mathit{alloc}(\phi_{1}*\phi_{2})$.
By Lemma 5.28, we deduce that
$(\mathfrak{s},\mathfrak{h}_{i})\models_{\mathfrak{R}}\phi_{i}$ for $i=1,2$.

It is clear that there is an application of  S on ${\cal
S}=(\phi_{1}*\phi_{2})\curlywedge\xi\models_{\mathfrak{R}}(\psi_{1}*\psi_{2})\curlywedge\top$
yielding the premises
$\phi_{i}\curlywedge\xi\vdash_{\mathfrak{R}}^{V_{i}}\psi_{i}$ for $i=1,2$,
where $V_{i}=V\cup\mathit{alloc}(\phi_{3-i})$. There remains to prove that
these premises are valid and that the application of the rule is allowed by
the strategy. Assume that one of these premises, say
$\phi_{1}\curlywedge\xi\vdash_{\mathfrak{R}}^{V_{1}}\psi_{1}$, is not valid.
By Corollary 5.26 applied with $U=U_{2}$,
$\phi_{1}\curlywedge\xi\vdash_{\mathfrak{R}}^{V_{1}}\psi_{1}$ admits a
counter-model $(\mathfrak{s}^{\prime},\mathfrak{h}_{1}^{\prime})$, where
$\mathit{dom}(\mathfrak{h}_{1}^{\prime})\cup\mathfrak{s}^{\prime}(\mathcal{V}_{\mathtt{loc}})\subseteq
U_{2}$. By construction we have
$\mathfrak{s}^{\prime}(V_{1})\cap\mathit{dom}(\mathfrak{h}_{1}^{\prime})=\emptyset$,
thus
$\mathfrak{s}^{\prime}(V)\cap\mathit{dom}(\mathfrak{h}_{1}^{\prime})=\emptyset$
since $V\subseteq V_{1}$. Moreover, $\mathfrak{s}^{\prime}$ is injective on
$V_{1}=V\cup\mathit{alloc}(\phi_{2})$. By Lemma 4.36, $\phi_{2}$ therefore
admits a model $(\mathfrak{s}^{\prime},\mathfrak{h}_{2}^{\prime})$ with
$\mathit{dom}(\mathfrak{h}_{2}^{\prime})\subseteq
U_{1}\cup\mathfrak{s}^{\prime}(\mathit{alloc}(\phi_{2}))$. We show that
$\mathfrak{h}_{1}^{\prime}$ and $\mathfrak{h}_{2}^{\prime}$ are disjoint.
Assume for the sake of contradiction that
$\ell\in\mathit{dom}(\mathfrak{h}_{1}^{\prime})\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime})$.
Since $U_{1}\cap U_{2}=\emptyset$, we have
$\mathit{dom}(\mathfrak{h}_{1}^{\prime})\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime})\subseteq\mathfrak{s}^{\prime}(\mathit{alloc}(\phi_{2}))$,
thus $\ell\in\mathfrak{s}^{\prime}(\mathit{alloc}(\phi_{2}))$. But since
$\mathfrak{s}^{\prime}(V_{1})\cap\mathit{dom}(\mathfrak{h}_{1}^{\prime})=\emptyset$
and $\mathit{alloc}(\phi_{2})\subseteq V_{1}$ we also have
$\ell\not\in\mathfrak{s}^{\prime}(\mathit{alloc}(\phi_{2}))$, a contradiction.
Thus $\mathfrak{h}_{1}^{\prime}$ and $\mathfrak{h}_{2}^{\prime}$ are disjoint
and we have
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1}^{\prime}\uplus\mathfrak{h}_{2}^{\prime})\models_{\mathfrak{R}}(\phi_{1}*\phi_{2})\curlywedge\xi=\phi\curlywedge\xi$.
If $\mathfrak{s}^{\prime}(V)\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime})$
contains a location $\ell$ then since $U_{1}\cap U_{2}=\emptyset$, necessarily
$\ell=\mathfrak{s}^{\prime}(x)$, for some $x\in\mathit{alloc}(\phi_{2})$, and
since $\mathfrak{s}^{\prime}$ is injective on
$V_{1}=V\cup\mathit{alloc}(\phi_{2})$ and $\ell\in\mathfrak{s}^{\prime}(V)$,
necessarily, $x\in V$ and ${\cal S}$ is an axiom, which contradicts the
hypotheses of the lemma. We deduce that
$\mathfrak{s}^{\prime}(V)\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime})=\emptyset$,
and since
$\mathfrak{s}^{\prime}(V)\cap\mathit{dom}(\mathfrak{h}_{1}^{\prime})=\emptyset$,
that
$\mathfrak{s}^{\prime}(V)\cap\mathit{dom}(\mathfrak{h}_{1}^{\prime}\uplus\mathfrak{h}_{2}^{\prime})=\emptyset$.
Furthermore, by construction, $\mathfrak{s}^{\prime}$ is injective on $V$.
Since ${\cal S}$ is valid, this entails that
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1}^{\prime}\uplus\mathfrak{h}_{2}^{\prime})\models_{\mathfrak{R}}(\psi_{1}*\psi_{2})$,
hence
$\mathfrak{h}_{1}^{\prime}\uplus\mathfrak{h}_{2}^{\prime}=\mathfrak{h}_{1}^{\prime\prime}\uplus\mathfrak{h}_{2}^{\prime\prime}$,
where
$(\mathfrak{s}^{\prime},\mathfrak{h}_{i}^{\prime\prime})\models_{\mathfrak{R}}\psi_{i}$.
By Lemma 3.9, since
$(\mathfrak{s}^{\prime},\mathfrak{h}_{2}^{\prime})\models_{\mathfrak{R}}\psi_{2}$
and $\mathfrak{R}$ is deterministic, we get
$\mathfrak{h}_{2}^{\prime\prime}=\mathfrak{h}_{2}^{\prime}$, and therefore
$\mathfrak{h}_{1}^{\prime\prime}=\mathfrak{h}_{1}^{\prime}$, thus
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1}^{\prime})\models_{\mathfrak{R}}\psi_{1}$.
This contradicts the fact that
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1}^{\prime})$ is a counter-model of
$\phi_{1}\curlywedge\xi\vdash_{\mathfrak{R}}^{V_{2}}\psi_{1}$.

If ${\cal S}$ is narrow, then the proof is completed, since all the
applications of rule  S are considered by the strategy in this case. If ${\cal
S}$ is not narrow, then the application of the rule may be blocked by
Condition 7 of Definition 4.43. In this case, this means that there exist
$\phi_{1}^{\prime},\phi_{2}^{\prime}$ such that
$\phi=\phi_{1}^{\prime}*\phi_{2}^{\prime}$ and
$\phi_{1}^{\prime}\curlywedge\xi\vdash_{\mathfrak{R}}^{V_{1}^{\prime}}\psi_{1}$
is valid, where $V_{1}^{\prime}=V\cup\mathit{alloc}(\phi_{2}^{\prime})$. We
assume that the other premise,
$\phi_{2}^{\prime}\curlywedge\xi\vdash_{\mathfrak{R}}^{V_{2}^{\prime}}\psi_{2}$
(with $V_{2}^{\prime}=V\cup\mathit{alloc}(\phi_{1}^{\prime})$) is not valid,
and we derive a contradiction. By Corollary 5.26, this premise admits a
counter-model $(\mathfrak{s}^{\prime\prime},\mathfrak{h}^{\prime\prime}_{2})$
such that
$\mathit{dom}(\mathfrak{h}^{\prime\prime}_{2})\cup\mathfrak{s}^{\prime\prime}(\mathcal{V}_{\mathtt{loc}})\subseteq
U_{1}$. We have
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{2}^{\prime\prime})\models_{\mathfrak{R}}\phi_{2}^{\prime}$,
$\mathfrak{s}^{\prime\prime}\models\xi$,
$\mathfrak{s}^{\prime\prime}(V_{2}^{\prime})\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime\prime})=\emptyset$,
$\mathfrak{s}^{\prime\prime}$ is injective on $V_{2}^{\prime}$ and
$(\mathfrak{s},\mathfrak{h}_{2}^{\prime\prime})\not\models_{\mathfrak{R}}\psi_{2}$.
By Lemma 4.36, $\phi_{1}^{\prime}$ admits a model
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{1}^{\prime\prime})$ such that
$\mathit{dom}(\mathfrak{h}_{1}^{\prime\prime})\subseteq
U_{2}\cup\mathfrak{s}^{\prime\prime}(\mathit{alloc}(\phi_{1}^{\prime}))$.

Note that $\mathfrak{h}_{1}^{\prime\prime}$ and
$\mathfrak{h}_{2}^{\prime\prime}$ are disjoint: if
$\ell\in\mathit{dom}(\mathfrak{h}_{1}^{\prime\prime})\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime\prime})$
then, as ${\mathit{dom}(\mathfrak{h}_{1}^{\prime\prime})\subseteq
U_{2}\cup\mathfrak{s}^{\prime\prime}(\mathit{alloc}(\phi_{1}^{\prime}))}$ and
$\mathit{dom}(\mathfrak{h}^{\prime\prime}_{2})\cup\mathfrak{s}^{\prime\prime}(\mathcal{V}_{\mathtt{loc}})\subseteq
U_{1}$, with $U_{1}\cap U_{2}=\emptyset$, we get
$\ell\in\mathfrak{s}^{\prime\prime}(\mathit{alloc}(\phi_{1}^{\prime}))$, so
that $\ell\in\mathfrak{s}^{\prime\prime}(V_{2}^{\prime})$, contradicting the
fact that
$\mathfrak{s}^{\prime\prime}(V_{2}^{\prime})\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime\prime})=\emptyset$.

We prove that $\mathfrak{s}^{\prime\prime}$ is injective on $V_{1}^{\prime}$,
and that
$\mathit{dom}(\mathfrak{h}_{1}^{\prime\prime})\cap\mathfrak{s}^{\prime\prime}(V_{1})=\emptyset$,
which entails that
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{1}^{\prime\prime})\models_{\mathfrak{R}}\psi_{1}$,
since
$\phi_{1}^{\prime}\curlywedge\xi\vdash_{\mathfrak{R}}^{V_{1}^{\prime}}\psi_{1}$
is valid. If there exist $x_{1},x_{2}$ such that
$\\{x_{1},x_{2}\\}\subseteq_{m}V_{1}^{\prime}=V\cup\mathit{alloc}(\phi_{2}^{\prime})$
and $\mathfrak{s}^{\prime\prime}(x_{1})=\mathfrak{s}^{\prime\prime}(x_{2})$
then, as $\mathfrak{s}^{\prime\prime}$ is injective on
$V_{2}^{\prime}=V\cup\mathit{alloc}(\phi_{1}^{\prime})$, necessarily at least
one of the variables $x_{1},x_{2}$ – say $x_{1}$ – is in
$\mathit{alloc}(\phi_{2}^{\prime})$. As
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{2}^{\prime\prime})\models\phi_{2}^{\prime}$,
we get
$\mathfrak{s}^{\prime\prime}(x_{1})\in\mathit{dom}(\mathfrak{h}_{2}^{\prime\prime})$
(by Lemma 4.2), and
$\\{x_{1},x_{2}\\}\not\subseteq_{m}\mathit{alloc}(\phi_{2}^{\prime})$ (by
Corollary 4.4). This entails that
$\mathfrak{s}^{\prime\prime}(x_{1})\not\in\mathfrak{s}^{\prime\prime}(V_{2}^{\prime})$
(as
$\mathfrak{s}^{\prime\prime}(V_{2}^{\prime})\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime\prime})=\emptyset$)
and $x_{2}\in V\subseteq V_{2}^{\prime}$, yielding a contradiction, since
$\mathfrak{s}^{\prime\prime}(x_{1})=\mathfrak{s}^{\prime\prime}(x_{2})$. Now
assume that there exists $y\in
V_{1}^{\prime}=V\cup\mathit{alloc}(\phi_{2}^{\prime})$ such that
$\mathfrak{s}^{\prime\prime}(y)\in\mathit{dom}(\mathfrak{h}_{1}^{\prime\prime})$.
As $\mathit{dom}(\mathfrak{h}_{1}^{\prime\prime})\subseteq
U_{2}\cup\mathfrak{s}^{\prime\prime}(\mathit{alloc}(\phi_{1}^{\prime}))$ and
$\mathit{dom}(\mathfrak{h}^{\prime\prime}_{2})\cup\mathfrak{s}^{\prime\prime}(\mathcal{V}_{\mathtt{loc}})\subseteq
U_{1}$, we get
$\mathfrak{s}^{\prime\prime}(y)\in\mathfrak{s}^{\prime\prime}(\mathit{alloc}(\phi_{1}^{\prime}))$,
i.e., there exists $y^{\prime}\in\mathit{alloc}(\phi_{1}^{\prime})$ such that
$\mathfrak{s}^{\prime\prime}(y)=\mathfrak{s}^{\prime\prime}(y^{\prime})$. If
$y\in V$, then $\\{y,y^{\prime}\\}\subseteq_{m}V_{2}^{\prime}$, contradicting
the fact that $\mathfrak{s}^{\prime\prime}$ is injective on $V_{2}^{\prime}$.
Thus $y\in\mathit{alloc}(\phi_{2}^{\prime})$, so that
$\mathfrak{s}(y)\in\mathit{dom}(\mathfrak{h}_{2}^{\prime\prime})$ (by Lemma
4.2), contradicting the fact that $\mathfrak{h}_{1}^{\prime\prime}$ and
$\mathfrak{h}_{2}^{\prime\prime}$ are disjoint.

Consequently,
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{1}^{\prime\prime}\uplus\mathfrak{h}_{2}^{\prime\prime})\models_{\mathfrak{R}}\phi_{1}^{\prime}*\phi_{2}^{\prime}=\phi$.
As $\mathfrak{s}^{\prime\prime}\models\xi$ and
${\mathfrak{s}^{\prime\prime}(V)\cap\mathit{dom}(\mathfrak{h}_{i}^{\prime\prime})\subseteq\mathfrak{s}(V_{i})\cap\mathit{dom}(\mathfrak{h}_{i}^{\prime\prime})}$
is empty, $\mathfrak{s}^{\prime\prime}$ is injective on $V$, and ${\cal S}$ is
valid, we get
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{1}^{\prime\prime}\uplus\mathfrak{h}_{2}^{\prime\prime})\models_{\mathfrak{R}}\psi_{1}*\psi_{2}$.
Therefore, there exist disjoint heaps
$\widehat{\mathfrak{h}}^{\prime\prime}_{i}$ (for $i=1,2$), such that
$(\mathfrak{s}^{\prime\prime},\widehat{\mathfrak{h}}_{i}^{\prime\prime})\models_{\mathfrak{R}}\psi_{i}$
and
$\mathfrak{h}_{1}^{\prime\prime}\uplus\mathfrak{h}_{2}^{\prime\prime}=\widehat{\mathfrak{h}}_{1}^{\prime\prime}\uplus\widehat{\mathfrak{h}}^{\prime\prime}_{2}$.
By Lemma 3.9, since
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{1}^{\prime\prime})\models_{\mathfrak{R}}\psi_{1}$,
we deduce that
$\mathfrak{h}_{1}^{\prime\prime}=\widehat{\mathfrak{h}}_{1}^{\prime\prime}$,
thus
$\mathfrak{h}_{2}^{\prime\prime}=\widehat{\mathfrak{h}}_{2}^{\prime\prime}$,
hence and
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{2}^{\prime\prime})\models_{\mathfrak{R}}\psi_{2}$,
which contradicts the fact that
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{2}^{\prime\prime})$ is a counter-
model of
$\phi_{2}^{\prime}\curlywedge\xi\vdash_{\mathfrak{R}}^{V_{2}^{\prime}}\psi_{2}$.

We handle the case of the other rules, more precisely we show that there is
always an inference rule that applies on a valid sequent (if it is not an
axiom):

###### Lemma 5.34

For any valid sequent
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ that is not
an axiom, there exists an application of the inference rules that yields valid
premises.

###### Proof 5.35

Since $\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ is not
an axiom, $\phi$ is heap-satisfiable, $V\cap\mathit{alloc}(\phi)=\emptyset$
and $V$ contains at most one occurrence of each variable. Note that if an
invertible rule applies on
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ then the
result holds, since the premises are necessarily valid. Thus we may assume
that $\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ is
irreducible by all invertible rules, hence (by Lemma 4.26) by all the rules
except  S.

Let $\mathfrak{s}$ be an injective store such that the set
$U=\mathfrak{U}_{\mathtt{loc}}\setminus\mathfrak{s}(\mathcal{V})$ is infinite.
If $\phi\not=\mathit{emp}$, then $\phi$ contains at least one variable of sort
$\mathtt{loc}$, and by Lemma 4.36, we deduce that $\phi$ admits a model
$(\mathfrak{s},\mathfrak{h})$ such that $\mathit{dom}(\mathfrak{h})\subseteq
U\cup\mathfrak{s}(\mathit{alloc}(\phi))$. If $\phi=\mathit{emp}$ then the same
property trivially holds, with $\mathfrak{h}=\emptyset$. Note in particular
that the assertion $\mathit{dom}(\mathfrak{h})\subseteq
U\cup\mathfrak{s}(\mathit{alloc}(\phi))$ entails that
$\mathfrak{s}(V)\cap\mathit{dom}(\mathfrak{h})=\emptyset$ since
$\mathfrak{s}(V)\cap U=\emptyset$, $V\cap\mathit{alloc}(\phi)=\emptyset$ and
$\mathfrak{s}$ is injective.

If $\xi$ contains an equation then rule  R applies, which contradicts our
assumption that the sequent is irreducible by all invertible rules; thus $\xi$
is a conjunction of disequations. Furthermore, none of these disequations may
be of the form $x\not\approx x$ because otherwise
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ would be an
axiom. This entails that $\mathfrak{s}\models\xi$. Since
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ is valid,
$\mathfrak{s}(V)\cap\mathit{dom}(\mathfrak{h})=\emptyset$ and $\mathfrak{s}$
is injective (hence injective on $V$ because $V$ contains at most one
occurrence of each variable), we deduce that

$(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\psi\curlywedge\zeta.\quad\quad(\dagger)$

Assume that $\zeta$ contains an equation $x\approx y$. If $x=y$ then Rule  E
applies, and otherwise, we necessarily have
$\mathfrak{s}(x)\not=\mathfrak{s}(y)$, hence
$(\mathfrak{s},\mathfrak{h})\not\models_{\mathfrak{R}}\psi\curlywedge\zeta$
which contradicts ($\dagger$). Thus $\zeta$ contains no equation. Now assume
that $\zeta$ contains a disequation $x\not\approx y$. If
$\\{x,y\\}\subseteq\mathcal{C}$ (i.e., both $x$ and $y$ are constants) or
$\\{x,y\\}\subseteq_{m}\mathit{alloc}(\phi)\cup V$ then
$\phi\curlywedge\xi\triangleright_{V}x\not\approx y$, and  E applies, which is
impossible by hypothesis. If $x=y$ then $x\not\approx y$ is unsatisfiable,
which contradicts ($\dagger$). Let $\mathfrak{s}^{\prime}$ be a store
verifying $\mathfrak{s}^{\prime}(x)=\mathfrak{s}^{\prime}(y)$, that maps all
other variables to pairwise distinct elements of the appropriate sort, also
distinct from $\mathfrak{s}(x)$, and such that
$U^{\prime}=\mathfrak{U}_{\mathtt{loc}}\setminus\mathfrak{s}^{\prime}(\mathcal{V})$
is infinite. Such a store exists since $\mathfrak{U}_{\mathtt{loc}}$ is
infinite and $\\{x,y\\}\not\subseteq\mathcal{C}$. If
$\mathfrak{s}^{\prime}\not\models\xi$, then since $\xi$ contains no equation,
$x\not\approx y$ must occur in $\xi$. Then the rule  E applies, which
contradicts our assumption that the sequent is irreducible by all invertible
rules. Thus $\mathfrak{s}^{\prime}\models\xi$. Since
$\\{x,y\\}\not\subseteq_{m}\mathit{alloc}(\phi)$, $\mathfrak{s}^{\prime}$ is
injective on $\mathit{alloc}(\phi)$. By Lemma 4.36, we deduce that $\phi$
admits a model of the form $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})$
with $\mathit{dom}(\mathfrak{h}^{\prime})\subseteq
U^{\prime}\cup\mathfrak{s}^{\prime}(\mathit{alloc}(\phi))$. If
$\mathfrak{s}^{\prime}(V)\cap\mathit{dom}(\mathfrak{h}^{\prime})$ contains a
location $\ell$, then
$\ell=\mathfrak{s}^{\prime}(z)=\mathfrak{s}^{\prime}(z^{\prime})$, for some
$z\in\mathit{alloc}(\phi)$ and $z^{\prime}\in V$. Since
$\mathit{alloc}(\phi)\cap V=\emptyset$ and $\mathfrak{s}^{\prime}$ is
injective on all pair of variables except on $\\{x,y\\}$, necessarily we have
either $x=z$ and $y=z^{\prime}$, or $x=z^{\prime}$ and $y=z$, which means that
$\\{x,y\\}\subseteq_{m}\mathit{alloc}(\phi)\cup V$, hence  E applies,
contradicting our assumption that the sequent is irreducible by all invertible
rules. We deduce that
$\mathfrak{s}^{\prime}(V)\cap\mathit{dom}(\mathfrak{h}^{\prime})=\emptyset$.
Since $\\{x,y\\}\not\subseteq_{m}V$, $\mathfrak{s}^{\prime}$ is necessarily
injective on $V$. As
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ is valid, we
deduce that
$(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\models_{\mathfrak{R}}\psi\curlywedge\zeta$
hence $\mathfrak{s}^{\prime}(x)\not=\mathfrak{s}^{\prime}(y)$, which
contradicts the definition of $\mathfrak{s}^{\prime}$. Therefore,
$\zeta=\top$.

If $\psi=\mathit{emp}$ then necessarily $\phi=\mathit{emp}$, since otherwise
by Corollary 4.6 we would have $\mathfrak{h}\not=\emptyset$, which contradicts
$(\dagger)$. Hence in this case,
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ is of the
form $\mathit{emp}\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\mathit{emp}$ and is
an axiom.

If $\psi$ is of the form $\psi_{1}*\psi_{2}$, where
$\psi_{i}\not=\mathit{emp}$ for $i=1,2$, then the proof follows from Lemma
5.32. Thus, we may assume that $\psi$ is a spatial atom. Let $x$ be the root
of $\psi$. If $x\not\in\mathit{roots}(\phi)$, then we have
$(\mathfrak{s},\mathfrak{h})\not\models_{\mathfrak{R}}\psi$ by Lemma 4.2,
which contradicts ($\dagger$). Therefore, $\phi$ contains a spatial atom with
root $x$. If this spatial atom is a predicate atom then  U can be applied. Now
assume that $\phi$ contains a points-to atom $x\mapsto(y_{1},\dots,y_{n})$,
i.e., is of the form $x\mapsto(y_{1},\dots,y_{n})*\phi^{\prime}$ (modulo AC).
Since $\psi$ is a spatial atom with root $x$, there are two cases to consider:

  1. 1.

$\psi$ is of the form $x\mapsto(y_{1}^{\prime},\dots,y_{n}^{\prime})$. We have
$\mathfrak{h}=\\{(\mathfrak{s}(x),\mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{n}))\\}\uplus\mathfrak{h}^{\prime}$,
where $\mathfrak{h}^{\prime}$ is a heap such that
$(\mathfrak{s},\mathfrak{h}^{\prime})\models_{\mathfrak{R}}\phi^{\prime}$ and
$\mathfrak{s}(x)\not\in\mathit{dom}(\mathfrak{h}^{\prime})$. By $(\dagger)$,
we have $(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\psi$, thus
$\mathfrak{h}=\\{(\mathfrak{s}(x),\mathfrak{s}(y_{1}^{\prime}),\dots,\mathfrak{s}(y_{n}^{\prime}))\\}$.
This entails that $\mathfrak{h}^{\prime}=\emptyset$ (hence
$\phi^{\prime}=\mathit{emp}$ by Corollary 4.6), and that
$\mathfrak{s}(y_{i})=\mathfrak{s}(y_{i}^{\prime})$ for all $i=1,\dots,n$.
Since $\mathfrak{s}$ is injective, we have $y_{i}=y_{i}^{\prime}$ for all
$i=1,\dots,n$. Therefore, $\psi=\phi$, and
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ is an axiom
(because $\zeta=\top$), which contradicts the hypothesis of the lemma.

  2. 2.

$\psi$ is a predicate atom. By ($\dagger$), we have
$(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\psi$ and by definition
there exists a formula $\gamma^{\prime}$ such that
$\psi\Leftarrow_{\mathfrak{R}}\gamma^{\prime}$, where
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{\mathfrak{R}}\gamma^{\prime}$
for some associate $\mathfrak{s}^{\prime}$ of $\mathfrak{s}$ w.r.t.
$\mathcal{V}(\gamma^{\prime})\setminus\mathcal{V}(\psi)$, and in particular we
have $\mathfrak{s}(x)=\mathfrak{s}^{\prime}(x)$. As the rules in
$\mathfrak{R}$ are $\mathtt{P}$-rules, $\gamma^{\prime}$ is of the form
${(x\mapsto(u_{1},\dots,u_{m})*\psi^{\prime})\curlywedge\zeta^{\prime}}$, with
$\mathcal{V}(\gamma^{\prime})\subseteq\mathcal{V}(\psi)\cup\\{u_{1},\dots,u_{m}\\}$,
and we have
$\mathfrak{h}(\mathfrak{s}(x))=\mathfrak{h}(\mathfrak{s}^{\prime}(x))=(\mathfrak{s}^{\prime}(u_{1}),\dots,\mathfrak{s}^{\prime}(u_{m}))$.
Since $\phi$ contains a points-to atom $x\mapsto(y_{1},\dots,y_{n})$ and
$(\mathfrak{s},\mathfrak{h})\models_{\mathfrak{R}}\phi$, necessarily
$\mathfrak{h}(\mathfrak{s}(x))=(\mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{n}))$.
Consequently $n=m$ and $\mathfrak{s}(y_{i})=\mathfrak{s}^{\prime}(u_{i})$ for
all $i=1,\dots,n$. Let $\sigma$ be the substitution mapping every variable
$u_{i}$ not occurring in $\mathcal{V}(\psi)$ to $y_{i}$. Note that $\sigma$ is
well-defined: if $u_{i}=u_{j}$ then $\mathfrak{s}(y_{i})=\mathfrak{s}(y_{j})$
and $y_{i}=y_{j}$ since $\mathfrak{s}$ is injective. It is straightforward to
check that $\mathfrak{s}^{\prime}(z)=\mathfrak{s}(z\sigma)$ for all variables
$z\in\mathcal{V}$, using the definition of $\sigma$ and the fact that
$\mathfrak{s}^{\prime}$ and $\mathfrak{s}$ coincide on all variables not
occurring in $u_{1},\dots,u_{n}$. If  I applies with this substitution
$\sigma$ then the proof is completed. Otherwise, we must have
$\phi\curlywedge\xi{\not\triangleright_{V}}\zeta^{\prime}\sigma$, i.e.,
$\zeta^{\prime}$ must contain a disequation $u^{\prime}\not\approx v^{\prime}$
such that
$\phi\curlywedge\xi{\not\triangleright_{V}}u^{\prime}\sigma\not\approx
v^{\prime}\sigma$. Note that this entails that $u^{\prime}\sigma$ and
$v^{\prime}\sigma$ cannot both be constants. Consider a store
$\mathfrak{s}^{\prime\prime}$ verifying
$\mathfrak{s}^{\prime\prime}(u^{\prime}\sigma)=\mathfrak{s}^{\prime\prime}(v^{\prime}\sigma)$,
and mapping all other variables to pairwise distinct elements of the
appropriate sort. We may assume that $\mathfrak{s}^{\prime\prime}$ is chosen
in such a way that the set
$U^{\prime}=\mathfrak{U}\setminus\mathfrak{s}^{\prime\prime}(\mathcal{V})$ is
infinite. By definition,
$\mathfrak{s}^{\prime\prime}\not\models\zeta^{\prime}\sigma$, and since
$\phi\curlywedge\xi{\not\triangleright_{V}}u^{\prime}\sigma\not\approx
v^{\prime}\sigma$, we have
$\\{u^{\prime}\sigma,v^{\prime}\sigma\\}\not\subseteq_{m}V\cup\mathit{alloc}(\phi)$,
thus $\mathfrak{s}^{\prime\prime}$ is injective on $\mathit{alloc}(\phi)\cup
V$ and $\mathfrak{s}^{\prime\prime}\models\xi$ (since $\xi$ is a conjunction
of disequations not containing $u^{\prime}\sigma\not\approx
v^{\prime}\sigma$). By Lemma 4.36, $\phi$ admits a model
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}^{\prime\prime})$ such that
$\mathit{dom}(\mathfrak{h}^{\prime\prime})\subseteq
U^{\prime\prime}\cup\mathfrak{s}^{\prime\prime}(\mathit{alloc}(\phi))$. This
entails that
$\mathfrak{s}^{\prime\prime}(V)\cap\mathit{dom}(\mathfrak{h}^{\prime\prime})=\emptyset$.
Since $\mathfrak{s}^{\prime\prime}$ is injective on $V$ and
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ is valid, we
deduce that
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}^{\prime\prime})\models_{\mathfrak{R}}\psi$,
thus $\psi\Leftarrow_{\mathfrak{R}}\gamma^{\prime\prime}$, where
$(\hat{\mathfrak{s}},\mathfrak{h}^{\prime\prime})\models_{\mathfrak{R}}\gamma^{\prime\prime}$,
for some formula $\gamma^{\prime\prime}$ and associate $\hat{\mathfrak{s}}$ of
$\mathfrak{s}^{\prime\prime}$ w.r.t.
$\mathcal{V}(\gamma^{\prime\prime})\setminus\mathcal{V}(\psi)$. Since the
rules in $\mathfrak{R}$ are $\mathtt{P}$-rules, $\gamma^{\prime\prime}$ is of
the form
$(x\mapsto(u_{1}^{\prime},\dots,u_{k}^{\prime})*\psi^{\prime\prime})\curlywedge\zeta^{\prime\prime}$,
and we have
$\mathfrak{h}^{\prime\prime}(\mathfrak{s}^{\prime\prime}(x))=(\hat{\mathfrak{s}}(u_{1}^{\prime}),\dots,\hat{\mathfrak{s}}(u_{k}^{\prime}))$.
We may assume, by renaming, that
$\\{u_{1}^{\prime},\dots,u_{k}^{\prime}\\}\cap\\{u_{1},\dots,u_{m}\\}\subseteq\mathcal{V}(\psi)$.
Since $\phi$ contains a points-to atom $x\mapsto(y_{1},\dots,y_{n})$ and
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}^{\prime\prime})\models_{\mathfrak{R}}\phi$,
necessarily
$\mathfrak{h}^{\prime\prime}(\mathfrak{s}^{\prime\prime}(x))=(\mathfrak{s}^{\prime\prime}(y_{1}),\dots,\mathfrak{s}^{\prime\prime}(y_{n}))$,
and thus we must have $k=n=m$ and for all $i=1,\dots,n$,
$\mathfrak{s}^{\prime\prime}(y_{i})=\hat{\mathfrak{s}}(u_{i}^{\prime})$. Let
$\sigma^{\prime}$ be the substitution mapping every variable $u_{i}^{\prime}$
not occurring in $\mathcal{V}(\psi)$ to the first variable $y_{j}$ in
$y_{1},\dots,y_{n}$ such that
$\mathfrak{s}^{\prime\prime}(y_{j})=\hat{\mathfrak{s}}(u_{i}^{\prime})$, and
let $\theta$ be the substitution mapping every variable $y_{i}$ to $y_{j}$,
where $j$ is the smallest index in $1,\dots,n$ such that
$\mathfrak{s}^{\prime\prime}\models y_{i}\approx y_{j}$. Let
$\hat{\sigma}=\sigma\cup\sigma^{\prime}$ and
$\theta^{\prime}=\hat{\sigma}\theta$; note that $\hat{\sigma}$ is well-defined
since $\mathit{dom}(\sigma)\cap\mathit{dom}(\sigma^{\prime})=\emptyset$, as
$\\{u_{1}^{\prime},\dots,u_{k}^{\prime}\\}\cap\\{u_{1},\dots,u_{m}\\}\subseteq\mathcal{V}(\psi)$.
By construction, $\theta^{\prime}$ is a unifier of $(u_{1},\dots,u_{n})$ and
$(u_{1}^{\prime},\dots,u_{n}^{\prime})$. Since $\mathfrak{R}$ is
$\mathtt{loc}$-deterministic, one of the two formulas $\zeta^{\prime}$ or
$\zeta^{\prime\prime}$ contains a disequation $v\not\approx w$ with
$v\theta^{\prime}=w\theta^{\prime}$ and $v,w\in\mathcal{V}_{\mathtt{loc}}$.
Note that $v\hat{\sigma}\not=w\hat{\sigma}$ since otherwise
$\zeta^{\prime}\sigma$ or $\zeta^{\prime\prime}\sigma^{\prime}$ would be
unsatisfiable. We show that $v\not\approx w$ occurs in $\zeta^{\prime}$.
Assume, for the sake of contradiction, that $v\not\approx w$ occurs in
$\zeta^{\prime\prime}$. Then $v\hat{\sigma}=v\sigma^{\prime}$ and
$w\hat{\sigma}=w\sigma^{\prime}$. By definition of $\sigma^{\prime}$ and
$\theta^{\prime}$, we have $z\sigma^{\prime}=z\theta^{\prime}$ for all
$z\in\mathit{dom}(\sigma^{\prime})$, thus we get
$v\sigma^{\prime}=w\sigma^{\prime}$, hence (by definition of
$\sigma^{\prime}$) $\hat{\mathfrak{s}}(v)=\hat{\mathfrak{s}}(w)$, which
contradicts the fact that
$(\hat{\mathfrak{s}},\mathfrak{h}^{\prime\prime})\models_{\mathfrak{R}}\gamma^{\prime\prime}=(x\mapsto(u_{1}^{\prime},\dots,u_{k}^{\prime})*\psi^{\prime\prime})\curlywedge\zeta^{\prime\prime}$.
Thus necessarily $v\not\approx w$ occurs in $\zeta^{\prime}$ and we have
$v\hat{\sigma}=v\sigma$ and $w\hat{\sigma}=w\sigma$. As all rules are
$\mathtt{P}$-rules, necessarily at least one of the two variables $v,w$ (say
$v$) is an existential variable, and we must have
$v\in\mathit{alloc}(\psi^{\prime})$. Since
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{\mathfrak{R}}\gamma^{\prime}=(x\mapsto(u_{1},\dots,u_{m})*\psi^{\prime})\curlywedge\zeta^{\prime}$,
we deduce by Lemma 4.2 that
$\mathfrak{s}^{\prime}(v)\in\mathit{dom}(\mathfrak{h})$, hence
$\mathfrak{s}(v\sigma)\in\mathit{dom}(\mathfrak{h})$. By definition of
$(\mathfrak{s},\mathfrak{h})$, this entails that
$\mathfrak{s}(v\sigma)\in\mathfrak{s}(\mathit{alloc}(\phi))$, and since
$\mathfrak{s}$ is injective we get $v\sigma\in\mathit{alloc}(\phi)$.

Assume that $w\sigma\in\mathit{alloc}(\phi)$. Then $\mathit{alloc}(\phi)$
contains spatial atoms with respective roots $w\sigma$ and $v\sigma$. These
atoms must be distinct since $v\sigma\not=w\sigma$. By Lemma 4.2 these
locations are allocated in disjoint part of the heap
$\mathfrak{h}^{\prime\prime}$, hence necessarily
$\mathfrak{s}^{\prime\prime}(w\sigma)\not=\mathfrak{s}^{\prime\prime}(v\sigma)$.
We deduce that $v\theta^{\prime}\not=w\theta^{\prime}$, which contradicts our
assumption. Thus $w\sigma\not\in\mathit{alloc}(\phi)$, and since
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ cannot be an
anti-axiom, necessarily $w\sigma\in\mathcal{V}(\psi)$. We also have
$w\sigma\not\in V$, since
$\mathit{dom}(\mathfrak{h}^{\prime\prime})\cap\mathfrak{s}^{\prime\prime}(V)=\emptyset$.
We may assume that the sequent
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$ is
irreducible by the rule  C, so that, as $\psi$ is a predicate atom, $\xi$
contains a disequation $v\sigma\not\approx w\sigma$ (since
$v\sigma\in\mathit{alloc}(\phi)$,
$w\sigma\in\mathcal{V}(\psi)\setminus(\mathit{alloc}(\phi)\cup V)$). But then
we have $\mathfrak{s}^{\prime\prime}\not\models\xi$, contradicting the
definition of $\mathfrak{s}^{\prime\prime}$.

The completeness result follows immediately:

###### Theorem 5.36

If ${\cal S}$ is a valid sequent, then it admits a fully expanded (possibly
infinite) proof tree.

###### Proof 5.37

The theorem follows from Lemma 5.34.

###  5.3 Termination and Complexity

We now show that the proof procedure runs in polynomial time. To this purpose
we provide (Definition 5.38 and Lemma 5.43) a characterization of the
I-reducible sequents that may occur in a proof tree.

###### Definition 5.38

Let $\kappa\in{\mathbb{N}}$. A sequent ${\cal S}$ is an $\kappa$-companion of
a symbolic heap $\phi\curlywedge\xi$ if ${\cal S}$ is of the form
$(\phi_{1}\sigma*\phi_{2}*\phi_{3})\curlywedge(\xi_{0}\wedge\xi_{1}\wedge\xi_{2})\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\top$,
where:

  1. 1.

$\xi_{0}$ is the set of disequations occurring in $\xi$ that are of the form
$x\not\approx t$ (up to commutativity), with
$x\in(\mathcal{V}(\phi_{1}\sigma*\phi_{2}*\phi_{3})\cup\mathcal{V}(\psi))\setminus\mathcal{V}_{\mathtt{loc}}$
and $t\not=x$.

  2. 2.

$\xi_{1}=\bigwedge_{x\in{\cal V}^{\star}({\cal S}),y\in A}x\not\approx y$,
where
$A=\mathit{alloc}(\phi_{1}\sigma*\phi_{2}*\phi_{3})\setminus\mathcal{V}(\psi)$.

  3. 3.

$\xi_{2}$ is a conjunction of disequations of the form $u\not\approx v$, where
$u,v\in\mathcal{V}(\psi)$.

  4. 4.

$\psi$ is a predicate atom.

  5. 5.

$V\subseteq\mathcal{V}(\psi)$.

  6. 6.

Either $\phi_{1}=\mathit{emp}$, or there exists a predicate atom $\alpha$ such
that $\mathit{root}(\alpha)=\mathit{root}(\psi)$ and
$\alpha\Leftarrow_{\mathfrak{R}}\phi_{1}$.

  7. 7.

$\mathit{len}(\phi_{2})\leq\kappa+1$.

  8. 8.

$\sigma$ is a substitution such that
$\mathit{card}(\mathit{dom}(\sigma))\leq\kappa$.

  9. 9.

$\phi\sigma$ is of the form $\phi_{3}*\eta_{1}*\eta_{2}$ (modulo AC), where
$\mathit{len}(\eta_{1})\leq 2\cdot\kappa$ and:

    1. (a)

no atom $\beta$ occurring in $\phi_{3}$ is such that
$\mathit{root}(\psi)\not\rightarrow_{\phi_{1}\sigma*\phi_{2}*\phi_{3}*\eta_{2}}^{*}\mathit{root}(\beta)$;
and

    2. (b)

no atom $\beta$ occurring in $\eta_{2}$ is such that
$\mathit{root}(\psi)\rightarrow_{\phi_{1}\sigma*\phi_{2}*\phi_{3}*\eta_{2}}^{*}\mathit{root}(\beta)$.

Intuitively, we aim at describing sequents ${\cal S}$ that are  I-reducible
and occur in some proof tree, where the formula $\phi\curlywedge\xi$ is meant
to denote the left-hand side of the root sequent. It is clear that the left-
hand side of ${\cal S}$ will contain some parts that are inherited from the
formula $\phi\curlywedge\xi$, together with some other parts, that are
introduced by the inference rules applied along the branch of ${\cal S}$ in
the proof tree. First, observe that Conditions 4 (stating that the right-hand
side of ${\cal S}$ is a predicate atom $\psi$) and 5 (stating that the
variables in $V$ must occur in $\psi$) are easy consequences of the fact that
${\cal S}$ is  I-reducible: rules  S and  V cannot be applied. The
substitution $\sigma$ is intended to encode the effect of the (cumulative)
applications of rule  C (in the left branch): some variables initially
occurring in $\phi\curlywedge\xi$ are replaced by other variables. Note that
Condition 8 bounds the size of this substitution, which is essential to avoid
any exponential blow-up. As we shall see, it stems from the fact that rule  C
only applies, by Definition 4.43 (4), to a variable in ${\cal V}^{\star}({\cal
S})$ which restricts the number of applications of the rule. The formula
$\xi_{0}$ denotes the set of disequations between variables of a sort distinct
from $\mathtt{loc}$, which are all inherited from $\xi$ (as the rules contain
no disequations of this form). On the other hand, $\xi_{1}$ denotes the set of
disequations that were introduced by previous applications of  C (in the right
branch). Note that since ${\cal S}$ is  I-reducible, we may assume that all
the possible applications of  C have been applied, leading either to the
elimination of a variable (encoded in $\sigma$) or to the addition of some
disequation, this is why $\xi_{1}$ contains the set of all possible
disequations. The formula $\xi_{2}$ denotes the set of disequations between
variables in $\psi$, which are arbitrary (this is not problematic as the
number of such disequations is bounded, as $\psi$ is an atom). The formula
$\phi_{1}$ denotes the part of the formula added in the left-hand side of the
sequent by the last application of  U. The formula may be empty, because such
application does not always exist (for instance if ${\cal S}$ is the root
sequent). The atom $\alpha$ then denotes the predicate atom on which  U was
previously applied. Observe that the root of this atom is always the same as
that of $\psi$, by Definition 4.43 (3). Note also that the formula contains no
atom obtained from any application of  U occurring before the last one (i.e.,
on atoms other than $\alpha$): indeed, we shall prove that all such atoms must
have been eliminated by previous decomposition steps when  I was applied. The
formula $\phi_{1}\sigma$ contains all spatial atoms inherited from the initial
formula $\phi$. Note that some atoms in $\phi$ may have been deleted, by
previous applications of  S. The difficulty here is that this could lead to an
exponential blow-up, since in principle one could consider all possible
subsets of $\phi$. To overcome this issue, we refine the criterion by taking
into account all the additional reachability conditions that prevent ${\cal
S}$ from being an axiom or an anti-axiom. We thus further split the
conjunction of atoms that were deleted from $\phi$ into two parts
$\eta_{1}*\eta_{2}$, where $\eta_{1}$ contains a bounded number of atoms that
can be chosen in an arbitrary way, and $\eta_{2}$ may contain an arbitrary
number of atoms, but is fully determined by the choice of $\phi_{1},\phi_{2}$
and $\eta_{1}$.

The following lemma shows that a formula has only polynomially many
$\kappa$-companions, up to a renaming of variables.

###### Lemma 5.39

Let $\phi\curlywedge\xi$ be a spatial formula and $E$ be a set of variables.
For every fixed number $\kappa$, if
$\mathit{ar}_{\mathit{max}}(\mathfrak{R})\leq\kappa$ (i.e., if the maximal
arity of the predicate symbols in bounded by $\kappa$), then the number of
sequents ${\cal S}$ that are $\kappa$-companions of $\phi\curlywedge\xi$ and
such that $\mathcal{V}({\cal S})\subseteq E$ is polynomial w.r.t.
$|\phi|+|\mathfrak{R}|+\mathit{card}(E)$ (up to AC), and the size of ${\cal
S}$ is polynomial w.r.t. $|\phi|+|\mathfrak{R}|$.

###### Proof 5.40

By Definition 5.38, ${\cal S}$ is of the form
$(\phi_{1}\sigma*\phi_{2}*\phi_{3})\curlywedge(\xi_{1}\wedge\xi_{2})\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\top$,
and satisfies Conditions $1$-$9$. Note that since $\psi$ is a predicate atom,
we have $|\psi|\leq 1+\mathit{ar}_{\mathit{max}}(\mathfrak{R})\leq\kappa+1$
and
$\mathit{card}(\mathcal{V}(\psi))\leq\mathit{ar}_{\mathit{max}}(\mathfrak{R})\leq\kappa$.

We have
$\mathit{len}(\phi_{1}*\phi_{2}*\phi_{3})=\mathit{len}(\phi_{1})+\mathit{len}(\phi_{2})+\mathit{len}(\phi_{3})\leq\mathit{len}(\phi_{1})+\kappa+1+\mathit{len}(\phi)\leq|\mathfrak{R}|+|\phi|+\kappa+1$,
thus
$|\phi_{1}\sigma*\phi_{2}*\phi_{3}|\leq(\kappa+1)\cdot(|\mathfrak{R}|+|\phi|+\kappa+1)=O(|\phi|+|\mathfrak{R}|)$.
Since
$\mathcal{V}(\zeta_{1})\cup\mathcal{V}(\zeta_{2})\subseteq\mathcal{V}(\phi_{1}\sigma*\phi_{2}*\phi_{3})\cup\mathcal{V}(\psi)$,
we deduce that $|\xi_{1}\wedge\xi_{2}|=O((|\phi|+|\mathfrak{R}|)^{2})$ hence
$|{\cal S}|=O((|\phi|+|\mathfrak{R}|)^{2})$.

Let $n=\mathit{card}(E)+|\phi|+\mathit{card}(\mathcal{C})+1$. Note that
$n\leq\mathit{card}(E)+|\phi|+|\mathfrak{R}|+1$. The number of possible
predicate atoms $\psi$ and $\alpha$ is at most
$\mathit{card}(\mathcal{P})\cdot n^{\kappa}\leq|\mathfrak{R}|\cdot
n^{\kappa}$. Similarly, the number of formulas $\phi_{2}$ is at most
$|\mathfrak{R}|^{\kappa+1}\cdot n^{(\kappa+1)^{2}}$. Once $\alpha$ is fixed,
the number of formulas $\phi_{1}$ cannot be greater than the number of rules
in $\mathfrak{R}$, up to a renaming of variables. Since
$\mathit{card}(\mathit{dom}(\sigma))\leq\kappa$, there are at most
$n^{2\cdot\kappa}$ possible substitutions $\sigma$ we only have to choose the
set $\mathit{dom}(\sigma)$, i.e., at most $\kappa$ elements among the
variables occurring in $\phi$ or $\phi_{1}$, and the image of each variable in
$\mathit{dom}(\sigma)$ among the variables in $E$. The number of formulas
$\phi_{3}$ is at most $\mathit{len}(\phi)^{2\cdot\kappa}$ (since we only have
to choose the formula $\eta_{1}$ in $\phi$, as $\eta_{2}$ is entirely
determined by the choice of $\phi_{1},\phi_{2}$ and $\eta_{1}$). We have
$\mathcal{V}(\xi_{2})\subseteq\mathcal{V}(\psi)$ thus
$\mathit{card}(\mathcal{V}(\xi_{2}))\leq\kappa$, and there are
$2^{\kappa^{2}}$ possible formulas $\xi_{2}$. Since
$V\subseteq\mathcal{V}(\psi)$, we have $\mathit{card}(V)\leq\kappa$ and the
number of possible sets $V$ is $2^{\kappa}$. Finally, the formulas $\xi_{0}$
and $\xi_{1}$ are fixed once $\phi$ and $\phi_{1},\phi_{2},\phi_{3}$ and
$\sigma$ are fixed.

Lemma 5.43 is used to prove that every sequent that is  I-reducible and occurs
in a proof tree is a companion of the left-hand side of the root of the proof
tree. Together with Lemma 5.39 and the result stated in Lemma 5.19 on the
number of  I-free descendants of a sequent, this will entail that the size of
the proof tree is polynomial w.r.t. the size of the root. We use the following
proposition, which is an easy consequence of the definition of the rules.

###### Proposition 5.41

Let ${\cal S}_{i}=\lambda_{i}\vdash_{\mathfrak{R}}^{V_{i}}\gamma_{i}$ (for
$i=1,2$) be sequents. If ${\cal S}_{2}$ is a successor of ${\cal S}_{1}$, then
$\mathit{alloc}(\lambda_{1})\cap\mathit{alloc}(\gamma_{1})\cap\mathit{alloc}(\lambda_{2})\subseteq\mathit{alloc}(\gamma_{2})$.

###### Proof 5.42

Assume that
$x\in\mathit{alloc}(\lambda_{1})\cap\mathit{alloc}(\gamma_{1})\cap\mathit{alloc}(\lambda_{2})$
and $x\not\in\mathit{alloc}(\gamma_{2})$. It is easy to check, by inspection
of the rules, that the only rule that can remove the variable $x$ from
$\mathit{alloc}(\gamma_{1})$ is  S (indeed,  I deletes a predicate atom but
introduce a points-to atom with the same root, and the rules  R and  C cannot
replace $x$ as otherwise it would not occur in $\lambda_{2}$ ). By definition
of the rule, ${\cal S}_{1}$ also has a successor ${\cal
S}_{2}^{\prime}=\lambda_{2}^{\prime}\vdash_{\mathfrak{R}}^{V_{2}^{\prime}}\gamma_{2}^{\prime}$
such that $x\in V_{2}^{\prime}$ (since $x\in\mathit{alloc}(\lambda_{2})$) and
$x\in\mathit{alloc}(\gamma_{2}^{\prime})$ (since
$x\not\in\mathit{alloc}(\gamma_{2})$). This entails that ${\cal
S}_{2}^{\prime}$ is an anti-axiom, contradicting Condition 1 in Definition
4.43.

###### Lemma 5.43

Assume that $\mathit{ar}_{\mathit{max}}(\mathfrak{R})\leq\kappa$ for
$\kappa\in{\mathbb{N}}$, and let ${\cal
S}=\phi\curlywedge\xi\vdash\psi\curlywedge\zeta$ be an equality-free sequent.
Every  I-reducible sequent occurring in a proof tree with root ${\cal S}$ is a
$\kappa$-companion of the left-hand side $\phi\curlywedge\xi$ of ${\cal S}$.

###### Proof 5.44

Let ${\cal
S}^{\prime}=\phi^{\prime}\curlywedge\xi^{\prime}\vdash_{\mathfrak{R}}^{V^{\prime}}\psi^{\prime}\curlywedge\zeta^{\prime}$
be an  I-reducible sequent occurring in a proof tree with root ${\cal S}$. Let
${\cal S}_{1},\dots,{\cal S}_{n}$, be a path from ${\cal S}$ to ${\cal
S}^{\prime}$, where ${\cal S}_{1}={\cal S}$, ${\cal S}_{n}={\cal S}^{\prime}$
and ${\cal S}_{i}=\lambda_{i}\vdash_{\mathfrak{R}}^{V_{i}}\gamma_{i}$ for
$i=1,\ldots,n$. We check that all the conditions in Definition 5.38 are
satisfied. Note that by Condition 1 in Definition 4.43, ${\cal S}^{\prime}$
cannot be an axiom or an anti-axiom.

  * •

Right-Hand Side. We first show that the right-hand side $\psi^{\prime}$ is
indeed a predicate atom. By Condition 2 in Definition 4.43,
$\zeta^{\prime}=\top$ and $\psi^{\prime}$ is a predicate atom, thus Condition
4 of Definition 5.38 holds.

  * •

Pure Formulas. We then prove that the pure formulas $\xi^{\prime}$ fulfill
Conditions 1, 2 and 3. If $\xi^{\prime}$ contains an equality then the rule  R
applies, hence ${\cal S}^{\prime}$ cannot be  I-reducible because  R has
priority over  I (Condition 6 in Definition 4.43). Thus $\xi^{\prime}$ is a
conjunction of disequations, and it can be written as
$\xi_{0}\curlywedge\xi_{1}\wedge\xi_{2}$ where $\xi_{0}$ is the set of
disequations in $\xi^{\prime}$ between terms of a sort distinct from
$\mathtt{loc}$,
$\mathcal{V}(\xi_{2})\subseteq\mathcal{V}(\psi^{\prime})\cap\mathcal{V}_{\mathtt{loc}}$
and $\xi_{1}$ only contains disequations of the form $u\not\approx v$ (up to
commutativity of $\not\approx$) with $u,v\in\mathcal{V}_{\mathtt{loc}}$ and
$u\not\in\mathcal{V}(\psi^{\prime})$. Note that each disequation involves
distinct terms because by hypothesis, ${\cal S}^{\prime}$ is not an axiom.
Consider one such disequation $u\not\approx v$ in $\xi_{1}$. If
$u\not\in\mathcal{V}(\phi^{\prime})$ then rule  W applies by the second
application condition of the rule, which is impossible since this rule has
priority over  I and ${\cal S}^{\prime}$ would not be  I-reducible. We deduce
that $u\in\mathcal{V}(\phi^{\prime})$, and since ${\cal S}^{\prime}$ is not an
anti-axiom, we must have $u\in\mathit{alloc}(\phi^{\prime})$. If
$v\not\in\mathcal{V}(\phi^{\prime})\cup\mathcal{V}(\psi^{\prime})$ or
$v\in\mathit{alloc}(\phi^{\prime})\cup V^{\prime}$ then rule  W also applies
(in the latter case, we have $\phi^{\prime}\triangleright_{V_{i}}u\not\approx
v$ by Condition 3 of Definition 4.13). Thus
$v\in\mathcal{V}(\phi^{\prime})\cup\mathcal{V}(\psi^{\prime})$ and
$v\not\in\mathit{alloc}(\phi^{\prime})\cup V$. This entails that
$v\in\mathcal{V}(\psi^{\prime})$ since otherwise ${\cal S}^{\prime}$ would be
an anti-axiom by Condition 5 of Definition 4.34 because
$u\in\mathit{alloc}(\phi^{\prime})$, hence $v$ is necessarily of sort
$\mathtt{loc}$. We therefore have $v\in{\cal V}^{\star}({\cal S}^{\prime})$
and $u\in\mathit{alloc}(\phi^{\prime})\setminus\mathcal{V}(\psi^{\prime})$.
Conversely, if a disequation $u\not\approx v$ with $v\in{\cal V}^{\star}({\cal
S}^{\prime})$ and
$u\in\mathit{alloc}(\phi^{\prime})\setminus\mathcal{V}(\psi^{\prime})$ does
not occur in $\xi_{1}$ then by Condition 4 in Definition 4.43,  C would be
applicable, which is impossible. Thus Conditions 2 and 3 in Definition 5.38
are satisfied. By Proposition 4.23 (5) no rule introduces a disequation
between terms of a sort distinct from $\mathtt{loc}$, all disequations in
$\xi_{0}$ must occur in $\xi$. Furthermore, such a disequation cannot be of
the form $t\not\approx t$ (otherwise ${\cal S}^{\prime}$ would be an axiom as
explained above) and must contain a variable occurring in $\phi^{\prime}$ or
$\psi^{\prime}$ (otherwise  W would apply). Conversely, no rule can delete a
disequation containing a variable in
$(\mathcal{V}(\phi^{\prime})\cup\mathcal{V}(\psi^{\prime}))\setminus\mathcal{V}_{\mathtt{loc}}$
from the left-hand side of the sequent. Thus Condition 1 holds.

  * •

Non Allocated Variables. We now check that Condition 5 applies, namely that
$V^{\prime}\subseteq\mathcal{V}(\psi^{\prime})$. Assume, for the sake of
contradiction, that $V^{\prime}$ contains a variable
$x\not\in\mathcal{V}(\psi^{\prime})$. Since ${\cal S}^{\prime}$ is not an
anti-axiom, we have
$V^{\prime}\cap(\mathcal{V}(\phi^{\prime})\setminus\mathcal{V}(\psi^{\prime}))=\emptyset$,
hence $x\not\in\mathcal{V}(\phi^{\prime})$. If $x\in\mathcal{V}(\xi^{\prime})$
then  W applies, and otherwise  V applies. In both cases, ${\cal S}^{\prime}$
cannot be  I-reducible (since  W and  V have priority over  I), which
contradicts our assumption. Thus Condition 5 holds.

  * •

Substitution $\sigma$. We now define the substitution $\sigma$, and we show
that Condition 8 holds. Let $i$ be the least number such that the right-hand
side $\gamma_{i}$ of ${\cal S}_{i}$ is a spatial atom ($i$ must exist since
$n$ fulfills this condition, by Condition 2 in Definition 4.43), and let
$V^{\star}={\cal V}^{\star}({\cal S}_{i})$. Note that $\gamma_{i}$ must be a
predicate atom. Indeed, the right-hand side of
$\gamma_{n}=\lambda_{n}\vdash_{\mathfrak{R}}^{V_{n}}\gamma_{n}$ is a predicate
atom since ${\cal S}_{n}$ is  I-reducible, and by Condition 6 of Proposition
4.23, the only rule that can introduce a predicate atom to the right-hand side
of a premise is  I, which by Condition 2 in Definition 4.43, applies only if
the right-hand side of the conclusion is a predicate atom. Thus $\gamma_{j}$
cannot be a points-to atom. By Proposition 5.5 we have ${\cal V}^{\star}({\cal
S}_{j})\subseteq V^{\star}$, for all $j=i,\dots,n$, and
$\mathit{card}(V^{\star})\leq\mathit{ar}_{\mathit{max}}(\mathfrak{R})\leq\kappa$
since $V^{\star}\subseteq\mathcal{V}({\cal S}_{i})$ and $\gamma_{i}$ is a
predicate atom. Let $I\subseteq\\{1,\dots,n\\}$ be the set of indices $j$ such
that rule  C applies on ${\cal S}_{j}$, and replaces a variable $x_{j}$ by a
variable $y_{j}$ (i.e., such that ${\cal S}_{j+1}$ is a left premise of an
application of  C on ${\cal S}_{j}$ with variables $x_{j}$ and $y_{j}$). By
Condition 4 of Definition 4.43,  C applies only if the right-hand side of the
conclusion is a predicate atom, thus we must have $I\subseteq\\{i,\dots,n\\}$.
Let $\sigma=\sigma_{n}$, where $\sigma_{0}=\id$,
$\sigma_{j+1}=\sigma_{j}\\{x_{j+1}\leftarrow y_{j+1}\\}$ if $j+1\in I$ and
$\sigma_{j+1}=\sigma_{j}$ otherwise. By Condition 4 in Definition 4.43, for
all $j\in I$, we have $y_{j}\in{\cal V}^{\star}({\cal S}_{j})\subseteq{\cal
V}^{\star}({\cal S}_{i})=V^{\star}$. Also, $y_{j}\not\in{\cal V}^{\star}({\cal
S}_{j+1})$ because $x_{j}$ must be allocated in the left-hand side of ${\cal
S}_{j}$, hence, after the replacement, $y_{j}$ is allocated in the left-hand
side of ${\cal S}_{j+1}$. Thus by Proposition 5.5, $y_{j}\not\in{\cal
V}^{\star}({\cal S}_{j^{\prime}})$, for all $j^{\prime}>j$, which entails that
the $y_{j}$ for $j\in I$ are pairwise distinct. Therefore,
$\mathit{card}(I)\leq\mathit{card}(V^{\star})\leq\kappa$, hence
$\mathit{card}(\mathit{dom}(\sigma))\leq\kappa$ and Condition 8 is satisfied.

  * •

Unfolded Atom. Now we define the unfolded predicate atom $\alpha$ and we prove
that Condition 6 holds. If rule  U is applied on a sequent ${\cal S}_{k}$ and
${\cal S}^{\prime}$ is an  I-free descendant of ${\cal S}_{k}$, then we denote
by $\alpha$ the predicate atom on which  U is applied, and by
$\phi_{1}\curlywedge\chi$ the formula occurring in ${\cal S}_{k+1}$ such that
$\alpha\Leftarrow_{\mathfrak{R}}\phi_{1}\curlywedge\chi$. If no such
application of  U exists then we simply set $\phi_{1}=\mathit{emp}$. Note that
if $k$ and $\alpha$ exist then they must be unique, since we assumed that
${\cal S}^{\prime}$ is an  I-free descendant of ${\cal S}_{k}$ and by
Corollary 5.12 there must be an application of  I along the path between any
two applications of  U. Also, by Condition 3 in Definition 4.43, $\gamma_{k}$
is a spatial atom and $\mathit{root}(\alpha)=\mathit{root}(\gamma_{k})$. By
Proposition 5.8, the only rules that can be applied on ${\cal
S}_{k+1},\dots,{\cal S}_{n-1}$ are  W,  C, or  V. Each of these rules only
affects the right-hand side of its premise by instantiating it with $\sigma$
thus $\mathit{root}(\alpha)\sigma=\mathit{root}(\psi^{\prime})$. First
consider the case where $k$ exists. Since the rules in $\mathfrak{R}$ are
$\mathtt{P}$-rules, $\lambda_{k+1}$ must contain a points-to atom. By
Condition 3 in Definition 4.43, the root of this atom must be the same as that
of $\gamma_{k}=\gamma_{k+1}$. Furthermore, $\lambda_{k+1}$ contains no
equation, since otherwise this equation would occur in $\lambda_{k}$, rule  R
would be applicable on ${\cal S}_{k}$ and this rule has priority over  U.
Therefore, ${\cal S}_{k+1}$ is quasi- I-reducible. By Proposition 5.8, this
entails that only the rules  W,  V or  C may be applied along the path ${\cal
S}_{k+1},\dots,{\cal S}_{n}$. These rules either do not affect spatial
formulas, or uniformly replace a variable $x_{j}$ (for $j\in I$) by
$y_{j}=x_{j}\sigma_{j}$ (hence eventually, every variable $x$ is replaced by
$x\sigma$). Thus $\phi^{\prime}$ is of the form
$\phi_{1}\sigma*\phi_{1}^{\prime}$. It is clear that the previous assertion
trivially holds in the case where $k$ does not exist by letting
$\phi_{1}=\mathit{emp}$. Thus Condition 6 holds.

  * •

Spatial Formula. We now prove that the spatial formula $\phi_{1}^{\prime}$ is
of the required form and fulfills Condition 7. The formula $\phi_{1}^{\prime}$
may be written as $\phi_{2}*\phi_{3}*\phi_{4}$, where:

    * –

$\mathit{alloc}(\phi_{2})\subseteq(V^{\star}\cup\mathit{alloc}(\psi^{\prime}))$,

    * –

$\mathit{alloc}(\phi_{3})\subseteq\mathcal{V}(\phi)\setminus(V^{\star}\cup\mathit{alloc}(\psi^{\prime}))$,

    * –

$\mathit{alloc}(\phi_{4})\cap(\mathcal{V}(\phi)\cup
V^{\star}\cup\mathit{alloc}(\psi^{\prime}))=\emptyset$.

If $\phi_{2}$ contains two atoms with the same root then $\phi^{\prime}$ is
heap-unsatisfiable and ${\cal S}^{\prime}$ is an axiom. Thus
$\mathit{len}(\phi_{2})\leq\mathit{card}(V^{\star})+1\leq\kappa+1$ and
Condition 7 holds.

The only rule that can add new predicate symbols to a premise is  U, replacing
an atom $\alpha^{\prime}$ by a formula $\lambda$ such that
$\alpha^{\prime}\Leftarrow_{\mathfrak{R}}\lambda$. Since the rules in
$\mathfrak{R}$ are $\mathtt{P}$-rules, the root of every predicate atom in
$\lambda$ must be a fresh variable $y$, not occurring in $\mathcal{V}(\phi)$.
If $y\in\mathit{dom}(\sigma)$ then $y$ is eventually replaced by some variable
in $V^{\star}$, hence the corresponding predicate atom from
$\phi_{1}^{\prime}$ is in $\phi_{2}$. If $y\not\in\mathit{dom}(\sigma)$, then
since this variable is never replaced, the corresponding atom must occur in
$\phi_{4}$ by construction. This entails that all the atoms in $\phi_{3}$ must
be obtained from atoms in $\phi$ after application of the substitution
$\sigma$, i.e., that $\phi\sigma=\phi_{3}*\eta$ for some formula $\eta$, up to
AC. The formula $\eta$ can be written as $\eta_{1}*\eta_{2}$ where
$\mathit{alloc}(\eta_{1})\subseteq\mathcal{V}(\psi^{\prime})\cup V^{\star}$
and $\mathit{alloc}(\eta_{2})\cap(\mathcal{V}(\psi^{\prime})\cup
V^{\star})=\emptyset$. This entails that $\mathit{len}(\eta_{1})\leq
2\cdot\kappa$, since $\mathit{card}(\mathcal{V}(\psi^{\prime}))\leq\kappa$ and
$\mathit{card}(V^{\star})\leq\kappa$.

We prove that necessarily $\phi_{4}=\mathit{emp}$. Assume for the sake of
contradiction that $\phi_{4}$ contains an atom $\alpha^{\prime}$, and let
$u=\mathit{root}(\alpha^{\prime})$. By definition of $\phi_{4}$,
$u\not\in\mathcal{V}(\phi)\cup V^{\star}\cup\mathit{alloc}(\psi^{\prime})$.
The variable $u$ must have been introduced by an application of rule  U on
some sequent ${\cal S}_{m}$, as  U is the only rule that can introduce new
variables to the left-hand side of a sequent. By Proposition 5.10, ${\cal
S}_{m+1}$ is quasi- I-reducible, and we must have $m\not=k$ (if $k$ exists),
since otherwise $\alpha^{\prime}$ would occur in $\phi_{1}\sigma$. Since the
rules in $\mathfrak{R}$ are $\mathtt{P}$-rules, we have $u\in{\cal
V}_{\mapsto}({\cal S}_{m+1})$. Since $m\not=k$, by Corollary 5.12, there
exists $m^{\prime}$ such that $m<m^{\prime}$ and ${\cal S}_{m^{\prime}}$ is
I-reducible, i.e., rule  I is applied on ${\cal S}_{m^{\prime}}$. Let
$m^{\prime}$ be the minimal number satisfying this property. The path ${\cal
S}_{m+1},\dots,{\cal S}_{m^{\prime}}$ only contains applications of  W,  V and
C, and $u\in{\cal V}_{\mapsto}({\cal S}_{m^{\prime}})$ by Proposition 5.8.
Note that if $k$ exists then necessarily $m^{\prime}<k$, moreover, none of
these rules can introduce new variables to the right-hand side of a sequent.
In particular, variable $u$, which is a fresh variable that does not occur in
$\gamma_{m}$, cannot occur on the right-hand side $\gamma_{m^{\prime}}$ of
${\cal S}_{m^{\prime}}$. Let $\theta$ denote the substitution used in the
application of  I on ${\cal S}_{m^{\prime}}$. As $u\in{\cal V}_{\mapsto}({\cal
S}_{m^{\prime}})$, there exists a variable $z\in\mathit{dom}(\theta)$ such
that $z\theta=u$. Since the rules in $\mathfrak{R}$ are $\mathtt{P}$-rules,
this entails that $u\in\mathit{alloc}(\gamma_{m^{\prime}+1})$. Consequently,
$u\in\mathit{alloc}(\lambda_{m^{\prime}+1})\cap\mathit{alloc}(\gamma_{m^{\prime}+1})$
and by (repeatedly) applying Proposition 5.41, we deduce that
$u\in\mathit{alloc}(\psi^{\prime})$ (since by hypothesis
$u\in\mathit{alloc}(\phi_{4})\subseteq\mathit{alloc}(\phi^{\prime})$), which
contradicts the definition of $\phi_{4}$.

  * •

Reachability Conditions. Finally, we show that Condition 9 holds, i.e., that
$\eta_{2}$ contains exactly the atoms $\beta$ in $\phi_{3}*\eta_{2}$ such that
$\mathit{root}(\psi^{\prime})\not\rightarrow_{\phi_{1}\sigma*\phi_{2}*\phi_{3}*\eta_{2}}\mathit{root}(\beta)$.
Assume that $\phi_{3}$ contains an atom $\beta$ such that
$\mathit{root}(\psi^{\prime})\not\rightarrow_{\phi_{1}\sigma*\phi_{2}*\phi_{3}*\eta_{2}}\mathit{root}(\beta)$.
Since $\phi^{\prime}=\phi_{1}\sigma*\phi_{2}*\phi_{3}$, we get
$\mathit{root}(\psi^{\prime})\not\rightarrow_{\phi^{\prime}}\mathit{root}(\beta)$,
$\mathit{root}(\beta)\in\mathit{alloc}(\phi^{\prime})$ and
$\mathit{root}(\beta)\not\in\mathit{alloc}(\psi^{\prime})$ (because
$\mathit{root}(\beta)\not=\mathit{root}(\psi^{\prime})$ and
$\mathit{alloc}(\psi^{\prime})=\\{\mathit{root}(\psi^{\prime})\\}$), thus
${\cal S}^{\prime}$ is an anti-axiom. Conversely, assume that $\eta_{2}$
contains an atom $\beta$ such that
$\mathit{root}(\psi^{\prime})\rightarrow_{\phi_{1}\sigma*\phi_{2}*\phi_{3}*\eta_{2}}\mathit{root}(\beta)$.
Note that $\mathit{root}(\beta)\not\in\mathcal{V}(\psi^{\prime})\cup
V^{\star}$, by definition of $\eta_{2}$, which entails that
$\mathit{root}(\beta)\not\in\mathit{codom}(\sigma)$. If
$\mathit{root}(\beta)\not\in\mathit{alloc}(\phi^{\prime})$, then by
considering the first variable
$y\not\in\mathit{alloc}(\phi^{\prime})=\mathit{alloc}(\phi_{1}\sigma*\phi_{2}*\phi_{3})$
along the path from $\mathit{root}(\psi^{\prime})$ to $\mathit{root}(\beta)$,
we have $y\in\mathcal{V}(\phi^{\prime})$,
$y\not\in\mathit{alloc}(\phi^{\prime})$ and $y\in\mathit{alloc}(\eta_{2})$,
hence $y\not\in\mathcal{V}(\psi^{\prime})$. Thus ${\cal S}^{\prime}$ is an
anti-axiom, contradicting our hypothesis. Therefore,
$\mathit{root}(\beta)\in\mathit{alloc}(\phi^{\prime})=\mathit{alloc}(\phi_{1}\sigma)\cup\mathit{alloc}(\phi_{2})\cup\mathit{alloc}(\phi_{3})$.
We distinguish the three cases:

    * –

Assume that $\mathit{root}(\beta)\in\mathit{alloc}(\phi_{1}\sigma)$ i.e., that
$k$ exists, $\phi_{1}\neq\mathit{emp}$ and
$\alpha\Leftarrow_{\mathfrak{R}}\phi_{1}\curlywedge\chi$. Since
$\mathit{root}(\beta)\not\in\mathit{codom}(\sigma)$, we also have
$\mathit{root}(\beta)\in\mathit{alloc}(\phi_{1})$. Since the rules in
$\mathfrak{R}$ are $\mathtt{P}$-rules, the variables in
$\mathit{alloc}(\phi_{1})$ are either the root of $\alpha$ or fresh variables.
Now $\mathit{root}(\alpha)\sigma$ must be distinct from
$\mathit{root}(\beta)$, since
$\mathit{root}(\beta)\not\in\mathcal{V}(\psi^{\prime})$ and
$\mathit{root}(\alpha)\sigma=\mathit{root}(\psi^{\prime})$. Furthermore, all
fresh variables are necessarily distinct from $\mathit{root}(\beta)$. Indeed,
they cannot occur in $\phi$, by definition, and
$\mathit{root}(\beta)\subseteq\mathit{alloc}(\phi)$, as
$\mathit{root}(\beta)\subseteq\mathit{alloc}(\eta_{2})\subseteq\mathit{alloc}(\eta)\subseteq\mathit{alloc}(\phi\sigma)$
and $\mathit{root}(\beta)\not\in\mathit{codom}(\sigma)$. Thus this case cannot
occur.

    * –

If $\mathit{root}(\beta)\in\mathit{alloc}(\phi_{2})$, then
$\mathit{root}(\beta)\in V^{\star}\cup\mathit{alloc}(\psi^{\prime})$ (by
definition of $\phi_{2}$), which contradicts the fact that
$\mathit{root}(\beta)\not\in\mathcal{V}(\psi^{\prime})\cup V^{\star}$.

    * –

If $\mathit{root}(\beta)\in\mathit{alloc}(\phi_{3})$, then
$\mathit{root}(\beta)$ occurs twice in $\mathit{alloc}(\phi\sigma)$ because
$\phi\sigma=\phi_{3}*\eta_{1}*\eta_{2}$; hence, it also occurs twice in
$\mathit{alloc}(\phi)$ because
$\mathit{root}(\beta)\not\in\mathit{codom}(\sigma)$. This entails that $\phi$
is heap-unsatisfiable, a contradiction.

Thus we get a contradiction, which entails that Condition 9 in Definition 4.43
is satisfied.

We now introduce a restricted form of variable renaming333Note that we cannot
assume that sequents are taken modulo variable renaming, since identity would
then be difficult to test (it would be equivalent to the well-known graph
isomorphism problem).. The definition is useful to straightforwardly detect
cycles in a proof tree, which is essential for efficiency. For each sort
${\mathtt{s}}$, we consider infinite (fixed) sequences of pairwise distinct
variables of sort ${\mathtt{s}}$: $x_{i}^{\mathtt{s}}$, with
$i\in{\mathbb{N}}$ (not occurring in the root sequent). A sequent ${\cal
S}^{\prime}$ occurring in a proof tree with root ${\cal S}$ is normalized if,
for every variable $y$ of sort ${\mathtt{s}}$ occurring in $\mathcal{V}({\cal
S}^{\prime})\setminus\mathcal{V}({\cal S})$, there exists $i\leq|{\cal
S}^{\prime}|$ such that $y=x_{i}^{\mathtt{s}}$. It is clear that every sequent
${\cal S}^{\prime}$ can be reduced in polynomial time to a normalized sequent.
Indeed, it suffices to rename all the variables $y_{1},\dots,y_{n}$ of sorts
${\mathtt{s}}_{1},\dots,{\mathtt{s}}_{n}$ occurring in ${\cal S}^{\prime}$ but
not in ${\cal S}$ by the variables
$x_{1}^{{\mathtt{s}}_{1}},\dots,x_{n}^{{\mathtt{s}}_{n}}$, respectively. As
$n$ cannot be greater than the size of ${\cal S}^{\prime}$, the obtained
sequent is normalized. Such an operation is called a normalization.

###### Lemma 5.45

Assume that $\mathit{ar}_{\mathit{max}}(\mathfrak{R})\leq\kappa$, for some
fixed $\kappa\in{\mathbb{N}}$. For every sequent ${\cal S}$, the number of
sequents occurring in a proot tree with root ${\cal S}$ is polynomial w.r.t.
$|{\cal S}|+|\mathfrak{R}|$, up to normalization.

###### Proof 5.46

By definition, every descendant of ${\cal S}$ is either an  I-free descendant
of ${\cal S}$ or an  I-free descendant of some  I-reducible sequent ${\cal
S}^{\prime}$. By Condition 6 in Definition 4.43,  R applies with the highest
priority on ${\cal S}$, eventually yielding a (unique) sequent equality-free
${\cal S}^{\prime\prime}$ of the form
$\phi\curlywedge\xi\vdash_{\mathfrak{R}}^{V}\psi\curlywedge\zeta$, with
$|{\cal S}^{\prime\prime}|\leq|{\cal S}|$ and
$\mathcal{V}(\phi)\subseteq\mathcal{V}({\cal S})$. By Lemma 5.43, every
I-free sequent ${\cal S}^{\prime}$ is a companion of of $\phi\curlywedge\xi$.
By Lemma 5.39, the number of such sequents ${\cal S}^{\prime}$, after
normalization (w.r.t. ${\cal S}^{\prime\prime}$), is polynomial w.r.t.
$|\phi|+|\mathfrak{R}|$ (hence w.r.t. $|{\cal S}|+|\mathfrak{R}|$). Indeed, it
is clear that the normalized form of ${\cal S}^{\prime}$ is also a companion
of $\phi\curlywedge\xi$ and by definition it only contains variables in
$\mathcal{V}({\cal S}^{\prime\prime})\cup\\{x_{i}^{\mathtt{s}}\mid i\leq|{\cal
S}^{\prime}|\\}$. Furthermore, $|{\cal S}^{\prime}|$ is polynomial w.r.t.
$|{\cal S}|+|\mathfrak{R}|$, thus the same property holds for
$\mathit{card}(\mathcal{V}({\cal S}^{\prime}))$. Then the proof follows
immediately from Lemma 5.19.

Putting everything together, we derive the main result of the paper:

###### Theorem 5.47

The validity problem for sequents $\lambda\vdash_{\mathfrak{R}}^{V}\gamma$,
where $\mathfrak{R}$ is a $\mathtt{loc}$-deterministic set of
$\mathtt{P}$-rules with $\mathit{ar}_{\mathit{max}}(\mathfrak{R})\leq\kappa$
and $\mathit{record}_{\mathit{max}}(\mathfrak{R})\leq\kappa$, for some fixed
number $\kappa$, is in PTime.

###### Proof 5.48

By Theorems 5.21 and 5.36, $\lambda\vdash_{\mathfrak{R}}^{V}\gamma$ is valid
iff it admits a fully expanded proof tree. We first apply inductively the
inference rules in all possible ways, starting with the initial sequent
$\lambda\vdash_{\mathfrak{R}}^{V}\gamma$ and proceeding with all the
descendants of $\lambda\vdash_{\mathfrak{R}}^{V}\gamma$, until we obtain
either an axiom or a sequent that has already been considered, up to
normalization. By Lemma 5.45, the number of such descendants (up to
normalization) is polynomial w.r.t. $|{\cal S}|+|\mathfrak{R}|$, thus it
suffices to show that each inference step can be performed in polynomial time.
This can be established by an inspection of the rules. We first observe that
the set of all possible rule applications can be computed in polynomial time
w.r.t. the size of the conclusion (in particular, both the number of premises
and their size are always polynomial w.r.t. the size of the conclusion): this
is straightforward to check for all rules except for  S, for which the result
stems from Proposition 4.47. Also, it is straightforward to verify that the
application conditions of the rules can be tested in polynomial time.

Afterwards, it suffices to compute the set of provable sequents among those
that are reachable from the initial one and check whether
$\lambda\vdash_{\mathfrak{R}}^{V}\gamma$ occurs in this set. Since infinite
proof trees are allowed, we actually compute the complement of this set, i.e.,
the set of sequents that are not provable. This can be done in polynomial
time, using a straightforward fixpoint algorithm, by computing the least set
of sequents ${\cal S}$ such that, for all rule applications with conclusion
${\cal S}$, at least one of the premises is not provable. More precisely, a
sequent is not provable if it has no successor (no rule can be applied on it),
or more generally, if for all possible rule applications, at least one of the
premises is not provable.

Note that, in order to apply rule  S on a sequent that is not narrow, it is
necessary to check that the left premise is valid, and this must be done by
recursively applying the proof procedure. This is feasible because the left
premise is always narrow (since its right-hand side is a predicate atom).
Consequently, the computation of valid sequents must be performed in two
steps, first for narrow sequents, then for those that are not narrow, as the
application of the rules on non narrow sequents depends on the validity of
narrow sequents. By Proposition 4.44 all the descendants of narrow sequents
are also narrow, hence the converse does not hold, and the procedure is well-
founded.

##  6 Conclusion

A proof procedure has been devised for checking entailments between Separation
Logic formulas with spatial predicates denoting recursive data structures, for
a new class of inductive rules, called $\mathtt{loc}$-deterministic. The
soundness and completeness of the calculus have been established. The
conditions imposed on the data structures are stronger than those considered
in [14, 15] but on the other hand the procedure terminates in polynomial time,
provided the arity of the predicates is bounded. Both the considered fragment
and the proof procedure are very different from previously known polynomial-
time decision procedures for testing entailments [8, 5]. In particular, the
considered formulas may contain several non-built-in and non-compositional
predicates (in the sense of [12]), and the structures may contain unallocated
nodes, denoting data (with no predicate other than equality). In addition,
several lower bounds have been established for the entailment problem, showing
that any relaxing of the proposed conditions makes the problem untractable.

Future work includes the implementation of the procedure and the evaluation of
its practical performance. The combination with theory reasoning (to reason on
data stored inside the structures) will also be considered. In particular, it
would be interesting to define a fragment that encompasses both the
$\mathtt{loc}$-deterministic $\mathtt{P}$-rules considered in the present
paper and the SHLIDe fragment defined in [19], as the conditions defining both
classes of rules are very different and non comparable, as evidenced by the
examples and explanations given in the introduction of the paper.

## References

  * [1] Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn.  Smallfoot: Modular automatic assertion checking with separation logic.  In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever, editors, Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures, volume 4111 of Lecture Notes in Computer Science, pages 115–137. Springer, 2005.
  * [2] Josh Berdine, Byron Cook, and Samin Ishtiaq.  Slayer: Memory safety for systems-level code.  In Ganesh Gopalakrishnan andShaz Qadeer, editor, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of LNCS, pages 178–183. Springer, 2011.
  * [3] Cristiano Calcagno and Dino Distefano.  Infer: An automatic program verifier for memory safety of C programs.  In Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, volume 6617 of Lecture Notes in Computer Science, pages 459–465. Springer, 2011.
  * [4] Cristiano Calcagno, Peter W. O’Hearn, and Hongseok Yang.  Local action and abstract separation logic.  In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 366–378. IEEE Computer Society, 2007.  doi:10.1109/LICS.2007.30.
  * [5] Taolue Chen, Fu Song, and Zhilin Wu.  Tractability of separation logic with inductive definitions: Beyond lists.  In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 37:1–37:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.