--- a/Journal/Paper.thy	Wed Sep 14 11:46:50 2011 +0000
+++ b/Journal/Paper.thy	Wed Sep 14 13:00:44 2011 +0000
@@ -2297,15 +2297,16 @@
   \end{lmm} 
 
   \begin{proof}
-  After unfolding the definitions, we need to establish that for @{term "i \<noteq> j"},
-  the equality \mbox{@{text "a\<^sup>i @ b\<^sup>j = a\<^sup>n @ b\<^sup>n"}} leads to a contradiction. This is clearly the case
-  if we test that the two strings have the same amount of @{text a}'s and @{text b}'s;
-  the string on the right-hand side satisfies this property, but not the one on
-  the left-hand side. Therefore the strings cannot be equal and we have a contradiction.
+  After unfolding the definition of @{text "B"}, we need to establish that given @{term "i \<noteq> j"},
+  the strings @{text "a\<^sup>i"} and @{text "a\<^sup>j"} are not Myhill-Nerode related by @{text "A"}.
+  That means we have to show that \mbox{@{text "\<forall>z. a\<^sup>i @ z \<in> A = a\<^sup>j @ z \<in> A"}} leads to 
+  a contradiction. Let us take @{text "b\<^sup>i"} for @{text "z"}. Then we know @{text "a\<^sup>i @ b\<^sup>i \<in> A"}.
+  But since @{term "i \<noteq> j"}, @{text "a\<^sup>j @ b\<^sup>i \<notin> A"}. Therefore  @{text "a\<^sup>i"} and @{text "a\<^sup>j"}
+  cannot be Myhill-Nerode related by @{text "A"} and we are done.
   \end{proof}
 
   \noindent
-  To conclude the proof on non-regularity of language @{text A}, the
+  To conclude the proof of non-regularity for the language @{text A}, the
   Continuation Lemma and the lemma above lead to a contradiction assuming
   @{text A} is regular. Therefore the language @{text A} is not regular, as we
   wanted to show.