From 34f1cfc20a999cb4937a00d335ad0fee75d65760 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 12 Sep 2021 20:50:14 +0100
Subject: Add missing variable in proof

---
 proof.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proof.tex')

diff --git a/proof.tex b/proof.tex
index 5caa382..9a192c6 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},\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}
 
-- 
cgit