proof.tex
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 05 Dec 2012 04:13:12 +0000
changeset 86 6a7fe83820c8
parent 34 eeff9953a1c1
permissions -rw-r--r--
added
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
\documentclass{article}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
\usepackage{charter}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
\usepackage{hyperref}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
\usepackage{amssymb}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
\usepackage{amsmath}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
\begin{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
\section*{Proof}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
Recall the definitions for regular expressions and the language associated with a regular expression:
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
\begin{tabular}{c}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
\begin{tabular}[t]{rcl}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
  $r$ & $::=$  & $\varnothing$  \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
         & $\mid$ & $\epsilon$       \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
         & $\mid$ & $c$                         \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
         & $\mid$ & $r_1 \cdot r_2$ \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
         & $\mid$ & $r_1 + r_2$  \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
         & $\mid$ & $r^*$                 \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
  \end{tabular}\hspace{10mm}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
\begin{tabular}[t]{r@{\hspace{1mm}}c@{\hspace{1mm}}l}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
$L(\varnothing)$ & $\dn$ & $\varnothing$ \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
$L(\epsilon)$       & $\dn$ & $\{\texttt{""}\}$       \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
$L(c)$                   & $\dn$ & $\{\texttt{"}c\texttt{"}\}$                         \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
$L(r_1 \cdot r_2)$   & $\dn$ & $L(r_1) \,@\, L(r_2)$ \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
$L(r_1 + r_2)$         & $\dn$ & $L(r_1) \cup L(r_2)$  \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
 $L(r^*)$        & $\dn$ & $\bigcup_{n\ge 0} L(r)^n$                 \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
\end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
\noindent
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
We also defined the notion of a derivative of a regular expression (the derivative with respect to a character):
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
\begin{tabular}{lcl}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
  $der\, c\, (\varnothing)$    & $\dn$ & $\varnothing$  \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
  $der\, c\, (\epsilon)$          & $\dn$ & $\varnothing$ \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
  $der\, c\, (d)$                      & $\dn$ & if $c = d$ then $\epsilon$ else $\varnothing$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
  $der\, c\, (r_1 + r_2)$        & $\dn$ & $(der\, c\, r_1) + (der\, c\, r_2)$ \\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
  $der\, c\, (r_1 \cdot r_2)$ & $\dn$  & if $nullable(r_1)$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
       & & then $((der\, c\, r_1) \cdot r_2) + (der\, c\, r_2)$\\ 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
       & & else $(der\, c\, r_1) \cdot r_2$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
  $der\, c\, (r^*)$                   & $\dn$ & $(der\, c\, r) \cdot (r^*)$\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
  \end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
\noindent
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
With our definition of regular expressions comes an induction principle. Given a property $P$ over 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
regular expressions. We can establish that $\forall r.\; P(r)$ holds, provided we can show the following:
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
\begin{enumerate}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
\item $P(\varnothing)$, $P(\epsilon)$ and $P(c)$ all hold,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
\item $P(r_1 + r_2)$ holds under the induction hypotheses that 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
$P(r_1)$ and $P(r_2)$ hold,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
\item $P(r_1 \cdot r_2)$ holds under the induction hypotheses that 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
$P(r_1)$ and $P(r_2)$ hold, and
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
\item $P(r^*)$ holds under the induction hypothesis that $P(r)$ holds.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
\end{enumerate}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
\noindent
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
Let us try out an induction proof. Recall the definition
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
$Der\, c\, A \dn \{ s\;\mid\; c\!::\!s \in A\}$
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
\noindent
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
whereby $A$ is a set of strings. We like to prove
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
\begin{tabular}{l}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
$P(r) \dn $ \hspace{4mm} $L(der\,c\,r) = Der\,c\,(L(r))$
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
\end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
\noindent
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
by induction over the regular expression $r$.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
\newpage
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
\noindent
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
{\bf Proof}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
\noindent
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
According to 1.~above we need to prove $P(\varnothing)$, $P(\epsilon)$ and $P(d)$. Lets do this in turn.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
\begin{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
\item First Case: $P(\varnothing)$ is $L(der\,c\,\varnothing) = Der\,c\,(L(\varnothing))$ (a). We have $der\,c\,\varnothing = \varnothing$ 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
and $L(\varnothing) = \varnothing$. We also have $Der\,c\,\varnothing = \varnothing$. Hence we have $\varnothing = \varnothing$ in (a). 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
\item Second  Case: $P(\epsilon)$ is $L(der\,c\,\epsilon) = Der\,c\,(L(\epsilon))$ (b). We have $der\,c\,\epsilon = \varnothing$,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
$L(\varnothing) = \varnothing$ and $L(\epsilon) = \{\texttt{""}\}$. We also have $Der\,c\,\{\texttt{""}\} = \varnothing$. Hence we have 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
$\varnothing = \varnothing$ in (b). 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
\item Third  Case: $P(d)$ is $L(der\,c\,d) = Der\,c\,(L(d))$ (c). We need to treat the cases $d = c$ and $d \not= c$. 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
$d = c$: We have $der\,c\,c = \epsilon$ and $L(\epsilon) = \{\texttt{""}\}$. 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
We also have $L(c) = \{\texttt{"}c\texttt{"}\}$ and $Der\,c\,\{\texttt{"}c\texttt{"}\} = \{\texttt{""}\}$. Hence we have 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
$\{\texttt{""}\} = \{\texttt{""}\}$ in (c). 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
$d \not=c$: We have $der\,c\,d = \varnothing$.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
We also have $Der\,c\,\{\texttt{"}d\texttt{"}\} = \varnothing$. Hence we have 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
$\varnothing = \varnothing$  in (c). 
34
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   108
\end{itemize}
20
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
34
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   110
\noindent
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   111
These were the easy base cases. Now come the inductive cases.
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   112
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   113
\begin{itemize}
20
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   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.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
We can assume already:
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
\begin{tabular}{ll}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
$P(r_1)$: & $L(der\,c\,r_1) = Der\,c\,(L(r_1))$ (I)\\
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
$P(r_2)$: & $L(der\,c\,r_2) = Der\,c\,(L(r_2))$ (II)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
\end{tabular}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
We have that $der\,c\,(r_1 + r_2) = (der\,c\,r_1) + (der\,c\,r_2)$ and also $L((der\,c\,r_1) + (der\,c\,r_2)) = L(der\,c\,r_1) \cup L(der\,c\,r_2)$.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
By (I) and (II) we know that the left-hand side is $Der\,c\,(L(r_1)) \cup Der\,c\,(L(r_2))$.  You need to ponder a bit, but you should see
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
that 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
$Der\,c(A \cup B) = (Der\,c\,A) \cup (Der\,c\,B)$
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
\end{center}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
holds for every set of strings $A$ and $B$. That means the right-hand side of (d) is also $Der\,c\,(L(r_1)) \cup Der\,c\,(L(r_2))$,
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
because $L(r_1 + r_2) = L(r_1) \cup L(r_2)$. And we are done with the fourth case.
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
 
21
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   135
\item Fifth Case: $P(r_1 \cdot r_2)$ is $L(der\,c\,(r_1 \cdot r_2)) = Der\,c\,(L(r_1 \cdot r_2))$ (e). We can assume already:
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   136
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   137
\begin{center}
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   138
\begin{tabular}{ll}
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   139
$P(r_1)$: & $L(der\,c\,r_1) = Der\,c\,(L(r_1))$ (I)\\
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   140
$P(r_2)$: & $L(der\,c\,r_2) = Der\,c\,(L(r_2))$ (II)
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   141
\end{tabular}
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   142
\end{center}
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   143
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   144
Let us first consider the case where $nullable(r_1)$ holds. Then 
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   145
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   146
\[
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   147
der\,c\,(r_1 \cdot r_2) = ((der\,c\,r_1) \cdot r_2) + (der\,c\,r_2).
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   148
\]
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   149
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   150
The corresponding language of the right-hand side is 
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   151
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   152
\[
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   153
(L(der\,c\,r_1) \,@\, L(r_2)) \cup L(der\,c\,r_2).
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   154
\]
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   155
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   156
By the induction hypotheses (I) and (II), this is equal to
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   157
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   158
\[
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   159
(Der\,c\,(L(r_1)) \,@\, L(r_2)) \cup (Der\,c\,(L(r_2)).\;\;(**)
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   160
\]
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   161
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   162
We also know that $L(r_1 \cdot r_2) = L(r_1) \,@\,L(r_2)$.  We have to know what
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   163
$Der\,c\,(L(r_1) \,@\,L(r_2))$ is.
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   164
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   165
Let us analyse what
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   166
$Der\,c\,(A \,@\, B)$ is for arbitrary sets of strings $A$ and $B$. If $A$ does \emph{not}
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   167
contain the empty string, then every string in $A\,@\,B$ is of the form $s_1 \,@\, s_2$ where
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   168
$s_1 \in A$ and $s_2 \in B$. So if $s_1$ starts with $c$ then we just have to remove it. Consequently,
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   169
$Der\,c\,(A \,@\, B) = (Der\,c\,(A)) \,@\, B$. This case does not apply here though, because we already 
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   170
proved that if $r_1$ is nullable, then $L(r_1)$ contains the empty string. In this case, every string
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   171
in  $A\,@\,B$ is either of the form $s_1 \,@\, s_2$, with $s_1 \in A$ and $s_2 \in B$, or
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   172
$s_3$ with $s_3 \in B$. This means $Der\,c\,(A \,@\, B) = ((Der\,c\,(A)) \,@\, B) \cup Der\,c\,B$.
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   173
But this proves that (**) is $Der\,c\,(L(r_1) \,@\, L(r_2))$.
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   174
4e5092ab450a one more case
Christian Urban <urbanc@in.tum.de>
parents: 20
diff changeset
   175
Similarly in the case where $r_1$ is \emph{not} nullable.
20
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
34
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   177
\item Sixth Case: $P(r^*)$ is $L(der\,c\,(r^*)) = Der\,c\,L(r^*)$. We can assume already:
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   178
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   179
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   180
\begin{tabular}{ll}
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   181
$P(r)$: & $L(der\,c\,r) = Der\,c\,(L(r))$ (I)
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   182
\end{tabular}
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   183
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   184
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   185
We have $der\,c\,(r^*) = der\,c\,r\cdot r^*$. Which means $L(der\,c\,(r^*)) = L(der\,c\,r\cdot r^*)$ and
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   186
further $L(der\,c\,r) \,@\, L(r^*)$. By induction hypothesis (I) we know that is equal to 
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   187
$(Der\,c\,L(r)) \,@\, L(r^*)$. (*)
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   188
20
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
\end{itemize}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
34
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   191
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   192
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   193
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   194
Let us now analyse $Der\,c\,L(r^*)$, which is equal to $Der\,c\,((L(r))^*)$. Now $(L(r))^*$ is defined
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   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 
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   196
separated the first union and then let the ``big-union'' start from $1$. Form this we can already infer
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   197
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   198
\begin{center}
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   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))$
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   200
\end{center}
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   201
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   202
The first union ``disappears'' since $Der\,c\,(L(r)^0) = \varnothing$.
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   203
Christian Urban <urbanc@in.tum.de>
parents: 21
diff changeset
   204
20
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
\end{document}
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
%%% Local Variables: 
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
%%% mode: latex
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
%%% TeX-master: t
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
%%% End: