diff -r fa92124d1fb7 -r b306628a0eab ChengsongTanPhdThesis/Chapters/Cubic.tex --- 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