n\\}]\,\varphi$ $\displaystyle=[\mathit{R}]\,[n/\mathit{y}]\varphi$
$\displaystyle[\mathit{R}\\{\mathit{y}\mapsto\mathit{a}\\}]\,\varphi$
$\displaystyle=[\mathit{R}]\,\varphi$
$\displaystyle\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)$
$\displaystyle=\Sigma_{\mathit{x}\in\mathit{dom}(\Gamma)}\,\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{x}),\Gamma(\mathit{x}))$
$\displaystyle\mathbf{own}\,(\mathit{H},\mathit{v},\tau)$
$\displaystyle=\begin{cases}\\{\mathit{a}\mapsto
r\\}+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{a}),\tau^{\prime})&\mathit{v}\,=\,\mathit{a}\wedge\mathit{a}\in\mathit{dom}(\mathit{H})\wedge\tau=\tau^{\prime}\operatorname{\mathbf{ref}}^{r}\\\
\emptyset&o.w.\end{cases}$

Figure 12: Machine state typing

##  Appendix 0.A Proof of Type Soundness (Theorem 3.1)

We first define a typing relation for machine configurations
$\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{e}}\right\rangle$ as shown
in Figure 12. The critical component of this typing relation is the
consistency relation $\mathbf{Cons}$. Intuitively, $\mathbf{Cons}$ expresses
that the current heap and registers are consistent with the ownership and
refinement information implied by $\Gamma$. We say triple
$(\mathit{H},\mathit{R},\Gamma)$ is _consistent_ , and write
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$. In the definitions for
$\mathbf{own}$ we write $\\{\mathit{a}\mapsto r\\}$ to denote a function
$\textbf{Addr}\rightarrow[0,1]$ which returns $r$ for $\mathit{a}$, and $0$
otherwise. We write $\emptyset$ to denote a constant function
$\textbf{Addr}\rightarrow[0,1]$ which always returns $0$. We define the
addition between two functions
$\mathit{O_{{\mathrm{1}}}},\mathit{O_{{\mathrm{2}}}}:\textbf{Addr}\rightarrow[0,1]$
as:
$(\mathit{O_{{\mathrm{1}}}}+\mathit{O_{{\mathrm{2}}}})(\mathit{a})=\mathit{O_{{\mathrm{1}}}}(\mathit{a})+\mathit{O_{{\mathrm{2}}}}(\mathit{a})$.
Finally, if a summation $\Sigma$ has no summands, we take its result to be
$\emptyset$.

The proof of Theorem 3.1 requires the following four key lemmas. These lemmas
are stated with respect to some well-typed program
$\left\langle{\mathit{D},\mathit{e}}\right\rangle$, i.e.
$\vdash\left\langle{\mathit{D},\mathit{e}}\right\rangle$.

###### Lemma 1

$\vdash_{\mathit{conf}}^{D}\left\langle{\emptyset,\emptyset,\cdot,\mathit{e}}\right\rangle$

###### Proof

Trivial, taking $\Gamma=\bullet$ and by inversion on
$\vdash\left\langle{\mathit{D},\mathit{e}}\right\rangle$.

###### Lemma 2

$\vdash_{\mathit{conf}}^{D}\mathbf{C}$ implies
$\mathbf{C}\neq\mathbf{AssertFail}$

###### Proof

Simple proof by contradiction, as the $\mathbf{AssertFail}$ is not well-typed.

###### Lemma 3

If
$\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{e}}\right\rangle$
and
$\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{e}}\right\rangle\longrightarrow_{\mathit{D}}\mathbf{C}$,
then $\vdash_{\mathit{conf}}^{D}\mathbf{C}$

###### Lemma 4

If $\vdash_{\mathit{conf}}^{D}\mathbf{C}$, then, one of the following
conditions hold:

  1. 1.

$\exists\mathbf{C}^{\prime},\mathbf{C}\longrightarrow_{\mathit{D}}\mathbf{C}^{\prime}$,
or

  2. 2.

$\mathbf{C}=\mathbf{AssertFail}$, or

  3. 3.

$\mathbf{C}=\left\langle{\mathit{H},\mathit{R},\cdot,\mathit{x}}\right\rangle$

Lemmas 3 and 4 are the heart of proof effort, we give their proofs in
Appendices 0.C and 0.D respectively.

We can now prove Theorem 3.1:

######  Proof (Theorem 3.1: Soundness)

From Lemmas 1 and 3 and an inductive argument, any configuration reachable
from the initial state must be well-typed. Then, by Lemma 2 every
configuration reachable from the initial state cannot be
$\mathbf{AssertFail}$, i.e., a well-typed program never experiences an
assertion failure. This completes the first part of the proof.

To prove the second portion of the theorem, it suffices to show that any
configuration reachable from the initial state can step or is a final
configuration. Again from Lemmas 1 and 3 and a simple inductive argument, we
must have that for any state $\mathbf{C}$ such that
$\left\langle{\emptyset,\emptyset,\cdot,\mathit{e}}\right\rangle\longrightarrow^{*}_{\mathit{D}}\mathbf{C}$
$\vdash_{\mathit{conf}}^{D}\mathbf{C}$. Then by Lemma 4 we have the
configuration may step or is one of the final configurations.

The remainder of this appendix proves Lemmas 3 and 4. We introduce some
auxiliary definitions and lemmas in Appendix 0.B, give the proof of Lemma 3 in
Appendix 0.C, and prove Lemma 4 in Appendix 0.D.

##  Appendix 0.B Auxiliary Lemmas and Definitions

$\begin{array}[]{r}\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall\,\mathit{x}\in\mathit{dom}(\Gamma).\mathcal{L}\mid\Gamma\vdash_{\mathit{WF}}\Gamma(\mathit{x})\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{L}\vdash_{\mathit{WF}}\Gamma\end{array}}\\\
\text{(\hbox{\sc WF-Env})}\end{array}$
$\begin{array}[]{r}\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{L}\mid\Gamma\vdash_{\mathit{WF}}\varphi\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{L}\mid\Gamma\vdash_{\mathit{WF}}\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}\end{array}}\\\
\text{(\hbox{\sc WF-Int})}\end{array}$
$\begin{array}[]{r}\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{L}\mid\Gamma\vdash_{\mathit{WF}}\tau\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{L}\mid\Gamma\vdash_{\mathit{WF}}\tau\operatorname{\mathbf{ref}}^{r}\end{array}}\\\
\text{(\hbox{\sc WF-Ref})}\end{array}$
$\begin{array}[]{r}\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall\,\mathit{x}\in\mathbf{FPV}\,(\varphi)\setminus\left\\{{\nu}\right\\}.\Gamma(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\\_}\right\\}\\\
\mathbf{FCV}\,(\varphi)\subseteq\mathbf{CV}\,(\mathcal{L})\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{L}\mid\Gamma\vdash_{\mathit{WF}}\varphi\end{array}}\\\
\text{(\hbox{\sc WF-Phi})}\end{array}$
$\begin{array}[]{r}\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{L}\mid\Gamma\vdash_{\mathit{WF}}\tau\quad\quad\mathcal{L}\vdash_{\mathit{WF}}\Gamma\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{L}\vdash_{\mathit{WF}}\tau\operatorname{\Rightarrow}\Gamma\end{array}}\\\
\text{(\hbox{\sc WF-Result})}\end{array}$
$\begin{array}[]{r}\displaystyle\frac{\begin{array}[]{@{}c@{}}\lambda\vdash_{\mathit{WF}}\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau_{{\mathrm{1}}},\ldots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau_{\mathit{n}}\\\
\lambda\vdash_{\mathit{WF}}\tau\operatorname{\Rightarrow}\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau^{\prime}_{{\mathrm{1}}},\ldots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau^{\prime}_{\mathit{n}}\end{array}}{\begin{array}[]{@{}c@{}}\vdash_{\mathit{WF}}\forall\lambda.\left\langle{\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau_{{\mathrm{1}}},\dots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau_{\mathit{n}}}\right\rangle\operatorname{\rightarrow}\left\langle{\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau^{\prime}_{{\mathrm{1}}},\dots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau^{\prime}_{\mathit{n}}\mid\tau}\right\rangle\end{array}}\\\
\text{(\hbox{\sc WF-FunType})}\end{array}$
$\begin{array}[]{r}\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall\,\mathit{f}\in\mathit{dom}(\Theta).\vdash_{\mathit{WF}}\Theta(\mathit{f})\end{array}}{\begin{array}[]{@{}c@{}}\vdash_{\mathit{WF}}\Theta\end{array}}\\\
\text{(\hbox{\sc WF-FunEnv})}\end{array}$

$\begin{array}[]{rrl}\text{Free Ctxt
Vars}&\mathbf{FCV}\,(\varphi_{{\mathrm{1}}}\vee\varphi_{{\mathrm{2}}})&=\mathbf{FCV}\,(\varphi_{{\mathrm{1}}})\cup\mathbf{FCV}\,(\varphi_{{\mathrm{2}}})\\\
&\mathbf{FCV}\,(\neg\varphi)&=\mathbf{FCV}\,(\varphi)\\\
&\mathbf{FCV}\,(\widehat{v}_{{\mathrm{1}}}\,=\,\widehat{v}_{{\mathrm{2}}})&=\mathbf{FCV}\,(\phi(\widehat{v}_{{\mathrm{1}}},\,..\,,\widehat{v}_{\mathit{n}}))=\emptyset\\\
&\mathbf{FCV}\,(\vec{\ell}\preceq\mathcal{C})&=\mathbf{FCV}\,(\mathcal{C})\\\
&\mathbf{FCV}\,(\ell:\mathcal{C})&=\mathbf{FCV}\,(\mathcal{C})\\\
&\mathbf{FCV}\,(\mathcal{L})&=\mathbf{CV}\,(\mathcal{L})\\\ \text{Ctxt
Vars}&\mathbf{CV}\,(\vec{\ell})&=\emptyset\\\
&\mathbf{CV}\,(\lambda)&=\left\\{{\lambda}\right\\}\end{array}$

Figure 13: Well-formedness of types and environments.

The well-formedness rules omitted from the main paper are found in Figure 13.
We write $\mathcal{L}\vdash_{\mathit{WF}}\tau\operatorname{\Rightarrow}\Gamma$
as shorthand for $\mathcal{L}\vdash_{\mathit{WF}}\Gamma$ and
$\mathcal{L}\mid\Gamma\vdash_{\mathit{WF}}\tau$.

We first prove that the subtyping relations are transitive.

###### Lemma 5

  1. 1.

If $\Gamma\leq\Gamma^{\prime}$ then
$\models\left\llbracket{\Gamma}\right\rrbracket\implies\left\llbracket{\Gamma^{\prime}}\right\rrbracket$.

  2. 2.

If $\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$ and
$\Gamma\vdash\tau_{{\mathrm{2}}}\leq\tau_{{\mathrm{3}}}$, then
$\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{3}}}$

  3. 3.

If $\Gamma\leq\Gamma^{\prime}$ and
$\Gamma^{\prime}\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$, then
$\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$

  4. 4.

If $\Gamma\leq\Gamma^{\prime}$,
$\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$, and
$\Gamma^{\prime}\vdash\tau_{{\mathrm{2}}}\leq\tau_{{\mathrm{3}}}$, then
$\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{3}}}$.

  5. 5.

If $\Gamma\leq\Gamma^{\prime}$ and $\Gamma^{\prime}\leq\Gamma^{\prime\prime}$,
then $\Gamma\leq\Gamma^{\prime\prime}$.

###### Proof

  1. 1.

It suffices to show that
$\models\left\llbracket{\Gamma}\right\rrbracket\implies[\mathit{x}/\,\nu\,]\,\varphi^{\prime}$
for any $\mathit{x}\in\mathit{dom}(\Gamma^{\prime})$ where
$\Gamma^{\prime}(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi^{\prime}}\right\\}$.
From $\Gamma\leq\Gamma^{\prime}$ we have
$\models\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi\implies\varphi^{\prime}$
where
$\Gamma(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}$.
We must then have
$\models\left\llbracket{\Gamma}\right\rrbracket\wedge[\mathit{x}/\,\nu\,]\,\varphi\implies[\mathit{x}/\,\nu\,]\,\varphi^{\prime}$.
From the definition of $\left\llbracket{\Gamma}\right\rrbracket$ we have
$\left\llbracket{\Gamma}\right\rrbracket\wedge[\mathit{x}/\,\nu\,]\,\varphi\iff\left\llbracket{\Gamma}\right\rrbracket$,
giving the desired result.

  2. 2.

By induction on $\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$. We
only consider the base case where
$\tau_{{\mathrm{1}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{1}}}}\right\\}$
and
$\tau_{{\mathrm{2}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{2}}}}\right\\}$,
the case for reference types follows from the induction hypothesis. By further
inversion on $\Gamma\vdash\tau_{{\mathrm{2}}}\leq\tau_{{\mathrm{3}}}$ we
therefore have:

τ_3 = {ν:int∣φ_3 }⊧⟦ Γ⟧ ∧φ_1 ⟹φ_2 ⊧⟦ Γ⟧ ∧φ_2 ⟹φ_3

From which it is immediate that we must have
$\models\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{3}}}$,
whereby S-Int gives $\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{3}}}$.

  3. 3.

By induction on
$\Gamma^{\prime}\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$. The case
for reference types is immediate from the inductive hypothesis, we focus on
the base case where
$\tau_{{\mathrm{1}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{1}}}}\right\\}$
and
$\tau_{{\mathrm{2}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{2}}}}\right\\}$,
and where
$\models\left\llbracket{\Gamma^{\prime}}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}$.
From $\Gamma\leq\Gamma^{\prime}$ and Item 1 above, we have
$\models\left\llbracket{\Gamma}\right\rrbracket\implies\left\llbracket{\Gamma^{\prime}}\right\rrbracket$
from which we can derive
$\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}$,
i.e., $\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$.

  4. 4.

Immediate from Items 2 and 3.

  5. 5.

Immediate corollary of Item 4.

###### Definition 1

A value $v$ reaches an integer with $n$ dereferences in heap $\mathit{H}$ when
it is in the relation $\mathit{H}\vdash v\Downarrow n$ defined as the smallest
relation closed under the following rules:

  1. 1.

If $v\in\mathbb{Z}$ then $\mathit{H}\vdash v\Downarrow 0$

  2. 2.

If $\mathit{H}\vdash v\Downarrow n$ and $\mathit{H}(\mathit{a})\,=\,v$ then
$\mathit{H}\vdash\mathit{a}\Downarrow n+1$

We will write $\mathit{H}\vdash v\Downarrow|\tau|$ to indicate a value $v$ is
shape consistent with $\tau$ in heap $\mathit{H}$, where $|\tau|$ is the
number of reference constructors in the type $\tau$.

We also prove a standard inversion lemma to handle the fact our typing rules
are not syntax directed.

######  Lemma 6 (Inversion)

If
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{e_{{\mathrm{0}}}}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$,
then there exists some $\Gamma_{\mathit{p}}$, $\tau_{\mathit{p}}$, and
$\Gamma^{\prime}_{\mathit{p}}$ such that $\Gamma\leq\Gamma_{\mathit{p}}$,
$\vec{\ell}\vdash_{\mathit{WF}}\Gamma_{\mathit{p}}$,
$\Gamma^{\prime}_{\mathit{p}},\tau_{\mathit{p}}\leq\Gamma^{\prime},\tau$, and:

  1. 1.

If $\mathit{e_{{\mathrm{0}}}}=\mathit{x}$ then
$\Gamma_{\mathit{p}}(\mathit{x})=\tau_{\mathit{p}}+\tau^{\prime}$,
$\Gamma^{\prime}_{\mathit{p}}=\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\tau^{\prime}]$.

  2. 2.

If
$\mathit{e_{{\mathrm{0}}}}=\operatorname{\mathbf{let}}\mathit{x}=\mathit{y}\operatorname{\mathbf{in}}\mathit{e}$,
then
$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}[\mathit{y}\hookleftarrow\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{1}}}}\mathit{x}],\mathit{x}:(\tau_{{\mathrm{2}}}\wedge_{\mathit{x}}\mathit{x}=_{\tau_{{\mathrm{2}}}}\mathit{y})\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$
and $\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime}_{\mathit{p}})$ where
$\Gamma_{\mathit{p}}(\mathit{y})=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$.

  3. 3.

If
$\mathit{e_{{\mathrm{0}}}}=\operatorname{\mathbf{let}}\mathit{x}=n\operatorname{\mathbf{in}}\mathit{e}$
then
$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}},\mathit{x}:\left\\{{\nu\operatorname{:}\mathbf{int}\mid\nu\,=\,n}\right\\}\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$
and $\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime}_{\mathit{p}})$.

  4. 4.

If
$\mathit{e_{{\mathrm{0}}}}=\operatorname{\mathbf{ifz}}\mathit{x}\operatorname{\mathbf{then}}\mathit{e_{{\mathrm{1}}}}\operatorname{\mathbf{else}}\mathit{e_{{\mathrm{2}}}}$
then:

     * •

$\Gamma_{\mathit{p}}(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}$

     * •

$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi\wedge\nu\,=\,0}\right\\}]\vdash\mathit{e_{{\mathrm{1}}}}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

     * •

$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi\wedge\nu\,\neq\,0}\right\\}]\vdash\mathit{e_{{\mathrm{2}}}}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

  5. 5.

If
$\mathit{e_{{\mathrm{0}}}}=\operatorname{\mathbf{let}}\mathit{x}=\operatorname{\mathbf{mkref}}\mathit{y}\operatorname{\mathbf{in}}\mathit{e}$,
then
$\Gamma_{\mathit{p}}(\mathit{y})=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$,
$\Theta\mid\mathcal{L}\mid\Gamma[\mathit{y}\hookleftarrow\tau_{{\mathrm{1}}}],\mathit{x}:(\tau_{{\mathrm{2}}}\wedge_{\mathit{x}}\mathit{x}=_{\tau_{{\mathrm{2}}}}\mathit{y})\operatorname{\mathbf{ref}}^{1}\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$,
and $\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime}_{\mathit{p}})$

  6. 6.

If
$\mathit{e_{{\mathrm{0}}}}=\operatorname{\mathbf{let}}\mathit{x}=*\mathit{y}\operatorname{\mathbf{in}}\mathit{e}$,
then:

     * •

$\Gamma_{\mathit{p}}(\mathit{y})=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r}$

     * •

$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}[\mathit{y}\hookleftarrow\tau^{\prime\prime}\operatorname{\mathbf{ref}}^{r}],\mathit{x}:\tau_{{\mathrm{2}}}\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

     * •

$\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime}_{\mathit{p}})$

     * •

$\tau^{\prime\prime}=\begin{cases}(\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{1}}}}\mathit{x})&r>0\\\
\tau_{{\mathrm{1}}}&r=0\end{cases}$

  7. 7.

If
$\mathit{e_{{\mathrm{0}}}}=\operatorname{\mathbf{let}}\mathit{x}=\mathit{f}^{\ell}(\mathit{y_{{\mathrm{1}}}},\ldots,\mathit{y_{\mathit{n}}})\operatorname{\mathbf{in}}\mathit{e}$
then:

     * •

$\Gamma_{\mathit{p}}(\mathit{y_{\mathit{i}}})=\sigma_{\alpha}\,\sigma_{x}\,\tau_{\mathit{i}}$
for each $i\in\left\\{{1,\ldots,n}\right\\}$

     * •

$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}[\mathit{y_{\mathit{i}}}\hookleftarrow\sigma_{\alpha}\,\sigma_{x}\,\tau^{\prime}_{\mathit{i}}],\mathit{x}:\sigma_{\alpha}\,\sigma_{x}\,\tau\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

     * •

$\Theta(\mathit{f})=\forall\lambda.\left\langle{\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau_{{\mathrm{1}}},\dots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau_{\mathit{n}}}\right\rangle\operatorname{\rightarrow}\left\langle{\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau^{\prime}_{{\mathrm{1}}},\dots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau^{\prime}_{\mathit{n}}\mid\tau}\right\rangle$

     * •

$\sigma_{\alpha}=[\ell:\mathcal{L}/\lambda]$

     * •

$\sigma_{x}=[\mathit{y_{{\mathrm{1}}}}/\mathit{x_{{\mathrm{1}}}}]\cdots[\mathit{y_{\mathit{n}}}/\mathit{x_{\mathit{n}}}]$

     * •

$\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime}_{\mathit{p}})$

  8. 8.

If
$\mathit{e_{{\mathrm{0}}}}=\mathit{y}\operatorname{:=}\mathit{x}\operatorname{;}\mathit{e}$
then:

     * •

$\Gamma_{\mathit{p}}(\mathit{x})=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$

     * •

$\Gamma_{\mathit{p}}(\mathit{y})=\tau^{\prime}\operatorname{\mathbf{ref}}^{1}$

     * •

$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\tau_{{\mathrm{1}}}][\mathit{y}\hookleftarrow(\tau_{{\mathrm{2}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{2}}}}\mathit{x})\operatorname{\mathbf{ref}}^{1}]\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

     * •

The shapes of $\tau^{\prime}$ and $\tau_{{\mathrm{2}}}$ are similar, i.e,
$|\tau^{\prime}|\,=\,|\tau_{{\mathrm{2}}}|$.

  9. 9.

If
$\mathit{e_{{\mathrm{0}}}}=\mathbf{alias}(\mathit{x}=\mathit{y})\operatorname{;}\mathit{e}$
then there exist some
$\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}},\tau^{\prime}_{{\mathrm{1}}},\tau^{\prime}_{{\mathrm{2}}},r_{{\mathrm{1}}},r_{{\mathrm{2}}},r^{\prime}_{{\mathrm{1}}},r^{\prime}_{{\mathrm{2}}}$
such that:

     * •

$\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}+\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}\approx\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}+\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}}$

     * •

$\Gamma_{\mathit{p}}(\mathit{x})=\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}$
and
$\Gamma_{\mathit{p}}(\mathit{y})=\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}$

     * •

$\Theta\mid\mathcal{L}\mid\Gamma[\mathit{x}\hookleftarrow\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}][\mathit{y}\hookleftarrow\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}}]\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

  10. 10.

If
$\mathit{e_{{\mathrm{0}}}}=\mathbf{alias}(\mathit{x}=*\mathit{y})\operatorname{;}\mathit{e}$
then there exist some
$\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}},\tau^{\prime}_{{\mathrm{1}}},\tau^{\prime}_{{\mathrm{2}}},r_{{\mathrm{1}}},r_{{\mathrm{2}}},r^{\prime}_{{\mathrm{1}}},r^{\prime}_{{\mathrm{2}}},r$,
such that:

     * •

$\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}+\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}\approx\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}+\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}}$

     * •

$\Gamma_{\mathit{p}}(\mathit{x})=\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}$
and
$\Gamma_{\mathit{p}}(\mathit{y})=(\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}})\operatorname{\mathbf{ref}}^{r}$

     * •

$\Theta\mid\mathcal{L}\mid\Gamma[\mathit{x}\hookleftarrow\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}][\mathit{y}\hookleftarrow(\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}})\operatorname{\mathbf{ref}}^{r}]\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

  11. 11.

If
$\mathit{e_{{\mathrm{0}}}}=\mathit{e_{{\mathrm{1}}}}\operatorname{;}\mathit{e_{{\mathrm{2}}}}$
then
$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}\vdash\mathit{e_{{\mathrm{1}}}}:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}$
and
$\Theta\mid\mathcal{L}\mid\Gamma_{{\mathrm{1}}}\vdash\mathit{e_{{\mathrm{2}}}}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

  12. 12.

If $\mathit{e_{{\mathrm{0}}}}=\mathit{x}\operatorname{;}\mathit{e^{\prime}}$
then
$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}[\mathit{x}:\tau^{\prime}+\tau_{{\mathrm{0}}}]\vdash\mathit{x}:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\tau_{{\mathrm{0}}}]$
and
$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\tau_{{\mathrm{0}}}]\vdash\mathit{e^{\prime}}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

  13. 13.

If
$\mathit{e_{{\mathrm{0}}}}=\mathbf{assert}(\varphi)\operatorname{;}\mathit{e}$
then $\Gamma_{\mathit{p}}\models\varphi$ and
$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

###### Proof

By straightforward induction on the typing relation and the transitivity of
the subtyping relation Lemma 5.

The only case of note is the case for
$\mathit{e_{{\mathrm{0}}}}=\mathit{x}\operatorname{;}\mathit{e_{{\mathrm{2}}}}$.
If the subderivation for $\mathit{x}$ has applications of T-Sub then the
subtypings on the output environment can be pushed into application subtyping
on input environments when typing $\mathit{e^{\prime}}$. Similarly, any input
subtypings on the input environment of the derivation of $\mathit{x}$ can be
pushed into T-Sub rules such that
$\Gamma\leq\Gamma_{\mathit{p}}[\mathit{x}:\tau^{\prime}+\tau_{{\mathrm{0}}}]$.

Lemmas 7 and 8 prove some standard properties of execution contexts: any
decomposition of a well-typed expression into a execution context and redex
can be well-typed, and substituting a well-typed expression matching a
context’s hole type yields a well-typed expression

###### Lemma 7

For any $\mathit{E}$ and $\mathit{e^{\prime}}$ such that
$\mathit{E}[\mathit{e^{\prime}}]=\mathit{e}$ where
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
there exists some $\tau_{{\mathrm{0}}}$, $\Gamma_{{\mathrm{0}}}$ such that
$\Theta\mid[]:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{0}}}\mid\mathcal{L}\vdash_{\mathit{ectx}}\mathit{E}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
and
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{e^{\prime}}:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{0}}}$.

###### Proof

By induction on the structure of $\mathit{E}$.

Case $\mathit{E}=[]$:
Trivial, by taking $\tau_{{\mathrm{0}}}=\tau$ and
$\Gamma_{{\mathrm{0}}}=\Gamma^{\prime}$.

Case
$\mathit{E}=\mathit{E^{\prime}}\operatorname{;}\mathit{e^{\prime\prime}}$:
Then
$\mathit{E}[\mathit{e^{\prime}}]=\mathit{E^{\prime}}[\mathit{e^{\prime}}]\operatorname{;}\mathit{e^{\prime\prime}}=\mathit{e}$.
By Lemma 6 we have

$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}\vdash\mathit{E^{\prime}}[\mathit{e^{\prime}}]:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}&\Theta\mid\mathcal{L}\mid\Gamma_{{\mathrm{1}}}\vdash\mathit{e^{\prime\prime}}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}\\\
\Gamma\leq\Gamma_{\mathit{p}}&\Gamma^{\prime}_{\mathit{p}},\tau_{\mathit{p}}\leq\Gamma^{\prime},\tau\end{array}$

for some $\Gamma_{\mathit{p}}$, $\Gamma^{\prime}_{\mathit{p}}$, and
$\tau_{\mathit{p}}$.

By the induction hypothesis we then have
$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}\vdash\mathit{e^{\prime}}:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{0}}}$
and
$\Theta\mid[]:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{0}}}\mid\mathcal{L}\vdash_{\mathit{ectx}}\mathit{E^{\prime}}:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}$.
for some $\tau_{{\mathrm{0}}}$ and $\Gamma_{{\mathrm{0}}}$.

Next, as
$\Gamma^{\prime}_{\mathit{p}},\tau_{\mathit{p}}\leq\Gamma^{\prime},\tau$ by an
application of T-Sub, we have
$\Theta\mid\mathcal{L}\mid\Gamma_{{\mathrm{1}}}\vdash\mathit{e^{\prime\prime}}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$.
By TE-Seq, we therefore have:
$\Theta\mid[]:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{0}}}\mid\mathcal{L}\vdash_{\mathit{ectx}}\mathit{E^{\prime}}\operatorname{;}\mathit{e^{\prime\prime}}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$.

Finally, from $\Gamma\leq\Gamma_{\mathit{p}}$ and
$\Theta\mid\mathcal{L}\mid\Gamma_{\mathit{p}}\vdash\mathit{e^{\prime}}:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{0}}}$,
and application of T-Sub, we have
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{e^{\prime}}:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{0}}}$.

###### Lemma 8

If
$\Theta\mid[]:\tau\operatorname{\Rightarrow}\Gamma^{\prime}\mid\mathcal{L}\vdash_{\mathit{ectx}}\mathit{E}:\tau^{\prime\prime}\operatorname{\Rightarrow}\Gamma^{\prime\prime}$
and
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
for some $\Gamma$, then
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{E}[\mathit{e}]:\tau^{\prime\prime}\operatorname{\Rightarrow}\Gamma^{\prime\prime}$.

###### Proof

By induction on the typing derivation of $\mathit{E}$.

Case TE-Seq:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathit{E}=\mathit{E^{\prime}}\operatorname{;}\mathit{e^{\prime}}\\\
\mathit{E}[\mathit{e}]=\mathit{E^{\prime}}[\mathit{e}]\operatorname{;}\mathit{e^{\prime}}\\\
\Theta\mid[]:\tau\operatorname{\Rightarrow}\Gamma^{\prime}\mid\mathcal{L}\vdash_{\mathit{ectx}}\mathit{E^{\prime}}:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{0}}}\\\
\Theta\mid\mathcal{L}\mid\Gamma_{{\mathrm{0}}}\vdash\mathit{e^{\prime}}:\tau^{\prime\prime}\operatorname{\Rightarrow}\Gamma^{\prime\prime}\\\
\end{array}$
By the induction hypothesis we have
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{E^{\prime}}[\mathit{e}]:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{0}}}$.
We then have our result via an application of T-Seq.

Case TE-Hole:
Trivial, as $\tau=\tau^{\prime\prime}$ and
$\Gamma^{\prime}=\Gamma^{\prime\prime}$ and
$\mathit{E}[\mathit{e}]=\mathit{e}$.

######  Lemma 9 (Context Variable Substitution)

  1. 1.

If $\tau_{{\mathrm{3}}}=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$ then
$[\mathcal{L}/\lambda]\,\tau_{{\mathrm{3}}}=[\mathcal{L}/\lambda]\,\tau_{{\mathrm{1}}}+[\mathcal{L}/\lambda]\,\tau_{{\mathrm{2}}}$

  2. 2.

For any $\vec{\ell}$:

    1. (a)

If $\lambda\vdash_{\mathit{WF}}\Gamma$ then
$\vec{\ell}\vdash_{\mathit{WF}}[\vec{\ell}/\lambda]\Gamma$

    2. (b)

If $\lambda\mid\Gamma\vdash_{\mathit{WF}}\tau$ then
$\vec{\ell}\mid[\vec{\ell}/\lambda]\Gamma\vdash_{\mathit{WF}}[\vec{\ell}/\lambda]\,\tau$

    3. (c)

If $\lambda\vdash_{\mathit{WF}}\tau\operatorname{\Rightarrow}\Gamma$ then
$\vec{\ell}\vdash_{\mathit{WF}}[\vec{\ell}/\lambda]\,\tau\operatorname{\Rightarrow}[\vec{\ell}/\lambda]\Gamma$

  3. 3.

For any $\Gamma$, $\tau_{{\mathrm{1}}}$, $\tau_{{\mathrm{2}}}$, $\lambda$ and
$\vec{\ell}$, If $\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$,
then
$[\vec{\ell}/\lambda]\Gamma\vdash[\vec{\ell}/\lambda]\,\tau_{{\mathrm{1}}}\leq[\vec{\ell}/\lambda]\,\tau_{{\mathrm{2}}}$

  4. 4.

If $\Gamma\models\varphi$ where $\lambda\not\in\mathbf{FCV}\,(\varphi)$ then
$[\vec{\ell}/\lambda]\Gamma\models\varphi$

  5. 5.

If
$\Theta\mid\lambda\mid\Gamma\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
then
$\Theta\mid\vec{\ell}\mid[\vec{\ell}/\lambda]\Gamma\vdash\mathit{e}:[\vec{\ell}/\lambda]\,\tau\operatorname{\Rightarrow}[\vec{\ell}/\lambda]\Gamma^{\prime}$

###### Proof

  1. 1.

By straightforward induction on the definition of
$\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}=\tau_{{\mathrm{3}}}$.

  2. 2.

Observe that any substitution of context variables cannot change simple types
within $\Gamma$ and thus all types and refinements remain well-formed with
respect to integer variables in $\Gamma$. It thus suffices to show that
$\mathbf{FCV}\,([\vec{\ell}/\lambda]\,\varphi)\subseteq\mathbf{CV}\,(\vec{\ell})=\emptyset$
for any refinement $\varphi$ appearing in $\tau$ or a type in $\Gamma$. By the
assumed well-formedness of $\tau$ with respect to context variable $\lambda$
(resp. $\Gamma$), after substitution all free context variables in $\tau$
(resp. the types in $\Gamma$) will be replaced with $\vec{\ell}$. Thus, post-
substitution no free context variables appear in the refinement of
$[\vec{\ell}/\lambda]\,\tau$ (resp. refinements of types in
$[\vec{\ell}/\lambda]\Gamma$), trivially satisfying our requirements.

  3. 3.

If $\lambda$ does not appear free in $\tau_{{\mathrm{1}}}$,
$\tau_{{\mathrm{2}}}$ or $\Gamma$, then the result trivially holds. Let us
then assume $\lambda$ appears free. We prove the result by induction on the
subtyping derivation.

Case S-Ref:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\tau_{{\mathrm{1}}}=\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}&\tau_{{\mathrm{2}}}=\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}\\\
[\vec{\ell}/\lambda]\,\tau_{{\mathrm{1}}}=([\vec{\ell}/\lambda]\,\tau^{\prime}_{{\mathrm{1}}})\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}&[\vec{\ell}/\lambda]\,\tau_{{\mathrm{2}}}=([\vec{\ell}/\lambda]\,\tau^{\prime}_{{\mathrm{2}}})\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}\\\
\Gamma\vdash\tau^{\prime}_{{\mathrm{1}}}\leq\tau^{\prime}_{{\mathrm{2}}}&r_{{\mathrm{2}}}\leq
r_{{\mathrm{1}}}\end{array}$
We must show that
$[\vec{\ell}/\lambda]\Gamma\vdash[\vec{\ell}/\lambda]\,\tau^{\prime}_{{\mathrm{1}}}\leq[\vec{\ell}/\lambda]\,\tau^{\prime}_{{\mathrm{2}}}$
which holds immediately from the induction hypothesis.

Case S-Int:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\tau_{{\mathrm{1}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{1}}}}\right\\}&\tau_{{\mathrm{2}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{2}}}}\right\\}\\\
[\vec{\ell}/\lambda]\,\tau_{{\mathrm{1}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid[\vec{\ell}/\lambda]\,\varphi_{{\mathrm{1}}}}\right\\}&[\vec{\ell}/\lambda]\,\tau_{{\mathrm{2}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid[\vec{\ell}/\lambda]\,\varphi_{{\mathrm{2}}}}\right\\}\\\
\Gamma\models\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}\end{array}$
We must show that
$[\vec{\ell}/\lambda]\Gamma\models[\vec{\ell}/\lambda]\,\varphi_{{\mathrm{1}}}\implies[\vec{\ell}/\lambda]\,\varphi_{{\mathrm{2}}}$,
i.e.
$\models\left\llbracket{[\vec{\ell}/\lambda]\Gamma}\right\rrbracket\wedge[\vec{\ell}/\lambda]\,\varphi_{{\mathrm{1}}}\implies[\vec{\ell}/\lambda]\,\varphi_{{\mathrm{2}}}$.
From our assumption that
$\Gamma\models\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}$ we have
that
$\models\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}$
is valid, whereby the formula
$\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}$
is true for any possible concrete valuation of the free context variable
$\lambda$. As $[\vec{\ell}/\lambda]\,\left\llbracket{\Gamma}\right\rrbracket$
is equivalent to $\left\llbracket{[\vec{\ell}/\lambda]\Gamma}\right\rrbracket$
we have the formula
$\left\llbracket{[\vec{\ell}/\lambda]\Gamma}\right\rrbracket\wedge[\vec{\ell}/\lambda]\,\varphi_{{\mathrm{1}}}\implies[\vec{\ell}/\lambda]\,\varphi_{{\mathrm{2}}}$
must also be valid.

  4. 4.

