# A Complete Axiomatisation for Quantifier-Free Separation Logic

Stéphane Demri, Etienne Lozes, Alessio Mansutti

► To cite this version:

Stéphane Demri, Etienne Lozes, Alessio Mansutti. A Complete Axiomatisation for Quantifier-Free Separation Logic. Logical Methods in Computer Science, 2021, 17 (3), pp.17:1–17:64. 10.46298/lmcs-17(3:17)2021 . hal-03005864

HAL Id: hal-03005864

https://hal.science/hal-03005864

Submitted on 28 Sep 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
A COMPLETE AXIOMATISATION FOR
QUANTIFIER-FREE SEPARATION LOGIC

STÉPHANE DEMRI, ÉTIENNE LOZES, AND ALESSIO MANSUTTI

LSV, CNRS, ENS Paris-Saclay - 4, avenue des Sciences - 91190 Gif-sur-Yvette
*e-mail address:* demri@lsv.fr

I3S - Les Algorithmes - Bâtiment Euclide B - 2000, route des Lucioles - 06900 Sophia Antipolis
*e-mail address:* etienne.lozes@i3s.unice.fr

LSV, CNRS, ENS Paris-Saclay - 4, avenue des Sciences - 91190 Gif-sur-Yvette
*e-mail address:* mansutti@lsv.fr

ABSTRACT. We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the concrete semantics needs to be taken into account. Therefore, we present the first internal Hilbert-style axiomatisation for quantifier-free separation logic. The calculus is divided in three parts: the axiomatisation of core formulae where Boolean combinations of core formulae capture the expressivity of the whole logic, axioms and inference rules to simulate a bottom-up elimination of separating connectives, and finally structural axioms and inference rules from propositional calculus and Boolean BI with the magic wand.

# 1. INTRODUCTION

