$\bigvee_{i=1}^{n}(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\psi_{i}\wedge(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal
R}}\psi_{i}^{\prime}$ into conjunctive normal form, by distributing the
implication over conjunctions and by replacing the entailments of the form
$(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\phi\wedge(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal
R}}\phi^{\prime}\implies(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\Gamma\vee(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal
R}}\Gamma^{\prime}$ by the logically stronger conjunction of the two
entailments $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\phi\implies(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\Gamma$ and
$(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal
R}}\phi^{\prime}\implies(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal
R}}\Gamma^{\prime}$. Also, the application conditions of the rules ensure that
redundant sequents are discarded, such as $p(x)\vdash_{{\cal
R}}p_{1}(x),p_{2}(x)$ w.r.t. $p(x)\vdash_{{\cal R}}p_{1}(x)$.

The Existential Decomposition rule (ED) allows one to shift existential
quantifiers on the right-hand side inside separating conjunctions. This rule
is useful to allow for further applications of Rule SC. The condition
$x\not\in\mathit{fv}_{{\cal T}}(\psi^{\prime})$ can be replaced by the
stronger condition “$\psi^{\prime}$ is $\emptyset$-constrained”, which is
easier to check (one does not have to compute the set $\mathit{fv}_{{\cal
T}}(\psi^{\prime})$). All the completeness results in Section 10 also hold
with this stronger condition (and with $\xi=\chi=\mathtt{emp}$). The intuition
behind the rule is that $\psi$ denotes the part of $\gamma$ the interpretation
of which depends on the value of $x$. In most cases, this formula is unique
and $m=1$, but there are cases where several decompositions of $\gamma$ must
be considered, depending on the unfolding.

######  Example 51.

Consider a sequent $p(x,z)*p(y,y)\vdash_{{\cal R}}\exists z.(q(x,z)*r(x,z))$,
with the rules $\\{p(u,v)\Leftarrow u\mapsto(v),q(u,v)\Leftarrow
u\mapsto(v),r(u,v)\Leftarrow u\mapsto(u)\\}$. Note that the interpretation of
$r(u,v)$ does not depend on $v$. One of the premises the rule ED yields is
$p(x,z)*p(y,y)\vdash_{{\cal R}}(\exists z.q(x,z))*r(x,x^{\prime})$.
Afterwards, the rule SC can be applied, yielding for instance the premises
$p(x,z)\vdash_{{\cal R}}\exists z.q(x,z)$ and $p(y,y)\vdash_{{\cal
R}}r(x,x^{\prime})$.

The ${\cal T}$-Simplification rule (TS) allows one to simplify ${\cal
T}$-formulas, depending on some external procedure, and $\prec$ denotes a
fixed well-founded order on ${\cal T}$-formulas. We assume that
$\chi\prec\chi*\xi$ for every formula $\xi\not=\mathtt{emp}$, and that
$\chi\prec\chi^{\prime}\implies\xi*\chi\prec\xi*\chi^{\prime}$, for every
formula $\xi$. Note that TS is not necessary for the completeness proofs in
Section 10.

The ${\cal T}$-Decomposition rule (TD) shifts ${\cal T}$-formulas from the
right-hand side to the left-hand side of a sequent. In particular, the rule
applies with $\chi^{\prime}=\neg\chi$ if the theory is closed under negation.
The completeness results in Section 10 hold under this requirement.

##### Axioms.

Axioms are represented in Figure 2. The Reflexivity axiom (R) gets rid of
trivial entailments, which can be proven simply by instantiating existential
variables on the right-hand side. For the completeness proofs in Section 10,
the case where $\sigma={\mathit{i}d}$ is actually sufficient. The Disjointness
axiom (D) handles the case where the same location is allocated in two
disjoint parts of the heap. Note that (by Definition 26) the left-hand side of
the sequent is pu-free, hence $\mathit{alloc}(\phi)$ and
$\mathit{alloc}(\phi^{\prime})$ are well-defined. The ${\cal T}$-Clash axiom
(TC) handles the case where the left-hand side is unsatisfiable modulo ${\cal
T}$, while the Empty Heap axiom (EH) applies when the left-hand side is a
${\cal T}$-formula.

R:  $\phi*\chi\;\vdash_{{\cal R}}\;\exists\mathbf{z}.\psi,\,\Gamma$ if $\chi$
is a ${\cal T}$-formula and there is a substitution $\sigma$ such that
$\mathit{dom}(\sigma)=\mathbf{z}$ and $\phi=\psi\sigma$. D:
$\phi*\phi^{\prime}\;\vdash_{{\cal R}}\;\Gamma$ if
$\mathit{alloc}(\phi)\cap\mathit{alloc}(\phi^{\prime})\neq\emptyset$ TC:
$\phi*\chi\;\vdash_{{\cal R}}\;\Gamma$ if $\chi$ is a ${\cal T}$-formula and
$\chi\models_{{\cal T}}^{i}\mathtt{false}$. EH:  $\chi\;\vdash_{{\cal
R}}\;\exists\mathbf{x}_{1}.\xi_{1},\dots,\exists\mathbf{x}_{n}.\xi_{n},\Gamma$
if $\chi,\xi_{1},\dots,\xi_{n}$ are ${\cal T}$-formulas and
$\chi\models_{{\cal
T}}^{i}\exists\mathbf{x}_{1}.\xi_{1}\vee\dots\vee\exists\mathbf{x}_{n}.\xi_{n}$.
Figure 2: Axioms

### Proof Trees

######  Definition 52.

A proof tree is a possibly infinite tree, in which each node is labeled by a
sequent, and if a node is labeled by some sequent $\phi\vdash_{{\cal
R}}\Gamma$, then its successors are labeled by $\phi_{i}\vdash_{{\cal
R}}\Gamma_{i}$ with $i=1,\dots,n$, for some rule application
$\phi_{1}\vdash_{{\cal R}}\Gamma_{1}\cdots\phi_{n}\vdash_{{\cal R}}\Gamma_{n}$
$\phi\vdash_{{\cal R}}\Gamma$ . A proof tree is rational if it contains a
finite number of subtrees, up to a renaming of variables. The end-sequent of a
proof tree is the sequent labeling the root of the tree.

In practice one is of course interested in constructing rational proof trees.
Such rational proof trees can be infinite, but they can be represented
finitely. The cycles in a rational proof tree may be seen as applications of
the induction principle. We provide a simple example showing applications of
the rules.

######  Example 53.

Consider the pc-SID consisting of the following rules:

$\begin{array}[]{rcl}p(x)&\Leftarrow&\exists y,z.\,x\mapsto(y,z)*p(y)*p(z)\\\
p(x)&\Leftarrow&x\mapsto(x,x)\\\ q(x,u)&\Leftarrow&\exists
y,z.\,x\mapsto(y,z)*p(y)*q(z,u)\\\ q(x,u)&\Leftarrow&x\mapsto(u,u)\end{array}$

The proof tree $\tau(x)$ below admits the end-sequent $p(x)\vdash_{{\cal
R}}\exists u.q(x,u)$:

R $x\mapsto(x,x)\vdash_{{\cal R}}\exists u.x\mapsto(u,u)$ UR
$x\mapsto(x,x)\vdash_{{\cal R}}\exists u.q(x,u)$ $\pi(x)$ $\exists
y,z.\,x\mapsto(y,z)*p(y)*p(z)\vdash_{{\cal R}}\exists u.q(x,u)$ UL
$p(x)\vdash_{{\cal R}}\exists u.q(x,u)$

where the proof tree $\pi(x)$ with end-sequent $\exists
y,z.\,x\mapsto(y,z)*p(y)*p(z)\vdash_{{\cal R}}\exists u.q(x,u)$ is defined as
follows (using $\phi$ to denote the pu-atom
$\Phi_{p(y)*q(z,u)\mathrel{\mbox{$\mathord{-}\mathord{-}\scalebox{0.9}{$\mathord{\bullet}$}$}}q(x,u)}^{x,y,z,u}[x,y,z,u]$):

R $x\mapsto(y,z)\vdash_{{\cal R}}x\mapsto(y,z)$ UR $x\mapsto(y,z)\vdash_{{\cal
R}}\phi$ R $p(y)\vdash_{{\cal R}}p(y)$ $\tau(z)$ $p(z)\vdash_{{\cal R}}\exists
u.q(z,u)$ SC $p(y)*p(z)\vdash_{{\cal R}}p(y)*\exists u.q(z,u)$ ED
$p(y)*p(z)\vdash_{{\cal R}}\exists u.(p(y)*q(z,u))$ SC
$x\mapsto(y,z)*p(y)*p(z)\vdash_{{\cal R}}\phi*\exists u.(p(y)*q(z,u))$ ED
$x\mapsto(y,z)*p(y)*p(z)\vdash_{{\cal R}}\exists u.(\phi*p(y)*q(z,u))$ HD
$x\mapsto(y,z)*p(y)*p(z)\vdash_{{\cal R}}\exists
u.(\Phi_{p(y)\mathrel{\mbox{$\mathord{-}\mathord{-}\scalebox{0.9}{$\mathord{\bullet}$}$}}q(x,y,u)}^{x,y,u}[x,y,u]*p(y))$
HD $x\mapsto(y,z)*p(y)*p(z)\vdash_{{\cal R}}\exists u.q(x,u)$ Sk $\exists
z.x\mapsto(y,z)*p(y)*p(z)\vdash_{{\cal R}}\exists u.q(x,u)$ Sk $\exists
y,z.\,x\mapsto(y,z)*p(y)*p(z)\vdash_{{\cal R}}\exists u.q(x,u)$

For the sake of readability, root-unsatisfiable formulas are removed. For
example, the rule Sk applied above also adds sequents with formulas on the
left-hand side such as $x\mapsto(y,z)*p(x)*p(z)$. Some weakening steps are
also silently applied to dismiss irrelevant formulas from the right-hand sides
of the sequents.

Note that the formula $q(x,u)$ on the right-hand side of a sequent is not
unfolded unless this unfolding yields a single points-to atom. Unfolding
$q(x,u)$ would be possible for this set of rules because $p(x)$ and $q(x,u)$
share the same root, but in general such a strategy would not terminate.
Instead the rule HD is used to perform a partial unfolding of $q(x,u)$ with a
split on variable $y$ for the first application. The sequent
$p(z)\vdash_{{\cal R}}\exists u.q(z,u)$ is identical to the root sequent, up
to a renaming of variables. The generated proof tree is thus infinite but
rational, up to a renaming of variables.

##  9 Soundness

We prove that the calculus is sound, in the sense that the end-sequent of
every (possibly infinite, even irrational) proof tree is valid. In the entire
section, we assume that ${\cal R}$ is $\mathit{alloc}$-compatible.

######  Lemma 54.

The conclusions of the rules R, D, TC and EH are all valid.

###### Proof.

We consider each axiom separately.

  * R

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi*\chi$. Since
$\chi$ is a ${\cal T}$-formula, we also have
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$. Let
$\mathfrak{s}^{\prime}$ be a store mapping each variable $z$ to
$\mathfrak{s}(z\sigma)$. Since $\mathit{dom}(\sigma)=\mathbf{z}$,
$\mathfrak{s}$ and $\mathfrak{s}^{\prime}$ coincide on all variables not
occurring in $\mathbf{z}$. Since $\phi=\psi\sigma$, we have
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\psi\sigma$, and by definition
of $\mathfrak{s}^{\prime}$, Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\exists\mathbf{z}.\psi$.

  * D

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi*\phi^{\prime}$,
where $x\in\mathit{alloc}(\phi)\cap\mathit{alloc}(\phi^{\prime})$. Then there
exist disjoint heaps $\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ with
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$,
$(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\phi$ and
$(\mathfrak{s},\mathfrak{h}_{2})\models_{{\cal R}}\phi^{\prime}$. By Lemma 34,
since ${\cal R}$ is $\mathit{alloc}$-compatible and
$x\in\mathit{alloc}(\phi)\cap\mathit{alloc}(\phi^{\prime})$, we have
$\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{1})\cap\mathit{dom}(\mathfrak{h}_{2})$,
contradicting the fact that $\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ are
disjoint.

  * TC

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi*\chi$, where
$\chi$ is a ${\cal T}$-formula. Then by definition of the semantics we must
have $(\mathfrak{s},\emptyset)\models_{{\cal R}}\chi$, hence $\chi$ cannot be
unsatisfiable.

  * EH

If $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\chi$ then since $\chi$ is a
${\cal T}$-formula necessarily $\mathfrak{h}=\emptyset$, hence
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists\mathbf{x}_{i}.\xi_{i}$,
for some $i=1,\dots,n$, by the application condition of the rule.

∎

######  Lemma 55.

The rules HF, UL, UR, W, HD, TS, TD are sound. More precisely, if
$(\mathfrak{s},\mathfrak{h})$ is a countermodel of the conclusion of the rule,
then it is also a countermodel of at least one of the premises.

###### Proof.

We consider each rule separately:

  * HF

The proof is immediate since it is clear that
$\exists\mathbf{y}^{\prime}.(x\mapsto(z_{1},\dots,z_{\kappa})*\psi)\sigma\models_{{\cal
R}}\exists\mathbf{y}.(x\mapsto(z_{1},\dots,z_{\kappa})*\psi)$.

  * UL

Let $\alpha=p(\mathbf{x})$, and assume
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\alpha*\phi$ and
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\Gamma$. Then
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$, with
$(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\alpha$ and
$(\mathfrak{s},\mathfrak{h}_{2})\models_{{\cal R}}\phi$. By definition of the
semantics of the predicate atoms, necessarily
$(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\psi$, for some $\psi$ such
that $\alpha\Leftarrow_{{\cal R}}\psi$. By definition of
$\\{\phi_{1},\dots,\phi_{n}\\}$, there exists $i\in\\{1,\dots,n\\}$ such that
$\psi=\phi_{i}$ (modulo $\alpha$-renaming). We deduce that
$(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\phi_{i}$, and that
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi_{i}*\phi$. Therefore,
$(\mathfrak{s},\mathfrak{h})$ is a countermodel of $\phi_{i}*\phi\vdash_{{\cal
R}}\Gamma$.

  * UR

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$,
$(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\exists\mathbf{x}.(\psi_{1}*\psi),\dots,\exists\mathbf{x}.(\psi_{n}*\psi),\Gamma$
and $(\mathfrak{s},\mathfrak{h})\not\models_{{\cal
R}}\exists\mathbf{x}.(\alpha*\psi),\Gamma$. Then necessarily,
$(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\exists\mathbf{x}.(\psi_{i}*\psi)$ holds for some $i=1,\dots,n$. Thus there
exist a store $\mathfrak{s}^{\prime}$ coinciding with $\mathfrak{s}$ on all
variables not occurring in $\mathbf{x}$ and disjoint heaps $\mathfrak{h}_{i}$
(for $i=1,2$) such that $\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$,
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1})\models\psi_{i}$ and
$(\mathfrak{s}^{\prime},\mathfrak{h}_{2})\models\psi$. Since by hypothesis
$\alpha\Leftarrow_{{\cal R}}\psi_{i}$, we deduce that
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1})\models\alpha$, so that
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})\models\alpha*\psi$,
hence $(\mathfrak{s},\mathfrak{h})\models\exists\mathbf{x}.(\alpha*\psi)$,
which contradicts our assumption.

  * W