If $\lambda$ does not appear free in
$\left\llbracket{\Gamma}\right\rrbracket$, then the result trivially holds.
Otherwise $\models\left\llbracket{\Gamma}\right\rrbracket\implies\varphi$
holds for any concrete valuation of the free context variable $\lambda$. Then
the formula
$\models\left\llbracket{[\vec{\ell}/\lambda]\Gamma}\right\rrbracket\implies\varphi$
must be valid from the equivalence of
$[\vec{\ell}/\lambda]\,\left\llbracket{\Gamma}\right\rrbracket$ and
$\left\llbracket{[\vec{\ell}/\lambda]\Gamma}\right\rrbracket$.

  5. 5.

By induction on the typing derivation
$\Theta\mid\lambda\mid\Gamma\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$.
In every case, that
$\vec{\ell}\vdash_{\mathit{WF}}[\vec{\ell}/\lambda]\,\tau\operatorname{\Rightarrow}[\vec{\ell}/\lambda]\Gamma^{\prime}$
and $\vec{\ell}\vdash_{\mathit{WF}}[\vec{\ell}/\lambda]\Gamma$ holds from Item
2.

Case T-Var:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathit{e}=\mathit{x}&\tau=\tau_{{\mathrm{2}}}\\\
\Gamma=\Gamma_{{\mathrm{0}}}[\mathit{x}:\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}]&\Gamma^{\prime}=\Gamma_{{\mathrm{0}}}[\mathit{x}\hookleftarrow\tau_{{\mathrm{2}}}]\end{array}$
By application of Item 1.

Case T-LetInt:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathit{e}=\operatorname{\mathbf{let}}\mathit{x}=n\operatorname{\mathbf{in}}\mathit{e^{\prime}}&\Theta\mid\lambda\mid\Gamma,\mathit{x}:\left\\{{\nu\operatorname{:}\mathbf{int}\mid\nu\,=\,n}\right\\}\vdash\mathit{e^{\prime}}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}\\\
\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime})&\end{array}$
The induction hypothesis gives

$\Theta\mid\vec{\ell}\mid[\vec{\ell}/\lambda]\Gamma,\mathit{x}:\left\\{{\nu\operatorname{:}\mathbf{int}\mid\nu\,=\,n}\right\\}\vdash\mathit{e}:[\vec{\ell}/\lambda]\,\tau\operatorname{\Rightarrow}[\vec{\ell}/\lambda]\Gamma^{\prime}$

We conclude
$\Theta\mid\vec{\ell}\mid[\vec{\ell}/\lambda]\Gamma\vdash\operatorname{\mathbf{let}}\mathit{x}=n\operatorname{\mathbf{in}}\mathit{e}:[\vec{\ell}/\lambda]\,\tau\operatorname{\Rightarrow}[\vec{\ell}/\lambda]\Gamma^{\prime}$
as required.

Case T-Let:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}&\mathit{e}=\operatorname{\mathbf{let}}\mathit{x}=\mathit{y}\operatorname{\mathbf{in}}\mathit{e^{\prime}}&\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime})\\\
&\Theta\mid\lambda\mid\Gamma_{{\mathrm{1}}}\vdash\mathit{e^{\prime}}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}&\Gamma_{{\mathrm{1}}}=\Gamma[\mathit{y}\hookleftarrow(\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{1}}}}\mathit{x})],\mathit{x}:(\tau_{{\mathrm{2}}}\wedge_{\mathit{x}}\mathit{x}=_{\tau_{{\mathrm{2}}}}\mathit{y})\\\
&\Gamma\quad(\mathit{y})=\mathit{y}\operatorname{:}\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}\end{array}$
By Item 1,
$([\vec{\ell}/\lambda]\Gamma)(\mathit{y})=[\vec{\ell}/\lambda]\,(\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})=([\vec{\ell}/\lambda]\,\tau_{{\mathrm{1}}}+[\vec{\ell}/\lambda]\,\tau_{{\mathrm{2}}})$.
We must then show that
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime}_{{\mathrm{1}}}\vdash\mathit{e^{\prime}}:[\vec{\ell}/\lambda]\,\tau\operatorname{\Rightarrow}[\vec{\ell}/\lambda]\Gamma^{\prime}$
where

$\Gamma^{\prime}_{{\mathrm{1}}}=([\vec{\ell}/\lambda]\Gamma)[\mathit{y}\hookleftarrow[\vec{\ell}/\lambda]\,\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}\,=\,\mathit{x}],\mathit{x}:([\vec{\ell}/\lambda]\,\tau_{{\mathrm{2}}}\wedge_{\mathit{x}}\mathit{x}\,=\,\mathit{y})$

As $\Gamma^{\prime}_{{\mathrm{1}}}=[\vec{\ell}/\lambda]\Gamma_{{\mathrm{1}}}$
the induction hypothesis gives the required typing judgment.

Case T-If,T-Seq:
By trivial application of the inductive hypothesis.

Case T-MkRef,T-Deref:
By reasoning similar to T-Let.

Case T-Call:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\mathit{e}=\operatorname{\mathbf{let}}\mathit{x}=\mathit{f}^{\ell}(\mathit{y_{{\mathrm{1}}}},\ldots,\mathit{y_{\mathit{n}}})\operatorname{\mathbf{in}}\mathit{e^{\prime}}\\\
\sigma_{x}=[\mathit{y_{{\mathrm{1}}}}/\mathit{x_{{\mathrm{1}}}}]\cdots[\mathit{y_{\mathit{n}}}/\mathit{x_{\mathit{n}}}]\\\
\sigma_{\alpha}=[\ell:\lambda/\lambda^{\prime}]\\\
\Theta\mid\lambda\mid\Gamma_{{\mathrm{1}}}\vdash\mathit{e^{\prime}}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}\\\
\mathit{y}\not\in\mathit{dom}(\Gamma^{\prime})\\\
\Theta(\mathit{f})=\forall\lambda^{\prime}.\left\langle{\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau_{{\mathrm{1}}},\dots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau_{\mathit{n}}}\right\rangle\operatorname{\rightarrow}\left\langle{\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau^{\prime}_{{\mathrm{1}}},\dots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau^{\prime}_{\mathit{n}}\mid\tau^{\prime}}\right\rangle\\\
\Gamma_{{\mathrm{1}}}=\Gamma[\mathit{y_{\mathit{i}}}\hookleftarrow\sigma_{\alpha}\,\sigma_{x}\,\tau^{\prime}_{\mathit{i}}],\mathit{x}:\sigma_{\alpha}\,\sigma_{x}\,\tau^{\prime}\end{array}$
We must first show that for
$\sigma_{\alpha}^{\prime}=[\ell:\vec{\ell}/\lambda^{\prime}]$:

$\Theta\mid\vec{\ell}\mid\Gamma_{{\mathrm{3}}}\vdash\mathit{e^{\prime}}:[\vec{\ell}/\lambda]\,\tau\operatorname{\Rightarrow}[\vec{\ell}/\lambda]\Gamma^{\prime}$

where
$\Gamma_{{\mathrm{3}}}=([\vec{\ell}/\lambda]\Gamma)[\mathit{y_{\mathit{i}}}\hookleftarrow\sigma_{\alpha}^{\prime}\,\sigma_{x}\,\tau^{\prime}_{\mathit{i}}],\mathit{x}:\sigma_{\alpha}^{\prime}\,\sigma_{x}\,\tau^{\prime}$.

We first observe that
$\Gamma_{{\mathrm{3}}}=[\vec{\ell}/\lambda]\Gamma_{{\mathrm{1}}}$ (this
follows from the equivalence of
$[\vec{\ell}/\lambda]\,[\ell:\lambda/\lambda^{\prime}]$ and
$[\ell:\vec{\ell}/\lambda^{\prime}]$) whereby the induction hypothesis gives
the required typing derivation.

We must also show that $\forall
i\in\left\\{{1..n}\right\\}.([\ell:\vec{\ell}/\lambda]\Gamma)(\mathit{y_{\mathit{i}}})=\sigma_{\alpha}^{\prime}\,\sigma_{x}\,\tau_{\mathit{i}}$.
From the assumed well-typing of the term under $\lambda$ we have that $\forall
i\in\left\\{{1..n}\right\\}.\Gamma(\mathit{y_{\mathit{i}}})=\sigma_{\alpha}\,\sigma_{x}\,\tau_{\mathit{i}}$.
Recall that $\sigma_{\alpha}^{\prime}$ is equivalent to
$[\vec{\ell}/\lambda]\,\sigma_{\alpha}$, whereby we have
$[\vec{\ell}/\lambda]\Gamma(\mathit{y_{\mathit{i}}})=[\vec{\ell}/\lambda]\,\sigma_{\alpha}\,\sigma_{x}\,\tau_{\mathit{i}}=\sigma_{\alpha}^{\prime}\,\sigma_{x}\,\tau_{\mathit{i}}$
for any $\mathit{i}$ as equality is preserved by consistent substitution.

Case T-Assign:
By the inductive hypothesis and application of Item 1.

Case T-Alias:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Theta\mid\lambda\mid\Gamma[\mathit{x}:\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}][\mathit{y}:\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}]\vdash\mathbf{alias}(\mathit{x}=\mathit{y})\operatorname{;}\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma\\\
\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}+\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}\approx\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}+\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}}\\\
\Theta\mid\lambda\mid\Gamma[\mathit{x}\hookleftarrow\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}][\mathit{y}\hookleftarrow\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}}]\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma\end{array}$
From Item 1 we have that
$[\vec{\ell}/\lambda]\,(\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}})+[\vec{\ell}/\lambda]\,(\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}})=[\vec{\ell}/\lambda]\,(\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}+\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}})$
and similarly for
$\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}+\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}}$.
It therefore remains to show that:

$[\vec{\ell}/\lambda]\,(\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}+\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}})\approx[\vec{\ell}/\lambda]\,(\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}+\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}})$

For which it suffices to show that
$\bullet\vdash[\vec{\ell}/\lambda]\,(\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}+\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}})\leq[\vec{\ell}/\lambda]\,(\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}+\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}})$
and
$\bullet\vdash[\vec{\ell}/\lambda]\,(\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}+\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}})\leq[\vec{\ell}/\lambda]\,(\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}+\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}})$.
From
$\tau_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}+\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}\approx\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{1}}}}+\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r^{\prime}_{{\mathrm{2}}}}$
these both follow from Item 3, whereby the result follows from the inductive
hypothesis.

Case T-AliasPtr:
By similar reasoning to the T-Alias case.

Case T-Sub:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Theta\mid\lambda\mid\Gamma_{{\mathrm{1}}}\vdash\mathit{e}:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}&\Gamma\leq\Gamma_{{\mathrm{1}}}\\\
\Gamma_{{\mathrm{2}}},\tau_{{\mathrm{1}}}\leq\Gamma^{\prime},\tau\\\
\end{array}$
By the induction hypothesis we have that:
$\Theta\mid\vec{\ell}\mid[\vec{\ell}/\lambda]\Gamma_{{\mathrm{1}}}\vdash\mathit{e}:[\vec{\ell}/\lambda]\,\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}[\vec{\ell}/\lambda]\Gamma_{{\mathrm{2}}}$.
If we show that
$[\vec{\ell}/\lambda]\Gamma\leq[\vec{\ell}/\lambda]\Gamma_{{\mathrm{1}}}$ and
$[\vec{\ell}/\lambda]\Gamma_{{\mathrm{2}}},[\vec{\ell}/\lambda]\,\tau_{{\mathrm{1}}}\leq[\vec{\ell}/\lambda]\Gamma^{\prime},[\vec{\ell}/\lambda]\,\tau$
we will have the required result. To show the first requirement, for any
$\mathit{x}\in\mathit{dom}(\Gamma)$ we have that
$[\vec{\ell}/\lambda]\Gamma\vdash[\vec{\ell}/\lambda]\Gamma(\mathit{x})\leq[\vec{\ell}/\lambda]\Gamma_{{\mathrm{1}}}(\mathit{x})$
from Item 3 so we have
$[\vec{\ell}/\lambda]\Gamma\leq[\vec{\ell}/\lambda]\Gamma_{{\mathrm{1}}}$. To
show the latter requirement, we observe that
$[\vec{\ell}/\lambda]\Gamma_{{\mathrm{2}}},[\vec{\ell}/\lambda]\,\tau_{{\mathrm{1}}}\leq[\vec{\ell}/\lambda]\Gamma^{\prime},[\vec{\ell}/\lambda]\,\tau$
is equivalent to showing
$[\vec{\ell}/\lambda](\Gamma_{{\mathrm{2}}},\mathit{x}:\tau_{{\mathrm{1}}})\leq[\vec{\ell}/\lambda](\Gamma^{\prime},\mathit{x}:\tau)$
for some $\mathit{x}\not\in\mathit{dom}(\Gamma_{{\mathrm{2}}})$, whereby we
have the required subtyping relationship from the application of Item 3.

Case T-Assert:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Theta\mid\lambda\mid\Gamma\vdash\mathbf{assert}(\varphi)\operatorname{;}\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}&\Gamma\models\varphi\\\
\Theta\mid\lambda\mid\Gamma\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}&\epsilon\mid\Gamma\vdash_{\mathit{WF}}\varphi\end{array}$
By induction hypothesis, the result holds if we can show
$[\vec{\ell}/\lambda]\Gamma\models\varphi$ which follows from Item 4 (that
$\lambda\not\in\mathbf{FCV}\,(\varphi)$ follows from the well-formedness of
$\varphi$ with respect to $\epsilon$).

######  Lemma 10 (Substitution)

If
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
and $\mathit{x^{\prime}}\not\in\mathit{dom}(\Gamma)$, then
$\Theta\mid\mathcal{L}\mid[\mathit{x^{\prime}}/\mathit{x}]\,\Gamma\vdash\mathit{e}:[\mathit{x^{\prime}}/\mathit{x}]\,\tau\operatorname{\Rightarrow}[\mathit{x^{\prime}}/\mathit{x}]\,\Gamma^{\prime}$.

###### Proof

By straightforward induction of typing rules.

We now prove that if every variable satisfies its refinement in a type
environment $\Gamma$, we must have
$\models[\mathit{R}]\,\left\llbracket{\Gamma}\right\rrbracket$.

###### Lemma 11

If $\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma)$ then
$\models[\mathit{R}]\,\left\llbracket{\Gamma}\right\rrbracket$.

###### Proof

To show $\models[\mathit{R}]\,\left\llbracket{\Gamma}\right\rrbracket$, it
suffices to show that for any $\mathit{x}\in\mathit{dom}(\Gamma)$ where
$\Gamma(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}$
$\models[\mathit{R}]\,[\mathit{x}/\,\nu\,]\,\varphi$ holds. From
$\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma)$, we must have
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{R}(\mathit{x}),\Gamma(\mathit{x}))$,
whereby we have $\mathit{R}(\mathit{x})\in\mathbb{Z}$ and
$[\mathit{R}]\,[\mathit{R}(\mathit{x})/\nu]\varphi$. As
$[\mathit{R}]\,[\mathit{x}/\,\nu\,]\,\varphi$ is equivalent to
$[\mathit{R}]\,[\mathit{R}(\mathit{x})/\nu]\varphi$, and we have the desired
result.

We prove that subtyping preserves the consistency relation in the following
sense.

###### Lemma 12

If $\Gamma\leq\Gamma^{\prime}$ and
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$ then:

  1. 1.

For any $\mathit{x}\in\mathit{dom}(\Gamma^{\prime})$,
$\forall\,\mathit{a}\in\mathit{dom}(\mathit{H}).\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{x}),\Gamma(\mathit{x}))(\mathit{a})\leq\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{x}),\Gamma^{\prime}(\mathit{x}))(\mathit{a})$

  2. 2.

$\forall\,\mathit{a}\in\mathit{dom}(\mathit{H}).\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma^{\prime})(\mathit{a})\leq
1$

  3. 3.

If $\Gamma\vdash\tau\leq\tau^{\prime}$ and
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau)$ then
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau^{\prime})$

  4. 4.

$\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma^{\prime})$

  5. 5.

$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma^{\prime})$

###### Proof

  1. 1.

By induction on
$\Gamma\vdash\Gamma(\mathit{x})\leq\Gamma^{\prime}(\mathit{x})$.

  2. 2.

Direct consequence of 1 and that
$\forall\,\mathit{a}\in\mathit{dom}(\mathit{H}).\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)(\mathit{a})\leq
1$ from $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$.

  3. 3.

From $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$ we have
$\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma)$ which by Lemma 11 we have
$\models[\mathit{R}]\,\left\llbracket{\Gamma}\right\rrbracket$. We now proceed
by induction on $\Gamma\vdash\tau\leq\tau^{\prime}$.

