More uniformness in the formulas

1 files changed, 3 insertions, 3 deletions

diff --git a/proof.tex b/proof.tex
index 73cd1dc..6a44ed6 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}, \yhfunction{tr\_ram}(h) = h' \land h \Downarrow B \implies h' \Downarrow B.
+    &\forall\ h\ B, B \in \texttt{Safe} \land \yhfunction{tr\_ram}(h) = h' \land h \Downarrow B \implies h' \Downarrow B.
   \end{align*}
 \end{lemma}
 
@@ -183,7 +183,7 @@ The HTL-to-Verilog simulation is conceptually simple, as the only transformation
 \begin{lemma}[Forward simulation from HTL to Verilog]\label{lemma:verilog}
   We write $\yhfunction{tr\_verilog}$ for the translation from HTL to Verilog. (Note that this translation cannot fail, so we do not need the \yhconstant{OK} constructor here.)
   \begin{align*}
-    &\forall h, V, B \in \texttt{Safe}, \yhfunction{tr\_verilog} (h) = V \land h \Downarrow B \implies V \Downarrow B.
+    &\forall\ h\ V\ B, B \in \texttt{Safe} \land \yhfunction{tr\_verilog} (h) = V \land h \Downarrow B \implies V \Downarrow B.
   \end{align*}
 \end{lemma}
 
@@ -202,7 +202,7 @@ The final lemma we need is that the Verilog we generate is deterministic. This r
   If a Verilog program $V$ admits both behaviours $B_1$ and $B_2$, then $B_1$ and $B_2$ must be the same.
 
   \begin{equation*}
-    \forall V, B_{1}, B_{2}, V \Downarrow B_{1} \land V \Downarrow B_{2} \implies B_{1} = B_{2}.
+    \forall\ V\ B_{1}\ B_{2}, V \Downarrow B_{1} \land V \Downarrow B_{2} \implies B_{1} = B_{2}.
   \end{equation*}
 \end{lemma}