diff -r 8c1195dd6136 -r de50a65d1b15 ninems/ninems.tex
--- a/ninems/ninems.tex	Wed Jul 24 20:37:40 2019 +0100
+++ b/ninems/ninems.tex	Thu Jul 25 11:46:06 2019 +0100
@@ -1206,50 +1206,58 @@
 %How do we get this "future" information? By the value $v$, which is
 %computed by a pass of the algorithm that uses
 %$inj$ as described in the previous section).  
-using information from both the derivative regular expression and the value.
-Sulzmann and Lu used this
-to connect the bitcoded algorithm to the older algorithm by the following
-equation:
+using information from both the derivative regular expression and the
+value. Sulzmann and Lu poroposed this function, but did not prove
+anything about it. Ausaf and Urban used it to connect the bitcoded
+algorithm to the older algorithm by the following equation:
  
  \begin{center} $inj \;a\; c \; v = \textit{decode} \; (\textit{retrieve}\;
-	 ((\textit{internalise}\; r)\backslash_{simp} c) v)$ 
+	 (r^\uparrow)\backslash_{simp} \,c)\,v)$ 
  \end{center} 
- A little fact that needs to be stated to aid comprehension:
-\begin{center} 
-	$r^\uparrow = a$($a$ stands for $\textit{annotated}).$
-\end{center} 
-Ausaf and Urban also used this fact to prove  the
-correctness of bitcoded algorithm without simplification.  Our purpose
-of using this, however, is to establish 
+
+\noindent
+whereby $r^\uparrow$ stands for the internalised version of $r$. Ausaf
+and Urban also used this fact to prove  the correctness of bitcoded
+algorithm without simplification.  Our purpose of using this, however,
+is to establish 
+
 \begin{center}
 $ \textit{retrieve} \;
-a \; v \;=\; \textit{retrieve}  \; \textit{simp}(a) \; v'.$
+a \; v \;=\; \textit{retrieve}  \; (\textit{simp}\,a) \; v'.$
 \end{center}
-The idea
-is that using $v'$, a simplified version of $v$ that had gone
-through the same simplification step as $\textit{simp}(a)$, we are
-able to extract the bit-sequence that gives the same parsing
-information as the unsimplified one.  After establishing this, we
-might be able to finally bridge the gap of proving
+The idea is that using $v'$, a simplified version of $v$ that had gone
+through the same simplification step as $\textit{simp}(a)$, we are able
+to extract the bitcode that gives the same parsing information as the
+unsimplified one. However, we noticed that constructing such a  $v'$
+from $v$ is not so straightforward. The point of this is that  we might
+be able to finally bridge the gap by proving
+
 \begin{center}
-$\textit{retrieve} \; r^\uparrow   \backslash  s \; v = \;\textit{retrieve} \;
-\textit{bsimp}(r^\uparrow)  \backslash  s \; v'$
+$\textit{retrieve} \; (r^\uparrow   \backslash  s) \; v = \;\textit{retrieve} \;
+\textit{simp}(r^\uparrow)  \backslash  s \; v'$
 \end{center}
+
+\noindent
 and subsequently
+
 \begin{center}
-$\textit{retrieve} \; r^\uparrow \backslash  s \; v\; = \; \textit{retrieve} \;
-r^\uparrow  \backslash_{simp}   s \; v'$.
+$\textit{retrieve} \; (r^\uparrow \backslash  s) \; v\; = \; \textit{retrieve} \;
+(r^\uparrow  \backslash_{simp}  \, s) \; v'$.
 \end{center}
-The $\textit{LHS}$ of the above equation is the bitcode we want.
-This proves that our simplified
-version of regular expression still contains all the bitcodes needed.
-The task here is to find a way to compute the correct $v'$.
+
+\noindent
+The $\textit{LHS}$ of the above equation is the bitcode we want. This
+would prove that our simplified version of regular expression still
+contains all the bitcodes needed. The task here is to find a way to
+compute the correct $v'$.
 
 The second task is to speed up the more aggressive simplification.
-Currently it is slower than a naive simplification(the naive version as
-implemented in ADU of course can explode in some cases). So it needs to
-be explored how to make it faster. Our possibility would be to explore
-again the connection to DFAs. This is very much work in progress.
+Currently it is slower than the original naive simplification by Ausaf
+and Urban (the naive version as implemented by Ausaf   and Urban of
+course can ``explode'' in some cases). So it needs to be explored how to
+make our algorithm faster on all inputs. Our possibility would be to
+explore again the connection to DFAs. This is very much work in
+progress.
 
 \section{Conclusion}