m

main.tex

@@ -20,7 +20,7 @@
 \newcommand{\sst}{\textsf{SST}\xspace}
 \newcommand{\mtt}{\textsf{MTT}\xspace}
 
-\newcommand{\dlin}{\textsc{DLinSpace}}
+\newcommand{\dlin}{\textsc{DLinSpace}\xspace}
 
 \newcommand{\ssign}{\mathfrak{S}}
 \newcommand{\tsign}{\mathfrak{T}}
@@ -132,7 +132,7 @@ It is easy to see that $subsets\in\textsf{ExpF}$.
     Let $T$ be an \msomi of dimension $d$ from structures over $\ssign$ to
      structures over $\tsign$, and let $\phi(x_1,\dots,x_k)$ be an \fo-formula over
     $\tsign$.
-    We can define an \mso-formula $\psi(\bar X_1,\ldots,\bar X_k)$  such that for any structure $A$ over $\ssign$, $A\models\psi(\bar S_1,\ldots,\bar S_k) $ if and only if $\sem T(A)\models \phi(\bar S_1,\ldots,\bar S_k)$.\footnote{Note that $\bar S_i$ is a position of the structure $\sem T(A)$}
+    We can define an \mso-formula $\psi(\bar X_1,\ldots,\bar X_k)$  such that for any structure $A$ over $\ssign$, $A\models\psi(\bar S_1,\ldots,\bar S_k) $ if and only if $\sem T(A)\models \phi(\bar S_1,\ldots,\bar S_k)$.\footnote{Note that $\bar S_i$ denotes either a tuple of sets of positions of $A$, or a position of $\sem T(A)$}
 \end{theorem}
 
 \begin{proof}
@@ -160,10 +160,11 @@ Does $\msot\circ \msomi \subseteq \msomi$ hold? Using Krohn-Rhodes theorem of Mi
 
 
 \begin{question}
-Given a (fixed) \msomi realizing $f$, can one compute the image of a word $u$ in time $O(|u|+|f(u)|)$ ?
+Given a (fixed) \msomi realizing $f$, can one compute the image of a word $u$ in time $O \big( |u|+|f(u)|\big)$ ?
 \end{question}
 \subsection{Closure properties}
 
+\subsubsection{Postcomposition by \foi}
 \begin{theorem}
     $\foi\ \circ \msomi\ = \msomi$
 \end{theorem}
@@ -178,6 +179,16 @@ From the backward translation theorem.
 \end{proof}
 
 
+\subsubsection{Precomposition by \msot}
+\begin{theorem}
+    $\msomi\ \circ \msot\ = \msomi$
+\end{theorem}
+
+\begin{proof}
+    From the usual proof of closure under composition of \msot.
+\end{proof}
+
+
 
 \subsection{\Expreg functions of polynomial growth}
 
@@ -195,7 +206,7 @@ From the backward translation theorem.
 \section{The case of the successor}
 
 \begin{theorem}
-\msomi with successor is equivalent to \dlin
+\msomi with successor is equivalent to \dlin reductions.
 \end{theorem}
 
 \begin{proof}