**The virtue of axiomatising program logics.** Designing a Hilbert-style axiomatisation for your favourite logic is usually quite challenging. This does not lead necessarily to optimal decision procedures, but the completeness proof usually provides essential insights to better understand the logic at hand. That is why many logics related to program verification have been axiomatised, often requiring non-trivial completeness proofs. By way of example, there are axiomatisations for the linear-time $\mu$-calculus [Kai95, Dou17], the modal $\mu$-calculus [Wal00] or for the alternating-time temporal logic ATL [GvD06], the full computation tree logic CTL* [Rey01], for probabilistic extensions of $\mu$-calculus [LMX16] or for a coalgebraic generalisation [SV18]. Concerning the separation logics that extend Hoare-Floyd logic to verify programs with mutable data structures (see e.g. [OP99, Rey02, IO01, O'H12, PSO18]), a Hilbert-style axiomatisation of Boolean BI has been introduced in [GLW06], but remained at the abstract level of Boolean BI. More recently, HyBBI [BV14],

*Key words and phrases:* separation logic, internal calculus, adjunct/quantifier elimination.

* This is the long version of the first part of [DLM20].
a hybrid version of Boolean BI has been introduced in order to axiomatise various classes of abstract separation logics; HyBBI naturally considers classes of abstract models (typically preordered partial monoids) but it does not fit exactly the heaplet semantics of separation logics. Furthermore, the addition of nominals (in the sense of hybrid modal logics, see e.g. [ABM01]) extends substantially the object language. Other frameworks to axiomatise classes of abstract separation logics can be found in [DP18, Doc19] and in [HCGT18], respectively with labelled tableaux calculi and with sequent-style proof systems.

**Our motivations.** Since the birth of separation logics, there has been a lot of interest in the study of decidability and computational complexity issues, see e.g. [COY01, BDL09, BIP10, CHO+11, DGLWM17, BK18, DLM18a, Man18, Man20], and comparatively less attention to the design of proof systems, and even less with the puristic approach that consists in discarding any external feature such as nominals or labels in the calculi. The well-known advantages of such an approach include an exhaustive understanding of the expressive power of the logic and discarding the use of any external artifact referring to semantical objects. For instance, a tableaux calculus with labels for quantifier-free separation logic is designed in [GM10], whereas Hilbert-style calculi for abstract separation logics with nominals are defined in [BV14]. Similarly, display calculi for bunched logics are provided in [Bro12] but such calculi extend Gentzen-style proof systems by allowing new structural connectives, which provides an elegant means to simulate labels. In this paper, we advocate a puristic approach and aim at designing a Hilbert-style proof system for quantifier-free separation logic SL(*, →*) (which includes the separating conjunction * and implication →, as well as all Boolean connectives) and more generally for other separation logics, while remaining within the very logical language (see the second part of [DLM20]).<fnref n="1" /> Consequently, in this work, we only focus on axiomatising separation logics, and we have no claim for practical applications in the field of program verification with separation logics. Aiming at internal calculi is a non-trivial task as the general frameworks for abstract separation logics make use of labels, see e.g. [DP18, HCGT18]. We cannot rely on label-free calculi for BI, see e.g. [Pym02, GLW06], as separation logics are usually understood as Boolean BI interpreted on models of heap memory and therefore require calculi that cannot abstract as much as it is the case for Boolean BI. Finally, there are many translations from separation logics into logics or theories, see e.g. [CGH05, PWZ13, BDL12, RISK16]. However, completeness cannot in general be inherited by sublogics as the proof system should only use the sublogic and therefore the axiomatisation of sublogics may lead to different methods. A more detailed discussion about the related work can be found in Section 7.

**Our contribution.** We propose a modular axiomatisation of quantifier-free separation logic, starting with a complete axiomatisation of a Boolean algebra of core formulae, and incrementally adding support for the spatial connectives: the separating conjunction and the separating implication (a.k.a. the magic wand). The same approach could be followed for other fragments of separation logic, as we did in the conference version of this paper [DLM20] (see also a similar approach in [DFM19]). Thus, our approach can be considered with the broader perspective of a generic method for axiomatising separation logics. Let us be a bit more precise.

<footnote n="1">¹We aim at defining *internal calculi* according to the terminology from the Workshop on External and Internal Calculi for Non-Classical Logics, FLOC’18, Oxford, http://weic2018.loria.fr.</footnote>
In Section 3, we present the first Hilbert-style proof system for SL(*, -*) that uses axiom schemas and rules involving only formulae of this logic. We mainly introduce our approach and present the notations that are used throughout the paper. Each formula of SL(*, -*) is equivalent to a Boolean combination of core formulae: simple formulae of the logic expressing elementary properties about the models [Loz04b]. Though core formulae (also called test formulae) have been handy in several occasions for establishing complexity results for separation logics, see e.g. [BDL09, DLM18a, Man18, EIP19], in the paper, these formulae are instrumental for the axiomatisation. Indeed, the axiomatisation of SL(*, -*) is designed starting from an axiomatisation of Boolean combinations of core formulae (introduced in Section 4), and adding axioms and rules that allow to syntactically transform every formula of SL(*, -*) into such Boolean combinations. This transformation is introduced in Section 5 and in Section 6: the former section shows how to eliminate the separating conjunction *, whereas the latter one treat the separating implication -*. Schematically, for a valid formula $\varphi$, we conclude $\vdash \varphi$ from $\vdash \varphi'$ and $\vdash \varphi' \Leftrightarrow \varphi$, where $\varphi'$ is a Boolean combination of core formulae. Our methodology leads to a calculus that is divided in three parts: (1) the axiomatisation of Boolean combinations of core formulae, (2) axioms and inference rules to simulate a bottom-up elimination of separating the separating conjunction, and (3) axioms and inference rules to simulate a bottom-up elimination of the magic wand. Such an approach that consists in first axiomatising a syntactic fragment of the whole logic (in our case, the core formulae), is best described in [Dou17] (see also [Wal00, vB11, WC13, Lüc18, DFM19]). Section 7 compares works from the literature with our contribution, either for separation logics (abstract versions, fragments, etc.) or for knowledge logics for which the axiomatisation has been performed by using a reduction to a strict syntactic fragment though expressively complete.

This paper is the complete version of the first part of [DLM20] dedicated to quantifier-free separation logic SL(*, -*). The complete version of the second part of [DLM20] dedicated to the new separation logic SL(*, $\exists$:=$\neg$) is too long to be included in the present document. A technical appendix contains syntactic derivations omitted from the body of the paper.

## 2. PRELIMINARIES

### 2.1. Quantifier-free separation logic.
We present the quantifier-free separation logic SL(*, -*), that includes standard features such as the separating conjunction *, the separating implication -* and closure under Boolean connectives. Let VAR = {$x, y, ...$} be a countably infinite set of program variables. The formulae $\varphi$ of SL(*, -*) and its atomic formulae $\pi$ are built from the grammars below where x, y $\in$ VAR.

$$ \pi ::= x = y \mid x \leftrightarrow y \mid \text{emp} \qquad \varphi ::= \pi \mid \neg\varphi \mid \varphi \land \varphi \mid \varphi * \varphi \mid \varphi ::= \varphi. $$

The connectives $\Rightarrow$, $\Leftrightarrow$ and $\lor$ are defined as usually. In the heaplet semantics, the formulae of SL(*, -*) are interpreted on memory states that are pairs $(s, h)$ where $s: VAR \to LOC$ is a variable valuation (the store) from the set of program variables to a countably infinite set of locations LOC = {$\ell_0, \ell_1, \ell_2, ...$}, whereas $h: LOC \to_{fin} LOC$ is a partial function with finite domain (the heap). We write dom($h$) to denote its domain and ran($h$) to denote its range. A memory cell of $h$ is understood as a pair of locations $(\ell, \ell')$ such that $\ell \in$ dom($h$) and $\ell' = h(\ell)$. As usual, the heaps $h_1$ and $h_2$ are said to be disjoint, written $h_1 \# h_2$, if dom($h_1$) $\cap$ dom($h_2$) = $\emptyset$; when this holds, we write $h_1 + h_2$ to denote the heap corresponding to the disjoint union of the graphs of $h_1$ and $h_2$, hence dom($h_1 + h_2$) = dom($h_1$) $\lor$ dom($h_2$).
When the domains of $h_1$ and $h_2$ are not disjoint, the composition $h_1 + h_2$ is not defined. Moreover, we write $h' \subseteq h$ to denote that $\text{dom}(h') \subseteq \text{dom}(h)$ and for all locations $\ell \in \text{dom}(h')$, we have $h'(\ell) = h(\ell)$. If $h' \subseteq h$ then $h'$ is said to be a subheap of $h$. The satisfaction relation $\models$ is defined as follows (we omit standard clauses for the Boolean connectives $\neg$ and $\wedge$):

$$
\begin{align*}
(s, h) &\models \mathbf{x} = \mathbf{y} \quad \begin{array}{@{}c@{\hspace{0.5em}}c@{}}
    \text{def} & \\
    \Leftrightarrow &
  \end{array}
  s(\mathbf{x}) = s(\mathbf{y}), \\
(s, h) &\models \mathbf{emp} \quad \begin{array}{@{}c@{\hspace{0.5em}}c@{}}
    \text{def} & \\
    \Leftrightarrow &
  \end{array}
  \text{dom}(h) = \emptyset, \\
(s, h) &\models \mathbf{x} \hookrightarrow \mathbf{y} \quad \begin{array}{@{}c@{\hspace{0.5em}}c@{}}
    \text{def} & \\
    \Leftrightarrow &
  \end{array}
  s(\mathbf{x}) \in \text{dom}(h) \text{ and } h(s(\mathbf{x})) = s(\mathbf{y}), \\
(s, h) &\models \varphi_1 * \varphi_2 \quad \begin{array}{@{}c@{\hspace{0.5em}}c@{}}
    \text{def} & \\
    \Leftrightarrow &
  \end{array}
  \text{there are } h_1, h_2 \text{ such that } h_1 \# h_2, (h_1 + h_2) = h, \\
  & \phantom{\text{there are }} (s, h_1) \models \varphi_1 \text{ and } (s, h_2) \models \varphi_2, \\
(s, h) &\models \varphi_1 * \neg \varphi_2 \quad \begin{array}{@{}c@{\hspace{0.5em}}c@{}}
    \text{def} & \\
    \Leftrightarrow &
  \end{array}
  \text{for all } h_1 \text{ such that } h_1 \# h \text{ and } (s, h_1) \models \varphi_1, \\
  & \phantom{\text{for all }} \text{we have } (s, h + h_1) \models \varphi_2.
\end{align*}
$$

We denote with $\perp$ the contradiction $\mathbf{x} \neq \mathbf{x}$, and with $\top$ its negation $\neg\perp$. The subtraction operator $\ominus$ (kind of dual of $\dashv$), defined by $\varphi \ominus \psi \stackrel{\text{def}}{=} \neg(\varphi \dashv \neg\psi)$, has the following semantics:

$$
(s, h) \models \varphi \ominus \psi \stackrel{\text{def}}{\Leftrightarrow} \text{there is a heap } h' \text{ such that } h \# h', (s, h') \models \varphi, \text{ and } (s, h + h') \models \psi.
$$

We adopt the standard precedence between classical connectives, and extend it for the connectives of separation logic as follows: $\{\neg\} > \{\wedge, \vee, \ast\} > \{\Rightarrow, \ast, \ominus\} > \{\leftrightarrow\}$. Notice that the separating conjunction $\ast$ has a higher precedence than the separating implication $\ast$, and it has the same precedence as the (classical) conjunction $\wedge$. For instance, $\varphi \ast \psi \Rightarrow \chi$ and $\neg\varphi \ast \psi \ast \psi$ stand for $(\varphi \ast \psi) \Rightarrow \chi$ and $(\neg\varphi) \ast (\psi \ast \psi)$, respectively.

A formula $\varphi$ is valid if $(s, h) \models \varphi$ for all memory states $(s, h)$ (and we write $\models \varphi$). For a complete description of separation logic, see e.g. [Rey02]. Given a set of formulae $\Gamma$, we write $\Gamma \models \varphi$ (semantical entailment) whenever $(s, h) \models \varphi$ holds for every memory state $(s, h)$ satisfying every formula in $\Gamma$.

It is worth noting that quantifier-free SL($\ast, \dashv\ast$) axiomatised in the paper admits a PSPACE-complete validity problem, see e.g. [COY01], and should not be confused with propositional separation logic with the stack-heap models shown undecidable in [BK14, Corollary 5.1] (see also [DD15, Section 4]), in which there are propositional variables interpreted by sets of memory states.

2.2. Core formulae. We introduce the following well-known shortcuts, that play an im-
portant role in the sequel. Let $\mathbf{x} \in \text{VAR}$ and $\beta \in \mathbb{N}$.

<table>
  <thead>
    <tr>
      <th>Shortcut:</th>
      <th>Definition:</th>
      <th>Semantics:</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>alloc(x) &harr; (x &mapsto; x) &ast; &perp;</td>
      <td></td>
      <td>(s, h) &models; alloc(x) iff s(x) &isin; dom(h)</td>
    </tr>
    <tr>
      <td>size &ge; &beta; &harr; {<br/> &perp;<br/> &neg;emp<br/> &neg;emp &ast; size &ge; &beta; &minus; 1</td>
      <td>
        <table>
          <tr>
            <td>&top;</td>
            <td>if &beta; = 0</td>
          </tr>
          <tr>
            <td>&neg;emp</td>
            <td>if &beta; = 1</td>
          </tr>
          <tr>
            <td>&neg;emp &ast; size &ge; &beta; &minus; 1</td>
            <td>otherwise</td>
          </tr>
        </table>
      </td>
      <td>(s, h) &models; size &ge; &beta; iff card dom(h) &ge; &beta;</td>
    </tr>
  </tbody>
</table>

We use $\mathbf{size}=\beta$ as a shorthand for $\mathbf{size}\ge\beta \wedge \neg\mathbf{size}\ge\beta+1$. We also write $\text{card}(X)$ to denote the cardinality of the set $X$.

The core formulae are expressions of the form $\mathbf{x} = \mathbf{y}$, $\text{alloc}(\mathbf{x})$, $\mathbf{x} \leftrightarrow \mathbf{y}$ and $\mathbf{size} \ge \beta$, where $\mathbf{x}, \mathbf{y} \in \text{VAR}$ and $\beta \in \mathbb{N}$. As we can see, the core formulae are simple SL($\ast, \dashv\ast$) formulae.
It is well-known, see e.g. [Yan01, Loz04a], that these formulae capture essential properties of the memory states. In particular, every formula of SL(*, -*) is logically equivalent to a Boolean combination of core formulae [Loz04a].

As a simple but crucial insight, since the core formulae are formulae of SL(*, -*), we can freely use them to help us defining the proof system for SL(*, -*), and preventing us from going outside the original language. Having this in mind, the resulting proof system is Hilbert-style and completely internal (the formal definition of these types of systems is recalled below).

Given $\mathbf{X} \subseteq_{\text{fin}} \text{VAR}$ and $\alpha \in \mathbb{N}$, we define $\text{Core}(\mathbf{X}, \alpha)$ as the set

$$ \{x = y, \text{alloc}(x), x \to y, \text{size} \ge \beta \mid x, y \in \mathbf{X}, \beta \in [0, \alpha]\}. $$

$\text{Bool}(\text{Core}(\mathbf{X}, \alpha))$ is defined as the set of Boolean combinations of formulae from $\text{Core}(\mathbf{X}, \alpha)$, whereas $\text{Conj}(\text{Core}(\mathbf{X}, \alpha))$ is the set of conjunctions of literals built upon $\text{Core}(\mathbf{X}, \alpha)$. As usual, a *literal* is understood as a core formula or its negation. Let $\varphi = L_1 \wedge \dots \wedge L_n \in \text{Conj}(\text{Core}(\mathbf{X}, \alpha))$ be a conjunction of literals $L_1, \dots, L_n$. We write $\text{Lt}(\varphi)$ to denote $\{L_1, \dots, L_n\}$. In forthcoming developments, we are interested in the maximum $\beta$ (if any) of formulae of the form $\text{size} \ge \beta$ occurring positively in a conjunction of literals, if any. For this reason, we write $\max_{\text{size}}(\varphi)$ for $\max(\{\beta \in \mathbb{N} \mid \text{size} \ge \beta \in \text{Lt}(\varphi)\} \cup \{0\})$. For instance, given $\varphi = \text{alloc}(x) \wedge \text{size} \ge 2 \wedge \neg \text{size} \ge 4$, we have $\text{Lt}(\varphi) = \{\text{alloc}(x), \text{size} \ge 2, \neg \text{size} \ge 4\}$, and $\max_{\text{size}}(\varphi) = 2$. Given two conjunctions of literals $\varphi \in \text{Conj}(\text{Core}(\mathbf{X}, \alpha_1))$ and $\psi \in \text{Conj}(\text{Core}(\mathbf{X}, \alpha_2))$, $\psi \subseteq_{\text{Lt}} \varphi$ stands for $\text{Lt}(\psi) \subseteq \text{Lt}(\varphi)$. Finally, we introduce a few more shortcuts and we write

* $\chi \subseteq_{\text{Lt}} \{\varphi \mid \psi\}$ for "$\chi \subseteq_{\text{Lt}} \varphi$ or $\chi \subseteq_{\text{Lt}} \psi$", $\chi \subseteq_{\text{Lt}} \{\varphi \mid \psi\}$ for "$\chi \subseteq_{\text{Lt}} \varphi$ and $\chi \subseteq_{\text{Lt}} \psi$", $\chi \subseteq_{\text{Lt}} \{\varphi \mid \psi\}$ for "$\chi \subseteq_{\text{Lt}} \varphi$ or $\psi \subseteq_{\text{Lt}} \chi$".

* $\{\varphi \mid \psi\} \subseteq_{\text{Lt}} \chi$ for "$\varphi \subseteq_{\text{Lt}} \chi$ or $\psi \subseteq_{\text{Lt}} \chi$".

Given a finite set of formulae $\Gamma = \{\varphi_1, \dots, \varphi_n\}$, we write $\wedge \Gamma$ as a shorthand for $\varphi_1 \wedge \dots \wedge \varphi_n$. Similarly, $*\Gamma$ stands for $\varphi_1 * \dots * \varphi_n$. It is important to notice that, similarly to the classical conjunction, the separating conjunction $*$ is associative and commutative (see the axioms $(A_8^*)$ and $(A_7^*)$ in Figure 1), and therefore the semantics of $*\Gamma$ is uniquely defined, regardless of the choice of ordering for $\varphi_1, \dots, \varphi_n$.

### 2.3. Hilbert-style proof systems.
A Hilbert-style proof system $\mathcal{H}$ is defined as a set of tuples $((\Phi_1, \dots, \Phi_n), \Psi)$ with $n \ge 0$, where $\Phi_1, \dots, \Phi_n, \Psi$ are formula schemata (a.k.a axiom schemata). When $n \ge 1$, $((\Phi_1, \dots, \Phi_n), \Psi)$ is called an inference rule, otherwise it is an axiom. As usual, formula schemata generalise the notion of formulae by allowing metavariables for formulae (typically $\varphi, \psi, \chi$), for program variables (typically $x, y, z$) or for any type of syntactic objects in formulae, depending on the context. The set of formulae derivable from $\mathcal{H}$ is the least set $S$ such that for all $((\Phi_1, \dots, \Phi_n), \Psi) \in \mathcal{H}$ and for all substitutions $\sigma$, if $\Phi_1\sigma, \dots, \Phi_n\sigma \in S$ then $\Psi\sigma \in S$. We write $\vdash_{\mathcal{H}} \varphi$ if $\varphi$ is derivable from $\mathcal{H}$. A proof system $\mathcal{H}$ is sound if all derivable formulae are valid. $\mathcal{H}$ is complete if all valid formulae are derivable. We say that $\mathcal{H}$ is adequate whenever it is both sound and complete. Lastly, $\mathcal{H}$ is strongly complete whenever for all sets of formulae $\Gamma$ and formulae $\varphi$, we have $\Gamma \models \varphi$ (semantical entailment) if and only if $\vdash_{\mathcal{H}} \Gamma \vdash \varphi$.

Interestingly enough, there is no strongly complete proof system for SL(*, -*), as strong completeness implies compactness and separation logic is not compact. Indeed, $\{\text{size} \ge \beta \mid \beta \in \mathbb{N}\}$ is unsatisfiable, as heaps have finite domains, but all finite subsets
<figure><img src="image_2.png" /><figcaption>Figure 1: The proof system $\mathcal{H}_C(*, -*)$.</figcaption></figure>

of it are satisfiable. Even for the weaker notion of completeness, deriving an Hilbert-style axiomatisation for SL(*, -*) remains challenging. Indeed, the satisfiability problem for SL(*, -*) reduces to its validity problem, making SL(*, -*) an unusual logic from a proof-theoretical point of view. Let us develop a bit further this point.

Let $\varphi$ be a formula built over program variables in $X \subseteq_{\text{fin}} \text{VAR}$, and let $\approx$ be an equivalence relation on $X$. The formula $\psi_{\approx} \stackrel{\text{def}}{=} (\text{emp} \wedge \bigwedge_{x \approx y} x = y \wedge \bigwedge_{x \not\approx y} x \neq y) \Rightarrow (\varphi \stackrel{\otimes}{\supset} \top)$ can be shown to be valid iff for every store $s$ agreeing on $\approx$, there is a heap $h$ such that $(s, h) \models \varphi$. It is known that for all stores $s, s'$ agreeing on $\approx$, and every heap $h$, the memory states $(s, h)$ and $(s', h)$ satisfy the same set of formulae having variables from $X$. Since the antecedent of $\psi_{\approx}$ is satisfiable, we conclude that $\psi_{\approx}$ is valid iff there are a store $s$ agreeing on $\approx$ and a heap $h$ such that $(s, h) \models \varphi$. To check whether $\varphi$ is satisfiable, it is sufficient to find an equivalence relation $\approx$ on $X$ such that $\psi_{\approx}$ is valid. As the number of equivalence relations on $X$ is finite, we obtain a Turing reduction from satisfiability to validity. Consequently, it is not possible to define sound and complete axiom systems for any extension of SL(*, -*) admitting an undecidable validity problem (as long as there is a reduction from satisfiability to validity, as above). A good example is the logic SL(*, -, ls) [DLM18b] (extension of SL(*, -*) with the well-known list-segment predicate ls); see also the first-order separation logic in [BDL12]. Indeed, to obtain a sound and complete axiom system, the validity problem has to be recursively enumerable (r.e.). However, this would imply that the satisfiability problem is also r.e.. As a formula $\varphi$ is not valid if and only if $\neg \varphi$ is satisfiable, we then conclude that the set of valid formulae is recursive, hence decidable, a contradiction.

### 3. HILBERT-STYLE PROOF SYSTEM FOR SL(*, -*)

In Figure 1, we present the proof system $\mathcal{H}_C(*, -*)$ that shall be shown to be sound and complete for quantifier-free separation logic SL(*, -*). $\mathcal{H}_C(*, -*)$ and all the subsequent
fragments of $\mathcal{H}_C(*, -*)$ contain the axiom schemata and modus ponens for the propositional calculus (we omit these rules in the presentation). In the axioms $(\mathbf{A}_{14}^*)$, $(\mathbf{A}_{21}^*)$ and $(\mathbf{A}_{23}^*)$, the notation $\varphi [\mathcal{B}]$ refers to the axiom schema $\varphi$ assuming that the Boolean condition $\mathcal{B}$ holds. We highlight the fact that, in these three axioms, $\mathcal{B}$ is a simple syntactical condition. In the axiom $(\mathbf{A}_{19}^*)$, $a \div b$, where $a, b \in \mathbb{N}$, stands for $\max(0, a - b)$.

Though the full proof system $\mathcal{H}_C(*, -*)$ is presented quite early in the paper, its final design remains the outcome of a refined analysis on principles behind SL(*, -*) tautologies. Fortunately, we do not start from scratch as the calculus must contain the axioms and rules from the Hilbert-style proof system for Boolean BI [GLW06]. At first glance the system $\mathcal{H}_C(*, -*)$ may seem quite arbitrary, but the role of the different axioms shall become clearer during the paper. In designing the system, we tried to define axioms that are as simple as possible, which helps highlighting the most fundamental properties of SL(*, -*). Note that we have not formally proved that our proof system $\mathcal{H}_C(*, -*)$ is minimal (though we have tried our best to have a small amount of small axioms). Such an investigation would be out of the scope of the paper, mainly for lack of space. The standard way to proceed would be to design models different from memory states and to establish that all axioms but one are valid (which would prove that this axiom is needed when all the other axioms are present).

We insist: the core formulae in $\mathcal{H}_C(*, -*)$ should be understood as mere abbreviations, which makes all the axioms in Figure 1 belong to the original language of SL(*, -*). In order to show the completeness of $\mathcal{H}_C(*, -*)$, we first establish the completeness for subsystems of $\mathcal{H}_C(*, -*)$, with respect to syntactical fragments of SL(*, -*). In particular, we consider

* $\mathcal{H}_C$: an adequate proof system for the propositional logic of core formulae (see Figure 4),

* $\mathcal{H}_C(*)$: an extension of $\mathcal{H}_C$ that is adequate for the logic SL(*, alloc), i.e. the logic obtained from SL(*, -*) by removing the separating implication $-*$ at the price of adding the formula alloc(x) (see Figure 5).

* The full $\mathcal{H}_C(*, -*)$, which can be seen as an extension of $\mathcal{H}_C(*)$ that allows to reason about the separating implication (see Figure 7).

For the completeness of $\mathcal{H}_C$ and $\mathcal{H}_C(*)$, we add intermediate axioms that reveal to be useless when the full proof system $\mathcal{H}_C(*, -*)$ is considered, as they become derivable. By convention, the axioms whose name is of the form $A_i^?$ are axioms that remain in $\mathcal{H}_C(*, -*)$ (see Figure 1) whereas those named $I_i^?$ are intermediate axioms that are instrumental for the proof of completeness of a subsystem among $\mathcal{H}_C$ and $\mathcal{H}_C(*)$ (and therefore none of them occur in Figure 1). The numbering of the axioms in Figure 1 is not consecutive, as intermediate axioms shall be placed within the holes. It is worth noting that the axiom $(\mathbf{A}_{13}^*)$ had an intermediate status in [DLM20] but we realised that actually this axiom does need to be considered as a first-class axiom in the proof system $\mathcal{H}_C(*, -*)$.

The choice of introducing $\mathcal{H}_C$ and $\mathcal{H}_C(*)$ naturally follows from the main steps required for the completeness of $\mathcal{H}_C(*, -*)$. In particular, the main “task” of $\mathcal{H}_C(*)$ is to produce a bottom-up elimination of the separating conjunction $*$, at the price of introducing Boolean combinations of core formulae, which can be proved valid thanks to $\mathcal{H}_C$. Similarly, the axioms and rules added to $\mathcal{H}_C(*)$ to define $\mathcal{H}_C(*, -*)$ are dedicated to perform a bottom-up elimination of the separating implication. A merit of this methodology is that only the completeness of the calculus $\mathcal{H}_C$ is proved using the standard countermodel method. The additional steps required to prove the completeness of $\mathcal{H}_C(*)$ and $\mathcal{H}_C(*, -*)$ are (almost) completely syntactical. For instance, to show the completeness of $\mathcal{H}_C(*)$, we consider arbitrary Boolean combinations of core formulae $\varphi$ and $\psi$, and exhibiting a Boolean combination of
core formulae $\chi$ such that $\varphi * \psi \Leftrightarrow \chi$ is valid. We show that this validity can be syntactically proved within $\mathcal{H}_C(*)$, and then rely on the fact that $\mathcal{H}_C$ is complete for Boolean combination of core formulae to deduce that $\mathcal{H}_C(*)$ is complete for $\text{SL}(*, \text{alloc})$.

Along the paper, we shall have the opportunity to explain the intuition between the axioms and rules. Below, we provide a few hints. The axioms $(A_1^C)-(A_4^C)$ deal with the core formulae and are quite immediate to grasp. More interestingly, whereas the axioms $(A_7^*)$-$((A_{11}^*)-(A_{20}^*))$ are quite general about separating conjunction and are inherited from Boolean BI, the axioms $(A_{14}^*)$-$((A_{20}^*)-(A_{14}^*))$ state how separating conjunction behaves with the core formulae. As for Boolean combinations of core formulae involved in the axioms $(A_1^C)-(A_4^C)$, these axioms $(A_{14}^*)$-$((A_{20}^*)-(A_{14}^*))$ are also not difficult to understand. Besides, the inference rules $\*-\text{Adj}$ and $\text{-Adj}$ simply reflect that separating conjunction and separating implication are adjoint operators, and are taken from Boolean BI, see e.g. [GLW06]. The axioms $(A_{21}^{*-})$-$((A_{23}^{*-})$) dedicated to the interaction between the separating implication and core formulae are expressed with the help of the setpraction operator $\oplus$ to ease the understanding but as well-known, setpraction is defined with the help of the separating implication and Boolean negation. For instance, the axiom $(A_{22}^{*-})$ states that it is always possible to add some one-memory-cell heap $h'$ to some heap $h$ while none of the variables from a finite set X is allocated in $h'$. This natural property in our framework would not hold in general if LOC were not infinite. Obviously, the setpraction $\oplus$ is also understood as an abbreviation.

As a sanity check, we show that the proof system $\mathcal{H}_C(*, \text{-})$ is sound with respect to $\text{SL}(*, \text{-})$. The proof does not pose any specific difficulty (as usual with most soundness proofs) but this is the opportunity for the reader to further get familiar with the axioms and rules from $\mathcal{H}_C(*, \text{-})$.

**Lemma 3.1.** $\mathcal{H}_C(*, \text{-})$ is sound.

The validity of the axioms $(A_1^C)$, $(A_2^C)$, $(A_3^C)$ and $(A_4^C)$ is straightforward. Moreover, the validity of the axioms $(A_7^*)$, $(A_8^*)$ and $(A_{11}^*)$ and the three inference rules ($\*-\text{Intro}$, $\*-\text{Adj}$ and $\text{-Adj}$) is inherited from Boolean BI (see [BV14] and [GLW06, Section 2]). Below, we show the validity of the remaining axioms, thus proving Lemma 3.1.

*Validity of the axiom (A<sub>13</sub><sup>*</sup>).* Let us show that $(\text{alloc}(x) * \text{alloc}(x))$ is not satisfiable. Ad absurdum, suppose there is a memory state $(s, h)$ such that $(s, h) \models (\text{alloc}(x) * \text{alloc}(x))$. By definition of $\models$, there are $h_1, h_2$ such that $h_1 \perp h_2$, $(h_1 + h_2) = h$, $(s, h_1) \models \text{alloc}(x)$ and $(s, h_2) \models \text{alloc}(x)$. Thus, $s(x) \in \text{dom}(h_1)$ and $s(x) \in \text{dom}(h_2)$, which leads to a contradiction with $h_1 \perp h_2$. $\square$

*Validity of the axiom (A<sub>14</sub><sup>*</sup>).* The proof of the validity of every instantiation of (A<sub>14</sub><sup>*</sup>) is similar (and quite easy), therefore we show just the case with $x \mapsto y * \top \Rightarrow x \mapsto y$. Suppose $(s, h) \models x \mapsto y * \top$. Then, there is a subheap $h_1 \subseteq h$ such that $(s, h_1) \models x \mapsto y$. Hence, $h_1(s(x)) = s(y)$. As $h_1 \subseteq h$, we obtain $h(s(x)) = s(y)$, which implies $(s, h) \models x \mapsto y$. $\square$

*Validity of the axiom (A<sub>15</sub><sup>*</sup>).* Suppose $(s, h) \models \neg \text{alloc}(x) * \neg \text{alloc}(x)$. Then, there are two disjoint heaps $h_1, h_2$ such that $h = h_1 + h_2$, $(s, h_1) \models \neg \text{alloc}(x)$ and $(s, h_2) \models \neg \text{alloc}(x)$. Then $s(x) \notin \text{dom}(h_1)$ and $s(x) \notin \text{dom}(h_2)$. Since $h = h_1 + h_2$, $\text{dom}(h) = \text{dom}(h_1) \cup \text{dom}(h_2)$ and therefore $s(x) \notin \text{dom}(h)$. We conclude that $(s, h) \models \neg \text{alloc}(x)$. $\square$

*Validity of the axiom (A<sub>16</sub><sup>*</sup>).* Suppose $(s, h) \models (\text{alloc}(x) \wedge \neg x \mapsto y) * \top$. Then there is a subheap $h_1 \subseteq h$ such that $(s, h_1) \models \text{alloc}(x) \wedge \neg x \mapsto y$. Hence, $s(x) \in \text{dom}(h_1)$ and
<figure><img src="image_3.png" /><figcaption>Figure 2: A proof of $\mathbf{emp} \Rightarrow ((\mathbf{alloc}(x) \wedge \mathbf{size} = 1) * \neg \mathbf{size} \ge 2)$.</figcaption></figure>

$h_1(s(x)) \neq s(y)$. As $h_1 \subseteq h$, we obtain $s(x) \in \text{dom}(h)$ and $h(s(x)) \neq s(y)$ which by definition implies $(s, h) \models \neg x \leftrightarrow y$. $\square$

Validity of the axiom ($\mathbf{A}_{17}^*$). Suppose $(s, h) \models \mathbf{alloc}(x)$. Let $h_1 \stackrel{\text{def}}{=} \{s(x) \mapsto h(s(x))\}$ As $s(x) \in \text{dom}(h)$, $h_1 \subseteq h$ and $(s, h_1) \models \mathbf{alloc}(x) \wedge \mathbf{size} = 1$. We define $h_2$ as the unique heap such that $h_2+h_1=h$. As $(s, h_2) \models \top$, we have $(s, h) \models (\mathbf{alloc}(x) \wedge \mathbf{size} = 1) * \top$. $\square$

The proof of axiom ($\mathbf{A}_{18}^*$) is similar to the one of ($\mathbf{A}_{17}^*$), and hence omitted herein.

Validity of the axiom ($\mathbf{A}_{19}^*$). Suppose $(s, h) \models \neg \mathbf{size} \ge \beta_1 * \neg \mathbf{size} \ge \beta_2$, where $\beta_1, \beta_2 \ge 0$. Since $\neg \mathbf{size} \ge 0$ is not satisfiable, this implies that necessarily $\beta_1, \beta_2 \ge 1$. Hence, the axiom ($\mathbf{A}_{19}^*$) is trivially valid when $\beta_1 = 0$ or $\beta_2 = 0$. In the sequel, $\beta_1, \beta_2 \ge 1$. Then, there are heaps $h_1, h_2$ such that $h_1 \# h_2$, $h_1 + h_2 = h$, $(s, h_1) \models \neg \mathbf{size} \ge \beta_1$ and $(s, h_2) \models \neg \mathbf{size} \ge \beta_2$. By definition, $\text{card}(\text{dom}(h_1)) \le \beta_1 - 1$ and $\text{card}(\text{dom}(h_2)) \le \beta_2 - 1$. Since $\text{dom}(h) = \text{dom}(h_1) \cup \text{dom}(h_2)$, we obtain $\text{card}(\text{dom}(h)) \le \beta_1 + \beta_2 - 2$, which implies $(s, h) \models \neg \mathbf{size} \ge \beta_1 + \beta_2 - 1$. $\square$

Validity of the axiom ($\mathbf{A}_{20}^*$). Suppose $(s, h) \models \mathbf{alloc}(x) \wedge \mathbf{alloc}(y) \wedge x \neq y$. By definition, $s(x) \neq s(y)$, and $s(x), s(y) \in \text{dom}(h)$. Hence, $\text{card}(\text{dom}(h)) \ge 2$, and $(s, h) \models \mathbf{size} \ge 2$. $\square$

Validity of the axiom ($\mathbf{A}_{21}^*$). Let $X \subseteq_{\text{fin}} \text{VAR}$ and $(s, h)$ be a memory state. Let $h_1$ be a heap of size one such that $h_1(\ell) = \ell$ for some $\ell \notin \text{dom}(h) \cup s(X)$. We write $s(X)$ to denote the set $\{s(x) \mid x \in X\}$. Trivially $(s, h_1) \models \mathbf{size} = 1 \wedge \bigwedge_{x \in X} \neg \mathbf{alloc}(x)$. Moreover $h_1 \# h$ holds, hence $h_1+h_2$ is defined and $(s, h+h_1) \models \top$. Then, $(s, h) \models (\mathbf{size} = 1 \wedge \bigwedge_{x \in X} \neg \mathbf{alloc}(x)) \ominus \top$. $\square$

Validity of the axiom ($\mathbf{A}_{22}^*$). Suppose $(s, h) \models \neg \mathbf{alloc}(x)$. Let $h_1$ be the heap of size one such that $h_1(s(x)) = s(y)$. Trivially, $(s, h_1) \models x \leftrightarrow y \wedge \mathbf{size} = 1$. Moreover, as $s(x) \notin \text{dom}(h)$, $h_1 \# h$ holds. Therefore, $h_1+h$ is defined, and $(s, h+h_1) \models \top$. Then, $(s, h) \models (x \leftrightarrow y \wedge \mathbf{size} = 1) \ominus \top$. $\square$

Validity of the axiom ($\mathbf{A}_{23}^*$). Suppose $(s, h) \models \neg \mathbf{alloc}(x)$. Let $X \subseteq_{\text{fin}} \text{VAR}$ and $h_1 \stackrel{\text{def}}{=} \{s(x) \mapsto \ell\}$, where $\ell \notin s(X)$. Hence, $(s, h_1) \models \mathbf{alloc}(x) \wedge \mathbf{size} = 1 \wedge \bigwedge_{y \in X} \neg x \leftrightarrow y$. Since $s(x) \notin \text{dom}(h)$, $h_1 \# h$. Therefore, the heap $h+h_1$ is defined and $(s, h+h_1) \models \top$. Then, $(s, h) \models (\mathbf{alloc}(x) \wedge \mathbf{size} = 1 \wedge \bigwedge_{y \in X} \neg x \leftrightarrow y) \ominus \top$. $\square$

**Example 3.2.** To further familiarise with the axioms and the rules of $\mathcal{H}_C(*, -*)$, in Figure 2, we present a proof of $\mathbf{emp} \Rightarrow (\mathbf{alloc}(x) \wedge \mathbf{size} = 1 * \neg \mathbf{size} \ge 2)$. In the proof, a line "$j \mid \chi A, i_1, \dots, i_k$" states that $\chi$ is a theorem denoted by the index $j$ and derivable by the
axiom or the rule A. If A is a rule, the indices $i_1, \dots, i_k < j$ denote the theorems used as premises in order to derive $\chi$. When a formula is obtained as a propositional tautology or by propositional reasoning from other formulae, we may write "PC" (standing for short 'Propositional Calculus'). Similarly, we provide any useful piece of information justifying the derivation, such as "Ind. hypothesis", "See ..." or "Previously derived". In the example, we use the rule *-Adj, which together with the rule *-Adj states that the connectives * and *- are adjoint operators, as well as the axiom ($A_{19}^*$), stating that $\text{card}(\text{dom}(h)) \le \beta_1+\beta_2$ holds whenever a heap $h$ can be split into two subheaps whose domains have less than $\beta_1+1$ and $\beta_2+1$ elements, respectively. We also use the following theorems and rules:

$$ (\wedge \mathbf{Er}) \quad \psi \wedge \varphi \Rightarrow \varphi \qquad (\neg\neg\mathbf{I}) \quad \varphi \Rightarrow \neg\neg\varphi \quad \Rightarrow\text{-Tr}: \quad \frac{\varphi \Rightarrow \chi \quad \chi \Rightarrow \psi}{\varphi \Rightarrow \psi} \qquad \text{-Ilr}: \quad \frac{\varphi \Rightarrow \varphi' \quad \psi \Rightarrow \psi'}{\varphi \ast \psi \Rightarrow \varphi' \ast \psi'} $$

The first two theorems and the first rule are derivable by pure propositional reasoning. By way of example, we show that the inference rule *-Ilr is admissible.

<table><tr><td>1</td><td>$\varphi \Rightarrow \varphi'$</td><td>Hypothesis</td><td>5</td><td>$\varphi' \ast \psi \Rightarrow \psi \ast \varphi'$</td><td>($A_7^*$)</td></tr><tr><td>2</td><td>$\psi \Rightarrow \psi'$</td><td>Hypothesis</td><td>6</td><td>$\psi' \ast \varphi' \Rightarrow \varphi' \ast \psi'$</td><td>($A_7^*$)</td></tr><tr><td>3</td><td>$\varphi \ast \psi \Rightarrow \varphi' \ast \psi$</td><td>*-Intro, 1</td><td>7</td><td>$\varphi \ast \psi \Rightarrow \psi \ast \varphi'$</td><td>$\Rightarrow\text{-Tr}, 3, 5$</td></tr><tr><td>4</td><td>$\psi \ast \varphi' \Rightarrow \psi' \ast \varphi'$</td><td>*-Intro, 2</td><td>8</td><td>$\varphi \ast \psi \Rightarrow \varphi' \ast \psi'$</td><td>$\Rightarrow\text{-Tr}$ twice, 7, 4, 6</td></tr></table>

**Remark 3.3.** Note that an alternative proof of theorem 5 in Figure 2 consists in applying $\Rightarrow\text{-Tr}$ to theorem 2 and $\text{emp} \ast (\text{alloc}(x) \wedge \text{size}=1) \Rightarrow \text{alloc}(x) \wedge \text{size}=1$, which holds by the axioms ($A_{11}^*$) and ($A_7^*$).

**Example 3.4.** In Figure 3, we develop the proof of $\text{emp} \Rightarrow (\text{alloc}(x) \wedge \text{size} = 1 - \ast \text{size} = 1)$ as a more complete example. We use the following theorems and rules:

$$ (\ast\neg\neg\text{-DistrL}) \quad (\varphi \ast \psi) \wedge (\varphi \ast \chi) \Rightarrow (\varphi \ast \psi \wedge \chi) \qquad (\wedge\top\text{IL}) \quad \varphi \Rightarrow \top \wedge \varphi \qquad \wedge\text{-Infl}: \quad \frac{\varphi \Rightarrow \chi}{\varphi \wedge \psi \Rightarrow \chi \wedge \psi} $$

The rightmost axiom and the only rule are derivable by propositional reasoning. We show the admissibility of the axiom $(\ast\neg\neg\text{-DistrL})$.

<table><tr><td>1</td><td>$(\varphi \oplus \neg\psi \vee \neg\chi) \Rightarrow (\varphi \oplus \neg\psi) \vee (\varphi \oplus \neg\chi)$</td><td>($I_{6.3.8}^*$), Lemma 6.3</td></tr><tr><td>2</td><td>$\neg(\varphi \ast \neg(\neg\psi \vee \neg\chi)) \Rightarrow \neg(\varphi \ast \neg\neg\psi) \vee \neg(\varphi \ast \neg\neg\chi)$</td><td>Def. $\oplus$, 1</td></tr><tr><td>3</td><td>$\neg(\varphi \ast \psi \wedge \chi) \Rightarrow \neg(\varphi \ast \psi) \vee \neg(\varphi \ast \chi)$</td><td>Replacement of equivalents, 2</td></tr><tr><td>4</td><td>$(\varphi \ast \psi) \wedge (\varphi \ast \chi) \Rightarrow (\varphi \ast \psi \wedge \chi)$</td><td>PC, 3</td></tr></table>

**Main ingredients of the method.** Before showing completeness of $\mathcal{H}_C(\ast, \neg\neg)$, let us recall the key ingredients of the method we follow, not only to provide a vade mecum for axiomatising other separation logics (which, in the second part of [DLM20], we illustrate on the newly introduced logic $\text{SL}(\ast, \exists:\text{w}\to\to)$), but also to identify the essential features and where variations are still possible. The Hilbert-style axiomatisation of $\text{SL}(\ast, \neg\neg)$ shall culminate with Theorem 6.5 that states the adequateness of the proof system $\mathcal{H}_C(\ast, \neg\neg)$.

In order to axiomatise $\text{SL}(\ast, \neg\neg)$ internally, as already emphasised several times, the core formulae play an essential role. The main properties of these formulae is that their Boolean combinations capture the full logic $\text{SL}(\ast, \neg\neg)$ [Loz04a] and all the core formulae can be expressed in $\text{SL}(\ast, \neg\neg)$. Generally speaking, our axiom system naturally leads to a form
<table><caption>Figure 3: A proof of $\text{emp} \Rightarrow (\text{alloc}(x) \wedge \text{size} = 1 -* \text{size} = 1)$.</caption>
  <tbody>
    <tr>
      <td>1</td>
      <td>T * (alloc(x) ^ size = 1) ⇒ (alloc(x) ^ size = 1) * T</td>
      <td>(A<sub>7</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>2</td>
      <td>alloc(x) ^ size = 1 ⇒ size ≥ 1</td>
      <td>(^Er)</td>
    </tr>
    <tr>
      <td>3</td>
      <td>(alloc(x) ^ size = 1) * T ⇒ size ≥ 1 * T</td>
      <td>*-Intro, 2</td>
    </tr>
    <tr>
      <td>4</td>
      <td>size ≥ 1 * T ⇒ size ≥ 1</td>
      <td>(A<sub>14</sub><sup>*</sup>) (size ≥ 1 <sup>def</sup> = -emp)</td>
    </tr>
    <tr>
      <td>5</td>
      <td>T * (alloc(x) ^ size = 1) ⇒ size ≥ 1</td>
      <td>⇒-Tr twice, 1, 3, 4</td>
    </tr>
    <tr>
      <td>6</td>
      <td>T ⇒ (alloc(x) ^ size = 1 -* size ≥ 1)</td>
      <td>*-Adj, 5</td>
    </tr>
    <tr>
      <td>7</td>
      <td>emp ⇒ (alloc(x) ^ size = 1 -* -size ≥ 2)</td>
      <td>See Example 3.2</td>
    </tr>
    <tr>
      <td>8</td>
      <td>(alloc(x) ^ size = 1 -* -size ≥ 2) ⇒</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>T ^ (alloc(x) ^ size = 1 -* -size ≥ 2)</td>
      <td>(^TIL)</td>
    </tr>
    <tr>
      <td>9</td>
      <td>T ^ (alloc(x) ^ size = 1 -* -size ≥ 2) ⇒</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>((alloc(x) ^ size = 1 -* size ≥ 1) ^</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>(alloc(x) ^ size = 1 -* -size ≥ 2))</td>
      <td>^-InfL, 6</td>
    </tr>
    <tr>
      <td>10</td>
      <td>((alloc(x) ^ size = 1 -* size ≥ 1) ^</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>(alloc(x) ^ size = 1 -* -size ≥ 2)) ⇒</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>(alloc(x) ^ size = 1 -* size = 1)</td>
      <td>(-*^-DistrL) + Def. size</td>
    </tr>
    <tr>
      <td>11</td>
      <td>(alloc(x) ^ size = 1 -* -size ≥ 2) ⇒</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>(alloc(x) ^ size = 1 -* size = 1)</td>
      <td>⇒-Tr twice, 8, 9, 10</td>
    </tr>
    <tr>
      <td>12</td>
      <td>emp ⇒ (alloc(x) ^ size = 1 -* size = 1)</td>
      <td>⇒-Tr, 7, 11</td>
    </tr>
  </tbody>
  <tfoot>
    <tr>
      <td colspan="3">(recall that size = β is a shortcut for size ≥ β ^ -size ≥ β+1)</td>
    </tr>
  </tfoot>
</table>

of constructive completeness, as advocated in [Dou17, Lüc18]: the axiomatisation provides proof-theoretical means to transform any formula into an equivalent Boolean combination of core formulae, and it contains also a part dedicated to the derivation of valid Boolean combinations of core formulae (understood as a syntactical fragment of SL(*, -*)). What is specific to each logic is the design of the set of core formulae and in the case of SL(*, -*), this was already known since [Loz04a].

Derivations in the proof system $\mathcal{H}_C(*, -*)$ shall simulate the bottom-up elimination of separating connectives (see forthcoming Lemmata 5.5 and 6.2) when the arguments are two Boolean combinations of core formulae. To do so, $\mathcal{H}_C(*, -*)$ contains axiom schemas that perform such an elimination in multiple “small-step” derivations, e.g. by deriving a single $\text{alloc}(x)$ predicate from $\text{alloc}(x) * \top$ (with forthcoming intermediate axiom $(I_{12}^*)$). Alternatively, it would have been possible to include “big-step” axiom schemas that, given the two Boolean combinations of core formulae, derive the equivalent formula in one single derivation step (see e.g. [EIP19]). The main difference is that small-step axioms provide a simpler understanding of the key properties of the logic.
<figure><img src="image_4.png" /><figcaption>Figure 4: Proof system $\mathcal{H}_C$ for Boolean combinations of core formulae.</figcaption></figure>

## 4. A SIMPLE CALCULUS FOR THE CORE FORMULAE

To axiomatise $SL(*, *)$, we start by introducing the proof system $\mathcal{H}_C$ dedicated to Boolean combinations of core formulae, see Figure 4. As explained earlier, it also contains the axiom schemata and modus ponens for the propositional calculus. Moreover, the axioms whose name is of the form $A_i^C$ are axioms that remain in the global system for $SL(*, *)$, whereas those named $I_i^C$ are intermediate axioms that are removed when considering the axioms dealing with the separating connectives. As explained before, the intermediate axioms are handy to establish results about the axiomatisation of Boolean combinations of core formulae but are not needed when all the axioms and rules of $\mathcal{H}_C(*, *)$ are considered.

In the axiom $(A_2^C)$, $\varphi[y \leftarrow x]$ stands for the formula obtained from $\varphi$ by replacing with the variable $x$ every occurrence of $y$. Let $(s, h)$ be a memory state. The axioms state that $=$ is an equivalence relation (first two axioms), $h(s(x)) = s(y)$ implies $s(x) \in \text{dom}(h)$ (axiom $(A_3^C)$) and that $h$ is a (partial) function (axiom $(A_4^C)$). Furthermore, there are two intermediate axioms about size formulae: $(I_5^C)$ states that if $\text{dom}(h)$ has at least $\beta+1$ elements, then it has at least $\beta$ elements, whereas $(I_6^C)$ states instead that if there are $\beta$ distinct memory cells corresponding to program variables, then indeed $\text{dom}(h) \ge \beta$. It is easy to check that $\mathcal{H}_C$ is sound (see also Lemma 3.1). In order to establish its completeness with respect to Boolean combinations of core formulae, we first show that $\mathcal{H}_C$ is complete for a subclass of Boolean combinations of core formulae, namely for core types defined below. Then, we show that every formula in $\text{Bool}(|\text{Core}(X, \alpha)|)$ is provably equivalent to a disjunction of core types (Lemma 4.2).

**Introduction to core types.** Let $X \subseteq_{\text{fin}} \text{VAR}$ and $\alpha \in \mathbb{N}^+$. We write $\text{CoreTypes}(X, \alpha)$ to denote the set of core types defined by

$$ \{\varphi \in \text{Conj}(\text{Core}(X, \alpha)) \mid \text{for all } \psi \in \text{Core}(X, \alpha), \{\psi \mid \neg \psi\} \subseteq_{\text{Lt}} \varphi, \text{ and } (\psi \land \neg \psi) \notin_{\text{Lt}} \varphi\}. $$

Note that if $\varphi \in \text{CoreTypes}(X, \alpha)$, then $\varphi$ is a conjunction such that for every $\psi \in \text{Core}(X, \alpha)$, there is exactly one literal in $\varphi$ built upon $\psi$.

**Lemma 4.1 (Refutational completeness).** Let $\varphi \in \text{CoreTypes}(X, \alpha)$, where $\alpha \ge \text{card}(X)$. The formula $\neg \varphi$ is valid if and only if $\vdash_{\mathcal{H}_C} \neg \varphi$.

*Proof.* We show that $\varphi$ is unsatisfiable if and only if $\vdash_{\mathcal{H}_C} \neg \varphi$. The “only if” part follows from the soundness of $\mathcal{H}_C$, so we prove the “if” part. Let $\varphi \in \text{CoreTypes}(X, \alpha)$ be such that $\vdash_{\mathcal{H}_C} \varphi \Rightarrow \bot$, and let us prove that $\varphi$ is satisfiable. By the axioms $(A_1^C)$ and $(A_2^C)$, there is an equivalence relation $\approx$ on $X$ such that $x \approx y$ iff $x = y$ occurs positively in $\varphi$. We write $[x]$ to denote the equivalence class of $x$ with respect to $\approx$. By the axioms $(A_2^C)$ and $(A_4^C)$, there is a partial map $f: (X/\approx) \to (X/\approx)$ on equivalence classes such that $x \to y$ occurs positively iff $f([x])$ is defined and $f([x]) = [y]$. Let $D = \{[x] \mid \text{alloc}(x) \text{ occurs positively in } \varphi\}$. By the axiom $(A_3^C)$, $\text{dom}(f) \subseteq D$. Let $n = \max_{\text{size}}(\varphi)$. We recall that, by definition of $\max_{\text{size}}()$, $n$ is the greatest $\beta$ such that $\text{size} \ge \beta$ occurs positively in $\varphi$ (or zero if there are none).
Let us show that $n \ge \text{card}(D)$. *Ad absurdum*, suppose that $n < \text{card}(D)$. From the axiom $(\mathbf{I}_6^C)$, $\vdash_{\mathcal{H}_C} \varphi \Rightarrow \text{size} \ge \text{card}(D)$ and by definition of $n$ and the fact that $\alpha \ge \text{card}(\mathbf{x}) \ge \text{card}(D)$, $\vdash_{\mathcal{H}_C} \varphi \Rightarrow \text{size} \ge n$ and $\vdash_{\mathcal{H}_C} \varphi \Rightarrow \neg(\text{size} \ge (n+1))$ since both $\text{size} \ge n$ and $(\text{size} \ge (n+1))$ (possibly negated) occur in $\varphi$ as $\alpha \ge \text{card}(\mathbf{x})$. By using the axiom $(\mathbf{I}_5^C)$ and propositional reasoning, we can get that $\vdash_{\mathcal{H}_C} \varphi \Rightarrow \neg(\text{size} \ge \text{card}(D))$ since $\vdash_{\mathcal{H}_C} \varphi \Rightarrow \neg(\text{size} \ge (n+1))$, which leads to a contradiction. Consequently, $n \ge \text{card}(D)$.

Let $\ell_0, \ell_1, \dots, \ell_n \in \text{LOC}$ be $n+1$ distinct locations, and let us fix an enumeration $C_1, \dots, C_{\text{card}(D)}$ on the equivalence classes of $\approx$. Let $(s, h)$ be defined by

* $s(\mathbf{x}) \stackrel{\text{def}}{=} \ell_i$ if $[x]$ is the $i$th equivalence class $C_i$,

* $h(\ell_i) \stackrel{\text{def}}{=} \ell_j$ if $0 < i \le \text{card}(D)$ and the $i$th equivalence class is mapped to the $j$th one by $f$,

* $h(\ell_i) \stackrel{\text{def}}{=} \ell_0$ if either $0 < i \le \text{card}(D)$ and the $i$th equivalence class is not in the domain of $f$, or $i > \text{card}(D)$.

Then, by construction, $(s, h)$ satisfies all positive literals of the form $\mathbf{x} = \mathbf{y}$ or $\mathbf{x} \leftrightarrow \mathbf{y}$ or $\text{alloc}(\mathbf{x})$ that occur positively in $\varphi$, and all negative literals that occur in $\varphi$. It also satisfies $\text{size} \ge n$, falsifies $\text{size} \ge n+1$ (assuming $n+1 \le \alpha$), and by the axiom $(\mathbf{I}_5^C)$, it satisfies all size literals in $\varphi$. $\square$

By classical reasoning, one can show that every $\varphi \in \text{Bool}(\text{Core}(\mathbf{X}, \alpha))$ is provably equivalent to a disjunction of core types. Together with Lemma 4.1, this implies that $\mathcal{H}_C$ is adequate with respect to the propositional logic of core formulae.

To prove forthcoming Theorem 4.3, let us first establish the following simple lemma.

**Lemma 4.2 (Core Types Lemma).** Let $\varphi \in \text{Bool}(\text{Core}(\mathbf{X}, \alpha))$. There is a disjunction $\psi = \psi_1 \lor \dots \lor \psi_n$ with $\psi_i \in \text{CoreTypes}(\mathbf{X}, \max(\text{card}(\mathbf{X}), \alpha))$ for all $i$ such that $\vdash_{\mathcal{H}_C} \varphi \Leftrightarrow \psi$.

*Proof*. Let $\psi_1 \lor \dots \lor \psi_n$ be a formula in disjunctive normal form logically equivalent to $\varphi$. If $\psi_i$ is not a core type in $\text{CoreTypes}(\mathbf{X}, \max(\text{card}(\mathbf{X}), \alpha))$, there is a core formula $\chi \in \text{Core}(\mathbf{X}, \max(\text{card}(\mathbf{X}), \alpha))$ that occurs neither positively nor negatively in $\psi_i$. Replacing $\psi_i$ with $(\psi_i \land \chi) \lor (\psi_i \land \neg\chi)$, and repeating this for all missing core formulae and for all $i$, we obtain a disjunction of core types of the expected form. Since all equivalences follow from pure propositional reasoning, the equivalence between $\varphi$ and the obtained formula can be proved in $\mathcal{H}_C$. $\square$

**Theorem 4.3 (Adequacy).** A Boolean combination of core formulae $\varphi$ is valid iff $\vdash_{\mathcal{H}_C} \varphi$.

*Proof*. Let $\varphi$ be a Boolean combination of core formulae in $\text{CoreTypes}(\mathbf{X}, \alpha)$ for some $\mathbf{X}$ and $\alpha$. As all the axioms are valid (Lemma 3.1), $\vdash_{\mathcal{H}_C} \varphi$ implies that $\varphi$ is valid. Let us assume that $\varphi$ is valid, and let us prove that $\vdash_{\mathcal{H}_C} \varphi$. By Lemma 4.2, there is a disjunction $\psi = \psi_1 \lor \dots \lor \psi_n$ of core types in $\text{CoreTypes}(\mathbf{X}, \max(\text{card}(\mathbf{X}), \alpha))$ such that $\vdash_{\mathcal{H}_C} (\neg\varphi) \Leftrightarrow \psi$. As $\varphi$ is valid, the formulae $\neg\varphi$, $\psi$ and all the $\psi_i$'s are unsatisfiable. By Lemma 4.1, $\vdash_{\mathcal{H}_C} \psi_i \Rightarrow \bot$, for all $i$. By propositional reasoning, $\vdash_{\mathcal{H}_C} \varphi$. $\square$

## 5. AXIOMATISATION FOR SL(*, alloc)

We write $\text{SL}(*, \text{alloc})$ to denote the fragment of $\text{SL}(*, \neg*)$ in which the separating implication is removed at the price of adding the atomic formulae of the form $\text{alloc}(\mathbf{x})$. We define an Hilbert-style axiomatisation for $\text{SL}(*, \text{alloc})$, obtained by enriching $\mathcal{H}_C$ with axioms and one inference rule that handle the separating conjunction *, leading to the proof system $\mathcal{H}_C(*)$.
<figure><img src="image_5.png" /><figcaption>Figure 5: Additional axioms and rule for $\mathcal{H}_C(*)$.</figcaption></figure>

Fundamentally, as we work now within SL(*, alloc), the core formula size ≥ β can be encoded in the logic. According to its definition, given in Section 2.2, we see size ≥ 0 as ⊤, size ≥ 1 as ¬emp and size ≥ β +2 as ¬emp * size ≥ β +1.

The axioms and the rule added to $\mathcal{H}_C$ in order to define $\mathcal{H}_C(*)$ are presented in Figure 5. Their soundness has been proved in Lemma 3.1, with the exception of the three intermediate axioms $(\mathbf{I}_9^*)$, $(\mathbf{I}_{10}^*)$ and $(\mathbf{I}_{12}^*)$, which are used for the completeness of $\mathcal{H}_C(*)$ with respect to SL(*, alloc), but are discharged from the proof system for SL(*, *) (Figure 1), as they become derivable (Lemma 6.1).

**Lemma 5.1.** $\mathcal{H}_C(*)$ is sound.

*Proof.* The axioms $(\mathbf{I}_9^*)$ and $(\mathbf{I}_{10}^*)$ are inherited from Boolean BI (see [BV14] and [GLW06, Section 2]). The soundness of $(\mathbf{I}_{12}^*)$ is straightforward. Indeed, suppose $(s, h) \models \text{alloc}(x)*\top$. So, there is $h' \sqsubseteq h$ such that $(s, h') \models \text{alloc}(x)$. By definition of $\text{alloc}(x)$, $s(x) \in \text{dom}(h')$. By $h' \sqsubseteq h$, $s(x) \in \text{dom}(h)$. We conclude that $(s, h) \models \text{alloc}(x)$. $\square$

Let us look further at the axioms in Figure 5. The axioms deal with the commutative monoid properties of (*, emp) and its distributivity over ∨ (as for Boolean BI, see e.g. [GLW06]). The rule *-Intro, sometimes called “frame rule” by analogy with the rule of the same name in program logic, states that logical equivalence is a congruence for *. $\mathcal{H}_C(*)$ is designed with the idea of being as simple as possible. On one side, this helps understanding the key ingredients of SL(*, alloc). On the other side, this makes the proof of completeness of $\mathcal{H}_C(*)$ more challenging. To work towards this proof while familiarising with the new axioms, we first show a set of intermediate theorems (see Appendix A).

**Lemma 5.2.** The following rules and axioms are admissible in $\mathcal{H}_C(*)$:

$$(\mathbf{I}_{5.2.1}) \quad x \sim y \wedge (\varphi * \psi) \Rightarrow (\varphi \wedge x \sim y) * \psi, \text{ where } \sim \text{ stands for } = \text{ or } \neq.$$

$$(\mathbf{I}_{5.2.2}) \quad x = y \wedge ((\varphi \wedge \text{alloc}(x)) * \psi) \Rightarrow (\varphi \wedge \text{alloc}(y)) * \psi.$$

$$(\mathbf{I}_{5.2.3}) \quad (\varphi \wedge \text{alloc}(x)) * \psi \Rightarrow \varphi * (\psi \wedge \neg \text{alloc}(x)).$$

$$(\mathbf{I}_{5.2.4}) \quad \neg \text{alloc}(x) \wedge (\varphi * \psi) \Rightarrow (\varphi \wedge \neg \text{alloc}(x)) * \psi.$$

$$(\mathbf{I}_{5.2.5}) \quad \text{alloc}(x) \wedge (\varphi * (\neg \text{alloc}(x) \wedge \psi)) \Rightarrow (\varphi \wedge \text{alloc}(x)) * (\neg \text{alloc}(x) \wedge \psi)$$

$$(\mathbf{I}_{5.2.6}) \quad x \leftrightarrow y \wedge ((\varphi \wedge \text{alloc}(x)) * \psi) \Rightarrow (\varphi \wedge x \leftrightarrow y) * \psi.$$

$$(\mathbf{I}_{5.2.7}) \quad \neg x \leftrightarrow y \wedge (\varphi * \psi) \Rightarrow (\varphi \wedge \neg x \leftrightarrow y) * \psi.$$
In $\mathcal{H}_C(*)$, the axioms $(\mathbf{I}_5^C)$ and $(\mathbf{I}_6^C)$ of $\mathcal{H}_C$ are superfluous and can be removed. Indeed, notice that both axioms do not appear in the proof system $\mathcal{H}_C(*, *)$ given in Figure 1.

**Lemma 5.3.** *The axioms $(\mathbf{I}_5^C)$ and $(\mathbf{I}_6^C)$ are derivable in $\mathcal{H}_C(*)$.*

*Validity of $(\mathbf{I}_5^C)$. The proof is by induction on $\beta$.*

**base case:** $\beta = 0$: The instance of the axiom $(\mathbf{I}_5^C)$ with $\beta = 0$ amounts to derive the formula
size $\ge 1 \Rightarrow$ size $\ge 0$. By definition size $\ge 1 = \neg \text{emp}$ and size $\ge 0 = \top$, and therefore,
by propositional reasoning, $\vdash_{\mathcal{H}_C(*)} \text{size} \ge 1 \Rightarrow \text{size} \ge 0$.

**induction step:** $\beta > 0$: By induction hypothesis, assume $\vdash_{\mathcal{H}_C(*)} \text{size} \ge \beta \Rightarrow \text{size} \ge \beta - 1$.
The formula size $\ge \beta + 1 \Rightarrow$ size $\ge \beta$ is derived as follows:

$$
\begin{array}{l@{\quad}l@{\qquad}l}
1 & \mathbf{size} \ge \beta \Rightarrow \mathbf{size} \ge \beta - 1 & \text{Induction hypothesis} \\
2 & (\mathbf{size} \ge \beta) * \neg \text{emp} \Rightarrow (\mathbf{size} \ge \beta - 1) * \neg \text{emp} & \text{-Intro, 1} \\
3 & \mathbf{size} \ge \beta + 1 \Rightarrow \mathbf{size} \ge \beta & \text{2, def. of size } \Box
\end{array}
$$

Before proving the validity of $(\mathbf{I}_6^C)$, we derive the intermediate theorem below. Let $X \subseteq_{\text{fin}} \text{VAR}$.

$$(\mathbf{I}_{5.3.1}^*) \bigwedge_{x \in X} (\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \Rightarrow (*(x \in X)(\text{alloc}(x) \wedge \text{size} = 1)) * \top.$$

*Validity of $(\mathbf{I}_{5.3.1}^*)$. The proof is by induction on the size of X. We distinguish two base cases, for $\text{card}(X) = 1$ and $\text{card}(X) = 0$.

**base case:** $\text{card}(X) = 1$: In this case, $(\mathbf{I}_{5.3.1}^*)$ is exactly $(\mathbf{A}_{17}^*)$.

**base case:** $\text{card}(X) = 0$: In this case, $(\mathbf{I}_{5.3.1}^*)$ is $\top \Rightarrow \top * \top$.

$$
\begin{array}{l@{\quad}l@{\qquad}l}
1 & \text{emp} \Rightarrow \top & \text{PC} \\
2 & \top \Rightarrow \top * \text{emp} & (\mathbf{A}_{11}^*) \\
3 & \top * \text{emp} \Rightarrow \text{emp} * \top & (\mathbf{A}_7^*) \\
4 & \text{emp} * \top \Rightarrow \top * \top & \text{-Intro, 1} \\
5 & \top \Rightarrow \top * \top & \Rightarrow \text{-Tr, 2, 3, 4}
\end{array}
$$

**induction step:** $\text{card}(X) \ge 2$: Let $z \in X$. By induction hypothesis,

$$\vdash_{\mathcal{H}_C(*)} \bigwedge_{u \in X \setminus \{z\}} (\text{alloc}(u) \wedge \bigwedge_{v \in X \setminus \{u,z\}} u \neq v) \Rightarrow (*(u \in X \setminus \{z\}) (\text{alloc}(u) \wedge \text{size} = 1)) * \top.$$

We write $\chi$ for the premise $\bigwedge_{u \in X \setminus \{z\}} (\text{alloc}(u) \wedge \bigwedge_{v \in X \setminus \{u,z\}} u \neq v)$ above. Below, we aim for a proof of

$$\vdash_{\mathcal{H}_C(*)} \bigwedge_{x \in X} (\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \Rightarrow (\text{alloc}(z) \wedge \text{size} = 1) * \chi.$$

In this way, the provability of $(\mathbf{I}_{5.3.1}^*)$ follows directly by induction hypothesis together with $(\mathbf{A}_7^*)$ and \*-Intro. We have

$$
\begin{array}{l@{\quad}l@{\qquad}l}
1 & \bigwedge_{x \in X} (\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \Rightarrow (\text{alloc}(z) \wedge \text{size} = 1) * \top & (\mathbf{A}_{17}^*) \text{ and PC} \\
2 & \top \Rightarrow \chi \lor \neg \chi & \text{PC} \\
3 & (\text{alloc}(z) \wedge \text{size} = 1) * \top \Rightarrow (\text{alloc}(z) \wedge \text{size} = 1) * (\chi \lor \neg \chi) & \text{-Intro, } (\mathbf{A}_7^*), 2 \\
4 & (\text{alloc}(z) \wedge \text{size} = 1) * (\chi \lor \neg \chi) \Rightarrow &
\end{array}
$$
$$5 \quad \left| \begin{array}{l} ((\text{alloc}(z) \wedge \text{size} = 1) * \chi) \vee ((\text{alloc}(z) \wedge \text{size} = 1) * \neg \chi) \quad (\mathbf{A}_7^*) \text{ and } (\mathbf{I}_9^*) \\ \bigwedge_{x \in X}(\text{alloc}(x) \wedge \bigwedge_{y \in X\setminus\{x\}} x \neq y) \Rightarrow \\ ((\text{alloc}(z) \wedge \text{size} = 1) * \chi) \vee ((\text{alloc}(z) \wedge \text{size} = 1) * \neg \chi) \quad \Rightarrow \text{-Tr} 1, 3, 4 \end{array} \right. $$

By propositional reasoning, $\neg \chi$ is equivalent to $\bigvee_{u \in X \setminus \{z\}} (\neg \text{alloc}(u) \vee \bigvee_{v \in X \setminus \{u, z\}} u = v)$. Due to the complexity of this formula, we proceed now rather informally, but our arguments entail the existence of a proper derivation. We aim at showing that

$$ \vdash_{\mathcal{H}_C(*)} \bigwedge_{x \in X} (\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \wedge ((\text{alloc}(z) \wedge \text{size} = 1) * \neg \chi) \Rightarrow \bot . \quad (\dagger) $$

By propositional calculus and $(\mathbf{I}_9^*)$, we can distribute conjunctions and separating conjunctions over disjunctions. We derive:

$$ \vdash_{\mathcal{H}_C(*)} \bigwedge_{x \in X} (\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \wedge ((\text{alloc}(z) \wedge \text{size} = 1) * \neg \chi) \Rightarrow \gamma' \vee \gamma'', $$

where $\gamma'$ and $\gamma''$ are defined, respectively, as

$$ \begin{aligned} & \bigvee_{u \in X \setminus \{z\}} \left( \bigwedge_{x \in X}(\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \wedge ((\text{alloc}(z) \wedge \text{size} = 1) * \neg \text{alloc}(u)) \right), \\ & \bigvee_{v \in X \setminus \{z, u\}} \left( \bigwedge_{x \in X}(\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \wedge ((\text{alloc}(z) \wedge \text{size} = 1) * u = v) \right). \end{aligned} $$

In order to deduce (†) it is sufficient to prove, in $\mathcal{H}_C(*)$, that every disjunct of $\gamma'$ and $\gamma''$ implies $\bot$. Clearly, if $\gamma'$ and $\gamma''$ do not have any disjunct, i.e. when $X \setminus \{z\}$ is empty, then the formula is propositionally equivalent to $\bot$, which allows us to conclude (†). Otherwise, let us consider each disjunct in $\gamma'$ and $\gamma''$ (separately), and prove their inconsistency.

**case:** $\gamma'$: Let $u \in X \setminus \{z\}$. We show the inconsistency of

$$ \bar{\gamma} \stackrel{\text{def}}{=} \bigwedge_{x \in X} (\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \wedge ((\text{alloc}(z) \wedge \text{size} = 1) * \neg \text{alloc}(u)). $$

$$ \begin{array}{l@{\quad}l@{\quad}l} 6 & \bigwedge_{x \in X} (\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \Rightarrow \text{alloc}(u) \wedge u \neq z & \text{PC} \\ 7 & \bar{\gamma} \Rightarrow \text{alloc}(u) \wedge u \neq z \wedge ((\text{alloc}(z) \wedge \text{size} = 1) * \neg \text{alloc}(u)) & \text{PC} \\ 8 & \text{alloc}(u) \wedge ((\text{alloc}(z) \wedge \text{size} = 1) * \neg \text{alloc}(u)) \Rightarrow \\ & \qquad ((\text{alloc}(z) \wedge \text{size} = 1 \wedge \text{alloc}(u)) * \neg \text{alloc}(u)) & (\mathbf{I}_{5.2.5}^*) \\ 9 & u \neq z \wedge ((\text{alloc}(z) \wedge \text{size} = 1 \wedge \text{alloc}(u)) * \neg \text{alloc}(u)) \Rightarrow \\ & \qquad ((\text{alloc}(z) \wedge \text{size} = 1 \wedge \text{alloc}(u) \wedge u \neq z) * \neg \text{alloc}(u)) & (\mathbf{I}_{5.2.1}^*) \\ 10 & \text{alloc}(z) \wedge \text{alloc}(u) \wedge u \neq z \Rightarrow \text{size} \ge 2 & (\mathbf{A}_{20}^*) \\ 11 & \text{size} = 1 \Rightarrow \neg \text{size} \ge 2 & \text{PC} \\ 12 & \text{alloc}(z) \wedge \text{size} = 1 \wedge \text{alloc}(u) \wedge u \neq z \Rightarrow \bot & \Rightarrow \text{-Tr}, \text{PC}, 10, 11 \\ 13 & \bar{\gamma} \Rightarrow (\text{alloc}(z) \wedge \text{size} = 1 \wedge \text{alloc}(u) \wedge u \neq z) * \neg \text{alloc}(u) & \text{PC}, 7, 8, 9 \\ 14 & (\text{alloc}(z) \wedge \text{size} = 1 \wedge \text{alloc}(u) \wedge u \neq z) * \neg \text{alloc}(u) \Rightarrow \bot * \neg \text{alloc}(u) & \text{-Intro}, 12 \\ 15 & \bot * \neg \text{alloc}(u) \Rightarrow \bot & (\mathbf{I}_{10}^*), 14 \\ 16 & \bar{\gamma} \Rightarrow \bot & \text{PC}, 13, 15 \end{array} $$

Since $\bar{\gamma}$ is an arbitrary disjunct appearing in $\gamma'$, we conclude that $\vdash_{\mathcal{H}_C(*)} \gamma' \Rightarrow \bot$.
**case:** $\gamma''$: Let $u \in X \setminus \{z\}$ and $v \in X \setminus \{z, u\}$. Notice that if $u$ or $v$ do not exist, then $\gamma''$ is defined as $\perp$ and so the proof is complete. Otherwise, we show the inconsistency of

$$ \hat{\gamma} \stackrel{\text{def}}{=} \bigwedge_{x \in X}(\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \wedge ((\text{alloc}(z) \wedge \text{size} = 1) * u = v). $$

<table>
  <tbody>
    <tr>
      <td>17</td>
      <td>$$ \bigwedge_{x \in X}(\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \Rightarrow u \neq v $$</td>
      <td>PC</td>
    </tr>
    <tr>
      <td>18</td>
      <td>$$ \text{alloc}(z) \wedge \text{size} = 1 \Rightarrow \top $$</td>
      <td>PC</td>
    </tr>
    <tr>
      <td>19</td>
      <td>$$ (\text{alloc}(z) \wedge \text{size} = 1) * u = v \Rightarrow u = v * \top $$</td>
      <td><b>*-Intro</b>, 18, (<b>A</b><sub>7</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>20</td>
      <td>$$ u = v * \top \Rightarrow u = v $$</td>
      <td>(<b>A</b><sub>14</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>21</td>
      <td>$$ ((\text{alloc}(z) \wedge \text{size} = 1) * u = v) \Rightarrow u = v $$</td>
      <td>⇒ <b>-Tr</b>, 19, 20</td>
    </tr>
    <tr>
      <td>22</td>
      <td>$$ \hat{\gamma} \Rightarrow \bot $$</td>
      <td>PC, 17, 21</td>
    </tr>
  </tbody>
</table>

Since $\hat{\gamma}$ is an arbitrary disjunct appearing in $\gamma''$, we conclude that $\vdash_{\mathcal{H}_C(*)} \gamma'' \Rightarrow \bot$.

From $\vdash_{\mathcal{H}_C(*)} \gamma' \Rightarrow \bot$ and $\vdash_{\mathcal{H}_C(*)} \gamma'' \Rightarrow \bot$ we conclude that (†) holds. From the theorem 5 derived in this proof, this allows us to conclude that

$$ \vdash_{\mathcal{H}_C(*)} \bigwedge_{x \in X}(\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \Rightarrow (\text{alloc}(z) \wedge \text{size} = 1) * \chi, $$

which concludes the proof, as explained at the beginning of the induction step. □

We complete the proof of Lemma 5.3 by showing a derivation of (<b>I</b><sub>6</sub><sup>C</sup>).

*Validity of (<b>I</b><sub>6</sub><sup>C</sup>).* Let $X \subseteq_{\text{fin}} \text{VAR}$. If $X = \emptyset$, then the instance of the axiom (<b>I</b><sub>6</sub><sup>C</sup>) becomes $\top \Rightarrow \text{size} \geq 0$, which, by definition of size $\geq 0$, is syntactically equivalent to $\top \Rightarrow \top$ and hence valid by propositional reasoning. Below, assume $X \neq \emptyset$ and fix $z \in X$.

<table>
  <tbody>
    <tr>
      <td>1</td>
      <td>$$ \bigwedge_{x \in X}(\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \Rightarrow (*_{x \in X}(\text{alloc}(x) \wedge \text{size} = 1)) * \top $$</td>
      <td>(<b>I</b><sub>5.3.1</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>2</td>
      <td>$$ \text{alloc}(x) \wedge \text{size} = 1 \Rightarrow \text{size} \geq 1 $$</td>
      <td>PC, def. of size = 1</td>
    </tr>
    <tr>
      <td>3</td>
      <td>$$ (*_{x \in X}(\text{alloc}(x) \wedge \text{size} = 1)) * \top \Rightarrow (*_{x \in X}(\text{size} \geq 1) * \top) $$</td>
      <td>multiple applications of <b>*-Intro</b>, 2, (<b>A</b><sub>7</sub><sup>*</sup>) and <b>⇒-Tr</b></td>
    </tr>
    <tr>
      <td>4</td>
      <td>$$ (*_{x \in X}(\text{size} \geq 1) * \top \Rightarrow (\text{size} \geq 1 * \top) * (*_{x \in X \setminus \{z\}}(\text{size} \geq 1)) $$</td>
      <td>(<b>A</b><sub>7</sub><sup>*</sup>), (<b>A</b><sub>8</sub><sup>*</sup>), def. of z</td>
    </tr>
    <tr>
      <td>5</td>
      <td>$$ \text{size} \geq 1 * \top \Rightarrow \text{size} \geq 1 $$</td>
      <td>(<b>A</b><sub>14</sub><sup>*</sup>), def. of size $\geq 1$</td>
    </tr>
    <tr>
      <td>6</td>
      <td>$$ (\text{size} \geq 1 * \top) * (*_{x \in X \setminus \{z\}}(\text{size} \geq 1)) \Rightarrow (*_{x \in X}(\text{size} \geq 1)) $$</td>
      <td><b>*-Intro</b></td>
    </tr>
    <tr>
      <td>7</td>
      <td>$$ (*_{x \in X}(\text{size} \geq 1) \Rightarrow \text{size} \geq \text{card}(X)) $$</td>
      <td>(<b>A</b><sub>8</sub><sup>*</sup>), def. of size $\geq \text{card}(X)$</td>
    </tr>
    <tr>
      <td>8</td>
      <td>$$ \bigwedge_{x \in X}(\text{alloc}(x) \wedge \bigwedge_{y \in X \setminus \{x\}} x \neq y) \Rightarrow \text{size} \geq \text{card}(X) $$</td>
      <td>⇒ <b>-Tr</b>, 1, 3, 4, 6, 7</td>
    </tr>
  </tbody>
</table>

From now on, we understand $\mathcal{H}_C(*)$ as the proof system obtained from $\mathcal{H}_C$ by adding all schemata from Figure 5 but by removing (<b>I</b><sub>5</sub><sup>C</sup>) and (<b>I</b><sub>6</sub><sup>C</sup>). We show that $\mathcal{H}_C(*)$ enjoys the $*$ elimination property when the argument formulae are core types. That is, given two satisfiable core types $\varphi$ and $\psi$, in CoreTypes($X$, $\alpha$), we show that the formula $\varphi * \psi$ is provably equivalent to the formula $\langle * \rangle(\varphi, \psi)$ in Conj(Core($X$, $2\alpha$)), defined in Figure 6.
<figure><img src="image_6.png" /><figcaption>Figure 6: The formula $\langle * \rangle(\varphi, \psi)$.</figcaption></figure>

**Lemma 5.4.** Let $X \subseteq_{\text{fin}} \text{VAR}$ and $\alpha \ge \text{card}(X)$. If $\varphi$ and $\psi$ are two satisfiable core types in $\text{CoreTypes}(X, \alpha)$, then $\vdash_{\mathcal{H}_C(*)} \varphi * \psi \Leftrightarrow \langle * \rangle(\varphi, \psi)$.

The equivalence $\varphi * \psi \Leftrightarrow \langle * \rangle(\varphi, \psi)$ is reminiscent to the one in [EIP19, Lemma 3] that is proved semantically. In a way, because $\mathcal{H}_C(*)$ will reveal to be complete, the restriction of [EIP19, Lemma 3] to $\text{SL}(*, \text{alloc})$ can be replayed completely syntactically within $\mathcal{H}_C(*)$.

*Structure of the proof of Lemma 5.4.* Before presenting the technical developments, let us explain the structure of the whole proof of Lemma 5.4, which might help to follow the different steps. In order to show that $\vdash_{\mathcal{H}_C(*)} \varphi * \psi \Leftrightarrow \langle * \rangle(\varphi, \psi)$, we start showing that $\vdash_{\mathcal{H}_C(*)} \varphi * \psi \Rightarrow \langle * \rangle(\varphi, \psi)$. This can be done rather mechanically since for every literal $L$ of $\langle * \rangle(\varphi, \psi)$, one can construct a derivation for $\vdash_{\mathcal{H}_C(*)} \varphi * \psi \Rightarrow L$. The main difficulty in the proof rests on showing that $\vdash_{\mathcal{H}_C(*)} \langle * \rangle(\varphi, \psi) \Rightarrow \varphi * \psi$. To do so, we build a sequence of formulae $\varphi^{(1)} * \psi^{(1)}$, $\varphi^{(2)} * \psi^{(2)}$, ..., $\varphi^{(k)} * \psi^{(k)}$ satisfying the following conditions:

* for all $i \in [1, k]$, $\vdash_{\mathcal{H}_C(*)} \langle * \rangle(\varphi, \psi) \Rightarrow \varphi^{(i)} * \psi^{(i)}$, the formulae $\varphi^{(i)}$ and $\psi^{(i)}$ are conjunctions of core formulae, and

* for all $j \in [1, i]$, $\varphi^{(j)} \subseteq_{\text{Lt}} \varphi^{(i)}$ and $\psi^{(j)} \subseteq_{\text{Lt}} \psi^{(i)}$.

* $\varphi = \varphi^{(k)}$ and $\psi = \psi^{(k)}$ (modulo associativity/commutativity of the classical conjunction). In order to build $\varphi^{i+1}$ (resp. $\psi^{i+1}$), we identify a literal $L$ in $\varphi$ (resp. in $\psi$) that does not occur yet in $\varphi^i$ and we show that $\vdash_{\mathcal{H}_C(*)} \langle * \rangle(\varphi, \psi) \Rightarrow \varphi^{(i+1)} * \psi^{(i+1)}$ with $\varphi^{i+1} \stackrel{\text{def}}{=} \varphi^{(i)} \wedge L$ (resp. $\psi^{(i+1)} \stackrel{\text{def}}{=} \psi^{(i)} \wedge L$) and $\varphi^{(i+1)} \stackrel{\text{def}}{=} \psi^{(i)}$ (resp. $\varphi^{(i+1)} \stackrel{\text{def}}{=} \varphi^{(i)}$). The case analysis on the shape of the literal $L$ is rather mechanical but it remains to specify how the first formulae $\varphi^{(1)}$ and $\psi^{(1)}$ are designed. In short, $\varphi^{(1)}$ (resp. $\psi^{(1)}$) is dedicated to the part of $\varphi$ (resp. $\psi$) related to the size of the heap domain and to the allocated variables. Details will follow.

To construct these above-mentioned derivations, some additional derivations are instru-
mental in particular to establish that the formulae below are derivable in $\mathcal{H}_C(*)$:

$$
\mathbf{size} \ge \beta_1 + \beta_2 \Rightarrow \mathbf{size} = \beta_1 * \mathbf{size} \ge \beta_2, \quad \mathbf{size} = \beta_1 + \beta_2 \Rightarrow \mathbf{size} = \beta_1 * \mathbf{size} = \beta_2.
$$

Such derivations can be found in Appendix B. We now develop the proof of Lemma 5.4.

*Proof of Lemma 5.4.* First of all, let us briefly explain what is the rationale for having literals of the form $x \neq x$ in the definition of $\langle * \rangle(\varphi, \psi)$. Recall that $\text{alloc}(x) \subseteq_{\text{Lt}} \{\varphi; \psi\}$ is a shortcut to state that $\text{alloc}(x)$ occurs in both the core types $\varphi$ and $\psi$. Since $(\text{alloc}(x) \wedge \varphi') * (\text{alloc}(x) \wedge \psi')$ is unsatisfiable, $\text{alloc}(x) \subseteq_{\text{Lt}} \{\varphi; \psi\}$ entails that $\langle * \rangle(\varphi, \psi)$ should be unsatisfiable. That is why, if $\text{alloc}(x) \subseteq_{\text{Lt}} \{\varphi; \psi\}$, then $x \neq x$ is part of $\langle * \rangle(\varphi, \psi)$.
(⇒): Let us show that $\vdash_{\mathcal{H}_C(*)} \varphi * \psi \Rightarrow \langle * \rangle(\varphi, \psi)$. We establish that $\vdash_{\mathcal{H}_C(*)} \varphi * \psi \Rightarrow L$ holds for every literal $L$ of $\langle * \rangle(\varphi, \psi)$. We reason by a case analysis on $L \subseteq_{\mathrm{Lt}} \langle * \rangle(\varphi, \psi)$.

**case: $L$ is an (in)equality or $L = x \leftrightarrow y$:** For all the equalities and inequalities in $\varphi$ or $\psi$, as well as all the literals of the form $x \leftrightarrow y$, $\vdash_{\mathcal{H}_C(*)} \varphi * \psi \Rightarrow L$ follows from the rule *-Intro and the axiom ($A_{14}^*$). Let us provide below the proper derivation when $L$ is a literal in $\varphi$ that is an equality, an inequality or of the form $x \leftrightarrow y$.

$$ \begin{array}{lclcl} 1 & \varphi \Rightarrow L & & \mathrm{PC} & 4 \\ 2 & \psi \Rightarrow \top & & \mathrm{PC} & 5 \\ 3 & \varphi * \psi \Rightarrow L * \top & & \mathrm{-Ilr}, 1, 2 & \end{array} \qquad \begin{array}{l} L * \top \Rightarrow L \\ \varphi * \psi \Rightarrow L \end{array} \qquad \begin{array}{l} (A_{14}^*) \\ \Rightarrow \mathrm{-Tr}, 3, 4 \end{array} $$

Assume there is a literal $x \neq x$ that occurs in $\langle * \rangle(\varphi, \psi)$. As both $\varphi$ and $\psi$ are satisfiable, and thanks to ($A_{1}^{C}$), this is necessarily due to $\mathrm{alloc}(x)$ occurring both in $\varphi$ and $\psi$.

$$ \begin{array}{lclcl} 1 & \varphi \Rightarrow \mathrm{alloc}(x) & & \mathrm{PC} & 4 \\ 2 & \psi \Rightarrow \mathrm{alloc}(x) & & \mathrm{PC} & 5 \\ 3 & \varphi * \psi \Rightarrow \mathrm{alloc}(x) * \mathrm{alloc}(x) & & \mathrm{-Ilr}, 1, 2 & 6 \end{array} \qquad \begin{array}{l} \mathrm{alloc}(x) * \mathrm{alloc}(x) \Rightarrow \bot \\ \bot \Rightarrow x \neq x \\ \varphi * \psi \Rightarrow x \neq x \end{array} \qquad \begin{array}{l} (A_{13}^*) \\ \mathrm{PC} \\ \Rightarrow \mathrm{-Tr}, 4, 5 \end{array} $$

**case: $L = \mathrm{alloc}(x)$:** Follows from ($I_{12}^*$) and *-Intro.

**case: $L = \neg \mathrm{alloc}(x)$:** Follows from ($A_{15}^*$) and *-Intro.

**case: $L = \neg x \leftrightarrow y$:** Let $\neg x \leftrightarrow y$ be a literal occurring in $\langle * \rangle(\varphi, \psi)$. So, $\mathrm{alloc}(x) \wedge \neg x \leftrightarrow y$ occurs in $\varphi$ or $\psi$, say in $\varphi$ (the other case is equivalent, due to ($A_{7}^*$)).

$$ \begin{array}{lclcl} 1 & \varphi \Rightarrow \mathrm{alloc}(x) \wedge \neg x \leftrightarrow y & & \mathrm{PC} & \\ 2 & \psi \Rightarrow \top & & \mathrm{PC} & \\ 3 & \varphi * \psi \Rightarrow (\mathrm{alloc}(x) \wedge \neg x \leftrightarrow y) * \top & & \mathrm{-Ilr}, 1, 2 & \\ 4 & (\mathrm{alloc}(x) \wedge \neg x \leftrightarrow y) * \top \Rightarrow \neg x \leftrightarrow y & & (A_{16}^*) & \\ 5 & \varphi * \psi \Rightarrow \neg x \leftrightarrow y & & \Rightarrow \mathrm{-Tr}, 3, 4 & \end{array} $$

**case : $L = \mathrm{size} \geq \beta_1 + \beta_2$, where $\mathrm{size} \geq \beta_1 \subseteq_{\mathrm{Lt}} \varphi$ and $\mathrm{size} \geq \beta_2 \subseteq_{\mathrm{Lt}} \psi$:**

$$ \begin{array}{lclcl} 1 & \varphi \Rightarrow \mathrm{size} \geq \beta_1 & & \mathrm{PC} & 3 \\ 2 & \psi \Rightarrow \mathrm{size} \geq \beta_2 & & \mathrm{PC} & 4 \\ 3 & \varphi * \psi \Rightarrow \mathrm{size} \geq \beta_1 * \mathrm{size} \geq \beta_2 & & \mathrm{-Ilr}, 1, 2 & \\ 4 & \varphi * \psi \Rightarrow \mathrm{size} \geq (\beta_1 + \beta_2) & & \mathrm{Def. size} & \end{array} $$

Notice that, as $\varphi$ and $\psi$ are satisfiable core types, $\mathrm{size} \geq 0$ appears positively in both these formulae, and thus appears in $\langle * \rangle(\varphi, \psi)$.

**case: $L = \neg \mathrm{size} \geq \beta_1 + \beta_2 \div 1$, where $\neg \mathrm{size} \geq \beta_1 \subseteq_{\mathrm{Lt}} \varphi$ and $\neg \mathrm{size} \geq \beta_2 \subseteq_{\mathrm{Lt}} \psi$:**

$$ \begin{array}{lclcl} 1 & \varphi \Rightarrow \neg \mathrm{size} \geq \beta_1 & & \mathrm{PC} & \\ 2 & \psi \Rightarrow \neg \mathrm{size} \geq \beta_2 & & \mathrm{PC} & \\ 3 & \varphi * \psi \Rightarrow \neg \mathrm{size} \geq \beta_1 * \neg \mathrm{size} \geq \beta_2 & & \mathrm{-Ilr}, 1, 2 & \\ 4 & \neg \mathrm{size} \geq \beta_1 * \neg \mathrm{size} \geq \beta_2 \Rightarrow \neg \mathrm{size} \geq \beta_1 + \beta_2 \div 1 & & (A_{19}^*) & \\ 5 & \varphi * \psi \Rightarrow \neg \mathrm{size} \geq \beta_1 + \beta_2 \div 1 & & \Rightarrow \mathrm{-Tr}, 3, 4 & \end{array} $$
(: Let us show that ⊢<sub>H<sub>C</sub>(*)</sub> <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) ⇒ <sub>ϕ</sub> * <sub>ψ</sub>. If <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) is unsatisfiable, then by completeness of <sub>H<sub>C</sub></sub> (Theorem 4.3), ⊢<sub>H<sub>C</sub></sub> <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) ⇒ ⊥, and thus ⊢<sub>H<sub>C</sub></sub> <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) ⇒ <sub>ϕ</sub> * <sub>ψ</sub>. Since <sub>H<sub>C</sub></sub>(* ) includes <sub>H<sub>C</sub></sub>, we conclude that ⊢<sub>H<sub>C</sub>(*)</sub> <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) ⇒ <sub>ϕ</sub> * <sub>ψ</sub>. Otherwise, below, we assume <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) to be satisfiable. In particular, this implies that no literals of the form <sub>x</sub> ≠ <sub>x</sub> or ¬<sub>size</sub> ≥ 0 appear in <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>). Moreover, by definition of <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>), this implies that <sub>ϕ</sub>, <sub>ψ</sub> and <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) agree on the satisfaction of the core formulae <sub>x</sub> = <sub>y</sub>, i.e. <sub>ϕ</sub>, <sub>ψ</sub> and <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) contain exactly the same (in)equalities. Since <sub>ϕ</sub> is satisfiable, these equalities define an equivalence relation. Let <sub>x<sub>1</sub></sub>, ..., <sub>x<sub>n</sub></sub> be a maximal enumeration of representatives of the equivalence classes (one per equivalence class) such that alloc(<sub>x<sub>i</sub></sub>) occurs in <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>). As it is maximal, for every alloc(<sub>x</sub>) ⊆<sub>LT</sub> <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) there is <sub>i</sub> ∈ [1, n] such that <sub>x<sub>i</sub></sub> is syntactically equal to <sub>x</sub>. Consequently, from the definition of <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>), if alloc(<sub>x</sub>) occurs in <sub>ϕ</sub> or in <sub>ψ</sub>, then there is some <sub>x<sub>i</sub></sub> such that <sub>x</sub> = <sub>x<sub>i</sub></sub> occurs in <sub>ϕ</sub> (and therefore also in <sub>ψ</sub> and in <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>)). Let us define the formula Alloc below:

$$
Alloc \stackrel{\text{def}}{=} (\text{alloc}(x_1) \wedge \text{size} = 1) * \dots * (\text{alloc}(x_n) \wedge \text{size} = 1).
$$

We have,

$$
\begin{array}{l@{\qquad}l@{\qquad}l}
1 & \langle\ast\rangle(\varphi, \psi) \Rightarrow \bigwedge_{i \in [1,n]} (\mathrm{alloc}(x_i) \wedge \bigwedge_{j \in [1,n]} \{i\} x_i \neq x_j) & \mathrm{PC, def. of } x_1, \dots, x_n \\
2 & \bigwedge_{i \in [1,n]} (\mathrm{alloc}(x_i) \wedge \bigwedge_{j \in [1,n]} \{i\} x_i \neq x_j) \Rightarrow \mathrm{Alloc} * \top & (\mathbf{I}_{5.3.1}^*) \\
3 & \langle\ast\rangle(\varphi, \psi) \Rightarrow \mathrm{Alloc} * \top & \Rightarrow \mathrm{-Tr}, 1, 2
\end{array}
$$

Moreover, we show that ⊢<sub>H<sub>C</sub>(*)</sub> Alloc ⇒ size ≥ n and ⊢<sub>H<sub>C</sub>(*)</sub> Alloc ⇒ ¬size ≥ n + 1 (theorems 4 and 7 below), and so ⊢<sub>H<sub>C</sub>(*)</sub> Alloc ⇒ size = n.

$$
\begin{array}{l@{\qquad}l}
1 & \chi \wedge \mathit{size} = 1 \Rightarrow \mathit{size} \ge 1 & \mathit{PC, def. of size} = 1 \\
2 & \chi \wedge \mathit{size} = 1 \Rightarrow \neg \mathit{size} \ge 2 & \mathit{PC, def. of size} = 1 \\
3 & \mathit{Alloc} \Rightarrow *_{i \in [1,n]} \mathit{size} \ge 1 & \text{multiple applications of} \\
& & \quad \text{\textbf{-Intro}, 1, } (\mathbf{A}_7^*) \text{ and } \Rightarrow\textbf{-Tr} \\
4 & \mathit{Alloc} \Rightarrow \mathit{size} \ge n & 3, \text{def. of } \mathit{size} \ge n \\
5 & \mathit{Alloc} \Rightarrow *_{i \in [1,n]} \neg \mathit{size} \ge 2 & \text{multiple applications of} \\
& & \quad \text{\textbf{-Intro}, 2, } (\mathbf{A}_7^*) \text{ and } \Rightarrow\textbf{-Tr} \\
6 & *_{i \in [1,n]} \neg \mathit{size} \ge 2 \Rightarrow \neg \mathit{size} \ge n + 1 & n \text{ applications of } (\mathbf{A}_{19}^*) \text{ and } \textbf{-Intro} \\
7 & \mathit{Alloc} \Rightarrow \neg \mathit{size} \ge n + 1 & \Rightarrow\textbf{-Tr}, 5, 6 \\
8 & \mathit{Alloc} \Rightarrow \mathit{size} = n & \mathit{PC}, 4, 7, \text{def. of } \mathit{size} = n
\end{array}
$$

After deriving ⊢<sub>H<sub>C</sub>(*)</sub> <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) ⇒ Alloc * ⊤ and ⊢<sub>H<sub>C</sub>(*)</sub> Alloc ⇒ size = n, the proof is divided in three steps: (1) we isolate the allocated cells and the garbage, (2) we distribute the alloc and size literals according to the goal <sub>ϕ</sub> * <sub>ψ</sub> and (3) we add the missing literals.

**Step 1, isolating allocated cells and garbage.** Since <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>) is a conjunction of literals built from core formulae, we can rely on max<sub>size</sub>(<sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>)), i.e. the maximum <sub>β</sub> among the formulae <sub>size</sub> ≥ <sub>β</sub> appearing positively in <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>). First, we show some important properties of <sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>), related to max<sub>size</sub>(<sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>)).

A. max<sub>size</sub>(<sup>*</sup>(<sub>ϕ</sub>, <sub>ψ</sub>)) = max<sub>size</sub>(<sub>ϕ</sub>) + max<sub>size</sub>(<sub>ψ</sub>),
B. If there is $\beta \in \mathbb{N}$ such that $\neg size \geq \beta \subseteq_{Lt} <^*>(\varphi, \psi)$, then

$$ \neg size \geq \max_{size}(\varphi) + 1 \subseteq_{Lt} \varphi, \quad \neg size \geq \max_{size}(\psi) + 1 \subseteq_{Lt} \psi. $$

C. If there is $\beta \in \mathbb{N}$ such that $\neg size \geq \beta \subseteq_{Lt} <^*>(\varphi, \psi)$, then

$$ \neg size \geq \max_{size}(<^*>(\varphi, \psi)) + 1 \subseteq_{Lt} <^*>(\varphi, \psi). $$

*Proof of (A).* By definition of $\max_{size}(.)$, we know that $size \geq \max_{size}(\varphi) \subseteq_{Lt} \varphi$ and $size \geq \max_{size}(\psi) \subseteq_{Lt} \psi$. By definition of $<^*>(\varphi, \psi)$, $size \geq \max_{size}(\varphi) + \max_{size}(\psi) \subseteq_{Lt} <^*>(\varphi, \psi)$. *Ad absurdum*, suppose that $\max_{size}(\varphi) + \max_{size}(\psi) \neq \max_{size}(<^*>(\varphi, \psi))$ and thus, by definition of $\max_{size}(.)$, there is $\beta > \max_{size}(\varphi) + \max_{size}(\psi)$ such that $size \geq \beta \subseteq_{Lt} <^*>(\varphi, \psi)$. By definition of $<^*>(\varphi, \psi)$, we conclude that there are $\beta_1$ and $\beta_2$ such that $\beta_1 + \beta_2 = \beta$, $size \geq \beta_1 \subseteq_{Lt} \varphi$ and $size \geq \beta_2 \subseteq_{Lt} \psi$. As $\beta_1 + \beta_2 > \max_{size}(\varphi) + \max_{size}(\psi)$, either $\beta_1 > \max_{size}(\varphi)$ or $\beta_2 > \max_{size}(\psi)$. Let us assume $\beta_1 > \max_{size}(\varphi)$ (the other case is analogous). We have $size \geq \beta_1 \subseteq_{Lt} \varphi$. However, this is contradictory, since by definition of $\max_{size}(.)$ for all $\beta' > \max_{size}(\varphi)$, $size \geq \beta' \notin_{Lt} \varphi$. Thus, $\max_{size}(\varphi) + \max_{size}(\psi) = \max_{size}(<^*>(\varphi, \psi))$. $\square$

*Proof of (B).* Let $\beta \in \mathbb{N}$ such that $\neg size \geq \beta \subseteq_{Lt} <^*>(\varphi, \psi)$. By definition of $<^*>(\varphi, \psi)$, this implies that there are $\beta_1, \beta_2 \in [0, \alpha]$ such that $\beta = \beta_1 + \beta_2 \div 1$, $\neg size \geq \beta_1 \subseteq_{Lt} \varphi$ and $\neg size \geq \beta_2 \subseteq_{Lt} \psi$. Since $\varphi$ and $\psi$ are satisfiable, by definition of $\max_{size}(.)$, we derive that $\beta_1 > \max_{size}(\varphi)$ and $\beta_2 > \max_{size}(\psi)$. This implies that the core formula $size \geq \max_{size}(\varphi) + 1$ belongs to $\text{Core}(X, \alpha)$ and, analogously, that the core formula $size \geq \max_{size}(\psi) + 1$ belongs to $\text{Core}(X, \alpha)$. Since $\varphi$ is in $\text{CoreTypes}(X, \alpha)$, this implies that $size \geq \max_{size}(\varphi) + 1$ is an atomic formula appearing in $\varphi$. By definition of $\max_{size}(\varphi)$, the formula cannot appear positively, i.e. $\neg size \geq \max_{size}(\varphi) + 1 \subseteq_{Lt} \varphi$. Analogously, $\psi$ is in $\text{CoreTypes}(X, \alpha)$, which leads to $\neg size \geq \max_{size}(\psi) + 1 \subseteq_{Lt} \psi$. $\square$

*Proof of (C).* Directly from (A) and (B). Indeed, by definition of $<^*>(\varphi, \psi)$, we know that for every $\neg size \geq \beta \subseteq_{Lt} \varphi$ and every $\neg size \geq \beta' \subseteq_{Lt} \psi$, $\neg size \geq \beta + \beta' \div 1 \subseteq_{Lt} <^*>(\varphi, \psi)$. $\square$

Now, let us consider $\beta_g = \max_{size}(<^*>(\varphi, \psi)) \div n$. We define the formula Garb below:

$$ \text{Garb} \stackrel{\text{def}}{=} \begin{cases} \text{size} = \beta_g & \text{if } \neg size \geq \beta \subseteq_{Lt} <^*>(\varphi, \psi), \text{ for some } \beta \\ \text{size} \geq \beta_g & \text{otherwise,} \end{cases} $$

where we recall that $size = \beta_g$ stands for $size \geq \beta_g \land \neg (size \geq \beta_g + 1)$. Notice that Garb is a conjunction of literals where at least one $size \geq \beta$ occurs positively (i.e. $size \geq 0$). The objective of this step of the proof is to show that $\vdash_{\mathcal{H}_C(*)} <^*>(\varphi, \psi) \Rightarrow \text{Alloc} * \text{Garb}$. First, we focus on the positive part of Garb, and prove $\vdash_{\mathcal{H}_C(*)} <^*>(\varphi, \psi) \Rightarrow \text{Alloc} * size \geq \beta_g$. If $\beta_g = 0$ then $size \geq \beta_g = \top$ and we have already shown $\vdash_{\mathcal{H}_C(*)} <^*>(\varphi, \psi) \Rightarrow \text{Alloc} * \top$. So, let us assume that $\beta_g > 1$. Notice that then $\max_{size}(<^*>(\varphi, \psi)) \div n = \max_{size}(<^*>(\varphi, \psi)) - n$. We have

1. $\top \Rightarrow size \geq \beta_g \lor \neg size \geq \beta_g$ \qquad PC
2. $\text{Alloc} * \top \Rightarrow \text{Alloc} * (size \geq \beta_g \lor \neg size \geq \beta_g)$ \qquad \text*-Intro, $(A_7^*)$, 1

3. $\text{Alloc} * (size \geq \beta_g \lor \neg size \geq \beta_g) \Rightarrow (\text{Alloc} * size \geq \beta_g) \lor (\text{Alloc} * \neg size \geq \beta_g)$ \qquad $(I_9^*)$, $(A_7^*)$

4. $\text{Alloc} \Rightarrow \neg size \geq n + 1$ \qquad Previously derived
<table>
  <tr>
    <td>5</td>
    <td>Alloc * &not;size &ge; &beta;<sub>g</sub> &rarr; (&not;size &ge; n + 1) * &not;size &ge; &beta;<sub>g</sub></td>
    <td>*-Intro, 4</td>
  </tr>
  <tr>
    <td>6</td>
    <td>(&not;size &ge; n + 1) * &not;size &ge; &beta;<sub>g</sub> &rarr; &not;size &ge; max<sub>size</sub>(&lang;&ast;&rang;(&varphi;, &psi;))</td>
    <td>(A<sub>19</sub><sup>*</sup>), def. of &beta;<sub>g</sub></td>
  </tr>
  <tr>
    <td>7</td>
    <td>Alloc * &top; &rarr; (Alloc * size &ge; &beta;<sub>g</sub>) &or; &not;size &ge; max<sub>size</sub>(&lang;&ast;&rang;(&varphi;, &psi;))</td>
    <td>PC, 2, 3, 5, 6</td>
  </tr>
  <tr>
    <td>8</td>
    <td>&lang;&ast;&rang;(&varphi;, &psi;) &rarr; size &ge; max<sub>size</sub>(&lang;&ast;&rang;(&varphi;, &psi;))</td>
    <td>PC, def. of max<sub>size</sub>(.)</td>
  </tr>
  <tr>
    <td>9</td>
    <td>&lang;&ast;&rang;(&varphi;, &psi;) &rarr; Alloc * &top;</td>
    <td>Previously derived</td>
  </tr>
  <tr>
    <td>10</td>
    <td>&lang;&ast;&rang;(&varphi;, &psi;) &rarr; (Alloc * size &ge; &beta;<sub>g</sub>) &or; &not;size &ge; max<sub>size</sub>(&lang;&ast;&rang;(&varphi;, &psi;))</td>
    <td>&rarr;-Tr, 7, 9</td>
  </tr>
  <tr>
    <td>11</td>
    <td>&lang;&ast;&rang;(&varphi;, &psi;) &rarr; Alloc * size &ge; &beta;<sub>g</sub></td>
    <td>PC, 8, 10</td>
  </tr>
</table>

If for every $\beta$, $\neg size \ge \beta \notin_{Lt} \langle * \rangle(\varphi, \psi)$, then by definition of Garb we conclude that

$$ \vdash_{\mathcal{H}_C(*)} \langle * \rangle(\varphi, \psi) \Rightarrow Alloc * Garb. $$

Otherwise, suppose that there is $\beta$ such that $\neg size \ge \beta \subseteq_{Lt} \langle * \rangle(\varphi, \psi)$. So, Garb is defined as $size \ge \beta_g \wedge \neg (size \ge \beta_g + 1)$. Directly from (C), we know that $\neg size \ge \max_{size}(\langle * \rangle(\varphi, \psi)) + 1 \subseteq_{Lt} \langle * \rangle(\varphi, \psi)$. By propositional reasoning,

$$ \vdash_{\mathcal{H}_C(*)} \langle * \rangle(\varphi, \psi) \Rightarrow \neg size \ge \max_{size}(\langle * \rangle(\varphi, \psi)) + 1. $$

Then, $\langle * \rangle(\varphi, \psi) \Rightarrow Alloc * Garb$ is derived as follows:

<table>
  <tbody>
    <tr>
      <td>1</td>
      <td>size &ge; &beta;<sub>g</sub> &rarr; (size &ge; &beta;<sub>g</sub> &and; size &ge; &beta;<sub>g</sub> + 1) &or; size = &beta;<sub>g</sub></td>
      <td>PC, def. of size = &beta;<sub>g</sub></td>
    </tr>
    <tr>
      <td>2</td>
      <td>Alloc * size &ge; &beta;<sub>g</sub> &rarr;</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>Alloc*((size &ge; &beta;<sub>g</sub> &and; size &ge; &beta;<sub>g</sub> +1) &or; size = &beta;<sub>g</sub>)</td>
      <td>*-Intro, (A<sub>7</sub><sup>*</sup>), 1</td>
    </tr>
    <tr>
      <td>3</td>
      <td>Alloc*((size &ge; &beta;<sub>g</sub> &and; size &ge; &beta;<sub>g</sub> +1) &or; size = &beta;<sub>g</sub>)</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>&rarr; (Alloc * (size &ge; &beta;<sub>g</sub> &and; size &ge; &beta;<sub>g</sub> +1)) &or; (Alloc * size = &beta;<sub>g</sub>)</td>
      <td>(I<sub>9</sub><sup>*</sup>, (A<sub>7</sub><sup>*</sup>))</td>
    </tr>
    <tr>
      <td>4</td>
      <td>size &ge; &beta;<sub>g</sub> &and; size &ge; &beta;<sub>g</sub> + 1 &rarr; size &ge; &beta;<sub>g</sub> + 1</td>
      <td>PC</td>
    </tr>
    <tr>
      <td>5</td>
      <td>Alloc &rarr; size &ge; n</td>
      <td>Previously derived</td>
    </tr>
    <tr>
      <td>6</td>
      <td>Alloc * (size &ge; &beta;<sub>g</sub> &and; size &ge; &beta;<sub>g</sub> +1) &rarr; size &ge; n * size &ge; &beta;<sub>g</sub> + 1</td>
      <td>*-Ilr, 4, 5</td>
    </tr>
    <tr>
      <td>7</td>
      <td>size &ge; n * size &ge; &beta;<sub>g</sub> + 1 &rarr; size &ge; max<sub>size</sub>(\langle * \rangle(\varphi, \psi)) + 1</td>
      <td>(A<sub>8</sub><sup>*</sup>), def. of size &ge; &beta;</td>
    </tr>
    <tr>
      <td>8</td>
      <td>Alloc * size &ge; &beta;<sub>g</sub> &rarr; size &ge; max<sub>size</sub>(\langle * \rangle(\varphi, \psi)) + 1</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>&or; (Alloc * size = &beta;<sub>g</sub>)</td>
      <td>PC, 2, 3, 6, 7</td>
    </tr>
    <tr>
      <td>9</td>
      <td>&lang;&ast;&rang;(&varphi;, &psi;) &rarr; Alloc * size &ge; &beta;<sub>g</sub></td>
      <td>Previously derived</td>
    </tr>
    <tr>
      <td>10</td>
      <td>&lang;&ast;&rang;(&varphi;, &psi;) &rarr; size &ge; max<sub>size</sub>(\langle * \rangle(\varphi, \psi)) + 1 &or; (Alloc * size = &beta;<sub>g</sub>)</td>
      <td>&rarr;-Tr, 8, 9</td>
    </tr>
    <tr>
      <td>11</td>
      <td>&lang;&ast;&rang;(&varphi;, &psi;) &rarr; &not;size &ge; max<sub>size</sub>(\langle * \rangle(\varphi, \psi)) + 1</td>
      <td>PC, see above</td>
    </tr>
    <tr>
      <td>12</td>
      <td>&lang;&ast;&rang;(&varphi;, &psi;) &rarr; (Alloc * size = &beta;<sub>g</sub>)</td>
      <td>PC, 10, 11</td>
    </tr>
  </tbody>
</table>

**Step 2, distributing alloc and size literals.** In this step, we aim at showing that

$$ \vdash_{\mathcal{H}_C(*)} Alloc * Garb \Rightarrow \varphi^{(1)} * \psi^{(1)} $$
where $\varphi^{(1)}$ and $\psi^{(1)}$ are two formulae defined as follows:

$$ \varphi^{(1)} \stackrel{\text{def}}{=} \begin{cases} \text{size} = \max_{\text{size}}(\varphi) \wedge \bigwedge \{\text{alloc}(x_i) \subseteq \text{Lt} \ \varphi \mid i \in [1, n]\} & \text{if } \max_{\text{size}}(\varphi) < \alpha \\ \text{size} \ge \max_{\text{size}}(\varphi) \wedge \bigwedge \{\text{alloc}(x_i) \subseteq \text{Lt} \ \varphi \mid i \in [1, n]\} & \text{otherwise} \end{cases} $$

$$ \psi^{(1)} \stackrel{\text{def}}{=} \begin{cases} \text{size} = \max_{\text{size}}(\psi) \wedge \bigwedge \{\text{alloc}(x_i) \subseteq \text{Lt} \ \psi \mid i \in [1, n]\} & \text{if } \max_{\text{size}}(\psi) < \alpha \\ \text{size} \ge \max_{\text{size}}(\psi) \wedge \bigwedge \{\text{alloc}(x_i) \subseteq \text{Lt} \ \psi \mid i \in [1, n]\} & \text{otherwise} \end{cases} $$

We use the notations $\varphi^{(1)}$ and $\psi^{(1)}$ since later in the proof, we shall consider sequences of formulae $\varphi^{(1)}, \dots, \varphi^{(k)}$ and $\psi^{(1)}, \dots, \psi^{(k)}$ with increasing amount of literals. That is why, using $\varphi^{(1)}$ and $\psi^{(1)}$ at this early stage is meaningful. Before tackling this derivation, a few more steps are required. First of all, notice that, if there is a formula $\text{alloc}(x)$ occurring both in $\varphi$ and $\psi$, then, by definition of $\langle * \rangle(\varphi, \psi)$, $x \neq x$ occurs in $\langle * \rangle(\varphi, \psi)$. This contradicts the fact that $\langle * \rangle(\varphi, \psi)$ is satisfiable. Therefore, we derive that the set of variables $x_1, \dots, x_n$ can be split into two disjoint subsets, the ones “allocated” in $\varphi$, and the others in $\psi$. Let $n_\varphi$ (resp. $n_\psi$) denote the number of equivalence classes of variables allocated in $\varphi$ (resp. $\psi$). Clearly, $n = n_\varphi + n_\psi$. Moreover, since $\varphi$ and $\psi$ are satisfiable core types in $\text{CoreTypes}(X, \alpha)$, where $\alpha \ge \text{card}(X)$, we must have $n_\varphi \le \max_{\text{size}}(\varphi)$ and $n_\psi \le \max_{\text{size}}(\psi)$ (see the axiom $(\mathbf{I}_6^C)$). By $(\mathbf{A})$, we conclude that $n \le \max_{\text{size}}(\langle * \rangle(\varphi, \psi))$. We define the following formulae

$$ \text{Alloc}(\varphi) \stackrel{\text{def}}{=} \ast \{\text{alloc}(x_i) \wedge \text{size} = 1 \mid \text{alloc}(x_i) \subseteq \text{Lt} \ \varphi, i \in [1, n]\} $$

$$ \text{Garb}(\varphi) \stackrel{\text{def}}{=} \begin{cases} \text{size} = \max_{\text{size}}(\varphi) - n_\varphi & \text{if } \max_{\text{size}}(\varphi) < \alpha \\ \text{size} \ge \max_{\text{size}}(\varphi) - n_\varphi & \text{otherwise} \end{cases} $$

Notice that, since $\max_{\text{size}}(\varphi) \ge n_\varphi$, the formula $\text{Garb}(\varphi)$ is well-defined. The formulae $\text{Alloc}(\psi)$ and $\text{Garb}(\psi)$ are defined accordingly. Obviously, $\text{Alloc}$ is equal to $\text{Alloc}(\varphi) \ast \text{Alloc}(\psi)$ modulo associativity and commutativity of the separating conjunction $\ast$. Hence, by taking advantage of the axioms $(\mathbf{A}_7^*)$ and $(\mathbf{A}_8^*)$, we have

$$ \vdash_{\mathcal{H}_C(\ast)} \text{Alloc} \Leftrightarrow \text{Alloc}(\varphi) \ast \text{Alloc}(\psi). $$

Let us now look at $\text{Garb}(\varphi)$ and $\text{Garb}(\psi)$. We aim at deriving

$$ \vdash_{\mathcal{H}_C(\ast)} \text{Garb} \Rightarrow \text{Garb}(\varphi) \ast \text{Garb}(\psi). $$

Since $\varphi$ is a core type, we know that if $\max_{\text{size}}(\varphi) < \alpha$ then, by definition of $\max_{\text{size}}(\varphi)$, $\neg \text{size} \ge \max_{\text{size}}(\varphi) + 1 \subseteq \text{Lt} \ \varphi$. A similar analysis can be done for $\psi$, which leads to the two following equivalences, by definition of $\text{Garb}(\varphi)$ and $\text{Garb}(\psi)$:

* $\neg \text{size} \ge \max_{\text{size}}(\varphi) + 1 \subseteq \text{Lt} \ \varphi$ if and only if $\text{Garb}(\varphi) = (\text{size} = \max_{\text{size}}(\varphi) - n_\varphi)$,

* $\neg \text{size} \ge \max_{\text{size}}(\psi) + 1 \subseteq \text{Lt} \ \psi$ if and only if $\text{Garb}(\psi) = (\text{size} = \max_{\text{size}}(\psi) - n_\psi)$.

By definition of $\text{Garb}$, $(\mathbf{B})$ and $(\mathbf{C})$, we know that $\text{Garb} = (\text{size} = \max_{\text{size}}(\langle * \rangle(\varphi, \psi)) \div n)$ holds if and only if $\neg \text{size} \ge \max_{\text{size}}(\varphi) + 1 \subseteq \text{Lt} \ \varphi$ and $\neg \text{size} \ge \max_{\text{size}}(\varphi) + 1 \subseteq \text{Lt} \ \psi$. From $n \le \max_{\text{size}}(\langle * \rangle(\varphi, \psi))$ and by relying on the previous two equivalences, this allows us to conclude that:

**D.** $\text{Garb}(\varphi) = (\text{size} = \max_{\text{size}}(\varphi) - n_\varphi)$ and $\text{Garb}(\psi) = (\text{size} = \max_{\text{size}}(\psi) - n_\psi)$ if and only if $\text{Garb} = (\text{size} = \max_{\text{size}}(\langle * \rangle(\varphi, \psi)) - n)$.

To show $\vdash_{\mathcal{H}_C(\ast)} \text{Garb} \Rightarrow (\text{Garb}(\varphi) \ast \text{Garb}(\psi))$, we split the proof depending on whether $\text{Garb}(\varphi) = (\text{size} = \max_{\text{size}}(\varphi) - n_\varphi)$ and $\text{Garb}(\psi) = (\text{size} = \max_{\text{size}}(\psi) - n_\psi)$ hold.
**case:** Garb($\varphi$) $\neq$ (size = max$_{size}$($\varphi$) - n$_{\varphi}$) and Garb($\psi$) $\neq$ (size = max$_{size}$($\psi$) - n$_{\psi}$):

We have Garb($\varphi$) = (size$\geq$max$_{size}$($\varphi$)-n$_{\varphi}$) and Garb($\psi$) = (size$\geq$max$_{size}$($\psi$)-n$_{\psi}$).
By definition of Garb and (D), Garb = (size$\geq$max$_{size}$(<\ast>($\varphi$, $\psi$)) - n). By n = n$_{\varphi}$ + n$_{\psi}$ and (A), max$_{size}$(<\ast>($\varphi$, $\psi$)) - n = (max$_{size}$($\varphi$)-n$_{\varphi}$) + (max$_{size}$($\psi$)-n$_{\psi}$). By definition of the core formula size $\geq$ $\beta$, Garb is already equivalent to Garb($\varphi$) * Garb($\psi$), modulo associativity and commutativity of the separating conjunction $\ast$. Hence, by taking advantage of the axioms (A\*_7) and (A\*_8), we have $\vdash_{H_C(\ast)}$ Garb $\Rightarrow$ Garb($\varphi$) * Garb($\psi$).

**case:** Garb($\varphi$) = (size = max$_{size}$($\varphi$)-n$_{\varphi}$) and Garb($\psi$) $\neq$ (size = max$_{size}$($\psi$)-n$_{\psi}$):

We have Garb($\psi$) = (size$\geq$max$_{size}$($\psi$)-n$_{\psi}$) and, by definition of Garb and (D), together with n = n$_{\varphi}$ + n$_{\psi}$ and (A), Garb = (size $\geq$ (max$_{size}$($\varphi$)-n$_{\varphi}$) + (max$_{size}$($\psi$)-n$_{\psi}$)). In this case, Garb $\Rightarrow$ Garb($\varphi$) * Garb($\psi$) is an instantiation of the following valid formula with $\beta_1$ = max$_{size}$($\varphi$)-n$_{\varphi}$ and $\beta_2$ = max$_{size}$($\psi$) - n$_{\psi}$:

$$size \geq \beta_1 + \beta_2 \Rightarrow size = \beta_1 * size \geq \beta_2.$$

The derivability of this formula in $H_C(\ast)$ is proven by induction on $\beta_1$ (see Appendix B).

**case:** Garb($\varphi$) $\neq$ (size = max$_{size}$($\varphi$)-n$_{\varphi}$) and Garb($\psi$) = (size = max$_{size}$($\psi$)-n$_{\psi}$):

Analogously to the previous case, we have Garb($\varphi$) = (size$\geq$max$_{size}$($\varphi$)-n$_{\varphi}$) and Garb = (size $\geq$ (max$_{size}$($\varphi$)-n$_{\varphi}$) + (max$_{size}$($\psi$)-n$_{\psi}$)). We instantiate the theorem

$$size \geq \beta_1 + \beta_2 \Rightarrow size = \beta_1 * size \geq \beta_2.$$

shown derivable in the previous case of the proof, with $\beta_1$ = max$_{size}$($\psi$)-n$_{\psi}$ and $\beta_2$ = max$_{size}$($\varphi$) - n$_{\varphi}$. This corresponds to Garb $\Rightarrow$ Garb($\psi$) * Garb($\varphi$). Afterwards, by commutativity of the separating conjunction (axiom (A\*_7)) and propositional reasoning, we conclude that $\vdash_{H_C(\ast)}$ Garb $\Rightarrow$ Garb($\varphi$) * Garb($\psi$).

**case:** Garb($\varphi$) = (size = max$_{size}$($\varphi$)-n$_{\varphi}$) and Garb($\psi$) = (size = max$_{size}$($\psi$)-n$_{\psi}$):

By (D), n = n$_{\varphi}$ + n$_{\psi}$ and (A), Garb = (size = (max$_{size}$($\varphi$)-n$_{\varphi}$) + (max$_{size}$($\psi$)-n$_{\psi}$)). In this case, Garb $\Rightarrow$ Garb($\varphi$) * Garb($\psi$) is an instantiation of the following valid formula, with $\beta_1$ = max$_{size}$($\varphi$)-n$_{\varphi}$ and $\beta_2$ = max$_{size}$($\psi$) - n$_{\psi}$:

$$size = \beta_1 + \beta_2 \Rightarrow size = \beta_1 * size = \beta_2.$$

Its derivation in $H_C(\ast)$ can be found in Appendix B.

Thanks to the case analysis above, we conclude that $\vdash_{H_C(\ast)}$ Garb $\Rightarrow$ Garb($\varphi$) * Garb($\psi$).
Thus, $\vdash_{H_C(\ast)}$ Alloc * Garb $\Rightarrow$ (Alloc($\varphi$) * Garb($\varphi$)) * (Alloc($\psi$) * Garb($\psi$)). Indeed,

<table><tr><td>1</td><td>Alloc $\Rightarrow$ Alloc($\varphi$) * Alloc($\psi$)</td><td>Previously derived</td></tr><tr><td>2</td><td>Garb $\Rightarrow$ Garb($\varphi$) * Garb($\psi$)</td><td>Previously derived</td></tr><tr><td>3</td><td>Alloc * Garb $\Rightarrow$ (Alloc($\varphi$) * Alloc($\psi$)) * (Garb($\varphi$) * Garb($\psi$))</td><td>*-Ilr, 1, 2</td></tr><tr><td>4</td><td>(Alloc($\varphi$) * Alloc($\psi$)) * (Garb($\varphi$) * Garb($\psi$)) $\Rightarrow$<br>(Alloc($\varphi$) * Garb($\varphi$)) * (Alloc($\psi$) * Garb($\psi$))</td><td>(A\*_7), (A\*_8)</td></tr><tr><td>5</td><td>Alloc * Garb $\Rightarrow$ (Alloc($\varphi$) * Garb($\varphi$)) * (Alloc($\psi$) * Garb($\psi$))</td><td>$\Rightarrow$-Tr, 3, 4</td></tr></table>

To conclude this step of the proof, it is sufficient to show $\vdash_{H_C(\ast)}$ Alloc($\varphi$) * Garb($\varphi$) $\Rightarrow$ $\varphi^{(1)}$ and $\vdash_{H_C(\ast)}$ Alloc($\psi$) * Garb($\psi$) $\Rightarrow$ $\psi^{(1)}$. Indeed, by relying on the rule *-Ilr, we then obtain $\vdash_{H_C(\ast)}$ Alloc * Garb $\Rightarrow$ $\varphi^{(1)}$ * $\psi^{(1)}$. Below, we show $\vdash_{H_C(\ast)}$ Alloc($\varphi$) * Garb($\varphi$) $\Rightarrow$ $\varphi^{(1)}$. The developments of $\vdash_{H_C(\ast)}$ Alloc($\psi$) * Garb($\psi$) $\Rightarrow$ $\psi^{(1)}$ are analogous. We recall that the formula
Alloc(φ) is defined as

$$Alloc(\varphi) = \*\{alloc(x_i) \wedge size = 1 | alloc(x_i) \subseteq_{Lt} \varphi\}.$$

First of all, let us show that $\vdash_{\mathcal{H}_C(*)} Alloc(\varphi) * \top \Rightarrow \bigwedge \{alloc(x_i) \subseteq_{Lt} \varphi \mid i \in [1, n]\}$. The proof is divided in three cases:

**case:** $\{alloc(x_i) \wedge size = 1 | alloc(x_i) \subseteq_{Lt} \varphi\} = \emptyset$: In this case, the formula we want to derive is syntactically equal to $\top * \top \Rightarrow \top$, which is derivable by propositional reasoning.

**case:** $card(\{alloc(x_i) \wedge size = 1 | alloc(x_i) \subseteq_{Lt} \varphi\}) = 1$: In this case, the formula we want to derive is syntactically equal to $(alloc(x) \wedge size = 1) * \top \Rightarrow alloc(x)$. Therefore, it is derivable in $\mathcal{H}_C(*)$ by $(\mathbf{I}_{12}^*)$ and $\*-\text{Intro}$.

**case:** $card(\{alloc(x_i) \wedge size = 1 | alloc(x_i) \subseteq_{Lt} \varphi\}) \ge 2$: In the derivation below, we write $Alloc(\varphi)^{-i}$ for $\*\{alloc(x_j) \wedge size = 1 \mid j \in [1, n] \setminus \{i\}, alloc(x_j) \subseteq_{Lt} \varphi\}$. Roughly speaking, $Alloc(\varphi)^{-i}$ is obtained from $Alloc(\varphi)$ by removing the subformula $alloc(x_i) \wedge size = 1$. Since $card(\{alloc(x_i) \wedge size = 1 | alloc(x_i) \subseteq_{Lt} \varphi\}) \ge 2$, the formula $Alloc(\varphi)^{-i}$ is different from $\top$. We have

<table><tr><td>1</td><td>Alloc(φ) * ⊤ ⇒<br/>(alloc(x<sub>i</sub>) ∧ size = 1) * (Alloc(φ)<sup>-i</sup> * ⊤) <br/> (A<sub>7</sub><sup>*</sup>, A<sub>8</sub><sup>*</sup>), def. of Alloc(φ)<br/> where alloc(x<sub>i</sub>) ⊆<sub>Lt</sub> φ and i ∈ [1, n]</td></tr><tr><td>2</td><td>Alloc(φ)<sup>-i</sup> * ⊤ ⇒ ⊤</td></tr><tr><td>3</td><td>alloc(x<sub>i</sub>) ∧ size = 1 ⇒ alloc(x<sub>i</sub>)</td></tr><tr><td>4</td><td>(alloc(x<sub>i</sub>) ∧ size = 1) * (Alloc(φ)<sup>-i</sup> * ⊤) ⇒<br/>alloc(x<sub>i</sub>) * ⊤ <br/> *-Ilr, 2, 3</td></tr><tr><td>5</td><td>alloc(x<sub>i</sub>) * ⊤ ⇒ alloc(x<sub>i</sub>)</td></tr><tr><td>6</td><td>Alloc(φ) * ⊤ ⇒ alloc(x<sub>i</sub>)</td></tr><tr><td>7</td><td>Alloc(φ) * ⊤ ⇒ ⋀{alloc(x<sub>i</sub>) ⊆<sub>Lt</sub> φ | i ∈ [1, n]}<br/>PC, repeating 6<br/>for all i ∈ [1, n] such that alloc(x<sub>i</sub>) ⊆<sub>Lt</sub> φ</td></tr></table>

So, we have $\vdash_{\mathcal{H}_C(*)} Alloc(\varphi) * \top \Rightarrow \bigwedge \{alloc(x_i) \subseteq_{Lt} \varphi \mid i \in [1, n]\}$.

Now, recall that $card(\{i \in [1, n] \mid alloc(x_i) \subseteq_{Lt} \varphi\}) = n_φ$. At the beginning of the proof, we have shown a derivation of $\vdash_{\mathcal{H}_C(*)} Alloc \Rightarrow size = n$, where Alloc is defined as $\*\{alloc(x_i) \wedge size = 1 \mid i \in [1, n]\}$. Replacing Alloc by Alloc(φ) and n by n_φ in the derivation of $Alloc \Rightarrow size = n$ leads to a derivation in $\mathcal{H}_C(*)$ of $Alloc(\varphi) \Rightarrow size = n_φ$.

To show $\vdash_{\mathcal{H}_C(*)} Alloc(\varphi) * Garb(\varphi) \Rightarrow \varphi^{(1)}$, we split the proof in two cases:

**case:** $\max_{size}(\varphi) = \alpha$: By definition of $\varphi^{(1)}$ and $Garb(\varphi)$, we have:

* $\varphi^{(1)} = size \ge \max_{size}(\varphi) \wedge \bigwedge \{alloc(x_i) \subseteq_{Lt} \varphi \mid i \in [1, n]\}$,

* $Garb(\varphi) = size \ge \max_{size}(\varphi) - n_φ$,

Then,

<table><tr><td>1</td><td>Alloc(φ) * ⊤ ⇒ ⋀{alloc(x<sub>i</sub>) ⊆<sub>Lt</sub> φ | i ∈ [1, n]}<br/>Previously derived</td></tr><tr><td>2</td><td>Garb(φ) ⇒ ⊤</td></tr><tr><td>3</td><td>Alloc(φ) * Garb(φ) ⇒ Alloc(φ) * ⊤ <br/> *-Intro, (A<sub>7</sub><sup>*</sup>, 2)</td></tr></table>
<table>
  <tbody>
    <tr>
      <td>4</td>
      <td>Alloc(φ) * Garb(φ) ⇒ ⋀{alloc(x<sub>i</sub>) ⊆<sub>LT</sub> φ | i ∈ [1, n]}</td>
      <td>⇒-Tr, 1, 3</td>
    </tr>
    <tr>
      <td>5</td>
      <td>Alloc(φ) ⇒ size = n<sub>φ</sub></td>
      <td>See above</td>
    </tr>
    <tr>
      <td>6</td>
      <td>size = n<sub>φ</sub> ⇒ size ≥ n<sub>φ</sub></td>
      <td>PC, def. of size = n<sub>φ</sub></td>
    </tr>
    <tr>
      <td>7</td>
      <td>Alloc(φ) ⇒ size ≥ n<sub>φ</sub></td>
      <td></td>
    </tr>
    <tr>
      <td>8</td>
      <td>Garb(φ) ⇒ size ≥ max<sub>size</sub>(φ) - n<sub>φ</sub></td>
      <td>PC, def. of Garb(φ)</td>
    </tr>
    <tr>
      <td>9</td>
      <td>Alloc(φ) * Garb(φ) ⇒ size ≥ n<sub>φ</sub> * size ≥ max<sub>size</sub>(φ) - n<sub>φ</sub></td>
      <td>*-Ilr, 7, 8</td>
    </tr>
    <tr>
      <td>10</td>
      <td>size ≥ n<sub>φ</sub> * size ≥ max<sub>size</sub>(φ) - n<sub>φ</sub> ⇒ size ≥ max<sub>size</sub>(φ)</td>
      <td>(A<sub>8</sub><sup>*</sup>), (A<sub>7</sub><sup>*</sup>), def. of size ≥ β</td>
    </tr>
    <tr>
      <td>11</td>
      <td>Alloc(φ) * Garb(φ) ⇒ size ≥ max<sub>size</sub>(φ)</td>
      <td>⇒-Tr, 9, 10</td>
    </tr>
    <tr>
      <td>12</td>
      <td>Alloc(φ) * Garb(φ) ⇒ φ<sup>(1)</sup></td>
      <td>PC, 4, 11, def. of φ<sup>(1)</sup></td>
    </tr>
  </tbody>
</table>

case: $\max_{\text{size}}(\varphi) \neq \alpha$: In this case, $\max_{\text{size}}(\varphi) < \alpha$ and so we have:

$$
\bullet \varphi^{(1)} = \text{size} = \max_{\text{size}}(\varphi) \wedge \bigwedge \{\text{alloc}(x_i) \subseteq \text{Lt} \ \varphi \mid i \in [1, n]\},
$$

$$
\bullet \text{Garb}(\varphi) = \text{size} = \max_{\text{size}}(\varphi) - n_{\varphi},
$$

We can rely on the previous case of the proof in order to show that

$$
\vdash_{H_C(*)} \mathrm{Alloc}(\varphi) * \mathrm{Garb}(\varphi) \Rightarrow \mathrm{size} \ge \max_{\mathrm{size}}(\varphi) \wedge \bigwedge \{\mathrm{alloc}(x_i) \subseteq_{\mathrm{Lt}} \varphi \mid i \in [1, n]\}.
$$

By propositional reasoning, we can derive $\vdash_{H_C(*)} Alloc(\varphi) * Garb(\varphi) \Rightarrow \varphi^{(1)}$ as soon as we show that $\vdash_{H_C(*)} Alloc(\varphi) * Garb(\varphi) \Rightarrow \neg size \ge \max_{size}(\varphi) + 1$, as we do now:

<table>
  <tbody>
    <tr>
      <td>1</td>
      <td>Alloc(φ) ⇒ size = n<sub>φ</sub></td>
      <td>Already discussed above</td>
    </tr>
    <tr>
      <td>2</td>
      <td>size = n<sub>φ</sub> ⇒ ¬size ≥ n<sub>φ</sub> + 1</td>
      <td>PC, def. of size = n<sub>φ</sub></td>
    </tr>
    <tr>
      <td>3</td>
      <td>Alloc(φ) ⇒ ¬size ≥ n<sub>φ</sub> + 1</td>
      <td>PC, ⇒-Tr, 1, 2</td>
    </tr>
    <tr>
      <td>4</td>
      <td>Garb(φ) ⇒ ¬size ≥ max<sub>size</sub>(φ) - n<sub>φ</sub> + 1</td>
      <td>PC, def. of size = β</td>
    </tr>
    <tr>
      <td>5</td>
      <td>Alloc(φ) * Garb(φ) ⇒</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>¬size ≥ n<sub>φ</sub> + 1 * ¬size ≥ max<sub>size</sub>(φ) - n<sub>φ</sub> + 1</td>
      <td>*-Ilr, 3, 4</td>
    </tr>
    <tr>
      <td>6</td>
      <td>¬size ≥ n<sub>φ</sub> + 1 * ¬size ≥ max<sub>size</sub>(φ) - n<sub>φ</sub> + 1 ⇒</td>
      <td></td>
    </tr>
    <tr>
      <td></td>
      <td>¬size ≥ max<sub>size</sub>(φ) + 1</td>
      <td>(A<sub>19</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>7</td>
      <td>Alloc(φ) * Garb(φ) ⇒ ¬size ≥ max<sub>size</sub>(φ) + 1</td>
      <td>⇒-Tr, 5, 6</td>
    </tr>
  </tbody>
</table>

This concludes the proof of $\vdash_{H_C(*)} Alloc(\varphi) * Garb(\varphi) \Rightarrow \varphi^{(1)}$. As already stated, one can analogously show that $\vdash_{H_C(*)} Alloc(\psi) * Garb(\psi) \Rightarrow \psi^{(1)}$. Afterwards, by *-Ilr and from $\vdash_{H_C(*)} Alloc * Garb \Rightarrow (Alloc(\varphi) * Garb(\varphi)) * (Alloc(\psi) * Garb(\psi))$, we conclude that

$$
\vdash_{H_C(*)} Alloc * Garb \Rightarrow \varphi^{(1)} * \psi^{(1)}.
$$

**Step 3, add the missing literals.** From the first and second step of the proof, and by propositional reasoning, $\vdash_{H_C(*)} \langle * \rangle(\varphi, \psi) \Rightarrow \varphi^{(1)} * \psi^{(1)}$. We now rely on $\langle * \rangle(\varphi, \psi)$ to add to $\varphi^{(1)}$ and $\psi^{(1)}$ missing literals from $\varphi$ and $\psi$, respectively. We add the literals progressively, building a sequence of formulae $\varphi^{(1)} * \psi^{(1)}$, $\varphi^{(2)} * \psi^{(2)}$, ..., $\varphi^{(k)} * \psi^{(k)}$, where for all $i \in [1, k]$, $\varphi^{(i)}$ and $\psi^{(i)}$ are conjunctions of core formulae such that $\vdash_{H_C(*)} \langle * \rangle(\varphi, \psi) \Rightarrow \varphi^{(i)} * \psi^{(i)}$, and
for all $j \in [1, i]$, $\varphi^{(j)} \subseteq_{\mathrm{Lt}} \varphi^{(i)}$ and $\psi^{(j)} \subseteq_{\mathrm{Lt}} \psi^{(i)}$. Fundamentally, we obtain $\varphi = \varphi^{(k)}$ and $\psi = \psi^{(k)}$ (modulo associativity and commutativity of the classical conjunction), which allows us to derive $\vdash_{\mathcal{H}_{C(*)}} \langle * \rangle(\varphi, \psi) \Rightarrow \varphi * \psi$, ending the proof. Below, we focus on the formula $\varphi^{(i)}$ and $\varphi$. Since $\langle * \rangle(\varphi, \psi)$ is equal to $\langle * \rangle(\psi, \varphi)$ (by definition) and the separating conjunction is commutative (axiom $(A_7^*)$), a similar analysis can be done for $\psi^{(i)}$ and $\psi$. Thus, we assume that $\vdash_{\mathcal{H}_{C(*)}} \langle * \rangle(\varphi, \psi) \Rightarrow \varphi^{(i)} * \psi^{(i)}$ holds, where in particular $\varphi^{(1)} \subseteq_{\mathrm{Lt}} \varphi^{(i)}$ and $\psi^{(1)} \subseteq_{\mathrm{Lt}} \psi^{(i)}$, and that there is a literal $L \subseteq_{\mathrm{Lt}} \varphi$ that does not appear in $\varphi^{(i)}$. By relying on the theorems in Lemma 5.2, we show that $\vdash_{\mathcal{H}_{C(*)}} \langle * \rangle(\varphi, \psi) \Rightarrow (\varphi^{(i)} \wedge L) * \psi^{(i)}$ by a case analysis on $L$.

**case:** $L = x \sim y$, where $\sim \in \{=, \ne\}$: By definition of $\langle * \rangle(\varphi, \psi)$, $x \sim y \subseteq_{\mathrm{Lt}} \langle * \rangle(\varphi, \psi)$.

<table><tr><td>1</td><td>⟨*⟩(φ, ψ) ⇒ φ<sup>(i)</sup> * ψ<sup>(i)</sup></td><td>Hypothesis</td></tr><tr><td>2</td><td>⟨*⟩(φ, ψ) ⇒ x ~ y</td><td>PC, def. of ⟨*⟩(φ, ψ), see above</td></tr><tr><td>3</td><td>⟨*⟩(φ, ψ) ⇒ x ~ y ∧ (φ<sup>(i)</sup> * ψ<sup>(i)</sup>)</td><td>PC, 1, 2</td></tr><tr><td>4</td><td>x ~ y ∧ (φ<sup>(i)</sup> * ψ<sup>(i)</sup>) ⇒ (φ<sup>(i)</sup> ∧ x ~ y) * ψ<sup>(i)</sup></td><td>(I<sub>5.2.1</sub><sup>*</sup>)</td></tr><tr><td>5</td><td>⟨*⟩(φ, ψ) ⇒ (φ<sup>(i)</sup> ∧ x ~ y) * ψ<sup>(i)</sup></td><td>⇒-Tr, 3, 4</td></tr></table>

**case:** $L = \mathrm{alloc}(x)$: Since $\mathrm{alloc}(x) \subseteq_{\mathrm{Lt}} \varphi$, by definition, $\mathrm{alloc}(x) \subseteq_{\mathrm{Lt}} \langle * \rangle(\varphi, \psi)$. By definition of $x_1, \dots, x_n$, there is $j \in [1, n]$ such that $x_j = x \subseteq_{\mathrm{Lt}} \langle * \rangle(\varphi, \psi)$. Since $\varphi$ is a core type, $\mathrm{alloc}(x_j) \subseteq_{\mathrm{Lt}} \varphi$. By definition of $\varphi^{(1)}$, $\mathrm{alloc}(x_j) \subseteq_{\mathrm{Lt}} \varphi^{(1)}$. From $\varphi^{(1)} \subseteq_{\mathrm{Lt}} \varphi^{(i)}$, we have $\mathrm{alloc}(x_j) \subseteq_{\mathrm{Lt}} \varphi^{(i)}$. Afterwards,

<table><tr><td>1</td><td>φ<sup>(i)</sup> ⇒ φ<sup>(i)</sup> ∧ alloc(x<sub>j</sub>)</td><td>PC, see above</td></tr><tr><td>2</td><td>⟨*⟩(φ, ψ) ⇒ φ<sup>(i)</sup> * ψ<sup>(i)</sup></td><td>Hypothesis</td></tr><tr><td>3</td><td>φ<sup>(i)</sup> * ψ<sup>(i)</sup> ⇒ (φ<sup>(i)</sup> ∧ alloc(x<sub>j</sub>)) * ψ<sup>(i)</sup></td><td>*-Intro, 1</td></tr><tr><td>4</td><td>⟨*⟩(φ, ψ) ⇒ x<sub>j</sub> = x</td><td>PC, see above</td></tr><tr><td>5</td><td>⟨*⟩(φ, ψ) ⇒ x<sub>j</sub> = x ∧ ((φ<sup>(i)</sup> ∧ alloc(x<sub>j</sub>)) * ψ<sup>(i)</sup>)</td><td>PC, 2, 3, 4</td></tr><tr><td>6</td><td>x<sub>j</sub> = x ∧ ((φ<sup>(i)</sup> ∧ alloc(x<sub>j</sub>)) * ψ<sup>(i)</sup>) ⇒ (φ<sup>(i)</sup> ∧ alloc(x)) * ψ<sup>(i)</sup></td><td>(I<sub>5.2.2</sub><sup>*</sup>)</td></tr><tr><td>7</td><td>⟨*⟩(φ, ψ) ⇒ ((φ<sup>(i)</sup> ∧ alloc(x)) * ψ<sup>(i)</sup>)</td><td>⇒-Tr, 5, 6</td></tr></table>

Without loss of generality, thanks to the derivation above dealing with $\mathrm{alloc}(x)$ literals, we now assume that for all $\mathrm{alloc}(x) \subseteq_{\mathrm{Lt}} \varphi$ and all $\mathrm{alloc}(y) \subseteq_{\mathrm{Lt}} \psi$, we have $\mathrm{alloc}(x) \subseteq_{\mathrm{Lt}} \varphi^{(i)}$ and $\mathrm{alloc}(y) \subseteq_{\mathrm{Lt}} \psi^{(i)}$.

**case:** $L = \neg \mathrm{alloc}(x)$: We distinguish two main subcases.

* First, assume $\neg \mathrm{alloc}(x) \subseteq_{\mathrm{Lt}} \psi$. By definition of $\langle * \rangle(\varphi, \psi)$, $\neg \mathrm{alloc}(x) \subseteq_{\mathrm{Lt}} \langle * \rangle(\varphi, \psi)$.

<table><tr><td>1</td><td>⟨*⟩(φ, ψ) ⇒ φ<sup>(i)</sup> * ψ<sup>(i)</sup></td><td>Hypothesis</td></tr><tr><td>2</td><td>⟨*⟩(φ, ψ) ⇒ ¬alloc(x)</td><td>PC, def. of ⟨*⟩(φ, ψ), see above</td></tr><tr><td>3</td><td>⟨*⟩(φ, ψ) ⇒ ¬alloc(x) ∧ (φ<sup>(i)</sup> * ψ<sup>(i)</sup>)</td><td>PC, 1, 2</td></tr><tr><td>4</td><td>¬alloc(x) ∧ (φ<sup>(i)</sup> * ψ<sup>(i)</sup>) ⇒ (φ<sup>(i)</sup> ∧ ¬alloc(x)) * ψ<sup>(i)</sup></td><td>(I<sub>5.2.4</sub><sup>*</sup>)</td></tr><tr><td>5</td><td>⟨*⟩(φ, ψ) ⇒ (φ<sup>(i)</sup> ∧ ¬alloc(x)) * ψ<sup>(i)</sup></td><td>⇒-Tr, 3, 4</td></tr></table>
• Otherwise, $alloc(x) \subseteq_{\mathrm{Lt}} \psi$. By assumption, $alloc(x) \subseteq_{\mathrm{Lt}} \psi^{(i)}$.

<table><tr><td>1</td><td>ψ<sup>(i)</sup> ⇒ ψ<sup>(i)</sup> ∧ alloc(x)</td><td>PC, see above</td></tr><tr><td>2</td><td>⟨∗⟩(φ, ψ) ⇒ φ<sup>(i)</sup> * ψ<sup>(i)</sup></td><td>Hypothesis</td></tr><tr><td>3</td><td>φ<sup>(i)</sup> * ψ<sup>(i)</sup> ⇒ (ψ<sup>(i)</sup> ∧ alloc(x)) * φ<sup>(i)</sup></td><td>(A<sub>7</sub><sup>*</sup>), <sup>-Intro</sup>, 1</td></tr><tr><td>4</td><td>(ψ<sup>(i)</sup> ∧ alloc(x)) * φ<sup>(i)</sup> ⇒ ψ<sup>(i)</sup> * (φ<sup>(i)</sup> ∧ ¬alloc(x))</td><td>(I<sub>5.2.3</sub><sup>*</sup>)</td></tr><tr><td>5</td><td>ψ<sup>(i)</sup> * (φ<sup>(i)</sup> ∧ ¬alloc(x)) ⇒ (φ<sup>(i)</sup> ∧ ¬alloc(x)) * ψ<sup>(i)</sup></td><td>(A<sub>7</sub><sup>*</sup>)</td></tr><tr><td>6</td><td>⟨∗⟩(φ, ψ) ⇒ (φ<sup>(i)</sup> ∧ ¬alloc(x)) * ψ<sup>(i)</sup></td><td>⇒ <sup>-Tr</sup>, 2, 3, 4, 5</td></tr></table>

case: $L = x \leftrightarrow y$: Similar to the case $L = alloc(x)$. Since $\varphi$ is a satisfiable core type, we have $alloc(x) \subseteq_{\mathrm{Lt}} \varphi$ (see axiom (A<sub>3</sub><sup>C</sup>)). By assumption, $alloc(x) \subseteq_{\mathrm{Lt}} \varphi^{(i)}$. By definition of $\langle * \rangle(\varphi, \psi)$, we have $x \leftrightarrow y \subseteq_{\mathrm{Lt}} \langle * \rangle(\varphi, \psi)$.

<table><tr><td>1</td><td>φ<sup>(i)</sup> ⇒ φ<sup>(i)</sup> ∧ alloc(x)</td><td>PC, see above</td></tr><tr><td>2</td><td>⟨*⟩(φ, ψ) ⇒ φ<sup>(i)</sup> * ψ<sup>(i)</sup></td><td>Hypothesis</td></tr><tr><td>3</td><td>⟨*⟩(φ, ψ) ⇒ x ↪→ y</td><td>PC, see above</td></tr><tr><td>4</td><td>φ<sup>(i)</sup> * ψ<sup>(i)</sup> ⇒ (φ<sup>(i)</sup> ∧ alloc(x)) * ψ<sup>(i)</sup></td><td><sup>-Intro</sup>, 1</td></tr><tr><td>5</td><td>⟨*⟩(φ, ψ) ⇒ x ↪→ y ∧ ((φ<sup>(i)</sup> ∧ alloc(x)) * ψ<sup>(i)</sup>)</td><td>PC, 3, 4</td></tr><tr><td>6</td><td>x ↪→ y ∧ ((φ<sup>(i)</sup> ∧ alloc(x)) * ψ<sup>(i)</sup>) ⇒ (φ<sup>(i)</sup> ∧ x ↪→ y) * ψ<sup>(i)</sup></td><td>(I<sub>5.2.6</sub><sup>*</sup>)</td></tr><tr><td>7</td><td>⟨*⟩(φ, ψ) ⇒ (φ<sup>(i)</sup> ∧ x ↪→ y) * ψ<sup>(i)</sup></td><td><sup>-Intro</sup>, 5, 6</td></tr></table>

Without loss of generality, thanks to the previous cases dealing with $\neg alloc(x)$ literals, below we assume that for every $\neg alloc(x) \subseteq_{\mathrm{Lt}} \varphi$ and every $\neg alloc(y) \subseteq_{\mathrm{Lt}} \psi$, we have $\neg alloc(x) \subseteq_{\mathrm{Lt}} \varphi^{(i)}$ and $\neg alloc(y) \subseteq_{\mathrm{Lt}} \psi^{(i)}$.

case: $L = \neg x \leftrightarrow y$: We distinguish two main subcases

• First, suppose $alloc(x) \subseteq_{\mathrm{Lt}} \varphi$. In this case, by definition of $\langle * \rangle(\varphi, \psi)$, we have $\neg x \leftrightarrow y \subseteq_{\mathrm{Lt}} \langle * \rangle(\varphi, \psi)$. Therefore,

<table><tr><td>1</td><td>⟨*⟩(φ, ψ) ⇒ ¬x ↪→ y</td><td>PC, see above</td></tr><tr><td>2</td><td>⟨*⟩(φ, ψ) ⇒ φ<sup>(i)</sup> * ψ<sup>(i)</sup></td><td>Hypothesis</td></tr><tr><td>3</td><td>⟨*⟩(φ, ψ) ⇒ ¬x ↪→ y ∧ (φ<sup>(i)</sup> * ψ<sup>(i)</sup>)</td><td>PC, 1, 2</td></tr><tr><td>4</td><td>¬x ↪→ y ∧ (φ<sup>(i)</sup> * ψ<sup>(i)</sup>) ⇒ (φ<sup>(i)</sup> ∧ ¬x ↪→ y) * ψ<sup>(i)</sup></td><td>(I<sub>5.2.7</sub><sup>*</sup>)</td></tr></table>

• Otherwise, we have $\neg alloc(x) \subseteq_{\mathrm{Lt}} \varphi$. By assumption, $\neg alloc(x) \subseteq_{\mathrm{Lt}} \varphi^{(i)}$, and thus

<table><tr><td>1</td><td>φ<sup>(i)</sup> ⇒ ¬alloc(x)</td><td>PC, see above</td></tr><tr><td>2</td><td>¬alloc(x) ⇒ ¬x ↪→ y</td><td>(A<sub>3</sub><sup>C</sup>), PC</td></tr><tr><td>3</td><td>φ<sup>(i)</sup> ⇒ ¬x ↪→ y</td><td>⇒ <sup>-Tr</sup>, 1, 2</td></tr><tr><td>4</td><td>φ<sup>(i)</sup> ⇒ φ<sup>(i)</sup> ∧ ¬x ↪→ y</td><td>PC, 3</td></tr><tr><td>5</td><td>⟨*⟩(φ, ψ) ⇒ φ<sup>(i)</sup> * ψ<sup>(i)</sup></td><td>Hypothesis</td></tr></table>
$$6 \quad | \quad \varphi^{(i)} * \psi^{(i)} \Rightarrow (\varphi^{(i)} \wedge \neg x \leftrightarrow y) * \psi^{(i)} \qquad \textbf{*-Intro, 4}$$

$$7 \quad | \quad \langle * \rangle(\varphi, \psi) \Rightarrow (\varphi^{(i)} \wedge \neg x \leftrightarrow y) * \psi^{(i)} \qquad \Rightarrow \textbf{-Tr}, 5, 6$$

**case:** $L = \mathbf{size} \ge \beta$: By definition of $\max_{\mathbf{size}}(.)$, $\beta \le \max_{\mathbf{size}}(\varphi)$. By definition of $\varphi^{(1)}$, $\mathbf{size} \ge \max_{\mathbf{size}}(\varphi) \subseteq \mathbf{Lt} \varphi^{(1)}$. From $\varphi^{(1)} \subseteq \mathbf{Lt} \varphi^{(i)}$, we get $\mathbf{size} \ge \max_{\mathbf{size}}(\varphi) \subseteq \mathbf{Lt} \varphi^{(i)}$.

$$1 \quad | \quad \varphi^{(i)} \Rightarrow \mathbf{size} \ge \max_{\mathbf{size}}(\varphi) \qquad \text{PC, see above}$$

$$2 \quad | \quad \mathbf{size} \ge \max_{\mathbf{size}}(\varphi) \Rightarrow \mathbf{size} \ge \beta \qquad \text{repeated } (\mathbf{I}_5^c), \text{ PC, as } \beta \le \max_{\mathbf{size}}(\varphi)$$

$$3 \quad | \quad \varphi^{(i)} \Rightarrow \varphi^{(i)} \wedge \mathbf{size} \ge \beta \qquad \text{PC, 1, 2}$$

$$4 \quad | \quad \langle * \rangle(\varphi, \psi) \Rightarrow \varphi^{(i)} * \psi^{(i)} \qquad \text{Hypothesis}$$

$$5 \quad | \quad \varphi^{(i)} * \psi^{(i)} \Rightarrow (\varphi^{(i)} \wedge \mathbf{size} \ge \beta) * \psi^{(i)} \qquad \textbf{*-Intro, 3}$$

$$6 \quad | \quad \langle * \rangle(\varphi, \psi) \Rightarrow (\varphi^{(i)} \wedge \mathbf{size} \ge \beta) * \psi^{(i)} \qquad \Rightarrow \textbf{-Tr}, 4, 5$$

**case:** $L = \neg \mathbf{size} \ge \beta$: In this case, $\max_{\mathbf{size}}(\varphi) < \alpha$. Since $\varphi$ is a satisfiable core type, we have $\beta > \max_{\mathbf{size}}(\varphi)$. Moreover, by definition of $\varphi^{(1)}$, $\neg \mathbf{size} \ge \max_{\mathbf{size}}(\varphi) + 1 \subseteq \mathbf{Lt} \varphi^{(1)}$. From $\varphi^{(1)} \subseteq \mathbf{Lt} \varphi^{(i)}$, we have $\neg \mathbf{size} \ge \max_{\mathbf{size}}(\varphi) + 1 \subseteq \mathbf{Lt} \varphi^{(i)}$.

$$1 \quad | \quad \varphi^{(i)} \Rightarrow \neg \mathbf{size} \ge \max_{\mathbf{size}}(\varphi) + 1 \qquad \text{PC, see above}$$

$$2 \quad | \quad \neg \mathbf{size} \ge \max_{\mathbf{size}}(\varphi) + 1 \Rightarrow \neg \mathbf{size} \ge \beta \qquad \text{repeated } (\mathbf{I}_5^c), \text{ PC, as } \beta > \max_{\mathbf{size}}(\varphi) \\ \text{by PC, the contrapositive of } (\mathbf{I}_5^c) \text{ is derivable}$$

$$3 \quad | \quad \varphi^{(i)} \Rightarrow \varphi^{(i)} \wedge \neg \mathbf{size} \ge \beta \qquad \text{PC, 1, 2}$$

$$4 \quad | \quad \langle * \rangle(\varphi, \psi) \Rightarrow \varphi^{(i)} * \psi^{(i)} \qquad \text{Hypothesis}$$

$$5 \quad | \quad \varphi^{(i)} * \psi^{(i)} \Rightarrow (\varphi^{(i)} \wedge \neg \mathbf{size} \ge \beta) * \psi^{(i)} \qquad \textbf{*-Intro, 3}$$

$$6 \quad | \quad \langle * \rangle(\varphi, \psi) \Rightarrow (\varphi^{(i)} \wedge \neg \mathbf{size} \ge \beta) * \psi^{(i)} \qquad \Rightarrow \textbf{-Tr}, 4, 5 \quad \square$$

**Corollary 5.5 (Star elimination).** Let $X \subseteq_{\text{fin}} \text{VAR}$ and $\alpha \ge \text{card}(X)$. Let $\varphi$ and $\psi$ in $\text{CoreTypes}(X, \alpha)$. There is $\chi$ in $\text{Conj}(\text{Core}(X, 2\alpha))$ such that $\vdash_{\mathcal{H}_C(*)} \varphi * \psi \Leftrightarrow \chi$.

*Proof.* If both $\varphi$ and $\psi$ are satisfiable, the results holds directly by Lemma 5.4, as $\langle * \rangle(\varphi, \psi)$ is in $\text{Conj}(\text{Core}(X, \alpha + \alpha))$. Otherwise, let us treat the case where one of the two formulas is unsatisfiable. For instance, assume that $\varphi$ is unsatisfiable. Then $\vdash_{\mathcal{H}_C} \varphi \Rightarrow \bot$ by completeness of $\mathcal{H}_C$ (Lemma 4.1) and, $\mathcal{H}_C(*)$ includes $\mathcal{H}_C$, $\vdash_{\mathcal{H}_C(*)} \varphi \Rightarrow \bot$. By the rule $\textbf{*-Intro}$ and by the axiom $(\mathbf{I}_{10}^*)$, we get $\vdash_{\mathcal{H}_C(*)} \varphi * \psi \Rightarrow \bot$. Thus $\chi$ can take the value $\neg (x = x)$. The case where $\psi$ is not satisfiable is analogous, thanks to $(\mathbf{A}_7^*)$. $\square$

By the distributivity axiom $(\mathbf{I}_9^*)$, Corollary 5.5 is extended from core types to arbitrary Boolean combinations of core formulae. $\mathcal{H}_C(*)$ is therefore complete for $\text{SL}(*, \text{alloc})$. In order to derive a valid formula $\varphi \in \text{SL}(*, \text{alloc})$, we repeatedly apply the elimination of $*$ in a bottom-up fashion, starting from the leaves of $\varphi$ (which are Boolean combinations of core formulae) and obtaining a Boolean combination of core formulae $\psi$ that is equivalent to $\varphi$. Then, we rely on the completeness of $\mathcal{H}_C$ (Theorem 4.3) to prove that $\psi$ is derivable.

**Theorem 5.6.** A formula $\varphi$ in $\text{SL}(*, \text{alloc})$ is valid iff $\vdash_{\mathcal{H}_C(*)} \varphi$.
*Proof.* Soundness of the proof system $\mathcal{H}_C(*)$ has been already established earlier.

As far as the completeness proof is concerned, we need to show that for every formula $\varphi$ in $\text{SL}(*, \text{alloc})$, there is a Boolean combination of core formulae $\psi$ such that $\vdash_{\mathcal{H}_C(*)} \varphi \Leftrightarrow \psi$. In order to conclude the proof, when $\varphi$ is valid for $\text{SL}(*, \text{alloc})$, by soundness of $\mathcal{H}_C(*)$, we obtain that $\psi$ is valid too and therefore $\vdash_{\mathcal{H}_C(*)} \psi$ as $\mathcal{H}_C$ is a subsystem of $\mathcal{H}_C(*)$ and $\mathcal{H}_C$ is complete by Theorem 4.3. By propositional reasoning, we get that $\vdash_{\mathcal{H}_C(*)} \varphi$.

To show that every formula $\varphi$ has a provably equivalent Boolean combination of core formulae, we heavily rely on Corollary 5.5. The proof is by simple induction on the number of occurrences of $*$ in $\varphi$ that are not involved in the definition of some core formula of the form $\mathbf{size} \ge \beta$. For the base case, when $\varphi$ has no occurrence of the separating conjunction, $x = y$ and $x \leftrightarrow y$ are already core formulae, and $\text{emp}$ is logically equivalent to $\neg \mathbf{size} \ge 1$.

Before performing the induction step, let us observe that in $\mathcal{H}_C(*)$, the replacement of provably equivalent formulae holds true, which is stated as follows:

**R0** Let $\varphi, \varphi'$ and $\psi$ be formulae of $\text{SL}(*, \text{alloc})$ such that $\vdash_{\mathcal{H}_C(*)} \varphi \Leftrightarrow \varphi'$. Then,

$$ \vdash_{\mathcal{H}_C(*)} \psi[\varphi]_{\rho} \Rightarrow \psi[\varphi']_{\rho} $$

Above, $\psi[\varphi]_{\rho}$ refers to the formula $\psi$ in which the subformula at the occurrence $\rho$ (in the standard sense) is replaced by $\varphi$. ($\varphi$ and $\varphi'$ are therefore placed at the same occurrence.)

To prove **R0**, we first note that the following rules can be shown admissible in $\mathcal{H}_C(*)$:

$$ \frac{\varphi \Leftrightarrow \varphi'}{\neg \varphi \Leftrightarrow \neg \varphi'} \qquad \frac{\varphi \Leftrightarrow \varphi'}{\varphi \lor \psi \Leftrightarrow \varphi' \lor \psi} \qquad \frac{\varphi \Leftrightarrow \varphi'}{\varphi \land \psi \Leftrightarrow \varphi' \land \psi} $$

Admissibility of such rules is a direct consequence of the presence of axioms and modus ponens for the propositional calculus. As a consequence of the presence of the rule $\text{*-Intro}$ in $\mathcal{H}_C(*)$, the rule below is also admissible:

$$ \frac{\varphi \Leftrightarrow \varphi'}{\varphi * \psi \Leftrightarrow \varphi' * \psi} $$

Consequently, by structural induction on $\psi$, one can conclude that $\vdash_{\mathcal{H}_C(*)} \varphi \Leftrightarrow \varphi'$ implies $\vdash_{\mathcal{H}_C(*)} \psi[\varphi]_{\rho} \Rightarrow \psi[\varphi']_{\rho}$ (the axiom $(\mathbf{A}_7^*)$ needs to be used here).

Assume that $\varphi$ is a formula in $\text{SL}(*, \text{alloc})$ with $n + 1$ occurrences of the separating conjunction not involved in the definition of some $\mathbf{size} \ge \beta$ ($n \ge 0$). Let $\psi$ be a subformula of $\varphi$ (at the occurrence $\rho$) of the form $\psi_1 * \psi_2$ such that $\psi_1$ and $\psi_2$ are Boolean combinations of core formulae, in $\text{Bool}({\text{Core}(X, \alpha_1)})$ and $\text{Bool}({\text{Core}(X, \alpha_2)})$. By pure propositional reasoning, one can show that there are formulae in disjunctive normal form $\psi_1^1 \lor \dots \lor \psi_1^{n_1}$ and $\psi_2^1 \lor \dots \lor \psi_2^{n_2}$ such that $\vdash_{\mathcal{H}_C} \psi_i \Leftrightarrow \psi_i^1 \lor \dots \lor \psi_i^{n_i}$ for $i \in \{1, 2\}$ and moreover, all the $\psi_i^{j_i}$'s are core types in $\text{CoreTypes}(X, \max(\text{card}(X), \alpha_1, \alpha_2))$. Again, by using propositional reasoning but this time using also the axiom $(\mathbf{I}_9^*)$ for distributivity, we have

$$ \vdash_{\mathcal{H}_C(*)} \psi_1 * \psi_2 \Leftrightarrow \bigvee_{j_1 \in [1, n_1], j_2 \in [1, n_2]} \psi_1^{j_1} * \psi_2^{j_2}. $$

We now rely on Corollary 5.5 and derive that there is a conjunction of core formulae $\psi_{1,j_1}, \psi_{2,j_2}$ in $\text{Conj}({\text{Core}(X, 2 \max(\text{card}(X), \alpha_1, \alpha_2)})}$ such that $\vdash_{\mathcal{H}_C(*)} \psi_1^{j_1} * \psi_2^{j_2} \Leftrightarrow \psi_{1,j_1}, \psi_{2,j_2}$. By propositional reasoning, we get

$$ \vdash_{\mathcal{H}_C(*)} \psi_1 * \psi_2 \Leftrightarrow \bigvee_{j_1 \in [1, n_1], j_2 \in [1, n_2]} \psi_{1,j_1}, \psi_{2,j_2}. $$
$$ (A_{21}^*) (\text{size} = 1 \land \bigwedge_{x \in X} \neg \text{alloc}(x)) \otimes \top \{X \subseteq \text{fin VAR}] $$

$$ (A_{22}^*) \neg \text{alloc}(x) \Rightarrow ((x \leftrightarrow y \land \text{size} = 1) \otimes \top) $$

$$ (A_{23}^*) \neg \text{alloc}(x) \Rightarrow ((\text{alloc}(x) \land \text{size} = 1 \land \bigwedge_{y \in X} \neg x \leftrightarrow y) \otimes \top) \{X \subseteq \text{fin VAR}] $$

$$ \begin{array}{l} \text{-Adj}: \frac{\varphi * \psi \Rightarrow \chi}{\varphi \Rightarrow (\psi * \chi)} & \text{-Adj}: \frac{\varphi \Rightarrow (\psi * \chi)}{\varphi * \psi \Rightarrow \chi} \\ \hline \end{array} $$

Figure 7: Additional axioms and rules for handling the separating implication.

Consequently (thanks to the property R0), we obtain

$$ \vdash_{\mathcal{H}_C(*)} \varphi \Leftrightarrow \varphi \left[ \bigvee_{j_1 \in [1, n_1], j_2 \in [1, n_2]} \psi^{j_1, j_2} \right]_{\rho} $$

Note that the right-hand side formula has $n$ occurrences of the separating conjunction that are not involved in the definition of some core formula of the form $\mathbf{size} \ge \beta$. The induction hypothesis applies, which concludes the proof. $\square$

## 6. A CONSTRUCTIVE ELIMINATION OF $\text{-Adj}$ LEADING TO FULL COMPLETENESS

In order to obtain the final proof system $\mathcal{H}_C(*, \text{-Adj})$, we add the axioms and rules from Figure 7 to the proof system $\mathcal{H}_C(*)$. These new axioms and rules are dedicated to the separating implication. The axioms involving $\otimes$ (kind of dual of $\text{-Adj}$, introduced in Section 2) express that it is always possible to extend a given heap with an extra cell, and that the address and the content of this cell can be fixed arbitrarily (provided it is not already allocated). The adjunction rules $\text{-Adj}$ and $\text{-Adj}$ are from the Hilbert-style axiomatisation of Boolean BI [GLW06, Section 2]. One can observe that, in $\mathcal{H}_C(*, \text{-Adj})$, the axioms $(\mathbf{I}_9^*)$, $(\mathbf{I}_{10}^*)$ and $(\mathbf{I}_{12}^*)$ of $\mathcal{H}_C(*)$ are derivable.

**Lemma 6.1.** *The axioms $(\mathbf{I}_9^*)$, $(\mathbf{I}_{10}^*)$ and $(\mathbf{I}_{12}^*)$ are derivable in $\mathcal{H}_C(*, \text{-Adj})$.*

The derivations of $(\mathbf{I}_9^*)$, $(\mathbf{I}_{10}^*)$ and $(\mathbf{I}_{12}^*)$ that lead to Lemma 6.1 are given in Appendix C.

Fundamentally, $\mathcal{H}_C(*, \text{-Adj})$ enjoys the $\text{-Adj}$ elimination property, as shown below. Actually, we state the property with the help of $\otimes$ as we find the related statements and developments more intuitive.

**Lemma 6.2.** Let $X \subseteq \text{fin VAR}$ and $\alpha \ge \text{card}(X)$. Let $\varphi$ and $\psi$ in CoreTypes$(X, \alpha)$. There is a conjunction $\chi \in \text{Conj}(\text{Core}(X, \alpha))$ such that $\vdash_{\mathcal{H}_C(*, \text{-Adj})} (\varphi \otimes \psi) \Leftrightarrow \chi$.

*Structure of the proof of Lemma 6.2.* In the proof of Lemma 6.2, the formula $\chi$ is explicitly constructed from $\varphi$ and $\psi$, following a pattern analogous to the construction of $\langle * \rangle(.,.)$ in Figure 6 (see forthcoming Figure 8). The derivation of the equivalence $(\varphi \otimes \psi) \Leftrightarrow \chi$ is shown as follows. First, the formulae $\chi * \varphi \Rightarrow \psi$ and $\neg \chi * \varphi \Rightarrow \neg \psi$ are shown valid (by using semantical means). As $\mathcal{H}_C(*)$ is complete for SL$(*, \text{alloc})$, it is a subsystem of $\mathcal{H}_C(*, \text{-Adj})$, and the formulae $\varphi$, $\psi$ and $\chi$ are Boolean combinations of core formulae, we get $\vdash_{\mathcal{H}_C(*, \text{-Adj})} \chi * \varphi \Rightarrow \psi$ and $\vdash_{\mathcal{H}_C(*, \text{-Adj})} \neg \chi * \varphi \Rightarrow \neg \psi$. The latter theorem leads to $\vdash_{\mathcal{H}_C(*, \text{-Adj})} (\varphi \otimes \psi) \Rightarrow \chi$ by using the definition of $\otimes$ and the rule $\text{-Adj}$. For the other direction, in order to show that $\vdash_{\mathcal{H}_C(*, \text{-Adj})} \chi \Rightarrow (\varphi \otimes \psi)$ holds, we take advantage of the admissibility of the theorem $(\mathbf{I}_{6.3.9}^*)$ (see Lemma 6.3) for which an instance is $(\varphi \otimes \top) \land (\varphi * \psi) \Rightarrow (\varphi \otimes (\top \land \psi))$. From $\vdash_{\mathcal{H}_C(*, \text{-Adj})} \chi * \varphi \Rightarrow \psi$ and by $\text{-Adj}$ we
have $\vdash_{\mathcal{H}_C(*,*)} \chi \Rightarrow (\varphi * \psi)$. Therefore, the main technical development lies in the proof of $\vdash_{\mathcal{H}_C(*,*)} \chi \Rightarrow (\varphi * \top)$, which allows us to take advantage of $(\mathbf{I}_{6.3.9}^*)$, and leads to $\vdash_{\mathcal{H}_C(*,*)} \chi \Rightarrow (\varphi * \psi)$ by propositional reasoning.

In order to formalise the proof of Lemma 6.2 sketched above, we start by establishing several admissible axioms and rules (Lemma 6.3). Afterwards, we define the formula $\chi$ and show the validity of $\chi * \varphi \Rightarrow \psi$ and $\neg \chi * \varphi \Rightarrow \neg \psi$ (Lemma 6.4). Then, come the final bits of the proof of Lemma 6.2 (see page 35).

**Lemma 6.3.** The following rules and axioms are admissible in $\mathcal{H}_C(*,*)$:

$$(\mathbf{I}_{6.3.1}^*) \perp \otimes \varphi \Rightarrow \perp$$

$$(\mathbf{I}_{6.3.2}^*) \varphi \otimes \perp \Rightarrow \perp$$

$$(\mathbf{I}_{6.3.3}^*) \varphi * (\varphi * \psi) \Rightarrow \psi$$

$$(\mathbf{I}_{6.3.4}^*) \frac{\varphi \Rightarrow \psi}{\varphi \otimes \chi \Rightarrow \psi \otimes \chi}$$

$$(\mathbf{I}_{6.3.5}^*) \frac{\varphi \Rightarrow \psi}{\chi \otimes \varphi \Rightarrow \chi \otimes \psi}$$

$$(\mathbf{I}_{6.3.6}^*) \varphi \otimes (\psi \otimes \chi) \Leftrightarrow (\varphi * \psi) \otimes \chi$$

$$(\mathbf{I}_{6.3.7}^*) (\varphi \vee \psi) \otimes \chi \Leftrightarrow (\varphi \otimes \chi) \vee (\psi \otimes \chi)$$

$$(\mathbf{I}_{6.3.8}^*) \chi \otimes (\varphi \vee \psi) \Leftrightarrow (\chi \otimes \varphi) \vee (\chi \otimes \psi)$$

$$(\mathbf{I}_{6.3.9}^*) (\varphi \otimes \psi) \wedge (\varphi * \chi) \Rightarrow (\varphi \otimes \psi \wedge \chi)$$

$$(\mathbf{I}_{6.3.10}^*) \mathbf{x} = \mathbf{y} \wedge (\varphi \otimes \psi) \Rightarrow (\varphi \wedge \mathbf{x} = \mathbf{y} \otimes \psi)$$

$$(\mathbf{I}_{6.3.11}^*) \mathbf{x} \neq \mathbf{y} \wedge (\varphi \otimes \psi) \Rightarrow (\varphi \wedge \mathbf{x} \neq \mathbf{y} \otimes \psi)$$

$$(\mathbf{I}_{6.3.12}^*) (\varphi_{\text{size}} \wedge \bigwedge_{\mathbf{x} \in \mathbf{X}} \neg \text{alloc}(\mathbf{x})) \otimes \top,$$

where, in axiom $(\mathbf{I}_{6.3.12}^*)$, $\mathbf{X} \subseteq_{\text{fin}} \text{VAR}$ and $\varphi_{\text{size}}$ is a satisfiable conjunction of literals of the form $\text{size} \ge \beta_1$ or $\neg \text{size} \ge \beta_2$.

The proof of Lemma 6.3 can be found in Appendix D.

Let $\varphi$ and $\psi$ be two satisfiable core types in $\text{Conj}(\text{Core}(\mathbf{X}, \alpha))$. Following the developments of Section 5, we define a formula $\langle \text{sep} \rangle(\varphi, \psi)$ in $\text{Conj}(\text{Core}(\mathbf{X}, \alpha))$, for which we show that $\varphi \otimes \psi \Leftrightarrow \langle \text{sep} \rangle(\varphi, \psi)$ is provable in $\mathcal{H}_C(*,*)$. The formula $\langle \text{sep} \rangle(\varphi, \psi)$ is defined in Figure 8.

**Lemma 6.4.** Let $\mathbf{X} \subseteq_{\text{fin}} \text{VAR}$, $\alpha \ge \text{card}(\mathbf{X})$ and $\varphi, \psi$ be satisfiable core types in $\text{CoreTypes}(\mathbf{X}, \alpha)$. The formulae $\langle \text{sep} \rangle(\varphi, \psi) * \varphi \Rightarrow \psi$ and $\neg \langle \text{sep} \rangle(\varphi, \psi) * \varphi \Rightarrow \neg \psi$ are valid.

Before presenting the proof for Lemma 6.4, let us observe that since we aim at proving the derivability of $\varphi \otimes \psi \Leftrightarrow \langle \text{sep} \rangle(\varphi, \psi)$ in $\mathcal{H}_C(*,*)$, the validity of the formula $(\neg \langle \text{sep} \rangle(\varphi, \psi)) * \varphi \Rightarrow \neg \psi$ should not surprise the reader. Indeed, by replacing $\langle \text{sep} \rangle(\varphi, \psi)$ with $\varphi \otimes \psi$ we obtain $(\neg (\varphi \otimes \psi)) * \varphi \Rightarrow \neg \psi$ which, unfolding the definition of $\otimes$, is equivalent to the valid formula $(\varphi * \neg \varphi) * \varphi \Rightarrow \neg \psi$ (see $(\mathbf{I}_{6.3.3}^*)$ in Lemma 6.3). On the other hand, the fact that $\langle \text{sep} \rangle(\varphi, \psi) * \varphi \Rightarrow \psi$ is valid can be puzzling at first, as the formula $(\varphi \otimes \psi) * \varphi \Rightarrow \psi$ is not valid (in general). In its essence, Lemma 6.4 shows that $(\varphi \otimes \psi) * \varphi \Rightarrow \psi$ is valid whenever $\varphi$ and $\psi$ are restricted to core types.

Below, we prove that $\langle \text{sep} \rangle(\varphi, \psi) * \varphi \Rightarrow \psi$ and $(\neg \langle \text{sep} \rangle(\varphi, \psi)) * \varphi \Rightarrow \neg \psi$ are valid, thus establishing Lemma 6.4. Notice that the proof is carried out through semantical arguments. Since $\varphi, \psi$ and $\langle \text{sep} \rangle(\varphi, \psi)$ are conjunctions of literals built from core formulae, derivability of these two tautologies in $\mathcal{H}_C(*,*)$ follows from the completeness of $\mathcal{H}_C(*)$ (Theorem 5.6).

Validity of $\langle \text{sep} \rangle(\varphi, \psi) * \varphi \Rightarrow \psi$. If $\langle \text{sep} \rangle(\varphi, \psi) * \varphi$ is inconsistent, then $\langle \text{sep} \rangle(\varphi, \psi) * \varphi \Rightarrow \psi$ is straightforwardly valid. Below, we assume that $\langle \text{sep} \rangle(\varphi, \psi) * \varphi$ is satisfiable. In particular, none of the conditions depicted in Figure 8 that result in $\langle \text{sep} \rangle(\varphi, \psi)$ having a literal $\mathbf{x} \neq \mathbf{x}$ applies. Let $(s, h) \models \langle \text{sep} \rangle(\varphi, \psi) * \varphi$. Therefore, there are two disjoint heaps $h_1$ and $h_2$ such that $h = h_1+h_2$, $(s, h_1) \models \langle \text{sep} \rangle(\varphi, \psi)$ and $(s, h_2) \models \varphi$. We show that $(s, h)$ satisfies each
<figure><img src="image_7.png" /><figcaption>Figure 8: The formula $\langle sep \rangle(\varphi, \psi)$.</figcaption></figure>

literal $L$ in $\psi$. We perform a simple case analysis on the shape of $L$. Notice that, below, we have $x, y \in X$ and $\beta_2 \in [0, \alpha]$, as $\psi$ is a core type in CoreTypes($X$, $\alpha$).

**case:** $L = x \sim y$, where $\sim \in \{=, \ne\}$: By definition of $\langle sep \rangle(\varphi, \psi)$, $x \sim y \subseteq_L \langle sep \rangle(\varphi, \psi)$ and so $(s, h_1) \models x \sim y$. We conclude that $s(x) \sim s(y)$, and thus $(s, h) \models x \sim y$.

**case:** $L = \text{alloc}(x)$: If $\text{alloc}(x) \subseteq_L \varphi$, then $(s, h_2) \models \text{alloc}(x)$, which implies $s(x) \in \text{dom}(h)$ directly from $h_2 \sqsubseteq h$. Thus, $(s, h) \models \text{alloc}(x)$. Otherwise, if $\text{alloc}(x) \not\subseteq_L \varphi$ then, since $\varphi$ is a core type in CoreTypes($X$, $\alpha$), we have $\neg \text{alloc}(x) \subseteq_L \varphi$. By definition of $\langle sep \rangle(\varphi, \psi)$, we derive that $\text{alloc}(x) \subseteq_L \langle sep \rangle(\varphi, \psi)$. So, $(s, h_1) \models \text{alloc}(x)$ and thus, by $h_1 \sqsubseteq h$, $s(x) \in \text{dom}(h)$. We conclude that $(s, h) \models \text{alloc}(x)$.

**case:** $L = \neg \text{alloc}(x)$: In this case, by definition of $\langle sep \rangle(\varphi, \psi)$, we have $\neg \text{alloc}(x) \subseteq_L \langle sep \rangle(\varphi, \psi)$, which implies $(s, h_1) \models \neg \text{alloc}(x)$. Ad absurdum, suppose $(s, h_2) \models \text{alloc}(x)$. Since $\varphi$ is a core type in CoreTypes($X$, $\alpha$), we conclude that $\text{alloc}(x) \subseteq_L \varphi$. However, by definition of $\langle sep \rangle(\varphi, \psi)$, this implies $x \neq x \subseteq_L \langle sep \rangle(\varphi, \psi)$, which contradicts the fact that $\langle sep \rangle(\varphi, \psi)$ is satisfiable. Thus, $(s, h_2) \models \neg \text{alloc}(x)$, which implies $s(x) \notin \text{dom}(h_2)$. From $h = h_1+h_2$ and $s(x) \notin \text{dom}(h_1)$ we conclude that $s(x) \notin \text{dom}(h)$. So, $(s, h) \models \neg \text{alloc}(x)$.

**case:** $L = x \leftrightarrow y$: If $\neg \text{alloc}(x) \subseteq_L \varphi$, then $x \leftrightarrow y \subseteq_L \langle sep \rangle(\varphi, \psi)$ holds by definition of $\langle sep \rangle(\varphi, \psi)$. So, $h_1(s(x)) = s(y)$ and, from $h_1 \sqsubseteq h$ we conclude that $(s, h) \models x \leftrightarrow y$. Otherwise, let us assume that $\text{alloc}(x) \subseteq_L \varphi$. Ad absurdum, suppose $\neg x \leftrightarrow y \subseteq_L \varphi$. Then, by definition of $\langle sep \rangle(\varphi, \psi)$, we derive $x \neq x \subseteq_L \langle sep \rangle(\varphi, \psi)$. However, this contradicts the satisfiability of $\langle sep \rangle(\varphi, \psi)$. Therefore, $\neg x \leftrightarrow y \not\subseteq_L \varphi$. Since $\varphi$ is a core type, this implies $x \leftrightarrow y \subseteq_L \varphi$, and therefore $h_2(s(x)) = s(y)$. From $h_2 \sqsubseteq h$ we conclude that $(s, h) \models x \leftrightarrow y$.

**case:** $L = \neg x \leftrightarrow y$: By definition of $\langle sep \rangle(x, y)$, we have $\neg x \leftrightarrow y \subseteq_L \langle sep \rangle(x, y)$, which implies that if $s(x) \in \text{dom}(h_1)$ then $h_1(s(x)) \neq s(y)$. Ad absurdum, suppose $x \leftrightarrow y \subseteq_L \varphi$. Then, by definition of $\langle sep \rangle(\varphi, \psi)$, we derive $x \neq x \subseteq_L \langle sep \rangle(\varphi, \psi)$. However, this contradicts the satisfiability of $\langle sep \rangle(\varphi, \psi)$. Therefore $x \leftrightarrow y \not\subseteq_L \varphi$ and, since $\varphi$ is a core type, the fact that $h_1(s(x)) \neq s(y)$, we conclude that $(s, h) \models \neg x \leftrightarrow y$.

**case:** $L = \text{size} \geq \beta_2$: If $\text{size} \geq \alpha \subseteq_L \varphi$, then $\text{card}(\text{dom}(h)) \geq \text{card}(\text{dom}(h_2)) \geq \alpha$, by $h_2 \sqsubseteq h$. As $\beta_2 \in [0, \alpha]$, this implies $(s, h) \models \text{size} \geq \beta_2$. Otherwise, assume $\text{size} \geq \alpha \not\subseteq_L \varphi$.
In particular, since $\varphi$ is in $\text{CoreTypes}(X, \alpha)$, this implies that $\max_{\text{size}}(\varphi) < \alpha$ and

$$ \text{size} \geq \max_{\text{size}}(\varphi) \wedge \neg \text{size} \geq \max_{\text{size}}(\varphi) + 1 \subseteq \text{Lt} \ \varphi. $$

We have $\text{card}(\text{dom}(h_2)) = \max_{\text{size}}(\varphi)$. If $\max_{\text{size}}(\varphi) \ge \beta_2$, then from $h_2 \subseteq h$ we conclude that $(s, h) \models \text{size} \ge \beta_2$. Otherwise, let us assume $\beta_2 > \max_{\text{size}}(\varphi)$. By definition of $\langle \text{sep} \rangle(\varphi, \psi)$, we conclude that $\text{size} \ge \beta_2 + 1 \div (\max_{\text{size}}(\varphi) + 1) \subseteq \text{Lt} \langle \text{sep} \rangle(\varphi, \psi)$. Together with $\beta_2 > \max_{\text{size}}(\varphi)$, this implies $\text{card}(\text{dom}(h_1)) \ge \beta_2 - \max_{\text{size}}(\varphi)$. With $\text{card}(\text{dom}(h_2)) = \max_{\text{size}}(\varphi)$ and $h = h_1+h_2$, this implies $(s, h) \models \text{size} \ge \beta_2$.

**case:** $L = \neg \text{size} \ge \beta_2$: Ad absurdum, suppose that $\text{size} \ge \alpha \subseteq \text{Lt} \ \varphi$. Then, by definition of $\langle \text{sep} \rangle(\varphi, \psi)$ we have $\neg \text{size} \ge \beta_2 \div \alpha \subseteq \text{Lt} \langle \text{sep} \rangle(\varphi, \psi)$. However, since $\beta_2 \in [0, \alpha]$, this means that $\neg \text{size} \ge 0 \subseteq \text{Lt} \langle \text{sep} \rangle(\varphi, \psi)$, which contradicts the satisfiability of $\langle \text{sep} \rangle(\varphi, \psi)$. Therefore, $\text{size} \ge \alpha \notin \text{Lt} \ \varphi$. As $\varphi$ is in $\text{CoreTypes}(X, \alpha)$, we derive $\max_{\text{size}}(\varphi) < \alpha$ and

$$ \text{size} \geq \max_{\text{size}}(\varphi) \wedge \neg \text{size} \geq \max_{\text{size}}(\varphi) + 1 \subseteq \text{Lt} \ \varphi. $$

We conclude that $\text{card}(\text{dom}(h_2)) \le \max_{\text{size}}(\varphi)$. From $\text{size} \ge \max_{\text{size}}(\varphi) \subseteq \text{Lt} \ \varphi$ and by definition of $\langle \text{sep} \rangle(\varphi, \psi)$, we conclude that

$$ \neg \text{size} \geq \beta_2 \div \max_{\text{size}}(\varphi) \subseteq \text{Lt} \langle \text{sep} \rangle(\varphi, \psi). $$

If $\beta_2 \le \max_{\text{size}}(\varphi)$, then $\neg \text{size} \ge 0 \subseteq \text{Lt} \langle \text{sep} \rangle(\varphi, \psi)$, which contradicts the satisfiability of $\langle \text{sep} \rangle(\varphi, \psi)$. Therefore, $\beta_2 > \max_{\text{size}}(\varphi)$. So, $\text{card}(\text{dom}(h_1)) < \beta_2 - \max_{\text{size}}(\varphi)$. Together with $\text{card}(\text{dom}(h_2)) \le \max_{\text{size}}(\varphi)$ and $h = h_1+h$, we conclude that $\text{card}(\text{dom}(h)) < \beta_2$, and thus $(s, h) \models \neg \text{size} \ge \beta_2$. $\square$

Validity of $(\neg \langle \text{sep} \rangle(\varphi, \psi)) * \varphi \Rightarrow \neg \psi$. Let us assume $(s, h) \models (\neg \langle \text{sep} \rangle(\varphi, \psi)) * \varphi$. Consequently, there is a literal $L$ of $\langle \text{sep} \rangle(\varphi, \psi)$ such that $(s, h) \models (\neg L) * \varphi$ holds. We show that $(s, h) \models \neg \psi$. Let $h_1$ and $h_2$ be two disjoint heaps such that $h = h_1+h_2$, $(s, h_1) \models \neg L$ and $(s, h_2) \models \varphi$. We perform a case analysis on the shape of $L$. As in the previous part of the proof, recall that $x, y \in X$ and $\beta_1, \beta_2 \in [0, \alpha]$.

**case:** $L = x \neq x$: Since $\varphi$ and $\psi$ are satisfiable, by definition of $\langle \text{sep} \rangle(\varphi, \psi)$, the fact that $x \neq x \subseteq \text{Lt} \langle \text{sep} \rangle(\varphi, \psi)$ implies that one of the following three cases holds:

1: $\text{alloc}(x) \wedge \neg x \leftrightarrow y \subseteq \text{Lt} \ \varphi$ and $x \leftrightarrow y \subseteq \text{Lt} \ \psi$.

From $\text{alloc}(x) \wedge \neg x \leftrightarrow y \subseteq \text{Lt} \ \varphi$ and $h_2 \subseteq h$, we have $s(x) \in \text{dom}(h)$ and $h(s(x)) \neq s(y)$.

Thus $(s, h) \models x \leftrightarrow y$, and so, by $x \leftrightarrow y \subseteq \text{Lt} \ \psi$, $(s, h) \models \neg \psi$.

2: $x \leftrightarrow y \subseteq \text{Lt} \ \varphi$ and $\neg x \leftrightarrow y \subseteq \text{Lt} \ \psi$.

From $x \leftrightarrow y \subseteq \text{Lt} \ \varphi$ and $h_2 \subseteq h$, $h(s(x)) = s(y)$. Thus $(s, h) \models x \leftrightarrow y$ and so, by

$\neg x \leftrightarrow y \subseteq \text{Lt} \ \psi$, $(s, h) \models \neg \psi$.

3: $\text{alloc}(x) \subseteq \text{Lt} \ \varphi$ and $\neg \text{alloc}(x) \subseteq \text{Lt} \ \psi$.

From $\text{alloc}(x) \subseteq \text{Lt} \ \varphi$ and $h_2 \subseteq h$, $s(x) \in \text{dom}(h)$. Thus $(s, h) \models \text{alloc}(x)$ and so, by

$\neg \text{alloc}(x) \subseteq \text{Lt} \ \psi$, $(s, h) \models \neg \psi$.

**case:** $L = x \sim y$, where $\sim \in \{=, \ne\}$: In this case, since $(s, h_1) \models \neg L$, then we have $(s, h) \models \neg L$. Now, it cannot be that $L \subseteq \text{Lt} \ \varphi$, as it would imply $(s, h) \models L$, which is contradictory. Therefore, by definition of $\langle \text{sep} \rangle(\varphi, \psi)$, we must have $L \subseteq \text{Lt} \ \psi$. This implies $(s, h) \models \neg \psi$.

**case:** $L = \text{alloc}(x)$: By definition of $\langle \text{sep} \rangle(\varphi, \psi)$, $\neg \text{alloc}(x) \subseteq \text{Lt} \ \varphi$ and $\text{alloc}(x) \subseteq \text{Lt} \ \psi$. From $(s, h_1) \models \neg \text{alloc}(x)$ we conclude that $s(x) \notin \text{dom}(h_1)$. By $\neg \text{alloc}(x) \subseteq \text{Lt} \ \varphi$, $s(x) \notin \text{dom}(h_2)$. By $h = h_1+h_2$, $s(x) \notin \text{dom}(h)$. As $\text{alloc}(x) \subseteq \text{Lt} \ \psi$, $(s, h) \models \neg \psi$.

**case:** $L = \neg \text{alloc}(x)$: As $(s, h_1) \models \neg L$, we have $s(x) \in \text{dom}(h_1)$. According to the definition of $\langle \text{sep} \rangle(\varphi, \psi)$, either $\text{alloc}(x) \subseteq \text{Lt} \ \varphi$ or $\neg \text{alloc}(x) \subseteq \text{Lt} \ \psi$. The first case
cannot hold, as it implies $s(x) \in \text{dom}(h_2)$ which contradicts the fact that $h_1$ and $h_2$ are disjoint. In the second case, from $s(x) \in \text{dom}(h_1)$ and $h_1 \subseteq h$, we have $(s, h) \models \text{alloc}(x)$. So, $(s, h) \models \neg \psi$.

**case:** $L = x \leftrightarrow y$: Then by definition of $\langle \text{sep} \rangle(\varphi, \psi)$, $\neg \text{alloc}(x) \subseteq \text{Lt} \varphi$ and $x \leftrightarrow y \subseteq \text{Lt} \psi$. From $(s, h_1) \models \neg L$, if $s(x) \in \text{dom}(h_1)$ then $h_1(s(x)) \neq s(y)$. As $\neg \text{alloc}(x) \subseteq \text{Lt} \varphi$, $s(x) \notin \text{dom}(h_2)$ and therefore, by $h = h_1+h_2$, $h(s(x)) \neq s(y)$. From $x \leftrightarrow y \subseteq \text{Lt} \psi$, we conclude that $(s, h) \models \neg \psi$.

**case:** $L = \neg x \leftrightarrow y$: Then, by definition of $\langle \text{sep} \rangle(\varphi, \psi)$, $\neg x \leftrightarrow y \subseteq \text{Lt} \psi$. From $(s, h_1) \models \neg L$ and $h_1 \subseteq h$, we derive $h(s(x)) = s(y)$. From $\neg x \leftrightarrow y \subseteq \text{Lt} \psi$, we derive $(s, h) \models \neg \psi$.

**case:** $L = \text{size} \geq \beta_2 + 1 \div \beta_1$, where $\text{size} \geq \beta_2 \subseteq \text{Lt} \psi$ and $\neg \text{size} \geq \beta_1 \subseteq \text{Lt} \varphi$: Since it holds that $(s, h_1) \models \neg L$ and $(s, h_2) \models \varphi$, we derive (respectively) $\text{card}(\text{dom}(h_1)) \leq \beta_2 \div \beta_1$ and $\text{card}(\text{dom}(h_2)) < \beta_1$. From $h = h_1+h_2$, we conclude that $\text{card}(\text{dom}(h)) < \beta_2$. From $\text{size} \geq \beta_2 \subseteq \text{Lt} \psi$, we derive $(s, h) \models \neg \psi$.

**case:** $L = \neg \text{size} \geq \beta_2 \div \beta_1$, where $\neg \text{size} \geq \beta_2 \subseteq \text{Lt} \psi$ and $\text{size} \geq \beta_1 \subseteq \text{Lt} \varphi$: Since we have $(s, h_1) \models \neg L$ and $(s, h_2) \models \varphi$, we conclude that $\text{card}(\text{dom}(h_1)) \geq \beta_2 \div \beta_1$ and $\text{card}(\text{dom}(h_2)) \geq \beta_1$. So, $h = h_1+h_2$ implies $\text{card}(\text{dom}(h)) \geq \beta_2$. By $\neg \text{size} \geq \beta_2 \subseteq \text{Lt} \psi$, we derive $(s, h) \models \neg \psi$. $\square$

We are now ready to tackle the proof of Lemma 6.2.

*Proof of Lemma 6.2.* As in the statement of the lemma, let us consider $X \subseteq_{\text{fin}} \text{VAR}$ and $\alpha \geq \text{card}(X)$, and two core types $\varphi$ and $\psi$ in $\text{CoreTypes}(X, \alpha)$. We want to show that there is a conjunction $\chi \in \text{Conj}(\text{Core}(X, \alpha))$ such that $\vdash_{\mathcal{H}_C(\*,\*)} (\varphi \otimes \psi) \Leftrightarrow \chi$.

First of all, if $\varphi$ or $\psi$ is unsatisfiable, then $\vdash_{\mathcal{H}_C(\*,\*)} \varphi \otimes \psi \Rightarrow \bot$ by using Lemma 4.1 and the admissible axioms $(\mathbf{I}_{6.3.4}^*)$ and $(\mathbf{I}_{6.3.5}^*)$ from Lemma 6.3. Therefore, in this case, it is enough to take $\chi$ equal to $\neg x = x$ to complete the proof. Otherwise, let us assume that $\varphi$ and $\psi$ are satisfiable. We consider $\chi \stackrel{\text{def}}{=} \langle \text{sep} \rangle(\varphi, \psi)$ (see Figure 8), and show that $\vdash_{\mathcal{H}_C(\*,\*)} (\varphi \otimes \psi) \Leftrightarrow \langle \text{sep} \rangle(\varphi, \psi)$. We derive each implication separately.

(⇒): Given Lemma 6.4, the proof of $\vdash_{\mathcal{H}_C(\*,\*)} \varphi \otimes \psi \Rightarrow \langle \text{sep} \rangle(\varphi, \psi)$ is straightforward:

<table><tr><td>1</td><td>$\neg\langle\text{sep}\rangle(\varphi, \psi) * \varphi \Rightarrow \neg\psi$</td><td>Lemma 6.4, Theorem 5.6</td></tr><tr><td>2</td><td>$\neg\langle\text{sep}\rangle(\varphi, \psi) \Rightarrow (\varphi * \neg\psi)$</td><td>*-Adj, 1</td></tr><tr><td>3</td><td>$\neg(\varphi * \neg\psi) \Rightarrow \langle\text{sep}\rangle(\varphi, \psi)$</td><td>PC, 2</td></tr><tr><td>4</td><td>$\langle\varphi \otimes \psi\rangle \Rightarrow \langle\text{sep}\rangle(\varphi, \psi)$</td><td>Def. of $\otimes$, 3</td></tr></table>

(↔): Let us now show that $\vdash_{\mathcal{H}_C(\*,\*)} \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi \otimes \psi$. First, let us note that, since $\langle \text{sep} \rangle(\varphi, \psi) * \varphi \Rightarrow \psi$ is valid (Lemma 6.4), it is derivable in $\mathcal{H}_C(\*)$ (Theorem 5.6), and therefore, by the rule *-Adj, $\vdash_{\mathcal{H}_C(\*,\*)} \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi * \psi$. From that, it follows that it is enough to show that $\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi \otimes \top$ is derivable in $\mathcal{H}_C(\*,\*)$. Indeed, from $\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi \otimes \top$ and $\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi * \psi$, we get, by $(\mathbf{I}_{6.3.9}^*)$, that $\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi \otimes \psi$ is derivable too.

Thus, let us prove that $\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi \otimes \top$ is derivable. If $\langle \text{sep} \rangle(\varphi, \psi)$ is unsatisfiable, then from the completeness of $\mathcal{H}_C$ with respect to Boolean combinations of core formulae (Theorem 4.3), we conclude that $\vdash_{\mathcal{H}_C} \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \bot$. Since $\mathcal{H}_C(\*,\*)$ extends $\mathcal{H}_C$, we
have $\vdash_{\mathcal{H}_C(*,*)} \langle sep \rangle(\varphi, \psi) \Rightarrow \bot$. By propositional reasoning, $\vdash_{\mathcal{H}_C(*,*)} \langle sep \rangle(\varphi, \psi) \Rightarrow \varphi \otimes \top$. Otherwise, let us assume that $\langle sep \rangle(\varphi, \psi)$ is satisfiable.

*Structure of the remaining part of the proof.* Before presenting the technical arguments for the derivation of $\vdash_{\mathcal{H}_C(*,*)} \langle sep \rangle(\varphi, \psi) \Rightarrow \varphi \otimes \top$ when $\langle sep \rangle(\varphi, \psi)$ is satisfiable, let us explain what are the main ingredients. The proof establishing that $\vdash_{\mathcal{H}_C(*,*)} \langle sep \rangle(\varphi, \psi) \Rightarrow \varphi \otimes \top$ is by induction on the number $j$ of variables $x \in X$ for which $alloc(x) \subseteq_L \varphi$ holds. As $\varphi$, $\psi$ and $\langle sep \rangle(\varphi, \psi)$ are currently assumed to be satisfiable, they have exactly the same equalities and inequalities and this is used in the proof. The base case $j = 0$ can be handled using several derivations taking advantage of Lemma 6.3. For the induction step $j > 0$, some more substantial work is needed and this is briefly described below. We distinguish the case $\max_{\text{size}}(\varphi) < \alpha$ from the case $\max_{\text{size}}(\varphi) = \alpha$. Both cases, we introduce the formula $Atom(x_i)$ where $alloc(x_i) \subseteq_L \varphi$.

$$Atom(x_i) \stackrel{\text{def}}{=} \begin{cases} x_i \to y \wedge \text{size} = 1 & \text{if } x_i \to y \subseteq_L \varphi, \text{ for some } y \in X \\ alloc(x_i) \wedge \text{size} = 1 \wedge \bigwedge_{y \in X} \neg x_i \to y & \text{otherwise} \end{cases}$$

In the case $\max_{\text{size}}(\varphi) < \alpha$, we introduce a formula $\varphi'$ as a very slight variant of $\varphi$ such that $\varphi'$ enjoys the following essential properties.

(A) $\varphi'$ is a satisfiable core type in CoreTypes($X$, $\alpha$).

(B) $(Atom(x_i) * \varphi') \Rightarrow \varphi$ is valid.

(C) $(\langle sep \rangle(\varphi, \psi) * Atom(x_i)) \Rightarrow \langle sep \rangle(\varphi', \psi)$ is valid.

In order to conclude $\vdash_{\mathcal{H}_C(*,*)} \langle sep \rangle(\varphi, \psi) \Rightarrow (\varphi \otimes \top)$, we take advantage of the completeness of $\mathcal{H}_C(*)$ to derive the tautologies in (B) and (C). Moreover, as by construction of $\varphi'$, we have $\neg alloc(x_i) \subseteq_L \varphi'$ and, for every $y \in X$, $\neg alloc(y) \subseteq_L \varphi$ implies $\neg alloc(y) \subseteq_L \varphi'$, we shall be able to apply the induction hypothesis on $\varphi'$ to get $\vdash_{\mathcal{H}_C(*,*)} \langle sep \rangle(\varphi', \psi) \Rightarrow (\varphi' \otimes \top)$, which will be essential in the final derivation for $\langle sep \rangle(\varphi, \psi) \Rightarrow (\varphi \otimes \top)$.

In the remaining case $\max_{\text{size}}(\varphi) = \alpha$, we are still looking for some formula $\varphi'$ such that $\varphi' * Atom(x_i) \Rightarrow \varphi$ is valid but we cannot hope for $\varphi'$ to be a core type in CoreTypes($X$, $\alpha$). Instead, we introduce two core types $\varphi'_\alpha$ and $\varphi'_{\alpha-1}$, and define $\varphi'$ as $\varphi'_\alpha \lor \varphi'_{\alpha-1}$. The only difference between $\varphi'_\alpha$ and $\varphi'_{\alpha-1}$ rests on the fact that $\text{size} \ge \alpha \subseteq_L \varphi'_\alpha$ whereas $\neg \text{size} \ge \alpha \subseteq_L \varphi'_{\alpha-1}$ (both formulae contain $\text{size} \ge \alpha - 1$). Similarly to the previous case, the properties below shall be shown.

(D) $\varphi'_\alpha$ and $\varphi'_{\alpha-1}$ are satisfiable core types in CoreTypes($X$, $\alpha$)

(E) $(Atom(x_i) * (\varphi'_\alpha \lor \varphi'_{\alpha-1})) \Rightarrow \varphi$ is valid.

(F) $(\langle sep \rangle(\varphi, \psi) * Atom(x_i)) \Rightarrow \langle sep \rangle(\varphi'_\alpha, \psi) \lor \langle sep \rangle(\varphi'_{\alpha-1}, \psi)$ is valid.

The derivation of $\vdash_{\mathcal{H}_C(*,*)} \langle sep \rangle(\varphi, \psi) \Rightarrow (\varphi \otimes \top)$ follows then a principle similar to one for the case $\max_{\text{size}}(\varphi) < \alpha$.

Now, let us present the technical developments. Directly from the definition of $\langle sep \rangle(\varphi, \psi)$, the following simple facts hold.

1. $\varphi$, $\psi$ and $\langle sep \rangle(\varphi, \psi)$ have exactly the same equalities and inequalities.

2. $\neg \text{size} \ge 0$ is not part of $\langle sep \rangle(\varphi, \psi)$, and therefore, following the definition of $\langle sep \rangle(\varphi, \psi)$, there are no $\text{size} \ge \beta_1 \subseteq_L \varphi$ and $\neg \text{size} \ge \beta_2 \subseteq_L \psi$ with $\beta_1 \ge \beta_2$.

3. $x \ne x$ does not belong to $\langle sep \rangle(\varphi, \psi)$. In particular, by definition of $\langle sep \rangle(\varphi, \psi)$, none of the following conditions apply:

- there is $x \in X$ such that $alloc(x) \subseteq_L \varphi$ and $\neg alloc(x) \subseteq_L \psi$,

- there are $x, y \in X$ such that $x \to y \in \varphi$ and $\neg x \to y \subseteq_L \psi$,
– there are $x, y \in X$ such that $\text{alloc}(x) \wedge \neg x \mapsto y \subseteq_{\text{Lt}} \varphi$ and $x \mapsto y \subseteq_{\text{Lt}} \psi$.

From (1), we know that $\langle \text{sep} \rangle(\varphi, \psi)$ and $\varphi$ satisfy the same (in)equalities. Similarly to the proof of Lemma 5.4, let $x_1, \dots, x_n$ be a maximal enumeration of representatives of the equivalence classes (one per equivalence class) such that $\text{alloc}(x_i)$ occurs in $\varphi$. As it is maximal, for every $\text{alloc}(x)$ in $\text{Lt}(\varphi)$ there is $i \in [1, n]$ such that $x_i$ is syntactically equal to $x$. Moreover, by definition of $\langle \text{sep} \rangle(\varphi, \psi)$, for every $i \in [1, n]$, $\neg \text{alloc}(x_i) \subseteq_{\text{Lt}} \langle \text{sep} \rangle(\varphi, \psi)$. The proof of $\vdash_{\mathcal{H}_C(*,*)} \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi \ominus \top$ is by induction on the number $j$ of variables $x \in X$ for which $\text{alloc}(x) \subseteq_{\text{Lt}} \varphi$ holds.

**base case: $j = 0$:** In the base case, no formula $\text{alloc}(x)$ occurs positively in $\varphi$. Since $\varphi$ is a core type, this implies that for every $x \in X$, $\neg \text{alloc}(x) \subseteq_{\text{Lt}} \varphi$. Moreover, since $\varphi$ is satisfiable, for every $x, y \in X$, $\neg x \mapsto y \subseteq_{\text{Lt}} \varphi$ (see the axiom $(A_3^C)$). Therefore, the core type $\varphi$ is syntactically equivalent (up to associativity and commutativity of conjunction) to the formula $\varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \wedge \varphi_{(\text{in})\text{eq}}$, where

* $\varphi_{\text{size}} \stackrel{\text{def}}{=} \bigwedge (\{\text{size} \ge \beta \subseteq_{\text{Lt}} \varphi\} \cup \{\neg \text{size} \ge \beta \subseteq_{\text{Lt}} \varphi\})$,

* $\varphi_{\neg \text{alloc}} \stackrel{\text{def}}{=} \bigwedge_{x \in X} \neg \text{alloc}(x)$,

* $\varphi_{\uparrow} \stackrel{\text{def}}{=} \bigwedge_{x, y \in X} \neg x \mapsto y$,

* $\varphi_{(\text{in})\text{eq}} \stackrel{\text{def}}{=} \bigwedge \{x \sim y \subseteq_{\text{Lt}} \varphi \mid \sim \in \{=, \ne\}\}$.

Since $\varphi$ is satisfiable, so is $\varphi_{\text{size}}$. We show that $\vdash_{\mathcal{H}_C(*,*)} (\varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow}) \ominus \top$:

<table><tr><td>1</td><td>$\varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \ominus \top$</td><td>(I<sub>6.3.12</sub><sup>*</sup>)</td></tr><tr><td>2</td><td>$\neg \text{alloc}(x) \Rightarrow \neg x \mapsto y$</td><td>(A<sub>3</sub><sup>C</sup>), PC</td></tr><tr><td>3</td><td>$\varphi_{\neg \text{alloc}} \Rightarrow \varphi_{\uparrow}$</td><td>PC, repeated 2</td></tr><tr><td>4</td><td>$\varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \Rightarrow \varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow}$</td><td>PC, 3</td></tr><tr><td>5</td><td>$\langle \varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \ominus \top \rangle \Rightarrow \langle \varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \ominus \top \rangle$</td><td>(I<sub>6.3.4</sub><sup>*</sup>), 4</td></tr><tr><td>6</td><td>$\varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \ominus \top$</td><td>Modus Ponens, 1, 5</td></tr></table>

Now, let us treat the formula $\varphi_{(\text{in})\text{eq}}$. From the definition of $\langle \text{sep} \rangle(\varphi, \psi)$, we have $\varphi_{(\text{in})\text{eq}} \subseteq_{\text{Lt}} \langle \text{sep} \rangle(\varphi, \psi)$, and so by propositional reasoning, $\vdash_{\mathcal{H}_C(*,*)} \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi_{(\text{in})\text{eq}}$. This allows us to conclude that

$$ \vdash_{\mathcal{H}_C(*,*)} \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow ((\varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \wedge \varphi_{(\text{in})\text{eq}}) \ominus \top), \quad (\dagger) $$

by induction on the number of literals $x \sim y$ appearing in $\varphi_{(\text{in})\text{eq}}$, and by relying on the two theorems $(I_{6.3.10}^*)$ and $(I_{6.3.11}^*)$. In the base case, $\varphi_{(\text{in})\text{eq}} = \top$, and so

<table><tr><td>7</td><td>$\varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \Rightarrow \varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \wedge \varphi_{(\text{in})\text{eq}}$</td><td>PC</td></tr><tr><td>8</td><td>$\langle \varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \ominus \top \rangle \Rightarrow \langle \varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \wedge \varphi_{(\text{in})\text{eq}} \ominus \top \rangle$</td><td>(I<sub>6.3.4</sub><sup>*</sup>), 7</td></tr><tr><td>9</td><td>$\varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \wedge \varphi_{(\text{in})\text{eq}} \ominus \top$</td><td>Modus Ponens, 6, 8</td></tr><tr><td>10</td><td>$\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \langle \varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \wedge \varphi_{(\text{in})\text{eq}} \ominus \top \rangle$</td><td>PC, 9</td></tr></table>

In the induction step, let $\varphi_{(\text{in})\text{eq}} = \varphi'_{(\text{in})\text{eq}} \wedge x \sim y$, where $x \sim y \notin_{\text{Lt}} \varphi'_{(\text{in})\text{eq}}$. We have,

$$ \text{Induction Hypothesis} \\ 1 \quad \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow (\varphi_{\text{size}} \wedge \varphi_{\neg \text{alloc}} \wedge \varphi_{\uparrow} \wedge \varphi'_{(\text{in})\text{eq}} \ominus \top) $$
<table><tr><td>2</td><td>&lt;sep&gt;(φ, ψ) ⇒ x ~ y</td><td>PC, as φ<sub>(in)eq</sub> ⊆<sub>Lt</sub> &lt;sep&gt;(φ, ψ)</td></tr><tr><td>3</td><td>x ~ y ∧ (φ<sub>size</sub> ∧ φ<sub>-alloc</sub> ∧ φ<sub>→</sub> ∧ φ'<sub>(in)eq</sub> ⊗ ⊤) ⇒<br/>(φ<sub>size</sub> ∧ φ<sub>-alloc</sub> ∧ φ<sub>→</sub> ∧ φ'<sub>(in)eq</sub> ∧ x ~ y ⊗ ⊤)</td><td>(I<sub>6.3.10</sub><sup>*</sup>)/(I<sub>6.3.11</sub><sup>*</sup>)</td></tr><tr><td>4</td><td>&lt;sep&gt;(φ, ψ) ⇒ (φ<sub>size</sub> ∧ φ<sub>-alloc</sub> ∧ φ<sub>→</sub> ∧ φ'<sub>(in)eq</sub> ∧ x ~ y ⊗ ⊤)</td><td>PC, 1, 2, 3</td></tr><tr><td>5</td><td>&lt;sep&gt;(φ, ψ) ⇒ (φ<sub>size</sub> ∧ φ<sub>-alloc</sub> ∧ φ<sub>→</sub> ∧ φ<sub>(in)eq</sub> ⊗ ⊤)</td><td>Def. of φ'<sub>(in)eq</sub>, 4</td></tr></table>

Since $\varphi_{\text{size}} \wedge \varphi_{-\text{alloc}} \wedge \varphi_{\downarrow} \wedge \varphi_{(\text{in})\text{eq}}$ is equivalent to $\varphi$, from (†) and by $(I_{6.3.4}^*)$, we conclude that $\vdash_{\mathcal{H}_{C(*,-*)}} \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \varphi \otimes \top$.

**induction step:** $j \ge 1$: In this case, let $i \in [1, n]$ such that $\text{alloc}(x_i) \subseteq_L \varphi$ and thus, by definition of $\langle \text{sep} \rangle(\varphi, \psi)$, $\neg \text{alloc}(x_i) \subseteq_L \langle \text{sep} \rangle(\varphi, \psi)$. As announced earlier, we define the formula:

$$ \text{Atom}(x_i) \stackrel{\text{def}}{=} \begin{cases} x_i \mapsto y \wedge \text{size} = 1 & \text{if } x_i \mapsto y \subseteq_L \varphi, \text{ for some } y \in X \\ \text{alloc}(x_i) \wedge \text{size} = 1 \wedge \bigwedge_{y \in X} \neg x_i \mapsto y & \text{otherwise} \end{cases} $$

Notice that, if there is $y \in X$ such that $x_i \mapsto y \subseteq_L \varphi$, then the axiom schema $(A_{22}^*)$ can be instantiated to $\neg \text{alloc}(x_i) \Rightarrow (\text{Atom}(x_i) \otimes \top)$. Otherwise (for all $y \in X$, $x_i \mapsto y \notin_L \varphi$) this formula is an instantiation of the axiom schema $(A_{23}^*)$. This allows us to show the following theorem:

$$ \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow (\text{Atom}(x_i) \otimes (\langle \text{sep} \rangle(\varphi, \psi) * \text{Atom}(x_i))) \quad (‡) $$

<table><tr><td>1</td><td>$\neg \text{alloc}(x_i) \Rightarrow (\text{Atom}(x_i) \otimes \top)$</td><td>$(A_{22}^*)/(A_{23}^*)$</td></tr><tr><td>2</td><td>$\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow \neg \text{alloc}(x_i)$</td><td>Def. of $\langle \text{sep} \rangle(\varphi, \psi)$, PC</td></tr><tr><td>3</td><td>$\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow (\text{Atom}(x_i) \otimes \top)$</td><td>$\Rightarrow \text{-Tr}$, 1, 2</td></tr><tr><td>4</td><td>$\langle \text{sep} \rangle(\varphi, \psi) * \text{Atom}(x_i) \Rightarrow \langle \text{sep} \rangle(\varphi, \psi) * \text{Atom}(x_i)$</td><td>PC</td></tr><tr><td>5</td><td>$\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow (\text{Atom}(x_i) * \langle \text{sep} \rangle(\varphi, \psi) * \text{Atom}(x_i))$</td><td>$\ast$-Adj, 4</td></tr><tr><td>6</td><td>$\langle \text{sep} \rangle(\varphi, \psi) \Rightarrow (\text{Atom}(x_i) \otimes \langle \text{sep} \rangle(\varphi, \psi) * \text{Atom}(x_i))$</td><td>$(I_{6.3.9}^*)$, 3, 5, PC</td></tr></table>

From the hypothesis $\text{card}(X) \le \alpha$, together with $\text{alloc}(x_i) \subseteq_L \varphi$ and the fact that $\varphi$ is satisfiable, we have $\max_{\text{size}}(\varphi) \ge 1$ (see $(I_6^C)$, instantiated with $X = \{x_i\}$). In order to show that $\vdash_{\mathcal{H}_{C(*,-*)}} \langle \text{sep} \rangle(\varphi, \psi) \Rightarrow (\varphi \otimes \top)$, we split the proof depending on whether $\max_{\text{size}}(\varphi) < \alpha$ holds.

**case:** $\max_{\text{size}}(\varphi) < \alpha$: Since $\varphi$ is a satisfiable core type in $\text{CoreTypes}(X, \alpha)$, by definition of $\max_{\text{size}}(.)$, we have $\text{size} \ge \max_{\text{size}}(\varphi) \wedge \neg \text{size} \ge \max_{\text{size}}(\varphi) + 1 \subseteq_L \varphi$. Below, we consider the formula $\varphi'$ obtained from $\varphi$ by:

* replacing $\text{size} \ge \max_{\text{size}}(\varphi) \subseteq_L \varphi$ with $\neg \text{size} \ge \max_{\text{size}}(\varphi)$,

* for every $x \in X$ such that $x = x_i \subseteq_L \varphi$, replacing every literal $\text{alloc}(x) \subseteq_L \varphi$ with $\neg \text{alloc}(x)$, and every literal $x \mapsto y \subseteq_L \varphi$ with $\neg x \mapsto y$, where $y \in X$.
Explicitly,

$$
\begin{align*}
\varphi' \stackrel{\text{def}}{=} & \bigwedge \{x \sim y \subseteq_{\text{Lt}} \varphi \mid \sim \in \{=, \ne\} \} \wedge \bigwedge \{\text{alloc}(x) \subseteq_{\text{Lt}} \varphi \mid x \ne x_i \subseteq_{\text{Lt}} \varphi\} \wedge \\
& \bigwedge \{\neg \text{alloc}(x) \subseteq_{\text{Lt}} \varphi\} \wedge \bigwedge \{\neg \text{alloc}(x) \mid x = x_i \subseteq_{\text{Lt}} \varphi\} \wedge \bigwedge \{x \leftrightarrow y \subseteq_{\text{Lt}} \varphi \mid x \ne x_i \subseteq_{\text{Lt}} \varphi\} \wedge \\
& \bigwedge \{\neg x \leftrightarrow y \subseteq_{\text{Lt}} \varphi\} \wedge \bigwedge \{\neg x \leftrightarrow y \mid x = x_i \wedge x \leftrightarrow y \subseteq_{\text{Lt}} \varphi\} \wedge \neg \text{size} \ge \max_{\text{size}}(\varphi) \wedge \\
& \bigwedge \{\text{size} \ge \beta \subseteq_{\text{Lt}} \varphi \mid \beta < \max_{\text{size}}(\varphi)\} \wedge \bigwedge \{\neg \text{size} \ge \beta \subseteq_{\text{Lt}} \varphi\}.
\end{align*}
$$

The formula $\varphi'$ enjoys the following properties (to be shown below):

A. $\varphi'$ is a satisfiable core type in CoreTypes($\mathbf{X}$, $\alpha$).

B. $(Atom(x_i) * \varphi') \Rightarrow \varphi$ is valid.

C. $(\langle sep \rangle(\varphi, \psi) * Atom(x_i)) \Rightarrow \langle sep \rangle(\varphi', \psi)$ is valid.

Fundamentally, $\varphi'$ enjoys the induction hypothesis, which reveals to be useful later on. *Proof of (A)*. Since $\varphi'$ is obtained from $\varphi$ simply by changing the polarity of some of the literals in $\text{Lt}(\varphi)$, clearly $\varphi'$ is in CoreTypes($\mathbf{X}$, $\alpha$). To show that $\varphi'$ is satisfiable, we rely on the fact that $\varphi$ is satisfiable. Let $(s, h)$ be a memory state satisfying $\varphi$. Since $\text{alloc}(x_i) \subseteq_{\text{Lt}} \varphi$, we conclude that $s(x_i) \in \text{dom}(h)$. Let us consider the disjoint heaps $h_1$ and $h_2$ such that $h = h_1 + h_2$ and $\text{dom}(h_1) = \{s(x_i)\}$. We show that $(s, h_2) \models \varphi'$ by considering every $L \in \text{Lt}(\varphi')$ and showing that $(s, h_2) \models L$.

case: $L = x \sim y$, where $\sim \in \{=, \ne\}$: By definition of $\varphi'$, $(s, h) \models L$ and therefore $s(x) \sim s(y)$. Thus, $(s, h_2) \models L$.

case: $L = \neg \text{alloc}(x)$: If $x = x_i \subseteq_{\text{Lt}} \varphi$ then $s(x) \in \text{dom}(h_1)$, and therefore, by $h_1 \not\models h_2$, $s(x) \notin \text{dom}(h_2)$. So, $(s, h_2) \models \neg \text{alloc}(x)$. Otherwise ($x \neq x_i \subseteq_{\text{Lt}} \varphi$), by definition of $\varphi'$, we have $\neg \text{alloc}(x) \subseteq_{\text{Lt}} \varphi$. So $s(x) \notin \text{dom}(h)$ and, from $h_2 \supseteq h$, we conclude that $(s, h_2) \models \neg \text{alloc}(x)$.

case: $L = \neg x \leftrightarrow y$: Similar to the previous case. Briefly, if $x = x_i \subseteq_{\text{Lt}} \varphi$ then, by definition of $Atom(x_i)$, $(s, h_2) \models \text{alloc}(x)$, which implies $(s, h_2) \models \neg x \leftrightarrow y$. Otherwise, by definition of $\varphi'$, $\neg x \leftrightarrow y \subseteq_{\text{Lt}} \varphi$ and thus $(s, h) \models \neg x \leftrightarrow y$. From $h_2 \supseteq h$, we conclude that $(s, h_2) \models \neg x \leftrightarrow y$.

case: $L = \text{alloc}(x)$: By definition of $\varphi'$, $\text{alloc}(x) \wedge x \neq x_i \subseteq_{\text{Lt}} \varphi$. Therefore $s(x) \in \text{dom}(h)$ and, by definition of $Atom(x_i)$, $s(x) \notin \text{dom}(h_1)$. Since $h = h_1+h_2$, we conclude that $(s, h_2) \models \text{alloc}(x)$.

case: $L = x \leftrightarrow y$: Similar to the previous case. By definition of $\varphi'$, we have $x \leftrightarrow y \wedge x \neq x_i \subseteq_{\text{Lt}} \varphi$. Thus, $h(s(x)) = s(y)$. By definition of $Atom(x_i)$, $s(x) \in \text{dom}(h_2)$ and thus $h_2(s(x)) = s(y)$. So, $(s, h_2) \models x \leftrightarrow y$.

case: $L = \text{size} \ge \beta$: By definition of $\varphi'$, $\beta < \max_{\text{size}}(\varphi)$. Since $(s, h) \models \varphi$, we have $\text{card}(\text{dom}(h)) \ge \max_{\text{size}}(\varphi)$. By definition of $Atom(x_i)$ and from $h = h_1+h_2$, we have $\text{card}(\text{dom}(h_2)) = \text{card}(\text{dom}(h))-1 \ge \max_{\text{size}}(\varphi)-1 \ge \beta$. Therefore, $(s, h_2) \models \text{size} \ge \beta$.

case: $L = \neg \text{size} \ge \beta$: By definition of $\varphi'$, $\neg \text{size} \ge \beta \subseteq_{\text{Lt}} \varphi$ or $\beta = \max_{\text{size}}(\varphi)$. In the former case, since $\varphi$ is satisfiable, we know that $\beta > \max_{\text{size}}(\varphi)$. Therefore, in both cases we have $\beta \ge \max_{\text{size}}(\varphi)$. Moreover, as $(s, h) \models \varphi$ and $\neg \text{size} \ge \max_{\text{size}}(\varphi) + 1 \subseteq_{\text{Lt}} \varphi$, we have $\text{card}(\text{dom}(h)) \le \max_{\text{size}}(\varphi)$. Since $\text{card}(\text{dom}(h_1)) = 1$, by $h = h_1+h_2$ we derive $\text{card}(\text{dom}(h_2)) < \max_{\text{size}}(\varphi) \le \beta$. Therefore, $(s, h_2) \models \neg \text{size} \ge \beta$. $\square$
<figure><img src="image_8.png" /><figcaption>Figure 9: The formula $\langle \text{sep} \rangle(\varphi', \psi)$.</figcaption></figure>

*Proof of (B).* Let $(s, h) \models Atom(x_i) * \varphi'$. So, there are $h_1$ and $h_2$ such that $h = h_1+h_2$, $(s, h_1) \models Atom(x_i)$ and $(s, h_2) \models \varphi'$. By definition of $Atom(x_i)$, $dom(h_1) = \{s(x_i)\}$. In order to prove (B), we show that $(s, h) \models L$, for every literal $L \in Lt(\varphi)$.

**case:** $L = x \sim y$, where $\sim \in \{=, \ne\}$: By definition of $\varphi'$, $(s, h_2) \models L$ and therefore $s(x) \sim s(y)$. Hence, $(s, h) \models L$.

**case:** $L = \neg alloc(x)$: By definition of $Atom(x_i)$, $alloc(x_i) \subseteq Lt \ \varphi$ and therefore $s(x) \notin dom(h_1)$. By definition of $\varphi'$, for every $y \in X$, $alloc(y) \subseteq Lt \ \varphi'$ implies $alloc(y) \subseteq Lt \ \varphi$. Therefore, $s(x) \notin dom(h_2)$. We conclude that $s(x) \notin dom(h)$, and so $(s, h) \models \neg alloc(x)$.

**case:** $L = \neg x \leftrightarrow y$: Similar to the previous case. Briefly, by definition of $Atom(x_i)$, $(s, h_1) \models \neg x \leftrightarrow y$. By definition of $\varphi'$, $(s, h_2) \models \neg x \leftrightarrow y$. So, $(s, h) \models \neg x \leftrightarrow y$.

**case:** $L = alloc(x)$: If $x = x_i \subseteq Lt \ \varphi$, then $s(x) = s(x_i)$ (first case of the proof), and by definition of $Atom(x_i)$, $s(x) \in dom(h_1)$. As $h_1 \subseteq h$, we conclude that $(s, h) \models alloc(x)$. Otherwise, if $x \neq x_i \subseteq Lt \ \varphi$, then by definition of $\varphi'$ we have $alloc(x) \subseteq Lt \ \varphi'$. This implies that $s(x) \in dom(h_2)$ and so, from $h_2 \subseteq h$, we conclude that $(s, h) \models alloc(x)$.

**case:** $L = x \leftrightarrow y$: Similar to the previous case. Briefly, if $x = x_i \subseteq Lt \ \varphi$ then, by definition of $Atom(x_i)$, $(s, h_1) \models x \leftrightarrow y$ and so $(s, h) \models x \leftrightarrow y$. Otherwise $(x \neq x_i \subseteq Lt \ \varphi)$, $x \leftrightarrow y \subseteq Lt \ \varphi'$ and therefore $(s, h_2) \models x \leftrightarrow y$. So, $(s, h) \models x \leftrightarrow y$.

**case:** $L = \text{size} \geq \beta$: If $\beta < \max_{\text{size}}(\varphi)$, then directly by definition of $\varphi'$, we have $(s, h_2) \models \text{size} \geq \beta$. From $h_2 \subseteq h$, we conclude that $(s, h) \models \text{size} \geq \beta$. Otherwise, $\beta = \max_{\text{size}}(\varphi)$. Recall that $\max_{\text{size}}(\varphi) \geq 1$ and so, by definition of $\varphi'$, $\text{size} \geq \max_{\text{size}}(\varphi) - 1 \subseteq Lt \ \varphi'$. Thus, $\text{card}(dom(h_2)) \geq \max_{\text{size}}(\varphi) - 1$. By definition of $Atom(x_i)$ we have $\text{card}(dom(h_1)) = 1$. As $h = h_1+h_2$, we conclude that $(s, h) \models \text{size} \geq \max_{\text{size}}(\varphi)$.

**case:** $L = \neg \text{size} \geq \beta$: As $\varphi$ is satisfiable, $\beta > \max_{\text{size}}(\varphi)$. By definition of the formula $\varphi'$, $\neg \text{size} \geq \max_{\text{size}}(\varphi) \subseteq Lt \ \varphi'$ and thus $\text{card}(dom(h_2)) < \max_{\text{size}}(\varphi)$. From $\text{card}(dom(h_1)) = 1$ we derive $\text{card}(dom(h)) \leq \max_{\text{size}}(\varphi) < \beta$, which allows us to conclude that $(s, h) \models \neg \text{size} \geq \beta$. $\square$

*Proof of (C).* Figure 9 recalls the definition of $\langle \text{sep} \rangle(\varphi', \psi)$. First of all, notice that it cannot be that there is $x \in X$ such that $x \neq x \subseteq Lt \ \langle \text{sep} \rangle(\varphi', \psi)$. Indeed, ad
absurdum, suppose the opposite. By definition of $\langle sep \rangle(\varphi', \psi)$, this implies that (1) $\text{alloc}(x) \wedge \neg x \mapsto y \subseteq_{\text{Lt}} \varphi'$ and $x \mapsto y \subseteq_{\text{Lt}} \psi$, (2) $x \mapsto y \subseteq_{\text{Lt}} \varphi'$ and $\neg x \mapsto y \subseteq_{\text{Lt}} \psi$, or (3) $\text{alloc}(x) \subseteq_{\text{Lt}} \varphi'$ and $\neg \text{alloc}(x) \subseteq_{\text{Lt}} \psi$. By definition of $\varphi'$, this implies that (1) $\text{alloc}(x) \wedge \neg x \mapsto y \subseteq_{\text{Lt}} \varphi$, (2) $x \mapsto y \subseteq_{\text{Lt}} \varphi$ or (3) $\text{alloc}(x) \subseteq_{\text{Lt}} \varphi$. However, by definition of $\langle sep \rangle(\varphi, \psi)$, this implies that $x \neq x \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$, in contradiction with the satisfiability of $\langle sep \rangle(\varphi, \psi)$. Therefore, below we assume that for all $x \in X$, $x \neq x \mathrel{\substack{\notin \\ \supseteq}}_{\text{Lt}} \langle sep \rangle(\varphi', \psi)$.

Let $(s, h) \models \langle sep \rangle(\varphi, \psi) * \text{Atom}(x_i)$. There are $h_1$ and $h_2$ such that $h = h_1+h_2$, $(s, h_1) \models \langle sep \rangle(\varphi, \psi)$ and $(s, h_2) \models \text{Atom}(x_i)$. By definition of $\text{Atom}(x_i)$, $\text{dom}(h_2) = \{s(x_i)\}$. To prove (C), we show that $(s, h) \models L$, for every literal $L \in \text{Lt}(\langle sep \rangle(\varphi', \psi))$.

**case:** $L = x \sim y$, where $\sim \in \{=, \ne\}$: By definition of $\langle sep \rangle(\varphi', \psi)$, $L \subseteq_{\text{Lt}} \{\varphi' | \psi\}$ and so, by definition of $\varphi'$, $L \subseteq_{\text{Lt}} \{\varphi | \psi\}$. By definition of $\langle sep \rangle(\varphi, \psi)$, $L \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$. From $(s, h_1) \models \langle sep \rangle(\varphi, \psi)$ we derive $s(x) \sim s(y)$. So, $(s, h) \models L$.

**case:** $L = \neg \text{alloc}(x)$: By definition of $\langle sep \rangle(\varphi', \psi)$, either $\neg \text{alloc}(x) \subseteq_{\text{Lt}} \psi$ or $\text{alloc}(x) \subseteq_{\text{Lt}} \varphi'$. In the first case, by definition of $\langle sep \rangle(\varphi, \psi)$, $\neg \text{alloc}(x) \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$, and therefore $s(x) \notin \text{dom}(h_1)$. Moreover, since $\langle sep \rangle(\varphi, \psi)$ is satisfiable, $\text{alloc}(x) \mathrel{\substack{\notin \\ \supseteq}}_{\text{Lt}} \varphi$ (otherwise we would have $x \neq x \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$). Therefore, by definition of $\text{Atom}(x_i)$, we conclude that $s(x) \notin \text{dom}(h_2)$. From $h = h_1+h_2$, we derive $s(x) \notin \text{dom}(h)$, and thus $(s, h) \models \neg \text{alloc}(x)$. In the second case, $(\text{alloc}(x) \subseteq_{\text{Lt}} \varphi')$, by definition of $\varphi'$ we have $\text{alloc}(x) \subseteq_{\text{Lt}} \varphi$ and $x \neq x_i \subseteq_{\text{Lt}} \varphi$. By definition of $\text{Atom}(x_i)$, $s(x) \notin \text{dom}(h_2)$. By definition of $\langle sep \rangle(\varphi, \psi)$, $\neg \text{alloc}(x) \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$, and therefore $s(x) \notin \text{dom}(h_1)$. Again, by $h = h_1+h_2$, we have $(s, h) \models \neg \text{alloc}(x)$.

**case:** $L = \neg x \mapsto y$: Following the definition of $\langle sep \rangle(\varphi', \psi)$, $\neg x \mapsto y \subseteq_{\text{Lt}} \psi$ and therefore $\neg x \mapsto y \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$. Therefore, $(s, h_1) \models \neg x \mapsto y$. Since $\langle sep \rangle(\varphi, \psi)$ is satisfiable, $\neg x \mapsto y \subseteq_{\text{Lt}} \varphi$. By definition of $\text{Atom}(x_i)$, we derive $(s, h_2) \models \neg x \mapsto y$. From $h = h_1+h_2$, $(s, h) \models \neg x \mapsto y$.

**case:** $L = \text{alloc}(x)$: By definition of $\langle sep \rangle(\varphi', \psi)$, we have $\neg \text{alloc}(x) \subseteq_{\text{Lt}} \varphi'$ and $\text{alloc}(x) \subseteq_{\text{Lt}} \psi$. First, let us suppose $\text{alloc}(x) \subseteq_{\text{Lt}} \varphi$. By definition of $\varphi'$, $x = x_i \subseteq_{\text{Lt}} \varphi$ and so, by definition of $\text{Atom}(x_i)$, $s(x) \in \text{dom}(h_2)$. From $h_2 \subseteq h$, $(s, h) \models \text{alloc}(x)$. Otherwise $(\neg \text{alloc}(x) \subseteq_{\text{Lt}} \varphi)$, by definition of $\langle sep \rangle(\varphi, \psi)$, $\text{alloc}(x) \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$. So, $s(x) \in \text{dom}(h_1)$, and by $h_1 \subseteq h$, $(s, h) \models \text{alloc}(x)$.

**case:** $L = x \mapsto y$: Similar to the previous case. By definition of $\langle sep \rangle(\varphi', \psi)$, $\neg \text{alloc}(x) \subseteq_{\text{Lt}} \varphi'$ and $x \mapsto y \subseteq_{\text{Lt}} \psi$. First, let us assume $\text{alloc}(x) \subseteq_{\text{Lt}} \varphi$. By definition of $\varphi'$, $x = x_i \subseteq_{\text{Lt}} \varphi$. By definition of $\text{Atom}(x_i)$, $s(x) \in \text{dom}(h_2)$. Ad absurdum, suppose $h(s(x)) \neq s(y)$. By definition of $\text{Atom}(x_i)$, we have that $\text{alloc}(x) \wedge \neg x \mapsto y \subseteq_{\text{Lt}} \varphi$. However, from $x \mapsto y \subseteq_{\text{Lt}} \psi$, this implies $x \neq x \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$, which contradicts the satisfiability of $\langle sep \rangle(\varphi, \psi)$. Therefore, $h(s(x)) = s(y)$ and, from $h_2 \subseteq h$, we conclude that $(s, h) \models x \mapsto y$. Otherwise $(\neg \text{alloc}(x) \subseteq_{\text{Lt}} \varphi)$, by definition of $\langle sep \rangle(\varphi, \psi)$, $x \mapsto y \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$. So, $h_1(s(x)) = s(y)$, and by $h_1 \subseteq h$, we derive $(s, h) \models x \mapsto y$.

**case:** $L = \text{size} \geq \beta_2+1 \div \beta_1$, where $\neg \text{size} \geq \beta_1 \subseteq_{\text{Lt}} \varphi'$ and $\text{size} \geq \beta_2 \subseteq_{\text{Lt}} \psi$: By definition of $\varphi'$, $\neg \text{size} \geq \beta_1 \subseteq_{\text{Lt}} \varphi$, and so $\beta_1 > \text{max}_{\text{size}}(\varphi)$, since $\varphi$ is satisfiable. By definition of $\langle sep \rangle(\varphi, \psi)$ and as $\neg \text{size} \geq \text{max}_{\text{size}}(\varphi) + 1 \subseteq_{\text{Lt}} \varphi$, we have $\text{size} \geq \beta_2 + 1 \div (\text{max}_{\text{size}}(\varphi) + 1) \subseteq_{\text{Lt}} \langle sep \rangle(\varphi, \psi)$, which in turn implies $\text{card}(\text{dom}(h_1)) \geq \beta_2 \div \text{max}_{\text{size}}(\varphi)$. By definition of $\text{Atom}(x_i)$,
card dom(h₂)) ≥ 1. By h = h₁+h₂, card dom(h)) ≥ (β₂ ÷ max size (φ)) + 1 ≥ (β₂ + 1) ÷ max size (φ). As β₁ > max size (φ), (s, h) |= size ≥ β₂+1 ÷ β₁.

case: L = ¬size ≥ β₂ ÷ β₁, where size ≥ β₁ ⊆ Lt φ' and ¬size ≥ β₂ ⊆ Lt ψ:
By definition of φ', β₁ < max_size(φ). By definition of <sep>(φ, ψ), we have
¬size ≥ β₂ ÷ max_size(φ) ⊆ Lt <sep>(φ, ψ). Notice that, since <sep>(φ, ψ) is
satisfiable, β₂ > max_size(φ). Thus, card dom(h₁)) < β₂ - max_size(φ). By
definition of Atom(xᵢ), card dom(h₂)) ≤ 1. From h = h₁+h₂, we conclude
that card dom(h)) < (β₂ - max_size(φ)) + 1. As β₁ < max_size(φ), we have
β₂ - max_size(φ) + 1 ≤ β₂ ÷ β₁. Therefore, (s, h) |= ¬size ≥ β₂ ÷ β₁.

Continuing with the proof of Lemma 6.2, we prove ⊢ₘC(\*,\*-\*) <sep>(φ, ψ) ⇒ (φ ⊗ T).
Notice that, by the completeness of ℋC(\*) (Theorem 5.6), we conclude that the tautolo-
gies in (B) and (C) are derivable in ℋC(\*,\*-\*). Moreover, notice that ¬alloc(xᵢ) ⊆ Lt
φ' and, for every y ∈ X, ¬alloc(y) ⊆ Lt φ implies ¬alloc(y) ⊆ Lt φ'. This allows us to
rely on the induction hypothesis, and conclude that ⊢ₘC(\*,\*-\*) <sep>(φ', ψ) ⇒ (φ' ⊗ T).
The derivation of <sep>(φ, ψ) ⇒ (φ ⊗ T) is given below:

<table>
  <tbody>
    <tr>
      <td>1</td>
      <td>&lt;sep&gt;(φ', ψ) ⇒ (φ' ⊗ T)</td>
      <td>Induction hypothesis</td>
    </tr>
    <tr>
      <td>2</td>
      <td>Atom(x<sub>i</sub>) * φ' ⇒ φ</td>
      <td>(B), Theorem 5.6</td>
    </tr>
    <tr>
      <td>3</td>
      <td>&lt;sep&gt;(φ, ψ) * Atom(x<sub>i</sub>) ⇒ &lt;sep&gt;(φ', ψ)</td>
      <td>(C), Theorem 5.6</td>
    </tr>
    <tr>
      <td>4</td>
      <td>(&lt;sep&gt;(φ, ψ) * Atom(x<sub>i</sub>)) ⇒ (φ' ⊗ T)</td>
      <td>⇒-Tr, 1, 3</td>
    </tr>
    <tr>
      <td>5</td>
      <td>&lt;sep&gt;(φ, ψ) ⇒ (Atom(x<sub>i</sub>) ⊗ &lt;sep&gt;(φ, ψ) * Atom(x<sub>i</sub>))</td>
      <td>(‡)</td>
    </tr>
    <tr>
      <td>6</td>
      <td>(Atom(x<sub>i</sub>) ⊗ &lt;sep&gt;(φ, ψ) * Atom(x<sub>i</sub>)) ⇒ (Atom(x<sub>i</sub>) ⊗ (φ' ⊗ T))</td>
      <td>(I<sub>6.3.5</sub>)*, 4</td>
    </tr>
    <tr>
      <td>7</td>
      <td>(Atom(x<sub>i</sub>) ⊗ (φ' ⊗ T)) ⇒ (Atom(x<sub>i</sub>) * φ' ⊗ T)</td>
      <td>(I<sub>6.3.6</sub>)*</td>
    </tr>
    <tr>
      <td>8</td>
      <td>(Atom(x<sub>i</sub>) * φ' ⊗ T) ⇒ (φ ⊗ T)</td>
      <td>(I<sub>6.3.4</sub>)*, 2</td>
    </tr>
    <tr>
      <td>9</td>
      <td>&lt;sep&gt;(φ, ψ) ⇒ (φ ⊗ T)</td>
      <td>⇒-Tr, 5, 6, 7, 8</td>
    </tr>
  </tbody>
</table>

case: max_size(φ) = α: In this case, we have size ≥ α ⊆<sub>Lt</sub> φ, where we recall that α = max_size(φ) ≥ 1. Following the developments of the previous case, we would like to define a formula φ' for which the formula φ' * Atom(x<sub>i</sub>) ⇒ φ is valid. However, since φ is in CoreTypes(X, α), we cannot hope for φ' to be a core type in CoreTypes(X, α). Indeed, because of size ≥ α ⊆<sub>Lt</sub> φ, in order to achieve the valid formula above we must differentiate between the case where φ is satisfied by a memory state (s, h) such that card dom(h)) > α, to the case where card dom(h)) = α. Therefore, below we introduce two core types φ'<sub>α</sub> and φ'<sub>α-1</sub>, and define φ' as φ'<sub>α</sub> ∨ φ'<sub>α-1</sub>. Since the separating conjunction distributes over disjunctions, after defining these two core types, we can easily adapt the arguments of the previous case to prove that <sep>(φ, ψ) ⇒ (φ ⊗ T). The formula φ'<sub>α</sub> is obtained from φ by replacing, for every x ∈ X such that x = x<sub>i</sub> ⊆<sub>Lt</sub> φ, every literal alloc(x) ⊆<sub>Lt</sub> φ with ¬alloc(x), and every x ↦ y ⊆<sub>Lt</sub> φ with ¬x ↦ y, where y ∈ X. Notice that φ'<sub>α</sub> is defined similarly to φ' (in the previous case of the proof), with the exception that we do not modify the polarity of size literals. Explicitly,
$\varphi'_{\alpha}$ is defined as follows.

$$ \varphi'_{\alpha} \stackrel{\text{def}}{=} \bigwedge \{x \sim y \subseteq_{\text{Lt}} \varphi \mid \sim \in \{=, \ne\}\} \wedge \bigwedge \{\text{alloc}(x) \subseteq_{\text{Lt}} \varphi \mid x \neq x_i \subseteq_{\text{Lt}} \varphi\} \wedge \bigwedge \{\neg \text{alloc}(x) \subseteq_{\text{Lt}} \varphi\} \wedge \\ \bigwedge \{\neg \text{alloc}(x) \mid x = x_i \subseteq_{\text{Lt}} \varphi\} \wedge \bigwedge \{x \mapsto y \subseteq_{\text{Lt}} \varphi \mid x \neq x_i \subseteq_{\text{Lt}} \varphi\} \wedge \bigwedge \{\neg x \mapsto y \subseteq_{\text{Lt}} \varphi\} \wedge \\ \bigwedge \{\neg x \mapsto y \mid x = x_i \wedge x \mapsto y \subseteq_{\text{Lt}} \varphi\} \wedge \bigwedge \{\text{size} \ge \beta \mid \beta \in [0, \alpha - 1]\} \wedge \text{size} \ge \alpha. $$

The formula $\varphi'_{\alpha-1}$ is obtained from $\varphi'_{\alpha}$ by replacing $\text{size} \ge \alpha$ (highlighted in the definition of $\varphi'_{\alpha}$ above), by $\neg \text{size} \ge \alpha$. The following properties are satisfied:

**D.** $\varphi'_{\alpha}$ and $\varphi'_{\alpha-1}$ are satisfiable core types in CoreTypes($\mathbf{X}$, $\alpha$),

**E.** $(Atom(x_i) * (\varphi'_{\alpha} \lor \varphi'_{\alpha-1})) \Rightarrow \varphi$ is valid.

**F.** $(\langle \text{sep} \rangle(\varphi, \psi) * Atom(x_i)) \Rightarrow \langle \text{sep} \rangle(\varphi'_{\alpha}, \psi) \lor \langle \text{sep} \rangle(\varphi'_{\alpha-1}, \psi)$ is valid.

**Proof of (D).** The proof is very similar to the one of the property (A). Here, we pinpoint the main differences. First of all, since both $\varphi'_{\alpha}$ and $\varphi'_{\alpha-1}$ are obtained from $\varphi$ by changing the polarity of some of the literals in $\text{Lt}(\varphi)$, they are both in CoreTypes($\mathbf{X}$, $\alpha$). To show that $\varphi'_{\alpha}$ and $\varphi'_{\alpha-1}$ are satisfiable, we rely on the fact that $\varphi$ is satisfiable. Let $(s, h)$ be a memory state satisfying $\varphi$. Since $\text{size} \ge \alpha \subseteq_{\text{Lt}} \varphi$, $\text{card}(\text{dom}(h)) \ge \alpha$. Without loss of generality, we can assume $\text{card}(\text{dom}(h)) > \alpha$. Indeed, if $\text{card}(\text{dom}(h)) = \alpha$ it is sufficient to add a memory cell $(\ell, \ell)$ to $h$, such that $\ell$ does not correspond to a program variable $\mathbf{x} \in \mathbf{X}$. It is straightforward to check that the resulting memory state still satisfies $\varphi$. We introduce a second heap $h'$. Let $L = \text{dom}(h) \cap \{s(\mathbf{x}) \mid \mathbf{x} \in \mathbf{X}\}$ be the set of locations in $\text{dom}(h)$ that corresponds to variables in $\mathbf{X}$. Since $\text{card}(\mathbf{X}) \le \alpha$, $\text{card}(L) \le \alpha$. Let $h' \subseteq h$ such that $L \subseteq \text{dom}(h')$ and $\text{card}(\text{dom}(h')) = \alpha$. Again, it is straightforward to see that $(s, h')$ satisfies $\varphi$. Intuitively, we rely on $(s, h)$ to show that $\varphi'_{\alpha}$ is satisfiable, and on $(s, h')$ to show that $\varphi'_{\alpha-1}$ is satisfiable. As $\text{alloc}(x_i) \subseteq_{\text{Lt}} \varphi$, we have $s(\mathbf{x}) \in \text{dom}(h)$ and $s(\mathbf{x}) \in \text{dom}(h')$. We consider heaps $h_1$ and $h_2$ such that $h = h_1+h_2$ and $\text{dom}(h_1) = \{s(x_i)\}$. Similarly, we consider heaps $h'_1$ and $h'_2$ such that $h' = h'_1+h'_2$ and $\text{dom}(h'_1) = \{s(x_i)\}$. We show that $(s, h_2) \models \varphi'_{\alpha}$ and $(s, h'_2) \models \varphi'_{\alpha-1}$. Let us first discuss the former result. Let $L \in \text{Lt}(\varphi'_{\alpha})$. If $L$ is not of the form $\text{size} \ge \beta$ or $\neg \text{size} \ge \beta$, then $(s, h_2) \models L$ follows exactly as in the proof of (A). Otherwise,

**case:** $L = \text{size} \ge \beta$: By definition of $h_2$, $\text{card}(\text{dom}(h_2)) = \text{card}(\text{dom}(h)) - 1 \ge \alpha$. Since $\beta \le \alpha$ (as $\varphi'_{\alpha}$ is in CoreTypes($\mathbf{X}$, $\alpha$)), we conclude that $(s, h_2) \models \text{size} \ge \beta$.

**case:** $L = \neg \text{size} \ge \beta$: By definition of $\varphi'_{\alpha}$, no literals of the form $\neg \text{size} \ge \beta$ belongs to $\text{Lt}(\varphi'_{\alpha})$. Therefore, this case does not occur.

This concludes the proof of $(s, h_2) \models \varphi'_{\alpha}$. For the proof of $(s, h'_2) \models \varphi'_{\alpha-1}$, let us consider $L \in \text{Lt}(\varphi'_{\alpha-1})$. Again, if $L$ is not of the form $\text{size} \ge \beta$ or $\neg \text{size} \ge \alpha$, then $(s, h'_2) \models L$ follows exactly as in the proof of (A) (replacing $h$ by $h'$ and $h_2$ by $h'_2$). Otherwise,

**case:** $L = \text{size} \ge \beta$: By definition of $\varphi'_{\alpha-1}$, we have $\beta < \alpha$. By definition of $h'_2$, $\text{card}(\text{dom}(h'_2)) = \text{card}(\text{dom}(h')) - 1 = \alpha - 1$. Therefore, $(s, h'_2) \models \text{size} \ge \beta$.

**case:** $L = \neg \text{size} \ge \beta$: By definition of $\varphi'_{\alpha-1}$, $\beta = \alpha$. Since $\text{card}(\text{dom}(h'_2)) = \alpha - 1$, we conclude that $(s, h'_2) \models \neg \text{size} \ge \beta$. $\square$

**Proof of (E).** The proof is very similar to the one of the property (B). We show that $(Atom(x_i) * \varphi'_{\alpha}) \Rightarrow \varphi$ and $(Atom(x_i) * \varphi'_{\alpha-1}) \Rightarrow \varphi$. Then, (E) follows as the separating conjunction distributes over disjunction. First, let us consider $(Atom(x_i) * \varphi'_{\alpha}) \Rightarrow \varphi$, and a memory state $(s, h)$ satisfying $Atom(x_i) * \varphi'_{\alpha}$. There are $h_1$ and $h_2$ such that