The Myhill–Nerode theorem