$h = h_1+h_2$, $(s, h_1) \models Atom(\mathbf{x}_i)$ and $(s, h_2) \models \varphi'_{\alpha}$. Let $L \in \mathbf{Lt}(\varphi)$. Notice that $\varphi$ does not contain negated $size \ge \beta$ literals. If $L$ is not $size \ge \beta$, for some $\beta \in [0, \alpha]$, then $(s, h) \models L$ follows exactly as it is shown in the proof of (B). Otherwise, suppose $L = size \ge \beta$, where $\beta \in [0, \alpha]$. By definition of $\varphi'_{\alpha}$, $size \ge \alpha \subseteq \mathbf{Lt} \varphi'_{\alpha}$. Hence, $\mathrm{card}(\mathrm{dom}(h_2)) \ge \alpha$ and, from $h_2 \subseteq h$, we derive $(s, h) \models size \ge \beta$. So, $(s, h) \models \varphi$. Let us now consider $(Atom(\mathbf{x}_i) * \varphi'_{\alpha-1}) \Rightarrow \varphi$ and a memory state $(s, h)$ satisfying $Atom(\mathbf{x}_i) * \varphi'_{\alpha-1}$. There are $h_1$ and $h_2$ such that $h = h_1+h_2$, $(s, h_1) \models Atom(\mathbf{x}_i)$ and $(s, h_2) \models \varphi'_{\alpha-1}$. Let $L \in \mathbf{Lt}(\varphi)$. Again, $\varphi$ does not contain negated $size \ge \beta$ literals, and if $L$ is not $size \ge \beta$, for some $\beta \in [0, \alpha]$, then $(s, h) \models L$ follows exactly as is shown in the proof of (B). Otherwise, suppose $L = size \ge \beta$, where $\beta \in [0, \alpha]$. By definition of $\varphi'_{\alpha-1}$, $size \ge \alpha \div 1 \subseteq \mathbf{Lt} \varphi'_{\alpha-1}$. Therefore, $\mathrm{card}(\mathrm{dom}(h_2)) \ge \alpha - 1$. By definition of $Atom(\mathbf{x}_i)$, $\mathrm{card}(\mathrm{dom}(h_1)) = 1$. From $h = h_1+h_2$, we conclude that $\mathrm{card}(\mathrm{dom}(h)) \ge \alpha$ and thus $(s, h) \models size \ge \beta$. Therefore, $(s, h) \models \varphi$. $\square$

*Proof of (F).* Recall that $\langle sep \rangle(\varphi, \psi)$ is satisfiable. In particular, from its definition together with $size \ge \alpha \subseteq \mathbf{Lt} \varphi$, this implies that $size \ge \alpha \subseteq \mathbf{Lt} \psi$, as otherwise we would have $\neg size \ge 0 \subseteq \mathbf{Lt} \langle sep \rangle(\varphi, \psi)$. So, as $\psi$ is a satisfiable core type in CoreTypes($\mathbf{X}$, $\alpha$), for all $\beta \in [0, \alpha]$, $size \ge \beta \subseteq \mathbf{Lt} \psi$. Alternatively, $\psi$ does not contain $\neg size \ge \beta$ literals. We look at the definitions of $\langle sep \rangle(\varphi'_{\alpha}, \psi)$ and $\langle sep \rangle(\varphi'_{\alpha-1}, \psi)$.

