--- a/Paper/Paper.thy	Sat Feb 19 19:27:33 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 19 20:15:59 2011 +0000
@@ -976,9 +976,26 @@
   where @{text "A"} and @{text "B"} are some arbitrary languages.
   We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
   then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
-  @{term "tag_str_ALT A B"} is a subset of this. It remains to be shown
-  that @{text "=tag\<^isub>A\<^isub>L\<^isub>T="} refines @{text "\<approx>(A \<union> B)"}.
+  @{term "tag_str_ALT A B"} is a subset of this product set. It remains to show
+  that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to 
+  showing
+  %
+  \begin{center}
+  @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
+  \end{center}
 
+  \noindent
+  which by unfolding the Myhill-Nerode relation is identical to
+  %
+  \begin{equation}\label{pattern}
+  @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
+  \end{equation}
+
+  \noindent
+  since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
+  \eqref{pattern} we just have to unfold the tagging-relation and analyse 
+  in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. Fianlly we
+  can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
   \end{proof}