The first subsection states and proves the Hopcroft and Ullman version of the Myhill-Nerode theorem. We modified their account slightly to enable a constructive proof, namely, we require an effective union in statement 2 and a decidable induced equivalence relation, . These changes are highlighted by enclosing
them in parentheses. We also use the terminology of the induced
equivalence relation defined at the end of section 4 rather than
defining that relation in the statement of the theorem as HU do.
After presenting the HU proof, we discuss its constructive
formalization and then examine the details of the proofs of the three
implications: called
,
called
and
called
. We
include text from the on-line libraries.