From eba6dc15d2f0cf26fc7a323658a8d57d5f288640 Mon Sep 17 00:00:00 2001
From: WZY <ziyao.wei.wzy@gmail.com>
Date: Wed, 9 Mar 2016 11:02:24 -0500
Subject: [PATCH] Typo - invariant should be AnswerIs(n_0!)

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

diff --git a/frap_book.tex b/frap_book.tex
index bd383c4..dc23a50 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -873,7 +873,7 @@ Another important property of invariants formalizes the connection with weakenin
 \end{theorem}
 
 Note that the larger $I'$ above may not be suitable to use in an inductive proof by Theorem \ref{invariant_induction}!
-For instance, for factorial, we might define $I' = \mathcal \{\mathsf{AnswerIs}(n_0)\} \cup \{\mathsf{WithAccumulator}(n, a) \mid n, a \in \mathbb N\}$, clearly a superset of $I$.
+For instance, for factorial, we might define $I' = \mathcal \{\mathsf{AnswerIs}(n_0!)\} \cup \{\mathsf{WithAccumulator}(n, a) \mid n, a \in \mathbb N\}$, clearly a superset of $I$.
 However, by forgetting everything that we know about intermediate $\mathsf{WithAccumulator}$ states, we will get stuck on the inductive step of the proof.
 Thus, what we call invariants here needn't also be \emph{inductive invariants}\index{inductive invariants}, and there may be slight terminology mismatches with other sources.