868   a regular expression that matches all its strings. For us it was important to find 

   868   a regular expression that matches all its strings. For us it was ineteresting to find 

   873 

   873   Our proof of the first direction is very much inspired by \emph{Brz

   874   algebraic mehod} used to convert a finite atomaton to a regular

   875   expression. The close connection can be seen by considering the equivalence

   876   classes as the states of the minimal automaton for the regular language.

   877   However there are some subtle differences. If we identify equivalence

   878   classes with the states of the automaton, then the most natural choice is to

   879   characterise each state with the set of strings starting from the initial

   880   state leading up to that state. Usually the states are characterised as the

   881   ones starting from that state leading to the terminal states.  The first

   882   choice has consequences how the initial equational system is set up. We have

   883   the $\lambda$-term on our ``initial state'', while Brz has it on the

   884   terminal states. This means we also need to reverse the direction of Arden's

   885   lemma.

   886 

   887   We briefly considered using the method Brz presented in the Appendix of ???

   888   in order to prove the second direction of the Myhill-Nerode thereom. There

   889   he calculates the derivatives for regular expressions and shows that there

   890   can be only finitely many of them. We could use as the tag of a string

   891   @{text s} the derivative of a regular expression generated with respect to

   892   @{text s}.  Using the fact that two strings are Myhill-Nerode related

   893   whenever their derivative is the same together with the fact that there are

   894   only finitely many derivatives for a regular expression would give us the

   895   same argument. However it seems not so easy to calculate the derivatives

   896   and then to count them. Therefore we preferred our direct method of

   897   using tagging-functions involving equivalence classes. This is also where

   898   our method shines, because we can completely side-step the standard 

   899   argument \cite{Kozen97} where automata need to be composed, which is not so 

   900   convenient to formalise in a HOL-based theorem prover.

   901   

   902 

   903   Lines of code / nuprl

   904 

   905   closure properties

   906