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