From 477788abaa511c6b17e0330a082561f8f756f7d1 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 5 Apr 2020 09:30:01 -0400
Subject: [PATCH] Missed loop invariant in big-step semantics

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

diff --git a/frap_book.tex b/frap_book.tex
index 20d5a01..243dd7d 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -3251,7 +3251,7 @@ $$\infer{\bigstep{(h, v, \{I\} \while{b}{c})}{(h', v')}}{
   \denote{b}(h, v)
   & \bigstep{(h, v, c; \{I\} \while{b}{c})}{(h', v')}
 }
-\quad \infer{\bigstep{(h, v, \while{b}{c})}{(h, v)}}{
+\quad \infer{\bigstep{(h, v, \{I\} \while{b}{c})}{(h, v)}}{
   \neg \denote{b}(h, v)
 }$$