Case:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\tau=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}&\tau^{\prime}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi^{\prime}}\right\\}\\\
\models\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi\implies\varphi^{\prime}\end{array}$
From $\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau)$ we have
$\models[\mathit{R}]\,[\mathit{v}/\nu]\varphi$. We must show that
$\models[\mathit{R}]\,[\mathit{v}/\nu]\varphi^{\prime}$. From
$\models\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi\implies\varphi^{\prime}$
we must have
$\models[\mathit{R}]\,[\mathit{v}/\nu]\left\llbracket{\Gamma}\right\rrbracket\wedge[\mathit{R}]\,[\mathit{v}/\nu]\varphi\implies[\mathit{R}]\,[\mathit{v}/\nu]\varphi^{\prime}$
is valid. As $\nu$ does not appear free in
$\left\llbracket{\Gamma}\right\rrbracket$, we have
$\models[\mathit{R}]\,\left\llbracket{\Gamma}\right\rrbracket\wedge[\mathit{R}]\,[\mathit{v}/\nu]\varphi\implies[\mathit{R}]\,[\mathit{v}/\nu]\varphi^{\prime}$
is valid whereby the result is immediate.

Case:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\tau=\tau_{\mathit{p}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}&\tau^{\prime}=\tau^{\prime}_{\mathit{p}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}\\\
r_{{\mathrm{2}}}\leq r_{{\mathrm{1}}}\end{array}$
Immediate from the induction hypothesis.

  4. 4.

Immediate consequence of 3 and that $\Gamma\leq\Gamma^{\prime}$ implies that
$\Gamma\vdash\Gamma(\mathit{x})\leq\Gamma^{\prime}(\mathit{x})$ for any
$\mathit{x}\in\mathit{dom}(\Gamma^{\prime})$.

  5. 5.

Immediate from 2 and 4.

To show consistency is preserved during evaluation, Lemmas 13 and 14 show
types equivalent according to $\approx$ are equivalent for the purposes of
$\mathbf{own}$ and $\mathbf{SATv}$. Then Lemmas 15 and 16 show that the type
addition operator $+$ “distributes” over $\mathbf{SATv}$ and $\mathbf{own}$.

######  Lemma 13 (Type Equivalence Preserves Satisfiability)

If $\tau_{{\mathrm{1}}}\approx\tau_{{\mathrm{2}}}$, then
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau_{{\mathrm{1}}})\iff\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau_{{\mathrm{2}}})$.

###### Proof

We prove the forward case by induction on
$\bullet\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$ as implied by
$\tau_{{\mathrm{1}}}\approx\tau_{{\mathrm{2}}}$. The inductive case follows
from the IH. In the the base case where
$\tau_{{\mathrm{1}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{1}}}}\right\\}$
and
$\tau_{{\mathrm{2}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{2}}}}\right\\}$,
from $\bullet\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$ we have that
$\models\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}$ is valid, from
which we must have
$\models[\mathit{R}]\,[\mathit{v}/\nu]\varphi_{{\mathrm{1}}}\implies[\mathit{R}]\,[\mathit{v}/\nu]\varphi_{{\mathrm{2}}}$,
where from the definition of
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau_{{\mathrm{1}}})$ we must
then have
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau_{{\mathrm{2}}})$.

The backwards case follows similar reasoning by induction on
$\bullet\vdash\tau_{{\mathrm{2}}}\leq\tau_{{\mathrm{1}}}$.

###### Lemma 14

If $\tau_{{\mathrm{1}}}\approx\tau_{{\mathrm{2}}}$, then
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{1}}})=\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{2}}})$.

###### Proof

By reasoning similar to that in Lemma 13.

###### Lemma 15

If $\tau_{\mathit{p}}=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$, then
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{\mathit{p}})=\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{1}}})+\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{2}}})$.

###### Proof

By induction on the rules used to derive
$\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}=\tau_{\mathit{p}}$.

Case Tadd-Int:
We have
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{\mathit{p}})=\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$,
where
$\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{1}}}\wedge\varphi_{{\mathrm{2}}}}\right\\}$,
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{1}}})$ and
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{2}}})$, where
$\tau_{{\mathrm{1}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{1}}}}\right\\},\tau_{{\mathrm{2}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{2}}}}\right\\}$.

From the definition of ownership, we have
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{\mathit{p}})=\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{1}}})=\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{2}}})=\emptyset$.
It is thus trivial that
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{\mathit{p}})=\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{1}}})+\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{2}}})$.

Case Tadd-Ref:
We assume $\mathit{v}\,=\,\mathit{a}$ and
$\mathit{a}\in\mathit{dom}(\mathit{H})$, otherwise the result trivially holds.

We have
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{\mathit{p}})=\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{1}}}+\tau_{{\mathrm{1}}})$,
where
$\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}=(\tau^{\prime}_{{\mathrm{1}}}+\tau^{\prime}_{{\mathrm{2}}})\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}+r_{{\mathrm{2}}}}$,
and
$\tau_{{\mathrm{1}}}=\tau^{\prime}_{{\mathrm{1}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{1}}}}$,
$\tau_{{\mathrm{2}}}=\tau^{\prime}_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{r_{{\mathrm{2}}}}$.

From the definition of ownership, we have
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{\mathit{p}})=\\{\mathit{a}\mapsto
r_{{\mathrm{1}}}+r_{{\mathrm{2}}}\\}+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{v}),\tau^{\prime}_{{\mathrm{1}}}+\tau^{\prime}_{{\mathrm{2}}})$
and:

$\displaystyle\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{1}}})+\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{2}}})$
$\displaystyle=\\{\mathit{a}\mapsto
r_{{\mathrm{1}}}\\}+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{v}),\tau^{\prime}_{{\mathrm{1}}})+\\{\mathit{a}\mapsto
r_{{\mathrm{2}}}\\}+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{v}),\tau^{\prime}_{{\mathrm{2}}})$
$\displaystyle=\\{\mathit{a}\mapsto
r_{{\mathrm{1}}}+r_{{\mathrm{2}}}\\}+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{v}),\tau^{\prime}_{{\mathrm{1}}})+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{v}),\tau^{\prime}_{{\mathrm{2}}})$

By the induction hypothesis, have that
$\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{v}),\tau^{\prime}_{{\mathrm{1}}}+\tau^{\prime}_{{\mathrm{2}}})=\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{v}),\tau^{\prime}_{{\mathrm{1}}})+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{v}),\tau^{\prime}_{{\mathrm{2}}})$
and can conclude that
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{\mathit{p}})=\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{1}}})+\mathbf{own}\,(\mathit{H},\mathit{v},\tau_{{\mathrm{2}}})$.

###### Lemma 16

If $\tau_{\mathit{p}}=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$, we have
$\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{\mathit{p}})$ iff.
$\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{{\mathrm{1}}})$ and
$\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{{\mathrm{2}}})$

###### Proof

By induction on the rules used to derive
$\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$. In the following we only prove the
forward direction of the implication; the backwards direction is symmetric.

Case Tadd-Int:
We have
$\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$,
where
$\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{1}}}\wedge\varphi_{{\mathrm{2}}}}\right\\}$,
we must show $\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{{\mathrm{1}}})$ and
$\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{{\mathrm{2}}})$, where
$\tau_{{\mathrm{1}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{1}}}}\right\\},\tau_{{\mathrm{2}}}=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi_{{\mathrm{2}}}}\right\\}$.

From the definition of $\mathbf{SATv}$, we must show
$[\mathit{R}]\,[v/\nu]\varphi_{{\mathrm{1}}}$ and
$[\mathit{R}]\,[\mathit{v}/\nu]\varphi_{{\mathrm{2}}}$. From
$\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$
we have
$[\mathit{R}]\,[\mathit{v}/\mathit{x}](\varphi_{{\mathrm{1}}}\wedge\varphi_{{\mathrm{2}}})$.
It is immediate that for any value $v$ such that
$[\mathit{R}]\,[\mathit{v}/\nu](\varphi_{{\mathrm{1}}}\wedge\varphi_{{\mathrm{2}}})$,
we must have $[\mathit{R}]\,[\mathit{v}/\nu]\varphi_{{\mathrm{1}}}$ and
$[\mathit{R}]\,[\mathit{v}/\nu]\varphi_{{\mathrm{2}}}$. We then conclude
$\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$
implies $\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{{\mathrm{1}}})$ and
$\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau_{{\mathrm{2}}})$.

Case Tadd-Ref:
Immediate from the definition of $\mathbf{SATv}$ and the inductive hypothesis.

###### Definition 2

The valid substitution relation, written $\mathit{R}\vdash_{vs}\tau$ is the
smallest relation closed under the following rules:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\forall\,\mathit{x}\in\mathbf{FPV}\,(\varphi)\setminus\left\\{{\nu}\right\\}.\exists\,n.\mathit{R}(\mathit{x})=n\end{array}}{\begin{array}[]{@{}c@{}}\mathit{R}\vdash_{vs}\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathit{R}\vdash_{vs}\tau\end{array}}{\begin{array}[]{@{}c@{}}\mathit{R}\vdash_{vs}\tau\operatorname{\mathbf{ref}}^{r}\end{array}}$

###### Lemma 17

If $\vec{\ell}\vdash_{\mathit{WF}}\Gamma$ and
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$, then
$\forall\,\mathit{x}\in\mathit{dom}(\Gamma).\mathit{R}\vdash_{vs}\Gamma(\mathit{x})$.

###### Proof

By $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$, all integer variables in
$\Gamma$ must be in the domain of $\mathit{R}$ and must be an integer. From
$\vec{\ell}\vdash_{\mathit{WF}}\Gamma$, any free variables in any refinement
of any type in $\Gamma$ must be an integer valued variable in $\Gamma$, which
gives the required result.

###### Definition 3

We will write $\mathit{R}\sqsubseteq\mathit{R^{\prime}}$ to denote two
register files such that:

  1. 1.

$\mathit{dom}(\mathit{R})\subseteq\mathit{dom}(\mathit{R^{\prime}})$, and

  2. 2.

$\forall\,\mathit{x}\in\mathit{dom}(\mathit{R}).\mathit{R}(\mathit{x})=\mathit{R^{\prime}}(\mathit{x})$

###### Definition 4

Two heaps $\mathit{H}$ and $\mathit{H^{\prime}}$ are _equivalent modulo
$\mathit{a}$_, written $\mathit{H}\approx_{\mathit{a}}\mathit{H^{\prime}}$ if:

  1. 1.

$\mathit{dom}(\mathit{H})=\mathit{dom}(\mathit{H^{\prime}})$

  2. 2.

$\forall\,\mathit{a^{\prime}}\in\mathit{dom}(\mathit{H}).\mathit{a^{\prime}}\,\neq\,\mathit{a}\implies\mathit{H}(\mathit{a})=\mathit{H}(\mathit{a^{\prime}})$

  3. 3.

For any $n$, $\mathit{H}\vdash\mathit{a}\Downarrow n$ iff
$\mathit{H^{\prime}}\vdash\mathit{a}\Downarrow n$

###### Lemma 18

For any type $\tau=\top_{\mathit{n}}$, $\mathit{H},\mathit{v}$,
$\mathbf{own}\,(\mathit{H},\mathit{v},\top_{\mathit{n}})=\emptyset$.

###### Proof

By induction on $\tau$. In the base case, the result is trivial. Then consider
the case where $\tau=\top_{{\mathit{n}-1}}\operatorname{\mathbf{ref}}^{0}$. If
$\mathit{v}\not\in\textbf{Addr}$, or if $\mathit{v}\,=\,\mathit{a}$ and
$\mathit{a}\not\in\mathit{dom}(\mathit{H})$, then the result trivially holds.
Otherwise the result holds from the inductive hypothesis, the definition of
$+$ and $\\{\mathit{a}\mapsto 0\\}$.

######  Lemma 19 (Heap Update Ownership Preservation)

If $\mathit{H}\approx_{\mathit{a}}\mathit{H^{\prime}}$ and
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau)(\mathit{a})=0$, then
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau)=\mathbf{own}\,(\mathit{H^{\prime}},\mathit{v},\tau)$.

###### Proof

By induction on the shape of $\tau$. If
$\tau=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}$ then the
result trivially holds. Otherwise,
$\tau=\tau^{\prime}\operatorname{\mathbf{ref}}^{r}$. We assume that
$\mathit{v}\,=\,\mathit{a^{\prime\prime}}$ and
$\mathit{a^{\prime\prime}}\in\mathit{dom}(\mathit{H})$ (otherwise the result
trivially holds, as
$\mathit{dom}(\mathit{H})=\mathit{dom}(\mathit{H^{\prime}})$ by
$\mathit{H}\approx_{\mathit{a}}\mathit{H^{\prime}}$). Consider the case where
$\mathit{a^{\prime\prime}}\,=\,\mathit{a}$. By definition
$\mathbf{own}\,(\mathit{H},\mathit{a},\tau)=\\{\mathit{a}\mapsto
r\\}+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{a}),\tau^{\prime})$, and by
the assumption that $\mathbf{own}\,(\mathit{H},\mathit{a},\tau)(\mathit{a})=0$
we must have that $r=0$. Further, by the ownership well-formedness of types,
we must have $\tau^{\prime}=\top_{\mathit{n}}$ for some $n$, thus by Lemma 18
we have
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau)=\emptyset=\\{\mathit{a}\mapsto
0\\}+\mathbf{own}\,(\mathit{H^{\prime}},\mathit{H^{\prime}}(\mathit{a}),\top_{\mathit{n}})=\mathbf{own}\,(\mathit{H^{\prime}},\mathit{v},\tau)$.

Finally, consider the case where
$\mathit{a^{\prime\prime}}\,\neq\,\mathit{a}$. Then from the definition of
$\mathbf{own}\,(\mathit{H},\mathit{a^{\prime\prime}},\tau)$ and our assumption
that
$\mathbf{own}\,(\mathit{H},\mathit{a^{\prime\prime}},\tau)(\mathit{a})=0$, we
have
$\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{a^{\prime\prime}}),\tau^{\prime})(\mathit{a})=0$,
and the result holds from the inductive hypothesis and that
$\mathit{H}(\mathit{a^{\prime\prime}})\,=\,\mathit{H^{\prime}}(\mathit{a^{\prime\prime}})$.

###### Lemma 20

For any $\mathit{H}$, $\mathit{R}$, $\mathit{v}$, and $\tau$, if
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau)$ then
$\mathit{H}\vdash\mathit{v}\Downarrow|\tau|$

###### Proof

By induction on $\tau$ and the definition of $\mathbf{SATv}$.

###### Lemma 21

For any $n$, if $\mathit{H}\vdash v\Downarrow n$ then for any $\mathit{R}$,
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\top_{\mathit{n}})$.

###### Proof

By induction on $n$. In the base case, by inversion on
$\mathit{H}\vdash\mathit{v}\Downarrow 0$ we have $\mathit{v}\in\mathbb{Z}$ and
as $[\mathit{R}]\,[\mathit{v}/\nu]\top\implies\top$, we conclude
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\top_{{\mathrm{0}}})$.

For $n>0$, by inversion on $\mathit{H}\vdash v\Downarrow n$ we have that
$\mathit{v}\,=\,\mathit{a}$, $\mathit{a}\in\mathit{dom}(\mathit{H})$, and
$\mathit{H}\vdash\mathit{H}(\mathit{a})\Downarrow n-1$, whereby the result
holds from the inductive hypothesis.

######  Lemma 22 (Heap Update Consistency Preservation)

If $\mathit{H}\approx_{\mathit{a}}\mathit{H^{\prime}}$ and
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau)(\mathit{a})=0$ and
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau)$, then
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{v},\tau)$.

###### Proof

By induction on the shape of $\tau$. The base case where
$\tau=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}$ is
trivial. We therefore consider the case where
$\mathit{v}\,=\,\mathit{a^{\prime}}$ and
$\tau=\tau^{\prime}\operatorname{\mathbf{ref}}^{r}$.

We first consider the case where $\mathit{a^{\prime}}\,=\,\mathit{a}$, then by
our assumption that
$\mathbf{own}\,(\mathit{H},\mathit{a},\tau)(\mathit{a})=0$, we must have that
$\tau=\tau^{\prime}\operatorname{\mathbf{ref}}^{0}$, whereby
$\tau=\top_{\mathit{n}}$ for some $\mathit{n}$. From
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{a},\tau)$ and Lemma 20, we must
have that $\mathit{H}\vdash\mathit{a}\Downarrow|\tau|$, and from
$\mathit{H}\approx_{\mathit{a}}\mathit{H^{\prime}}$, we therefore have that
$\mathit{H^{\prime}}\vdash\mathit{a}\Downarrow|\tau|$ whereby the result holds
from Lemma 21.

Otherwise, we have that $\mathit{a^{\prime}}\,\neq\,\mathit{a}$, and by
definition we must have that
$\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{a}),\tau^{\prime})(\mathit{a})=0$
and $\mathit{H^{\prime}}(\mathit{a})\,=\,\mathit{H}(\mathit{a})$ hence the
result follows from the inductive hypothesis.

######  Lemma 23 (Register Weakening)

If $\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau)$ and
$\mathit{R}\vdash_{vs}\tau$, then for any $\mathit{R^{\prime}}$ such that
$\mathit{R}\sqsubseteq\mathit{R^{\prime}}$,
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},v,\tau)$.

###### Proof

By induction on the shape of $\tau$. If
$\tau=\tau^{\prime}\operatorname{\mathbf{ref}}^{r}$, then the result follows
from the inductive hypothesis. We therefore consider the case where
$\tau=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}$. Without
loss of generality, we consider the case where
$\mathit{dom}(\mathit{R^{\prime}})\setminus\mathit{dom}(\mathit{R})=\left\\{{x}\right\\}$,
and $\mathit{R^{\prime}}(\mathit{x})\,=\,n$. (If
$\mathit{R^{\prime}}(\mathit{x})\,=\,\mathit{a}$, the extra binding also has
no effect, and the case where more than one binding is added follows from $n$
applications of the following argument.)

