appendix-defns.tex

% !TEX root = hazelnut-dynamics.tex

\newcommand{\additionalDefnsSec}{Additional Definitions for Hazelnut Live}
\section{\protect\additionalDefnsSec} % don't like the all-caps thing that the template does, so protecting it from that
\label{sec:additional-defns}

\subsection{Substitution}
\label{sec:substitution}
\judgbox
  {[\dexp/x]\dexp' = \dexp''}
  {$\dexp''$ is obtained by substituting $\dexp$ for $x$ in $\dexp'$}
  %% {$\dexp''$ is the result of substituting $\dexp$ for $u$ in $\dexp'$}

\vspace{5pt}
\judgbox
  {[\dexp/x]\sigma = \sigma'}
  {$\sigma'$ is obtained by substituting $\dexp$ for $x$ in $\sigma$}
  %% {$\dexp''$ is the result of substituting $\dexp$ for $u$ in $\dexp'$}
\[
\begin{array}{lcll}
\substitute{\dexp}{x}{c}
&=&
c\\
\substitute{\dexp}{x}{x}
&=&
\dexp
\\%
\substitute{\dexp}{x}{y}
&=&
y
& \text{when $x \neq y$}
\\
\substitute{\dexp}{x}{\halam{x}{\htau}{\dexp'}}
&=&
\halam{x}{\htau}{\dexp'}\\
\substitute{\dexp}{x}{\halam{y}{\htau}{\dexp'}}
&=&
\halam{y}{\htau}{\substitute{\dexp}{x}{\dexp'}}
& \text{when $x \neq y$ and $y \notin \fvof{d}$}
\\
\substitute{\dexp}{x}{\dap{\dexp_1}{\dexp_2}}
&=&
\dap{(\substitute{\dexp}{x}{\dexp_1})}{\substitute{\dexp}{x}{\dexp_2}}
\\
\substitute{\dexp}{x}{\dehole{u}{\subst}{}}
&=&
\dehole{u}{\substitute{\dexp}{x}{\subst}}{}
\\
\substitute{\dexp}{x}{\dhole{\dexp'}{u}{\subst}{}}
&=&
\dhole{\substitute{\dexp}{x}{\dexp'}}{u}{\substitute{\dexp}{x}{\subst}}{}
\\
\substitute{\dexp}{x}{\dcasttwo{\dexp'}{\htau_1}{\htau_2}}
&=&
\dcasttwo{(\substitute{\dexp}{x}{\dexp'})}{\htau_1}{\htau_2}
\\
\substitute{\dexp}{x}{\dcastfail{\dexp'}{\htau_1}{\htau_2}}
&=&
\dcastfail{(\substitute{\dexp}{x}{\dexp'})}{\htau_1}{\htau_2}
\\[6px]
\substitute{\dexp}{x}{\cdot}
&=&
\cdot\\
\substitute{\dexp}{x}{\sigma, d/y}
&=&
\substitute{\dexp}{x}{\sigma}, \substitute{\dexp}{x}{d}/y
%% {[\dexp_1 / x] \dcast{\htau}{\dexp}}
%% &=&
%% \dcast{\htau}{[\dexp_1 / x] \dexp}
\end{array}
\]

\vspace{5pt}
\begin{lem}[Substitution] \label{thm:substitution}~
\begin{enumerate}[nolistsep]
\item If $\hasType{\hDelta}{\hGamma, x : \htau'}{d}{\htau}$ and $\hasType{\hDelta}{\hGamma}{d'}{\htau'}$ then $\hasType{\hDelta}{\hGamma}{[d'/x]d}{\htau}$.
\item If $\hasType{\hDelta}{\hGamma, x : \htau'}{\sigma}{\hGamma'}$ and $\hasType{\hDelta}{\hGamma}{d'}{\htau'}$ then $\hasType{\hDelta}{\hGamma}{[d'/x]\sigma}{\hGamma'}$.
\end{enumerate}
\end{lem}
% \begin{proof} By rule induction on the first assumption in each case. The conclusion follows from the definition of substitution in each case. \end{proof}

\subsection{Canonical Forms}
\label{sec:canonical-forms}

\begin{lem}[Canonical Value Forms]\label{thm:canonincal-value-forms}
  If $\hasType{\hDelta}{\emptyset}{\dexp}{\htau}$ and $\isValue{\dexp}$
  then $\htau\neq\tehole$ and
  \begin{enumerate}[nolistsep]
    \item If $\htau=b$ then $\dexp=c$.
    \item If $\htau=\tarr{\htau_1}{\htau_2}$
          then $\dexp=\halam{x}{\htau_1}{\dexp'}$
          where $\hasType{\hDelta}{x : \htau_1}{\dexp'}{\htau_2}$.
  \end{enumerate}
\end{lem}

\begin{lem}[Canonical Boxed Forms]\label{thm:canonical-boxed-forms}
  If $\hasType{\hDelta}{\emptyset}{\dexp}{\htau}$ and $\isBoxedValue{\dexp}$
  then
  \begin{enumerate}[nolistsep]
    \item If $\htau=b$ then $\dexp=c$.
    \item If $\htau=\tarr{\htau_1}{\htau_2}$ then either
      \begin{enumerate}
        \item
          $\dexp=\halam{x}{\htau_1}{\dexp'}$
          where $\hasType{\hDelta}{x : \htau_1}{\dexp'}{\htau_2}$, or
        \item
          $\dexp=\dcasttwo{\dexp'}{\tarr{\htau_1'}{\htau_2'}}{\tarr{\htau_1}{\htau_2}}$
          where $\tarr{\htau_1'}{\htau_2'}\neq\tarr{\htau_1}{\htau_2}$
          and $\hasType{\hDelta}{\emptyset}{\dexp'}{\tarr{\htau_1'}{\htau_2'}}$.
      \end{enumerate}
    \item If $\htau=\tehole$
          then $\dexp=\dcasttwo{\dexp'}{\htau'}{\tehole}$
          where $\isGround{\htau'}$
          and $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$.
  \end{enumerate}
\end{lem}

\begin{lem}[Canonical Indeterminate Forms]
  If $\hasType{\hDelta}{\emptyset}{\dexp}{\htau}$
  and $\isIndet{\dexp}$
  then
  \begin{enumerate}[nolistsep]
    \item 
      If $\htau = b$ then either
        \begin{enumerate}
          \item $\dexp = \dehole{u}{\subst}{}$ where $\Dbinding{u}{\Gamma}{b} \in \hDelta$ and $\hasType{\hDelta}{\emptyset}{\subst}{\hGamma}$, or
          \item $\dexp = \dhole{\dexp'}{u}{\subst}{}$ where $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$ and $\isFinal{\dexp'}$ and $\Dbinding{u}{\Gamma}{b} \in \hDelta$ and $\hasType{\hDelta}{\emptyset}{\subst}{\hGamma}$, or
          \item $\dexp = \dap{\dexp_1}{\dexp_2}$ where $\hasType{\hDelta}{\emptyset}{\dexp_1}{\tarr{\htau_2}{b}}$ and $\hasType{\hDelta}{\emptyset}{\dexp_2}{\htau_2}$ and $\isIndet{\dexp_1}$ and $\isFinal{\dexp_2}$ and $\dexp_1 \neq \dcasttwo{\dexp_1'}{\tarr{\htau_3}{\htau_4}}{\tarr{\htau_3'}{\htau_4'}}$ for any $\dexp_1', \htau_3, \htau_4, \htau_3', \htau_4'$, or 
          \item $\dexp = \dcasttwo{\dexp'}{\tehole}{b}$ where $\hasType{\hDelta}{\emptyset}{\dexp'}{\tehole}$ and $\isIndet{\dexp'}$ and $\dexp' \neq \dcasttwo{\dexp''}{\htau'}{\tehole}$ for any $\dexp'', \htau'$, or 
          \item $\dexp = \dcastfail{\dexp'}{\htau'}{b}$ where $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$ and $\isGround{\htau'}$ and $\htau' \neq b$.
        \end{enumerate}
    \item 
      If $\htau = \tarr{\htau_1}{\htau_2}$ then either 
        \begin{enumerate}
          \item $\dexp = \dehole{u}{\subst}{}$ where $\Dbinding{u}{\Gamma}{\tarr{\htau_1}{\htau_2}} \in \hDelta$ and $\hasType{\hDelta}{\emptyset}{\subst}{\hGamma}$, or
          \item $\dexp = \dhole{\dexp'}{u}{\subst}{}$ where $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$ and $\isFinal{\dexp'}$ and $\Dbinding{u}{\Gamma}{\tarr{\htau_1}{\htau_2}} \in \hDelta$ and $\hasType{\hDelta}{\emptyset}{\subst}{\hGamma}$, or
          \item $\dexp = \dap{\dexp_1}{\dexp_2}$ where $\hasType{\hDelta}{\emptyset}{\dexp_1}{\tarr{\htau_2'}{\tarr{\htau_1}{\htau_2}}}$ and $\hasType{\hDelta}{\emptyset}{\dexp_2}{\htau_2'}$ and $\isIndet{\dexp_1}$ and $\isFinal{\dexp_2}$ and $\dexp_1 \neq \dcasttwo{\dexp_1'}{\tarr{\htau_3}{\htau_4}}{\tarr{\htau_3'}{\htau_4'}}$ for any $\dexp_1', \htau_3, \htau_4, \htau_3', \htau_4'$, or 
          \item $\dexp = \dcasttwo{\dexp'}{\tarr{\htau_1'}{\htau_2'}}{\tarr{\htau_1}{\htau_2}}$ where $\hasType{\hDelta}{\emptyset}{\dexp'}{\tarr{\htau_1'}{\htau_2'}}$ and $\isIndet{\dexp'}$ and $\tarr{\htau_1'}{\htau_2'} \neq \tarr{\htau_1}{\htau_2}$, or 
          \item $\dexp = \dcasttwo{\dexp'}{\tehole}{\tarr{\tehole}{\tehole}}$ and $\htau_1 = \tehole$ and $\htau_2 = \tehole$ where $\hasType{\hDelta}{\emptyset}{\dexp'}{\tehole}$ and $\isIndet{\dexp'}$ and $\dexp' \neq \dcasttwo{\dexp''}{\htau'}{\tehole}$ for any $\dexp'', \htau'$, or 
          \item $\dexp = \dcastfail{\dexp'}{\htau'}{\tarr{\tehole}{\tehole}}$ and $\htau_1 = \tehole$ and $\htau_2 = \tehole$ where $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$ and $\isGround{\htau'}$ and $\htau' \neq \tarr{\tehole}{\tehole}$.
        \end{enumerate}
    \item 
      If $\htau = \tehole$ then either 
        \begin{enumerate}
          \item $\dexp = \dehole{u}{\subst}{}$ where $\Dbinding{u}{\Gamma}{\tehole} \in \hDelta$ and $\hasType{\hDelta}{\emptyset}{\subst}{\hGamma}$, or
          \item $\dexp = \dhole{\dexp'}{u}{\subst}{}$ where $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$ and $\isFinal{\dexp'}$ and $\Dbinding{u}{\Gamma}{\tehole} \in \hDelta$ and $\hasType{\hDelta}{\emptyset}{\subst}{\hGamma}$, or
          \item $\dexp = \dap{\dexp_1}{\dexp_2}$ and $\hasType{\hDelta}{\emptyset}{\dexp_1}{\tarr{\htau_2}{\tehole}}$ and $\hasType{\hDelta}{\emptyset}{\dexp_2}{\htau_2}$ and $\isIndet{\dexp_1}$ and $\isFinal{\dexp_2}$ and $\dexp_1 \neq \dcasttwo{\dexp_1'}{\tarr{\htau_3}{\htau_4}}{\tarr{\htau_3'}{\htau_4'}}$ for any $\dexp_1', \htau_3, \htau_4, \htau_3', \htau_4'$, or 
          \item $\dexp = \dcasttwo{\dexp'}{\htau'}{\tehole}$ where $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$ and $\isGround{\htau'}$ and $\isIndet{\dexp'}$.
        \end{enumerate}
  \end{enumerate}
  % \begin{enumerate}[nolistsep]
  %   \item
  %     $\dexp=\dehole{u}{\subst}{}$
  %     and $\Dbinding{u}{\Gamma'}{\htau}\in\hDelta$, or
  %   \item
  %     $\dexp=\dhole{\dexp'}{u}{\subst}{}$
  %     and $\isFinal{\dexp'}$
  %     and $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$
  %     and $\Dbinding{u}{\Gamma'}{\htau}\in\hDelta$, or
  %   \item
  %     $\dexp=\dap{\dexp_1}{\dexp_2}$
  %     and $\hasType{\hDelta}{\emptyset}{\dexp_1}{\tarr{\htau_2}{\htau}}$
  %     and $\hasType{\hDelta}{\emptyset}{\dexp_2}{\htau_2}$
  %     and $\isIndet{\dexp_1}$
  %     and $\isFinal{\dexp_2}$
  %     and $\dexp_1\neq\dcasttwo{\dexp_1}{\tarr{\htau_3}{\htau_4}}
  %                                       {\tarr{\htau_3'}{\htau_4'}}$, or
  %   %% \item
  %   %%   \begin{enumerate}
  %   %%     \item blah
  %   %%     \item blah
  %   %%     \item blah
  %   %%   \end{enumerate}
  %   \item
  %     $\htau=b$
  %     and $\dexp=\dcasttwo{\dexp'}{\tehole}{b}$
  %     and $\isIndet{\dexp'}$
  %     and $\dexp'\neq\dcasttwo{\dexp''}{\htau'}{\tehole}$, or
  %   \item
  %     $\htau=b$
  %     and $\dexp=\dcastfail{\dexp'}{\htau'}{b}$
  %     and $\isGround{\htau'}$
  %     and $\htau'\neq{b}$
  %     and $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$, or
  %   \item
  %     $\htau=\tarr{\htau_{11}}{\htau_{12}}$
  %     and $\dexp=\dcasttwo{\dexp'}{\tarr{\htau_1}{\htau_2}}
  %                                 {\tarr{\htau_{11}}{\htau_{12}}}$
  %     and $\isIndet{\dexp'}$
  %     and $\tarr{\htau_1}{\htau_2}\neq\tarr{\htau_{11}}{\htau_{12}}$, or
  %   \item
  %     $\htau=\tarr{\tehole}{\tehole}$
  %     %% $\htau=\tarr{\htau_{11}}{\htau_{12}}$
  %     %% and $\htau_{11}=\tehole$
  %     %% and $\htau_{12}=\tehole$
  %     and $\dexp=\dcastthree{\dexp'}{\tehole}{\tehole}{\tehole}$
  %     and $\isIndet{\dexp'}$
  %     and $\dexp'\neq\dcasttwo{\dexp''}{\htau'}{\tehole}$, or
  %   \item
  %     $\htau=\tarr{\tehole}{\tehole}$
  %     %% $\htau=\tarr{\htau_{11}}{\htau_{12}}$
  %     %% and $\htau_{11}=\tehole$
  %     %% and $\htau_{12}=\tehole$
  %     and $\dexp=\dcastfail{\dexp'}{\htau'}{\tarr{\tehole}{\tehole}}$
  %     %% and $\dexp=\dcastfail{\dexp'}{\htau'}{\tarr{\htau_{11}}{\htau_{12}}}$
  %     and $\htau'\neq\htau$
  %     and $\isGround{\htau'}$
  %     and $\isIndet{\dexp'}$
  %     and $\hasType{\hDelta}{\emptyset}{\dexp'}{\htau'}$, or
  %   \item
  %     $\htau=\tehole$
  %     and $\dexp=\dcasttwo{\dexp'}{\htau'}{\tehole}$
  %     and $\isGround{\htau'}$
  %     and $\isIndet{\dexp'}$.
  % \end{enumerate}
\end{lem}

% The proofs for all three of these theorems follow by straightforward rule induction.

% No weakening for Gammas in Delta:
% If $\hasType{\Delta, \Dbinding{u}{\hGamma}{\tau}}{\hGamma'}{d}{\tau'}$ then $\hasType{\Delta, \Dbinding{u}{\hGamma, x : \tau''}{\tau}}{\hGamma'}{d}{\tau'}$.

\subsection{Complete Programs}
\label{sec:complete-programs}

\input{fig-complete}

\subsection{Multiple Steps}
\label{sec:multi-step}

\input{fig-multi-step}

\subsection{Hole Filling}\label{sec:hole-filling}
\begin{lem}[Filling] ~
  \begin{enumerate}[nolistsep]
  \item If $\hasType{\hDelta, \Dbinding{u}{\hGamma'}{\htau'}}{\hGamma}{\dexp}{\tau}$
  and $\hasType{\hDelta}{\hGamma'}{\dexp'}{\htau'}$
  then $\hasType{\hDelta}{\hGamma}{\instantiate{\dexp'}{u}{\dexp}}{\tau}$.
  \item If $\hasType{\hDelta, \Dbinding{u}{\hGamma'}{\htau'}}{\hGamma}{\sigma}{\hGamma''}$
  and $\hasType{\hDelta}{\hGamma'}{\dexp'}{\htau'}$
  then $\hasType{\hDelta}{\hGamma}{\instantiate{\dexp'}{u}{\sigma}}{\hGamma''}$.
  \end{enumerate}
\end{lem}
\begin{proof}
In each case, we proceed by rule induction on the first assumption, appealing to the Substitution Lemma as necessary.
\end{proof}

To prove the Commutativity theorem, we need the auxiliary definitions in Fig.~\ref{fig:evalctx-filling}, which lift hole filling to evaluation contexts taking care to consider the special situation where the mark is inside the hole that is being filled.
\input{fig-evalctx-instantiation}

We also need the following lemmas, which characterize how hole filling interacts with substitution and instruction transitions. 
\begin{lem}[Substitution Commutativity]
  If
  \begin{enumerate}[nolistsep]
  	\item $\hasType{\hDelta, \Dbinding{u}{\hGamma'}{\htau'}}{x : \htau_2}{\dexp_1}{\tau}$ and
  	\item $\hasType{\hDelta, \Dbinding{u}{\hGamma'}{\htau'}}{\emptyset}{\dexp_2}{\htau_2}$ and
  	\item $\hasType{\hDelta}{\hGamma'}{\dexp'}{\htau'}$
  \end{enumerate}

  then  $\instantiate{d'}{u}{\substitute{d_2}{x}{d_1}} = \substitute{\instantiate{d'}{u}{d_2}}{x}{\instantiate{d'}{u}{d_1}}$.
\end{lem}
\begin{proof}
We proceed by structural induction on $d_1$ and rule induction on the typing premises, which serve to ensure that the free
variables in $d'$ are accounted for by every closure for $u$.
\end{proof}

\begin{lem}[Instruction Commutativity]
  If
  \begin{enumerate}[nolistsep]
  	\item $\hasType{\hDelta, \Dbinding{u}{\hGamma'}{\htau'}}{\emptyset}{\dexp_1}{\tau}$ and
  	\item $\hasType{\hDelta}{\hGamma'}{\dexp'}{\htau'}$ and
  	\item $\reducesE{}{\dexp_1}{\dexp_2}$
  \end{enumerate}

  then $\reducesE{}{\instantiate{\dexp'}{u}{\dexp_1}}
                     {\instantiate{\dexp'}{u}{\dexp_2}}$.
\end{lem}
\begin{proof}
We proceed by cases on the instruction transition assumption (no induction is needed). For Rule \rulename{ITLam}, we defer to the Substitution Commutativity lemma above. For the remaining cases, the conclusion follows from the definition of hole filling.
\end{proof}

\begin{lem}[Filling Totality]
Either $\inhole{u}{\evalctx}$ or $\instantiate{d}{u}{\evalctx}=\evalctx'$ for some $\evalctx'$.
\end{lem}
\begin{proof} We proceed by structural induction on $\evalctx$. Every case is handled by one of the two judgements. \end{proof}

\begin{lem}[Discarding] If
	\begin{enumerate}[nolistsep]
	\item $\selectEvalCtx{d_1}{\evalctx}{\dexp_1'}$ and
	\item $\selectEvalCtx{d_2}{\evalctx}{\dexp_2'}$ and
	\item $\inhole{u}{\evalctx}$
	\end{enumerate}

	then $\instantiate{d}{u}{d_1} = \instantiate{d}{u}{d_2}$.
\end{lem}
\begin{proof} We proceed by structural induction on $\evalctx$ and rule induction on all three assumptions. Each case follows from the definition of instruction selection and hole filling. \end{proof}


\begin{lem}[Filling Distribution] If
	$\selectEvalCtx{d_1}{\evalctx}{d_1'}$ and $\instantiate{d}{u}{\evalctx}=\evalctx'$ then $\selectEvalCtx{\instantiate{d}{u}{d_1}}{\evalctx'}{\instantiate{d}{u}{d_1'}}$.
\end{lem}
\begin{proof} We proceed by rule induction on both assumptions. Each case follows from the definition of instruction selection and hole filling. \end{proof}


\begin{thm}[Commutativity]
  If
  \begin{enumerate}[nolistsep]
  \item $\hasType{\hDelta, \Dbinding{u}{\hGamma'}{\htau'}}{\emptyset}{\dexp_1}{\tau}$ and
  \item $\hasType{\hDelta}{\hGamma'}{\dexp'}{\htau'}$ and
  \item $\multiStepsTo{\dexp_1}{\dexp_2}$
\end{enumerate}

  then $\multiStepsTo{\instantiate{\dexp'}{u}{\dexp_1}}
                     {\instantiate{\dexp'}{u}{\dexp_2}}$.
\end{thm}
\begin{proof}
By rule induction on assumption (3). The reflexive case is immediate. In the inductive case, we proceed by rule induction on the stepping premise. There is one rule, Rule~\rulename{Step}. By Filling Totality, either $\inhole{u}{\evalctx}$ or $\instantiate{d}{u}{\evalctx} = \evalctx'$. In the former case, by Discarding, we can conclude by \rulename{MultiStepRefl}. In the latter case, by Instruction Commutativity and Filling Distribution we can take a \rulename{Step}, and we can conclude via \rulename{MultiStepSteps} by applying Filling, Preservation and then the induction hypothesis.
\end{proof}

% We excluded these proofs and definitions from the Agda mechanization
% for two reasons.
% %
% First, fill-and-resume is merely an optimization, and unlike the meta
% theory of \Secref{sec:calculus}, these properties are generally not
% conserved by certain reasonable extensions of the core
% calculus~(e.g., reference cells and other non-commuting effects).
% %
% Second, to properly encode the hole filling operation, such a
% mechanization requires a more complex representation of
% hole environments; unfortunately, Agda cannot be easily convinced that
% the definition of hole filling is well-founded (\citet{Nanevski2008}
% establish that it is in fact well-founded).
% %
% By contrast, the developments in \Secref{sec:calculus} do not require
% these more complex representations. 


\subsection{Confluence and Resumption}\label{sec:confluence}
There are various ways to encode the intuition that ``evaluation order does not matter''. One way to do so is
by establishing a confluence property (which is closely related to
the Church-Rosser property \cite{church1936some}).

The most general confluence property does not hold for the dynamic
semantics in Sec.~\ref{sec:calculus} for the usual reason: we do not
reduce under binders (\citet{DBLP:conf/birthday/BlancLM05} discuss the
standard counterexample).
%
We could recover confluence by specifying reduction under binders,
either generally or in a more restricted form where only closed
sub-expressions are
reduced \cite{DBLP:journals/tcs/CagmanH98,DBLP:conf/birthday/BlancLM05,levy1999explicit}.
%
However, reduction under binders conflicts with the standard implementation approaches
for most programming languages \cite{DBLP:conf/birthday/BlancLM05}.
%
A more satisfying approach considers confluence modulo equality \cite{Huet:1980ng}.
%
The simplest such approach restricts our interest to top-level expressions
of base type that result in values, in which case the following
special case of confluence does hold (trivially when the only base
type has a single value, but also more generally for other base
types).
\begin{lem}[Base Confluence]
  If $\hasType{\Delta}{\emptyset}{\dexp}{b}$ and
  $\multiStepsTo{\dexp}{\dexp_1}$
  and $\isValue{\dexp_1}$
  and $\multiStepsTo{\dexp}{\dexp_2}$
  then $\multiStepsTo{\dexp_2}{\dexp_1}$.
\end{lem}
We can then prove the following property, which establishes that fill-and-resume is sound.
\begin{thm}[Resumption]
  If $\hasType{\hDelta, \Dbinding{u}{\hGamma'}{\htau'}}{\emptyset}{\dexp}{b}$
  and $\hasType{\hDelta}{\hGamma'}{\dexp'}{\htau'}$
  and $\multiStepsTo{\dexp}{\dexp_1}$
  and $\multiStepsTo{\instantiate{\dexp'}{u}{\dexp}}{\dexp_2}$
  and $\isValue{\dexp_2}$
  then $\multiStepsTo{\instantiate{\dexp'}{u}{\dexp_1}}{\dexp_2}$.
  \begin{proof}
    By Commutativity,
    $\multiStepsTo{\instantiate{\dexp'}{u}{\dexp}}
                  {\instantiate{\dexp'}{u}{\dexp_1}}$.
    By Base Confluence, we can conclude.
  \end{proof}
\end{thm}