--- a/ChengsongTanPhdThesis/Chapters/Inj.tex	Fri Dec 30 01:52:32 2022 +0000
+++ b/ChengsongTanPhdThesis/Chapters/Inj.tex	Fri Dec 30 17:37:51 2022 +0000
@@ -1383,7 +1383,16 @@
 and therefore can be thrown away.
 
 Ausaf et al. \cite{AusafDyckhoffUrban2016} 
-have come up with some simplification steps, however those steps
+have come up with some simplification steps, 
+and incorporated the simplification into $\lexer$.
+They call this lexer $\textit{lexer}_{simp}$ and proved that
+\[
+	\lexer \; r\; s = \textit{lexer}_{simp} \; r \; s
+\]
+The function $\textit{lexer}_{simp}$
+involves some fiddly manipulation of value rectification,
+which we omit here.
+however those steps
 are not yet sufficiently strong, to achieve the above effects.
 And even with these relatively mild simplifications, the proof
 is already quite a bit more complicated than the theorem \ref{lexerCorrectness}.