proof.tex
changeset 34 eeff9953a1c1
parent 21 4e5092ab450a
equal deleted inserted replaced
33:92b3e287d87e 34:eeff9953a1c1
   103 $\{\texttt{""}\} = \{\texttt{""}\}$ in (c). 
   103 $\{\texttt{""}\} = \{\texttt{""}\}$ in (c). 
   104 
   104 
   105 $d \not=c$: We have $der\,c\,d = \varnothing$.
   105 $d \not=c$: We have $der\,c\,d = \varnothing$.
   106 We also have $Der\,c\,\{\texttt{"}d\texttt{"}\} = \varnothing$. Hence we have 
   106 We also have $Der\,c\,\{\texttt{"}d\texttt{"}\} = \varnothing$. Hence we have 
   107 $\varnothing = \varnothing$  in (c). 
   107 $\varnothing = \varnothing$  in (c). 
   108 
   108 \end{itemize}
       
   109 
       
   110 \noindent
       
   111 These were the easy base cases. Now come the inductive cases.
       
   112 
       
   113 \begin{itemize}
   109 \item Fourth Case: $P(r_1 + r_2)$ is $L(der\,c\,(r_1 + r_2)) = Der\,c\,(L(r_1 + r_2))$ (d). This is what we have to show.
   114 \item Fourth Case: $P(r_1 + r_2)$ is $L(der\,c\,(r_1 + r_2)) = Der\,c\,(L(r_1 + r_2))$ (d). This is what we have to show.
   110 We can assume already:
   115 We can assume already:
   111 
   116 
   112 \begin{center}
   117 \begin{center}
   113 \begin{tabular}{ll}
   118 \begin{tabular}{ll}
   167 $s_3$ with $s_3 \in B$. This means $Der\,c\,(A \,@\, B) = ((Der\,c\,(A)) \,@\, B) \cup Der\,c\,B$.
   172 $s_3$ with $s_3 \in B$. This means $Der\,c\,(A \,@\, B) = ((Der\,c\,(A)) \,@\, B) \cup Der\,c\,B$.
   168 But this proves that (**) is $Der\,c\,(L(r_1) \,@\, L(r_2))$.
   173 But this proves that (**) is $Der\,c\,(L(r_1) \,@\, L(r_2))$.
   169 
   174 
   170 Similarly in the case where $r_1$ is \emph{not} nullable.
   175 Similarly in the case where $r_1$ is \emph{not} nullable.
   171 
   176 
   172 \item Sixth Case:
   177 \item Sixth Case: $P(r^*)$ is $L(der\,c\,(r^*)) = Der\,c\,L(r^*)$. We can assume already:
       
   178 
       
   179 \begin{center}
       
   180 \begin{tabular}{ll}
       
   181 $P(r)$: & $L(der\,c\,r) = Der\,c\,(L(r))$ (I)
       
   182 \end{tabular}
       
   183 \end{center}
       
   184 
       
   185 We have $der\,c\,(r^*) = der\,c\,r\cdot r^*$. Which means $L(der\,c\,(r^*)) = L(der\,c\,r\cdot r^*)$ and
       
   186 further $L(der\,c\,r) \,@\, L(r^*)$. By induction hypothesis (I) we know that is equal to 
       
   187 $(Der\,c\,L(r)) \,@\, L(r^*)$. (*)
       
   188 
   173 \end{itemize}
   189 \end{itemize}
       
   190 
       
   191 
       
   192 
       
   193 
       
   194 Let us now analyse $Der\,c\,L(r^*)$, which is equal to $Der\,c\,((L(r))^*)$. Now $(L(r))^*$ is defined
       
   195 as $\bigcup_{n \ge 0} L(r)$. We can write this as $L(r)^0 \cup \bigcup_{n \ge 1} L(r)$, where we just 
       
   196 separated the first union and then let the ``big-union'' start from $1$. Form this we can already infer
       
   197 
       
   198 \begin{center}
       
   199 $Der\,c\,(L(r^*)) = Der\,c\,(L(r)^0 \cup \bigcup_{n \ge 1} L(r)) = (Der\,c\,L(r)^0) \cup Der\,c\,(\bigcup_{n \ge 1} L(r))$
       
   200 \end{center}
       
   201 
       
   202 The first union ``disappears'' since $Der\,c\,(L(r)^0) = \varnothing$.
       
   203 
   174 
   204 
   175 \end{document}
   205 \end{document}
   176 
   206 
   177 %%% Local Variables: 
   207 %%% Local Variables: 
   178 %%% mode: latex
   208 %%% mode: latex