--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Mon Sep 12 23:32:18 2022 +0200
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Thu Sep 22 00:31:09 2022 +0100
@@ -396,43 +396,47 @@
 
 \begin{center}
 	\begin{tabular}{@{}lcl@{}}
-$r \backslash_{rsimps} (c\!::\!s) $ & $\dn$ & $(r \backslash_{rsimp}\, c) \backslash_{rsimps}\, s$ \\
+$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.
+We do not define an r-regular expression version of $\blexersimp$,
+as our proof does not involve its use. 
+Everything about the size of annotated regular expressions
+can be calculated via the size of r-regular expressions:
 \begin{lemma}\label{sizeRelations}
 	The following equalities hold:
 	\begin{itemize}
 		\item
-			$\asize{\bsimp{a}} = \rsize{\rsimp{\rerase{a}}}$
+			$\asize{\bsimps \; a} = \rsize{\rsimp{ \rerase{a}}}$
 		\item
 			$\asize{\bderssimp{a}{s}} =  \rsize{\rderssimp{\rerase{a}}{s}}$
 	\end{itemize}
 \end{lemma}
+\begin{proof}
+	The first part is by induction on the inductive cases
+	of $\textit{bsimp}$.
+	The second part is by induction on the string $s$,
+	where the inductive step follows from part one.
+\end{proof}
 \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.
-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
+we will be able to focus on 
+estimating only
+$\rsize{\rderssimp{\rerase{a}}{s}}$
+in later parts because
+\begin{center}
+	$\rsize{\rderssimp{\rerase{a}}{s}} \leq N_r \quad$
+	implies
+	$\quad \llbracket a \backslash_{bsimps} s \rrbracket \leq N_r$.
+\end{center}
+Unless stated otherwise in the rest of 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
-regular expression.
-
+For the binary alternative r-regular expression $\RALTS{[r_1, r_2]}$,
+we use the notation $r_1 + r_2$
+for brevity.
 
 
 %-----------------------------------
@@ -473,6 +477,31 @@
 %\noindent
 %We explain in detail how we reached those claims.
 \subsection{Basic Properties needed for Closed Forms}
+If we attempt to prove 
+\begin{center}
+	$\forall r. \; \exists N_r.\;\; s.t. \llbracket r\backslash_{bsimps} s \rrbracket_r \leq N_r$
+\end{center}
+using a naive induction on the structure of $r$,
+then we are stuck at the inductive cases such as
+$r_1\cdot r_2$.
+The inductive hypotheses are:
+\begin{center}
+	1: $\text{for } r_1, \text{there exists } N_{r_1}.\;\; s.t. 
+	\;\;\forall s.  \llbracket r_1 \backslash_{bsimps} s \rrbracket_r \leq N_{r_1}. $\\
+	2: $\text{for } r_2, \text{there exists } N_{r_2}.\;\; s.t. 
+	\;\; \forall s. \llbracket r_2 \backslash_{bsimps} s \rrbracket_r \leq N_{r_2}. $
+\end{center}
+The inductive step to prove would be 
+\begin{center}
+	$\text{there exists } N_{r_1\cdot r_2}. \;\; s.t. \forall s. 
+	\llbracket (r_1 \cdot r_2) \backslash_{bsimps} s \rrbracket_r \leq N_{r_1\cdot r_2}.$
+\end{center}
+The problem is that it is not clear what 
+$(r_1\cdot r_2) \backslash_{bsimps} s$ looks like,
+and therefore $N_{r_1}$ and $N_{r_2}$ in the
+inductive hypotheses cannot be directly used.
+
+
 The next steps involves getting a closed form for
 $\rderssimp{r}{s}$ and then obtaining
 an estimate for the closed form.