|
|
@ -14598,7 +14598,7 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$. |
|
|
$N' \approxa \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ as |
|
|
$N' \approxa \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ as |
|
|
desired. |
|
|
desired. |
|
|
\item Inductive step: Assume $admin(\EC')$ and |
|
|
\item Inductive step: Assume $admin(\EC')$ and |
|
|
$M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. |
|
|
|
|
|
|
|
|
$M' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. |
|
|
\end{enumerate} |
|
|
\end{enumerate} |
|
|
\end{proof} |
|
|
\end{proof} |
|
|
% \begin{proof} |
|
|
% \begin{proof} |
|
|
|