From 8c67fc54681d40ab2c4bfe6c3497f29c2d8718d3 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Fri, 29 Apr 2016 17:37:17 -0400
Subject: [PATCH] ConcurrentSeparationLogic chapter: proofreading

---
 frap_book.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/frap_book.tex b/frap_book.tex
index a53040d..d0c4cfd 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -3983,7 +3983,7 @@ Two lemmas express crucial techniques to isolate elements within iterated conjun
 \end{proof}
 
 \begin{lemma}\label{cslinvariant}
-  If $\hoare{P}{c}{Q}$, and if a heap $h$ satisfies the predicate $(P * \bigstar{\ell}{L}{\mathcal I(\ell)})$, then an invariant of the system starting at state $(h, \emptyset, c)$ is: for reachable state $(h', l', c')$, there exists $P'$ where $\hoare{P'}{c'}{Q}$, such that $h'$ satisfies $(P' * \bigstar{\ell}{L}{\guarded{\ell \notin L}{\mathcal I(\ell)}})$.
+  If $\hoare{P}{c}{Q}$, and if a heap $h$ satisfies the predicate $(P * \bigstar{\ell}{L}{\mathcal I(\ell)})$, then an invariant of the system starting at state $(h, \emptyset, c)$ is: for reachable state $(h', l', c')$, there exists $P'$ where $\hoare{P'}{c'}{Q}$, such that $h'$ satisfies $(P' * \bigstarp{\ell}{L}{\guarded{\ell \notin l'}{\mathcal I(\ell)}})$.
 \end{lemma}
 \begin{proof}
   By invariant induction\index{invariant induction}, using Lemma \ref{nonelocked} for the base case and Lemma \ref{cslpreservation} for the induction step, the latter with $R = \emp$.
@@ -3996,7 +3996,7 @@ Two lemmas express crucial techniques to isolate elements within iterated conjun
   By induction on the derivation of $\hoare{P}{c}{Q}$.
 \end{proof}
 
-The overall soundness proof proceeds by invariant weakening\index{invariant weakening} to the invariant established by Lemma \ref{cslinvariant}.
+The overall soundness proof proceeds by invariant weakening\index{invariant weakening} with the invariant established by Lemma \ref{cslinvariant}.
 We prove the inclusion of new invariant in old by Lemma \ref{cslprogress}.