From 099d8e47dfaab5bd1f3995fb663354430e4bd0b7 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 13 Sep 2021 09:56:14 +0100
Subject: Remove space

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

(limited to 'proof.tex')

diff --git a/proof.tex b/proof.tex
index 529d229..66197dc 100644
--- a/proof.tex
+++ b/proof.tex
@@ -52,7 +52,7 @@ As HTL is quite far removed from 3AC, this first translation is the most involve
   \end{equation*}
 \end{lemma}
 
-\begin{proof}[Proof sketch] 
+\begin{proof}[Proof sketch]
   We prove this lemma by first establishing a specification of the translation function $\yhfunction{tr\_htl}$ that captures its important properties, and then splitting the proof into two parts: one to show that the translation function does indeed meet its specification, and one to show that the specification implies the desired simulation result. This strategy is in keeping with standard \compcert{} practice. % The forward simulation is then proven by showing that the initial states and final states between the 3AC semantics and HTL semantics match, and then showing that the simulation diagram in Lemma~\ref{lemma:simulation_diagram} holds.
 \end{proof}
 
-- 
cgit 

