tr-NA-proof.tex

% tried and failed ...
% - asymmetric B<=B relations, to keep boundaries in sync,
%   but they aren't always in sync --- H can "remove" some after they pass
%   (maybe we need to remember those)
%
% - ignorant <= relation, U(e) = U(e')
%   but this gives too-weak premises for the simulation lemmas to pass
%
% - contexts matched, holes allow monitor mismatches (not caring about
%   matching monitors on functions)
%
% - contexts matches via (stat dyn e0 <~ blame [b0 b1] e1)
%   trouble is need to allow (stat e0 <~ e1) mis-matches
%   and it is a lot of case analysis, approaching N^2

\begin{flushleft}

\lbl{\fbox{$\rexpr{\svalue}{\svalue}$}}{\begin{mathpar}
  \inferrule*{
  }{
    \rexpr{\sint_0}{\sint_0}
  }

  \inferrule*{
  }{
    \rexpr{\sint_0}{\ehist{\sblist_0}{\sint_0}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\svalue_2}
    \\
    \rexpr{\svalue_1}{\svalue_3}
  }{
    \rexpr{\epair{\svalue_0}{\svalue_1}}{\epair{\svalue_2}{\svalue_3}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\emopt{\fbndfst{\sbnd_0}}{\svalue_2}}
    \\
    \rexpr{\svalue_1}{\emopt{\fbndsnd{\sbnd_0}}{\svalue_3}}
  }{
    \rexpr{\epair{\svalue_0}{\svalue_1}}{\emon{\sbnd_0}{\epair{\svalue_2}{\svalue_3}}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\faddtrace{\fbndfst{\sblist_0}}{\svalue_2}}
    \\
    \rexpr{\svalue_1}{\faddtrace{\fbndsnd{\sblist_0}}{\svalue_3}}
  }{
    \rexpr{\epair{\svalue_0}{\svalue_1}}{\ehist{\sblist_0}{\epair{\svalue_2}{\svalue_3}}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\faddtrace{\fbndfst{\sblist_0}}{(\emopt{\fbndfst{\sbnd_1}}{\svalue_2})}}
    \\\\
    \rexpr{\svalue_1}{\faddtrace{\fbndsnd{\sblist_0}}{(\emopt{\fbndsnd{\sbnd_1}}{\svalue_3})}}
  }{
    \rexpr{\epair{\svalue_0}{\svalue_1}}{\ehist{\sblist_0}{(\emon{\sbnd_1}{\epair{\svalue_2}{\svalue_3}})}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\emopt{\fbndfst{\sbnd_0}}{(\faddtrace{\fbndfst{\sblist_1}}{\svalue_2})}}
    \\
    \rexpr{\svalue_1}{\emopt{\fbndsnd{\sbnd_1}}{(\faddtrace{\fbndsnd{\sblist_1}}{\svalue_3})}}
  }{
    \rexpr{\epair{\svalue_0}{\svalue_1}}{\emon{\sbnd_0}{(\ehist{\sblist_1}{\epair{\svalue_2}{\svalue_3}})}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\emopt{\fbndfst{\sbnd_0}}{(\emopt{\fbndfst{\sbnd_1}}{\svalue_2})}}
    \\
    \rexpr{\svalue_1}{\emopt{\fbndsnd{\sbnd_0}}{(\emopt{\fbndsnd{\sbnd_1}}{\svalue_3})}}
  }{
    \rexpr{\epair{\svalue_0}{\svalue_1}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{\epair{\svalue_2}{\svalue_3}})}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\emopt{\fbndfst{\sbnd_0}}{(\faddtrace{\fbndfst{\sblist_1}}{(\emon{\fbndfst{\sbnd_2}}{\svalue_2}))})}}
    \\
    \rexpr{\svalue_1}{\emopt{\fbndsnd{\sbnd_0}}{(\faddtrace{\fbndsnd{\sblist_1}}{(\emon{\fbndsnd{\sbnd_2}}{\svalue_3}))})}}
  }{
    \rexpr{\epair{\svalue_0}{\svalue_1}}{\emon{\sbnd_0}{(\ehist{\sblist_1}{(\emon{\sbnd_2}{\epair{\svalue_2}{\svalue_3}})})}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\emoptplus{\fbndfst{\sblist_0}}{(\emopt{\fbndfst{\sbnd_1}}{(\emopt{\fbndfst{\sbnd_2}}{\svalue_2})})}}
    \\
    \rexpr{\svalue_1}{\emoptplus{\fbndsnd{\sblist_0}}{(\emopt{\fbndsnd{\sbnd_1}}{(\emopt{\fbndsnd{\sbnd_2}}{\svalue_3})})}}
  }{
    \rexpr{\epair{\svalue_0}{\svalue_1}}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\emon{\sbnd_2}{\epair{\svalue_2}{\svalue_3}})})}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\emoptplus{\fbndfst{\sblist_0}}{(\emopt{\fbndfst{\sbnd_1}}{(\faddtrace{\fbndfst{\sblist_2}}{(\emopt{\fbndfst{\sbnd_3}}{\svalue_2})})})}}
    \\
    \rexpr{\svalue_1}{\emoptplus{\fbndsnd{\sblist_0}}{(\emopt{\fbndsnd{\sbnd_1}}{(\faddtrace{\fbndsnd{\sblist_2}}{(\emopt{\fbndsnd{\sbnd_3}}{\svalue_3})})})}}
  }{
    \rexpr{\epair{\svalue_0}{\svalue_1}}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_2}{\svalue_3}})})})}}
  }

  \inferrule*{
    \rexpr{\sexpr_0}{\sexpr_1}
  }{
    \rexpr{\efun{\svar_0}{\sexpr_0}}{\efun{\svar_0}{\sexpr_1}}
  }

  \inferrule*{
    \rexpr{\sexpr_0}{\sexpr_1}
  }{
    \rexpr{\efun{\tann{\svar_0}{\stype_0}}{\sexpr_0}}{\efun{\tann{\svar_0}{\stype_0}}{\sexpr_1}}
  }

  \inferrule*{
    \svalue_1 \in \efun{\svar}{\sexpr} \cup \emon{\sbnd}{(\efun{\tann{\svar}{\stype}}{\sexpr})}
    \\\\
    \sbnd_0 \subteq \sbnd_2
    \\
    \sbnd_1 \subteq \sbnd_3
    \\
    \rexpr{\svalue_0}{\svalue_1}
  }{
    \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_1}{\svalue_0})}}{\ehist{\fconcat{\sbnd_2}{\fconcat{\sbnd_3}{\snil}}}{\svalue_1}}
  }

  \inferrule*{
    \svalue_1 \in \efun{\svar}{\sexpr} \cup \emon{\sbnd}{(\efun{\tann{\svar}{\stype}}{\sexpr})}
    \\\\
    \sbnd_0 \subteq \sbnd_2
    \\
    \sbnd_1 \subteq \sbnd_3
    \\
    \rexpr{\svalue_0}{\ehist{\sblist_4}{\svalue_1}}
  }{
    \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_1}{\svalue_0})}}{\ehist{\fconcat{\sbnd_2}{\fconcat{\sbnd_3}{\sblist_4}}}{\svalue_1}}
  }

  \inferrule*{
    \sbnd_0 \subteq \sbnd_1
    \\
    \rexpr{\svalue_0}{\svalue_1}
  }{
    \rexpr{\emon{\sbnd_0}{\svalue_0}}{\emon{\sbnd_1}{\svalue_1}}
  }

\end{mathpar}}

\lbl{\fbox{$\rexpr{\sexpr}{\sexpr}$}}{\begin{mathpar}
  \inferrule*{
  }{
    \rexpr{\svar_0}{\svar_0}
  }

  \inferrule*{
    \rexpr{\sexpr_0}{\sexpr_2}
    \\
    \rexpr{\sexpr_1}{\sexpr_3}
  }{
    \rexpr{\epair{\sexpr_0}{\sexpr_1}}{\epair{\sexpr_2}{\sexpr_3}}
  }

  \inferrule*{
    \rexpr{\sexpr_0}{\sexpr_2}
    \\
    \rexpr{\sexpr_1}{\sexpr_3}
  }{
    \rexpr{\eapp{\toptional_0}{\sexpr_0}{\sexpr_1}}{\eapp{\toptional_0}{\sexpr_2}{\sexpr_3}}
  }

  \inferrule*{
    \rexpr{\sexpr_0}{\sexpr_1}
  }{
    \rexpr{\eunopt{\stoptional}{\sexpr_0}}{\eunopt{\stoptional}{\sexpr_1}}
  }

  \inferrule*{
    \rexpr{\sexpr_0}{\sexpr_2}
    \\
    \rexpr{\sexpr_1}{\sexpr_3}
  }{
    \rexpr{\ebinopt{\stoptional}{\sexpr_0}{\sexpr_1}}{\ebinopt{\stoptional}{\sexpr_2}{\sexpr_3}}
  }

  \inferrule*{
    \sbnd_0 \subteq \sbnd_1
    \\
    \rexpr{\sexpr_0}{\sexpr_1}
  }{
    \rexpr{\edynb{\sbnd_0}{\sexpr_0}}{\edynb{\sbnd_1}{\sexpr_1}}
  }

  \inferrule*{
    \sbnd_0 \subteq \sbnd_1
    \\
    \rexpr{\sexpr_0}{\sexpr_1}
  }{
    \rexpr{\estab{\sbnd_0}{\sexpr_0}}{\estab{\sbnd_1}{\sexpr_1}}
  }

  \inferrule*{
    \sbnd_0 \subteq \sbnd_2
    \\
    \sbnd_1 \subteq \sbnd_3
    \\\\
    \rexpr{\sexpr_0}{\eprehist{\sblist_4}{\sexpr_1}}
  }{
    \rexpr{\estab{\sbnd_0}{(\edynb{\sbnd_1}{\sexpr_0})}}{\eprehist{\fconcat{\sbnd_2}{\fconcat{\sbnd_3}{\sblist_4}}}{\sexpr_1}}
  }

  \inferrule*{
  }{
    \rexpr{\tagerrorS}{\tagerrorS}
  }

  \inferrule*{
  }{
    \rexpr{\tagerrorD}{\tagerrorD}
  }


  \inferrule*{
  }{
    \rexpr{\divisionbyzeroerror}{\divisionbyzeroerror}
  }

  \inferrule*{
  }{
    \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\sexpr_1}
  }

\end{mathpar}}

\lbl{\fbox{$\rctx{\ctx}{\ctx}$}}{\begin{mathpar}
  \inferrule*{
  }{
    \rctx{\ctxhole}{\ctxhole}
  }

  \inferrule*{
    \rctx{\ctx_0}{\ctx_2}
    \\
    \rexpr{\sexpr_1}{\sexpr_3}
  }{
    \rctx{\epair{\ctx_0}{\sexpr_1}}{\epair{\ctx_2}{\sexpr_3}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\svalue_2}
    \\
    \rctx{\ctx_1}{\ctx_3}
  }{
    \rctx{\epair{\svalue_0}{\ctx_1}}{\epair{\svalue_2}{\ctx_3}}
  }

  \inferrule*{
    \rctx{\ctx_0}{\ctx_2}
    \\
    \rexpr{\sexpr_1}{\sexpr_3}
  }{
    \rctx{\eapp{\toptional_0}{\ctx_0}{\sexpr_1}}{\eapp{\toptional_0}{\ctx_2}{\sexpr_3}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\svalue_2}
    \\
    \rctx{\ctx_1}{\ctx_3}
  }{
    \rctx{\eapp{\toptional_0}{\svalue_0}{\ctx_1}}{\eapp{\toptional_0}{\svalue_2}{\ctx_3}}
  }

  \inferrule*{
    \rctx{\ctx_0}{\ctx_1}
  }{
    \rctx{\eunopt{\stoptional}{\ctx_0}}{\eunopt{\stoptional}{\ctx_1}}
  }

  \inferrule*{
    \rctx{\ctx_0}{\ctx_2}
    \\
    \rexpr{\sexpr_1}{\sexpr_3}
  }{
    \rctx{\ebinopt{\stoptional}{\ctx_0}{\sexpr_1}}{\ebinopt{\stoptional}{\ctx_2}{\sexpr_3}}
  }

  \inferrule*{
    \rexpr{\svalue_0}{\svalue_2}
    \\
    \rctx{\ctx_1}{\ctx_3}
  }{
    \rctx{\ebinopt{\stoptional}{\svalue_0}{\ctx_1}}{\ebinopt{\stoptional}{\svalue_2}{\ctx_3}}
  }

  \inferrule*{
    \sbnd_0 \subteq \sbnd_1
    \\
    \rctx{\ctx_0}{\ctx_1}
  }{
    \rctx{\edynb{\sbnd_0}{\ctx_0}}{\edynb{\sbnd_1}{\ctx_1}}
  }

  \inferrule*{
    \sbnd_0 \subteq \sbnd_1
    \\
    \rctx{\ctx_0}{\ctx_1}
  }{
    \rctx{\estab{\sbnd_0}{\ctx_0}}{\estab{\sbnd_1}{\ctx_1}}
  }

  \inferrule*{
    \sbnd_0 \subteq \sbnd_2
    \\
    \sbnd_1 \subteq \sbnd_3
    \\
    \rctx{\ctx_0}{\eprehist{\sblist_4}{\ctx_1}}
  }{
    \rctx{\estab{\sbnd_0}{(\edynb{\sbnd_1}{\ctx_0})}}{\eprehist{\fconcat{\sbnd_2}{\fconcat{\sbnd_3}{\sblist_4}}}{\ctx_1}}
  }
\end{mathpar}}

\end{flushleft}

\vfill
%% -----------------------------------------------------------------------------
\newpage

\begin{corollary}
  If\/ $\fwellformed{\sexpr_0}{\stoptional}$
  and\/ $\sexpr_0 \rredA \boundaryerror{\sblist_2}{\svalue_2}$
  then\/ $\sexpr_0 \rredN \boundaryerror{\sbnd_1}{\svalue_1}$
\end{corollary}
\begin{lamportproof}
  By \lemmaref{HA-simulation}
  and the fact that $\rexpr{\sexpr}{\boundaryerror{\sblist_2}{\svalue_2}}$ implies $\sexpr \in \boundaryerror{\sbnd}{\svalue}$
\end{lamportproof}

\begin{example}
  There exists\/ $\fwellformed{\sexpr_0}{\stoptional}$
  such that\/ $\sexpr_0 \rredA \boundaryerror{\sblist_2}{\svalue_2}$
  and\/ $\sexpr_0 \rredN \boundaryerror{\sbnd_1}{\svalue_1}$
  and\/ $\sbnd_1 \not\in \sblist_2$
\end{example}
\begin{lamportproof}
  Choose any $\sexpr_0$ where \Nname{} detects an error that \Aname{} misses,
   and then \Aname{} detects an error at a boundary between two different
   components, e.g.:

  \(\begin{array}{l@{~}l}
    \sexpr_0 \eeq \ssum & {(\efst{\tnat}{(\edynb{\obnd{\sowner_0}{\obars{\tpair{\tnat}{\tnat}}{\sowner_1}}{\sowner_1}}{\epair{0}{{-1}}})})}
    \\                  & {(\edynb{\obnd{\sowner_0}{\obars{\tnat}{\sowner_1}}{\sowner_1}}{(\estab{\obnd{\sowner_1}{\obars{\tnat}{\sowner_2}}{\sowner_2}}{(\edynb{\obnd{\sowner_2}{\obars{\tnat}{\sowner_3}}{\sowner_3}}{{-1}})})})}
  \end{array}\)
\end{lamportproof}

\begin{theorem}
  If\/ $\fwellformed{\sexpr_0}{\stoptional}$
  and\/ $\sexpr_0 \rredN \sexpr_1 \credN \boundaryerror{\sbnd_1}{\svalue_1}$
  then\/ $\exists\,\sexpr_2$ such that $\sexpr_0 \rredA \sexpr_2$ and one of the following holds:
  \begin{itemize}
    \item
      $\rexpr{\sexpr_1}{\sexpr_2}$, or
    \item
      $\sexpr_1 \eeq \ctx_1[\eapp{\stype_2}{\svalue_0}{(\edynb{\sbnd_1}{\svalue_1})}]$
      and\/ $\sexpr_2 \eeq \ctx_2[\eapp{\stype_2}{(\ehist{\sblist_2}{\svalue_2})}{\svalue_3}]$
      and\/ $\rctx{\ctx_1}{\ctx_2}$ and $\fflip{\sbnd_1} \in \sblist_2$
  \end{itemize}
\end{theorem}
\begin{lamportproof}
  by \lemmaref{HA-simulation} and \lemmaref{H-app-A-bnd}.
\end{lamportproof}

\begin{example}
  There exists\/ $\fwellformed{\sexpr_0}{\stoptional}$
  such that\/ $\sexpr_0 \rredN \boundaryerror{\sbnd_1}{\svalue_1}$
  and\/ $\sexpr_0 \rredA \svalue_1$
\end{example}
\begin{lamportproof}
  $\sexpr_0 \eeq \edynb{\obnd{\sowner_0}{\tpair{\tnat}{\tnat}}{\sowner_1}}{\epair{-1}{{-2}}}$
\end{lamportproof}

\begin{lemma}[$\srexpr$ surface reflexivity]
  If\/ $\fwellformed{\sexpr_0}{\stoptional}$
  then\/ $\rexpr{\sexpr_0}{\sexpr_0}$
\end{lemma}{
  \newcommand{\shortpf}{By induction on $\sexpr_0$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\sexpr_0 \eeq \svar_0$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\svar_0}{\svar_0}$
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\sexpr_0 \eeq \sint_0$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\sint_0}{\sint_0}$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\sexpr_0 \eeq \efun{\svar_1}{\sexpr_1}$}}
    \begin{pfproof}
      \step{2.0}{$\rexpr{\sexpr_1}{\sexpr_1}$}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\efun{\svar_1}{\sexpr_1}}{\efun{\svar_1}{\sexpr_1}}$
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\sexpr_0 \eeq \epair{\sexpr_1}{\sexpr_2}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\sexpr_0 \eeq \eapp{\stoptional}{\sexpr_1}{\sexpr_2}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\sexpr_0 \eeq \eunopt{\stoptional}{\sexpr_1}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\sexpr_0 \eeq \ebinopt{\stoptional}{\sexpr_1}{\sexpr_2}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\sexpr_0 \eeq \edynb{\sbnd_0}{\sexpr_1}$}}
    \begin{pfproof}
      \step{7.0}{$\sbnd_0 \subteq \sbnd_0$}
        \begin{pfproof}
          by reflexivity $\subteq$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\sexpr_0 \eeq \estab{\sbnd_0}{\sexpr_1}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}[simulation]\label{HA-simulation}\leavevmode
  \begin{itemize}
    \item if\/ $\rexpr{\sexpr_0}{\sexpr_2}$
          and\/ $\sexpr_0 \credN \sexpr_1$
          then\/ $\exists\,\sexpr_3,\sexpr_4$
          such that\/ $\sexpr_1 \rredN \sexpr_3$
          and\/ $\sexpr_2 \rredA \sexpr_4$
          and\/ $\rexpr{\sexpr_3}{\sexpr_4}$
    \item if\/ $\rexpr{\sexpr_0}{\sexpr_2}$
          and\/ $\sexpr_2 \credA \sexpr_3$
          then\/ $\exists\,\sexpr_1,\sexpr_4$
          such that\/ $\sexpr_3 \rredA \sexpr_4$
          and\/ $\sexpr_0 \rredN \sexpr_1$
          and\/ $\rexpr{\sexpr_1}{\sexpr_4}$
  \end{itemize}
