--- a/Closures.thy	Wed Sep 14 11:46:50 2011 +0000
+++ b/Closures.thy	Wed Sep 14 13:00:44 2011 +0000
@@ -253,29 +253,34 @@
 definition
   "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)"
 
-lemma length_test:
-  "x = y \<Longrightarrow> length_test x a b = length_test y a b"
-by simp
-
 lemma an_bn_not_regular:
   shows "\<not> regular (\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n})"
 proof
   def A\<equiv>"\<Union>n. {CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n}"
   def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}"
-
   assume as: "regular A"
   def B\<equiv>"\<Union>n. {CHR ''a'' ^^^ n}"
+
+  have length_test: "\<And>s. s \<in> A \<Longrightarrow> length_test s (CHR ''a'') (CHR ''b'')"
+    unfolding A_def length_test_def by auto
+
   have b: "infinite B"
     unfolding infinite_iff_countable_subset
     unfolding inj_on_def B_def
     by (rule_tac x="\<lambda>n. CHR ''a'' ^^^ n" in exI) (auto)
   moreover
-  have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" 
-    apply(auto simp add: B_def A_def)
-    apply(auto simp add: str_eq_def)
-    apply(drule_tac x="CHR ''b'' ^^^ aa" in spec)
+  have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)"
+    apply(auto)
+    unfolding B_def
     apply(auto)
-    apply(drule_tac a="CHR ''a''" and b="CHR ''b''" in length_test)
+    apply(simp add: str_eq_def)
+    apply(drule_tac x="CHR ''b'' ^^^ n" in spec)
+    apply(subgoal_tac "CHR ''a'' ^^^ na @ CHR ''b'' ^^^ n \<notin> A")
+    apply(subgoal_tac "CHR ''a'' ^^^ n @ CHR ''b'' ^^^ n \<in> A")
+    apply(blast)
+    apply(auto simp add: A_def)[1]
+    apply(rule notI)
+    apply(drule length_test)
     apply(simp add: length_test_def)
     done
   ultimately 

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