dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 11:08:25 +00:00
Code Issues Releases Wiki Activity

Remove redundant 'Proof's

Browse Source
This commit is contained in:
Daniel Hillerström
2020-09-16 23:22:25 +01:00
parent 63cfd44374
commit 381a43444c
1 changed files with 8 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
thesis.tex
View File

@@ -1340,7 +1340,7 @@ realisable function in \BCalc{} is effect-free and total.
\end{theorem} \end{theorem}
% %
\begin{proof} \begin{proof}
Proof by induction on typing derivations. By induction on typing derivations.
\end{proof} \end{proof}
% %
% \begin{corollary} % \begin{corollary}
@@ -1357,7 +1357,7 @@ some other computation $M'$, then $M'$ is also well typed.
\end{theorem} \end{theorem}
% %
\begin{proof} \begin{proof}
Proof by induction on typing derivations. By induction on typing derivations.
\end{proof} \end{proof}
\section{A primitive effect: recursion} \section{A primitive effect: recursion}
@@ -3038,8 +3038,8 @@ CPS translation commutes with substitution.
\end{lemma} \end{lemma}
% %
\begin{proof} \begin{proof}
Proof is by mutual induction on the structure of $W$, $M$, $\hret$, By mutual induction on the structure of $W$, $M$, $\hret$, and
and $\hops$. $\hops$.
\end{proof} \end{proof}
% %
It follows as a corollary that top-level substitution is well-behaved. It follows as a corollary that top-level substitution is well-behaved.
@@ -3088,7 +3088,7 @@ context.
\end{lemma} \end{lemma}
% %
\begin{proof} \begin{proof}
Proof by structural induction on the evaluation context $\EC$. By structural induction on the evaluation context $\EC$.
\end{proof} \end{proof}
% %
Even though we have eliminated the static administrative redexes, we Even though we have eliminated the static administrative redexes, we
@@ -3126,7 +3126,7 @@ reductions, i.e.
\end{lemma} \end{lemma}
% %
\begin{proof} \begin{proof}
Proof is by induction on the structure of $M$. By induction on the structure of $M$.
\end{proof} \end{proof}
% %
We next observe that the CPS translation simulates forwarding. We next observe that the CPS translation simulates forwarding.
@@ -3144,7 +3144,7 @@ If $\ell \notin dom(H_1)$ then
\end{lemma} \end{lemma}
% %
\begin{proof} \begin{proof}
Proof by direct calculation. By direct calculation.
\end{proof} \end{proof}
% %
Now we show that the translation simulates the \semlab{Op} Now we show that the translation simulates the \semlab{Op}
@@ -3179,7 +3179,7 @@ If $M \reducesto N$ then $\pcps{M} \reducesto^+ \areducesto^* \pcps{N}$.
\end{theorem} \end{theorem}
% %
\begin{proof} \begin{proof}
Proof is by case analysis on the reduction relation using Lemmas By case analysis on the reduction relation using Lemmas
\ref{lem:decomposition}--\ref{lem:handle-op}. The \semlab{Op} case \ref{lem:decomposition}--\ref{lem:handle-op}. The \semlab{Op} case
follows from Lemma~\ref{lem:handle-op}. follows from Lemma~\ref{lem:handle-op}.
\end{proof} \end{proof}