Fix variable in proof

1 files changed, 1 insertions, 1 deletions

diff --git a/proof.tex b/proof.tex
index 3499b4e..41e01c6 100644
--- a/proof.tex
+++ b/proof.tex
@@ -27,7 +27,7 @@ The main correctness theorem is analogous to that stated in \compcert{}~\cite{le
 %The following `backwards simulation' theorem describes the correctness theorem, where $\Downarrow$ stands for simulation and execution respectively.
 
 \begin{theorem}
-  Whenever the translation from $C$ succeeds and produces Verilog $V$, and all observable behaviours of $C$ are safe (i.e. $\mathit{Safe} (C)$ is defined as $\forall B,\ S \Downarrow B \implies B \in \texttt{Safe}$) then $V$ has behaviour $B$ only if $C$ has behaviour $B$.
+  Whenever the translation from $C$ succeeds and produces Verilog $V$, and all observable behaviours of $C$ are safe (i.e. $\mathit{Safe} (C)$ is defined as $\forall B,\ C \Downarrow B \implies B \in \texttt{Safe}$) then $V$ has behaviour $B$ only if $C$ has behaviour $B$.
   \begin{equation*}
     \forall C, V, B,\quad \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land \mathit{Safe}(C) \implies (V \Downarrow B \implies C \Downarrow B).
   \end{equation*}