# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1443737360 -3600
# Node ID f16120cb4e194693319ce021a4da0bd7f8779b6d
# Parent  885ac2b6c27db03f8cad354c4823b60b75744793
updated

diff -r 885ac2b6c27d -r f16120cb4e19 handouts/ho02.tex
--- a/handouts/ho02.tex	Thu Oct 01 22:51:32 2015 +0100
+++ b/handouts/ho02.tex	Thu Oct 01 23:09:20 2015 +0100
@@ -570,6 +570,8 @@
 
 \section*{Proofs}
 
+
+
 \end{document}
 
 
diff -r 885ac2b6c27d -r f16120cb4e19 slides/slides02.pdf
Binary file slides/slides02.pdf has changed
diff -r 885ac2b6c27d -r f16120cb4e19 slides/slides02.tex
--- a/slides/slides02.tex	Thu Oct 01 22:51:32 2015 +0100
+++ b/slides/slides02.tex	Thu Oct 01 23:09:20 2015 +0100
@@ -236,10 +236,16 @@
 \bl{\begin{tabular}{l@{\hspace{2mm}}c@{\hspace{2mm}}l}
 $Der\,f\,A$ & $=$ & $\{\textit{oo}, \textit{rak}\}$\\
 $Der\,b\,A$ & $=$ &  $\{\textit{ar}\}$\\  
-$Der\,a\,A$ & $=$ & $\varnothing$\\
+$Der\,a\,A$ & $=$ & $\varnothing$\\\pause
 \end{tabular}}
 \end{center}
 
+\small
+We can extend this definition to strings
+\[
+\bl{Ders\,s\,A = \{s'\;|\;s\,@\,s' \in A\}}
+\]
+
 \end{itemize}
  
 \end{frame}
@@ -783,17 +789,16 @@
 \frametitle{Proofs about Rexp (4)}
 
 \begin{center}
-\bl{\begin{tabular}{r@{\hspace{1mm}}c@{\hspace{1mm}}l}
+\bl{\begin{tabular}{r@{\hspace{2mm}}c@{\hspace{2mm}}l}
 $rev(\varnothing)$   & $\dn$ & $\varnothing$\\
-$rev(\epsilon)$         & $\dn$ & $\epsilon$\\
-$rev(c)$                      & $\dn$ & $c$\\
-$rev(r_1 + r_2)$        & $\dn$ & $rev(r_1) + rev(r_2)$\\
-$rev(r_1 \cdot r_2)$  & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\
-$rev(r^*)$                   & $\dn$ & $rev(r)^*$\\
+$rev(\epsilon)$      & $\dn$ & $\epsilon$\\
+$rev(c)$             & $\dn$ & $c$\\
+$rev(r_1 + r_2)$     & $\dn$ & $rev(r_1) + rev(r_2)$\\
+$rev(r_1 \cdot r_2)$ & $\dn$ & $rev(r_2) \cdot rev(r_1)$\\
+$rev(r^*)$           & $\dn$ & $rev(r)^*$\\
 \end{tabular}}
 \end{center}
 
-
 We can prove
 
 \begin{center}
@@ -805,6 +810,38 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}
+  Correctness Proof\\[-1mm] for our Matcher\end{tabular}}
+
+\begin{itemize}
+\item We started from
+
+\begin{center}
+\begin{tabular}{rp{4cm}}
+  & \bl{$s \in L(r)$}\medskip\\
+\bl{$\Leftrightarrow$} & \bl{$[] \in Ders\,s\,(L(r))$}\pause  
+\end{tabular}
+\end{center}
+
+\item if we can show \bl{$Ders\, s\,(L(r)) = L(ders\,s\,r)$} we 
+have
+
+\begin{center}
+\begin{tabular}{rp{4cm}}
+\bl{$\Leftrightarrow$} & \bl{$[] \in L(ders\,s\,r)$}\medskip\\
+\bl{$\Leftrightarrow$} & \bl{$nullable(ders\,s\,r)$}\medskip\\
+\bl{$\dn$} & \bl{$matches\,s\,r$}
+\end{tabular}
+\end{center}
+
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{Proofs about Rexp (5)}
@@ -826,11 +863,9 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
 \begin{frame}[c]
-\frametitle{\begin{tabular}{c}Proofs about Strings\end{tabular}}
+\frametitle{Proofs about Strings}
 
 If we want to prove something, say a property \bl{$P(s)$}, for all strings \bl{$s$} then \ldots\bigskip
 
@@ -839,13 +874,19 @@
 \item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}
 already holds for \bl{$s$}
 \end{itemize}
-\end{frame}}
+\end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
 \begin{frame}[c]
-\frametitle{\begin{tabular}{c}Proofs about Strings (2)\end{tabular}}
+\frametitle{Proofs about Strings (2)}
+
+We can then prove
+
+\begin{center}
+\bl{$Ders\,s\,(L(r)) = L(ders\,s\,r)$}  
+\end{center}
+
 
 We can finally prove
 
@@ -854,7 +895,7 @@
 \end{center}
 
 
-\end{frame}}
+\end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
 \end{document}