497   Property @{text "(iv)"} states that a non-empty string in @{term "A\<star>"} can

   497   Property @{text "(iv)"} states that a non-empty string in @{term "A\<star>"} can

   498   always be split up into a non-empty prefix belonging to @{text "A"} and the

   498   always be split up into a non-empty prefix belonging to @{text "A"} and the

   499   rest being in @{term "A\<star>"}. We omit

   499   rest being in @{term "A\<star>"}. We omit

   500   the proofs for these properties, but invite the reader to consult our

   500   the proofs for these properties, but invite the reader to consult our

   501   formalisation.\footnote{Available in the Archive of Formal Proofs at 

   501   formalisation.\footnote{Available in the Archive of Formal Proofs at 

   503   \cite{myhillnerodeafp11}.}

   503   \cite{myhillnerodeafp11}.}

   504 

   504 

   505   The notation in Isabelle/HOL for the quotient of a language @{text A}

   505   The notation in Isabelle/HOL for the quotient of a language @{text A}

   506   according to an equivalence relation @{term REL} is @{term "A // REL"}. We

   506   according to an equivalence relation @{term REL} is @{term "A // REL"}. We

   507   will write @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined as

   507   will write @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined as

  2472   needed approximately 3 months and this included the time to find our proof

  2472   needed approximately 3 months and this included the time to find our proof

  2473   arguments. Unlike Constable et al, who were able to follow the Myhill-Nerode 

  2473   arguments. Unlike Constable et al, who were able to follow the Myhill-Nerode 

  2474   proof from \cite{HopcroftUllman69}, we had to find our own arguments.  So for us the

  2474   proof from \cite{HopcroftUllman69}, we had to find our own arguments.  So for us the

  2475   formalisation was not the bottleneck.  The code of

  2475   formalisation was not the bottleneck.  The code of

  2476   our formalisation can be found in the Archive of Formal Proofs at

  2476   our formalisation can be found in the Archive of Formal Proofs at

  2478   \cite{myhillnerodeafp11}.\medskip

  2478   \cite{myhillnerodeafp11}.\medskip

  2479   

  2479   

  2480   \noindent

  2480   \noindent

  2481   {\bf Acknowledgements:}

  2481   {\bf Acknowledgements:}

  2482   We are grateful for the comments we received from Larry Paulson.  Tobias

  2482   We are grateful for the comments we received from Larry Paulson.  Tobias