Davide Grossi edited section_Fixpoint_Logics_for_Boolean__.tex  about 8 years ago

Commit id: 3418dd25cf6df76d48c95f979a3446f94ac7bac0

deletions | additions      

       

Let $\Model = \tuple{\N, \G, \O}$ be an influence model. The two following statements are equivalent:  \begin{enumerate}{(i)}  \item $i \in \N$ stabilizes for issue $p \in \Atoms$;  \item $\Model, i \models \mu x. p-\Stb \Stb(p)  \vee \box{p} x$ \end{enumerate}  \end{proposition}  \begin{proof}