--- a/ChengsongTanPhdThesis/Chapters/Cubic.tex	Fri Sep 02 19:35:55 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Cubic.tex	Sat Sep 03 00:14:20 2022 +0100
@@ -572,5 +572,32 @@
 %----------------------------------------------------------------------------------------
 
 \section{Bounded Repetitions}
+We define for the $r^{n}$ constructor something similar to $\starupdate$
+and $\starupdates$:
+\begin{center}
+	\begin{tabular}{lcl}
+		$\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
+		$\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
+						     & & $\textit{if} \; 
+						     (\rnullable \; (\rders \; r \; s))$ \\
+						     & & $\textit{then} \;\; (s @ [c]) :: [c] :: (
+						     \starupdate \; c \; r \; Ss)$ \\
+						     & & $\textit{else} \;\; (s @ [c]) :: (
+						     \starupdate \; c \; r \; Ss)$
+	\end{tabular}
+\end{center}
+\noindent
+As a generalisation from characters to strings,
+$\starupdates$ takes a string instead of a character
+as the first input argument, and is otherwise the same
+as $\starupdate$.
+\begin{center}
+	\begin{tabular}{lcl}
+		$\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\
+		$\starupdates \; (c :: cs) \; r \; Ss$ &  $=$ &  $\starupdates \; cs \; r \; (
+		\starupdate \; c \; r \; Ss)$
+	\end{tabular}
+\end{center}
+\noindent
 
 

--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Fri Sep 02 19:35:55 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Sat Sep 03 00:14:20 2022 +0100
@@ -354,27 +354,53 @@
 and the flatten function for $\rrexp$s:
  \begin{center}
   \begin{tabular}{@{}lcl@{}}
-  $\textit{rflts} \; (_{bs}\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \;
-     (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{rflts} \; as' $ \\
+  $\textit{rflts} \; (\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $as \; @ \; \textit{rflts} \; as' $ \\
   $\textit{rflts} \; \ZERO :: as'$ & $\dn$ & $ \textit{rflts} \;  \textit{as'} $ \\
     $\textit{rflts} \; a :: as'$ & $\dn$ & $a :: \textit{rflts} \; \textit{as'}$ \quad(otherwise) 
 \end{tabular}    
 \end{center}  
 \noindent
-
 one can chain together all the other modules
-of $\bsimp{\_}$ (removing the functionalities related to bit-sequences)
-and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$.
+such as $\rsimpalts$:
+\begin{center}
+  \begin{tabular}{@{}lcl@{}}
+	  $\rsimpalts \;\; nil$ & $\dn$ & $\RZERO$\\
+	  $\rsimpalts \;\; r::nil$ & $\dn$ & $r$\\
+	  $\rsimpalts \;\; rs$ & $\dn$ & $\sum rs$\\
+\end{tabular}    
+\end{center}  
+\noindent
+and $\rsimpseq$:
+\begin{center}
+  \begin{tabular}{@{}lcl@{}}
+	  $\rsimpseq \;\; \RZERO \; \_ $ &   $=$ &   $\RZERO$\\
+	  $\rsimpseq \;\; \_ \; \RZERO $ &   $=$ &   $\RZERO$\\
+	  $\rsimpseq \;\; \RONE \cdot r_2$ & $\dn$ & $r_2$\\
+	  $\rsimpseq \;\; r_1 r_2$ & $\dn$ & $r_1 \cdot r_2$\\
+\end{tabular}    
+\end{center}  
+and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$:
 \begin{center}
   \begin{tabular}{@{}lcl@{}}
    
-	  $\textit{rsimp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ \textit{rsimp}_{ASEQ} \; bs \;(\textit{rsimp} \; a_1) \; (\textit{rsimp}  \; a_2)  $ \\
-	  $\textit{rsimp} \; (_{bs}\sum \textit{as})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; as)) \; \rerases \; \varnothing) $ \\
-   $\textit{rsimp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$   
+	  $\textit{rsimp} \; (r_1\cdot r_2)$ & $\dn$ & $ \textit{rsimp}_{SEQ} \; bs \;(\textit{rsimp} \; r_1) \; (\textit{rsimp}  \; r_2)  $ \\
+	  $\textit{rsimp} \; (_{bs}\sum \textit{rs})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; rs)) \; \rerases \; \varnothing) $ \\
+   $\textit{rsimp} \; r$ & $\dn$ & $\textit{r} \qquad \textit{otherwise}$   
 \end{tabular}    
 \end{center} 
