Chunhan Wu, Xingyuan Zhang, Christian Urban. The Myhill-Nerode Theorem Based on Regular Expressions. Archive of Formal Proofs, 2011, 2011. [doi]
@article{WuZU11-0, title = {The Myhill-Nerode Theorem Based on Regular Expressions}, author = {Chunhan Wu and Xingyuan Zhang and Christian Urban}, year = {2011}, url = {http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}, note = {Formal proof development}, researchr = {https://researchr.org/publication/WuZU11-0}, cites = {0}, citedby = {0}, journal = {Archive of Formal Proofs}, volume = {2011}, }