--- a/etnms/etnms.tex	Mon Feb 24 11:03:45 2020 +0000
+++ b/etnms/etnms.tex	Fri Feb 28 22:48:10 2020 +0000
@@ -3,9 +3,11 @@
 \usepackage{data}
 \usepackage{tikz-cd}
 \usepackage{tikz}
-\usetikzlibrary{graphs}
-\usetikzlibrary{graphdrawing}
-\usegdlibrary{trees}
+
+%\usetikzlibrary{graphs}
+%\usetikzlibrary{graphdrawing}
+%\usegdlibrary{trees}
+
 %\usepackage{algorithm}
 \usepackage{amsmath}
 \usepackage{xcolor}
@@ -1551,9 +1553,20 @@
 $r \gg \textit{bs}$.
 The $\gg$ operator with the
 regular expression $r$ may also be seen as a 
-
-\end{tikzpicture}
-\end{center}
+regular language by itself on the alphabet
+$\Sigma = {0,1}$.
+The definition of contains relation
+is given in an inductive form, similar to that
+of regular expressions, it might not be surprising 
+that the set it denotes contains basically 
+ everything a regular expression can 
+produce during the derivative and lexing process.
+This can be seen in the subsequent lemmas we have
+proved about contains:
+\begin{itemize}
+\item
+$\textit{if} \models v:r \; \textit{then} \; \rup \gg \textit{code}(v)$
+\end{itemize}
 \subsection{the $\textit{ders}_2$ Function}
 If we want to prove the result 
 \begin{center}