(*<*)
theory Paper
imports "../Myhill" "LaTeXsugar"
begin

declare [[show_question_marks = false]]

notation (latex output)
  str_eq_rel ("\<approx>\<^bsub>_\<^esub>")

(*>*)

section {* Introduction *}

text {*
  
*}


section {* Regular expressions have finitely many partitions *}

text {*

  \begin{lemma}
  Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.
  \end{lemma}  

  \begin{proof}
  By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}
  and @{const CHAR} are starightforward, because we can easily establish

  \begin{center}
  \begin{tabular}{l}
  @{thm quot_null_eq}\\
  @{thm quot_empty_subset}\\
  @{thm quot_char_subset}
  \end{tabular}
  \end{center}

  

  \end{proof}

*}


(*<*)
end
(*>*)