$4$ | $(\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Alloc}}(\psi))\ast(\textit{\small{Garb}}(\varphi)\ast\textit{\small{Garb}}(\psi))\Rightarrow$ |
| $(\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi))\ast(\textit{\small{Alloc}}(\psi)\ast\textit{\small{Garb}}(\psi))$ | ($\mathbf{A^{\ast}_{7}}$), ($\mathbf{A^{\ast}_{9}}$)
$5$ | $\textit{\small{Alloc}}\ast\textit{\small{Garb}}\Rightarrow(\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi))\ast(\textit{\small{Alloc}}(\psi)\ast\textit{\small{Garb}}(\psi))$ | 3, 3, 4

To conclude this step of the proof, it is sufficient to show
${\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\varphi^{(1)}}$
and
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\psi)\ast\textit{\small{Garb}}(\psi)\Rightarrow\psi^{(1)}$.
Indeed, by relying on the rule 3, we then obtain
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}\ast\textit{\small{Garb}}\Rightarrow\varphi^{(1)}\ast\psi^{(1)}$.
Below, we show
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\varphi^{(1)}$.
The developments of
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\psi)\ast\textit{\small{Garb}}(\psi)\Rightarrow\psi^{(1)}$
are analogous. We recall that the formula $\textit{\small{Alloc}}(\varphi)$ is
defined as

$\textit{\small{Alloc}}(\varphi)\,=\,\Asterisk\\{\mathtt{alloc}(\mathtt{x}_{i})\wedge\mathtt{size}=1\mid\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\\}.$

First of all, let us show that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\varphi)\ast\top\Rightarrow\bigwedge\\{\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\mid
i\in[1,n]\\}$. The proof is divided in three cases:

case:
$\\{\mathtt{alloc}(\mathtt{x}_{i})\wedge\mathtt{size}=1\mid\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\\}=\emptyset$:

In this case, the formula we want to derive is syntactically equal to
$\top\ast\top\Rightarrow\top$, which is derivable by propositional reasoning.

case: ${\rm
card}(\\{\mathtt{alloc}(\mathtt{x}_{i})\wedge\mathtt{size}=1\mid\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\\})=1$:

In this case, the formula we want to derive is syntactically equal to
$(\mathtt{alloc}(\mathtt{x})\land\mathtt{size}=1)\ast\top\Rightarrow\mathtt{alloc}(\mathtt{x})$.
Therefore, it is derivable in $\mathcal{H}_{\mathsf{C}}(\ast)$ by
($\mathbf{I^{\ast}_{17}}$) and $\ast$-Intro:.

case: ${\rm
card}(\\{\mathtt{alloc}(\mathtt{x}_{i})\wedge\mathtt{size}=1\mid\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\\}){\geq}2$:

In the derivation below, we write $\textit{\small{Alloc}}(\varphi)^{-i}$ for
$\Asterisk\\{\mathtt{alloc}(\mathtt{x}_{j})\land\mathtt{size}=1\mid
j\in[1,n]\setminus\\{i\\},\mathtt{alloc}(\mathtt{x}_{j})\subseteq_{\mathsf{Lt}}\varphi\\}$.
Roughly speaking, $\textit{\small{Alloc}}(\varphi)^{-i}$ is obtained from
$\textit{\small{Alloc}}(\varphi)$ by removing the subformula
$\mathtt{alloc}(\mathtt{x}_{i})\land\mathtt{size}=1$. Since ${\rm
card}(\\{\mathtt{alloc}(\mathtt{x}_{i})\wedge\mathtt{size}=1\mid\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\\}){\geq}2$,
the formula $\textit{\small{Alloc}}(\varphi)^{-i}$ is different from $\top$.
We have

$1$ | $\textit{\small{Alloc}}(\varphi)\ast\top\Rightarrow$ |
---|---|---
| $\quad(\mathtt{alloc}(\mathtt{x}_{i})\land\mathtt{size}=1)\ast(\textit{\small{Alloc}}(\varphi)^{-i}\ast\top)$ | ($\mathbf{A^{\ast}_{7}}$), ($\mathbf{A^{\ast}_{9}}$), def. of $\textit{\small{Alloc}}(\varphi)$
|  | where $\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi$ and $i\in[1,n]$
$2$ | $\textit{\small{Alloc}}(\varphi)^{-i}\ast\top\Rightarrow\top$ | PC
$3$ | $\mathtt{alloc}(\mathtt{x}_{i})\land\mathtt{size}=1\Rightarrow\mathtt{alloc}(\mathtt{x}_{i})$ | PC
$4$ | $(\mathtt{alloc}(\mathtt{x}_{i})\land\mathtt{size}=1)\ast(\textit{\small{Alloc}}(\varphi)^{-i}\ast\top)\Rightarrow$ |
| $\quad\mathtt{alloc}(\mathtt{x}_{i})\ast\top$ | 3, 2, 3
$5$ | $\mathtt{alloc}(\mathtt{x}_{i})\ast\top\Rightarrow\mathtt{alloc}(\mathtt{x}_{i})$ | ($\mathbf{I^{\ast}_{17}}$)
$6$ | $\textit{\small{Alloc}}(\varphi)\ast\top\Rightarrow\mathtt{alloc}(\mathtt{x}_{i})$ | 3, 1, 4, 5
$7$ | $\textit{\small{Alloc}}(\varphi)\ast\top\Rightarrow\bigwedge\\{\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\mid i\in[1,n]\\}$ | PC, repeating 6
|  | for all $i\in[1,n]$ such that $\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi$

So, we have
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\varphi)\ast\top\Rightarrow\bigwedge\\{\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\mid
i\in[1,n]\\}$.

Now, recall that ${\rm
card}(\\{i\in[1,n]\mid\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\\})=n_{\varphi}$.
At the beginning of the proof, we have shown a derivation of
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}\Rightarrow\mathtt{size}=n$,
where Alloc is defined as
$\Asterisk\\{\mathtt{alloc}(\mathtt{x}_{i})\wedge\mathtt{size}=1\mid
i\in[1,n]\\}$. Replacing Alloc by $\textit{\small{Alloc}}(\varphi)$ and $n$ by
$n_{\varphi}$ in the derivation of
$\textit{\small{Alloc}}\Rightarrow\mathtt{size}=n$ leads to a derivation in
$\mathcal{H}_{\mathsf{C}}(\ast)$ of
$\textit{\small{Alloc}}(\varphi)\Rightarrow\mathtt{size}=n_{\varphi}$.

To show
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\varphi^{(1)}$,
we split the proof in two cases:

case: $\max_{\mathtt{size}}(\varphi)=\alpha$:

By definition of $\varphi^{(1)}$ and $\textit{\small{Garb}}(\varphi)$, we
have:

  * •:

$\varphi^{(1)}\,=\,\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\land\bigwedge\\{\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\mid
i\in[1,n]\\}$,

  * •:

$\textit{\small{Garb}}(\varphi)\,=\,\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)-n_{\varphi}$,

Then,

$1$ | $\textit{\small{Alloc}}(\varphi)\ast\top\Rightarrow\bigwedge\\{\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\mid i\in[1,n]\\}$ | Previously derived
---|---|---
$2$ | $\textit{\small{Garb}}(\varphi)\Rightarrow\top$ | PC
$3$ | $\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\textit{\small{Alloc}}(\varphi)\ast\top$ | $\ast$-Intro:, ($\mathbf{A^{\ast}_{7}}$), 2
$4$ | $\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\bigwedge\\{\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\mid i\in[1,n]\\}$ | 3, 1, 3
$5$ | $\textit{\small{Alloc}}(\varphi)\Rightarrow\mathtt{size}=n_{\varphi}$ | See above
$6$ | $\mathtt{size}=n_{\varphi}\Rightarrow\mathtt{size}\geq n_{\varphi}$ | PC, def. of $\mathtt{size}=n_{\varphi}$
$7$ | $\textit{\small{Alloc}}(\varphi)\Rightarrow\mathtt{size}\geq n_{\varphi}$ |
$8$ | $\textit{\small{Garb}}(\varphi)\Rightarrow\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)-n_{\varphi}$ | PC, def. of $\textit{\small{Garb}}(\varphi)$
$9$ | $\textit{\small{Alloc}}(\varphi){\ast}\textit{\small{Garb}}(\varphi)\Rightarrow\mathtt{size}\geq n_{\varphi}\ast\mathtt{size}\geq\max_{\mathtt{size}}(\varphi){-}n_{\varphi}$ | 3, 7, 8
$10$ | $\mathtt{size}\geq n_{\varphi}\ast\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)-n_{\varphi}\Rightarrow\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)$ | ($\mathbf{A^{\ast}_{9}}$), ($\mathbf{A^{\ast}_{7}}$), def. of $\mathtt{size}\geq\beta$
$11$ | $\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)$ | 3, 9, 10
$12$ | $\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\varphi^{(1)}$ | PC, 4, 11, def. of $\varphi^{(1)}$
case: $\max_{\mathtt{size}}(\varphi)\neq\alpha$:

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

  * •:

$\varphi^{(1)}\,=\,\mathtt{size}=\max_{\mathtt{size}}(\varphi)\land\bigwedge\\{\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\mid
i\in[1,n]\\}$,

  * •:

$\textit{\small{Garb}}(\varphi)\,=\,\mathtt{size}=\max_{\mathtt{size}}(\varphi)-n_{\varphi}$,

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

$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\land\bigwedge\\{\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi\mid
i\in[1,n]\\}.$

By propositional reasoning, we can derive
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\varphi^{(1)}$
as soon as we show that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1$,
as we do now:

$1$ | $\textit{\small{Alloc}}(\varphi)\Rightarrow\mathtt{size}=n_{\varphi}$ | Already discussed above
---|---|---
$2$ | $\mathtt{size}=n_{\varphi}\Rightarrow\lnot\mathtt{size}\geq n_{\varphi}+1$ | PC, def. of $\mathtt{size}=n_{\varphi}$
$3$ | $\textit{\small{Alloc}}(\varphi)\Rightarrow\lnot\mathtt{size}\geq n_{\varphi}+1$ | PC, 3, 1, 2
$4$ | $\textit{\small{Garb}}(\varphi)\Rightarrow\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)-n_{\varphi}+1$ | PC, def. of $\mathtt{size}=\beta$
$5$ | $\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow$ |
| $\qquad\lnot\mathtt{size}\geq n_{\varphi}+1\ast\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)-n_{\varphi}+1$ | 3, 3, 4
$6$ | $\lnot\mathtt{size}\geq n_{\varphi}+1\ast\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)-n_{\varphi}+1\Rightarrow$ |
| $\qquad\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1$ | ($\mathbf{A^{\ast}_{31}}$)
$7$ | $\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1$ | 3, 5, 6

This concludes the proof of
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi)\Rightarrow\varphi^{(1)}$.
As already stated, one can analogously show that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}(\psi)\ast\textit{\small{Garb}}(\psi)\Rightarrow\psi^{(1)}$.
Afterwards, by 3 and from
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}\ast\textit{\small{Garb}}\Rightarrow(\textit{\small{Alloc}}(\varphi)\ast\textit{\small{Garb}}(\varphi))\ast(\textit{\small{Alloc}}(\psi)\ast\textit{\small{Garb}}(\psi))$,
we conclude that

$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\textit{\small{Alloc}}\ast\textit{\small{Garb}}\Rightarrow\varphi^{(1)}\ast\psi^{(1)}.$

#### Step 3, add the missing literals

From the first and second step of the proof, and by propositional reasoning,
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(1)}\ast\psi^{(1)}$.
We now rely on ${\langle\mbox{$\ast$}\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)}\\!\ast\psi^{(1)}$, $\varphi^{(2)}\\!\ast\psi^{(2)}$,
$\dots$, $\varphi^{(k)}\\!\ast\psi^{(k)}$, where for all $i\in[1,k]$,
$\varphi^{(i)}$ and $\psi^{(i)}$ are conjunctions of core formulae such that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$,
and for all $j\in[1,i]$, $\varphi^{(j)}\subseteq_{\mathsf{Lt}}\varphi^{(i)}$
and $\psi^{(j)}\subseteq_{\mathsf{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}_{\mathsf{C}}(\ast)}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi\ast\psi$,
ending the proof. Below, we focus on the formula $\varphi^{(i)}$ and
$\varphi$. Since ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$ is equal to
${\langle\mbox{$\ast$}\rangle}(\psi,\varphi)$ (by a quick inspection of the
definition) and the separating conjunction is commutative (axiom
($\mathbf{A^{\ast}_{7}}$)), a similar analysis can be done for $\psi^{(i)}$
and $\psi$. Thus, we assume that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$
holds, where in particular $\varphi^{(1)}\subseteq_{\mathsf{Lt}}\varphi^{(i)}$
and $\psi^{(1)}\subseteq_{\mathsf{Lt}}\psi^{(i)}$, and that there is a literal
$L\subseteq_{\mathsf{Lt}}\varphi$ that does not appear in $\varphi^{(i)}$. By
relying on the theorems in Lemma 7, we show that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow(\varphi^{(i)}\land
L)\ast\psi^{(i)}$ by a case analysis on $L$.

