# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1309459545 -7200
# Node ID 636403068f28de29cfb94bff9161615515d3476f
# Parent  1d28f5f04efdb8539814813912e82281f786e861
Begin with model checking.

diff -r 1d28f5f04efd -r 636403068f28 paper/src/paper.tex
--- a/paper/src/paper.tex	Thu Jun 30 19:08:30 2011 +0200
+++ b/paper/src/paper.tex	Thu Jun 30 20:45:45 2011 +0200
@@ -314,7 +314,7 @@
 \item $S_0 = \{A \in \mathbb{AT_\varphi} \mid \varphi \in A\}$
 %\item $(A, P, B) \in \Delta$ for $A, B \in \mathbb{AT_\varphi}$ and $P = A \cap Voc(\varphi) \iff (X \psi \in A \iff \psi \in B)$
 \item $\Delta = \{(A, P, \mathbb{B}) \mid A, \mathbb{B} \in \mathbb{AT_\varphi}, P = A \cap Voc(\varphi), X \psi \in A \iff \psi \in \mathbb{B}\}$
-\item $\forall{i \in \N, i < k = |\mathbb{U}_{FL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi \notin A$ or $\chi \in A\}$
+%\item $\forall{i \in \N, i < k = |\mathbb{U}_{FL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi \notin A$ or $\chi \in A\}$
 \item $F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi = \mathbb{U}_{\varphi_i}, \psi U \chi \notin A$ or $\chi \in A\}$ and therefore $k = |\mathbb{U}_{\varphi}|$
 %Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
 %$P = A \cap Voc(\varphi)$ and For all $X \psi \in CL(\varphi): X \psi \in A$ iff $\psi \in B$.