On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions

Peltier, Nicolas

doi:10.4230/LIPIcs.CSL.2026.16

On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions

Nicolas Peltier

Univ. Grenoble Alpes, CNRS, LIG, F-38000 Grenoble, France

Abstract

Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules – known as PCE (Progressing, Connected, and Established) – has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated.

Keywords and phrases:

Separation logic, Dynamic logic, Entailment problem

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic and verification ; Theory of computation

\rightarrow

Automated reasoning

Acknowledgements:

The author wishes to thank the anonymous referees for their valuable comments.

Funding:

This work has been partially funded by the French National Research Agency under project ANR-21-CE48-0011.

DOI:

10.4230/LIPIcs.CSL.2026.16

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Separation Logic (SL) has emerged as a central formalism for reasoning about mutable data structures in program verification [14, 17]. Its core contribution lies in enabling local reasoning: the ability to specify and verify properties of program fragments by focusing only on the memory cells they access, without requiring global knowledge of the entire heap. This locality principle has proved useful in scaling formal verification to realistic programs, particularly those involving pointer manipulation and dynamic memory allocation. At the heart of SL is the separating conjunction, a connective that expresses spatial separation between heap fragments. Combined with inductive definitions with a fixpoint semantics, this allows for elegant and concise specifications of custom linked data structures such as lists or trees. This gives rise to rich logical systems that support expressive specifications. These extensions introduce significant challenges for automation: while satisfiability is decidable [2], the entailment problem – deciding whether one SL formula is a logical consequence of another – is undecidable in general. Consequently, a substantial body of work has been devoted to identifying fragments of Separation Logic with recursive definitions for which the entailment problem is decidable (see, e.g., [1, 3, 4, 11, 10, 6, 13, 18]). Among these, a particularly expressive and well-structured class of inductive definitions, known as PCE rules (for Progressing, Connected, and Established), was introduced in [12]. For this class, entailment in SL was shown to be $2$ -ExpTime complete [15]. The original proof is based on a reduction to monadic second-order logic (MSO) over graphs of bounded tree width, a highly general approach that, however, does not yield efficient procedures in practice. More recently, optimal (doubly exponential) decision procedures for the PCE fragment have been proposed (e.g., [15, 9]), significantly improving the theoretical and practical feasibility of automated reasoning.

Despite these advances, traditional forms of SL remain insufficient to express and verify certain dynamic behaviors of programs, particularly those involving changes in control flow or temporal evolution of the heap. To address these limitations, Dynamic Separation Logic (DSL) has been proposed [5] as an extension of SL with dynamic modalities, inspired by dynamic logic. These modalities enable reasoning not only about static heap configurations but also about how these configurations evolve during program execution. By incorporating modalities for program actions, DSL enables to express the result of actions that operate on data structures directly within the logic’s syntax (using construction of the form $[\mathtt{a}]\,\phi$ , meaning that $\phi$ holds after action $\mathtt{a}$ is applied). This extension increases the expressiveness of SL, making it well-suited for modeling and verifying complex program behaviors, including dynamic allocation patterns. This approach provides a compelling alternative to traditional methods based on Hoare logic and weakest precondition calculi [16] for reasoning about sequential heap manipulations. It avoids the use of the separating implication, which, although essential in the weakest precondition calculus (as it enables to express extensions of the heap), poses challenges for automated reasoning.

This paper builds on these foundational insights to explore the entailment problem in Dynamic Separation Logic (DSL), focusing on inductive definitions that satisfy the PCE conditions established in [12]. We prove that entailment is decidable for a specific fragment – namely, formulas built on the connectives $\vee,\wedge,\star$ together with existential quantifications and dynamic modalities – by showing that the dynamic modalities introduced in DSL can be systematically and automatically eliminated (for PCE rules). Specifically, we present a transformation procedure that rewrites both the formulas and the inductive rules defining spatial predicates, while preserving equivalence. This reduction reduces the entailment problem in DSL to one in standard SL and enables the application of existing proof techniques and decision procedures. Remarkably, one of the crucial properties that enables this reduction is the same one that guarantees the decidability of the entailment problem [8]: the establishment property of [12]. Intuitively, this property ensures that the considered structures contain only a bounded number of “pending edges” (see Proposition 7).

The rest of the paper is structured as follows. Section 2 defines the syntax and semantics of the fragment of dynamic separation logic considered in this work. Section 3 recalls the definition of the properties of inductive rules that ensure the decidability of entailment. Section 4 introduces several useful transformations on formulas and rules, and shows that these transformations preserve equivalence under certain conditions. Section 5, the heart of the paper, presents a systematic and automatic procedure for eliminating dynamic modalities from formulas that meet the conditions defined in Section 3. Finally, Section 6 concludes the paper by outlining some interesting directions for future work.

2 Dynamic Separation Logic

We define the syntax and semantics of Dynamic Separation Logic as a natural extension of the definitions in [12], which address basic separation logic with recursive spatial predicates, and [5], which introduces dynamic modalities.

Basic notations

We begin by reviewing some basic notations. For any partial function $f$ , $\mathsf{dom}(f)$ denotes the domain of $f$ , $\mathit{img}(f)$ denotes its image (i.e., $\mathit{img}(f)=\{f(x)\mid x\in\mathsf{dom}(f)\}$ ) and $f|_{D}$ denotes the restriction of $f$ to $D$ . Two partial functions $f$ and $g$ are disjoint if their domains are disjoint, in which case $f\cup g$ denotes the function $h$ of domain $\mathsf{dom}(f)\cup\mathsf{dom}(g)$ defined as follows:

h(x)=\left\{\begin{array}[]{lr}f(x)&\text{if $x\in\mathsf{dom}(f)$}\\ g(x)&\text{if $x\in\mathsf{dom}(g)$}\\ \mathit{undefined}&\text{otherwise}\end{array}\right.

For every function $f$ and elements $x$ , $y$ , we denote by $f[x\leftarrow y]$ the function such that $\mathsf{dom}(f[x\leftarrow y])=\mathsf{dom}(f)\cup\{x\}$ , $f[x\leftarrow y](x)=y$ and $f[x\leftarrow y](x^{\prime})=f(x^{\prime})$ if $x^{\prime}\in\mathsf{dom}(f)\setminus\{x\}$ . For any binary relation $\rightarrow$ , $\rightarrow^{+}$ (resp. $\rightarrow^{*}$ ) denotes the transitive closure (resp. the reflexive and transitive closure) of $\rightarrow$ .

Syntax

We now define the syntax of DSL. We begin by defining the notion of actions, which are atomic operations on structures, including assignments $x\leftarrow y$ , look-ups $x\leftarrow z.i$ , redirections $x.i\leftarrow y$ , disallocations $\mathtt{dispose(x)}$ and allocations $x\leftarrow\mathtt{cons}(z_{1},\dots,z_{\kappa})$ ( $x$ is allocated with fields pointing to $z_{1},\dots,z_{\kappa}$ ). The semantics of actions is intuitive and will be formally defined in a later section.

Definition 1 (Actions).

Let ${\cal V}$ be a countably infinite set of variables and let $\kappa\in\mathbb{N}$ (denoting a number of record fields). The set of actions ${\cal A}$ is the set of expressions of the following forms:

x\leftarrow y\quad|\quad x\leftarrow z.i\quad|\quad x.i\leftarrow y\quad|\quad% \mathtt{dispose(x)}\quad|\quad x\leftarrow\mathtt{cons}(z_{1},\dots,z_{\kappa})

with $x,y,z\in{\cal V}$ , $x\not=z$ , $z_{1},\dots,z_{\kappa}$ is a tuple of variables not containing $x$ and $i\in\{1,\dots,\kappa\}$ .

The conditions $x\not=z$ and $x\not\in\{z_{1},\dots,z_{\kappa}\}$ are meant to simplify forthcoming definitions (they are not restrictive; for instance, an action $z\leftarrow z.1$ could be replaced by a sequence of two actions $z^{\prime}\leftarrow z.1$ and $z\leftarrow z^{\prime}$ , where $z^{\prime}$ is a fresh variable).

The syntax of DSL formulas includes the standard logical connectives $\vee,\wedge$ and quantifier $\exists$ , as well as the special connective $\star$ of separation logic and a modality $[\mathtt{a}]\,\psi$ , which asserts that formula $\psi$ holds after action $\mathtt{a}$ is applied. Atomic formulas include points-to atoms $y\mapsto(x_{1},\dots,x_{\kappa})$ , stating that $y$ is the only allocated locations and refers to the tuple $(x_{1},\dots,x_{\kappa})$ , as well a spatial predicate atoms, which are intended to denote recursive data structures (e.g., lists or trees). As usual in SL, negations are not allowed.

Definition 2 (Syntax of Dynamic Separation Logic).

Let ${\cal P}$ be a set of predicate symbols, where each symbol in $p\in{\cal P}$ is associated with a unique arity $\#(p)$ . A DSL formula $\phi$ (or simply formula) is built inductively as follows:

p(x_{1},\dots,x_{n})\quad|\quad y\mapsto(x_{1},\dots,x_{\kappa})\quad|\quad x% \simeq y\quad|\quad x\not\simeq y\quad|\quad

(\phi_{1}\star\phi_{2})\quad|\quad(\phi_{1}\vee\phi_{2})\quad|\quad(\phi_{1}% \wedge\phi_{2})\quad|\quad\exists x\,\psi\quad|\quad[\mathtt{a}]\,\psi

where $n\in{\mathbb{N}}$ , $p$ is a predicate in ${\cal P}$ of arity $n$ , $x,x_{i}$ and $y$ are variables, $\mathtt{a}$ is an action and $\phi_{1},\phi_{2},\psi$ are formulas. The false formula $\bot$ is a shorthand for $x\not\simeq x$ (where $x$ is an arbitrary variable) and $\mathtt{emp}$ is a shorthand for $x\simeq x$ .

We emphasize that $x\not\simeq y$ it not exactly the negation of $x\simeq y$ , as both atoms require the heap to be empty (see Definition 5). For simplicity, the syntax excludes constants (e.g., $\mathtt{nil}$ ). This is not a limitation, as constants can be readily represented by variables passed as parameters to every predicate symbol. Formulas of the form $y\mapsto(x_{1},\dots,x_{\kappa})$ (resp. $p(x_{1},\dots,x_{n})$ ) are called $\mapsto$ -atoms (resp. ${\cal P}$ -atoms). We denote by $|\phi|$ the size of the formula $\phi$ (i.e., the number of occurrences of symbols in it). If $S=\{\phi_{1},\dots,\phi_{n}\}$ is a finite set of formulas, then $\bigvee S$ denotes the formula $\bigvee_{i=1}^{n}\phi_{i}$ . For every formula $\phi$ we denote by $\mathsf{fv}(\phi)$ the set of variables freely occurring in $\phi$ .

A formula is static if it contains no subformula of the form $[\mathtt{a}]\,\psi$ . A symbolic heap is a static formula that contains no occurrence of $\vee$ or $\wedge$ . If $\vec{x}=(x_{1},\dots,x_{n})$ and $\vec{y}=(y_{1},\dots,y_{n})$ are tuples of variables, then $\vec{x}\simeq\vec{y}$ is a shorthand for $\bigstar_{i=1}^{n}(x_{i}\simeq y_{i})$ (we use $\star$ instead of $\wedge$ to obtain a symbolic heap).

We now introduce the inductive rules that define the semantics of the predicates in ${\cal P}$ . A set of inductive rules (SID) is a set ${\cal R}$ of rules $p(x_{1},\dots,x_{n})\Leftarrow\phi$ , where $p$ is a predicate of arity $n$ in ${\cal P}$ and $\phi$ is a symbolic heap such that $\mathsf{fv}(\phi)\subseteq\{x_{1},\dots,x_{n}\}$ . We assume that for any given predicate $p$ there are finitely many rules of the above form (but the sets ${\cal P}$ and ${\cal R}$ may be infinite). Examples of inductive definitions will be presented in a later section. Given two predicate symbols $p,q\in{\cal P}$ , we write $p\succ_{{\cal R}}q$ if ${\cal R}$ contains a rule of the form $p(x_{1},\dots,x_{n})\Leftarrow\phi$ where $q$ occurs in $\phi$ . Note that actions are not allowed inside inductive rules (such rules are used to denote recursive data structures of unbounded size, not sequences of operations).

A substitution is a mapping from variables to variables. If $x_{1},\dots,x_{n}$ are pairwise distinct, then the set $\{x_{i}\leftarrow y_{i}\mid 1\leq i\leq n\}$ denotes a substitution $\sigma$ such that $\sigma(x_{i})=y_{i}$ for all $i\in\{1,\dots,n\}$ and $\sigma(z)=z$ if $z\not\in\{x_{1},\dots,x_{n}\}$ . For any expression (formula, variable or tuples of variables) $\phi$ and substitution $\sigma$ , $\phi\sigma$ denotes the expression obtained from $\phi$ by replacing every free occurrence of every variable $x$ by $\sigma(x)$ (using $\alpha$ -renaming to avoid variable capture).

If ${\cal R}$ is a SID, we write $\psi\rightarrow_{{\cal R}}\psi^{\prime}$ (and say that “ $\psi$ unfolds to $\psi^{\prime}$ ”) if ${\cal R}$ contains a rule $p(x_{1},\dots,x_{n})\Leftarrow\phi$ and $\psi^{\prime}$ is obtained from $\psi$ by replacing one occurrence of a formula $p(y_{1},\dots,y_{n})$ by $\phi\{x_{i}\leftarrow y_{i}\mid 1\leq i\leq n\}$ (i.e., the formal parameters $x_{i}$ are replaced by the actual parameters $y_{i}$ , the existential variables in $\phi$ are renamed if needed to avoid collisions with variables occurring in $\psi$ ).

Semantics

We are now in the position to define the semantics of DSL. The formulas are interpreted in structures defined as follows.

Definition 3 (Structures).

Let ${\cal L}$ be a countably infinite set of locations. A store is a function mapping every variable to a location. A heap is a partial function mapping some locations to $\kappa$ -tuples of locations, with a finite domain. A structure is a pair $(\mathfrak{s},\mathfrak{h})$ , where $\mathfrak{s}$ is a store and $\mathfrak{h}$ is a heap.
A location $\ell$ (resp. a variable $x$ ) is allocated in a heap $\mathfrak{h}$ (resp. in a structure $(\mathfrak{s},\mathfrak{h})$ ) if $\ell\in\mathsf{dom}(\mathfrak{h})$ (resp. if $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ ).

A heap $\mathfrak{h}$ of domain $\ell_{1},\dots,\ell_{n}$ with $\mathfrak{h}(\ell_{i})=\vec{t}_{i}$ for all $i\in\{1,\dots,n\}$ is denoted by $\{\ell_{1}\mapsto\vec{t}_{1},\dots,\ell_{n}\mapsto\vec{t}_{n}\}$ . We denote by $|\mathfrak{h}|$ the size of $\mathfrak{h}$ , i.e., the cardinality of $\mathsf{dom}(\mathfrak{h})$ (which is finite by hypothesis) and by $\mathit{locs}(\mathfrak{h})$ the set of locations occurring in $\mathfrak{h}$ , i.e.: $\mathit{locs}(\mathfrak{h})=\{\ell_{i}\mid\ell_{0}\in\mathsf{dom}(\mathfrak{h}% ),\mathfrak{h}(\ell_{0})=(\ell_{1},\dots,\ell_{\kappa}),0\leq i\leq\kappa\}$ .

The relation $\leadsto_{\mathtt{a}}$ formalizes the effect of applying an action on a structure:

Definition 4 (Applying Actions on Structures).

Let $(\mathfrak{s},\mathfrak{h})$ and $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})$ be two structures and let $\mathtt{a}\in{\cal A}$ . We write $(\mathfrak{s},\mathfrak{h})\leadsto_{\mathtt{a}}(\mathfrak{s}^{\prime},% \mathfrak{h}^{\prime})$ if one of the following assertions holds:

$\blacksquare$

$\mathtt{a}=x\leftarrow y$ , $\mathfrak{h}^{\prime}=\mathfrak{h}$ and $\mathfrak{s}^{\prime}=\mathfrak{s}[x\leftarrow\mathfrak{s}(y)]$
$\blacksquare$

$\mathtt{a}=x.i\leftarrow y$ , $\mathfrak{s}^{\prime}=\mathfrak{s}$ , $\mathfrak{h}(\mathfrak{s}(x))=(\ell_{1},\dots,\ell_{\kappa})$ and $\mathfrak{h}^{\prime}$ is the following heap:
$\mathfrak{h}^{\prime}=\mathfrak{h}[\mathfrak{s}(x)\leftarrow(\ell_{1},\dots,% \ell_{i-1},\mathfrak{s}(y),\ell_{i+1},\dots,\ell_{\kappa})]$ .
$\blacksquare$

$\mathtt{a}=x\leftarrow y.i$ , $\mathfrak{h}^{\prime}=\mathfrak{h}$ , $\mathfrak{h}(\mathfrak{s}(y))=(\ell_{1},\dots,\ell_{\kappa})$ and $\mathfrak{s}^{\prime}=\mathfrak{s}[x\leftarrow\ell_{i}]$ .
$\blacksquare$