case: $L\,=\,\mathtt{x}\sim\mathtt{y}$, where $\sim\in\\{=,\neq\\}$:

By definition of ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$,
$\mathtt{x}\sim\mathtt{y}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$.

$1$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$ | Hypothesis
---|---|---
$2$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\mathtt{x}\sim\mathtt{y}$ | PC, def. of ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$, see above
$3$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\mathtt{x}\sim\mathtt{y}\land(\varphi^{(i)}\ast\psi^{(i)})$ | PC, 1, 2
$4$ | $\mathtt{x}\sim\mathtt{y}\land(\varphi^{(i)}\ast\psi^{(i)})\Rightarrow(\varphi^{(i)}\land\mathtt{x}\sim\mathtt{y})\ast\psi^{(i)}$ | ($\mathbf{I^{\ast}_{\ref{lemma:separate-auxiliary-stuff}.1}}$)
$5$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow(\varphi^{(i)}\land\mathtt{x}\sim\mathtt{y})\ast\psi^{(i)}$ | 3, 3, 4
case: $L\,=\,\mathtt{alloc}(\mathtt{x})$:

Since $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$, by
definition,
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$.
By definition of $\mathtt{x}_{1},\dots,\mathtt{x}_{n}$, there is $j\in[1,n]$
such that
$\mathtt{x}_{j}=\mathtt{x}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$.
Since $\varphi$ is a core type,
$\mathtt{alloc}(\mathtt{x}_{j})\subseteq_{\mathsf{Lt}}\varphi$. By definition
of $\varphi^{(1)}$,
$\mathtt{alloc}(\mathtt{x}_{j})\subseteq_{\mathsf{Lt}}\varphi^{(1)}$. From
$\varphi^{(1)}\subseteq_{\mathsf{Lt}}\varphi^{(i)}$, we have
$\mathtt{alloc}(\mathtt{x}_{j})\subseteq_{\mathsf{Lt}}\varphi^{(i)}$.
Afterwards,

$1$ | $\varphi^{(i)}\Rightarrow\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x}_{j})$ | PC, see above
---|---|---
$2$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$ | Hypothesis
$3$ | $\varphi^{(i)}\ast\psi^{(i)}\Rightarrow(\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x}_{j}))\ast\psi^{(i)}$ | $\ast$-Intro:, 1
$4$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\mathtt{x}_{j}=\mathtt{x}$ | PC, see above
$5$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\mathtt{x}_{j}=\mathtt{x}\land((\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x}_{j}))\ast\psi^{(i)})$ | PC, 2, 3, 4
$6$ | $\mathtt{x}_{j}=\mathtt{x}\land((\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x}_{j}))\ast\psi^{(i)})\Rightarrow(\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x}))\ast\psi^{(i)}$ | ($\mathbf{I^{\ast}_{\ref{lemma:separate-auxiliary-stuff}.3}}$)
$7$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow((\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x}))\ast\psi^{(i)})$ | 3, 5, 6

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

case: $L\,=\,\lnot\mathtt{alloc}(\mathtt{x})$:

We distinguish two main subcases.

  * •:

First, assume $\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$. By
definition of ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$,
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$.

$1$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$ | Hypothesis
---|---|---
$2$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\lnot\mathtt{alloc}(\mathtt{x})$ | PC, def. of ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$, see above
$3$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\lnot\mathtt{alloc}(\mathtt{x})\land(\varphi^{(i)}\ast\psi^{(i)})$ | PC, 1, 2
$4$ | $\lnot\mathtt{alloc}(\mathtt{x})\land(\varphi^{(i)}\ast\psi^{(i)})\Rightarrow(\varphi^{(i)}\land\lnot\mathtt{alloc}(\mathtt{x}))\ast\psi^{(i)}$ | ($\mathbf{I^{\ast}_{\ref{lemma:separate-auxiliary-stuff}.7}}$)
$5$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow(\varphi^{(i)}\land\lnot\mathtt{alloc}(\mathtt{x}))\ast\psi^{(i)}$ | 3, 3, 4
  * •:

Otherwise, $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$. By
assumption, $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi^{(i)}$.

$1$ | $\psi^{(i)}\Rightarrow\psi^{(i)}\land\mathtt{alloc}(\mathtt{x})$ | PC, see above
---|---|---
$2$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$ | Hypothesis
$3$ | $\varphi^{(i)}\ast\psi^{(i)}\Rightarrow(\psi^{(i)}\land\mathtt{alloc}(\mathtt{x}))\ast\varphi^{(i)}$ | ($\mathbf{A^{\ast}_{7}}$), $\ast$-Intro:, 1
$4$ | $(\psi^{(i)}\land\mathtt{alloc}(\mathtt{x}))\ast\varphi^{(i)}\Rightarrow\psi^{(i)}\ast(\varphi^{(i)}\land\lnot\mathtt{alloc}(\mathtt{x}))$ | ($\mathbf{I^{\ast}_{\ref{lemma:separate-auxiliary-stuff}.5}}$)
$5$ | $\psi^{(i)}\ast(\varphi^{(i)}\land\lnot\mathtt{alloc}(\mathtt{x}))\Rightarrow(\varphi^{(i)}\land\lnot\mathtt{alloc}(\mathtt{x}))\ast\psi^{(i)}$ | ($\mathbf{A^{\ast}_{7}}$)
$6$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow(\varphi^{(i)}\land\lnot\mathtt{alloc}(\mathtt{x}))\ast\psi^{(i)}$ | 3, 2, 3, 4, 5

case: $L\,=\,\mathtt{x}\hookrightarrow\mathtt{y}$:

Similar to the case $L=\mathtt{alloc}(\mathtt{x})$. Since $\varphi$ is a
satisfiable core type, we have
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ (see axiom
($\mathbf{A^{\mathsf{C}}_{5}}$)). By assumption,
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{(i)}$. By
definition of ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$, we have
${\mathtt{x}\hookrightarrow\mathtt{y}}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$.

$1$ | $\varphi^{(i)}\Rightarrow\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x})$ | PC, see above
---|---|---
$2$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$ | Hypothesis
$3$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\mathtt{x}\hookrightarrow\mathtt{y}$ | PC, see above
$4$ | $\varphi^{(i)}\ast\psi^{(i)}\Rightarrow(\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x}))\ast\psi^{(i)}$ | $\ast$-Intro:, 1
$5$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\mathtt{x}\hookrightarrow\mathtt{y}\land((\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x}))\ast\psi^{(i)})$ | PC, 3, 4
$6$ | $\mathtt{x}\hookrightarrow\mathtt{y}\land((\varphi^{(i)}\land\mathtt{alloc}(\mathtt{x}))\ast\psi^{(i)})\Rightarrow(\varphi^{(i)}\land\mathtt{x}\hookrightarrow\mathtt{y})\ast\psi^{(i)}$ | ($\mathbf{I^{\ast}_{\ref{lemma:separate-auxiliary-stuff}.11}}$)
$7$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow(\varphi^{(i)}\land\mathtt{x}\hookrightarrow\mathtt{y})\ast\psi^{(i)}$ | $\ast$-Intro:, 5, 6

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

case: $L\,=\,\lnot\mathtt{x}\hookrightarrow\mathtt{y}$:

We distinguish two main subcases

  * •:

First, suppose $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$. In
this case, by definition of ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$, we
have
${\lnot\mathtt{x}\hookrightarrow\mathtt{y}}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$.
Therefore,

$1$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\lnot\mathtt{x}\hookrightarrow\mathtt{y}$ | PC, see above
---|---|---
$2$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$ | Hypothesis
$3$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\lnot\mathtt{x}\hookrightarrow\mathtt{y}\land(\varphi^{(i)}\ast\psi^{(i)})$ | PC, 1, 2
$4$ | $\lnot\mathtt{x}\hookrightarrow\mathtt{y}\land(\varphi^{(i)}\ast\psi^{(i)})\Rightarrow(\varphi^{(i)}\land\lnot\mathtt{x}\hookrightarrow\mathtt{y})\ast\psi^{(i)}$ | ($\mathbf{I^{\ast}_{\ref{lemma:separate-auxiliary-stuff}.13}}$)
  * •:

Otherwise, we have
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$. By
assumption,
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{(i)}$, and
thus

$1$ | $\varphi^{(i)}\Rightarrow\lnot\mathtt{alloc}(\mathtt{x})$ | PC, see above
---|---|---
$2$ | $\lnot\mathtt{alloc}(\mathtt{x})\Rightarrow\lnot\mathtt{x}\hookrightarrow\mathtt{y}$ | ($\mathbf{A^{\mathsf{C}}_{5}}$), PC
$3$ | $\varphi^{(i)}\Rightarrow\lnot\mathtt{x}\hookrightarrow\mathtt{y}$ | 3, 1, 2
$4$ | $\varphi^{(i)}\Rightarrow\varphi^{(i)}\land\lnot\mathtt{x}\hookrightarrow\mathtt{y}$ | PC, 3
$5$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$ | Hypothesis
$6$ | $\varphi^{(i)}\ast\psi^{(i)}\Rightarrow(\varphi^{(i)}\land\lnot\mathtt{x}\hookrightarrow\mathtt{y})\ast\psi^{(i)}$ | $\ast$-Intro:, 4
$7$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow(\varphi^{(i)}\land\lnot\mathtt{x}\hookrightarrow\mathtt{y})\ast\psi^{(i)}$ | 3, 5, 6

case: $L=\mathtt{size}\geq\beta$:

By definition of $\max_{\mathtt{size}}(.)$,
$\beta\leq\max_{\mathtt{size}}(\varphi)$. By definition of $\varphi^{(1)}$,
$\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\subseteq_{\mathsf{Lt}}\varphi^{(1)}$.
From $\varphi^{(1)}\subseteq_{\mathsf{Lt}}\varphi^{(i)}$, we get
$\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\subseteq_{\mathsf{Lt}}\varphi^{(i)}$.

$1$ | $\varphi^{(i)}\Rightarrow\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)$ | PC, see above
---|---|---
$2$ | $\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\Rightarrow\mathtt{size}\geq\beta$ | repeated ($\mathbf{I^{\mathsf{C}}_{9}}$), PC, as $\beta\leq\max_{\mathtt{size}}(\varphi)$
$3$ | $\varphi^{(i)}\Rightarrow\varphi^{(i)}\land\mathtt{size}\geq\beta$ | PC, 1, 2
$4$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$ | Hypothesis
$5$ | $\varphi^{(i)}\ast\psi^{(i)}\Rightarrow(\varphi^{(i)}\land\mathtt{size}\geq\beta)\ast\psi^{(i)}$ | $\ast$-Intro:, 3
$6$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow(\varphi^{(i)}\land\mathtt{size}\geq\beta)\ast\psi^{(i)}$ | 3, 4, 5
case: $L=\lnot\mathtt{size}\geq\beta$:

In this case, $\max_{\mathtt{size}}(\varphi)<\alpha$. Since $\varphi$ is a
satisfiable core type, we have $\beta>\max_{\mathtt{size}}(\varphi)$.
Moreover, by definition of $\varphi^{(1)}$,
$\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1\subseteq_{\mathsf{Lt}}\varphi^{(1)}$.
From $\varphi^{(1)}\subseteq_{\mathsf{Lt}}\varphi^{(i)}$, we have
$\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1\subseteq_{\mathsf{Lt}}\varphi^{(i)}$.

$1$ | $\varphi^{(i)}\Rightarrow\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi){+}1$ | PC, see above
---|---|---
$2$ | $\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi){+}1\Rightarrow\lnot\mathtt{size}\geq\beta$ | repeated ($\mathbf{I^{\mathsf{C}}_{9}}$), PC, as $\beta>\max_{\mathtt{size}}(\varphi)$
|  | by PC, the contrapositive of ($\mathbf{I^{\mathsf{C}}_{9}}$) is derivable
$3$ | $\varphi^{(i)}\Rightarrow\varphi^{(i)}\land\lnot\mathtt{size}\geq\beta$ | PC, 1, 2
$4$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow\varphi^{(i)}\ast\psi^{(i)}$ | Hypothesis
$5$ | $\varphi^{(i)}\ast\psi^{(i)}\Rightarrow(\varphi^{(i)}\land\lnot\mathtt{size}\geq\beta)\ast\psi^{(i)}$ | $\ast$-Intro:, 3
$6$ | ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)\Rightarrow(\varphi^{(i)}\land\lnot\mathtt{size}\geq\beta)\ast\psi^{(i)}$ | 3, 4, 5

######  Corollary 10 (Star elimination).

