--- a/Paper/Paper.thy	Thu Feb 17 11:42:16 2011 +0000
+++ b/Paper/Paper.thy	Thu Feb 17 13:25:29 2011 +0000
@@ -865,12 +865,45 @@
 
 text {*
   In this paper we took the view that a regular language is one where there exists 
-  a regular expression that matches all its strings. For us it was important to find 
+  a regular expression that matches all its strings. For us it was ineteresting to find 
   out how far we can push this point of view. Having formalised the Myhill-Nerode
   theorem means pushed quite far. Having the Myhill-Nerode theorem means we can 
   formalise much of the textbook results in this subject. 
 
+  Our proof of the first direction is very much inspired by \emph{Brz
+  algebraic mehod} used to convert a finite atomaton to a regular
+  expression. The close connection can be seen by considering the equivalence
+  classes as the states of the minimal automaton for the regular language.
+  However there are some subtle differences. If we identify equivalence
+  classes with the states of the automaton, then the most natural choice is to
+  characterise each state with the set of strings starting from the initial
+  state leading up to that state. Usually the states are characterised as the
+  ones starting from that state leading to the terminal states.  The first
+  choice has consequences how the initial equational system is set up. We have
+  the $\lambda$-term on our ``initial state'', while Brz has it on the
+  terminal states. This means we also need to reverse the direction of Arden's
+  lemma.
 
+  We briefly considered using the method Brz presented in the Appendix of ???
+  in order to prove the second direction of the Myhill-Nerode thereom. There
+  he calculates the derivatives for regular expressions and shows that there
+  can be only finitely many of them. We could use as the tag of a string
+  @{text s} the derivative of a regular expression generated with respect to
+  @{text s}.  Using the fact that two strings are Myhill-Nerode related
+  whenever their derivative is the same together with the fact that there are
+  only finitely many derivatives for a regular expression would give us the
+  same argument. However it seems not so easy to calculate the derivatives
+  and then to count them. Therefore we preferred our direct method of
+  using tagging-functions involving equivalence classes. This is also where
+  our method shines, because we can completely side-step the standard 
+  argument \cite{Kozen97} where automata need to be composed, which is not so 
+  convenient to formalise in a HOL-based theorem prover.
+  
+
+  Lines of code / nuprl
+
+  closure properties
+  
 *}