The proof is immediate, since by definition every countermodel of
$\phi\vdash_{{\cal R}}\psi,\Gamma$ is also a countermodel of
$\phi\vdash_{{\cal R}}\Gamma$.

  * HD

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ and that
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\psi$. By Lemma 49, since
$\mathrm{split}_{x}(\psi)=\\{\psi_{1},\dots,\psi_{n}\\}$, we deduce that
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\psi_{1},\dots,\psi_{n}$.

  * TS

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi*\chi^{\prime}$,
$\mathfrak{s}$ is injective and $(\mathfrak{s},\mathfrak{h})\not\models_{{\cal
R}}\Gamma$. Since $\chi$ is a ${\cal T}$-formula, this entails that
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ and
$\mathfrak{s}\models_{{\cal T}}\chi^{\prime}$, thus
$\mathfrak{s}\models_{{\cal T}}\chi^{\prime}$. By the application condition of
the rule we have $\chi^{\prime}\models_{{\cal T}}^{i}\chi$, hence
$\mathfrak{s}\models_{{\cal T}}\chi$ because $\mathfrak{s}$ is injective. We
deduce that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi*\chi$, and that
$(\mathfrak{s},\mathfrak{h})$ is a countermodel of $\phi*\chi\vdash_{{\cal
R}}\Gamma$.

  * TD

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ and
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\chi*\phi^{\prime},\Gamma$.
We distinguish two cases. If $(\mathfrak{s},\emptyset)\models_{{\cal R}}\chi$
then $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi*\chi$, since
$\mathfrak{h}=\mathfrak{h}\uplus\emptyset$. Furthermore, since
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\chi*\phi^{\prime}$,
necessarily, $(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\phi^{\prime}$
and $(\mathfrak{s},\mathfrak{h})$ is a countermodel of $\phi*\chi\vdash_{{\cal
R}}\phi^{\prime},\Gamma$. Otherwise,
$(\mathfrak{s},\emptyset)\not\models_{{\cal R}}\chi$, hence
$(\mathfrak{s},\emptyset)\models_{{\cal R}}\chi^{\prime}$ because
$\chi\vee\chi^{\prime}$ is valid, and
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi*\chi^{\prime}$. Therefore,
$(\mathfrak{s},\mathfrak{h})$ is a countermodel of
$\phi*\chi^{\prime}\vdash_{{\cal R}}\Gamma$.

∎

######  Lemma 56.

The rule SC is sound. More precisely, if $(\mathfrak{s},\mathfrak{h})$ is a
countermodel of the rule conclusion, then at least one of the premises admits
a countermodel $(\mathfrak{s},\mathfrak{h}^{\prime})$, where
$\mathfrak{h}^{\prime}$ is a proper subheap of $\mathfrak{h}$.

###### Proof.

Let $(\mathfrak{s},\mathfrak{h})$ be a countermodel of
$\phi*\phi^{\prime}\vdash_{{\cal
R}}\psi_{1}*\psi_{1}^{\prime},\dots,\psi_{n}*\psi_{n}^{\prime}$, and assume
that for every proper subheap $\mathfrak{h}^{\prime}\subset\mathfrak{h}$,
$(\mathfrak{s},\mathfrak{h}^{\prime})$ satisfies all the premises.
Necessarily, $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\phi*\phi^{\prime}$, hence there exist heaps $\mathfrak{h}_{1}$ and
$\mathfrak{h}_{2}$ such that
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$,
$(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\phi$ and
$(\mathfrak{s},\mathfrak{h}_{2})\models_{{\cal R}}\phi^{\prime}$. Furthermore,
since $\phi$ and $\phi^{\prime}$ both contain at least one spatial atom, both
$\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ must be nonempty by Proposition 13,
and are therefore both proper subheaps of $\mathfrak{h}$. Since
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\psi_{x}*\psi_{x}^{\prime}$,
for every $x\in\\{1,\dots,n\\}$, we have either
$(\mathfrak{s},\mathfrak{h}_{1})\not\models_{{\cal R}}\psi_{x}$ or
$(\mathfrak{s},\mathfrak{h}_{2})\not\models_{{\cal R}}\psi_{x}^{\prime}$. By
gathering all the indices $x$ satisfying the first assertion, we obtain a set
$X\subseteq\\{1,\dots,n\\}$ such that $x\in
X\Rightarrow(\mathfrak{s},\mathfrak{h}_{1})\not\models_{{\cal R}}\psi_{x}$
($\dagger$) and $x\in\\{1,\dots,n\\}\setminus
X\Rightarrow(\mathfrak{s},\mathfrak{h}_{2})\not\models_{{\cal
R}}\psi_{x}^{\prime}$ ($\ddagger$).

By the application condition of the rule, we have either $I_{i}\subseteq X$
for some $i\in\\{1,\dots,m\\}$, or $J_{j}\subseteq\\{1,\dots,n\\}\setminus X$
for some $j\in\\{1,\dots,l\\}$. First assume that $I_{i}\subseteq X$. Then
since $(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\phi$ and
$\mathfrak{h}_{1}$ is a proper subheap of $\mathfrak{h}$, we deduce that
$(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\bigvee_{x\in
I_{i}}\psi_{x}$, which contradicts ($\dagger$). Similarly if
$J_{j}\subseteq\\{1,\dots,n\\}\setminus X$, then, since
$(\mathfrak{s},\mathfrak{h}_{2})\models_{{\cal R}}\phi^{\prime}$ and
$\mathfrak{h}_{2}$ is a proper subheap of $\mathfrak{h}$, we have
$(\mathfrak{s},\mathfrak{h}_{2})\models_{{\cal R}}\bigvee_{x\in
J_{j}}\psi_{x}^{\prime}$, which contradicts ($\ddagger$). ∎

######  Lemma 57.

Let $\phi$ be a formula, $x$ be a variable not occurring in
$\mathit{fv}_{{\cal T}}(\phi)$ and let $(\mathfrak{s},\mathfrak{h})$ be a
model of $\phi$ such that $\mathfrak{s}(x)\not\in\mathit{loc}(\mathfrak{h})$.
Then, for every store $\mathfrak{s}^{\prime}$ coinciding with $\mathfrak{s}$
on all variables distinct from $x$, we have
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi$.

###### Proof.

The proof is by induction on the satisfiability relation. We distinguish
several cases.

  * •

If $\phi$ is a ${\cal T}$-formula then
$\mathit{fv}\left(\phi\right)=\mathit{fv}_{{\cal T}}(\phi)$, hence by
hypothesis $x\not\in\mathit{fv}\left(\phi\right)$ and
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi$.

  * •

If $\phi=x_{0}\mapsto(x_{1},\dots,x_{\kappa})$ then since
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$,
$\mathfrak{h}=\left\\{(\mathfrak{s}(x_{0}),\dots,\mathfrak{s}(x_{\kappa}))\right\\}$,
and $\mathit{loc}(\mathfrak{h})=\\{\mathfrak{s}(x_{i})\mid 0\leq
i\leq\kappa\\}$. Since $\mathfrak{s}(x)\not\in\mathit{loc}(\mathfrak{h})$ we
deduce that $\mathfrak{s}(x)\not=\mathfrak{s}(x_{i})$ for all
$i=0,\dots,\kappa$, thus $x\not=x_{i}$ and $\mathfrak{s}^{\prime}$ coincides
with $\mathfrak{s}$ on $x_{0},\dots,x_{\kappa}$. We conclude that
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi$.

  * •

Assume that $\phi$ is of the form
$\Phi_{\beta\mathrel{\mbox{$\mathord{-}\mathord{-}\scalebox{0.9}{$\mathord{\bullet}$}$}}\alpha}^{\mathbf{u}}[\mathbf{u}\theta]$.
Then there exist a formula $\exists\mathbf{y}.~{}(\beta^{\prime}*\psi)$, a
substitution $\sigma$ with $\mathit{dom}(\sigma)\subseteq\mathbf{y}$ and a
store $\hat{\mathfrak{s}}$ coinciding with $\mathfrak{s}$ on all variables not
occurring in $\mathbf{y}$ such that $\alpha\Leftarrow_{{\cal
R}}^{+}\exists\mathbf{y}.~{}(\beta^{\prime}*\psi)$,
$(\hat{\mathfrak{s}},\mathfrak{h})\models_{{\cal R}}\psi\sigma\theta$ and
$\beta=\beta^{\prime}\sigma$. We assume by $\alpha$-renaming that
$x\not\in\mathbf{y}$. Let $\hat{\mathfrak{s}}^{\prime}$ be a store coinciding
with $\hat{\mathfrak{s}}$ on all variables distinct from $x$, and such that
$\hat{\mathfrak{s}}^{\prime}(x)=\mathfrak{s}^{\prime}(x)$. By construction,
$\hat{\mathfrak{s}}^{\prime}$ coincides with $\mathfrak{s}^{\prime}$ on all
variables not occurring in $\mathbf{y}$. By definition of the extension of
$\Leftarrow_{{\cal R}}^{*}$ to formulas containing pu-atoms, we have
$\phi\Leftarrow_{{\cal R}}^{*}\exists\mathbf{y}^{\prime}.\psi\sigma\theta$,
where $\mathbf{y}^{\prime}=\mathbf{y}\setminus\mathit{dom}(\sigma)$. Assume
that $x\in\mathit{fv}_{{\cal T}}(\psi\sigma\theta)$. As $x\not\in\mathbf{y}$,
this entails that $x\in\mathit{fv}_{{\cal
T}}(\exists\mathbf{y}^{\prime}.\psi\sigma\theta)$, and by Definition 39
$x\in\mathit{fv}_{{\cal T}}(\phi)$, which contradicts the hypothesis of the
lemma. Thus $x\not\in\mathit{fv}_{{\cal T}}(\psi\sigma)$ and by the induction
hypothesis we have $(\hat{\mathfrak{s}}^{\prime},\mathfrak{h})\models_{{\cal
R}}\psi\sigma$. We deduce that
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi$.

  * •

If $\phi=\phi_{1}*\phi_{2}$ or $\phi=\phi_{1}\vee\phi_{2}$ then the result is
an immediate consequence of the induction hypothesis.

  * •

If $\phi=\exists y.~{}\psi$ then there exists a store $\hat{\mathfrak{s}}$
coinciding with $\mathfrak{s}$ on all variables distinct from $y$ such that
$(\hat{\mathfrak{s}},\mathfrak{h})\models_{{\cal R}}\psi$. Let
$\hat{\mathfrak{s}}^{\prime}$ be the store coinciding with
$\mathfrak{s}^{\prime}$ on $x$ and with $\hat{\mathfrak{s}}$ on all other
variables. By the induction hypothesis we get
$(\hat{\mathfrak{s}}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi$ thus
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi$.

∎

######  Lemma 58.

The rules Sk and ED are sound. More precisely, if
$(\mathfrak{s},\mathfrak{h})$ is a countermodel of the conclusion of the rule,
then there exists a store $\mathfrak{s}^{\prime}$ such that
$(\mathfrak{s}^{\prime},\mathfrak{h})$ is a countermodel of the premise of the
rule.

###### Proof.

We consider each rule separately.

  * Sk

Let $(\mathfrak{s},\mathfrak{h})$ be a countermodel of $\exists
x.~{}\phi\vdash_{{\cal R}}\Gamma$. Then $\mathfrak{s}$ is injective,
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists x.~{}\phi$ and
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\Gamma$. This entails that
there exists a store $\mathfrak{s}^{\prime\prime}$, coinciding with
$\mathfrak{s}$ on all variables distinct from $x$, such that
$(\mathfrak{s}^{\prime\prime},\mathfrak{h})\models_{{\cal R}}\phi$. Let
$\\{x_{1},\dots,x_{n}\\}=\mathit{fv}\left(\exists
x.\phi\right)\cup\mathit{fv}\left(\Gamma\right)$; note that by the application
condition of the rule, $x\not\in\left\\{x_{1},\dots,x_{n}\right\\}$. Assume
that there exists $i\in\\{1,\dots,n\\}$ such that
$\mathfrak{s}^{\prime\prime}(x)=\mathfrak{s}^{\prime\prime}(x_{i})=\mathfrak{s}(x_{i})$.
Then $(\mathfrak{s}^{\prime\prime},\mathfrak{h})\models_{{\cal
R}}\phi\\{x\leftarrow x_{i}\\}$, and since $\mathfrak{s}^{\prime\prime}$ and
$\mathfrak{s}$ coincide on all variables freely occurring in
$\phi\\{x\leftarrow x_{i}\\}$, we have
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\\{x\leftarrow x_{i}\\}$.
This entails that $(\mathfrak{s},\mathfrak{h})$ is a countermodel of
$\phi\\{x\leftarrow x_{i}\\}\vdash_{{\cal R}}\Gamma$, and the proof is
completed, with $\mathfrak{s}^{\prime}=\mathfrak{s}$. Otherwise, consider any
injective store $\hat{\mathfrak{s}}$ coinciding with
$\mathfrak{s}^{\prime\prime}$ on all variables in $\mathit{fv}\left(\exists
x.\phi\right)\cup\mathit{fv}\left(\Gamma\right)$ and such that
$\hat{\mathfrak{s}}(x^{\prime})=\mathfrak{s}^{\prime\prime}(x)$. Since
$(\mathfrak{s}^{\prime\prime},\mathfrak{h})\models\phi$ and
$(\mathfrak{s},\mathfrak{h})\not\models\Gamma$ we have
$(\hat{\mathfrak{s}},\mathfrak{h})\models\phi\\{x\leftarrow x^{\prime}\\}$ and
$(\hat{\mathfrak{s}},\mathfrak{h})\not\models\Gamma$. The proof is thus
completed with $\mathfrak{s}^{\prime}=\hat{\mathfrak{s}}$.

  * ED

Let $(\mathfrak{s},\mathfrak{h})$ be a countermodel of
$\phi*\phi^{\prime}\vdash_{{\cal R}}\exists\mathbf{y}.\exists
x.\gamma,\Gamma$. Then $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\phi*\phi^{\prime}$ and $(\mathfrak{s},\mathfrak{h})\not\models_{{\cal
R}}\exists\mathbf{y}.\exists x.\gamma,\Gamma$. Let $\mathfrak{s}^{\prime}$ be
an injective store coinciding with $\mathfrak{s}$ on all variables distinct
from $x^{\prime}$ and such that $\mathfrak{s}^{\prime}(x^{\prime})$ is a
location not occurring in $\mathit{loc}(\mathfrak{h})$. Since $x^{\prime}$
does not occur free in the considered sequent, we have
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi*\phi^{\prime}$,
and $(\mathfrak{s}^{\prime},\mathfrak{h})\not\models_{{\cal
R}}\exists\mathbf{y}.\exists x.\gamma,\Gamma$, so that
$(\mathfrak{s}^{\prime},\mathfrak{h})\not\models_{{\cal
R}}\exists\mathbf{y}.\gamma\\{x\leftarrow x_{i}\\}$, for every $i=1,\dots,n$.

Assume that $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal
R}}\exists\mathbf{y}.(\exists x.\psi)*\psi^{\prime}\\{x\leftarrow
x^{\prime}\\}*\xi$, for some formulas $\psi,\psi^{\prime}$ and $\chi$ such
that $\gamma=(\psi*\psi^{\prime}*\chi)$, $\chi$ and $\xi$ are ${\cal
T}$-formulas with $\xi\models\chi$, and $x\not\in\mathit{fv}_{{\cal
T}}(\psi^{\prime})\cup\mathit{fv}\left(\chi\right)$. Then there exists a store
$\mathfrak{s}^{\prime\prime}$ coinciding with $\mathfrak{s}^{\prime}$ on all
variables not occurring in $\mathbf{y}$, and disjoint heaps
$\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$,
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{1})\models_{{\cal R}}\exists
x.\psi$, $(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{2})\models_{{\cal
R}}\psi^{\prime}\\{x\leftarrow x^{\prime}\\}$ and
$(\mathfrak{s}^{\prime\prime},\emptyset)\models\xi$. This entails that there
exists a store $\hat{\mathfrak{s}}$ coinciding with
$\mathfrak{s}^{\prime\prime}$ on all variables distinct from $x$ such that
$(\hat{\mathfrak{s}},\mathfrak{h}_{1})\models_{{\cal R}}\psi$. Since
$x\not\in\mathit{fv}_{{\cal T}}(\psi^{\prime})$, necessarily,
$x^{\prime}\not\in\mathit{fv}_{{\cal T}}(\psi^{\prime}\\{x\leftarrow
x^{\prime}\\})$. By Lemma 57, since
$\mathfrak{s}^{\prime}(x^{\prime})\not\in\mathit{loc}(\mathfrak{h}_{2})$, this
entails that $(\hat{\mathfrak{s}},\mathfrak{h}_{2})\models_{{\cal
R}}\psi^{\prime}\\{x\leftarrow x^{\prime}\\}$. Now
$(\mathfrak{s}^{\prime\prime},\emptyset)\models\xi$ and by the application
condition of the rule we have $x\not\in\mathit{fv}\left(\xi\right)$, so that
$(\hat{\mathfrak{s}},\emptyset)\models_{{\cal R}}\xi$. This entails that
$(\hat{\mathfrak{s}},\emptyset)\models_{{\cal R}}\chi$ because
$\xi\models_{{\cal T}}\chi$, again by the application condition of the rule.
Hence we get $(\hat{\mathfrak{s}},\mathfrak{h})\models_{{\cal
R}}\psi*\psi^{\prime}*\chi$, and
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal
R}}\exists\mathbf{y}.\exists
x.(\psi*\psi^{\prime}*\chi)=\exists\mathbf{y}.\exists x.\gamma$, which
contradicts our assumption. We deduce that
$(\mathfrak{s}^{\prime},\mathfrak{h})$ is a countermodel of the premise.

∎

We introduce a measure on sequents. For every formula $\phi$ we denote by
${\phi}^{h}$ (resp. ${\phi}^{{\cal T}}$) the formula obtained from $\phi$ by
replacing every ${\cal T}$-formula (resp. every spatial atom) by
$\mathtt{emp}$. We denote by $N_{\exists}(\phi)$ the number of existential
quantifications in the prefix of $\phi$. For all sequents $S=\phi\vdash_{{\cal
R}}\psi_{1},\dots,\psi_{n}$, we denote by $\mu(S)$ the tuple
$\left(\mathit{size}({\phi}^{h}),\\{\mu^{\prime}(\psi_{i})\mid
i\in\\{1,\dots,n\\}\\},{\phi}^{{\cal T}}\right)$, where

$\mu^{\prime}(\psi_{i})=\left(\mathit{card}(\mathit{alloc}(\phi)\setminus\mathit{roots}_{r}(\psi_{i})),\mathit{size}({\psi_{i}}^{h}),N_{\exists}(\psi_{i}),{\psi_{i}}^{{\cal
T}}\right).$

The measure $\mu$ is ordered by the lexicographic and multiset extensions of
the natural ordering on natural numbers and of the order $\prec$ on ${\cal
T}$-formulas. We assume that all variables have the same size and that the
weights of the predicates in ${\cal P}_{S}$ are chosen in such a way that the
size of every predicate atom is strictly greater than that of all points-to
atoms.

We say that a rule with conclusion $\phi\vdash_{{\cal R}}\Gamma$ decreases
$\mu$ if the inequality $\mu(\phi\vdash_{{\cal
R}}\Gamma)>\mu(\psi\vdash_{{\cal R}}\Delta)$ holds for all the premises
$\psi\vdash_{{\cal R}}\Delta$ of the rule.

######  Lemma 59.

All the rules, except UL, decrease $\mu$.

###### Proof.

