by (box) and conclude this case. _Case(unbox)_. As above. _Case(let)_. Then
$t=\textsf{let}_{m}\ z=s\ \textsf{in}\ u$,
$\Gamma,x:_{\left\\{\right\\}}P,\Delta\vdash s\colon U$,
$\Gamma,x:_{D}P,\Delta,z:_{\left\\{\right\\}}U\vdash u\colon T$, and
${\Gamma,x:_{D}P,\Delta}\vdash{s}\ \bowtie\ {u}$. By IH, we have
$\Gamma,\theta\Delta\vdash\theta s\colon\theta U$, and
$\Gamma,\theta\Delta,z:_{\left\\{\right\\}}\theta U\vdash\theta u\colon\theta
T$. By Lemma B.61, we show that ${\Gamma,\theta\Delta}\vdash{\theta s}\
\bowtie\ {\theta u}$. Now we can conclude this case by (let). _Case(dvar)_.
Then $t=\textsf{var}_{D_{z}}\ z:=y\ \textsf{in}\ s$,
$\Gamma,x:_{D}P,\Delta\vdash y\colon S$,
$\Gamma,x:_{D}P,\Delta,z:_{D_{z}}\left\\{\textbf{{cap}}{}\right\\}\,\textsf{Ref}[{S}]\vdash
s\colon T$. We can conclude this case by IH and (dvar). _Case(read) and
(write)_. By IH and the same rule. ∎

##### Type Substitution

###### Lemma B.63 (Type substitution preserves reader checking).

If (i) ${\Gamma,X<:S,\Delta}\vdash{T}\uparrow\textsf{Rdr}$, and (ii)
$\Gamma\vdash R<:S$, then $\textsf{is-reader}_{\Gamma,\theta\Delta}\ {\theta
T}$, where $\theta=\left[{X}\mapsto{R}\right]$.

###### Proof.

By induction on the derivation. _Case(rd-reader)_. We conclude immediately
using the same rule. _Case(rd-tvar)_. Then
$T=X\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C$
for some $C,Y$, $Y<:S_{0}\in\Gamma,X<:S,\Delta$, and
${\Gamma,X<:S,\Delta}\vdash{S_{0}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C}\uparrow\textsf{Rdr}$.
By the IH we can show that
${\Gamma,\theta\Delta}\vdash{\theta(S_{0}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C)}\uparrow\textsf{Rdr}$.
Now, we proceed by a case analysis on where $Y$ is bound.

  * –

If $Y=X$. Then
$\theta(Y\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C)=R\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C$
and $S_{0}=S$. First, by the wellformedness we can show that
$\theta(S_{0}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C)=S_{0}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C$,
and therefore
${\Gamma,\theta\Delta}\vdash{S_{0}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C}\uparrow\textsf{Rdr}$.
Now we conclude this case by weakening and Lemma B.15.

  * –

If $Y$ is bound in either $\Gamma$ or $\Delta$ then in both cases we have
$Y<:\theta S_{0}\in\Gamma,\theta\Delta$. We conclude by the IH and the (rd-
tvar) rule.

∎

###### Lemma B.64 (Type substitution preserves is-reader).

If (i) $\textsf{is-reader}_{\Gamma,X<:S,\Delta}\ {z}$, and (ii) $\Gamma\vdash
R<:S$, then $\textsf{is-reader}_{\Gamma,\theta\Delta}\ {\theta z}$, where
$\theta=\left[{X}\mapsto{R}\right]$.

###### Proof.

Then we have $z:T\in\Gamma,X<:S,\Delta$, and $\Gamma,X<:S,\Delta\vdash
T<:\textsf{Rdr}[{S_{0}}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C_{0}$
for some $C_{0},S_{0}$. We first invoke Lemma B.15 to show that
${\Gamma,X<:S,\Delta}\vdash{T}\uparrow\textsf{Rdr}$. Then, by Lemma B.63 we
can show that ${\Gamma,\theta\Delta}\vdash{\theta T}\uparrow\textsf{Rdr}$. By
inspecting where $z$ is bound, we can show that $z:\theta
T\in\Gamma,\theta\Delta$, and finally conclude by Lemma B.16 and the (rd-tvar)
rule. ∎

###### Lemma B.65 (Type substitution preserves subcapturing).

If (i) $\Gamma,X<:S,\Delta\vdash C<:D$, and (ii) $\Gamma\vdash R<:S$, then
$\Gamma,\theta\Delta\vdash C\colon D$, where
$\theta=\left[{X}\mapsto{R}\right]$.

###### Proof.

By induction on the subcapture derivation, wherein most cases do not rely on
the type bindings in the context and thus can be concluded immediatley by the
IH and the same rule. In the (sc-reader) case we invoke Lemma B.64 to
conclude. ∎

###### Lemma B.66 (Type substitution preserves subtyping).

If (i) $\Gamma,X<:S,\Delta\vdash T<:U$, and (ii) $\Gamma\vdash R<:S$, then
$\Gamma,\theta\Delta\vdash\theta T<:\theta U$, where
$\theta=\left[{X}\mapsto{R}\right]$.

###### Proof.

By induction on the subtype derivation. _Case(refl) and (top)_. By the same
rule. _Case(capt)_. By Lemma B.65, and (capt). _Case(trans), (boxed), (fun)
and (tfun)_. By IH and application of the same rule. _Case(tvar)_. Then $T=Y$,
$Y<:S^{\prime}\in\Gamma,X<:S,\Delta$, and $U=S^{\prime}$. Our goal is
$\Gamma,\theta\Delta\vdash\theta Y<:\theta S^{\prime}$. Now we inspect where
$Y$ is bound.

  * –

_When $X=Y$_. Then $S^{\prime}=S$, and the goal becomes
$\Gamma,\theta\Delta\vdash R<:\theta S$. By the well-formedness, we can show
that $X\notin\textsf{fv}(S)$ and therefore $\theta S=S$. Now we conclude by
weakening the premise.

  * –

_When $Y\in\textsf{dom}(\Gamma)$_. By the well-formedness,
$X\notin\textsf{fv}(S^{\prime})$. Therefore, $\theta S^{\prime}=S^{\prime}$.
Also, $\theta Y=Y$, and $Y<:S^{\prime}\in\Gamma,\theta\Delta$. This case is
therefore concluded by (tvar).

  * –

_When $Y\in\textsf{dom}(\Delta)$_. Then $Y<:\theta
S^{\prime}\in\Gamma,\theta\Delta$. This case is therefore concluded by (tvar).

∎

###### Lemma B.67 (Type substitution preserves separation).

If (i) ${\Gamma,X<:S,\Delta}\vdash{C_{1}}\ \bowtie\ {C_{2}}$, and (ii)
$\Gamma\vdash R<:S$, then ${\Gamma,\theta\Delta}\vdash{C_{1}}\ \bowtie\
{C_{2}}$, where $\theta=\left[{X}\mapsto{R}\right]$.

###### Proof.

By induction on the separation derivation. _Case(ni-symm)_. Then
${\Gamma,X<:S,\Delta}\vdash{C_{2}}\ \bowtie\ {C_{1}}$. We conclude this case
by the IH and (ni-symm). _Case(ni-set)_. Then
$\overline{{\Gamma,X<:S,\Delta}\vdash{y}\ \bowtie\ {C_{2}}}^{y\in C_{1}}$. By
applying the IH repeated, we can show that
$\overline{{\Gamma,\theta\Delta}\vdash{y}\ \bowtie\ {C_{2}}}^{y\in C_{1}}$.
This case is therefore concluded by (ni-set). _Case(ni-degree)_. Then
$C_{1}=\left\\{x\right\\}$, $C_{2}=\left\\{y\right\\}$,
$x:_{D}T\in\Gamma,X<:S,\Delta$, and $y\in D$. Note that $X\notin D$, therefore
we have $\theta D=D$. Therefore, no matter where $x$ is bound, we have
$x:_{D}T^{\prime}\in\Gamma,\theta\Delta$. This case can therefore be concluded
by (ni-degree). _Case(ni-var)_. Then $C_{1}=\left\\{x\right\\}$,
$C_{2}=\left\\{y\right\\}$, $x:_{D}T\in\Gamma,X<:S,\Delta$, and
${\Gamma,X<:S,\Delta}\vdash{\textsf{cs}\left({T}\right)}\ \bowtie\ {y}$.
Depending on where $x$ is bound, either $x:_{D}T\in\Gamma,\theta\Delta$, or
$x:_{\theta D}\theta T\in\theta\Delta$. Since
$X\notin\textsf{cs}\left({T}\right)$, we can show that
$\textsf{cs}\left({\theta
T}\right)=\theta\textsf{cs}\left({T}\right)=\textsf{cs}\left({T}\right)$. By
IH, we can show that
${\Gamma,\theta\Delta}\vdash{\textsf{cs}\left({T}\right)}\ \bowtie\ {y}$. We
can therefore conclude this case by (ni-var). _Case(ni-reader)_. By applying
the IH, Lemma B.65 and the same rule. ∎

###### Lemma B.68 (Type substitution preserves typing).

If (i) $\Gamma,X<:S,\Delta\vdash t\colon T$, and (ii) $\Gamma\vdash R<:S$,
then $\Gamma,\theta\Delta\vdash\theta t\colon\theta T$ where
$\theta=\left[{X}\mapsto{R}\right]$.

###### Proof.

By induction on the typing derivation. _Case(var)_. Then $t=x$,
$x:S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}\in\Gamma,X<:S,\Delta$,
and the goal becomes $\Gamma,\theta\Delta\vdash\theta
x\colon\theta(S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{\left\\{x\right\\}})$.
Since $x\neq X$, we have $\theta x=x$. Now we inspect where $x$ is bound.

  * –

_When $x\in\textsf{dom}(\Gamma)$_. By the well-formedness we can show that
$X\notin\textsf{fv}(S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C})$.
Therefore, $\theta S^{\prime}=S^{\prime}$. We have
$x:S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}\in\Gamma,\theta\Delta$.
This case is concluded by (var).

  * –

_When $x\in\textsf{dom}(\Delta)$_. We have
$x:\theta(S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C})\in\Gamma,\theta\Delta$.
This case is therefore concluded by (var).

_Case(abs) and (tabs)_. In both cases we conclude by IH and the same rule.
_Case(app-r)_. Then $t=x\,y$, $\Gamma,X<:S,\Delta\vdash x\colon
C\,\forall(z:_{D}U)T^{\prime}$, $\Gamma,X<:S,\Delta\vdash y\colon U$,
${\Gamma,X<:S,\Delta}\vdash{D}\ \bowtie\ {y}$, and
$T=\left[{z}\mapsto{y}\right]T^{\prime}$. We can conclude this case by IH,
Lemma B.67, the fact that
$\theta\left[{z}\mapsto{y}\right]T^{\prime}=\left[{z}\mapsto{y}\right]\theta
T^{\prime}$ and the (app-r) rule. _Case(tapp)_. Then $t=x[S^{\prime}]$,
$\Gamma,X<:S,\Delta\vdash x\colon C\,\forall[Z<:S^{\prime}]T^{\prime}$ and
$T=\left[{Z}\mapsto{S^{\prime}}\right]T^{\prime}$. The goal becomes
${\Gamma,\theta\Delta}\vdash{\theta(x[S^{\prime}])}:{\theta\left[{Z}\mapsto{S^{\prime}}\right]T^{\prime}}$.
By IH we have $\Gamma,\theta\Delta\vdash\theta x\colon\theta
C\,\forall[Z<:\theta S^{\prime}]\theta T^{\prime}$. By (tapp) we can show that
$\Gamma,\theta\Delta\vdash\theta(x[S^{\prime}])\colon\left[{Z}\mapsto{\theta
S^{\prime}}\right]\theta T^{\prime}$. We observe that $\left[{Z}\mapsto{\theta
S^{\prime}}\right]\theta
T^{\prime}=\theta\left[{Z}\mapsto{S^{\prime}}\right]T^{\prime}$ and conclude
this case. _Case(box)_. Then $t=\Box\ y$ $\Gamma,X<:S,\Delta\vdash y\colon
S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}$,
and $C\subseteq\textsf{dom}(\Gamma,X<:S,\Delta)$. The goal becomes
$\Gamma,\theta\Delta\vdash\theta(\Box\ y)\colon\theta(\Box\
S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C})$.
Note that since $y\neq X$, we have $\theta y=y$. Proof proceeds by inspecting
the location of $y$ in the context.

  * –