$\mathtt{a}=\mathtt{dispose(x)}$ , $\mathfrak{s}^{\prime}=\mathfrak{s}$ , $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ and $\mathfrak{h}^{\prime}$ is the restriction of $\mathfrak{h}$ such that $\mathsf{dom}(\mathfrak{h}^{\prime})=\mathsf{dom}(\mathfrak{h})\setminus\{% \mathfrak{s}(x)\}$ .
$\blacksquare$

$\mathtt{a}=x\leftarrow\mathtt{cons}(y_{1},\dots,y_{\kappa})$ , $\ell\in{\cal L}\setminus\mathsf{dom}(\mathfrak{h})$ , $\mathfrak{s}^{\prime}=\mathfrak{s}[x\leftarrow\ell]$ , $\mathfrak{h}^{\prime}=\mathfrak{h}[\ell\leftarrow(\mathfrak{s}(y_{1}),\dots,% \mathfrak{s}(y_{\kappa}))]$ .

An action $\mathtt{a}$ fails on $(\mathfrak{s},\mathfrak{h})$ if there is no structure $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})$ such that $(\mathfrak{s},\mathfrak{h})\leadsto_{\mathtt{a}}(\mathfrak{s}^{\prime},% \mathfrak{h}^{\prime})$ .

The satisfiability relations $\models_{{\cal R}}^{n}$ and $\models_{{\cal R}}$ are defined as follows (the exponent $n$ denotes the maximal number of nested applications of inductive rules in ${\cal R}$ ).

Definition 5 (Satisfiability Relation).

We write $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi$ if one of the following conditions holds:

$\blacksquare$

$\phi$ is of the form $(x\simeq y)$ (resp. $(x\not\simeq y)$ ), $\mathfrak{h}=\emptyset$ and $\mathfrak{s}(x)=\mathfrak{s}(y)$ (resp. $(\mathfrak{s}(x)\not=\mathfrak{s}(y)$ ).
$\blacksquare$

$\phi$ is of the form $x\mapsto(y_{1},\dots,y_{\kappa})$ and $\mathfrak{h}=\{\mathfrak{s}(x)\mapsto(\mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y% _{\kappa}))\}$ .
$\blacksquare$

$\phi$ is of the form $\phi_{1}\vee\phi_{2}$ (resp. $\phi_{1}\wedge\phi_{2}$ ) and $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi_{i}$ holds for some $i\in\{1,2\}$ (resp. for all $i\in\{1,2\}$ ).
$\blacksquare$

$\phi$ is of the form $\phi_{1}\star\phi_{2}$ and there exist disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that $\mathfrak{h}=\mathfrak{h}_{1}\cup\mathfrak{h}_{2}$ and $(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}^{n}\phi_{i}$ , for all $i\in\{1,2\}$ .
$\blacksquare$

$\phi$ is of the form $\exists x\,\psi$ and there exists $\ell\in{\cal L}$ such that $(\mathfrak{s}[x\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}^{n}\psi$ .
$\blacksquare$

$\phi$ is of the form $p(x_{1},\dots,x_{n})$ , $\phi\rightarrow_{{\cal R}}\psi$ , $n>0$ and $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n-1}\psi$ .
$\blacksquare$

$\phi$ is of the form $[\mathtt{a}]\,\psi$ , $\mathtt{a}$ does not fail on $(\mathfrak{s},\mathfrak{h})$ and $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\models_{{\cal R}}^{n}\psi$ for all $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})$ such that $(\mathfrak{s},\mathfrak{h})\leadsto_{\mathtt{a}}(\mathfrak{s}^{\prime},% \mathfrak{h}^{\prime})$ .

We write $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ if $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi$ for some $n\in\mathbb{N}$ , and in this case $(\mathfrak{s},\mathfrak{h})$ is called an ${\cal R}$ -model of $\phi$ . We write $\phi\models_{{\cal R}}\psi$ if the entailment $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\implies(\mathfrak{s},% \mathfrak{h})\models_{{\cal R}}\psi$ holds for all structures $(\mathfrak{s},\mathfrak{h})$ , and $\phi\equiv_{{\cal R}}\psi$ if we have both $\phi\models_{{\cal R}}\psi$ and $\psi\models_{{\cal R}}\phi$ .

It is straightforward to verify that $\models_{{\cal R}}^{n}\subseteq\models_{{\cal R}}^{n+1}$ for all $n\in\mathbb{N}$ . Moreover, if $\phi$ contains no predicate symbols, then the satisfiability relation does not depend on ${\cal R}$ , and we may write $(\mathfrak{s},\mathfrak{h})\models\phi$ instead of $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ . Finally, if $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ , then there exists a formula $\psi$ containing no symbols from ${\cal P}$ such that $\phi\rightarrow_{{\cal R}}^{*}\psi$ and $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\psi$ .

Note that equalities and disequalities are satisfied only by structures with an empty heap. This convention simplifies the notation by allowing us to omit standard conjunctions in certain cases, and it is not restrictive in our setting. Also note that there is no formula that is satisfied by all structures – this property is essential for the decidability of entailment in standard SL, if standard conjunctions are allowed [15].

3 PCE Rules

We now recall several definitions from [12], introducing conditions on the inductive rules that, in standard Separation Logic, ensure the decidability of the entailment problem. Intuitively, these conditions ensure that each rule allocates exactly one location, that the set of allocated locations has a tree-shaped structure, and that every location is either allocated or associated with a free variable.

Definition 6 (Progress, Connectedness and Establishment (PCE)).

A rule $p(x_{1},\dots,x_{n})\leftarrow\exists\vec{y}\,\phi$ is:

$\blacksquare$

progressing if $\phi$ is of the form $x_{1}\mapsto(z_{1},\dots,z_{\kappa})\star\phi^{\prime}$ , where $\phi^{\prime}$ contains no $\mapsto$ -atom (i.e., the rule allocates exactly one location $x_{1}$ );
$\blacksquare$

connected if, moreover, every predicate atom in $\phi^{\prime}$ is of the form $q(z,\vec{v})$ with $z\in\{z_{1},\dots,z_{\kappa}\}$ (i.e., the locations allocated by the called predicates are successors of $x_{1}$ ).

A SID ${\cal R}$ is progressing (resp. connected) if all the rules in ${\cal R}$ are progressing (resp. connected). It is established if for every atom $p(x_{1},\dots,x_{n})$ and for every formula $\phi$ containing no predicate symbol, if $p(x_{1},\dots,x_{n})\rightarrow_{{\cal R}}^{*}\phi$ and $x$ is existentially quantified in $\phi$ then $\phi$ contains atoms $y_{i}\simeq y_{i+1}$ (for $i=0,\dots,n$ , with $n\geq 0$ ) such that $x=y_{n+1}$ and either $\phi$ contains a $\mapsto$ -atom of the form $y_{0}\mapsto(\vec{z})$ or $y_{0}\in\{x_{1},\dots,x_{n}\}$ (i.e., every existentially quantified variable either is equal to a free variable or is eventually allocated).

The following proposition recalls a key property of PCE rules: in every model of a quantifier-free formula, all locations that do not correspond to free variables are allocated.

Proposition 7.

Let $\phi$ be a static formula containing no quantifier. Let $(\mathfrak{s},\mathfrak{h})$ be an ${\cal R}$ -model of $\phi$ . If ${\cal R}$ is PCE, then $\mathit{locs}(\mathfrak{h})\subseteq\mathsf{dom}(\mathfrak{h})\cup\{\mathfrak{% s}(x)\mid x\in\mathsf{fv}(\phi)\}$ .

Example 8.

The following rules, defining a non empty list segment from $x$ to $y$ are PCE:

\mathtt{lseg}(x,y)\Leftarrow x\mapsto(y)\qquad\mathtt{lseg}(x,y)\Leftarrow% \exists z\,\bigl(x\mapsto(z)\star\mathtt{lseg}(z,y)\bigr)

In contrast, the following rules, defining the same structures, are not PCE, because the second rule contains no $\mapsto$ -atom (hence is not progressing):

\mathtt{lseg}^{\prime}(x,y)\Leftarrow x\mapsto(y)\qquad\mathtt{lseg}^{\prime}(% x,y)\Leftarrow\exists z\,\bigl(\mathtt{lseg}^{\prime}(x,z)\star\mathtt{lseg}^{% \prime}(z,y)\bigr)

The following rules, defining a list segment with last cell $z$ , are not connected.

\mathtt{lseg}^{\prime\prime}(z,x,y)\Leftarrow z\mapsto(y)\star z\simeq x\qquad% \mathtt{lseg}^{\prime\prime}(z,x,y)\Leftarrow\exists u\,\bigl(z\mapsto(y)\star% \mathtt{lseg}(u,x,z)\bigr)

The following PCE rules define a tree rooted at $x$ , where all nodes have an additional pointer to their parent node $y$ and the leaves point to $z$ :

\begin{array}[]{lcl}\mathtt{tree}(x,y,z)&\Leftarrow&\exists x_{1},x_{2}\,\bigl% (x\mapsto(x_{1},x_{2},y)\star\mathtt{tree}(x_{1},x,z)\star\mathtt{tree}(x_{2},% x,z)\bigr)\\ \mathtt{tree}(x,y,z)&\Leftarrow&x\mapsto(z,z,y)\end{array}

4 Some Basic Transformations on Inductive Predicates

In this section, we introduce a set of transformations that apply to formulas and the inductive rules defining the predicates they contain. These transformations preserve equivalence (under certain conditions) and will serve as the foundation for the algorithm that eliminates modalities, presented in the next section. We begin with the notion of context predicates (borrowed and adapted from [18, 9]), which enable the extraction of some predicate calls $q$ from the rules of a predicate symbol $p$ , lifting them to the initial formula.

Definition 9 (Context Predicates).

For every pair of predicates $p, q$ with $\#(p)=n$ and $\#(q)=m$ , we define a predicate $(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}p)$ of arity $n+m$ associated with the following rules, for each rule of the form $p(u_{1},\dots,u_{n})\Leftarrow\exists\vec{w}\,(u_{1}\mapsto(\vec{y})\star p^{% \prime}(\vec{z})\star\psi)$ in ${\cal R}$ (modulo AC):

(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}p)(u_{1},\dots,u_{n},v_{1},\dots,v_{m})\Leftarrow\exists\vec{w}% \,(u_{1}\mapsto(\vec{y})\star(q\mathrel{\includegraphics{dagpub-standalone-% manual-2026-03-04-19-20-35-page-2.pdf2svg.svg}}p^{\prime})(\vec{z},v_{1},\dots% ,v_{m})\star\psi)

(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}p)(u_{1},\dots,u_{n},v_{1},\dots,v_{m})\Leftarrow\exists\vec{w}% \,(u_{1}\mapsto(\vec{y})\star\vec{z}\simeq(v_{1},\dots,v_{m})\star\psi)\text{% \quad if $q=p^{\prime}$}

The rules of $(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}p)(x_{1},\dots,x_{n},y_{1},\dots,y_{m})$ are obtained from those of $p(x_{1},\dots,x_{n})$ by removing exactly one call to the atom $q(y_{1},\dots,y_{m})$ (occurring at some non-root position in the derivation tree). Consequently, $(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}p)(x_{1},\dots,x_{n},y_{1},\dots,y_{m})$ is satisfied by all (non-empty) structures that will satisfy $p(x_{1},\dots,x_{n})$ after a disjoint heap satisfying $q(y_{1},\dots,y_{m})$ is added to the current heap. It is easy to check that the rules of $(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}p)$ fulfill the conditions of Definition 6.

Example 10.

Let $p, q$ be predicates associated with the following rules:

\begin{array}[]{lcl}p(x)&\Leftarrow&\exists y,z\,\bigl(x\mapsto(y,z)\star p(y)% \star q(z,y)\bigr)\\ q(z,y)&\Leftarrow&\exists z^{\prime}\,\bigl(z\mapsto(z^{\prime},z^{\prime})% \star q(z^{\prime},z)\bigr)\\ q(z,y)&\Leftarrow&z\mapsto(y,y)\end{array}

The predicate $(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}p)$ is defined as follows:

\begin{array}[]{lcl}(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-% 03-04-19-20-35-page-2.pdf2svg.svg}}p)(x,u,v)&\Leftarrow&\exists y,z\,\bigl(x% \mapsto(y,z)\star(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-% 04-19-20-35-page-2.pdf2svg.svg}}p)(y,u,v)\star q(z,y)\bigr)\\ (q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}p)(x,u,v)&\Leftarrow&\exists y,z\,\bigl(x\mapsto(y,z)\star p(y)% \star(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-% page-2.pdf2svg.svg}}q)(z,y,u,v)\bigr)\\ (q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}p)(x,u,v)&\Leftarrow&\exists y,z\,\bigl(x\mapsto(y,z)\star p(y)% \star z\simeq u\star y\simeq v\bigr)\\ (q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}q)(z,y,u,v)&\Leftarrow&\exists z^{\prime}\,\bigl(z\mapsto(z^{% \prime},z^{\prime})\star(q\mathrel{\includegraphics{dagpub-standalone-manual-2% 026-03-04-19-20-35-page-2.pdf2svg.svg}}q)(z^{\prime},z,u,v)\bigr)\\ (q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-% 2.pdf2svg.svg}}q)(z,y,u,v)&\Leftarrow&\exists z^{\prime}\,\bigl(z\mapsto(z^{% \prime},z^{\prime})\star z^{\prime}\simeq u\star z\simeq v\bigr)\\ \end{array}

The following lemma states that $q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-2% .pdf2svg.svg}}p$ denotes the structures obtained by removing the subheap satisfying $q$ from a structure that satisfies $p$ .

Lemma 11.

Assume that ${\cal R}$ is PCE. Let $(\mathfrak{s},\mathfrak{h})$ be a structure, let $x$ be a variable and let $p(y_{1},\dots,y_{n})$ be a formula. If $\mathfrak{s}(x)\in dom(\mathfrak{h})$ and $\mathfrak{s}(x)\not=\mathfrak{s}(y_{1})$ then the two following assertions are equivalent:

$\blacksquare$

$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}p(y_{1},\dots,y_{n})$ .
$\blacksquare$

There exists a predicate $q$ of arity $m$ , pairwise distinct variables $z_{2},\dots,z_{m}$ , distinct from $x,y_{1},\dots,y_{n}$ and locations $\ell_{2},\dots,\ell_{n}$ such that $p\succ_{{\cal R}}^{+}q$ and:

$(\hat{\mathfrak{s}},\mathfrak{h})\models_{{\cal R}}(q\mathrel{\includegraphics% {dagpub-standalone-manual-2026-03-04-19-20-35-page-2.pdf2svg.svg}}p)(y_{1},% \dots,y_{n},x,z_{2},\dots,z_{m})\star q(x,z_{2},\dots,z_{m})$

with $\hat{\mathfrak{s}}=\mathfrak{s}[z_{i}\leftarrow\ell_{i}\mid i\in\{2,\dots,m\}]$ .

The following result follows immediately from Lemma 11:

Corollary 12.

Assume that ${\cal R}$ is PCE. Let $(\mathfrak{s},\mathfrak{h})$ be a structure such that $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ . Let $(z_{i})_{i\in\mathbb{N}}$ be a sequence of pairwise distinct variables, all distinct from $x,y_{1},\dots,y_{n}$ . Then the following equivalence holds:

(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}y_{1}\not\simeq x\star p(y_{1},% \dots,y_{n})\iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}y_{1}\not\simeq x% \star\bigvee\{\phi_{q}\mid p\succ_{{\cal R}}^{+}q\}

with $\phi_{q}=\exists z_{2},\dots,z_{m}\,\bigl((q\mathrel{\includegraphics{dagpub-% standalone-manual-2026-03-04-19-20-35-page-2.pdf2svg.svg}}p)(y_{1},\dots,y_{n}% ,x,z_{2},\dots,z_{m})\star q(x,z_{2},\dots,z_{m})\bigr)$ and $m=\#(q)$ .

The following definition associates each pair $(\phi,x)$ , consisting of a static formula $\phi$ and a variable $x$ , with a formula $\langle\phi\rangle^{\mathtt{N}(x)}$ . This transformation enriches $\phi$ by explicitly adding assertions that ensure $x$ is not allocated (see Lemma 15). It also implicitly extends the SID ${\cal R}$ by introducing new predicate symbols and rules, which enforce that $x$ is not allocated within the data structures described by the predicates occurring in $\phi$ .

Definition 13.

Let $\phi$ be a static formula and let $x$ be a variable. We denote by $\langle\phi\rangle^{\mathtt{N}(x)}$ the formula inductively defined as follows.

$\blacksquare$

If $\phi$ is of the form $y\simeq z$ or $y\not\simeq z$ then $\langle\phi\rangle^{\mathtt{N}(x)}=\phi$ .
$\blacksquare$

