650 $P(\varepsilon)$ and $P(c)$. I leave this to you.

   650 $P(\varepsilon)$ and $P(c)$. I leave this to you to check.

   651 

   652 Next we need to check the inductive cases, for example

   653 $P(r_1 + r_2)$, which is

   654 

   655 \[

   656 nullable(r_1 + r_2) \;\;\text{if and only if}\;\; 

   657 []\in L(r_1 + r_2)

   658 \]

   659 

   660 \noindent The difference to the base cases is that in this

   661 case we can already assume we proved

   662 

   663 \begin{center}

   664 \begin{tabular}{l}

   665 $nullable(r_1) \;\;\text{if and only if}\;\; []\in L(r_1)$\\

   666 $nullable(r_2) \;\;\text{if and only if}\;\; []\in L(r_2)$\\

   667 \end{tabular}

   668 \end{center}

   669 

   670 \noindent These are the induction hypotheses. To check this 

   671 case we can start from $nullable(r_1 + r_2)$, which by 

   672 definition is

   673 

   674 \[

   675 nullable(r_1) \vee nullable(r_2)

   676 \]

   677 

   678 \noindent Using the induction hypotheses we can transform

   679 this into 

   680 

   681 \[

   682 [] \in L(r_1) \vee []\in(r_2)

   683 \]

   684 

   685 \noindent We just replaced the $nullable(\ldots)$ parts by

   686 the equivalent $[] \in L(\ldots)$ from the induction 

   687 hypotheses. A bit of thinking convinces you that if

   688 $[] \in L(r_1) \vee []\in(r_2)$ then the empty string

   689 must be in the union $L(r_1)\cup L(r_2)$, that is

   690 

   691 \[

   692 [] \in L(r_1)\cup L(r_2)

   693 \]

   694 

   695 \noindent but this is by definition of $L$ exactly

   696 $[] \in L(r_1 + r_2)$, which we needed to establish.

   697 What we have shown is that starting from 

   698 $nullable(r_1 + r_2)$ we have done equivalent transformations

   699 to end up with $[] \in L(r_1 + r_2)$. Consequently we have 

   700 established that $P(r_1 + r_2)$ holds.

   701 

   702 In order to complete the proof we would now need to look 

   703 at the cases $P(r_1\cdot r_2)$ and $P(r^*)$. Again I let you

   704 check the details.

   705 

   706 Finally, you might have to do induction proofs over strings. 

   707 That means you want to establish a property $P(s)$ for all

   708 strings $s$. For this remember strings are lists of 

   709 characters. These lists can be either the empty list or a

   710 list of the form $c::s$. If you want to perform an induction

   711 proof for strings you need to consider the cases

   712 

   713 \begin{itemize}

   714 \item $P$ has to hold for $[]$ (this is the base case).

   715 \item $P$ has to hold for $c::s$ under the assumption 

   716    that $P$ already holds for $s$.

   717 \end{itemize}

   718 

   719 \noindent

   720 Given this recipe, I let you show

   721 

   722 \[

   723 Ders\,s\,(L(r)) = L(ders\,s\,r)

   724 \]

   725 

   726 \noindent by induction on $s$. In this proof you can

   727 assume the property for $der$ and $Der$ has already been

   728 proved, that is you can assume

   729 

   730 \[

   731 L(der\,c\,r) = Der\,c\,(L(r))

   732 \]

   733 

   734 \noindent holds (this would be of course a property that

   735 needs to be proved in a side-lemma by induction on $r$).