a. Since for all $\beta \in [0, \alpha]$, $size \ge \beta \subseteq \mathbf{Lt} \varphi'_{\alpha}$ and $size \ge \beta \subseteq \mathbf{Lt} \psi$, we derive that $\langle sep \rangle(\varphi'_{\alpha}, \psi)$ does not contain $size \ge \beta$ nor $\neg size \ge \beta$ literals (for all $\beta \in [0, \alpha]$). This holds directly by definition of $\langle sep \rangle(\varphi'_{\alpha}, \psi)$, which can be retrieved by substituting $\varphi'$ by $\varphi'_{\alpha}$ in Figure 9.

b. Analogously, we know that $\neg size \ge \alpha \subseteq \mathbf{Lt} \varphi'_{\alpha-1}$ whereas for every $\beta \in [0, \alpha - 1]$, $size \ge \beta \subseteq \mathbf{Lt} \varphi'_{\alpha-1}$, and therefore among all the literals $size \ge \beta$ or $\neg size \ge \beta$ ($\beta \in [0, \alpha]$), $\langle sep \rangle(\varphi'_{\alpha-1}, \psi)$ only contains $size \ge 1$ (occurring positively).

By definition and with the sole exception of the polarity of the formula $size \ge \alpha$ (occurring positively in $\varphi'_{\alpha}$ and negatively in $\varphi'_{\alpha-1}$), the two core types $\varphi'_{\alpha-1}$ and $\varphi'_{\alpha}$ are equal. Directly by definition of $\langle sep \rangle(\varphi'_{\alpha}, \psi)$ and $\langle sep \rangle(\varphi'_{\alpha-1}, \psi)$, together with (a) and (b), this implies that $\langle sep \rangle(\varphi'_{\alpha-1}, \psi)$ is syntactically equal to $\langle sep \rangle(\varphi'_{\alpha}, \psi) \wedge size \ge 1$ (up to commutativity and associativity of conjunction). This means that the formula $\langle sep \rangle(\varphi'_{\alpha-1}, \psi) \Rightarrow \langle sep \rangle(\varphi'_{\alpha}, \psi)$ is valid, and suggests us that, in order to show (F), we can simply establish that $(\langle sep \rangle(\varphi, \psi) * Atom(\mathbf{x}_i)) \Rightarrow \langle sep \rangle(\varphi'_{\alpha}, \psi)$ is valid. As we already stated, $\varphi'_{\alpha}$ is defined as $\varphi'$ (in the previous step of the proof), with the exception that we do not modify the polarity of $size \ge \beta$ literals. Because of this, we can rely on the proof of (C). Briefly, we consider a memory state $(s, h)$ satisfying $\langle sep \rangle(\varphi, \psi) * Atom(\mathbf{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 Atom(\mathbf{x}_i)$. Let $L \in \mathbf{Lt}(\langle sep \rangle(\varphi'_{\alpha-1}, \psi))$. By (a), $L$ is neither of the form $size \ge \beta$ nor of the form $\neg size \ge \beta$. Therefore, $(s, h) \models L$ follows exactly as shown in the proof of (C). $\square$

We are now ready to prove that $\langle sep \rangle(\varphi, \psi) \Rightarrow (\varphi \ominus \top)$. By Theorem 5.6, the tautologies in (D) and (F) are derivable in $\mathcal{H}_C(*, -*)$. Moreover, since $\neg \mathrm{alloc}(\mathbf{x}_i) \subseteq \mathbf{Lt} \{\varphi'_{\alpha}; \varphi'_{\alpha-1}\}$ and, for every $y \in \mathbf{X}$, $\neg \mathrm{alloc}(y) \subseteq \mathbf{Lt} \varphi$ implies $\neg \mathrm{alloc}(y) \subseteq \{\varphi'_{\alpha}; \varphi'_{\alpha-1}\}$, we rely on the induction hypothesis to derive

$$ \vdash_{\mathcal{H}_C(*, -*)} \langle sep \rangle(\varphi'_{\alpha}, \psi) \Rightarrow (\varphi'_{\alpha} \ominus \top), \quad \vdash_{\mathcal{H}_C(*, -*)} \langle sep \rangle(\varphi'_{\alpha-1}, \psi) \Rightarrow (\varphi'_{\alpha-1} \ominus \top). $$

We derive $\langle sep \rangle(\varphi, \psi) \Rightarrow (\varphi \ominus \top)$ (see Figure 10) concluding the proof of Lemma 6.2. $\square$

<figure><img src="image_9.png" /></figure>
<table><caption>Figure 10: Proof of Lemma 6.2: the final derivation.</caption><tr><td>1</td><td>⟨sep⟩(φ'α, ψ) ⇒ (φ'α ⊗ ⊤)</td><td>Induction hypothesis</td></tr><tr><td>2</td><td>⟨sep⟩(φ'α-1, ψ) ⇒ (φ'α-1 ⊗ ⊤)</td><td>Induction hypothesis</td></tr><tr><td>3</td><td>Atom(x<sub>i</sub>) * (φ'α ∨ φ'α-1) ⇒ φ</td><td>(E), Theorem 5.6</td></tr><tr><td>4</td><td>⟨sep⟩(φ, ψ) * Atom(x<sub>i</sub>) ⇒ ⟨sep⟩(φ'α, ψ) ∨ ⟨sep⟩(φ'α-1, ψ)</td><td>(F), Theorem 5.6</td></tr><tr><td>5</td><td>⟨sep⟩(φ'α, ψ) ∨ ⟨sep⟩(φ'α-1, ψ) ⇒ (φ'α ⊗ ⊤) ∨ (φ'α-1 ⊗ ⊤)</td><td>PC, 1, 2</td></tr><tr><td>6</td><td>(φ'α ⊗ ⊤) ∨ (φ'α-1 ⊗ ⊤) ⇒ (φ'α ∨ φ'α-1 ⊗ ⊤)</td><td>(I<sub>6.3.7</sub><sup>*</sup>)</td></tr><tr><td>7</td><td>⟨sep⟩(φ, ψ) * Atom(x<sub>i</sub>) ⇒ (φ'α ∨ φ'α-1 ⊗ ⊤)</td><td>⇒ -Tr, 4, 5, 6</td></tr><tr><td>8</td><td>⟨sep⟩(φ, ψ) ⇒ (Atom(x<sub>i</sub>) ⊗ ⟨sep⟩(φ, ψ) * Atom(x<sub>i</sub>))</td><td>(‡)</td></tr><tr><td>9</td><td>(Atom(x<sub>i</sub>) ⊗ ⟨sep⟩(φ, ψ) * Atom(x<sub>i</sub>)) ⇒ (Atom(x<sub>i</sub>) ⊗ (φ'α ∨ φ'α-1 ⊗ ⊤))</td><td>(I<sub>6.3.5</sub><sup>*</sup>), 7</td></tr><tr><td>10</td><td>(Atom(x<sub>i</sub>) ⊗ (φ'α ∨ φ'α-1 ⊗ ⊤)) ⇒ (Atom(x<sub>i</sub>) * (φ'α ∨ φ'α-1) ⊗ ⊤)</td><td>(I<sub>6.3.6</sub><sup>*</sup>)</td></tr><tr><td>11</td><td>(Atom(x<sub>i</sub>) * (φ'α ∨ φ'α-1) ⊗ ⊤) ⇒ (φ ⊗ ⊤)</td><td>(I<sub>6.3.4</sub><sup>*</sup>), 3</td></tr><tr><td>12</td><td>⟨sep⟩(φ, ψ) ⇒ (φ ⊗ ⊤)</td><td>⇒ -Tr, 8, 9, 10, 11</td></tr></table>

Lemma 6.2 in which $\varphi$ and $\psi$ are core types can be extended to arbitrary Boolean combinations of core formulae, as we show that the distributivity of $\otimes$ over disjunctions is provable in $\mathcal{H}_C(*, -*)$. As a consequence of this development, we achieve the main result of the paper.

**Theorem 6.5.** $\mathcal{H}_C(*, -*)$ is sound and complete for SL(*, -*).

*Proof.* Soundness of the proof system $\mathcal{H}_C(*, -*)$ has been already established earlier, see Lemma 3.1. As far as the completeness proof is concerned, its structure is very similar to the proof of Theorem 5.6 except that we have to be able to handle the separating implication. In order to be self-contained, we reproduce some of its arguments albeit adapted to $\mathcal{H}_C(*, -*)$.

We need to show that for every formula $\varphi$ in SL(*, -*), 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 SL(*, -*), 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$.

In order to show that every formula $\varphi$ has a provably equivalent Boolean combination of core formulae, we heavily rely on Corollary 5.5 and on Lemma 6.2. The proof is by simple induction on the number of occurrences of * or -* in $\varphi$ that are not involved in the definition of some core formula of the form $\mathbf{size} \ge \beta$ or $\mathbf{alloc}(x)$. For the base case, when $\varphi$ has no occurrence of the separating connectives, $x = y$ and $x \leftrightarrow y$ are already core formulae, whereas `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:
**R1** Let $\varphi, \varphi'$ and $\psi$ be formulae of $\mathrm{SL}(*, -*)$ such that $\vdash_{\mathcal{H}_C(*, -*)} \varphi \Leftrightarrow \varphi'$. Then,

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

In order to prove **R1**, we are almost done as we have already shown **R0** in the proof of Theorem 5.6 and the same properties hold for $\mathrm{SL}(*, -*)$ though the language is richer.

As a direct consequence of the admissibility of the rules $(\mathbf{I}_{6.3.4}^*)$ and $(\mathbf{I}_{6.3.5}^*)$ from Lemma 6.3, the rules below are also admissible:

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

We need the two rules as $-*$ is not commutative. 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}$.

Now, assume $\varphi$ is a formula in $\mathrm{SL}(*, -*)$. Without loss of generality, we can assume that the separating connectives in $\varphi$ are restricted to $*$ and $\oplus$ for the occurrences that are not related to abbreviations for core formulae. Indeed, $\psi' \oplus \psi$ is a shortcut for $\neg(\psi' -* \neg\psi)$ and therefore one can replace every occurrence of $\psi' -* \psi$ by $\neg(\psi' \oplus \neg\psi)$ assuming that $\psi'$ and $\psi$ are already of the appropriate shape. Such a replacement is possible thanks to **R1**.

Assume that $\varphi$ is a formula in $\mathrm{SL}(*, \oplus)$ with $n+1$ occurrences of $*$ or $\oplus$ not involved in the definition of core formulae.

Let $\psi$ be a subformula of $\varphi$ (at the occurrence $\rho$) of the form $\psi_1 \oplus \psi_2$ such that $\psi_1$ and $\psi_2$ are in $\mathrm{Bool}(\mathrm{Core}(\mathbf{X}, \alpha_1))$ and $\mathrm{Bool}(\mathrm{Core}(\mathbf{X}, \alpha_2))$, respectively. By propositional reasoning, one can show that there are formulae in disjunctive normal form $\psi_1^1 \vee \dots \vee \psi_1^{n_1}$ and $\psi_2^1 \vee \dots \vee \psi_2^{n_2}$ such that $\vdash_{\mathcal{H}_C} \psi_i \Leftrightarrow \psi_i^1 \vee \dots \vee \psi_i^{n_i}$ for $i \in \{1, 2\}$, and moreover every $\psi_i^j$'s is a core type in $\mathrm{CoreTypes}(\mathbf{X}, \max(\mathrm{card}(\mathbf{X}), \alpha_1, \alpha_2))$. Again, by using propositional reasoning but this time establishing also distributivity of $\vee$ over $\oplus$, we have

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

We rely on Lemma 6.2, and conclude that there is a conjunction of core formulae $\psi^{j_1, j_2}$ in $\mathrm{Conj}(\mathrm{Core}(\mathbf{X}, \max(\mathrm{card}(\mathbf{X}), \alpha_1, \alpha_2)))$ such that $\vdash_{\mathcal{H}_C(*, -*)} \psi_1^{j_1} \oplus \psi_2^{j_2} \Leftrightarrow \psi^{j_1, j_2}$. By propositional reasoning, we get

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

Consequently (thanks to the property **R1**), we obtain

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

Note that the right-hand side formula has $n$ occurrences of the separating connectives that are not involved in the definition of some core formula. The induction hypothesis applies, which concludes the proof.

The case when $\psi$ is a subformula of $\varphi$ (at the occurrence $\rho$) of the form $\psi_1 * \psi_2$ is treated as in the proof of Theorem 5.6 and therefore is omitted herein. $\square$
## 7. RELATED WORK

In this section, we briefly compare our Hilbert-style proof system $\mathcal{H}_C(*, \dashv)$ with existing proof systems for SL$(*, \dashv)$, fragments or extensions and we recall a few landmark works proposing proof systems for abstract separation logics or for logics that are variants of Boolean BI. Those latter proof systems are not necessarily Hilbert-style and may contain labels or other similar machineries. So, this section completes the presentation of the context from Section 1 while pinpointing the main original features of our calculus. Finally, we also evoke several works that use the idea of axiomatising a fragment of a logic and to provide in the proof system means to transform any formula into an equivalent formula from that fragment. This is clearly similar to the approach we have followed, but we aim at picking examples from outside the realm of spatial and resource logics. In order to keep the length of this section reasonable, we limit ourselves to the main bibliographical entries but additional relevant works can be found in the cited materials.

**Proof systems for quantifier-free separation logic.** Surprisingly, as far as we know, sound and complete proof systems for SL$(*, \dashv)$ are very rare and the only system we are aware of is a tableaux-based calculus from [GM10] with labelled formulae (each formula is enriched with a label to be interpreted by some heap) and with resource graphs to encode symbolically constraints between heap expressions (i.e. labels). Of course, translations from separation logics into logics or theories have been designed, see e.g. [CGH05, RISK16], but the finding of proof systems for SL$(*, \dashv)$ with all Boolean connectives and the separating connectives $*$ and $\dashv$ has been quite challenging. Unlike [GM10], $\mathcal{H}_C(*, \dashv)$ uses only SL$(*, \dashv)$ formulae and therefore can be viewed as a quite orthodox Hilbert-style calculus with no extra syntactic objects. In particular, $\mathcal{H}_C(*, \dashv)$ has no syntactic machinery to refer to heaps or to other semantical objects related to SL$(*, \dashv)$. In [GM10], the resource graphs attached to the tableaux are designed to reason about heap constraints, and to provide control for designing strategies that lead to termination. Interestingly, the calculus in [GM10] is intended to be helpful to synthesize countermodels (which is a standard feature for labelled deduction systems [Gab96]) or to be extended to the first-order case, which is partly done in [GM10] but we know that completeness is theoretically impossible. Besides, a sound labelled sequent calculus for the first-order extension of SL$(*, \dashv)$ is presented in [HGT15] but completeness for the sublogic SL$(*, \dashv)$ is not established. The calculus in [HGT15] has also labels, which differs from our puristic approach. A complete sequent-style calculus for the symbolic heap fragment has been designed quite early in [BCO04] but does not deal with full SL$(*, \dashv)$ (in particular it is not closed under Boolean connectives and does not contain the separating implication). A complexity-wise optimal decision procedure for the symbolic heap fragment is designed in [CHO$^+$11] based on a characterisation in terms of homomorphisms.

**Framesworks for abstract separation logics.** Bunched logics, such as the original bunched logic BI in [OP99], are known to be closely related to separation logics that can be viewed as concretisation of (Boolean) BI with models made of memory states, see e.g. [Pym02, Rey02, GM05, PSO18]. Actually, bunched logics come with different flavours, Boolean BI being considered as the genuine abstract version of SL$(*, \dashv)$. Though Boolean BI has been shown undecidable in [LG13, BK14], a Hilbert-style axiomatisation can be found in [GLW06]. Our proof system $\mathcal{H}_C(*, \dashv)$ inherits all the axiom schemas and inference rules for Boolean BI from [GLW06], which is expected as SL$(*, \dashv)$ can be viewed as Boolean
BI on concrete heaps but with the notable difference of having built-in atomic formulae $x = y$ and $x \leftrightarrow y$. Bunched logics, such as Boolean BI, can be defined in several ways, for instance assuming classical or intuitionistic connectives, and in [Bro12], a unified proof theory based on display calculi [Bel82] is designed for a variety of four bunched logics, including Boolean BI (see also the nested sequent calculus for Boolean BI in [PSP13]). In display calculi, structural connectives enrich the sequent-style structures, providing a family of structural connectives accompanying the standard comma from sequent-style calculi. The main results in [Bro12] include cut-elimination, soundness and completeness. So, compared to our calculus $\mathcal{H}_C(*, \dashv)$, the calculi in [Bro12] are designed for logics with more abstract semantical structures and owns a proof-theoretical machinery that does not include labels but instead complex structured sequents.

The quest for designing frameworks dedicated to classes of abstract separation logics have been pursued in several directions. For instance, models for Boolean BI are typically relational commutative monoids but properties can be added leading to a separation theory. In [BV14], a hybrid version of Boolean BI is introduced, called HyBBI, in which nominals (in the sense of hybrid modal logics, see e.g. [ABM01]) are added in order to be able to express rich standard properties in separation theory, such as cancellativity. Not only an Hilbert-style proof system is provided for HyBBI [BV14] but also a parametric completeness result is shown. More precisely, any extension of the proof system for HyBBI with a set of specific axioms is actually complete with respect to the class of models that satisfy the axioms, which is analogous to Sahlqvist's Theorem for modal logics [Sah75, BdRV01]. This provides a very general means to axiomatise variants of Boolean BI but at the cost of having the extra machinery for nominals. Moreover, as HyBBI and its extensions are abstract separation logics with no atomic formulae of the form $x = y$ or $x \leftrightarrow y$, the tools developed in [BV14] are of no help to design an Hilbert-style proof system for SL$(*, \dashv)$ (except that its part dealing with Boolean BI is precisely borrowed from [GLW06] too).

Besides, in [HCGT18] labelled sequent calculi are designed for several abstract separation logics by considering different sets of properties. The sequents contain labelled formulae (a formula prefixed by a label to be interpreted as an abstract heap) as well as relational atoms to express relationships between abstract heaps. Though the framework in [HCGT18] is modular and very general to handle abstract separation logics, it is not tailored to separation logics with concrete semantics, see [HCGT18, Section 7] for possible future directions. In contrast, as explained already, the paper [HGT15] deals with first-order separation logic with concrete semantics and presents a sound labelled sequent calculus for it. Of course, the calculus cannot be complete but more importantly in the context of the current paper, completeness is not established for the quantifier-free fragment. In [HGT15], the sequents contain labelled formulae and relational atoms, similarly to [HCGT18] (see also [Hóu15]). Hence, this does not meet our requirements to have a pure axiomatisation in which only logical formulae from quantifier-free separation logic are allowed.

Modularity of the approaches from [Bro12, BV14, HCGT18] is further developed in the recent work [DP18, Doc19] by proposing a framework for labelled tableaux systems parametrised by the choice of separation theories (in the very sense of [BV14]). It is remarkable that the developments in [DP18, Doc19] are very general as it can handle separation theories that can be expressed in the rich class of so-called coherent first-order formulae, included in the first-order fragment $Π_2$. The first-order axioms are directly translated into inference rules. The calculi use labelled formulae (every formula is decorated by a sign and by a label) as well as constraints enforcing properties between worlds/resources.
Unlike [GM10], the reasoning about labels is not outsourced but handled directly by the calculus. As several works mentioned above, the framework in [DP18, Doc19] does not provide for free a proof system for SL(*, -*) (which might have been a close cousin of the one in [GM10]). More importantly, similarly to the works [GM10, BV14, HCGT18], the labelled tableaux systems handle syntactic objects referring to semantical concepts related to the abstract separation logics that go beyond the only presence of formulae. In a way, modularity of the approach prevents from having a puristic calculus for SL(*, -*), apart from the fact that SL(*, *) is not part of the logics handled in [DP18].

**Axiomatising knowledge logics with reduction axioms.** In order to conclude this section, let us recall that the derivations in $\mathcal{H}_C(*, -*)$ are able to simulate the bottom-up elimination of separating connectives, leading to Boolean combinations of core formulae for which the system $\mathcal{H}_C(*, -*)$ is also complete. As the core formulae are (simple) formulae in $SL(*, -*)$, the axiomatisation provided by $\mathcal{H}_C(*, -*)$ uses only $SL(*, -*)$ formulae and is complete for the full logic $SL(*, -*)$ (and not only for Boolean combinations of core formulae). Note that as a by-product of our completeness proof for $SL(*, -*)$, we get expressive completeness of $SL(*, -*)$ with respect to Boolean combinations of core formulae, with a proof different from the developments in [Loz04a, BDL09, EIP19].

This general principle described above is familiar for axiomatising dynamic epistemic logics in which dynamic connectives might be eliminated with the help of so-called *reduction axioms*, see e.g. standard examples in [vDvdHK08, vB11, WC13, FVQ19]. In a nutshell, every formula containing a dynamic operator is provably reduced to a formula without such an operator. Completeness is then established thanks to the completeness of the underlying ‘basic’ language. A similar approach for the linear $\mu$-calculus is recently presented in [Dou17] for which a form of constructive completeness is advocated, see also [Lüc18]. Hilbert-style axiomatisations following similar high-level principles for the modal separation logics MSL(*,◊) and MSL(*,◊) introduced in [DF19], have been designed in [DFM19].

## 8. CONCLUSION

We presented a method to axiomatise internally quantifier-free separation logic $SL(*, -*)$ based on the axiomatisation of Boolean combinations of core formulae (and even more precisely, based on the restricted fragment of core types). We designed the first proof system for $SL(*, -*)$ that is completely internal and highlights the essential ingredients of the heaplet semantics. The fact that the calculus is internal simply means that the axioms and inference rules involve schemas instantiated by formulae in $SL(*, -*)$ (no use of nominals, labels or other syntactic objects that are not $SL(*, -*)$ formulae). Obviously, the Hilbert-style proof system presented in the paper is of theoretical interest, at least to grasp what are the essential features of $SL(*, -*)$. Still, it remains to be seen whether applications are possible for designing decision procedures, for instance to feed provers with appropriate axiom instances to accelerate the proof search. Furthermore, we have not investigated whether the proof system $\mathcal{H}_C(*, -*)$ (see Figure 1) can be simplified without losing completeness. This might be rewarding for using the calculus for other logics or for other applications. Most probably the most obvious part to study in that respect would be $\mathcal{H}_C(*).

To provide further evidence that our method is robust, it is desirable to apply it to axiomatisate other separation logics, for instance by adding the list segment predicate $ls$ [BCO04] (or more generally user-defined inductive predicates) or by adding first-order quantification.
A key step in our approach is first to show that the logic admits a characterisation in terms of core formulae and such formulae need to be designed adequately. Of course, it is required that the set of valid formulae is recursively enumerable, which discards any attempt with SL(*, →, 1s) or with the first-order version of SL(*, →) [DLM18a, BDL12]. The second part of the paper [DLM20] introduces an extension of SL(*, 1s) and presents an axiomatisation with our method. More separation logics could be axiomatised that way, other good candidates are the version of separation logic with one individual variable studied in [DGLWM17] as well as the quantifier-free separation logic with general universes from [EIP19].

**Acknowledgements.** We would like to thank the anonymous reviewers for their numerous remarks and suggestions that help us to improve the quality of the document.

## REFERENCES

[ABM01] C. Areces, P. Blackburn, and M. Marx. Hybrid logics: characterization, interpolation and complexity. *The Journal of Symbolic Logic*, 66(3):977–1010, 2001.

[BCO04] J. Berdine, C. Calcagno, and P.W. O'Hearn. A decidable fragment of separation logic. In *FST&TCS'04*, volume 3328 of LNCS, pages 97–109. Springer, 2004.

[BDL09] R. Brochenin, S. Demri, and É. Lozes. Reasoning about sequences of memory states. *Annals of Pure and Applied Logic*, 161(3):305–323, 2009.

[BDL12] R. Brochenin, S. Demri, and É. Lozes. On the almighty wand. *Information and Computation*, 211:106–137, 2012.

[BdRV01] P. Blackburn, M. de Rijke, and Y. Venema. *Modal Logic*. Cambridge University Press, 2001.

[Bel82] N. Belnap. Display logic. *Journal of Philosophical Logic*, 11:375–417, 1982.

[BIP10] M. Bozga, R. Iosif, and S. Perarnau. Quantitative separation logic and programs with lists. *Journal of Automated Reasoning*, 45(2):131–156, 2010.

[BK14] J. Brotherston and M. Kanovich. Undecidability of propositional separation logic and its neighbours. *Journal of the Association for Computing Machinery*, 61(2), 2014.

[BK18] J. Brotherston and M. Kanovich. On the complexity of pointer arithmetic in separation logic. In *APLAS'18*, volume 11275 of LNCS, pages 329–349. Springer, 2018.

[Bro12] J. Brotherston. Bunched logics displayed. *Studia Logica*, 100(6):1223–1254, 2012.

[BV14] J. Brotherston and J. Villard. Parametric completeness for separation theories. In *POPL'14*, pages 453–464. ACM, 2014.

[CGH05] C. Calcagno, Ph. Gardner, and M. Hague. From separation logic to first-order logic. In *FoSSaCS'05*, volume 3441 of LNCS, pages 395–409. Springer, 2005.

[CHO$^{+}$11] B. Cook, C. Haase, J. Ouaknine, M. Parkinson, and J. Worrell. Tractable reasoning in a fragment of separation logic. In *CONCUR'11*, volume 6901 of LNCS, pages 235–249. Springer, 2011.

[COY01] C. Calcagno, P.W. O'Hearn, and H. Yang. Computability and complexity results for a spatial assertion language for data structures. In *FST&TCS'01*, volume 2245 of LNCS, pages 108–119. Springer, 2001.

[DD15] S. Demri and M. Deters. Separation logics and modalities: A survey. *Journal of Applied Non-Classical Logics*, 25(1):50–99, 2015.

[DF19] S. Demri and R. Fervari. The power of modal separation logics. *Journal of Logic and Computation*, 29(8):1139–1184, 2019.

[DFM19] S. Demri, R. Fervari, and A. Mansutti. Axiomatising logics with separating conjunction and modalities. In *JELIA'19*, volume 11468 of LNAI, pages 692–708. Springer, 2019.

[DGLWM17] S. Demri, D. Galmiche, D. Larchey-Wendling, and D. Mery. Separation logic with one quantified variable. *Theory of Computing Systems*, 61:371–461, 2017.

[DLM18a] S. Demri, É. Lozes, and A. Mansutti. The effects of adding reachability predicates in propositional separation logic. In *FoSSaCS'18*, volume 10803 of LNCS, pages 476–493. Springer, 2018.
[DLM18b] S. Demri, É. Lozes, and A. Mansutti. The effects of adding reachability predicates in propositional separation logic. arXiv:1810.05410, October 2018. 44 pages. Long version of [DLM18a].

[DLM20] S. Demri, É. Lozes, and A. Mansutti. Internal calculi for separation logics. In *CSL '20*, Leibniz International Proceedings in Informatics, pages 19:1–19:18. Leibniz-Zentrum für Informatik, 2020.

[Doc19] S. Docherty. *Bunched logics: a uniform approach*. PhD thesis, University College London, 2019.

[Dou17] A. Doumane. Constructive completeness for the linear-time $\mu$-calculus. In *LiCS '17*, pages 1–12. IEEE Computer Society, 2017.

[DP18] S. Docherty and D. Pym. Modular tableaux calculi for separation theories. In *FoSSaCS '18*, volume 10803 of LNCS, pages 441–458. Springer, 2018.

[EIP19] M. Echenim, R. Iosif, and N. Peltier. The Bernays-Schönfinkel-Ramsey class of separation logic on arbitrary domains. In *FoSSaCS '19*, volume 11425 of LNCS, pages 242–259. Springer, 2019.

[FVQ19] R. Fervari and F. R. Velázquez-Quesada. Introspection as an action in relational models. *Journal of Logical and Algebraic Methods in Programming*, 108:1–23, 2019.

[Gab96] D. Gabbay. *Labelled Deductive Systems*. Oxford University Press, 1996.

[GLW06] D. Galmiche and D. Larchey-Wending. Expressivity properties of boolean BI through relational models. In *FST&TCS '06*, volume 4337 of LNCS, pages 358–369. Springer, 2006.

[GM05] D. Galmiche and D. Mery. Characterizing provability in BI's pointer logic through resource graphs. In *LPAR '05*, volume 3835 of LNCS, pages 459–473. Springer, 2005.

[GM10] D. Galmiche and D. Méry. Tableaux and resource graphs for separation logic. *Journal of Logic and Computation*, 20(1):189–231, 2010.

[GvD06] V. Goranko and G. van Drimmelen. Complete axiomatization and decidability of alternating-time temporal logic. *Theoretical Computer Science*, 353(1-3):93–117, 2006.

[HCGT18] Z. Hóu, R. Clouston, R. Goré, and A. Tiu. Modular labelled sequent calculi for abstract separation logics. *ACM Transactions on Computational Logic*, 19(2):13:1–13:35, 2018.

[HGT15] Z. Hóu, R. Goré, and A. Tiu. Automated theorem proving for assertions in separation logic with all connectives. In *CADE '15*, volume 9195 of LNCS, pages 501–516. Springer, 2015.

[Hóu15] Z. Hóu. *Labelled sequent calculi and automated reasoning for assertions in separation logic*. PhD thesis, Australian National University, November 2015.

[IO01] S. Ishtiaq and P.W. O'Hearn. BI as an assertion language for mutable data structures. In *POPL '01*, pages 14–26. ACM, 2001.

[Kai95] R. Kaivola. Axiomatising linear time mu-calculus. In *CONCUR '95*, volume 962 of LNCS, pages 423–437. Springer, 1995.

[LG13] D. Larchey-Wendling and D. Galmiche. Nondeterministic phase semantics and the undecidability of Boolean BI. *ACM Transactions on Computational Logic*, 14(1), 2013.

[LMX16] K.G. Larsen, R. Mardare, and B. Xue. Probabilistic mu-calculus: Decidability and complete axiomatization. In *FST&TCS '16*, volume 65 of LIPIcs, pages 25:1–25:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.

[Loz04a] É. Lozes. *Expressivité des Logiques Spatiales*. PhD thesis, ENS Lyon, 2004.

[Loz04b] É. Lozes. Separation logic preserves the expressive power of classical logic. In *SPACE '04*, 2004.

[Lüc18] M. Lück. Axiomatizations of team logics. *Annals of Pure and Applied Logic*, 169(9):928–969, 2018.

[Man18] A. Mansutti. Extending propositional separation logic for robustness properties. In *FST&TCS '18*, volume 122 of LIPIcs, pages 42:1–42:23. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018.

[Man20] A. Mansutti. *Reasoning with Separation Logics: Complexity, Expressive Power, Proof Systems*. PhD thesis, Université Paris-Saclay, December 2020.

[O'H12] P.W. O'Hearn. A primer on separation logic. In *Software Safety and Security: Tools for Analysis and Verification*, volume 33 of NATO Science for Peace and Security Series, pages 286–318, 2012.

[OP99] P.W. O'Hearn and D. Pym. The logic of bunched implications. *Bulletin of Symbolic Logic*, 5(2):215–244, 1999.

[PSO18] D. Pym, J. Spring, and P.W. O'Hearn. Why separation logic works. *Philosophy & Technology*, pages 1–34, 2018.
[PSP13] J. Park, J. Seo, and S. Park. A theorem prover for Boolean BI. In *POPL'13*, pages 219–232. ACM, 2013.

[PWZ13] R. Piskać, Th. Wies, and D. Zufferey. Automating separation logic using SMT. In *CAV'13*, volume 8044 of LNCS, pages 773–789. Springer, 2013.

[Pym02] D. Pym. *The Semantics and Proof Theory of the Logic of Bunched Implications*, volume 26 of Applied Logic. Kluwer Academic Publishers, 2002.

[Rey01] M. Reynolds. An axiomatization of full computation tree logic. *The Journal of Symbolic Logic*, 66(3):1011–1057, 2001.

[Rey02] J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In *LiCS'02*, pages 55–74. IEEE, 2002.

[RISK16] A. Reynolds, R. Iosif, C. Serban, and T. King. A decision procedure for separation logic in SMT. In *ATVA'16*, volume 9938 of LNCS, pages 244–261, 2016.

[Sah75] H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logics. In S. Kanger, editor, *3rd Scandinavian Logic Symposium, Uppsala, Sweden, 1973*, pages 110–143. North Holland, 1975.

[SV18] L. Schröder and Y. Venema. Completeness of flat coalgebraic fixpoint logics. *ACM Transactions on Computational Logic*, 19(1):4:1–4:34, 2018.

[vB11] J. van Benthem. *Logical Dynamics of Information and Interaction*. Cambridge University Press, 2011.

[vDvdHK08] H. van Ditmarsch, W. van der Hoek, and B. Kooi. *Dynamic Epistemic Logic*, volume 337 of Synthese Library Series. Springer, Dordrecht, 2008.

[Wal00] I. Walukiewicz. Completeness of Kozen's axiomatisation of the propositional μ-calculus. *Information and Computation*, 157(1–2):142–182, 2000.

[WC13] Y. Wang and Q. Cao. On axiomatizations of public announcement logic. *Synthese*, 190(Supplement-1):103–134, 2013.

[Yan01] H. Yang. *Local Reasoning for Stateful Programs*. PhD thesis, University of Illinois, Urbana-Champaign, 2001.
As in the rest of the paper, in the derivations below we use the following precedence between the various connectives of SL(*, -*): {¬} > {∧, ∨, *} > {⇒, -*, ⊕} > {↔}.

## APPENDIX A. PROOF OF LEMMA 5.2

*Proof of (I<sub>5.2.1</sub>).*

<table><tr><td>1</td><td>φ ⇒ (φ ∧ x ~ y) ∨ (φ ∧ ¬x ~ y)</td><td>PC</td></tr><tr><td>2</td><td>φ * ψ ⇒ ((φ ∧ x ~ y) ∨ (φ ∧ ¬x ~ y)) * ψ</td><td>*-Intro, 1</td></tr><tr><td>3</td><td>((φ ∧ x ~ y) ∨ (φ ∧ ¬x ~ y)) * ψ ⇒ ((φ ∧ x ~ y) * ψ) ∨ ((φ ∧ ¬x ~ y) * ψ)</td><td>(I<sub>9</sub><sup>*</sup>)</td></tr><tr><td>4</td><td>φ ∧ ¬x ~ y ⇒ ¬x ~ y</td><td>PC</td></tr><tr><td>5</td><td>ψ ⇒ ⊤</td><td>PC</td></tr><tr><td>6</td><td>(φ ∧ ¬x ~ y) * ψ ⇒ (¬x ~ y) * ⊤</td><td>*-Ilr, 4, 5</td></tr><tr><td>7</td><td>(¬x ~ y) * ⊤ ⇒ ¬x ~ y</td><td>(A<sub>14</sub><sup>*</sup>)</td></tr><tr><td>8</td><td>(φ ∧ ¬x ~ y) * ψ ⇒ ¬x ~ y</td><td>⇒-Tr, 6, 7</td></tr><tr><td>9</td><td>((φ ∧ x ~ y) * ψ) ∨ ((φ ∧ ¬x ~ y) * ψ) ⇒ ((φ ∧ x ~ y) * ψ) ∨ ¬x ~ y</td><td>8, PC</td></tr><tr><td>10</td><td>φ * ψ ⇒ ((φ ∧ x ~ y) * ψ) ∨ ¬x ~ y</td><td>⇒-Tr, 2, 3, 9</td></tr><tr><td>11</td><td>x ~ y ∧ (φ * ψ) ⇒ (φ ∧ x ~ y) * ψ</td><td>10, PC □</td></tr></table>

*Proof of (I<sub>5.2.2</sub>).*

<table><tr><td>1</td><td>alloc(x) ∧ x = y ⇒ alloc(y)</td><td>(A<sub>2</sub><sup>C</sup>)</td></tr><tr><td>2</td><td>x = y ∧ ((φ ∧ alloc(x)) * ψ) ⇒ ((φ ∧ alloc(x) ∧ x = y) * ψ)</td><td>(I<sub>5.2.1</sub><sup>*</sup>)</td></tr><tr><td>3</td><td>(φ ∧ alloc(x) ∧ x = y) * ψ ⇒ (φ ∧ alloc(y)) * ψ</td><td>PC, *-Intro, 1</td></tr><tr><td>4</td><td>x = y ∧ ((φ ∧ alloc(x)) * ψ) ⇒ (φ ∧ alloc(y)) * ψ</td><td>⇒-Tr, 2, 3 □</td></tr></table>

*Proof of (I<sub>5.2.3</sub>).*

<table><tr><td>1</td><td>ψ ⇒ (ψ ∧ alloc(x)) ∨ (ψ ∧ ¬alloc(x))</td><td>PC</td></tr><tr><td>2</td><td>(φ ∧ alloc(x)) * ψ ⇒<br/>(φ ∧ alloc(x)) * ((ψ ∧ alloc(x)) ∨ (ψ ∧ ¬alloc(x)))</td><td>(A<sub>7</sub><sup>*</sup>), *-Intro, 1</td></tr><tr><td>3</td><td>(φ ∧ alloc(x)) * ((ψ ∧ alloc(x)) ∨ (ψ ∧ ¬alloc(x))) ⇒<br/>((φ ∧ alloc(x)) * (ψ ∧ alloc(x))) ∨ ((φ ∧ alloc(x)) * (ψ ∧ ¬alloc(x)))</td><td>(A<sub>7</sub><sup>*</sup>), (I<sub>9</sub><sup>*</sup>), 2</td></tr><tr><td>4</td><td>χ ∧ alloc(x) ⇒ alloc(x)</td><td>(χ ∈ {φ, ψ}), PC</td></tr><tr><td>5</td><td>(φ ∧ alloc(x)) * (ψ ∧ alloc(x)) ⇒ alloc(x) * alloc(x)</td><td>*-Ilr, 4</td></tr><tr><td>6</td><td>alloc(x) * alloc(x) ⇒ ⊥</td><td>(A<sub>13</sub><sup>*</sup>)</td></tr><tr><td>7</td><td>(φ ∧ alloc(x)) * (ψ ∧ alloc(x)) ⇒ ⊥</td><td>⇒-Tr, 5, 6</td></tr><tr><td>8</td><td>(φ ∧ alloc(x)) * ψ ⇒ ⊥ ∨ ((φ ∧ alloc(x)) * (ψ ∧ ¬alloc(x)))</td><td>PC, 2, 3, 7</td></tr></table>
$$
\begin{array}{l@{\quad}l}
9 & (\varphi \wedge \text{alloc}(x)) * \psi \Rightarrow (\varphi \wedge \text{alloc}(x)) * (\psi \wedge \neg \text{alloc}(x)) & \text{PC, 8} \\
10 & \varphi \wedge \text{alloc}(x) \Rightarrow \varphi & \text{PC} \\
11 & (\varphi \wedge \text{alloc}(x)) * (\psi \wedge \neg \text{alloc}(x)) \Rightarrow \varphi * (\psi \wedge \neg \text{alloc}(x)) & \textit{-Intro, 10} \\
12 & (\varphi \wedge \text{alloc}(x)) * \psi \Rightarrow \varphi * (\psi \wedge \neg \text{alloc}(x)) & \Rightarrow\text{-Tr, 9, 11} \quad \square
\end{array}
$$

Proof of (I\*_5.2.4).

$$
\begin{array}{l@{\quad}l}
1 & \varphi \Rightarrow (\varphi \wedge \text{alloc}(x)) \lor (\varphi \wedge \neg \text{alloc}(x)) & \text{PC} \\
2 & \varphi * \psi \Rightarrow ((\varphi \wedge \text{alloc}(x)) \lor (\varphi \wedge \neg \text{alloc}(x))) * \psi & \textit{-Intro, 1} \\
3 & ((\varphi \wedge \text{alloc}(x)) \lor (\varphi \wedge \neg \text{alloc}(x))) * \psi \Rightarrow & \\
& ((\varphi \wedge \text{alloc}(x)) * \psi) \lor ((\varphi \wedge \neg \text{alloc}(x)) * \psi) & \text{(I\*_9)} \\
4 & \varphi \wedge \text{alloc}(x) \Rightarrow \text{alloc}(x) & \text{PC} \\
5 & \psi \Rightarrow \top & \text{PC} \\
6 & (\varphi \wedge \text{alloc}(x)) * \psi \Rightarrow (\text{alloc}(x) * \top) & \textit{-Ilr, 4, 5} \\
7 & \text{alloc}(x) * \top \Rightarrow \text{alloc}(x) & \text{(I\*_12)} \\
8 & \varphi * \psi \Rightarrow \text{alloc}(x) \lor ((\varphi \wedge \neg \text{alloc}(x)) * \psi) & \text{PC, 2, 3, 6, 7} \\
9 & \neg \text{alloc}(x) \wedge (\varphi * \varphi) \Rightarrow (\varphi \wedge \neg \text{alloc}(x)) * \psi & \text{PC, 8} \quad \square
\end{array}
$$

Proof of (I\*_5.2.5).

$$
\begin{array}{l@{\quad}l}
1 & \varphi \Rightarrow (\varphi \wedge \text{alloc}(x)) \lor (\varphi \wedge \neg \text{alloc}(x)) & \text{PC} \\
2 & \varphi * (\neg \text{alloc}(x) \wedge \psi) \Rightarrow \\
& ((\varphi \wedge \text{alloc}(x)) * (\psi \wedge \neg \text{alloc}(x))) \lor ((\varphi \wedge \neg \text{alloc}(x)) * (\psi \wedge \neg \text{alloc}(x))) & \textit{-Intro, 1, (I\*_9)} \\
3 & \chi \wedge \neg \text{alloc}(x) \Rightarrow \neg \text{alloc}(x) & (\chi \in \{\varphi, \psi\}), \text{PC} \\
4 & (\varphi \wedge \neg \text{alloc}(x)) * (\psi \wedge \neg \text{alloc}(x)) \Rightarrow \neg \text{alloc}(x) * \neg \text{alloc}(x) & \text{PC, -Ilr, 3} \\
5 & \neg \text{alloc}(x) * \neg \text{alloc}(x) \Rightarrow \neg \text{alloc}(x) & \text{(A\*_15)} \\
6 & \varphi * (\neg \text{alloc}(x) \wedge \psi) \Rightarrow ((\varphi \wedge \text{alloc}(x)) * (\psi \wedge \neg \text{alloc}(x))) \lor \neg \text{alloc}(x) & \text{PC, 2, 4, 5} \\
7 & \text{alloc}(x) \wedge (\varphi * (\neg \text{alloc}(x) \wedge \psi)) \Rightarrow (\varphi \wedge \text{alloc}(x)) * (\psi \wedge \neg \text{alloc}(x)) & \text{PC, 6} \quad \square
\end{array}
$$

Proof of (I\*_5.2.6).

$$
\begin{array}{l@{\quad}l}
1 & \varphi \wedge \text{alloc}(x) \Rightarrow (\varphi \wedge \text{alloc}(x) \wedge x \leftrightarrow y) \lor (\varphi \wedge \text{alloc}(x) \wedge \neg x \leftrightarrow y) & \text{PC} \\
2 & (\varphi \wedge \text{alloc}(x)) * \psi \Rightarrow \\
& ((\varphi \wedge \text{alloc}(x) \wedge x \leftrightarrow y) \lor (\varphi \wedge \text{alloc}(x) \wedge \neg x \leftrightarrow y)) * \psi & \textit{-Intro, 1} \\
3 & (\varphi \wedge \text{alloc}(x)) * \psi \Rightarrow \\
& ((\varphi \wedge \text{alloc}(x) \wedge x \leftrightarrow y) * \psi) \lor ((\varphi \wedge \text{alloc}(x) \wedge \neg x \leftrightarrow y) * \psi) & \text{(I\*_9)}, \Rightarrow\text{-Tr, 2} \\
4 & \varphi \wedge \text{alloc}(x) \wedge \neg x \leftrightarrow y \Rightarrow \text{alloc}(x) \wedge \neg x \leftrightarrow y & \text{PC}
\end{array}
$$
<table><tr><td>5</td><td>ψ ⇒ ⊤</td><td>PC</td></tr><tr><td>6</td><td>(φ ∧ alloc(x) ∧ ¬x ↦ y) * ψ ⇒ (alloc(x) ∧ ¬x ↦ y) * ⊤</td><td>*-Ilr</td></tr><tr><td>7</td><td>(alloc(x) ∧ ¬x ↦ y) * ⊤ ⇒ ¬x ↦ y</td><td>(A<sub>16</sub><sup>*</sup>)</td></tr><tr><td>8</td><td>(φ ∧ alloc(x)) * ψ ⇒ ((φ ∧ alloc(x) ∧ x ↦ y) * ψ) ∨ ¬x ↦ y</td><td>PC, 3, 6, 7</td></tr><tr><td>9</td><td>x ↦ y ∧ ((alloc(x) ∧ φ) * ψ) ⇒ (φ ∧ alloc(x) ∧ x ↦ y) * ψ</td><td>PC, 8</td></tr><tr><td>10</td><td>φ ∧ alloc(x) ∧ x ↦ y ⇒ φ ∧ x ↦ y</td><td>PC</td></tr><tr><td>11</td><td>(φ ∧ alloc(x) ∧ x ↦ y) * ψ ⇒ (φ ∧ x ↦ y) * ψ</td><td>*-Intro, 10</td></tr><tr><td>12</td><td>x ↦ y ∧ ((alloc(x) ∧ φ) * ψ) ⇒ (φ ∧ x ↦ y) * ψ</td><td>⇒-Tr, 9, 11 ☐</td></tr></table>

Proof of (I<sub>5.2.7</sub><sup>*</sup>). Similar to the proof of (I<sub>5.2.4</sub><sup>*</sup>), by replacing alloc(x) with x ↦ y.

<table><tr><td>1</td><td>φ ⇒ (φ ∧ x ↦ y) ∨ (φ ∧ ¬x ↦ y)</td><td>PC</td></tr><tr><td>2</td><td>φ * ψ ⇒ ((φ ∧ x ↦ y) * ψ) ∨ ((φ ∧ ¬x ↦ y) * ψ)</td><td>*-Intro, 1, (I<sub>9</sub><sup>*</sup>)</td></tr><tr><td>3</td><td>φ ∧ x ↦ y ⇒ x ↦ y</td><td>PC</td></tr><tr><td>4</td><td>ψ ⇒ ⊤</td><td>PC</td></tr><tr><td>5</td><td>(φ ∧ x ↦ y) * ψ ⇒ (x ↦ y * ⊤)</td><td>*-Ilr, 3, 4</td></tr><tr><td>6</td><td>x ↦ y * ⊤ ⇒ x ↦ y</td><td>(A<sub>14</sub><sup>*</sup>)</td></tr><tr><td>7</td><td>φ * ψ ⇒ x ↦ y ∨ ((φ ∧ ¬x ↦ y) * ψ)</td><td>PC, 2, 5, 6</td></tr><tr><td>8</td><td>¬x ↦ y ∧ (φ * ψ) ⇒ (φ ∧ ¬x ↦ y) * ψ</td><td>PC, 7 ☐</td></tr></table>

## APPENDIX B. DERIVATION OF THE size FORMULAE REQUIRED FOR LEMMA 5.4

In this appendix, we show the derivations in $\mathcal{H}_C(*)$ of $size \ge \beta_1+\beta_2 \Rightarrow size = \beta_1*size \ge \beta_2$ and $size = \beta_1+\beta_2 \Rightarrow size = \beta_1*size = \beta_2$, which are required for the proof of Lemma 5.4.

The derivation of $size \ge \beta_1+\beta_2 \Rightarrow size = \beta_1*size \ge \beta_2$ is proven by induction on $\beta_1$. The derivation for the base case $\beta_1 = 0$ is:

<table><tr><td>1</td><td>size ≥ β<sub>2</sub> ⇒ emp * size ≥ β<sub>2</sub></td><td>(A<sub>11</sub><sup>*</sup>)</td></tr><tr><td>2</td><td>emp ⇒ size ≥ 0 ∧ ¬size ≥ 1</td><td>PC, def. of size ≥ 1</td></tr><tr><td>3</td><td>emp * size ≥ β<sub>2</sub> ⇒ size = 0 * size ≥ β<sub>2</sub></td><td>*-Intro, 2, def. of size = 0</td></tr><tr><td>4</td><td>size ≥ β<sub>2</sub> ⇒ size = 0 * size ≥ β<sub>2</sub></td><td>⇒-Tr, 1, 3</td></tr></table>

For the induction step, let us suppose the formula to be derivable for a certain $\beta_1$, and let us prove that it is also derivable for $\beta_1 + 1$.

<table><tr><td>1</td><td>size ≥ β<sub>1</sub> + 1 + β<sub>2</sub> ⇒ size ≥ 1 * size ≥ β<sub>1</sub> + β<sub>2</sub></td><td>def. of size ≥ β, (A<sub>7</sub><sup>*</sup>), (A<sub>8</sub><sup>*</sup>)</td></tr><tr><td>2</td><td>size ≥ 1 ⇒ size = 1 * ⊤</td><td>(A<sub>18</sub><sup>*</sup>), def. of size ≥ 1</td></tr><tr><td>3</td><td>size ≥ 1 * size ≥ β<sub>1</sub> + β<sub>2</sub> ⇒ (size = 1 * ⊤) * size ≥ β<sub>1</sub> + β<sub>2</sub></td><td>*-Intro, 2</td></tr></table>
<table>
  <tbody>
    <tr>
      <td>4</td>
      <td>(size = 1 * T) * size ≥ β₁ + β₂ ⇒<br>size = 1 * size ≥ β₁ + β₂</td>
      <td>PC, (A<sub>7</sub><sup>*</sup>), (A<sub>8</sub><sup>*</sup>), (A<sub>14</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>5</td>
      <td>size ≥ β₁ + β₂ ⇒ size = β₁ * size ≥ β₂</td>
      <td>Induction Hypothesis</td>
    </tr>
    <tr>
      <td>6</td>
      <td>size = 1 * size ≥ β₁ + β₂ ⇒<br>(size = 1 * size = β₁) * size ≥ β₂</td>
      <td>(A<sub>7</sub><sup>*</sup>), *-Intro, (A<sub>8</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>7</td>
      <td>size = β̃ ⇒ size ≥ β̃</td>
      <td>PC, def. of size = β̃</td>
    </tr>
    <tr>
      <td>8</td>
      <td>size = β̃ ⇒ ¬size ≥ β̃ + 1</td>
      <td>PC, def. of size = β̃</td>
    </tr>
    <tr>
      <td>9</td>
      <td>size = 1 * size = β₁ ⇒ size ≥ 1 * size ≥ β₁</td>
      <td>*-Ilr, 7</td>
    </tr>
    <tr>
      <td>10</td>
      <td>size = 1 * size = β₁ ⇒ ¬size ≥ 2 * ¬size ≥ β₁ + 1</td>
      <td>*-Ilr, 8</td>
    </tr>
    <tr>
      <td>11</td>
      <td>size ≥ 1 * size ≥ β₁ ⇒ size ≥ β₁ + 1</td>
      <td>def. of size ≥ β, (A<sub>7</sub><sup>*</sup>), (A<sub>8</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>12</td>
      <td>¬size ≥ 2 * ¬size ≥ β₁ + 1 ⇒ ¬size ≥ β₁ + 2</td>
      <td>(A<sub>19</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>13</td>
      <td>size = 1 * size = β₁ ⇒ size = β₁ + 1</td>
      <td>PC, 9–12, def. of size = β₁</td>
    </tr>
    <tr>
      <td>14</td>
      <td>(size = 1 * size = β₁) * size ≥ β₂ ⇒<br>size = β₁ + 1 * size ≥ β₂</td>
      <td>*-Intro, 13</td>
    </tr>
    <tr>
      <td>15</td>
      <td>size ≥ β₁ + 1 + β₂ ⇒ size = β₁ + 1 * size ≥ β₂</td>
      <td>⇒-Tr, 1, 3, 4, 6, 14</td>
    </tr>
  </tbody>
</table>

The derivation of the formula $size = \beta_1 + \beta_2 \Rightarrow size = \beta_1 * size = \beta_2$ is provided below.

<table>
  <tbody>
    <tr>
      <td>1</td>
      <td>size = β<sub>1</sub> + β<sub>2</sub> ⇒ size ≥ β<sub>1</sub> + β<sub>2</sub></td>
      <td>PC, def. of size = β</td>
    </tr>
    <tr>
      <td>2</td>
      <td>size ≥ β<sub>1</sub> + β<sub>2</sub> ⇒ size = β<sub>1</sub> * size ≥ β<sub>2</sub></td>
      <td>Previously derived</td>
    </tr>
    <tr>
      <td>3</td>
      <td>size ≥ β<sub>2</sub> ⇒ (size ≥ β<sub>2</sub> ∧ size ≥ β<sub>2</sub> + 1) ∨ size = β<sub>2</sub></td>
      <td>PC, def. of size = β<sub>2</sub></td>
    </tr>
    <tr>
      <td>4</td>
      <td>size = β<sub>1</sub> * size ≥ β<sub>2</sub> ⇒<br>size = β<sub>1</sub> * ((size ≥ β<sub>2</sub> ∧ size ≥ β<sub>2</sub> + 1) ∨ size = β<sub>2</sub>)</td>
      <td>(A<sub>7</sub><sup>*</sup>), *-Intro, 3</td>
    </tr>
    <tr>
      <td>5</td>
      <td>size = β<sub>1</sub> * ((size ≥ β<sub>2</sub> ∧ size ≥ β<sub>2</sub> + 1) ∨ size = β<sub>2</sub>) ⇒<br>(size = β<sub>1</sub> * (size ≥ β<sub>2</sub> ∧ size ≥ β<sub>2</sub> + 1)) ∨ (size = β<sub>1</sub> * size = β<sub>2</sub>)</td>
      <td>(A<sub>7</sub><sup>*</sup>), (I<sub>9</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>6</td>
      <td>size ≥ β̃ ∧ χ ⇒ size ≥ β̃</td>
      <td>PC</td>
    </tr>
    <tr>
      <td>7</td>
      <td>size = β<sub>1</sub> * (size ≥ β<sub>2</sub> ∧ size ≥ β<sub>2</sub> + 1) ⇒<br>size ≥ β<sub>1</sub> * size ≥ β<sub>2</sub> + 1</td>
      <td>PC, *-Ilr, 6</td>
    </tr>
    <tr>
      <td>8</td>
      <td>size ≥ β<sub>1</sub> * size ≥ β<sub>2</sub> + 1 ⇒ size ≥ β<sub>1</sub> + β<sub>2</sub> + 1</td>
      <td>(A<sub>7</sub><sup>*</sup>), (A<sub>8</sub><sup>*</sup>)</td>
    </tr>
    <tr>
      <td>9</td>
      <td>size = β<sub>1</sub> * (size ≥ β<sub>2</sub> ∧ size ≥ β<sub>2</sub> + 1) ⇒ size ≥ β<sub>1</sub> + β<sub>2</sub> + 1</td>
      <td>⇒-Tr, 7, 8</td>
    </tr>
    <tr>
      <td>10</td>
      <td>size = β<sub>1</sub> * ((size ≥ β<sub>2</sub> ∧ size ≥ β<sub>2</sub> + 1) ∨ size = β<sub>2</sub>) ⇒<br>size ≥ β<sub>1</sub> + β<sub>2</sub> + 1 ∨ (size = β<sub>1</sub> * size = β<sub>2</sub>)</td>
      <td>PC, 5, 9</td>
    </tr>
    <tr>
      <td>11</td>
      <td>size = β<sub>1</sub> + β<sub>2</sub> ⇒ size ≥ β<sub>1</sub> + β<sub>2</sub> + 1 ∨ (size = β<sub>1</sub> * size = β<sub>2</sub>)</td>
      <td>⇒-Tr, 1, 2, 4, 10</td>
    </tr>
    <tr>
      <td>12</td>
      <td>size = β<sub>1</sub> + β<sub>2</sub> ⇒ ¬size ≥ β<sub>1</sub> + β<sub>2</sub> + 1</td>
      <td>PC, def. of size = β</td>
    </tr>
    <tr>
      <td>13</td>
      <td>size = β<sub>1</sub> + β<sub>2</sub> ⇒ size = β<sub>1</sub> * size = β<sub>2</sub></td>
      <td>PC, 11, 12</td>
    </tr>
  </tbody>
</table>
## APPENDIX C. PROOF OF LEMMA 6.1

*Proof of (I\*_9).*

<table><tr><td>1</td><td>(φ * χ) ⇒ (φ * χ) ∨ (ψ * χ)</td><td>PC</td></tr><tr><td>2</td><td>(ψ * χ) ⇒ (φ * χ) ∨ (ψ * χ)</td><td>PC</td></tr><tr><td>3</td><td>φ ⇒ (χ -* (φ * χ) ∨ (ψ * χ))</td><td>*-Adj, 1</td></tr><tr><td>4</td><td>ψ ⇒ (χ -* (φ * χ) ∨ (ψ * χ))</td><td>*-Adj, 2</td></tr><tr><td>5</td><td>φ ∨ ψ ⇒ (χ -* (φ * χ) ∨ (ψ * χ))</td><td>PC, 3, 4</td></tr><tr><td>6</td><td>(φ ∨ ψ) * χ ⇒ (φ * χ) ∨ (ψ * χ)</td><td>*-Adj, 5 ☐</td></tr></table>

*Proof of (I\*_10).* The axiom (I\*_10) is provable by *-Adj. Indeed, proving (⊥ * φ) ⇒ ⊥ reduces to proving ⊥ ⇒ (φ-* ⊥). The latter is a tautology by propositional reasoning. ☐

*Proof of (I\*_12).*

<table><tr><td>1</td><td>⊥ * ⊤ ⇒ ⊥</td><td>(I\*_10)</td></tr><tr><td>2</td><td>(x ↣ x-* ⊥) ⇒ (x ↣ x-* ⊥)</td><td>PC</td></tr><tr><td>3</td><td>(x ↣ x-* ⊥) * x ↣ x ⇒ ⊥</td><td>*-Adj, 2</td></tr><tr><td>4</td><td>x ↣ x * (x ↣ x-* ⊥) ⇒ (x ↣ x-* ⊥) * x ↣ x</td><td>(A\*_7)</td></tr><tr><td>5</td><td>x ↣ x * (x ↣ x-* ⊥) ⇒ ⊥</td><td>⇒-Tr, 4, 3</td></tr><tr><td>6</td><td>((x ↣ x-* ⊥) * ⊤) * (x ↣ x) ⇒ (x ↣ x * (x ↣ x-* ⊥)) * ⊤</td><td>*-Intro, 5</td></tr><tr><td>7</td><td>((x ↣ x-* ⊥) * ⊤) * (x ↣ x) ⇒ ⊥</td><td>(A\*_7), (A\*_8)</td></tr><tr><td>8</td><td>((x ↣ x-* ⊥) * ⊤) * (x ↣ x) ⇒ ⊥</td><td>⇒-Tr, 7, 6, 1</td></tr><tr><td>9</td><td>(x ↣ x-* ⊥) * ⊤ ⇒ (x ↣ x-* ⊥)</td><td>*-Adj, 8</td></tr><tr><td>10</td><td>alloc(x) * ⊤ ⇒ alloc(x)</td><td>Def. alloc(x), 9 ☐</td></tr></table>

## APPENDIX D. PROOF OF LEMMA 6.3

*Proof of (I\*_6.3.1).*

<table><tr><td>1</td><td>⊥ * ⊤ ⇒ ⊥</td><td>(I\*_10)</td><td>4</td><td>⊤ ⇒ (⊥ -*¬φ)</td><td>(A\*_7), *-Adj</td></tr><tr><td>2</td><td>⊥ ⇒ ¬φ</td><td>PC</td><td>5</td><td>⊤ ⇒ ¬(⊥ ⊗ φ)</td><td>Def. ⊗, PC</td></tr><tr><td>3</td><td>⊥ * ⊤ ⇒ ¬φ</td><td>⇒-Tr, 1, 2</td><td>6</td><td>(⊥ ⊗ φ) ⇒ ⊥</td><td>5, PC ☐</td></tr></table>

*Proof of (I\*_6.3.2).*

<table><tr><td>1</td><td>⊤ * φ ⇒ ⊤</td><td>PC</td><td>3</td><td>¬(φ -* ⊤) ⇒ ⊥</td><td>PC, 2</td></tr><tr><td>2</td><td>⊤ ⇒ (φ -* ⊤)</td><td>*-Adj</td><td>4</td><td>(φ ⊗ ⊥) ⇒ ⊥</td><td>Def. ⊗, PC</td></tr></table>
Note that implicitly, we have assumed that we can replace $\neg \top$ by $\bot$ in the scope of $\otimes$ or $-*$, which is possible as the replacement of equivalents holds in the calculus $\mathcal{H}_C(*, -*)$ (see e.g. the proof of Theorem 6.5). $\square$

### Proof of ($\mathbf{I}_{6.3.3}^*$).

$$
\begin{array}{lcl}
1 & (\varphi * \psi) \Rightarrow (\varphi * \psi) & \text{PC} \\
2 & (\varphi * \psi) * \varphi \Rightarrow \psi & \text{\*-Adj, 1} \\
3 & \varphi * (\varphi * \psi) \Rightarrow (\varphi * \psi) * \varphi & (\mathbf{A}_7^*) \\
4 & \varphi * (\varphi * \psi) \Rightarrow \psi & \Rightarrow \text{-Tr, 3, 2} \quad \square
\end{array}
$$

### Proof of ($\mathbf{I}_{6.3.4}^*$).

$$
\begin{array}{lcl}
1 & \varphi \Rightarrow \psi & \text{Hypothesis} \\
2 & \psi * (\psi * \neg \chi) \Rightarrow \neg \chi & (\mathbf{I}_{6.3.3}^*) \\
3 & (\psi * \neg \chi) * \varphi \Rightarrow \varphi * (\psi * \neg \chi) & (\mathbf{A}_7^*) \\
4 & \varphi * (\psi * \neg \chi) \Rightarrow \psi * (\psi * \neg \chi) & \text{\*-Intro, 1} \\
5 & \varphi * (\psi * \neg \chi) \Rightarrow \neg \chi & \Rightarrow \text{-Tr, 2, 4} \\
6 & (\psi * \neg \chi) * \varphi \Rightarrow \neg \chi & \Rightarrow \text{-Tr, 3, 5} \\
7 & \psi * \neg \chi \Rightarrow \varphi * \neg \chi & \text{\*-Adj, 6} \\
8 & \neg (\varphi * \neg \chi) \Rightarrow \neg (\psi * \neg \chi) & \text{PC, 7} \\
9 & (\varphi \otimes \chi) \Rightarrow (\psi \otimes \chi) & \text{Def. } \otimes, 8 \quad \square
\end{array}
$$

### Proof of ($\mathbf{I}_{6.3.5}^*$).

$$
\begin{array}{lcl}
1 & \varphi \Rightarrow \psi & \text{Hypothesis} \\
2 & \neg \psi \Rightarrow \neg \varphi & \text{PC, 1} \\
3 & \chi * (\chi * \neg \psi) \Rightarrow \neg \psi & (\mathbf{I}_{6.3.3}^*) \\
4 & \chi * (\chi * \neg \psi) \Rightarrow \neg \varphi & \Rightarrow \text{-Tr, 3, 2} \\
5 & (\chi * \neg \psi) * \chi \Rightarrow \chi * (\chi * \neg \psi) & (\mathbf{A}_7^*) \\
6 & (\chi * \neg \psi) * \chi \Rightarrow \neg \varphi & \Rightarrow \text{-Tr, 4, 5} \\
7 & (\chi * \neg \psi) \Rightarrow (\chi * \neg \varphi) & \text{\*-Adj, 6} \\
8 & \neg (\chi * \neg \varphi) \Rightarrow \neg (\chi * \neg \psi) & \text{PC, 7} \\
9 & (\chi \otimes \varphi) \Rightarrow (\chi \otimes \psi) & \text{Def. } \otimes \quad \square
\end{array}
$$

### Proof of ($\mathbf{I}_{6.3.6}^*$). By definition of the separation operator $\otimes$, ($\mathbf{I}_{6.3.6}^*$) is equivalent to $\varphi * (\psi * \neg \chi) \Leftrightarrow (\varphi * \psi) * \neg \chi$. This equivalence is provable in $\mathcal{H}_C(*, -*)$, thanks to the adjunction rules, as we now show.
<table><tr><td>1</td><td>(φ * ψ) * (φ * ψ * ¬χ) ⇒ ¬χ</td><td>(I<sub>6.3.3</sub><sup>*</sup>)</td></tr><tr><td>2</td><td>ψ * (φ * (φ * ψ * ¬χ)) ⇒ ¬χ</td><td>(A<sub>7</sub><sup>*</sup>), (A<sub>8</sub><sup>*</sup>), 1</td></tr><tr><td>3</td><td>φ * (φ * ψ * ¬χ) ⇒ (ψ * ¬χ)</td><td>*-Adj, 2</td></tr><tr><td>4</td><td>(φ * ψ * ¬χ) ⇒ (φ * (ψ * ¬χ))</td><td>*-Adj, 3, (A<sub>7</sub><sup>*</sup>)</td></tr><tr><td>5</td><td>φ * (φ * (ψ * ¬χ)) ⇒ (ψ * ¬χ)</td><td>(I<sub>6.3.3</sub><sup>*</sup>)</td></tr><tr><td>6</td><td>ψ * φ * (φ * (ψ * ¬χ)) ⇒ ¬χ</td><td>*-Adj, 5, (A<sub>7</sub><sup>*</sup>), (A<sub>8</sub><sup>*</sup>)</td></tr><tr><td>7</td><td>(φ * ψ) * (φ * (ψ * ¬χ)) ⇒ ¬χ</td><td>(A<sub>7</sub><sup>*</sup>), (A<sub>8</sub><sup>*</sup>), 6</td></tr><tr><td>8</td><td>(φ * (ψ * ¬χ)) ⇒ (φ * ψ * ¬χ)</td><td>*-Adj, 7</td></tr><tr><td>9</td><td>φ * (ψ * ¬χ) ⇔ (φ * ψ) * ¬χ</td><td>PC, 4, 8 □</td></tr></table>

Proof of (I<sub>6.3.7</sub><sup>*</sup>). We derive each implication separately.

<table><tr><td>1</td><td>(φ * ¬χ) ∧ (ψ * ¬χ) ⇒ (ψ * ¬χ)</td><td>PC</td></tr><tr><td>2</td><td>ψ * ((φ * ¬χ) ∧ (ψ * ¬χ)) ⇒ ψ * (ψ * ¬χ)</td><td>*-Ilr, 1</td></tr><tr><td>3</td><td>(φ * ¬χ) ∧ (ψ * ¬χ) ⇒ (φ * ¬χ)</td><td>PC</td></tr><tr><td>4</td><td>φ * ((φ * ¬χ) ∧ (ψ * ¬χ)) ⇒ φ * (φ * ¬χ)</td><td>*-Ilr, 3</td></tr><tr><td>5</td><td>φ * (φ * ¬χ) ⇒ ¬χ</td><td>(I<sub>6.3.3</sub><sup>*</sup>)</td></tr><tr><td>6</td><td>ψ * (ψ * ¬χ) ⇒ ¬χ</td><td>(I<sub>6.3.3</sub><sup>*</sup>)</td></tr><tr><td>7</td><td>ψ * ((φ * ¬χ) ∧ (ψ * ¬χ)) ⇒ ¬χ</td><td>⇒-Tr, 2, 6</td></tr><tr><td>8</td><td>φ * ((φ * ¬χ) ∧ (ψ * ¬χ)) ⇒ ¬χ</td><td>⇒-Tr, 4, 5</td></tr><tr><td>9</td><td>(φ ∨ ψ) * ((φ * ¬χ) ∧ (ψ * ¬χ)) ⇒<br/>(φ * (φ * ¬χ ∧ ψ * ¬χ)) ∨ (ψ * (φ * ¬χ ∧ ψ * ¬χ))</td><td>(I<sub>9</sub><sup>*</sup>)</td></tr><tr><td>10</td><td>(φ ∨ ψ) * ((φ * ¬χ) ∧ (ψ * ¬χ)) ⇒ ¬χ</td><td>PC, 7, 8, 9</td></tr><tr><td>11</td><td>((φ * ¬χ) ∧ (ψ * ¬χ)) * (φ ∨ ψ) ⇒ (φ ∨ ψ) * ((φ * ¬χ) ∧ (ψ * ¬χ))</td><td>(A<sub>7</sub><sup>*</sup>)</td></tr><tr><td>12</td><td>((φ * ¬χ) ∧ (ψ * ¬χ)) * (φ ∨ ψ) ⇒ ¬χ</td><td>⇒-Tr, 12, 10</td></tr><tr><td>13</td><td>(φ * ¬χ) ∧ (ψ * ¬χ) ⇒ (φ ∨ ψ * ¬χ)</td><td>*-Adj, 12</td></tr><tr><td>14</td><td>¬(φ ∨ ψ * ¬χ) ⇒ ¬(φ * ¬χ) ∨ ¬(ψ * ¬χ)</td><td>PC, 13</td></tr><tr><td>15</td><td>(φ ∨ ψ ⊗ χ) ⇒ (φ ⊗ χ) ∨ (ψ ⊗ χ)</td><td>Def. ⊗, 14</td></tr></table>

The derivation of the other implication can be found below.

<table><tr><td>1</td><td>φ ⇒ φ ∨ ψ</td><td>PC</td></tr><tr><td>2</td><td>ψ ⇒ φ ∨ ψ</td><td>PC</td></tr><tr><td>3</td><td>(φ ⊗ χ) ⇒ (φ ∨ ψ ⊗ χ)</td><td>(I<sub>6.3.4</sub><sup>*</sup>), 1</td></tr><tr><td>4</td><td>(ψ ⊗ χ) ⇒ (φ ∨ ψ ⊗ χ)</td><td>(I<sub>6.3.4</sub><sup>*</sup>), 2</td></tr><tr><td>5</td><td>(ψ ⊗ χ) ∨ (φ ⊗ χ) ⇒ (φ ∨ ψ ⊗ χ)</td><td>PC, 3, 4 □</td></tr></table>
*Proof of (I<sub>6.3.8</sub><sup>*</sup>). We handle each implication separately, and we follow a pattern similar to the one used in the proof of (I<sub>6.3.7</sub><sup>*</sup>).*

<table><tr><td>1</td><td>χ * (χ * ¬φ) ⇒ ¬φ</td><td>(I<sub>6.3.3</sub><sup>*</sup>)</td></tr><tr><td>2</td><td>(χ * ¬φ) ∧ (χ * ¬ψ) ⇒ χ * ¬φ</td><td>PC</td></tr><tr><td>3</td><td>χ * ((χ * ¬φ) ∧ (χ * ¬ψ)) ⇒ χ * (χ * ¬φ)</td><td>*-Ilr, 2</td></tr><tr><td>4</td><td>χ * ((χ * ¬φ) ∧ (χ * ¬ψ)) ⇒ ¬φ</td><td>⇒-Tr, 3, 1</td></tr><tr><td>5</td><td>χ * (χ * ¬ψ) ⇒ ¬ψ</td><td>(I<sub>6.3.3</sub><sup>*</sup>)</td></tr><tr><td>6</td><td>(χ * ¬φ) ∧ (χ * ¬ψ) ⇒ (χ * ¬ψ)</td><td>PC</td></tr><tr><td>7</td><td>χ * ((χ * ¬φ) ∧ (χ * ¬ψ)) ⇒ χ * (χ * ¬ψ)</td><td>*-Ilr, 6</td></tr><tr><td>8</td><td>χ * ((χ * ¬φ) ∧ (χ * ¬ψ)) ⇒ ¬ψ</td><td>⇒-Tr, 7, 5</td></tr><tr><td>9</td><td>χ * ((χ * ¬φ) ∧ (χ * ¬ψ)) ⇒ ¬(φ ∨ ψ)</td><td>PC, 4, 8</td></tr><tr><td>10</td><td>((χ * ¬φ) ∧ (χ * ¬ψ)) * χ ⇒ ¬(φ ∨ ψ)</td><td>(A<sub>7</sub><sup>*</sup>) + ⇒-Tr, 9</td></tr><tr><td>11</td><td>(χ * ¬φ) ∧ (χ * ¬ψ) ⇒ (χ * ¬(φ ∨ ψ))</td><td>*-Adj, 10</td></tr><tr><td>12</td><td>¬(χ * ¬(φ ∨ ψ)) ⇒ ¬(χ * ¬φ) ∨ ¬(χ * ¬ψ)</td><td>PC, 11</td></tr><tr><td>13</td><td>(χ ⊗ (φ ∨ ψ)) ⇒ (χ ⊗ φ) ∨ (χ ⊗ ψ)</td><td>Def. ⊗, 12</td></tr></table>

The derivation of the other implication can be found below.

<table><tr><td>1</td><td>φ ⇒ φ ∨ ψ</td><td>PC</td></tr><tr><td>2</td><td>ψ ⇒ φ ∨ ψ</td><td>PC</td></tr><tr><td>3</td><td>(χ ⊗ φ) ⇒ (χ ⊗ φ ∨ ψ)</td><td>(I<sub>6.3.5</sub><sup>*</sup>), 1</td></tr><tr><td>4</td><td>(χ ⊗ ψ) ⇒ (χ ⊗ φ ∨ ψ)</td><td>(I<sub>6.3.5</sub><sup>*</sup>), 2</td></tr><tr><td>5</td><td>(χ ⊗ φ) ∨ (χ ⊗ ψ) ⇒ (χ ⊗ φ ∨ ψ)</td><td>PC, 3, 4 □</td></tr></table>

*Proof of (I<sub>6.3.9</sub><sup>*</sup>).*

<table><tr><td>1</td><td>φ * (φ * χ) ⇒ χ</td><td>(I<sub>6.3.3</sub><sup>*</sup>)</td></tr><tr><td>2</td><td>φ * (φ * ¬(ψ ∧ χ)) ⇒ ¬(ψ ∧ χ)</td><td>(I<sub>6.3.3</sub><sup>*</sup>)</td></tr><tr><td>3</td><td>(φ * (φ * χ)) ∧ (φ * (φ * ¬(ψ ∧ χ))) ⇒ ¬ψ</td><td>PC, 1, 2</td></tr><tr><td>4</td><td>φ * ((φ * χ) ∧ (φ * ¬(ψ ∧ χ))) ⇒<br/>(φ * (φ * χ)) ∧ (φ * (φ * ¬(ψ ∧ χ)))</td><td>*-Ilr, PC<br/>⇒-Tr, 4</td></tr><tr><td>5</td><td>φ * ((φ * χ) ∧ (φ * ¬(ψ ∧ χ))) ⇒ ¬ψ</td><td>(A<sub>7</sub><sup>*</sup>), *-Adj, 5</td></tr><tr><td>6</td><td>(φ * χ) ∧ (φ * ¬(ψ ∧ χ)) ⇒ (φ * ¬ψ)</td><td>PC</td></tr><tr><td>7</td><td>(φ * χ) ∧ (φ * ¬(ψ ∧ χ)) ⇒ (φ * ¬(ψ ∧ χ))</td><td>PC</td></tr><tr><td>8</td><td>(φ * χ) ∧ (φ * ⊗ ψ) ⇒ (φ * ⊗ ψ ∧ χ)</td><td>Def. ⊗, 7 □</td></tr></table>
Proof of ($\mathbf{I}_{6.3.10}^*$) and ($\mathbf{I}_{6.3.11}^*$). Below, we provide the derivation for the admissible axiom schema ($\mathbf{I}_{6.3.10}^*$) (the derivation for $\mathbf{I}_{6.3.11}^*$) is very similar and is thus omitted).

<table><tr><td>1</td><td>φ ⇒ (φ ∧ x = y) ∨ (φ ∧ x ≠ y)</td><td>PC</td></tr><tr><td>2</td><td>(φ ⊗ ψ) ⇒ ((φ ∧ x = y) ∨ (φ ∧ x ≠ y) ⊗ ψ)</td><td>(I<sub>6.3.4</sub><sup>*</sup>), 1</td></tr><tr><td>3</td><td>(φ ⊗ ψ) ⇒ (φ ∧ x = y ⊗ ψ) ∨ (φ ∧ x ≠ y ⊗ ψ)</td><td>(I<sub>6.3.7</sub><sup>*</sup>), ⇒-Tr, 2</td></tr><tr><td>4</td><td>x = y * x ≠ y ⇒ x = y</td><td>(A<sub>14</sub><sup>*</sup>), *-Ilr</td></tr><tr><td>5</td><td>x ≠ y * x = y ⇒ x ≠ y</td><td>(A<sub>14</sub><sup>*</sup>), *-Ilr</td></tr><tr><td>6</td><td>x = y * x ≠ y ⇒ x = y ∧ x ≠ y</td><td>(A<sub>7</sub><sup>*</sup>), ⇒-Tr, PC, 4, 5</td></tr><tr><td>7</td><td>x = y * x ≠ y ⇒ ¬T</td><td>PC, 6</td></tr><tr><td>8</td><td>¬T ⇒ ¬ψ</td><td>PC</td></tr><tr><td>9</td><td>x = y * x ≠ y ⇒ ¬ψ</td><td>PC, 7, 8</td></tr><tr><td>10</td><td>x = y ⇒ (x ≠ y -*ψ)</td><td>*-Adj, 9</td></tr><tr><td>11</td><td>¬(x ≠ y -*ψ) ⇒ x ≠ y</td><td>PC, 10</td></tr><tr><td>12</td><td>(x ≠ y ⊗ ψ) ⇒ x ≠ y</td><td>Def. ⊗, 11</td></tr><tr><td>13</td><td>φ ∧ x ≠ y ⇒ x ≠ y</td><td>PC</td></tr><tr><td>14</td><td>(φ ∧ x ≠ y ⊗ ψ) ⇒ (x ≠ y ⊗ ψ)</td><td>(I<sub>6.3.4</sub><sup>*</sup>), 13</td></tr><tr><td>15</td><td>(φ ∧ x ≠ y ⊗ ψ) ⇒ x ≠ y</td><td>⇒-Tr, 12, 14</td></tr><tr><td>16</td><td>x = y ∧ (φ ⊗ ψ) ⇒ (φ ∧ x = y ⊗ ψ) ∨ x ≠ y</td><td>PC, 3, 15</td></tr><tr><td>17</td><td>x = y ∧ (φ ⊗ ψ) ⇒ (φ ∧ x = y ⊗ ψ)</td><td>PC, 16</td></tr></table>

Proof of ($\mathbf{I}_{6.3.12}^*$). Notice that, since $\varphi_{\text{size}}$ is satisfiable, for every $\beta_1, \beta_2 \in \mathbb{N}$ such that $\text{size} \ge \beta_1 \wedge \neg \text{size} \ge \beta_2 \subseteq_{\text{Lt}} \varphi_{\text{size}}$, we must have $\beta_1 < \beta_2$. Moreover, thanks to ($\mathbf{I}_5^C$) and ($\mathbf{I}_{6.3.4}^*$), without loss of generality, we can restrict ourselves to $\varphi_{\text{size}}$ of the form:

(1) $\varphi_{\text{size}} = \text{size} \ge \beta$ for some $\beta \ge 0$,

(2) $\varphi_{\text{size}} = \neg(\text{size} \ge \beta)$ for some $\beta > 0$,

(3) $\varphi_{\text{size}} = \text{size} \ge \beta_1 \wedge \neg(\text{size} \ge \beta_2)$ for some $\beta_2 > \beta_1$.

Indeed, given an arbitrary $\varphi_{\text{size}}$, every positive literal $\text{size} \ge \beta$ such that $\beta < \max_{\text{size}}(\varphi_{\text{size}})$ can be derived starting from $\text{size} \ge \max_{\text{size}}(\varphi_{\text{size}})$, by repeated applications of ($\mathbf{I}_5^C$). Similarly, let $\bar{\beta}$ be the smallest natural number such that $\neg \text{size} \ge \bar{\beta} \subseteq_{\text{Lt}} \varphi_{\text{size}}$, if any. Every literal $\neg \text{size} \ge \beta' \subseteq_{\text{Lt}} \varphi_{\text{size}}$ with $\beta' \ge \bar{\beta}$ can be derived from $\neg \text{size} \ge \bar{\beta}$, by repeated applications of the axiom ($\mathbf{I}_5^C$) (taken in contrapositive form i.e. $\neg \text{size} \ge \beta \Rightarrow \neg \text{size} \ge \beta+1$, which is derivable in $\mathcal{H}_C$ by propositional reasoning).

We write $U(X)$ to denote the conjunction $\bigwedge_{x \in X} \neg \text{alloc}(x)$ ('U' stands for 'unallocated'). Below, given $\beta \in \mathbb{N}$, we aim at deriving the formula ($\text{size} = \beta \wedge U(X) \neg \top$ since this implies that ($\mathbf{I}_{6.3.12}^*$) is derivable in its instances (1)-(3), as shown below.

case (1): Let $\varphi_{\text{size}} = \text{size} \ge \beta$.

$$1 \mid \text{size} = \beta \wedge U(X) \neg \top$$

Hypothesis
2 | size = β ∧ U(X) ⇒ size ≥ β ∧ U(X) PC, def. of size = β

3 | (size = β ∧ U(X) ⊗ ⊤) ⇒ (size ≥ β ∧ U(X) ⊗ ⊤) (I<sub>6.3.4</sub><sup>*</sup>), 2

4 | size ≥ β ∧ U(X) ⊗ ⊤ Modus Ponens, 1, 3

case (2): Let $\varphi_{\text{size}} = \neg \text{size} \geq \beta$. Since $\varphi_{\text{size}}$ is satisfiable, we have $\beta \geq 1$.

1 | size = β−1 ∧ U(X) ⊗ ⊤ Hypothesis

2 | size = β−1 ∧ U(X) ⇒ ¬size ≥ β ∧ U(X) PC, def. of size = β−1

3 | (size = β−1 ∧ U(X) ⊗ ⊤) ⇒ (¬size ≥ β ∧ U(X) ⊗ ⊤) (I<sub>6.3.4</sub><sup>*</sup>), 2

4 | ¬size ≥ β ∧ U(X) ⊗ ⊤ Modus Ponens, 1, 3

case (3): Let $\varphi_{\text{size}} = \text{size} \geq \beta_1 \wedge \neg \text{size} \geq \beta_2$. Since $\varphi_{\text{size}}$ is satisfiable, $\beta_2 > \beta_1$.

1 | size = β₂−1 ∧ U(X) ⊗ ⊤ Hypothesis

2 | size = β₂−1 ⇒ size ≥ β₁ repeated (I<sub>5</sub><sup>C</sup>), as β₂ > β₁

3 | size = β₂−1 ⇒ ¬size ≥ β₂ PC, def. of size = β−1

4 | size = β₂−1 ∧ U(X) ⇒ size ≥ β₁ ∧ ¬size ≥ β₂ ∧ U(X) PC, 2, 3

5 | (size = β₂−1 ∧ U(X) ⊗ ⊤) ⇒ (size ≥ β₁ ∧ ¬size ≥ β₂ ∧ U(X) ⊗ ⊤) (I<sub>6.3.4</sub><sup>*</sup>), 4

6 | size ≥ β₁ ∧ ¬size ≥ β₂ ∧ U(X) ⊗ ⊤ Modus Ponens, 1, 5

To conclude the proof, let us show that (size = β ∧ U(X)) ⊗ ⊤ is derivable in $\mathcal{H}_C(*, *)$.
The proof is by induction on $\beta$, with two base cases, for $\beta = 0$ and $\beta = 1$.

base case: $\beta = 0$: In this case, $size = 0$ is equal to $size \ge 0 \wedge \neg size \ge 1$. We have,

1 | (emp-* ⊥) ⇒ emp * (emp-* ⊥) (A<sub>11</sub><sup>*</sup>)

2 | emp * (emp-* ⊥) ⇒ ⊥ (I<sub>6.3.3</sub><sup>*</sup>)

3 | (emp-* ⊥) ⇒ ⊥ ⇒ -Tr, 1, 2

4 | emp ⊗ ⊤ PC, 3, def. of ⊗

5 | alloc(x) ⇒ size ≥ 1 (I<sub>6</sub><sup>C</sup>)

6 | emp ⇒ ¬alloc(x) PC, 5, as size ≥ 1 = ¬emp

7 | emp ⇒ U(X) PC, 6 used for all x ∈ X

8 | emp ⇒ size ≥ 0 ∧ ¬(size ≥ 1) PC, def. of size ≥ β

9 | emp ⇒ size ≥ 0 ∧ ¬(size ≥ 1) ∧ U(X) PC, 7, 8

10 | (emp ⊗ ⊤) ⇒ (size ≥ 0 ∧ ¬(size ≥ 1) ∧ U(X) ⊗ ⊤) (I<sub>6.3.4</sub><sup>*</sup>), 9

11 | size ≥ 0 ∧ ¬(size ≥ 1) ∧ U(X) ⊗ ⊤ Modus Ponens, 4, 10

base case: $\beta = 1$: This case corresponds exactly to the axiom ($A_{21}^*$).
**induction step: $\beta \ge 2$: First of all, we notice that the following formula is valid:**

$$ (\mathbf{size} = 1 \wedge \mathbf{U}(\mathbf{X})) * (\mathbf{size} = \beta - 1 \wedge \mathbf{U}(\mathbf{X})) \Rightarrow \mathbf{size} = \beta \wedge \mathbf{U}(\mathbf{X}). \quad (\dagger) $$

Indeed, let $(s, h)$ be a memory state satisfying the antecedent of the implication above. So, there are disjoint heaps $h_1$ and $h_2$ such that $h = h_1+h_2$, $\text{card}(\text{dom}(h_1)) = 1$, $\text{card}(\text{dom}(h_2)) = \beta - 1$, and for every $\mathbf{x} \in \mathbf{X}$, $s(\mathbf{x}) \notin \text{dom}(h_1)$ and $s(\mathbf{x}) \notin \text{dom}(h_2)$. By $h = h_1+h_2$, $\text{card}(\text{dom}(h)) = \text{card}(\text{dom}(h_1)) + \text{card}(\text{dom}(h_2)) = \beta$, and for every $\mathbf{x} \in \mathbf{X}$, $s(\mathbf{x}) \notin \text{dom}(h)$. Thus, $(s, h) \models \mathbf{size} = \beta \wedge \mathbf{U}(\mathbf{X})$.

As $(\dagger)$ can be seen as a formula in $\text{SL}(*, \text{alloc})$, by Theorem 5.6 it is derivable in $\mathcal{H}_C(*)$ and thus in $\mathcal{H}_C(*, -*)$. Now, let us derive $(\mathbf{size} = \beta \wedge \mathbf{U}(\mathbf{X})) \dashv\vdash \top$. Let us consider as induction hypothesis the derivability of $(\mathbf{size} = \beta - 1 \wedge \mathbf{U}(\mathbf{X})) \dashv\vdash \top$. Therefore,

<table><tr><td>1</td><td>size = &beta; &minus; 1 &and; U(X) &ominus; T</td><td>Induction Hypothesis</td></tr><tr><td>2</td><td>(size = 1 &and; U(X)) * (size = &beta; &minus; 1 &and; U(X)) &rarr; size = &beta; &and; U(X)</td><td>(&dagger;), see above</td></tr><tr><td>3</td><td>size = 1 &and; U(X) &ominus; T</td><td>(A<sub>21</sub><sup>*</sup>)</td></tr><tr><td>4</td><td>T &rarr; (size = &beta; &minus; 1 &and; U(X) &ominus; T)</td><td>PC, 1</td></tr><tr><td>5</td><td>(size = 1 &and; U(X) &ominus; T) &rarr;</td><td></td></tr><tr><td></td><td>(size = 1 &and; U(X) &ominus; (size = &beta; &minus; 1 &and; U(X) &ominus; T)))</td><td>(I<sub>6.3.5</sub><sup>*</sup>), 4</td></tr><tr><td>6</td><td>(size = 1 &and; U(X) &ominus; (size = &beta; &minus; 1 &and; U(X) &ominus; T)) &rarr;</td><td></td></tr><tr><td></td><td>((size = 1 &and; U(X)) * (size = &beta; &minus; 1 &and; U(X)) &ominus; T))</td><td>(I<sub>6.3.6</sub><sup>*</sup>)</td></tr><tr><td>7</td><td>((size = 1 &and; U(X)) * (size = &beta; &minus; 1 &and; U(X)) &ominus; T) &rarr;</td><td></td></tr><tr><td></td><td>(size = &beta; &and; U(X) &ominus; T)</td><td>(I<sub>6.3.4</sub><sup>*</sup>), 2</td></tr><tr><td>8</td><td>(size = 1 &and; U(X) &ominus; T) &rarr; (size = &beta; &and; U(X) &ominus; T)</td><td>&rarr;-Tr, 5, 6, 7</td></tr><tr><td>9</td><td>size = &beta; &and; U(X) &ominus; T</td><td>Modus Ponens, 3, 8 &square;</td></tr></table>