52 introduce the subject by describing finite automata and only mentioning on the

    52 introduce the subject by describing finite automata and only mentioning on the

    53 side a connection with regular expressions. Unfortunately, automata are difficult

    53 side a connection with regular expressions. Unfortunately, automata are difficult

    54 to formalise in HOL-based theorem provers. The reason is that

    54 to formalise in HOL-based theorem provers. The reason is that

    55 they need to be represented as graphs, matrices or functions, none of which

    55 they need to be represented as graphs, matrices or functions, none of which

    56 are inductive datatypes. Also convenient operations for disjoint unions of

    56 are inductive datatypes. Also convenient operations for disjoint unions of

    58 expressions can be defined conveniently as a datatype and a corresponding

    58 expressions can be defined conveniently as a datatype and a corresponding

    59 reasoning infrastructure comes for free. We show in this paper that a central

    59 reasoning infrastructure comes for free. We show in this paper that a central

    60 result from formal language theory---the Myhill-Nerode theorem---can be

    60 result from formal language theory---the Myhill-Nerode theorem---can be

    61 recreated using only regular expressions.

    61 recreated using only regular expressions.

    62 \end{abstract}

    62 \end{abstract}