If $\phi$ is of the form $x^{\prime}\mapsto(y_{1},\dots,y_{\kappa})$ then $\langle\phi\rangle^{\mathtt{N}(x)}=\phi\star(x\not\simeq x^{\prime})$ .
$\blacksquare$

If $\phi=\phi_{1}\wedge\phi_{2}$ then $\langle\phi\rangle^{\mathtt{N}(x)}=\langle\phi_{1}\rangle^{\mathtt{N}(x)}% \wedge\phi_{2}$ .
$\blacksquare$

If $\phi=\phi_{1}\bullet\phi_{2}$ (with $\bullet\in\{\vee,\star\}$ ) then $\langle\phi\rangle^{\mathtt{N}(x)}=\langle\phi\rangle^{\mathtt{N}(x)}\bullet% \langle\phi_{2}\rangle^{\mathtt{N}(x)}$ .
$\blacksquare$

If $\phi=\exists y\,\psi$ then $\langle\phi\rangle^{\mathtt{N}(x)}=\exists y\,\langle\psi\rangle^{\mathtt{N}(x)}$ (we assume by $\alpha$ -renaming that $x\not=y$ ).
$\blacksquare$

If $\phi=p(x_{1},\dots,x_{n})$ then $\langle\phi\rangle^{\mathtt{N}(x)}={p}^{\prime}(x_{1},\dots,x_{n},x)$ if ${p}^{\prime}$ is a predicate symbol of arity $n+1$ , associated with rules of the form ${p}^{\prime}(y_{1},\dots,y_{n},y)\Leftarrow\langle\phi\rangle^{\mathtt{N}(y)}$ , for all rules of the form $p(y_{1},\dots,y_{n})\Leftarrow\phi$ occurring in ${\cal R}$ .

Note that, alternatively, one could define $\langle\phi_{1}\wedge\phi_{2}\rangle^{\mathtt{N}(x)}$ as $\langle\phi\rangle^{\mathtt{N}(x)}\wedge\langle\phi_{2}\rangle^{\mathtt{N}(x)}$ ; however, the chosen definition is more flexible and tends to yield simpler formulas. Due to the commutativity of $\wedge$ , the transformation can be applied to either conjunct without loss of generality. Since the transformation can be applied recursively, it may generate predicates of the form ${{p}^{\prime}}^{\prime}$ , ${{{p}^{\prime}}^{\prime}}^{\prime}$ , and so on. Consequently, both the set of rules ${\cal R}$ and the set of predicates ${\cal P}$ are infinite. This is not problematic in practice, as new predicates and rules are generated on demand.

Example 14.

Let $\phi$ be the formula $y\mapsto(u,v)\star(p(u)\vee p(v))$ where $p$ is defined as in Example 10. Then $\langle\phi\rangle^{\mathtt{N}(x)}$ is $y\mapsto(u,v)\star y\not\simeq x\star(p^{\prime}(u,x)\vee p^{\prime}(v,x))$ , where $p^{\prime}$ is defined as follows ( $x$ is renamed into $x^{\prime}$ in the first rule to avoid conflict):

\begin{array}[]{lcl}p^{\prime}(x,x^{\prime})&\Leftarrow&\exists y,z\,\bigl(x% \mapsto(y,z)\star x^{\prime}\not\simeq x\star p^{\prime}(y,x^{\prime})\star q^% {\prime}(z,y,x^{\prime})\bigr)\\ q^{\prime}(z,y,x)&\Leftarrow&\exists z^{\prime}\,\bigl(z\mapsto(z^{\prime},z^{% \prime})\star x\not\simeq z\star q^{\prime}(z^{\prime},z,x)\bigr)\\ q^{\prime}(z,y,x)&\Leftarrow&z\mapsto(y,y)\star z\not\simeq x\end{array}

Note that in every model of $\phi$ , $x$ is not allocated, because each $\mapsto$ -atom $u\mapsto(\dots)$ is associated with a disequation $x\not\simeq u$ .

We now establish the soundness of the transformation. Lemma 15 shows that $\langle\phi\rangle^{\mathtt{N}(x)}$ indeed captures the intended properties, i.e., that $\phi$ is true and $x$ is not allocated.

Lemma 15.

For every structure $(\mathfrak{s},\mathfrak{h})$ , for every static formula and for every variable $x$ , the following equivalence holds:

(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\langle\phi\rangle^{\mathtt{N}(x)% }\iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\wedge\mathfrak{s}(x)% \not\in\mathsf{dom}(\mathfrak{h})

We now introduce a similar but slightly more complex transformation. It associates every formula $\phi$ and variables $x,y_{1},\dots,y_{\kappa}$ with a formula $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ which is intended to denote the structures in which $\phi$ holds after a mapping $x\mapsto(y_{1},\dots,y_{\kappa})$ is added to the heap (see Lemma 18). In other words $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ is equivalent to the formula $(x\mapsto(y_{1},\dots,y_{\kappa}))\mathrel{\includegraphics{dagpub-standalone-% manual-2026-03-04-19-20-35-page-1.pdf2svg.svg}}\phi$ , where $\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-1.% pdf2svg.svg}}$ is the usual separating implication (a.k.a. “magic wand”) of SL (as defined for instance in [17]).

Definition 16.

Assume that ${\cal R}$ is PCE. Let $\phi$ be a static formula and let $x,y_{1},\dots,y_{\kappa}$ be variables. We denote by $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ the formula inductively defined as follows.

$\blacksquare$

If $\phi$ is of the form $y\simeq z$ or $y\not\simeq z$ then $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}=\bot$ .
$\blacksquare$

If $\phi$ is of the form $x^{\prime}\mapsto(y_{1}^{\prime},\dots,y_{\kappa}^{\prime})$ then $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}=(x\simeq x^{\prime})% \star\bigstar_{i=1}^{\kappa}(y_{i}\simeq y_{i}^{\prime})$ .
$\blacksquare$

If $\phi=\phi_{1}\bullet\phi_{2}$ (with $\bullet\in\{\vee,\wedge\}$ ) then $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}=\langle\phi_{1}\rangle|% _{x\mapsto(y_{1},\dots,y_{\kappa})}\bullet\langle\phi_{2}\rangle|_{x\mapsto(y_% {1},\dots,y_{\kappa})}$ .
$\blacksquare$

If $\phi=\phi_{1}\star\phi_{2}$ then $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ is the formula: $(\langle\phi_{1}\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}\star\phi_{2})\vee(% \phi_{1}\star\langle\phi_{2}\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})})$ .
$\blacksquare$

If $\phi=\exists z\,\psi$ then $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}=\exists z\,\langle\psi% \rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ (we assume by $\alpha$ -renaming that $z\not\in\{x,y_{1},\dots,y_{\kappa}\}$ ).
$\blacksquare$

If $\phi=p(z_{1},\dots,z_{n})$ and $z_{1}=x$ then $\langle p(z_{1},\dots,z_{n})\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ is:

$\bigvee\{\exists\vec{u}\,(\psi\star\bigstar_{j=1}^{\kappa}(y_{i}\simeq y_{i}^{% \prime}))\mid p(z_{1},\dots,z_{n})\rightarrow_{{\cal R}}\exists\vec{u}\,(z_{1}% \mapsto(y_{1}^{\prime},\dots,y_{\kappa}^{\prime})\star\psi)\}$

Note that the above set is finite (up to a renaming of variables) as there are finitely many rules associated with any given predicate $p$ .
$\blacksquare$

If $\phi=p(z_{1},\dots,z_{n})$ and $z_{1}\not=x$ then $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ is:

$(\langle p(x,z_{2},\dots,z_{n})\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}% \star(z_{1}\simeq x))\\ \vee\bigvee_{p\succ_{{\cal R}}^{+}q,\#(q)=m}(\exists u_{2},\dots,u_{m}\,% \langle q(x,u_{2},\dots,u_{m})\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}\\ \star(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-% page-2.pdf2svg.svg}}p)(z_{1},\dots,z_{n},x,u_{2},\dots,u_{m})\star(z_{1}\not% \simeq x))$

It is straightforward to check that the computation of $\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ always terminates. Indeed, in every item except the last one, the size of $\phi$ decreases strictly at each recursive call, whereas in the last item, all the calls are of the form $\langle r(x,\vec{z})\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ (for some $r\in{\cal P}$ ) and thus terminate immediately as there is no recursive call for the formulas of this form (see penultimate item).

Example 17.

Let $\phi$ be the formula $x\mapsto(y)\star\mathtt{lseg}(y,z)$ , where $\mathtt{lseg}$ is defined as in Example 8. Then $\langle\phi\rangle|_{u\mapsto(v)}$ is given by the following disjunction:

\begin{array}[]{c}x\simeq u\star y\simeq v\star\mathtt{lseg}(y,z)\\ \vee\;x\mapsto(y)\star\exists y^{\prime}\,\bigl(\mathtt{lseg}(y^{\prime},z)% \star y^{\prime}\simeq v\bigr)\star y\simeq u\\ \vee\;x\mapsto(y)\star\exists z^{\prime}\,\bigl(z^{\prime}\simeq v\star(% \mathtt{lseg}\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-% 20-35-page-2.pdf2svg.svg}}\mathtt{lseg})(y,z,u,z^{\prime})\bigr)\star y\not% \simeq u\\ \vee\;x\mapsto(y)\star\exists z^{\prime},x^{\prime}\,\bigl(x^{\prime}\simeq v% \star\mathtt{lseg}(x^{\prime},z^{\prime})\star(\mathtt{lseg}\mathrel{% \includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page-2.pdf2svg.% svg}}\mathtt{lseg})(y,z,u,z^{\prime})\bigr)\star y\not\simeq u\end{array}

The structures described by $\langle\phi\rangle|_{u\mapsto(v)}$ are obtained by removing the mapping $u\mapsto(v)$ from the heap described by $\phi$ . The first disjunct corresponds to the case where the removed mapping is exactly $x\mapsto(y)$ . The second disjunct handles the case where the removed mapping is the first one in the list segment $\mathtt{lseg}(y,z)$ (which entails that $y=u$ ). The third disjunct covers the case where the removed mapping is the last one in the list segment $\mathtt{lseg}(y,z)$ . The fourth disjunct accounts for the case where the removed mapping is part of the structure generated by $\mathtt{lseg}(y,z)$ , but is not its first or last element. The formula can be further simplified by replacing $z^{\prime}$ with $z$ (since the second argument of $\mathtt{lseg}$ remains unchanged through recursive calls) and $x^{\prime},y^{\prime}$ by $v$ (based on the equations $x^{\prime}\simeq v$ and $y^{\prime}\simeq v$ ).

Lemma 18.

Assume that ${\cal R}$ is PCE. Let $(\mathfrak{s},\mathfrak{h})$ be a structure, let $\phi$ be a static formula and let $x,y_{1},\dots,y_{\kappa}$ be variables. If $\mathfrak{h}=\mathfrak{h}^{\prime}\cup\{\mathfrak{s}(x)\mapsto(\mathfrak{s}(y_% {1}),\dots,\mathfrak{s}(y_{\kappa}))\}$ (with $\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h}^{\prime})$ ), then:

(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\iff(\mathfrak{s},\mathfrak{h% }^{\prime})\models_{{\cal R}}\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{% \kappa})}

For any static formula $\phi$ and variable $x$ , we denote by $\langle\phi\rangle^{\mathtt{A}(x)}$ the formula defined as follows: ${\exists z_{1},\dots,z_{\kappa}\,\bigl(x\mapsto(z_{1},\dots,z_{\kappa})\star% \langle\phi\rangle|_{x\mapsto(z_{1},\dots,z_{\kappa})}\bigr)}$ . Intuively, $\langle\phi\rangle^{\mathtt{A}(x)}$ asserts that $\phi$ holds and that $x$ is allocated. The following two lemmata follow from Lemma 18.

Lemma 19.

Assume that ${\cal R}$ is PCE. For every structure $(\mathfrak{s},\mathfrak{h})$ , for every static formula and variable $x$ the following equivalence holds:

(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\langle\phi\rangle^{\mathtt{A}(x)% }\iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\wedge\mathfrak{s}(x)\in% \mathsf{dom}(\mathfrak{h})

Lemma 20.

For every structure $(\mathfrak{s},\mathfrak{h})$ , for every static formula and variable $x$ the following two assertions are equivalent:

$\blacksquare$

$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}x\mapsto(y_{1},\dots,y_{\kappa})% \star\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ .
$\blacksquare$

$(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\wedge\mathfrak{s}(x)=(% \mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{\kappa})).$

Proof.

The proof is similar to that of Lemma 19. $\hfill\blacktriangleleft$

5 Elimination of Modalities

Building on the results in Section 4, we now show how dynamic modalities can be eliminated (if the rules satisfy the PCE conditions), thereby proving that any formula can be transformed into an equivalent static formula. We distinguish several cases, depending on the actions considered. In essence, eliminating modalities reduces to computing the weakest precondition of the corresponding modal formulas. The case of assignments can be handled using the following standard property:

Proposition 21.

For all static formulas $\phi$ and all variables $x, y$ : $[x\leftarrow y]\,\phi\equiv_{{\cal R}}\phi\{x\leftarrow y\}$

Desallocations $[\mathtt{dispose(x)}]\,\phi$ are also straightforward to handle: it is sufficient to assert that the desallocated variable $x$ is initially allocated and that the remainder of the heap satisfies $\phi$ :

Proposition 22.

For all static formulas $\phi$ for all variables $x$ , and for all pairwise distinct variables $y_{1},\dots,y_{\kappa}$ not occurring in $\phi$ :

[\mathtt{dispose(x)}]\,\phi\;\equiv_{{\cal R}}\;\exists y_{1},\dots,y_{\kappa}% \,\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi\bigr)

Example 23.

Consider the formula $\phi=[y\leftarrow x]\,[\mathtt{dispose(y)}]\,\mathtt{lseg}(x,x)$ . We get:

\begin{array}[]{rclr}\phi&\equiv&[y\leftarrow x]\,\,\exists z\,\bigl(y\mapsto(% z)\star\mathtt{lseg}(x,x)\bigr)&(\text{Proposition \ref{prop:unalloc}})\\ &\equiv&\exists z\,\bigl(x\mapsto(z)\star\mathtt{lseg}(x,x)\bigr)&(\text{% Proposition \ref{prop:affect}})\\ &\equiv&\bot\\ \end{array}

While the previous reductions (for assignments and deallocations) apply to any formula and set of rules, the remaining actions are more challenging to address. Their handling relies on the transformations described in Section 4, which crucially depend on the rules being PCE. We begin by presenting results that aim to enforce additional properties on the formulas appearing under the considered modality, based on the semantics of actions and their post-conditions. These properties will later simplify the elimination of modalities. We first consider redirections and look-ups:

Lemma 24.

Assume that ${\cal R}$ is PCE. Let $\phi$ be a static formula. If $\mathtt{a}$ is an action of the form $x.i\leftarrow y$ or $y\leftarrow x.i$ , then: $[\mathtt{a}]\,\phi\equiv_{{\cal R}}[\mathtt{a}]\,\langle\phi\rangle^{\mathtt{A% }(x)}$

Allocations are addressed in a similar way, using Lemma 20:

Lemma 25.

Assume that ${\cal R}$ is PCE. Let $\phi$ be a static formula. If $\mathtt{a}$ is an action of the form $x\leftarrow\mathtt{cons}(y_{1},\ldots,y_{\kappa})$ , then: $[\mathtt{a}]\,\phi\equiv_{{\cal R}}[\mathtt{a}]\,(x\mapsto(y_{1},\dots,y_{% \kappa})\star\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa}))})$

Next, Lemma 26 can be applied to eliminate redirection modalities, provided that the considered formula has a specific form, which will be ensured by applying Lemma 24.

Lemma 26.

For all formulas $\phi$ , for all variables $x,y_{1},\dots,y_{n},y$ , for all $i\in\{1,\dots,\kappa\}$ , for all sequences of variables $\vec{z}$ (not containing $x$ or $y$ ) and for all variables $u$ not occurring in $x,y_{1},\dots,y_{n},y$ , $\vec{z}$ or $\phi$ , the following equivalence holds:

[x.i\leftarrow y]\,\exists\vec{z}\,\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star% \phi)\bigr)\equiv_{{\cal R}}\\ \exists\vec{z}\,\exists u\,\bigl(x\mapsto(y_{1},\dots,y_{i-1},u,y_{i+1},y_{% \kappa})\star\phi\star y_{i}\simeq y\bigr)

(1)

Proof.

Let $(\mathfrak{s},\mathfrak{h})$ be a structure. By Definition 4, $x.i\leftarrow y$ fails on $(\mathfrak{s},\mathfrak{h})$ if $\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ . Moreover, $(\mathfrak{s},\mathfrak{h})\leadsto_{x.i\leftarrow y}(\mathfrak{s}^{\prime},% \mathfrak{h}^{\prime})$ exactly when $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ , $\mathfrak{s}^{\prime}=\mathfrak{s}$ and $\mathfrak{h}^{\prime}=\mathfrak{h}[\mathfrak{s}(x)\leftarrow(\ell_{1},\dots,% \ell_{i-1},\mathfrak{s}(y),\ell_{i+1},\dots,\ell_{\kappa})]$ with $\mathfrak{h}(\mathfrak{s}(x))=(\ell_{1},\dots,\ell_{\kappa})$ .

