diff -r b2d0de6aee18 -r 7f4c353c0f6b ChengsongTanPhdThesis/Chapters/Cubic.tex
--- a/ChengsongTanPhdThesis/Chapters/Cubic.tex	Thu Sep 01 23:47:37 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Cubic.tex	Fri Sep 02 00:14:19 2022 +0100
@@ -170,11 +170,11 @@
 using  a function similar to $\distinctBy$,
 but this time 
 we allow a more general list rewrite:
-	\begin{mathpar}
+\begin{mathpar}\label{cubicRule}
 		\inferrule{\vspace{0mm} }{rs_a@[a]@rs_c 
 			\stackrel{s}{\rightsquigarrow }
 		rs_a@[\textit{prune} \; a \; rs_a]@rs_c }
-	\end{mathpar}
+\end{mathpar}
 %L \; a_1' = L \; a_1 \setminus (\cup_{a \in rs_a} L \; a)
 where $\textit{prune} \;a \; acc$ traverses $a$
 without altering the structure of $a$, removing components in $a$
@@ -402,27 +402,24 @@
 \begin{conjecture}\label{cubicConjecture}
 	$\blexerStrong \;r \; s = \blexer\; r\;s$
 \end{conjecture}
-
-To implement this idea into an algorithm, we define a "pruning function"
-$\textit{prune}$, that takes away parts of all terms in $r$ that belongs to
-$\textit{acc}$, which acts as an element
-is a stronger version of $\textit{distinctBy}$.
-Here is a concise version of it (in the style of Scala):
-
-
-
+\noindent
+We introduce the new rule \ref{cubicRule}
+and augment our proofs in chapter \ref{Bitcoded2}.
+The idea is to maintain the properties like
+$r \stackrel{*}{\rightsquigarrow} \textit{bsimp} \; r$ etc.
 
-\noindent
-The pruning function can be defined recursively:
-
-
-
-
+In the next section,
+we will describe why we 
+believe a cubic bound can be achieved.
+We give an introduction to the
+partial derivatives,
+which was invented by Antimirov \cite{Antimirov95},
+and then link it with the result of the function
+$\bdersStrongs$.
+ 
+\section{Antimirov's partial derivatives}
 This suggests a link towrads "partial derivatives"
- introduced by Antimirov \cite{Antimirov95}.
- 
- \section{Antimirov's partial derivatives}
- The idea behind Antimirov's partial derivatives
+ introduced  The idea behind Antimirov's partial derivatives
 is to do derivatives in a similar way as suggested by Brzozowski, 
 but maintain a set of regular expressions instead of a single one:
 
@@ -500,7 +497,12 @@
 
 
 
-
+ \section{The NTIMES Constructor, and the Size Bound and Correctness Proof for it}
+The NTIMES construct has the following closed form:
+\begin{verbatim}
+"rders_simp (RNTIMES r0 (Suc n)) (c#s) = 
+rsimp ( RALTS ( (map (optermsimp r0 ) (nupdates s r0 [Some ([c], n)]) ) ))"
+\end{verbatim}
 %----------------------------------------------------------------------------------------
 %	SECTION 1
 %----------------------------------------------------------------------------------------