--- a/Myhill_1.thy	Tue Feb 15 10:37:56 2011 +0000
+++ b/Myhill_1.thy	Tue Feb 15 12:01:29 2011 +0000
@@ -1148,10 +1148,15 @@
     unfolding Solve_def by (rule while_rule)
 qed
 
-lemma last_cl_exists_rexp:
-  assumes Inv_ES: "invariant {(X, xrhs)}"
-  shows "\<exists>r::rexp. L r = X" 
-proof-
+lemma every_eqcl_has_reg:
+  assumes finite_CS: "finite (UNIV // \<approx>A)"
+  and X_in_CS: "X \<in> (UNIV // \<approx>A)"
+  shows "\<exists>r::rexp. X = L r" 
+proof -
+  from finite_CS X_in_CS 
+  obtain xrhs where Inv_ES: "invariant {(X, xrhs)}"
+    using Solve by metis
+
   def A \<equiv> "Arden X xrhs"
   have "rhss xrhs \<subseteq> {X}" using Inv_ES 
     unfolding valid_eqs_def invariant_def rhss_def lhss_def
@@ -1172,19 +1177,7 @@
     by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn)
   then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp
   then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto
-  then show "\<exists>r::rexp. L r = X" by blast
-qed
-
-lemma every_eqcl_has_reg: 
-  assumes finite_CS: "finite (UNIV // \<approx>A)"
-  and X_in_CS: "X \<in> (UNIV // \<approx>A)"
-  shows "\<exists>r::rexp. L r = X"
-proof -
-  from finite_CS X_in_CS 
-  obtain xrhs where "invariant {(X, xrhs)}"
-    using Solve by metis
-  then show "\<exists>r::rexp. L r = X"
-    using last_cl_exists_rexp by auto
+  then show "\<exists>r::rexp. X = L r" by blast
 qed
 
 lemma bchoice_finite_set:

--- a/Paper/Paper.thy	Tue Feb 15 10:37:56 2011 +0000
+++ b/Paper/Paper.thy	Tue Feb 15 12:01:29 2011 +0000
@@ -705,6 +705,10 @@
   and @{term "invariant {(X, rhs)}"}.
   \end{lemma}
 
+  \noindent
+  With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
+  there exists a regular expression.
+
   \begin{lemma}\label{every_eqcl_has_reg}
   @{thm[mode=IfThen] every_eqcl_has_reg}
   \end{lemma}
@@ -714,20 +718,25 @@
   that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
   and that the invariant holds for this equation. That means we 
   know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
-  this is equal to @{text "\<Union>\<calL> ` (Arden X rhs)"} using ???.
-
+  this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties in the 
+  invariant and Lem.~???. Using the validity property for the equation @{text "X = rhs"},
+  we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation
+  removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
+  That means @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
+  So we can collect those (finitely many) regular expressions and have @{term "X = L (\<Uplus>rs)"}.
+  With this we can conclude the proof.\qed
   \end{proof}
 
-  \begin{theorem}
-  @{thm[mode=IfThen] Myhill_Nerode1}
-  \end{theorem}
+  \noindent
+  Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
+  of the Myhill-Nerode theorem.
 
-  \begin{proof}
+  \begin{proof}[of Thm.~\ref{myhillnerodeone}]
   By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular language for
   every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
   a subset of  @{term "UNIV // \<approx>A"}, we also know that for every equvalence class
   in @{term "finals A"} there exists a regular language. Moreover by assumption 
-  we know that @{term "finals A"} must be finite, therefore there must be a finite
+  we know that @{term "finals A"} must be finite, and therefore there must be a finite
   set of regular expressions @{text "rs"} such that
 
   \begin{center}