2 %\documentclass[acmtocl,final]{acmtrans2m}

     2 %\documentclass[acmtocl,final]{acmtrans2m}

     3 \usepackage{isabelle}

     3 \usepackage{isabelle}

     4 \usepackage{isabellesym}

     4 \usepackage{isabellesym}

     5 \usepackage{amsmath}

     5 \usepackage{amsmath}

     6 \usepackage{amssymb}

     6 \usepackage{amssymb}

     7 \usepackage{tikz}

     8 \usepackage{tikz}

     8 \usepackage{pgf}

     9 \usepackage{pgf}

     9 \usetikzlibrary{arrows,automata,decorations,fit,calc}

    10 \usetikzlibrary{arrows,automata,decorations,fit,calc}

    10 \usetikzlibrary{shapes,shapes.arrows,snakes,positioning}

    11 \usetikzlibrary{shapes,shapes.arrows,snakes,positioning}

    11 \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf

    12 \usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf

    39 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}}

    40 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}}

    40 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

    41 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}

    41 

    42 

    42 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}

    43 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}

    43 

    44 

    48 

    49 

    49 \begin{document}

    50 \begin{document}

    50 

    51 

    51 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular

    52 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular

    52   Expressions$^\star$\thanks{$^\star$ This is a revised and much expanded version of \cite{WuZhangUrban11}.}}

    53   Expressions$^\star$\thanks{$^\star$ This is a revised and much expanded version of \cite{WuZhangUrban11}.}}

    56 %Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and

    57 %Xingyuan Zhang\\PLA University of Science and Technology Nanjing, China \and

    57 %Christian Urban\\ King's College London, United Kingdom}

    58 %Christian Urban\\ King's College London, United Kingdom}

    58 

    59 

    59 \author{Chunhan Wu \and Xingyuan Zhang \and Christian Urban}

    60 \author{Chunhan Wu \and Xingyuan Zhang \and Christian Urban}

    60 \institute{Chunhan Wu \and Xingyuan Zhang \at PLA University of Science and Technology Nanjing, China \and

    61 \institute{Chunhan Wu \and Xingyuan Zhang \at PLA University of Science and Technology Nanjing, China \and

    62 

    63 

    63 \date{Received: date / Accepted: date}

    64 \date{Received: date / Accepted: date}

    64 

    65 

    65 %\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular

    66 %\markboth{C.~Wu et al.}{A Formalisation of the Myhill-Nerode Theorem based on Regular

    66 %  Expressions}

    67 %  Expressions}