--- a/etnms/etnms.tex	Sun Jan 12 22:49:23 2020 +0000
+++ b/etnms/etnms.tex	Mon Jan 13 16:57:13 2020 +0000
@@ -180,57 +180,39 @@
 only.need to \emph{not} change the language, but also not change
 the value (computed result).
 
-\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt}
-Do you want to keep this? You essentially want to say that the old
-method used retrieve, which unfortunately cannot be adopted to 
-the simplification rules. You could just say that and give an example.
-However you have to think about how you give the example....nobody knows
-about AZERO etc yet. Maybe it might be better to use normal regexes
-like $a + aa$, but annotate bitsequences as subscript like $_1(_0a + _1aa)$.
+
 
-\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt}
-REPLY:\\
-Yes, I am essentially saying that the old method
-cannot be adopted without adjustments.
-But this does not mean we should skip
-the proof of the bit-coded algorithm
-as it is still the main direction we are looking into
-to prove things. We are trying to modify
-the old proof to suit our needs, but not give 
-up it totally, that is why i believe the old 
-proof is fundamental in understanding
-what we are doing in the past 6 months.
+For this we have started with looking at the original proof that
+established that the bitsequence algorithm produces the same result as
+the algorithm not using bitsequences. Formally this proof estabilshed
 
-\bigskip\noindent\rule[1.5ex]{\linewidth}{5pt}
-
-The correctness proof of
 \begin{center}
 $\blexer \; r^\uparrow  s = \lexer \;r \;s$
 \end{center}
-\noindent
-might provide us insight into proving 
-\begin{center}
-$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$
-\end{center}
+
 \noindent
-(that is also
-why we say the new proof builds on the older one).
-The proof defined the function $\flex$ as another way of
-expressing the $\lexer$ function:
-\begin{center}
-$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; r\backslash s)$
-\end{center}.
-\noindent
-(proof for the above equality will be explained later)
-The definition of $flex$ is as follows:
+The proof used two ''tricks", One is that it defined
+ a $\flex$-function
+
 \begin{center}
 \begin{tabular}{lcl}
 $\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \;  (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\
 $\textit{flex} \;r\; f\;  [\,] $ & $\dn$ & $f$
 \end{tabular}
 \end{center}
+
 \noindent
-here $\flex$ essentially does lexing by
+and then proved for the right-hand side in \eqref{lexer}
+
+\begin{center}
+$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; r\backslash s)$
+\end{center}.
+
+
+\noindent\rule[1.5ex]{\linewidth}{1pt}
+
+\noindent
+The $\flex$-function essentially does lexing by
 stacking up injection functions while doing derivatives,
 explicitly showing the order of characters being
 injected back in each step.