From ccd1f59d576df32128508842caebcebd705ef3b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Thu, 27 May 2021 00:50:09 +0100
Subject: [PATCH] WIP

---
 thesis.tex | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/thesis.tex b/thesis.tex
index 7b23386..2dd203c 100644
--- a/thesis.tex
+++ b/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}