Let $\mathtt{X}\subseteq_{\mathsf{fin}}\mathsf{VAR}$ and $\alpha\geq{\rm
card}(\mathtt{X})$. Let $\varphi$ and $\psi$ in
$\mathsf{CoreTypes}(\mathtt{X},\alpha)$. There is $\chi$ in
$\mathsf{Conj}(\mathsf{Core}(\mathtt{X},2\alpha))$ such that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\varphi\ast\psi\Leftrightarrow\chi$.

######  Proof 5.10.

If both $\varphi$ and $\psi$ are satisfiable, the results holds directly by
Lemma 9, as ${\langle\mbox{$\ast$}\rangle}(\varphi,\psi)$ is in
$\mathsf{Conj}(\mathsf{Core}(\mathtt{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}_{\mathsf{C}}}\varphi\Rightarrow\bot$ by completeness of
$\mathcal{H}_{\mathsf{C}}$ (Lemma 3) and, $\mathcal{H}_{\mathsf{C}}(\ast)$
includes $\mathcal{H}_{\mathsf{C}}$,
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\varphi\Rightarrow\bot$. By the rule
$\ast$-Intro: and by the axiom ($\mathbf{I^{\ast}_{13}}$), we get
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\varphi*\psi\Rightarrow\bot$. Thus
$\chi$ can take the value $\lnot(\mathtt{x}=\mathtt{x})$. The case where
$\psi$ is not satisfiable is analogous, thanks to ($\mathbf{A^{\ast}_{7}}$).

By the distributivity axiom ($\mathbf{I^{\ast}_{11}}$), Corollary 10 is
extended from core types to arbitrary Boolean combinations of core formulae.
$\mathcal{H}_{\mathsf{C}}(\ast)$ is therefore complete for
$\mathsf{SL(}\ast,\mathtt{alloc}\mathsf{)}$. In order to derive a valid
formula $\varphi\in\mathsf{SL(}\ast,\mathtt{alloc}\mathsf{)}$, we repeatedly
apply the elimination of $\ast$ 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}_{\mathsf{C}}$
(Theorem 5) to prove that $\psi$ is derivable.

######  Theorem 11.

A formula $\varphi$ in $\mathsf{SL(}\ast,\mathtt{alloc}\mathsf{)}$ is valid
iff $\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\varphi$.

######  Proof 5.11.

Soundness of the proof system $\mathcal{H}_{\mathsf{C}}(\ast)$ has been
already established earlier.

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

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

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

  1. R0

Let $\varphi,\varphi^{\prime}$ and $\psi$ be formulae of
$\mathsf{SL(}\ast,\mathtt{alloc}\mathsf{)}$ such that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\varphi\Leftrightarrow\varphi^{\prime}$.
Then,

$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\psi[\varphi]_{\rho}\Rightarrow\psi[\varphi^{\prime}]_{\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^{\prime}$ are therefore placed at the same
occurrence.)

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

$\text{}\frac{\displaystyle\varphi\Leftrightarrow\varphi^{\prime}}{\displaystyle\neg\varphi\Leftrightarrow\neg\varphi^{\prime}}\
\ \
\text{}\frac{\displaystyle\varphi\Leftrightarrow\varphi^{\prime}}{\displaystyle\varphi\vee\psi\Leftrightarrow\varphi^{\prime}\vee\psi}\
\ \
\text{}\frac{\displaystyle\varphi\Leftrightarrow\varphi^{\prime}}{\displaystyle\varphi\wedge\psi\Leftrightarrow\varphi^{\prime}\wedge\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 $\ast$-Intro: in $\mathcal{H}_{\mathsf{C}}(\ast)$, the
rule below is also admissible:

$\text{}\frac{\displaystyle\varphi\Leftrightarrow\varphi^{\prime}}{\displaystyle\varphi\ast\psi\Leftrightarrow\varphi^{\prime}\ast\psi}$

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

Assume that $\varphi$ is a formula in
$\mathsf{SL(}\ast,\mathtt{alloc}\mathsf{)}$ with $n+1$ occurrences of the
separating conjunction not involved in the definition of some
$\mathtt{size}\geq\beta$ ($n\geq 0$). Let $\psi$ be a subformula of $\varphi$
(at the occurrence $\rho$) of the form $\psi_{1}\ast\psi_{2}$ such that
$\psi_{1}$ and $\psi_{2}$ are Boolean combinations of core formulae, in
$\mathsf{Bool}(\mathsf{Core}(\mathtt{X},\alpha_{1}))$ and
$\mathsf{Bool}(\mathsf{Core}(\mathtt{X},\alpha_{2}))$. By pure propositional
reasoning, one can show that there are formulae in disjunctive normal form
$\psi_{1}^{1}\vee\cdots\vee\psi_{1}^{n_{1}}$ and
${\psi_{2}^{1}\vee\cdots\vee\psi_{2}^{n_{2}}}$ such that
$\vdash_{\mathcal{H}_{\mathsf{C}}}\psi_{i}\Leftrightarrow\psi_{i}^{1}\vee\cdots\vee\psi_{i}^{n_{i}}$
for $i\in\\{1,2\\}$ and moreover, all the $\psi_{i}^{j}$’s are core types in
$\mathsf{CoreTypes}(\mathtt{X},\max({\rm
card}(\mathtt{X}),\alpha_{1},\alpha_{2}))$. Again, by using propositional
reasoning but this time using also the axiom ($\mathbf{I^{\ast}_{11}}$) for
distributivity, we have

$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\psi_{1}\ast\psi_{2}\Leftrightarrow\bigvee_{j_{1}\in[1,n_{1}],j_{2}\in[1,n_{2}]}\psi_{1}^{j_{1}}\ast\psi_{2}^{j_{2}}.$

We now rely on Corollary 10 and derive that there is a conjunction of core
formulae $\psi^{j_{1},j_{2}}$ in
$\mathsf{Conj}(\mathsf{Core}(\mathtt{X},2\max({\rm
card}(\mathtt{X}),\alpha_{1},\alpha_{2})))$ such that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\psi_{1}^{j_{1}}\ast\psi_{2}^{j_{2}}\Leftrightarrow\psi^{j_{1},j_{2}}$.
By propositional reasoning, we get

$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\psi_{1}\ast\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 R0), we obtain

$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast)}\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
conjunction that are not involved in the definition of some core formula of
the form $\mathtt{size}\geq\beta$. The induction hypothesis applies, which
concludes the proof.

##  6\. A constructive elimination of $\mathbin{-\mkern-6.0mu*}$ leading to
full completeness

($\mathbf{A^{\mathbin{-\mkern-6.0mu*}}_{21}}$)
$(\mathtt{size}=1\land\bigwedge_{\mathtt{x}\in\mathtt{X}}\lnot\mathtt{alloc}(\mathtt{x}))\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top\\!\
\blacktriangleleft\\!\\!\\!\left[\mathtt{X}\subseteq_{\mathsf{fin}}\mathsf{VAR}\right]$
($\mathbf{A^{\mathbin{-\mkern-6.0mu*}}_{23}}$)
$\lnot\mathtt{alloc}(\mathtt{x})\Rightarrow((\mathtt{x}\hookrightarrow\mathtt{y}\land\mathtt{size}=1)\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$
($\mathbf{A^{\mathbin{-\mkern-6.0mu*}}_{25}}$)
$\lnot\mathtt{alloc}(\mathtt{x})\Rightarrow((\mathtt{alloc}(\mathtt{x})\land\mathtt{size}=1\land\bigwedge_{\mathtt{y}\in\mathtt{X}}\lnot\mathtt{x}\hookrightarrow\mathtt{y})\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)\
\blacktriangleleft\\!\\!\\!\left[\mathtt{X}\subseteq_{\mathsf{fin}}\mathsf{VAR}\right]$
$\ast$-Adj:
$\text{}\frac{\displaystyle\varphi\ast\psi\Rightarrow\chi}{\displaystyle\varphi\Rightarrow(\psi\mathbin{-\mkern-6.0mu*}\chi)}{}$
$\mathbin{-\mkern-6.0mu*}$-Adj:
$\text{}\frac{\displaystyle\varphi\Rightarrow(\psi\mathbin{-\mkern-6.0mu*}\chi)}{\displaystyle\varphi\ast\psi\Rightarrow\chi}{}$

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

In order to obtain the final proof system
$\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$, we add the axioms
and rules from Figure 7 to the proof system $\mathcal{H}_{\mathsf{C}}(\ast)$.
These new axioms and rules are dedicated to the separating implication. The
axioms involving
$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$
(kind of dual of $\mathbin{-\mkern-6.0mu*}$, 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 7 and 7 are from the Hilbert-
style axiomatisation of Boolean BI [GLW06, Section 2]. One can observe that,
in $\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$, the axioms
($\mathbf{I^{\ast}_{11}}$), ($\mathbf{I^{\ast}_{13}}$) and
($\mathbf{I^{\ast}_{17}}$) of $\mathcal{H}_{\mathsf{C}}(\ast)$ are derivable.

######  Lemma 12.

The axioms ($\mathbf{I^{\ast}_{11}}$), ($\mathbf{I^{\ast}_{13}}$) and
($\mathbf{I^{\ast}_{17}}$) are derivable in
$\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$.

The derivations of ($\mathbf{I^{\ast}_{11}}$), ($\mathbf{I^{\ast}_{13}}$) and
($\mathbf{I^{\ast}_{17}}$) that lead to Lemma 12 are given in Appendix C.

Fundamentally, $\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$
enjoys the $\mathbin{-\mkern-6.0mu*}$ elimination property, as shown below.
Actually, we state the property with the help of
$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$ as
we find the related statements and developments more intuitive.

######  Lemma 13.

Let $\mathtt{X}\subseteq_{\mathsf{fin}}\mathsf{VAR}$ and $\alpha\geq{\rm
card}(\mathtt{X})$. Let $\varphi$ and $\psi$ in
$\mathsf{CoreTypes}(\mathtt{X},\alpha)$. There is a conjunction
$\chi\in\mathsf{Conj}(\mathsf{Core}(\mathtt{X},\alpha))$ such that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\Leftrightarrow\chi$.

######  Proof 6.1 (Structure of the proof of Lemma 13).

In the proof of Lemma 13, the formula $\chi$ is explicitly constructed from
$\varphi$ and $\psi$, following a pattern analogous to the construction of
${\langle\mbox{$\ast$}\rangle}(.\,,.)$ in Figure 6 (see forthcoming Figure 8).
The derivation of the equivalence
$(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\Leftrightarrow\chi$
is shown as follows. First, the formulae $\chi\ast\varphi\Rightarrow\psi$ and
$\neg\chi\ast\varphi\Rightarrow\neg\psi$ are shown valid (by using semantical
means). As $\mathcal{H}_{\mathsf{C}}(\ast)$ is complete for
$\mathsf{SL(}\ast,\mathtt{alloc}\mathsf{)}$, it is a subsystem of
$\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$, and the formulae
$\varphi$, $\psi$ and $\chi$ are Boolean combinations of core formulae, we get
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}\chi\ast\varphi\Rightarrow\psi$
and
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}\neg\chi\ast\varphi\Rightarrow\neg\psi$.
The latter theorem leads to
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\Rightarrow\chi$
by using the definition of
$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$ and
the rule 7. For the other direction, in order to show that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}\chi\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)$
holds, we take advantage of the admissibility of the theorem
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.17}}$)
(see Lemma 14 below) for which an instance is
$(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)\wedge(\varphi\mathbin{-\mkern-6.0mu*}\psi)\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}(\top\wedge\psi))$.
From
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}\chi\ast\varphi\Rightarrow\psi$
and by 7 we have
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}\chi\Rightarrow(\varphi\mathbin{-\mkern-6.0mu*}\psi)$.
Therefore, the main technical development lies in the proof of
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}\chi\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$,
which allows us to take advantage of
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.17}}$),
and leads to
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}\chi\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)$
by propositional reasoning.

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

######  Lemma 14.

The following rules and axioms are admissible in
$\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$:

  1. ($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.1}}$)

$\bot\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\varphi\Rightarrow\bot$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.3}}$)
$\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\bot\Rightarrow\bot$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.5}}$)
$\varphi\ast(\varphi\mathbin{-\mkern-6.0mu*}\psi)\Rightarrow\psi$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.7}}$)
$\text{}\frac{\displaystyle\varphi\Rightarrow\psi}{\displaystyle\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\chi\Rightarrow\psi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\chi}{}$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.9}}$)
$\text{}\frac{\displaystyle\varphi\Rightarrow\psi}{\displaystyle\chi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\varphi\Rightarrow\chi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi}{}$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.11}}$)
$\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}(\psi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\chi)\
\Leftrightarrow\
(\varphi*\psi)\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\chi$

  2. ($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.13}}$)

