--- a/ChengsongTanPhdThesis/Chapters/Finite.tex Mon Oct 03 02:08:49 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex Mon Oct 03 13:32:25 2022 +0100
@@ -575,10 +575,10 @@
\end{proof}
\noindent
-$\rdistinct{\_}{\_}$ will cancel out all regular expression terms
+$\textit{rdistinct}$ will cancel out all regular expression terms
that are in the accumulator, therefore prepending a list $rs_a$ with an arbitrary
-list $rs$ whose elements are all from the accumulator, and then call $\rdistinct{\_}{\_}$
-on the resulting list, the output will be as if we had called $\rdistinct{\_}{\_}$
+list $rs$ whose elements are all from the accumulator, and then call $\textit{rdistinct}$
+on the resulting list, the output will be as if we had called $\textit{rdistinct}$
without the prepending of $rs$:
\begin{lemma}\label{rdistinctConcat}
The elements appearing in the accumulator will always be removed.
@@ -929,7 +929,7 @@
We are also
-\subsubsection{$\rsimp$ is Idempotent}
+\subsection{$\rsimp$ is Idempotent}
The idempotency of $\rsimp$ is very useful in
manipulating regular expression terms into desired
forms so that key steps allowing further rewriting to closed forms
@@ -1042,7 +1042,7 @@
We need more equalities like the above to enable a closed form,
but to proceed we need to introduce two rewrite relations,
to make things smoother.
-\subsubsection{The rewrite relation $\hrewrite$ , $\scfrewrites$ , $\frewrite$ and $\grewrite$}
+\subsection{The rewrite relation $\hrewrite$ , $\scfrewrites$ , $\frewrite$ and $\grewrite$}
Insired by the success we had in the correctness proof
in \ref{Bitcoded2}, where we invented
a term rewriting system to capture the similarity between terms,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ChengsongTanPhdThesis/re-dart.data Mon Oct 03 13:32:25 2022 +0100
@@ -0,0 +1,15 @@
+%% LaTeX2e file `re-dart.data'
+%% generated by the `filecontents' environment
+%% from source `slides01' on 2022/03/16.
+%%
+20 0.042
+21 0.084
+22 0.190
+23 0.340
+24 0.678
+25 1.369
+26 2.700
+27 5.462
+28 10.908
+29 21.725
+30 43.492
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ChengsongTanPhdThesis/re-swift.data Mon Oct 03 13:32:25 2022 +0100
@@ -0,0 +1,13 @@
+%% LaTeX2e file `re-swift.data'
+%% generated by the `filecontents' environment
+%% from source `slides01' on 2022/03/16.
+%%
+5 0.001
+10 0.001
+15 0.009
+20 0.178
+23 1.399
+24 2.893
+25 5.671
+26 11.357
+27 22.430