deletions | additions       diff --git a/section_Fixpoint_Logics_for_Boolean__.tex b/section_Fixpoint_Logics_for_Boolean__.tex  index 10ae711..8849744 100644  --- a/section_Fixpoint_Logics_for_Boolean__.tex  +++ b/section_Fixpoint_Logics_for_Boolean__.tex 
...
\begin{align*}  \Stb(p) := \nu x. \pm p \land \lbox{p} x   \end{align*}  then agent $i \in \N$ is stable for $p$.\footnote{Notice that $\pm p$ is used as a variable ranging over $\set{p, \neg p}$.} p}$. Technically the above formula is to be read as a scheme for $\nu x. p \land \lbox{p} x$ and $\nu x. \pm \neg p \land \lbox{p} x$.}  \end{fact}  \begin{proof}  Assume $\Model, i \models \Stb(p)$. By the semantics of the $\mu$-calculus, formula $\Stb(p)$ denotes the largest fixpoint of function $\pm p \land \lbox{p}(\cdot)$, that is, formula $\lbox{p^*} \pm p$ where $\lbox{p^*}$ is the modal box interpreted over the reflexive and transitive closure of $R_p$. That is, there exists no $j$ such that $\O_i (p) \neq \O_j(p)$ which is connected by a finite $R_p$ path to $i$. It follows that in the stream generated by the BDP dynamics $i$ cannot change its opinion.