--- 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}