deletions | additions       diff --git a/subsection_b_This_follows_immediately__.tex b/subsection_b_This_follows_immediately__.tex  index 26ac534..afc36df 100644  --- a/subsection_b_This_follows_immediately__.tex  +++ b/subsection_b_This_follows_immediately__.tex 
...
\subsection*{b}  This follows immediately from part $a$. In run $r_1$ at the decision-time $m$ we have that $(\I,r_1,m) \vDash i \in \N \wedge deciding_\N(0)$; $i \in \N$ by assumption, and $deciding_\N(0)$ as argued in that section. We do not, however, have $K_i deciding_\N(0)$ - $(\I,r_1,m) \not\vDash K_i deciding_\N(0)$ - because $r_{1i}(m) = r_{2i}(m)$, and $(\I,r_2,m) \vDash deciding_\N(1)$. So we cannot satisfy the conditions of $K_i$. We do, however, have $(\I,r_1,m) \vDash B^\N_i deciding_\N(0)$; as $P$ is deterministic, all points $(r',m')$ in which $r_1i(m) = r'_i('m)$ must have $i$ take the same action, which in this case is decide 0. Furthermore, as $P$ is correct, all runs in which $i \in \N$ must have $i$ decide on the correct value. The combination of these two constraints - that $i$ is correct and that $(r',m')$ is locally-indistinguishable from $(r_1,m)$ to $i$ - are the requirements for belief. Thus $(\I,r_1,m) \vDash (i \in \N \wedge deciding_\N(0)) \RightarrowB^\N_i \Rightarrow B^\N_i  deciding_\N(0)$.