-We omit these functions, as they are routine. Please refer to the formalisation
-(in file BasicIdentities.thy) for the exact definition.
+\begin{center}
+	\begin{tabular}{@{}lcl@{}}
+		$r\backslash_{rsimp} \, c$ & $\dn$ & $\rsimp \; (r\backslash_r \, c)$
+	\end{tabular}
+\end{center}
+
+\begin{center}
+	\begin{tabular}{@{}lcl@{}}
+$r \backslash_{rsimps} (c\!::\!s) $ & $\dn$ & $(r \backslash_{rsimp}\, c) \backslash_{rsimps}\, s$ \\
+$r \backslash_{rsimps} [\,] $ & $\dn$ & $r$
+	\end{tabular}
+\end{center}
+\noindent
 With $\rrexp$ the size caclulation of annotated regular expressions'
 simplification and derivatives can be done by the size of their unlifted 
 counterpart with the unlifted version of simplification and derivatives applied.
@@ -384,14 +410,24 @@
 		\item
 			$\asize{\bsimp{a}} = \rsize{\rsimp{\rerase{a}}}$
 		\item
-			$\asize{\bderssimp{r}{s}} =  \rsize{\rderssimp{\rerase{r}}{s}}$
+			$\asize{\bderssimp{a}{s}} =  \rsize{\rderssimp{\rerase{a}}{s}}$
 	\end{itemize}
 \end{lemma}
 \noindent
+With lemma \ref{sizeRelations},
+a bound on $\rsize{\rderssimp{\rerase{a}}{s}}$
+\[
+	\llbracket \rderssimp{a}{s} \rrbracket_r \leq N_r
+\]
+\noindent
+would apply to $\asize{\bderssimp{a}{s}}$ as well.
+\[
+	\llbracket a \backslash_{bsimps} s \rrbracket \leq N_r.
+\]
 In the following content, we will focus on $\rrexp$'s size bound.
-We will piece together this bound and show the same bound for annotated regular 
-expressions in the end.
-Unless stated otherwise in this chapter all $\textit{rexp}$s without
+Whatever bounds we proved for $ \rsize{\rderssimp{\rerase{r}}{s}}$  
+will automatically apply to $\asize{\bderssimp{r}{s}}$.\\
+Unless stated otherwise in this chapter all regular expressions without
 bitcodes are seen as $\rrexp$s.
 We also use $r_1 + r_2$ and $\RALTS{[r_1, r_2]}$ interchageably
 as the former suits people's intuitive way of stating a binary alternative
@@ -400,57 +436,46 @@
 
 
 %-----------------------------------
-%	SECTION ?
+%	SUB SECTION ROADMAP RREXP BOUND
 %-----------------------------------
-\subsection{Finiteness Proof Using $\rrexp$s}
-Now that we have defined the $\rrexp$ datatype, and proven that its size changes
-w.r.t derivatives and simplifications mirrors precisely those of annotated regular expressions,
-we aim to bound the size of $r \backslash s$ for any $\rrexp$  $r$.
-Once we have a bound like: 
-\[
-	\llbracket r \backslash_{rsimp} s \rrbracket_r \leq N_r
-\]
-\noindent
-we could easily extend that to 
-\[
-	\llbracket a \backslash_{bsimps} s \rrbracket \leq N_r.
-\]
 
-\subsection{Roadmap to a Bound for $\textit{Rrexp}$}
+%\subsection{Roadmap to a Bound for $\textit{Rrexp}$}
 
