
diff -r b0f0d884a547 -r d5e9bcb384ec ChengsongTanPhdThesis/Chapters/Finite.tex
--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Wed Oct 12 14:01:33 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Wed Oct 12 14:08:06 2022 +0100
@@ -785,6 +785,320 @@
 	$\rder{x}{(\rsimpalts \; rs)} = \rsimpalts \; (\map \; (\rder{x}{\_}) \; rs)$
 \end{lemma}
 \noindent
+
+\subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s}
+Much like the definition of $L$ on plain regular expressions, one could also 
+define the language interpretation of $\rrexp$s.
+\begin{center}
+	\begin{tabular}{lcl}
+		$RL \; (\ZERO)$ & $\dn$ & $\phi$\\
+		$RL \; (\ONE)$ & $\dn$ & $\{[]\}$\\
+		$RL \; (c)$ & $\dn$ & $\{[c]\}$\\
+		$RL \; \sum rs$ & $\dn$ & $ \bigcup_{r \in rs} (RL \; r)$\\
+		$RL \; (r_1 \cdot r_2)$ & $\dn$ & $ RL \; (r_1) @ RL \; (r_2)$\\
+		$RL \; (r^*)$ & $\dn$ & $ (RL(r))^*$
+	\end{tabular}
+\end{center}
+\noindent
+The main use of $RL$ is to establish some connections between $\rsimp{}$ 
+and $\rnullable{}$:
+\begin{lemma}
+	The following properties hold:
+	\begin{itemize}
+		\item
+			If $\rnullable{r}$, then $\rsimp{r} \neq \RZERO$.
+		\item
+			$\rnullable{r \backslash s} \quad $ if and only if $\quad \rnullable{\rderssimp{r}{s}}$.
+	\end{itemize}
+\end{lemma}
+\begin{proof}
+	The first part is by induction on $r$. 
+	The second part is true because property 
+	\[ RL \; r = RL \; (\rsimp{r})\] holds.
+\end{proof}
+
+\subsubsection{Simplified $\textit{Rrexp}$s are Good}
+We formalise the notion of ``good" regular expressions,
+which means regular expressions that
+are not fully simplified. For alternative regular expressions that means they
+do not contain any nested alternatives like 
+\[ r_1 + (r_2 + r_3) \], un-removed $\RZERO$s like \[\RZERO + r\]
+or duplicate elements in a children regular expression list like \[ \sum [r, r, \ldots]\]:
+\begin{center}
+	\begin{tabular}{@{}lcl@{}}
+		$\good\; \RZERO$ & $\dn$ & $\textit{false}$\\
+		$\good\; \RONE$ & $\dn$ & $\textit{true}$\\
+		$\good\; \RCHAR{c}$ & $\dn$ & $\btrue$\\
+		$\good\; \RALTS{[]}$ & $\dn$ & $\bfalse$\\
+		$\good\; \RALTS{[r]}$ & $\dn$ & $\bfalse$\\
+		$\good\; \RALTS{r_1 :: r_2 :: rs}$ & $\dn$ & 
+		$\textit{isDistinct} \; (r_1 :: r_2 :: rs) \;$\\
+						   & & $\textit{and}\; (\forall r' \in (r_1 :: r_2 :: rs).\; \good \; r'\; \,  \textit{and}\; \, \textit{nonAlt}\; r')$\\
+		$\good \; \RSEQ{\RZERO}{r}$ & $\dn$ & $\bfalse$\\
+		$\good \; \RSEQ{\RONE}{r}$ & $\dn$ & $\bfalse$\\
+		$\good \; \RSEQ{r}{\RZERO}$ & $\dn$ & $\bfalse$\\
+		$\good \; \RSEQ{r_1}{r_2}$ & $\dn$ & $\good \; r_1 \;\, \textit{and} \;\, \good \; r_2$\\
+		$\good \; \RSTAR{r}$ & $\dn$ & $\btrue$\\
+	\end{tabular}
+\end{center}
+\noindent
+The predicate $\textit{nonAlt}$ evaluates to true when the regular expression is not an
+alternative, and false otherwise.
+The $\good$ property is preserved under $\rsimp_{ALTS}$, provided that
+its non-empty argument list of expressions are all good themsleves, and $\textit{nonAlt}$, 
+and unique:
+\begin{lemma}\label{rsimpaltsGood}
+	If $rs \neq []$ and forall $r \in rs. \textit{nonAlt} \; r$ and $\textit{isDistinct} \; rs$,
+	then $\good \; (\rsimpalts \; rs)$ if and only if forall $r \in rs. \; \good \; r$.
+\end{lemma}
+\noindent
+We also note that
+if a regular expression $r$ is good, then $\rflts$ on the singleton
+list $[r]$ will not break goodness:
+\begin{lemma}\label{flts2}
+	If $\good \; r$, then forall $r' \in \rflts \; [r]. \; \good \; r'$ and $\textit{nonAlt} \; r'$.
+\end{lemma}
+\begin{proof}
+	By an induction on $r$.
+\end{proof}
+\noindent
+The other observation we make about $\rsimp{r}$ is that it never
+comes with nested alternatives, which we describe as the $\nonnested$
+property:
+\begin{center}
+	\begin{tabular}{lcl}
+		$\nonnested \; \, \sum []$ & $\dn$ & $\btrue$\\
+		$\nonnested \; \, \sum ((\sum rs_1) :: rs_2)$ & $\dn$ & $\bfalse$\\
+		$\nonnested \; \, \sum (r :: rs)$ & $\dn$ & $\nonnested (\sum rs)$\\
+		$\nonnested \; \, r $ & $\dn$ & $\btrue$
+	\end{tabular}
+\end{center}
+\noindent
+The $\rflts$ function
+always opens up nested alternatives,
+which enables $\rsimp$ to be non-nested:
+
+\begin{lemma}\label{nonnestedRsimp}
+	$\nonnested \; (\rsimp{r})$
+\end{lemma}
+\begin{proof}
+	By an induction on $r$.
+\end{proof}
+\noindent
+With this we could prove that a regular expressions
+after simplification and flattening and de-duplication,
+will not contain any alternative regular expression directly:
+\begin{lemma}\label{nonaltFltsRd}
+	If $x \in \rdistinct{\rflts\; (\map \; \rsimp{} \; rs)}{\varnothing}$ 
+	then $\textit{nonAlt} \; x$.
+\end{lemma}
+\begin{proof}
+	By \ref{nonnestedRsimp}.
+\end{proof}
+\noindent
+The other thing we know is that once $\rsimp{}$ had finished
+processing an alternative regular expression, it will not
+contain any $\RZERO$s, this is because all the recursive 
+calls to the simplification on the children regular expressions
+make the children good, and $\rflts$ will not take out
+any $\RZERO$s out of a good regular expression list,
+and $\rdistinct{}$ will not mess with the result.
+\begin{lemma}\label{flts3Obv}
+	The following are true:
+	\begin{itemize}
+		\item
+			If for all $r \in rs. \, \good \; r $ or $r = \RZERO$,
+			then for all $r \in \rflts\; rs. \, \good \; r$.
+		\item
+			If $x \in \rdistinct{\rflts\; (\map \; rsimp{}\; rs)}{\varnothing}$
+			and for all $y$ such that $\llbracket y \rrbracket_r$ less than
+			$\llbracket rs \rrbracket_r + 1$, either
+			$\good \; (\rsimp{y})$ or $\rsimp{y} = \RZERO$,
+			then $\good \; x$.
+	\end{itemize}
+\end{lemma}
+\begin{proof}
+	The first part is by induction on $rs$, where the induction
+	rule is the inductive cases for $\rflts$.
+	The second part is a corollary from the first part.
+\end{proof}
+
+And this leads to good structural property of $\rsimp{}$,
+that after simplification, a regular expression is
+either good or $\RZERO$:
+\begin{lemma}\label{good1}
+	For any r-regular expression $r$, $\good \; \rsimp{r}$ or $\rsimp{r} = \RZERO$.
+\end{lemma}
+\begin{proof}
+	By an induction on $r$. The inductive measure is the size $\llbracket \rrbracket_r$.
+	Lemma \ref{rsimpSize} says that 
+	$\llbracket \rsimp{r}\rrbracket_r$ is smaller than or equal to
+	$\llbracket r \rrbracket_r$.
+	Therefore, in the $r_1 \cdot r_2$ and $\sum rs$ case,
+	Inductive hypothesis applies to the children regular expressions
+	$r_1$, $r_2$, etc. The lemma \ref{flts3Obv}'s precondition is satisfied
+	by that as well.
+	The lemmas \ref{nonnestedRsimp} and  \ref{nonaltFltsRd} are used
+	to ensure that goodness is preserved at the topmost level.
+\end{proof}
+We shall prove that any good regular expression is 
+a fixed-point for $\rsimp{}$.
+First we prove an auxiliary lemma:
+\begin{lemma}\label{goodaltsNonalt}
+	If $\good \; \sum rs$, then $\rflts\; rs = rs$.
+\end{lemma}
+\begin{proof}
+	By an induction on $\sum rs$. The inductive rules are the cases
+	for $\good$.
+\end{proof}
+\noindent
+Now we are ready to prove that good regular expressions are invariant
+of $\rsimp{}$ application:
+\begin{lemma}\label{test}
+	If $\good \;r$ then $\rsimp{r} = r$.
+\end{lemma}
+\begin{proof}
+	By an induction on the inductive cases of $\good$, using lemmas
+	\ref{goodaltsNonalt} and \ref{rdistinctOnDistinct}.
+	The lemma \ref{goodaltsNonalt} is used in the alternative
+	case where 2 or more elements are present in the list.
+\end{proof}
+\noindent
+Given below is a property involving $\rflts$, $\rdistinct{}{}$, $\rsimp{}$ and $\rsimp_{ALTS}$,
+which requires $\ref{good1}$ to go through smoothly.
+It says that an application of $\rsimp_{ALTS}$ can be "absorbed",
+if it its output is concatenated with a list and then applied to $\rflts$.
+\begin{lemma}\label{flattenRsimpalts}
+	$\rflts \; ( (\rsimp_{ALTS} \; 
+	(\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing})) :: 
+	\map \; \rsimp{} \; rs' ) = 
+	\rflts \; ( (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing}) @ (
+	\map \; \rsimp{rs'}))$
+
+
+\end{lemma}
+\begin{proof}
+	By \ref{good1}.
+\end{proof}
+\noindent
+
+
+
+
+
+We are also ready to prove that $\textit{rsimp}$ is idempotent.
+\subsubsection{$\rsimp$ is Idempotent}
+The idempotency of $\rsimp$ is very useful in 
+manipulating regular expression terms into desired
+forms so that key steps allowing further rewriting to closed forms
+are possible.
+\begin{lemma}\label{rsimpIdem}
+	$\rsimp{r} = \rsimp{\rsimp{r}}$
+\end{lemma}
+
+\begin{proof}
+	By \ref{test} and \ref{good1}.
+\end{proof}
+\noindent
+This property means we do not have to repeatedly
+apply simplification in each step, which justifies
+our definition of $\blexersimp$.
+
+
+On the other hand, we could repeat the same $\rsimp{}$ applications
+on regular expressions as many times as we want, if we have at least
+one simplification applied to it, and apply it wherever we would like to:
+\begin{corollary}\label{headOneMoreSimp}
+	The following properties hold, directly from \ref{rsimpIdem}:
+
+	\begin{itemize}
+		\item
+			$\map \; \rsimp{(r :: rs)} = \map \; \rsimp{} \; (\rsimp{r} :: rs)$
+		\item
+			$\rsimp{(\RALTS{rs})} = \rsimp{(\RALTS{\map \; \rsimp{} \; rs})}$
+	\end{itemize}
+\end{corollary}
+\noindent
+This will be useful in later closed form proof's rewriting steps.
+Similarly, we point out the following useful facts below:
+\begin{lemma}
+	The following equalities hold if $r = \rsimp{r'}$ for some $r'$:
+	\begin{itemize}
+		\item
+			If $r  = \sum rs$ then $\rsimpalts \; rs = \sum rs$.
+		\item
+			If $r = \sum rs$ then $\rdistinct{rs}{\varnothing} = rs$.
+		\item
+			$\rsimpalts \; (\rdistinct{\rflts \; [r]}{\varnothing}) = r$.
+	\end{itemize}
+\end{lemma}
+\begin{proof}
+	By application of lemmas \ref{rsimpIdem} and \ref{good1}.
+\end{proof}
+
+\noindent
+With the idempotency of $\rsimp{}$ and its corollaries, 
+we can start proving some key equalities leading to the 
+closed forms.
+Now presented are a few equivalent terms under $\rsimp{}$.
+We use $r_1 \sequal r_2 $ here to denote $\rsimp{r_1} = \rsimp{r_2}$.
+\begin{lemma}
+	\begin{itemize}
+		The following equivalence hold:
+	\item
+		$\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$
+	\item
+		$\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$
+	\item
+		$\RALTS{\RALTS{rs}} \sequal \RALTS{rs}$
+	\item
+		$\sum ((\sum rs_a) :: rs_b) \sequal \sum rs_a @ rs_b$
+	\item
+		$\RALTS{rs} = \RALTS{\map \; \rsimp{} \; rs}$
+\end{itemize}
+\end{lemma}
+\begin{proof}
+	By induction on the lists involved.
+\end{proof}
+\noindent
+The above allows us to prove
+two similar equalities (which are a bit more involved).
+It says that we could flatten out the elements
+before simplification and still get the same result.
+\begin{lemma}\label{simpFlatten3}
+	One can flatten the inside $\sum$ of a $\sum$ if it is being 
+	simplified. Concretely,
+	\begin{itemize}
+		\item
+			If for all $r \in rs, rs', rs''$, we have $\good \; r $
+			or $r = \RZERO$, then $\sum (rs' @ rs @ rs'') \sequal 
+			\sum (rs' @ [\sum rs] @ rs'')$ holds. As a corollary,
+		\item
+			$\sum (rs' @ [\sum rs] @ rs'') \sequal \sum (rs' @ rs @ rs'')$
+	\end{itemize}
+\end{lemma}
+\begin{proof}
+	By rewriting steps involving the use of \ref{test} and \ref{rdistinctConcatGeneral}.
+	The second sub-lemma is a corollary of the previous.
+\end{proof}
+%Rewriting steps not put in--too long and complicated-------------------------------
+\begin{comment}
+	\begin{center}
+		$\rsimp{\sum (rs' @ rs @ rs'')}  \stackrel{def of bsimp}{=}$  \\
+		$\rsimpalts \; (\rdistinct{\rflts \; ((\map \; \rsimp{}\; rs') @ (\map \; \rsimp{} \; rs ) @ (\map \; \rsimp{} \; rs''))}{\varnothing})$ \\
+		$\stackrel{by \ref{test}}{=} 
+		\rsimpalts \; (\rdistinct{(\rflts \; rs' @ \rflts \; rs @ \rflts \; rs'')}{
+		\varnothing})$\\
+		$\stackrel{by \ref{rdistinctConcatGeneral}}{=}
+		\rsimpalts \; (\rdistinct{\rflts \; rs'}{\varnothing} @ \rdistinct{(
+		\rflts\; rs @ \rflts \; rs'')}{\rflts \; rs'})$\\
+
+	\end{center}
+\end{comment}
+%Rewriting steps not put in--too long and complicated-------------------------------
+\noindent
+
+
 We need more equalities like the above to enable a closed form,
 for which we need to introduce a few rewrite relations
 to help
@@ -1629,317 +1943,6 @@
 	By \ref{rsimpMonoLemmas}.
 \end{proof}
 
-\subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s}
-Much like the definition of $L$ on plain regular expressions, one could also 
-define the language interpretation of $\rrexp$s.
-\begin{center}
-	\begin{tabular}{lcl}
-		$RL \; (\ZERO)$ & $\dn$ & $\phi$\\
-		$RL \; (\ONE)$ & $\dn$ & $\{[]\}$\\
-		$RL \; (c)$ & $\dn$ & $\{[c]\}$\\
-		$RL \; \sum rs$ & $\dn$ & $ \bigcup_{r \in rs} (RL \; r)$\\
-		$RL \; (r_1 \cdot r_2)$ & $\dn$ & $ RL \; (r_1) @ RL \; (r_2)$\\
-		$RL \; (r^*)$ & $\dn$ & $ (RL(r))^*$
-	\end{tabular}
-\end{center}
-\noindent
-The main use of $RL$ is to establish some connections between $\rsimp{}$ 
-and $\rnullable{}$:
-\begin{lemma}
-	The following properties hold:
-	\begin{itemize}
-		\item
-			If $\rnullable{r}$, then $\rsimp{r} \neq \RZERO$.
-		\item
-			$\rnullable{r \backslash s} \quad $ if and only if $\quad \rnullable{\rderssimp{r}{s}}$.
-	\end{itemize}
-\end{lemma}
-\begin{proof}
-	The first part is by induction on $r$. 
-	The second part is true because property 
-	\[ RL \; r = RL \; (\rsimp{r})\] holds.
-\end{proof}
-
-\subsubsection{Simplified $\textit{Rrexp}$s are Good}
-We formalise the notion of ``good" regular expressions,
-which means regular expressions that
-are not fully simplified. For alternative regular expressions that means they
-do not contain any nested alternatives like 
-\[ r_1 + (r_2 + r_3) \], un-removed $\RZERO$s like \[\RZERO + r\]
-or duplicate elements in a children regular expression list like \[ \sum [r, r, \ldots]\]:
-\begin{center}
-	\begin{tabular}{@{}lcl@{}}
-		$\good\; \RZERO$ & $\dn$ & $\textit{false}$\\
-		$\good\; \RONE$ & $\dn$ & $\textit{true}$\\
-		$\good\; \RCHAR{c}$ & $\dn$ & $\btrue$\\
-		$\good\; \RALTS{[]}$ & $\dn$ & $\bfalse$\\
-		$\good\; \RALTS{[r]}$ & $\dn$ & $\bfalse$\\
-		$\good\; \RALTS{r_1 :: r_2 :: rs}$ & $\dn$ & 
-		$\textit{isDistinct} \; (r_1 :: r_2 :: rs) \;$\\
-						   & & $\textit{and}\; (\forall r' \in (r_1 :: r_2 :: rs).\; \good \; r'\; \,  \textit{and}\; \, \textit{nonAlt}\; r')$\\
-		$\good \; \RSEQ{\RZERO}{r}$ & $\dn$ & $\bfalse$\\
-		$\good \; \RSEQ{\RONE}{r}$ & $\dn$ & $\bfalse$\\
-		$\good \; \RSEQ{r}{\RZERO}$ & $\dn$ & $\bfalse$\\
-		$\good \; \RSEQ{r_1}{r_2}$ & $\dn$ & $\good \; r_1 \;\, \textit{and} \;\, \good \; r_2$\\
-		$\good \; \RSTAR{r}$ & $\dn$ & $\btrue$\\
-	\end{tabular}
-\end{center}
-\noindent
-The predicate $\textit{nonAlt}$ evaluates to true when the regular expression is not an
-alternative, and false otherwise.
-The $\good$ property is preserved under $\rsimp_{ALTS}$, provided that
-its non-empty argument list of expressions are all good themsleves, and $\textit{nonAlt}$, 
-and unique:
-\begin{lemma}\label{rsimpaltsGood}
-	If $rs \neq []$ and forall $r \in rs. \textit{nonAlt} \; r$ and $\textit{isDistinct} \; rs$,
-	then $\good \; (\rsimpalts \; rs)$ if and only if forall $r \in rs. \; \good \; r$.
-\end{lemma}
-\noindent
-We also note that
-if a regular expression $r$ is good, then $\rflts$ on the singleton
-list $[r]$ will not break goodness:
-\begin{lemma}\label{flts2}
-	If $\good \; r$, then forall $r' \in \rflts \; [r]. \; \good \; r'$ and $\textit{nonAlt} \; r'$.
-\end{lemma}
-\begin{proof}
-	By an induction on $r$.
-\end{proof}
-\noindent
-The other observation we make about $\rsimp{r}$ is that it never
-comes with nested alternatives, which we describe as the $\nonnested$
-property:
-\begin{center}
-	\begin{tabular}{lcl}
-		$\nonnested \; \, \sum []$ & $\dn$ & $\btrue$\\
-		$\nonnested \; \, \sum ((\sum rs_1) :: rs_2)$ & $\dn$ & $\bfalse$\\
-		$\nonnested \; \, \sum (r :: rs)$ & $\dn$ & $\nonnested (\sum rs)$\\
-		$\nonnested \; \, r $ & $\dn$ & $\btrue$
-	\end{tabular}
-\end{center}
-\noindent
-The $\rflts$ function
-always opens up nested alternatives,
-which enables $\rsimp$ to be non-nested:
-
-\begin{lemma}\label{nonnestedRsimp}
-	$\nonnested \; (\rsimp{r})$
-\end{lemma}
-\begin{proof}
-	By an induction on $r$.
-\end{proof}
-\noindent
-With this we could prove that a regular expressions
-after simplification and flattening and de-duplication,
-will not contain any alternative regular expression directly:
-\begin{lemma}\label{nonaltFltsRd}
-	If $x \in \rdistinct{\rflts\; (\map \; \rsimp{} \; rs)}{\varnothing}$ 
-	then $\textit{nonAlt} \; x$.
-\end{lemma}
-\begin{proof}
-	By \ref{nonnestedRsimp}.
-\end{proof}
-\noindent
-The other thing we know is that once $\rsimp{}$ had finished
-processing an alternative regular expression, it will not
-contain any $\RZERO$s, this is because all the recursive 
-calls to the simplification on the children regular expressions
-make the children good, and $\rflts$ will not take out
-any $\RZERO$s out of a good regular expression list,
-and $\rdistinct{}$ will not mess with the result.
-\begin{lemma}\label{flts3Obv}
-	The following are true:
-	\begin{itemize}
-		\item
-			If for all $r \in rs. \, \good \; r $ or $r = \RZERO$,
-			then for all $r \in \rflts\; rs. \, \good \; r$.
-		\item
-			If $x \in \rdistinct{\rflts\; (\map \; rsimp{}\; rs)}{\varnothing}$
-			and for all $y$ such that $\llbracket y \rrbracket_r$ less than
-			$\llbracket rs \rrbracket_r + 1$, either
-			$\good \; (\rsimp{y})$ or $\rsimp{y} = \RZERO$,
-			then $\good \; x$.
-	\end{itemize}
-\end{lemma}
-\begin{proof}
-	The first part is by induction on $rs$, where the induction
-	rule is the inductive cases for $\rflts$.
-	The second part is a corollary from the first part.
-\end{proof}
-
-And this leads to good structural property of $\rsimp{}$,
-that after simplification, a regular expression is
-either good or $\RZERO$:
-\begin{lemma}\label{good1}
-	For any r-regular expression $r$, $\good \; \rsimp{r}$ or $\rsimp{r} = \RZERO$.
-\end{lemma}
-\begin{proof}
-	By an induction on $r$. The inductive measure is the size $\llbracket \rrbracket_r$.
-	Lemma \ref{rsimpSize} says that 
-	$\llbracket \rsimp{r}\rrbracket_r$ is smaller than or equal to
-	$\llbracket r \rrbracket_r$.
-	Therefore, in the $r_1 \cdot r_2$ and $\sum rs$ case,
-	Inductive hypothesis applies to the children regular expressions
-	$r_1$, $r_2$, etc. The lemma \ref{flts3Obv}'s precondition is satisfied
-	by that as well.
-	The lemmas \ref{nonnestedRsimp} and  \ref{nonaltFltsRd} are used
-	to ensure that goodness is preserved at the topmost level.
-\end{proof}
-We shall prove that any good regular expression is 
-a fixed-point for $\rsimp{}$.
-First we prove an auxiliary lemma:
-\begin{lemma}\label{goodaltsNonalt}
-	If $\good \; \sum rs$, then $\rflts\; rs = rs$.
-\end{lemma}
-\begin{proof}
-	By an induction on $\sum rs$. The inductive rules are the cases
-	for $\good$.
-\end{proof}
-\noindent
-Now we are ready to prove that good regular expressions are invariant
-of $\rsimp{}$ application:
-\begin{lemma}\label{test}
-	If $\good \;r$ then $\rsimp{r} = r$.
-\end{lemma}
-\begin{proof}
-	By an induction on the inductive cases of $\good$, using lemmas
-	\ref{goodaltsNonalt} and \ref{rdistinctOnDistinct}.
-	The lemma \ref{goodaltsNonalt} is used in the alternative
-	case where 2 or more elements are present in the list.
-\end{proof}
-\noindent
-Given below is a property involving $\rflts$, $\rdistinct{}{}$, $\rsimp{}$ and $\rsimp_{ALTS}$,
-which requires $\ref{good1}$ to go through smoothly.
-It says that an application of $\rsimp_{ALTS}$ can be "absorbed",
-if it its output is concatenated with a list and then applied to $\rflts$.
-\begin{lemma}\label{flattenRsimpalts}
-	$\rflts \; ( (\rsimp_{ALTS} \; 
-	(\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing})) :: 
-	\map \; \rsimp{} \; rs' ) = 
-	\rflts \; ( (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing}) @ (
-	\map \; \rsimp{rs'}))$
-
-
-\end{lemma}
-\begin{proof}
-	By \ref{good1}.
-\end{proof}
-\noindent
-
-
-
-
-
-We are also ready to prove that $\textit{rsimp}$ is idempotent.
-\subsubsection{$\rsimp$ is Idempotent}
-The idempotency of $\rsimp$ is very useful in 
-manipulating regular expression terms into desired
-forms so that key steps allowing further rewriting to closed forms
-are possible.
-\begin{lemma}\label{rsimpIdem}
-	$\rsimp{r} = \rsimp{\rsimp{r}}$
-\end{lemma}
-
-\begin{proof}
-	By \ref{test} and \ref{good1}.
-\end{proof}
-\noindent
-This property means we do not have to repeatedly
-apply simplification in each step, which justifies
-our definition of $\blexersimp$.
-
-
-On the other hand, we could repeat the same $\rsimp{}$ applications
-on regular expressions as many times as we want, if we have at least
-one simplification applied to it, and apply it wherever we would like to:
-\begin{corollary}\label{headOneMoreSimp}
-	The following properties hold, directly from \ref{rsimpIdem}:
-
-	\begin{itemize}
-		\item
-			$\map \; \rsimp{(r :: rs)} = \map \; \rsimp{} \; (\rsimp{r} :: rs)$
-		\item
-			$\rsimp{(\RALTS{rs})} = \rsimp{(\RALTS{\map \; \rsimp{} \; rs})}$
-	\end{itemize}
-\end{corollary}
-\noindent
-This will be useful in later closed form proof's rewriting steps.
-Similarly, we point out the following useful facts below:
-\begin{lemma}
-	The following equalities hold if $r = \rsimp{r'}$ for some $r'$:
-	\begin{itemize}
-		\item
-			If $r  = \sum rs$ then $\rsimpalts \; rs = \sum rs$.
-		\item
-			If $r = \sum rs$ then $\rdistinct{rs}{\varnothing} = rs$.
-		\item
-			$\rsimpalts \; (\rdistinct{\rflts \; [r]}{\varnothing}) = r$.
-	\end{itemize}
-\end{lemma}
-\begin{proof}
-	By application of lemmas \ref{rsimpIdem} and \ref{good1}.
-\end{proof}
-
-\noindent
-With the idempotency of $\rsimp{}$ and its corollaries, 
-we can start proving some key equalities leading to the 
-closed forms.
-Now presented are a few equivalent terms under $\rsimp{}$.
-We use $r_1 \sequal r_2 $ here to denote $\rsimp{r_1} = \rsimp{r_2}$.
-\begin{lemma}
-	\begin{itemize}
-		The following equivalence hold:
-	\item
-		$\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$
-	\item
-		$\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$
-	\item
-		$\RALTS{\RALTS{rs}} \sequal \RALTS{rs}$
-	\item
-		$\sum ((\sum rs_a) :: rs_b) \sequal \sum rs_a @ rs_b$
-	\item
-		$\RALTS{rs} = \RALTS{\map \; \rsimp{} \; rs}$
-\end{itemize}
-\end{lemma}
-\begin{proof}
-	By induction on the lists involved.
-\end{proof}
-\noindent
-The above allows us to prove
-two similar equalities (which are a bit more involved).
-It says that we could flatten out the elements
-before simplification and still get the same result.
-\begin{lemma}\label{simpFlatten3}
-	One can flatten the inside $\sum$ of a $\sum$ if it is being 
-	simplified. Concretely,
-	\begin{itemize}
-		\item
-			If for all $r \in rs, rs', rs''$, we have $\good \; r $
-			or $r = \RZERO$, then $\sum (rs' @ rs @ rs'') \sequal 
-			\sum (rs' @ [\sum rs] @ rs'')$ holds. As a corollary,
-		\item
-			$\sum (rs' @ [\sum rs] @ rs'') \sequal \sum (rs' @ rs @ rs'')$
-	\end{itemize}
-\end{lemma}
-\begin{proof}
-	By rewriting steps involving the use of \ref{test} and \ref{rdistinctConcatGeneral}.
-	The second sub-lemma is a corollary of the previous.
-\end{proof}
-%Rewriting steps not put in--too long and complicated-------------------------------
-\begin{comment}
-	\begin{center}
-		$\rsimp{\sum (rs' @ rs @ rs'')}  \stackrel{def of bsimp}{=}$  \\
-		$\rsimpalts \; (\rdistinct{\rflts \; ((\map \; \rsimp{}\; rs') @ (\map \; \rsimp{} \; rs ) @ (\map \; \rsimp{} \; rs''))}{\varnothing})$ \\
-		$\stackrel{by \ref{test}}{=} 
-		\rsimpalts \; (\rdistinct{(\rflts \; rs' @ \rflts \; rs @ \rflts \; rs'')}{
-		\varnothing})$\\
-		$\stackrel{by \ref{rdistinctConcatGeneral}}{=}
-		\rsimpalts \; (\rdistinct{\rflts \; rs'}{\varnothing} @ \rdistinct{(
-		\rflts\; rs @ \rflts \; rs'')}{\rflts \; rs'})$\\
-
-	\end{center}
-\end{comment}
-%Rewriting steps not put in--too long and complicated-------------------------------
-\noindent
 \subsection{Estimating the Closed Forms' sizes}
 We now summarize the closed forms below:
 \begin{itemize}




