575 

   575 We define for the $r^{n}$ constructor something similar to $\starupdate$

   576 

   576 and $\starupdates$:

   577 \begin{center}

   578 	\begin{tabular}{lcl}

   579 		$\starupdate \; c \; r \; [] $ & $\dn$ & $[]$\\

   580 		$\starupdate \; c \; r \; (s :: Ss)$ & $\dn$ & \\

   581 						     & & $\textit{if} \; 

   582 						     (\rnullable \; (\rders \; r \; s))$ \\

   583 						     & & $\textit{then} \;\; (s @ [c]) :: [c] :: (

   584 						     \starupdate \; c \; r \; Ss)$ \\

   585 						     & & $\textit{else} \;\; (s @ [c]) :: (

   586 						     \starupdate \; c \; r \; Ss)$

   587 	\end{tabular}

   588 \end{center}

   589 \noindent

   590 As a generalisation from characters to strings,

   591 $\starupdates$ takes a string instead of a character

   592 as the first input argument, and is otherwise the same

   593 as $\starupdate$.

   594 \begin{center}

   595 	\begin{tabular}{lcl}

   596 		$\starupdates \; [] \; r \; Ss$ & $=$ & $Ss$\\

   597 		$\starupdates \; (c :: cs) \; r \; Ss$ &  $=$ &  $\starupdates \; cs \; r \; (

   598 		\starupdate \; c \; r \; Ss)$

   599 	\end{tabular}

   600 \end{center}

   601 \noindent

   602 

   603