deletions | additions       diff --git a/section_Fixpoint_Logics_for_Boolean__.tex b/section_Fixpoint_Logics_for_Boolean__.tex  index 0a55538..f377344 100644  --- a/section_Fixpoint_Logics_for_Boolean__.tex  +++ b/section_Fixpoint_Logics_for_Boolean__.tex 
...
\end{theorem}  \begin{proof}  \fbox{$1) \Rightarrow 2)$} Assume that $i$ stabilizes for issue $p \in \Atoms$.   \fbox{$2) \Rightarrow 1)$} Assume $\Model, i \models \mu x. \Stb(p) \vee \lbox{p} x$. By the semantics of the $\mu$-calculus $i$ belongs to the smallest fixpoint of equation $\pm p \lequiv \Stb(p) \vee \lbox{p} \pm p$. By the Knaster-Tarski theorem and the fact that influence models are finite, we can compute such fixpoint as $\bigcup_{0 \leq n < \omega} \true{\Stb(p)^n}$ where $\true{\Stb(p)^0} = \true{\true{\Stb(p) \vee \lbox{p} \bot}$ (notice that $\lbox{p} \bot \lequiv \bot$ on influence models) and $\true{\Stb(p)^{n+1}} = \true{\Stb(p) \vee \lbox{p}\Stb(p)^n}$. Rephrasing this fixpoint approximation byFact  \ref{fact:stable} that means, either $i$ is stable for issue $p$ or has access in a finite number of steps to a an agent who is stable for $p$. It follows that $i$ will therefore stabilize for $p$. \end{proof}  We immediately obtain that the complexity of checking whether a given agent stabilizes in a given influence model is $O(m \cdot n^{2})$ with $n$ being the size of the model and $m$ the size of $\mu x. \left(\nu y. \pm p \land \lbox{p} y \right) \vee \lbox{p} x$.