From 24ffd784521e5721a49746d0be12e6f72ba53106 Mon Sep 17 00:00:00 2001
From: John Wickerson <j.wickerson@imperial.ac.uk>
Date: Mon, 13 Sep 2021 08:33:19 +0000
Subject: Update on Overleaf.

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

(limited to 'proof.tex')

diff --git a/proof.tex b/proof.tex
index e94266c..36794bd 100644
--- a/proof.tex
+++ b/proof.tex
@@ -159,7 +159,7 @@ A similar specification is created for the load.  We then also prove that the im
 
 \subsubsection{From Specification to Simulation}
 
-Another simulation proof is performed to prove that the insertion of the RAM is semantics preserving.  As in the simulation proof shown in Lemma~\ref{lemma:simulation_diagram}, some invariants need to be defined, which always hold at the start of the simulation and at the end of the simulation.  The invariants needed for the simulation of the RAM insertion are quite different to the previous invariants, so we can define these invariants $\mathcal{I}_{r}$ to be the following:
+Another simulation proof is performed to prove that the insertion of the RAM is semantics preserving.  As in Lemma~\ref{lemma:simulation_diagram}, we require some invariants that always hold at the start and end of the simulation.  The invariants needed for the simulation of the RAM insertion are quite different to the previous ones, so we can define these invariants $\mathcal{I}_{r}$ to be the following:
 
 \begin{itemize}
   \item The association map for arrays $\Gamma_{a}$ always needs to have the same arrays present, and these arrays should never change in size.
-- 
cgit 