$(\varphi\vee\psi)\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\chi\
\Leftrightarrow\
(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\chi)\vee(\psi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\chi)$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.15}}$)
$\chi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}(\varphi\vee\psi)\
\Leftrightarrow\
(\chi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\varphi)\vee(\chi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.17}}$)
$(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\wedge(\varphi\mathbin{-\mkern-6.0mu*}\chi)\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi\wedge\chi)$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.19}}$)
$\mathtt{x}=\mathtt{y}\land(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\Rightarrow(\varphi\land\mathtt{x}=\mathtt{y}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.21}}$)
$\mathtt{x}\neq\mathtt{y}\land(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\Rightarrow(\varphi\land\mathtt{x}\neq\mathtt{y}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)$
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.23}}$)
$(\varphi_{\mathtt{size}}\land\bigwedge_{\mathtt{x}\in\mathtt{X}}\lnot\mathtt{alloc}(\mathtt{x}))\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$,

  3. where, in axiom ($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.23}}$), $\mathtt{X}\subseteq_{\mathsf{fin}}\mathsf{VAR}$ and $\varphi_{\mathtt{size}}$ is a satisfiable conjunction of literals of the form $\mathtt{size}\geq\beta_{1}$ or $\lnot\mathtt{size}\geq\beta_{2}$.

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

Let $\varphi$ and $\psi$ be two satisfiable core types in
$\mathsf{Conj}(\mathsf{Core}(\mathtt{X},\alpha))$. Following the developments
of Section 5, we define a formula
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
in $\mathsf{Conj}(\mathsf{Core}(\mathtt{X},\alpha))$, for which we show that
$\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi\Leftrightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is provable in $\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$. The
formula
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is defined in Figure 8.

######  Lemma 15.

Let $\mathtt{X}\subseteq_{\mathsf{fin}}\mathsf{VAR}$, $\alpha\geq{\rm
card}(\mathtt{X})$ and $\varphi$, $\psi$ be satisfiable core types in
$\mathsf{CoreTypes}(\mathtt{X},\alpha)$. The formulae
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi\Rightarrow\psi$
and
$(\lnot{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi))\ast\varphi\Rightarrow\lnot\psi$
are valid.