\end{lemma}
\begin{lamportproof}
  By \lemmaref{HA-simulation-H} and \lemmaref{HA-simulation-A}.
\end{lamportproof}

\newcommand{\reducedsurfaceexpressions}{reduced WF expressions}
\begin{definition}[\reducedsurfaceexpressions]
  Expressions\/ $\sexpr_1$
  and\/ $\sexpr_2$ are \emph{\reducedsurfaceexpressions}
  if\/ $\fwellformed{\sexpr_0}{\stoptional}$
  and\/ $\sexpr_0 \rredN \sexpr_1$
  and\/ $\sexpr_0 \rredA \sexpr_2$
\end{definition}

\begin{lemma}[H-step simulation]\label{HA-simulation-H}\leavevmode
  If\/ $\sexpr_0$ and $\sexpr_2$ are \reducedsurfaceexpressions{}
  and\/ $\rexpr{\sexpr_0}{\sexpr_2}$
  and\/ $\sexpr_0 \credN \sexpr_1$
  then\/ $\exists\,\sexpr_3,\sexpr_4$
  such that\/ $\sexpr_1 \rredN \sexpr_3$
  and\/ $\sexpr_2 \rredA \sexpr_4$
  and\/ $\rexpr{\sexpr_3}{\sexpr_4}$
\end{lemma}{
  \newcommand{\shortproof}{By case analysis of $\sexpr_0 \credN \sexpr_1$}
\begin{lamportproof*}
  \shortproof
\mainproof
  \shortproof

  \step{0}{\case{$\sexpr_0 \eeq \ctx_0[\boundaryerror{\sbnd_0}{\svalue_0}]$ and $\sexpr_0 \credN \boundaryerror{\sbnd_0}{\svalue_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          trivial, $\rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\sexpr_2}$
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\sexpr_0 \eeq \ctx_0[\eerr_0]$ and $\eerr_0 \not\in \boundaryerror{\sblist}{\svalue}$ and $\sexpr_0 \credN \eerr_0$}}
    \begin{pfproof}
      \step{1.0}{$\sexpr_2 \eeq \ctx_2[\eerr_1]$ and $\rctx{\ctx_0}{\ctx_2}$ and $\rexpr{\eerr_0}{\eerr_1}$}
        \begin{pfproof}
          by \lemmaref{H-context-matching}
        \end{pfproof}
      \step{1.1}{$\sexpr_2 \credA \eerr_1$}
        \begin{pfproof}
          by definition $\credA$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\eerr_0}{\eerr_1}$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{\(
    \sexpr_0 \eeq \ctx_0[\edynb{\sbnd_0}{\svalue_0}]
  \) and \(
    \edynb{\sbnd_0}{\svalue_0} \nredNS \sexpr_3
  \)}}
    \begin{pfproof}
      \step{2.0}{$\sexpr_2 \eeq \ctx_2[\edynb{\sbnd_2}{\svalue_2}]$ and $\rctx{\ctx_0}{\ctx_2}$ and $\rexpr{\edynb{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_2}{\svalue_2}}$}
        \begin{pfproof}
          by \lemmaref{H-context-matching}
        \end{pfproof}
      \step{2.1}{${\edynb{\sbnd_0}{\svalue_0}} \rredN \sexpr_3$ and $\edynb{\sbnd_2}{\svalue_2} \rredA \sexpr_4$ and $\rexpr{\sexpr_3}{\sexpr_4}$}
        \begin{pfproof}
          by \lemmaref{H-dyn-A-dyn}
        \end{pfproof}
      \qedstep
        by \lemmaref{HA-hole-subst}
    \end{pfproof}

  \step{3}{\case{\(
    \sexpr_0 \eeq \ctx_0[\estab{\sbnd_0}{\svalue_0}]
  \) and \(
    \estab{\sbnd_0}{\svalue_0} \nredND \sexpr_3
  \)}}
    \begin{pfproof}
      \step{2.0}{$\sexpr_2 \eeq \ctx_2[\estab{\sbnd_2}{\svalue_2}]$ and $\rctx{\ctx_0}{\ctx_2}$ and $\rexpr{\estab{\sbnd_0}{\svalue_0}}{\estab{\sbnd_2}{\svalue_2}}$}
        \begin{pfproof}
          by \lemmaref{H-context-matching}
        \end{pfproof}
      \step{2.1}{${\estab{\sbnd_0}{\svalue_0}} \rredN \sexpr_3$ and $\estab{\sbnd_2}{\svalue_2} \rredA \sexpr_4$ and $\rexpr{\sexpr_3}{\sexpr_4}$}
        \begin{pfproof}
          by \lemmaref{H-sta-A-sta}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-hole-subst}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\sexpr_0 \eeq \ctx_0[\eunopt{\stoptional}{\svalue_0}]$ and $\eunopt{\stoptional}{\svalue_0} \nredNS \sdeltaH(\sunop, \svalue_0)$}}
    \begin{pfproof}
      \step{4.0}{$\sexpr_2 \eeq \ctx_2[\eunopt{\stoptional}{\svalue_2}]$ and $\rctx{\ctx_0}{\ctx_2}$ and $\rexpr{\eunopt{\stoptional}{\svalue_0}}{\eunopt{\stoptional}{\svalue_2}}$}
        \begin{pfproof}
          by \lemmaref{H-context-matching}
        \end{pfproof}
      \step{4.1}{$\snil \sWTN \eunopt{\stoptional}{\svalue_0} : \stype_0$ and $\snil \sWTA \eunopt{\stoptional}{\svalue_2} : \stype_0$}
        \begin{pfproof}
          by type soundness
        \end{pfproof}
      \step{4.2}{$\eunopt{\stoptional}{\svalue_2} \rredA \svalue_3$ and $\rexpr{\sdeltaH(\sunop, \svalue_0)}{\svalue_3}$}
        \begin{pfproof}
          by \lemmaref{HA-S-unop}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-hole-subst}
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\sexpr_0 \eeq \ctx_0[\eunopt{\stoptional}{\svalue_0}]$ and $\eunopt{\stoptional}{\svalue_0} \nredND \sexpr_1$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-D-unop}
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{\(
    \sexpr_0 \eeq \ctx_0[\eapp{\stype_0}{(\emon{\obnd{\sowner_0}{(\tfun{\stype_1}{\stype_2})}{\sowner_1}}{\svalue_0})}{\svalue_1}]
    \) \\ and \(
    \eapp{\stype_0}{(\emon{\obnd{\sowner_0}{(\tfun{\stype_1}{\stype_2})}{\sowner_1}}{\svalue_0})}{\svalue_1}
    \nredNS
    \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\eapp{\tdyn}{\svalue_0}{(\estab{\obnd{\sowner_1}{\stype_1}{\sowner_0}}{\svalue_1})})}
  \)}}
    \begin{pfproof}
      \step{7.0}{$\sexpr_2 \eeq \ctx_2[\eapp{\stype_0}{\svalue_3}{\svalue_4}]$}
        \begin{pfproof}
          by \lemmaref{H-context-matching}
        \end{pfproof}
      \step{7.1}{\scase{$\svalue_3 \eeq \emon{\obnd{\sowner_0}{(\tfun{\stype_3}{\stype_4})}{\sowner_1}}{\svalue_5}$}}
        \begin{pfproof}
          \step{7.1.0}{\(
            \eapp{\stype_0}{(\emon{\obnd{\sowner_0}{(\tfun{\stype_3}{\stype_4})}{\sowner_1}}{\svalue_5})}{\svalue_4}
            \nredAS
            \edynb{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\eapp{\tdyn}{\svalue_5}{(\estab{\obnd{\sowner_1}{\stype_3}{\sowner_0}}{\svalue_4})})}
          \)}
            \begin{pfproof}
              by definition $\nredAS$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              by \lemmaref{HA-hole-subst}
            \end{pfproof}
        \end{pfproof}
      \step{7.2}{\scase{$\svalue_3 \eeq \ehist{\sblist_0}{\svalue_5}$}}
        \begin{pfproof}
          \absurdstep
            \begin{pfproof}
              $\snil \sWTA \eapp{\stype_0}{\svalue_3}{\svalue_4} : \stype_0$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{\(
    \sexpr_0 \eeq \ctx_0[\eapp{\tdyn}{(\emon{\obnd{\sowner_0}{(\tfun{\stype_0}{\stype_1})}{\sowner_1}}{\svalue_0})}{\svalue_1}]
  \) \\ and \(
    \eapp{\tdyn}{(\emon{\obnd{\sowner_0}{(\tfun{\stype_0}{\stype_1})}{\sowner_1}}{\svalue_0})}{\svalue_1}
    \nredND
    \estab{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\eapp{\stype_1}{\svalue_0}{(\estab{\obnd{\sowner_1}{\stype_0}{\sowner_0}}{\svalue_1})})}
  \)}}
    \begin{pfproof}
      \step{8.0}{$\sexpr_2 \eeq \ctx_2[\eapp{\tdyn}{\svalue_3}{\svalue_4}]$}
        \begin{pfproof}
          by \lemmaref{H-context-matching}
        \end{pfproof}
      \step{8.1}{\scase{$\svalue_3 \eeq \emon{\obnd{\sowner_0}{(\tfun{\stype_3}{\stype_4})}{\sowner_1}}{\svalue_3}$ and $\rexpr{\svalue_0}{\svalue_3}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              by definition $\nredAD$ and $\srexpr$
            \end{pfproof}
        \end{pfproof}
      \step{8.2}{\scase{$\svalue_3 \eeq \ehist{\sblist_2}{\svalue_5}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              by \lemmaref{H-app-A-bnd}
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{\(
    \sexpr_0 \eeq \ctx_0[\eapp{\stype_0}{(\efun{\tann{\svar_0}{\stype_1}}{\sexpr_0})}{\svalue_1}]
  \) and \(
    \sexpr_0 \nredNS \ctx_0[\esubst{\sexpr_0}{\svar_0}{\svalue_1}]
  \)}}
    \begin{pfproof}
      \step{9.0}{$\sexpr_2 \eeq \ctx_2[\eapp{\stype_0}{\svalue_2}{\svalue_3}]$}
        \begin{pfproof}
          by \lemmaref{H-context-matching}
        \end{pfproof}
      \step{9.1}{$\svalue_2 \eeq \efun{\tann{\svar_0}{\stype_1}}{\sexpr_4}$ and $\rexpr{\sexpr_0}{\sexpr_4}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-subst}
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{\(
    \sexpr_0 \eeq \ctx_0[\eapp{\tdyn}{(\efun{\svar_0}{\sexpr_0})}{\svalue_1}]
  \) and \(
    \sexpr_0 \nredND \ctx_0[\esubst{\sexpr_0}{\svar_0}{\svalue_1}]
  \)}}
    \begin{pfproof}
      \step{10.0}{$\sexpr_2 \eeq \ctx_2[\eapp{\stype_0}{\svalue_2}{\svalue_3}]$}
        \begin{pfproof}
          by \lemmaref{H-context-matching}
        \end{pfproof}
      \step{10.1}{$\svalue_2 \eeq \efun{\svar_0}{\sexpr_4}$ and $\rexpr{\sexpr_0}{\sexpr_4}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-subst}
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{$\sexpr_0 \eeq \ctx_0[\ebinopt{\stoptional}{\svalue_0}{\svalue_1}]$ and $\sexpr_0 \credN \ctx_0[\sexpr_1]$}}
    \begin{pfproof}
      \step{11.0}{$\sexpr_2 \eeq \ctx_2[\ebinopt{\stoptional}{\svalue_2}{\svalue_3}]$}
        \begin{pfproof}
          by \lemmaref{H-context-matching}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-binop}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}[A-step simulation]\label{HA-simulation-A}\leavevmode
  If\/ $\sexpr_0$ and $\sexpr_2$ are \reducedsurfaceexpressions{}
  and\/ $\rexpr{\sexpr_0}{\sexpr_2}$
  and\/ $\sexpr_2 \credA \sexpr_3$
  then\/ $\exists\,\sexpr_1,\sexpr_4$
  such that\/ $\sexpr_3 \rredA \sexpr_4$
  and\/ $\sexpr_0 \rredN \sexpr_1$
  and\/ $\rexpr{\sexpr_1}{\sexpr_4}$
\end{lemma}{
  \newcommand{\shortproof}{By case analysis of $\sexpr_2 \credA \sexpr_3$}
\begin{lamportproof*}
  \shortproof
\mainproof
  \shortproof

  \step{1}{\case{$\sexpr_0$ contains a boundary error; $\sexpr_0 \eeq \ctx_0[\boundaryerror{\sbnd_0}{\svalue_0}]$}}
    \begin{pfproof}
      \step{1.0}{$\sexpr_0 \credN \boundaryerror{\sbnd_0}{\svalue_0}$}
        \begin{pfproof}
          by definition $\credN$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\sexpr_3}$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{
      $\sexpr_2 \eeq \ctx_2[\eerr_2]$
      and $\sexpr_2 \credA \eerr_2$}}
    \begin{pfproof}
      \step{2.0}{$\sexpr_0 \eeq \ctx_0[\eerr_0]$ and $\rctx{\ctx_0}{\ctx_2}$ and $\rexpr{\eerr_0}{\eerr_2}$}
        \begin{pfproof}
          by \lemmaref{A-context-matching}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\sexpr_0 \credN \rexpr{\eerr_0}{\eerr_2}$
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\sexpr_2 \eeq \ctx_2[\edynb{\sbnd_2}{\svalue_2}]$
      and $\edynb{\sbnd_2}{\svalue_2} \nredAS \sexpr_3$}}
    \begin{pfproof}
      \step{3.0}{$\sexpr_0 \eeq \ctx_0[\edynb{\sbnd_0}{\svalue_0}]$ and $\rexpr{\edynb{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_2}{\svalue_2}}$}
        \begin{pfproof}
          by \lemmaref{A-context-matching}
        \end{pfproof}
      \step{3.1}{${\edynb{\sbnd_0}{\svalue_0}} \rredN \sexpr_1$ and $\edynb{\sbnd_2}{\svalue_2} \rredA \sexpr_4$ and $\rexpr{\sexpr_1}{\sexpr_4}$}
        \begin{pfproof}
          by \lemmaref{H-dyn-A-dyn}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-hole-subst}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\sexpr_2 \eeq \ctx_2[\estab{\sbnd_2}{\svalue_2}]$
      and $\estab{\sbnd_2}{\svalue_2} \nredAD \sexpr_3$}}
    \begin{pfproof}
      \step{4.0}{$\sexpr_0 \eeq \ctx_0[\estab{\sbnd_0}{\svalue_0}]$
          and $\rexpr{\estab{\sbnd_0}{\svalue_0}}{\estab{\sbnd_2}{\svalue_2}}$}
        \begin{pfproof}
          by \lemmaref{A-context-matching}
        \end{pfproof}
      \step{4.1}{$\estab{\sbnd_0}{\svalue_0} \rredN \sexpr_1$ and $\estab{\sbnd_2}{\svalue_2} \rredA \sexpr_4$ and $\rexpr{\sexpr_1}{\sexpr_4}$}
        \begin{pfproof}
          by \lemmaref{H-sta-A-sta}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-hole-subst}
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\sexpr_2 \eeq \ctx_2[\eunopt{\stoptional}{\svalue_2}]$ and $\eunopt{\stoptional}{\svalue_2} \nredAS \sexpr_3$}}
    \begin{pfproof}
      \step{5.0}{$\sexpr_0 \eeq \ctx_0[\eunopt{\stoptional}{\svalue_0}]$ and $\rexpr{\ctx_0}{\ctx_2}$ and $\rexpr{\svalue_0}{\svalue_2}$}
        \begin{pfproof}
          by \lemmaref{A-context-matching}
        \end{pfproof}
      \step{5.1}{$\snil \sWTN \eunopt{\stoptional}{\svalue_0} : \stype_0$ and $\snil \sWTA \eunopt{\stoptional}{\svalue_2} : \stype_0$}
        \begin{pfproof}
          by type soundness
        \end{pfproof}
      \step{5.2}{$\eunopt{\stoptional}{\svalue_2} \rredA \svalue_4$ and $\rexpr{\sdeltaH(\sunop, \svalue_0)}{\svalue_4}$}
        \begin{pfproof}
          by \lemmaref{HA-S-unop}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-hole-subst}
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\sexpr_2 \eeq \ctx_2[\eunopt{\stoptional}{\svalue_2}]$ and $\eunopt{\stoptional}{\svalue_2} \nredAD \sexpr_3$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-D-unop}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{\(
    \sexpr_2 \eeq \ctx_2[\eapp{\stype_2}{(\emon{\obnd{\sowner_0}{(\tfun{\stype_3}{\stype_4})}{\sowner_1}}{\svalue_2})}{\svalue_3}]
    \) \\ and \(
    \sexpr_2 \credA \ctx_2[\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\eapp{\tdyn}{\svalue_2}{(\estab{\obnd{\sowner_1}{\stype_3}{\sowner_0}}{\svalue_3})})}]
  \)}}
    \begin{pfproof}
      \step{8.0}{$\stype_4 \subteq \stype_2$}
        \begin{pfproof}
          by inversion $\sWTA$
        \end{pfproof}
      \step{8.1}{$\sexpr_0 \eeq \ctx_0[\eapp{\stype_2}{\svalue_0}{\svalue_1}]$}
        \begin{pfproof}
          by \lemmaref{A-context-matching}
        \end{pfproof}
      \step{8.2}{$\svalue_0 \eeq \emon{\obnd{\sowner_0}{(\tfun{\stype_0}{\stype_1})}{\sowner_1}}{\svalue_4}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \(\eapp{\stype_2}{\svalue_0}{\svalue_1} \nredNS \edynb{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\eapp{\tdyn}{\svalue_4}{(\estab{\obnd{\sowner_1}{\stype_3}{\sowner_0}}{\svalue_1})})}\)
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{\(
    \sexpr_2 \eeq \ctx_2[\eapp{\tdyn}{(\ehist{\fconcat{\sbnd_0}{\sblist_1}}{\svalue_2})}{\svalue_3}]
  \)}}
    \begin{pfproof}
      \step{9.0}{$\sexpr_0 \eeq \ctx_0[\eapp{\tdyn}{\svalue_0}{\svalue_1}]$}
        \begin{pfproof}
          by \lemmaref{A-context-matching}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{H-app-A-bnd}
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{\(\sexpr_2 \eeq \ctx_2[\eapp{\stype_0}{(\efun{\tann{\svar_1}{\stype_1}}{\sexpr_2})}{\svalue_3}]\)}}
    \begin{pfproof}
      \step{10.0}{$\sexpr_0 \eeq \ctx_0[\eapp{\stype_0}{\svalue_0}{\svalue_1}]$}
        \begin{pfproof}
          by \lemmaref{A-context-matching}
        \end{pfproof}
      \step{10.1}{$\svalue_0 \eeq \efun{\svar_0}{\sexpr_1}$ and $\rexpr{\sexpr_1}{\sexpr_2}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-subst}
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{\(\sexpr_2 \eeq \ctx_2[\ebinopt{\stoptional}{\svalue_2}{\svalue_3}] \mbox{ and } \sexpr_2 \credA \ctx_2[\sexpr_4]\)}}
    \begin{pfproof}
      \step{12.0}{$\sexpr_0 \eeq \ctx_0[\ebinopt{\stoptional}{\svalue_0}{\svalue_1}]$}
        \begin{pfproof}
          by \lemmaref{A-context-matching}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-binop}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}[H context-matching]\label{H-context-matching}\leavevmode
  If\/ $\rexpr{\ctx_0[\sexpr_0]}{\sexpr_1}$
  and\/ $\sexpr_0 \not\in \svalue$
  then\/ $\exists\,\ctx_2,\sexpr_2$
  such that\/ $\sexpr_1 \eeq \ctx_2[\sexpr_2]$
  and\/ $\rctx{\ctx_0}{\ctx_2}$
  and\/ $\rexpr{\sexpr_0}{\sexpr_2}$
