Update on Overleaf.

1 files changed, 1 insertions, 1 deletions

diff --git a/proof.tex b/proof.tex
index 86e20de..9ad825f 100644
--- a/proof.tex
+++ b/proof.tex
@@ -33,7 +33,7 @@ As HTL is quite different to 3AC, this first translation is the most involved an
 \end{lemma}
 
 \begin{proof}
-  Follows by using a specification of the important properties $\yhfunction{tr\_htl}}$ which can be used as an assumption in the proof instead.  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.
+  Follows by using a specification of the important properties $\yhfunction{tr\_htl}$ which can be used as an assumption in the proof instead.  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}
 
 \subsubsection{Specification}\label{sec:proof:3ac_htl:specification}