Some formula fixes

1 files changed, 7 insertions, 7 deletions

diff --git a/proof.tex b/proof.tex
index 4f58746..63200c1 100644
--- a/proof.tex
+++ b/proof.tex
@@ -29,7 +29,7 @@ The main correctness theorem is analogous to that stated in \compcert{}~\cite{le
 \begin{theorem}
   For any safe behaviour $B$, whenever the translation from $C$ succeeds and produces Verilog $V$, then $V$ has behaviour $B$ only if $C$ has behaviour $B$.
   \begin{equation*}
-    \forall C, V, B \in \texttt{Safe},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow B \implies C \Downarrow B.
+    \forall\ C\ V\ B, B \in \texttt{Safe} \land \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow B \implies C \Downarrow B.
   \end{equation*}
 \end{theorem}
 
@@ -47,7 +47,7 @@ As HTL is quite far removed from 3AC, this first translation is the most involve
 \begin{lemma}[Forward simulation from 3AC to HTL]\label{lemma:htl}
   We write \texttt{tr\_htl} for the translation from 3AC to HTL.
   \begin{equation*}
-    \forall c, h, B \in \texttt{Safe}, \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B.
+    \forall\ c\ h\ B, B \in \texttt{Safe} \land \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B.
   \end{equation*}
 \end{lemma}
 
@@ -58,12 +58,12 @@ We prove this lemma by first establishing a specification of the translation fun
 %To simplify the proof, instead of using the translation algorithm as an assumption, as was done in Lemma~\ref{lemma:htl}, a specification of the translation can be constructed instead which contains all the properties that are needed to prove the correctness.  For example, for the translation from 3AC to HTL, 
 The specification for the translation of 3AC instructions into HTL data-path and control logic can be defined by the following predicate:
 \begin{equation*}
-  \yhfunction{spec\_instr } \mathit{fin }\ \mathit{ret }\ \sigma\ \mathit{stk }\ i\ \mathit{data }\ \mathit{control}
+  \yhfunction{spec\_instr}\ \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ i\ \mathit{data}\ \mathit{control}
 \end{equation*}
 
 \noindent Here, the $\mathit{control}$ and $\mathit{data}$ parameters are the statements that the current 3AC instruction $i$ should translate to. The other parameters are the special registers defined in Section~\ref{sec:verilog:integrating}. An example of a rule describing the translation of an arithmetic/logical operation from 3AC is the following:
 \begin{equation*}
-  \inferrule[Iop]{\yhfunction{tr\_op } \mathit{op }\ \vec{a} = \yhconstant{OK } e}{\yhfunction{spec\_instr } \mathit{fin }\ \mathit{ret }\ \sigma\ \mathit{stk }\ (\yhconstant{Iop } \mathit{op }\ \vec{a}\ d\ n)\ (d\ \yhkeyword{<=}\ e)\ (\sigma\ \yhkeyword{<=}\ n)}
+  \inferrule[Iop]{\yhfunction{tr\_op}\ \mathit{op}\ \vec{a} = \yhconstant{OK}\ e}{\yhfunction{spec\_instr}\ \mathit{fin}\ \mathit{ret}\ \sigma\ \mathit{stk}\ (\yhconstant{Iop}\ \mathit{op}\ \vec{a}\ d\ n)\ (d\ \yhkeyword{<=}\ e)\ (\sigma\ \yhkeyword{<=}\ n)}
 \end{equation*}
 
 \noindent Assuming that the translation of the operator $\mathit{op}$ with operands $\vec{a}$ is successful and results in expression $e$, the rule describes how the destination register $d$ is updated to $e$ via a non-blocking assignment in the data path, and how the program counter $\sigma$ is updated to point to the next CFG node $n$ via another non-blocking assignment in the control logic.
@@ -73,7 +73,7 @@ In the following lemma, $\yhfunction{spec\_htl}$ is the top-level specification
 \begin{lemma}\label{lemma:specification}
   If a 3AC program $c$ is translated correctly to an HTL program $h$, then the specification of the translation holds.
   \begin{equation*}
-    \forall\ c\ h,\ \yhfunction{tr\_htl} (c) = \yhconstant{OK}(h) \implies \yhfunction{spec\_htl}\ c\ h.
+    \forall\ c\ h, \yhfunction{tr\_htl} (c) = \yhconstant{OK}(h) \implies \yhfunction{spec\_htl}\ c\ h.
   \end{equation*}
 \end{lemma}
 
@@ -110,9 +110,9 @@ We can now define the simulation diagram for the translation. The 3AC state can
     \begin{tikzpicture}
       \begin{scope}
         \node[circle] (s1) at (0,1.5) {$R, M, \mathit{pc}$};
-        \node[circle] (r1) at (7.2,1.5) {$\Gamma_{r}, \Gamma_{a}$};
+        \node[circle] (r1) at (8.5,1.5) {$\Gamma_{r}, \Gamma_{a}$};
         \node[circle] (s2) at (0,0) {$R', M', \mathit{pc}'$};
-        \node[circle] (r2) at (7.2,0) {$\Gamma_{r}', \Gamma_{a}'$};
+        \node[circle] (r2) at (8.5,0) {$\Gamma_{r}', \Gamma_{a}'$};
         %\node at (6.8,0.75) {+};
         \draw (s1) -- node[above] {$\mathcal{I} \land (R \le \Gamma_{r}) \land (M \le \Gamma_{a}) \land (\mathit{pc} = \Gamma_{r}[\sigma])$} ++ (r1);
         \draw[-{Latex}] ($(s1.south) + (0,0.4)$) -- ($(s2.north) - (0,0.4)$);