\end{lemma}{
  \newcommand{\shortpf}{By induction on the structure of $\ctx_0$}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\ctx_0 \eeq \ctxhole$}}
    \begin{pfproof}
      trivial, $\ctx_2 \sassign \ctxhole$ and $\sexpr_2 \sassign \sexpr_1$
    \end{pfproof}

  \step{1}{\case{$\ctx_0 \eeq \epair{\ctx_3}{\sexpr_4}$}}
    \begin{pfproof}
      \step{1.0}{$\ctx[\sexpr_0] \eeq \rexpr{\epair{\ctx_3[\sexpr_0]}{\sexpr_4}}{\sexpr_1}$}
        \begin{pfproof}
          by assumption
        \end{pfproof}
      \step{1.1}{$\sexpr_1 \eeq \epair{\sexpr_5}{\sexpr_6}$ and $\rexpr{\ctx_3[\sexpr_0]}{\sexpr_5}$ and $\rexpr{\sexpr_4}{\sexpr_6}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{1.2}{$\sexpr_4 \eeq \ctx_7[\sexpr_8]$ and $\rctx{\ctx_3}{\ctx_7}$ and $\rexpr{\sexpr_0}{\sexpr_8}$}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\ctx_1 \sassign \epair{\ctx_7}{\sexpr_6}$ and $\sexpr_2 \sassign \sexpr_8$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\ctx_0 \eeq \epair{\svalue_3}{\ctx_4}$}}
    \begin{pfproof}
      \step{2.0}{$\sexpr_1 \eeq \epair{\sexpr_5}{\sexpr_6}$ and $\rexpr{\svalue_3}{\sexpr_5}$ and $\rexpr{\ctx_4[\sexpr_0]}{\sexpr_6}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\ctx_0 \eeq \eapp{\toptional_0}{\ctx_3}{\sexpr_4}$}}
    \begin{pfproof}
      \step{4.0}{$\sexpr_1 \eeq \eapp{\toptional_0}{\sexpr_5}{\sexpr_6}$ and $\rexpr{\ctx_3[\sexpr_0]}{\sexpr_5}$ and $\rexpr{\sexpr_4}{\sexpr_6}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\ctx_0 \eeq \eapp{\toptional_0}{\svalue_3}{\ctx_4}$}}
    \begin{pfproof}
      \step{4.0}{$\sexpr_1 \eeq \eapp{\toptional_0}{\sexpr_5}{\sexpr_6}$ and $\rexpr{\svalue_3}{\sexpr_5}$ and $\rexpr{\ctx_4[\sexpr_0]}{\sexpr_6}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\ctx_0 \eeq \eunopt{\stoptional}{\ctx_3}$}}
    \begin{pfproof}
      \step{5.0}{$\sexpr_1 \eeq \eunopt{\stoptional}{\sexpr_4}$ and $\rexpr{\ctx_3[\sexpr_0]}{\sexpr_4}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\ctx_0 \eeq \ebinopt{\stoptional}{\ctx_3}{\sexpr_4}$}}
    \begin{pfproof}
      \step{6.0}{$\sexpr_1 \eeq \ebinopt{\stoptional}{\sexpr_5}{\sexpr_6}$ and $\rexpr{\ctx_3[\sexpr_0]}{\sexpr_5}$ and $\rexpr{\sexpr_4}{\sexpr_6}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\ctx_0 \eeq \ebinopt{\stoptional}{\svalue_3}{\ctx_4}$}}
    \begin{pfproof}
      \step{7.0}{$\sexpr_1 \eeq \ebinopt{\stoptional}{\svalue_5}{\sexpr_6}$ and $\rexpr{\svalue_3}{\svalue_5}$ and $\rexpr{\ctx_4[\sexpr_0]}{\sexpr_6}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\ctx_0 \eeq \edynb{\sbnd_0}{\ctx_3}$}}
    \begin{pfproof}
      \step{8.1}{$\sexpr_1 \eeq \edynb{\sbnd_1}{\sexpr_4}$ and $\rexpr{\ctx_3[\sexpr_0]}{\sexpr_4}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{$\ctx_0 \eeq \estab{\sbnd_0}{\ctx_3}$}}
    \begin{pfproof}
      \step{8.1}{$\sexpr_1 \eeq \estab{\sbnd_1}{\sexpr_4}$ and $\rexpr{\ctx_3[\sexpr_0]}{\sexpr_4}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}[A context-matching]\label{A-context-matching}\leavevmode
  If\/ $\rexpr{\sexpr_0}{\ctx_2[\sexpr_2]}$
  and\/ $\sexpr_2 \not\in \svalue$
  and\/ $\sexpr_0$ does not contain a subterm\/ $\boundaryerror{\sbnd}{\svalue}$
  then\/ $\exists\,\ctx_1,\sexpr_1$
  such that\/ $\sexpr_0 \eeq \ctx_1[\sexpr_1]$
  and\/ $\rctx{\ctx_1}{\ctx_2}$
  and\/ $\rexpr{\sexpr_1}{\sexpr_2}$
