Less prolo symbols.
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}