By an inspection of the rules (we refer to the definitions of the rules and of
$\mu$ for notations). The result is straightforward for the rules W, R, D and
EH. The rule Sk decreases $\mathit{size}({\phi}^{h})$, since it removes an
existential quantifier. The rule HF has no influence on the left-hand side of
the conclusion. This rule does not remove variables from
$\mathit{roots}_{r}(\psi_{i})$, because it only instantiates existential
variables and by definition, no existential variable may occur in
$\mathit{roots}_{r}(\psi_{i})$. It eliminates at least one existential
quantifier from the right-hand side of the sequence since
$\mathit{dom}(\sigma)\not=\emptyset$; hence there is a
$\mathit{size}({\psi_{i}}^{h})$ that decreases strictly. Rule UR has no
influence on the left-hand side of the conclusion and replaces a pu-atom on
the right-hand side by the conjunction of a points-to atom and a ${\cal
T}$-formula. By the above assumption on the weight of the predicate symbols,
one of $\mathit{size}({\psi_{i}}^{h})$ decreases (note that by the progress
condition the roots of $\psi_{i}$ are unchanged, hence
$\mathit{card}(\mathit{alloc}(\phi)\setminus\mathit{roots}_{r}(\psi_{i}))$
cannot increase). Rule HD decreases one of
$\mathit{card}(\mathit{alloc}(\phi)\setminus\mathit{roots}_{r}(\psi_{i}))$,
since by Proposition 48, we have
$\mathit{roots}_{r}(\psi_{i})=\\{x\\}\cup\mathit{roots}_{r}(\phi)$ for every
$\psi_{i}\in\mathrm{split}_{x}(\phi)$ (furthermore, by the application
condition of the rule, there exists $i=1,\dots,n$ such that
$x\in\mathit{alloc}(\phi)\setminus\mathit{roots}_{r}(\psi_{i})$). For rule SC,
we have $\mathit{size}({\phi}^{h})<\mathit{size}({(\phi*\phi^{\prime})}^{h})$
and
$\mathit{size}({\phi^{\prime}}^{h})<\mathit{size}({(\phi*\phi^{\prime})}^{h})$
since both $\phi$ and $\phi^{\prime}$ contain a spatial atom. Rule ED does not
affect $\mathit{alloc}(\phi)\setminus\mathit{roots}_{r}(\psi_{i})$ or
$\mathit{size}({\psi_{i}}^{h})$, and the rule reduces one of the
$N_{\exists}(\psi_{i})$, since an existential quantifier is shifted into the
scope of a separating conjunction, by the application condition of the rule
$\psi^{\prime}\not=\mathtt{emp}$. The rule TS does not affect ${\phi}^{h}$ or
the right-hand side and strictly decreases ${\phi}^{{\cal T}}$ by definition
of the rule. The rule TD does not affect ${\phi}^{h}$ and decreases one of the
${\psi_{i}}^{{\cal T}}$ (note that, since the formula $\chi$ in the rule is a
${\cal T}$-formula, no new variables may be added in $\mathit{alloc}(\psi)$).
∎

Let $wp(\phi)=2*m+l$, where $m$ (resp. $l$) denotes the number of occurrences
of points-to atoms (resp. of predicate atoms) in $\phi$. Let
$\tau(\phi\vdash_{{\cal R}}\Gamma)$ be the measure defined as follows:

$\tau(\phi\vdash_{{\cal R}}\Gamma)=(N_{h}(\phi\vdash_{{\cal
R}}\Gamma),-wp(\phi),\mu(\phi\vdash_{{\cal R}}\Gamma)),$

where $N_{h}(\phi\vdash_{{\cal R}}\Gamma)$ denotes the least size of a
countermodel of $\phi\vdash_{{\cal R}}\Gamma$, or $\infty$ if
$\phi\vdash_{{\cal R}}\Gamma$ is valid. $\tau(\phi)$ is ordered using the
lexicographic extension of the usual ordering on integers and of the ordering
on $\mu(\phi\vdash_{{\cal R}}\Gamma)$. Note that this order is well-founded on
non-valid sequents, because the number of points-to atoms in $\phi$ cannot be
greater than $N_{h}(\phi\vdash_{{\cal R}}\Gamma)$, since any countermodel must
satisfy the left-hand side of the sequent (hence $wp(\phi)\leq
2.N_{h}(\phi\vdash_{{\cal R}}\Gamma)$).

######  Lemma 60.

Let  $\phi_{1}\vdash_{{\cal R}}\Gamma_{1}\ \dots\ \phi_{n}\vdash_{{\cal
R}}\Gamma_{n}$ $\phi\vdash_{{\cal R}}\Gamma$ be a rule application. If
$\phi\vdash_{{\cal R}}\Gamma$ admits a countermodel, then there exists
$i\in\\{1,\dots,n\\}$ such that $\tau(\phi_{i}\vdash_{{\cal
R}}\Gamma_{i})<\tau(\phi\vdash_{{\cal R}}\Gamma)$.

###### Proof.

By Lemma 54 the conclusions of all axioms are valid and do not admit any
countermodel, thus the considered rule must admit at least one premise. If the
rule is ${\color[rgb]{0,0,1}{\tt SC}}$, then the result follows immediately
from Lemma 56. Rule UL does not affect the least-size of countermodels by
Lemma 55 and, since the rules are progressing, we have
$wp(p(\mathbf{x})*\phi)<wp(\phi_{i}*\phi)$. By Lemma 59, all the other rules
decrease $\mu$, and it is straightforward to check, by an inspection of the
rules, that $wp(\phi)$ cannot decrease (except for SC). By Lemmas 55 and 58,
there exists $i\in\\{1,\dots,n\\}$ such that $N_{h}(\phi_{i}\vdash_{{\cal
R}}\Gamma_{i})=N_{h}(\phi\vdash_{{\cal R}}\Gamma)$, which entails that
$\tau(\phi_{i}\vdash_{{\cal R}}\Gamma_{i})<\tau(\phi\vdash_{{\cal R}}\Gamma)$.
∎

######  Theorem 61.

(Soundness) Let ${\cal R}$ be an $\mathit{alloc}$-compatible pc-SID. If
$\phi\vdash_{{\cal R}}\Gamma$ is the end-sequent of a (possibly infinite)
proof tree, then $\phi\vdash_{{\cal R}}\Gamma$ is valid.

###### Proof.

Let  $\phi_{1}\vdash_{{\cal R}}\Gamma_{1}\ \dots\ \phi_{n}\vdash_{{\cal
R}}\Gamma_{n}$ $\phi\vdash_{{\cal R}}\Gamma$ be a rule application in the
proof tree such that $\phi\vdash_{{\cal R}}\Gamma$ is not valid. We assume,
w.l.o.g., that $\tau(\phi\vdash_{{\cal R}}\Gamma)$ is minimal. By Lemma 60,
there exists $i\in\\{1,\dots,n\\}$ such that $\tau(\phi_{i}\vdash_{{\cal
R}}\Gamma_{i})<\tau(\phi\vdash_{{\cal R}}\Gamma)$. Note that this implies that
$\phi_{i}\vdash_{{\cal R}}\Gamma_{i}$ is not valid, as otherwise we would have
$N_{h}(\phi_{i}\vdash_{{\cal R}}\Gamma_{i})=\infty>N_{h}(\phi\vdash_{{\cal
R}}\Gamma)$, contradicting the fact that $\tau(\phi_{i}\vdash_{{\cal
R}}\Gamma_{i})<\tau(\phi\vdash_{{\cal R}}\Gamma)$. Hence we get a
contradiction about the minimality of $\phi\vdash_{{\cal R}}\Gamma$. ∎

######  Remark 62.

In general, with infinite proof trees, soundness requires some well-
foundedness condition, to rule out infinite paths of invalid statements (see,
e.g., [3]). In our case, no further condition is needed because every rule
application either reduces the considered sequent into simpler ones or unfolds
a predicate atom.

##  10 Completeness And Termination Results

###  10.1 The General Case

We first show that every valid sequent admits a (possibly infinite) proof
tree. Together with Theorem 61, this result shows that the calculus can be
used as a semi-decision procedure for detecting non-validity: the procedure
will be “stuck” eventually in some branch, in the sense that one obtains a
sequent on which no rule is applicable, iff the initial sequent is non-valid.

We shall assume that all the formulas in the considered root sequent are in
prenex form. However, the sequents occurring within the proof tree will
fulfill a slightly less restrictive condition, stated below:

######  Definition 63.

A sequent $\phi\vdash_{{\cal R}}\phi_{1},\dots,\phi_{n}$ is quasi-prenex if
$\phi$ is in prenex form and all the formulas $\phi_{i}$ that are not in
prenex form are separating conjunctions of two prenex formulas.

It is easy to check that the premises of a rule with a quasi-prenex conclusion
are always quasi-prenex.

######  Lemma 64.

The rules Sk, HF, UL, HD are invertible. More precisely, if
$(\mathfrak{s},\mathfrak{h})$ is a countermodel of one of the premises then it
is also a countermodel of the conclusion.

###### Proof.

Each rule is considered separately:

  * Sk

If $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\bigvee_{i=1}^{n}\phi\\{x\leftarrow x_{i}\\}\vee\phi\\{x\leftarrow
x^{\prime}\\}$ and $(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\Gamma$,
then it is clear that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists
x.~{}\phi$, thus $(\mathfrak{s},\mathfrak{h})$ is a countermodel of $\exists
x.~{}\phi\vdash_{{\cal R}}\Gamma$.

  * HF

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}x\mapsto(y_{1},\dots,y_{\kappa})*\phi$ and
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal
R}}\exists\mathbf{y}^{\prime}.(x\mapsto(z_{1},\dots,z_{\kappa})*\psi)\sigma,\Gamma$.
If
$(\mathfrak{s},\mathfrak{h})\models\exists\mathbf{y}.(x\mapsto(z_{1},\dots,z_{\kappa})*\psi)$,
then there exist two disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ and a
store $\mathfrak{s}^{\prime}$ coinciding with $\mathfrak{s}$ on all variables
not occurring in $\mathbf{y}$ such that
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$,
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1})\models
x\mapsto(z_{1},\dots,z_{\kappa})$, and
$(\mathfrak{s}^{\prime},\mathfrak{h}_{2})\models\psi$. By the application
condition of the rule, we have
$\mathbf{y}\cap\\{x,y_{1},\dots,y_{\kappa}\\}=\emptyset$, hence
$\mathfrak{s}(x)=\mathfrak{s}^{\prime}(x)$. Since
$(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}x\mapsto(y_{1},\dots,y_{\kappa})*\phi$, we have
$\mathfrak{h}(\mathfrak{s}(x))=(\mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{\kappa}))$,
thus $\mathfrak{s}^{\prime}(z_{i})=\mathfrak{s}(y_{i})$, for all
$i=1,\dots,\kappa$. If $z_{i}\in\mathit{dom}(\sigma)$ then by definition we
have $z_{i}\sigma=y_{i}$ so that
$\mathfrak{s}^{\prime}(z_{i}\sigma)=\mathfrak{s}^{\prime}(y_{i})=\mathfrak{s}(y_{i})=\mathfrak{s}^{\prime}(z_{i})$.
We deduce that for all variables $y$,
$\mathfrak{s}^{\prime}(y\sigma)=\mathfrak{s}^{\prime}(y)$ and by Proposition
25, $(\mathfrak{s}^{\prime},\mathfrak{h}_{1})\models
x\mapsto(z_{1},\dots,z_{\kappa})\sigma$ and
$(\mathfrak{s}^{\prime},\mathfrak{h}_{2})\models\psi\sigma$. We now show that
no variable occurring in $(x\mapsto(z_{1},\dots,z_{\kappa})*\psi)\sigma$ but
not in $\mathbf{y}^{\prime}$ can occur in $\mathbf{y}$. Consider a variable
$z^{\prime}$ that occurs in $(x\mapsto(z_{1},\dots,z_{\kappa})*\psi)\sigma$
but not in $\mathbf{y}^{\prime}$. Then $z^{\prime}$ is of the form $z\sigma$
and we distinguish two cases. If $z\in\mathit{dom}(\sigma)$ then since
$\mathbf{y}\cap\\{x,y_{1},\dots,y_{\kappa}\\}=\emptyset$, we have the result.
Otherwise, since $\mathbf{y}^{\prime}$ is the vector of variables occurring in
$\mathbf{y}$ but not in $\mathit{dom}(\sigma)$, we deduce that $z^{\prime}$
cannot occur in $\mathbf{y}$ either. We deduce that $\mathfrak{s}$ and
$\mathfrak{s}^{\prime}$ coincide on all variables occurring in
$(x\mapsto(z_{1},\dots,z_{\kappa})*\psi)\sigma$ but not in
$\mathbf{y}^{\prime}$. This entails that
$(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\exists\mathbf{y}^{\prime}.(x\mapsto(z_{1},\dots,z_{\kappa})*\psi)\sigma$,
which contradicts our assumption.

  * UL

Assume that $(\mathfrak{s},\mathfrak{h})$ is a countermodel of
$\phi_{i}*\phi\models_{{\cal R}}\Gamma$, for some $i\in\\{1,\dots,n\\}$, say,
$i=1$. Then $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi_{1}*\phi$ and
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\Gamma$. We deduce that
there exist disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$,
$(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\phi_{1}$ and
$(\mathfrak{s},\mathfrak{h}_{2})\models_{{\cal R}}\phi$. By definition of the
semantics of the predicate atom, since $\alpha\Leftarrow_{{\cal R}}\phi_{1}$,
we have $(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\alpha$, thus
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\alpha*\phi$. Therefore,
$(\mathfrak{s},\mathfrak{h})$ is a countermodel of $\alpha*\phi\vdash_{{\cal
R}}\Gamma$.

  * HD

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ and that
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\psi_{1},\dots,\psi_{n}$. By
the application condition of the rule, we have $x\in\mathit{alloc}(\phi)$,
thus, by Lemma 34, necessarily $\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h})$.
Since $\mathfrak{s}$ is injective by hypothesis, we deduce by Lemma 49 that
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\psi$.

∎

######  Theorem 65.

If ${\cal T}$ is closed under negation, then for all valid disjunction-free,
prenex and $\mathit{alloc}$-compatible sequents $\phi\vdash_{{\cal R}}\Gamma$
there exists a (possibly infinite and irrational) proof tree with end-sequent
$\phi\vdash_{{\cal R}}\Gamma$.

###### Proof.

It suffices to show that for every valid, disjunction-free, quasi-prenex
sequent $\phi\vdash_{{\cal R}}\Gamma$ there exists a rule application with
conclusion $\phi\vdash_{{\cal R}}\Gamma$ such that all the premises are valid;
this ensures that an infinite proof tree can be constructed in an iterative
way. Note that in particular this property holds if an invertible rule is
applicable on $\phi\vdash_{{\cal R}}\Gamma$, since all premises are valid in
this case. The sequence $\Gamma$ can be written as
$\exists\mathbf{x}_{1}.\psi_{1},\dots,\exists\mathbf{x}_{n}.\psi_{n}$ where no
$\psi_{i}$ is an existential formula. If $\phi$ contains an existential
variable or a predicate atom then one of the rules Sk or UL applies and both
rules are invertible, by Lemma 64. Thus we may assume that $\phi$ is of the
form $x_{1}\mapsto\mathbf{y}_{1}*\dots*x_{m}\mapsto\mathbf{y}_{m}*\chi$, where
$\chi$ is a ${\cal T}$-formula. Since by Lemma 64 HF and HD are invertible, we
may assume that $\phi\vdash_{{\cal R}}\Gamma$ is irreducible w.r.t. these
rules (and also w.r.t. the axioms D, TC, R and EH). Note that for every model
$(\mathfrak{s},\mathfrak{h})$ of $\phi$,
$\mathit{card}(\mathit{dom}(\mathfrak{h}))=m$. By irreducibility w.r.t. D and
TC, we assume that the variables $x_{1},\dots,x_{m}$ are pairwise distinct,
and that $\chi$ is satisfiable (on injective structures), so that $\phi$
admits an injective model.

If $m=0$, then $\phi$ is a ${\cal T}$-formula and every model of $\phi$ must
be of the form $(\mathfrak{s},\emptyset)$. Let $I$ be the set of indices
$i\in\\{1,\dots,n\\}$ such that $\psi_{i}$ is a ${\cal T}$-formula. Since
$\phi\vdash_{{\cal R}}\Gamma$ is valid, for every model
$(\mathfrak{s},\emptyset)$ of $\phi$, there exists an $i\in\\{1,\dots,n\\}$
such that $(\mathfrak{s},\emptyset)\models\exists\mathbf{x}_{i}.\psi_{i}$. By
Proposition 13, $\psi_{i}$ cannot contain any spatial atom, and therefore
$i\in I$. Therefore, $\phi\models\bigvee_{i\in
I}\exists\mathbf{x}_{i}.\psi_{i}$ and rule EH applies, which contradicts our
assumption.

We now assume that $m>0$. Since HD is not applicable on $\phi\vdash_{{\cal
R}}\Gamma$, for every $i=1,\dots,n$, and $j=1,\dots,m$, $\psi_{i}$ is such
that $x_{j}\in\mathit{roots}_{r}(\psi_{i})$. Assume that there exists
$i\in\\{1,\dots,n\\}$ such that $\psi_{i}$ is of the form
$\alpha*\phi_{i}^{\prime}$, where $\mathit{roots}_{r}(\alpha)=\\{x_{1}\\}$ and
$\alpha$ is a pu-atom. Then the rule UR applies on $\alpha*\phi_{i}^{\prime}$,
yielding a premise of the form $\phi\vdash_{{\cal
R}}\gamma_{1},\dots,\gamma_{p},\Gamma^{\prime}$, where $\Gamma^{\prime}$ is
the sequence of formulas $\exists\mathbf{x}_{j}.\psi_{j}$ with $j\not=i$. We
show that this premise is valid. Assume for the sake of contradiction that it
admits a countermodel $(\mathfrak{s},\mathfrak{h})$. Then
$(\mathfrak{s},\mathfrak{h})\models\phi$, and since $\phi\vdash_{{\cal
R}}\Gamma$ is valid, necessarily, $(\mathfrak{s},\mathfrak{h})\models\Gamma$.
But $(\mathfrak{s},\mathfrak{h})\not\models\Gamma^{\prime}$, hence
$(\mathfrak{s},\mathfrak{h})\models\exists\mathbf{x}_{i}.\psi_{i}$ and there
exists a store $\mathfrak{s}^{\prime}$ coinciding with $\mathfrak{s}$ on all
variables not occurring in $\mathbf{x}_{i}$ and heaps
$\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$,
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1})\models\alpha$ and
$(\mathfrak{s}^{\prime},\mathfrak{h}_{2})\models\phi_{i}^{\prime}$. This
entails that $\alpha\Leftarrow_{{\cal R}}^{+}\exists\mathbf{u}.\psi$, and
there exists a store $\mathfrak{s}^{\prime\prime}$ coinciding with
$\mathfrak{s}^{\prime}$ on all variables not occurring in $\mathbf{u}$, and a
substitution $\sigma$ such that $\mathit{dom}(\sigma)\subseteq\mathbf{u}$ and
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{1})\models\psi\sigma$. W.l.o.g.,
we assume that $\psi$ contains no predicate symbol. The formula
$\phi_{i}^{\prime}$ contains at least $m-1$ spatial atoms (one atom for each
variable $x_{2},\dots,x_{m}$), hence
$\mathit{card}(\mathit{dom}(\mathfrak{h}_{2}))\geq m-1$, since by Proposition
23, every such atom allocates at least one variable. We deduce that
$\mathit{card}(\mathit{dom}(\mathfrak{h}_{1}))\leq\mathit{card}(\mathit{dom}(\mathfrak{h}))-(m-1)=1$.
This entails by Proposition 23 that $\psi$ contains at most one spatial atom,
and since $\psi$ contains no predicate atom, this atom must be a points-to
atom. Because of the progress condition, each unfolding of a predicate atom
introduces exactly one points-to atom, thus the derivation from $\alpha$ to
$\exists\mathbf{u}.\psi$ is of length $1$, i.e., we have
$\alpha\Leftarrow_{{\cal R}}\exists\mathbf{u}.\psi$. By definition of the rule
UR, the formula $\exists\mathbf{x}_{i}.\exists\mathbf{u}^{\prime}.\psi\sigma$,
occurs in $\gamma_{1},\dots,\gamma_{p}$ (where $\mathbf{u}^{\prime}$ is
defined in the rule UR), thus
$(\mathfrak{s},\mathfrak{h})\models\gamma_{1},\dots,\gamma_{p}$ and the
premise is therefore valid.

