--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Mon Jul 04 12:50:48 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Mon Jul 04 13:15:18 2022 +0100
@@ -1434,7 +1434,7 @@
 if forall $r \in rs$, $\rsize{r} \leq N$, then the output of 
 $\rdistinct{rs}{\varnothing}$ is a list of regular
 expressions of finite size depending on $N$ only. 
-\begin{corollary}
+\begin{corollary}\label{finiteSizeNCorollary}
 	Assumes that for all $r \in rs. \rsize{r} \leq N$,
 	and the cardinality of $\sizeNregex \; N$ is $c_N$
 	then$\rsize{\rdistinct{rs}{\varnothing}} \leq c*N$.
@@ -1487,28 +1487,24 @@
 \begin{center}
 \begin{tabular}{lcll}
 & & $ \llbracket   \rderssimp{r_1\cdot r_2 }{s} \rrbracket_r $\\
-& $ = $ & $\llbracket \rsimp{(\sum(r_1 \backslash s \cdot r_2 \; \;  :: \; \; 
-\map \; (\lambda s'. r_2\backslash_{rsimp} s') (\vsuf{s}{r})))} \rrbracket_r $ & (1) \\
-& $\leq$ & $\llbracket \rsimp{(\sum(r_1 \backslash s \cdot r_2 ::
-\map \; (\lambda s'. r_2\backslash_{rsimp} s') (\vsuf{s}{r})))} \rrbracket_r $ & (2) \\
-									 
+& $ = $ & $\llbracket \rsimp{(\sum(r_1 \backslash_{rsimp} s \cdot r_2 \; \;  :: \; \; 
+\map \; (r_2\backslash_{rsimp} \_)\; (\vsuf{s}{r})))} \rrbracket_r $ & (1) \\			
+& $\leq$ & $\llbracket \rdistinct{(r_1 \backslash_{rsimp} s \cdot r_2 \; \;  :: \; \; 
+\map \; (r_2\backslash_{rsimp} \_)\; (\vsuf{s}{r}))}{\varnothing} \rrbracket_r  + 1$ & (2) \\
+										     & $\leq$ & $2 + N_1 + \rsize{r_2} + (N_2 * (card\;(\sizeNregex \; N_2)))$ & (3)\\
+$\rsize{(r_1 \cdot r_2) \backslash_r s}$& $\leq$ & $max \; (2 + N_1 + \llbracket r_2 \rrbracket_r + N_2 * (card\; (\sizeNregex \; N_2))) \; \rsize{r_1\cdot r_2}$ & (4)
 \end{tabular}
 \end{center}
+\noindent
+(1) is by the corollary \ref{seqEstimate1}.
+(2) is by \ref{altsSimpControl}.
+(3) is by \ref{finiteSizeNCorollary}.
+(4) is by splitting the case when $s = []$ and $s \neq []$.
 
+We reason similarly for  $\STAR$.\medskip
 \end{proof}
 
 \noindent
-(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
-by flattening it and removing $\ZERO$s first before applying $\distinctWith$ on it.
-Section 3 is dedicated to its proof.
-In (3) we know that  $\llbracket \ASEQ{bs}{(\rderssimp{ r_1}{s}}{r_2}\rrbracket$ is 
-bounded by $N_1 + \llbracket{}r_2\rrbracket + 1$. In (5) we know the list comprehension contains only regular expressions of size smaller
-than $N_2$. The list length after  $\distinctWith$ is bounded by a number, which we call $l_{N_2}$. It stands
-for the number of distinct regular expressions smaller than $N_2$ (there can only be finitely many of them).
-We reason similarly for  $\STAR$.\medskip
 
 %-----------------------------------
 %	SECTION 2