Before presenting the proof for Lemma 15, let us observe that since we aim at
proving the derivability of
$\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi\Leftrightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
in $\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$, the validity of
${(\lnot{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi))\ast\varphi\Rightarrow\lnot\psi}$
should not surprise the reader. Indeed, by replacing
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
with
$\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi$
we obtain
$(\lnot(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi))\ast\varphi\Rightarrow\lnot\psi$
which, unfolding the definition of
$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$, is
equivalent to the valid formula
$(\varphi\mathbin{-\mkern-6.0mu*}\lnot\psi)\ast\varphi\Rightarrow\lnot\psi$
(see
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.5}}$)
in Lemma 14). On the other hand, the fact that
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi\Rightarrow\psi$
is valid can be puzzling at first, as the formula
$(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\ast\varphi\Rightarrow\psi$
is not valid (in general). In its essence, Lemma 15 shows that
$(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\ast\varphi\Rightarrow\psi$
is valid whenever $\varphi$ and $\psi$ are restricted to core types.

$\begin{array}[]{rll}&\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\sim\mathtt{y}\subseteq_{\mathsf{Lt}}\\{\varphi\mathbin{|}\psi\\}\,\middle|\,{{{\begin{array}[]{r}\sim\in\\{=,\neq\\}\end{array}}}}\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{alloc}(\mathtt{x})\,\middle|\,{{{\begin{array}[]{r}\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi\\\
\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\lnot\mathtt{alloc}(\mathtt{x})\,\middle|\,{{{\begin{array}[]{r}\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\lnot\mathtt{x}{\hookrightarrow}\mathtt{y}\subseteq_{\mathsf{Lt}}\psi\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\hookrightarrow\mathtt{y}\,\middle|\,{{{\begin{array}[]{r}\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi\\\
\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\neq\mathtt{x}\,\middle|\,{{{\begin{array}[]{r}\mathtt{alloc}(\mathtt{x})\land\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi\\\
\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{size}\geq\beta_{2}{+}1{\mathbin{\text{\ooalign{\raise
6.19998pt\hbox{.}\cr$-$\cr}}}}\beta_{1}\,\middle|\,{{{\begin{array}[]{r}\lnot\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi\\\
\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\neq\mathtt{x}\,\middle|\,{{{\begin{array}[]{r}\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi\\\
\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\lnot\mathtt{size}\geq\beta_{2}{\mathbin{\text{\ooalign{\raise
6.19998pt\hbox{.}\cr$-$\cr}}}}\beta_{1}\,\middle|\,{{{\begin{array}[]{r}\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi\\\
\lnot\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\neq\mathtt{x}\,\middle|\,{{{\begin{array}[]{r}\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi\\\
\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\end{array}$
Figure 8. The formula
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.

Below, we prove that
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi\Rightarrow\psi$
and
$(\lnot{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi))\ast\varphi\Rightarrow\lnot\psi$
are valid, thus establishing Lemma 15. Notice that the proof is carried out
through semantical arguments. Since $\varphi$, $\psi$ and
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
are conjunctions of literals built from core formulae, derivability of these
two tautologies in $\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$
follows from the completeness of $\mathcal{H}_{\mathsf{C}}(\ast)$ (Theorem
11).

######  Proof 6.2 (Validity of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi\Rightarrow\psi$).

If
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi$
is inconsistent, then
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi\Rightarrow\psi$
is straightforwardly valid. Below, we assume that
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi$
is satisfiable. In particular, none of the conditions depicted in Figure 8
that result in
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
having a literal $\mathtt{x}\neq\mathtt{x}$ applies. Let
$(s,h)\models{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi$.
Therefore, there are two disjoint heaps $h_{1}$ and $h_{2}$ such that
$h=h_{1}{+}h_{2}$,
$(s,h_{1})\models{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
and $(s,h_{2})\models\varphi$. We show that $(s,h)$ satisfies each literal $L$
in $\psi$. We perform a simple case analysis on the shape of $L$. Notice that,
below, we have $\mathtt{x},\mathtt{y}\in\mathtt{X}$ and
$\beta_{2}\in[0,\alpha]$, as $\psi$ is a core type in
$\mathsf{CoreTypes}(\mathtt{X},\alpha)$.

case: $L\ =\ \mathtt{x}\sim\mathtt{y}$, where $\sim\in\\{=,\neq\\}$:

By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$\mathtt{x}\sim\mathtt{y}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
and so $(s,h_{1})\models\mathtt{x}\sim\mathtt{y}$. We conclude that
$s(\mathtt{x})\sim s(\mathtt{y})$, and thus
$(s,h)\models\mathtt{x}\sim\mathtt{y}$.

case: $L\ =\ \mathtt{alloc}(\mathtt{x})$:

If $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$, then
$(s,h_{2})\models\mathtt{alloc}(\mathtt{x})$, which implies
$s(\mathtt{x})\in{\rm dom}(h)$ directly from $h_{2}{\sqsubseteq}h$. Thus,
$(s,h)\models\mathtt{alloc}(\mathtt{x})$. Otherwise, if
$\mathtt{alloc}(\mathtt{x})\not\subseteq_{\mathsf{Lt}}\varphi$ then, since
$\varphi$ is a core type in $\mathsf{CoreTypes}(\mathtt{X},\alpha)$, we have
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$. By definition
of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
we derive that
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
So, $(s,h_{1})\models\mathtt{alloc}(\mathtt{x})$ and thus, by
$h_{1}{\sqsubseteq}h$, $s(\mathtt{x})\in{\rm dom}(h)$. We conclude that
$(s,h)\models\mathtt{alloc}(\mathtt{x})$.

case: $L\ =\ \lnot\mathtt{alloc}(\mathtt{x})$:

In this case, by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
we have
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
which implies $(s,h_{1})\models\lnot\mathtt{alloc}(\mathtt{x})$. _Ad absurdum_
, suppose $(s,h_{2})\models\mathtt{alloc}(\mathtt{x})$. Since $\varphi$ is a
core type in $\mathsf{CoreTypes}(\mathtt{X},\alpha)$, we conclude that
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$. However, by
definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
this implies
$\mathtt{x}\neq\mathtt{x}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
which contradicts the fact that
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is satisfiable. Thus, $(s,h_{2})\models\lnot\mathtt{alloc}(\mathtt{x})$, which
implies $s(\mathtt{x})\not\in{\rm dom}(h_{2})$. From $h=h_{1}{+}h_{2}$ and
$s(\mathtt{x})\not\in{\rm dom}(h_{1})$ we conclude that
$s(\mathtt{x})\not\in{\rm dom}(h)$. So,
$(s,h)\models\lnot\mathtt{alloc}(\mathtt{x})$.

case: $L\ =\ \mathtt{x}\hookrightarrow\mathtt{y}$:

If $\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$, then
${\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
holds by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
So, $h_{1}(s(\mathtt{x}))=s(\mathtt{y})$ and, from $h_{1}{\sqsubseteq}h$ we
conclude that $(s,h)\models\mathtt{x}\hookrightarrow\mathtt{y}$. Otherwise,
let us assume that $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$.
_Ad absurdum_ , suppose
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$.
Then, by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
we derive
$\mathtt{x}\neq\mathtt{x}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
However, this contradicts the satisfiability of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
Therefore,
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\not\subseteq_{\mathsf{Lt}}\varphi$.
Since $\varphi$ is a core type, this implies
$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$, and
therefore $h_{2}(s(\mathtt{x}))=s(\mathtt{y})$. From $h_{2}{\sqsubseteq}h$ we
conclude that $(s,h)\models\mathtt{x}\hookrightarrow\mathtt{y}$.

case: $L\ =\ \lnot\mathtt{x}\hookrightarrow\mathtt{y}$:

By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\mathtt{x},\mathtt{y})$,
we have
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\mathtt{x},\mathtt{y})$,
which implies that if $s(\mathtt{x})\in{\rm dom}(h_{1})$ then
$h_{1}(s(\mathtt{x}))\neq s(\mathtt{y})$. _Ad absurdum_ , suppose
$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$. Then, by
definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
we derive
$\mathtt{x}\neq\mathtt{x}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
However, this contradicts the satisfiability of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
Therefore
$\mathtt{x}\hookrightarrow\mathtt{y}\not\subseteq_{\mathsf{Lt}}\varphi$ and,
since $\varphi$ is a core type,
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$. So,
if $s(\mathtt{x})\in{\rm dom}(h_{2})$ then $h_{2}(s(\mathtt{x}))\neq
s(\mathtt{y})$. By $h=h_{1}+h_{2}$ and the fact that $h_{1}(s(\mathtt{x}))\neq
s(\mathtt{y})$, we conclude that
$(s,h)\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$.

case: $L\ =\ \mathtt{size}\geq\beta_{2}$:

If $\mathtt{size}\geq\alpha\subseteq_{\mathsf{Lt}}\varphi$, then ${\rm
card}({\rm dom}(h))\geq{\rm card}({\rm dom}(h_{2}))\geq\alpha$, by
$h_{2}{\sqsubseteq}h$. As $\beta_{2}\in[0,\alpha]$, this implies
$(s,h)\models\mathtt{size}\geq\beta_{2}$. Otherwise, assume
$\mathtt{size}\geq\alpha\not\subseteq_{\mathsf{Lt}}\varphi$. In particular,
since $\varphi$ is in $\mathsf{CoreTypes}(\mathtt{X},\alpha)$, this implies
that $\max_{\mathtt{size}}(\varphi)<\alpha$ and

$\textstyle\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\land\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1\
\subseteq_{\mathsf{Lt}}\ \varphi.$

We have ${\rm card}({\rm dom}(h_{2}))=\max_{\mathtt{size}}(\varphi)$. If
$\max_{\mathtt{size}}(\varphi)\geq\beta_{2}$, then from $h_{2}{\sqsubseteq}h$
we conclude that $(s,h)\models\mathtt{size}\geq\beta_{2}$. Otherwise, let us
assume $\beta_{2}>\max_{\mathtt{size}}(\varphi)$. By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
we conclude that $\mathtt{size}\geq\beta_{2}+1\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}(\max_{\mathtt{size}}(\varphi)+1)\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
Together with $\beta_{2}>\max_{\mathtt{size}}(\varphi)$, this implies ${\rm
card}({\rm dom}(h_{1}))\geq\beta_{2}-\max_{\mathtt{size}}(\varphi)$. With
${\rm card}({\rm dom}(h_{2}))=\max_{\mathtt{size}}(\varphi)$ and
$h=h_{1}{+}h_{2}$, this implies $(s,h)\models\mathtt{size}\geq\beta_{2}$.

case: $L\ =\ \lnot\mathtt{size}\geq\beta_{2}$:

_Ad absurdum_ , suppose that
$\mathtt{size}\geq\alpha\subseteq_{\mathsf{Lt}}\varphi$. Then, by definition
of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
we have $\lnot\mathtt{size}\geq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\alpha\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
However, since $\beta_{2}\in[0,\alpha]$, this means that
$\lnot\mathtt{size}\geq
0\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
which contradicts the satisfiability of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
Therefore, $\mathtt{size}\geq\alpha\not\subseteq_{\mathsf{Lt}}\varphi$. As
$\varphi$ is in $\mathsf{CoreTypes}(\mathtt{X},\alpha)$, we derive
$\max_{\mathtt{size}}(\varphi)<\alpha$ and

$\textstyle\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\land\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1\
\subseteq_{\mathsf{Lt}}\ \varphi.$

We conclude that ${\rm card}({\rm
dom}(h_{2}))\leq\max_{\mathtt{size}}(\varphi)$. From
$\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\subseteq_{\mathsf{Lt}}\varphi$
and by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
we conclude that

$\textstyle\lnot\mathtt{size}\geq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\max_{\mathtt{size}}(\varphi)\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi).$

If $\beta_{2}\leq\max_{\mathtt{size}}(\varphi)$, then $\lnot\mathtt{size}\geq
0\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
which contradicts the satisfiability of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
Therefore, $\beta_{2}>\max_{\mathtt{size}}(\varphi)$. So, ${\rm card}({\rm
dom}(h_{1}))<\beta_{2}-\max_{\mathtt{size}}(\varphi)$. Together with ${\rm
card}({\rm dom}(h_{2}))\leq\max_{\mathtt{size}}(\varphi)$ and $h=h_{1}{+}h$,
we conclude that ${\rm card}({\rm dom}(h))<\beta_{2}$, and thus
$(s,h)\models\lnot\mathtt{size}\geq\beta_{2}$.

######  Proof 6.3 (Validity of
$(\lnot{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi))\ast\varphi\Rightarrow\lnot\psi$).

Let us assume
$(s,h)\models(\neg{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi))\ast\varphi$.
Consequently, there is a literal $L$ of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
such that $(s,h)\models(\neg L)\ast\varphi$ holds. We show that
$(s,h)\models\lnot\psi$. Let $h_{1}$ and $h_{2}$ be two disjoint heaps such
that $h=h_{1}{+}h_{2}$, $(s,h_{1})\models\lnot 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
$\mathtt{x},\mathtt{y}\in\mathtt{X}$ and $\beta_{1},\beta_{2}\in[0,\alpha]$.

case: $L\ =\ \mathtt{x}\neq\mathtt{x}$:

Since $\varphi$ and $\psi$ are satisfiable, by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
the fact that
$\mathtt{x}\neq\mathtt{x}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
implies that one of the following three cases holds:

  * 1::

$\mathtt{alloc}(\mathtt{x})\wedge\neg\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$
and $\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$.

  * From $\mathtt{alloc}(\mathtt{x})\wedge\neg\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$ and $h_{2}{\sqsubseteq}h$, we have $s(\mathtt{x})\in{\rm dom}(h)$ and $h(s(\mathtt{x}))\neq s(\mathtt{y})$. Thus $(s,h)\not\models\mathtt{x}\hookrightarrow\mathtt{y}$, and so, by $\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$, $(s,h)\models\lnot\psi$.

  * 2::

$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$ and
$\neg\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$.

  * From $\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$ and $h_{2}{\sqsubseteq}h$, $h(s(\mathtt{x}))=s(\mathtt{y})$. Thus $(s,h)\models\mathtt{x}\hookrightarrow\mathtt{y}$ and so, by $\neg\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$, $(s,h)\models\lnot\psi$.

  * 3::

$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ and
$\neg\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$.

  * From $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ and $h_{2}{\sqsubseteq}h$, $s(\mathtt{x})\in{\rm dom}(h)$. Thus $(s,h)\models\mathtt{alloc}(\mathtt{x})$ and so, by $\neg\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$, $(s,h)\models\lnot\psi$.

case: $L\ =\ \mathtt{x}\sim\mathtt{y}$, where $\sim\in\\{=,\neq\\}$:

In this case, since $(s,h_{1})\models\lnot L$, then we have $(s,h)\models\lnot
L$. Now, it cannot be that $L\subseteq_{\mathsf{Lt}}\varphi$, as it would
imply $(s,h)\models L$, which is contradictory. Therefore, by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
we must have $L\subseteq_{\mathsf{Lt}}\psi$. This implies
$(s,h)\models\lnot\psi$.

case: $L\ =\ \mathtt{alloc}(\mathtt{x})$:

By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$\neg\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ and
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$. From
$(s,h_{1})\models\lnot\mathtt{alloc}(\mathtt{x})$ we conclude that
$s(\mathtt{x})\not\in{\rm dom}(h_{1})$. By
$\neg\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$,
$s(\mathtt{x})\not\in{\rm dom}(h_{2})$. By $h=h_{1}{+}h_{2}$,
$s(\mathtt{x})\not\in{\rm dom}(h)$. As
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$,
${(s,h)\models\lnot\psi}$.

case: $L\ =\ \neg\mathtt{alloc}(\mathtt{x})$:

As $(s,h_{1})\models\lnot L$, we have $s(\mathtt{x})\in{\rm dom}(h_{1})$.
According to the definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
either $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ or
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$. The first case
cannot hold, as it implies $s(\mathtt{x})\in{\rm dom}(h_{2})$ which
contradicts the fact that $h_{1}$ and $h_{2}$ are disjoint. In the second
case, from $s(\mathtt{x})\in{\rm dom}(h_{1})$ and $h_{1}{\sqsubseteq}h$, we
have $(s,h)\models\mathtt{alloc}(\mathtt{x})$. So, $(s,h)\models\lnot\psi$.

case: $L\ =\ \mathtt{x}\hookrightarrow\mathtt{y}$:

Then by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$\neg\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ and
$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$. From
$(s,h_{1})\models\lnot L$, if $s(\mathtt{x})\in{\rm dom}(h_{1})$ then
$h_{1}(s(\mathtt{x}))\neq s(\mathtt{y})$. As
$\neg\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$,
$s(\mathtt{x})\not\in{\rm dom}(h_{2})$ and therefore, by $h=h_{1}{+}h_{2}$,
$h(s(\mathtt{x}))\neq s(\mathtt{y})$. From
$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$, we conclude
that $(s,h)\models\lnot\psi$.

case: $L\ =\ \neg\mathtt{x}\hookrightarrow\mathtt{y}$:

Then, by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$\neg\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$. From
$(s,h_{1})\models\lnot L$ and $h_{1}{\sqsubseteq}h$, we derive
$h(s(\mathtt{x}))=s(\mathtt{y})$. From
$\neg\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$, we
derive $(s,h)\models\lnot\psi$.

case: $L\ =\ \mathtt{size}\geq\beta_{2}+1\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\beta_{1}$, where
$\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi$ and
$\neg\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi$:

Since it holds that $(s,h_{1})\models\lnot L$ and $(s,h_{2})\models\varphi$,
we derive (respectively) ${\rm card}({\rm
dom}(h_{1}))\leq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\beta_{1}$ and ${{\rm card}({\rm
dom}(h_{2}))<\beta_{1}}$. From $h=h_{1}{+}h_{2}$, we conclude that ${\rm
card}({\rm dom}(h))<\beta_{2}$. From
$\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi$, we derive
$(s,h)\models\lnot\psi$.

case: $L\ =\ \neg\mathtt{size}\geq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\beta_{1}$, where
$\neg\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi$ and
$\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi$:

Since we have $(s,h_{1})\models\lnot L$ and $(s,h_{2})\models\varphi$, we
conclude that ${\rm card}({\rm
dom}(h_{1}))\geq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\beta_{1}$ and ${\rm card}({\rm
dom}(h_{2}))\geq\beta_{1}$. So, $h=h_{1}{+}h_{2}$ implies ${\rm card}({\rm
dom}(h))\geq\beta_{2}$. By
$\neg\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi$, we derive
$(s,h)\models\lnot\psi$.

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

######  Proof 6.4 (Proof of Lemma 13).

As in the statement of the lemma, let us consider
$\mathtt{X}\subseteq_{\mathsf{fin}}\mathsf{VAR}$ and $\alpha\geq{\rm
card}(\mathtt{X})$, and two core types $\varphi$ and $\psi$ in
$\mathsf{CoreTypes}(\mathtt{X},\alpha)$. We want to show that there is a
conjunction $\chi\in\mathsf{Conj}(\mathsf{Core}(\mathtt{X},\alpha))$ such that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\Leftrightarrow\chi$.

First of all, if $\varphi$ or $\psi$ is unsatisfiable, then
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi\Rightarrow\bot$
by using Lemma 3 and the admissible axioms
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.7}}$)
and
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.9}}$)
from Lemma 14. Therefore, in this case, it is enough to take $\chi$ equal to
$\lnot\mathtt{x}=\mathtt{x}$ to complete the proof. Otherwise, let us assume
that $\varphi$ and $\psi$ are satisfiable. We consider
$\chi\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
(see Figure 8), and show that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\Leftrightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
We derive each implication separately.

#### ($\Rightarrow$):

Given Lemma 15, the proof of
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi\Rightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is straightforward:

$1$ | $\neg{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi\Rightarrow\neg\psi$ | Lemma 15, Theorem 11
---|---|---
$2$ | $\neg{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi\mathbin{-\mkern-6.0mu*}\neg\psi)$ | 7, 1
$3$ | $\neg(\varphi\mathbin{-\mkern-6.0mu*}\neg\psi)\Rightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$ | PC, 2
$4$ | $(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi)\Rightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$ | Def. of $\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$, 3

#### ($\Leftarrow$):

Let us now show that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi$.
First, let us note that, since
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\varphi\Rightarrow\psi$
is valid (Lemma 15), it is derivable in $\mathcal{H}_{\mathsf{C}}(\ast){}$
(Theorem 11), and therefore, by the rule 7,
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{-\mkern-6.0mu*}\psi$.
From that, it follows that it is enough to show that
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$
is derivable in $\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$.
Indeed, from
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$
and
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{-\mkern-6.0mu*}\psi$,
we get, by
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.17}}$),
that
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\psi$
is derivable too.

Thus, let us prove that
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$
is derivable. If
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is unsatisfiable, then from the completeness of $\mathcal{H}_{\mathsf{C}}$
with respect to Boolean combinations of core formulae (Theorem 5), we conclude
that
$\vdash_{\mathcal{H}_{\mathsf{C}}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\perp$.
Since $\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$ extends
$\mathcal{H}_{\mathsf{C}}$, we have
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\perp$.
By propositional reasoning,
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$.
Otherwise, let us assume that
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is satisfiable.

######  Proof 6.5 (Structure of the remaining part of the proof).

Before presenting the technical arguments for the derivation of
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$
when
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is satisfiable, let us explain what are the main ingredients. The proof
establishing that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$
is by induction on the number $j$ of variables $\mathtt{x}\in\mathtt{X}$ for
which $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ holds. As
$\varphi$, $\psi$ and
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\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 14. For the
induction step $j>0$, some more substantial work is needed and this is briefly
described below. We distinguish the case
$\max_{\mathtt{size}}(\varphi)<\alpha$ from the case
$\max_{\mathtt{size}}(\varphi)=\alpha$. Both cases, we introduce the formula
$\textit{\small{Atom}}(\mathtt{x}_{i})$ where
$\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi$.

$\textit{\small{Atom}}(\mathtt{x}_{i})\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\begin{cases}\mathtt{x}_{i}\hookrightarrow\mathtt{y}\land\mathtt{size}=1&\text{if}~{}\mathtt{x}_{i}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi,\text{
for some }\mathtt{y}\in\mathtt{X}\\\
\mathtt{alloc}(\mathtt{x}_{i})\land\mathtt{size}=1\land\bigwedge_{\mathtt{y}\in\mathtt{X}}\lnot\mathtt{x}_{i}\hookrightarrow\mathtt{y}&\text{otherwise}\end{cases}$

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

  * A. :

$\varphi^{\prime}$ is a satisfiable core type in
$\mathsf{CoreTypes}(\mathtt{X},\alpha)$.

  * B. :

$(\textit{\small{Atom}}(\mathtt{x}_{i})\ast\varphi^{\prime})\Rightarrow\varphi$
is valid.

  * C. :

$({\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\textit{\small{Atom}}(\mathtt{x}_{i}))\Rightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$
is valid.

In order to conclude
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$,
we take advantage of the completeness of $\mathcal{H}_{\mathsf{C}}(\ast)$ to
derive the tautologies in B. :  and C. : . Moreover, as by construction of
$\varphi^{\prime}$, we have
$\lnot\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$
and, for every $\mathtt{y}\in\mathtt{X}$,
$\lnot\mathtt{alloc}(\mathtt{y})\subseteq_{\mathsf{Lt}}\varphi$ implies
$\lnot\mathtt{alloc}(\mathtt{y})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$, we
shall be able to apply the induction hypothesis on $\varphi^{\prime}$ to get
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)\Rightarrow(\varphi^{\prime}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$,
which will be essential in the final derivation for
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$.

In the remaining case $\max_{\mathtt{size}}(\varphi)=\alpha$, we are still
looking for some formula $\varphi^{\prime}$ such that
$\varphi^{\prime}\ast\textit{\small{Atom}}(\mathtt{x}_{i})\Rightarrow\varphi$
is valid but we cannot hope for $\varphi^{\prime}$ to be a core type in
$\mathsf{CoreTypes}(\mathtt{X},\alpha)$. Instead, we introduce two core types
$\varphi_{\alpha}^{\prime}$ and $\varphi_{\alpha-1}^{\prime}$, and define
$\varphi^{\prime}$ as
$\varphi_{\alpha}^{\prime}\lor\varphi_{\alpha-1}^{\prime}$. The only
difference between $\varphi_{\alpha}^{\prime}$ and
$\varphi_{\alpha-1}^{\prime}$ rests on the fact that
$\mathtt{size}\geq\alpha\subseteq_{\mathsf{Lt}}\varphi_{\alpha}^{\prime}$
whereas
$\neg\mathtt{size}\geq\alpha\subseteq_{\mathsf{Lt}}\varphi_{\alpha-1}^{\prime}$
(both formulae contain $\mathtt{size}\geq\alpha-1$). Similarly to the previous
case, the properties below shall be shown.

  * D. :

$\varphi_{\alpha}^{\prime}$ and $\varphi_{\alpha-1}^{\prime}$ are satisfiable
core types in $\mathsf{CoreTypes}(\mathtt{X},\alpha)$

  * E. :

$(\textit{\small{Atom}}(\mathtt{x}_{i})\ast(\varphi_{\alpha}^{\prime}\lor\varphi_{\alpha-1}^{\prime}))\Rightarrow\varphi$
is valid.

  * F. :

$({\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\textit{\small{Atom}}(\mathtt{x}_{i}))\Rightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi_{\alpha}^{\prime},\psi)\lor{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi_{\alpha-1}^{\prime},\psi)$
is valid.

The derivation of
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$
follows then a principle similar to one for the case
$\max_{\mathtt{size}}(\varphi)<\alpha$.

Now, let us present the technical developments. Directly from the definition
of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
the following simple facts hold.

  * 1\.

$\varphi$, $\psi$ and
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
have exactly the same equalities and inequalities.

  * 2\.

$\neg\mathtt{size}\geq 0$ is not part of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
and therefore, following the definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
there are no $\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi$ and
$\neg\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi$ with
$\beta_{1}\geq\beta_{2}$.

  * 3\.

$\mathtt{x}\neq\mathtt{x}$ does not belong to
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
In particular, by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
none of the following conditions apply:

    * –

there is $\mathtt{x}\in\mathtt{X}$ such that
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ and
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$,

    * –

there are $\mathtt{x},\mathtt{y}\in\mathtt{X}$ such that
$\mathtt{x}\hookrightarrow\mathtt{y}\in\varphi$ and
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$,

    * –

there are $\mathtt{x},\mathtt{y}\in\mathtt{X}$ such that
$\mathtt{alloc}(\mathtt{x})\land\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$
and $\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$.

From 1., we know that
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
and $\varphi$ satisfy the same (in)equalities. Similarly to the proof of Lemma
9, let $\mathtt{x}_{1},\ldots\mathtt{x}_{n}$ be a maximal enumeration of
representatives of the equivalence classes (one per equivalence class) such
that $\mathtt{alloc}(\mathtt{x}_{i})$ occurs in $\varphi$. As it is maximal,
for every $\mathtt{alloc}(\mathtt{x})$ in $\mathsf{Lt}(\varphi)$ there is
$i\in[1,n]$ such that $\mathtt{x}_{i}$ is syntactically equal to $\mathtt{x}$.
Moreover, by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
for every $i\in[1,n]$,
$\lnot\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
The proof of
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$
is by induction on the number $j$ of variables $\mathtt{x}\in\mathtt{X}$ for
which $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ holds.

base case: $j=0$:

In the base case, no formula $\mathtt{alloc}(\mathtt{x})$ occurs positively in
$\varphi$. Since $\varphi$ is a core type, this implies that for every
$\mathtt{x}\in\mathtt{X}$,
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$. Moreover,
since $\varphi$ is satisfiable, for every
$\mathtt{x},\mathtt{y}\in\mathtt{X}$,
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$ (see
the axiom ($\mathbf{A^{\mathsf{C}}_{5}}$)). Therefore, the core type $\varphi$
is syntactically equivalent (up to associativity and commutativity of
conjunction) to the formula
$\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}},$
where

  * •:

$\varphi_{\mathtt{size}}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\bigwedge\big{(}\\{\mathtt{size}\geq\beta\subseteq_{\mathsf{Lt}}\varphi\\}\cup\\{\lnot\mathtt{size}\geq\beta\subseteq_{\mathsf{Lt}}\varphi\\}\big{)}$,

  * •:

$\varphi_{\lnot\mathtt{alloc}}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\bigwedge_{\mathtt{x}\in\mathtt{X}}\lnot\mathtt{alloc}(\mathtt{x})$,

  * •:

$\varphi_{\not\hookrightarrow}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\bigwedge_{\mathtt{x},\mathtt{y}\in\mathtt{X}}\lnot\mathtt{x}\hookrightarrow\mathtt{y}$,

  * •:

$\varphi_{\texttt{(in)eq}}\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\bigwedge\\{\mathtt{x}\sim\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi\mid\sim\in\\{=,\neq\\}\\}$.

Since $\varphi$ is satisfiable, so is $\varphi_{\mathtt{size}}$. We show that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow})\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$:

$1$ | $\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$ | ($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.23}}$)
---|---|---
$2$ | $\lnot\mathtt{alloc}(\mathtt{x})\Rightarrow\lnot\mathtt{x}\hookrightarrow\mathtt{y}$ | ($\mathbf{A^{\mathsf{C}}_{5}}$), PC
$3$ | $\varphi_{\lnot\texttt{alloc}}\Rightarrow\varphi_{\not\hookrightarrow}$ | PC, repeated 2
$4$ | $\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\Rightarrow\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}$ | PC, 3
$5$ | $(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)\Rightarrow(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | ($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.7}}$), 4
$6$ | $\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$ | Modus Ponens, 1, 5

Now, let us treat the formula $\varphi_{\texttt{(in)eq}}$. From the definition
of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
we have
$\varphi_{\texttt{(in)eq}}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
and so by propositional reasoning,
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi_{\texttt{(in)eq}}$.
This allows us to conclude that

$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\big{(}(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}})\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top\big{)},$
($\dagger$)

by induction on the number of literals $\mathtt{x}\sim\mathtt{y}$ appearing in
$\varphi_{\texttt{(in)eq}}$, and by relying on the two theorems
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.19}}$)
and
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.21}}$).
In the base case, $\varphi_{\texttt{(in)eq}}=\top$, and so

$7$ | $\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\Rightarrow\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}$ | PC
---|---|---
$8$ | $(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)\Rightarrow(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | ($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.7}}$), 7
$9$ | $\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$ | Modus Ponens, 6, 8
$10$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | PC, 9

