--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Sun Jul 09 02:08:12 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Mon Jul 10 00:44:45 2023 +0100
@@ -360,6 +360,8 @@
 will definitely not contribute to a POSIX value,
 even if they are attached with different bitcodes.
 These duplicates therefore need to be removed.
+
+
 To achieve this, we call $\rerases$ as the function $f$ during the distinction
 operation. The function
 $\rerases$ is very similar to $\erase$, except that it preserves the structure
@@ -375,7 +377,7 @@
 the new datatype used by $\rerases$ (as our plain
 regular expression datatype does not allow non-binary alternatives).
 For now we can think of 
-$\rerases$ as the function $(\_)_\downarrow$ defined in chapter \ref{Bitcoded1}
+$\rerases$ as the function erase ($(\_)_\downarrow$) defined in chapter \ref{Bitcoded1}
 and $\rrexp$ as plain regular expressions, but having a general list constructor
 for alternatives:
 \begin{figure}[H]
@@ -400,6 +402,10 @@
 $\rerase{_{bs} a ^*}$ & $\dn$ & $\rerase{a}^*$
 \end{tabular}
 \end{center}
+We will provide more details in \ref{whyRerase} for why a new
+erase function and new datatype is needed. But briefly speaking
+it is for backward-compatibility with $\blexer$'s correctness proof and 
+the path we (naturally) took during our proof engineering of the finiteness property.
 
 \subsection{Putting Things Together}
 We can now give the definition of our  simplification function: