diff --git a/main.tex b/main.tex
index d7e0eb68a26faaf6021a2b8b4f59b1bc465d242a..a0f6a369f99bcdcf33c2ebc17f9562fefbb73f3c 100644
--- a/main.tex
+++ b/main.tex
@@ -4,8 +4,8 @@
 \usepackage{amssymb,amsthm,amsmath,stmaryrd}
 \usepackage{xspace}
 
-\newcommand{\expreg}{expregular}
-\newcommand{\Expreg}{Expregular\xspace}
+\newcommand{\expreg}{exp-regular\xspace}
+\newcommand{\Expreg}{Exp-regular\xspace}
 \newcommand{\mso}{\textsf{MSO}\xspace}
 \newcommand{\fo}{\textsf{FO}\xspace}
 \newcommand{\msot}{\textsf{MSO-T}\xspace}
@@ -15,6 +15,7 @@
 \newcommand{\msomi}{\textsf{MSO-MI}\xspace}
 \newcommand{\fomi}{\textsf{FO-MI}\xspace}
 \newcommand{\nmsomi}{\textsf{NMSO-MI}\xspace}
+\newcommand{\rev}{\textsf{rev}\xspace}
 
 \newcommand{\sst}{\textsf{SST}\xspace}
 \newcommand{\mtt}{\textsf{MTT}\xspace}