In the induction step, let
$\varphi_{\texttt{(in)eq}}=\varphi_{\texttt{(in)eq}}^{\prime}\land\mathtt{x}\sim\mathtt{y}$,
where
$\mathtt{x}\sim\mathtt{y}\not\subseteq_{\mathsf{Lt}}\varphi_{\texttt{(in)eq}}^{\prime}$.
We have,

$1$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}^{\prime}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | Induction Hypothesis
---|---|---
$2$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\mathtt{x}\sim\mathtt{y}$ | PC, as $\varphi_{\texttt{(in)eq}}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
$3$ | $\mathtt{x}\sim\mathtt{y}\land(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}^{\prime}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)\Rightarrow$ |
| $\qquad(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}^{\prime}\land\mathtt{x}\sim\mathtt{y}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | ($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.19}}$)/($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.21}}$)
$4$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}^{\prime}\land\mathtt{x}\sim\mathtt{y}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | PC, 1, 2, 3
$5$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | Def. of $\varphi_{\texttt{(in)eq}}^{\prime}$, 4

Since
$\varphi_{\mathtt{size}}\land\varphi_{\lnot\texttt{alloc}}\land\varphi_{\not\hookrightarrow}\land\varphi_{\texttt{(in)eq}}$
is equivalent to $\varphi$, from ($\dagger$ ‣ base case: $j=0$: ) and by
($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.7}}$),
we conclude that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top$.

induction step: $j\geq 1$:

In this case, let $i\in[1,n]$ such that
$\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi$ and thus, by
definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$\lnot\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
As announced earlier, we define the formula:

$\textit{\small{Atom}}(\mathtt{x}_{i})\stackrel{{\scriptstyle\mbox{\tiny
def}}}{{=}}\begin{cases}\mathtt{x}_{i}\hookrightarrow\mathtt{y}\land\mathtt{size}=1&\text{if}~{}\mathtt{x}_{i}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi,\text{
for some }\mathtt{y}\in\mathtt{X}\\\
\mathtt{alloc}(\mathtt{x}_{i})\land\mathtt{size}=1\land\bigwedge_{\mathtt{y}\in\mathtt{X}}\lnot\mathtt{x}_{i}\hookrightarrow\mathtt{y}&\text{otherwise}\end{cases}$

Notice that, if there is $\mathtt{y}\in\mathtt{X}$ such that
$\mathtt{x}_{i}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$, then
the axiom schema ($\mathbf{A^{\mathbin{-\mkern-6.0mu*}}_{23}}$) can be
instantiated to
$\lnot\mathtt{alloc}(\mathtt{x}_{i})\Rightarrow(\textit{\small{Atom}}(\mathtt{x}_{i})\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$.
Otherwise (for all $\mathtt{y}\in\mathtt{X}$,
$\mathtt{x}_{i}\hookrightarrow\mathtt{y}\not\subseteq_{\mathsf{Lt}}\varphi$)
this formula is an instantiation of the axiom schema
($\mathbf{A^{\mathbin{-\mkern-6.0mu*}}_{25}}$). This allows us to show the
following theorem:

${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\big{(}\textit{\small{Atom}}(\mathtt{x}_{i})\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}({\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\textit{\small{Atom}}(\mathtt{x}_{i}))\big{)}$
($\ddagger$)

$1$ | $\neg\mathtt{alloc}(\mathtt{x}_{i})\Rightarrow(\textit{\small{Atom}}(\mathtt{x}_{i})\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | ($\mathbf{A^{\mathbin{-\mkern-6.0mu*}}_{23}}$)/($\mathbf{A^{\mathbin{-\mkern-6.0mu*}}_{25}}$)
---|---|---
$2$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow\neg\mathtt{alloc}(\mathtt{x}_{i})$ | Def. of ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$, PC
$3$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\textit{\small{Atom}}(\mathtt{x}_{i})\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | 3, 1, 2
$4$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\textit{\small{Atom}}(\mathtt{x}_{i})\Rightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\textit{\small{Atom}}(\mathtt{x}_{i})$ | PC
$5$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\textit{\small{Atom}}(\mathtt{x}_{i})\mathbin{-\mkern-6.0mu*}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\textit{\small{Atom}}(\mathtt{x}_{i}))$ | 7, 4
$6$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\textit{\small{Atom}}(\mathtt{x}_{i})\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\textit{\small{Atom}}(\mathtt{x}_{i}))$ | ($\mathbf{I^{\mathbin{-\mkern-6.0mu*}}_{\ref{lemma:septractionadmissible}.17}}$), 3, 5, PC

From the hypothesis ${\rm card}(\mathtt{X})\leq\alpha$, together with
$\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi$ and the fact
that $\varphi$ is satisfiable, we have $\max_{\mathtt{size}}(\varphi)\geq 1$
(see ($\mathbf{I^{\mathsf{C}}_{11}}$), instantiated with
$\mathtt{X}=\\{\mathtt{x}_{i}\\}$). In order to show that
$\vdash_{\mathcal{H}_{\mathsf{C}}{\ast,\mathbin{-\mkern-6.0mu*}}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$,
we split the proof depending on whether $\max_{\mathtt{size}}(\varphi)<\alpha$
holds.

case: $\max_{\mathtt{size}}(\varphi)<\alpha$:

Since $\varphi$ is a satisfiable core type in
$\mathsf{CoreTypes}(\mathtt{X},\alpha)$, by definition of
$\max_{\mathtt{size}}(.)$, we have
$\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\land\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1\subseteq_{\mathsf{Lt}}\varphi$.
Below, we consider the formula $\varphi^{\prime}$ obtained from $\varphi$ by:

  * •:

replacing
$\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\subseteq_{\mathsf{Lt}}\varphi$
with $\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)$,

  * •:

for every $\mathtt{x}\in\mathtt{X}$ such that
$\mathtt{x}=\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$, replacing every
literal $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ with
$\lnot\mathtt{alloc}(\mathtt{x})$, and every literal
$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$ with
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}$, where $\mathtt{y}\in\mathtt{X}$.

Explicitly,

