# HG changeset patch
# User Chengsong
# Date 1579858023 0
# Node ID c19f2d20d92cc0d2c230e9bd45470207b3f2597f
# Parent  af2c63f9bdf9b3d5c9a304ada1280ba6b722dd0f
added section

diff -r af2c63f9bdf9 -r c19f2d20d92c etnms/etnms.tex
--- 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