@@ -28,13 +29,20 @@
 \newcommand{\tuple}[1]{\left(#1\right)}
 \newcommand{\sem}[1]{\left\llbracket #1\right\rrbracket}
 
+\newcommand{\eg}{\textit{e.g.~}}
+\newcommand{\ie}{\textit{i.e.~}}
+
 \newtheorem{theorem}{Theorem}
 \newtheorem{corollary}{Corollary}
 
+\theoremstyle{definition}
+\newtheorem{remark}{Remark}
+\newtheorem{question}{Question}
+
 
 \bibliographystyle{alpha}% the mandatory bibstyle
 
-\title{\Expreg functions} %TODO Please add
+\title{\Expreg transductions} %TODO Please add
 \author{}
 
 
@@ -64,11 +72,19 @@
 \label{sec:prelim}
 \subsection{Words, languages and transductions}
 \subsection{Relational structures and logical interpretations}
+
+\subsubsection{Relational structures}
+\paragraph{The orderned model of words}
+
+\paragraph{The powerset model of words}~\\
+
+Any \mso-formula can be seen as an \fo-formula over the powerset model
+\subsubsection{Logical interpretation}
 Here define \msoi and \foi.
 \subsection{Monadic interpretation}
 
 \footnote{We
-could add copy to MSOMI just as in Courcelle to avoid undesirable
+could add copy to \msomi just as in Courcelle to avoid undesirable
 cornercase behaviours with small words.}
 
 Given two relational signatures $\ssign,\tsign$, an \mso monadic interpretation $T$ of dimension $d$ from structures over $\ssign$ to structures over $\tsign$ is given by:
@@ -106,9 +122,15 @@ $$
 It is easy to see that $subsets\in\textsf{ExpF}$. 
 
 
+
+
+\section{Expressiveness of \expreg\ functions}
+
+\subsection{Backward translation theorem}
+
 \begin{theorem}[Backward translation theorem]
-    Let $T$ be an \msomi $T$ of dimension $d$ from structures over $\ssign$ to
-     structures over $\tsign$ ,and let $\phi(x_1,\dots,x_k)$ be an \fo-formula over
+    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)$}
 \end{theorem}
@@ -126,10 +148,20 @@ It is easy to see that $subsets\in\textsf{ExpF}$.
     regular domains. 
 \end{corollary}
 
+\begin{remark}
+\label{rem:power}
+An \msomi can also be seen as an \foi over the powerset model.
+\end{remark}
 
+\begin{question}
+Does $\msot\circ \msomi \subseteq \msomi$ hold? Using Krohn-Rhodes theorem of Miko\l aj, it seems that the only difficult case
+      is to post-compose an \msomi with a reversible Mealy machine. That is the problem can be rephrased as: does $\rev\circ \msomi \subseteq \msomi$ hold? 
+\end{question}
 
-\section{Expressiveness of \expreg\ functions}
 
+\begin{question}
+Given a (fixed) \msomi realizing $f$, can one compute the image of a word $u$ in time $O(|u|+|f(u)|)$ ?
+\end{question}
 \subsection{Closure properties}
 
 \begin{theorem}
@@ -137,122 +169,57 @@ It is easy to see that $subsets\in\textsf{ExpF}$.
 \end{theorem}
 
 \begin{proof}
-    Use standard ideas for composition logical transductions: formula
-    substitutions. The first-order parameters of the FOI becomes
+From the backward translation theorem.
+    Use standard ideas for composition of logical transductions: formula
+    substitutions. The first-order parameters of the \foi become
     monadic parameters. 
+    
+    Alternatively this comes from Remark~\ref{rem:power}, and the fact that \foi are closed under composition.
 \end{proof}
 
 
-\begin{theorem}
-    NSST$_{copy}$ $\subseteq$ \textsf{ExpR}. 
-\end{theorem}
-
-\begin{proof}
-    See IPAD notes. 
-\end{proof}
-
-\subsection{Lexicographic MSOMI and SST}
-
-An MSOMI $T$ is lexicographic if
-$\phi_{\leq}(\overline{X},\overline{Y})$ is of the following form, for
-$n=|\overline{X}|=|\overline{Y}|$:
-
-$$
-\overline{X} = \overline{Y}\vee \bigvee_{i=1}^{n} (\bigwedge_{1\leq
-  j<i} X_j = Y_j)\wedge \exists x\ \textsf{first-diff}(x,X_i,Y_i)\wedge \psi_i(x,X_i,Y_i)
-$$
-where $\psi_i$ are MSO-formulas and $\textsf{first-diff}(x,X_i,Y_i)$
-holds true if $x$ is the $\leq$-smallest position in $X_i\cup Y_i$
-such that $x\in X_i\leftrightarrow y\not\in Y_i$. 
-
-
-An MSOMI $T$ is \emph{purely} lexicographic if all $\psi_i(x,X_i,Y_i)$
-are of the form $x\not\in X_i \wedge x\in Y_i$.
-
-\begin{theorem}
-    A transduction $f$ is definable by an SST with copy iff it is
-    definable by a purely lexicographic MSOMI. 
-\end{theorem}
-
-\subsection{Polyregular functions}
-
-
-\begin{theorem}
-    \textsf{PolyF} $\subseteq$ \textsf{ExpF}
-\end{theorem}
-
-\begin{proof}
-\textsf{PolyF} = MSOI $\subseteq$ MSOMI = \textsf{ExpF}
-\end{proof}
-
 
 \subsection{\Expreg functions of polynomial growth}
 
 \begin{theorem}
-    $\textsf{ExpF}\cap O(n^d) = \textsf{PolyF}$
+    An \msomi of growth $O(n^d)$ can be realized by an \msoi of dimension $d$.
 \end{theorem}
 
-\begin{proof}
-    See mail Nathan sent to Mikolaj on Saturday 2 April
-    2022. Moreover, an MSOMI of $O(n^d)$ growth can be converted into
-    an MSOI of dimension $d$ (with $d$ first-order parameters). 
-\end{proof}
-
-Moreover, it is decidable whether an
 
 
 
-\subsection{Layered marble transducer}
 
-We define a model of transducers based on marble transducers.
-\section{FO model-checking of transductions with origins: SSTs and pebble transducers}
-\label{sec:mc}
-\subsection{Model-checking (copyfull) SSTs with origin}
 
-\begin{itemize}
-\item Origin := input position where the output position was created in a
-register update.
-\item FO[o] := FO[$\leq_in,\leq_out,o(x,y)$], i.e. FO over origin graphs
-\end{itemize}
 
 
-\begin{theorem}
-    Model-checking non-deterministic SST with copy against FO[o] is decidable.
-\end{theorem}
-
-\begin{proof}
-    Use the backward translation theorem.
-\end{proof}
+\section{The case of the successor}
 
 \begin{theorem}
-    Model-checking $O(n^2)$ deterministic SST with copy against MSO[o] is undecidable.
+\msomi with successor is equivalent to \dlin
 \end{theorem}
 
 \begin{proof}
-    See IPAD notes.
+Given an \msomi, we can define a rational letter-to-letter relation which realizes the successor and from this obtain a linear bounded automaton.
+From a linear bounded automaton, the next configuration relation can be defined in \mso.
 \end{proof}
 
+\begin{question}
 
-\subsection{Model-checking pebble transducers with origin}
-
-Origin = head position
 
-\begin{theorem}
-    Model-checking non-deterministic 2-pebble transducers against FO[o] is undecidable.
-\end{theorem}
-
-\begin{proof}
-    See IPAD notes.
-\end{proof}
+Does the model $a_1\cdots a_n\mapsto f\circ f_{a_1}\circ \cdots \circ f_{a_n}(\epsilon)$ compute \dlin ?
 
+\end{question}
+\section{Nested marble transducer}
 
+We define a model of transducers based on marble transducers.
+pebble transducer model. candidate:
+    layered marble transducers. A finite number of layers. a marble of layer k cannot go through another marble of layer k. However it can go through marbles of layers $<k$.
+    TODO: find a better name than "marble"
+    
 \begin{theorem}
-    Model-checking deterministic pebble transducers against FO[o] is decidable.
+   Any transduction defined by a nested marble transducer can be expressed as an \msomi. 
 \end{theorem}
 
-\begin{proof}
-    Use DPT = MSOI and the backward translation theorem. 
-\end{proof}
 
 
 \section{Some remaining questions}
@@ -260,32 +227,12 @@ Origin = head position
 \subsection{Expressiveness}
 
 
-\begin{itemize}
-    \item does $\msot\circ \msomi \subseteq \msomi$ holds ? Using Khrone
-      Rhodes theorem of Miko\l aj, it seems that the only difficult case
-      is to post-compose an \msomi with a reversible Mealy machine. Candidate composition which does not seem to be easy to
-      show its membership to \msomi:
-      $$
-      even-filter \circ (1-filter \circ subsets)
-      $$
-      where $1-filter$ only keeps the positions marked $1$ in
-      the results of the function $subsets$ and $even-filter$ only
-      keeps the even positions. It is easy to see that $(1-filter
-      \circ subsets)$ is \msomi.
-\end{itemize}
 
-\section{The case of the successor}
+   
+
 
-\begin{theorem}
-\msomi with successor is equivalent to \dlin
-\end{theorem}
 
-\begin{proof}
-Given an \msomi, we can define a rational letter-to-letter relation which realizes the successor and from this obtain a linear bounded automaton.
-From a linear bounded automaton, the next configuration relation can be defined in \mso.
-\end{proof}
 
-Does the model $a_1\cdots a_n\mapsto f\circ f_{a_1}\circ \cdots \circ f_{a_n}(\epsilon)$ compute \dlin ?
 
 \subsection{Computational models}
 
@@ -294,12 +241,12 @@ Does the model $a_1\cdots a_n\mapsto f\circ f_{a_1}\circ \cdots \circ f_{a_n}(\e
       they capture \msomi  ?
     \item recursive programming language corresponding or being
       captured by \msomi ?
-    \item pebble transducer model. candidate:
-    layered marble transducers. A finite number of layers. a marble of layer k cannot go through another marble of layer k. However it can go through marbles of layers $<k$.
-	\item Krohn-Rhodes like decomposition eg $\mathsf{polyreg}\circ \mathsf{exp} \circ \mathsf{reg}$, with $\mathsf{exp}$ being some simple class of exponential growth function.
+	\item Krohn-Rhodes like decomposition \eg $\mathsf{polyreg}\circ \mathsf{exp} \circ \mathsf{reg}$, with $\mathsf{exp}$ being some simple class of exponential growth function.
 \end{itemize}
 
 
+
+
 \bibliography{biblio}
 
 \end{document}