$\varphi^{\prime}\stackrel{{\scriptstyle\mbox{\tiny def}}}{{=}}\begin{aligned}
&\bigwedge\\{\mathtt{x}\sim\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi\mid\sim\in\\{=,\neq\\}\\}\land\bigwedge\\{\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi\mid\mathtt{x}\neq\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi\\}\land\\\
&\bigwedge\\{\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi\\}\land\bigwedge\\{\lnot\mathtt{alloc}(\mathtt{x})\mid\mathtt{x}=\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi\\}\land\bigwedge\\{\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi\mid\mathtt{x}\neq\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi\\}\land\\\
&\bigwedge\\{\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi\\}\land\bigwedge\\{\lnot\mathtt{x}\hookrightarrow\mathtt{y}\mid\mathtt{x}=\mathtt{x}_{i}\land\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi\\}\land\lnot\mathtt{size}\geq{\textstyle\max_{\mathtt{size}}(\varphi)}\land\\\
&\bigwedge\\{\mathtt{size}\geq\beta\subseteq_{\mathsf{Lt}}\varphi\mid\beta<{\textstyle\max_{\mathtt{size}}(\varphi)}\\}\land\bigwedge\\{\lnot\mathtt{size}\geq\beta\subseteq_{\mathsf{Lt}}\varphi\\}.\end{aligned}$

The formula $\varphi^{\prime}$ enjoys the following properties (to be shown
below):

  * A. :

$\varphi^{\prime}$ is a satisfiable core type in
$\mathsf{CoreTypes}(\mathtt{X},\alpha)$.

  * B. :

$(\textit{\small{Atom}}(\mathtt{x}_{i})\ast\varphi^{\prime})\Rightarrow\varphi$
is valid.

  * C. :

$({\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\textit{\small{Atom}}(\mathtt{x}_{i}))\Rightarrow{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$
is valid.

Fundamentally, $\varphi^{\prime}$ enjoys the induction hypothesis, which
reveals to be useful later on.

######  Proof 6.6 (Proof of A. : ).

Since $\varphi^{\prime}$ is obtained from $\varphi$ simply by changing the
polarity of some of the literals in $\mathsf{Lt}(\varphi)$, clearly
$\varphi^{\prime}$ is in $\mathsf{CoreTypes}(\mathtt{X},\alpha)$. To show that
$\varphi^{\prime}$ is satisfiable, we rely on the fact that $\varphi$ is
satisfiable. Let $(s,h)$ be a memory state satisfying $\varphi$. Since
$\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi$, we conclude
that $s(\mathtt{x}_{i})\in{\rm dom}(h)$. Let us consider the disjoint heaps
$h_{1}$ and $h_{2}$ such that $h=h_{1}+h_{2}$ and ${\rm
dom}(h_{1})=\\{s(\mathtt{x}_{i})\\}$. We show that
$(s,h_{2})\models\varphi^{\prime}$ by considering every
$L\in\mathsf{Lt}(\varphi^{\prime})$ and showing that $(s,h_{2})\models L$.

case: $L\,=\,\mathtt{x}\sim\mathtt{y}$, where $\sim\in\\{=,\neq\\}$:

By definition of $\varphi^{\prime}$, $(s,h)\models L$ and therefore
$s(\mathtt{x})\sim s(\mathtt{y})$. Thus, $(s,h_{2})\models L$.

case: $L\,=\,\lnot\mathtt{alloc}(\mathtt{x})$:

If $\mathtt{x}=\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$ then
$s(\mathtt{x})\in{\rm dom}(h_{1})$, and therefore, by $h_{1}\sharp h_{2}$,
$s(\mathtt{x})\not\in{\rm dom}(h_{2})$. So,
$(s,h_{2})\models\lnot\mathtt{alloc}(\mathtt{x})$. Otherwise
($\mathtt{x}\neq\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$), by definition
of $\varphi^{\prime}$, we have
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$. So
$s(\mathtt{x})\not\in{\rm dom}(h)$ and, from $h_{2}{\sqsubseteq}h$, we
conclude that $(s,h_{2})\models\lnot\mathtt{alloc}(\mathtt{x})$.

case: $L\,=\,\lnot\mathtt{x}\hookrightarrow\mathtt{y}$:

Similar to the previous case. Briefly, if
$\mathtt{x}=\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$ then, by definition
of $\textit{\small{Atom}}(\mathtt{x}_{i})$,
$(s,h_{2})\not\models\mathtt{alloc}(\mathtt{x})$, which implies
$(s,h_{2})\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$. Otherwise, by
definition of $\varphi^{\prime}$,
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$ and
thus $(s,h)\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$. From
$h_{2}{\sqsubseteq}h$, we conclude that
$(s,h_{2})\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$.

case: $L\,=\,\mathtt{alloc}(\mathtt{x})$:

By definition of $\varphi^{\prime}$,
$\mathtt{alloc}(\mathtt{x})\land\mathtt{x}\neq\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$.
Therefore $s(\mathtt{x})\in{\rm dom}(h)$ and, by definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$, $s(\mathtt{x})\not\in{\rm
dom}(h_{1})$. Since $h=h_{1}{+}h_{2}$, we conclude that
$(s,h_{2})\models\mathtt{alloc}(\mathtt{x})$.

case: $L\,=\,\mathtt{x}\hookrightarrow\mathtt{y}$:

Similar to the previous case. By definition of $\varphi^{\prime}$, we have
${\mathtt{x}\hookrightarrow\mathtt{y}}\land\mathtt{x}\neq\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$.
Thus, $h(s(\mathtt{x}))=s(\mathtt{y})$. By definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$, $s(\mathtt{x})\in{\rm dom}(h_{2})$
and thus $h_{2}(s(\mathtt{x}))=s(\mathtt{y})$. So,
$(s,h_{2})\models\mathtt{x}\hookrightarrow\mathtt{y}$.

case: $L\,=\,\mathtt{size}\geq\beta$:

By definition of $\varphi^{\prime}$, $\beta<\max_{\mathtt{size}}(\varphi)$.
Since $(s,h)\models\varphi$, we have ${\rm card}({\rm
dom}(h))\geq\max_{\mathtt{size}}(\varphi)$. By definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$ and from $h=h_{1}{+}h_{2}$, we have
${\rm card}({\rm dom}(h_{2}))={\rm card}({\rm
dom}(h)){-}1\geq\max_{\mathtt{size}}(\varphi){-}1\geq\beta$. So,
${(s,h_{2})\models\mathtt{size}\geq\beta}$.

case: $L\,=\,\lnot\mathtt{size}\geq\beta$:

By definition of $\varphi^{\prime}$,
${\lnot\mathtt{size}\geq\beta\subseteq_{\mathsf{Lt}}\varphi}$ or
${\beta=\max_{\mathtt{size}}(\varphi)}$. In the former case, since $\varphi$
is satisfiable, we know that $\beta>\max_{\mathtt{size}}(\varphi)$. Hence, in
both cases we have $\beta\geq\max_{\mathtt{size}}(\varphi)$. As
$(s,h)\models\varphi$ and
$\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1\subseteq_{\mathsf{Lt}}\varphi$,
we have ${\rm card}({\rm dom}(h))\leq\max_{\mathtt{size}}(\varphi)$. Since
${\rm card}({\rm dom}(h_{1}))=1$, by $h=h_{1}{+}h_{2}$ we derive ${\rm
card}({\rm dom}(h_{2}))<\max_{\mathtt{size}}(\varphi)\leq\beta$. Therefore,
$(s,h_{2})\models\lnot\mathtt{size}\geq\beta$.

######  Proof 6.7 (Proof of B. : ).

Let $(s,h)\models\textit{\small{Atom}}(\mathtt{x}_{i})\ast\varphi^{\prime}$.
So, there are $h_{1}$ and $h_{2}$ such that $h=h_{1}{+}h_{2}$,
$(s,h_{1})\models\textit{\small{Atom}}(\mathtt{x}_{i})$ and
$(s,h_{2})\models\varphi^{\prime}$. By definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$, ${\rm
dom}(h_{1})=\\{s(\mathtt{x}_{i})\\}$. In order to prove B. : , we show that
$(s,h)\models L$, for every literal $L\in\mathsf{Lt}(\varphi)$.

case: $L\,=\,\mathtt{x}\sim\mathtt{y}$, where $\sim\in\\{=,\neq\\}$:

By definition of $\varphi^{\prime}$, $(s,h_{2})\models L$ and therefore
$s(\mathtt{x})\sim s(\mathtt{y})$. Hence, $(s,h)\models L$.

case: $L\,=\,\lnot\mathtt{alloc}(\mathtt{x})$:

By definition of $\textit{\small{Atom}}(\mathtt{x}_{i})$,
$\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi$ and therefore
$s(\mathtt{x})\not\in{\rm dom}(h_{1})$. By definition of $\varphi^{\prime}$,
for every $\mathtt{y}\in\mathtt{X}$,
$\mathtt{alloc}(\mathtt{y})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$ implies
$\mathtt{alloc}(\mathtt{y})\subseteq_{\mathsf{Lt}}\varphi$. Therefore,
$s(\mathtt{x})\not\in{\rm dom}(h_{2})$. We conclude that
$s(\mathtt{x})\not\in{\rm dom}(h)$, and so
$(s,h)\models\lnot\mathtt{alloc}(\mathtt{x})$.

case: $L\,=\,\lnot\mathtt{x}\hookrightarrow\mathtt{y}$:

Similar to the previous case. Briefly, by definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$,
$(s,h_{1})\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$. By definition of
$\varphi^{\prime}$,
$(s,h_{2})\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$. So,
$(s,h)\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$.

case: $L\,=\,\mathtt{alloc}(\mathtt{x})$:

If $\mathtt{x}=\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$, then
$s(\mathtt{x})=s(\mathtt{x}_{i})$ (first case of the proof), and by definition
of $\textit{\small{Atom}}(\mathtt{x}_{i})$, $s(\mathtt{x})\in{\rm
dom}(h_{1})$. As $h_{1}{\sqsubseteq}h$, we conclude that
$(s,h)\models\mathtt{alloc}(\mathtt{x})$. Otherwise, if
$\mathtt{x}\neq\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$, then by
definition of $\varphi^{\prime}$ we have
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$. This
implies that $s(\mathtt{x})\in{\rm dom}(h_{2})$ and so, from
$h_{2}{\sqsubseteq}h$, we conclude that
$(s,h)\models\mathtt{alloc}(\mathtt{x})$.

case: $L\,=\,\mathtt{x}\hookrightarrow\mathtt{y}$:

Similar to the previous case. Briefly, if
$\mathtt{x}=\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$ then, by definition
of $\textit{\small{Atom}}(\mathtt{x}_{i})$,
$(s,h_{1})\models\mathtt{x}\hookrightarrow\mathtt{y}$ and so
$(s,h)\models\mathtt{x}\hookrightarrow\mathtt{y}$. Else
(${\mathtt{x}\neq\mathtt{x}_{i}}\subseteq_{\mathsf{Lt}}\varphi$),
$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi^{\prime}$
and therefore $(s,h_{2})\models\mathtt{x}\hookrightarrow\mathtt{y}$. So,
$(s,h)\models\mathtt{x}\hookrightarrow\mathtt{y}$.

case: $L\,=\,\mathtt{size}\geq\beta$:

If $\beta<\max_{\mathtt{size}}(\varphi)$, then directly by definition of
$\varphi^{\prime}$, we have $(s,h_{2})\models\mathtt{size}\geq\beta$. From
$h_{2}{\sqsubseteq}h$, we conclude that $(s,h)\models\mathtt{size}\geq\beta$.
Otherwise, $\beta=\max_{\mathtt{size}}(\varphi)$. Recall that
$\max_{\mathtt{size}}(\varphi)\geq 1$ and so, by definition of
$\varphi^{\prime}$,
$\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)-1\subseteq_{\mathsf{Lt}}\varphi^{\prime}$.
Thus, ${\rm card}({\rm dom}(h_{2}))\geq\max_{\mathtt{size}}(\varphi)-1$. By
definition of $\textit{\small{Atom}}(\mathtt{x}_{i})$ we have ${\rm card}({\rm
dom}(h_{1}))=1$. As $h=h_{1}{+}h_{2}$, we conclude that
$(s,h)\models\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)$.

case: $L\,=\,\lnot\mathtt{size}\geq\beta$:

As $\varphi$ is satisfiable, $\beta>\max_{\mathtt{size}}(\varphi)$. By
definition of the formula $\varphi^{\prime}$,
${\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)\subseteq_{\mathsf{Lt}}\varphi^{\prime}}$
and thus ${\rm card}({\rm dom}(h_{2}))<\max_{\mathtt{size}}(\varphi)$. From
${{\rm card}({\rm dom}(h_{1}))=1}$ we can derive ${\rm card}({\rm
dom}(h))\leq\max_{\mathtt{size}}(\varphi)<\beta$, which allows us to conclude
that ${(s,h)\models\lnot\mathtt{size}\geq\beta}$.

