--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Fri Sep 02 19:18:50 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Fri Sep 02 19:35:55 2022 +0100
@@ -344,13 +344,35 @@
 \end{center}
 %TODO: definition of rsimp (maybe only the alternative clause)
 \noindent
-Notice there is a difference between our $\rdistincts$ and
-the Isabelle $\textit {distinct}$ function.
-In Isabelle $\textit{distinct}$ is a predicate
-that tests if all the elements of a list are unique.\\
-With $\textit{rdistinct}$ one can chain together all the other modules
+We would like to make clear
+a difference between our $\rdistincts$ and
+the Isabelle $\textit {distinct}$ predicate.
+In Isabelle $\textit{distinct}$ is a function that returns a boolean
+rather than a list.
+It tests if all the elements of a list are unique.\\
+With $\textit{rdistinct}$,
+and the flatten function for $\rrexp$s:
+ \begin{center}
+  \begin{tabular}{@{}lcl@{}}
+  $\textit{rflts} \; (_{bs}\sum \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \;
+     (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{rflts} \; as' $ \\
+  $\textit{rflts} \; \ZERO :: as'$ & $\dn$ & $ \textit{rflts} \;  \textit{as'} $ \\
+    $\textit{rflts} \; a :: as'$ & $\dn$ & $a :: \textit{rflts} \; \textit{as'}$ \quad(otherwise) 
+\end{tabular}    
+\end{center}  
+\noindent
+
+one can chain together all the other modules
 of $\bsimp{\_}$ (removing the functionalities related to bit-sequences)
 and get $\textit{rsimp}$ and $\rderssimp{\_}{\_}$.
+\begin{center}
+  \begin{tabular}{@{}lcl@{}}
+   
+	  $\textit{rsimp} \; (_{bs}a_1\cdot a_2)$ & $\dn$ & $ \textit{rsimp}_{ASEQ} \; bs \;(\textit{rsimp} \; a_1) \; (\textit{rsimp}  \; a_2)  $ \\
+	  $\textit{rsimp} \; (_{bs}\sum \textit{as})$ & $\dn$ & $\textit{rsimp}_{ALTS} \; \textit{bs} \; (\textit{rdistinct} \; ( \textit{rflts} ( \textit{map} \; rsimp \; as)) \; \rerases \; \varnothing) $ \\
+   $\textit{rsimp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$   
+\end{tabular}    
+\end{center} 
 We omit these functions, as they are routine. Please refer to the formalisation
 (in file BasicIdentities.thy) for the exact definition.
 With $\rrexp$ the size caclulation of annotated regular expressions'