--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Wed Aug 31 12:51:53 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Wed Aug 31 23:57:42 2022 +0100
@@ -308,20 +308,24 @@
 annotated regular expressions
 whereas $\erase$ would turn it back into a binary structure.
 Not having to mess with the structure 
-greatly simplifies the finiteness proof in chapter \ref{Finite}.
+greatly simplifies the finiteness proof in chapter 
+\ref{Finite} (we will follow up with more details there).
 We give the definitions of $\rerases$ here together with
 the new datatype used by $\rerases$ (as our plain
-regular expression datatype does not allow non-binary alternatives),
-and explain in detail
-why we want it in the next chapter.
+regular expression datatype does not allow non-binary alternatives).
 For the moment the reader can just think of 
 $\rerases$ as $\erase$ and $\rrexp$ as plain regular expressions.
-\[			\rrexp ::=   \RZERO \mid  \RONE
+\begin{figure}[H]
+\begin{center}	
+	$\rrexp ::=   \RZERO \mid  \RONE
 			 \mid  \RCHAR{c}  
 			 \mid  \RSEQ{r_1}{r_2}
 			 \mid  \RALTS{rs}
-			 \mid \RSTAR{r}        
-\]
+			 \mid \RSTAR{r}        $
+\end{center}
+\caption{$\rrexp$: plain regular expressions, but with $\sum$ alternative 
+constructor}\label{rrexpDef}
+\end{figure}
 The notation of $\rerases$ also follows that of $\erase$,
 which is a postfix operator written as a subscript,
 except that it has an \emph{r} attached to it to distinguish against $\erase$: