deletions | additions       diff --git a/section_6_23_We_describe__.tex b/section_6_23_We_describe__.tex  index 8463ee4..8afc958 100644  --- a/section_6_23_We_describe__.tex  +++ b/section_6_23_We_describe__.tex 
...
We prove first that for an arbitrary $k$, $\forall r \in \I^{rom}: (\I,r,1) \vDash E^k_\NS \exists 0 \vee E^k_\N \exists 1$. We show this by induction.  Base case: k = 0. We recall again that the definition of $E_0_S \varphi$ is simply $\varphi$; As we have $ \I \vDash 0 \wedge \vee  1$ as an axiom in SBA between 0 and 1, we can easily see that $\I \vDash E^0_\N 0 \wedge \vee  E^0_\N 1$ follows by definition. Other base case, just in case we don't like the definition of $E^0$: k = 1. As before, we quantify based on the definition of $E^k_\N$: $\forall r \in \I^{rom}: \forall i \in \N(r,1): \forall (r',m')$ s.t. $r_i(1) = r'_i(m'): \bigl($ Observe that $m'$ must not be 0, as 1 and $m'$ states are locally-indistinguishable, messages were sent in round 0, and (as we are quantifying over only non-faulty nodes) those messages sent in round 0 must have been received and recorded in local state. By round 1  $i$ received some message; thus $(\I,r',m') \vDash received_i(0) \vee received_i(1)$. It is clear that $received_i(y) \Rightarrow \exists y$, as our fault-model does not permit lying \footnote{except in cases where the protocol explicitly stipulates it, in which case $i$ would know that we are in such a case and be able to reason accordingly}. Thus we have that $(\I,r',m') \vDash \exists 0 \wedge \vee  \exists 1$. $\bigr)$ $\bigr)$. We observe that the statement $\forall r \in \I^{rom}: \forall i \in \N(r,1): \forall (r',m')$ s.t. $r_i(1) = r'_i(m'): \exists 0 \vee \exists 1$  Inductive step: $k - 1 \Rightarrow k$: As before, we quantify based on the definition of $E^k_\N$: $\forall r \in \I^{rom}: \forall i \in \N(r,1): \forall (r',m')$ s.t. $r_i(1) = r'_i(m'): \bigl($ Observe that $m'$ must not be 0, as 1 and $m'$ are locally-indistinguishable and   $\bigr)$