equal
deleted
inserted
replaced
20 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
20 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
21 \renewcommand{\isasymequiv}{$\dn$} |
21 \renewcommand{\isasymequiv}{$\dn$} |
22 \renewcommand{\isasymemptyset}{$\varnothing$} |
22 \renewcommand{\isasymemptyset}{$\varnothing$} |
23 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
23 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
24 |
24 |
25 |
25 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}} |
26 \begin{document} |
26 \begin{document} |
27 |
27 |
28 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
28 \title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular |
29 Expressions (Proof Pearl)} |
29 Expressions (Proof Pearl)} |
30 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}} |
30 \author{Chunhan Wu\inst{1} \and Xingjuan Zhang\inst{1} \and Christian Urban\inst{2}} |