--- a/ChengsongTanPhdThesis/Chapters/Cubic.tex Fri Sep 02 19:35:55 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Cubic.tex Sat Sep 03 00:14:20 2022 +0100
@@ -572,5 +572,32 @@
%----------------------------------------------------------------------------------------
\section{Bounded Repetitions}
+We define for the $r^{n}$ constructor something similar to $\starupdate$
+and $\starupdates$:
+\begin{center}
+ \begin{tabular}{lcl}
+ $\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\
+ $\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\
+ & & $\textit{if} \;
+ (\rnullable \; (\rders \; r \; s))$ \\
+ & & $\textit{then} \;\; (s @ [c]) :: [c] :: (
+ \starupdate \; c \; r \; Ss)$ \\
+ & & $\textit{else} \;\; (s @ [c]) :: (
+ \starupdate \; c \; r \; Ss)$
+ \end{tabular}
+\end{center}
+\noindent
+As a generalisation from characters to strings,
+$\starupdates$ takes a string instead of a character
+as the first input argument, and is otherwise the same
+as $\starupdate$.
+\begin{center}
+ \begin{tabular}{lcl}
+ $\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\
+ $\starupdates \; (c :: cs) \; r \; Ss$ & $=$ & $\starupdates \; cs \; r \; (
+ \starupdate \; c \; r \; Ss)$
+ \end{tabular}
+\end{center}
+\noindent