--- a/etnms/etnms.tex	Sat Feb 08 21:37:20 2020 +0000
+++ b/etnms/etnms.tex	Sat Feb 08 21:53:06 2020 +0000
@@ -109,7 +109,6 @@
 
 
 \section{Introduction}
-test
 While we believe derivatives of regular expressions, written
 $r\backslash s$, are a beautiful concept (in terms of ease of
 implementing them in functional programming languages and in terms of
@@ -125,6 +124,21 @@
 of simplification rules that keep the sizes of derivatives uniformly
 small.
 
+This has been partially addressed by the function $\blexer_{simp}$,
+which after  the simplification the $(a+aa)^*$ example's 8000 nodes will be
+reduced to just 6 and stays constant in each derivative step.
+The part that still needs more work is the correctness proof of this 
+function, namely,
+\begin{equation}\label{mainthm}
+\blexers \; r \; s = \blexer \;r\;s
+\end{equation}
+
+\noindent
+and this is what this report is mainly about. A condensed 
+version of the last report will be provided in the next section
+to help the reader understand the report, and the attempts 
+on the problem will follow.
+
 
 \section{Recapitulation of Concepts From the Last Report}