Add missing variable in proof

2 files changed, 3 insertions, 3 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 6282664..930ce00 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -121,7 +121,7 @@ endmodule
       \node[draw,circle,inner sep=6pt] (s0) at (0,0) {$S_{\mathit{start}} / \texttt{x}$};
       \node[draw,circle,inner sep=8pt] (s1) at (1.5,-3) {$S_{0} / \texttt{1}$};
       \node[draw,circle,inner sep=8pt] (s2) at (3,0) {$S_{1} / \texttt{1}$};
-      \node (s2s) at ($(s2.west) + (-0.3,1)$) {\texttt{x0}};
+      \node (s2s) at ($(s2.west) + (-0.3,1)$) {\texttt{00}};
       \node (s2ss) at ($(s2.east) + (0.3,1)$) {\texttt{1x}};
       \draw[-{Latex[length=2mm,width=1.4mm]}] ($(s0.west) + (-0.3,1)$) to [out=0,in=120] (s0);
       \draw[-{Latex[length=2mm,width=1.4mm]}] (s0)
@@ -137,7 +137,7 @@ endmodule
     \end{tikzpicture}
   \end{subfigure}
   \Description{Verilog code of a state machine, and its equivalent state machine diagram.}
-  \caption{A simple state machine implemented in Verilog, with its diagrammatic representation on the right. The x's stand for don't cares and each transition is labelled with the values of the inputs \texttt{rst} and \texttt{y} that trigger the transition.  The output that will be produced is shown in each state.}%
+  \caption{A simple state machine implemented in Verilog, with its diagrammatic representation on the right. The \texttt{x} stands for ``don't care'' and each transition is labelled with the values of the inputs \texttt{rst} and \texttt{y} that trigger the transition.  The output that will be produced is shown in each state.}%
   \label{fig:tutorial:state_machine}
 \end{figure}
 
diff --git a/proof.tex b/proof.tex
index 5caa382..9a192c6 100644
--- a/proof.tex
+++ b/proof.tex
@@ -171,7 +171,7 @@ The other invariants and assumptions for defining two matching states in HTL are
   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, B \in \texttt{Safe},\quad \yhfunction{tr\_ram\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B.
+    \forall h, h', B \in \texttt{Safe},\quad \yhfunction{tr\_ram\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B.
   \end{align*}
 \end{lemma}