diff -r 5e47080a7164 -r bc340e8f4165 etnms/etnms.tex
--- a/etnms/etnms.tex	Tue Mar 03 21:36:53 2020 +0000
+++ b/etnms/etnms.tex	Tue Mar 03 21:56:09 2020 +0000
@@ -909,20 +909,15 @@
 
 
 \noindent
-linking $\flex$ and $\lexer$,
+This property links $\flex$ and $\lexer$,
 it essentially does lexing by
 stacking up injection functions while doing derivatives,
 explicitly showing the order of characters being
 injected back in each step.
-With $\flex$ we can write $\lexer$ this way: 
-
-\begin{center}
-$\lexer \;r\; s = \flex \;id \; r\;s \;(\mkeps (r\backslash s))$
-\end{center}
 
 \noindent
 The other trick, which is the crux in the existing proof, 
-is the use of $\retrieve$-function by Sulzmann and Lu:
+is the use of the $\retrieve$-function by Sulzmann and Lu:
 \begin{center}
 \begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
   $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\
@@ -946,11 +941,11 @@
 This function assembles the bitcode 
 using information from both the derivative regular expression and the
 value. Sulzmann and Lu proposed this function, but did not prove
-anything about it. Ausaf and Urban made this important use of the
-fact about $\retrieve$ in the proof:
+anything about it. Ausaf and Urban made use of the
+fact about $\retrieve$ in their proof:
  
  \begin{center} 
- $\retrieve \rup \backslash c \; v = \retrieve  \rup (\inj \;r \;c \; v)$
+ $\retrieve\; \rup \backslash c \; v = \retrieve \;  \rup (\inj \;r \;c \; v)$
  \end{center} 
 
 \noindent
@@ -973,13 +968,13 @@
 \end{center}
 \noindent
 where $\mkeps(r\backslash s) $ is denoted using $v$,
-then a reverse induction technique is 
-best suited here to make use of 
+then a reverse induction  
+helps with using 
 the fact~\eqref{flex} in proving the $n+1$ step:
 \begin{center} 
 $ \flex \; r\; id\; (s@[c])\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$
 \end{center}
-and using a lemma that
+Using a lemma that
 \begin{center}
 $\textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\; = \textit{retrieve}\; (\rup \backslash s@[c])  \; v\; $
 \end{center}
@@ -989,9 +984,27 @@
 \end{center}
 and the inductive step is done because
 \begin{center} 
-$ \textit{retrieve}\; (\rup \backslash s@[c]) \; \mkeps(r\backslash s) =  \bmkeps \;(\rup \backslash s@[c])$
+$ \textit{retrieve}\; (\rup \backslash s@[c]) \; \mkeps(r\backslash s) =  \bmkeps \;(\rup \backslash s@[c])$.
 \end{center}
 
+\noindent
+To use 
+$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$
+ for our 
+correctness proof, simply replace the $v$ with
+$\mkeps\;(r\backslash s)$, and apply the lemma that
+\begin{center}
+$ \; \bmkeps \; \rup =  (\textit{retrieve} \; \rup \; \mkeps(r))$
+\end{center}
+\noindent
+We get the correctness of our bit-coded algorithm:
+\begin{center}
+$\flex \;r\;  id \; s \; (\mkeps \; (r\backslash s)) = \textit{decode} \; (\bmkeps \; \rup\backslash s) \; r$.
+\end{center}
+\noindent
+
+
+
 \subsubsection{Using Retrieve Function In a New Setting}
  Ausaf
 and Urban used $\retrieve$  to prove  the correctness of bitcoded
@@ -1005,41 +1018,9 @@
 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
-
-\noindent
-By using a property of retrieve we have the $\textit{RHS}$ of the above equality is
-$decode (retrieve (r^\uparrow \backslash(s @ [c])) v) r$, and this gives the 
-main lemma result:
-
-\begin{center}
-$ \flex \;r\;  id \; (s@[c]) \; v =\textit{decode}(\textit{retrieve} (\rup \backslash (s@[c])) \;v) r$
-\end{center}
-
-
-
-
-\noindent
-To use this lemma result for our 
-correctness proof, simply replace the $v$ in the
-$\textit{RHS}$ of the above equality with
-$\mkeps\;(r\backslash (s@[c]))$, and apply the lemma that
- 
-\begin{center}
-$\textit{decode} \; \bmkeps \; \rup \; r = \textit{decode} \; (\textit{retrieve} \; \rup \; \mkeps(r)) \;r$
-\end{center}
-\noindent
-We get the correctness of our bit-coded algorithm:
-\begin{center}
-$\flex \;r\;  id \; s \; (\mkeps \; r\backslash s) = \textit{decode} \; \bmkeps \; \rup\backslash s \; r$
-\end{center}
-\noindent
-The bridge between the above chain of equalities
-is the use of $\retrieve$,
-if we want to use a similar technique for the 
-simplified version of algorithm,
+unsimplified one. 
+If we want to use a similar technique as
+that of the existing proof,
 we face the problem that in the above 
 equalities,
 $\retrieve \; a \; v$ is not always defined.