-The way we obtain the bound for $\rrexp$s is by two steps:
-\begin{itemize}
-	\item
-		First, we rewrite $r\backslash s$ into something else that is easier
-		to bound. This step is especially important for the inductive case 
-		$r_1 \cdot r_2$ and $r^*$, where the derivative can grow and bloat in a wild way,
-		but after simplification they will always be equal or smaller to a form consisting of an alternative
-		list of regular expressions $f \; (g\; (\sum rs))$ with some functions applied to it, where each element will be distinct after the function application.
-	\item
-		Then, for such a sum  list of regular expressions $f\; (g\; (\sum rs))$, we can control its size
-		by estimation, since $\distinctBy$ and $\flts$ are well-behaved and working together would only 
-		reduce the size of a regular expression, not adding to it.
-\end{itemize}
-
-\section{Step One: Closed Forms}
-We transform the function application $\rderssimp{r}{s}$
-into an equivalent 
-form $f\; (g \; (\sum rs))$.
-The functions $f$ and $g$ can be anything from $\flts$, $\distinctBy$ and other helper functions from $\bsimp{\_}$.
-This way we get a different but equivalent way of expressing : $r\backslash s = f \; (g\; (\sum rs))$, we call the
-right hand side the "closed form" of $r\backslash s$.
-
-\begin{quote}\it
-	Claim: For regular expressions $r_1 \cdot r_2$, we claim that
-	\begin{center}
-		$ \rderssimp{r_1 \cdot r_2}{s} = 
-		\rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r2}{\_} \;(\vsuf{s}{r_1})))}$
-	\end{center}
-\end{quote}
-\noindent
-We explain in detail how we reached those claims.
+%The way we obtain the bound for $\rrexp$s is by two steps:
+%\begin{itemize}
+%	\item
+%		First, we rewrite $r\backslash s$ into something else that is easier
+%		to bound. This step is especially important for the inductive case 
+%		$r_1 \cdot r_2$ and $r^*$, where the derivative can grow and bloat in a wild way,
+%		but after simplification they will always be equal or smaller to a form consisting of an alternative
+%		list of regular expressions $f \; (g\; (\sum rs))$ with some functions applied to it, where each element will be distinct after the function application.
+%	\item
+%		Then, for such a sum  list of regular expressions $f\; (g\; (\sum rs))$, we can control its size
+%		by estimation, since $\distinctBy$ and $\flts$ are well-behaved and working together would only 
+%		reduce the size of a regular expression, not adding to it.
+%\end{itemize}
+%
+%\section{Step One: Closed Forms}
+%We transform the function application $\rderssimp{r}{s}$
+%into an equivalent 
+%form $f\; (g \; (\sum rs))$.
+%The functions $f$ and $g$ can be anything from $\flts$, $\distinctBy$ and other helper functions from $\bsimp{\_}$.
+%This way we get a different but equivalent way of expressing : $r\backslash s = f \; (g\; (\sum rs))$, we call the
+%right hand side the "closed form" of $r\backslash s$.
+%
+%\begin{quote}\it
+%	Claim: For regular expressions $r_1 \cdot r_2$, we claim that
+%	\begin{center}
+%		$ \rderssimp{r_1 \cdot r_2}{s} = 
+%		\rsimp{(\sum (r_1 \backslash s \cdot r_2 ) \; :: \;(\map \; \rderssimp{r2}{\_} \;(\vsuf{s}{r_1})))}$
+%	\end{center}
+%\end{quote}
+%\noindent
+%We explain in detail how we reached those claims.
 \subsection{Basic Properties needed for Closed Forms}
-
+The next steps involves getting a closed form for
+$\rderssimp{r}{s}$ and then obtaining
+an estimate for the closed form.
 \subsubsection{$\textit{rdistinct}$'s Deduplicates Successfully}
 The $\textit{rdistinct}$ function, as its name suggests, will
 remove duplicates in an \emph{r}$\textit{rexp}$ list, 

--- a/ChengsongTanPhdThesis/Chapters/Introduction.tex	Fri Sep 02 19:35:55 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex	Sat Sep 03 00:14:20 2022 +0100
@@ -20,7 +20,7 @@
 \newcommand\sflat[1]{\llparenthesis #1 \rrparenthesis }
 \newcommand{\ASEQ}[3]{\textit{ASEQ}_{#1} \, #2 \, #3}
 \newcommand{\bderssimp}[2]{#1 \backslash_{bsimps} #2}
-\newcommand{\rderssimp}[2]{#1 \backslash_{rsimp} #2}
+\newcommand{\rderssimp}[2]{#1 \backslash_{rsimps} #2}
 \def\derssimp{\textit{ders}\_\textit{simp}}
 \def\rders{\textit{rders}}
 \newcommand{\bders}[2]{#1 \backslash #2}
@@ -137,6 +137,9 @@
 \def\rflts{\textit{rflts}}
 \def\rrewrite{\textit{rrewrite}}
 \def\bsimpalts{\textit{bsimp}_{ALTS}}
+\def\bsimpaseq{\textit{bsimp}_{ASEQ}}
+\def\rsimlalts{\textit{rsimp}_{ALTs}}
+\def\rsimpseq{\textit{rsimp}_{SEQ}}
 
 \def\erase{\textit{erase}}
 \def\STAR{\textit{STAR}}