From da4c87863958178e76750ce42b7fb4b298c828be Mon Sep 17 00:00:00 2001
From: "nathan.lhote" <nathan.lhote@lis-lab.fr>
Date: Fri, 24 Jun 2022 17:06:58 +0200
Subject: [PATCH] m

---
 main.tex | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/main.tex b/main.tex
index 5fbc2c0..a87b03e 100644
--- a/main.tex
+++ b/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}
-- 
GitLab