From $\mathbf{SATv}(\mathit{H},\mathit{R},v,\tau)$, we conclude that
$v\in\mathbb{Z}$ and that $[\mathit{R}]\,[v/\nu]\varphi$. If
$\mathit{x}\not\in\mathbf{FPV}\,(\varphi)$ then
$[\mathit{R}]\,[v/\nu]\varphi\iff[\mathit{R^{\prime}}]\,[v/\nu]\varphi$ and
the result holds trivially. Otherwise, if
$\mathit{x}\in\mathbf{FPV}\,(\varphi)$ and
$\mathit{x}\not\in\mathit{dom}(\mathit{R})$ then $\mathit{R}$ is not a valid
substitution, violating our assumption.

######  Lemma 24 (Heap Extension Consistency Preservation)

If we have heap $H$, such that
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau)$, for any heap
$\mathit{H^{\prime}}=\mathit{H}\\{\mathit{a}\mapsto\mathit{v^{\prime}}\\},\mathit{a}\not\in\mathit{dom}(\mathit{H})$,
then we have $\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{v},\tau)$.

###### Proof

By induction on the shape of $\tau$. The base case where
$\tau=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}$ is
trivial. Next, we consider the case where
$\tau=\tau^{\prime}\operatorname{\mathbf{ref}}^{r}$. We must show that
$\mathit{v}\in\mathit{dom}(\mathit{H^{\prime}})$ and
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{H^{\prime}}(\mathit{v}),\tau^{\prime})$.
The first condition is immediately satisfied by inversion on
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau^{\prime})$, and from
$\mathit{a}\not\in\mathit{dom}(\mathit{H})$, we have $v\neq a$, which gives
that $H^{\prime}(v)=H(v)$. That is we must show
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{H}(\mathit{v}),\tau^{\prime})$,
which is follows from the induction hypothesis.

######  Lemma 25 (Heap Extension Ownership Preservation)

If $\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau)$, then for any
$\mathit{a}\not\in\mathit{dom}(\mathit{H})$
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau)=\mathbf{own}\,(\mathit{H}\\{\mathit{a}\mapsto\mathit{v^{\prime}}\\},\mathit{v},\tau)$
for any value $\mathit{v^{\prime}}$.

###### Proof

By induction on $\tau$. The base case is trivial as
$\mathbf{own}\,(\mathit{H},\mathit{v},\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\})=\emptyset=\mathbf{own}\,(\mathit{H}\\{\mathit{a}\mapsto\mathit{v}\\},\mathit{v},\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\})$.
We therefore consider the case where
$\tau=\tau^{\prime}\operatorname{\mathbf{ref}}^{r}$.

From $\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau)$ we must have that
$\mathit{v}\,=\,\mathit{a^{\prime}}$ and
$\mathit{a^{\prime}}\in\mathit{dom}(\mathit{H})$ (and by extension
$\mathit{a^{\prime}}\in\mathit{dom}(\mathit{H}\\{\mathit{a}\mapsto\mathit{v^{\prime}}\\})$).
From the definition of the ownership function, we have that
$\mathbf{own}\,(\mathit{H},\mathit{v},\tau)=\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{a}),\tau^{\prime})+\\{\mathit{a^{\prime}}\mapsto
r\\}$. and
$\mathbf{own}\,(\mathit{H}\\{\mathit{a}\mapsto\mathit{v^{\prime}}\\},\mathit{v},\tau)=\mathbf{own}\,(\mathit{H}\\{\mathit{a}\mapsto\mathit{v^{\prime}}\\},\mathit{H}\\{\mathit{a}\mapsto\mathit{v^{\prime}}\\}(\mathit{a^{\prime}}),\tau^{\prime})+\\{\mathit{a^{\prime}}\mapsto
r\\}$ Then from our requirement that
$\mathit{a}\not\in\mathit{dom}(\mathit{H})$, we have
$\mathit{a}\,\neq\,\mathit{a^{\prime}}$ and therefore
$\mathit{H}(\mathit{a^{\prime}})\,=\,\mathit{H}\\{\mathit{a}\mapsto\mathit{v^{\prime}}\\}(\mathit{a^{\prime}})$,
whereby the result holds from the inductive hypothesis.

######  Lemma 26 (Environment Weakening)

Define the partial operation
$\Gamma_{{\mathrm{1}}}\uplus\Gamma_{{\mathrm{2}}}$ for two environments such
$\mathit{dom}(\Gamma_{{\mathrm{1}}})\cap\mathit{dom}(\Gamma_{{\mathrm{2}}})=\emptyset$:

$(\Gamma_{{\mathrm{1}}}\uplus\Gamma_{{\mathrm{2}}})\quad(\mathit{x})=\begin{cases}\Gamma_{{\mathrm{1}}}\quad(\mathit{x})&\mathit{x}\in\mathit{dom}(\Gamma_{{\mathrm{1}}})\\\
\Gamma_{{\mathrm{2}}}\quad(\mathit{x})&\mathit{x}\in\mathit{dom}(\Gamma_{{\mathrm{2}}})\\\
\textit{undef}&o.w.\end{cases}$

Then, for any $\Gamma$ and $\Gamma^{\prime\prime}$ where
$\mathit{dom}(\Gamma)\cap\mathit{dom}(\Gamma^{\prime\prime})=\emptyset$:

  1. 1.

$\Gamma\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$ implies
$\Gamma\uplus\Gamma^{\prime\prime}\vdash\tau_{{\mathrm{1}}}\leq\tau_{{\mathrm{2}}}$

  2. 2.

$\Gamma\leq\Gamma^{\prime}$ implies
$\Gamma\uplus\Gamma^{\prime\prime}\leq\Gamma^{\prime}\uplus\Gamma^{\prime\prime}$

  3. 3.

If
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$,
$\mathcal{L}\vdash_{\mathit{WF}}\Gamma\uplus\Gamma^{\prime\prime}$, and
$\mathcal{L}\vdash_{\mathit{WF}}\Gamma^{\prime}\uplus\Gamma^{\prime\prime}$,
then
$\Theta\mid\mathcal{L}\mid\Gamma\uplus\Gamma^{\prime\prime}\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime\prime}\uplus\Gamma$

###### Proof

  1. 1.

As in the proof of Lemma 9 (part 3), at the root of the subtyping derivation
is a logical judgment of the form
$\models\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}$
which can be shown to be valid. We must then show that
$\models\left\llbracket{\Gamma\uplus\Gamma^{\prime\prime}}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}$
is valid. As
$\left\llbracket{\Gamma^{\prime\prime}\uplus\Gamma}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}=\left\llbracket{\Gamma^{\prime\prime}}\right\rrbracket\wedge\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi$
only strengthens the pre-condition
$\left\llbracket{\Gamma}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}$,
$\models\left\llbracket{\Gamma^{\prime\prime}\uplus\Gamma}\right\rrbracket\wedge\varphi_{{\mathrm{1}}}\implies\varphi_{{\mathrm{2}}}$
must also be valid.

  2. 2.

It suffices to show that
$\Gamma\uplus\Gamma^{\prime\prime}\vdash(\Gamma\uplus\Gamma^{\prime\prime})(\mathit{x})\leq(\Gamma^{\prime}\uplus\Gamma^{\prime\prime})(\mathit{x})$
for any arbitrary
$\mathit{x}\in\mathit{dom}(\Gamma^{\prime}\uplus\Gamma^{\prime\prime})$. If
$\mathit{x}\in\mathit{dom}(\Gamma^{\prime})$ then we must have
$\Gamma\vdash\Gamma(\mathit{x})\leq\Gamma^{\prime}(\mathit{x})$ by inversion
on $\Gamma\leq\Gamma^{\prime}$, whereby
$\Gamma\uplus\Gamma^{\prime\prime}\vdash(\Gamma\uplus\Gamma^{\prime\prime})(\mathit{x})=\Gamma(\mathit{x})\leq\Gamma^{\prime}\uplus\Gamma^{\prime\prime}(\mathit{x})=\Gamma^{\prime}(\mathit{x})$
from part 1.

If $\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime})$, then we must show
$(\Gamma\uplus\Gamma^{\prime\prime})\vdash\Gamma^{\prime\prime}(\mathit{x})\leq\Gamma^{\prime\prime}(\mathit{x})$,
which trivially holds.

  3. 3.

By induction on the typing derivation of
$\Theta\mid\mathcal{L}\mid\Gamma\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$.
We assume that the variables bound in any let expressions that appear within
$\mathit{e}$ are not in the domain of $\Gamma^{\prime\prime}$; this
requirement can be easily enforced with consistent renaming and is preserved
during evaluation. The only interesting cases are T-Sub and T-Assert and the
let bindings; the other cases follow from the induction hypothesis.

We now prove the relevant cases.

Case T-Let:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Theta\mid\mathcal{L}\mid\Gamma\vdash\operatorname{\mathbf{let}}\mathit{x}=\mathit{y}\operatorname{\mathbf{in}}\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}\\\
\Theta\mid\mathcal{L}\mid\Gamma[\mathit{y}\hookleftarrow\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{1}}}}\mathit{x}],\mathit{x}:\tau_{{\mathrm{2}}}\wedge_{\mathit{x}}\mathit{x}=_{\tau_{{\mathrm{2}}}}\mathit{y}\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}\\\
\Gamma(\mathit{y})=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}\quad\quad\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime})\end{array}$
Let
$\Gamma^{\prime\prime\prime}=\Gamma^{\prime\prime}\uplus\Gamma[\mathit{y}\hookleftarrow\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{1}}}}\mathit{x}],\mathit{x}:\tau_{{\mathrm{2}}}\wedge_{\mathit{x}}\mathit{x}=_{\tau_{{\mathrm{2}}}}\mathit{y}$.
To use the inductive hypothesis, we must show that
$\mathcal{L}\vdash_{\mathit{WF}}\Gamma^{\prime\prime\prime}$ and
$\mathcal{L}\vdash_{\mathit{WF}}\Gamma^{\prime}\uplus\Gamma^{\prime\prime}$.
The latter holds by assumption. To show the former, it suffices to show
$\mathcal{L}\mid\Gamma^{\prime\prime\prime}\vdash_{\mathit{WF}}\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{1}}}}\mathit{x}$
and
$\mathcal{L}\mid\Gamma^{\prime\prime\prime}\vdash_{\mathit{WF}}\tau_{{\mathrm{2}}}\wedge_{\mathit{x}}\mathit{x}=_{\tau_{{\mathrm{2}}}}\mathit{y}$.
From the assumed well-formedness
$\mathcal{L}\vdash_{\mathit{WF}}\Gamma\uplus\Gamma^{\prime\prime}$, we must
have
$\mathcal{L}\mid\Gamma\uplus\Gamma^{\prime\prime}\vdash_{\mathit{WF}}\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$,
and in particular
$\mathcal{L}\mid\Gamma\uplus\Gamma^{\prime\prime}\vdash_{\mathit{WF}}\tau_{{\mathrm{1}}}$
and
$\mathcal{L}\mid\Gamma\uplus\Gamma^{\prime\prime}\vdash_{\mathit{WF}}\tau_{{\mathrm{2}}}$.
From this we conclude both conditions hold. To show the well-typing of the
overall let expression, we must show
$\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime}\uplus\Gamma^{\prime\prime})$,
which follows from our assumption and
$\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime})$. Finally, we must also show
that
$\mathcal{L}\mid\Gamma^{\prime}\uplus\Gamma^{\prime\prime}\vdash_{\mathit{WF}}\tau$.
From $\mathcal{L}\mid\Gamma^{\prime}\vdash_{\mathit{WF}}\tau$ and the fact
that$\forall\,\mathit{x}\in\mathit{dom}(\Gamma^{\prime}).\Gamma^{\prime}(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\\_}\right\\}$
iff
$(\Gamma^{\prime}\uplus\Gamma^{\prime\prime})(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\\_}\right\\}$,
we must have
$\mathcal{L}\mid\Gamma^{\prime}\uplus\Gamma^{\prime\prime}\vdash_{\mathit{WF}}\tau$.

Cases T-LetInt, T-Mkref, T-Mkref, T-Deref, T-Call:
Similar to the reasoning in T-Let.

Case T-Sub:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\Gamma\leq\Gamma_{{\mathrm{1}}}&\Theta\mid\mathcal{L}\mid\Gamma_{{\mathrm{1}}}\vdash\mathit{e}:\tau_{{\mathrm{2}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}\\\
\Gamma_{{\mathrm{2}}},\tau_{{\mathrm{2}}}\leq\Gamma^{\prime},\tau\\\
\end{array}$
From the rules for subtyping, we must have
$\mathit{dom}(\Gamma_{{\mathrm{1}}})\subseteq\mathit{dom}(\Gamma)$ and
$\mathit{dom}(\Gamma^{\prime})\subseteq\mathit{dom}(\Gamma_{{\mathrm{2}}})$. A
simple inductive argument gives that
$\mathit{dom}(\Gamma_{{\mathrm{2}}})\subseteq\mathit{dom}(\Gamma_{{\mathrm{1}}})$,
therefore we have
$\mathit{dom}(\Gamma^{\prime})\subseteq\mathit{dom}(\Gamma_{{\mathrm{1}}})$.
Let $\mathcal{LV}$ be the set of free variables in the refinements of
$\Gamma^{\prime\prime}$ that are not in the domain of $\Gamma^{\prime\prime}$.
From the assumed well-formedness of
$\mathcal{L}\vdash_{\mathit{WF}}\Gamma^{\prime}\uplus\Gamma^{\prime\prime}$,
we must have that $\forall
x\in\mathcal{LV}.\mathit{x}\in\mathit{dom}(\Gamma^{\prime})\wedge\Gamma^{\prime}(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\\_}\right\\}$.
Thus, $\mathcal{LV}\subseteq\Gamma_{{\mathrm{1}}}$ and
$\mathcal{LV}\subseteq\Gamma_{{\mathrm{2}}}$. Further, by definition, for any
$\Gamma_{\mathit{p}}\leq\Gamma_{\mathit{q}}$, if
$\Gamma_{\mathit{q}}(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\\_}\right\\}$
then
$\Gamma_{\mathit{p}}(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\\_}\right\\}$,
i.e. subtyping preserves simple types. We conclude that
$\mathcal{L}\vdash_{\mathit{WF}}\Gamma_{{\mathrm{1}}}\uplus\Gamma^{\prime\prime}$
and
$\mathcal{L}\vdash_{\mathit{WF}}\Gamma_{{\mathrm{2}}}\uplus\Gamma^{\prime\prime}$,
whereby the inductive hypothesis gives
$\Theta\mid\mathcal{L}\mid\Gamma_{{\mathrm{1}}}\uplus\Gamma^{\prime\prime}\vdash\mathit{e}:\tau_{{\mathrm{2}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}\uplus\Gamma^{\prime\prime}$.
To prove the overall result, we must show that
$\Gamma\uplus\Gamma^{\prime\prime}\leq\Gamma_{{\mathrm{1}}}\uplus\Gamma^{\prime\prime}$
and
$\Gamma_{{\mathrm{2}}}\uplus\Gamma^{\prime\prime},\tau_{{\mathrm{2}}}\leq\Gamma^{\prime}\uplus\Gamma^{\prime\prime},\tau$
which follow from parts 1 and 2 above. That
$\mathcal{L}\mid\Gamma_{{\mathrm{2}}}\uplus\Gamma^{\prime\prime}\vdash_{\mathit{WF}}\tau_{{\mathrm{2}}}$
follows by reasoning to the case for T-Let above.

Case T-Assert:
We must show that
$\models\left\llbracket{\Gamma^{\prime\prime}\uplus\Gamma}\right\rrbracket\implies\varphi$
which is equivalent to
$\models\left\llbracket{\Gamma^{\prime\prime}}\right\rrbracket\wedge\left\llbracket{\Gamma}\right\rrbracket\implies\varphi$.
As the source term was well typed,
$\models\left\llbracket{\Gamma}\right\rrbracket\implies\varphi$ is valid, we
must then have
$\models\left\llbracket{\Gamma^{\prime\prime}}\right\rrbracket\wedge\left\llbracket{\Gamma}\right\rrbracket\implies\varphi$
whereby the inductive hypothesis gives the required result.

##  Appendix 0.C Proof of Lemma 3

We first prove two additional lemmas. Lemmas 27 and 28 give key facts used in
the return and call cases respectively; we have separated them into separate
lemmas for clarity.

###### Lemma 27

For any $\Gamma_{{\mathrm{0}}}$ such that
$\Theta\mid\ell:\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\mathit{x}:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}$
and
$\Theta\mid[]:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}\mid\vec{\ell}\vdash_{\mathit{ectx}}\mathit{E}[\operatorname{\mathbf{let}}\mathit{y}=[]^{\ell}\operatorname{\mathbf{in}}\mathit{e}]:\tau_{{\mathrm{2}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}$
then
$\Theta\mid\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\mathit{E}[\operatorname{\mathbf{let}}\mathit{y}=[]^{\ell}\operatorname{\mathbf{in}}\mathit{e}][\mathit{x}]:\tau_{{\mathrm{2}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}$.

###### Proof

It suffices to show that
$\Theta\mid\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\operatorname{\mathbf{let}}\mathit{y}=\mathit{x}\operatorname{\mathbf{in}}\mathit{e}:\tau^{\prime}_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{1}}}$
and
$\Theta\mid[]:\tau^{\prime}_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{1}}}\mid\vec{\ell}\vdash_{\mathit{ectx}}\mathit{E}:\tau_{{\mathrm{2}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}$
for some $\tau^{\prime}_{{\mathrm{1}}}$ and $\Gamma^{\prime}_{{\mathrm{1}}}$
whereby the result will hold from Lemma 8.

By inversion on
$\Theta\mid[]:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}\mid\vec{\ell}\vdash_{\mathit{ectx}}\mathit{E}[\operatorname{\mathbf{let}}\mathit{y}=[]^{\ell}\operatorname{\mathbf{in}}\mathit{e}]:\tau_{{\mathrm{2}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}$
we have

$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma_{{\mathrm{1}}},\mathit{y}:\tau_{{\mathrm{1}}}\vdash\mathit{e}:\tau^{\prime\prime}_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma^{\prime\prime}_{{\mathrm{1}}}$
(1)
$\displaystyle\Theta\mid[]:\tau^{\prime\prime}_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma^{\prime\prime}_{{\mathrm{1}}}\mid\mathcal{L}\vdash_{\mathit{ectx}}\mathit{E}:\tau_{{\mathrm{2}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}$
(2)
$\displaystyle\mathit{y}\not\in\mathit{dom}(\Gamma^{\prime\prime}_{{\mathrm{1}}})$
(3)

We take $\Gamma^{\prime}_{{\mathrm{1}}}=\Gamma^{\prime\prime}_{{\mathrm{1}}}$,
$\tau^{\prime}_{{\mathrm{1}}}=\tau^{\prime\prime}_{{\mathrm{1}}}$, and then
Equation 2 gives the necessary typing for $\mathit{E}$.

It remains to to show that

$\Theta\mid\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\operatorname{\mathbf{let}}\mathit{y}=\mathit{x}\operatorname{\mathbf{in}}\mathit{e}:\tau^{\prime}_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{1}}}$

