5 

     6 declare [[show_question_marks = false]]

     7 

     8 notation (latex output)

     9   str_eq_rel ("\<approx>\<^bsub>_\<^esub>")

    10 

    19 

    20 section {* Regular expressions have finitely many partitions *}

    21 

    22 text {*

    23 

    24   \begin{lemma}

    25   Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.

    26   \end{lemma}  

    27 

    28   \begin{proof}

    29   By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}

    30   and @{const CHAR} are starightforward, because we can easily establish

    31 

    32   \begin{center}

    33   \begin{tabular}{l}

    34   @{thm quot_null_eq}\\

    35   @{thm quot_empty_subset}\\

    36   @{thm quot_char_subset}

    37   \end{tabular}

    38   \end{center}

    39 

    40   

    41 

    42   \end{proof}

    43 

    44 *}

    45 

    46