Remove proof

1 files changed, 4 insertions, 6 deletions

diff --git a/proof.tex b/proof.tex
index 9ad825f..1284458 100644
--- a/proof.tex
+++ b/proof.tex
@@ -12,13 +12,11 @@ The main correctness theorem is the exact same correctness theorem as stated in
   \end{equation*}
 \end{theorem}
 
-\begin{proof}
-  The first observation that should be made is that instead of proving the backwards simulation, we can prove the forwards simulation, followed by a proof that the target semantics of the translation, which in our case is Verilog, is deterministic.  This means that there is only one possible behaviour $B$ for $V$, and that therefore the backwards simulation holds as well.
+To prove this the first observation that should be made is that instead of proving the backwards simulation, we can prove the forwards simulation, followed by a proof that the target semantics of the translation, which in our case is Verilog, is deterministic.  This means that there is only one possible behaviour $B$ for $V$, and that therefore the backwards simulation holds as well.
 
-  The second observation that needs to be made is that to prove the forward simulation, it suffices to prove the forward simulations between each intermediate language, as they can be composed to prove the correctness of the whole HLS tool.
+The second observation that needs to be made is that to prove the forward simulation, it suffices to prove the forward simulations between each intermediate language, as they can be composed to prove the correctness of the whole HLS tool.
 
-  The forward simulation between 3AC and HTL is proven in Lemma~\ref{lemma:htl}, next the forward simulation between HTL and Verilog is shown in Lemma~\ref{lemma:verilog} and finally, the proof that Verilog is deterministic is given in Lemma~\ref{lemma:deterministic}.
-\end{proof}
+The forward simulation between 3AC and HTL is proven in Lemma~\ref{lemma:htl}, next the forward simulation between HTL and Verilog is shown in Lemma~\ref{lemma:verilog} and finally, the proof that Verilog is deterministic is given in Lemma~\ref{lemma:deterministic}.
 
 \subsection{Forward simulation between 3AC and HTL}\label{sec:proof:3ac_htl}
 
@@ -65,7 +63,7 @@ To simplify the proof, instead of using the translation algorithm as an assumpti
 The first step in proving the forward simulation is to define a relation that matches an 3AC state to an HTL state, which shows when the states are equivalent.  This relation also defines assumptions that are made about the 3AC code that we receive, so that these assumptions can be used to prove the translations correct.  These assumptions then have to be proven to always hold assuming the HTL code was created by the translation algorithm.  Some of these assertions that need to be made about the 3AC and HTL code for a state to match are:
 
 \begin{itemize}
-  \item the 3AC register file $R \le \Gamma_{r}$ needs to be ``less defined'' than the HTL register map $\Gamma_{r}$ and the RAM values represented by a Verilog array in $\Gamma_{a}$ need to match the 3AC function's stack contents, which are part of the memory $M$: $M \le \Gamma_{a}$,
+  \item the 3AC register file $R \le \Gamma_{r}$ needs to be ``less defined'' than the HTL register map $\Gamma_{r}$, meaning all entries should be  and the RAM values represented by a Verilog array in $\Gamma_{a}$ need to match the 3AC function's stack contents, which are part of the memory $M$: $M \le \Gamma_{a}$,
   \item the state is well formed, meaning the value of the state register matches the current value of the program counter: $\textit{pc} = \Gamma_{r}!\sigma$,
 \end{itemize}