1.1 --- a/paper/src/paper.tex	Thu Jun 30 17:35:02 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Thu Jun 30 18:00:04 2011 +0200
     1.3 @@ -295,31 +295,31 @@
     1.4  \[\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}\]
     1.5  
     1.6  \begin{def:atoms}
     1.7 -Let $\varphi$ be a formula and $FL(\varphi)$ its closure. $\mathbb{A}_\varphi \subseteq FL(\varphi)$ is an \emph{atom} if following holds:
     1.8 +Let $\varphi$ be a formula and $FL(\varphi)$ its closure. $A \subseteq FL(\varphi)$ is an \emph{atom} if following holds:
     1.9  \begin{itemize}
    1.10 -\item $\forall{\psi \in FL(\varphi)}: \psi \in \mathbb{A}_\varphi \iff \neg \psi \notin \mathbb{A_\varphi}$
    1.11 -\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$ 
    1.12 -\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}$ 
    1.13 +\item $\forall{\psi \in FL(\varphi)}: \psi \in A \iff \neg \psi \notin A$
    1.14 +\item $\forall{\psi \lor \chi \in FL(\varphi)}: \psi \lor \chi \in A \iff \psi \in A$ or $\chi \in A$ 
    1.15 +\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$ 
    1.16  \end{itemize}
    1.17 -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}\}$.
    1.18 +We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{A \subseteq FL({\varphi}) \mid A \text{ is an atom}\}$.
    1.19  \end{def:atoms}
    1.20  
    1.21  \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:
    1.22  \begin{itemize}
    1.23  \item $\Sigma = 2^{Voc(\varphi)}$
    1.24  \item $S = \mathbb{AT_\varphi}$
    1.25 -\item $S_0 = \{\mathbb{A} \in \mathbb{AT_\varphi} \mid \varphi \in \mathbb{A}\}$
    1.26 +\item $S_0 = \{A \in \mathbb{AT_\varphi} \mid \varphi \in A\}$
    1.27  %\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)$
    1.28 -\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}\}$
    1.29 -\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}\}$
    1.30 -\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}|$
    1.31 +\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}\}$
    1.32 +\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\}$
    1.33 +\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}|$
    1.34  %Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
    1.35  %$P = A \cap Voc(\varphi)$ and For all $X \psi \in CL(\varphi): X \psi \in A$ iff $\psi \in B$.
    1.36  \end{itemize}
    1.37  
    1.38  \begin{thm:model language}
    1.39  Let $\M_\varphi = (\F, V_\varphi)$ be a model and $rep(\M_\varphi)$ its infinite representation word, then following holds:
    1.40 -\[\M_\varphi \in L(A_\varphi) \iff \M_\varphi,0 \models \varphi\]
    1.41 +\[rep(\M_\varphi) \in L(\A_\varphi) \iff \M_\varphi,0 \models \varphi\]
    1.42  \end{thm:model language}
    1.43  \noindent
    1.44  \begin{proof}