We now assume that every formula $\psi_{i}$ is of the form
$x_{1}\mapsto\mathbf{z}_{i}*\psi_{i}^{\prime}$. First suppose that
$\mathbf{z}_{i}\cap\mathbf{x}_{i}\not=\emptyset$, for some $i=1,\dots,n$. If
for all models $(\hat{\mathfrak{s}},\hat{\mathfrak{h}})$ of $\phi$ such that
$\hat{\mathfrak{s}}$ is injective, we have
$(\hat{\mathfrak{s}},\hat{\mathfrak{h}})\not\models\exists\mathbf{x}_{i}.\psi_{i}$,
then we may apply the rule W, to remove the formula
$\exists\mathbf{x}_{i}.\psi_{i}$ and obtain a premise that is valid. Thus we
assume that
$(\hat{\mathfrak{s}},\hat{\mathfrak{h}})\models\exists\mathbf{x}_{i}.\psi_{i}$
for at least one model $(\hat{\mathfrak{s}},\hat{\mathfrak{h}})$ of $\phi$
such that $\hat{\mathfrak{s}}$ is injective. Then we have
$\hat{\mathfrak{h}}(\hat{\mathfrak{s}}(x_{1}))=\hat{\mathfrak{s}}(\mathbf{y}_{1})$,
and there exists a store $\hat{\mathfrak{s}}^{\prime}$ coinciding with
$\hat{\mathfrak{s}}$ on all variables not occurring in $\mathbf{x}_{i}$ such
that
$\hat{\mathfrak{h}}(\hat{\mathfrak{s}}(x_{1}))=\hat{\mathfrak{s}}^{\prime}(\mathbf{z}_{i})$,
hence
$\hat{\mathfrak{s}}^{\prime}(\mathbf{z}_{i})=\hat{\mathfrak{s}}(\mathbf{y}_{1})$.
Since $\hat{\mathfrak{s}}$ is injective, this entails that there exists a
substitution $\sigma_{i}$ with domain $\mathbf{z}_{i}\cap\mathbf{x}_{i}$ such
that $\sigma_{i}(\mathbf{z}_{i})=\mathbf{y}_{1}$. Since
$\mathbf{z}_{i}\cap\mathbf{x}_{i}\not=\emptyset$ we have
$\mathit{dom}(\sigma_{i})\not=\emptyset$, thus the rule HF applies, and the
proof is completed.

We now assume that $\mathbf{z}_{i}\cap\mathbf{x}_{i}=\emptyset$, for all
$i=1,\dots,n$. If $\mathbf{x}_{i}$ is not empty then ED applies. Indeed, by
letting $\gamma=\psi_{i}$, $m=1$, $\chi=\xi=\mathtt{emp}$,
$\psi=\psi_{i}^{\prime}$ and $\psi^{\prime}=(x_{1}\mapsto\mathbf{z}_{i})$, the
application conditions of the rule are fulfilled because
$\mathtt{emp}\models_{{\cal T}}\mathtt{emp}$ and $\mathit{fv}_{{\cal
T}}(x_{1}\mapsto\mathbf{z}_{i})\cup\mathit{fv}\left(\xi\right)=\emptyset$. The
application of ED shifts all variables $\mathbf{x}_{i}$ behind the formula
$\psi_{i}^{\prime}$. Note that this application of the rule preserves the
validity of the sequent, because $x_{1}\mapsto\mathbf{z}_{i}$ contains no
variable in $\mathbf{x}_{i}$.

We finally assume that every $\mathbf{x}_{i}$ is empty, and therefore that
$\Gamma$ is of the form
$x_{1}\mapsto\mathbf{z}_{1}*\psi_{1}^{\prime},\dots,x_{1}\mapsto\mathbf{z}_{n}*\psi_{n}^{\prime}$.
We distinguish two cases.

  * •

$m=1$. If there exists $i\in\\{1,\dots,n\\}$ such that $\psi_{i}^{\prime}$ is
a ${\cal T}$-formula (other than $\mathtt{emp}$) then the rule TD applies,
since ${\cal T}$ is closed under negation (by letting $\chi=\psi_{i}^{\prime}$
and $\chi^{\prime}=\neg\psi_{i}^{\prime}$). Moreover, it is clear that the
obtained sequent is valid. Now let $i\in\\{1,\dots,n\\}$ and suppose
$\psi_{i}^{\prime}$ is not a ${\cal T}$-formula. Then all the models of
$\psi_{i}$ are of size at least $2$, and thus no model of $\phi$ can satisfy
$\psi_{i}$, since $\phi$ admits only models of cardinality $m=1$. Similarly,
if $\mathbf{z}_{i}\not=\mathbf{y}_{1}$, then for all injective models
$(\mathfrak{s},\mathfrak{h})$ of $\psi_{i}$ we have
$\mathfrak{h}(\mathfrak{s}(x_{1}))=\mathfrak{s}(\mathbf{z}_{i})\not=\mathfrak{s}(\mathbf{y}_{1})$,
thus $(\mathfrak{s},\mathfrak{h})\not\models\phi$. Since $\phi\vdash_{{\cal
R}}\Gamma$ is valid and $\phi$ is satisfiable, this entails that there exists
$i=1,\dots,n$ such that $\psi_{i}^{\prime}=\mathtt{emp}$ and
$\mathbf{z}_{i}=\mathbf{y}_{1}$. Then rule R applies.

  * •

$m\geq 2$. Let $I$ be the set of indices $i$ such that
$\mathbf{z}_{i}=\mathbf{y}_{1}$ and $\psi_{i}^{\prime}$ contains at least one
spatial atom. We apply rule SC, with the decompositions
$\phi=(x_{1}\mapsto\mathbf{y}_{1})*(x_{2}\mapsto\mathbf{y}_{2}*\dots*x_{m}\mapsto\mathbf{y}_{m}*\chi)$
and $\psi_{i}=x_{1}\mapsto\mathbf{z}_{i}*\psi_{i}^{\prime}$ and with the sets
$\\{\\{i\\}\mid i\in I\\}$ and $I$. It is clear that these sets satisfy the
application condition of the rule: indeed, for every
$X\subseteq\\{1,\dots,n\\}$, either $X\cap I\not=\emptyset$ and then
$\\{i\\}\subseteq X$ for some $i\in I$, or $\\{1,\dots,n\\}\setminus
X\supseteq I$. This yields the two premises:
$x_{1}\mapsto\mathbf{y}_{1}\vdash_{{\cal R}}x_{1}\mapsto\mathbf{y}_{1}$ (more
precisely this premise is obtained $\mathit{card}(I)$ times) and
$\phi^{\prime}\vdash_{{\cal R}}\Gamma^{\prime\prime}$, where
$\phi^{\prime}=x_{2}\mapsto\mathbf{y}_{2}*\dots*x_{m}\mapsto\mathbf{y}_{m}*\chi$
and $\Gamma^{\prime\prime}$ is the sequence of formulas $\psi_{i}^{\prime}$
for $i\in I$. We prove that these premises are all valid. This is
straightforward for the former one. Let $(\mathfrak{s},\mathfrak{h})$ be an
injective model of $\phi^{\prime}$. Since the $x_{1},\dots,x_{m}$ are
distinct, the heaps $\mathfrak{h}$ and
$\mathfrak{h}^{\prime}=\\{(\mathfrak{s}(x_{1}),\mathfrak{s}(\mathbf{y}_{1}))\\}$
are disjoint, and we have
$(\mathfrak{s},\mathfrak{h}\uplus\mathfrak{h}^{\prime})\models\phi$, thus
$(\mathfrak{s},\mathfrak{h}\uplus\mathfrak{h}^{\prime})\models
x_{1}\mapsto\mathbf{z}_{j}*\psi_{j}^{\prime}$, for some $j\in\\{1,\dots,m\\}$.
This entails that $\mathfrak{s}(\mathbf{z}_{j})=\mathfrak{s}(\mathbf{y}_{1})$
(hence $\mathbf{y}_{1}=\mathbf{z}_{j}$ since $\mathfrak{s}$ is injective) and
that $(\mathfrak{s},\mathfrak{h})\models\psi_{j}^{\prime}$. Since $m\geq 2$
necessarily $\mathfrak{h}\not=\emptyset$, thus $\psi_{j}^{\prime}$ contains a
spatial atom. Since $\mathbf{y}_{1}=\mathbf{z}_{j}$, this entails that $j\in
I$, hence the proof is completed.

∎

The calculus is a decision procedure for sequents in which the rules defining
the left-hand side terminate, if ${\cal T}$ is closed under negation and some
decision procedure exists for checking entailments between ${\cal
T}$-formulas:

######  Definition 66.

A sequent $\phi\vdash_{{\cal R}}\Gamma$ is left-terminating iff for every
predicate $p\in{\cal P}_{S}$ such that $\phi\geq_{{\cal R}}p$, we have
$p\not\geq_{{\cal R}}p$.

######  Lemma 67.

Every proof tree with a left-terminating end-sequent is finite.

###### Proof.

Let $\tau$ be a proof tree with a left-terminating end-sequent
$\phi\vdash_{{\cal R}}\Gamma$. By hypothesis, $\geq_{{\cal R}}$ is an order on
the set of predicates $p$ such that $\phi\geq_{{\cal R}}p$. Thus we may assume
in the definition of the measure $\mu$ that the weight of any such predicate
$p$ is strictly greater than the size of every formula $\psi$ such that
$p(\mathbf{x})\Leftarrow\psi$ is a rule in ${\cal R}$. Then every application
of a rule UL on an atom of the form $p(\mathbf{y})$ with $\phi\geq_{{\cal
R}}p$ strictly decreases $\mu$. Furthermore, since the rule UL is the only
rule that can add new predicate atoms on the left-hand side of the sequent, it
is easy to check that $\phi\geq_{{\cal R}}q$ holds for every atom
$q(\mathbf{y})$ occurring on the left-hand side of a sequent in $\tau$.
Consequently, we deduce by Lemma 59 that all the rules decrease $\mu$, which
entails that $\tau$ is finite, since $\mu$ is well-founded. ∎

######  Theorem 68.

If ${\cal T}$ is closed under negation, then for every valid disjunction-free,
pu-free, $\mathit{alloc}$-compatible and left-terminating sequent
$\phi\vdash_{{\cal R}}\Gamma$ there exists a finite proof tree of end-sequent
$\phi\vdash_{{\cal R}}\Gamma$.

###### Proof.

This is an immediate consequence of Theorem 65 and Lemma 67. ∎

###  10.2 Entailments Without Theories

In this section, we show that every valid, $\emptyset$-constrained sequent
admits a rational proof tree. This shows that the calculus is a decision
procedure for $\emptyset$-constrained sequents, and also, using the reduction
in Theorem 42, for $\\{\approx,\not\approx\\}$-constrained sequents. We first
introduce a notion of strong validity:

######  Definition 69.

A sequent $\phi\vdash_{{\cal R}}\Gamma$ is strongly valid relatively to a
decomposition $\phi=\phi_{1}*\phi_{2}$ (modulo AC) if, for every structure
$(\mathfrak{s},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})$ such that:

  * •

$\mathfrak{s}$ is injective,

  * •

$(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}\phi_{i}$ and

  * •

$x\in\mathit{alloc}(\phi_{i})$ whenever
$\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{i})$ for $i=1,2$,

there exists a formula of the form $\exists\mathbf{x}.(\psi_{1}*\psi_{2})$ in
$\Gamma$ and a store $\mathfrak{s}^{\prime}$ coinciding with $\mathfrak{s}$ on
every variable not occurring in $\mathbf{x}$ such that
$(\mathfrak{s}^{\prime},\mathfrak{h}_{i})\models_{{\cal R}}\psi_{i}$ for
$i=1,2$.

Using Lemma 72 below, it is possible to show that if a $\emptyset$-constrained
sequent is strongly valid then it is also valid, but the converse does not
hold. The intuition is that in a strongly valid sequent, the decomposition of
the heap associated with the separating conjunction on the left-hand side
corresponds to a syntactic decomposition of a formula on the right-hand side.
Note that the notion of strong validity is relative to a decomposition
$\phi=\phi_{1}*\phi_{2}$ which will always be clear from the context. For
instance, the sequent $\mathtt{ls}(x,y)*\mathtt{ls}(y,z)\vdash_{{\cal
R}}\mathtt{ls}(x,z)$ is valid (where $\mathtt{ls}$ is defined as in Example
47), but not strongly valid, because the decomposition of the left-hand side
does not correspond to any decomposition of the right-hand side. On the other
hand, $\mathtt{ls}(x,y)*\mathtt{ls}(y,z)\vdash_{{\cal R}}\exists
u.~{}(\mathtt{ls}(x,u)*\mathtt{ls}(u,z))$ is strongly valid.

######  Definition 70.

Let $\mathfrak{h}$ be a heap. For any mapping $\eta:{\cal L}\rightarrow{\cal
L}$ that is injective on $\mathit{dom}(\mathfrak{h})$, we denote by
$\eta(\mathfrak{h})$ the heap
$\\{(\eta(\ell_{0}),\dots,\eta(\ell_{\kappa}))\mid(\ell_{0},\dots,\ell_{n})\in\mathfrak{h}\\}$.

######  Proposition 71.

Let $(\mathfrak{s},\mathfrak{h})$ be a structure and let $\eta:{\cal
L}\rightarrow{\cal L}$ be a mapping that is injective on
$\mathit{dom}(\mathfrak{h})$. If $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\psi$ and $\psi$ is $\emptyset$-constrained then
$(\eta\circ\mathfrak{s},\eta(\mathfrak{h}))\models_{{\cal R}}\psi$.

###### Proof.

We prove the result by induction on the satisfiability relation
$\models_{{\cal R}}$.

  * •

Assume that
$\psi=\Phi_{\beta\mathrel{\mbox{$\mathord{-}\mathord{-}\scalebox{0.9}{$\mathord{\bullet}$}$}}\alpha}^{\mathbf{u}}[\mathbf{u}\theta]$,
$\alpha\Leftarrow_{{\cal R}}^{+}\exists\mathbf{x}.(\gamma*\beta^{\prime})$,
and there exists a store $\mathfrak{s}^{\prime}$ coinciding with
$\mathfrak{s}$ on all variables not occurring in $\mathbf{x}$ and a
substitution $\sigma$ such that
$\mathit{dom}(\sigma)\subseteq\mathbf{x}\cap\mathit{fv}\left(\beta^{\prime}\right)$,
$\beta=\beta^{\prime}\sigma$ and
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\gamma\sigma\theta$. By
the induction hypothesis we get
$(\eta\circ\mathfrak{s}^{\prime},\eta(\mathfrak{h}))\models_{{\cal
R}}\gamma\sigma\theta$. But $\eta\circ\mathfrak{s}^{\prime}$ coincides with
$\eta\circ\mathfrak{s}$ on all variables not occurring in $\mathbf{x}$, thus
$(\eta\circ\mathfrak{s},\eta(\mathfrak{h}))\models_{{\cal
R}}\Phi_{\beta\mathrel{\mbox{$\mathord{-}\mathord{-}\scalebox{0.9}{$\mathord{\bullet}$}$}}\alpha}^{\mathbf{u}}[\mathbf{u}\theta]=\psi$.

  * •

If $\psi=\mathtt{emp}$ then $\mathfrak{h}=\emptyset$, hence
$\eta(\mathfrak{h})=\emptyset$ and
$(\eta\circ\mathfrak{s},\eta(\mathfrak{h}))\models_{{\cal R}}\psi$.

  * •

