diff -r 2072a8d54e3e -r ae6010c14e49 ChengsongTanPhdThesis/Chapters/Finite.tex
--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Sun Nov 06 23:06:10 2022 +0000
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Mon Nov 07 21:31:07 2022 +0000
@@ -370,6 +370,14 @@
 \end{center}  
 \noindent
 where we omit the definition of $\textit{rnullable}$.
+The generalisation from derivative w.r.t to character to
+derivative w.r.t string is given as
+\begin{center}
+	\begin{tabular}{lcl}
+		$r \backslash_{rs} []$ & $\dn$ & $r$\\
+		$r \backslash_{rs} c::s$ & $\dn$ & $(r\backslash_r c) \backslash_{rs} s$
+	\end{tabular}
+\end{center}
 
 The function $\distinctBy$ for r-regular expressions does not need 
 a function checking equivalence because
@@ -778,7 +786,7 @@
 
 \subsubsection{The Properties of $\textit{Rflts}$} 
 We give in this subsection some properties
-involving $\backslash_r$, $\backslash_{rsimp}$, $\textit{rflts}$ and 
+involving $\backslash_r$, $\backslash_{rsimps}$, $\textit{rflts}$ and 
 $\textit{rsimp}_{ALTS} $, together with any non-trivial lemmas that lead to them.
 These will be helpful in later closed form proofs, when
 we want to transform derivative terms which have
@@ -1430,7 +1438,7 @@
 	As corollaries of \ref{insideSimpRemoval}, we have
 	\begin{itemize}
 		\item
-			If $s \neq []$ then $\rderssimp{r}{s} = \rsimp{(\rders \; r \; s)}$.
+			If $s \neq []$ then $\rderssimp{r}{s} = \rsimp{( r \backslash_{rs} s)}$.
 		\item
 			$\rsimpalts \; (\map \; (\_ \backslash_r x) \;
 			(\rdistinct{rs}{\varnothing})) \sequal
@@ -1844,7 +1852,7 @@
 		$\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
 		$\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
 						     & & $\textit{if} \; 
-						     (\rnullable \; (\rders \; r \; s))$ \\
+						     (\rnullable \; (r \backslash_{rs} s))$ \\
 						     & & $\textit{then} \;\; (s @ [c]) :: [c] :: (
 						     \starupdate \; c \; r \; Ss)$ \\
 						     & & $\textit{else} \;\; (s @ [c]) :: (
@@ -2034,7 +2042,7 @@
 	of the shape $\sum_{s' \in sS} (r\backslash_r s') \cdot r^*$,
 	where $sS = \starupdates \; s \; r \; [[c]]$. Namely,
 	\begin{center}
-		$\hflataux{(\rders{( (\rder{c}{r_0})\cdot(r_0^*))}{s})} = 
+	$\hflataux{(( (\rder{c}{r_0})\cdot(r_0^*))\backslash_{rs} s)} = 
 		\map \; (\lambda s_1. (r_0 \backslash_r s_1) \cdot (r_0^*)) \; 
 		(\starupdates \; s \; r_0 \; [[c]])$
 	\end{center}
@@ -2095,7 +2103,7 @@
 			\sum \; ( ( \sum (\lambda s. (r\backslash_r s) \cdot r^*) \; (
 			\starupdates \; s \; r \; [ c::[]] ) ) )$
 		\item
-			$r \backslash_{rsimp} (c::s) = \textit{rsimp} \; ( (
+			$r \backslash_{rsimps} (c::s) = \textit{rsimp} \; ( (
 			\sum ( (\map \; (\lambda s_1. (r\backslash s_1) \; r^*) \;
 			(\starupdates \;s \; r \; [ c::[] ])))))$
 		\item
@@ -2113,7 +2121,7 @@
 			s \; r \; [ c::[] ])))))$\\
 			$\sequal$\\
 			$( ( \sum ( ( \map \ (\lambda s. \;\;
-			( r \backslash_{rsimp} s)) \cdot r^*) \; (\starupdates \;
+			( r \backslash_{rsimps} s)) \cdot r^*) \; (\starupdates \;
 			s \; r \; [ c::[] ]))))$\\
 	\end{itemize}
 \end{lemma}
@@ -2483,10 +2491,10 @@
 	\begin{center}
 		\begin{tabular}{lcll}
 & & $ \llbracket   \rderssimp{r_1\cdot r_2 }{s} \rrbracket_r $\\
-& $ = $ & $\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) \\
+& $ = $ & $\llbracket \rsimp{(\sum(r_1 \backslash_{rsimps} s \cdot r_2 \; \;  :: \; \; 
+		\map \; (r_2\backslash_{rsimps} \_)\; (\vsuf{s}{r})))} \rrbracket_r $ & (1) \\			
+										     & $\leq$ & $\llbracket \rdistinct{(r_1 \backslash_{rsimps} s \cdot r_2 \; \;  :: \; \; 
+	\map \; (r_2\backslash_{rsimps} \_)\; (\vsuf{s}{r}))}{\varnothing} \rrbracket_r  + 1$ & (2) \\
 											     & $\leq$ & $2 + N_1 + \rsize{r_2} + (N_2 * (card\;(\sizeNregex \; N_2)))$ & (3)\\
 \end{tabular}
 \end{center}
@@ -2514,12 +2522,12 @@
 \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\; 
+& $ = $ & $\llbracket \rsimp{(\sum (\map \; (\lambda s. (r \backslash_{rsimps} s) \cdot r^*) \; (\starupdates\; 
 	cs \; r \; [[c]] )) )} \rrbracket_r $ & (5) \\			
 					      & $\leq$ & $\llbracket 
 					      \rdistinct{
 						      (\map \; 
-						      (\lambda s. (r \backslash_{rsimp} s) \cdot r^*) \; 
+						      (\lambda s. (r \backslash_{rsimps} s) \cdot r^*) \; 
 						      (\starupdates\; cs \; r \; [[c]] )
 					      )}
 	{\varnothing} \rrbracket_r  + 1$ & (6) \\
@@ -2547,8 +2555,8 @@
 \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) \\
+& $ = $ & $\llbracket \rsimp{(\sum (\map \; (\_ \backslash_{rsimps} s)  \; rs) )} \rrbracket_r $ & (9) \\			
+& $\leq$ & $\llbracket (\sum (\map \; (\_ \backslash_{rsimps} s)  \; rs) ) \rrbracket_r $  & (10) \\
 & $\leq$ & $1 + N * (length \; rs) $ & (11)\\
 	\end{tabular}
 \end{center}