diff options
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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},\quad \yhfunction{tr\_ram\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B. + \forall h, h', B \in \texttt{Safe},\quad \yhfunction{tr\_ram\_ins}(h) = h' \land h \Downarrow B \implies h' \Downarrow B. \end{align*} \end{lemma} |