diff -r 4e195992ef41 -r 947cbbd4e4a7 ChengsongTanPhdThesis/Chapters/Chapter2.tex
--- 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: