--- a/ChengsongTanPhdThesis/Chapters/Cubic.tex	Fri Dec 30 01:52:32 2022 +0000
+++ b/ChengsongTanPhdThesis/Chapters/Cubic.tex	Fri Dec 30 17:37:51 2022 +0000
@@ -27,14 +27,13 @@
 size bound from the previous chapter can be 
 improved to a cubic bound.
 We implemented our conjecture in Scala.
-We intend to formalise this part in Isabelle/HOL at a
-later stage.
+We have not formalised this part in Isabelle/HOL. 
 %we have not been able to finish due to time constraints of the PhD.
 Nevertheless, we outline the ideas we intend to use for the proof.
 
 \section{A Stronger Version of Simplification}
 
-We present further improvements
+Let us first present further improvements
 for our lexer algorithm $\blexersimp$.
 We devise a stronger simplification algorithm,
 called $\bsimpStrong$, which can prune away
@@ -70,7 +69,8 @@
 	aa \cdot a^*+ a \cdot a^* + aa\cdot a^*
 \]
 contains three terms, 
-expressing three possibilities for how it can match some input.
+expressing three possibilities for how it can match some more
+input of the form $a \ldots a$.
 The first and the third terms are identical, which means we can eliminate
 the latter as it will not contribute to a POSIX value.
 In $\bsimps$, the $\distinctBy$ function takes care of 
@@ -302,7 +302,11 @@
 
 \end{lstlisting}
 \caption{The helper functions of $\textit{prune}$: 
-  $\textit{atMostEmpty}$, $\textit{isOne}$ and $\textit{removeSeqTail}$}
+$\textit{atMostEmpty}$, $\textit{isOne}$ and $\textit{removeSeqTail}$. $\textit{atMostEmpty}
+$ is a function that takes a regular expression and returns true only in case that it
+contains nothing more than the empty string in its language. $\textit{isOne}$ tests whether
+a regular expression is equivalent to $\ONE$. $\textit{removeSeqTail}$ is a function that
+takes away the tail of a sequence regular expression.}
 \end{figure}
 \noindent
 Suppose we feed 
@@ -388,7 +392,9 @@
         }
 
 \end{lstlisting}
-\caption{A Stronger Version of $\textit{distinctBy}$ XXX}
+\caption{A Stronger Version of $\textit{distinctBy}$. This function allows ``partial de-duplication''
+of a regular expression. When part of a regular expression has appeared before in the accumulator, we 
+can remove that verbose component.}
 \end{figure}
 \noindent
 Once a regular expression has been pruned,
@@ -437,9 +443,9 @@
 $\textit{prune}$ refining the finiteness bound
 to a cubic bound has not been formalised yet.
 Therefore we choose to use Scala code rather than an Isabelle-style formal 
-definition like we did for $\simp$, as the definitions might change
+definition like we did for $\textit{bsimp}$, as the definitions might change
 to suit our proof needs.
-In the rest of the chapter we will use this convention consistently.
+%In the rest of the chapter we will use this convention consistently.
 
 %The function $\textit{prune}$ is used in $\distinctWith$.
 %$\distinctWith$ is a stronger version of $\distinctBy$
@@ -669,7 +675,7 @@
 in our derivative is also only $n * (n + 1) / 2$.
 Therefore
 we conjecture that $\bsimpStrong$ is also able to achieve this
-upper limit in general
+upper limit in general.
 \begin{conjecture}\label{bsimpStrongInclusionPder}
 	Using a suitable transformation $f$, we have that
 	\begin{center}