(That
$\vec{\ell}\vdash_{\mathit{WF}}\tau^{\prime}_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{1}}}$
follows from Equation 1)

By Lemma 6, from
$\Theta\mid\ell:\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\mathit{x}:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}$
we conclude there exists some $\Gamma_{\mathit{p}}$, $\tau_{\mathit{p}}$, and
$\Gamma^{\prime}_{\mathit{p}}$ such:

$\displaystyle\Gamma_{{\mathrm{0}}}\leq\Gamma_{\mathit{p}}$ (4)
$\displaystyle\Gamma^{\prime}_{\mathit{p}},\tau_{\mathit{p}}\leq\Gamma_{{\mathrm{1}}},\tau_{{\mathrm{1}}}$
(5)
$\displaystyle\Gamma^{\prime}_{\mathit{p}}=\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\tau^{\prime}_{\mathit{p}}]$
(6)
$\displaystyle\Gamma_{\mathit{p}}(\mathit{x})=\tau_{\mathit{p}}+\tau^{\prime}_{\mathit{p}}$
(7) $\displaystyle\vec{\ell}\vdash_{\mathit{WF}}\Gamma_{\mathit{p}}$ (8)

We first apply T-Sub with Equations 4 and 8, so it remains to show

$\Theta\mid\vec{\ell}\mid\Gamma_{\mathit{p}}[\mathit{x}:\tau_{\mathit{p}}+\tau^{\prime}_{\mathit{p}}]\vdash\operatorname{\mathbf{let}}\mathit{y}=\mathit{x}\operatorname{\mathbf{in}}\mathit{e}:\tau^{\prime}_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{1}}}$

which, by T-Let holds if we show that:

$\Theta\mid\vec{\ell}\mid\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\tau^{\prime}_{\mathit{p}}\wedge_{\mathit{x}}\mathit{x}=_{\tau^{\prime}_{\mathit{p}}}\mathit{y}],\mathit{y}:\tau_{\mathit{p}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{\mathit{p}}}\mathit{x}\vdash\mathit{e}:\tau^{\prime}_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{1}}}$

($\mathit{y}\not\in\mathit{dom}(\Gamma^{\prime}_{{\mathrm{1}}})$ follows from
Equation 3, and the well-formedness of
$\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\tau^{\prime}_{\mathit{p}}\wedge_{\mathit{x}}\mathit{x}=_{\tau^{\prime}_{\mathit{p}}}\mathit{y}],\mathit{y}:\tau_{\mathit{p}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{\mathit{p}}}\mathit{x}$
follows from the well-formedness of $\Gamma_{\mathit{p}}$, $\tau_{\mathit{p}}$
and $\tau^{\prime}_{\mathit{p}}$ and that $\mathit{x}$ and $\mathit{y}$ appear
in the refinements iff they are mapped to integer types in the new type
environment.)

We can use T-Sub to weaken the type environment to:

$\Theta\mid\vec{\ell}\mid\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\tau^{\prime}_{\mathit{p}}],\mathit{y}:\tau_{\mathit{p}}\vdash\mathit{e}:\tau^{\prime}_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{1}}}$

From Equation 5 above, we have that
$\Gamma_{\mathit{p}}[\mathit{x}\hookleftarrow\tau^{\prime}_{\mathit{p}}],\mathit{y}:\tau_{\mathit{p}}\leq\Gamma_{{\mathrm{1}}},\mathit{y}:\tau_{{\mathrm{1}}}$,
whereby one final application of T-Sub allows us to use to Equation 1 above.

###### Lemma 28

Let
$\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=\mathit{f}^{\ell}(\mathit{y_{{\mathrm{1}}}},\ldots,\mathit{y_{\mathit{n}}})\operatorname{\mathbf{in}}\mathit{e^{\prime}}]$
be a term such that:

Θ∣→ℓ∣Γ_0 ⊢letx = f ^ℓ( y_1 ,…, y_n ) ine’ : τ_1 ⇒Γ_1 σ_α = [ ℓ: →ℓ/ λ] Θ∣[]:
τ_1 ⇒Γ_1 ∣→ℓ⊢_ectx E : τ_2 ⇒Γ_2 σ_x = [ y_1 / x_1 ] ⋯[ y_n / x_n ] f ↦( x_1 ,
.. , x_n ) e ∈D Θ⊢f ↦( x_1 , .. , x_n ) e ⊢_WF Θ

where
$\Theta(\mathit{f})=\forall\lambda.\left\langle{\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau_{{\mathrm{1}}},\dots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau_{\mathit{n}}}\right\rangle\operatorname{\rightarrow}\left\langle{\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau^{\prime}_{{\mathrm{1}}},\dots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau^{\prime}_{\mathit{n}}\mid\tau_{\mathit{q}}}\right\rangle$.

Then there exist some $\tau_{{\mathrm{3}}}$ and $\Gamma_{{\mathrm{3}}}$:

$\displaystyle\Theta\mid\ell:\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\sigma_{x}\mathit{e}:\tau_{{\mathrm{3}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{3}}}$
$\displaystyle\Theta\mid[]:\tau_{{\mathrm{3}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{3}}}\mid\vec{\ell}\vdash_{\mathit{ectx}}\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=[]^{\ell}\operatorname{\mathbf{in}}\mathit{e}]:\tau_{{\mathrm{2}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}$

###### Proof

From Lemma 6 on
$\Theta\mid\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\operatorname{\mathbf{let}}\mathit{x}=\mathit{f}^{\ell}(\mathit{y_{{\mathrm{1}}}},\ldots,\mathit{y_{\mathit{n}}})\operatorname{\mathbf{in}}\mathit{e^{\prime}}:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}$
we have, for some
$\Gamma_{\mathit{p}},\tau_{\mathit{p}},\Gamma^{\prime}_{\mathit{p}}$, that:

$\displaystyle\Gamma_{{\mathrm{0}}}\leq\Gamma_{\mathit{p}}$ (9)
$\displaystyle\Gamma^{\prime}_{\mathit{p}},\tau_{\mathit{p}}\leq\Gamma_{{\mathrm{1}}},\tau_{{\mathrm{1}}}$
(10)
$\displaystyle\Gamma_{\mathit{p}}(\mathit{y_{\mathit{i}}})=\sigma_{\alpha}\,\sigma_{x}\,\tau_{\mathit{i}}$
(11) $\displaystyle\vec{\ell}\vdash_{\mathit{WF}}\Gamma_{\mathit{p}}$ (12)
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma_{\mathit{p}}[\mathit{y_{\mathit{i}}}\hookleftarrow\sigma_{\alpha}\,\sigma_{x}\,\tau^{\prime}_{\mathit{i}}],\mathit{x}:\sigma_{\alpha}\,\sigma_{x}\,\tau_{\mathit{q}}\vdash\mathit{e^{\prime}}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$
(13)
$\displaystyle\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime}_{\mathit{p}})$
(14)

To prove the first part, from the well-typing of the function body, we have
$\Theta\mid\lambda\mid\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau_{{\mathrm{1}}},\ldots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau_{\mathit{n}}\vdash\mathit{e}:\tau_{\mathit{q}}\operatorname{\Rightarrow}\mathit{x_{{\mathrm{1}}}}\operatorname{:}\tau^{\prime}_{{\mathrm{1}}},\ldots,\mathit{x_{\mathit{n}}}\operatorname{:}\tau^{\prime}_{\mathit{n}}$.
From our assumption that all variable names are distinct, by $n$ applications
of the substitution lemma (Lemma 10) we have:
$\Theta\mid\lambda\mid\mathit{y_{{\mathrm{1}}}}\operatorname{:}\sigma_{x}\,\tau_{{\mathrm{1}}},\ldots,\mathit{y_{\mathit{n}}}\operatorname{:}\sigma_{x}\,\tau_{\mathit{n}}\vdash\sigma_{x}\mathit{e}:\sigma_{x}\,\tau_{\mathit{q}}\operatorname{\Rightarrow}\mathit{y_{{\mathrm{1}}}}\operatorname{:}\sigma_{x}\,\tau^{\prime}_{{\mathrm{1}}},\ldots,\mathit{y_{\mathit{n}}}\operatorname{:}\sigma_{x}\,\tau^{\prime}_{\mathit{n}}$.
By Lemma 9 (part 5) we then have
$\Theta\mid\ell:\vec{\ell}\mid\mathit{y_{{\mathrm{1}}}}\operatorname{:}\sigma_{\alpha}\,\sigma_{x}\,\tau_{{\mathrm{1}}},\ldots,\mathit{y_{\mathit{n}}}\operatorname{:}\sigma_{\alpha}\,\sigma_{x}\,\tau_{\mathit{n}}\vdash\sigma_{x}\mathit{e}:\sigma_{\alpha}\,\sigma_{x}\,\tau_{\mathit{q}}\operatorname{\Rightarrow}\mathit{y_{{\mathrm{1}}}}\operatorname{:}\sigma_{\alpha}\,\sigma_{x}\,\tau^{\prime}_{{\mathrm{1}}},\ldots,\mathit{y_{\mathit{n}}}\operatorname{:}\sigma_{\alpha}\,\sigma_{x}\,\tau^{\prime}_{\mathit{n}}$.
We take $\tau_{{\mathrm{3}}}=\sigma_{\alpha}\,\sigma_{x}\,\tau_{\mathit{q}}$
and
$\Gamma_{{\mathrm{3}}}=\Gamma_{\mathit{p}}[\mathit{y_{\mathit{i}}}\hookleftarrow\sigma_{\alpha}\,\sigma_{x}\,\tau^{\prime}_{\mathit{i}}]$.

By the well-formedness of function types and well-formedness of
$\Gamma_{\mathit{p}}$, we must have that
$\ell:\vec{\ell}\vdash_{\mathit{WF}}\Gamma_{{\mathrm{3}}}$. Then by Equations
11, 12 and 26 we have
$\Theta\mid\ell:\vec{\ell}\mid\Gamma_{\mathit{p}}\vdash\sigma_{x}\mathit{e}:\tau_{{\mathrm{3}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{3}}}$,
whereby Equation 9 and an application of T-Sub gives
$\Theta\mid\ell:\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\sigma_{x}\mathit{e}:\tau_{{\mathrm{3}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{3}}}$,
i.e., the first result.

To prove the second part, from the typing rule for TE-Stack we must show:

$\displaystyle\Theta\mid[]:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}\mid\vec{\ell}\vdash_{\mathit{ectx}}\mathit{E}:\tau_{{\mathrm{2}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{2}}}$
(15) $\displaystyle\mathit{x}\not\in\mathit{dom}(\Gamma_{{\mathrm{1}}})$ (16)
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma_{{\mathrm{3}}},\mathit{x}:\tau_{{\mathrm{3}}}\vdash\mathit{e^{\prime}}:\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}$
(17)

Equation 15 holds by assumption, and Equation 16 follows from Equation 14 and
that $\Gamma^{\prime}_{\mathit{p}}\leq\Gamma_{{\mathrm{1}}}$ implies
$\mathit{dom}(\Gamma_{{\mathrm{1}}})\subseteq\mathit{dom}(\Gamma^{\prime}_{\mathit{p}})$.
$\vec{\ell}\vdash_{\mathit{WF}}\tau_{{\mathrm{1}}}\operatorname{\Rightarrow}\Gamma_{{\mathrm{1}}}$
follows from the well-typing of the function call term, and
$\vec{\ell}\vdash_{\mathit{WF}}\Gamma_{{\mathrm{3}}},\mathit{x}:\tau_{{\mathrm{3}}}$
follows from Equation 13.

From Equations 10 and 13 we then have Equation 17 via an application of T-Sub.

######  Proof (Preservation; Lemma 3)

The proof is organized by cases analysis on the transition rule used of
$\mathit{e}$, and showing that the output configuration is well typed by
$\vdash_{\mathit{conf}}^{D}$. We must therefore find a $\Gamma^{\prime\prime}$
that is consistent with $\mathit{H^{\prime}}$ and $\mathit{R^{\prime}}$ and
also satisfies the other conditions imposed by the definition of
$\vdash_{\mathit{conf}}^{D}$. Here
$\Gamma^{\prime\prime},\mathit{H^{\prime}},\mathit{R^{\prime}}$ represent the
type environment, heap and register after the transition respectively. We
identify the heap and register file before transition with $\mathit{H}$ and
$\mathit{R}$ respectively. In order to show that the ownership invariant is
preserved, we need to prove that
$\forall\,\mathit{a}\in\mathit{dom}(\mathit{H}).\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma^{\prime\prime})(\mathit{a})\leq
1$. In many cases, we will show that
$\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)=\mathbf{Own}\,(\mathit{H^{\prime}},\mathit{R^{\prime}},\Gamma^{\prime\prime})$,
whereby from the assumption that
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$ as implied by
$\vdash_{\mathit{conf}}^{D}$ we have
$\forall\,\mathit{a}\in\mathit{dom}(\mathit{H}).\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)(\mathit{a})\leq
1$, giving the desired result.

Case R-Var:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},F_{{\mathit{n}-1}}:\vec{F},\mathit{x}}\right\rangle,\left\langle{\mathit{H},\mathit{R},F_{{\mathit{n}-1}}:\vec{F},\mathit{x}}\right\rangle\longrightarrow_{\mathit{D}}\left\langle{\mathit{H},\mathit{R},\vec{F},F_{{\mathit{n}-1}}[\mathit{x}]}\right\rangle\\\
\end{array}$
By inversion on configuration typing
$\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},F_{{\mathit{n}-1}}:\vec{F},\mathit{x}}\right\rangle$,
we have:

$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma\vdash\mathit{x}:\tau_{\mathit{n}}\operatorname{\Rightarrow}\Gamma_{\mathit{n}}$
$\displaystyle\forall
i\in\left\\{{1..n}\right\\}.\Theta\mid[]:\tau_{\mathit{i}}\operatorname{\Rightarrow}\Gamma_{\mathit{i}}\mid\vec{\ell}_{{\mathit{i}-1}}\vdash_{\mathit{ectx}}F_{{\mathit{i}-1}}:\tau_{{\mathit{i}-1}}\operatorname{\Rightarrow}\Gamma_{{\mathit{i}-1}}$

Using Lemma 27, we can conclude that
$\Theta\mid\vec{\ell}_{{\mathit{n}-1}}\mid\Gamma\vdash
F_{{\mathit{n}-1}}[\mathit{x}]:\tau_{{\mathit{n}-1}}\operatorname{\Rightarrow}\Gamma_{{\mathit{n}-1}}$.
We therefore take $\Gamma^{\prime\prime}=\Gamma$.

It remains to show that
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma^{\prime\prime})$ which follows
immediately from $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$.

Case R-Deref:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=*\mathit{y}\operatorname{\mathbf{in}}\mathit{e}]}\right\rangle\\\
\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=*\mathit{y}\operatorname{\mathbf{in}}\mathit{e}]}\right\rangle\longrightarrow_{\mathit{D}}\left\langle{\mathit{H},\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{v}\\},\vec{F},\mathit{E}[[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}]}\right\rangle\\\
\mathit{H}(\mathit{a})\,=\,\mathit{v}\quad\quad\mathit{R}(\mathit{y})\,=\,\mathit{a}\quad\quad\mathit{R^{\prime}}=\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{v}\\}\\\
\end{array}$
By inversion on the configuration typing relationship, we have that:

$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=*\mathit{y}\operatorname{\mathbf{in}}\mathit{e}]:\tau_{\mathit{n}}\operatorname{\Rightarrow}\Gamma_{\mathit{n}}$
$\displaystyle\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma_{{\mathrm{0}}})$

By Lemma 7, we have some $\tau,\Gamma^{\prime}_{{\mathrm{0}}}$ such that:

$\displaystyle\Theta\mid[]:\tau\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{0}}}\mid\vec{\ell}\vdash_{\mathit{ectx}}\mathit{E}:\tau_{\mathit{n}}\operatorname{\Rightarrow}\Gamma_{\mathit{n}}$
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma_{{\mathrm{0}}}\vdash\operatorname{\mathbf{let}}\mathit{x}=*\mathit{y}\operatorname{\mathbf{in}}\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{0}}}$

Using Lemma 6, we have some $\Gamma_{\mathit{p}}$,
$\Gamma^{\prime}_{\mathit{p}}$ and $\tau_{\mathit{p}}$ such that:

$\displaystyle\Gamma_{{\mathrm{0}}}\leq\Gamma_{\mathit{p}}\quad\quad\vec{\ell}\vdash_{\mathit{WF}}\Gamma_{\mathit{p}}\quad\quad\Gamma^{\prime}_{\mathit{p}},\tau_{\mathit{p}}\leq\Gamma^{\prime}_{{\mathrm{0}}},\tau$
$\displaystyle\Gamma_{\mathit{p}}(\mathit{y})=(\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})\operatorname{\mathbf{ref}}^{r}\quad\quad\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime}_{\mathit{p}})$
$\displaystyle\tau^{\prime\prime}=\begin{cases}(\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{1}}}}\mathit{x})&r>0\\\
\tau_{{\mathrm{1}}}&r=0\end{cases}$
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma_{\mathit{p}}[\mathit{y}\hookleftarrow\tau^{\prime\prime}\operatorname{\mathbf{ref}}^{r}],\mathit{x}:\tau_{{\mathrm{2}}}\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$

