--- 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