--- a/Paper/Paper.thy	Sun Feb 20 12:52:35 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 20 13:43:00 2011 +0000
@@ -1117,7 +1117,7 @@
   If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
   then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
   @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
-  We have to show injectivity of this tagging function as
+  We have to show injectivity of this tagging-function as
 
   \begin{center}
   @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
@@ -1156,8 +1156,9 @@
   \end{proof}
   
   \noindent
-  The case for @{const STAR} is similar, but poses a few extra challenges. When
-  we analyse the case that @{text "x @ z"} is element in @{text "A\<star>"}, we 
+  The case for @{const STAR} is similar as @{const SEQ}, but poses a few extra challenges. When
+  we analyse the case that @{text "x @ z"} is element in @{text "A\<star>"} and @{text x} is not the 
+  empty string, we 
   have the following picture:
 
   \begin{center}
@@ -1199,8 +1200,8 @@
   \end{center}
 
   \noindent
-  We can find a prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"}
-  and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string 
+  We can find a strict prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"},
+  @{text "x' < x"} and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string 
   @{text "[]"} would do.
   There are many such prefixes, but there can only be finitely many of them (the 
   string @{text x} is finite). Let us therefore choose the longest one and call it 
@@ -1223,8 +1224,40 @@
   \end{center}
 
   \begin{proof}[@{const STAR}-Case]
+  If @{term "finite (UNIV // \<approx>A)"} 
+  then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
+  @{term "tag_str_STAR A"} is a subset of this set, and therefore finite.
+  Again we have to show injectivity of this tagging-function as  
 
+  \begin{center}
+  @{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
+  \end{center}  
 
+  \noindent
+  We first need to consider the case that @{text x} is the empty string.
+  From the assumption we can infer @{text y} is the empty string and
+  clearly have @{text "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
+  string, we can devide the string @{text "x @ z"} as shown in the picture 
+  above. By the tagging function we have
+
+  \begin{center}
+  @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"}
+  \end{center}
+
+  \noindent
+  which by assumption is equal to
+  
+  \begin{center}
+  @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
+  \end{center}
+
+  \noindent 
+  and we know that we have a @{text "y'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"} and @{text "y'\<^isub>m\<^isub>a\<^isub>x < y"}
+  and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y'\<^isub>m\<^isub>a\<^isub>x)"}. Unfolding the Myhill-Nerode
+  relation we know @{term "(y - y'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}. We also know that @{text "z\<^isub>b \<in> A\<star>"}.
+  Therefore, finally, @{text "y'\<^isub>m\<^isub>a\<^isub>x @ ((y - y'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
+  @{term "y @ z \<in> A\<star>"}. As a last step we have to set @{text "A"} to @{text "L r"} and
+  complete the proof.
   \end{proof}
 *}