From Lemma 12, we then have
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma_{\mathit{p}})$. We will now show
that:

$\displaystyle\mathbf{Cons}\,(\mathit{H},\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{v}\\},\Gamma^{\prime\prime})$
(18)
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}:[\mathit{x^{\prime}}/\mathit{x}]\,\tau_{\mathit{p}}\operatorname{\Rightarrow}[\mathit{x^{\prime}}/\mathit{x}]\,\Gamma^{\prime}_{\mathit{p}}$
(19)

where
$\Gamma^{\prime\prime}=\Gamma_{\mathit{p}}[\mathit{y}\hookleftarrow([\mathit{x^{\prime}}/\mathit{x}]\,\tau^{\prime\prime})\operatorname{\mathbf{ref}}^{r}],\mathit{x^{\prime}}:\tau_{{\mathrm{2}}}$.

Together these give our desired result. To see how, from
$\Theta\mid\vec{\ell}\mid\Gamma_{\mathit{p}}[\mathit{y}\hookleftarrow\tau^{\prime\prime}\operatorname{\mathbf{ref}}^{r}],\mathit{x}:\tau_{{\mathrm{2}}}\vdash\mathit{e}:\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$
above, we must have that
$\vec{\ell}\vdash_{\mathit{WF}}\tau_{\mathit{p}}\operatorname{\Rightarrow}\Gamma^{\prime}_{\mathit{p}}$.
From $\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime}_{\mathit{p}})$ we must
therefore have that
$[\mathit{x^{\prime}}/\mathit{x}]\,\tau_{\mathit{p}}=\tau_{\mathit{p}}$ and
$[\mathit{x^{\prime}}/\mathit{x}]\,\Gamma^{\prime}_{\mathit{p}}=\Gamma^{\prime}_{\mathit{p}}$.
As
$\Gamma^{\prime}_{\mathit{p}},\tau_{\mathit{p}}\leq\Gamma^{\prime}_{{\mathrm{0}}},\tau$
an application of T-Sub gives
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}_{{\mathrm{0}}}$.
Then Lemma 8 will give that
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash\mathit{E}[[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}]:\tau_{\mathit{n}}\operatorname{\Rightarrow}\Gamma_{\mathit{n}}$.

As $\mathit{E}$ and the stack $\vec{F}$ remained unchanged, combined with
Equation 18 this gives
$\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{v}\\},\vec{F},\mathit{E}[[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}]}\right\rangle$
as required. As the above argument is used almost completely unchanged in all
of the following cases, we will invert the redex without regard for the T-Sub
rule, with the understanding that the subtyping rule is handled with an
argument identical to the above.

We now show that
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}:[\mathit{x}/\mathit{x^{\prime}}]\,\tau_{\mathit{p}}\operatorname{\Rightarrow}[\mathit{x^{\prime}}/\mathit{x}]\,\Gamma^{\prime}$
and
$\mathbf{Cons}\,(\mathit{H},\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{v}\\},\Gamma^{\prime\prime})$.
The first is easy to obtain using Lemma 10; from
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$, we have that
$\forall\,\mathit{x}\in\mathit{dom}(\Gamma).\mathit{x}\in\mathit{dom}(\mathit{R})$,
whereby from $\mathit{x}\not\in\mathit{dom}(\mathit{R})$ we have
$\mathit{x^{\prime}}\not\in\mathit{dom}(\Gamma)$. It therefore remains to show
$\mathbf{Cons}\,(\mathit{H},\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{v}\\},\Gamma^{\prime\prime})$.

To show $\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma^{\prime\prime})$, it
suffices to show that
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\tau_{{\mathrm{2}}})$
and
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{H}(\mathit{R^{\prime}}(\mathit{y})),\tau^{\prime\prime})$
(that $\mathbf{SATv}$ holds for all other variables $\mathit{z}$ follows from
$\Gamma(\mathit{z})=\Gamma^{\prime\prime}(\mathit{z})$ and Lemmas 17 and 23).
If $\tau_{{\mathrm{1}}}$ is an integer type and $r>0$, then by the definition
of the strengthening operator, the latter is equivalent to show that
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{H}(\mathit{R^{\prime}}(\mathit{y})),\tau_{{\mathrm{1}}})$
and that
$\mathit{R^{\prime}}(\mathit{x^{\prime}})=\mathit{H}(\mathit{R^{\prime}}(\mathit{y}))=\mathit{H}(\mathit{R}(\mathit{y}))$,
which is immediate from the definition of R-Deref. If $\tau_{{\mathrm{1}}}$ is
not an integer or if $r=0$, then we must only show that
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{H}(\mathit{R^{\prime}}(\mathit{y})),\tau_{{\mathrm{1}}})$.

From $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma_{\mathit{p}})$, we know
that $\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma_{\mathit{p}})$, in
particular,
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{R}(\mathit{y}),\Gamma_{\mathit{p}}(\mathit{y}))$.
Then by Lemmas 16, 17 and 23, from $\mathit{R}\sqsubseteq\mathit{R^{\prime}}$,
$\vec{\ell}\vdash_{\mathit{WF}}\Gamma_{\mathit{p}}$, and
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$
we obtain that
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{v},\tau_{{\mathrm{1}}})$
and
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{v},\tau_{{\mathrm{2}}})$,
where $\mathit{v}\,=\,\mathit{H}(\mathit{R}(\mathit{y}))$. We thus have that
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\tau_{{\mathrm{2}}})$
and
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{H}(\mathit{R^{\prime}}(\mathit{y})),\tau_{{\mathrm{1}}})$
are satisfied.

We must also show that the ownership invariant is preserved. Then, it’s to
show
$\forall\,\mathit{a}\in\mathit{dom}(\mathit{H}).\mathbf{Own}\,(\mathit{H},\mathit{R^{\prime}},\Gamma^{\prime\prime})(\mathit{a})\leq
1$. Define $\mathit{O^{\prime}_{{\mathrm{0}}}}$ and
$\mathit{O^{\prime}_{{\mathrm{1}}}}$ as follows:

$\displaystyle\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma_{\mathit{p}})$
$\displaystyle=\mathit{O^{\prime}_{{\mathrm{0}}}}+\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{y}),\Gamma_{\mathit{p}}(\mathit{y}))$
$\displaystyle\mathbf{Own}\,(\mathit{H},\mathit{R^{\prime}},\Gamma^{\prime\prime})$
$\displaystyle=\mathit{O^{\prime}_{{\mathrm{1}}}}+\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{y}),\Gamma^{\prime\prime}(\mathit{y}))+\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\Gamma^{\prime\prime}(\mathit{x^{\prime}}))$
$\displaystyle\mathit{O^{\prime}_{{\mathrm{0}}}}$
$\displaystyle=\Sigma_{\mathit{z}\in\mathit{dom}(\Gamma)\setminus\left\\{{\mathit{y}}\right\\}}\,\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{z}),\Gamma_{\mathit{p}}(\mathit{z}))$
$\displaystyle\mathit{O^{\prime}_{{\mathrm{1}}}}$
$\displaystyle=\Sigma_{\mathit{z}\in\mathit{dom}(\Gamma^{\prime\prime})\setminus\\{\mathit{y},\mathit{x^{\prime}}\\}}\,\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{z^{\prime}}),\Gamma^{\prime\prime}(\mathit{z^{\prime}}))$

By Lemma 19,
$\mathit{O^{\prime}_{{\mathrm{0}}}}=\mathit{O^{\prime}_{{\mathrm{1}}}}$ holds.
Then, it suffices to show that
$\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{y}),\Gamma_{\mathit{p}}(\mathit{y}))=\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{y}),\Gamma^{\prime\prime}(\mathit{y}))+\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\Gamma^{\prime\prime}(\mathit{x^{\prime}}))$.

As
$\mathit{R^{\prime}}(\mathit{x^{\prime}})=\mathit{H}(\mathit{R^{\prime}}(\mathit{y}))=\mathit{H}(\mathit{R}(\mathit{y}))$
and from the definition of $\Gamma^{\prime\prime}$, we have:

$\displaystyle\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\Gamma^{\prime\prime}(\mathit{x^{\prime}}))$
$\displaystyle=\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{R}(\mathit{y})),\tau_{{\mathrm{2}}})$
$\displaystyle\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{y}),\Gamma^{\prime\prime}(\mathit{y}))$
$\displaystyle=\\{\mathit{a}\mapsto
r\\}+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{R}(\mathit{y})),\tau_{{\mathrm{1}}})$

From the definition of the ownership function, we have that

$\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{y}),\Gamma_{\mathit{p}}(\mathit{y}))=\\{\mathit{a}\mapsto
r\\}+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{R}(\mathit{y})),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$

which, by Lemma 15, is equivalent to:

$\\{\mathit{a}\mapsto
r\\}+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{R}(\mathit{y})),\tau_{{\mathrm{1}}})+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{R}(\mathit{y})),\tau_{{\mathrm{2}}})$

We therefore have
$\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{y}),\Gamma(\mathit{y}))=\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{y}),\Gamma^{\prime\prime}(\mathit{y}))+\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\Gamma^{\prime\prime}(\mathit{x^{\prime}}))$,
and conclude that
$\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)=\mathbf{Own}\,(\mathit{H},\mathit{R^{\prime}},\Gamma^{\prime\prime})$.

Case R-Seq:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\mathit{x}\operatorname{;}\mathit{e}]}\right\rangle\\\
\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\mathit{x}\operatorname{;}\mathit{e}]}\right\rangle\longrightarrow_{\mathit{D}}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\mathit{e}]}\right\rangle\\\
\end{array}$
By inversion (see R-Deref) we have for some $\Gamma$ that:

$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma[\mathit{x}:\tau_{{\mathrm{0}}}+\tau_{{\mathrm{1}}}]\vdash\mathit{x}:\tau_{{\mathrm{0}}}\operatorname{\Rightarrow}\Gamma[\mathit{x}\hookleftarrow\tau_{{\mathrm{1}}}]$
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma[\mathit{x}\hookleftarrow\tau_{{\mathrm{1}}}]\vdash\mathit{e}:\tau^{\prime}\operatorname{\Rightarrow}\Gamma^{\prime}$
$\displaystyle\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$

We take
$\Gamma^{\prime\prime}=\Gamma[\mathit{x}\hookleftarrow\tau_{{\mathrm{1}}}]$.

It suffices to show (see R-Deref) that
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash\mathit{e}:\tau^{\prime}\operatorname{\Rightarrow}\Gamma^{\prime}$,
and $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma^{\prime\prime})$. The first
is immediate from the inversion above, and
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma^{\prime\prime})$ follows from
Lemmas 15 and 16.

Case R-Let:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=\mathit{y}\operatorname{\mathbf{in}}\mathit{e}]}\right\rangle\\\
\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=\mathit{y}\operatorname{\mathbf{in}}\mathit{e}]}\right\rangle\longrightarrow_{\mathit{D}}\left\langle{\mathit{H},\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{R}(\mathit{y})\\},\vec{F},\mathit{E}[[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}]}\right\rangle\\\
\mathit{x^{\prime}}\not\in\mathit{dom}(\mathit{R})\quad\quad\mathit{R^{\prime}}=\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{R}(\mathit{y})\\}\end{array}$
By inversion (see R-Deref) we have that for some $\Gamma$ that:

$\displaystyle\vec{\ell}\vdash_{\mathit{WF}}\Gamma$
$\displaystyle\Gamma(\mathit{y})=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma[\mathit{y}\hookleftarrow\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{1}}}}\mathit{x}],\mathit{x}:(\tau_{{\mathrm{2}}}\wedge_{\mathit{x}}\mathit{x}=_{\tau_{{\mathrm{2}}}}\mathit{y})\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
$\displaystyle\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)\quad\quad\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime})$

We give
$\Gamma^{\prime\prime}=\Gamma[\mathit{y}\hookleftarrow\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{1}}}}\mathit{x^{\prime}}],\mathit{x^{\prime}}:(\tau_{{\mathrm{2}}}\wedge_{\mathit{x^{\prime}}}\mathit{x^{\prime}}=_{\tau_{{\mathrm{2}}}}\mathit{y})$.

It suffices to show (see R-Deref) that
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
and
$\mathbf{Cons}\,(\mathit{H},\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{R}(\mathit{y})\\},\Gamma^{\prime\prime})$.
The first is easy to obtain using reasoning as in the R-Deref case. It
therefore remains to show
$\mathbf{Cons}\,(\mathit{H},\mathit{R^{\prime}},\Gamma^{\prime\prime})$.

To show that the output environment is consistent, we must show that
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\tau_{{\mathrm{2}}}\wedge_{\mathit{x^{\prime}}}\mathit{x^{\prime}}\,=\,\mathit{y})$
and
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{y}),\tau_{{\mathrm{1}}}\wedge_{\mathit{y}}\mathit{y}\,=\,\mathit{x^{\prime}})$.
By reasoning similar to that in R-Deref, it suffices to show that
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\tau_{{\mathrm{2}}})$
and
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{y}),\tau_{{\mathrm{1}}})$.
We know that $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$, from which me
have $\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma)$, in particular
$\mathit{y}\in\mathit{dom}(\mathit{R})$ and
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{R}(\mathit{y}),\Gamma(\mathit{y}))$.
As $\mathit{R}\sqsubseteq\mathit{R^{\prime}}$ and
$\vec{\ell}\vdash_{\mathit{WF}}\Gamma$, from Lemmas 16, 17 and 23, we obtain
from
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{v},\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$
that
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{v},\tau_{{\mathrm{1}}})$
and
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{v},\tau_{{\mathrm{2}}})$
where $v=R(y)$. We then have
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\tau_{{\mathrm{2}}})$
and
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{y}),\tau_{{\mathrm{1}}})$
are satisfied.

We must also show that the ownership invariant is preserved. Then, it’s to
show
$\forall\,\mathit{a}\in\mathit{dom}(\mathit{H}).\mathbf{Own}\,(\mathit{H},\mathit{R^{\prime}},\Gamma^{\prime\prime})(\mathit{a})\leq
1$. Define $\mathit{O^{\prime}_{{\mathrm{0}}}}$ and
$\mathit{O^{\prime}_{{\mathrm{1}}}}$ as follows:

$\displaystyle\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)$
$\displaystyle=\mathit{O^{\prime}_{{\mathrm{0}}}}+\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{y}),\Gamma(\mathit{y}))$
$\displaystyle\mathbf{Own}\,(\mathit{H},\mathit{R^{\prime}},\Gamma^{\prime\prime})$
$\displaystyle=\mathit{O^{\prime}_{{\mathrm{1}}}}+\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{y}),\Gamma^{\prime\prime}(\mathit{y}))+\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\Gamma^{\prime\prime}(\mathit{x^{\prime}}))$
$\displaystyle\mathit{O^{\prime}_{{\mathrm{0}}}}$
$\displaystyle=\Sigma_{\mathit{z}\in\mathit{dom}(\Gamma)\setminus\left\\{{\mathit{y}}\right\\}}\,\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{z}),\Gamma(\mathit{z}))$
$\displaystyle\mathit{O^{\prime}_{{\mathrm{1}}}}$
$\displaystyle=\Sigma_{\mathit{z}\in\mathit{dom}(\Gamma^{\prime\prime})\setminus\\{\mathit{y},\mathit{x^{\prime}}\\}}\,\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{z^{\prime}}),\Gamma^{\prime\prime}(\mathit{z^{\prime}}))$

By Lemma 19,
$\mathit{O^{\prime}_{{\mathrm{0}}}}=\mathit{O^{\prime}_{{\mathrm{1}}}}$ holds.
That
$\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\tau_{{\mathrm{2}}})+\mathbf{own}\,(\mathit{H},\mathit{R^{\prime}}(\mathit{y}),\tau_{{\mathrm{1}}})=\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{y}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$
follows immediately from Lemma 15 and the condition
$\mathit{R}(\mathit{y})=\mathit{R^{\prime}}(\mathit{x^{\prime}})=\mathit{R^{\prime}}(\mathit{y})$.
We therefore conclude that
$\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)=\mathbf{Own}\,(\mathit{H},\mathit{R^{\prime}},\Gamma^{\prime\prime})$.

Case R-LetInt:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=n\operatorname{\mathbf{in}}\mathit{e}]}\right\rangle\\\
\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=n\operatorname{\mathbf{in}}\mathit{e}]}\right\rangle\longrightarrow_{\mathit{D}}\left\langle{\mathit{H},\mathit{R}\\{\mathit{x^{\prime}}\mapsto
n\\},\vec{F},\mathit{E}[[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}]}\right\rangle\end{array}$
By inversion (see R-Deref) we have that, for some $\Gamma$:

$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma,\mathit{x}:\left\\{{\nu\operatorname{:}\mathbf{int}\mid\nu\,=\,n}\right\\}\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
$\displaystyle\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)\quad\quad\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime})$

We give that
$\Gamma^{\prime\prime}=\Gamma,\mathit{x^{\prime}}:\left\\{{\nu\operatorname{:}\mathbf{int}\mid\nu\,=\,n}\right\\}$,
and it thus suffices to show that
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
and $\mathbf{Cons}\,(\mathit{H},\mathit{R}\\{\mathit{x^{\prime}}\mapsto
n\\},\Gamma^{\prime\prime})$. The first one is easy to obtain using the Lemma
10 (see R-Deref) and the latter is trivial by similar reasoning to the T-Let
and T-Deref cases.

