From ee4aec520b5af5d8efe1b8bc9feb6cc4f02e2c46 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 11 Oct 2016 14:36:26 -0400 Subject: [PATCH] Correct definition of reachability --- frap_book.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frap_book.tex b/frap_book.tex index 8cceb88..0ae35f3 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -1085,7 +1085,7 @@ There we have $\to^2\ns(S_0)$, $\to^3\ns(S_0)$, and $\to^4\ns(S_0$). It follows that the set of states reachable after $n$ steps is: \begin{eqnarray*} - \mathsf{reach}(n) &=& \bigcup_{i < n} \to^i\ns(S_0) + \mathsf{reach}(n) &=& \bigcup_{i \leq n} \to^i\ns(S_0) \end{eqnarray*} This iteration process is not obviously executable yet, because, a priori, we seem to need to consider all possible $n$ values, to characterize the state space fully.