$\blacksquare$

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[x.i\leftarrow y]\,\exists\vec{z}% \,\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi)\bigr)$ . By Definition 5, we deduce that $x.i\leftarrow y$ does not fail on $(\mathfrak{s},\mathfrak{h})$ (i.e., $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ ), and that $(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal R}}(\exists\vec{z}\,(x% \mapsto(y_{1},\dots,y_{\kappa})\star\phi)$ , with $\mathfrak{h}^{\prime}=\mathfrak{h}[\mathfrak{s}(x)\leftarrow(\ell_{1},\dots,% \ell_{i-1},\mathfrak{s}(y),\ell_{i+1},\dots,\ell_{\kappa})]$ and $\mathfrak{h}(\mathfrak{s}(x))=(\ell_{1},\dots,\ell_{\kappa})$ . Consequently, there exist a vector of locations $\vec{m}$ and disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that $\mathfrak{h}_{1}\cup\mathfrak{h}_{2}=\mathfrak{h}^{\prime}$ , $(\mathfrak{s}[\vec{z}\leftarrow\vec{m}],\mathfrak{h}_{1})\models_{{\cal R}}x% \mapsto(y_{1},\dots,y_{\kappa})$ and $(\mathfrak{s}[\vec{z}\leftarrow\vec{m}],\mathfrak{h}_{2})\models_{{\cal R}}\phi$ . This entails that $\mathsf{dom}(\mathfrak{h}_{1})=\{\mathfrak{s}(x)\}$ (as $x$ does not occur in $\vec{z}$ ), $\mathsf{dom}(\mathfrak{h}_{2})=\mathsf{dom}(\mathfrak{h})\setminus\{\mathfrak{% s}(x)\}$ , $\mathfrak{s}[\vec{z}\leftarrow\vec{m}](y_{j})=\ell_{j}$ , for all $j\in\{1,\dots,i-1,i+1,\dots,\kappa\}$ and $\mathfrak{s}[\vec{z}\leftarrow\vec{m}](y_{i})=\mathfrak{s}(y)=\mathfrak{s}[% \vec{z}\leftarrow\vec{m}](y)$ (as $y$ does not occur in $\vec{z}$ ). This implies that $\mathfrak{h}=\{\mathfrak{s}(x)\mapsto(\ell_{1},\dots,\ell_{\kappa})\}\cup% \mathfrak{h}_{2}$ , and that $(\mathfrak{s}[\vec{z}\leftarrow\vec{m}],\{\mathfrak{s}(x)\mapsto(\ell_{1},% \dots,\ell_{\kappa})\})\models_{{\cal R}}\exists u\,x\mapsto(y_{1},\dots,y_{i-% 1},u,y_{i+1},\dots,y_{\kappa})$ . Consequently, $(\mathfrak{s}[\vec{z}\leftarrow\vec{m}],\mathfrak{h})\models_{{\cal R}}\exists u% \,\bigl(x\mapsto(y_{1},\dots,y_{i-1},u,y_{i+1},\dots,y_{\kappa})\star\phi\bigr)$ . Since $\mathfrak{s}[\vec{z}\leftarrow\vec{m}](y_{i})=\mathfrak{s}[\vec{z}\leftarrow% \vec{m}](y)$ , we also have $(\mathfrak{s}[\vec{z}\leftarrow\vec{m}],\mathfrak{h})\models_{{\cal R}}\exists u% \,\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi\star y\simeq y_{i}\bigr)$ , so that $(\mathfrak{s},\mathfrak{h})$ is an ${\cal R}$ -model of $\exists\vec{z}\,\exists u\,\bigl(x\mapsto(y_{1},\dots,y_{i-1},u,y_{i+1},y_{% \kappa})\star\phi\star y_{i}\simeq y\bigr)$ .
$\blacksquare$

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists\vec{z}\,\exists u\,\bigl(% x\mapsto(y_{1},\dots,y_{i-1},u,y_{i+1},y_{\kappa})\star\phi\star y_{i}\simeq y\bigr)$ . This means that there exist a sequence of locations $\vec{m},\ell$ and disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that $\mathfrak{h}=\mathfrak{h}_{1}\cup\mathfrak{h}_{2}$ , $(\mathfrak{s}[\vec{z}\leftarrow\vec{m},u\leftarrow\ell],\mathfrak{h}_{1})% \models_{{\cal R}}x\mapsto(y_{1},\dots,y_{i-1},u,y_{i+1},y_{\kappa})$ , $(\mathfrak{s}[\vec{z}\leftarrow\vec{m},\mathfrak{h}_{2})\models_{{\cal R}}\phi$ and $\mathfrak{s}[\vec{z}\leftarrow\vec{m}](y_{i})=\mathfrak{s}[\vec{z}\leftarrow% \vec{m}](y)=\mathfrak{s}(y)$ (as $u\not=y_{i}$ and $y$ does not occur in $\vec{z}$ ). Therefore $\mathsf{dom}(\mathfrak{h}_{1})=\{\mathfrak{s}[\vec{z}\leftarrow\vec{m},u% \leftarrow\ell](x)\}=\{\mathfrak{s}(x)\}$ (as $x$ does not occur in $\vec{z},u$ ), $\mathsf{dom}(\mathfrak{h}_{2})=\mathsf{dom}(\mathfrak{h})\setminus\{\mathfrak{% s}(x)\}$ , and $\mathfrak{h}(\mathfrak{s}(x))=\mathfrak{h}_{1}(\mathfrak{s}(x))=(\ell_{1},% \dots,\ell_{\kappa})$ , with $\ell_{i}=\mathfrak{s}[\vec{z}\leftarrow\vec{m},u\leftarrow\ell](u)=\ell$ and $\ell_{j}=\mathfrak{s}[\vec{z}\leftarrow\vec{m},u\leftarrow\ell](y_{i})=% \mathfrak{s}[\vec{z}\leftarrow\vec{m}](y_{i})$ for all $j\in\{1,\dots,i-1,i+1,\dots,\kappa\}$ . Let $\mathfrak{h}_{1}^{\prime}$ be the heap $\{\mathfrak{s}(x)\mapsto(\ell_{1},\dots,\ell_{i-1},\mathfrak{s}(y),\ell_{i+1},% \dots,\ell_{\kappa})\}$ . From the previous assertions we derive that $(\mathfrak{s}[\vec{z}\leftarrow\vec{m}],\mathfrak{h}_{1}^{\prime})\models_{{% \cal R}}x\mapsto(y_{1},\dots,y_{\kappa})$ . As $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ , $x.i\leftarrow y$ does not fail on $(\mathfrak{s},\mathfrak{h})$ . Let $\mathfrak{h}^{\prime}=\mathfrak{h}[\mathfrak{s}(x)\leftarrow(\ell_{1},\dots,% \ell_{i-1},\mathfrak{s}(y),\ell_{i+1},\dots,\ell_{\kappa})]$ . It is clear that $\mathfrak{h}^{\prime}=\mathfrak{h}_{1}^{\prime}\cup\mathfrak{h}_{2}$ , so that $(\mathfrak{s}[\vec{z}\leftarrow\vec{m}],\mathfrak{h}^{\prime})\models_{{\cal R% }}x\mapsto(y_{1},\dots,y_{\kappa})\star\phi$ , and thus $(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal R}}\exists\vec{z}\,(x% \mapsto(y_{1},\dots,y_{\kappa})\star\phi)$ . It follows that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[x.i\leftarrow y]\,\exists\vec{z}% \,\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi)\bigr)$ .

$\hfill\blacktriangleleft$

Example 27.

Let $\phi=[x.1\leftarrow y]\,\mathtt{lseg}(x,x)$ . We get:

\begin{array}[]{rclr}\phi&\equiv&[x.1\leftarrow y]\,\langle\mathtt{lseg}(x,x)% \rangle^{\mathtt{A}(x)}&(\text{Lemma \ref{lem:actheap}})\\ &\equiv&[x.1\leftarrow y]\,\exists z\,\bigl(x\mapsto(z)\star\langle\mathtt{% lseg}(x,x)\rangle|_{x\mapsto(z)}\bigr)&\\ &\equiv&[x.1\leftarrow y]\,\exists z,z^{\prime}\,\bigl(x\mapsto(z)\star z% \simeq z^{\prime}\star\mathtt{lseg}(z^{\prime},x)\bigr)&(\text{Definition \ref% {def:rmmap}})\\ &\equiv&\exists z,z^{\prime},u\,\bigl(x\mapsto(u)\star z\simeq z^{\prime}\star% \mathtt{lseg}(z^{\prime},x)\star z\simeq y\bigr)&(\text{Lemma \ref{lem:redir}}% )\\ &\equiv&\exists u\,\bigl(x\mapsto(u)\star\mathtt{lseg}(y,x)\bigr)\end{array}

A similar result holds for look-ups (we recall that actions $y\leftarrow x.i$ with $y=x$ are not allowed in the syntax):

Lemma 28.

For all formulas $\phi$ , for all variables $x,y_{1},\dots,y_{n},y$ (with $x\not=y$ ), for all $i\in\{1,\dots,\kappa\}$ , and for all sequences of variables $\vec{z}$ (not containing $x$ or $y$ ), the following equivalence holds: $[y\leftarrow x.i]\,\exists\vec{z}\,\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star% \phi)\bigr)\equiv_{{\cal R}}\exists\vec{z}\,\bigl(x\mapsto(y_{1},\dots,y_{% \kappa}))\star\phi\bigr)\{y\leftarrow y_{i}\})$

It remains to consider the case of allocation actions $[x\leftarrow\mathtt{cons}(y_{1},\dots,y_{\kappa})]\,\phi$ . This introduces new challenges, because the action associates the variable $x$ with a fresh, unallocated location $\ell$ . We need to ensure that the formula $\phi$ holds for all possible choices of $\ell$ (provided $\ell$ is unallocated). The most natural way to express this would be through universal quantification or separating implication. However, this is not feasible within our fragment – these constructs are not supported by existing entailment procedures for separation logic with inductive definitions. To address this, we establish Lemma 30 below. Intuitively, it states that the truth value of a static formula within a structure remains unchanged when some locations are replaced, as long as the replacement preserves variable aliasing and does not affect the heap. This will allow us to consider only a finite number of possible choices for the location $\ell$ as all locations outside the image of the store behave identically. More formally, we introduce the following equivalence relation on structures:

Definition 29.

Let $(\mathfrak{s}_{i},\mathfrak{h}_{i})$ (for $i\in\{1,2\}$ ) be two structures and let $V$ be a finite set of variables. We write $(\mathfrak{s}_{1},\mathfrak{h}_{1})\sim_{V}(\mathfrak{s}_{2},\mathfrak{h}_{2})$ if the three following conditions are fulfilled:

1.

$\mathfrak{h}_{1}=\mathfrak{h}_{2}$ .
2.

The equivalence $\mathfrak{s}_{1}(x)=\mathfrak{s}_{1}(y)\iff\mathfrak{s}_{2}(x)=\mathfrak{s}_{2% }(y)$ holds for all variables $x,y\in V$ .
3.

For all variables $x\in V$ , if $\mathfrak{s}_{1}(x)\in\mathit{locs}(\mathfrak{h}_{1})$ or $\mathfrak{s}_{2}(x)\in\mathit{locs}(\mathfrak{h}_{1})$ then $\mathfrak{s}_{1}(x)=\mathfrak{s}_{2}(x)$ .

Lemma 30.

Let $(\mathfrak{s}_{i},\mathfrak{h}_{i})$ (for $i\in\{1,2\}$ ) be two structures with $(\mathfrak{s}_{1},\mathfrak{h}_{1})\sim_{\mathsf{fv}(\phi)}(\mathfrak{s}_{2},% \mathfrak{h}_{2})$ . Let $\phi$ be a static formula. If $(\mathfrak{s}_{1},\mathfrak{h}_{1})\models_{{\cal R}}^{n}\phi$ then $(\mathfrak{s}_{2},\mathfrak{h}_{2})\models_{{\cal R}}^{n}\phi$ .

Proof.

The result is established by induction on $(n,|\phi|)$ . By Definition 29 (1) $\mathfrak{h}_{1}=\mathfrak{h}_{2}$ .

$\blacksquare$

If $\phi=(x\simeq y)$ then, as $(\mathfrak{s}_{1},\mathfrak{h}_{1})\models_{{\cal R}}\phi$ , we must have $\mathfrak{h}_{1}=\emptyset$ and $\mathfrak{s}_{1}(x)=\mathfrak{s}_{1}(y)$ , thus $\mathfrak{s}_{2}(x)=\mathfrak{s}_{2}(y)$ by Definition 29 (2), and $(\mathfrak{s}_{2},\mathfrak{h}_{1})\models_{{\cal R}}\phi$ . The proof is similar if $\phi=(x\not\simeq y)$ .
$\blacksquare$

If $\phi=y_{0}\mapsto(y_{1},\dots,y_{\kappa})$ then $\mathfrak{h}_{1}=\{\mathfrak{s}_{1}(y_{0})\mapsto(\mathfrak{s}_{1}(y_{1}),% \dots,\mathfrak{s}_{1}(y_{\kappa}))\}$ thus $\mathfrak{s}_{1}(y_{i})\in\mathit{locs}(\mathfrak{h}_{1})$ for all $i\in\{0,\dots,\kappa\}$ . Consequently $\mathfrak{s}_{1}(y_{i})=\mathfrak{s}_{2}(y_{i})$ by Definition 29 (3) and $\mathfrak{h}_{1}=\{\mathfrak{s}_{2}(y_{0})\mapsto(\mathfrak{s}_{2}(y_{1}),% \dots,\mathfrak{s}_{2}(y_{\kappa}))\}$ . Hence $(\mathfrak{s}_{2},\mathfrak{h}_{1})\models_{{\cal R}}^{n}\phi$ .
$\blacksquare$

If $\phi=\phi_{1}\vee\phi_{2}$ then $(\mathfrak{s}_{1},\mathfrak{h}_{1})\models_{{\cal R}}^{n}\phi_{i}$ for some $i\in\{1,2\}$ . By the induction hypothesis we get $(\mathfrak{s}_{2},\mathfrak{h}_{2})\models_{{\cal R}}^{n}\phi_{i}$ and $(\mathfrak{s}_{2},\mathfrak{h}_{1})\models_{{\cal R}}^{n}\phi$ .
$\blacksquare$

The proof is similar if $\phi=\phi_{1}\wedge\phi_{2}$ .
$\blacksquare$

If $\phi=\phi_{1}\star\phi_{2}$ then there exist heaps $\mathfrak{h}_{1}^{1},\mathfrak{h}_{1}^{2}$ such that $\mathfrak{h}_{1}=\mathfrak{h}_{1}^{1}\cup\mathfrak{h}_{1}^{2}$ and $(\mathfrak{s}_{1},\mathfrak{h}_{1}^{i})\models_{{\cal R}}^{n}\phi_{i}$ for all $i\in\{1,2\}$ . It is straightforward to verify that $(\mathfrak{s}_{1},\mathfrak{h}_{1}^{i})\sim_{\mathsf{fv}(\phi)}(\mathfrak{s}_{% 2},\mathfrak{h}_{1}^{i})$ , as $\mathit{locs}(\mathfrak{h}_{1}^{i})\subseteq\mathit{locs}(\mathfrak{h}_{1})$ . By the induction hypothesis, we get $(\mathfrak{s}_{2},\mathfrak{h}_{1}^{i})\models_{{\cal R}}^{n}\phi_{i}$ (for all $i\in\{1,2\}$ ) thus $(\mathfrak{s}_{2},\mathfrak{h}_{1})\models_{{\cal R}}^{n}\phi$ .
$\blacksquare$
If $\phi=\exists x\,\psi$ then there exists $\ell_{1}\in{\cal L}$ such that $(\mathfrak{s}_{1}[x\leftarrow\ell],\mathfrak{h}_{1})\models_{{\cal R}}\psi$ . We distinguish several cases. In every case we show that there exists a location $\ell_{2}$ such that $(\mathfrak{s}_{1}[x\leftarrow\ell_{1}],\mathfrak{h}_{1})\sim_{\mathsf{fv}(\psi% )}(\mathfrak{s}_{2}[x\leftarrow\ell_{2}],\mathfrak{h}_{1})$ , i.e., such that Conditions 2 and 3 in Definition 29 both hold.
- –
  If $\ell_{1}\in\mathit{locs}(\mathfrak{h}_{1})$ then we take $\ell_{2}=\ell_{1}$ . It is easy to check that Condition 3 holds, as it trivially holds for $x$ and it also holds for all $y\in\mathsf{fv}(\psi)\setminus\{x\}$ since $\mathfrak{s}_{1}\sim_{\mathsf{fv}(\phi)}\mathfrak{s}_{2}$ by hypothesis and $\mathfrak{s}_{i}[x\leftarrow\ell_{i}]$ coincides with $\mathfrak{s}_{i}$ on all $y\not=x$ . Now consider two variables $u,v\in\mathsf{fv}(\psi)$ . We show that $\mathfrak{s}_{1}[x\leftarrow\ell_{1}](u)=\mathfrak{s}_{1}[x\leftarrow\ell_{1}]% (v)\iff\mathfrak{s}_{2}[x\leftarrow\ell_{2}](u)=\mathfrak{s}_{2}[x\leftarrow% \ell_{2}](v)$ . The proof is trivial if $u=v$ , thus we assume that $u\not=v$ .
  - *
    
    If $u, v$ are both distinct from $x$ then $\mathfrak{s}_{1}[x\leftarrow\ell_{1}](u)=\mathfrak{s}_{1}[x\leftarrow\ell_{1}]% (v)\iff\mathfrak{s}_{1}(u)=\mathfrak{s}_{1}(v)\iff\mathfrak{s}_{2}(u)=% \mathfrak{s}_{2}(v)$ (as $\mathfrak{s}_{1}\sim_{\mathsf{fv}(\phi)}\mathfrak{s}_{2}$ and $u,v\in\mathsf{fv}(\phi)$ ). Thus the above equivalence holds.
  - *
    
    If one of the variables, say $u$ is $x$ , and if, for some $i\in\{1,2\}$ , $\mathfrak{s}_{i}[x\leftarrow\ell_{i}](u)=\mathfrak{s}_{i}[x\leftarrow\ell_{i}]% (v)$ , then, as $\ell_{1}\in\mathit{locs}(\mathfrak{h}_{1})$ and $\ell_{2}=\ell_{1}$ , we get $\ell_{1}=\mathfrak{s}_{i}[x\leftarrow\ell_{i}](v)=\mathfrak{s}_{i}(v)\in% \mathit{locs}(\mathfrak{h}_{1})$ and by Condition 3, $\mathfrak{s}_{i}(v)=\mathfrak{s}_{3-i}(v)$ , thus $\mathfrak{s}_{3-i}[x\leftarrow\ell_{3-i}](u)=\mathfrak{s}_{3-i}[x\leftarrow% \ell_{3-i}](v)$ .
