# HG changeset patch
# User Chengsong
# Date 1656978126 -3600
# Node ID 57e33978e55d5e8863f6b9d9611ca0755e4aa796
# Parent  486fb297ac7c60a94d4add5f18c8d73401dbfab6
more

diff -r 486fb297ac7c -r 57e33978e55d ChengsongTanPhdThesis/Chapters/Finite.tex
--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Mon Jul 04 13:15:18 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Tue Jul 05 00:42:06 2022 +0100
@@ -1481,8 +1481,11 @@
 We prove this by induction on $r$. The base cases for $\RZERO$,
 $\RONE $ and $\RCHAR{c}$ are straightforward. 
 In the sequence $r_1 \cdot r_2$ case,
-the inductive hypotheses state $\exists N_1. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N_1$ and
-$\exists N_2. \forall s. \; \llbracket \rderssimp{r_2}{s} \rrbracket \leq N_2$. We can reason as follows
+the inductive hypotheses state 
+$\exists N_1. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N_1$ and
+$\exists N_2. \forall s. \; \llbracket \rderssimp{r_2}{s} \rrbracket \leq N_2$. 
+
+When the string $s$ is not empty, we can reason as follows
 %
 \begin{center}
 \begin{tabular}{lcll}
@@ -1492,16 +1495,81 @@
 & $\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 []$.
+
+
+Combining the cases when $s = []$ and $s \neq []$, we get (4):
+\begin{center}
+	\begin{tabular}{lcll}
+		$\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}
 
-We reason similarly for  $\STAR$.\medskip
+We reason similarly for  $\STAR$.
+The inductive hypothesis is
+$\exists N. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N$.
+Let $\n_r = \llbracket r^* \rrbracket_r$.
+When $s = c :: cs$ is not empty,
+\begin{center}
+\begin{tabular}{lcll}
+& & $ \llbracket   \rderssimp{r^* }{c::cs} \rrbracket_r $\\
+& $ = $ & $\llbracket \rsimp{(\sum (\map \; (\lambda s. (r \backslash_{rsimp} s) \cdot r^*) \; (\starupdates\; 
+cs \; r \; [[c]] )) )} \rrbracket_r $ & (5) \\			
+& $\leq$ & $\llbracket 
+\rdistinct{
+	(\map \; 
+		(\lambda s. (r \backslash_{rsimp} s) \cdot r^*) \; 
+		(\starupdates\; cs \; r \; [[c]] )
+	)}
+	{\varnothing} \rrbracket_r  + 1$ & (6) \\
+					 & $\leq$ & $1 + (\textit{card} (\sizeNregex \; (N + n_r)))
+	* (1 + (N + n_r)) $ & (7)\\
+\end{tabular}
+\end{center}
+\noindent
+(5) is by the lemma  \ref{starClosedForm}.
+(6) is by \ref{altsSimpControl}.
+(7) is by \ref{finiteSizeNCorollary}.
+Combining with the case when $s = []$, one gets
+\begin{center}
+\begin{tabular}{lcll}
+	$\rsize{r^* \backslash_r s}$ & $\leq$ & $max \; n_r \; 1 + (\textit{card} (\sizeNregex \; (N + n_r)))
+	* (1 + (N + n_r)) $ & (8)\\
+\end{tabular}
+\end{center}
+\noindent
+
+The alternative case is slightly less involved.
+The inductive hypothesis 
+is equivalent to $\exists N. \forall r \in (\map \; (\_ \backslash_r s) \; rs). \rsize{r} \leq N$.
+In the case when $s = c::cs$, we have 
+\begin{center}
+\begin{tabular}{lcll}
+& & $ \llbracket   \rderssimp{\sum rs }{c::cs} \rrbracket_r $\\
+& $ = $ & $\llbracket \rsimp{(\sum (\map \; (\_ \backslash_{rsimp} s)  \; rs) )} \rrbracket_r $ & (9) \\			
+& $\leq$ & $\llbracket (\sum (\map \; (\_ \backslash_{rsimp} s)  \; rs) ) \rrbracket_r $  & (10) \\
+& $\leq$ & $1 + N * (length \; rs) $ & (11)\\
+\end{tabular}
+\end{center}
+\noindent
+(9) is by \ref{altsClosedForm}, (10) by \ref{rsimpSize} and (11) by inductive hypothesis.
+
+Combining with the case when $s = []$, one gets
+\begin{center}
+\begin{tabular}{lcll}
+	$\rsize{\sum rs \backslash_r s}$ & $\leq$ & $max \; \rsize{\sum rs} \; 1+N*(length \; rs)$ 
+	 & (12)\\
+\end{tabular}
+\end{center}
+(4), (8), and (12) are all the inductive cases proven.
 \end{proof}
 
 \noindent