deletions | additions       diff --git a/subsubsection_ii_I_assume_that__.tex b/subsubsection_ii_I_assume_that__.tex  index c5e41d7..138db3b 100644  --- a/subsubsection_ii_I_assume_that__.tex  +++ b/subsubsection_ii_I_assume_that__.tex 
...
I assume that S is non-empty at $(r,m)$; when S is empty at $(r,m)$, $C_S \varphi$ hold vacuously, and (as "S-reachable" is now an empty set) the other half of our iff statement also holds vacuously.   Other direction. I start by proving a related lemma. Lemma: if there exists some $(r',m')$ $\forall (r',m')$  s.t. $(\I,r',m') \vDash\neg  \varphi$ S-reachable from $(r,s)$ in $k$ steps, then $(\I,r,m) \vDash \neg E^k_S \varphi$. Case $k = 0$: $\forall \varphi$ s.t.  $(\I,r,m) \vDash \neg\varphi$, as \varphi$,  all states reachable from some state s in 0 steps are simply that state $s$. $s$; thus our "if-test" clause holds.  We observe that $E_S^0 \varphi \Leftrightarrow \varphi$ by definition; thus $(\I,r,m) \vDash \neg E_S^0 \varphi$ \varphi$.  Case $k -1 \Rightarrow k$: (pay attention to the parens in order to determine scope of the quantifiers)