Case R-IfTrue:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{ifz}}\mathit{y}\operatorname{\mathbf{then}}\mathit{e_{{\mathrm{1}}}}\operatorname{\mathbf{else}}\mathit{e_{{\mathrm{2}}}}]}\right\rangle\\\
\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{ifz}}\mathit{y}\operatorname{\mathbf{then}}\mathit{e_{{\mathrm{1}}}}\operatorname{\mathbf{else}}\mathit{e_{{\mathrm{2}}}}]}\right\rangle\longrightarrow_{\mathit{D}}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\mathit{e_{{\mathrm{1}}}}]}\right\rangle\end{array}$
By inversion (see R-Deref) we have that for some $\Gamma$:

$\displaystyle\Gamma(\mathit{x})=\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi}\right\\}$
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma[\mathit{x}\hookleftarrow\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi\wedge\nu\,=\,0}\right\\}]\vdash\mathit{e_{{\mathrm{1}}}}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
$\displaystyle\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$

We take
$\Gamma^{\prime\prime}=\Gamma[\mathit{x}\hookleftarrow\left\\{{\nu\operatorname{:}\mathbf{int}\mid\varphi\wedge\nu\,=\,0}\right\\}]$,
and want to show that
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma^{\prime\prime})$ (that
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash\mathit{e_{{\mathrm{1}}}}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
is immediate).

By definition, from $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$ we have
$\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma)$, in particular
$\mathit{x}\in\mathit{dom}(\mathit{R})$, $\mathit{R}(\mathit{x})\in\mathbb{Z}$
and $[\mathit{R}]\,[\mathit{R}(\mathit{x})/\nu]\varphi$. The refinement
predicates $\varphi$ still holds in the output environment, since nothing
changes in the register after transition. Also from precondition of R-IfTrue,
we have $\mathit{R}(\mathit{x})\,=\,0$, thus $\mathit{x}$ satisfies the
refinement that $\nu\,=\,0$. Thus
$[\mathit{R}]\,[\mathit{R}(\mathit{x})/\nu](\varphi\wedge\nu\,=\,0)$ is
trivially satisfied.

Case R-IfFalse:
Similar to the case for R-IfTrue.

Case R-MkRef:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=\operatorname{\mathbf{mkref}}\mathit{y}\operatorname{\mathbf{in}}\mathit{e}]}\right\rangle\\\
\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\operatorname{\mathbf{let}}\mathit{x}=\operatorname{\mathbf{mkref}}\mathit{y}\operatorname{\mathbf{in}}\mathit{e}]}\right\rangle\longrightarrow_{\mathit{D}}\left\langle{\mathit{H^{\prime}},\mathit{R^{\prime}},\vec{F},\mathit{E}[[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}]}\right\rangle\\\
\mathit{a}\not\in\mathit{dom}(\mathit{H})\quad\quad\mathit{x^{\prime}}\not\in\mathit{dom}(\mathit{R})\\\
\mathit{H^{\prime}}=\mathit{H}\\{\mathit{a}\mapsto\mathit{R}(\mathit{y})\\}\quad\quad\mathit{R^{\prime}}=\mathit{R}\\{\mathit{x^{\prime}}\mapsto\mathit{a}\\}\end{array}$
By inversion (see R-Deref) we have that for some $\Gamma$:

$\displaystyle\vec{\ell}\vdash_{\mathit{WF}}\Gamma$
$\displaystyle\Gamma(\mathit{y})=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma[\mathit{y}\hookleftarrow\tau_{{\mathrm{1}}}],\mathit{x}:(\tau_{{\mathrm{2}}}\wedge_{\mathit{x}}\mathit{x}\,=\,\mathit{y})\operatorname{\mathbf{ref}}^{1}\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
$\displaystyle\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)\quad\quad\mathit{x}\not\in\mathit{dom}(\Gamma^{\prime})$

We give
$\Gamma^{\prime\prime}=\Gamma[\mathit{y}\hookleftarrow\tau_{{\mathrm{1}}}],\mathit{x^{\prime}}:(\tau_{{\mathrm{2}}}\wedge_{\mathit{x^{\prime}}}\mathit{x^{\prime}}\,=\,\mathit{y})\operatorname{\mathbf{ref}}^{1}$,
and must show that
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash[\mathit{x^{\prime}}/\mathit{x}]\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
and
$\mathbf{Cons}\,(\mathit{H^{\prime}},\mathit{R^{\prime}},\Gamma^{\prime\prime})$.
The first follows from Lemma 10 and the reasoning found in R-Deref, and the
second from the assumed well-formedness of
$\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$.

It remains to show
$\mathbf{Cons}\,(\mathit{H^{\prime}},\mathit{R^{\prime}},\Gamma^{\prime\prime})$.
To show that the output environment is consistent, we must show that
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{x^{\prime}}),(\tau_{{\mathrm{2}}}\wedge_{\mathit{x^{\prime}}}\mathit{x^{\prime}}\,=\,\mathit{y})\operatorname{\mathbf{ref}}^{1})$
and
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{y}),\tau_{{\mathrm{1}}})$.
By reasoning similar to that in R-Deref, it suffices to show that
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{1})$
and
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{y}),\tau_{{\mathrm{1}}})$.
We know that $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$, from which we
have $\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma)$, in particular
$\mathit{y}\in\mathit{dom}(\mathit{R})$ and
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{R}(\mathit{y}),\Gamma(\mathit{y}))$.
As $\mathit{R}\sqsubseteq\mathit{R^{\prime}}$ and
$\vec{\ell}\vdash_{\mathit{WF}}\Gamma$, from Lemmas 23 and 17, we have
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{R}(\mathit{y}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$
implies
$\mathbf{SATv}(\mathit{H},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{y}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$.
By Lemma 24, we then have
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R^{\prime}},\mathit{R}(\mathit{y}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$.
Then by Lemma 16, we have
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R^{\prime}},\mathit{v},\tau_{{\mathrm{1}}})$
and
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R^{\prime}},\mathit{v},\tau_{{\mathrm{2}}})$
where $\mathit{v}\,=\,\mathit{R}(\mathit{y})$. We then have
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{x^{\prime}}),\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{1})$
and
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R^{\prime}},\mathit{R^{\prime}}(\mathit{y}),\tau_{{\mathrm{1}}})$
are satisfied.

We must also show that the ownership invariant is preserved. Then, it’s to
show
$\forall\,\mathit{a^{\prime}}\in\mathit{dom}(\mathit{H}).\mathbf{Own}\,(\mathit{H^{\prime}},\mathit{R^{\prime}},\Gamma^{\prime\prime})(\mathit{a^{\prime}})\leq
1$. From $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$ and Lemmas 25 and 15
we have:

$\displaystyle\mathbf{Own}\,(\mathit{H^{\prime}},\mathit{R^{\prime}},\Gamma^{\prime\prime})$
$\displaystyle=\Sigma_{\mathit{z}\in\mathit{dom}(\Gamma^{\prime\prime})}\,\mathbf{own}\,(\mathit{H^{\prime}},\mathit{R^{\prime}}(\mathit{z}),\Gamma^{\prime\prime}(\mathit{z}))$
$\displaystyle=\Sigma_{\mathit{z}\in\mathit{dom}(\Gamma)}\,\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{z}),\Gamma(\mathit{z}))+\\{\mathit{a}\mapsto
1\\}$
$\displaystyle=\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)+\\{\mathit{a}\mapsto
1\\}$

Since $\mathit{a}\not\in\mathit{dom}(\mathit{H})$ and
$\forall\,\mathit{a^{\prime}}\in\mathit{dom}(\mathit{H}).\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)(\mathit{a^{\prime}})\leq
1$, we have
$\forall\,\mathit{a^{\prime}}\in\mathit{dom}(\mathit{H}).\mathbf{Own}\,(\mathit{H^{\prime}},\mathit{R^{\prime}},\Gamma^{\prime\prime})(\mathit{a^{\prime}})\leq
1$.

Case R-Assign:
$\quad\begin{array}[t]{@{}l@{\qquad}l@{\qquad}l@{\qquad}l}\vdash_{\mathit{conf}}^{D}\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\mathit{y}\operatorname{:=}\mathit{x}\operatorname{;}\mathit{e}]}\right\rangle\\\
\left\langle{\mathit{H},\mathit{R},\vec{F},\mathit{E}[\mathit{y}\operatorname{:=}\mathit{x}\operatorname{;}\mathit{e}]}\right\rangle\longrightarrow_{\mathit{D}}\left\langle{\mathit{H^{\prime}},\mathit{R^{\prime}},\vec{F},\mathit{E}[\mathit{e}]}\right\rangle\\\
\mathit{a}\,=\,\mathit{R}(\mathit{y})\quad\quad\mathit{H^{\prime}}=\mathit{H}\\{\mathit{a}\hookleftarrow\mathit{R}(\mathit{x})\\}\quad\quad\mathit{R^{\prime}}=\mathit{R}\end{array}$
By inversion (see the R-Deref case) we have that

$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma[\mathit{x}:\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}][\mathit{y}:\tau^{\prime}\operatorname{\mathbf{ref}}^{1}]\vdash\mathit{y}\operatorname{:=}\mathit{x}\operatorname{;}\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
$\displaystyle\Theta\mid\vec{\ell}\mid\Gamma[\mathit{x}\hookleftarrow\tau_{{\mathrm{1}}}][\mathit{y}\hookleftarrow(\tau_{{\mathrm{2}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{2}}}}\mathit{x})\operatorname{\mathbf{ref}}^{1}]\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
$\displaystyle\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$

We give
$\Gamma^{\prime\prime}=\Gamma[\mathit{x}\hookleftarrow\tau_{{\mathrm{1}}}][\mathit{y}\hookleftarrow(\tau_{{\mathrm{2}}}\wedge_{\mathit{y}}\mathit{y}=_{\tau_{{\mathrm{2}}}}\mathit{x})\operatorname{\mathbf{ref}}^{1}]$.
That
$\Theta\mid\vec{\ell}\mid\Gamma^{\prime\prime}\vdash\mathit{e}:\tau\operatorname{\Rightarrow}\Gamma^{\prime}$
is immediate.

We must therefore show that
$\mathbf{Cons}\,(\mathit{H^{\prime}},\mathit{R^{\prime}},\Gamma^{\prime\prime})$.
To show that the output environment is consistent, we must show that
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{R}(\mathit{y}),(\tau_{{\mathrm{2}}}\wedge_{\mathit{y}}\mathit{y}\,=\,\mathit{x})\operatorname{\mathbf{ref}}^{1})$
and
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}})$.
By reasoning similar to that in R-Deref, it suffices to show that
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{R}(\mathit{y}),\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{1})$
and
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}})$.

From $\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$, we know that
$\mathbf{SAT}\,(\mathit{H},\mathit{R},\Gamma)$, in particular,
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{R}(\mathit{x}),\Gamma(\mathit{x}))$.
If we show that
$\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})(\mathit{a})=0$
and $\mathit{H}\approx_{\mathit{a}}\mathit{H^{\prime}}$, then, by Lemma 22, we
will obtain
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$,
from which, by Lemma 16,
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}})$
and
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{R}(\mathit{x}),\tau_{{\mathrm{2}}})$
follow. We then have
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{R}(\mathit{y}),\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{1})$
and
$\mathbf{SATv}(\mathit{H^{\prime}},\mathit{R},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}})$
as $\mathit{H^{\prime}}(\mathit{R}(\mathit{y}))\,=\,\mathit{R}(\mathit{x})$.
(That any other variables $\mathit{z}$ is consistent will follow from
$\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{z}),\Gamma(\mathit{z}))(\mathit{a})=0$
as proved below and lemma 22.)

To show
$\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})(\mathit{a})=0$,
we define
$\mathit{O^{\prime}_{{\mathrm{0}}}},\mathit{O^{\prime\prime}_{{\mathrm{0}}}},\mathit{O^{\prime}_{{\mathrm{1}}}}$
and $\mathit{O^{\prime\prime}_{{\mathrm{1}}}}$ as below:

$\displaystyle\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)$
$\displaystyle=\mathit{O^{\prime}_{{\mathrm{0}}}}+\mathit{O^{\prime\prime}_{{\mathrm{0}}}}$
$\displaystyle\mathbf{Own}\,(\mathit{H^{\prime}},\mathit{R},\Gamma^{\prime\prime})$
$\displaystyle=\mathit{O^{\prime}_{{\mathrm{1}}}}+\mathit{O^{\prime\prime}_{{\mathrm{1}}}}$
$\displaystyle\mathit{O^{\prime}_{{\mathrm{0}}}}$
$\displaystyle=\Sigma_{\mathit{z}\in\mathit{dom}(\Gamma)\setminus\\{\mathit{y},\mathit{x}\\}}\,\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{z}),\Gamma(\mathit{z}))$
$\displaystyle\mathit{O^{\prime\prime}_{{\mathrm{0}}}}$
$\displaystyle=\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{y}),\Gamma(\mathit{y}))+\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{x}),\Gamma(\mathit{x}))$
$\displaystyle\mathit{O^{\prime}_{{\mathrm{1}}}}$
$\displaystyle=\Sigma_{\mathit{z}\in\mathit{dom}(\Gamma^{\prime\prime})\setminus\\{\mathit{y},\mathit{x}\\}}\,\mathbf{own}\,(\mathit{H^{\prime}},\mathit{R}(\mathit{z}),\Gamma^{\prime\prime}(\mathit{z}))$
$\displaystyle\mathit{O^{\prime\prime}_{{\mathrm{1}}}}$
$\displaystyle=\mathbf{own}\,(\mathit{H^{\prime}},\mathit{R}(\mathit{y}),\Gamma^{\prime\prime}(\mathit{y}))+\mathbf{own}\,(\mathit{H^{\prime}},\mathit{R}(\mathit{x}),\Gamma^{\prime\prime}(\mathit{x}))$

By the definition of the ownership function,
$\Gamma(\mathit{y})=\tau^{\prime}\operatorname{\mathbf{ref}}^{1}$ and
$\Gamma(\mathit{x})=\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$, we have:

$\displaystyle\mathit{O^{\prime\prime}_{{\mathrm{0}}}}$
$\displaystyle=\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{R}(\mathit{y})),\tau^{\prime})+\\{\mathit{a}\mapsto
1\\}+\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$
$\displaystyle\mathit{O^{\prime\prime}_{{\mathrm{1}}}}$
$\displaystyle=\mathbf{own}\,(\mathit{H^{\prime}},\mathit{H^{\prime}}(\mathit{R}(\mathit{y})),\tau_{{\mathrm{2}}})+\\{\mathit{a}\mapsto
1\\}+\mathbf{own}\,(\mathit{H^{\prime}},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}})$

As $\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)(\mathit{a})\leq 1$ (from
$\mathbf{Cons}\,(\mathit{H},\mathit{R},\Gamma)$) and from

$\displaystyle\mathbf{Own}\,(\mathit{H},\mathit{R},\Gamma)(\mathit{a})$
$\displaystyle=\mathit{O^{\prime}_{{\mathrm{0}}}}(\mathit{a})+\mathit{O^{\prime\prime}_{{\mathrm{0}}}}(\mathit{a})$
$\displaystyle=\mathit{O^{\prime}_{{\mathrm{0}}}}(\mathit{a})+\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{R}(\mathit{y})),\tau^{\prime})(\mathit{a})+1+\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})(\mathit{a})$
$\displaystyle=1$

we have that:

$\displaystyle\mathbf{own}\,(\mathit{H},\mathit{H}(\mathit{R}(\mathit{y})),\tau^{\prime})(\mathit{a})$
$\displaystyle=\mathbf{own}\,(\mathit{H},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})(\mathit{a})$
$\displaystyle=\mathit{O^{\prime}_{{\mathrm{0}}}}(\mathit{a})=0$

We now show that $\mathit{H}\approx_{\mathit{a}}\mathit{H^{\prime}}$. The
first two conditions are clear, so it remains to show that, for any $n$,
$\mathit{H}\vdash\mathit{a}\Downarrow n$ iff
$\mathit{H^{\prime}}\vdash\mathit{a}\Downarrow n$. From Lemma 20, we have
$\mathit{H}\vdash\mathit{a}\Downarrow|\tau^{\prime}\operatorname{\mathbf{ref}}^{1}|$,
and a proof by contradiction gives that
$|\tau^{\prime}\operatorname{\mathbf{ref}}^{1}|$ is the only such $n$ for
which $\mathit{H}\vdash\mathit{a}\Downarrow n$. We now argue the forward case
for the bi-implication, the backwards case follows similar reasoning.

Given
$\mathit{H}\vdash\mathit{a}\Downarrow|\tau^{\prime}\operatorname{\mathbf{ref}}^{1}|$,
we must show
$\mathit{H}\\{\mathit{a}\hookleftarrow\mathit{R}(\mathit{x})\\}\vdash\mathit{a}\Downarrow|\tau_{{\mathrm{2}}}\operatorname{\mathbf{ref}}^{1}|$,
for which it suffices to show
$\mathit{H}\\{\mathit{a}\hookleftarrow\mathit{R}(\mathit{x})\\}\vdash\mathit{R}(\mathit{x})\Downarrow|\tau_{{\mathrm{2}}}|$.
From our requirement that $\tau^{\prime}$ and $\tau_{{\mathrm{2}}}$ (and
therefore $\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}$) have similar shapes, we
have
$|\tau^{\prime}|=|\tau_{{\mathrm{2}}}|=|\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}}|$.
By inverting the well-typing of the input configuration, we must have
$\mathbf{SATv}(\mathit{H},\mathit{R},\mathit{R}(\mathit{x}),\tau_{{\mathrm{1}}}+\tau_{{\mathrm{2}}})$,
thus by Lemma 20 we must have
$\mathit{H}\vdash\mathit{R}(\mathit{x})\Downarrow|\tau_{{\mathrm{2}}}|$. As