--- a/Journal/Paper.thy	Thu Oct 03 15:29:03 2013 +0100
+++ b/Journal/Paper.thy	Sun Nov 10 17:07:19 2013 +0000
@@ -496,8 +496,8 @@
   To our best knowledge, our proof of the Myhill-Nerode Theorem is the first
   that is based on regular expressions, only. The part of this theorem stating
   that finitely many partitions imply regularity of the language is proved by
-  an argument about solving equational systems.  This argument appears to be
-  folklore. For the other part, we give two proofs: one direct proof using
+  an argument about solving equational systems.  This argument requires a
+  `reversed' version of Arden's Lemma. For the other part, we give two proofs: one direct proof using
   certain tagging-functions, and another indirect proof using Antimirov's
   partial derivatives (\citeyear{Antimirov95}). Again to our best knowledge, the
   tagging-functions have not been used before for establishing the Myhill-Nerode
@@ -2502,7 +2502,7 @@
   Pumping Lemma).  We can also use it to establish the standard
   textbook results about closure properties of regular languages. The case of 
   closure under complement follows easily from the Myhill-Nerode Theorem.
-  So our answer to Gasarch is ``{\it yes we can''}!  
+  So our answer to Gasarch is `{\it yes we can'}!  
 
   %Our insistence on regular expressions for proving the Myhill-Nerode Theorem
   %arose from the problem of defining formally the regularity of a language.
@@ -2551,8 +2551,9 @@
   been formally established, we refer the reader to 
   \citeN{OwensSlind08}. In our opinion, their formalisation is considerably
   slicker than for example the approach to regular expression matching taken
-  by \citeN{Harper99} and by \citeN{Yi06}.
+  by \citeN{Harper99} and by \citeN{Yi06}. 
 
+ 
   Our proof of the first direction is very much inspired by \emph{Brzozowski's
   algebraic method} \citeyear{Brzozowski64} used to convert a finite automaton to a regular expression. 
   The close connection can be seen by considering the
@@ -2566,8 +2567,8 @@
   equational system is set up. We have the $\lambda$-term on our `initial
   state', while Brzozowski has it on the terminal states. This means we also
   need to reverse the direction of Arden's Lemma. We have not found anything
-  in the `pencil-and-paper-reasoning' literature about our way of proving the 
-  first direction of the Myhill-Nerode Theorem, but it appears to be folklore.
+  in the literature about our way of proving the 
+  first direction of the Myhill-Nerode Theorem.
 
   We presented two proofs for the second direction of the
   Myhill-Nerode Theorem. One direct proof using tagging-functions and
@@ -2677,6 +2678,16 @@
   our formalisation \cite{myhillnerodeafp11} can be found in the Archive of Formal Proofs at 
   \mbox{\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}}.
   
+   In this paper we leave out a discussion
+  about the computational content of our proofs. While the described algorithms
+  (for instance for solving our equational systems) are exectuable as is, we 
+  have cut some `computational corners' in our formalisation. For example, we did 
+  not specify which particular equation should be chosen in each step, rather 
+  proved that any choice will do. Similarly with our $\bigplus$-operation, we 
+  did not specify the order in which the regular expression should be composed, rather
+  proved that any composition with @{term PLUS} will do.
+ 
+
   Our future work will focus on formalising the regular expression matchers
   developed by \citeN{Sulzmann12} which generate variable assignments for
   regular expression sub-matching. For this they use both, derivatives and

Binary file journal.pdf has changed