788 

   789 \subsubsection{The $RL$ Function: Language Interpretation of $\textit{Rrexp}$s}

   790 Much like the definition of $L$ on plain regular expressions, one could also 

   791 define the language interpretation of $\rrexp$s.

   792 \begin{center}

   793 	\begin{tabular}{lcl}

   794 		$RL \; (\ZERO)$ & $\dn$ & $\phi$\\

   795 		$RL \; (\ONE)$ & $\dn$ & $\{[]\}$\\

   796 		$RL \; (c)$ & $\dn$ & $\{[c]\}$\\

   797 		$RL \; \sum rs$ & $\dn$ & $ \bigcup_{r \in rs} (RL \; r)$\\

   798 		$RL \; (r_1 \cdot r_2)$ & $\dn$ & $ RL \; (r_1) @ RL \; (r_2)$\\

   799 		$RL \; (r^*)$ & $\dn$ & $ (RL(r))^*$

   800 	\end{tabular}

   801 \end{center}

   802 \noindent

   803 The main use of $RL$ is to establish some connections between $\rsimp{}$ 

   804 and $\rnullable{}$:

   805 \begin{lemma}

   806 	The following properties hold:

   807 	\begin{itemize}

   808 		\item

   809 			If $\rnullable{r}$, then $\rsimp{r} \neq \RZERO$.

   810 		\item

   811 			$\rnullable{r \backslash s} \quad $ if and only if $\quad \rnullable{\rderssimp{r}{s}}$.

   812 	\end{itemize}

   813 \end{lemma}

   814 \begin{proof}

   815 	The first part is by induction on $r$. 

   816 	The second part is true because property 

   817 	\[ RL \; r = RL \; (\rsimp{r})\] holds.

   818 \end{proof}

   819 

   820 \subsubsection{Simplified $\textit{Rrexp}$s are Good}

   821 We formalise the notion of ``good" regular expressions,

   822 which means regular expressions that

   823 are not fully simplified. For alternative regular expressions that means they

   824 do not contain any nested alternatives like 

   825 \[ r_1 + (r_2 + r_3) \], un-removed $\RZERO$s like \[\RZERO + r\]

   826 or duplicate elements in a children regular expression list like \[ \sum [r, r, \ldots]\]:

   827 \begin{center}

   828 	\begin{tabular}{@{}lcl@{}}

   829 		$\good\; \RZERO$ & $\dn$ & $\textit{false}$\\

   830 		$\good\; \RONE$ & $\dn$ & $\textit{true}$\\

   831 		$\good\; \RCHAR{c}$ & $\dn$ & $\btrue$\\

   832 		$\good\; \RALTS{[]}$ & $\dn$ & $\bfalse$\\

   833 		$\good\; \RALTS{[r]}$ & $\dn$ & $\bfalse$\\

   834 		$\good\; \RALTS{r_1 :: r_2 :: rs}$ & $\dn$ & 

   835 		$\textit{isDistinct} \; (r_1 :: r_2 :: rs) \;$\\

   836 						   & & $\textit{and}\; (\forall r' \in (r_1 :: r_2 :: rs).\; \good \; r'\; \,  \textit{and}\; \, \textit{nonAlt}\; r')$\\

   837 		$\good \; \RSEQ{\RZERO}{r}$ & $\dn$ & $\bfalse$\\

   838 		$\good \; \RSEQ{\RONE}{r}$ & $\dn$ & $\bfalse$\\

   839 		$\good \; \RSEQ{r}{\RZERO}$ & $\dn$ & $\bfalse$\\

   840 		$\good \; \RSEQ{r_1}{r_2}$ & $\dn$ & $\good \; r_1 \;\, \textit{and} \;\, \good \; r_2$\\

   841 		$\good \; \RSTAR{r}$ & $\dn$ & $\btrue$\\

   842 	\end{tabular}

   843 \end{center}

   844 \noindent

   845 The predicate $\textit{nonAlt}$ evaluates to true when the regular expression is not an

   846 alternative, and false otherwise.

   847 The $\good$ property is preserved under $\rsimp_{ALTS}$, provided that

   848 its non-empty argument list of expressions are all good themsleves, and $\textit{nonAlt}$, 

   849 and unique:

   850 \begin{lemma}\label{rsimpaltsGood}

   851 	If $rs \neq []$ and forall $r \in rs. \textit{nonAlt} \; r$ and $\textit{isDistinct} \; rs$,

   852 	then $\good \; (\rsimpalts \; rs)$ if and only if forall $r \in rs. \; \good \; r$.

   853 \end{lemma}

   854 \noindent

   855 We also note that

   856 if a regular expression $r$ is good, then $\rflts$ on the singleton

   857 list $[r]$ will not break goodness:

   858 \begin{lemma}\label{flts2}

   859 	If $\good \; r$, then forall $r' \in \rflts \; [r]. \; \good \; r'$ and $\textit{nonAlt} \; r'$.

   860 \end{lemma}

   861 \begin{proof}

   862 	By an induction on $r$.

   863 \end{proof}

   864 \noindent

   865 The other observation we make about $\rsimp{r}$ is that it never

   866 comes with nested alternatives, which we describe as the $\nonnested$

   867 property:

   868 \begin{center}

   869 	\begin{tabular}{lcl}

   870 		$\nonnested \; \, \sum []$ & $\dn$ & $\btrue$\\

   871 		$\nonnested \; \, \sum ((\sum rs_1) :: rs_2)$ & $\dn$ & $\bfalse$\\

   872 		$\nonnested \; \, \sum (r :: rs)$ & $\dn$ & $\nonnested (\sum rs)$\\

   873 		$\nonnested \; \, r $ & $\dn$ & $\btrue$

   874 	\end{tabular}

   875 \end{center}

   876 \noindent

   877 The $\rflts$ function

   878 always opens up nested alternatives,

   879 which enables $\rsimp$ to be non-nested:

   880 

   881 \begin{lemma}\label{nonnestedRsimp}

   882 	$\nonnested \; (\rsimp{r})$

   883 \end{lemma}

   884 \begin{proof}

   885 	By an induction on $r$.

   886 \end{proof}

   887 \noindent

   888 With this we could prove that a regular expressions

   889 after simplification and flattening and de-duplication,

   890 will not contain any alternative regular expression directly:

   891 \begin{lemma}\label{nonaltFltsRd}

   892 	If $x \in \rdistinct{\rflts\; (\map \; \rsimp{} \; rs)}{\varnothing}$ 

   893 	then $\textit{nonAlt} \; x$.

   894 \end{lemma}

   895 \begin{proof}

   896 	By \ref{nonnestedRsimp}.

   897 \end{proof}

   898 \noindent

   899 The other thing we know is that once $\rsimp{}$ had finished

   900 processing an alternative regular expression, it will not

   901 contain any $\RZERO$s, this is because all the recursive 

   902 calls to the simplification on the children regular expressions

   903 make the children good, and $\rflts$ will not take out

   904 any $\RZERO$s out of a good regular expression list,

   905 and $\rdistinct{}$ will not mess with the result.

   906 \begin{lemma}\label{flts3Obv}

   907 	The following are true:

   908 	\begin{itemize}

   909 		\item

   910 			If for all $r \in rs. \, \good \; r $ or $r = \RZERO$,

   911 			then for all $r \in \rflts\; rs. \, \good \; r$.

   912 		\item

   913 			If $x \in \rdistinct{\rflts\; (\map \; rsimp{}\; rs)}{\varnothing}$

   914 			and for all $y$ such that $\llbracket y \rrbracket_r$ less than

   915 			$\llbracket rs \rrbracket_r + 1$, either

   916 			$\good \; (\rsimp{y})$ or $\rsimp{y} = \RZERO$,

   917 			then $\good \; x$.

   918 	\end{itemize}

   919 \end{lemma}

   920 \begin{proof}

   921 	The first part is by induction on $rs$, where the induction

   922 	rule is the inductive cases for $\rflts$.

   923 	The second part is a corollary from the first part.

   924 \end{proof}

   925 

   926 And this leads to good structural property of $\rsimp{}$,

   927 that after simplification, a regular expression is

   928 either good or $\RZERO$:

   929 \begin{lemma}\label{good1}

   930 	For any r-regular expression $r$, $\good \; \rsimp{r}$ or $\rsimp{r} = \RZERO$.

   931 \end{lemma}

   932 \begin{proof}

   933 	By an induction on $r$. The inductive measure is the size $\llbracket \rrbracket_r$.

   934 	Lemma \ref{rsimpSize} says that 

   935 	$\llbracket \rsimp{r}\rrbracket_r$ is smaller than or equal to

   936 	$\llbracket r \rrbracket_r$.

   937 	Therefore, in the $r_1 \cdot r_2$ and $\sum rs$ case,

   938 	Inductive hypothesis applies to the children regular expressions

   939 	$r_1$, $r_2$, etc. The lemma \ref{flts3Obv}'s precondition is satisfied

   940 	by that as well.

   941 	The lemmas \ref{nonnestedRsimp} and  \ref{nonaltFltsRd} are used

   942 	to ensure that goodness is preserved at the topmost level.

   943 \end{proof}

   944 We shall prove that any good regular expression is 

   945 a fixed-point for $\rsimp{}$.

   946 First we prove an auxiliary lemma:

   947 \begin{lemma}\label{goodaltsNonalt}

   948 	If $\good \; \sum rs$, then $\rflts\; rs = rs$.

   949 \end{lemma}

   950 \begin{proof}

   951 	By an induction on $\sum rs$. The inductive rules are the cases

   952 	for $\good$.

   953 \end{proof}

   954 \noindent

   955 Now we are ready to prove that good regular expressions are invariant

   956 of $\rsimp{}$ application:

   957 \begin{lemma}\label{test}

   958 	If $\good \;r$ then $\rsimp{r} = r$.

   959 \end{lemma}

   960 \begin{proof}

   961 	By an induction on the inductive cases of $\good$, using lemmas

   962 	\ref{goodaltsNonalt} and \ref{rdistinctOnDistinct}.

   963 	The lemma \ref{goodaltsNonalt} is used in the alternative

   964 	case where 2 or more elements are present in the list.

   965 \end{proof}

   966 \noindent

   967 Given below is a property involving $\rflts$, $\rdistinct{}{}$, $\rsimp{}$ and $\rsimp_{ALTS}$,

   968 which requires $\ref{good1}$ to go through smoothly.

   969 It says that an application of $\rsimp_{ALTS}$ can be "absorbed",

   970 if it its output is concatenated with a list and then applied to $\rflts$.

   971 \begin{lemma}\label{flattenRsimpalts}

   972 	$\rflts \; ( (\rsimp_{ALTS} \; 

   973 	(\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing})) :: 

   974 	\map \; \rsimp{} \; rs' ) = 

   975 	\rflts \; ( (\rdistinct{(\rflts \; (\map \; \rsimp{}\; rs))}{\varnothing}) @ (

   976 	\map \; \rsimp{rs'}))$

   977 

   978 

   979 \end{lemma}

   980 \begin{proof}

   981 	By \ref{good1}.

   982 \end{proof}

   983 \noindent

   984 

   985 

   986 

   987 

   988 

   989 We are also ready to prove that $\textit{rsimp}$ is idempotent.

   990 \subsubsection{$\rsimp$ is Idempotent}

   991 The idempotency of $\rsimp$ is very useful in 

   992 manipulating regular expression terms into desired

   993 forms so that key steps allowing further rewriting to closed forms

   994 are possible.

   995 \begin{lemma}\label{rsimpIdem}

   996 	$\rsimp{r} = \rsimp{\rsimp{r}}$

   997 \end{lemma}

   998 

   999 \begin{proof}

  1000 	By \ref{test} and \ref{good1}.

  1001 \end{proof}

  1002 \noindent

  1003 This property means we do not have to repeatedly

  1004 apply simplification in each step, which justifies

  1005 our definition of $\blexersimp$.

  1006 

  1007 

  1008 On the other hand, we could repeat the same $\rsimp{}$ applications

  1009 on regular expressions as many times as we want, if we have at least

  1010 one simplification applied to it, and apply it wherever we would like to:

  1011 \begin{corollary}\label{headOneMoreSimp}

  1012 	The following properties hold, directly from \ref{rsimpIdem}:

  1013 

  1014 	\begin{itemize}

  1015 		\item

  1016 			$\map \; \rsimp{(r :: rs)} = \map \; \rsimp{} \; (\rsimp{r} :: rs)$

  1017 		\item

  1018 			$\rsimp{(\RALTS{rs})} = \rsimp{(\RALTS{\map \; \rsimp{} \; rs})}$

  1019 	\end{itemize}

  1020 \end{corollary}

  1021 \noindent

  1022 This will be useful in later closed form proof's rewriting steps.

  1023 Similarly, we point out the following useful facts below:

  1024 \begin{lemma}

  1025 	The following equalities hold if $r = \rsimp{r'}$ for some $r'$:

  1026 	\begin{itemize}

  1027 		\item

  1028 			If $r  = \sum rs$ then $\rsimpalts \; rs = \sum rs$.

  1029 		\item

  1030 			If $r = \sum rs$ then $\rdistinct{rs}{\varnothing} = rs$.

  1031 		\item

  1032 			$\rsimpalts \; (\rdistinct{\rflts \; [r]}{\varnothing}) = r$.

  1033 	\end{itemize}

  1034 \end{lemma}

  1035 \begin{proof}

  1036 	By application of lemmas \ref{rsimpIdem} and \ref{good1}.

  1037 \end{proof}

  1038 

  1039 \noindent

  1040 With the idempotency of $\rsimp{}$ and its corollaries, 

  1041 we can start proving some key equalities leading to the 

  1042 closed forms.

  1043 Now presented are a few equivalent terms under $\rsimp{}$.

  1044 We use $r_1 \sequal r_2 $ here to denote $\rsimp{r_1} = \rsimp{r_2}$.

  1045 \begin{lemma}

  1046 	\begin{itemize}

  1047 		The following equivalence hold:

  1048 	\item

  1049 		$\rsimpalts \; (\RZERO :: rs) \sequal \rsimpalts\; rs$

  1050 	\item

  1051 		$\rsimpalts \; rs \sequal \rsimpalts (\map \; \rsimp{} \; rs)$

  1052 	\item

  1053 		$\RALTS{\RALTS{rs}} \sequal \RALTS{rs}$

  1054 	\item

  1055 		$\sum ((\sum rs_a) :: rs_b) \sequal \sum rs_a @ rs_b$

  1056 	\item

  1057 		$\RALTS{rs} = \RALTS{\map \; \rsimp{} \; rs}$

  1058 \end{itemize}

  1059 \end{lemma}

  1060 \begin{proof}

  1061 	By induction on the lists involved.

  1062 \end{proof}

  1063 \noindent

  1064 The above allows us to prove

  1065 two similar equalities (which are a bit more involved).

  1066 It says that we could flatten out the elements

  1067 before simplification and still get the same result.

  1068 \begin{lemma}\label{simpFlatten3}

  1069 	One can flatten the inside $\sum$ of a $\sum$ if it is being 

  1070 	simplified. Concretely,

  1071 	\begin{itemize}

  1072 		\item

  1073 			If for all $r \in rs, rs', rs''$, we have $\good \; r $

  1074 			or $r = \RZERO$, then $\sum (rs' @ rs @ rs'') \sequal 

  1075 			\sum (rs' @ [\sum rs] @ rs'')$ holds. As a corollary,

  1076 		\item

  1077 			$\sum (rs' @ [\sum rs] @ rs'') \sequal \sum (rs' @ rs @ rs'')$

  1078 	\end{itemize}

  1079 \end{lemma}

  1080 \begin{proof}

  1081 	By rewriting steps involving the use of \ref{test} and \ref{rdistinctConcatGeneral}.

  1082 	The second sub-lemma is a corollary of the previous.

  1083 \end{proof}

  1084 %Rewriting steps not put in--too long and complicated-------------------------------

  1085 \begin{comment}

  1086 	\begin{center}

  1087 		$\rsimp{\sum (rs' @ rs @ rs'')}  \stackrel{def of bsimp}{=}$  \\

  1088 		$\rsimpalts \; (\rdistinct{\rflts \; ((\map \; \rsimp{}\; rs') @ (\map \; \rsimp{} \; rs ) @ (\map \; \rsimp{} \; rs''))}{\varnothing})$ \\

  1089 		$\stackrel{by \ref{test}}{=} 

  1090 		\rsimpalts \; (\rdistinct{(\rflts \; rs' @ \rflts \; rs @ \rflts \; rs'')}{

  1091 		\varnothing})$\\

  1092 		$\stackrel{by \ref{rdistinctConcatGeneral}}{=}

  1093 		\rsimpalts \; (\rdistinct{\rflts \; rs'}{\varnothing} @ \rdistinct{(

  1094 		\rflts\; rs @ \rflts \; rs'')}{\rflts \; rs'})$\\

  1095 

  1096 	\end{center}

  1097 \end{comment}

  1098 %Rewriting steps not put in--too long and complicated-------------------------------

  1099 \noindent

  1100 

  1101