--- a/ChengsongTanPhdThesis/Chapters/Inj.tex	Wed Jun 21 22:43:04 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Inj.tex	Tue Jun 27 01:09:36 2023 +0100
@@ -1346,83 +1346,6 @@
 \]
 \end{property}
 \noindent
-Pictorially, this looks as follows:\\
-\vspace{3mm}
-
-\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}{\xrightarrow{\hspace*{8cm}}}$
-}
-\Longstack{
-	\notate{$r\backslash c$}{1}{$L \; (r\backslash c)=
-	\{\ldots,\;s_1,\;\ldots\}$}
-}\\ 
-\vspace{ 3mm }
-
-The derivatives on regular expression can again be 
-generalised to strings.
-One could compute $r_{start} \backslash s$  and test membership of $s$
-in $L \; r_{start}$ by checking
-whether the empty string is in the language of 
-$r_{end}$ (that is $r_{start}\backslash s$).\\
-
-\vspace{2mm}
-\Longstack{
-	\notate{$r_{start}$}{4}{
-		\Longstack{$L \; r_{start} = \{\ldots, \;$ 
-			\notate{$s$}{1}{$c_1::s_1$} 
-		$, \ldots\} $
-		}
-	} 
-}
-\Longstack{
-	$\stackrel{\backslash c_1}{ \xrightarrow{\hspace*{1.8cm}} }$
-}
-\Longstack{
-	\notate{$r_1$}{3}{
-		$r_1 = r_{start}\backslash c_1$,
-		$L \; r_1 = $
-	\Longstack{
-		$\{ \ldots,\;$  \notate{$s_1$}{1}{$c_2::s_2$} 
-		$,\; \ldots \}$
-	}
-}
-}
-\Longstack{
-	$\stackrel{\backslash c_2}{\xrightarrow{\hspace*{1.8cm}}}$ 
-}
-\Longstack{
-	$r_2$	
-}
-\Longstack{
-	$  \xdashrightarrow{\hspace*{0.3cm} \backslash c_3 \ldots \ldots \ldots \hspace*{0.3cm}} $	
-}
-\Longstack{
-	\notate{$r_{end}$}{1}{
-	$L \; r_{end} = \{\ldots, \; [], \ldots\}$}
-}
-
-
-We have the property that
-\begin{property}
-	$s \in L \; r_{start} \iff [] \in L \; r_{end}$
-\end{property}
-\noindent
 Next, we give the recursive definition of derivative on
 regular expressions so that it satisfies the properties above.
 %The derivative function, written $r\backslash c$,