If $\psi=(x\mapsto(y_{1},\dots,y_{\kappa})$ and
$\mathfrak{h}=\\{(\mathfrak{s}(x),\mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{\kappa}))\\}$,
then
$\eta(\mathfrak{h})=\\{(\eta(\mathfrak{s}(x)),\eta(\mathfrak{s}(y_{1})),\dots,\eta(\mathfrak{s}(y_{\kappa})))\\}$,
so that $(\eta\circ\mathfrak{s},\eta(\mathfrak{h}))\models_{{\cal R}}\phi$.

  * •

Assume that $\psi=\phi_{1}*\phi_{2}$ and that there exist disjoint heaps
$\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that
$\mathfrak{h}=\mathfrak{h}_{1}\uplus\mathfrak{h}_{2}$ and
$(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}\phi_{i}$. By the induction
hypothesis, we deduce that
$(\eta\circ\mathfrak{s},\eta(\mathfrak{h}_{i}))\models_{{\cal R}}\phi_{i}$. It
is clear that
$\eta(\mathfrak{h})=\eta(\mathfrak{h}_{1})\uplus\eta(\mathfrak{h}_{2})$, hence
$(\eta\circ\mathfrak{s},\eta(\mathfrak{h}))\models_{{\cal
R}}\phi_{1}*\phi_{2}$.

  * •

The proof is similar if $\psi=\phi_{1}\vee\phi_{2}$ and
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi_{i}$, for some $i=1,2$.

  * •

Assume that $\psi=\exists x.\gamma$ and that there exists a store
$\mathfrak{s}^{\prime}$, coinciding with $\mathfrak{s}$ on all variables
distinct from $x$, such that
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\gamma$. By the
induction hypothesis, we have
$(\eta\circ\mathfrak{s}^{\prime},\eta(\mathfrak{h}))\models_{{\cal R}}\gamma$.
Now, $\eta(\mathfrak{s}^{\prime})$ coincides with $\eta(\mathfrak{s})$ on all
variables distinct from $x$, therefore
$(\eta\circ\mathfrak{s},\eta(\mathfrak{h}))\models_{{\cal R}}\psi$.

∎

######  Lemma 72.

Let $\phi\vdash_{{\cal R}}\Gamma$ be a $\emptyset$-constrained sequent, where
$\phi$ is disjunction-free. If $\phi\vdash_{{\cal R}}\Gamma$ admits a
countermodel $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})$, then there
exists a structure $(\mathfrak{s},\mathfrak{h})$ satisfying the following
properties:

  * •

$(\mathfrak{s},\mathfrak{h})$ is a countermodel of $\phi\vdash_{{\cal
R}}\Gamma$;

  * •

for all variables $x$:
$x\not\in\mathit{alloc}(\phi)\implies\mathfrak{s}(x)\not\in\mathit{dom}(\mathfrak{h})$;

  * •

there exists an injective mapping $\eta$ such that
$\mathfrak{s}^{\prime}=\eta\circ\mathfrak{s}$ and
$\mathfrak{h}^{\prime}=\eta(\mathfrak{h})$.

###### Proof.

Since $\phi$ is $\emptyset$-constrained, we have $\phi\Leftarrow_{{\cal
R}}^{*}\exists\mathbf{x}.x_{1}\mapsto\mathbf{y}_{1}*\dots*x_{n}\mapsto\mathbf{y}_{n}$
and
$\mathfrak{h}^{\prime}=\\{(\mathfrak{s}^{\prime\prime}(x_{i}),\mathfrak{s}^{\prime\prime}(\mathbf{y}_{i}))\mid
1\leq i\leq n\\}$, for some store $\mathfrak{s}^{\prime\prime}$ coinciding
with $\mathfrak{s}^{\prime}$ on all variables not occurring in $\mathbf{x}$.
We assume, w.l.o.g., that ${\cal
L}\setminus\mathit{img}(\mathfrak{s}^{\prime})$ is infinite. Modulo
$\alpha$-renaming, we may also assume that
$\mathit{fv}\left(\phi\right)\cap\mathbf{x}=\emptyset$. Since ${\cal R}$ is
$\mathit{alloc}$-compatible, we have

$\begin{array}[]{rcl}\mathit{alloc}(\phi)&=&\mathit{alloc}(\exists\mathbf{x}.x_{1}\mapsto\mathbf{y}_{1}*\dots*x_{n}\mapsto\mathbf{y}_{n})\\\
&=&\\{x_{1},\dots,x_{n}\\}\cap\mathit{fv}\left(\phi\right)\\\
&=&\\{x_{1},\dots,x_{n}\\}\setminus\mathbf{x}.\end{array}$

Let $\mathfrak{s}$ be a store mapping all variables to pairwise distinct
locations not occurring in
$\mathit{loc}(\mathfrak{h})\cup\mathit{img}(\mathfrak{s}^{\prime\prime})$.
Note that $\mathfrak{s}$ is injective by construction. Let
$\hat{\mathfrak{s}}$ be the store mapping each variable $x\in\mathbf{x}$ to
$\mathfrak{s}^{\prime\prime}(x)$ and coinciding with $\mathfrak{s}$ on all
other variables. It is clear that $\hat{\mathfrak{s}}$ is injective, thus the
heap
$\mathfrak{h}=\\{(\hat{\mathfrak{s}}(x_{i}),\hat{\mathfrak{s}}(\mathbf{y}_{i}))\mid
1\leq i\leq n\\}$ is well-defined, and by construction,
$(\hat{\mathfrak{s}},\mathfrak{h})\models_{{\cal
R}}x_{1}\mapsto\mathbf{y}_{1}*\dots*x_{n}\mapsto\mathbf{y}_{n}$, so that
$({\mathfrak{s}},\mathfrak{h})\models_{{\cal R}}\phi$. Consider the function
$\eta$ that maps each location $\mathfrak{s}(x)$ to $\mathfrak{s}^{\prime}(x)$
and leaves all other locations unchanged. Note that $\eta$ is injective
because both $\mathfrak{s}$ and $\mathfrak{s}^{\prime}$ are injective, and by
definition, $\mathfrak{s}^{\prime}=\eta\circ\mathfrak{s}$. Let $x$ be a
variable. If $x\in\mathbf{x}$ then
$\hat{\mathfrak{s}}(x)=\mathfrak{s}^{\prime\prime}(x)$, hence
$(\eta\circ\hat{\mathfrak{s}})(x)=\eta(\mathfrak{s}^{\prime\prime}(x))$. By
definition of $\mathfrak{s}$ we have
$\mathfrak{s}^{\prime\prime}(x)\not\in\mathit{img}(\mathfrak{s})$, hence
$\eta(\mathfrak{s}^{\prime\prime}(x))=\mathfrak{s}^{\prime\prime}(x)$ and we
deduce that $(\eta\circ\hat{\mathfrak{s}})(x)=\mathfrak{s}^{\prime\prime}(x)$.
If $x\not\in\mathbf{x}$ then $\hat{\mathfrak{s}}(x)=\mathfrak{s}(x)$ and
$\mathfrak{s}^{\prime\prime}(x)=\mathfrak{s}^{\prime}(x)$, thus again
$(\eta\circ\hat{\mathfrak{s}})(x)=\mathfrak{s}^{\prime\prime}(x)$. We deduce
that $\mathfrak{h}^{\prime}=\eta(\mathfrak{h})$. If
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\Gamma$ then by Proposition 71
we have $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\models_{{\cal
R}}\Gamma$, which contradicts the definition of
$(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})$. Thus
$(\mathfrak{s},\mathfrak{h})$ is a countermodel of $\phi\vdash_{{\cal
R}}\Gamma$, and by construction, for all variables $x$,
$x\not\in\mathit{alloc}(\phi)\implies\mathfrak{s}(x)\not\in\mathit{dom}(\mathfrak{h})$.
∎

######  Lemma 73.

Let $\phi\vdash_{{\cal R}}\Gamma$ be a $\emptyset$-constrained and non-valid
sequent, where $\phi$ is disjunction-free. Let $\mathfrak{s}$ be an injective
store and $L$ be an infinite set of locations such that
$L\cap\mathit{img}(\mathfrak{s})=\emptyset$. Then $\phi\vdash_{{\cal
R}}\Gamma$ admits a countermodel $(\mathfrak{s},\mathfrak{h})$ with
$\mathit{dom}(\mathfrak{h})\subseteq L\cup\mathfrak{s}(\mathit{alloc}(\phi))$.

###### Proof.

