diff -r 3e1b699696b6 -r f47fc4840579 ChengsongTanPhdThesis/Chapters/Inj.tex
--- a/ChengsongTanPhdThesis/Chapters/Inj.tex	Fri Aug 12 00:39:23 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Inj.tex	Sun Aug 14 09:44:27 2022 +0100
@@ -102,9 +102,37 @@
 However, for the purposes here, the $\textit{Ders}$ definition with 
 a single string is sufficient.
 
+The reason for defining derivatives
+is that it provides a different approach
+to test membership of a string in 
+a set of strings. 
+For example, to test whether the string
+$bar$ is contained in the set $\{foo, bar, brak\}$, one takes derivative of the set with
+respect to the string $bar$:
+\begin{center}
+\begin{tabular}{lclll}
+	$S = \{foo, bar, brak\}$ & $ \stackrel{\backslash b}{\rightarrow }$ & 
+	$\{ar, rak\}$ & 
+	$\stackrel{\backslash a}{\rightarrow}$ &
+	\\
+	$\{r \}$ & $\stackrel{\backslash r}{\rightarrow}$ & $\{[]\}$ &
+	$\stackrel{[] \in S \backslash bar}{\longrightarrow}$ & $bar \in S$\\
+\end{tabular}	
+\end{center}
+\noindent
+and in the end test whether the set
+has the empty string \footnote{ we use the infix notation $A\backslash c$
+	instead of $\Der \; c \; A$ for brevity, as it is clear we are operating
+on languages rather than regular expressions }.
+In general, if we have a language $S_{start}$,
+then we can test whether $s$ is in $S_{start}$
+by testing whether $[] \in S \backslash s$.
+
 With the sequencing, Kleene star, and $\textit{Der}$ operator on languages,
 we have a  few properties of how the language derivative can be defined using 
 sub-languages.
+For example, for the sequence operator, we have
+something similar to the ``chain rule'' of the calculus derivative:
 \begin{lemma}
 \[
 	\Der \; c \; (A @ B) =
@@ -198,13 +226,95 @@
 %all strings in that set, Brzozowski defined a derivative operation on regular expressions
 %so that after derivative $L(r\backslash c)$ 
 %will look as if it was obtained by doing a language derivative on $L(r)$:
-Recall that the semantic derivative acts on a set of 
-strings. Brzozowski noticed that this operation
+Recall that the semantic derivative acts on a 
+language (set of strings).
+One can decide whether a string $s$ belongs
+to a language $S$ by taking derivative with respect to
+that string and then checking whether the empty 
+string is in the derivative:
+\begin{center}
+\parskip \baselineskip
+\def\myupbracefill#1{\rotatebox{90}{\stretchto{\{}{#1}}}
+\def\rlwd{.5pt}
+\newcommand\notate[3]{%
+  \unskip\def\useanchorwidth{T}%
+  \setbox0=\hbox{#1}%
+  \def\stackalignment{c}\stackunder[-6pt]{%
+    \def\stackalignment{c}\stackunder[-1.5pt]{%
+      \stackunder[-2pt]{\strut #1}{\myupbracefill{\wd0}}}{%
+    \rule{\rlwd}{#2\baselineskip}}}{%
+  \strut\kern7pt$\hookrightarrow$\rlap{ \footnotesize#3}}\ignorespaces%
+}
+\Longstack{
+\notate{$\{ \ldots ,\;$ 
+	\notate{s}{1}{$(c_1 :: s_1)$} 
+	$, \; \ldots \}$ 
+}{1}{$S_{start}$} 
+}
+\Longstack{
+	$\stackrel{\backslash c_1}{\longrightarrow}$
+}
+\Longstack{
+	$\{ \ldots,\;$  \notate{$s_1$}{1}{$(c_2::s_2)$} 
+	$,\; \ldots \}$
+}
+\Longstack{
+	$\stackrel{\backslash c_2}{\longrightarrow}$ 
+}
+\Longstack{
+	$\{ \ldots,\;  s_2
+	,\; \ldots \}$
+}
+\Longstack{
+	$ \xdashrightarrow{\backslash c_3\ldots\ldots} $	
+}
+\Longstack{
+	\notate{$\{\ldots, [], \ldots\}$}{1}{$S_{end} = 
+	S_{start}\backslash s$}
+}
+\end{center}
+\begin{center}
+	$s \in S_{start} \iff [] \in S_{end}$
+\end{center}
+\noindent
+Brzozowski noticed that this operation
 can be ``mirrored" on regular expressions which
 he calls the derivative of a regular expression $r$
 with respect to a character $c$, written
-$r \backslash c$.
-He defined this operation such that the following property holds:
+$r \backslash c$. This infix operator
+takes an original regular expression $r$ as input
+and a character as a right operand and
+outputs a result, which is a new regular expression.
+The derivative operation on regular expression
+is defined such that the language of the derivative result 
+coincides with the language of the original 
+regular expression's language being taken the language 
+derivative with respect to the same character:
+\begin{center}
+\parskip \baselineskip
+\def\myupbracefill#1{\rotatebox{90}{\stretchto{\{}{#1}}}
+\def\rlwd{.5pt}
+\newcommand\notate[3]{%
+  \unskip\def\useanchorwidth{T}%
+  \setbox0=\hbox{#1}%
+  \def\stackalignment{c}\stackunder[-6pt]{%
+    \def\stackalignment{c}\stackunder[-1.5pt]{%
+      \stackunder[-2pt]{\strut #1}{\myupbracefill{\wd0}}}{%
+    \rule{\rlwd}{#2\baselineskip}}}{%
+  \strut\kern8pt$\hookrightarrow$\rlap{ \footnotesize#3}}\ignorespaces%
+}
+\Longstack{
+	\notate{$r$}{1}{$L \; r = \{\ldots, \;c::s_1, 
+\;\ldots\}$}
+}
+\Longstack{
+	$\stackrel{\backslash c}{\longrightarrow}$
+}
+\Longstack{
+	\notate{$r\backslash c$}{2}{$L \; (r\backslash c)=
+	\{\ldots,\;s_1,\;\ldots\}$}
+}
+\end{center}
 \begin{center}
 
 \[
@@ -212,6 +322,10 @@
 \]
 \end{center}
 \noindent
+where we do derivatives on the regular expression
+$r$ and test membership of $s$ by checking
+whether the empty string is in the language of 
+$r\backslash s$.
 For example in the sequence case we have 
 \begin{center}
 	\begin{tabular}{lcl}