_When $y\in\textsf{dom}(\Gamma)$_. By the well-formedness we can show that
$X\notin\textsf{fv}(S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C})$.
Therefore,
$\theta(S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C})=S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}$.
We observe that
$y:S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}\in\Gamma,\theta\Delta$,
and show that $\Gamma,\theta\Delta\vdash y\colon
S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}$
by (var). Now this case can be concluded by (box).

  * –

_When $y\in\textsf{dom}(\Delta)$_. Then we observe that
$y:\theta(S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C})\in\Gamma,\theta\Delta$,
and derive that $\Gamma,\theta\Delta\vdash
y\colon\theta(S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C})$
by (var). This case is concluded by (box).

_Case(unbox)_. Analogous to the previous case. _Case(sub)_. By IH, Lemma B.66
and (sub). _Case(let)_. Then $t=\textsf{let}_{m}\ x=s\ \textsf{in}\ u$,
$\Gamma,X<:S,\Delta\vdash s\colon T_{0}$,
$\Gamma,X<:S,\Delta,x:_{\left\\{\right\\}}T_{0}\vdash u\colon T$, and
${\Gamma,X<:S,\Delta}\vdash{s}\ \bowtie\ {u}$. By IH we can show that
$\Gamma,\theta\Delta\vdash\theta s\colon\theta T_{0}$, and
$\Gamma,\theta\Delta,x:_{\left\\{\right\\}}\theta T_{0}\vdash\theta
u\colon\theta T$. Since
$X\notin\textsf{cv}\left({s}\right),\textsf{cv}\left({u}\right),\textsf{cs}\left({T_{0}}\right)$,
we can show that
$\theta\textsf{cv}\left({s}\right)=\textsf{cv}\left({s}\right)$, and
$\theta\textsf{cv}\left({u}\right)=\textsf{cv}\left({u}\right)$. By Lemma
B.67, we can show that ${\Gamma,\theta\Delta}\vdash{\theta s}\ \bowtie\
{\theta u}$. We can therefore conclude this case by (let). _Case(dvar)_. Then
$t=\textsf{var}\ x:=y\ \textsf{in}\ s$, $\Gamma,X<:S,\Delta\vdash y\colon S$,
$\Gamma,X<:S,\Delta,x:_{D}\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{\left\\{\textbf{{cap}}{}\right\\}}\vdash
s\colon T$, and $\Gamma,X<:S,\Delta\vdash{D}\ \textbf{wf}$. By IH we can show
that $\Gamma,\theta\Delta\vdash\theta y\colon\theta S$, and
$\Gamma,\theta\Delta,x:_{\theta
D}\theta(\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{\left\\{\textbf{{cap}}{}\right\\}})\vdash\theta
s\colon\theta T$. Also, we can show that $\Gamma,\theta\Delta\vdash{D}\
\textbf{wf}$. This case is therefore concluded by (dvar). _Case(read) and
(write)_. By IH and the same rule. ∎

####  B.2.7. Soundness Theorems

###### Lemma B.69 (Canonical forms: term abstraction).

$\Gamma\vdash v\colon C\,\forall(x:_{D}U)T$ implies
$v=\lambda(x:_{D}U^{\prime})t$ for some $U^{\prime}$ and $t$, such that
$\Gamma\vdash U<:U^{\prime}$ and $\Gamma,x:_{D}U^{\prime}\vdash t\colon T$.

###### Proof.

By induction on the typing derivation. _Case(abs)_. We conclude immediately
from the premise. _Case(sub)_. Then $\Gamma\vdash v\colon T_{0}$, and
$\Gamma\vdash T_{0}<:C\,\forall(x:_{D}U)T$. By Lemma B.23 and Lemma B.43, we
can show that $T_{0}=C_{0},\forall(x:_{D}U_{0})T_{0}$, $\Gamma\vdash
U<:U_{0}$, and $\Gamma,x:_{D}U_{0}\vdash T_{0}<:T$. Invoking IH, we can show
that $v=\lambda(x:_{D}U^{\prime})t$ such that $\Gamma\vdash
U_{0}<:U^{\prime}$, and $\Gamma,x:_{D}U^{\prime}\vdash t\colon T_{0}$. We
conclude by the (trans) and the (sub) rule. ∎

###### Lemma B.70 (Canonical forms: type abstraction).

$\Gamma\vdash v\colon C\,\forall[X<:S]T$ implies $v=\lambda[X<:S^{\prime}]t$
for some $S^{\prime}$ and $t$, such that $\Gamma\vdash S<:S^{\prime}$ and
$\Gamma,X<:S^{\prime}\vdash t\colon T$.

###### Proof.

Analogous to the proof of Lemma B.69. ∎

###### Lemma B.71 (Canonical forms: boxed term).

$\Gamma\vdash v\colon C\,\Box\ T$ implies $v=\Box\ x$ for some $x$, such that
$\Gamma\vdash x\colon T$ and
${\textsf{cs}\left({T}\right)}\subseteq{\textsf{dom}(\Gamma)}$.

###### Proof.

Analogous to the proof of Lemma B.69. ∎

###### Lemma B.72 (Canonical forms: reader).

$\Gamma\vdash v\colon C\,\textsf{Rdr}[{S}]$ implies $v=\textsf{reader}\ x$ for
some $x$, such that $\Gamma\vdash x\colon C\,\textsf{Ref}[{S}]$.

###### Proof.

Analogous to the proof of Lemma B.69. ∎

###### Lemma B.73 (Store lookup inversion: typing).

If (i) ${}\vdash{\gamma}\ \sim\ {\Gamma}$ (ii) $\Gamma,\Delta\vdash x\colon
S\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}$,
(iii) $\gamma(\textsf{val}\ {x})=v$, then $\Gamma,\Delta\vdash v\colon
S\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C^{\prime}}$.

###### Proof.

By induction on the derivation of ${}\vdash{\gamma}\ \sim\ {\Gamma}$.
_Case(st-empty)_. Contradictory. _Case(st-val)_. Then
$\gamma=\gamma_{0},\textsf{val}\ {y}\mapsto v$, ${}\vdash{\gamma_{0}}\ \sim\
{\Gamma_{0}}$, $\Gamma_{0}\vdash v\colon T$, and $\Gamma=\Gamma_{0},y:T$. If
$x=y$, then $x:T\in\Gamma,\Delta$. We have $\gamma(\textsf{val}\ {x})=v$. By
inspecting the typing derivation $\Gamma,\Delta\vdash x\colon
S\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}$, we
can show that $\Gamma,\Delta\vdash\left\\{x\right\\}<:C$ and
$\Gamma,\Delta\vdash S^{\prime}<:S$ where
$T=S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C^{\prime}}$
for some $C^{\prime}$. By weakening we show that $\Gamma,\Delta\vdash v\colon
S^{\prime}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C^{\prime}}$.
Then, we invoke the (sub) rule and conclude. Otherwise, we have $x\neq y$.
Finally by the IH we conclude this case. _Case(st-var)_. Then
$\gamma=\gamma_{0},\textsf{var}\ {y}=v$, ${}\vdash{\gamma_{0}}\ \sim\
{\Gamma_{0}}$, $\Gamma_{0}\vdash v\colon S$, and
$\Gamma=\Gamma_{0},y:_{\textsf{dom}(\Gamma_{0})}\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{\left\\{\textbf{{cap}}{}\right\\}}$.
If $x=y$, it contradicts with $\gamma(\textsf{val}\ {x})=v$. Otherwise, we
have $x\neq y$, we conclude this case by the IH. _Case(st-set)_. By IH. ∎

###### Lemma B.74 (Store lookup inversion: term abstraction).

If (i) ${}\vdash{\gamma;e}\ \sim\ {\Gamma;\Delta}$; (ii) $\Gamma,\Delta\vdash
x\colon C\,\forall(z:_{D}T)U$ and (iii) $\gamma(\textsf{val}\
{x})=\lambda(z:_{D}T^{\prime})t$, then $\Gamma,\Delta\vdash T<:T^{\prime}$ and
$\Gamma,\Delta,z:T^{\prime}\vdash t\colon U$.

###### Proof.

We first invoke Lemma B.73 to show that
$\Gamma,\Delta\vdash\lambda(z:_{D}T^{\prime})t\colon\forall(z:_{D}T)U\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C^{\prime}}$.
By Lemma B.69, we can show that $\Gamma,\Delta\vdash T<:T^{\prime}$, and
$\Gamma,\Delta,z:_{D}T^{\prime}\vdash t\colon U$. We therefore conclude. ∎

###### Lemma B.75 (Store lookup inversion: type abstraction).

If (i) ${}\vdash{\gamma;e}\ \sim\ {\Gamma;\Delta}$; (ii) $\Gamma,\Delta\vdash
x\colon C\,\forall[X<:S]U$ and (iii) $\gamma(\textsf{val}\
{x})=\lambda[X<:S^{\prime}]t$, then $\Gamma,\Delta\vdash S<:S^{\prime}$ and
$\Gamma,\Delta,X<:S^{\prime}\vdash t\colon U$.

###### Proof.

Analogous to the proof of Lemma B.74. ∎

###### Lemma B.76 (Store lookup inversion: boxed term).

If (i) ${}\vdash{\gamma;e}\ \sim\ {\Gamma;\Delta}$; (ii) $\Gamma,\Delta\vdash
x\colon C^{\prime}\,\Box\
S\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}$ and
(iii) $\gamma(\textsf{val}\ {x})=\Box\ y$, then $\Gamma,\Delta\vdash y\colon
S\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}$.

###### Proof.

Analogous to the proof of Lemma B.74. ∎

###### Lemma B.77 (Store lookup inversion: reader).

If (i) ${}\vdash{\gamma;e}\ \sim\ {\Gamma;\Delta}$; (ii) $\Gamma,\Delta\vdash
x\colon C\,\textsf{Rdr}[{S}]$ and (iii) $\gamma(\textsf{val}\
{x})=\textsf{reader}\ y$, then $\Gamma,\Delta\vdash y\colon
C^{\prime}\,\textsf{Ref}[{S}]$.

###### Proof.

Analogous to the proof of Lemma B.74. ∎

###### Lemma B.78 (Value typing with strict capture set).

$\Gamma\vdash v\colon T$ implies $\exists T^{\prime}$ such that $\Gamma\vdash
v\colon T^{\prime}$ and
$\textsf{cs}\left({T^{\prime}}\right)=\textsf{cv}\left({v}\right)$.

###### Proof.

By induction on the typing derivation. Only the following cases are
applicable. _Case(abs)_. Then $v=\lambda(x:_{D}U)t$, $\Gamma,x:_{D}U\vdash
t\colon T^{\prime}$, and $T=\textsf{cv}\left({t}\right)/x\
\forall(z:_{D}U)T^{\prime}$. Then
$\textsf{cs}\left({T}\right)=\textsf{cv}\left({v}\right)=\textsf{cv}\left({t}\right)/x$.
This case is therefore concluded. _Case(tabs) and (box)_. Analogous to (abs).
_Case(sub)_. By IH. ∎

