--- a/Paper/Paper.thy	Sat Feb 19 10:23:51 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 19 12:01:16 2011 +0000
@@ -365,10 +365,13 @@
   The key definition in the Myhill-Nerode theorem is the
   \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two 
   strings are related, provided there is no distinguishing extension in this
-  language. This can be defined as tertiary relation:
+  language. This can be defined as tertiary relation.
 
-  \begin{definition}[Myhill-Nerode Relation]\mbox{}\\
+  \begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
+  @{text y} are related provided
+  \begin{center}
   @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
+  \end{center}
   \end{definition}
 
   \noindent
@@ -877,10 +880,52 @@
   \end{proof}
 
   \noindent
-  Much more interesting are the inductive cases, which seem hard to be solved 
-  directly. The reader is invited to try. Our method will rely on some
+  Much more interesting, however, are the inductive cases. They seem hard to be solved 
+  directly. The reader is invited to try. 
+
+  Our method will rely on some
   \emph{tagging} functions of strings. Given the inductive hypothesis, it will 
   be easy to prove that the range of these tagging functions is finite.
+  With this we will be able to infer that the tagging functions, seen as a relation,
+  give rise to finitely many equivalence classes of @{const UNIV}. Finally we 
+  will show that the tagging relation is more refined than @{term "\<approx>(L r)"}, which
+  implies that @{term "UNIV // \<approx>(L r)"} must also be finite. For this we define the 
+  notion of a \emph{tag-relation} (which is often also called a kernel relation).
+
+  \begin{definition}[Tag-Relation] Given a tag-function @{text tag}, then two strings @{text x}
+  and @{text y} are tag-related provided
+  \begin{center}
+  @{text "x =tag= y \<equiv> tag x = tag y"}
+  \end{center}
+  \end{definition}
+
+  \begin{lemma}\label{finone}
+  @{thm[mode=IfThen] finite_eq_tag_rel}
+  \end{lemma}
+
+  \begin{proof}
+
+  \end{proof}
+
+  \noindent
+  
+
+  \begin{lemma}\label{fintwo} 
+  Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, then
+  if @{thm (prem 1) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+  and @{thm (prem 2) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+  then @{thm (concl) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
+  \end{lemma}
+
+  \begin{proof}
+
+  \end{proof}
+
+  \noindent
+  Stringing Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
+  that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose
+  range is finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
+
 
   @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]}
 
@@ -890,6 +935,7 @@
 *}
 
 
+
 section {* Conclusion and Related Work *}
 
 text {*