By hypothesis, there exists an injective store $\mathfrak{s}^{\prime}$ and a
heap $\mathfrak{h}^{\prime}$ such that
$(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\models_{{\cal R}}\phi$ and
$(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\not\models_{{\cal R}}\Gamma$.
By Lemma 72, we may assume that for all variables
$x\in\mathit{fv}\left(\phi\right)\cup\mathit{fv}\left(\Gamma\right)$, if
$x\not\in\mathit{alloc}(\phi)$ then
$\mathfrak{s}^{\prime}(x)\not\in\mathit{dom}(\mathfrak{h}^{\prime})$
($\dagger$). Let $\eta:{\cal L}\rightarrow
L\cup\mathfrak{s}(\mathit{fv}\left(\phi\right)\cup\mathit{fv}\left(\Gamma\right))$
be a bijective mapping such that
$\eta(\mathfrak{s}^{\prime}(x))=\mathfrak{s}(x)$, for all variables
$x\in\mathit{fv}\left(\phi\right)\cup\mathit{fv}\left(\Gamma\right)$. Such a
mapping necessarily exists. Indeed, since $L$ is infinite, there exists a
bijection between ${\cal
L}\setminus\mathfrak{s}^{\prime}(\mathit{fv}\left(\phi\right)\cup\mathit{fv}\left(\Gamma\right))$
and $L$; and since both $\mathfrak{s}$ and $\mathfrak{s}^{\prime}$ are
injective, there exists a bijection between
$\mathfrak{s}^{\prime}(\mathit{fv}\left(\phi\right)\cup\mathit{fv}\left(\Gamma\right))$
and
$\mathfrak{s}(\mathit{fv}\left(\phi\right)\cup\mathit{fv}\left(\Gamma\right))$.
Let $\mathfrak{h}=\eta(\mathfrak{h}^{\prime})$. By construction, for every
location $\ell\in\mathit{dom}(\mathfrak{h})$, we have
$\eta^{-1}(\ell)\in\mathit{dom}(\mathfrak{h}^{\prime})$, and if $\ell\not\in
L$, then necessarily $\ell=\mathfrak{s}(x)$ and
$\eta^{-1}(\ell)=\mathfrak{s}^{\prime}(x)$, for some
$x\in\mathit{fv}\left(\phi\right)\cup\mathit{fv}\left(\Gamma\right)$. Since
$\mathfrak{s}^{\prime}(x)\in\mathit{dom}(\mathfrak{h}^{\prime})$, by
($\dagger$) we have $x\in\mathit{alloc}(\phi)$, and therefore
$\mathit{dom}(\mathfrak{h})\subseteq L\cup\mathfrak{s}(\mathit{alloc}(\phi))$.

We now show that $(\mathfrak{s},\mathfrak{h})$ is a countermodel of
$\phi\vdash_{{\cal R}}\Gamma$. Since
$(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\models_{{\cal R}}\phi$, we
deduce by Proposition 71 that
$(\eta\circ\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi$.
Moreover, since $\eta\circ\mathfrak{s}^{\prime}$ and $\mathfrak{s}$ agree on
all variables in $\mathit{fv}\left(\phi\right)$ by construction, this entails
that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$. Assume that
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\Gamma$. Applying Proposition 71
with $\eta^{-1}$, we get
$(\eta^{-1}\circ\mathfrak{s},\eta^{-1}(\mathfrak{h}))\models_{{\cal
R}}\Gamma$. But we have
$\eta^{-1}(\mathfrak{h})=\eta^{-1}(\eta(\mathfrak{h}^{\prime}))=\mathfrak{h}^{\prime}$,
thus $(\eta^{-1}\circ\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal
R}}\Gamma$. Since $\eta^{-1}\circ\mathfrak{s}$ and $\mathfrak{s}^{\prime}$
agree on all variables in $\mathit{fv}\left(\Gamma\right)$ by construction, we
deduce that $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\models_{{\cal
R}}\Gamma$, contradicting our initial assumption. Thus
$(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\Gamma$ and
$(\mathfrak{s},\mathfrak{h})$ is a countermodel of $\phi\vdash_{{\cal
R}}\Gamma$. ∎

######  Definition 74.

A path from $\ell$ to $\ell^{\prime}$ in a heap $\mathfrak{h}$ is a nonempty
sequence of locations $(\ell_{1},\dots,\ell_{n})$ such that $\ell_{1}=\ell$,
$\ell_{n}=\ell^{\prime}$ and for every $i\in\\{1,\dots,n-1\\}$,
$\ell_{i+1}\in\mathfrak{h}(\ell_{i})$.

The following proposition states an important property of pc-SIDs.

######  Proposition 75.

Let $p(x_{1},\dots,x_{n})$ be a predicate atom and let
$(\mathfrak{s},\mathfrak{h})$ be a model of $p(x_{1},\dots,x_{n})$. If
$\ell=\mathfrak{s}(x_{1})$ and $\ell^{\prime}\in\mathit{loc}(\mathfrak{h})$
then there exists a path from $\ell$ to $\ell^{\prime}$ in $\mathfrak{h}$.

###### Proof.

The proof is by induction on $\mathit{card}(\mathit{dom}(\mathfrak{h}))$. We
have $p(x_{1},\dots,x_{n})\Leftarrow_{{\cal R}}\exists\mathbf{x}.\phi$ for
some quantifier-free formula $\phi$, and there exists a store
$\mathfrak{s}^{\prime}$ coinciding with $\mathfrak{s}$ on all variables not
occurring in $\mathbf{x}$, such that
$(\mathfrak{s}^{\prime},\mathfrak{h})\models\phi$. If $\ell=\ell^{\prime}$
then the result is immediate (a path of length $1$ always exists from any
location $\ell$ to $\ell$). Assume that $\ell\not=\ell^{\prime}$. By the
progress condition, $\phi$ is of the form
$x_{1}\mapsto(y_{1},\dots,y_{\kappa})*p_{1}(z_{1}^{1},\dots,z_{\\#(p_{1})}^{1})*\cdots*p_{m}(z_{1}^{m},\dots,z_{\\#(p_{m})}^{m})*\chi$,
for some ${\cal T}$-formula $\chi$. Thus there exist disjoint heaps
$\mathfrak{h}_{1},\dots,\mathfrak{h}_{m}$ such that
$\mathfrak{h}=\\{(\mathfrak{s}(x_{1}),\mathfrak{s}^{\prime}(y_{1}),\dots,\mathfrak{s}^{\prime}(y_{\kappa}))\\}\uplus\mathfrak{h}_{1}\uplus\dots\uplus\mathfrak{h}_{m}$
and $(\mathfrak{s},\mathfrak{h}_{i})\models
p_{i}(z_{1}^{i},\dots,z_{\\#(p_{i})}^{i})$ for $i=1,\dots,m$. If
$\mathfrak{s}(y_{i})=\ell^{\prime}$, for some $i=1,\dots,\kappa$ we have
$\ell^{\prime}\in\mathfrak{h}(\mathfrak{s}(x_{1}))=\mathfrak{h}(\ell)$ and the
proof is completed. Otherwise, $\ell^{\prime}$ cannot occur in
$\\{\mathfrak{s}(x_{1}),\mathfrak{s}^{\prime}(y_{1}),\dots,\mathfrak{s}^{\prime}(y_{\kappa})\\}$,
hence $\ell^{\prime}$ necessary occurs in $\mathit{loc}(\mathfrak{h}_{i})$ for
some $i=1,\dots,m$, since $\ell^{\prime}\in\mathit{loc}(\mathfrak{h})$ by
hypothesis. By the induction hypothesis, there exists a path in
$\mathfrak{h}_{i}$ from $\mathfrak{s}^{\prime}(z_{1}^{i})$ to $\ell^{\prime}$,
and by the connectivity condition
$\mathfrak{s}^{\prime}(z_{1}^{i})\in(\mathfrak{s}^{\prime}(y_{1}),\dots,\mathfrak{s}^{\prime}(y_{\kappa}))=\mathfrak{h}(\mathfrak{s}(x_{1}))=\mathfrak{h}(\ell)$.
Thus there exists a path in $\mathfrak{h}$ from $\ell$ to $\ell^{\prime}$. ∎

######  Lemma 76.

Let $\phi_{1}*\phi_{2}\vdash_{{\cal R}}\Gamma$ be a valid prenex
$\emptyset$-constrained sequent, where $\phi_{i}\not=\mathtt{emp}$ for
$i=1,2$, $\phi_{1}$ and $\phi_{2}$ are quantifier-free and disjunction-free.
If the rule HD is not applicable on $\phi_{1}*\phi_{2}\vdash_{{\cal R}}\Gamma$
and $\Gamma$ is in prenex form then $\phi_{1}*\phi_{2}\vdash_{{\cal R}}\Gamma$
is strongly valid.

###### Proof.

Assume that there exists a structure
$(\mathfrak{s},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})$ such that
$(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}\phi_{i}$ for $i=1,2$ and
$\forall
x\in\mathit{fv}\left(\phi_{i}\right),\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{i})\implies
x\in\mathit{alloc}(\phi_{i})$ ($\dagger$). Since
$\phi_{1}*\phi_{2}\vdash_{{\cal R}}\Gamma$ is valid, and $\Gamma$ is in prenex
form, $\Gamma$ contains a formula
$\psi=\exists\mathbf{x}.(\psi_{1}*\cdots*\psi_{n})$ such that
$(\mathfrak{s},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})\models_{{\cal R}}\psi$
and each formula $\psi_{i}$ ($i\in\\{1,\dots,n\\}$) is either a points-to atom
or a pu-atom. Thus there exist a store $\mathfrak{s}^{\prime}$, coinciding
with $\mathfrak{s}$ on all variables not occurring in $\mathbf{x}$ and
disjoint heaps $\mathfrak{h}_{1}^{\prime},\dots,\mathfrak{h}_{n}^{\prime}$
such that $(\mathfrak{s}^{\prime},\mathfrak{h}_{i}^{\prime})\models_{{\cal
R}}\psi_{i}$ for $i=1,\dots,n$ and
$\mathfrak{h}_{1}*\mathfrak{h}_{2}=\mathfrak{h}_{1}^{\prime}*\dots*\mathfrak{h}_{n}^{\prime}$.
By $\alpha$-renaming, we assume that
$\mathit{fv}\left(\phi_{1}*\phi_{2}\right)\cap\mathbf{x}=\emptyset$, so that
$\mathfrak{s}$ and $\mathfrak{s}^{\prime}$ coincide on
$\mathit{fv}\left(\phi_{1}*\phi_{2}\right)$. Note that by hypothesis
$\phi_{1}$ and $\phi_{2}$ are separating conjunctions of atoms.

Assume that one of the heap $\mathfrak{h}_{i}^{\prime}$ for $i=1,\dots,n$ is
such that $\mathfrak{h}_{i}^{\prime}\not\subseteq\mathfrak{h}_{1}$ and
$\mathfrak{h}_{i}^{\prime}\not\subseteq\mathfrak{h}_{2}$. This entails that
$\psi_{i}$ cannot be a points-to atom because
$\mathit{card}(\mathit{dom}(\mathfrak{h}_{i}^{\prime}))=1$ in this case, hence
that $\psi_{i}$ is a pu-atom. By Proposition 37,
$\mathfrak{s}^{\prime}(\mathit{roots}(\alpha_{i}))\subseteq\mathit{dom}(\mathfrak{h}_{i}^{\prime})\subseteq\mathit{dom}(\mathfrak{h}_{1})\cup\mathit{dom}(\mathfrak{h}_{2})$.
We assume by symmetry that
$\mathfrak{s}^{\prime}(\mathit{roots}(\alpha_{i}))\subseteq\mathit{dom}(\mathfrak{h}_{1})$,
the other case is similar. Let
$\ell\in\mathit{dom}(\mathfrak{h}_{i}^{\prime})\setminus\mathit{dom}(\mathfrak{h}_{1})$.
By Proposition 75, there exists a sequence of locations
$\ell_{1},\dots,\ell_{m}$ with
$\\{\ell_{1}\\}=\mathfrak{s}^{\prime}(\mathit{roots}(\alpha_{i}))$,
$\ell_{m}=\ell$ and $\ell_{i+1}\in\mathfrak{h}_{i}^{\prime}(\ell_{i})$ for
$i=1,\dots,m$. We may assume, by considering the location $\ell$ associated
with the minimal sequence ending outside of $\mathit{dom}(\mathfrak{h}_{1})$,
that $\ell_{i}\in\mathit{dom}(\mathfrak{h}_{1})$ for all $i<m$. This entails
that $\ell\in\mathfrak{h}_{1}(\ell_{m-1})$ so that
$\ell\in\mathit{loc}(\mathfrak{h}_{1})\setminus\mathit{dom}(\mathfrak{h}_{1})$,
and by Lemma 15 we deduce that $\ell=\mathfrak{s}(x)$ for some
$x\in\mathit{fv}\left(\phi_{1}\right)$. Furthermore, since
$\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{2})$ we must have
$x\in\mathit{alloc}(\phi_{2})$ by ($\dagger$). Since the rule HD is not
applicable, the variable $x$ must occur in
$\mathit{roots}(\psi_{1}*\dots*\psi_{n})$. This entails that there exists $j$
such that $\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{j}^{\prime})$ by
Proposition 37. But $x$ cannot be the main root of $\psi_{i}$, because
$\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ are disjoint,
$\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{2})$ and
$\mathfrak{s}^{\prime}(\mathit{roots}(\alpha_{i})\subseteq\mathit{dom}(\mathfrak{h}_{1})$,
hence $i\neq j$. This contradicts the fact that the
$\mathfrak{h}_{1}^{\prime},\dots,\mathfrak{h}_{n}^{\prime}$ are disjoint.

Therefore, every heap $\mathfrak{h}_{i}^{\prime}$ is a subheap of either
$\mathfrak{h}_{1}$ or $\mathfrak{h}_{2}$. By regrouping the formulas
$\psi_{i}$ such that $\mathfrak{h}_{i}^{\prime}\subseteq\mathfrak{h}_{j}$ in a
formula $\psi_{j}^{\prime}$ (for $j=1,2$), we get a decomposition of
$\exists\mathbf{x}.(\psi_{1}*\dots*\psi_{n})$ of the form:
$\exists\mathbf{x}.(\psi_{1}^{\prime}*\psi_{2}^{\prime})$, where
$(\mathfrak{s}^{\prime},\mathfrak{h}_{j})\models_{{\cal R}}\psi_{j}^{\prime}$
for $j=1,2$. Thus $\phi_{1}*\phi_{2}\vdash_{{\cal R}}\Gamma$ is strongly
valid. ∎

######  Lemma 77.

Let $\phi_{1}*\phi_{2}\vdash_{{\cal R}}\exists\mathbf{y}.\exists
x.\gamma,\Gamma$ be a strongly valid, $\emptyset$-constrained and quasi-prenex
sequent, with $\phi_{i}\not=\mathtt{emp}$ for $i=1,2$. There exists an
application of the rule ED with conclusion $\phi_{1}*\phi_{2}\vdash_{{\cal
R}}\exists\mathbf{y}.\exists x.\gamma,\Gamma$, such that the premise is
strongly valid and quasi-prenex.

###### Proof.

We apply the rule ED where $\\{\gamma_{1},\dots,\gamma_{m}\\}$ is the set of
all formulas satisfying the conditions of the rule, the formulas $\phi$ and
$\phi^{\prime}$ in the application condition of ED are prenex formulas and
$\chi=\mathtt{emp}$. Recall from the rule definition that
$\\{x_{1},\ldots,x_{n}\\}=\mathit{fv}\left(\phi\right)\cap\mathit{fv}\left(\phi^{\prime}\right)$.
It is straightforward to verify that the premise is quasi-prenex. Note that
both $\psi$ and $\psi^{\prime}$ are $\emptyset$-constrained by hypothesis. Let
$(\mathfrak{s},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})$ be a structure such
that for all $i=1,2$, $(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal
R}}\phi_{i}$ and $\forall
x\in\mathit{fv}\left(\phi_{i}\right),\mathfrak{s}(x)\in\mathit{dom}(\phi_{i})\implies
x\in\mathit{alloc}(\phi_{i})$. We have $\mathfrak{h}_{i}\not=\emptyset$,
because $\phi_{i}\not=\mathtt{emp}$. We show that the right-hand side of the
premise contains a formula satisfying the conditions of Definition 69. Since
$\phi_{1}*\phi_{2}\vdash_{{\cal R}}\exists\mathbf{y}.\exists x.\gamma,\Gamma$
is strongly valid there exist a formula of the form
$\exists\mathbf{x}.(\psi_{1}*\psi_{2})$ in $\exists\mathbf{y}.\exists
x.\gamma,\Gamma$ and a store $\mathfrak{s}^{\prime}$ coinciding with
$\mathfrak{s}$ on every variable not occurring in $\mathbf{x}$ such that
$(\mathfrak{s}^{\prime},\mathfrak{h}_{i})\models_{{\cal R}}\psi_{i}$ for
$i=1,2$. Since the considered sequent is quasi-prenex, $\psi_{1}$ and
$\psi_{2}$ are in prenex form. If $\exists\mathbf{x}.(\psi_{1}*\psi_{2})$
occurs in $\Gamma$ then the proof is completed. Otherwise we have
$\mathbf{y}.x=\mathbf{x}$ and $\gamma=\psi_{1}*\psi_{2}$. If
$\mathfrak{s}^{\prime}(x)=\mathfrak{s}(x_{j})$, for some $j=1,\dots,n$, then
$(\mathfrak{s}^{\prime},\mathfrak{h}_{i})\models_{{\cal
R}}\psi_{i}\\{x\leftarrow x_{j}\\}$, and $\psi_{1}\\{x\leftarrow
x_{j}\\}*\psi_{2}\\{x\leftarrow x_{j}\\}=\gamma\\{x\leftarrow x_{j}\\}$ occurs
on the right-hand side of the premise, by definition of the rule ED. Thus, the
result also holds in this case. Now assume that
$\mathfrak{s}^{\prime}(x)\not=\mathfrak{s}(x_{j})$, for all $j=1,\dots,n$. By
Lemma 15, since $(\mathfrak{s},\mathfrak{h}_{i})\models\phi_{i}$, we have
$\mathit{loc}(\mathfrak{h}_{i})\setminus\mathit{dom}(\mathfrak{h}_{i})\subseteq\mathfrak{s}(\mathit{fv}\left(\phi_{i}\right))$,
for $i=1,2$. Since $\mathfrak{s}^{\prime}(x)\not=\mathfrak{s}(x_{j})$, for all
$j=1,\dots,n$,
$\mathfrak{s}^{\prime}(x)\not\in\mathfrak{s}(\mathit{fv}\left(\phi_{i}\right))$
hence
$\mathfrak{s}^{\prime}(x)\not\in\mathit{loc}(\mathfrak{h}_{i})\setminus\mathit{dom}(\mathfrak{h}_{i})$.
If
$\mathfrak{s}^{\prime}(x)\in\mathit{loc}(\mathfrak{h}_{1})\cap\mathit{loc}(\mathfrak{h}_{2})$,
then we would have
$\mathfrak{s}^{\prime}(x)\in\mathit{dom}(\mathfrak{h}_{1})\cap\mathit{dom}(\mathfrak{h}_{2})$,
contradicting the fact that $\mathfrak{h}_{1}$ and $\mathfrak{h}_{2}$ are
disjoint. This entails that
$\mathfrak{s}^{\prime}(x)\not\in\mathit{loc}(\mathfrak{h}_{1})\cap\mathit{loc}(\mathfrak{h}_{2})$.
We assume, by symmetry, that
$\mathfrak{s}^{\prime}(x)\not\in\mathit{loc}(\mathfrak{h}_{2})$. Then by Lemma
57, we deduce that
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{2})\models_{{\cal R}}\psi_{2}$,
for every store $\mathfrak{s}^{\prime\prime}$ coinciding with
$\mathfrak{s}^{\prime}$ on all variables distinct from $x$. We also have
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}_{1})\models_{{\cal R}}\exists
x.\psi_{1}$, since $(\mathfrak{s}^{\prime},\mathfrak{h}_{1})\models_{{\cal
R}}\psi_{1}$. By definition of the rule, the right-hand side of the premise
contains a formula $\exists\mathbf{y}.((\exists
x.\psi_{1})*\psi_{2}\\{x\leftarrow x^{\prime}\\})$, hence the conditions of
Definition 69 are fulfilled (note that $\psi_{2}$ cannot be $\mathtt{emp}$,
since $\mathfrak{h}_{2}\not=\emptyset$). ∎

######  Lemma 78.

Let $\phi_{1}*\phi_{2}\vdash_{{\cal R}}\Gamma$ be a strongly valid and
$\emptyset$-constrained sequent. If rules ED and D do not apply on
$\phi_{1}*\phi_{2}\vdash_{{\cal R}}\Gamma$ then rule SC applies on
$\phi_{1}*\phi_{2}\vdash_{{\cal R}}\Gamma$, with a valid premise.

###### Proof.

Let $\Delta$ be the subsequence of formulas in $\Gamma$ that are not separated
conjunctions, so that $\Gamma$ is of the form
$\psi_{1}^{1}*\psi_{1}^{2},\dots,\psi_{n}^{1}*\psi_{n}^{2},\Delta$. By
definition of the notion of strong validity, if
$(\mathfrak{s},\mathfrak{h}_{1}\uplus\mathfrak{h}_{2})\models_{{\cal
R}}\phi_{1}*\phi_{2}$ and $\forall
x\,(\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{i})\implies
x\in\mathit{alloc}(\phi_{i}))$, then $\Gamma$ contains a formula of the form
$\exists\mathbf{x}.(\psi_{1}*\psi_{2})$ such that
$(\mathfrak{s}^{\prime},\mathfrak{h}_{1})\models\psi_{1}$ and
$(\mathfrak{s}^{\prime},\mathfrak{h}_{2})\models\psi_{2}$, where
$\mathfrak{s}^{\prime}$ coincides with $\mathfrak{s}$ on all variables not
occurring in $\mathbf{x}$. By Lemma 77, none of the formulas in $\Gamma$ may
be existentially quantified, since otherwise rule ED applies. Thus
$\mathbf{x}$ is empty,
$\exists\mathbf{x}.(\psi_{1}*\psi_{2})=\psi_{1}*\psi_{2}$ does not occur in
$\Delta$ and there exists $i=1,\dots,n$ such that $\psi_{1}=\psi_{i}^{1}$ and
$\psi_{2}=\psi_{i}^{2}$.

Let $I_{1},\dots,I_{m}$ denote the inclusion-minimal subsets of
$\\{1,\dots,n\\}$ such that for all $j=1,\ldots,m$, $\phi_{1}\vdash_{{\cal
R}}\bigvee_{c\in I_{j}}\psi_{c}^{1}$ is valid. Similarly, let
$J_{1},\dots,J_{l}$ denote the inclusion-minimal subsets of $\\{1,\dots,n\\}$
such that for all $j=1,\ldots,l$, $\phi_{2}\vdash_{{\cal R}}\bigvee_{c\in
J_{j}}\psi_{c}^{2}$ is valid. If the rule SC applies with such sets, then, by
construction all the premises are valid, hence the proof is completed.
Otherwise, by the application condition of the rule, there exists a set $X$
such that $X\not\supseteq I_{i}$ for all $i=1,\dots,n$ and
$\\{1,\dots,n\\}\setminus X\not\supseteq J_{j}$ for all $j=1,\dots,l$. This
entails that $\phi_{1}\vdash_{{\cal R}}\bigvee_{c\in X}\psi_{c}^{1}$ is not
valid, since otherwise $X$ would contain one of the $I_{i}$ which are
inclusion-minimal by construction. Similarly, $\phi_{2}\vdash_{{\cal
R}}\bigvee_{c\in\\{1,\dots,n\\}\setminus X}\psi_{c}^{2}$ is not valid because
otherwise $\\{1,\dots,n\\}\setminus X$ would contain one of the $J_{j}$.
Therefore, there exist injective stores $\mathfrak{s}_{i}$ and heaps
$\mathfrak{h}_{i}$ for $i=1,2$, such that
$(\mathfrak{s}_{i},\mathfrak{h}_{i})\models_{{\cal R}}\phi_{i}$,
$(\mathfrak{s}_{1},\mathfrak{h}_{1})\not\models_{{\cal R}}\bigvee_{c\in
X}\psi_{c}^{1}$ and $(\mathfrak{s}_{2},\mathfrak{h}_{2})\not\models_{{\cal
R}}\bigvee_{c\in\\{1,\dots,n\\}\setminus X}\psi_{c}^{2}$. Let $\mathfrak{s}$
be an injective store such that ${\cal L}\setminus\mathit{img}(\mathfrak{s})$
is infinite, and let $L_{1},L_{2}$ be disjoint infinite subsets of ${\cal
L}\setminus\mathit{img}(\mathfrak{s})$. By applying Lemma 73 twice on
$\mathfrak{h}_{1},\mathfrak{h}_{2}$ with $L_{1}$ and $L_{2}$ respectively, we
obtain two heaps $\mathfrak{h}_{1}^{\prime}$ and $\mathfrak{h}_{2}^{\prime}$
such that:

  * •

$\mathit{dom}(\mathfrak{h}_{i}^{\prime})\subseteq
L_{i}\cup\mathfrak{s}(\mathit{alloc}(\phi_{i}))$ for $i=1,2$,

  * •

$(\mathfrak{s},\mathfrak{h}_{i}^{\prime})\models_{{\cal R}}\phi_{i}$ for
$i=1,2$,

  * •

$(\mathfrak{s},\mathfrak{h}_{1}^{\prime})\not\models_{{\cal R}}\bigvee_{c\in
X}\psi_{c}^{1}$,

  * •

$(\mathfrak{s},\mathfrak{h}_{2}^{\prime})\not\models_{{\cal
R}}\bigvee_{c\in\\{1,\dots,n\\}\setminus X}\psi_{c}^{2}$.

In particular, since $L_{1}$ and $L_{2}$ are disjoint, we have
$\mathit{dom}(\mathfrak{h}_{1}^{\prime})\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime})\subseteq\mathfrak{s}(\mathit{alloc}(\phi_{1}))\cap\mathfrak{s}(\mathit{alloc}(\phi_{2}))$.
Assume that
$\mathit{dom}(\mathfrak{h}_{1}^{\prime})\cap\mathit{dom}(\mathfrak{h}_{2}^{\prime})$
is nonempty, and contains a location $\ell$. Then for $i=1,2$, there exists a
variable $x_{i}\in\mathit{fv}\left(\phi_{i}\right)$ such that
$\ell=\mathfrak{s}(x_{i})$. Since $\mathfrak{s}$ is injective, necessarily
$x_{1}=x_{2}$, and
$\mathit{alloc}(\phi_{1})\cap\mathit{alloc}(\phi_{2})\not=\emptyset$; this
entails that the rule D is applicable, which contradicts the hypothesis of the
lemma.