###### Lemma B.79 (Value typing inversion: capture set).

$\Gamma\vdash v\colon T$ implies
$\Gamma\vdash\textsf{cv}\left({v}\right)<:\textsf{cs}\left({T}\right)$.

###### Proof.

Analogous to the proof of Lemma B.78. ∎

See 4.1

###### Proof.

Proceed by case analysis on the reduction derivation. _Case(apply)_. Then
$t={e}[\,{x\,y}\,]$, $\gamma(\textsf{val}\ {x})=\lambda(z:_{D}U)s$,
$t^{\prime}=\left[{z}\mapsto{y}\right]s$, and $\gamma^{\prime}=\gamma$. By
Lemma B.50, $\exists\Delta,Q$ such that ${\Gamma}\vdash{e}\ \sim\
{\Delta}:\left[{Q}\ @\ {x\,y}\right]\Rightarrow{T}$ and $\Gamma,\Delta\vdash
x\,y\colon Q^{\prime}$, where $Q=\left[{z}\mapsto{y}\right]Q^{\prime}$. Now,
by induction on this typing derivation, we prove that (i) $\Gamma,\Delta\vdash
x\colon C\,\forall(z:_{D}U^{\prime}){Q^{\prime}}$ (ii)
${\Gamma,\Delta}\vdash{y}:_{D^{\prime}}{U^{\prime}}$, and (iii)
${\Gamma,\Delta}\vdash{D}\ \bowtie\ {y}$. For the (app) case, it is conclude
immediately from the preconditions. For the (sub) case, it can be concluded
from IH and (sub). Other cases are not applicable. By Lemma B.74, we can show
that $\Gamma,\Delta\vdash U^{\prime}<:U$, and $\Gamma,\Delta,z:_{D}U\vdash
s\colon Q^{\prime}$. We invoke Lemma B.62 to show that
$\Gamma,\Delta\vdash\left[{z}\mapsto{y}\right]s\colon\left[{z}\mapsto{y}\right]Q^{\prime}$.
Since $\gamma(\textsf{val}\ {x})=\lambda(z:_{D}U)s$ and ${}\vdash{\gamma}\
\sim\ {\Gamma}$, we have $x:T_{x}\in\Gamma$ for some $T_{x}$ where
$\textsf{cs}\left({T_{x}}\right)=\textsf{cv}\left({s}\right)/z$. We can show
that
$\textsf{cv}\left({\left[{z}\mapsto{y}\right]s}\right)\subseteq\textsf{cv}\left({x\,y}\right)\setminus\left\\{x\right\\}\cup\textsf{cs}\left({T_{x}}\right)$.
Now we invoke Lemma B.35 to show that
${\Gamma;\Delta}\vdash{\left[{z}\mapsto{y}\right]s}\,\triangleleft\colon\,{x\,y}$.
By evaluation context reification, we show that
$\Gamma\vdash{e}[\,{\left[{z}\mapsto{y}\right]s}\,]\colon T$ and conclude this
case. _Case(tapply)_. As above, but making use of Corollary B.33.
_Case(open)_. As above, but making use of Lemma B.32. _Case(get)_. As above.
_Case(lift-let)_. Then $t={e}[\,{\textsf{let}_{m}\ x=v\ \textsf{in}\ s}\,]$,
$\gamma^{\prime}=\gamma,\textsf{val}_{m}\ {x}\mapsto v$,
$t^{\prime}={e}[\,{s}\,]$, and $\textsf{fv}(v)\cup
D\subseteq\textsf{dom}(\gamma)$. Now we invoke Lemma B.50 to show that
$\exists\Delta,Q$ such that ${\Gamma}\vdash{e}\ \sim\ {\Delta}:\left[{Q}\ @\
{\textsf{let}_{m}\ x=v\ \textsf{in}\ s}\right]\Rightarrow{T}$, and
$\Gamma,\Delta\vdash\textsf{let}_{m}\ x=v\ \textsf{in}\ s\colon Q$. By
inspecting this typing derivation, we can show that $\Gamma,\Delta\vdash
v\colon U$, $\Gamma,\Delta,x:_{\left\\{\right\\}}U\vdash s\colon Q$, and
${\Gamma,\Delta}\vdash{v}\ \bowtie\ {s}$ if $m=\textsf{par}$. By Lemma B.78,
narrowing, and Lemma B.29, we can show that $\exists U^{\prime}$ such that
$\textsf{cs}\left({U^{\prime}}\right)=\textsf{cv}\left({v}\right)$,
$\Gamma,\Delta\vdash v\colon U^{\prime}$, and
$\Gamma,\Delta,x:_{D}U^{\prime}\vdash s\colon Q$. Set
$\Gamma^{\prime}=\Gamma,x:_{D}U^{\prime}$. We can show that
${}\vdash{\gamma^{\prime}}\ \sim\ {\Gamma^{\prime}}$ by (st-val). In the next,
we show that
$\Gamma,\Delta,x:_{D}U^{\prime}\vdash\textsf{cv}\left({s}\right)<:\textsf{cv}\left({\textsf{let}_{D}\
x=v\ \textsf{in}\ s}\right)$. If $x\notin\textsf{cv}\left({s}\right)$, we have
$\textsf{cv}\left({\textsf{let}_{D}\ x=v\ \textsf{in}\
s}\right)=\textsf{cv}\left({s}\right)=\textsf{cv}\left({s}\right)\setminus\left\\{x\right\\}$.
And the sub-goal is proven by the reflexivity of subcapturing. Otherwise, if
$x\in\textsf{cv}\left({s}\right)$, we have
$\textsf{cv}\left({\textsf{let}_{D}\ x=v\ \textsf{in}\
s}\right)=\textsf{cv}\left({s}\right)\setminus\left\\{x\right\\}\cup\textsf{cv}\left({v}\right)$,
and
$\textsf{cv}\left({s}\right)\subseteq\textsf{cv}\left({s}\right)\setminus\left\\{x\right\\}\cup\left\\{x\right\\}$.
We can show that
$\Gamma,\Delta\vdash\left\\{x\right\\}<:\textsf{cv}\left({v}\right)$. By the
reflexivity of subcapturing and Corollary B.13, we can prove the goal. Since
$\textsf{cv}\left({v}\right)\subseteq\textsf{dom}(\gamma)$, we can show that
$\Gamma,x:_{\left\\{\right\\}}U^{\prime}$ is well-formed. Therefore by
permutation we have
$\Gamma,x:_{\left\\{\right\\}}U^{\prime},\Delta\vdash\textsf{cv}\left({s}\right)<:\textsf{cv}\left({\textsf{let}_{D}\
x=v\ \textsf{in}\ s}\right)$. Now we invoke Lemma B.32 to show that
${\Gamma,x:_{\left\\{\right\\}}U^{\prime};\Delta}\vdash{s}\,\triangleleft\colon\,{\textsf{let}_{D}\
x=v\ \textsf{in}\ s}$. By Lemma B.51, we can show that
${\Gamma,x:_{\left\\{\right\\}}U^{\prime}}\vdash{e}\ \sim\ {\Delta}:\left[{Q}\
@\ {\textsf{let}_{D}\ x=v\ \textsf{in}\ s}\right]\Rightarrow{T}$. Again by
permutation, we show that
$\Gamma,x:_{\left\\{\right\\}}U^{\prime},\Delta\vdash s\colon Q$. We can
therefore invoke the reification to show that
$\Gamma^{\prime}\vdash{e}[\,{s}\,]\colon T$ and conclude this case.
_Case(rename)_. Then $t={e}[\,{\textsf{let}_{m}\ x=y\ \textsf{in}\ s}\,]$,
$t^{\prime}={e}[\,{\left[{x}\mapsto{y}\right]s}\,]$, and
$\gamma^{\prime}=\gamma$. We start by invoking Lemma B.50 to show that
$\exists\Delta,Q$ such that ${\Gamma}\vdash{e}\ \sim\ {\Delta}:\left[{Q}\ @\
{\textsf{let}_{m}\ x=y\ \textsf{in}\ s}\right]\Rightarrow{T}$ and
$\Gamma,\Delta\vdash\textsf{let}_{m}\ x=y\ \textsf{in}\ s\colon Q$. By
inspecting this typing derivation, we can show that $\Gamma,\Delta\vdash
y\colon U$ for some $U$, $\Gamma,\Delta,x:_{m}U\vdash s\colon Q$, and
${\Gamma,\Delta}\vdash{y}\ \bowtie\ {s}$. Now we invoke Lemma B.62 to show
that
$\Gamma,\Delta\vdash\left[{x}\mapsto{y}\right]s\colon\left[{x}\mapsto{y}\right]Q$.
Since $x\notin\textsf{fv}(Q)$, we have $\left[{x}\mapsto{y}\right]Q=Q$. Note
that we have
$\textsf{cv}\left({\left[{x}\mapsto{y}\right]s}\right)=\textsf{cv}\left({\textsf{let}_{D}\
x=y\ \textsf{in}\ s}\right)$. By Corollary B.33, we can show that
${\Gamma;\Delta}\vdash{\left[{x}\mapsto{y}\right]s}\,\triangleleft\colon\,{\textsf{let}_{D}\
x=y\ \textsf{in}\ s}$. Now we invoke the reification of evaluation context to
show that $\Gamma\vdash{e}[\,{\left[{x}\mapsto{y}\right]s}\,]\colon T$ and
conclude this case. _Case(lift-var)_. Then $t={e}[\,{\textsf{var}\ x:=y\
\textsf{in}\ s}\,]$, $\gamma(\textsf{val}\ {y})=v$,
$\gamma^{\prime}=\gamma,\textsf{var}\ {x}=v$, and $t^{\prime}={e}[\,{s}\,]$.
By Lemma B.56, we show that
$\Gamma,x:_{\textsf{dom}(\Gamma)}\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}\left\\{\textbf{{cap}}{}\right\\}\vdash{e}[\,{s}\,]\colon
T$. We can show that ${\Gamma}\vdash{\gamma^{\prime}}\ \sim\
{\Gamma,x:_{\textsf{dom}(\Gamma)}\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}\left\\{\textbf{{cap}}{}\right\\}}$
by Lemma (st-var). We can therefore conclude this case. _Case(lift-set)_. Then
$t={e}[\,{{x}:={y}}\,]$, $\gamma(\textsf{val}\ {y})=v$,
$t^{\prime}={e}[\,{v}\,]$, and $\gamma^{\prime}=\gamma,\textsf{set}\ {x}=v$.
Now we invoke Lemma B.50 to show that $\exists\Delta,Q$ such that
${\Gamma}\vdash{e}\ \sim\ {\Delta}:\left[{Q}\ @\
{{x}:={y}}\right]\Rightarrow{T}$, and $\Gamma,\Delta\vdash{x}:={y}\colon Q$.
By induction on this typing derivation, we can show that $\exists S$ such that
$\Gamma,\Delta\vdash x\colon C\,\textsf{Ref}[{S}]$, $\Gamma,\Delta\vdash
y\colon S$, and $\Gamma,\Delta\vdash S<:Q$. By Lemma B.73, we can show that
$\Gamma,\Delta\vdash v\colon S$. By Lemma B.79, we have
$\Gamma,\Delta\vdash\textsf{cv}\left({v}\right)<:\varemptyset$. Therefore we
have
$\Gamma,\Delta\vdash\textsf{cv}\left({v}\right)<:\textsf{cv}\left({{x}:={y}}\right)$.
Now we invoke Lemma B.32 to show that
${\Gamma;\Delta}\vdash{v}\,\triangleleft\colon\,{{x}:={y}}$. Now we reify the
evaluation context to show that $\Gamma\vdash{e}[\,{v}\,]\colon T$. The
remaining to be shown is that ${}\vdash{\gamma^{\prime}}\ \sim\ {\Gamma}$. By
inverting the typing judgment $\Gamma,\Delta\vdash
x\colon\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C$
and considering that $x\in\textsf{dom}(\Gamma)$, we can show that
$x:_{D}\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C^{\prime}\in\Gamma$.
By induction on ${}\vdash{\gamma}\ \sim\ {\Gamma}$, we can show that
$\Gamma\vdash v\colon S$ by the fact that $\gamma(\textsf{val}\ {y})=v$ and
weakening. Now ${}\vdash{\gamma^{\prime}}\ \sim\ {\Gamma}$ can be derived by
(st-set). This case is therefore concluded. ∎

