
diff -r 2f6c10f79d5f -r 8a76c724883c paper/src/paper.tex
--- a/paper/src/paper.tex	Thu Jun 30 17:35:02 2011 +0200
+++ b/paper/src/paper.tex	Thu Jun 30 18:00:04 2011 +0200
@@ -295,31 +295,31 @@
 \[\mathbb{U}_\varphi = \{\psi U \chi \in FL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]
 
 \begin{def:atoms}
-Let $\varphi$ be a formula and $FL(\varphi)$ its closure. $\mathbb{A}_\varphi \subseteq FL(\varphi)$ is an \emph{atom} if following holds:
+Let $\varphi$ be a formula and $FL(\varphi)$ its closure. $A \subseteq FL(\varphi)$ is an \emph{atom} if following holds:
 \begin{itemize}
-\item $\forall{\psi \in FL(\varphi)}: \psi \in \mathbb{A}_\varphi \iff \neg \psi \notin \mathbb{A_\varphi}$
-\item $\forall{\psi \lor \chi \in FL(\varphi)}: \psi \lor \chi \in \mathbb{A}_\varphi \iff \psi \in \mathbb{A}_\varphi$ or $\chi \in \mathbb{A}_\varphi$ 
-\item $\forall{\psi U \chi \in FL(\varphi)}: \psi U \chi \in \mathbb{A}_\varphi \iff \chi \in \mathbb{A}_\varphi$ or $\psi, X(\psi U \chi) \in \mathbb{A_\varphi}$ 
+\item $\forall{\psi \in FL(\varphi)}: \psi \in A \iff \neg \psi \notin A$
+\item $\forall{\psi \lor \chi \in FL(\varphi)}: \psi \lor \chi \in A \iff \psi \in A$ or $\chi \in A$ 
+\item $\forall{\psi U \chi \in FL(\varphi)}: \psi U \chi \in A \iff \chi \in A$ or $\psi, X(\psi U \chi) \in A$ 
 \end{itemize}
-We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{\mathbb{A_\varphi} \subseteq FL({\varphi}) \mid \mathbb{A_\varphi} \text{ is an atom}\}$.
+We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{A \subseteq FL({\varphi}) \mid A \text{ is an atom}\}$.
 \end{def:atoms}
 
 \noindent Now that we have the required ingredients, we begin with the construction of automaton $\A_\varphi$ for formula $\varphi$. Let $\A_\varphi = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ with:
 \begin{itemize}
 \item $\Sigma = 2^{Voc(\varphi)}$
 \item $S = \mathbb{AT_\varphi}$
-\item $S_0 = \{\mathbb{A} \in \mathbb{AT_\varphi} \mid \varphi \in \mathbb{A}\}$
+\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 = \{(\mathbb{A}, P, \mathbb{B}) \mid \mathbb{A}, \mathbb{B} \in \mathbb{AT_\varphi}, P = \mathbb{A} \cap Voc(\varphi), X \psi \in \mathbb{A} \iff \psi \in \mathbb{B}\}$
-\item $\forall{i \in \N, i < k = |\mathbb{U}_{FL(\varphi)}|}: F_i = \{\mathbb{A} \in \mathbb{AT}_\varphi \mid \psi U \chi \notin \mathbb{A}$ or $\chi \in \mathbb{A}\}$
-\item $F_i = \{\mathbb{A} \in \mathbb{AT}_\varphi \mid \psi U \chi = \mathbb{U}_{\varphi_i}, \psi U \chi \notin \mathbb{A}$ or $\chi \in \mathbb{A}\}$ and therefore $k = |\mathbb{U}_{\varphi}|$
+\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 $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$.
 \end{itemize}
 
 \begin{thm:model language}
 Let $\M_\varphi = (\F, V_\varphi)$ be a model and $rep(\M_\varphi)$ its infinite representation word, then following holds:
-\[\M_\varphi \in L(A_\varphi) \iff \M_\varphi,0 \models \varphi\]
+\[rep(\M_\varphi) \in L(\A_\varphi) \iff \M_\varphi,0 \models \varphi\]
 \end{thm:model language}
 \noindent
 \begin{proof}




