640 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   641 \begin{frame}[c]

   642   \frametitle{$der$ for $n$-times}

   643 

   644 Case \bl{$n = 2$} and \bl{$r \cdot r$}: 

   645 

   646 \begin{center}

   647   \begin{tabular}{lcl}

   648     \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\

   649                               &   & \bl{then \; \alert<3>{$(der\,c\,r)\cdot r + der\,c\,r$}}\\

   650                               &   & \bl{else \; $(der\,c\,r)\cdot r$}\bigskip\pause\\

   651     my claim                  &   & \bl{$\equiv\;$} \bl{$(der\,c\,r)\cdot r$}\\

   652     (in this case)                                

   653   \end{tabular} 

   654 \end{center}  

   655 

   656 \end{frame}

   657 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   658 

   659 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   660 \begin{frame}[t]

   661 

   662 We know \bl{$nullable(r)$} holds!\pause 

   663 

   664 \begin{center}

   665   \begin{tabular}{@{}lcl}

   666     \bl{$(der\,c\,r)\cdot r + der\,c\,r$}\pause

   667     & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot r + (der\,c\,r) \cdot \ONE$}\medskip\pause\\

   668     & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot (r + \ONE)$}\medskip\pause\\

   669     & \bl{$\equiv$} & \bl{$(der\,c\,r)\cdot r$}\\

   670     \multicolumn{3}{r}{\small(remember \bl{$r$} is nullable)}

   671   \end{tabular} 

   672 \end{center}\pause

   673 

   674 \rule{13cm}{0.8mm}

   675 

   676 \begin{textblock}{13}(2,10)

   677 \only<6>{%

   678   \begin{tabular}{lcl}

   679     \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\

   680                           &   & \bl{then \; $(der\,c\,r)\cdot r + der\,c\,r$}\\

   681                           &   & \bl{else \; $(der\,c\,r)\cdot r$}                                

   682   \end{tabular}}

   683 \only<7>{%

   684   \begin{tabular}{lcl}

   685     \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{if \; $nullable(r)$}\\

   686                           &   & \bl{then \; $(der\,c\,r)\cdot r$}\\

   687                           &   & \bl{else \; $(der\,c\,r)\cdot r$}                                

   688   \end{tabular}}

   689 \only<8>{%

   690   \begin{tabular}{lcl}

   691     \bl{$der\,c\,(r\cdot r)$} & \bl{$\dn$} & \bl{$(der\,c\,r)\cdot r$}                                

   692   \end{tabular}}

   693 \end{textblock}

   694 

   695 

   696 \end{frame}

   697 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   698 

   699 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   700 \begin{frame}[c]

   701 

   702 \begin{center}

   703 \begin{tabular}{ll@{\hspace{10mm}}l}

   704 & \bl{$r\{n\}$} & \bl{$der$}\hspace{20mm}\mbox{}\\\hline\\[-4mm]    

   705 \bl{$n = 0$} : & \bl{$\ONE$}           & \bl{$\ZERO$}\\

   706 \bl{$n = 1$} : & \bl{$r$}              & \bl{$(der\,c\,r)$}\\

   707 \bl{$n = 2$} : & \bl{$r\cdot r$}       & \bl{$(der\,c\,r)\cdot r$}\\

   708 \bl{$n = 3$} : & \bl{$r\cdot r\cdot r$}& \only<1>{???}\only<2->{\bl{$(der\,c\,r)\cdot r\cdot r$}}\\

   709 \quad\vdots  

   710 \end{tabular} 

   711 \end{center}

   712 

   713 \begin{textblock}{13}(1,11)

   714 \only<3->{%

   715   \begin{tabular}{rcl}

   716     \bl{$nullable(r\{n\})$} & \bl{$\dn$} &

   717                           \bl{if\; $n = 0$\; then\; $true$\; else\; $nullable(r)$}\\

   718     \bl{$der\,c\,(r\{n\})$} & \bl{$\dn$} &

   719                           \bl{if\; $n = 0$\; then\; $\ZERO$\; else\; $(der\,c\,r)\cdot r\{n - 1\}$}

   720   \end{tabular}}

   721 \end{textblock}

   722 

   723 \end{frame}

   724 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   725 

   726 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   727 \begin{frame}[c]

   728 

   729 \begin{textblock}{13}(1.5,4)

   730   \only<1-6>{%

   731   \begin{tabular}{@{}lcl@{}}

   732     \bl{$der\,c\,(r\cdot r\cdot r)$}

   733     & \bl{$\dn$} & \bl{if $nullable(r)$}\medskip\\

   734     & & \only<1>{\bl{then\; $(der\,c\,r)\cdot r\cdot r + der\,c\,(r\cdot r)$}}%

   735         \only<2>{\bl{then\; $(der\,c\,r)\cdot r\cdot r + (der\,c\,r)\cdot r$}}%

   736         \only<3>{\bl{then\; $(der\,c\,r)\cdot (r\cdot r + r)$}}%

   737         \only<4>{\bl{then\; $(der\,c\,r)\cdot (r\cdot (r + \ONE))$}}%

   738         \only<5>{\bl{then\; $(der\,c\,r)\cdot (r\cdot r)$}}%

   739         \only<6>{\bl{then\; $(der\,c\,r)\cdot r\cdot r$}}\medskip\\

   740     & & \bl{else\; $(der\,c\,r)\cdot r\cdot r$}\\

   741   \end{tabular}}

   742   \only<7->{%

   743   \begin{tabular}{@{}lcl@{}}

   744     \bl{$der\,c\,(r\cdot r\cdot r)$}

   745     & \bl{$\dn$} & \bl{$(der\,c\,r)\cdot r\cdot r$}%

   746   \end{tabular}} 

   747 \end{textblock}

   748 

   749 \end{frame}

   750 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   751