deletions | additions       diff --git a/subsubsection_ii_I_assume_that__.tex b/subsubsection_ii_I_assume_that__.tex  index 074557a..7379c3b 100644  --- a/subsubsection_ii_I_assume_that__.tex  +++ b/subsubsection_ii_I_assume_that__.tex 
...
Case $k -1 \Rightarrow k$: (pay attention to the parens in order to determine scope of the quantifiers)   Assume that, $\forall (r',m')$ s-reachable in at most $k$ steps from $(r,m)$, $(\I,r',m') \vDash \varphi$. (Else the statement holds vacuously.)   $\forall i \in S(r,m): \forall (r',m')$ s.t. $r_i(m) = r'_i(m'): \bigl($\footnote{(observe $i \in S(r,m)$ from initial quantification)} $(r',m')$ is 1 step away from $(r,m)$; we can immediately derive from our case assumption that $\forall (r'',m'')$ s-reachable in at most $k-1$ steps from $(r',m')$, $(\I,r',m') $(\I,r'',m'')  \vDash \varphi$. We can therefore use our inductive hypothesis to conclude $(\I,r',m') \vDash E^{k-1}_S \varphi \bigr )$. We observe that $\forall i \in S(r,m): \forall (r',m')$ s.t. $r_i(m) = r'_i(m'): (\I,r',m') \vDash E^{k-1}_S \varphi$ is just the statement $E^k_S \varphi$ expanded first by its definition, and second by the definition of $B^i_S$; thus $E^k_S \varphi$ holds.