###### Lemma B.80 (Evaluation context trampolining).

Consider a reduction derivation
${\gamma}\mid{t}\,\longmapsto\,{\gamma^{\prime}}\mid{t^{\prime}}$. We have
${\gamma}\mid{{e}[\,{t}\,]}\,\longmapsto\,{\gamma^{\prime}}\mid{{e}[\,{t^{\prime}}\,]}$
for any $e$.

###### Proof.

By straightforward case analysis on the reduction derivation. No rule makes
use of the evaluation context. All cases are analogous, thus we present only
the (apply) case. _Case(apply)_. Then $t={e^{\prime}}[\,{x\,y}\,]$,
$\gamma(\textsf{val}\ {x})=\lambda(z:_{D}T)s$, $\gamma^{\prime}=\gamma$, and
$t^{\prime}={e^{\prime}}[\,{\left[{z}\mapsto{y}\right]s}\,]$. None of these
preconditions depends on the evaluation context $e$. We therefore conclude
this case by the same rule. ∎

###### Theorem B.81 (Progress).

If (i) ${}\vdash{\gamma}\ \sim\ {\Gamma}$, (ii) $\Gamma\vdash t\colon T$, then
either $t$ is an answer, or $\exists\gamma^{\prime},t^{\prime}$ such that
${\gamma}\mid{t}\,\longmapsto\,{\gamma^{\prime}}\mid{t^{\prime}}$.

###### Proof.

By induction on the typing derivation. _Case(var)_. Then $t=x$. We can
conclude this case because $x$ is an answer. _Case(sub)_. We directly apply
the IH and conclude. _Case(abs), (tabs), (box) and (reader)_. We conclude
these cases because $t$ is a value. _Case(app)_. Then $t=x\,y$, $\Gamma\vdash
x\colon C\,\forall(z:_{D}U)T^{\prime}$ where
$T=\left[{z}\mapsto{y}\right]T^{\prime}$, and $\Gamma\vdash y\colon U$. By
Lemma B.47, we can show that there exists $v$ such that $\gamma(\textsf{val}\
{x})=v$. By Lemma B.73, we have $\Gamma\vdash v\colon
C\,\forall(z:_{D}U)T^{\prime}$. By Lemma B.69, we have
$v=\lambda(z:_{D}U^{\prime})s$ for some $U^{\prime}$ and $s$. Now we conclude
by (apply). _Case(tapp)_. As above. _Case(unbox)_. Then
$t={C}\multimapinv{x}$, $\Gamma\vdash x\colon\Box\
(S\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C)$,
and $C\subseteq\textsf{dom}(\Gamma)$. By Lemma B.46, we can show that $\exists
v$ such that $\gamma(\textsf{val}\ {x})=v$. By Lemma B.73, we can show that
$\Gamma\vdash v\colon\Box\
(S\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C)$. By
Lemma B.71, we have $z=\Box\ y$ for some $y$. Now we conclude by (open).
_Case(let)_. Then $t=\textsf{let}_{m}\ x=s\ \textsf{in}\ u$, $\Gamma\vdash
s\colon T_{0}$ for some $T_{0}$, and $\Gamma,x:_{\left\\{\right\\}}T_{0}\vdash
s\colon T$. Proceed by a case analysis on the kind of $s$.

  * –

If $s$ is a value, we can show that
$\textsf{fv}(s)\subseteq\textsf{dom}(\Gamma)=\textsf{dom}(\gamma)$. This
allows for the application of the (lift-let) rule.

  * –

If $s$ is a variable, we can conclude by (rename).

  * –

Otherwise $s$ is a term. By IH we can show that
${\gamma}\mid{s}\,\longmapsto\,{\gamma^{\prime}}\mid{{s^{\prime}}}$ for some
$\gamma^{\prime}$ and $s^{\prime}$. By Lemma B.80, we can derive that
${\gamma}\mid{\textsf{let}_{D}\ x=s\ \textsf{in}\
u}\,\longmapsto\,{\gamma^{\prime}}\mid{\textsf{let}_{D}\ x=s^{\prime}\
\textsf{in}\ u}$ and conclude this case.

_Case(dvar)_. Then $t=\textsf{var}\ x:=y\ \textsf{in}\ s$, $\Gamma\vdash
y\colon S$, and
$\Gamma,x:_{D}\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}\left\\{\textbf{{cap}}\right\\}\vdash
s\colon T$. We can show that $\gamma(\textsf{val}\ {y})=v$ for some $v$. This
case is therefore concluded by (lift-var). _Case(read)_. Then
$t=\textsf{read}\,{x}$, and $\Gamma\vdash
x\colon\textsf{Rdr}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{C}$.
By Lemma B.49, we can show that $\exists y.\gamma(\textsf{val}\
{x})=\textsf{reader}\ y$. Now we invoke Lemma B.72 to show that $\Gamma\vdash
y\colon\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C$.
By using Lemma B.45 we can show that $\exists v$ such that
$\gamma(\textsf{var}\ {y})=v$. Now we conclude this case by (get).
_Case(write)_. Then $t={x}:={y}$, $\Gamma\vdash
x\colon\textsf{Ref}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}C$,
and $\Gamma\vdash y\colon S$. By Lemma B.46, we can show that $\exists v$ such
that $\gamma(\textsf{val}\ {y})=v$. Now we conclude this case by (lift-set). ∎

###  B.3. Confluence

####  B.3.1. Properties of Evaluation Context Focuses

A focus is one way to split a term $t$ into an evaluation context $e$ and the
focused term $s$ such that $t={e}[\,{s}\,]$. When evaluating a let-binding,
either the bindee or the continuation get reduced, resulting in multiple
possible focuses for the same term. Each focus is determined by the part we
choose to reduce for each let expression.

###### Definition B.0 (Subfocus).

We say $t={e_{1}}[\,{t_{1}}\,]$ is a _subfocus_ of $t={e_{2}}[\,{t_{2}}\,]$,
written ${e_{1}}[\,{t_{1}}\,]\preceq{e_{2}}[\,{t_{2}}\,]$, iff $\exists e$
such that $t_{1}={e}[\,{t_{2}}\,]$ and $e_{2}={e_{1}}[\,{e}\,]$.

###### Definition B.0 (Branched focus).

We say $t={e_{1}}[\,{t_{1}}\,]$ and $t={e_{2}}[\,{t_{2}}\,]$ are a pair of
branched focuses, written
${e_{1}}[\,{t_{1}}\,]\leftrightarrow{e_{2}}[\,{t_{2}}\,]$, iff $\exists
e,D,e^{\prime}_{1},e^{\prime}_{2}$ such that $t={e}[\,{\textsf{let}_{D}\
x={e^{\prime}_{1}}[\,{t_{1}}\,]\ \textsf{in}\
{e^{\prime}_{2}}[\,{t_{2}}\,]}\,]$, $e_{1}={e}[\,{\textsf{let}_{D}\
x={e^{\prime}_{1}}[\,{}\,]\ \textsf{in}\ {e^{\prime}_{2}}[\,{t_{2}}\,]}\,]$,
and $e_{2}={e}[\,{\textsf{let}_{D}\ x={e^{\prime}_{1}}[\,{t_{1}}\,]\
\textsf{in}\ {e^{\prime}_{2}}[\,{}\,]}\,]$.

###### Lemma B.84 (Extending subfocus).

Given two focuses of the same term
$t={e_{1}}[\,{s_{1}}\,]={e_{2}}[\,{s_{2}}\,]$, we can show that for any
$e^{\prime}$, ${e_{1}}[\,{s_{1}}\,]\preceq{e_{2}}[\,{s_{2}}\,]$ implies
${e^{\prime}}[\,{{e_{1}}[\,{s_{1}}\,]}\,]\preceq{e^{\prime}}[\,{{e}[\,{2}\,]}\,]$.

###### Proof.

Then for some $e$, we have $s_{1}={e}[\,{s_{2}}\,]$, and
$e_{2}={e_{1}}[\,{e}\,]$ First of all, we can show that
${e}[\,{t}\,]={e}[\,{{e_{1}}[\,{s_{1}}\,]}\,]={e}[\,{{e_{2}}[\,{s_{2}}\,]}\,]$,
which means that the extended focuses are still for the same term.
$s_{1}={e}[\,{s_{2}}\,]$ is unaffected by the extension. And
${e^{\prime}}[\,{e_{2}}\,]={e^{\prime}}[\,{{e_{1}}[\,{e}\,]}\,]$ is trivial. ∎

###### Lemma B.85 (Extending branched focus).

Given two focuses of the same term
$t={e_{1}}[\,{s_{1}}\,]={e_{2}}[\,{s_{2}}\,]$, for any $e^{\prime}$ we can
show that ${e_{1}}[\,{s_{1}}\,]\leftrightarrow{e_{2}}[\,{s_{2}}\,]$ implies
${e^{\prime}}[\,{{e_{1}}[\,{s_{1}}\,]}\,]\leftrightarrow{e^{\prime}}[\,{{e_{2}}[\,{s_{2}}\,]}\,]$.

###### Proof.

Analogous to proof of Lemma B.84. ∎

###### Lemma B.86 (Different focuses of the same term).

Given two focuses ${e_{1}}[\,{s_{1}}\,]$ and ${e_{2}}[\,{s_{2}}\,]$ of the
same term $t$, we can show that one of the followings holds:

  1. (i)

${e_{1}}[\,{s_{1}}\,]\preceq{e_{2}}[\,{s_{2}}\,]$;

  2. (ii)

${e_{2}}[\,{s_{2}}\,]\preceq{e_{1}}[\,{s_{1}}\,]$;

  3. (iii)

${e_{1}}[\,{s_{1}}\,]\leftrightarrow{e_{2}}[\,{s_{2}}\,]$;

  4. (iv)

${e_{2}}[\,{s_{2}}\,]\leftrightarrow{e_{1}}[\,{s_{1}}\,]$.

###### Proof.

We begin by induction on the first evaluation context $e_{1}$. _Case
$e_{1}=[]$_. Then we can demonstrate that
${e_{1}}[\,{s_{1}}\,]\preceq{e_{2}}[\,{c_{2}}\,]$ by setting $e=e_{2}$. _Case
$e_{1}=\textsf{let}_{D}\ x=e^{\prime}_{1}\ \textsf{in}\ u$_. We proceed the
proof by induction on $e_{2}$.

  * –

_Case $e_{2}=[]$_. Then we conclude by showing that
${e_{2}}[\,{s_{2}}\,]\preceq{e_{1}}[\,{s_{1}}\,]$.

  * –

_Case $e_{2}=\textsf{let}_{m}\ x=e^{\prime}_{2}\ \textsf{in}\ u$_. We can
invoke IH and use Lemma B.84 and Lemma B.85 to conclude this case.

  * –