- –
  
  If $\ell_{1}\not\in\mathit{locs}(\mathfrak{h}_{1})$ and $\ell_{1}=\mathfrak{s}_{1}(y)$ for some variable $y\in\mathsf{fv}(\phi)$ then we take $\ell_{2}=\mathfrak{s}_{2}(y)$ . We show that Condition 3 holds. Assume that $\mathfrak{s}_{i}[x\leftarrow\ell_{i}](y)\in\mathit{locs}(\mathfrak{h}_{1})$ for some $i\in\{1,2\}$ . Since $y\in\mathsf{fv}(\phi)$ , $y\not=x$ , which entails that $\mathfrak{s}_{i}(y)\in\mathit{locs}(\mathfrak{h}_{1})$ , and thus $\mathfrak{s}_{i}(y)=\mathfrak{s}_{3-i}(y)$ by Condition 3. Then we show that Condition 2 holds. Consider two variables $u,v\in\mathsf{fv}(\psi)$ and assume that $\mathfrak{s}_{i}[x\leftarrow\ell_{i}](u)=\mathfrak{s}_{i}[x\leftarrow\ell_{i}]% (v)$ for some $i\in\{1,2\}$ . We show that $\mathfrak{s}_{3-i}[x\leftarrow\ell_{3-i}](u)=\mathfrak{s}_{3-i}[x\leftarrow% \ell_{3-i}](v)$ . We may assume, w.l.o.g., that $u\not=v$ . If one of the variables, say $u$ , is $x$ , then we get $\mathfrak{s}_{i}(y)=\ell_{i}=\mathfrak{s}_{i}[x\leftarrow\ell_{i}](v)=% \mathfrak{s}_{i}(v)$ , hence $\ell_{3-i}=\mathfrak{s}_{3-i}(y)=\mathfrak{s}_{3-i}(v)$ by Condition 2, as $(\mathfrak{s}_{1},\mathfrak{h}_{1})\sim_{\mathsf{fv}(\phi)}(\mathfrak{s}_{2},% \mathfrak{h}_{1})$ . Thus $\mathfrak{s}_{3-i}[x\leftarrow\ell_{3-i}](u)=\mathfrak{s}_{3-i}[x\leftarrow% \ell_{3-i}](v)$ . If $x\not\in\{u,v\}$ then $\{u,v\}\subseteq\mathsf{fv}(\phi)$ and the proof follows from the fact that $(\mathfrak{s}_{1},\mathfrak{h}_{1})\sim_{\mathsf{fv}(\phi)}(\mathfrak{s}_{2},% \mathfrak{h}_{1})$ .
- –
  
  Otherwise (i.e., if $\ell_{1}\not\in\mathfrak{s}_{1}(\mathsf{fv}(\phi))\cup\mathit{locs}(\mathfrak{% h}_{1})$ ), $\ell_{2}$ is any location not occurring in $\mathfrak{s}_{2}(\mathsf{fv}(\phi))\cup\mathit{locs}(\mathfrak{h}_{2})$ (such a location exists as ${\cal L}$ is infinite). Condition 3 trivially holds for $x$ as $\{\ell_{1},\ell_{2}\}\cap\mathit{locs}(\mathfrak{h}_{1})=\emptyset$ , and also holds for all variables $y$ distinct from $x$ since $\mathfrak{s}_{i}[x\leftarrow\ell_{i}]$ coincides with $\mathfrak{s}_{i}$ on all $y\not=x$ . Now consider two variables $u,v\in\mathsf{fv}(\psi)$ and assume that $\mathfrak{s}_{i}[x\leftarrow\ell_{i}](u)=\mathfrak{s}_{i}[x\leftarrow\ell_{i}]% (v)$ for some $i\in\{1,2\}$ . We show that $\mathfrak{s}_{3-i}[x\leftarrow\ell_{3-i}](u)=\mathfrak{s}_{3-i}[x\leftarrow% \ell_{3-i}](v)$ . The proof is immediate if $u=v$ , thus we assume that $u\not=v$ . This implies that $x\not\in\{u,v\}$ , as $\ell_{i}\not\in\mathfrak{s}_{i}(\mathsf{fv}(\phi))$ (due to the conditions above on $\ell_{1}$ and to the choice of $\ell_{2}$ ), so that $\{u,v\}\subseteq\mathsf{fv}(\phi)$ . Then the proof follows from the fact that $(\mathfrak{s}_{1},\mathfrak{h}_{1})\sim_{\mathsf{fv}(\phi)}(\mathfrak{s}_{2},% \mathfrak{h}_{1})$ , as $\mathfrak{s}_{i}[x\leftarrow\ell_{i}](y)=\mathfrak{s}_{i}(y)$ for all $y\not=x$ .
Consequently, we get in all cases $(\mathfrak{s}_{2}[x\leftarrow\ell_{2}],\mathfrak{h}_{1})\models_{{\cal R}}^{n}\psi$ by the induction hypothesis, which implies that $(\mathfrak{s}_{2},\mathfrak{h}_{1})\models_{{\cal R}}^{n}\phi$ .
$\blacksquare$

Assume that $\phi$ is of the form $p(x_{1},\dots,x_{n})$ . By Definition 5, there exists a formula $\psi$ such that $\phi\rightarrow_{{\cal R}}\psi$ and $(\mathfrak{s}_{1},\mathfrak{h}_{1})\models_{{\cal R}}^{n-1}\psi$ . By the induction hypothesis, we get $(\mathfrak{s}_{2},\mathfrak{h}_{2})\models_{{\cal R}}^{n-1}\psi$ , thus $(\mathfrak{s}_{2},\mathfrak{h}_{2})\models_{{\cal R}}^{n-1}\phi$ .

$\hfill\blacktriangleleft$

Based on the previous result and on the key proposition 7, we now establish the equivalence that permits the elimination of allocations.

Lemma 31.

Assume that ${\cal R}$ is PCE. Let $\phi=\exists v_{1},\dots,v_{m}\,\chi$ be a static formula in prenex form (where $\chi$ is quantifier-free) and let $x,x^{\prime},y_{1},\dots,y_{\kappa}$ be variables, where $x^{\prime}\not\in\mathsf{fv}(\chi)$ . Let $\{z_{1},\dots,z_{n}\}=(\mathsf{fv}(\chi)\setminus\{x\})\cup\{x^{\prime}\}$ . The following equivalence holds:

[x\leftarrow\mathtt{cons}(y_{1},\dots,y_{\kappa})]\,\bigl(x\mapsto(y_{1},\dots% ,y_{\kappa})\star\phi\bigr)\equiv\exists v_{1},\dots,v_{m},x^{\prime}\,\big(% \psi_{1}\wedge\psi_{2}\wedge\psi_{3})

where:

$\blacksquare$

$\psi_{1}=\langle\chi\{x\leftarrow x^{\prime}\}\rangle^{\mathtt{N}(x^{\prime})}$ ;
$\blacksquare$

$\psi_{2}=\exists x\,\bigl(\langle\phi\rangle^{\mathtt{N}(x)}\star\bigstar_{i=1% }^{n}x\not\simeq z_{i}\bigr)$ ;
$\blacksquare$

$\psi_{3}=\bigwedge_{i=1}^{n}(\langle\psi_{1}\rangle^{\mathtt{A}(z_{i})}\vee% \phi\{x\leftarrow z_{i}\})$

Intuitively, the formula $\psi_{1}$ (which states that $\chi\{x\leftarrow x^{\prime}\}$ holds and that $x^{\prime}$ is not allocated) is obtained by applying the allocation $x\leftarrow\mathtt{cons}(y_{1},\dots,y_{\kappa})$ using any (arbitrary chosen) unallocated location $x^{\prime}$ . As the resulting structure satisfies $x\mapsto(y_{1},\dots,y_{\kappa})\star\phi$ , there must exist $v_{1},\dots,v_{m}$ such that $\chi\{x\leftarrow x^{\prime}\}$ holds, and since $x^{\prime}$ is not allocated, this implies that $\langle\chi\{x\leftarrow x^{\prime}\}\rangle^{\mathtt{N}(x^{\prime})}$ also holds. Afterwards, the action is applied again, this time mapping $x$ to another unallocated location distinct from the values of all (free or existential) variables occurring in the previous formula $\psi_{1}$ , yielding the formula $\psi_{2}$ . Finally, the formula $\psi_{3}$ is obtained by mapping $x$ to each (unallocated) location $z_{i}$ . The disjunct $\langle\psi_{1}\rangle^{\mathtt{A}(z_{i})}$ is added to exclude allocated locations. To establish the converse, we observe that the locations that are unallocated and distinct from the free variables in $\psi_{1}$ cannot occur in the heap (by Proposition 7), and are therefore indiscernible (by Lemma 30). Consequently, the variable $x$ in $\psi_{2}$ serves as a single representative for all such locations. More formally:

Proof.

Let $(\mathfrak{s},\mathfrak{h})$ be a structure. By Definition 4, $x\leftarrow\mathtt{cons}(y_{1},\dots,y_{\kappa})$ never fails on $(\mathfrak{s},\mathfrak{h})$ (as $\mathfrak{h}$ is finite and ${\cal L}$ is infinite) and $(\mathfrak{s},\mathfrak{h})\leadsto_{x\leftarrow\mathtt{cons}(y_{1},\dots,y_{% \kappa})}(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})$ iff $\mathfrak{s}^{\prime}=\mathfrak{s}[x\leftarrow\ell]$ and $\mathfrak{h}^{\prime}=\mathfrak{h}\cup\{\ell\mapsto(\mathfrak{s}(y_{1}),\dots,% \mathfrak{s}(y_{\kappa}))\}$ , for some $\ell\not\in\mathsf{dom}(\mathfrak{h})$ .

$\blacksquare$

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[x\leftarrow\mathtt{cons}(y_{1},% \dots,y_{\kappa})]\,\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi\bigr)$ . Let $\ell$ be any location not occurring in $\mathsf{dom}(\mathfrak{h})$ . By definition of the semantics, there exist disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that $\mathfrak{h}\cup\{\ell\mapsto(\mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{\kappa% }))\}=\mathfrak{h}_{1}\cup\mathfrak{h}_{2}$ , $(\mathfrak{s}[x\leftarrow\ell],\mathfrak{h}_{1})\models_{{\cal R}}x\mapsto(y_{% 1},\dots,y_{\kappa})$ and $(\mathfrak{s}[x\leftarrow\ell],\mathfrak{h}_{2})\models_{{\cal R}}\phi$ . This implies that $\mathfrak{h}_{1}=\{\ell\mapsto(\mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{% \kappa}))\}$ and $\mathfrak{h}_{2}=\mathfrak{h}$ thus $(\mathfrak{s}[x\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}\phi$ , and (as $\phi=\exists v_{1},\dots,v_{m}\,\chi$ ), there exist locations $\ell_{1},\dots,\ell_{m}$ such that $(\mathfrak{s}[x\leftarrow\ell,v_{i}\leftarrow\ell_{i}\mid 1\leq i\leq n],% \mathfrak{h})\models_{{\cal R}}\chi$ , thus $(\mathfrak{s}[x^{\prime}\leftarrow\ell,v_{i}\leftarrow\ell_{i}\mid 1\leq i\leq n% ],\mathfrak{h})\models_{{\cal R}}\chi\{x\leftarrow x^{\prime}\}$ . By Lemma 15, since $\ell\not\in\mathsf{dom}(\mathfrak{h})$ , we get $(\mathfrak{s}[x^{\prime}\leftarrow\ell,v_{i}\leftarrow\ell_{i}\mid 1\leq i\leq n% ],\mathfrak{h})\models_{{\cal R}}\langle\chi\{x\leftarrow x^{\prime}\}\rangle^% {\mathtt{N}(x^{\prime})}$ . Hence $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi_{1}$ , with $\mathfrak{s}^{\prime}=\mathfrak{s}[x^{\prime}\leftarrow\ell,v_{i}\leftarrow% \ell_{i}\mid 1\leq i\leq n]$ . We now prove that $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi_{2}$ . Let $\ell^{\prime}$ be any location not occurring in $\{\mathfrak{s}^{\prime}(z_{i})\mid 1\leq i\leq n\}\cup\mathsf{dom}(\mathfrak{h})$ . Using the same reasoning as before, we show (by definition of the semantics of allocations), that $(\mathfrak{s}[x\leftarrow\ell^{\prime}],\mathfrak{h})\models_{{\cal R}}\langle% \phi\rangle^{\mathtt{N}(x)}$ and therefore $(\mathfrak{s}^{\prime}[x\leftarrow\ell^{\prime}],\mathfrak{h})\models_{{\cal R% }}\langle\phi\rangle^{\mathtt{N}(x)}$ (since the variables $v_{1},\dots,v_{m}$ are not free in $\phi$ , thus in $\langle\phi\rangle^{\mathtt{N}(x)}$ ). As $\ell^{\prime}\not=\ell_{i}=\mathfrak{s}^{\prime}(z_{i})$ we get $(\mathfrak{s}^{\prime}[x\leftarrow\ell^{\prime}],\mathfrak{h})\models_{{\cal R% }}\langle\phi\rangle^{\mathtt{N}(x)}\star\bigstar_{i=1}^{n}x\not\simeq z_{i}$ which implies that $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\exists x\,\bigl(\langle% \phi\rangle^{\mathtt{N}(x)}\star\bigstar_{i=1}^{n}x\not\simeq z_{i}\bigr)=\psi% _{2}$ . Finally, we prove that $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi_{3}$ . Consider any $i\in\{1,\dots,n\}$ . If $\mathfrak{s}^{\prime}(z_{i})\in\mathsf{dom}(\mathfrak{h})$ then by Lemma 19, $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\langle\psi_{1}\rangle^{% \mathtt{A}(z_{i})}$ (since $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi_{1}$ ). Otherwise, by definition of the semantics, $(\mathfrak{s}^{\prime}[x\leftarrow\mathfrak{s}^{\prime}(z_{i})],\mathfrak{h})% \models_{{\cal R}}\phi$ , and therefore $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi\{x\leftarrow z_{i}\}$ . Therefore, we have $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi_{1}\wedge\psi_{2}% \wedge\psi_{3}$ which implies that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists v_{1},\dots,v_{m}\,\big(% \psi_{1}\wedge\psi_{2}\wedge\psi_{3})$ .
$\blacksquare$
Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists v_{1},\dots,v_{m}\,\big(% \psi_{1}\wedge\psi_{2}\wedge\psi_{3})$ . Let $\ell$ be any location not occurring in $\mathsf{dom}(\mathfrak{h})$ , we need to show that $(\mathfrak{s}[x\leftarrow\ell],\mathfrak{h}\cup\{\ell\mapsto(\mathfrak{s}(y_{1% }),\dots,\mathfrak{s}(y_{\kappa}))\})\models_{{\cal R}}x\mapsto(y_{1},\dots,y_% {\kappa})\star\phi$ . Since $(\mathfrak{s}[x\leftarrow\ell],\{\ell\mapsto(\mathfrak{s}(y_{1}),\dots,% \mathfrak{s}(y_{\kappa}))\})\models_{{\cal R}}x\mapsto(y_{1},\dots,y_{\kappa})$ (as $x$ does not occur in $y_{1},\dots,y_{\kappa}$ , by Definition 1), we only have to prove that $(\mathfrak{s}[x\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}\phi$ . By definition, there exists a store $\mathfrak{s}^{\prime}$ , coinciding with $\mathfrak{s}$ on all variables distinct from $v_{1},\dots,v_{m},x^{\prime}$ , such that $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi_{1}\wedge\psi_{2}% \wedge\psi_{3}$ . We distinguish two cases.
- –
  
  Assume that $\ell=\mathfrak{s}^{\prime}(z_{i})$ , for some $i\in\{1,\dots,n\}$ . Then, by Lemma 19, we cannot have $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\langle\psi_{1}\rangle^{% \mathtt{A}(x)}$ (otherwise $\ell$ would occur in $\mathsf{dom}(\mathfrak{h})$ ), thus we must have $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\phi\{x\leftarrow z_{i}\}$ , hence $(\mathfrak{s}^{\prime}[x\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}\phi$ . Since $v_{1},\dots,v_{m},x^{\prime}$ do not freely occur in $\phi$ , this implies that $(\mathfrak{s}[x\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}\phi$ .
- –
  
  Assume that $\ell\not=\mathfrak{s}^{\prime}(z_{i})$ , for all $i\in\{1,\dots,n\}$ . In this case, as $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}\psi_{2}$ , there exists $\ell^{\prime}$ such that $(\mathfrak{s}^{\prime}[x\leftarrow\ell^{\prime}],\mathfrak{h})\models_{{\cal R% }}\langle\phi\rangle^{\mathtt{N}(x)}$ and $\ell^{\prime}\not=\mathfrak{s}(z_{i})$ , for all $i\in\{1,\dots,m\}$ . By Proposition 7, since $\psi_{1}$ is quantifier-free, $\mathit{locs}(\mathfrak{h})\subseteq\mathsf{dom}(\mathfrak{h})\cup\{\mathfrak{% s}^{\prime}(u)\mid u\in\mathsf{fv}(\psi_{1})\}\subseteq\mathsf{dom}(\mathfrak{% h})\cup\{\mathfrak{s}^{\prime}(z_{i})\mid 1\leq i\leq n\}$ . Since $\ell,\ell^{\prime}\not\in\mathsf{dom}(\mathfrak{h})\cup\{\mathfrak{s}^{\prime}% (z_{i})\mid 1\leq i\leq n\}$ , we deduce that $\ell,\ell^{\prime}\not\in\mathit{locs}(\mathfrak{h})$ , which implies that $(\mathfrak{s}^{\prime}[x\leftarrow\ell],\mathfrak{h})\sim_{\{z_{1},\dots,z_{n}% ,x\}}(\mathfrak{s}^{\prime}[x\leftarrow\ell^{\prime}],\mathfrak{h})$ . By Lemma 30, this entails that $(\mathfrak{s}^{\prime}[x\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}\langle% \phi\rangle^{\mathtt{N}(x)}$ , thus (by Lemma 18) $(\mathfrak{s}[x\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}\phi$ (since $v_{1},\dots,v_{m},x^{\prime}$ are not free in $\phi$ ).

$\hfill\blacktriangleleft$

Lemma 32.

There exists an algorithm transforming every formula (with a PCE set of rules) of the form $[\mathtt{a}]\,\gamma$ , where $\gamma$ is static, into an equivalent static formula $\delta$ .

Proof.

If $\mathtt{a}$ is of the form $x\leftarrow y$ , then by Proposition 21 it suffices to take $\delta=\phi\{x\leftarrow y\}$ . If $\gamma$ is of the form $\exists\vec{z}\,(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi)$ and $\mathtt{a}$ is of the form $x.i\leftarrow y$ or $y\leftarrow i.x$ then by Lemmata 26 or 28 it suffices to take $\delta=\exists\vec{z}\,(\exists u\,(x\mapsto(y_{1},\dots,y_{i-1},u,y_{i+1},y_{% \kappa}))\star\phi\star y_{i}\simeq y)$ or $\delta=\exists\vec{z}\,((x\mapsto(y_{1},\dots,y_{\kappa}))\star\phi^{\prime})% \{y\leftarrow y_{i}\})$ respectively. If $\mathtt{a}$ is of the form $x.i\leftarrow y$ or $y\leftarrow i.x$ but $\gamma$ is not of the form $\exists\vec{z}\,(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi)$ , then it suffices to apply Lemma 24, to transform $\gamma$ into a formula of the latter form and get back to the previous case. If $\gamma$ is of the form $\exists\vec{z}\,(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi)$ and $\mathtt{a}$ is of the form $x\leftarrow\mathtt{cons}(y_{1},\dots,_{\kappa})$ then we take the formula $\delta=\exists v_{1},\dots,v_{m},x^{\prime}\,\big(\psi_{1}\wedge\psi_{2}\wedge% \psi_{3})$ , as defined in Lemma 31. If $\mathtt{a}$ is of the form $x\leftarrow\mathtt{cons}(y_{1},\dots,y_{\kappa})$ but $\gamma$ is not of the form $\exists\vec{z}\,(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi)$ , then it suffices to apply Lemma 25 to get an equivalent formula of the previous form and to get back to the previous case. $\hfill\blacktriangleleft$ We derive the following theorem, which constitutes the main result of the paper:

Theorem 33.

There exists an algorithm transforming every formula (with a PCE set of rules) into an equivalent static formula.

Proof.

It suffices to apply Lemma 32 recursively, on every subformula of the form $[\mathtt{a}]\,\phi$ occurring innermost in the fomula (so that $\phi$ is static), until no such subformula exists (exactly one dynamic modality is eliminated at each application of the lemma). $\hfill\blacktriangleleft$ In particular, the entailment problem for DSL formulas (with PCE rules) can thus be reduced to an entailment problem in SL, which is decidable [12].

6 Future Work

We devised an algorithm for eliminating dynamic modalities from Dynamic Separation Logic formulas satisfying the PCE conditions in [12], while preserving semantic equivalence. The reduction exploits key properties of the structures generated by PCE rules. In particular, when addressing allocation actions, the fact that the structures contain a bounded number of unallocated referenced locations is essential. The result implies that entailment remains decidable for DSL PCE formulas, thereby extending the applicability of SL-based reasoning to dynamic program behaviors while retaining automation benefits.

Future work includes implementing the proposed transformation and integrating it into existing verification frameworks. Since entailment testing is doubly exponential in the worst case [7], an important research direction is to reduce the computational overhead introduced by the transformation. To this end, one could refine the transformation process to minimize the size of the resulting formulas and the number of additional inductive rules. It could also be interesting to identify subclasses of formulas and inductive definitions for which the transformation is tractable, thereby enhancing the practical usability of the presented reduction.

Another possibility would be to enrich the base SL fragment to make the transformation more efficient, by introducing new constructs that express the necessary constraints more concisely and efficiently. For example, atomic constraints stating that a variable is unallocated (or does not occur in the heap) could be added to the logic, using formulas with negations, such as: $\forall y_{1},\dots,y_{\kappa}\,\neg\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\bigr)$ or $\forall y_{0}\,y_{1},\dots,y_{\kappa}\,\bigl(y_{0}\mapsto(y_{1},\dots,y_{% \kappa})\Rightarrow\bigwedge_{i=0}^{\kappa}(x\not\simeq y_{i})\bigr)$ . This would eliminate the need to introduce additional inductive rules to enforce these properties. Naturally, such negations must be carefully restricted to preserve the decidability of entailment, and the entailment procedure must be extended to deal with such constructs.

Extending the proposed transformation to handle rules that do not satisfy the PCE conditions could also be explored. It should be noted that inductive rules do not involve dynamic modalities. Allowing recursion in the actions would be interesting, as it would enable the expression of unbounded sequences of transformations.

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. doi:10.1007/978-3-540-30538-5_9.
[2] James Brotherston, Carsten Fuhs, Juan Antonio Navarro Pérez, and Nikos Gorogiannis. A decision procedure for satisfiability in separation logic with inductive predicates. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, pages 25:1–25:10. ACM, 2014. doi:10.1145/2603088.2603091.
[3] Cristiano Calcagno, Hongseok Yang, and Peter 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. doi:10.1007/3-540-45294-X_10.
[4] 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. doi:10.1007/978-3-642-23217-6_16.
[5] Frank S. de Boer, Hans-Dieter A. Hiep, and Stijn de Gouw. Dynamic separation logic. In Marie Kerjean and Paul Blain Levy, editors, Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, MFPS XXXIX, Indiana University, Bloomington, IN, USA, June 21-23, 2023, volume 3 of EPTICS. EpiSciences, 2023. doi:10.46298/ENTICS.12297.
[6] Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, and Daniel Méry. Separation logic with one quantified variable. In CSR’14, volume 8476 of LNCS, pages 125–138. Springer, 2014. doi:10.1007/978-3-319-06686-8_10.
[7] Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment checking in separation logic with inductive definitions is 2-exptime hard. In Elvira Albert and Laura Kovács, editors, 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. doi:10.29007/F5WH.
[8] Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules. Inf. Process. Lett., 173:106169, 2022. doi:10.1016/j.ipl.2021.106169.
[9] Mnacho Echenim and Nicolas Peltier. A proof procedure for separation logic with inductive definitions and data. J. Autom. Reason., 67(3):30, 2023. doi:10.1007/S10817-023-09680-4.
[10] Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. Compositional entailment checking for a fragment of separation logic. Formal Methods Syst. Des., 51(3):575–607, 2017. doi:10.1007/S10703-017-0289-4.
[11] Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. On automated lemma generation for separation logic with inductive definitions. In ATVA 2015, Proceedings, pages 80–96, 2015. doi:10.1007/978-3-319-24953-7_7.
[12] Radu Iosif, Adam Rogalewicz, and Jiri Simacek. The tree width of separation logic with recursive definitions. In Proc. of CADE-24, volume 7898 of LNCS, 2013.
[13] Radu Iosif, Adam Rogalewicz, and Tomás Vojnar. Deciding entailments in inductive separation logic with tree automata. In Franck Cassez and Jean-François Raskin, editors, ATVA 2014, Proceedings, volume 8837 of LNCS, pages 201–218. Springer, 2014. doi:10.1007/978-3-319-11936-6_15.
[14] Samin S Ishtiaq and Peter W O’Hearn. Bi as an assertion language for mutable data structures. In ACM SIGPLAN Notices, volume 36, pages 14–26, 2001. doi:10.1145/360204.375719.
[15] Christoph Matheja, Jens Pagel, and Florian Zuleger. A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. ACM Trans. Comput. Log., 24(1):1:1–1:76, 2023. doi:10.1145/3534927.
[16] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Laurent 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. doi:10.1007/3-540-44802-0_1.
[17] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55–74. IEEE Computer Society, 2002. doi:10.1109/LICS.2002.1029817.
[18] Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with inductive definitions. In Anthony Widjaja 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. doi:10.1007/978-3-030-34175-6_19.

Appendix A Proof of Lemma 15

We use the following proposition, which is immediate to prove:

Proposition 34.

For every structure $(\mathfrak{s},\mathfrak{h})$ , static formula $\phi$ , natural number $n$ , and substitution $\sigma$ : $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi\sigma\iff(\mathfrak{s}^{% \prime},\mathfrak{h})\models_{{\cal R}}^{n}\phi$ , where $\mathfrak{s}^{\prime}(x)=\mathfrak{s}(\sigma(x))$ , for all variables $x$ .

We show that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}\iff{(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi\wedge\mathfrak% {s}(x)\not\in\mathsf{dom}(\mathfrak{h})}$ by induction on the pair $(n,|\phi|)$ , ordered by lexicographic extension of the usual order on natural numbers (the result follows immediately).

$\blacksquare$

If $\phi$ is of the form $y\bowtie z$ (with $\bowtie\in\{\simeq,\not\simeq\}$ ) then $\langle\phi\rangle^{\mathtt{N}(x)}=\phi$ and $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi$ only if $\mathfrak{h}=\emptyset$ , thus the proof is immediate.
$\blacksquare$

If $\phi$ is of the form $x^{\prime}\mapsto(y_{1},\dots,y_{\kappa})$ then $\langle\phi\rangle^{\mathtt{N}(x)}=\phi\star(x\not\simeq x^{\prime})$ . Moreover, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi$ only if $\mathsf{dom}(\mathfrak{h})=\{\mathfrak{s}(x^{\prime})\}$ , hence the equivalence $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})\iff\mathfrak{s}(x)=\mathfrak{s}(x% ^{\prime})$ holds for all ${\cal R}$ -models $(\mathfrak{s},\mathfrak{h})$ of $\phi$ . Consequently, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi\star(x\not\simeq x^{% \prime})\iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\wedge\mathfrak{s% }(x)\not\in\mathsf{dom}(\mathfrak{h})$ .
$\blacksquare$

If $\phi$ is of the form $\phi_{1}\wedge\phi_{2}$ then $\langle\phi\rangle^{\mathtt{N}(x)}=\langle\phi_{1}\rangle^{\mathtt{N}(x)}% \wedge\phi_{2}$ . By Definition 5, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}$ iff $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi_{1}\rangle^{% \mathtt{N}(x)}$ and $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi_{2}$ . By the induction hypothesis, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi_{1}\rangle^{% \mathtt{N}(x)}\iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi_{1}% \wedge\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ , hence $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}$ is equivalent to: $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi_{i}$ (for all $i\in\{1,2\}$ ) and $\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ . Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}\iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi\wedge\mathfrak{% s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ .
$\blacksquare$

If $\phi$ is of the form $\phi_{1}\vee\phi_{2}$ then $\langle\phi\rangle^{\mathtt{N}(x)}=\langle\phi_{1}\rangle^{\mathtt{N}(x)}\vee% \langle\phi_{2}\rangle^{\mathtt{N}(x)}$ . By definition, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}$ iff $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi_{i}\rangle^{% \mathtt{N}(x)}$ (for some $i\in\{1,2\}$ ). By the induction hypothesis, ${(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi_{i}\rangle^{% \mathtt{N}(x)}}\iff{(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi_{i}% \wedge\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})}$ . Therefore the assertion $\exists i\in\{1,2\}\,\text{s.t.\ }(\mathfrak{s},\mathfrak{h})\models_{{\cal R}% }^{n}\langle\phi_{i}\rangle^{\mathtt{N}(x)}$ holds iff ${\exists i\in\{1,2\}\,\text{s.t.\ }(\mathfrak{s},\mathfrak{h})\models_{{\cal R% }}^{n}\phi_{i}}$ and ${\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})}$ . Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}$ iff $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi\wedge\mathfrak{s}(x)\not% \in\mathsf{dom}(\mathfrak{h})$ .
$\blacksquare$

If $\phi$ is of the form $\phi_{1}\star\phi_{2}$ then $\langle\phi\rangle^{\mathtt{N}(x)}=\langle\phi_{1}\rangle^{\mathtt{N}(x)}\star% \langle\phi_{2}\rangle^{\mathtt{N}(x)}$ . By Definition 5, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}$ iff there exist disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that $\mathfrak{h}=\mathfrak{h}_{1}\cup\mathfrak{h}_{2}$ and $(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}^{n}\langle\phi_{i}\rangle^{% \mathtt{N}(x)}$ (for all $i\in\{1,2\}$ ). By the induction hypothesis, ${(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}^{n}\langle\phi_{i}\rangle^{% \mathtt{N}(x)}}\iff{(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}^{n}\phi_% {i}\wedge\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h}_{i})}$ , so that $(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}^{n}\langle\phi_{i}\rangle^{% \mathtt{N}(x)}$ (for all $i\in\{1,2\}$ ) iff $(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}^{n}\phi_{i}$ (for all $i\in\{1,2\}$ ) and $\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h}_{1})\cup\mathsf{dom}(\mathfrak% {h}_{2})$ . Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}$ iff there exist disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that $\mathfrak{h}=\mathfrak{h}_{1}\cup\mathfrak{h}_{2}$ and $(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}^{n}\phi_{i}$ (for all $i\in\{1,2\}$ ) and $x\not\in\mathsf{dom}(\mathfrak{h})$ , i.e., $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}\iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi\wedge\mathfrak{% s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ .
$\blacksquare$

If $\phi=\exists y\,\psi$ (with $x\not=y$ ), then $\langle\phi\rangle^{\mathtt{N}(x)}=\exists y\,\langle\phi\rangle^{\mathtt{N}(x)}$ . By Definition 5, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}$ iff there exists $\ell\in{\cal L}$ such that $(\mathfrak{s}[y\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}^{n}\langle\psi% \rangle^{\mathtt{N}(x)}$ . By the induction hypothesis $(\mathfrak{s}[y\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}^{n}\langle\psi% \rangle^{\mathtt{N}(x)}$ holds iff $(\mathfrak{s}[y\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}^{n}\psi\wedge% \mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ . Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}\iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi\wedge\mathfrak{% s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ .
$\blacksquare$

Now assume that $\phi=p(x_{1},\dots,x_{n})$ . Then $\langle\phi\rangle^{\mathtt{N}(x)}={p}^{\prime}(x_{1},\dots,x_{n},x)$ . By definition of the rules of $\langle\phi\rangle^{\mathtt{N}(x)}$ , $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}$ iff there exists a rule $p(y_{1},\dots,y_{n})\Leftarrow\psi$ such that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n-1}\langle\psi\rangle^{\mathtt% {N}(y)}\sigma$ , with $\sigma=\{y\leftarrow x,y_{i}\leftarrow x_{i}\mid i\in\{1,\dots,n\}\}$ . By Proposition 34, this is equivalent to $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}^{n-1}\langle\psi\rangle% ^{\mathtt{N}(y)}$ , with $\mathfrak{s}^{\prime}(y)=\mathfrak{s}(x)$ and $\mathfrak{s}^{\prime}(y_{i})=\mathfrak{s}(x_{i})$ for all $i\in\{1,\dots,n\}$ . By the induction hypothesis, $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}^{n-1}\langle\psi\rangle% ^{\mathtt{N}(y)}$ iff $(\mathfrak{s}^{\prime},\mathfrak{h})\models_{{\cal R}}^{n-1}\psi$ and $\mathfrak{s}^{\prime}(y)\not\in\mathsf{dom}(\mathfrak{h})$ , i.e., iff $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n-1}\psi\sigma$ and $\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ . Thus we obtain the equivalence $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\langle\phi\rangle^{\mathtt{N% }(x)}\iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}^{n}\phi\wedge\mathfrak{% s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ .

Appendix B Proof of Lemma 18

Let $\phi^{\prime}=\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ . We establish the equivalence $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\iff(\mathfrak{s},\mathfrak{h% }^{\prime})\models_{{\cal R}}\phi^{\prime}$ by induction on $|\phi|$ .

$\blacksquare$

If $\phi$ is of the form $y\bowtie z$ (with $\bowtie\in\{\simeq,\not\simeq\}$ ) then $\phi^{\prime}=\bot$ and $(\mathfrak{s},\mathfrak{h})\not\models_{{\cal R}}\phi$ (as $\mathfrak{h}$ is not empty while $\phi$ is satisfied only by structures with an empty heap by Definition 5). Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\iff(\mathfrak{s},\mathfrak{h% }^{\prime})\models_{{\cal R}}\phi^{\prime}$ .
$\blacksquare$

If $\phi$ is of the form $x^{\prime}\mapsto(y_{1}^{\prime},\dots,y_{\kappa}^{\prime})$ then $\phi^{\prime}=x\simeq x^{\prime}\star\bigstar_{i=1}^{\kappa}(y_{i}\simeq y_{i}% ^{\prime})$ . By Definition 5, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff $\mathfrak{h}=\{\mathfrak{s}(x^{\prime})\mapsto(\mathfrak{s}(y_{1}^{\prime}),% \dots,\mathfrak{s}(y_{\kappa}^{\prime}))\}$ , i.e., if $\mathfrak{h}^{\prime}=\emptyset$ , $\mathfrak{s}(x)=\mathfrak{s}(x^{\prime})$ and $\mathfrak{s}(y_{i})=\mathfrak{s}(y_{i}^{\prime})$ (for all $i\in\{1,\dots,\kappa\}$ ), since $\mathfrak{h}=\mathfrak{h}^{\prime}\cup\{\mathfrak{s}(x)\mapsto(\mathfrak{s}(y_% {1}),\dots,\mathfrak{s}(y_{\kappa}))\}$ by the hypothesis of the lemma. Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\iff(\mathfrak{s},\mathfrak{h% }^{\prime})\models_{{\cal R}}\phi^{\prime}$ .
$\blacksquare$

If $\phi$ is of the form $\phi_{1}\wedge\phi_{2}$ then $\phi^{\prime}=\phi_{1}^{\prime}\wedge\phi_{2}^{\prime}$ with $\phi_{i}^{\prime}=\langle\phi_{i}\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ (for all $i\in\{1,2\}$ ). By Definition 5, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi_{i}$ for all $i\in\{1,2\}$ . By the induction hypothesis, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi_{i}\iff(\mathfrak{s},% \mathfrak{h}^{\prime})\models_{{\cal R}}\phi_{i}^{\prime}$ , so that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff $(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal R}}\phi_{1}^{\prime}\wedge% \phi_{2}^{\prime}=\phi^{\prime}$ .
$\blacksquare$

The proof is similar if $\phi=\phi_{1}\vee\phi_{2}$ .
$\blacksquare$

If $\phi$ is of the form $\phi_{1}\star\phi_{2}$ then $\phi^{\prime}=(\phi_{1}^{\prime}\star\phi_{2})\vee(\phi_{1}\star\phi_{2}^{% \prime})$ with $\phi_{i}^{\prime}=\langle\phi_{i}\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ (for all $i\in\{1,2\}$ ). By Definition 5, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff there exist disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that $\mathfrak{h}=\mathfrak{h}_{1}\cup\mathfrak{h}_{2}$ , and $(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}\phi_{i}$ for all $i\in\{1,2\}$ . By definition, as $\mathfrak{h}=\mathfrak{h}^{\prime}\cup\{\mathfrak{s}(x)\mapsto(\mathfrak{s}(y_% {1}),\dots,\mathfrak{s}(y_{\kappa}))\}$ for all such $\mathfrak{h}_{1},\mathfrak{h}_{2}$ , there is $i\in\{1,2\}$ such that $\mathfrak{h}_{i}=\mathfrak{h}_{i}^{\prime}\cup\{\mathfrak{s}(x)\mapsto(% \mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{\kappa}))\}$ and $\mathfrak{h}^{\prime}=\mathfrak{h}_{i}^{\prime}\cup\mathfrak{h}_{3-i}$ . By the induction hypothesis, $(\mathfrak{s},\mathfrak{h}_{i})\models_{{\cal R}}\phi_{i}\iff(\mathfrak{s},% \mathfrak{h}_{i}^{\prime})\models_{{\cal R}}\phi_{i}^{\prime}$ , so that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff there exist $\mathfrak{h}_{1},\mathfrak{h}_{2}$ and $i\in\{1,2\}$ such that $\mathfrak{h}=\mathfrak{h}_{1}\cup\mathfrak{h}_{2}$ , $(\mathfrak{s},\mathfrak{h}_{3-i})\models_{{\cal R}}\phi_{3-i}$ and $(\mathfrak{s},\mathfrak{h}_{i}^{\prime})\models_{{\cal R}}\phi_{i}^{\prime}$ (with $\mathfrak{h}_{i}=\mathfrak{h}_{i}^{\prime}\cup\{\mathfrak{s}(x)\mapsto(% \mathfrak{s}(y_{1}),\dots,\mathfrak{s}(y_{\kappa}))\}$ and $\mathfrak{h}^{\prime}=\mathfrak{h}_{i}^{\prime}\cup\mathfrak{h}_{3-i}$ ). By Definition 5, this is equivalent to $(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal R}}(\phi_{1}^{\prime}\star% \phi_{2})\vee(\phi_{1}\star\phi_{2}^{\prime})$ .
$\blacksquare$

if $\phi=\exists z\,\psi$ then $\phi^{\prime}=\exists z\,\psi^{\prime}$ , with $\psi^{\prime}=\langle\psi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ . By Definition 5, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff there exists $\ell\in{\cal L}$ such that $(\mathfrak{s}[z\leftarrow\ell],\mathfrak{h})\models_{{\cal R}}\psi$ . By the induction hypothesis, this is equivalent to: $\exists\ell\in{\cal L}$ s.t. $(\mathfrak{s}[z\leftarrow\ell],\mathfrak{h}^{\prime})\models_{{\cal R}}\psi^{\prime}$ , i.e., to $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi^{\prime}$ .
$\blacksquare$

Assume that $\phi=p(z_{1},\dots,z_{n})$ with $z_{1}=x$ . Let $\{\rho_{1},\dots,\rho_{m}\}$ be the set of formulas $\rho$ such that $\phi\rightarrow_{{\cal R}}\rho$ (this set is finite, up to $\alpha$ -renaming, as there are finitely many rules associated with $p$ ). As ${\cal R}$ is progressing, each formula $\rho_{i}$ (for $i\in\{1,\dots,m\}$ ) contains exactly one $\mapsto$ -atom and the left-hand side of this atom must be $z_{1}$ (i.e. $x$ ). Thus $\rho_{i}$ is of the form $\exists\vec{u}_{i}\,(z_{1}\mapsto(y_{1}^{i},\dots,y_{\kappa}^{i})\star\psi_{i})$ . By Definition 5, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\rho_{i}$ for some $i\in\{1,\dots,m\}$ , i.e., iff there exist a natural number $i\in\{1,\dots,m\}$ , locations $\vec{\ell}$ , and heaps $\mathfrak{h}_{i}^{1},\mathfrak{h}_{i}^{2}$ such that $\mathfrak{h}=\mathfrak{h}_{i}^{1}\cup\mathfrak{h}_{i}^{2}$ , $(\mathfrak{s}[\vec{z}\leftarrow\vec{\ell}],\mathfrak{h}_{i}^{1})\models_{{\cal R% }}z_{1}\mapsto(y_{1}^{i},\dots,y_{\kappa}^{i})$ and $(\mathfrak{s}[\vec{z}\leftarrow\vec{\ell}],\mathfrak{h}_{i}^{2})\models_{{\cal R% }}\psi_{i}$ . The conditions above hold only if $\mathsf{dom}(\mathfrak{h}_{i}^{1})=\{\mathfrak{s}(z_{1})\}=\{\mathfrak{s}(x)\}$ , thus only if we have $\mathfrak{h}_{i}^{1}=\{\mathfrak{s}(x)\mapsto(\mathfrak{s}(y_{1}),\dots,% \mathfrak{s}(y_{\kappa}))\}$ , $\mathfrak{s}(y_{j}^{i})=\mathfrak{s}(y_{j})$ for all $j\in\{1,\dots,\kappa\}$ ) and $\mathfrak{h}_{i}^{2}=\mathfrak{h}^{\prime}$ . Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff there exist $i\in\{1,\dots,m\}$ and $\vec{\ell}$ , such that $(\mathfrak{s}[\vec{z}\leftarrow\vec{\ell}],\emptyset)\models_{{\cal R}}% \bigstar_{j=1}^{\kappa}(y_{j}\simeq y_{j}^{i})$ and $(\mathfrak{s}[\vec{z}\leftarrow\vec{\ell}],\mathfrak{h}^{\prime})\models_{{% \cal R}}\psi_{i}$ . By Definition 5, this is equivalent to $(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal R}}\bigvee_{i=1}^{m}\exists% \vec{u}_{i}\,(\psi_{i}\star\bigstar_{j=1}^{\kappa}(y_{j}\simeq y_{j}^{i}))=% \phi^{\prime}$ .

\blacksquare

Finally, assume that $\phi=p(z_{1},\dots,z_{n})$ and $z_{1}\not=x$ . We have $\phi\equiv_{{\cal R}}(z_{1}\simeq x\star\phi)\vee(z_{1}\not\simeq x\star\phi)$ . It is clear that $z_{1}\simeq x\star\phi$ is equivalent to $z_{1}\simeq x\star p(x,z_{2},\dots,z_{n})$ and by Corollary 12, $z_{1}\not\simeq x\star\phi$ has the same truth value in $(\mathfrak{s},\mathfrak{h})$ as $z_{1}\not\simeq x\star\bigvee_{p\succ_{{\cal R}}^{+}q,\#(q)=m}\exists u_{2},% \dots,u_{m},\bigl(q(x,u_{2},\dots,u_{m})\star(q\mathrel{\includegraphics{% dagpub-standalone-manual-2026-03-04-19-20-35-page-2.pdf2svg.svg}}p)(z_{1},% \dots,z_{n},x,u_{2},\dots,u_{m})\bigr)$ . We obtain:

\begin{array}[]{ccc}\langle z_{1}\simeq x\star\phi\rangle|_{x\mapsto(y_{1},% \dots,y_{\kappa})}&=&\langle z_{1}\simeq x\rangle|_{x\mapsto(y_{1},\dots,y_{% \kappa})}\star\phi\\ &&\vee z_{1}\simeq x\star\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})% }\\ &=&(\bot\star\phi)\vee(z_{1}\simeq x\star\langle\phi\rangle|_{x\mapsto(y_{1},% \dots,y_{\kappa})})\\ &\equiv_{{\cal R}}&z_{1}\simeq x\star\langle\phi\rangle|_{x\mapsto(y_{1},\dots% ,y_{\kappa})}\\ \end{array}

