From c8052f2dc3999cb9707f640f5b807a8360af3e11 Mon Sep 17 00:00:00 2001 From: Yann Herklotz 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(-) 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