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}