Unified Decision Procedures for Regular Expression Equivalence by Tobias Nipkow and Dmitriy Traytel Jan 30