summaryrefslogtreecommitdiffstats
path: root/proof.tex
diff options
context:
space:
mode:
Diffstat (limited to 'proof.tex')
-rw-r--r--proof.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/proof.tex b/proof.tex
index 6749482..5f7dc16 100644
--- a/proof.tex
+++ b/proof.tex
@@ -147,7 +147,7 @@ Another simulation proof is performed to prove that the insertion of the RAM is
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}\label{lemma:simulation_diagram_ram}
+%\begin{lemma}\label{lemma:simulation_diagram_ram}
\subsection{Forward simulation from HTL to Verilog}\label{sec:proof:htl_verilog}