--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Mon Jul 04 12:27:13 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Mon Jul 04 12:43:03 2022 +0100
@@ -1046,7 +1046,7 @@
 \end{proof}
 \noindent
 This closed form has a variant which can be more convenient in later proofs:
-\begin{corollary}
+\begin{corollary}{altsClosedForm1}
 	If $s \neq []$ then 
 	$\rderssimp \; (\sum \; rs) \; s = 
 	\rsimp{(\sum \; (\map \; \rderssimp{\_}{s} \; rs))}$.
@@ -1498,8 +1498,7 @@
 \end{proof}
 
 \noindent
-where in (1) the $\textit{Suffix}( r_1, s)$ are the all the suffixes of $s$ where $\rderssimp{ r_1}{s'}$ is nullable ($s'$ being a suffix of $s$).
-The reason why we could write the derivatives of a sequence this way is described in section 2.
+(1) is by the corollary \ref{seqEstimate1}
 The term (2) is used to control (1). 
 That is because one can obtain an overall
 smaller regex list

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ChengsongTanPhdThesis/a_aa_star_bsimp.data	Mon Jul 04 12:43:03 2022 +0100
@@ -0,0 +1,21 @@
+0 6
+1 10
+2 17
+3 17
+4 17
+5 17
+6 17
+7 17
+8 17
+9 17
+10 17
+11 17
+12 17
+13 17
+14 17
+15 17
+16 17
+17 17
+18 17
+19 17
+20 17
\ No newline at end of file