\end{lemma}{
  \newcommand{\shortpf}{By induction on the structure of $\ctx_2$}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\ctx_2 \eeq \ctxhole$}}
    \begin{pfproof}
      trivial, $\ctx_1 \sassign \ctxhole$ and $\sexpr_1 \sassign \sexpr_0$
    \end{pfproof}

  \step{1}{\case{$\ctx_2 \eeq \epair{\ctx_3}{\sexpr_3}$}}
    \begin{pfproof}
      \step{1.0}{$\sexpr_0 \eeq \rexpr{\epair{\sexpr_4}{\sexpr_5}}{\epair{\ctx_3[\sexpr_2]}{\sexpr_3}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\ctx_2 \eeq \epair{\svalue_3}{\ctx_3}$}}
    \begin{pfproof}
      \step{2.0}{$\sexpr_0 \eeq \rexpr{\epair{\sexpr_4}{\sexpr_5}}{\epair{\svalue_3}{\ctx_3[\sexpr_2]}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\ctx_2 \eeq \eapp{\toptional_0}{\ctx_3}{\sexpr_3}$}}
    \begin{pfproof}
      \step{3.0}{$\sexpr_0 \eeq \rexpr{\eapp{\toptional_0}{\sexpr_4}{\sexpr_5}}{\eapp{\toptional_0}{\ctx_3[\sexpr_2]}{\sexpr_3}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\ctx_2 \eeq \eapp{\toptional_0}{\svalue_3}{\ctx_3}$}}
    \begin{pfproof}
      \step{4.0}{$\sexpr_0 \eeq \rexpr{\eapp{\toptional_0}{\sexpr_4}{\sexpr_5}}{\eapp{\toptional_0}{\svalue_3}{\ctx_3[\sexpr_2]}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\ctx_2 \eeq \eunopt{\stoptional}{\ctx_3}$}}
    \begin{pfproof}
      \step{5.0}{$\sexpr_0 \eeq \rexpr{\eunopt{\stoptional}{\sexpr_4}}{\eunopt{\stoptional}{\ctx_3[\sexpr_2]}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\ctx_2 \eeq \ebinopt{\stoptional}{\ctx_3}{\sexpr_3}$}}
    \begin{pfproof}
      \step{6.0}{$\sexpr_0 \eeq \rexpr{\ebinopt{\stoptional}{\sexpr_4}{\sexpr_5}}{\ebinopt{\stoptional}{\ctx_3[\sexpr_2]}{\sexpr_3}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\ctx_2 \eeq \ebinopt{\stoptional}{\svalue_3}{\ctx_3}$}}
    \begin{pfproof}
      \step{7.0}{$\sexpr_0 \eeq \rexpr{\ebinopt{\stoptional}{\sexpr_4}{\sexpr_5}}{\ebinopt{\stoptional}{\svalue_3}{\ctx_3[\sexpr_2]}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\ctx_2 \eeq \edynb{\sbnd_0}{\ctx_3}$}}
    \begin{pfproof}
      \step{8.0}{$\sexpr_0 \eeq \rexpr{\edynb{\sbnd_0}{\sexpr_4}}{\edynb{\sbnd_2}{\ctx_3[\sexpr_2]}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{$\ctx_2 \eeq \estab{\sbnd_0}{\ctx_3}$}}
    \begin{pfproof}
      \step{9.0}{$\sexpr_0 \eeq \rexpr{\estab{\sbnd_0}{\sexpr_4}}{\estab{\sbnd_1}{\ctx_3[\sexpr_2]}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{$\ctx_2 \eeq \eprehist{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\sblist_2}}}{\ctx_3}$}}
    \begin{pfproof}
      \step{10.0}{$\sexpr_0 \eeq \estab{\sbnd_3}{\edynb{\sbnd_4}{\sexpr_4}}$ and $\rexpr{\sexpr_4}{\ctx_3[\sexpr_0]}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \pfih
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{H-dyn-A-dyn}
  If\/ ${(\edynb{\sbnd_0}{\svalue_0})}$
  and\/ $(\edynb{\sbnd_1}{\svalue_1})$ are \reducedsurfaceexpressions{}
  and\/ $\rexpr{\edynb{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
  then\/ ${\edynb{\sbnd_0}{\svalue_0}} \rredN \sexpr_2$
  and\/ ${\edynb{\sbnd_1}{\svalue_1}} \rredA \sexpr_3$
  then\/ $\rexpr{\sexpr_2}{\sexpr_3}$
\end{lemma}{
  \newcommand{\shortpf}{By case analysis of $\rexpr{\svalue_0}{\svalue_1}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\svalue_0 \eeq \rexpr{\sint_0}{\sint_0} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{0.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{0.0.0}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \svalue_0$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{0.0.1}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
            \begin{pfproof}
              by \lemmaref{HA-D-compat}
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_1}{\svalue_1} \nredAS \svalue_1$
            \end{pfproof}
        \end{pfproof}
      \step{0.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\svalue_0 \eeq \rexpr{\sint_0}{\ehist{\sblist_2}{\sint_0}} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{1.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{1.0.0}{$\edyn{\sbnd_0}{\svalue_0} \nredNS \svalue_0$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{1.0.1}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
            \begin{pfproof}
              by \lemmaref{HA-D-compat}
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              $\edyn{\sbnd_1}{\svalue_1} \nredAS \svalue_1$
            \end{pfproof}
        \end{pfproof}
      \step{1.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\svalue_0 \eeq \rexpr{\epair{\svalue_2}{\svalue_3}}{\epair{\svalue_4}{\svalue_5}} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{2.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{2.0.0}{let $\sbnd_0 \eeq \obnd{\sowner_0}{\stype_0}{\sowner_1}$ and $\sbnd_1 \eeq \obnd{\sowner_0}{\stype_1}{\sowner_1}$}
          \step{2.0.1}{$\rexpr{\svalue_2}{\svalue_4}$ and $\rexpr{\svalue_3}{\svalue_5}$}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \step{2.0.2}{$\stype_0 \eeq \tpair{\stype_2}{\stype_3} \subteq \tpair{\stype_4}{\stype_5} \eeq \stype_1$}
            \begin{pfproof}
              by \stepref{2.0} and inversion $\subteq$
            \end{pfproof}
          \step{2.0.3}{$\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredNS \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{2.0.4}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
            \begin{pfproof}
              by \lemmaref{HA-D-compat}
            \end{pfproof}
          \step{2.0.5}{$\edynb{\sbnd_1}{\svalue_1} \nredAS \emon{\sbnd_1}{\svalue_1}$}
            \begin{pfproof}
              by definition $\nredAS$
            \end{pfproof}
          \step{2.0.6}{\(
            {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\sexpr_6}{\emon{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\svalue_4}}
          \) \\ and \(
            {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\sexpr_7}{\emon{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\svalue_5}}
          \)}
            \begin{pfproof}
              by \lemmaref{H-dyn-A-bnd}
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              either $\sexpr_6$ or $\sexpr_7 \in \boundaryerror{\sbnd}{\svalue}$ or:
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\svalue_4}}
                  \\
                  \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\svalue_5}}
                }{
                  \rexpr{\epair{\sexpr_6}{\sexpr_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\epair{\svalue_4}{\svalue_5}}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{2.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\svalue_0 \eeq \rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}}} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{3.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{3.0.0}{
            let $\sbnd_0 \eeq \obnd{\sowner_0}{\stype_0}{\sowner_1}$
            \\ and $\sbnd_1 \eeq \obnd{\sowner_0}{\stype_1}{\sowner_1}$
          }
          \step{3.0.1}{$\rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4}}$ and $\rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5}}$}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \step{3.0.2}{$\stype_0 \eeq \tpair{\stype_2}{\stype_3} \subteq \tpair{\stype_4}{\stype_5} \eeq \stype_1$}
            \begin{pfproof}
              by \stepref{3.0} and inversion $\subteq$
            \end{pfproof}
          \step{3.0.3}{$\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredNS \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{3.0.4}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
            \begin{pfproof}
              by \lemmaref{HA-D-compat}
            \end{pfproof}
          \step{3.0.5}{$\edynb{\sbnd_1}{\svalue_1} \nredAS \emon{\sbnd_1}{\svalue_1}$}
            \begin{pfproof}
              by definition $\nredAS$
            \end{pfproof}
          \step{3.0.6}{\(
            {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})}}
          \) \\ and \(
            {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})}}
          \)}
            \begin{pfproof}
              by \lemmaref{H-dyn-A-bnd}
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              either $\sexpr_6$ or $\sexpr_7 \in \boundaryerror{\sbnd}{\svalue}$ or:
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})}}
                  \\
                  \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})}}
                }{
                  \rexpr{\epair{\sexpr_6}{\sexpr_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{3.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\svalue_0 \eeq \rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}}} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{4.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{4.0.0}{
            let $\sbnd_0 \eeq \obnd{\sowner_0}{\stype_0}{\sowner_1}$
            \\ and $\sbnd_1 \eeq \obnd{\sowner_0}{\stype_1}{\sowner_1}$
          }
          \step{4.0.1}{$\rexpr{\svalue_2}{\faddtrace{\sblist_2}{\svalue_4}}$ and $\rexpr{\svalue_3}{\faddtrace{\sblist_2}{\svalue_5}}$}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \step{4.0.2}{$\stype_0 \eeq \tpair{\stype_2}{\stype_3} \subteq \tpair{\stype_4}{\stype_5} \eeq \stype_1$}
            \begin{pfproof}
              by \stepref{4.0} and inversion $\subteq$
            \end{pfproof}
          \step{4.0.3}{$\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredNS \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{4.0.4}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
            \begin{pfproof}
              by \lemmaref{HA-D-compat}
            \end{pfproof}
          \step{4.0.5}{$\edynb{\sbnd_1}{\svalue_1} \nredAS \emon{\sbnd_1}{\svalue_1}$}
            \begin{pfproof}
              by definition $\nredAS$
            \end{pfproof}
          \step{4.0.6}{\(
            {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_4})}}
          \) \\ and \(
            {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_5})}}
          \)}
            \begin{pfproof}
              by \lemmaref{H-dyn-A-bnd}
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              either $\sexpr_6$ or $\sexpr_7 \in \boundaryerror{\sbnd}{\svalue}$ or:
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_4})}}
                  \\
                  \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_5})}}
                }{
                  \rexpr{\epair{\sexpr_6}{\sexpr_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{4.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\svalue_0 \eeq \rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_2}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}})}} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{5.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{5.0.0}{
            let $\sbnd_0 \eeq \obnd{\sowner_0}{\stype_0}{\sowner_1}$
            \\ and $\sbnd_1 \eeq \obnd{\sowner_0}{\stype_1}{\sowner_1}$
          }
          \step{5.0.1}{\(
            \rexpr{\svalue_2}{\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})}}
          \) and \(
            \rexpr{\svalue_3}{\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})}}
          \)}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \step{5.0.2}{$\stype_0 \eeq \tpair{\stype_2}{\stype_3} \subteq \tpair{\stype_4}{\stype_5} \eeq \stype_1$}
            \begin{pfproof}
              by \stepref{5.0} and inversion $\subteq$
            \end{pfproof}
          \step{5.0.3}{$\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredNS \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{5.0.4}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
            \begin{pfproof}
              by \lemmaref{HA-D-compat}
            \end{pfproof}
          \step{5.0.5}{$\edynb{\sbnd_1}{\svalue_1} \nredAS \emon{\sbnd_1}{\svalue_1}$}
            \begin{pfproof}
              by definition $\nredAS$
            \end{pfproof}
          \step{5.0.6}{\(
            {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})})}}
          \) \\ and \(
            {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})})}}
          \)}
            \begin{pfproof}
              by \lemmaref{H-dyn-A-bnd}
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              either $\sexpr_6$ or $\sexpr_7 \in \boundaryerror{\sbnd}{\svalue}$ or:
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})})}}
                  \\
                  \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})})}}
                }{
                  \rexpr{\epair{\sexpr_6}{\sexpr_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\ehist{\sblist_2}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}})})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{5.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\svalue_0 \eeq \rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_2}{(\ehist{\sblist_3}{\epair{\svalue_4}{\svalue_5}})}} \eeq \svalue_1$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\svalue_0 \eeq \rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})}} \eeq \svalue_1$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\svalue_0 \eeq \rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_2}{(\ehist{\sblist_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})}} \eeq \svalue_1$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{$\svalue_0 \eeq \rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})}} \eeq \svalue_1$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{$\svalue_0 \eeq \rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\epair{\svalue_4}{\svalue_5}})})})}} \eeq \svalue_1$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{$\svalue_0 \eeq \rexpr{\efun{\svar_2}{\sexpr_2}}{\efun{\svar_2}{\sexpr_3}} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{11.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \emon{\sbnd_0}{\svalue_0}$
              and
              $\edynb{\sbnd_1}{\svalue_1} \nredAS \emon{\sbnd_1}{\svalue_1}$
            \end{pfproof}
        \end{pfproof}
      \step{11.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{12}{\case{$\svalue_0 \eeq \rexpr{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2}}{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3}} \eeq \svalue_1$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \svalue_0 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{13}{\case{$\svalue_0 \eeq \rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{\ehist{\fconcat{\sbnd_4}{\sbnd_5}}{(\efun{\svar_0}{\sexpr_3})}} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{13.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{13.0.0}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \emon{\sbnd_0}{\svalue_0}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{13.0.1}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
            \begin{pfproof}
              by \lemmaref{HA-D-compat}
            \end{pfproof}
          \step{13.0.2}{$\edynb{\sbnd_1}{\svalue_1} \nredAS \emon{\sbnd_1}{\svalue_1}$}
            \begin{pfproof}
              by definition $\nredAS$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{\ehist{\fconcat{\sbnd_4}{\sbnd_5}}{(\efun{\svar_0}{\sexpr_3})}}
                }{
                  \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})})}}{\emon{\sbnd_1}{(\ehist{\fconcat{\sbnd_4}{\sbnd_5}}{(\efun{\svar_0}{\sexpr_3})})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{13.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{14}{\case{$\svalue_0 \eeq \rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{(\ehist{\fconcat{\sbnd_4}{\fconcat{\sbnd_5}{\sblist_6}}}{(\efun{\svar_3}{\sexpr_3})})} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{14.0}{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}
        \begin{pfproof}
          \step{14.0.0}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \emon{\sbnd_0}{\svalue_0}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{14.0.1}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
            \begin{pfproof}
              by \lemmaref{HA-D-compat}
            \end{pfproof}
          \step{14.0.2}{$\edynb{\sbnd_1}{\svalue_1} \nredAS \emon{\sbnd_1}{\svalue_1}$}
            \begin{pfproof}
              by definition $\nredAS$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{(\ehist{\fconcat{\sbnd_4}{\fconcat{\sbnd_5}{\sblist_6}}}{(\efun{\svar_3}{\sexpr_3})})}
                }{
                  \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})})}}{\emon{\sbnd_1}{(\ehist{\fconcat{\sbnd_4}{\fconcat{\sbnd_5}{\sblist_6}}}{(\efun{\svar_3}{\sexpr_3})})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{14.1}{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{15}{\case{$\svalue_0 \eeq \rexpr{\emon{\sbnd_2}{\svalue_2}}{\emon{\sbnd_3}{\svalue_3}} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{15.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{15.0.0}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \emon{\sbnd_0}{\svalue_0}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{15.0.1}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
            \begin{pfproof}
              by \lemmaref{HA-D-compat}
            \end{pfproof}
          \step{15.0.2}{$\edynb{\sbnd_1}{\svalue_1} \nredAS \emon{\sbnd_1}{\svalue_1}$}
            \begin{pfproof}
              by definition $\nredAS$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\emon{\sbnd_2}{\svalue_2}}{\emon{\sbnd_3}{\svalue_3}}
                }{
                  \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_2}{\svalue_2})}}{\emon{\sbnd_1}{(\emon{\sbnd_3}{\svalue_3})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{15.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{H-dyn-A-bnd}
  If\/ $\snil \sWTN \svalue_0 : \tdyn$
  and\/ $\snil \sWTA \svalue_1 : \tdyn$
  and\/ $\rexpr{\svalue_0}{\svalue_1}$
  and\/ $\sbnd_0 \subteq \sbnd_1$
  then\/ $\edynb{\sbnd_0}{\svalue_0} \rredN \sexpr_2$
  and\/ $\rexpr{\sexpr_2}{\emopt{\sbnd_1}{\svalue_1}}$.
\end{lemma}{
  \newcommand{\shortpf}{By induction on $\svalue_0$ via case analysis of $\rexpr{\svalue_0}{\svalue_1}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \step{0.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{0.0.1}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \svalue_0$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              $\emopt{\sbnd_1}{\svalue_1} \feq \svalue_1$
            \end{pfproof}
        \end{pfproof}
      \step{0.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edyn{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\emopt{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_2}{\sint_0}}$}}
    \begin{pfproof}
      \step{1.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{1.0.1}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \svalue_0$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              $\emopt{\sbnd_1}{\svalue_1} \feq \svalue_1$
            \end{pfproof}
        \end{pfproof}
      \step{1.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edyn{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\emopt{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\epair{\svalue_4}{\svalue_5}}$}}
    \begin{pfproof}
      \step{2.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{2.0.0}{let $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$ and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_4}{\stype_5}}{\sowner_1}$}
          \step{2.0.1}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{2.0.2}{$\rexpr{\svalue_2}{\svalue_4}$ and $\rexpr{\svalue_3}{\svalue_5}$}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \step{2.0.3}{\(
            {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\svalue_4}}
          \) \\ and \(
            {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\svalue_5}}
          \)}
            \begin{pfproof}
              by \pfih
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              either $\sexpr_6$ or $\sexpr_7 \in \boundaryerror{\sbnd}{\svalue}$, or:
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\svalue_4}}
                  \\
                  \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\svalue_5}}
                }{
                  \rexpr{\epair{\sexpr_6}{\sexpr_7}}{\emon{\sbnd_1}{\epair{\svalue_4}{\svalue_5}}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{2.1}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edyn{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\emopt{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{3.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{3.0.0}{let $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$ and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_4}{\stype_5}}{\sowner_1}$}
          \step{3.0.1}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{3.0.2}{$\rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4}}$ and $\rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5}}$}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \step{3.0.3}{\(
            {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})}}
          \) \\ and \(
            {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})}}
          \)}
            \begin{pfproof}
              by \pfih
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              either $\sexpr_6$ or $\sexpr_7 \in \boundaryerror{\sbnd}{\svalue}$, or:
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})}}
                  \\
                  \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})}}
                }{
                  \rexpr{\epair{\sexpr_6}{\sexpr_7}}{\emon{\sbnd_1}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{3.1}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edyn{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\emopt{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{4.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{4.0.0}{let $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$ and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_4}{\stype_5}}{\sowner_1}$}
          \step{4.0.1}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{4.0.2}{\(
            \rexpr{\svalue_2}{\faddtrace{\sblist_2}{\svalue_4}}
          \) and \(
            \rexpr{\svalue_3}{\faddtrace{\sblist_2}{\svalue_5}}
          \)}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \step{4.0.3}{\(
            {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_4})}}
          \) \\ and \(
            {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_5})}}
          \)}
            \begin{pfproof}
              by \pfih
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              either $\sexpr_6$ or $\sexpr_7 \in \boundaryerror{\sbnd}{\svalue}$, or:
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_4})}}
                  \\
                  \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_5})}}
                }{
                  \rexpr{\epair{\sexpr_6}{\sexpr_7}}{\emon{\sbnd_1}{(\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{4.1}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edyn{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\emopt{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{5.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{5.0.0}{let $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$ and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_4}{\stype_5}}{\sowner_1}$}
          \step{5.0.1}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{5.0.2}{\(
            \rexpr{\svalue_2}{\faddtrace{\sblist_2}{\svalue_4}}
          \) and \(
            \rexpr{\svalue_3}{\faddtrace{\sblist_2}{\svalue_5}}
          \)}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \step{5.0.3}{\(
            {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_4})}}
          \) \\ and \(
            {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_5})}}
          \)}
            \begin{pfproof}
              by \pfih
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              either $\sexpr_6$ or $\sexpr_7 \in \boundaryerror{\sbnd}{\svalue}$, or:
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_4})}}
                  \\
                  \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_5})}}
                }{
                  \rexpr{\epair{\sexpr_6}{\sexpr_7}}{\emon{\sbnd_1}{(\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{5.1}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edyn{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\emopt{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_2}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_1}}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{6.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{6.0.0}{let $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$ and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_4}{\stype_5}}{\sowner_1}$}
          \step{6.0.1}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \step{6.0.2}{\(
            \rexpr{\svalue_2}{\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_7}}{\svalue_4})}}
          \) and \(
            \rexpr{\svalue_3}{\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_7}}{\svalue_5})}}
          \)}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \step{6.0.3}{\(
            {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_7}}{\svalue_4})})}}
          \) \\ and \(
            {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_7}}{\svalue_5})})}}
          \)}
            \begin{pfproof}
              by \pfih
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              either $\sexpr_6$ or $\sexpr_7 \in \boundaryerror{\sbnd}{\svalue}$, or:
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\sexpr_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_7}}{\svalue_4})})}}
                  \\
                  \rexpr{\sexpr_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_7}}{\svalue_5})})}}
                }{
                  \rexpr{\epair{\sexpr_6}{\sexpr_7}}{\emon{\sbnd_1}{(\ehist{\sblist_2}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}})})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{6.1}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edyn{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\emopt{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_2}{(\ehist{\sblist_3}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{8.1}{\(
        \rexpr{\svalue_2}{\emopt{\sbnd_2}{(\emopt{\sbnd_3}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\sbnd_2}{(\emopt{\sbnd_3}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{8.2}{\(
        \edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{8.3}{\(
        {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\sbnd_2}{(\emopt{\sbnd_3}{\svalue_4})})}}
      \) \\ and \(
        {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\sbnd_2}{(\emopt{\sbnd_3}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\sbnd_2}{(\emopt{\sbnd_3}{\svalue_4})})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\sbnd_2}{(\emopt{\sbnd_3}{\svalue_5})})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emon{\sbnd_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_2}{(\ehist{\sblist_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \step{9.1}{\(
        \rexpr{\svalue_2}{\emopt{\sbnd_2}{(\ehist{\sblist_3}{(\emopt{\sbnd_4}{\svalue_4})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\sbnd_2}{(\ehist{\sblist_3}{(\emopt{\sbnd_4}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{9.2}{\(
        \edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{9.3}{\(
        {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\sbnd_2}{(\ehist{\sblist_3}{(\emopt{\sbnd_4}{\svalue_4})})})}}
      \) \\ and \(
        {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\sbnd_2}{(\ehist{\sblist_3}{(\emopt{\sbnd_4}{\svalue_5})})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\sbnd_2}{(\ehist{\sblist_3}{(\emopt{\sbnd_4}{\svalue_4})})})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\sbnd_2}{(\ehist{\sblist_3}{(\emopt{\sbnd_4}{\svalue_5})})})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emon{\sbnd_2}{(\ehist{\sblist_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \step{10.1}{\(
        \rexpr{\svalue_2}{\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_4})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{10.2}{\(
        \edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{10.3}{\(
        {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_4})})})}}
      \) \\ and \(
        {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_5})})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_4})})})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_5})})})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{({\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})}})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \step{11.1}{\(
        \rexpr{\svalue_2}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_4})})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_5})})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{11.2}{\(
        \edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{11.3}{\(
        {\edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_4})})})})}}
      \) \\ and \(
        {\edynb{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_5})})})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_4})})})})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_5})})})})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\epair{\svalue_4}{\svalue_5}})})})})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{12}{\case{$\rexpr{\efun{\svar_2}{\sexpr_2}}{\efun{\svar_2}{\sexpr_3}}$}}
    \begin{pfproof}
      \step{12.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\emon{\sbnd_0}{\svalue_0}}{\emon{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
      \step{12.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{13}{\case{$\rexpr{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2}}{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \svalue_0 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{14}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{\ehist{\fconcat{\sbnd_4}{\sbnd_5}}{(\efun{\svar_0}{\sexpr_3})}}$}}
    \begin{pfproof}
      \step{14.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{14.0.0}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \emon{\sbnd_0}{\svalue_0}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{\ehist{\fconcat{\sbnd_4}{\sbnd_5}}{(\efun{\svar_0}{\sexpr_3})}}
                }{
                  \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})})}}{\emon{\sbnd_1}{(\ehist{\fconcat{\sbnd_4}{\sbnd_5}}{(\efun{\svar_0}{\sexpr_3})})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{14.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{15}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{(\ehist{\fconcat{\sbnd_4}{\fconcat{\sbnd_5}{\sblist_6}}}{(\efun{\svar_3}{\sexpr_3})})}$}}
    \begin{pfproof}
      \step{15.0}{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}
        \begin{pfproof}
          \step{15.0.0}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \emon{\sbnd_0}{\svalue_0}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{(\ehist{\fconcat{\sbnd_4}{\fconcat{\sbnd_5}{\sblist_6}}}{(\efun{\svar_3}{\sexpr_3})})}
                }{
                  \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})})}}{\emon{\sbnd_1}{(\ehist{\fconcat{\sbnd_4}{\fconcat{\sbnd_5}{\sblist_6}}}{(\efun{\svar_3}{\sexpr_3})})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{15.1}{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{16}{\case{$\svalue_0 \eeq \rexpr{\emon{\sbnd_2}{\svalue_2}}{\emon{\sbnd_3}{\svalue_3}} \eeq \svalue_1$}}
    \begin{pfproof}
      \step{16.0}{\scase{$\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \step{16.0.0}{$\edynb{\sbnd_0}{\svalue_0} \nredNS \emon{\sbnd_0}{\svalue_0}$}
            \begin{pfproof}
              by definition $\nredNS$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              \begin{mathpar}
                \inferrule*{
                  \rexpr{\emon{\sbnd_2}{\svalue_2}}{\emon{\sbnd_3}{\svalue_3}}
                }{
                  \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_2}{\svalue_2})}}{\emon{\sbnd_1}{(\emon{\sbnd_3}{\svalue_3})}}
                }
              \end{mathpar}
            \end{pfproof}
        \end{pfproof}
      \step{16.1}{\scase{$\neg\fshallow{\tagof{\stype_0}}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\sbnd_0}{\svalue_0} \nredNS \rexpr{\boundaryerror{\sbnd_0}{\svalue_0}}{\edynb{\sbnd_1}{\svalue_1}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{H-sta-A-sta}
  If\/ ${\estab{\sbnd_0}{\svalue_0}}$
  and\/ ${\estab{\sbnd_1}{\svalue_1}}$ are \reducedsurfaceexpressions{}
  and\/ $\rexpr{\estab{\sbnd_0}{\svalue_0}}{\estab{\sbnd_1}{\svalue_1}}$
  and\/ ${\estab{\sbnd_0}{\svalue_0}} \nredND \sexpr_2$
  and\/ ${\estab{\sbnd_1}{\svalue_1}} \nredAD \sexpr_3$
  then\/ $\rexpr{\sexpr_2}{\sexpr_3}$
\end{lemma}{
  \newcommand{\shortpf}{By case analysis of $\rexpr{\svalue_0}{\svalue_1}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \step{0.0}{$\estab{\sbnd_0}{\svalue_0} \nredND \svalue_0$ and $\estab{\sbnd_1}{\svalue_1} \nredAD \svalue_1$}
        \begin{pfproof}
          by definition $\nredND$, $\nredAD$
        \end{pfproof}
      \qedstep
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_2}{\sint_0}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\epair{\svalue_4}{\svalue_5}}$}}
    \begin{pfproof}
      \step{2.0}{let
        $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$
        and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$}
      \step{2.1}{$\rexpr{\svalue_2}{\svalue_4}$ and $\rexpr{\svalue_3}{\svalue_5}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{2.2}{\(
        \estab{\sbnd_0}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \) \\ and \(
        \estab{\sbnd_1}{\svalue_1} \nredAD \emon{\sbnd_1}{\svalue_1}
      \)}
        \begin{pfproof}
          by definition $\nredND$ and $\nredAD$
        \end{pfproof}
      \step{2.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\svalue_4}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\svalue_5}}
      \)}
        \begin{pfproof}
          by \lemmaref{H-sta-A-bnd}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\svalue_4}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\svalue_5}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\sbnd_1}{\epair{\svalue_4}{\svalue_5}}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{3.0}{let
        $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$
        and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$}
      \step{3.1}{\(
        \rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{3.2}{\(
        \estab{\sbnd_0}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \) \\ and \(
        \estab{\sbnd_1}{\svalue_1} \rredA \ehist{\fconcat{\sbnd_1}{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}}{\epair{\svalue_4}{\svalue_5}}
      \)}
        \begin{pfproof}
          by definition $\nredND$ and $\nredAD$
        \end{pfproof}
      \step{3.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by \lemmaref{H-sta-A-bnd}
        \end{pfproof}
      \step{3.4}{\(
        \rexpr{\svalue_6}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\obnd{\sowner_2}{\stype_6}{\sowner_3}}}{\svalue_4}}
      \) \\ and \(
        \rexpr{\svalue_7}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\obnd{\sowner_2}{\stype_7}{\sowner_3}}}{\svalue_5}}
      \)}
        \begin{pfproof}
          by \lemmaref{HA-mon-trace}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\obnd{\sowner_2}{\stype_6}{\sowner_3}}}{\svalue_4}}
              \\
              \rexpr{\svalue_7}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\obnd{\sowner_2}{\stype_7}{\sowner_3}}}{\svalue_5}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\ehist{\fconcat{\sbnd_1}{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}}{\epair{\svalue_4}{\svalue_5}}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{(\ehist{\sblist_4}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{6.0}{let
        $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$
        and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$}
      \step{6.1}{\(
        \rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{6.2}{\(
        \estab{\sbnd_0}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \) \\ and \(
        \estab{\sbnd_1}{\svalue_1} \rredA \ehist{\fconcat{\sbnd_1}{\fconcat{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\sblist_4}}}{\epair{\svalue_4}{\svalue_5}}
      \)}
        \begin{pfproof}
          by definition $\nredND$ and $\nredAD$
        \end{pfproof}
      \step{6.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_4})})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by \lemmaref{H-sta-A-bnd}
        \end{pfproof}
      \step{6.4}{\(
        \rexpr{\svalue_6}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\obnd{\sowner_2}{\stype_6}{\sowner_3}}}{(\faddtrace{\sblist_4}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_7}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\obnd{\sowner_2}{\stype_7}{\sowner_3}}}{(\faddtrace{\sblist_4}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by \lemmaref{HA-mon-trace}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\fconcat{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\sblist_4}}}{\svalue_4}}
              \\
              \rexpr{\svalue_7}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\fconcat{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\sblist_4}}}{\svalue_5}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\ehist{\fconcat{\sbnd_1}{\fconcat{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\sblist_4}}}{\epair{\svalue_4}{\svalue_5}}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{(\emon{\obnd{\sowner_4}{\tpair{\stype_8}{\stype_9}}{\sowner_5}}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{7.0}{let
        $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$
        and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$}
      \step{7.1}{\(
        \rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_8}{\sowner_5}}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_9}{\sowner_5}}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{7.2}{\(
        \estab{\sbnd_0}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \) \\ and \(
        \estab{\sbnd_1}{\svalue_1} \rredA \ehist{\fconcat{\sbnd_1}{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}}{(\emon{\obnd{\sowner_4}{\tpair{\stype_8}{\stype_9}}{\sowner_5}}{\epair{\svalue_4}{\svalue_5}})}
      \)}
        \begin{pfproof}
          by definition $\nredND$ and $\nredAD$
        \end{pfproof}
      \step{7.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_8}{\sowner_5}}{\svalue_4})})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_9}{\sowner_5}}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by \lemmaref{H-sta-A-bnd}
        \end{pfproof}
      \step{7.4}{\(
        \rexpr{\svalue_6}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\obnd{\sowner_2}{\stype_6}{\sowner_3}}}{(\emopt{\obnd{\sowner_4}{\stype_8}{\sowner_5}}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_7}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\obnd{\sowner_2}{\stype_7}{\sowner_3}}}{(\emopt{\obnd{\sowner_4}{\stype_9}{\sowner_5}}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by \lemmaref{HA-mon-trace}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\obnd{\sowner_2}{\stype_6}{\sowner_3}}}{(\emopt{\obnd{\sowner_4}{\stype_8}{\sowner_5}}{\svalue_4})}}
              \\
              \rexpr{\svalue_7}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\obnd{\sowner_2}{\stype_7}{\sowner_3}}}{(\emopt{\obnd{\sowner_4}{\stype_9}{\sowner_5}}{\svalue_5})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\ehist{\fconcat{\sbnd_1}{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}}{(\emon{\obnd{\sowner_4}{\tpair{\stype_8}{\stype_9}}{\sowner_5}}{\epair{\svalue_4}{\svalue_5}})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{(\ehist{\sblist_4}{(\emon{\obnd{\sowner_5}{\tpair{\stype_8}{\stype_9}}{\sowner_6}}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \step{8.0}{let
        $\sbnd_0 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$
        and $\sbnd_1 \eeq \obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}$}
      \step{8.1}{\(
        \rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_8}{\sowner_6}}{\svalue_4})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_9}{\sowner_6}}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{8.2}{\(
        \estab{\sbnd_0}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \) \\ and \(
        \estab{\sbnd_1}{\svalue_1} \rredA \ehist{\fconcat{\sbnd_1}{\fconcat{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\sblist_4}}}{(\emon{\obnd{\sowner_5}{\tpair{\stype_8}{\stype_9}}{\sowner_6}}{\epair{\svalue_4}{\svalue_5}})}
      \)}
        \begin{pfproof}
          by definition $\nredND$ and $\nredAD$
        \end{pfproof}
      \step{8.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_8}{\sowner_6}}{\svalue_4})})})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_9}{\sowner_6}}{\svalue_5})})})}}
      \)}
        \begin{pfproof}
          by \lemmaref{H-sta-A-bnd}
        \end{pfproof}
      \step{8.4}{\(
        \rexpr{\svalue_6}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\obnd{\sowner_2}{\stype_6}{\sowner_3}}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_8}{\sowner_6}}{\svalue_4})})}}
      \) \\ and \(
        \rexpr{\svalue_7}{\faddtrace{\fconcat{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\obnd{\sowner_2}{\stype_7}{\sowner_3}}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_9}{\sowner_6}}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by \lemmaref{HA-mon-trace}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\faddtrace{\fconcat{\sbnd_1}{\fconcat{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\sblist_4}}}{(\emopt{\obnd{\sowner_5}{\stype_8}{\sowner_6}}{\svalue_4})}}
              \\
              \rexpr{\svalue_7}{\faddtrace{\fconcat{\sbnd_1}{\fconcat{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\sblist_4}}}{(\emopt{\obnd{\sowner_5}{\stype_9}{\sowner_6}}{\svalue_5})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\ehist{\fconcat{\sbnd_1}{\fconcat{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\sblist_4}}}{(\emon{\obnd{\sowner_5}{\tpair{\stype_8}{\stype_9}}{\sowner_6}}{\epair{\svalue_4}{\svalue_5}})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-S-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-S-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{$\rexpr{\efun{\svar_2}{\sexpr_2}}{\efun{\svar_2}{\sexpr_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \svalue_0 : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{12}{\case{$\rexpr{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2}}{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\estab{\sbnd_0}{\svalue_0} \nredND \emon{\sbnd_0}{\svalue_0}$ and $\estab{\sbnd_1}{\svalue_1} \nredND \emon{\sbnd_1}{\svalue_1}$}
        \end{pfproof}
    \end{pfproof}

  \step{13}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{\ehist{\sblist_4}{\svalue_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{14}{\case{$\rexpr{\emon{\sbnd_2}{\svalue_2}}{\emon{\sbnd_3}{\svalue_3}}$}}
    \begin{pfproof}
      \step{14.0}{$\estab{\sbnd_0}{\svalue_0} \nredND \emon{\sbnd_0}{\svalue_0}$}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{14.1}{$\estab{\sbnd_1}{\svalue_1} \nredAD \faddtrace{\fconcat{\sbnd_1}{\fconcat{\sbnd_3}{\fgettrace{\svalue_3}}}}{\fremtrace{\svalue_3}}$}
        \begin{pfproof}
          by definition $\nredAD$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \sbnd_0 \subteq \sbnd_1
              \\
              \sbnd_1 \subteq \sbnd_3
              \\
              \rexpr{\svalue_2}{\ehist{\fgettrace{\svalue_3}}{\fremtrace{\svalue_3}}}
            }{
              \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_1}{\svalue_2})}}{\ehist{\fconcat{\sbnd_1}{\fconcat{\sbnd_3}{\fgettrace{\svalue_3}}}}{\fremtrace{\svalue_3}}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{H-sta-A-bnd}
  If\/ $\svalue_0$ and\/ $\svalue_1$ are \reducedsurfaceexpressions{}
  and\/ $\rexpr{\svalue_0}{\svalue_1}$
  and\/ $\snil \sWTN \svalue_0 : \stype_0$
  and\/ $\snil \sWTA \svalue_1 : \stype_1$
  and\/ $\stype_0 \subteq \stype_1$
  then\/ $\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \rredN \svalue_2$
  and\/ $\rexpr{\svalue_2}{\emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_3}}$
\end{lemma}{
  \newcommand{\shortpf}{By induction on $\svalue_0$ via case analysis of $\rexpr{\svalue_0}{\svalue_1}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \rexpr{\svalue_0}{\emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1}}$}
        \end{pfproof}
      \qedstep
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_2}{\sint_0}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\epair{\svalue_4}{\svalue_5}}$}}
    \begin{pfproof}
      \step{2.1}{$\rexpr{\svalue_2}{\svalue_4}$ and $\rexpr{\svalue_3}{\svalue_5}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{2.2}{\(
        \estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{2.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\svalue_4}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\svalue_5}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{\svalue_4}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{\svalue_5}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\epair{\svalue_4}{\svalue_5}}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{3.1}{\(
        \rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{3.2}{\(
        \estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{3.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{\svalue_4})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{\svalue_5})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\tpair{\stype_4}{\stype_5}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{(\ehist{\sblist_4}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{6.1}{\(
        \rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{6.2}{\(
        \estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{6.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_4})})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_4})})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\faddtrace{\sblist_4}{\svalue_5})})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\tpair{\stype_4}{\stype_5}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{(\ehist{\sblist_4}{\epair{\svalue_4}{\svalue_5}})})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{(\emon{\obnd{\sowner_4}{\tpair{\stype_8}{\stype_9}}{\sowner_5}}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{7.1}{\(
        \rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_8}{\sowner_5}}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_9}{\sowner_5}}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{7.2}{\(
        \estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{7.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_8}{\sowner_5}}{\svalue_4})})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_9}{\sowner_5}}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_8}{\sowner_5}}{\svalue_4})})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\emopt{\obnd{\sowner_4}{\stype_9}{\sowner_5}}{\svalue_5})})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\tpair{\stype_4}{\stype_5}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{(\emon{\obnd{\sowner_4}{\tpair{\stype_8}{\stype_9}}{\sowner_5}}{\epair{\svalue_4}{\svalue_5}})})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{(\ehist{\sblist_4}{(\emon{\obnd{\sowner_5}{\tpair{\stype_8}{\stype_9}}{\sowner_6}}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \step{8.1}{\(
        \rexpr{\svalue_2}{\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_8}{\sowner_6}}{\svalue_4})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_9}{\sowner_6}}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{8.2}{\(
        \estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{8.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_8}{\sowner_6}}{\svalue_4})})})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_9}{\sowner_6}}{\svalue_5})})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_6}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_8}{\sowner_6}}{\svalue_4})})})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_7}{\sowner_3}}{(\ehopt{\sblist_4}{(\emopt{\obnd{\sowner_5}{\stype_9}{\sowner_6}}{\svalue_5})})})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\tpair{\stype_6}{\stype_7}}{\sowner_3}}{(\ehist{\sblist_4}{(\emon{\obnd{\sowner_5}{\tpair{\stype_8}{\stype_9}}{\sowner_6}}{\epair{\svalue_4}{\svalue_5}})})})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \step{9.1}{\(
        \rexpr{\svalue_2}{\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_4})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{9.2}{\(
        \estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{9.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_4})})})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_5})})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_4})})})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emoptplus{\sblist_2}{(\emopt{\sbnd_3}{(\emopt{\sbnd_4}{\svalue_5})})})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{({\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})}})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \step{10.1}{\(
        \rexpr{\svalue_2}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_4})})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_5})})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{10.2}{\(
        \estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \epair{\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}}{\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{10.3}{\(
        {\estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_2}} \rredN \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_4})})})})}}
      \) \\ and \(
        {\estab{\obnd{\sowner_0}{\stype_3}{\sowner_1}}{\svalue_3}} \rredN \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_5})})})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_6}{\emopt{\obnd{\sowner_0}{\stype_4}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_4})})})})}}
              \\
              \rexpr{\svalue_7}{\emopt{\obnd{\sowner_0}{\stype_5}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\svalue_5})})})})}}
            }{
              \rexpr{\epair{\svalue_6}{\svalue_7}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emonplus{\sblist_2}{(\emon{\sbnd_3}{(\ehist{\sblist_4}{(\emon{\sbnd_5}{\epair{\svalue_4}{\svalue_5}})})})})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{$\rexpr{\efun{\svar_2}{\sexpr_2}}{\efun{\svar_2}{\sexpr_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \svalue_0 : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{12}{\case{$\rexpr{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2}}{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \rexpr{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1}}$
        \end{pfproof}
    \end{pfproof}

  \step{13}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{\ehist{\sblist_4}{\svalue_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{14}{\case{$\rexpr{\emon{\sbnd_2}{\svalue_2}}{\emon{\sbnd_3}{\svalue_3}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredND \rexpr{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0}}{\emon{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1}}$
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{HA-mon-trace}
  If\/ $\snil \sWTN \svalue_0 : \tdyn$
  and\/ $\snil \sWTA \emopt{\sbnd_0}{(\emopt{\sbnd_1}{\svalue_1})} : \tdyn$
  and\/ $\rexpr{\svalue_0}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{\svalue_1})}}$
  then\/ $\rexpr{\svalue_0}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{\svalue_1}}$.
\end{lemma}{
  \newcommand{\shortpf}{By induction on $\svalue_0$ via case analysis of $\rexpr{\svalue_0}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{\svalue_1})}}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\sint_0}{\ehist{\fconcat{\sbnd_0}{\sbnd_1}}{\sint_0}}$
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_2}{\sint_0}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\sint_0}{\ehist{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\sblist_2}}}{\sint_0}}$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{2.0}{\(
        \rexpr{\svalue_2}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{2.1}{\(
        \rexpr{\svalue_2}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{\svalue_4}}
      \) \\ and \(
        \rexpr{\svalue_3}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{\svalue_5}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_2}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{\svalue_4}}
              \\
              \rexpr{\svalue_3}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{\svalue_5}}
            }{
              \rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\fconcat{\sbnd_0}{\sbnd_1}}{\epair{\svalue_4}{\svalue_5}}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{(\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \step{3.0}{\(
        \rexpr{\svalue_2}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{(\faddtrace{\sblist_2}{\svalue_4})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{(\faddtrace{\sblist_2}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{3.1}{\(
        \rexpr{\svalue_2}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\faddtrace{\sblist_2}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\faddtrace{\sblist_2}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_2}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\faddtrace{\sblist_2}{\svalue_4})}}
              \\
              \rexpr{\svalue_3}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\faddtrace{\sblist_2}{\svalue_5})}}
            }{
              \rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\sblist_2}}}{\epair{\svalue_4}{\svalue_5}}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{(\emon{\sbnd_2}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \step{4.0}{\(
        \rexpr{\svalue_2}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{(\emopt{\sbnd_2}{\svalue_4})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{(\emopt{\sbnd_2}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{4.1}{\(
        \rexpr{\svalue_2}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\emopt{\sbnd_2}{\svalue_4})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\emopt{\sbnd_2}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_2}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\emopt{\sbnd_2}{\svalue_4})}}
              \\
              \rexpr{\svalue_3}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\emopt{\sbnd_2}{\svalue_5})}}
            }{
              \rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\fconcat{\sbnd_0}{\sbnd_1}}{(\emon{\sbnd_2}{\epair{\svalue_4}{\svalue_5}})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \step{5.0}{\(
        \rexpr{\svalue_2}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{(\faddtrace{\sblist_2}{(\emopt{\sbnd_3}{\svalue_4})})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{(\faddtrace{\sblist_2}{(\emopt{\sbnd_3}{\svalue_5})})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{5.1}{\(
        \rexpr{\svalue_2}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\faddtrace{\sblist_2}{(\emopt{\sbnd_3}{\svalue_4})})}}
      \) \\ and \(
        \rexpr{\svalue_3}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{(\faddtrace{\sblist_2}{(\emopt{\sbnd_3}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_2}{\faddtrace{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\sblist_2}}}{(\emopt{\sbnd_3}{\svalue_4})}}
              \\
              \rexpr{\svalue_3}{\faddtrace{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\sblist_2}}}{(\emopt{\sbnd_3}{\svalue_5})}}
            }{
              \rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\sblist_2}}}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})}}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{\efun{\svar_3}{\sexpr_3}})}}$}}
    \begin{pfproof}
      \step{6.0}{$\rexpr{\svalue_2}{\efun{\svar_3}{\sexpr_3}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_2}{\efun{\svar_3}{\sexpr_3}}
            }{
              \rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{(\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{\efun{\svar_3}{\sexpr_3}})}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{\emon{\sbnd_0}{(\emon{\sbnd_n}{(\ehist{\sblist_6}{\efun{\svar_3}{\sexpr_3}})})}}$}}
    \begin{pfproof}
      \step{7.0}{$\rexpr{\svalue_2}{(\ehist{\sblist_6}{\efun{\svar_3}{\sexpr_3}})}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          \begin{mathpar}
            \inferrule*{
              \rexpr{\svalue_2}{\efun{\svar_3}{\sexpr_3}}
            }{
              \rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{(\faddtrace{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\sblist_6}}}{\efun{\svar_3}{\sexpr_3}})}
            }
          \end{mathpar}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_2})}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{\efun{\tann{\svar_3}{\stype_3}}{\sexpr_3}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \tdyn$
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}


