# HG changeset patch
# User Chengsong
# Date 1582065870 0
# Node ID 5ca3b84e0eba029801d9d21c5a352e7a158680c5
# Parent  0172d422e93e79be15fa421ddadcb808f87ff3bb
v

diff -r 0172d422e93e -r 5ca3b84e0eba etnms/etnms.tex
--- a/etnms/etnms.tex	Sun Feb 16 22:37:26 2020 +0000
+++ b/etnms/etnms.tex	Tue Feb 18 22:44:30 2020 +0000
@@ -873,13 +873,9 @@
 
 \subsubsection*{Existing Proof}
 
-For this we have started with looking at the original proof that
-established that the bitsequence algorrithm produces the same result
-as the algorithm not using bitsequences. Formally this proof
-established
-
+For this we have started with looking at the proof of
 \begin{equation}\label{lexer}
-\blexer \; (r^\uparrow)  s = \lexer \;r \;s
+\blexer \; (r^\uparrow)  s = \lexer \;r \;s,
 \end{equation}
 
 %\noindent
@@ -889,6 +885,9 @@
 %\end{center}
 
 \noindent
+which established the bit-sequence algorithm produces the same
+result as the original algorithm, which does not use 
+bit-sequence.
 The proof uses two ``tricks''. One is that it uses a \flex-function
 
 \begin{center}
@@ -899,19 +898,18 @@
 \end{center}
 
 \noindent
-and then proves for the right-hand side in \eqref{lexer}
+to prove for the right-hand side in \eqref{lexer}
 
 \begin{center}
-$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$
-\end{center}.
-
+$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$.
+\end{center}
 
 
 
 \noindent
-The $\flex$-function essentially does lexing by
-stacking up injection functions while doing derivatives.
-
+linking $\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: