--- a/etnms/etnms.tex	Thu Jan 23 22:49:19 2020 +0000
+++ b/etnms/etnms.tex	Fri Jan 24 09:27:03 2020 +0000
@@ -1304,13 +1304,42 @@
 $  \oplus[\ZERO \;, \; _{bs}\oplus \textit{rs} ]$
 \end{center}
 and this will always trigger the $\flatten$ to 
-spill out the sequence $\textit{bs}$,
+spill out the inner alternative's bitcode $\textit{bs}$,
 whereas when
 simplification is done along the way, 
 the structure of nested alternatives is never created(we can
 actually prove that simplification function never allows nested
 alternatives to happen, more on this later).
 
+\subsection{Properties of the Function $\simp$}
+
+We have proved in Isabelle quite a few properties
+of the $\simp$-function, which helps the proof to go forward
+and we list them here to aid comprehension.
+
+To start, we need a bit of auxiliary notations,
+which is quite basic and is only written here
+for clarity.
+$\textit{sub}(r_1 \cdot r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r\}$\\
+$\textit{sub}(r_1 + r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1+r_2\}$\\
+
+$\textit{good}(r) \dn r \neq \ZERO \land \\
+\forall r' \in \textit{sub}(r), \textit{if} \; r' = _{bs_1}\oplus(rs_1), \;
+\textit{then} \nexists r'' \in \textit{rs}_1 \; s.t.\;
+r'' = _{bs_2}\oplus \textit{rs}_2 $
+
+The properties are mainly the ones below:
+\begin{itemize}
+\item
+\begin{center}
+$\simp(\simp(r)) = \simp(r)$
+\end{center}
+\item
+\begin{center}
+$\textit{if} r = \simp(r') \textit{then} \; \textit{good}(r) $
+\end{center}
+\end{itemize}
+
 %CONSTRUCTION SITE HERE
 that is to say, despite the bits are being moved around on the regular expression
 (difference in bits), the structure of the (unannotated)regular expression