_Case $e_{2}=\textsf{let}_{m}\ x=u^{\prime}\ \textsf{in}\ e^{\prime}_{2}$_.
Then we can show that $u^{\prime}={e^{\prime}_{1}}[\,{s_{1}}\,]$ and
$u={e^{\prime}_{2}}[\,{s_{2}}\,]$. We can therefore conclude this case
immediately by showing that
${e_{1}}[\,{s_{1}}\,]\leftrightarrow{e_{2}}[\,{s_{2}}\,]$.

_Case $e_{1}=\textsf{let}_{m}\ x=u\ \textsf{in}\ e^{\prime}_{1}$_. Analogous
to the previous case. They are symmetric. ∎

####  B.3.2. Confluence Theorems

Now we demonstrate that the reduction of the calculus is _confluent_. This
means that though we can arbitrarily interleave the reduction of both sides of
the let bindings, the result of the program will always be the same, which
implies the absence of data races and thus achieves the safe concurrency
guarantee. First of all, in different reduction paths, the store bindings can
be lifted to the store in different orders. For example, we may introduce
variables in different orders, or have the set-bindings arranged in different
ways. Regardless of these permutations, the respective stores should possess
the same interpretations. Thus, to carry out the proof we have consider the
equivalence between the stores up to the permutations. To this end, we define
the _equivalence_ between two evaluation stores up to permutation.

###### Definition B.0 (Equivalent stores).

We say two stores $\gamma_{1}$ and $\gamma_{2}$ are equivalent, written
$\gamma_{1}\cong\gamma_{2}$, iff

  1. (1)

$\gamma_{2}$ is permuted from $\gamma_{1}$;

  2. (2)

$\forall x\in\textsf{bvar}\left({\gamma_{1}}\right)$,
$\gamma_{1}(\textsf{var}\ {x})=\gamma_{2}(\textsf{var}\ {x})$.

###### Definition B.0 (Equivalent configurations).

We say two configurations ${\gamma_{1}}\mid{t_{1}}$ and
${\gamma_{2}}\mid{t_{2}}$ are equivalent iff $\gamma_{1}\cong\gamma_{2}$ and
$t_{1}=t_{2}$.

###### Fact B.89 (Store equivalence is an equivalence relation).

The equivalence between stores $\gamma_{1}\cong\gamma_{2}$ is an equivalence
relation: it is reflexive, symmetric and transitive.

###### Lemma B.90 (Value lookup in equivalent stores).

If $\gamma_{1}\cong\gamma_{2}$ then $\gamma_{1}(\textsf{val}\
{x})=\gamma_{2}(\textsf{val}\ {x})$.

###### Proof.

By the definition of store equivalence and the lookup function. The result of
the lookup function does not rely on the order of bindings. ∎

###### Lemma B.91 (Variable lookup in equivalent stores).

If $\gamma_{1}\cong\gamma_{2}$, then $\gamma_{1}(\textsf{var}\
{x})=\gamma_{2}(\textsf{var}\ {x})$.

###### Proof.

This follows directly from the definition of store equivalence. ∎

###### Lemma B.92 (Typing implies separation).

Given non-value terms $s_{1}$ and $s_{2}$,
$\Gamma\vdash\textsf{let}_{\textsf{par}}\ x={e_{1}}[\,{s_{1}}\,]\ \textsf{in}\
{e_{2}}[\,{s_{2}}\,]\colon T$ implies ${\Gamma}\vdash{s_{1}}\ \bowtie\
{s_{2}}$.

###### Proof.

By induction on the typing derivation. _Case(let)_. Then we have
${\Gamma}\vdash{{e_{1}}[\,{s_{1}}\,]}\ \bowtie\ {{e_{2}}[\,{s_{2}}\,]}$. Since
neither $s_{1}$ nor $s_{2}$ is a value, by straightforward induction on
$e_{1}$ and $e_{2}$ we can show that
$\textsf{cv}\left({s_{1}}\right)\cap\textsf{dom}(\Gamma)\subseteq\textsf{cv}\left({{e_{1}}[\,{s_{1}}\,]}\right)\cap\textsf{dom}(\Gamma)$
and
$\textsf{cv}\left({s_{2}}\right)\cap\textsf{dom}(\Gamma)\subseteq\textsf{cv}\left({{e_{2}}[\,{s_{2}}\,]}\right)\cap\textsf{dom}(\Gamma)$.
Now we can conclude by applying Corollary B.30. _Case(sub)_. By the IH. ∎

###### Lemma B.93 (Exclusiveness of root capability).

If ${\Gamma}\vdash{C_{1}}\ \bowtie\ {C_{2}}$, then (i) $\textbf{{cap}}{}\in
C_{1}$ implies $\Gamma\vdash C_{2}<:\left\\{\right\\}$, and (ii)
$\textbf{{cap}}{}\in C_{2}$ implies $\Gamma\vdash C_{1}<:\left\\{\right\\}$.

###### Proof.

By induction on the derivation. _Case(ni-symm)_. By swapping the two
conclusions in the IH. _Case(ni-set)_. Then $\overline{{\Gamma}\vdash{x}\
\bowtie\ {C_{2}}}^{x\in C_{1}}$. By applying the IH repeatedly, we can show
that for any $x\in C_{1}$, we have (1) $\textbf{{cap}}\in\left\\{x\right\\}$
implies $\Gamma\vdash C_{2}<:\left\\{\right\\}$, and (2) $\textbf{{cap}}\in
C_{2}$ implies $\Gamma\vdash\left\\{x\right\\}<:\left\\{\right\\}$. First, if
$\textbf{{cap}}\in C_{1}$, then exists $x\in C_{1}$ such that
$\textbf{{cap}}\in\left\\{x\right\\}$, which implies that $\Gamma\vdash
C_{2}<:\left\\{\right\\}$ by the IH. Besides, if $x\in C_{2}$, we can show
that $\Gamma\vdash\left\\{x\right\\}<:\left\\{\right\\}$ for any $x\in C_{1}$.
By invoking Lemma B.11 repeatedly we can show that $\Gamma\vdash
C_{1}<:\left\\{\right\\}$. We can therefore conclude this case. _Case(ni-
degree)_. Then $C_{1}=\left\\{x\right\\}$ and $C_{2}=\left\\{y\right\\}$. We
can show that $x\neq\textbf{{cap}}$ and $y\neq\textbf{{cap}}$ by definition,
and thus conclude this case. _Case(ni-var)_. Then $C_{1}=\left\\{x\right\\}$,
$C_{2}=\left\\{y\right\\}$, $x:T\in\Gamma$, and
${\Gamma}\vdash{\textsf{cs}\left({T}\right)}\ \bowtie\ {y}$. Firstly, we have
$x\neq\textbf{{cap}}$ and therefore $\textbf{{cap}}\notin\left\\{x\right\\}$.
Secondly, if $\textbf{{cap}}\in\left\\{y\right\\}$ then by the IH we can show
that $\Gamma\vdash\textsf{cs}\left({T}\right)<:\left\\{\right\\}$. Now we
conclude this case using the (sc-var) rule. _Case(ni-reader)_. Then
$C_{1}=\left\\{x\right\\}$, $C_{2}=\left\\{y\right\\}$,
$\Gamma\vdash\left\\{x\right\\}<:\left\\{\textbf{{rdr}}\right\\}$, and
$\Gamma\vdash\left\\{y\right\\}<:\left\\{\textbf{{rdr}}\right\\}$. By
straightforward induction on
$\Gamma\vdash\left\\{x\right\\}<:\left\\{\textbf{{rdr}}\right\\}$ we can show
that $\textbf{{cap}}\notin\left\\{x\right\\}$ and similarly for
$\textbf{{cap}}\notin\left\\{y\right\\}$. We can therefore conclude this case.
∎

###### Lemma B.94.

Given any
$x:_{D}S\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{\left\\{\textbf{{cap}}\right\\}}\in\Gamma$,
${\Gamma}\vdash{x}\ \bowtie\ {x}$ is impossible.

###### Proof.

By induction on the derivation of ${\Gamma}\vdash{x}\ \bowtie\ {x}$, wherein
we derive contradiction for each case. _Case(ni-symm) and (ni-set)_. By the
IH. _Case(ni-degree)_. Then $x\in D$. This is contradictory with the well-
formedness. _Case(ni-var)_. Then
${\Gamma}\vdash{\left\\{\textbf{{cap}}\right\\}}\ \bowtie\ {x}$. By Lemma B.93
we can show that $\Gamma\vdash\left\\{x\right\\}<:\left\\{\right\\}$. By
straightforward induction on it we can derive the contradiction. _Case(ni-
reader)_. Then
$\Gamma\vdash\left\\{x\right\\}<:\left\\{\textbf{{rdr}}\right\\}$. By
straightforward induction on this derivation, we can derive the contradiction
too. ∎

###### Lemma B.95.

In an inert environment $\Gamma$, given any
$x:\textsf{Rdr}[{S}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}{\left\\{y\right\\}}\in\Gamma$,
and
$y:{S^{\prime}}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}\left\\{\textbf{{cap}}\right\\}\in\Gamma$,
${\Gamma}\vdash{x}\ \bowtie\ {y}$ is impossible.

###### Proof.

By induction on the derivation of ${\Gamma}\vdash{x}\ \bowtie\ {y}$. _Case(ni-
symm) and (ni-set)_. By the IH. _Case(ni-degree)_. Then $x\in D_{y}$ or $y\in
D_{x}$, where $D_{x}$ and $D_{y}$ denotes the separation degree of $x$ and $y$
in the environment respectively. We can show that $y\notin D_{x}$ by the well-
formedness. If $y\in D_{x}$, then by the inertness we can show that
${\Gamma}\vdash{y}\ \bowtie\ {y}$. Now we derive the contradiction via Lemma
B.94. _Case(ni-var)_. Then either ${\Gamma}\vdash{\textbf{{cap}}}\ \bowtie\
{x}$, or ${\Gamma}\vdash{y}\ \bowtie\ {y}$. In the first case we can show that
$\Gamma\vdash\left\\{x\right\\}<:\left\\{\right\\}$ by Lemma B.93, from which
we can derive the contradiction. In the second case, we invoke Lemma B.94 to
derive the contradiction. _Case(ni-reader)_. Then we have
$\Gamma\vdash\left\\{y\right\\}<:\left\\{\textbf{{rdr}}\right\\}$. By
induction on the derivation of it, we can show contradiction in each case. ∎

###### Corollary B.96.

If (i) ${\Gamma}\vdash{x}\ \bowtie\ {y}$, (ii)
$x:S_{1}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}\left\\{\textbf{{cap}}\right\\}\in\Gamma$
and (iii)
$y:S_{2}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}\left\\{\textbf{{cap}}\right\\}\in\Gamma$,
then we have $x\neq y$.

###### Corollary B.97.

If (i) ${\Gamma}\vdash{x}\ \bowtie\ {y}$, (ii)
$x:\textsf{Rdr}[{S_{1}}]\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}\left\\{z\right\\}\in\Gamma$
and (iii)
$y:S_{2}\mathrel{\\!\text{\raisebox{3.01385pt}{\scalebox{0.6}{$\wedge$}}}\\!}\left\\{\textbf{{cap}}\right\\}\in\Gamma$,
then $z\neq y$.

###### Theorem B.98 (Diamond property of reduction).