We deduce that $\mathfrak{h}_{1}^{\prime}$ and $\mathfrak{h}_{2}^{\prime}$ are
disjoint. Then we have
$(\mathfrak{s},\mathfrak{h}_{1}^{\prime}\uplus\mathfrak{h}_{2}^{\prime})\models_{{\cal
R}}\phi_{1}*\phi_{2}$ and for all $c\in\\{1,\dots,n\\}$, either
$(\mathfrak{s},\mathfrak{h}_{1}^{\prime})\not\models_{{\cal R}}\psi_{c}^{1}$
or $(\mathfrak{s},\mathfrak{h}_{2}^{\prime})\not\models_{{\cal
R}}\psi_{c}^{2}$. Furthermore, if
$\mathfrak{s}(x)\in\mathit{dom}(\mathfrak{h}_{i}^{\prime})$, then
$\mathfrak{s}(x)\in\mathfrak{s}(\mathit{alloc}(\phi_{i}))$, thus
$x\in\mathit{alloc}(\phi_{i})$ because $\mathfrak{s}$ is injective. This
contradicts that fact that $\phi_{1}*\phi_{2}\vdash_{{\cal R}}\Gamma$ is
strongly valid.

∎

######  Definition 79.

Let $\phi\vdash_{{\cal R}}\psi,\Gamma$ be a sequent. The formula $\psi$ is
root-redundant if there exists a variable $x$ such that either
$x\in\mathit{roots}_{r}(\psi)$ and $x\not\in\mathit{alloc}(\phi)$, or
$x\in\mathit{roots}_{l}(\psi)$ and $x\not\in\mathit{fv}\left(\phi\right)$.
This formula is variable-redundant if there exist two injective substitutions
$\sigma,\theta$ such that $\psi\sigma\in\Gamma\theta$ and
$(\mathit{dom}(\sigma)\cup\mathit{dom}(\theta))\cap\mathit{fv}\left(\phi\right)=\emptyset$.

######  Proposition 80.

If $(\mathfrak{s},\mathfrak{h})\models\phi$ then
$\mathfrak{s}(\mathit{roots}_{l}(\phi))\subseteq\mathit{loc}(\mathfrak{h})$.

###### Proof.

The proof is by induction on the satisfiability relation. We only handle the
case where
$\phi=\Phi_{\beta\mathrel{\mbox{$\mathord{-}\mathord{-}\scalebox{0.9}{$\mathord{\bullet}$}$}}\alpha}^{\mathbf{u}}[\mathbf{u}\theta]$,
the other cases are straightforward. By definition, there exists a formula
$\exists\mathbf{x}.(\beta^{\prime}*\psi)$, a substitution $\sigma$ with
$\mathit{dom}(\theta)\subseteq\mathbf{x}$ and a store $\mathfrak{s}^{\prime}$
coinciding with $\mathfrak{s}\circ\sigma$ on all variables not occurring in
$\mathbf{x}$ such that $\alpha\Leftarrow_{{\cal
R}}^{+}\exists\mathbf{x}.(\beta^{\prime}*\psi)$, $\beta^{\prime}\sigma=\beta$
and $(\mathfrak{s}^{\prime},\mathfrak{h})\models\psi\sigma\theta$. Let
$x\in\mathit{roots}_{l}(\phi)$. By definition, $\beta$ contains a predicate
atom of the form $p(x,\mathbf{y})$, thus $\beta^{\prime}$ contains a predicate
atom of the form $p(x^{\prime},\mathbf{y}^{\prime})$, with
$x^{\prime}\sigma=x$. This predicate atom must be introduced in the derivation
$\alpha\Leftarrow_{{\cal R}}^{+}\exists\mathbf{x}.(\beta^{\prime}*\psi)$ by
unfolding some predicate atom $q(u,\mathbf{v})$. By the progress and
connectivity condition this entails that $\psi$ contains a points-to atom of
the form $u\mapsto(\dots,x^{\prime},\dots)$. Since
$(\mathfrak{s}^{\prime},\mathfrak{h})\models\psi\sigma$ this entails that
$\mathfrak{s}^{\prime}(x^{\prime}\sigma)\in\mathit{loc}(\mathfrak{h})$, thus
$\mathfrak{s}(x)\in\mathit{loc}(\mathfrak{h})$. ∎

######  Proposition 81.

If $(\mathfrak{s}\circ\sigma,\mathfrak{h})\models_{{\cal R}}\phi$ then
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\sigma$.

###### Proof.

The proof is by induction on the satisfiability relation. We only handle the
case where
$\phi=\Phi_{\beta\mathrel{\mbox{$\mathord{-}\mathord{-}\scalebox{0.9}{$\mathord{\bullet}$}$}}\alpha}^{\mathbf{u}}[\mathbf{u}\theta]$.
By definition, there exists a formula
$\exists\mathbf{x}.(\beta^{\prime}*\psi)$, a substitution $\theta$ with
$\mathit{dom}(\theta)\subseteq\mathbf{x}$ and a store $\mathfrak{s}^{\prime}$
coinciding with $\mathfrak{s}\circ\sigma$ on all variables not occurring in
$\mathbf{x}$ such that $\alpha\Leftarrow_{{\cal
R}}^{+}\exists\mathbf{x}.(\beta^{\prime}*\psi)$, $\beta^{\prime}\theta=\beta$
and $(\mathfrak{s}^{\prime},\mathfrak{h})\models\psi\theta\eta$. By
$\alpha$-renaming, we assume that
$\mathbf{x}\cap(\mathit{dom}(\sigma)\cup\mathit{img}(\sigma))=\emptyset$. Let
$\hat{\mathfrak{s}}$ be the store such that
$\hat{\mathfrak{s}}(x)=\mathfrak{s}(x)$ if $x\not\in\mathbf{x}$ and
$\hat{\mathfrak{s}}(x)=\mathfrak{s}^{\prime}(x)$ if $x\in\mathbf{x}$. By
construction we have $\mathfrak{s}^{\prime}=\hat{\mathfrak{s}}\circ\sigma$. By
the induction hypothesis, we deduce that and
$(\hat{\mathfrak{s}},\mathfrak{h})\models\psi\theta\sigma$. Furthermore,
$\beta^{\prime}\theta\sigma=\beta\sigma$, and $\alpha\sigma\Leftarrow_{{\cal
R}}^{+}\exists\mathbf{x}.(\beta^{\prime}*\psi)\sigma=\exists\mathbf{x}.(\beta^{\prime}\sigma*\psi\sigma)$.
Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\sigma$. ∎

######  Lemma 82.

Let $\phi\vdash_{{\cal R}}\psi,\Gamma$ be a valid $\emptyset$-constrained
disjunction-free sequent. If $\psi$ is root-unsatisfiable, root-redundant or
variable-redundant, then $\phi\vdash_{{\cal R}}\Gamma$ is valid.

###### Proof.

We consider the three cases separately.

  * •

If $\psi$ is root-unsatisfiable, then $\psi$ is unsatisfiable, thus every
model of $\psi,\Gamma$ is also a model of $\Gamma$. Therefore
$\phi\vdash_{{\cal R}}\Gamma$ if and only if $\phi\vdash_{{\cal
R}}\psi,\Gamma$.

  * •

Assume that $\psi$ is root-redundant and let $(\mathfrak{s},\mathfrak{h})$ be
an injective model of $\phi$. By Lemma 72, applied on any sequent
$\phi\vdash_{{\cal R}}\phi^{\prime}$ such that $\phi^{\prime}$ is
unsatisfiable, there exists an injective mapping $\eta$ and a model
$(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})$ of $\phi$ such that
$\mathfrak{s}=\eta\circ\mathfrak{s}^{\prime}$,
$\mathfrak{h}=\eta(\mathfrak{h}^{\prime})$ and
$\mathfrak{s}^{\prime}(x)\in\mathit{dom}(\mathfrak{h}^{\prime})\implies
x\in\mathit{alloc}(\phi)$. Let $\mathfrak{s}^{\prime\prime}$ be a store
coinciding with $\mathfrak{s}^{\prime}$ on all the variables in
$\mathit{fv}\left(\phi\right)$ and such that
$\mathfrak{s}^{\prime\prime}(y)\not\in\mathit{loc}(\mathfrak{h}^{\prime})$,
for all $y\notin\mathit{fv}\left(\phi\right)$. Since
$\mathfrak{s}^{\prime\prime}$ and $\mathfrak{s}^{\prime}$ coincide on
$\mathit{fv}\left(\phi\right)$, necessarily
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}^{\prime})\models\phi$. Also, if
$\mathfrak{s}^{\prime\prime}(x)\in\mathit{dom}(\mathfrak{h}^{\prime})\subseteq\mathit{loc}(\mathfrak{h}^{\prime})$,
then necessarily $x\in\mathit{fv}\left(\phi\right)$, so that
$\mathfrak{s}^{\prime\prime}(x)=\mathfrak{s}^{\prime}(x)$ and
$x\in\mathit{alloc}(\phi)$. Therefore,
$\mathfrak{s}^{\prime\prime}(x)\in\mathit{dom}(\mathfrak{h}^{\prime})\implies
x\in\mathit{alloc}(\phi)$. We distinguish two cases.

    * –

Assume that
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}^{\prime})\not\models\Gamma$. Since
$\phi\vdash_{{\cal R}}\psi,\Gamma$ is valid we have
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}^{\prime})\models\psi,\Gamma$ and
necessarily, $(\mathfrak{s}^{\prime\prime},\mathfrak{h}^{\prime})\models\psi$.
If there exists $x\in\mathit{roots}_{r}(\psi)$ such that
$x\not\in\mathit{alloc}(\phi)$, then by Proposition 37 we have
$\mathfrak{s}^{\prime\prime}(x)\in\mathit{dom}(\mathfrak{h}^{\prime})$, which
contradicts the above implication. Otherwise, since $\psi$ is root-redundant,
there exists a variable
$x\in\mathit{roots}_{l}(\psi)\setminus\mathit{fv}\left(\phi\right)$. Since
$x\in\mathit{roots}_{l}(\psi)$, we have
$\mathfrak{s}^{\prime\prime}(x)\in\mathit{loc}(\mathfrak{h}^{\prime})$ by
Proposition 80, which contradicts the definition of
$\mathfrak{s}^{\prime\prime}$ because $x\not\in\mathit{fv}\left(\phi\right)$.

    * –

Assume that
$(\mathfrak{s}^{\prime\prime},\mathfrak{h}^{\prime})\models\Gamma$. Let
$\eta^{\prime}$ be the function mapping all locations of the form
$\mathfrak{s}^{\prime\prime}(y)$ to $\mathfrak{s}^{\prime}(y)$ and leaving all
other locations unchanged. By definition, we have
$\mathfrak{s}=\eta\circ\eta^{\prime}\circ\mathfrak{s}^{\prime}$ and for all
$y\in{\cal V}$, if
$\mathfrak{s}^{\prime\prime}(y)\in\mathit{loc}(\mathfrak{h}^{\prime})$ then we
must have $y\in\mathit{fv}\left(\phi\right)$, so that
$\mathfrak{s}^{\prime\prime}(y)=\mathfrak{s}^{\prime}(y)$. We deduce that
$\eta^{\prime}$ is the identity on every location in
$\mathit{loc}(\mathfrak{h}^{\prime})$ and that
$\eta(\eta^{\prime}(\mathfrak{h}^{\prime}))=\mathfrak{h}$. By Proposition 71,
$(\eta\circ\eta^{\prime}\circ\mathfrak{s}^{\prime},\eta(\eta^{\prime}(\mathfrak{h})))\models\Gamma$,
i.e., $(\mathfrak{s},\mathfrak{h})\models\Gamma$, contradicting our
assumption.

  * •

