Automata Library

Aleksey Nogin took the original automata library and removed unnecessary exponentials from the proof of Myhill - Nerode theorem (see his technical report for more information).