Given two equivalent configurations
${\gamma_{1}}\mid{t}\equiv{\gamma_{2}}\mid{t}$, if (1) $\gamma_{1}\vdash t$
and $\gamma_{2}\vdash t$; (2)
${\gamma_{1}}\mid{t}\,\longmapsto\,{\gamma^{\prime}_{1}}\mid{t_{1}}$; and (3)
${\gamma_{2}}\mid{t}\,\longmapsto\,{\gamma^{\prime}_{2}}\mid{t_{2}}$, then
either $t_{1}=t_{2}$, or there exists
$\gamma^{\prime\prime}_{1},t^{\prime},\gamma^{\prime\prime}_{2}$ such that (1)
${\gamma^{\prime}_{1}}\mid{t_{1}}\,\longmapsto\,{\gamma^{\prime\prime}_{1}}\mid{t^{\prime}}$,
(2)
${\gamma^{\prime}_{2}}\mid{t_{2}}\,\longmapsto\,{\gamma^{\prime\prime}_{2}}\mid{t^{\prime}}$,
and (3)
${\gamma^{\prime\prime}_{1}}\mid{t^{\prime}}\equiv{\gamma^{\prime\prime}_{2}}\mid{t^{\prime}}$.

###### Proof.

Begin with a case analysis on the derivation of
${\gamma_{1}}\mid{t}\,\longmapsto\,{\gamma^{\prime}_{1}}\mid{t_{1}}$.
_Case(apply), (tapply) and (open)_. Proceed by a case analysis on the
derivation of
${\gamma_{2}}\mid{t}\,\longmapsto\,{\gamma^{\prime}_{2}}\mid{t_{2}}$.

  * –

_Case(apply), (tapply), (open) and (get)_. We only present the proof when both
derivations are derived by the (apply) case, and all other possibilities
follow analogously. Firstly, from the preconditions we know that
$t={e_{1}}[\,{x_{1}\,y_{1}}\,]$ for some $e_{1},x_{1},y_{1}$,
$\gamma_{1}(\textsf{val}\ {x_{1}})=\lambda(z:T_{1})s_{1}$, and
$t^{\prime}_{1}={e_{1}}[\,{\left[{z}\mapsto{y_{1}}\right]{s_{1}}}\,]$. Also,
we have $t={e_{2}}[\,{x_{2}\,y_{2}}\,]$ for some $e_{2},x_{2},y_{2}$,
$\gamma_{2}(\textsf{val}\ {x_{2}})=\lambda(z:T_{2})s_{2}$, and
$t^{\prime}_{2}={e_{2}}[\,{\left[{z}\mapsto{y_{2}}\right]{s_{2}}}\,]$. By
invoking Lemma B.86, we can show that either $e_{1}=e_{2}$ and
$x_{1}\,y_{1}=x_{2}\,y_{2}$, or
${e_{1}}[\,{x_{1}\,y_{1}}\,]\leftrightarrow{e_{2}}[\,{x_{2}\,y_{2}}\,]$, or
${e_{2}}[\,{x_{2}\,y_{2}}\,]\leftrightarrow{e_{1}}[\,{x_{1}\,y_{1}}\,]$.

    * –

When $e_{1}=e_{2}$, $x_{1}=x_{2}$ and $y_{1}=y_{2}$.

    * –

When ${e_{1}}[\,{x_{1}\,y_{1}}\,]\leftrightarrow{e_{2}}[\,{x_{2}\,y_{2}}\,]$.
Then $t=e[\textsf{let}_{D}\ x={e_{1}}[\,{x_{1}\,y_{1}}\,]\ \textsf{in}\
{e_{2}}[\,{x_{2}\,y_{2}}\,]]$. Therefore, we have
$t_{1}={e}[\,{\textsf{let}_{D}\
x={e_{1}}[\,{\left[{z}\mapsto{y_{1}}\right]s_{1}}\,]\ \textsf{in}\
{e_{2}}[\,{x_{2}\,y_{2}}\,]}\,]$. We let $t^{\prime}=e[\ \textsf{let}_{D}\
x={e_{1}}[\,{\left[{z}\mapsto{y_{1}}\right]s_{1}}\,]\ \textsf{in}\
{e_{2}}[\,{{e_{2}}[\,{\left[{z}\mapsto{y_{2}}\right]s_{2}}\,]}\,]\ ]$, and can
derive that
${\gamma_{1}}\mid{t_{1}}\,\longmapsto\,{\gamma_{1}}\mid{t^{\prime}}$.
Similarly, we can show that
${\gamma_{2}}\mid{t_{2}}\,\longmapsto\,{\gamma_{2}}\mid{t^{\prime}}$, and thus
conclude by the fact that $\gamma_{1}\cong\gamma_{2}$.

    * –

When ${e_{2}}[\,{x_{2}\,y_{2}}\,]\leftrightarrow{e_{1}}[\,{x_{1}\,y_{1}}\,]$.
Analogous to the previous case.

  * –

_Case(lift-let)_. We only present the proof of the (apply) case, and other
cases follows analogously. Then $t={e_{1}}[\,{x_{1}\,y_{1}}\,]$ for some
$e_{1},x_{1},y_{1}$, $\gamma_{1}(\textsf{val}\
{x_{1}})=\lambda(z:T_{1})s_{1}$, and
$t_{1}={e_{1}}[\,{\left[{z}\mapsto{y_{1}}\right]s_{1}}\,]$. Also,
$t={e_{2}}[\,{\textsf{let}_{D}\ x=v\ \textsf{in}\ u}\,]$,
$\gamma^{\prime}_{2}=\gamma_{2},\textsf{val}\ {x}\mapsto v$, and
$t_{2}={e_{2}}[\,{u}\,]$. Now we proceed the proof by invoking Lemma B.86 to
analyze the relationship of two focuses
$t={e_{1}}[\,{x_{1}\,y_{1}}\,]={e_{2}}[\,{\textsf{let}_{D}\ x=v\ \textsf{in}\
u}\,]$.

    * –

_When ${e_{1}}[\,{x_{1}\,y_{1}}\,]\preceq{e_{2}}[\,{\textsf{let}_{m}\ x=v\
\textsf{in}\ u}\,]$._ This implies that for some $e$ we have
$x_{1}\,y_{1}={e}[\,{\textsf{let}_{m}\ x=v\ \textsf{in}\ u}\,]$, which is
impossible.

    * –

_When ${e_{2}}[\,{\textsf{let}_{m}\ x=v\ \textsf{in}\
u}\,]\preceq{e_{1}}[\,{x_{1}\,y_{1}}\,]$._ Then for some $e$ we have
$\boxed{\textsf{let}_{m}\ x=v\ \textsf{in}\ u}={e}[\,{x_{1}\,y_{1}}\,]$ and
$e_{1}={e_{2}}[\,{e}\,]$. By analyzing the equality, we can show that
$t={e_{2}}[\,{\textsf{let}_{m}\ x=v\ \textsf{in}\
{e^{\prime}}[\,{x_{1}\,y_{1}}\,]}\,]$ and $e_{1}={e_{2}}[\,{\textsf{let}_{m}\
x=v\ \textsf{in}\ e^{\prime}}\,]$. Set
$t^{\prime}={e_{2}}[\,{{e^{\prime}}[\,{\left[{z}\mapsto{y_{1}}\right]{s_{1}}}\,]}\,]$.
First, we can derive that
${\gamma_{1}}\mid{{e_{1}}[\,{\left[{z}\mapsto{y_{1}}\right]{s_{1}}}\,]}\,\longmapsto\,{\gamma_{1},\textsf{val}\
{x}\mapsto
v}\mid{{e_{2}}[\,{{e^{\prime}}[\,{\left[{z}\mapsto{y_{1}}\right]{s_{1}}}\,]}\,]}$
by showing that $\textsf{fv}(v)\subseteq\textsf{dom}(\gamma_{1})$ and then
apply the (lift-let) rule. Then, we can derive that ${\gamma_{2},\textsf{val}\
{x}\mapsto
v}\mid{{e_{2}}[\,{{e^{\prime}}[\,{x_{1}\,y_{1}}\,]}\,]}\,\longmapsto\,{\gamma_{2},\textsf{val}_{D}\
{x}\mapsto
v}\mid{{e_{2}}[\,{{e^{\prime}}[\,{\left[{z}\mapsto{y_{1}}\right]s_{1}}\,]}\,]}$
by applying Lemma B.90 and the (apply) rule. Now we can show that
$(\gamma_{1},\textsf{val}\ {x}\mapsto v)\cong(\gamma_{2},\textsf{val}\
{x}\mapsto v)$ and conclude this case.

    * –

_When ${e_{1}}[\,{x_{1}\,y_{1}}\,]\leftrightarrow{e_{2}}[\,{\textsf{let}_{m}\
x=v\ \textsf{in}\ u}\,]$._ Then $t={e}[\,{\textsf{let}_{n}\
y={e^{\prime}_{1}}[\,{x_{1}\,y_{1}}\,]\ \textsf{in}\
{e^{\prime}_{2}}[\,{\textsf{let}_{m}\ x=v\ \textsf{in}\ u}\,]}\,]$ for some
$e,n,y,e^{\prime}_{1}$ and $e^{\prime}_{2}$. Let
$\gamma^{\prime\prime}_{1}=\gamma_{1},\textsf{val}_{m}\ {x}\mapsto v$,
$\gamma^{\prime\prime}_{2}=\gamma_{2},\textsf{val}_{m}\ {x}\mapsto v$, and
$t^{\prime}=e[\textsf{let}_{E}{y}={e^{\prime}_{1}[\left[{z}\mapsto{y_{1}}\right]s_{1}]}$
$\,\textsf{in}\,{{e^{\prime}_{2}}[\,{u}\,]}]$. For both $t_{1},t_{2}$, we can
invoke the other rule to reduce to $t^{\prime}$. We can therefore conclude
this case.

    * –

_When ${e_{2}}[\,{\textsf{let}_{m}\ x=v\ \textsf{in}\
u}\,]\leftrightarrow{e_{1}}[\,{x_{1}\,y_{1}}\,]$._ Analogous to the above
case. These two cases are symmetric.

  * –

_Case(rename), (lift-var) and (lift-set)_. Analogous to the previous case.

_Case(get)_. Then $t={e_{1}}[\,{\textsf{read}\,{x}}\,]$,
$t_{1}={e_{1}}[\,{v}\,]$, $\gamma(\textsf{val}\ {x})=\textsf{reader}\
x^{\prime}$ and $\gamma(\textsf{var}\ {x^{\prime}})=v$. We proceed the proof
by case analysis on the second derivation, wherein the (apply), (tapply) and
the (open) cases are symmetric to the above proven cases. The proof of (lift-
let), (lift-var) and (rename) is analogous to the previous case. Notably, in
the (lift-var) we are sure that the lifted variable is not $x$ since it is a
freshly created local variable.

  * –

_Case(get)_. To prove this case, we begin by invoking Lemma B.86 to analyze
the relation between two focuses, wherein in each possibility we can invoke
Lemma B.91 to demonstrate the equality between the result of variable lookup
in two equivalent stores, and therefore invoke (get) again to reduce both
sides to the same term.

  * –

