equal
deleted
inserted
replaced
1 \documentclass[11pt]{article} |
1 \documentclass[11pt]{article} |
2 \usepackage[left]{lineno} |
2 \usepackage[left]{lineno} |
3 \usepackage{amsmath} |
3 \usepackage{amsmath} |
4 |
4 |
5 \begin{document} |
5 \begin{document} |
6 %%\linenumbers |
6 %%%\linenumbers |
7 |
7 |
8 \noindent |
8 \noindent |
9 We already proved that |
9 We already proved that |
10 |
10 |
11 \[ |
11 \[ |
346 \hline |
346 \hline |
347 $Right(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Left(w_2)$ |
347 $Right(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Left(w_2)$ |
348 \end{tabular} |
348 \end{tabular} |
349 \end{center} |
349 \end{center} |
350 |
350 |
|
351 \subsection*{Test Proof} |
|
352 |
|
353 We want to prove that |
|
354 |
|
355 \[ |
|
356 nullable(r) \;\text{implies}\; POSIX (mkeps\; r)\; r |
|
357 \] |
|
358 |
|
359 \noindent |
|
360 We prove this by induction on $r$. There are 5 subcases, and |
|
361 only the $r_1 + r_2$-case is interesting. In this case we know the |
|
362 induction hypotheses are |
|
363 |
|
364 \begin{center} |
|
365 \begin{tabular}{ll} |
|
366 (IMP1) & $nullable(r_1) \;\text{implies}\; |
|
367 POSIX (mkeps\; r_1)\; r_1$ \\ |
|
368 (IMP2) & $nullable(r_2) \;\text{implies}\; |
|
369 POSIX (mkeps\; r_2)\; r_2$ |
|
370 \end{tabular} |
|
371 \end{center} |
|
372 |
|
373 \noindent and know that $nullable(r_1 + r_2)$ holds. From this |
|
374 we know that either $nullable(r_1)$ holds or $nullable(r_2)$. |
|
375 Let us consider the first case where we know $nullable(r_1)$. |
|
376 |
|
377 |
351 \subsection*{Problems in the paper proof} |
378 \subsection*{Problems in the paper proof} |
352 |
379 |
353 I cannot verify |
380 I cannot verify |
354 |
381 |
355 \end{document} |
382 \end{document} |