WIP

thesis.tex

@@ -14545,7 +14545,7 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
     %
     \begin{derivation}
     & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
-    =\reducesto^\ast& \reason{\semlab{Op} ($\ell \notin \BL(\sdtrans{\EC})$), $2\times$\semlab{Let},\semlab{Split},\semlab{App}, Lemma~\ref{lem:sdtrans-subst}}\\
+    =\reducesto^+& \reason{\semlab{Op} ($\ell \notin \BL(\sdtrans{\EC})$), $2\times$\semlab{Let},\semlab{Split},\semlab{App}, Lemma~\ref{lem:sdtrans-subst}}\\
    &\sdtrans{N_\ell[\lambda x.
              \bl
              \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
@@ -14588,9 +14588,16 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
   \sdtrans{\EC}[\Return\;W]$.
 
   \item Inductive step: Assume $M' \reducesto M''$ and
-    $M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Take $N' = M''$ then by the induction hypothesis $M' \reducesto N'$
-
-  \item Inductive step: Assume $admin(\EC)$ and
+    $M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Using a similar argument to above we get that
+    \[
+      \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}
+      \reducesto^+ \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}.
+    \]
+    Take $N' = M''$ then by the first induction hypothesis
+    $M' \reducesto N'$ and by the second induction hypothesis
+    $N' \approxa \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ as
+    desired.
+  \item Inductive step: Assume $admin(\EC')$ and
     $M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$.
   \end{enumerate}
 \end{proof}