_Case(lift-set)_. Then $t={e_{2}}[\,{{y_{1}}:={y_{2}}}\,]$,
$\gamma_{2}(\textsf{val}\ {y_{2}})=w$,
$\gamma^{\prime}_{2}=\gamma_{2},\textsf{set}\ {y_{1}}=w$, and
$t_{2}={e_{2}}[\,{w}\,]$. Now we have to show that $y_{1}\neq x^{\prime}$ so
that the read and the write can be swapped. We first invoke Lemma B.86 to
analyze the relation between two focuses. The two cases where
${e_{1}}[\,{\textsf{read}\,{x}}\,]\preceq{e_{2}}[\,{{y_{1}}:={y_{2}}}\,]$ or
${e_{2}}[\,{{y_{1}}:={y_{2}}}\,]\preceq{e_{1}}[\,{\textsf{read}\,{x}}\,]$ are
impossible. Now we show the proof when
${e_{1}}[\,{\textsf{read}\,{x}}\,]\leftrightarrow{e_{2}}[\,{{y_{1}}:={y_{2}}}\,]$,
whereas the other case is analogous. We have
$t=e[\textsf{let}_{m}{x}={{e^{\prime}_{1}}[\,{\textsf{read}\,{x}}\,]}\,$
$\textsf{in}\,{e^{\prime}_{2}}[\,{{y_{1}}:={y_{2}}}\,]]$. Let
$t^{\prime}={e}[\,{\textsf{let}_{m}\ x={e^{\prime}_{1}}[\,{v}\,]\ \textsf{in}\
{e^{\prime}_{2}}[\,{w}\,]}\,]$. By invoking Lemma B.90 we can show that
$\gamma_{1}(\textsf{val}\ {y_{2}})=w$, and therefore derive that
${\gamma_{1}}\mid{t_{1}}\,\longmapsto\,{\gamma_{1},\textsf{set}\
{y_{1}}=w}\mid{t^{\prime}}$ by the (lift-set) rule. Since $\gamma_{2}\vdash t$
we know that $\Gamma_{2}\vdash t\colon T_{2}$ for some $\Gamma_{2}$ and
$T_{2}$. By Lemma B.50 we can show that
$\Gamma_{2},\Delta_{2}\vdash\textsf{let}_{m}\
x={e^{\prime}_{1}}[\,{\textsf{read}\,{x}}\,]\ \textsf{in}\
{e^{\prime}_{2}}[\,{{y_{1}}:={y_{2}}}\,]\colon U$ for some $\Delta_{2}$ and
$U$. Now we invoke Lemma B.92 and Lemma B.26 to show that
${\Gamma_{2},\Delta_{2}}\vdash{x}\ \bowtie\ {y_{1}}$. By induction on
${}\vdash{\gamma}\ \sim\ {\Gamma_{2}}$, we can show that
$x:\left\\{x^{\prime}\right\\}\,\textsf{Rdr}[{S_{0}}]\in\Gamma_{2}$, and
$y_{1}:\left\\{\textbf{{cap}}\right\\}\,\textsf{Ref}[{S_{1}}]\in\Gamma_{2}$
for some $S_{0},S_{1}$. Now we invoke Corollary B.97 to show that
$x^{\prime}\neq y_{1}$. Therefore, we can show that
$\gamma^{\prime}_{2}(\textsf{var}\ {x^{\prime}})=\gamma(\textsf{var}\
{x^{\prime}})=v$ where $\gamma^{\prime}_{2}=\gamma_{2},\textsf{set}\
{y_{1}}=w$. We can thus derive that
${\gamma^{\prime}_{2}}\mid{t_{2}}\,\longmapsto\,{\gamma^{\prime}_{2}}\mid{t^{\prime}}$.
Finally, we can show that $\gamma_{1},\textsf{set}\ {y_{1}}=w$ and
$\gamma_{2},\textsf{set}\ {y_{1}}=w$ are still equivalent and conclude this
case.

_Case(rename)_. Then $t={e_{1}}[\,{\textsf{let}_{D_{1}}\ x_{1}=y_{1}\
\textsf{in}\ s_{1}}\,]$ for some $e_{1}$, and
$t_{1}={e_{1}}[\,{\left[{x}\mapsto{y}\right]u}\,]$. We proceed by case
analysis on the other reduction. The proof of (apply), (tapply), (open) and
(get) cases are symmetric to the proof of the previous cases.

  * –

_Case(rename)_. Then $t={e_{2}}[\,{\textsf{let}_{D_{2}}\ x_{2}=y_{2}\
\textsf{in}\ s_{2}}\,]$ for some $e_{2}$. Now we use Lemma B.86 to analyze the
relation between two focuses.

    * –

_When ${e_{1}}[\,{\textsf{let}_{D_{1}}\ x_{1}=y_{1}\ \textsf{in}\
s_{1}}\,]\preceq{e_{2}}[\,{\textsf{let}_{D_{2}}\ x_{2}=y_{2}\ \textsf{in}\
s_{2}}\,]$_. Then we have $\textsf{let}_{D_{1}}\ x_{1}=y_{1}\ \textsf{in}\
s_{1}={e}[\,{\textsf{let}_{D_{2}}\ x_{2}=y_{2}\ \textsf{in}\ s_{2}}\,]$ for
some $e$, and $e_{2}={e_{1}}[\,{e}\,]$. If $e=[]$, then we have $t_{1}=t_{2}$.
Then we have
$t=e[\textsf{let}_{D_{1}}{x_{1}}={y_{1}}\,\textsf{in}\,{{e^{\prime}}[\,{\textsf{let}_{D}\
x_{2}=y_{2}\ \textsf{in}\ s_{2}}\,]}]$ for some $e^{\prime}$. Let
$t^{\prime}=e_{1}[{e^{\prime}}[\left[{x_{1}}\mapsto{y_{1}}\right]\left[{x_{2}}\mapsto{\left[{x_{1}}\mapsto{y_{1}}\right]y_{2}}\right]s_{2}]]$.
Now we inspect whether $x_{1}=y_{2}$, and in both cases we can derive that
${\gamma_{1}}\mid{t_{1}}\,\longmapsto\,{\gamma_{1}}\mid{t^{\prime}}$, and
${\gamma_{2}}\mid{t_{2}}\,\longmapsto\,{\gamma_{1}}\mid{t^{\prime}}$, which
allow us to conclude this case.

    * –

_When ${e_{2}}[\,{\textsf{let}_{D_{2}}\ x_{2}=y_{2}\ \textsf{in}\
s_{2}}\,]\preceq{e_{1}}[\,{\textsf{let}_{D_{1}}\ x_{1}=y_{1}\ \textsf{in}\
s_{1}}\,]$_. Analogous to the previous case.

    * –

_When ${e_{1}}[\,{\textsf{let}_{D_{1}}\ x_{1}=y_{1}\ \textsf{in}\
s_{1}}\,]\leftrightarrow{e_{2}}[\,{\textsf{let}_{D_{2}}\ x_{2}=y_{2}\
\textsf{in}\ s_{2}}\,]$_. Then for both directions, we can apply (rename) to
rename the variable in the other branch, wherein the renaming in one branch is
independent from the renaming in the other branch. We can therefore conclude
this case.

    * –

_When ${e_{2}}[\,{\textsf{let}_{D_{2}}\ x_{2}=y_{2}\ \textsf{in}\
s_{2}}\,]\leftrightarrow{e_{1}}[\,{\textsf{let}_{D_{1}}\ x_{1}=y_{1}\
\textsf{in}\ s_{1}}\,]$_. Analogous to the previous case.

  * –

_Case(lift-let)_. Then $t={e_{2}}[\,{\textsf{let}_{D_{2}}\ x_{2}=v_{2}\
\textsf{in}\ s_{2}}\,]$, $\gamma^{\prime}_{2}=\gamma_{2},\textsf{val}_{D}\
{x_{2}}\mapsto v_{2}$, and $t_{2}={e_{2}}[\,{s_{2}}\,]$. Now we apply Lemma
B.86 to analyze the relation between two focuses.

    1. (i)

_When ${e_{1}}[\,{\textsf{let}_{D_{1}}\ x_{1}=y_{1}\ \textsf{in}\
s_{1}}\,]\preceq{e_{2}}[\,{\textsf{let}_{D_{2}}\ x_{2}=v_{2}\ \textsf{in}\
s_{2}}\,]$_. Then, by inspecting the equality we can show that
$t={e_{1}}[\,{\textsf{let}_{D_{1}}\ x_{1}=y_{1}\ \textsf{in}\
{e}[\,{\textsf{let}_{D_{2}}\ x_{2}=v_{2}\ \textsf{in}\ s_{2}}\,]}\,]$. We set
$t^{\prime}={e_{1}}[\,{{e}[\,{\left[{x_{1}}\mapsto{y_{1}}\right]s_{2}}\,]}\,]$.
Importantly, since $\textsf{cv}\left({v_{2}}\right)\cap
D_{2}\subseteq\textsf{dom}(\gamma_{2})$, we can show that
$\left[{x_{1}}\mapsto{y_{1}}\right]{v_{2}}=v_{2}$ and
$\left[{x_{1}}\mapsto{y_{1}}\right]D_{2}=D_{2}$. We can derive that
${\gamma_{1}}\mid{t_{1}}\,\longmapsto\,{\gamma_{1},\textsf{val}_{D_{2}}\
{x_{2}}\mapsto v_{2}}\mid{t^{\prime}}$ and ${\gamma_{2},\textsf{val}_{D_{2}}\
{x_{2}}\mapsto
v_{2}}\mid{t_{2}}\,\longmapsto\,{\gamma_{2},\textsf{val}_{D_{2}}\
{x_{2}}\mapsto v_{2}}\mid{t^{\prime}}$. This case can thus be concluded as
$\gamma_{1},\textsf{val}_{D_{2}}\ {x_{2}}\mapsto v_{2}$ and
$\gamma_{2},\textsf{val}_{D_{2}}\ {x_{2}}\mapsto v_{2}$ are still equivalent.

    2. (ii)

_Other cases_. In these cases, the renaming and the binding lifting do not
influence each other. So in each case, for both directions we apply the
corresponding rule in the other direction to conclude.

  * –

_Case(lift-var) and (lift-set)_. In this two cases, we can show that the
variable that is looked up is already in the store, and by the well-formedness
their value does not mention the renamed variable, thus staying unaffected by
the renaming. We can apply the corresponding rule to conclude each case.

_Case(lift-let) and (lift-var)_. Proceed by case analysis on the other
reduction derivation. The proof of the (apply), (tapply), (open), (get), and
(rename) cases are again symmetric to the previous proof. In the remaining
cases, we can always swap the order the two lifted store bindings while
preserving store equivalence. _Case(lift-set)_. We do a case analysis on the
other reduction derivation, wherein all but one cases can be proven
symmetrically to the previous ones. The only unproven case is when both
reductions are derived by the (lift-set) rule. Then
$t={e_{1}}[\,{{x_{1}}:={y_{1}}}\,]$, $\gamma_{1}(\textsf{val}\
{y_{1}})=v_{1}$, $\gamma^{\prime}_{1}=\gamma_{1},\textsf{set}\ {x_{1}}=v_{1}$,
and $t_{1}={e_{1}}[\,{v_{1}}\,]$. Also, $t={e_{2}}[\,{{x_{2}}:={y_{2}}}\,]$,
$\gamma_{2}(\textsf{val}\ {y_{2}})=v_{2}$,
$\gamma^{\prime}_{2}=\gamma_{2},\textsf{set}\ {x_{2}}=v_{2}$, and
$t_{2}={e_{2}}[\,{v_{2}}\,]$. By invoking Lemma B.86 we can show that either
$e_{1}=e_{2}$, or
${e_{1}}[\,{{x_{1}}:={y_{1}}}\,]\leftrightarrow{e_{2}}[\,{{x_{2}}:={y_{2}}}\,]$
or
${e_{2}}[\,{{x_{2}}:={y_{2}}}\,]\leftrightarrow{e_{1}}[\,{{x_{1}}:={y_{1}}}\,]$.
In the first case we can conclude immediately since this implies that
$t_{1}=t_{2}$. Otherwise, we invoke Lemma B.50, Lemma B.92, and Corollary B.96
to show that $x_{1}\neq x_{2}$. Therefore, swapping the two set-bindings
preserves the store equivalence. For both directions, we can apply the (lift-
set) rule to reduce to the same term. This case is therefore concluded. ∎

###### Definition B.0 (Reduction closures).

