Update on Overleaf.

1 files changed, 5 insertions, 5 deletions

diff --git a/proof.tex b/proof.tex
index 36794bd..e54a9af 100644
--- a/proof.tex
+++ b/proof.tex
@@ -163,13 +163,13 @@ Another simulation proof is performed to prove that the insertion of the RAM is
 
 \begin{itemize}
   \item The association map for arrays $\Gamma_{a}$ always needs to have the same arrays present, and these arrays should never change in size.
-  \item The RAM should always be disabled at the start of the simulation, and at the end of the simulation step.  This is the reason for why the self-disabling RAM was needed.
+  \item The RAM should always be disabled at the start and the end of each simulation step. (This is why self-disabling RAM is needed.)
 \end{itemize}
 
-The other invariants and assumptions for defining two matching states in HTL are quite similar to the simulation performed in Lemma~\ref{lemma:simulation_diagram}, such as ensuring that the states have the same value, and that the values in the registers are less-defined.  In particular, the less-defined relation matches up all the registers, except for the new registers introduced by the RAM.
+The other invariants and assumptions for defining two matching states in HTL are quite similar to the simulation performed in Lemma~\ref{lemma:simulation_diagram}, such as ensuring that the states have the same value, and that the values in the registers are less defined.  In particular, the less defined relation matches up all the registers, except for the new registers introduced by the RAM.
 
 \begin{lemma}[Forward simulation from HTL to HTL after inserting the RAM]\label{lemma:htl_ram}
-  Given an HTL program, the forward simulation relation should hold after inserting the RAM and wiring the load, store and control signals.
+  Given an HTL program, the forward-simulation relation should hold after inserting the RAM and wiring the load, store, and control signals.
 
   \begin{align*}
     \forall h, h', B \in \texttt{Safe},\quad \yhfunction{tr\_ram\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B.
@@ -178,7 +178,7 @@ The other invariants and assumptions for defining two matching states in HTL are
 
 \subsection{Forward Simulation from HTL to Verilog}\label{sec:proof:htl_verilog}
 
-The HTL-to-Verilog simulation is conceptually simple, as the only transformation is from the map representation of the code to the case-statement representation.  The proof is more involved, as the semantics of a map structure are quite different to the semantics of the case-statement they are converted to.
+The HTL-to-Verilog simulation is conceptually simple, as the only transformation is from the map representation of the code to the case-statement representation.  The proof is more involved, as the semantics of a map structure is quite different to that of the case-statement to which it is converted.
 
 %\YH{Maybe want to split this up into two lemmas?  One which states the proof about the map property of uniqueness of keys, and another proving the final theorem?}
 \begin{lemma}[Forward simulation from HTL to Verilog]\label{lemma:verilog}
@@ -189,7 +189,7 @@ The HTL-to-Verilog simulation is conceptually simple, as the only transformation
 \end{lemma}
 
 \begin{proof}[Proof sketch]
-  The translation from maps to case-statements is done by turning each node of the tree into a case-expression with the statements in each being the same.  The main difficulty for the proof is that a random-access structure is transformed into an inductive structure where a certain number of constructors need to be called to get to the correct case. 
+  The translation from maps to case-statements is done by turning each node of the tree into a case-expression containing the same statements.  The main difficulty is that a random-access structure is being transformed into an inductive structure where a certain number of constructors need to be called to get to the correct case. 
   %\JW{I would chop from here.}\YH{Looks good to me.}
   %The proof of the translation from maps to case-statements follows by induction over the list of elements in the map and the fact that each key will be unique.  In addition to that, the statement that is currently being evaluated is guaranteed by the correctness of the list of elements to be in that list.  The latter fact therefore eliminates the base case, as an empty list does not contain the element we know is in the list.  The other two cases follow by the fact that either the key is equal to the evaluated value of the case expression, or it isn't.  In the first case we can then evaluate the statement and get the state after the case expression, as the uniqueness of the key tells us that the key cannot show up in the list anymore.  In the other case we can just apply the inductive hypothesis and remove the current case from the case statement, as it did not match.
 \end{proof}