\begin{lemma}\label{HA-D-compat}
  If\/ $\snil \sWTN \svalue_0 : \tdyn$
  and\/ $\snil \sWTA \svalue_1 : \tdyn$
  and\/ $\fshallow{\tagof{\stype_0}}{\svalue_0}$
  and\/ $\rexpr{\svalue_0}{\svalue_1}$
  then\/ $\fshallow{\tagof{\stype_0}}{\svalue_1}$
\end{lemma}{
  \newcommand{\shortpf}{By induction on $\svalue_1$ via case analysis of $\rexpr{\svalue_0}{\svalue_1}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \step{0.0}{$\stype_0 \in \tnat \cup \tint$}
        \begin{pfproof}
          by inversion $\sshallow$
        \end{pfproof}
      \step{0.1}{\scase{$\stype_0 \eeq \tnat$}}
        \begin{pfproof}
          \step{0.1.0}{$\sint_0 \in \naturals$}
            \begin{pfproof}
              by inversion $\sshallow$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              $\fshallow{\tagof{\tnat}}{\sint_0}$
            \end{pfproof}
        \end{pfproof}
      \step{0.2}{\scase{$\stype_0 \eeq \tint$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\fshallow{\tagof{\tint}}{\sint_0}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_0}{\sint_0}}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\epair{\svalue_4}{\svalue_5}}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_6}{\stype_7}}{\sowner_1}}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_0}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{5}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_0}{(\emon{\obnd{\sowner_1}{\tpair{\stype_6}{\stype_7}}{\sowner_2}}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{6}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_6}{\stype_7}}{\sowner_1}}{(\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{7}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_6}{\stype_6}}{\sowner_1}}{(\emon{\sbnd_2}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{8}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sowner_0}{\tpair{\stype_6}{\stype_7}}{\sowner_1}}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})})}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{9}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\emon{\sbnd_2}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{10}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \step{10.0}{$\stype_0 \in \tpair{\stype}{\stype}$}
        \begin{pfproof}
          by inversion $\sshallow$
        \end{pfproof}
      \qedstep
    \end{pfproof}

  \step{11}{\case{$\rexpr{\efun{\svar_2}{\sexpr_2}}{\efun{\svar_2}{\sexpr_3}}$}}
    \begin{pfproof}
      \step{11.0}{$\stype_0 \in \tfun{\stype}{\stype}$}
        \begin{pfproof}
          by inversion $\sshallow$
        \end{pfproof}
      \qedstep
    \end{pfproof}

  \step{12}{\case{$\rexpr{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2}}{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \svalue_0 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{13}{\case{$\rexpr{\emon{\obnd{\sowner_0}{\tfun{\stype_2}{\stype_3}}{\sowner_1}}{(\emon{\sbnd_2}{\svalue_2})}}{\ehist{\sblist_3}{\efun{\svar_3}{\sexpr_3}}}$}}
    \begin{pfproof}
      \step{13.0}{$\stype_0 \in \tfun{\stype}{\stype}$}
        \begin{pfproof}
          by inversion $\sshallow$
        \end{pfproof}
      \qedstep
    \end{pfproof}

  \step{14}{\case{$\rexpr{\emon{\obnd{\sowner_0}{\tfun{\stype_2}{\stype_3}}{\sowner_1}}{\svalue_2}}{\emon{\obnd{\sowner_0}{\tfun{\stype_4}{\stype_5}}{\sowner_1}}{\svalue_3}}$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{HA-S-compat-1}
  If\/ $\svalue_0$ and\/ ${\emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1}}$ are \reducedsurfaceexpressions{}
  and\/ $\snil \sWTN \svalue_0 : \stype_0\!\!$
  and\/ $\snil \sWTA {\emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1}} : \stype_1$
  and\/ $\stype_0 \subteq \stype_1$
  and\/ $\rexpr{\svalue_0}{\emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1}}$
  then\/ $\edynb{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1} \rredA \svalue_2$
  and\/ $\rexpr{\svalue_0}{\svalue_2}$.
\end{lemma}{
  \newcommand{\shortpf}{By case analysis of $\stype_0$ and $\srexpr$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\stype_0 \eeq \tnat$}}
    \begin{pfproof}
      \step{0.0}{$\svalue_0 \in \naturals$}
        \begin{pfproof}
          by inversion $\sWTN$
        \end{pfproof}
      \step{0.1}{\scase{$\rexpr{\svalue_0}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1} \nredAS \svalue_0 \feq \emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1}$
            \end{pfproof}
        \end{pfproof}
      \step{0.2}{\scase{$\rexpr{\svalue_0}{\ehist{\sblist_0}{\svalue_0}}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1} \nredAS {\ehist{\sblist_0}{\svalue_0}} \feq \emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{\svalue_1}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\stype_0 \eeq \tint$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{2}{\case{$\stype_0 \eeq \tpair{\stype_1}{\stype_2}$}}
    \begin{pfproof}
      \step{2.0}{$\svalue_0 \in \epair{\svalue}{\svalue}$}
        \begin{pfproof}
          by inversion $\sWTN$
        \end{pfproof}
      \step{2.2}{\scase{$\rexpr{\svalue_0}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\epair{\svalue_2}{\svalue_3}}}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1} \nredAS \emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1}$
            \end{pfproof}
        \end{pfproof}
      \step{2.4}{\scase{$\rexpr{\svalue_0}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{(\ehist{\sblist_2}{\epair{\svalue_2}{\svalue_3}})}}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1} \nredAS \emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1}$
            \end{pfproof}
        \end{pfproof}
      \step{2.5}{\scase{$\rexpr{\svalue_0}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{(\emon{\sbnd_2}{\epair{\svalue_2}{\svalue_3}})}}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1} \nredAS \emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1}$
            \end{pfproof}
        \end{pfproof}
      \step{2.6}{\scase{$\rexpr{\svalue_0}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_2}{\svalue_3}})})}}$}}
        \begin{pfproof}
          \absurdstep
            \begin{pfproof}
              $\snil \sWTA \svalue_1 : \tdyn$
            \end{pfproof}
        \end{pfproof}
      \step{2.7}{\scase{$\rexpr{\svalue_0}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\emon{\sbnd_2}{\epair{\svalue_2}{\svalue_3}})})}}$}}
        \begin{pfproof}
          \absurdstep
            \begin{pfproof}
              by \lemmaref{A-D-mon-limit}
            \end{pfproof}
        \end{pfproof}
      \step{2.8}{\scase{$\rexpr{\svalue_0}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_2}{\svalue_3}})})})}}$}}
        \begin{pfproof}
          \absurdstep
            \begin{pfproof}
              by \lemmaref{A-D-mon-limit}
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\stype_0 \eeq \tfun{\stype_1}{\stype_2}$}}
    \begin{pfproof}
      \step{3.0}{$\svalue_0 \in \efun{\svar}{\sexpr} \cup \emon{\sbnd}{\svalue}$}
        \begin{pfproof}
          by inversion $\sWTN$
        \end{pfproof}
      \step{3.1}{\scase{$\rexpr{\svalue_0}{\emon{\obnd{\sowner_0}{\tfun{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1}}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\tfun{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1} \nredAS \emon{\obnd{\sowner_0}{\tfun{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{HA-S-compat-2}
  If\/ $\svalue_0$ and\/ ${\emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_2}{\sowner_3}}{\svalue_1})}}$ are \reducedsurfaceexpressions{}
  and\/ $\snil \sWTN \svalue_0 : \stype_0$
  and\/ $\snil \sWTA {\emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_2}{\sowner_3}}{\svalue_1})}} : \stype_1$
  and\/ $\rexpr{\svalue_0}{\emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_2}{\sowner_3}}{\svalue_1})}}$
  and\/ $\stype_0 \subteq \stype_1$
  then\/ $\edynb{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\estab{\obnd{\sowner_2}{\stype_2}{\sowner_3}}{\svalue_1})} \rredA \svalue_2$
  and\/ $\rexpr{\svalue_0}{\svalue_2}$.
