--- a/etnms/etnms.tex	Thu Jan 09 22:21:04 2020 +0000
+++ b/etnms/etnms.tex	Fri Jan 10 13:03:37 2020 +0000
@@ -37,6 +37,7 @@
 \def\lexer{\mathit{lexer}}
 \def\blexer{\textit{blexer}}
 \def\blexers{\mathit{blexer\_simp}}
+\def\simp{\mathit{simp}}
 \def\mkeps{\mathit{mkeps}}
 \def\bmkeps{\textit{bmkeps}}
 \def\inj{\mathit{inj}}
@@ -250,6 +251,12 @@
 is defined, but not $\retrieve \; \AONE(\Z\S) \; \Left(\Empty)$,
 though we can extract the same POSIX
 bits from the two annotated regular expressions.
+The latter might occur when we try to retrieve from 
+a simplified regular expression using the same value
+as the unsimplified one.
+This is because $\Left(\Empty)$ corresponds to
+the regular expression structure $\AALTS$ instead of
+$\AONE$, this v
 That means, if we 
 want to prove that 
 \begin{center}
@@ -265,6 +272,11 @@
 \noindent
 we would need to rectify the value $\mkeps(r\backslash s)$ into something simpler
 to make the retrieve function defined.\\
+One way to do this is to prove the following:
+\begin{center}
+$\retrieve \; \rup\backslash_{simp} s \; \mkeps(\simp(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
+\end{center}
+\noindent
 %HERE CONSTRUCTION SITE
 The vsimp function, defined as follows
 tries to simplify the value in lockstep with