From 2efec7b61da67ccb49af93697fc4e9266d044678 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Tue, 14 Apr 2020 11:55:26 -0400
Subject: [PATCH] Typo fix

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

diff --git a/frap_book.tex b/frap_book.tex
index 9f9e7ec..86b7800 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -4168,7 +4168,7 @@ This result can be composed with soundness of any Hoare logic for the source lan
 The associated Coq code defines one, essentially following our separation logic\index{separation logic} from last chapter.
 
 \begin{theorem}
-  If $\hoare{P}{c}{Q}$, $P(h)$, $\dscomp{v}{c}{s}$, and $\texttt{result} \notin \dom{v}$, then it is invariant of the transition system starting in $(h, v, s)$ that execution never gets stuck.
+  If $\hoare{P}{c}{Q}$, $P(h)$, $\dscomp{v}{c}{s}$, and $\texttt{result} \notin \dom{v}$, then it is an invariant of the transition system starting in $(h, v, s)$ that execution never gets stuck.
 \end{theorem}
 \begin{proof}
   First, we switch to proving an invariant of the system $(h, c)$ using the simulation from Theorem \ref{dscompsim}.