$\begin{array}[]{rll}&\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\sim\mathtt{y}\subseteq_{\mathsf{Lt}}\\{\varphi^{\prime}\mathbin{|}\psi\\}\,\middle|\,{{{\begin{array}[]{r}\sim\in\\{=,\neq\\}\end{array}}}}\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{alloc}(\mathtt{x})\,\middle|\,{{{\begin{array}[]{r}\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}\\\
\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\lnot\mathtt{alloc}(\mathtt{x})\,\middle|\,{{{\begin{array}[]{r}\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\lnot\mathtt{x}{\hookrightarrow}\mathtt{y}\subseteq_{\mathsf{Lt}}\psi\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\hookrightarrow\mathtt{y}\,\middle|\,{{{\begin{array}[]{r}\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}\\\
\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\neq\mathtt{x}\,\middle|\,{{{\begin{array}[]{r}\mathtt{alloc}(\mathtt{x})\land\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi^{\prime}\\\
\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{size}\geq\beta_{2}{+}1{\mathbin{\text{\ooalign{\raise
6.19998pt\hbox{.}\cr$-$\cr}}}}\beta_{1}\,\middle|\,{{{\begin{array}[]{r}\lnot\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi^{\prime}\\\
\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\neq\mathtt{x}\,\middle|\,{{{\begin{array}[]{r}\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi^{\prime}\\\
\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}&\land\bigwedge{\scalebox{0.8}{$\left\\{\lnot\mathtt{size}\geq\beta_{2}{\mathbin{\text{\ooalign{\raise
6.19998pt\hbox{.}\cr$-$\cr}}}}\beta_{1}\,\middle|\,{{{\begin{array}[]{r}\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi^{\prime}\\\
\lnot\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\\\
\land&\bigwedge{\scalebox{0.8}{$\left\\{\mathtt{x}\neq\mathtt{x}\,\middle|\,{{{\begin{array}[]{r}\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}\\\
\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi\end{array}}}}\right\\}$}}\end{array}$
Figure 9. The formula
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$.

  * Proof of C. : .:

Figure 9 recalls the definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$.
First of all, notice that it cannot be that there is $\mathtt{x}\in\mathtt{X}$
such that
$\mathtt{x}\neq\mathtt{x}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$.
Indeed, _ad absurdum_ , suppose the opposite. By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$,
this implies that (1)
$\mathtt{alloc}(\mathtt{x})\land\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi^{\prime}$
and $\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$, (2)
$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi^{\prime}$
and $\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$, or
(3) $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$ and
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$. By definition of
$\varphi^{\prime}$, this implies that (1)
$\mathtt{alloc}(\mathtt{x})\land\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$,
(2) $\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$ or (3)
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$. However, by
definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
this implies that
$\mathtt{x}\neq\mathtt{x}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
in contradiction with the satisfiability of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
Therefore, below we assume that for all $\mathtt{x}\in\mathtt{X}$,
$\mathtt{x}\neq\mathtt{x}\not\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$.

Let
$(s,h)\models{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\ast\textit{\small{Atom}}(\mathtt{x}_{i})$.
There are $h_{1}$ and $h_{2}$ such that $h=h_{1}{+}h_{2}$,
$(s,h_{1})\models{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
and $(s,h_{2})\models\textit{\small{Atom}}(\mathtt{x}_{i})$. By definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$, ${\rm
dom}(h_{2})=\\{s(\mathtt{x}_{i})\\}$. To prove C. : , we show that
$(s,h)\models L$, for every literal
$L\in\mathsf{Lt}({\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi))$.

case: $L\,=\,\mathtt{x}\sim\mathtt{y}$, where $\sim\in\\{=,\neq\\}$:

By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$,
$L\subseteq_{\mathsf{Lt}}\\{\varphi^{\prime}\mathbin{|}\psi\\}$ and so, by
definition of $\varphi^{\prime}$,
$L\subseteq_{\mathsf{Lt}}\\{\varphi\mathbin{|}\psi\\}$. By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$L\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
From
$(s,h_{1})\models{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
we derive $s(\mathtt{x})\sim s(\mathtt{y})$. So, $(s,h)\models L$.

case: $L\,=\,\lnot\mathtt{alloc}(\mathtt{x})$:

From the definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$,
either we have $\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$ or
we have $\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$.
In the first case, by definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
and therefore $s(\mathtt{x})\not\in{\rm dom}(h_{1})$. Moreover, since
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is satisfiable, $\mathtt{alloc}(\mathtt{x})\not\subseteq_{\mathsf{Lt}}\varphi$
(otherwise we would have
$\mathtt{x}\neq\mathtt{x}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$).
Therefore, by definition of $\textit{\small{Atom}}(\mathtt{x}_{i})$, we
conclude that $s(\mathtt{x})\not\in{\rm dom}(h_{2})$. From $h=h_{1}{+}h_{2}$,
we derive $s(\mathtt{x})\not\in{\rm dom}(h)$, and thus
$(s,h)\models\lnot\mathtt{alloc}(\mathtt{x})$.

In the second case,
($\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$), by
definition of $\varphi^{\prime}$ we have
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$ and
$\mathtt{x}\neq\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$. By definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$, $s(\mathtt{x})\not\in{\rm
dom}(h_{2})$. By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
and therefore $s(\mathtt{x})\not\in{\rm dom}(h_{1})$. Again, by
$h=h_{1}{+}h_{2}$, we have $(s,h)\models\lnot\mathtt{alloc}(\mathtt{x})$.

case: $L\,=\,\lnot\mathtt{x}\hookrightarrow\mathtt{y}$:

Following the definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$,
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$ and
therefore
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
Therefore, $(s,h_{1})\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$. Since
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is satisfiable,
$\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi$. By
definition of $\textit{\small{Atom}}(\mathtt{x}_{i})$, we derive
$(s,h_{2})\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$. From
$h=h_{1}{+}h_{2}$, $(s,h)\models\lnot\mathtt{x}\hookrightarrow\mathtt{y}$.

case: $L\,=\,\mathtt{alloc}(\mathtt{x})$:

By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$,
we have
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$ and
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\psi$. First, let us suppose
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$. By definition of
$\varphi^{\prime}$, $\mathtt{x}=\mathtt{x}_{i}\subseteq_{\mathsf{Lt}}\varphi$
and so, by definition of $\textit{\small{Atom}}(\mathtt{x}_{i})$,
$s(\mathtt{x})\in{\rm dom}(h_{2})$. From $h_{2}{\sqsubseteq}h$,
$(s,h)\models\mathtt{alloc}(\mathtt{x})$. Otherwise
($\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$), by
definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
So, $s(\mathtt{x})\in{\rm dom}(h_{1})$, and by $h_{1}{\sqsubseteq}h$,
$(s,h)\models\mathtt{alloc}(\mathtt{x})$.

case: $L\,=\,\mathtt{x}\hookrightarrow\mathtt{y}$:

By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)$,
we have
$\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$ and
${\mathtt{x}\hookrightarrow\mathtt{y}}\subseteq_{\mathsf{Lt}}\psi$. First,
suppose ${\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi}$. By
definition of $\varphi^{\prime}$,
${\mathtt{x}=\mathtt{x}_{i}}\subseteq_{\mathsf{Lt}}\varphi$. By definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$, $s(\mathtt{x})\in{\rm dom}(h_{2})$.
_Ad absurdum_ , suppose $h(s(\mathtt{x}))\neq s(\mathtt{y})$. By definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$, we have that
${\mathtt{alloc}(\mathtt{x})\land\lnot\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\varphi}$.
However, from
$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}\psi$, this implies
$\mathtt{x}\neq\mathtt{x}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
which contradicts the satisfiability of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
Therefore, $h(s(\mathtt{x}))=s(\mathtt{y})$ and, from $h_{2}{\sqsubseteq}h$,
we conclude that $(s,h)\models\mathtt{x}\hookrightarrow\mathtt{y}$. Otherwise
($\lnot\mathtt{alloc}(\mathtt{x})\subseteq_{\mathsf{Lt}}\varphi$), by
definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
$\mathtt{x}\hookrightarrow\mathtt{y}\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
So, $h_{1}(s(\mathtt{x}))=s(\mathtt{y})$, and by $h_{1}{\sqsubseteq}h$, we
derive $(s,h)\models\mathtt{x}\hookrightarrow\mathtt{y}$.

case: $L\,=\,\mathtt{size}\geq\beta_{2}{+}1\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\beta_{1}$, where
$\lnot\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi^{\prime}$ and
$\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi$ :

By definition of $\varphi^{\prime}$,
$\lnot\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi$, and so
$\beta_{1}>\max_{\mathtt{size}}(\varphi)$, since $\varphi$ is satisfiable. By
definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
and as
$\lnot\mathtt{size}\geq\max_{\mathtt{size}}(\varphi)+1\subseteq_{\mathsf{Lt}}\varphi$,
we have $\mathtt{size}\geq\beta_{2}+1\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}(\max_{\mathtt{size}}(\varphi)+1)\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
which in turn implies ${\rm card}({\rm
dom}(h_{1}))\geq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\max_{\mathtt{size}}(\varphi)$. By definition of
$\textit{\small{Atom}}(\mathtt{x}_{i})$, ${{\rm card}({\rm dom}(h_{2}))\geq
1}$. By ${h=h_{1}{+}h_{2}}$, ${\rm card}({\rm
dom}(h))\geq(\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\max_{\mathtt{size}}(\varphi))+1\geq(\beta_{2}+1)\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\max_{\mathtt{size}}(\varphi)$. As
$\beta_{1}>\max_{\mathtt{size}}(\varphi)$,
$(s,h)\models\mathtt{size}\geq\beta_{2}{+}1\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\beta_{1}$.

case: $L\,=\,\lnot\mathtt{size}\geq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\beta_{1}$, where
$\mathtt{size}\geq\beta_{1}\subseteq_{\mathsf{Lt}}\varphi^{\prime}$ and
$\lnot\mathtt{size}\geq\beta_{2}\subseteq_{\mathsf{Lt}}\psi$ :

By definition of $\varphi^{\prime}$,
$\beta_{1}<\max_{\mathtt{size}}(\varphi)$. By definition of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$,
we have $\lnot\mathtt{size}\geq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\max_{\mathtt{size}}(\varphi)\subseteq_{\mathsf{Lt}}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$.
Notice that, since
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)$
is satisfiable, $\beta_{2}>\max_{\mathtt{size}}(\varphi)$. Thus, ${\rm
card}({\rm dom}(h_{1}))<\beta_{2}-\max_{\mathtt{size}}(\varphi)$. By
definition of $\textit{\small{Atom}}(\mathtt{x}_{i})$, ${\rm card}({\rm
dom}(h_{2}))\leq 1$. From $h=h_{1}{+}h_{2}$, we conclude that ${\rm card}({\rm
dom}(h))<(\beta_{2}-\max_{\mathtt{size}}(\varphi))+1$. As
$\beta_{1}<\max_{\mathtt{size}}(\varphi)$, we have
${\beta_{2}-\max_{\mathtt{size}}(\varphi)+1}\leq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\beta_{1}$. Therefore,
$(s,h)\models\lnot\mathtt{size}\geq\beta_{2}\mathbin{\text{\ooalign{\raise
4.30554pt\hbox{.}\cr$-$\cr}}}\beta_{1}$.

Continuing the proof of Lemma 13, we prove
${\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)}$.
Notice that, by the completeness of $\mathcal{H}_{\mathsf{C}}(\ast)$ (Theorem
11), we conclude that the tautologies in B. :  and C. :  are derivable in
$\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})$. Moreover, notice
that
$\lnot\mathtt{alloc}(\mathtt{x}_{i})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$
and, for every $\mathtt{y}\in\mathtt{X}$,
$\lnot\mathtt{alloc}(\mathtt{y})\subseteq_{\mathsf{Lt}}\varphi$ implies
$\lnot\mathtt{alloc}(\mathtt{y})\subseteq_{\mathsf{Lt}}\varphi^{\prime}$. This
allows us to rely on the induction hypothesis, and conclude that
$\vdash_{\mathcal{H}_{\mathsf{C}}(\ast,\mathbin{-\mkern-6.0mu*})}{\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)\Rightarrow(\varphi^{\prime}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$.
The derivation of
${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi,\psi)\Rightarrow(\varphi\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$
is given below:

$1$ | ${\langle\mbox{$\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}$}\rangle}(\varphi^{\prime},\psi)\Rightarrow(\varphi^{\prime}\mathbin{{-\mkern-8.0mu{\raisebox{0.6pt}{$\scriptstyle{\circledast}$}}}}\top)$ | Induction hypothesis
---|---|---
$2$ | $\textit{\small{Atom}}(\mathtt{x}_{i})\ast\varphi^{\prime}\Rightarrow\varphi$ | B. : , Theorem 11