--- 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
%----------------------------------------------------------------------------------------