\end{lemma}{
  \newcommand{\shortpf}{By case analysis of $\stype_0$ and $\srexpr$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\stype_0 \eeq \tnat$}}
    \begin{pfproof}
      \step{0.0}{$\svalue_0 \in \naturals$}
        \begin{pfproof}
          by inversion $\sWTN$
        \end{pfproof}
      \step{0.1}{\scase{$\rexpr{\svalue_0}{\svalue_0}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\estab{\obnd{\sowner_2}{\stype_2}{\sowner_3}}{\svalue_1})} \rredA \svalue_0 \feq \emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_2}{\sowner_3}}{\svalue_1})}$
            \end{pfproof}
        \end{pfproof}
      \step{0.2}{\scase{$\rexpr{\svalue_0}{\ehist{\sblist_0}{\svalue_0}}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\estab{\obnd{\sowner_2}{\stype_2}{\sowner_3}}{\svalue_1})} \rredA \svalue_0 \feq \emopt{\obnd{\sowner_0}{\stype_1}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_2}{\sowner_3}}{\svalue_1})}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\stype_0 \eeq \tint$}}
    \begin{pfproof}
      similar to previous case
    \end{pfproof}

  \step{2}{\case{$\stype_0 \eeq \tpair{\stype_1}{\stype_2}$}}
    \begin{pfproof}
      \step{2.0}{$\svalue_0 \in \epair{\svalue}{\svalue}$}
        \begin{pfproof}
          by inversion $\sWTN$
        \end{pfproof}
      \step{2.2}{\scase{$\rexpr{\svalue_0}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\epair{\svalue_2}{\svalue_3}}}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1} \nredAS \emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1}$
            \end{pfproof}
        \end{pfproof}
      \step{2.4}{\scase{$\rexpr{\svalue_0}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{(\ehist{\sblist_2}{\epair{\svalue_2}{\svalue_3}})}}$}}
        \begin{pfproof}
          \qedstep
            \begin{pfproof}
              $\edynb{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1} \nredAS \emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\svalue_1}$
            \end{pfproof}
        \end{pfproof}
      \step{2.5}{\scase{$\rexpr{\svalue_0}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{\epair{\svalue_2}{\svalue_3}})}}$}}
        \begin{pfproof}
          \step{2.5.0}{$\stype_5 \in \tpair{\stype}{\stype}$}
            \begin{pfproof}
              by inversion $\sWTA$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              ${\edynb{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{(\estab{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{\epair{\svalue_2}{\svalue_3}})}} \nredAS
               {\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{\epair{\svalue_2}{\svalue_3}})}}$
            \end{pfproof}
        \end{pfproof}
      \step{2.7}{\scase{$\rexpr{\svalue_0}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\emon{\sbnd_2}{\epair{\svalue_2}{\svalue_3}})})}}$}}
        \begin{pfproof}
          \absurdstep
            \begin{pfproof}
              by \lemmaref{A-S-mon-limit}
            \end{pfproof}
        \end{pfproof}
      \step{2.8}{\scase{$\rexpr{\svalue_0}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_2}{\svalue_3}})})})}}$}}
        \begin{pfproof}
          \absurdstep
            \begin{pfproof}
              by \lemmaref{A-S-mon-limit}
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\stype_0 \eeq \tfun{\stype_1}{\stype_2}$}}
    \begin{pfproof}
      \step{3.0}{$\svalue_0 \in \efun{\svar}{\sexpr} \cup \emon{\sbnd}{\svalue}$}
        \begin{pfproof}
          by inversion $\sWTN$
        \end{pfproof}
      \step{3.1}{\scase{$\rexpr{\svalue_0}{\emon{\obnd{\sowner_0}{\tfun{\stype_3}{\stype_4}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{\svalue_1})}}$}}
        \begin{pfproof}
          \step{3.1.0}{$\stype_5 \in \tfun{\stype}{\stype}$}
            \begin{pfproof}
              by inversion $\sWTA$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              ${\emon{\obnd{\sowner_0}{\tfun{\stype_3}{\stype_4}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{\svalue_1})}} \nredAS {\emon{\obnd{\sowner_0}{\tfun{\stype_3}{\stype_4}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{\svalue_1})}}$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{A-compat-subt}
  If\/ $\fshallow{\tagof{\stype_0}}{\svalue_0}$
  and\/ $\stype_0 \subteq \stype_1$
  then\/ $\fshallow{\tagof{\stype_1}}{\svalue_0}$.
\end{lemma}{
  \newcommand{\shortpf}{By induction on $\svalue_0$ via case analysis of $\fshallow{\tagof{\stype_0}}{\svalue_0}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\fshallow{\tagof{\tnat}}{\sint_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\stype_1 \in \tnat \cup \tint$}
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\fshallow{\tagof{\tint}}{\sint_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\stype_1 \in \tint$}
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\fshallow{\tagof{\tfun{\stype_2}{\stype_3}}}{\efun{\svar_0}{\sexpr_0}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\stype_1 \in \tfun{\stype}{\stype}$}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\fshallow{\tagof{\tfun{\stype_3}{\stype_4}}}{\efun{\tann{\svar_0}{\stype_2}}{\sexpr_0}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\stype_1 \in \tfun{\stype}{\stype}$}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\fshallow{\tagof{\tpair{\stype_2}{\stype_3}}}{\epair{\svalue_2}{\svalue_3}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\stype_1 \in \tpair{\stype}{\stype}$}
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\fshallow{\tagof{\tfun{\stype_4}{\stype_5}}}{\emon{\obnd{\sowner_0}{\tfun{\stype_2}{\stype_3}}{\sowner_1}}{\svalue_1}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\stype_1 \in \tfun{\stype}{\stype}$}
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\fshallow{\tagof{\tpair{\stype_4}{\stype_5}}}{\emon{\obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}}{\svalue_1}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\stype_1 \in \tpair{\stype}{\stype}$}
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\fshallow{\tagof{\stype_0}}{\ehist{\sblist_0}{\svalue_1}}$}}
    \begin{pfproof}
      \step{7.0}{$\fshallow{\tagof{\stype_0}}{\svalue_1}$}
        \begin{pfproof}
          by inversion $\sshallow$
        \end{pfproof}
      \step{7.1}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
      \qedstep
        \begin{pfproof}
          by definition $\sshallow$
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{A-dyn-mopt}
  If\/ $\fshallow{\tagof{\stype_0}}{\svalue_0}$
  and\/ $\snil \sWTA \svalue_0 : \tdyn$
  then\/ $\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredAS \emopt{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0}$.
\end{lemma}{
  \newcommand{\shortpf}{By case analysis of $\fshallow{\tagof{\stype_0}}{\svalue_0}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\fshallow{\tagof{\tnat}}{\snat_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\edynb{\obnd{\sowner_0}{\tnat}{\sowner_1}}{\snat_0} \nredAS \snat_0$
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\fshallow{\tagof{\tint}}{\sint_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\edynb{\obnd{\sowner_0}{\tint}{\sowner_1}}{\sint_0} \nredAS \sint_0$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\fshallow{\tagof{\tfun{\stype_1}{\stype_2}}}{\efun{\svar_0}{\sexpr_0}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredAS \emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0}$
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\fshallow{\tagof{\tfun{\stype_2}{\stype_3}}}{\efun{\tann{\svar_0}{\stype_1}}{\sexpr_0}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_0 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\fshallow{\tagof{\tpair{\stype_1}{\stype_2}}}{\epair{\svalue_1}{\svalue_2}}$}}
    \begin{pfproof}
      $\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredAS \emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0}$
    \end{pfproof}

  \step{5}{\case{$\fshallow{\tagof{\tfun{\stype_3}{\stype_4}}}{\emon{\obnd{\sowner_0}{\tfun{\stype_1}{\stype_2}}{\sowner_1}}{\svalue_1}}$}}
    \begin{pfproof}
      $\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredAS \emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0}$
    \end{pfproof}

  \step{6}{\case{$\fshallow{\tagof{\tpair{\stype_3}{\stype_4}}}{\emon{\obnd{\sowner_0}{\tpair{\stype_1}{\stype_2}}{\sowner_1}}{\svalue_1}}$}}
    \begin{pfproof}
      $\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0} \nredAS \emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_0}$
    \end{pfproof}

  \step{7}{\case{$\fshallow{\tagof{\stype_1}}{\ehist{\sblist_0}{\svalue_1}}$}}
    \begin{pfproof}
      \step{7.0}{$\fshallow{\tagof{\stype_1}}{\svalue_1}$}
        \begin{pfproof}
          by inversion $\sshallow$
        \end{pfproof}
      \step{7.1}{$\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1} \nredAS \emopt{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1}$}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          {$\edynb{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\ehist{\sblist_0}{\svalue_1}} \nredAS \emopt{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\ehist{\sblist_0}{\svalue_1})}$}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{HA-S-unop}
  If\/ $\svalue_0$ and\/ $\svalue_1$ are \reducedsurfaceexpressions{}
  and\/ $\rexpr{\eunopt{\stoptional}{\svalue_0}}{\eunopt{\stoptional}{\svalue_1}}$
  and\/ $\snil \sWTN {\eunopt{\stoptional}{\svalue_0}} : \stype_0$
  and\/ $\snil \sWTA {\eunopt{\stoptional}{\svalue_1}} : \stype_1$
  and\/ $\stype_0 \subteq \stype_1$
  then\/ $\eunopt{\stoptional}{\svalue_1} \rredA \svalue_2$
  and\/ $\rexpr{\sdeltaH(\sunop, \svalue_0)}{\svalue_2}$
