325   @{thm finals_def}

   325   @{thm finals_def}

   326   \end{equation}

   326   \end{equation}

   327 

   327 

   328   \noindent

   328   \noindent

   329   It is straightforward to show that @{thm lang_is_union_of_finals} and 

   329   It is straightforward to show that @{thm lang_is_union_of_finals} and 

   331   Therefore if we know that there exists a regular expression for every

   331   Therefore if we know that there exists a regular expression for every

   332   equivalence class in @{term "finals A"} (which by assumption must be

   332   equivalence class in @{term "finals A"} (which by assumption must be

   333   a finite set), then we can combine these regular expressions with @{const ALT}

   333   a finite set), then we can combine these regular expressions with @{const ALT}

   334   and obtain a regular expression that matches every string in @{text A}.

   334   and obtain a regular expression that matches every string in @{text A}.

   335 

   335 

   336 

   336 

   337   We prove Thm.~\ref{myhillnerodeone} by giving a method that can calculate a

   337   We prove Thm.~\ref{myhillnerodeone} by giving a method that can calculate a

   339   in @{term "finals A"}. We

   339   in @{term "finals A"}. We

   340   first define a notion of \emph{transition} between equivalence classes

   340   first define a notion of \emph{transition} between equivalence classes

   341   %

   341   %

   342   \begin{equation} 

   342   \begin{equation} 

   343   @{thm transition_def}

   343   @{thm transition_def}