# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1443739811 -3600
# Node ID c49122dbcdd17977490c8280d82fc1bab050a89f
# Parent  bc395ccfba7f076dc28df4df3b3f4ef1ca72cca7
updated

diff -r bc395ccfba7f -r c49122dbcdd1 handouts/ho02.pdf
Binary file handouts/ho02.pdf has changed
diff -r bc395ccfba7f -r c49122dbcdd1 handouts/ho02.tex
--- a/handouts/ho02.tex	Thu Oct 01 23:25:11 2015 +0100
+++ b/handouts/ho02.tex	Thu Oct 01 23:50:11 2015 +0100
@@ -632,7 +632,92 @@
 impossible that the empty string $[]$ is in the empty set. 
 Therefore also the right-hand side is false. Consequently we
 verified this case. We would still need to do this for 
-$P(\varepsilon)$ and $P(c)$. I leave this to you.
+$P(\varepsilon)$ and $P(c)$. I leave this to you to check.
+
+Next we need to check the inductive cases, for example
+$P(r_1 + r_2)$, which is
+
+\[
+nullable(r_1 + r_2) \;\;\text{if and only if}\;\; 
+[]\in L(r_1 + r_2)
+\]
+
+\noindent The difference to the base cases is that in this
+case we can already assume we proved
+
+\begin{center}
+\begin{tabular}{l}
+$nullable(r_1) \;\;\text{if and only if}\;\; []\in L(r_1)$\\
+$nullable(r_2) \;\;\text{if and only if}\;\; []\in L(r_2)$\\
+\end{tabular}
+\end{center}
+
+\noindent These are the induction hypotheses. To check this 
+case we can start from $nullable(r_1 + r_2)$, which by 
+definition is
+
+\[
+nullable(r_1) \vee nullable(r_2)
+\]
+
+\noindent Using the induction hypotheses we can transform
+this into 
+
+\[
+[] \in L(r_1) \vee []\in(r_2)
+\]
+
+\noindent We just replaced the $nullable(\ldots)$ parts by
+the equivalent $[] \in L(\ldots)$ from the induction 
+hypotheses. A bit of thinking convinces you that if
+$[] \in L(r_1) \vee []\in(r_2)$ then the empty string
+must be in the union $L(r_1)\cup L(r_2)$, that is
+
+\[
+[] \in L(r_1)\cup L(r_2)
+\]
+
+\noindent but this is by definition of $L$ exactly
+$[] \in L(r_1 + r_2)$, which we needed to establish.
+What we have shown is that starting from 
+$nullable(r_1 + r_2)$ we have done equivalent transformations
+to end up with $[] \in L(r_1 + r_2)$. Consequently we have 
+established that $P(r_1 + r_2)$ holds.
+
+In order to complete the proof we would now need to look 
+at the cases $P(r_1\cdot r_2)$ and $P(r^*)$. Again I let you
+check the details.
+
+Finally, you might have to do induction proofs over strings. 
+That means you want to establish a property $P(s)$ for all
+strings $s$. For this remember strings are lists of 
+characters. These lists can be either the empty list or a
+list of the form $c::s$. If you want to perform an induction
+proof for strings you need to consider the cases
+
+\begin{itemize}
+\item $P$ has to hold for $[]$ (this is the base case).
+\item $P$ has to hold for $c::s$ under the assumption 
+   that $P$ already holds for $s$.
+\end{itemize}
+
+\noindent
+Given this recipe, I let you show
+
+\[
+Ders\,s\,(L(r)) = L(ders\,s\,r)
+\]
+
+\noindent by induction on $s$. In this proof you can
+assume the property for $der$ and $Der$ has already been
+proved, that is you can assume
+
+\[
+L(der\,c\,r) = Der\,c\,(L(r))
+\]
+
+\noindent holds (this would be of course a property that
+needs to be proved in a side-lemma by induction on $r$).
 
 \end{document}