Assume that $\psi$ is variable-redundant and let $(\mathfrak{s},\mathfrak{h})$
be a model of $\phi$, where $\mathfrak{s}$ is injective. We show that
$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\Gamma$. Let
$\mathfrak{s}^{\prime}$ be an injective store coinciding with $\mathfrak{s}$
on every variable in $\mathit{fv}\left(\phi\right)$ and such that
$\mathfrak{s}^{\prime}(x)\not\in\mathit{loc}(\mathfrak{h})$ for every
$x\not\in\mathit{fv}\left(\phi\right)$ ($\ddagger$). It is clear that
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi$, thus
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi,\Gamma$, since
$\phi\vdash_{{\cal R}}\psi,\Gamma$ is valid by hypothesis. If
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\Gamma$ then by Lemma
57 we deduce that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\Gamma$, and
the proof is completed. Otherwise,
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi$. By hypothesis,
there exist injective substitutions $\sigma$ and $\theta$ such that
$\psi\sigma\in\Gamma\theta$ and
$(\mathit{dom}(\sigma)\cup\mathit{dom}(\theta))\cap\mathit{fv}\left(\phi\right)=\emptyset$.
By ($\ddagger$), we have
$(\mathfrak{s}^{\prime}\circ\sigma)(x)=\mathfrak{s}^{\prime}(x)$ for all $x$
such that $\mathfrak{s}^{\prime}(x)\in\mathit{loc}(\mathfrak{h})$, since in
this case $x$ cannot be in $\mathit{dom}(\sigma)$. By Lemma 57, we deduce that
$(\mathfrak{s}^{\prime}\circ\sigma,\mathfrak{h})\models_{{\cal R}}\psi$, thus
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi\sigma$ by
Proposition 81. Since $\psi\sigma\in\Gamma\theta$, we deduce that
$(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\Gamma\theta$, hence
(as $\theta$ is injective)
$(\mathfrak{s}^{\prime}\circ\theta,\mathfrak{h})\models_{{\cal R}}\Gamma$. If
$x$ is a variable such that
$(\mathfrak{s}^{\prime}\circ\theta)(x)\in\mathit{loc}(\mathfrak{h})$ then by
definition of $\mathfrak{s}^{\prime}$, we have
$\theta(x)\in\mathit{fv}\left(\phi\right)$. Since
$\mathit{dom}(\theta)\cap\mathit{fv}\left(\phi\right)=\emptyset$, we deduce
that $\theta(x)=x$, and
$(\mathfrak{s}^{\prime}\circ\theta)(x)=\mathfrak{s}^{\prime}(x)=\mathfrak{s}(x)$.
By Lemma 57, we conclude that $(\mathfrak{s},\mathfrak{h})\models_{{\cal
R}}\Gamma$.

∎

######  Theorem 83.

(Termination) For all valid, $\emptyset$-constrained, prenex, disjoint-free,
$\mathit{alloc}$-compatible and pu-free sequents $\phi\vdash_{{\cal
R}}\Gamma$, there exists a rational proof tree with end-sequent
$\phi\vdash_{{\cal R}}\Gamma$. Furthermore, the size of the proof tree is at
most $\mathcal{O}(2^{2^{c.N^{3}}})$, where $c$ is a constant and
$N=\mathit{width}(\phi\vdash_{{\cal R}}\Gamma)$.

###### Proof.

Let $A=\max\\{\kappa+1,\\#(p)\mid p\in{\cal P}_{S}\\}$ and $P=\max\\{\|p\|\mid
p\in{\cal P}_{S}\\}$. We assume, w.l.o.g., that all the predicate in ${\cal
P}_{S}$ occur in ${\cal R}$, so that $A=\mathcal{O}(N)$ and
$P=\mathcal{O}(N)$. The proof tree is constructed in a similar way as in the
proof of Theorem 65, except that rule UL will be applied only when the left-
hand side of the sequent contains a unique spatial atom. We show that there is
some rule that is applicable to every valid sequent, in such a way that all
the premises are valid. All the inference rules that are axioms are applied
with the highest priority, whenever possible. Afterwards, the rule W is
applied to remove from the right-hand side of the sequents all the formulas
that are root-unsatisfiable, root-redundant or variable-redundant; Lemma 82
guarantees that the validity the sequent is preserved. Rules Sk and HD are
then applied as much as possible. If the process terminates, then we
eventually obtain a sequent of the form $\psi\vdash_{{\cal R}}\Delta$, such
that $\psi$ is quantifier-free (by irreducibility w.r.t. Sk) and
$\mathit{alloc}(\psi)\subseteq\mathit{roots}(\psi^{\prime})$, for every
$\psi^{\prime}$ in $\Delta$ (by irreducibility w.r.t. ${\color[rgb]{0,0,1}{\tt
HD}}$).

We now distinguish several cases, depending on the form of $\psi$. First if
$\psi$ is a points-to atom, then by Theorem 65, there exists a rule
application yielding valid premises, and the applied rule cannot be UL, since
by hypothesis $\psi$ contains no predicate atom. Otherwise, if $\psi$ is a
single predicate atom then we apply the rule UL101010Note that in the proof of
Theorem 65 rule UL is applied when $\psi$ _contains_ a predicate atom.
However, this strategy is not applicable here because it may produce an
infinite proof tree. and validity is preserved thanks to Lemma 64. Otherwise,
$\psi$ must be a separating conjunction. By Lemma 76, $\psi\vdash_{{\cal
R}}\Delta$ is strongly valid. Rule ED is then applied as much as possible.
Note that, by Lemma 77, if the prefix of a formula in $\Delta$ contains an
existential variable then there exists an application of
${\color[rgb]{0,0,1}{\tt ED}}$ such that the obtained sequents are strongly
valid and quasi-prenex. If ED is not applicable then by Lemma 78, rule SC
necessarily applies.

We now prove that the constructed proof tree is rational. To this purpose, we
analyze the form of the sequents occurring in it. Consider any sequent
$\gamma\vdash_{{\cal R}}\gamma_{1},\dots,\gamma_{n}$ occurring in the proof
tree and assume that none of the formulas $\gamma_{1},\dots,\gamma_{n}$ is
root-unsatisfiable, root-redundant or variable-redundant. We prove the
following invariant.

######  Invariant 84.

For every $i=1,\dots,n$, the following properties hold:

  1. 1.

If an existential variable is the main root of a pu-atom in $\gamma_{i}$, then
it is the main root of an atom occurring in the initial sequent
$\phi\vdash_{{\cal R}}\Gamma$. Moreover, existential variables cannot be
auxiliary roots.

  2. 2.

Both $\mathit{roots}_{r}(\gamma_{i})$ and $\mathit{roots}_{l}(\gamma_{i})$ are
sets (i.e., contain at most one occurrence of each variable), and
$\mathit{roots}(\gamma_{i})\subseteq\mathit{fv}\left(\gamma\right)$.

  3. 3.

If $x\in\mathit{roots}_{l}(\gamma_{i})$ and
$x\not\in\mathit{roots}_{r}(\gamma_{i})$ then
$x\not\in\mathit{alloc}(\gamma)$.

  4. 4.

The number of variables occurring in $\gamma$ is at most
$\max(N_{\mathit{i}nit},N_{{\cal R}})$, where
$N_{\mathit{i}nit}=\mathit{card}(\mathit{fv}\left(\phi\right)\cup\mathit{fv}\left(\Gamma\right))$
and $N_{{\cal R}}$ is the maximal number of free or bound variables occurring
in a rule in ${\cal R}$.

###### Proof.

We assume, w.l.o.g., that $\gamma\vdash_{{\cal R}}\gamma_{1},\dots,\gamma_{n}$
is the first sequent not satisfying these properties, along some (possibly
infinite) path from the root.

  1. 1.

It is straightforward to check, by inspection of the rules, that no rule can
add atoms with existentially quantified roots in the premise: the only rule
that can add new atoms to the right-hand side of a sequent is HD (by applying
the function $\mathrm{split}()$ defined in Section 7), and the roots of these
atoms must be free variables. Then the proof follows from the fact that the
initial sequent is pu-free. Note that no rule can rename the existential
variables occurring in the sequents; the only variables that are renamed are
those occurring in the inductive rules.

  2. 2.

The inclusion
$\mathit{roots}(\gamma_{i})\subseteq\mathit{fv}\left(\gamma\right)$ follows
from the fact that the $\gamma_{i}$ are not root-redundant. If
$\mathit{roots}_{r}(\gamma_{i})$ contains two occurrences of the same variable
for some $i\in\\{1,\dots,n\\}$, then $\gamma_{i}$ is root-unsatisfiable,
contradicting our assumption. Assume that a multiset
$\mathit{roots}_{l}(\gamma_{i})$ contains two occurrences of the same variable
$x$. The initial sequent is pu-free, hence contains no auxiliary root, and the
only rule that can add new auxiliary roots to a sequent is HD. Thus assume
that $\gamma\vdash_{{\cal R}}\gamma_{1},\dots,\gamma_{n}$ is obtained from a
sequent of the form $\gamma\vdash_{{\cal
R}}\gamma_{1}^{\prime},\Gamma^{\prime}$, by applying rule HD on
$\gamma_{1}^{\prime}$ with variable $x$. By the application condition of the
rule, necessarily $x\in\mathit{alloc}(\gamma)$. Furthermore, since by
definition of the splitting operation, HD introduces exactly one auxiliary
root in $\gamma_{i}$, and $x$ occurs twice in
$\mathit{roots}_{l}(\gamma_{i})$, necessarily
$x\in\mathit{roots}_{l}(\gamma_{1}^{\prime})$. By Property 3 of the invariant,
applied to the sequent $\gamma\vdash_{{\cal
R}}\gamma_{1}^{\prime},\Gamma^{\prime}$ which satisfies the invariant by
hypothesis, since $x\in\mathit{alloc}(\gamma)$, necessarily
$x\in\mathit{roots}_{r}(\gamma_{1}^{\prime})$. But HD also introduces an atom
with main root $x$, which entails that $x$ occurs twice in
$\mathit{roots}_{r}(\gamma_{i})$, hence that $\gamma_{i}$ is root-
unsatisfiable, yielding a contradiction.

  3. 3.

The only rules that can add affect the roots of the right-hand side of the
sequent are ED, HD, and SC.

     * •

ED may generate new roots by instantiating an existential variable with a free
variable, however by Property 1, existential variables cannot be auxiliary
roots, hence Property 3 is preserved.

     * •

HD adds a new auxiliary root $x$ to the right-hand side of the sequent.
However, for each such atom, HD also adds an atom with main root $x$, hence
the property is preserved.

     * •

SC may remove main roots from the right-hand side of the sequent. If some
premise of SC does not fulfill Property 3 of the invariant, then, using the
notations of the rule, there exists an index $i\in\\{1,\dots,n\\}$ such that
either $x\in\mathit{roots}_{l}(\psi_{i})$,
$x\not\in\mathit{roots}_{r}(\psi_{i})$ and $x\in\mathit{alloc}(\phi)$, or
$x\in\mathit{roots}_{l}(\psi_{i}^{\prime})$,
$x\not\in\mathit{roots}_{r}(\psi_{i}^{\prime})$ and
$x\in\mathit{alloc}(\phi^{\prime})$. We assume by symmetry that the former
assertion holds. Since
$\mathit{alloc}(\phi)\subseteq\mathit{alloc}(\phi*\phi^{\prime})$, we have
$x\in\mathit{alloc}(\phi*\phi^{\prime})$, which entails that
$x\in\mathit{roots}_{r}(\psi_{i}^{\prime})$, since the conclusion satisfies
Property 3. By irreducibility w.r.t. D,
$\mathit{alloc}(\phi)\cap\mathit{alloc}(\phi^{\prime})=\emptyset$, thus
$x\not\in\mathit{alloc}(\phi^{\prime})$. This entails that the formula
$\psi_{i}^{\prime}$ is root-redundant in all sequents with left-hand side
$\phi^{\prime}$, contradicting our assumption.

  4. 4.

Property 4 stems from the fact that no rule may add variables to the left-hand
side of a sequent, except for UL. However, UL is always applied on a sequent
with a left-hand side that is an atom, which entails that the number of
variables occurring on the left-hand side after any application of the rule is
bounded by $N_{{\cal R}}$.

∎

Properties 2, 1 and 4 in Invariant 84 entail that the number of roots in every
formula $\gamma_{i}$ is at most $2\cdot\max(N_{\mathit{i}nit},N_{{\cal
R}})+N_{\exists}$, where $N_{\exists}$ denotes the number of existential
variables in the end-sequent. Indeed, a free variable may occur at most twice
as a root, once as an auxiliary root and once as a main root, and an
existential variable may occur at most once as a main root. Note that
$N_{\mathit{i}nit}=\mathcal{O}(N)$, $N_{{\cal R}}=\mathcal{O}(N)$ and
$N_{\exists}=\mathcal{O}(N)$. Thus the number of (free or existential)
variables in $\gamma_{i}$ is bounded by
$A\cdot(2\cdot\max(N_{\mathit{i}nit},N_{{\cal R}})+N_{\exists})$. Hence we may
assume (up to a renaming of variables) that the total number of variables
occurring in the considered sequent at most
$A\cdot(2\cdot\max(N_{\mathit{i}nit},N_{{\cal R}})+N_{\exists})$ so that every
such variable may be represented by a word of length
$\log(A\cdot(2\cdot\max(N_{\mathit{i}nit},N_{{\cal R}})+N_{\exists}))$. Let
$\gamma_{1}^{\prime},\dots,\gamma_{n}^{\prime}$ be formulas obtained from
$\gamma_{1},\dots,\gamma_{n}$ by replacing all the free variables not
occurring in $\mathit{fv}\left(\gamma\right)$ by some unique fixed variable
$u$. The size of every expression of the form $p(\mathbf{x})$ occurring in
$\gamma_{1}^{\prime},\dots,\gamma_{n}^{\prime}$ (possibly within a pu-atom) is
bounded by $P+A\cdot\log(A\cdot(2\cdot\max(N_{\mathit{i}nit},N_{{\cal
R}})+N_{\exists}))=\mathcal{O}(N^{2})$, thus the size of the formulas
$\gamma_{i}^{\prime}$ is bounded by $\mathcal{O}(N^{3})$. By Proposition 31,
the size of the set $\\{\gamma_{1}^{\prime},\dots,\gamma_{n}^{\prime}\\}$ is
therefore at most $\mathcal{O}(2^{d\cdot N^{3}})$ for some constant $d$. If
the size of the sequence $\gamma_{1},\dots,\gamma_{n}$ is greater than
$\mathcal{O}(2^{d\cdot N^{3}})$, then there must exist distinct formulas
$\gamma_{i}$ and $\gamma_{j}$ such that
$\gamma_{i}^{\prime}=\gamma_{j}^{\prime}$, i.e., $\gamma_{i}$ and $\gamma_{j}$
are identical up to the replacement of variables not occurring in
$\mathit{fv}\left(\gamma\right)$. But then $\gamma_{i}$ and $\gamma_{j}$ would
be variable-redundant, which contradicts our assumption. Therefore,
$\Sigma_{i=1}^{n}\mathit{size}(\gamma_{i})=\mathcal{O}(2^{d\cdot N^{3}})$.

Necessarily $\mathit{size}(\gamma)=\mathcal{O}(N)$, because no rule can
increase the size of the left-hand side of the sequents above $N$: indeed, the
only rule that can add new atoms to the left-hand side is UL, and this rule is
applied only on single atoms, which entails that the left-hand side of the
obtained sequent is of the same size as the right-hand side of one of the
rules in ${\cal R}$.

We deduce that the size of the sequents occurring in the proof tree is at most
$\mathcal{O}(2^{d\cdot N^{3}})$ for some constant $d$, and by Proposition 30,
there are at most $\mathcal{O}(2^{2^{c\cdot N^{3}}})$ distinct sequents (for
some constant $c$, up to a renaming of variables). This entails that the
constructed proof tree is rational. ∎

##  11 Discussion

Due to the high expressive power of pc-SIDs, the conditions ensuring
termination (Theorems 68 and 83) are necessarily restrictive. In the light of
the undecidability result in [13], one cannot hope for more. Theorem 65 shows
that, even if the conditions are not satisfied, the calculus is still useful
as a semi-decision procedure to detect non-validity. The complexity of the
procedure for $\emptyset$-constrained formulas cannot be improved
significantly since entailment checking is $2$-$\mathsf{EXPTIME}$-hard [11].
The high complexity of entailment testing is unsatisfactory in practice. We
thus plan to investigate fragments of inductive rules for which the devised
calculus yields an efficient decision procedure. As emphasized by the lower-
bound result in [11], which relies on very simple data structures and by the
fact that language inclusion is already $\mathsf{EXPTIME}$-complete for tree
automata [30], there is no hope that this can be achieved by restricting only
the shape of the structures: it is also necessary to strongly restrict the
class of inductive rules (forbidding for instance overlapping rules). We will
also try to identify classes of entailments for which the procedure terminates
for nonempty theories, under reasonable conditions on the theory. Another
problem that can be of practical interest is to extract countermodels of non-
valid (or irreducible) entailments. Finally, we plan to extend the proof
procedure in order to solve bi-abduction problems, a generalized form of
abduction which plays a central rôle for the efficiency and scalability of
program analysis algorithms [5].

#### Acknowledgments.

This work has been partially funded by the the French National Research Agency
(ANR-21-CE48-0011). The authors wish to thank Radu Iosif for his comments on
the paper and for fruitful discussions.

## References

  * [1] J. Berdine, C. Calcagno, and P. W. O’Hearn.  A decidable fragment of separation logic.  In Proc. of FSTTCS’04, volume 3328 of LNCS. Springer, 2004\.
  * [2] J. Berdine, B. Cook, and S. Ishtiaq.  Slayer: Memory safety for systems-level code.  In G. G. 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] J. Brotherston and A. Simpson.  Sequent calculi for induction and infinite descent.  Journal of Logic and Computation, 21(6):1177–1216, December 2011\.
  * [4] C. Calcagno, D. Distefano, J. Dubreil, D. Gabi, P. Hooimeijer, M. Luca, P. W. O’Hearn, I. Papakonstantinou, J. Purbrick, and D. Rodriguez.  Moving fast with software verification.  In K. Havelund, G. J. Holzmann, and R. Joshi, editors, NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, volume 9058 of LNCS, pages 3–11. Springer, 2015.
  * [5] C. Calcagno, D. Distefano, P. W. O’Hearn, and H. Yang.  Compositional shape analysis by means of bi-abduction.  J. ACM, 58(6):26:1–26:66, 2011.
  * [6] C. Calcagno, H. Yang, and P. W. O’hearn.  Computability and complexity results for a spatial assertion language for data structures.  In FST TCS 2001, Proceedings, pages 108–119. Springer, 2001.
  * [7] B. Cook, C. Haase, J. Ouaknine, M. J. Parkinson, and J. Worrell.  Tractable reasoning in a fragment of separation logic.  In Proc. of CONCUR’11, volume 6901 of LNCS. Springer, 2011\.
  * [8] S. Demri, D. Galmiche, D. Larchey-Wendling, and D. Méry.  Separation logic with one quantified variable.  In CSR’14, volume 8476 of LNCS, pages 125–138. Springer, 2014.
  * [9] M. Dodds and D. Plump.  From hyperedge replacement to separation logic and back.  Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 16, 2008.
  * [10] K. Dudka, P. Peringer, and T. Vojnar.  Predator: A practical tool for checking manipulation of dynamic data structures using separation logic.  In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of LNCS, pages 372–378. Springer, 2011.
  * [11] M. Echenim, R. Iosif, and N. Peltier.  Entailment checking in separation logic with inductive definitions is 2-exptime hard.  In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 191–211. EasyChair, 2020.
  * [12] M. Echenim, R. Iosif, and N. Peltier.  Decidable entailments in separation logic with inductive definitions: Beyond establishment.  In CSL 2021: 29th International Conference on Computer Science Logic, EPiC Series in Computing. EasyChair, 2021.
  * [13] M. Echenim and N. Peltier.  Two results on separation logic with theory reasoning.  In ASL 2022 (Workshop on Advancing Separation Logic), 2022.  https://arxiv.org/abs/2206.09389.
  * [14] C. Enea, O. Lengál, M. Sighireanu, and T. Vojnar.  Compositional entailment checking for a fragment of separation logic.  Formal Methods Syst. Des., 51(3):575–607, 2017.
  * [15] C. Enea, M. Sighireanu, and Z. Wu.  On automated lemma generation for separation logic with inductive definitions.  In ATVA 2015, Proceedings, pages 80–96, 2015.
  * [16] D. Galmiche and D. Méry.  Labelled cyclic proofs for separation logic.  J. Log. Comput., 31(3):892–922, 2021.
  * [17] R. Iosif, A. Rogalewicz, and J. Simacek.  The tree width of separation logic with recursive definitions.  In Proc. of CADE-24, volume 7898 of LNCS, 2013.
  * [18] R. Iosif, A. Rogalewicz, and T. Vojnar.  Deciding entailments in inductive separation logic with tree automata.  In F. Cassez and J. Raskin, editors, ATVA 2014, Proceedings, volume 8837 of LNCS, pages 201–218. Springer, 2014.
  * [19] S. S. Ishtiaq and P. W. O’Hearn.  Bi as an assertion language for mutable data structures.  In ACM SIGPLAN Notices, volume 36, pages 14–26, 2001.
  * [20] C. Jansen, F. Göbe, and T. Noll.  Generating inductive predicates for symbolic execution of pointer-manipulating programs.  In H. Giese and B. König, editors, ICGT 2014, volume 8571 of LNCS, pages 65–80. Springer, 2014.
  * [21] Q. L. Le.  Compositional satisfiability solving in separation logic.  In F. Henglein, S. Shoham, and Y. Vizel, editors, Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings, volume 12597 of Lecture Notes in Computer Science, pages 578–602. Springer, 2021\.
  * [22] K. Nakazawa, M. Tatsuta, D. Kimura, and M. Yamamura.  Cyclic Theorem Prover for Separation Logic by Magic Wand.  In ADSL 18 (First Workshop on Automated Deduction for Separation Logics), July 2018.  Oxford, United Kingdom.
  * [23] P. W. O’Hearn, J. C. Reynolds, and H. Yang.  Local reasoning about programs that alter data structures.  In L. Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of LNCS, pages 1–19. Springer, 2001.
  * [24] J. Pagel, C. Matheja, and F. Zuleger.  Complete entailment checking for separation logic with inductive definitions, 2020.
  * [25] J. Pagel and F. Zuleger.  Beyond symbolic heaps: Deciding separation logic with inductive definitions.  In LPAR-23, volume 73 of EPiC Series in Computing, pages 390–408. EasyChair, 2020.
  * [26] J. A. N. Pérez and A. Rybalchenko.  Separation logic modulo theories.  In C. Shan, editor, Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013\. Proceedings, volume 8301 of LNCS, pages 90–106. Springer, 2013.
  * [27] R. Piskac, T. Wies, and D. Zufferey.  Automating separation logic using SMT.  In N. Sharygina and H. Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of LNCS, pages 773–789. Springer, 2013.
  * [28] X. Qiu, P. Garg, A. Stefanescu, and P. Madhusudan.  Natural proofs for structure, data, and separation.  In H. Boehm and C. Flanagan, editors, ACM SIGPLAN PLDI ’13, pages 231–242. ACM, 2013.
  * [29] J. Reynolds.  Separation Logic: A Logic for Shared Mutable Data Structures.  In Proc. of LICS’02, 2002.
  * [30] H. Seidl.  Haskell overloading is dexptime-complete.  Inf. Process. Lett., 52(2):57–60, 1994.
  * [31] M. Tatsuta, K. Nakazawa, and D. Kimura.  Completeness of cyclic proofs for symbolic heaps with inductive definitions.  In A. W. Lin, editor, Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, volume 11893 of LNCS, pages 367–387. Springer, 2019.
  * [32] Z. Xu, T. Chen, and Z. Wu.  Satisfiability of compositional separation logic with tree predicates and data constraints.  In L. de Moura, editor, CADE 26, volume 10395 of LNCS, pages 509–527. Springer, 2017.