--- a/Myhill_1.thy	Tue Feb 15 14:17:31 2011 +0000
+++ b/Myhill_1.thy	Wed Feb 16 06:51:58 2011 +0000
@@ -328,7 +328,7 @@
 definition 
   finals :: "lang \<Rightarrow> lang set"
 where
-  "finals A \<equiv> {\<approx>A `` {x} | x . x \<in> A}"
+  "finals A \<equiv> {\<approx>A `` {s} | s . s \<in> A}"
 
 
 lemma lang_is_union_of_finals: 

--- a/Paper/Paper.thy	Tue Feb 15 14:17:31 2011 +0000
+++ b/Paper/Paper.thy	Wed Feb 16 06:51:58 2011 +0000
@@ -371,7 +371,7 @@
   \noindent
   It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
   partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
-  equivalence classes. To illustrate this quotient construction, let us give an 
+  equivalence classes. To illustrate this quotient construction, let us give a simple 
   example: consider the regular language containing just
   the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
   into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and  @{text "X\<^isub>3"}
@@ -483,10 +483,12 @@
   \noindent
   The reason for adding the @{text \<lambda>}-marker to our initial equational system is 
   to obtain this equation: it only holds with the marker, since none of 
-  the other terms contain the empty string. 
+  the other terms contain the empty string. The point of the initial equational system is
+  that solving it means we will be able to extract a regular expression for every equivalence class. 
 
   Our representation for the equations in Isabelle/HOL are pairs,
-  where the first component is an equivalence class and the second component
+  where the first component is an equivalence class (a set of strings)
+  and the second component
   is a set of terms. Given a set of equivalence
   classes @{text CS}, our initial equational system @{term "Init CS"} is thus 
   formally defined as
@@ -515,16 +517,16 @@
   \noindent
   Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
   initial equational system into one in \emph{solved form} maintaining the invariant
-  in Lemma \ref{inv}. From the solved form we will be able to read
+  in Lem.~\ref{inv}. From the solved form we will be able to read
   off the regular expressions. 
 
   In order to transform an equational system into solved form, we have two 
   operations: one that takes an equation of the form @{text "X = rhs"} and removes
-  the recursive occurences of @{text X} in the @{text rhs} using our variant of Arden's 
+  any recursive occurences of @{text X} in the @{text rhs} using our variant of Arden's 
   Lemma. The other operation takes an equation @{text "X = rhs"}
   and substitutes @{text X} throughout the rest of the equational system
   adjusting the remaining regular expressions approriately. To define this adjustment 
-  we define the \emph{append-operation} 
+  we define the \emph{append-operation} taking a term and a regular expression as argument
 
   \begin{center}
   @{thm append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
@@ -532,7 +534,7 @@
   \end{center}
 
   \noindent
-  which we also lift to entire right-hand sides of equations, written as
+  We lift this operation to entire right-hand sides of equations, written as
   @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
   the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
   
@@ -590,10 +592,10 @@
   will be left in the system. However, we not just want to have any equation
   as being the last one, but the one involving the equivalence class for 
   which we want to calculate the regular 
-  expression. Let us suppose the equivalence class is @{text X}. 
+  expression. Let us suppose this equivalence class is @{text X}. 
   Since @{text X} is the one to be solved, in every iteration step we have to pick an
-  equation to be eliminated that which is different from @{text X}. In this way 
-  @{text X} is kept to the final step. The choice is implemented by Hilbert's choice 
+  equation to be eliminated that is different from @{text X}. In this way 
+  @{text X} is kept to the final step. The choice is implemented using Hilbert's choice 
   operator, written @{text SOME} in the definition below.
   
   \begin{center}
@@ -623,7 +625,7 @@
   properties about our definition of @{const Solve} when we ``call'' it with
   the equivalence class @{text X} and the initial equational system 
   @{term "Init (UNIV // \<approx>A)"} from
-  \eqref{initcs}:
+  \eqref{initcs} using the principle:
 
 
   \begin{center}
@@ -648,7 +650,7 @@
   once the condition does not hold anymore then the property @{text P} must hold.
 
   The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
-  returns with a single equation @{text "X = xrhs"}, for some @{text "xrhs"} and
+  returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and
   that this equational system still satisfies the invariant. In order to get
   the proof through, the invariant is composed of the following six properties:
 
@@ -667,7 +669,26 @@
  
   \noindent
   The first two ensure that the equational system is always finite (number of equations
-  and number of terms in each equation); \ldots
+  and number of terms in each equation); the second makes sure the ``meaning'' of the 
+  equations is preserved under our transformations. The other properties are a bit more
+  technical, but are needed to get our proof through. Distinctness states that every
+  equation in the system is distinct; @{text "ardenable"} ensures that we can always
+  apply the arden operation. For this we have to make sure that in every @{text rhs}, 
+  terms of the form @{term "Trn Y r"} cannot have a regular expresion that matches the
+  empty string. Therefore @{text "rhs_nonempty"} is defined as
+
+  \begin{center}
+  @{thm rhs_nonempty_def}
+  \end{center}
+
+  \noindent
+  The last property states that every @{text rhs} can only contain equivalence classes
+  for which there is an equation. Therefore @{text lhss} is just the set containing 
+  the first components of an equational system,
+  while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the 
+  form @{term "Trn X r"} (that means @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"} 
+  and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}).
+  
 
   It is straightforward to prove that the inital equational system satisfies the
   invariant.