We define
${\gamma}\mid{t}\,\longmapsto^{*}\,{\gamma^{\prime}}\mid{t^{\prime}}$ as the
reflexive and transitive closure of
${\gamma}\mid{t}\,\longmapsto\,{\gamma^{\prime}}\mid{t^{\prime}}$.
${\gamma}\mid{t}\,\longmapsto^{\leq 1}\,{\gamma^{\prime}}\mid{t^{\prime}}$
denotes the union of the reduction relation
${\gamma}\mid{t}\,\longmapsto\,{\gamma^{\prime}}\mid{t^{\prime}}$ and the
reflexive relation. In other words, ${\gamma}\mid{t}\,\longmapsto^{\leq
1}\,{\gamma^{\prime}}\mid{t^{\prime}}$ means a reduction of zero or one step.

###### Corollary B.100 (Diamond property of $\,\longmapsto^{\leq 1}\,{}$).

Given two equivalent configurations
${\gamma_{1}}\mid{t}\cong{\gamma_{2}}\mid{t}$, if (1) $\gamma_{1}\vdash t$ and
$\gamma_{2}\vdash t$; (2) ${\gamma_{1}}\mid{t}\,\longmapsto^{\leq
1}\,{\gamma^{\prime}_{1}}\mid{t_{1}}$; and (3)
${\gamma_{2}}\mid{t}\,\longmapsto^{\leq 1}\,{\gamma^{\prime}_{2}}\mid{t_{2}}$,
then there exists
$\gamma^{\prime\prime}_{1},t^{\prime},\gamma^{\prime\prime}_{2}$ such that (1)
${\gamma^{\prime}_{1}}\mid{t_{1}}\,\longmapsto^{\leq
1}\,{\gamma^{\prime\prime}_{1}}\mid{t^{\prime}}$, (2)
${\gamma^{\prime}_{2}}\mid{t_{2}}\,\longmapsto^{\leq
1}\,{\gamma^{\prime\prime}_{2}}\mid{t^{\prime}}$, and (3)
${\gamma^{\prime\prime}_{1}}\mid{t^{\prime}}\cong{\gamma^{\prime\prime}_{2}}\mid{t^{\prime}}$.

###### Fact B.101.

The transitive and reflexive closure of ${\gamma}\mid{t}\,\longmapsto^{\leq
1}\,{\gamma^{\prime}}\mid{t^{\prime}}$ equals
${\gamma}\mid{t}\,\longmapsto^{*}\,{\gamma^{\prime}}\mid{t^{\prime}}$.

###### Lemma B.102 (Store equivalence preserves reduction).

If (i)
${\gamma_{1}}\mid{t}\,\longmapsto\,{\gamma_{1}^{\prime}}\mid{t^{\prime}}$ and
(ii) $\gamma_{1}\cong\gamma_{2}$ then there exists $\gamma_{2}^{\prime}$ such
that (i)
${\gamma_{2}}\mid{t}\,\longmapsto\,{\gamma_{2}^{\prime}}\mid{t^{\prime}}$ and
(ii) $\gamma_{1}^{\prime}\cong\gamma_{2}^{\prime}$.

###### Proof.

By straightforward case analysis on the reduction derivation, wherein in each
case we apply the same typing rule. In the cases where store lookup is
involved, we use Lemma B.90 and Lemma B.91 to show that the result is the same
under the two equivalent stores. In the cases where the store is extended in
the reduction step, we can straightforwardly show that the resulted stores are
still equivalent to each other. ∎

###### Corollary B.103.

If (i)
${\gamma_{1}}\mid{t}\,\longmapsto^{*}\,{\gamma_{1}^{\prime}}\mid{t^{\prime}}$
and (ii) $\gamma_{1}\cong\gamma_{2}$ then there exists $\gamma_{2}^{\prime}$
such that (i)
${\gamma_{2}}\mid{t}\,\longmapsto^{*}\,{\gamma_{2}^{\prime}}\mid{t^{\prime}}$
and (ii) $\gamma_{1}^{\prime}\cong\gamma_{2}^{\prime}$.

###### Lemma B.104 (Asymmetric diamond property of reduction closure).

Given two equivalent configurations
${\gamma_{1}}\mid{t}\cong{\gamma_{2}}\mid{t}$, if (1) $\gamma_{1}\vdash t$ and
$\gamma_{2}\vdash t$; (2) ${\gamma_{1}}\mid{t}\,\longmapsto^{\leq
1}\,{\gamma^{\prime}_{1}}\mid{t_{1}}$; and (3)
${\gamma_{2}}\mid{t}\,\longmapsto^{*}\,{\gamma^{\prime}_{2}}\mid{t_{2}}$, then
there exists $\gamma^{\prime\prime}_{1},t^{\prime},\gamma^{\prime\prime}_{2}$
such that (1)
${\gamma^{\prime}_{1}}\mid{t_{1}}\,\longmapsto^{*}\,{\gamma^{\prime\prime}_{1}}\mid{t^{\prime}}$,
(2) ${\gamma^{\prime}_{2}}\mid{t_{2}}\,\longmapsto^{\leq
1}\,{\gamma^{\prime\prime}_{2}}\mid{t^{\prime}}$, and (3)
${\gamma^{\prime\prime}_{1}}\mid{t^{\prime}}\cong{\gamma^{\prime\prime}_{2}}\mid{t^{\prime}}$.

###### Proof.

By induction on the length of the reduction
${\gamma_{2}}\mid{t}\,\longmapsto^{*}\,{\gamma^{\prime}_{2}}\mid{t_{2}}$.
_When there is zero step_. Then $\gamma^{\prime}_{2}=\gamma_{2}$ and
$t_{2}=t$. We can set $t^{\prime}=t_{1}$, then reduce $t_{2}$ one step to
$t_{1}$, and reduce $t_{1}$ zero step. _When
${\gamma_{2}}\mid{t}\,\longmapsto^{*}\,{\gamma^{\prime}_{2}}\mid{t_{2}}={\gamma_{2}}\mid{t}\,\longmapsto^{\leq
1}\,{\gamma_{0}}\mid{t_{0}}\,\longmapsto^{*}\,{\gamma^{\prime}_{2}}\mid{t_{2}}$_.
By Corollary B.100 we can show that there exists $t^{\prime}$ such that
${\gamma^{\prime}_{1}}\mid{t_{1}}\,\longmapsto^{\leq
1}\,{\gamma^{\prime\prime}_{1}}\mid{t^{\prime}}$,
${\gamma_{0}}\mid{t_{0}}\,\longmapsto^{\leq
1}\,{\gamma^{\prime}_{0}}\mid{t^{\prime}}$, and
$\gamma^{\prime\prime}_{1}\cong\gamma^{\prime}_{0}$ Now we use the
preservation theorem so that we can invoke IH to show that there exists
$t^{\prime\prime}$ such that
${\gamma^{\prime}_{0}}\mid{t^{\prime}}\,\longmapsto^{*}\,{\gamma^{\prime\prime}_{0}}\mid{t^{\prime\prime}}$,
${\gamma^{\prime}_{2}}\mid{t_{2}}\,\longmapsto^{\leq
1}\,{\gamma^{\prime\prime}_{2}}\mid{t^{\prime\prime}}$, and
$\gamma^{\prime\prime}_{0}\cong\gamma^{\prime\prime}_{2}$. Now we invoke
Corollary B.103 to show that there exists $\gamma^{\prime\prime\prime}_{1}$
such that
${\gamma^{\prime\prime}_{1}}\mid{t^{\prime}}\,\longmapsto^{*}\,{\gamma^{\prime\prime\prime}_{1}}\mid{t^{\prime\prime}}$,
and $\gamma^{\prime\prime\prime}_{1}\cong\gamma^{\prime\prime}_{0}$.
Therefore, we can show that
${\gamma^{\prime}_{1}}\mid{t_{1}}\,\longmapsto^{*}\,{\gamma^{\prime\prime\prime}_{1}}\mid{t^{\prime\prime}}$.
Also, we can show that
$\gamma^{\prime\prime\prime}_{1}\cong\gamma^{\prime\prime}_{2}$, and thus
conclude this case. ∎

###### Proof.

By induction on the length of the first reduction. _When the length is zero_.
This case can be trivially concluded. _When
${\gamma_{1}}\mid{t}\,\longmapsto^{\leq
1}\,{\gamma_{0}}\mid{t_{0}}\,\longmapsto^{*}\,{\gamma^{\prime}_{1}}\mid{t_{1}}$_.
We first invoke Lemma B.104 to show that $\exists t^{\prime}$ such that
${\gamma_{0}}\mid{t_{0}}\,\longmapsto^{*}\,{\gamma^{\prime}_{0}}\mid{t^{\prime}}$,
${\gamma^{\prime}_{2}}\mid{t_{2}}\,\longmapsto^{\leq
1}\,{\gamma^{\prime\prime}_{2}}\mid{t^{\prime}}$, and
$\gamma^{\prime}_{0}\cong\gamma^{\prime\prime}_{2}$. Then, we use the
preservation lemma so that we can invoke IH, showing that $\exists
t^{\prime\prime}$ such that
${\gamma^{\prime}_{1}}\mid{t_{1}}\,\longmapsto^{*}\,{\gamma^{\prime\prime}_{1}}\mid{t^{\prime\prime}}$,
${\gamma^{\prime}_{0}}\mid{t_{0}}\,\longmapsto^{*}\,{\gamma^{\prime\prime}_{0}}\mid{t^{\prime\prime}}$,
and $\gamma^{\prime\prime}_{1}\cong\gamma^{\prime\prime}_{0}$. Now by
Corollary B.103 we can show that $\exists\gamma^{\prime\prime\prime}_{2}$ such
that
${\gamma^{\prime\prime}_{2}}\mid{t^{\prime}}\,\longmapsto^{*}\,{\gamma^{\prime\prime\prime}_{2}}\mid{t^{\prime\prime}}$
and $\gamma^{\prime\prime\prime}_{2}\cong\gamma^{\prime\prime}_{0}$.
Therefore, we have
${\gamma^{\prime}_{2}}\mid{t_{2}}\,\longmapsto^{*}\,{\gamma^{\prime\prime\prime}_{2}}\mid{t^{\prime\prime}}$
and can show that
$\gamma^{\prime\prime\prime}_{2}\cong\gamma^{\prime\prime}_{1}$, thus
concluding this case. ∎

###### Lemma B.105 (Answers do not reduce).

Given any store $\gamma$ and an answer $a$,
${\gamma}\mid{a}\,\longmapsto\,{\gamma^{\prime}}\mid{t^{\prime}}$ is
impossible.

###### Proof.

By straightforward case analysis on the reduction derivation, wherein none of
the rules reduces an answer. ∎

###### Corollary B.106.

Given any store $\gamma$ and an answer $a$,
${\gamma}\mid{a}\,\longmapsto^{*}\,{\gamma^{\prime}}\mid{t}$ implies that
$\gamma^{\prime}=\gamma$ and $t=a$.

See 4.4

###### Proof.

We first use Theorem 4.3 to show that
$\exists\gamma_{1}^{\prime},\gamma_{2}^{\prime},t^{\prime}$ such that
${\gamma_{1}}\mid{a_{1}}\,\longmapsto^{*}\,{\gamma^{\prime}_{1}}\mid{t^{\prime}}$
and
${\gamma_{2}}\mid{a_{1}}\,\longmapsto^{*}\,{\gamma^{\prime}_{2}}\mid{t^{\prime}}$
where $\gamma^{\prime}_{1}\cong\gamma^{\prime}_{2}$. Now we use Corollary
B.106 to show that $t^{\prime}=a_{1}=a_{2}$, $\gamma_{1}=\gamma^{\prime}_{1}$
and $\gamma_{2}=\gamma^{\prime}_{2}$, which conclude our goal. ∎