Consider the formula $\gamma=z_{1}\not\simeq x\star\bigvee_{p\succ_{{\cal R}}^{+}q,\#(q)=m}\exists% \vec{u}_{m}\,(\gamma_{q,m}\star\lambda_{q,m})$ with $\vec{u}_{m}=(u_{2},\dots,u_{m})$ , $\gamma_{q,m}=q(x,u_{2},\dots,u_{m})$ and $\lambda_{q,m}$ is the formula ${(q\mathrel{\includegraphics{dagpub-standalone-manual-2026-03-04-19-20-35-page% -2.pdf2svg.svg}}p)(z_{1},\dots,z_{n},x,u_{2},\dots,u_{m})}$ . In a similar way as for the previous formula, we can show that $\langle\gamma\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}$ is equivalent to the formula: $z_{1}\not\simeq x\star\bigvee_{p\succ_{{\cal R}}^{+}q,\#(q)=m}\exists\vec{u}_{% m}\,\bigl((\gamma_{q,m}^{\prime}\star\lambda_{q,m})\vee(\gamma_{q,m}\star% \lambda_{q,m}^{\prime})\bigr)$ , with $\gamma_{q,m}^{\prime}=\langle\gamma_{q,m}\rangle|_{x\mapsto(y_{1},\dots,y_{% \kappa})}$ and $\lambda_{q,m}^{\prime}=\langle\lambda_{q,m}\rangle|_{x\mapsto(y_{1},\dots,y_{% \kappa})}$ . Furthermore, as $\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h}^{\prime})$ , it is clear that $(\mathfrak{s},\mathfrak{h}^{\prime})\not\models_{{\cal R}}(\gamma_{q,m}\star% \lambda_{q,m}^{\prime})$ , since (as ${\cal R}$ is PCE) $\gamma_{q,m}$ unfolds to a formula containing a $\mapsto$ -atom of the form $x\mapsto(\dots)$ . Consequently, $(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal R}}\langle\gamma\rangle|_{x% \mapsto(y_{1},\dots,y_{\kappa})}$ iff $(\mathfrak{s},\mathfrak{h}^{\prime})\models_{{\cal R}}z_{1}\not\simeq x\star% \bigvee_{p\succ_{{\cal R}}^{+}q,\#(q)=m}\exists\vec{u}_{m}\,(\gamma_{q,m}^{% \prime}\star\lambda_{q,m})$ . Using the equivalences established in the previous items, we obtain that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ iff $(\mathfrak{s},\mathfrak{h}^{\prime})$ is an ${\cal R}$ -model of $\bigl(z_{1}\simeq x\star\langle\phi\rangle|_{x\mapsto(y_{1},\dots,y_{\kappa})}% \bigr)\vee\bigl(z_{1}\not\simeq x\star\bigvee_{p\succ_{{\cal R}}^{+}q,\#(q)=m}% \exists\vec{u}_{m}\,(\gamma_{q,m}^{\prime}\star\lambda_{q,m})\bigr)$ , which completes the proof.

Appendix C Proof of Lemma 19

By definition, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\wedge\mathfrak{s}(x)\in% \mathsf{dom}(\mathfrak{h})$ iff there exist locations $\ell_{1},\dots,\ell_{\kappa}$ such that $\mathfrak{h}=\mathfrak{h}^{\prime}\cup\{\mathfrak{s}(x)\mapsto(\ell_{1},\dots,% \ell_{k})\}$ and $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi$ . Let $z_{1},\dots,z_{\kappa}$ be fresh variables and let $\hat{\mathfrak{s}}=\mathfrak{s}[z_{i}\leftarrow\ell_{i}\mid 1\leq i\leq\kappa]$ . By definition, $(\hat{\mathfrak{s}},\{\mathfrak{s}(x)\mapsto(\ell_{1},\dots,\ell_{k})\})% \models_{{\cal R}}x\mapsto(z_{1},\dots,z_{\kappa})$ . By Lemma 18, we have $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\iff(\hat{\mathfrak{s}},% \mathfrak{h}^{\prime})\models_{{\cal R}}\langle\phi\rangle|_{x\mapsto(z_{1},% \dots,z_{\kappa})}$ , if $\mathfrak{h}=\mathfrak{h}^{\prime}\cup\{\mathfrak{s}(x)\mapsto(\ell_{1},\dots,% \ell_{k})\}$ . Consequently, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\iff(\hat{\mathfrak{s}},% \mathfrak{h})\models_{{\cal R}}\exists z_{1},\dots,z_{\kappa}\ (x\mapsto(z_{1}% ,\dots,z_{\kappa})\star\langle\phi\rangle|_{x\mapsto(z_{1},\dots,z_{\kappa})})% \iff(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\langle\phi\rangle^{\mathtt{A% }(x)}$ .

Appendix D Proof of Proposition 21

Let $(\mathfrak{s},\mathfrak{h})$ be a structure. By Definition 4, $(\mathfrak{s},\mathfrak{h})\leadsto_{x\leftarrow y}(\mathfrak{s}^{\prime},% \mathfrak{h}^{\prime})\iff\mathfrak{s}^{\prime}=\mathfrak{s}[x\leftarrow y]% \wedge\mathfrak{h}^{\prime}=\mathfrak{h}$ , thus, by Definition 5, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[x\leftarrow y]\,\phi\iff(% \mathfrak{s}[x\leftarrow y],\mathfrak{h})\models_{{\cal R}}\phi$ . Consequently $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[x\leftarrow y]\,\phi\iff(% \mathfrak{s}[x\leftarrow y],\mathfrak{h})\models_{{\cal R}}\phi\{x\leftarrow y\}$ (as $\mathfrak{s}[x\leftarrow y](x)=\mathfrak{s}[x\leftarrow y](y)$ ), and $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[x\leftarrow y]\,\phi\iff(% \mathfrak{s},\mathfrak{h})\models_{{\cal R}}\phi\{x\leftarrow y\}$ (since $x$ does not occur in $\phi\{x\leftarrow y\}$ while $\mathfrak{s}[x\leftarrow y]$ and $\mathfrak{s}$ coincide on all variables other than $x$ ).

Appendix E Proof of Proposition 22

Let $(\mathfrak{s},\mathfrak{h})$ be a structure. By Definition 4, $\mathtt{dispose(x)}$ fails on $(\mathfrak{s},\mathfrak{h})$ if $\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ and $(\mathfrak{s},\mathfrak{h})\leadsto_{\mathtt{dispose(x)}}(\mathfrak{s}^{\prime% },\mathfrak{h}^{\prime})$ iff $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ , $\mathfrak{s}^{\prime}=\mathfrak{s}$ and $\mathfrak{h}^{\prime}$ is the restriction of $\mathfrak{h}$ of domain $\mathsf{dom}(\mathfrak{h})\setminus\{\mathfrak{s}(x)\}$ .

$\blacksquare$

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[\mathtt{dispose(x)}]\,\phi$ . By Definition 5 we deduce that $\mathtt{dispose(x)}$ does not fail on $(\mathfrak{s},\mathfrak{h})$ (that i.e., $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ ) and that $(\mathfrak{s},\mathfrak{h}|_{\mathsf{dom}(\mathfrak{h})\setminus\{\mathfrak{s}% (x)\}})\models_{{\cal R}}\phi$ . As $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ , there exist $\ell_{1},\dots,\ell_{\kappa}\in{\cal L}$ such that $\mathfrak{h}(\mathfrak{s}(x))=(\ell_{1},\dots,\ell_{\kappa})$ . Since $y_{1},\dots,y_{\kappa}$ are pairwise distinct, $\mathfrak{s}[y_{i}\leftarrow\ell_{i}\mid 1\leq i\leq\kappa]$ is well-defined and by definition the structure $(\mathfrak{s}[y_{i}\leftarrow\ell_{i}\mid 1\leq i\leq\kappa],\{\mathfrak{s}(x)% \mapsto(\ell_{1},\dots,\ell_{\kappa})\})$ is an ${\cal R}$ -model of $x\mapsto(y_{1},\dots,y_{\kappa})$ . Thus $(\mathfrak{s},\{\mathfrak{s}(x)\mapsto(\ell_{1},\dots,\ell_{\kappa})\})\models% _{{\cal R}}\exists y_{1},\dots,y_{\kappa}\,x\mapsto(y_{1},\dots,y_{\kappa})$ . As $\mathfrak{h}=\mathfrak{h}|_{\mathsf{dom}(\mathfrak{h})\setminus\{\mathfrak{s}(% x)\}}\cup\{\mathfrak{s}(x)\mapsto(\ell_{1},\dots,\ell_{\kappa})\}$ , we get $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists y_{1},\dots,y_{\kappa}\,% \bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi\bigr)$ .
$\blacksquare$

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists y_{1},\dots,y_{\kappa}\,x% \mapsto(y_{1},\dots,y_{\kappa})\star\phi$ . By definition, (since $y_{1},\dots,y_{\kappa}$ does not occur in $\phi$ ) there exist disjoint heaps $\mathfrak{h}_{1},\mathfrak{h}_{2}$ such that $\mathfrak{h}=\mathfrak{h}_{1}\cup\mathfrak{h}_{2}$ , $(\mathfrak{s},\mathfrak{h}_{1})\models_{{\cal R}}\exists y_{1},\dots,y_{\kappa% }\,x\mapsto(y_{1},\dots,y_{\kappa})$ and $(\mathfrak{s},\mathfrak{h}_{2})\models_{{\cal R}}\phi$ . This entails that $\mathsf{dom}(\mathfrak{h}_{1})=\{\mathfrak{s}(x)\}$ , hence $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ , so that $\mathtt{dispose(x)}$ does not fail on $(\mathfrak{s},\mathfrak{h})$ . Moreover, $\mathsf{dom}(\mathfrak{h}_{2})=\mathsf{dom}(\mathfrak{h})\setminus\{\mathfrak{% s}(x)\}$ , so that $(\mathfrak{s},\mathfrak{h}|_{\mathsf{dom}(\mathfrak{h})\setminus\{\mathfrak{s}% (x)\}})\models_{{\cal R}}\phi$ and consequently $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[\mathtt{dispose(x)}]\,\phi$ .

Appendix F Proof of Lemma 24

Let $(\mathfrak{s},\mathfrak{h})$ be a structure. By definition, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[\mathtt{a}]\,\phi$ iff $\mathtt{a}$ does not fail on $(\mathfrak{s},\mathfrak{h})$ and $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\models_{{\cal R}}\phi$ , for all $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})$ such that $(\mathfrak{s},\mathfrak{h})\leadsto_{\mathtt{a}}(\mathfrak{s}^{\prime},% \mathfrak{h}^{\prime})$ . As $\mathtt{a}$ is of the form $x.i\leftarrow y$ or $y\leftarrow x.i$ , $\mathtt{a}$ fails iff $\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ . If $\mathtt{a}$ fails, then $[\mathtt{a}]\,\phi$ and $[\mathtt{a}]\,\langle\phi\rangle^{\mathtt{A}(x)}$ are both false in $(\mathfrak{s},\mathfrak{h})$ . Otherwise, $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ . Moreover, if $(\mathfrak{s},\mathfrak{h})\leadsto_{\mathtt{a}}(\mathfrak{s}^{\prime},% \mathfrak{h}^{\prime})$ then $\mathsf{dom}(\mathfrak{h})=\mathsf{dom}(\mathfrak{h}^{\prime})$ , as the actions $x.i\leftarrow y$ or $y\leftarrow x.i$ cannot affect the domain of the heap. Moreover, $\mathfrak{s}(x)=\mathfrak{s}^{\prime}(x)$ , since $x.i\leftarrow y$ does not affect the store and $y\leftarrow x.i$ does not affect the image of $x$ (as $x\not=y$ , by the condition in Definition 1). Thus $\mathfrak{s}^{\prime}(x)\in\mathsf{dom}(\mathfrak{h}^{\prime})$ . By Lemma 19 we deduce that $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\models_{{\cal R}}\phi$ is equivalent to $(\mathfrak{s}^{\prime},\mathfrak{h}^{\prime})\models_{{\cal R}}\langle\phi% \rangle^{\mathtt{A}(x)}$ . Consequently, $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[\mathtt{a}]\,\phi\iff(\mathfrak{% s},\mathfrak{h})\models_{{\cal R}}[\mathtt{a}]\,\langle\phi\rangle^{\mathtt{A}% (x)}$ .

Appendix G Proof of Lemma 25

The proof is similar to that of Lemma 24. Let $(\mathfrak{s},\mathfrak{h})$ be a structure. If $\mathtt{a}$ fails, then $[\mathtt{a}]\,\phi$ and $[\mathtt{a}]\,(x\mapsto(y_{1},\dots,y_{\kappa})\star\langle\phi\rangle|_{x% \mapsto(y_{1},\dots,y_{\kappa}))})$ are both false in $(\mathfrak{s},\mathfrak{h})$ . Otherwise, by definition of $\leadsto_{\mathtt{a}}$ , if $(\mathfrak{s},\mathfrak{h})\leadsto_{\mathtt{a}}(\mathfrak{s}^{\prime},% \mathfrak{h}^{\prime})$ then $\mathfrak{h}^{\prime}(\mathfrak{s}^{\prime}(x))=(\mathfrak{s}^{\prime}(y_{1}),% \dots,\mathfrak{s}^{\prime}(y_{\kappa}))$ . The proof follows by Lemma 20.

Appendix H Proof of Lemma 28

Let $(\mathfrak{s},\mathfrak{h})$ be a structure. By Definition 4, $y\leftarrow x.i$ fails on $(\mathfrak{s},\mathfrak{h})$ if $\mathfrak{s}(x)\not\in\mathsf{dom}(\mathfrak{h})$ and otherwise $(\mathfrak{s},\mathfrak{h})\leadsto_{y\leftarrow x.i}(\mathfrak{s}^{\prime},% \mathfrak{h}^{\prime})$ iff $\mathfrak{s}^{\prime}=\mathfrak{s}\{y\leftarrow\ell_{i}\}$ and $\mathfrak{h}^{\prime}=\mathfrak{h}$ with $\mathfrak{h}(\mathfrak{s}(x))=(\ell_{1},\dots,\ell_{\kappa})$ .

$\blacksquare$

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[y\leftarrow x.i]\,\exists\vec{z}% \,\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi)\bigr)$ . Then $y\leftarrow x.i$ does not fail on $(\mathfrak{s},\mathfrak{h})$ (thus $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ ), and $(\mathfrak{s}[y\leftarrow\ell_{i}],\mathfrak{h})\models_{{\cal R}}\exists\vec{% z}\,\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi)\bigr)$ , with $\mathfrak{s}(x)=(\ell_{1},\dots,\ell_{\kappa})$ . Thus there exists a sequence of locations $\vec{m}$ such that $(\mathfrak{s}[y\leftarrow\ell_{i},\vec{z}\leftarrow\vec{m}],\mathfrak{h})% \models_{{\cal R}}x\mapsto(y_{1},\dots,y_{\kappa})\star\phi$ . In particular, (as $x$ or $y$ does not occur in $\vec{z}$ and $x\not=y$ , by Definition 1) we must have $\ell_{i}=\mathfrak{s}[y\leftarrow\ell_{i},\vec{z}\leftarrow\vec{m}](y_{i})$ , hence $\mathfrak{s}[y\leftarrow\ell_{i},\vec{z}\leftarrow\vec{m}](y)=\mathfrak{s}[y% \leftarrow\ell_{i},\vec{z}\leftarrow\vec{m}](y_{i})$ . Consequently, $(\mathfrak{s}[y\leftarrow\ell_{i},\vec{z}\leftarrow\vec{m}],\mathfrak{h})% \models_{{\cal R}}\bigl(x\mapsto(y_{1},\dots,y_{\kappa})\star\phi\bigr)\{y% \leftarrow y_{i}\}$ . This implies that $(\mathfrak{s}[\vec{z}\leftarrow\vec{m}],\mathfrak{h})\models_{{\cal R}}(x% \mapsto(y_{1},\dots,y_{\kappa})\star\phi)\{y\leftarrow y_{i}\}$ and $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists\vec{z}\,\bigl(x\mapsto(y_% {1},\dots,y_{\kappa}))\star\phi\bigr)\{y\leftarrow y_{i}\}$ .
$\blacksquare$

Assume that $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}\exists\vec{z}\,\bigl(x\mapsto(y_% {1},\dots,y_{\kappa}))\star\phi\bigr)\{y\leftarrow y_{i}\}$ . This entails that there exist a sequence of locations $\vec{m}$ such that $(\mathfrak{s}[\vec{z}\leftarrow\vec{m}],\mathfrak{h})\models_{{\cal R}}\bigl(x% \mapsto(y_{1},\dots,y_{\kappa}))\star\phi\bigr)\{y\leftarrow y_{i}\}$ , i.e., $(\mathfrak{s}[y\leftarrow\ell_{i},\vec{z}\leftarrow\vec{m}],\mathfrak{h})% \models_{{\cal R}}x\mapsto(y_{1},\dots,y_{\kappa})\star\phi$ , with $\ell_{i}=\mathfrak{s}[\vec{z}\leftarrow\vec{m}](y_{i})$ and $\mathfrak{h}(\mathfrak{s}(x))=(\ell_{1},\dots,\ell_{\kappa})$ (as $x$ does not occur in $\vec{z}$ ). In particular, this entails that $\mathfrak{s}(x)\in\mathsf{dom}(\mathfrak{h})$ , thus $y\leftarrow x.i$ does not fail on $(\mathfrak{s},\mathfrak{h})$ , and $(\mathfrak{s}[y\leftarrow\ell_{i}],\mathfrak{h})\models_{{\cal R}}\exists\vec{% z}\,\bigl(x\mapsto(y_{1},\dots,y_{\kappa}))\star\phi\bigr)$ . Thus $(\mathfrak{s},\mathfrak{h})\models_{{\cal R}}[y\leftarrow x.i]\,(\exists\vec{z% }\,(x\mapsto(y_{1},\dots,y_{\kappa}))\star\phi))$ .

[bib.bib1] [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. doi:10.1007/978-3-540-30538-5_9.

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

[bib.bib3] [3] Cristiano Calcagno, Hongseok Yang, and Peter 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. doi:10.1007/3-540-45294-X_10.

[bib.bib4] [4] 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. doi:10.1007/978-3-642-23217-6_16.

[bib.bib5] [5] Frank S. de Boer, Hans-Dieter A. Hiep, and Stijn de Gouw. Dynamic separation logic. In Marie Kerjean and Paul Blain Levy, editors, Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, MFPS XXXIX, Indiana University, Bloomington, IN, USA, June 21-23, 2023, volume 3 of EPTICS. EpiSciences, 2023. doi:10.46298/ENTICS.12297.

[bib.bib6] [6] Stéphane Demri, Didier Galmiche, Dominique Larchey-Wendling, and Daniel Méry. Separation logic with one quantified variable. In CSR’14, volume 8476 of LNCS, pages 125–138. Springer, 2014. doi:10.1007/978-3-319-06686-8_10.

[bib.bib7] [7] Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment checking in separation logic with inductive definitions is 2-exptime hard. In Elvira Albert and Laura Kovács, editors, 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. doi:10.29007/F5WH.

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

[bib.bib9] [9] Mnacho Echenim and Nicolas Peltier. A proof procedure for separation logic with inductive definitions and data. J. Autom. Reason., 67(3):30, 2023. doi:10.1007/S10817-023-09680-4.

[bib.bib10] [10] Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomás Vojnar. Compositional entailment checking for a fragment of separation logic. Formal Methods Syst. Des., 51(3):575–607, 2017. doi:10.1007/S10703-017-0289-4.

[bib.bib11] [11] Constantin Enea, Mihaela Sighireanu, and Zhilin Wu. On automated lemma generation for separation logic with inductive definitions. In ATVA 2015, Proceedings, pages 80–96, 2015. doi:10.1007/978-3-319-24953-7_7.

[bib.bib12] [12] Radu Iosif, Adam Rogalewicz, and Jiri Simacek. The tree width of separation logic with recursive definitions. In Proc. of CADE-24, volume 7898 of LNCS, 2013.

[bib.bib13] [13] Radu Iosif, Adam Rogalewicz, and Tomás Vojnar. Deciding entailments in inductive separation logic with tree automata. In Franck Cassez and Jean-François Raskin, editors, ATVA 2014, Proceedings, volume 8837 of LNCS, pages 201–218. Springer, 2014. doi:10.1007/978-3-319-11936-6_15.

[bib.bib14] [14] Samin S Ishtiaq and Peter W O’Hearn. Bi as an assertion language for mutable data structures. In ACM SIGPLAN Notices, volume 36, pages 14–26, 2001. doi:10.1145/360204.375719.

[bib.bib15] [15] Christoph Matheja, Jens Pagel, and Florian Zuleger. A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. ACM Trans. Comput. Log., 24(1):1:1–1:76, 2023. doi:10.1145/3534927.

[bib.bib16] [16] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Laurent 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. doi:10.1007/3-540-44802-0_1.

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

[bib.bib18] [18] Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with inductive definitions. In Anthony Widjaja 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. doi:10.1007/978-3-030-34175-6_19.