From c8052f2dc3999cb9707f640f5b807a8360af3e11 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 10 Sep 2021 16:40:58 +0100
Subject: More uniformness in the formulas

---
 proof.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'proof.tex')

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}
 
-- 
cgit 