\end{lemma}{
  \newcommand{\shortpf}{By induction on $\svalue_1$ via case analysis of $\srexpr$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf
  The cases for $\sunop \eeq \tinst{\sfst}{\stype_2}$ and $\sunop \eeq \tinst{\ssnd}{\stype_2}$  are analogous; we show only the $\sfst$ cases.

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \eunopt{\stoptional}{\svalue_0} : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_0}{\sint_0}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \eunopt{\stoptional}{\svalue_0} : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\epair{\svalue_4}{\svalue_5}}$}}
    \begin{pfproof}
      \step{2.0}{$\rexpr{\svalue_2}{\svalue_4}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{2.1}{$\sdeltaH(\sunop, \svalue_0) \feq \svalue_2$}
        \begin{pfproof}
          by definition $\sdeltaH$
        \end{pfproof}
      \step{2.2}{$\eunopt{\stoptional}{\svalue_1} \nredAS \svalue_4$}
        \begin{pfproof}
          by definition $\nredAS$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \stepref{2.0}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{3.0}{$\rexpr{\svalue_2}{\emopt{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_4}}$}
        \begin{pfproof}
          by inversion $\srexpr$ and $\stype_3 \subteq \stype_2$
        \end{pfproof}
      \step{3.1}{$\sdeltaH(\sunop, \svalue_0) \feq \svalue_2$}
        \begin{pfproof}
          by definition $\sdeltaH$
        \end{pfproof}
      \step{3.2}{$\eunopt{\stoptional}{\svalue_1}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\eunopt{\stoptional}{\epair{\svalue_4}{\svalue_5}})}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_4}$}
        \begin{pfproof}
          by definition $\credA$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-S-compat-1}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_0}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_0}{(\emon{\obnd{\sowner_1}{\tpair{\stype_3}{\stype_4}}{\sowner_2}}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_1$
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{(\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{6.0}{$\rexpr{\svalue_2}{\emopt{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_4})}}$}
        \begin{pfproof}
          by inversion $\srexpr$ and $\stype_3 \subteq \stype_2$
        \end{pfproof}
      \step{6.1}{$\sdeltaH(\sunop, \svalue_0) \feq \svalue_2$}
        \begin{pfproof}
          by definition $\sdeltaH$
        \end{pfproof}
      \step{6.2}{$\eunopt{\stoptional}{\svalue_1}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\eunopt{\stoptional}{(\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}})})}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\faddtrace{\sblist_2}{\svalue_4})}$}
        \begin{pfproof}
          by definition $\credA$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-S-compat-1}
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_3}{\stype_4}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\tpair{\stype_5}{\stype_6}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{7.0}{$\rexpr{\svalue_2}{\emopt{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\emopt{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{\svalue_4})}}$}
        \begin{pfproof}
          by inversion $\srexpr$ and $\stype_3 \subteq \stype_2$
        \end{pfproof}
      \step{7.1}{$\sdeltaH(\sunop, \svalue_0) \feq \svalue_2$}
        \begin{pfproof}
          by definition $\sdeltaH$
        \end{pfproof}
      \step{7.2}{$\eunopt{\stoptional}{\svalue_1}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\eunopt{\stoptional}{(\emon{\obnd{\sowner_2}{\tpair{\stype_5}{\stype_6}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}})})}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\estab{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{(\eunopt{\stoptional}{\epair{\svalue_4}{\svalue_5}})})}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\estab{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{\svalue_4})}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\estab{\obnd{\sowner_2}{\stype_5}{\sowner_3}}{\svalue_4})}$}
        \begin{pfproof}
          by definition $\credA$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-S-compat-2}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}}{(\ehist{\sblist_2}{(\emon{\obnd{\sowner_3}{\tpair{\stype_4}{\stype_5}}{\sowner_4}}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \step{8.0}{$\rexpr{\svalue_2}{\emopt{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\faddtrace{\sblist_2}{(\emopt{\obnd{\sowner_3}{\stype_4}{\sowner_4}}{\svalue_4})})}}$}
        \begin{pfproof}
          by inversion $\srexpr$ and $\stype_3 \subteq \stype_2$
        \end{pfproof}
      \step{8.1}{$\sdeltaH(\sunop, \svalue_0) \feq \svalue_2$}
        \begin{pfproof}
          by definition $\sdeltaH$
        \end{pfproof}
      \step{8.2}{$\eunopt{\stoptional}{\svalue_1}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\eunopt{\stoptional}{(\ehist{\sblist_2}{(\emon{\obnd{\sowner_3}{\tpair{\stype_4}{\stype_5}}{\sowner_4}}{\epair{\svalue_4}{\svalue_5}})})})}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\eprehist{\sblist_2}{(\estab{\obnd{\sowner_3}{\stype_4}{\sowner_4}}{(\eunopt{\stoptional}{\epair{\svalue_4}{\svalue_5}})})})}
                  \\\credA \edynb{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\eprehist{\sblist_2}{(\estab{\obnd{\sowner_3}{\stype_4}{\sowner_4}}{\svalue_4})})}$}
        \begin{pfproof}
          by definition $\credA$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{HA-S-compat-2}
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\emon{\sbnd_2}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-S-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-S-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{$\rexpr{\efun{\svar_2}{\sexpr_2}}{\efun{\svar_2}{\sexpr_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \eunopt{\stoptional}{\svalue_0} : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{12}{\case{$\rexpr{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2}}{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \eunopt{\stoptional}{\svalue_0} : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{13}{\case{$\rexpr{\emon{\obnd{\sowner_0}{\tfun{\stype_2}{\stype_3}}{\sowner_1}}{(\emon{\sbnd_2}{\svalue_2})}}{\ehist{\sblist_3}{\efun{\svar_3}{\sexpr_3}}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \eunopt{\stoptional}{\svalue_0} : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{14}{\case{$\rexpr{\emon{\obnd{\sowner_0}{\tfun{\stype_2}{\stype_3}}{\sowner_1}}{\svalue_2}}{\emon{\obnd{\sowner_0}{\tfun{\stype_4}{\stype_5}}{\sowner_1}}{\svalue_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \eunopt{\stoptional}{\svalue_0} : \stype_0$
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{HA-D-unop}
  If\/ $\svalue_0$ and\/ $\svalue_1$ are \reducedsurfaceexpressions{}
  and\/ $\rexpr{\eunopt{\stoptional}{\svalue_0}}{\eunopt{\stoptional}{\svalue_1}}$
  and\/ $\snil \sWTN {\eunopt{\stoptional}{\svalue_0}} : \tdyn$
  and\/ $\snil \sWTA {\eunopt{\stoptional}{\svalue_1}} : \tdyn$
  then\/ $\eunopt{\stoptional}{\svalue_0} \nredND \sexpr_2$
  and\/ $\eunopt{\stoptional}{\svalue_1} \rredA \sexpr_3$
  and\/ $\rexpr{\sexpr_2}{\sexpr_3}$.
\end{lemma}{
  \newcommand{\shortpf}{By cases on $\rexpr{\svalue_0}{\svalue_1}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf
  The cases for $\sunop \eeq \tinst{\sfst}{\stype}$ and $\sunop \eeq \tinst{\ssnd}{\stype}$ are similar; we present only the $\sfst$ cases.

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\eunopt{\stoptional}{\svalue_0} \nredND \tagerrorD$}
          and
          {$\eunopt{\stoptional}{\svalue_1} \nredAD \tagerrorD$}
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_0}{\sint_0}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\eunopt{\stoptional}{\svalue_0} \nredND \tagerrorD$}
          and
          {$\eunopt{\stoptional}{\svalue_1} \nredAD \tagerrorD$}
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\epair{\svalue_4}{\svalue_5}}$}}
    \begin{pfproof}
      \step{2.0}{$\rexpr{\svalue_2}{\svalue_4}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          {$\eunopt{\stoptional}{\svalue_0} \nredND \svalue_2$}
          and
          {$\eunopt{\stoptional}{\svalue_1} \nredAD \svalue_4$}
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{3.0}{$\rexpr{\svalue_2}{\emopt{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_4}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{3.1}{$\eunopt{\stoptional}{\svalue_0} \nredND \svalue_2$}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{3.2}{$\eunopt{\stoptional}{\svalue_1}
                  \\\credA \estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{(\eunopt{\stoptional}{\epair{\svalue_4}{\svalue_5}})}
                  \\\credA \estab{\obnd{\sowner_0}{\stype_2}{\sowner_1}}{\svalue_4}$}
        \begin{pfproof}
          by definition $\credA$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{A-sta-mopt}
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_0}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{4.0}{$\rexpr{\svalue_2}{\faddtrace{\sblist_0}{\svalue_4}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{4.1}{$\eunopt{\stoptional}{\svalue_0} \nredND \svalue_2$}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{4.2}{$\eunopt{\stoptional}{\svalue_1} \nredAD \faddtrace{\sblist_0}{\svalue_4}$}
        \begin{pfproof}
          by definition $\nredAD$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \stepref{4.0}
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_0}{(\emon{\obnd{\sowner_1}{\tpair{\stype_2}{\stype_3}}{\sowner_2}}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{5.0}{$\rexpr{\svalue_2}{\faddtrace{\sblist_0}{(\emopt{\obnd{\sowner_1}{\stype_2}{\sowner_2}}{\svalue_4})}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{5.1}{$\eunopt{\stoptional}{\svalue_0} \nredND \svalue_2$}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{5.2}{$\eunopt{\stoptional}{\svalue_1}
                  \\\credA \eprehist{\sblist_0}{(\estab{\obnd{\sowner_1}{\stype_2}{\sowner_2}}{(\eunopt{\stoptional}{\epair{\svalue_4}{\svalue_5}})})}
                  \\\credA \eprehist{\sblist_0}{(\estab{\obnd{\sowner_1}{\stype_2}{\sowner_2}}{\svalue_4})}
                  \\\credA \eprehist{\sblist_0}{(\emopt{\obnd{\sowner_1}{\stype_2}{\sowner_2}}{\svalue_4})}
                  \\\credA \faddtrace{\sblist_0}{(\emopt{\obnd{\sowner_1}{\stype_2}{\sowner_2}}{\svalue_4})}$}
        \begin{pfproof}
          by definition $\credA$ and \lemmaref{A-sta-mopt}
        \end{pfproof}
      \qedstep
    \end{pfproof}

  \step{6}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}}{(\ehist{\sblist_2}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\obnd{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}}{(\emon{\obnd{\sowner_2}{\tpair{\stype_4}{\stype_5}}{\sowner_3}}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sowner_0}{\tpair{\stype_2}{\stype_3}}{\sowner_1}}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})})}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\emon{\sbnd_2}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_0}{(\emon{\sbnd_1}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{$\rexpr{\efun{\svar_2}{\sexpr_2}}{\efun{\svar_2}{\sexpr_3}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\eunopt{\stoptional}{\svalue_0} \nredND \tagerrorD$}
          and 
          {$\eunopt{\stoptional}{\svalue_1} \nredAD \tagerrorD$}
        \end{pfproof}
    \end{pfproof}

  \step{12}{\case{$\rexpr{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2}}{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTN \svalue_0 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{13}{\case{$\rexpr{\emon{\obnd{\sowner_0}{\tfun{\stype_2}{\stype_3}}{\sowner_1}}{(\emon{\sbnd_2}{\svalue_2})}}{\ehist{\sblist_3}{\efun{\svar_3}{\sexpr_3}}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\eunopt{\stoptional}{\svalue_0} \nredND \tagerrorD$}
          and 
          {$\eunopt{\stoptional}{\svalue_1} \nredAD \tagerrorD$}
        \end{pfproof}
    \end{pfproof}

  \step{14}{\case{$\rexpr{\emon{\obnd{\sowner_0}{\tfun{\stype_2}{\stype_3}}{\sowner_1}}{\svalue_2}}{\emon{\obnd{\sowner_0}{\tfun{\stype_4}{\stype_5}}{\sowner_1}}{\svalue_3}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          {$\eunopt{\stoptional}{\svalue_0} \nredND \tagerrorD$}
          and 
          {$\eunopt{\stoptional}{\svalue_1} \nredAD \tagerrorD$}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{A-sta-mopt}
  If\/ $\svalue_0$ and\/ $\svalue_1$ are \reducedsurfaceexpressions{}
  and\/ $\snil \sWTN \svalue_0 : \tdyn$
  and\/ $\snil \sWTA \svalue_1 : \stype_0$
  and\/ $\rexpr{\svalue_0}{\emopt{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1}}$
  then\/ $\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1} \rredA \svalue_2$
  and\/ $\rexpr{\svalue_0}{\svalue_2}$.
\end{lemma}{
  \newcommand{\shortpf}{By case analysis of $\srexpr$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1} \nredAD \svalue_1$
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_2}{\sint_0}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1} \nredAD \svalue_0$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_3}{\svalue_4}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\epair{\svalue_5}{\svalue_6}}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1} \nredAD \emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1}$
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_3}{\svalue_4}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\ehist{\sblist_2}{\epair{\svalue_5}{\svalue_6}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_3}{\svalue_4}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\emon{\sbnd_2}{\epair{\svalue_5}{\svalue_6}})}}$}}
    \begin{pfproof}
      \step{4.0}{\(
        \rexpr{\svalue_3}{\emopt{\obnd{\sowner_0}{\ftypefst{\stype_0}}{\sowner_1}}{(\emon{\fbndfst{\sbnd_2}}{\svalue_5})}}
      \) \\ and \(
        \rexpr{\svalue_4}{\emopt{\obnd{\sowner_0}{\ftypesnd{\stype_0}}{\sowner_1}}{(\emon{\fbndsnd{\sbnd_2}}{\svalue_6})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{4.1}{\(
        \estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\emon{\sbnd_2}{\epair{\svalue_5}{\svalue_6}})}
        \nredAD
        \ehist{\fconcat{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\sbnd_2}}{\epair{\svalue_5}{\svalue_6}}
      \)}
        \begin{pfproof}
          by definition $\nredAD$
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\rexpr{\epair{\svalue_3}{\svalue_4}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\ehist{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\rexpr{\epair{\svalue_3}{\svalue_4}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\emon{\sbnd_2}{(\ehopt{\sblist_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \step{6.0}{$\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1} \nredAD \ehist{\fconcat{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\fconcat{\sbnd_2}{\sblist_3}}}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})}$}
        \begin{pfproof}
          by definition $\nredAD$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{A-moptmopt-bnd}
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\rexpr{\epair{\svalue_3}{\svalue_4}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\emon{\sbnd_2}{(\emon{\sbnd_3}{(\ehopt{\sblist_4}{(\emon{\sbnd_5}{\epair{\svalue_4}{\svalue_5}})})})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\rexpr{\emon{\sbnd_2}{(\efun{\svar_2}{\sexpr_2})}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\efun{\svar_2}{\sexpr_3})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \stype_0$
        \end{pfproof}
    \end{pfproof}

  \step{9}{\case{$\rexpr{\emon{\sbnd_2}{(\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2})}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3})}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1} \nredAD \emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1}$
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{(\efun{\svar_2}{\sexpr_2})})}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\emon{\sbnd_4}{(\ehopt{\sblist_5}{(\efun{\svar_2}{\sexpr_3})})})}}$}}
    \begin{pfproof}
      \step{10.0}{$\estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1} \nredND \faddtrace{\fconcat{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\fconcat{\sbnd_4}{\sblist_5}}}{(\efun{\svar_2}{\sexpr_3})}$}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{A-moptmopt-bnd}
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{(\efun{\svar_2}{\sexpr_2})})})}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\emon{\sbnd_5}{(\ehopt{\sblist_6}{(\emon{\sbnd_7}{(\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3})})})})}}$}}
    \begin{pfproof}
      \step{10.0}{\(
        \estab{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\svalue_1}
        \nredND
        \faddtrace{\fconcat{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{\fconcat{\sbnd_4}{\fconcat{\sbnd_5}{\sblist_6}}}}{(\emon{\sbnd_7}{(\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3})})}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by \lemmaref{A-moptmopt-bnd}
        \end{pfproof}
    \end{pfproof}

  \step{12}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{(\emon{\sbnd_5}{(\efun{\svar_2}{\sexpr_2})})})})}}{\emon{\obnd{\sowner_0}{\stype_0}{\sowner_1}}{(\emon{\sbnd_5}{(\emon{\sbnd_6}{(\emon{\sbnd_7}{\svalue_2})})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{A-moptmopt-bnd}
  If\/ $\svalue_0$ and\/ $\svalue_1$ are \reducedsurfaceexpressions{}
  and\/ $\snil \sWTN \svalue_0 : \tdyn$
  and\/ $\snil \sWTA \svalue_1 : \tdyn$
  and\/ $\rexpr{\svalue_0}{\emopt{\sbnd_0}{(\emopt{\sbnd_1}{\svalue_1})}}$
  then\/ $\rexpr{\svalue_0}{\faddtrace{\fconcat{\sbnd_0}{\sbnd_1}}{\svalue_1}}$.
\end{lemma}{
  \newcommand{\shortpf}{By induction on $\svalue_0$ via case analysis of $\srexpr$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\sint_0}{\ehist{\fconcat{\sbnd_0}{\sbnd_1}}{\sint_0}}$
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_2}{\sint_0}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\sint_0}{\ehist{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\sblist_2}}}{\sint_0}}$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{2.0}{\(
        \rexpr{\svalue_2}{\emopt{\fbndfst{\sbnd_0}}{(\emopt{\fbndfst{\sbnd_1}}{\svalue_4})}}
      \) \\and \(
        \rexpr{\svalue_3}{\emopt{\fbndsnd{\sbnd_0}}{(\emopt{\fbndsnd{\sbnd_1}}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{2.1}{\(
        \rexpr{\svalue_2}{\faddtrace{\fconcat{\fbndfst{\sbnd_0}}{\fbndfst{\sbnd_1}}}{\svalue_4}}
      \) \\and \(
        \rexpr{\svalue_3}{\faddtrace{\fconcat{\fbndsnd{\sbnd_0}}{\fbndsnd{\sbnd_1}}}{\svalue_5}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{(\ehopt{\sblist_2}{(\emon{\sbnd_3}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \step{3.0}{\(
        \rexpr{\svalue_2}{\emopt{\fbndfst{\sbnd_0}}{(\emopt{\fbndfst{\sbnd_1}}{(\faddtrace{\fbndfst{\sblist_2}}{(\emon{\sbnd_3}{\svalue_4})})})}}
      \) \\and \(
        \rexpr{\svalue_3}{\emopt{\fbndsnd{\sbnd_0}}{(\emopt{\fbndsnd{\sbnd_1}}{(\faddtrace{\fbndsnd{\sblist_2}}{(\emon{\sbnd_3}{\svalue_5})})})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{2.1}{\(
        \rexpr{\svalue_2}{\faddtrace{\fconcat{\fbndfst{\sbnd_0}}{\fbndfst{\sbnd_1}}}{(\faddtrace{\fbndfst{\sblist_2}}{(\emon{\sbnd_3}{\svalue_4})})}}
      \) \\and \(
        \rexpr{\svalue_3}{\faddtrace{\fconcat{\fbndsnd{\sbnd_0}}{\fbndsnd{\sbnd_1}}}{(\faddtrace{\fbndsnd{\sblist_2}}{(\emon{\sbnd_3}{\svalue_5})})}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{(\emon{\sbnd_2}{(\ehopt{\sblist_3}{(\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}})})})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{(\efun{\svar_2}{\sexpr_2})})}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{(\efun{\svar_2}{\sexpr_3})})}}$}}
    \begin{pfproof}
      \step{5.0}{$\rexpr{\efun{\svar_2}{\sexpr_2}}{\efun{\svar_2}{\sexpr_3}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by definition $\srexpr$
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{(\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2})})})}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{(\emon{\sbnd_5}{(\efun{\svar_2}{\sexpr_3})})})}}$}}
    \begin{pfproof}
      \step{6.0}{$\rexpr{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2}}{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3}}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by definition $\srexpr$
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\rexpr{\emon{\sbnd_2}{(\emon{\sbnd_3}{(\emon{\sbnd_4}{(\emon{\sbnd_5}{\svalue_2})})})}}{\emon{\sbnd_0}{(\emon{\sbnd_1}{(\emon{\sbnd_6}{(\emon{\sbnd_7}{\svalue_3})})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{H-app-A-bnd}
  If\/ ${\eapp{\tdyn}{\svalue_0}{\svalue_1}}$
  and\/ ${\eapp{\tdyn}{(\ehist{\fconcat{\sbnd_0}{\sblist_1}}{\svalue_2})}{\svalue_3}}$
  are \reducedsurfaceexpressions{}
  and\/ $\rexpr{\eapp{\tdyn}{\svalue_0}{\svalue_1}}{\eapp{\tdyn}{(\ehist{\fconcat{\sbnd_0}{\sblist_1}}{\svalue_2})}{\svalue_3}}$
  then one of the following holds:
  \begin{itemize}
    \item
      \({\eapp{\tdyn}{\svalue_0}{\svalue_1}} \rredN \ctx_0[\eapp{\stoptional}{\svalue_4}{(\boundaryerror{\sbnd_3}{\svalue_5})}]\)
      \\and\/ \(\rctx{\ctx_0}{\eprehist{\sbnd_0\cdots\sbnd_i}{\ctxhole}}\)
      \\and\/ \(\rexpr{\svalue_4}{\faddtrace{\sbnd_i\cdots\sbnd_n}{\svalue_2}}\)
    \item
      \( {\eapp{\tdyn}{\svalue_0}{\svalue_1}} \rredN \ctx_0[\eapp{\stoptional}{\svalue_4}{\svalue_5}] \)
      \\and\/ \( \rctx{\ctx_0}{\eprehist{\fconcat{\sbnd_0}{\sblist_1}}{\ctxhole}} \)
      \\and\/ \( \rexpr{\svalue_4}{\svalue_2} \)
      \\and\/ \( \rexpr{\svalue_5}{\faddtrace{\fflip{\fconcat{\sbnd_0}{\sblist_1}}}{\svalue_3}} \)
  \end{itemize}
\end{lemma}{
  \newcommand{\shortpf}{By induction on the length of $\sblist_1$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{$\sblist_1 = \snil$}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by $\srexpr$
        \end{pfproof}
    \end{pfproof}

  \step{1}{$\sblist_1 = \sbnd_1$}
    \begin{pfproof}
      \step{1.0}{\(
        \svalue_0 \eeq \emon{\sbnd_2}{(\emon{\sbnd_3}{\svalue_4})}
      \) and \(
        \sbnd_2 \subteq \sbnd_0
      \) and \(
        \sbnd_3 \subteq \sbnd_1
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{1.1}{\(
        \eapp{\tdyn}{\svalue_0}{\svalue_1}
        \nredND
        \estab{\fbndcod{\sbnd_2}}{(\eapp{\stype_1}{(\emon{\sbnd_3}{\svalue_4})}{(\edynb{\fbnddom{\sbnd_2}}{\svalue_1})})}
      \)}
        \begin{pfproof}
          by definition $\nredND$
        \end{pfproof}
      \step{1.2}{\assume{$\edynb{\fbnddom{\sbnd_2}{\svalue_1} \eeq \svalue_5$}}}
        \begin{pfproof}
          otherwise, end with a boundary error
        \end{pfproof}
      \step{1.4}{\(
        \eapp{\stype_1}{(\emon{\sbnd_3}{\svalue_4})}{\svalue_5}
        \nredNS
        \edynb{\fbndcod{\sbnd_3}}{(\eapp{\tdyn}{\svalue_4}{(\estab{\fbnddom{\sbnd_3}}{\svalue_5})})}
      \) and \(
        \estab{\fbnddom{\sbnd_3}}{\svalue_5} \nredND \svalue_6
      \)}
        \begin{pfproof}
          by definition $\nredNS$ and $\nredND$
        \end{pfproof}
      \step{1.5}{$\rexpr{\svalue_6}{\faddtrace{\fflip{\fconcat{\fbnddom{\sbnd_0}}{\fbnddom{\sbnd_1}}}}{\svalue_3}}$}
        \begin{pfproof}
          by \lemmaref{H-stadyn-A-bndbnd}
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\rexpr{\estab{\fbndcod{\sbnd_2}}{(\edynb{\fbndcod{\sbnd_3}}{(\eapp{\tdyn}{\svalue_4}{\svalue_6})})}}{\ehist{\fconcat{\sbnd_0}{\sbnd_1}}{(\eapp{\tdyn}{\svalue_2}{\ehist{\fflip{\fconcat{\sbnd_0}{\sbnd_1}}}{\svalue_3}})}}$
        \end{pfproof}
    \end{pfproof}

  \step{2}{$\sblist_1 = \fconcat{\sbnd_1}{\fconcat{\sbnd_2}{\sblist_3}}$}
    \begin{pfproof}
      \step{2.0}{$\svalue_0 \eeq \emon{\sbnd_3}{(\emon{\sbnd_4}{\svalue_4})}$
                 and $\sbnd_3 \subteq \sbnd_1$ and $\sbnd_4 \subteq \sbnd_2$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{2.1}{\(
        \eapp{\tdyn}{\svalue_0}{\svalue_1} \rredN \estab{\fbndcod{\sbnd_3}}{(\edynb{\fbnddom{\sbnd_4}}{(\eapp{\tdyn}{\svalue_4}{\svalue_6})})}
      \) \\ and \(
        \rexpr{\svalue_4}{\ehist{\sblist_3}{\svalue_2}}
      \) and \(
        \rexpr{\svalue_6}{\ehist{\fflip{\fconcat{\sbnd_0}{\sbnd_1}}}{\svalue_3}}
      \)}
        \begin{pfproof}
          by similar reasoning as the previous case
        \end{pfproof}
      \step{2.2}{$\eapp{\tdyn}{\svalue_4}{\svalue_6} \rredN \ctx_1[\eapp{\tdyn}{\svalue_7}{\svalue_8}]$}
        \begin{pfproof}
          by \pfih, assuming no boundary errors
        \end{pfproof}
      \qedstep
        \begin{pfproof}\(
          \rexpr{\estab{\sbnd_3}{(\edynb{\sbnd_4}{(\ctx_1[\eapp{\tdyn}{\svalue_7}{\svalue_8}])})}}{\faddtrace{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\fconcat{\sbnd_2}{\sblist_3}}}}{\eapp{\tdyn}{\svalue_2}{(\ehist{\fflip{\fconcat{\sbnd_0}{\fconcat{\sbnd_1}{\sblist_2}}}}{\svalue_3}}}}
        \)\end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{H-stadyn-A-bndbnd}
  If\/ $\svalue_0$ and\/ $\svalue_1$ are \reducedsurfaceexpressions{}
  and\/ $\snil \sWTN \svalue_0 : \tdyn$
  and\/ $\snil \sWTA \svalue_1 : \tdyn$
  and\/ $\rexpr{\svalue_0}{\svalue_1}$
  and\/ $\sbnd_0 \subteq \sbnd_2$
  and\/ $\sbnd_1 \subteq \sbnd_3$
  then\/ $\estab{\sbnd_0}{(\edynb{\sbnd_1}{\svalue_0})} \rredN \sexpr_2$
  and\/ $\rexpr{\sexpr_2}{\faddtrace{\fconcat{\sbnd_2}{\sbnd_3}}{\svalue_1}}$.
\end{lemma}{
  \newcommand{\shortpf}{By induction on $\svalue_0$ via cases on $\rexpr{\svalue_0}{\svalue_1}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  We assume below that every subexpression of the form $\edynb{\sbnd}{\svalue}$ steps to a value, because otherwise $\sexpr_2$ is a boundary error and the result is immediate.

  \step{0}{\case{$\rexpr{\sint_0}{\sint_0}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\sbnd_0}{(\edynb{\sbnd_1}{\sint_0})} \rredN \rexpr{\sint_0}{\ehist{\fconcat{\sbnd_2}{\sbnd_3}}{\sint_0}}$
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\rexpr{\sint_0}{\ehist{\sblist_0}{\ehist{\sblist_4}{\sint_0}}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\sbnd_0}{(\edynb{\sbnd_1}{\sint_0})} \rredN \rexpr{\sint_0}{\ehist{\fconcat{\sbnd_2}{\fconcat{\sbnd_3}{\sblist_4}}}{\sint_0}}$
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\epair{\svalue_4}{\svalue_5}}$}}
    \begin{pfproof}
      \step{2.0}{$\rexpr{\svalue_2}{\svalue_4}$ and $\rexpr{\svalue_3}{\svalue_5}$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{2.1}{$\estab{\sbnd_0}{(\edynb{\sbnd_1}{\epair{\svalue_2}{\svalue_3}})} \credN \estab{\sbnd_0}{\epair{\edynb{\fbndfst{\sbnd_1}}{\svalue_2}}{\edynb{\fbndsnd{\sbnd_1}}{\svalue_3}}}$}
        \begin{pfproof}
          by definition $\credN$
        \end{pfproof}
      \step{2.2}{\(
        \estab{\sbnd_0}{\epair{\edynb{\fbndfst{\sbnd_1}}{\svalue_2}}{\edynb{\fbndsnd{\sbnd_1}}{\svalue_3}}} \rredN \epair{\svalue_6}{\svalue_7}
      \) \\ if and only if \(
        \epair{\estab{\fbndfst{\sbnd_0}}{(\edynb{\fbndfst{\sbnd_1}}{\svalue_2})}}{\estab{\fbndsnd{\sbnd_0}}{(\edynb{\fbndsnd{\sbnd_1}}{\svalue_3})}} \rredN \epair{\svalue_6}{\svalue_7}
      \)}
        \begin{pfproof}
          by \lemmaref{H-stadyn-pair}
        \end{pfproof}
      \step{2.3}{\(
        \rexpr{\svalue_6}{\faddtrace{\fconcat{\fbndfst{\sbnd_2}}{\fbndfst{\sbnd_3}}}{\svalue_4}}
      \) \\ and \(
        \rexpr{\svalue_7}{\faddtrace{\fconcat{\fbndsnd{\sbnd_2}}{\fbndsnd{\sbnd_3}}}{\svalue_4}}
      \)}
        \begin{pfproof}
          by \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by definition $\srexpr$
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_4}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{3.0}{\(
        \rexpr{\svalue_2}{\emopt{\fbndfst{\sbnd_4}}{\svalue_4}}
      \) and \(
        \rexpr{\svalue_3}{\emopt{\fbndsnd{\sbnd_4}}{\svalue_5}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{3.1}{\(
        \estab{\sbnd_0}{(\edynb{\sbnd_1}{\epair{\svalue_2}{\svalue_3}})} \rredN \epair{\svalue_6}{\svalue_7}
      \) \\ and \(
        \rexpr{\svalue_6}{\faddtrace{\fconcat{\fbndfst{\sbnd_2}}{\fbndfst{\sbnd_3}}}{\emopt{\fbndfst{\sbnd_4}}{\svalue_4}}}
      \) \\ and \(
        \rexpr{\svalue_7}{\faddtrace{\fconcat{\fbndsnd{\sbnd_2}}{\fbndsnd{\sbnd_3}}}{\emopt{\fbndsnd{\sbnd_4}}{\svalue_5}}}
      \)}
        \begin{pfproof}
          by definition $\credN$ and \lemmaref{H-stadyn-pair} and \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by definition $\srexpr$
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_4}{\epair{\svalue_4}{\svalue_5}}}$}}
    \begin{pfproof}
      \step{4.0}{\(
        \rexpr{\svalue_2}{\faddtrace{\fbndfst{\sblist_4}}{\svalue_4}}
      \) and \(
        \rexpr{\svalue_3}{\faddtrace{\fbndsnd{\sblist_4}}{\svalue_5}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{4.1}{\(
        \estab{\sbnd_0}{(\edynb{\sbnd_1}{\epair{\svalue_2}{\svalue_3}})} \rredN \epair{\svalue_6}{\svalue_7}
      \) \\ and \(
        \rexpr{\svalue_6}{\faddtrace{\fconcat{\fbndfst{\sbnd_2}}{\fbndfst{\sbnd_3}}}{\faddtrace{\fbndfst{\sblist_4}}{\svalue_4}}}
      \) \\ and \(
        \rexpr{\svalue_7}{\faddtrace{\fconcat{\fbndsnd{\sbnd_2}}{\fbndsnd{\sbnd_3}}}{\faddtrace{\fbndsnd{\sblist_4}}{\svalue_5}}}
      \)}
        \begin{pfproof}
          by definition $\credN$ and \lemmaref{H-stadyn-pair} and \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by definition $\srexpr$
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\ehist{\sblist_4}{(\emon{\sbnd_5}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \step{5.0}{\(
        \rexpr{\svalue_2}{\faddtrace{\fbndfst{\sblist_4}}{(\emopt{\fbndfst{\sbnd_5}}{\svalue_4})}}
      \) and \(
        \rexpr{\svalue_3}{\faddtrace{\fbndsnd{\sblist_4}}{(\emopt{\fbndsnd{\sbnd_5}}{\svalue_5})}}
      \)}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \step{5.1}{\(
        \estab{\sbnd_0}{(\edynb{\sbnd_1}{\epair{\svalue_2}{\svalue_3}})} \rredN \epair{\svalue_6}{\svalue_7}
      \) \\ and \(
        \rexpr{\svalue_6}{\faddtrace{\fconcat{\fbndfst{\sbnd_2}}{\fbndfst{\sbnd_3}}}{\faddtrace{\fbndfst{\sblist_4}}{(\emopt{\fbndfst{\sbnd_5}}{\svalue_4})}}}
      \) \\ and \(
        \rexpr{\svalue_7}{\faddtrace{\fconcat{\fbndsnd{\sbnd_2}}{\fbndsnd{\sbnd_3}}}{\faddtrace{\fbndsnd{\sblist_4}}{(\emopt{\fbndsnd{\sbnd_5}}{\svalue_5})}}}
      \)}
        \begin{pfproof}
          by definition $\credN$ and \lemmaref{H-stadyn-pair} and \pfih
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by definition $\srexpr$
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_4}{(\ehist{\sblist_5}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_4}{(\emon{\sbnd_5}{\epair{\svalue_4}{\svalue_5}})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emon{\sbnd_4}{(\ehist{\sblist_5}{(\emon{\sbnd_6}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{8}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_4}{(\emon{\sbnd_5}{(\emon{\sbnd_6}{\epair{\svalue_4}{\svalue_5}})})}}$}}
    \begin{pfproof}
      xxx
    \end{pfproof}

  \step{9}{\case{$\rexpr{\epair{\svalue_2}{\svalue_3}}{\emonplus{\sblist_4}{(\emon{\sbnd_5}{(\ehist{\sbnd_6}{(\emon{\sbnd_7}{\epair{\svalue_4}{\svalue_5}})})})}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          by \lemmaref{A-D-mon-limit}
        \end{pfproof}
    \end{pfproof}

  \step{10}{\case{$\rexpr{\efun{\svar_2}{\sexpr_2}}{\efun{\svar_2}{\sexpr_3}}$}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\sbnd_0}{(\edynb{\sbnd_1}{\svalue_0})} \rredN \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_1}{\svalue_0})}}{\ehist{\fconcat{\sbnd_2}{\sbnd_3}}{\svalue_1}}$
        \end{pfproof}
    \end{pfproof}

  \step{11}{\case{$\rexpr{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_2}}{\efun{\tann{\svar_2}{\stype_2}}{\sexpr_3}}$}}
    \begin{pfproof}
      \absurdstep
        \begin{pfproof}
          $\snil \sWTA \svalue_1 : \tdyn$
        \end{pfproof}
    \end{pfproof}

  \step{12}{\case{\(
    \rexpr{\emon{\sbnd_4}{(\emon{\sbnd_5}{\svalue_3})}}{\ehist{\fconcat{\sbnd_6}{\sbnd_7}}{\svalue_4}}
  \) \\ and \(
    \svalue_4 \in \efun{\svar}{\sexpr} \cup \emon{\sbnd}{(\efun{\tann{\svar}{\stype}}{\sexpr})}
  \)}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\sbnd_0}{(\edynb{\sbnd_1}{\svalue_0})} \rredN \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_1}{\svalue_0})}}{\ehist{\fconcat{\sbnd_2}{\fconcat{\sbnd_3}{\fconcat{\sbnd_6}{\sbnd_7}}}}{\svalue_4}}$
        \end{pfproof}
    \end{pfproof}

  \step{13}{\case{\(
    \rexpr{\emon{\sbnd_4}{(\emon{\sbnd_5}{\svalue_3})}}{\ehist{\fconcat{\sbnd_6}{\fconcat{\sbnd_7}{\sblist_8}}}{\svalue_4}}
  \) \\ and \(
    \svalue_4 \in \efun{\svar}{\sexpr} \cup \emon{\sbnd}{(\efun{\tann{\svar}{\stype}}{\sexpr})}
  \)}}
    \begin{pfproof}
      \qedstep
        \begin{pfproof}
          $\estab{\sbnd_0}{(\edynb{\sbnd_1}{\svalue_0})} \rredN \rexpr{\emon{\sbnd_0}{(\emon{\sbnd_1}{\svalue_0})}}{\ehist{\fconcat{\sbnd_2}{\fconcat{\sbnd_3}{\fconcat{\sbnd_6}{\fconcat{\sbnd_7}{\sblist_8}}}}}{\svalue_4}}$
        \end{pfproof}
    \end{pfproof}

  \step{14}{\case{$\rexpr{\emon{\sbnd_4}{\svalue_3}}{\emon{\sbnd_5}{\svalue_4}}$}}
    \begin{pfproof}
      \step{16.0}{$\svalue_4 \in \efun{\tann{\svar}{\stype}}{\sexpr}$}
        \begin{pfproof}
          by inversion $\sWTA$ and $\srexpr$ and \lemmaref{A-D-mon-limit}
        \end{pfproof}
      \step{16.1}{$\estab{\sbnd_0}{(\edynb{\sbnd_1}{\svalue_0})} \rredN \emon{\sbnd_0}{(\emon{\sbnd_1}{\svalue_0})}$}
        \begin{pfproof}
          by definition $\credN$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          by definition $\srexpr$
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{H-stadyn-pair}
  $\estab{\sbnd_0}{\epair{\edynb{\sbnd_1}{\svalue_0}}{\edynb{\sbnd_2}{\svalue_1}}} \rredN \epair{\svalue_2}{\svalue_3}$
  if and only if
  \\
  $\epair{\estab{\fbndfst{\sbnd_0}}{(\edynb{\sbnd_1}{\svalue_0})}}{\estab{\fbndsnd{\sbnd_0}}{(\edynb{\sbnd_2}{\svalue_1})}} \rredN \epair{\svalue_2}{\svalue_3}$
\end{lemma}{
  \newcommand{\shortpf}{By definition of $\nredNS$ and $\nredND$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf
\end{lamportproof*}}

\begin{lemma}\label{HA-binop}
  If\/ $\rexpr{\ebinopt{\stoptional}{\svalue_0}{\svalue_1}}{\ebinopt{\stoptional}{\svalue_2}{\svalue_3}}$
  then\/ ${\ebinopt{\stoptional}{\svalue_0}{\svalue_1}} \credN \sexpr_4$
  if and only if\/ ${\ebinopt{\stoptional}{\svalue_2}{\svalue_3}} \credA \sexpr_5$
\end{lemma}{
  \newcommand{\shortpf}{The binary operations are only defined for integers and $\srexpr$ relates integers iff they are equal.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf

  \step{0}{\case{$\ebinopt{\stoptional}{\svalue_0}{\svalue_1} \nredND \tagerrorD$}}
    \begin{pfproof}
      \step{0.0}{\scase{$\svalue_0 \not\in \sint$}}
        \begin{pfproof}
          \step{0.0.0}{$\svalue_2 \not\in \sint$}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              $\ebinopt{\stoptional}{svalue_2}{\svalue_3} \nredAD \tagerrorD$
            \end{pfproof}
        \end{pfproof}
      \step{0.1}{\scase{$\svalue_1 \not\in \sint$}}
        \begin{pfproof}
          \step{0.1.0}{$\svalue_3 \not\in \sint$}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              $\ebinopt{\stoptional}{\svalue_2}{\svalue_3} \nredAD \tagerrorD$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{1}{\case{$\ebinopt{\stoptional}{\svalue_2}{\svalue_3} \nredAD \tagerrorD$}}
    \begin{pfproof}
      \step{1.0}{\scase{$\fremtrace{\svalue_2} \not\in \sint$}}
        \begin{pfproof}
          \step{1.0.0}{$\svalue_0 \not\in \sint$}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              $\ebinopt{\stoptional}{svalue_0}{\svalue_1} \nredND \tagerrorD$
            \end{pfproof}
        \end{pfproof}
      \step{1.1}{\scase{$\fremtrace{\svalue_3} \not\in \sint$}}
        \begin{pfproof}
          \step{1.1.0}{$\svalue_1 \not\in \sint$}
            \begin{pfproof}
              by inversion $\srexpr$
            \end{pfproof}
          \qedstep
            \begin{pfproof}
              $\ebinopt{\stoptional}{\svalue_0}{\svalue_1} \nredND \tagerrorD$
            \end{pfproof}
        \end{pfproof}
    \end{pfproof}

  \step{2}{\case{$\sbinop = \ssum$ and $\svalue_0 \eeq \sint_0$ and $\svalue_1 \eeq \sint_1$}}
    \begin{pfproof}
      \step{2.0}{$\ebinopt{\stoptional}{\svalue_0}{\svalue_1} \credN \svalue_0 + \svalue_1$}
        \begin{pfproof}
          by definition $\nredNS$, $\nredND$, and $\sdeltaH$
        \end{pfproof}
      \step{2.1}{$\fremtrace{\svalue_2} \eeq \svalue_0$ and $\fremtrace{\svalue_3} \eeq \svalue_1$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\ebinopt{\stoptional}{\svalue_2}{\svalue_3} \credA \svalue_0 + \svalue_1$
        \end{pfproof}
    \end{pfproof}

  \step{3}{\case{$\sbinop = \ssum$ and $\fremtrace{\svalue_2} \eeq \sint_0$ and $\fremtrace{\svalue_3} \eeq \sint_1$}}
    \begin{pfproof}
      \step{3.0}{$\ebinopt{\stoptional}{\svalue_2}{\svalue_3} \credA \sint_0 + \sint_1$}
        \begin{pfproof}
          by definition $\nredAS$, $\nredAD$, and $\sdeltaA$
        \end{pfproof}
      \step{3.1}{${\svalue_0} \eeq \sint_0$ and $\svalue_1 \eeq \sint_1$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\ebinopt{\stoptional}{\svalue_0}{\svalue_1} \credN \svalue_2 + \svalue_3$
        \end{pfproof}
    \end{pfproof}

  \step{4}{\case{$\sbinop = \squotient$ and $\svalue_0 = \sint_0$ and $\svalue_1 = \sint_1$ and $\sint_1 = 0$}}
    \begin{pfproof}
      \step{4.0}{$\ebinopt{\stoptional}{\svalue_0}{\svalue_1} \credN \tagerrorD$}
        \begin{pfproof}
          by definition $\nredNS$, $\nredND$, and $\sdeltaH$
        \end{pfproof}
      \step{4.1}{$\fremtrace{\svalue_2} \eeq \sint_0$ and $\fremtrace{\svalue_3} \eeq 0$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\ebinopt{\stoptional}{\svalue_2}{\svalue_3} \credA \tagerrorD$
        \end{pfproof}
    \end{pfproof}

  \step{5}{\case{$\sbinop = \squotient$ and $\fremtrace{\svalue_2} = \sint_2$ and $\fremtrace{\svalue_3} = \sint_3$ and $\sint_3 = 0$}}
    \begin{pfproof}
      \step{5.0}{$\ebinopt{\stoptional}{\svalue_2}{\svalue_3} \credA \tagerrorD$}
        \begin{pfproof}
          by definition $\nredAS$, $\nredAD$, and $\sdeltaA$
        \end{pfproof}
      \step{5.1}{$\svalue_0 \eeq \sint_2$ and $\svalue_1 \eeq 0$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\ebinopt{\stoptional}{\svalue_0}{\svalue_1} \credN \tagerrorD$
        \end{pfproof}
    \end{pfproof}

  \step{6}{\case{$\sbinop = \squotient$ and $\svalue_0 = \sint_0$ and $\svalue_1 = \sint_1$ and $\sint_1 \neq 0$}}
    \begin{pfproof}
      \step{6.0}{$\ebinopt{\stoptional}{\svalue_0}{\svalue_1} \credN {\floorof{\sint_0 / \sint_1}}$}
        \begin{pfproof}
          by definition $\nredNS$, $\nredND$, and $\sdeltaH$
        \end{pfproof}
      \step{6.1}{$\fremtrace{\svalue_2} \eeq \sint_0$ and $\fremtrace{\svalue_3} \eeq \sint_1$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\ebinopt{\stoptional}{\svalue_2}{\svalue_3} \credA {\floorof{\sint_0 / \sint_1}}$
        \end{pfproof}
    \end{pfproof}

  \step{7}{\case{$\sbinop = \squotient$ and $\fremtrace{\svalue_2} = \sint_2$ and $\fremtrace{\svalue_3} = \sint_3$ and $\sint_3 \neq 0$}}
    \begin{pfproof}
      \step{7.0}{$\ebinopt{\stoptional}{\svalue_2}{\svalue_3} \credA {\floorof{\sint_2 / \sint_3}}$}
        \begin{pfproof}
          by definition $\nredAS$, $\nredAD$, and $\sdeltaA$
        \end{pfproof}
      \step{7.1}{$\svalue_0 \eeq \sint_0$ and $\svalue_1 \eeq \sint_1$}
        \begin{pfproof}
          by inversion $\srexpr$
        \end{pfproof}
      \qedstep
        \begin{pfproof}
          $\ebinopt{\stoptional}{\svalue_0}{\svalue_1} \credN {\floorof{\sint_0 / \sint_1}}$
        \end{pfproof}
    \end{pfproof}

\end{lamportproof*}}

\begin{lemma}\label{HA-subst}
  If\/ $\rexpr{\sexpr_0}{\sexpr_1}$ and\/ $\rexpr{\svalue_0}{\svalue_1}$
  then\/ $\rexpr{\esubst{\sexpr_0}{\svar_0}{\svalue_0}}{\esubst{\sexpr_1}{\svar_0}{\svalue_1}}$
\end{lemma}{
  \newcommand{\shortpf}{By induction on the structure of both expressions (or rather, the pair $\epair{\sexpr_0}{\sexpr_1}$) via case analysis of $\rexpr{\sexpr_0}{\sexpr_1}$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf
\end{lamportproof*}}

\begin{lemma}\label{HA-hole-subst}
  If\/ $\rexpr{\sexpr_0}{\sexpr_1}$
  and\/ $\rctx{\ctx_0}{\ctx_1}$
  then\/ $\rexpr{\ctx_0[\sexpr_0]}{\ctx_1[\sexpr_1]}$
\end{lemma}{
  \newcommand{\shortpf}{By induction on the structure of $\ctx_0$.}
\begin{lamportproof*}
  \shortpf
\mainproof
  \shortpf
\end{lamportproof*}}