--- a/ChengsongTanPhdThesis/Chapters/Chapter2.tex	Fri May 27 20:29:54 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Chapter2.tex	Fri May 27 22:37:08 2022 +0100
@@ -900,9 +900,13 @@
 %	SUBSECTION 1
 %-----------------------------------
 \section{Specifications of Certain Functions to be Used}
-To be completed.
-
-
+Here we give some functions' definitions, 
+which we will use later.
+\begin{center}
+\begin{tabular}{ccc}
+$\retrieve \; \ACHAR \, \textit{bs} \, c \; \Char(c) = \textit{bs}
+\end{tabular}
+\end{center}
 
 
 %----------------------------------------------------------------------------------------
@@ -933,11 +937,8 @@
 $\textit{flex} \; r \; f \; s@[c] \; v= \flex \; r \; f\; s \; (\inj \; (r\backslash s) \; c \; v) $
 \end{lemma}
 
-And for $\blexer$ we have something with stepwise properties like $\flex$ as well,
-called $\retrieve$:
-\[
-\retrieve \; \ACHAR \, \textit{bs} \, c \; \Char(c) = \textit{bs}
-\]
+And for $\blexer$ we have a function with stepwise properties like $\flex$ as well,
+called $\retrieve$\ref{retrieveDef}.
 $\retrieve$ takes bit-codes from annotated regular expressions
 guided by a value.
 $\retrieve$ is connected to the $\blexer$ in the following way:

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ChengsongTanPhdThesis/re-chengsong.data	Fri May 27 22:37:08 2022 +0100
@@ -0,0 +1,14 @@
+%% data points for derivative size explosion with bsimp
+0 6
+1 23
+2 195
+3 2691
+4 17897
+5 538719
+6 1080927
+7 8727607
+8 39089493 
+%%21141189
+%%9 26506133
+%%10 32488813
+%%11 39089493
\ No newline at end of file