420 \begin{center}

   420 \begin{center}

   421 $\ldots \dn Stars(\inj\,r\,c\,v\,::\,vs)$

   421 $\ldots \dn Stars(\inj\,r\,c\,v\,::\,vs)$

   422 \end{center}  

   422 \end{center}  

   423 

   423 

   424 \noindent It is a value of the right shape, namely $Stars$. It injected 

   424 \noindent It is a value of the right shape, namely $Stars$. It injected 

   426 undo the derivative. Remember again the shape of the derivative of $r^*$.

   426 undo the derivative. Remember again the shape of the derivative of $r^*$.

   427 In place where we chopped off the $c$, we now need to do the $\inj$ of $c$.

   427 In place where we chopped off the $c$, we now need to do the $\inj$ of $c$.

   428 Therefore $\inj\,r\,c\,v$ in the definition above. That is the same with

   428 Therefore $\inj\,r\,c\,v$ in the definition above. That is the same with

   429 the other clauses in $\inj$. 

   429 the other clauses in $\inj$. 

   430 

   430 

   745 is for strings where the first character is $c$, say, and the

   745 is for strings where the first character is $c$, say, and the

   746 rest of the string is $s$. We first build the derivative of

   746 rest of the string is $s$. We first build the derivative of

   747 $r$ with respect to $c$; simplify the resulting regular

   747 $r$ with respect to $c$; simplify the resulting regular

   748 expression. We continue lexing with the simplified regular

   748 expression. We continue lexing with the simplified regular

   749 expression and the string $s$. Whatever will be returned as

   749 expression and the string $s$. Whatever will be returned as

   751 simplification and finally inject $c$ back into the

   751 simplification and finally inject $c$ back into the

   752 (rectified) value.

   752 (rectified) value.

   753 

   753 

   754 

   754 

   755 \subsubsection*{Records}

   755 \subsubsection*{Records}