deletions | additions       diff --git a/subsection_b_bf_Knowledge_generalization__.tex b/subsection_b_bf_Knowledge_generalization__.tex  index d4f4b64..b19a216 100644  --- a/subsection_b_bf_Knowledge_generalization__.tex  +++ b/subsection_b_bf_Knowledge_generalization__.tex 
...
\\  $(b)$ I will argue by contradiction. Assume that we have some $M \vDash \varphi \Rightarrow E_S(\psi \wedge \varphi)$, but there is some $(M,s) \vDash \varphi \wedge \neg C_S \psi$. As $(M,s) \vDash \varphi \wedge \varphi \Rightarrow E_S(\psi \wedge \varphi)$ we conclude $(M,s) \vDash E_S(\psi \wedge \varphi)$. Again by our non-empty assumption, part (a), and knowledge-axiom analog, we get $(M,s) \vDash \varphi \wedge \psi$. In fact, we can perform this argument at all states $s'$ in which $(M,s') \vDash \varphi \wedge \neg C_S \psi$. Consider the set of S-reachable states from s; in these states, either $\varphi \wedge \neg C_S\psi$, $\varphi \wedge C_S\psi$, or $\neg\varphi$. In the states where $\neg\varphi$ holds, the statement $\varphi \Rightarrow C_S \psi$ holds vacuously. If there are any states where $C_S \psi$ holds, then $C_S \psi$ should have held at $s$, so we safely conclude there are no such states. This leaves us only with states where $\varphi \wedge \neg C_S \psi$. But in all these states, we have $\varphi \wedge psi$, which in turn means that we should have $\varphi \Rightarrow C_S \psi$ at these states. This contradicts our initial assumption; we conclude $(c)$ holds. \subsection*{e}  Again by contradiction, one direction at a time. There is some $M, s, i$ where $(M,s) \vDash i \in S \wedge B_i^S C_S \varphi \wedge \neg C_S \varphi$. From our analogue of the knowledge generalization axiom, we immediately conclude from $(M,s) \vDash i \in S \wedge B_i^S C_S \varphi$ that $(M,s) \vDash C_S \varphi$. But this contradicts our initial assumption; this direction holds.   The other direction: There is some $M, s, i$ where $(M,s) \vDash i \in S \wedge C_S \varphi \wedge \neg B_i^S C_S \varphi$. As $\neg B_i^S C_S \varphi$, there is some state s' which $i$ considers possible in which $i$ is correct where $(M,s') \vDash \neg C_S \varphi$. But that $s'$ is $S$-reachable from $s$, and so must also have $(M,s') \vDash C_S \varphi$. This is a contradiction.