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

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

    57 graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular

    57 graphs, matrices and functions are not easily formalisiable in HOL. In contrast, regular

    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

    62 \end{abstract}

    63 \end{abstract}

    63 \maketitle

    64 \maketitle

    64 

    65 

    65 \input{session}

    66 \input{session}

    66 

    67