
diff -r c4893e84c88e -r 2455db3b06ac Journal/Paper.thy
--- a/Journal/Paper.thy	Wed Aug 03 00:52:41 2011 +0000
+++ b/Journal/Paper.thy	Wed Aug 03 12:36:23 2011 +0000
@@ -61,10 +61,10 @@
   uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
   tag_Plus ("+tag _ _" [100, 100] 100) and
   tag_Plus ("+tag _ _ _" [100, 100, 100] 100) and
-  tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
-  tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
-  tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
-  tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and
+  tag_Times ("\<times>tag _ _" [100, 100] 100) and
+  tag_Times ("\<times>tag _ _ _" [100, 100, 100] 100) and
+  tag_Star ("\<star>tag _" [100] 100) and
+  tag_Star ("\<star>tag _ _" [100, 100] 100) and
   tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
   Delta ("\<Delta>'(_')") and
   nullable ("\<delta>'(_')") and
@@ -640,7 +640,7 @@
   @{term "X\<^isub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
   @{term "X\<^isub>2"} & @{text "="} & @{text "(X\<^isub>1, ATOM c)"}\\
   @{term "X\<^isub>3"} & @{text "="} & @{text "(X\<^isub>1, ATOM d\<^isub>1) + \<dots> + (X\<^isub>1, ATOM d\<^isub>n)"}\\
-               & & \mbox{}\hspace{3mm}@{text "+ (X\<^isub>3, ATOM c\<^isub>1) + \<dots> + (X\<^isub>3, ATOM c\<^isub>m)"}
+               & & \mbox{}\hspace{10mm}@{text "+ (X\<^isub>3, ATOM c\<^isub>1) + \<dots> + (X\<^isub>3, ATOM c\<^isub>m)"}
   \end{tabular}}
   \end{equation}
   
@@ -756,9 +756,9 @@
   \begin{center}
   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
   @{term "X\<^isub>3"} & @{text "="} & 
-    @{text "(X\<^isub>1, TIMES (ATOM d\<^isub>1) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>,ATOM c\<^isub>m})) + \<dots> "}\\
+    @{text "(X\<^isub>1, TIMES (ATOM d\<^isub>1) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m})) + \<dots> "}\\
   & & \mbox{}\hspace{13mm}
-     @{text "\<dots> + (X\<^isub>1, TIMES (ATOM d\<^isub>n) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>,ATOM c\<^isub>m}))"}
+     @{text "\<dots> + (X\<^isub>1, TIMES (ATOM d\<^isub>n) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m}))"}
   \end{tabular}
   \end{center}
 
@@ -766,7 +766,7 @@
   \noindent
   That means we eliminated the dependency of @{text "X\<^isub>3"} on the
   right-hand side.  Note we used the abbreviation 
-  @{text "\<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>,ATOM c\<^isub>m}"} 
+  @{text "\<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m}"} 
   to stand for a regular expression that matches with every character. In 
   our algorithm we are only interested in the existence of such a regular expression
   and do not specify it any further. 
@@ -1141,9 +1141,15 @@
   The relation @{term "\<approx>(lang r)"} partitions the set of all strings into some
   equivalence classes. To show that there are only finitely many of them, it
   suffices to show in each induction step that another relation, say @{text
-  R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}. A
-  relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"}
-  provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. For constructing @{text R} will
+  R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}. 
+
+  \begin{dfntn}
+  A relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"}
+  provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. 
+  \end{dfntn}
+
+  \noindent
+  For constructing @{text R} will
   rely on some \emph{tagging-functions} defined over strings. Given the
   inductive hypothesis, it will be easy to prove that the \emph{range} of
   these tagging-functions is finite. The range of a function @{text f} is
@@ -1235,9 +1241,10 @@
 
   \noindent
   where @{text "A"} and @{text "B"} are some arbitrary languages. The reason for this choice 
-  is that we need to that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}. This amounts
-  to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption
-  @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. The definition will allow to infer this.
+  is that we need to establish that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}. 
+  This amounts to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption
+  @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. As we shall see, this definition will 
+  provide us just the right assumptions in order to get the proof through.
 
  \begin{proof}[@{const "PLUS"}-Case]
   We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite
@@ -1245,49 +1252,68 @@
   holds. The range of @{term "tag_Plus A B"} is a subset of this product
   set---so finite. For the refinement proof-obligation, we know that @{term
   "(\<approx>A `` {x}, \<approx>B `` {x}) = (\<approx>A `` {y}, \<approx>B `` {y})"} holds by assumption. Then
-  clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"} hold, as we needed to
+  clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"}, as we needed to
   show. Finally we can discharge this case by setting @{text A} to @{term
   "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
   \end{proof}
 
+  \noindent
+  The @{const TIMES}-case is slightly more complicated. We first prove the
+  following lemma, which will aid the refinement-proofs.
+
+  \begin{lmm}\label{refinement}
+  The relation @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} refines @{term "\<approx>A"}, provided for
+  all strings @{text x}, @{text y} and @{text z} we have \mbox{@{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y"}}
+  and @{term "x @ z \<in> A"} imply @{text "y @ z \<in> A"}.
+  \end{lmm}
+
 
   \noindent
-  The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
-  they are slightly more complicated. In the @{const TIMES}-case we essentially have
-  to be able to infer that 
-  %
-  \begin{center}
-  @{text "\<dots>"}@{term "x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
-  \end{center}
-  %
-  \noindent
-  using the information given by the appropriate tagging-function. The complication 
-  is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A \<cdot> B"}
-  (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the
-  notions of \emph{string prefixes} 
-  %
-  \begin{center}
-  \begin{tabular}{l}
-  @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\
-  @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
-  \end{tabular}
-  \end{center}
-  %
-  \noindent
-  and \emph{string subtraction}:
+  We therefore can clean information from how the strings @{text "x @ z"} are in @{text A}
+  and construct appropriate tagging-functions to infer that @{term "y @ z \<in> A"}.
+  For the @{const Times}-case we additionally need the notion of the set of all
+  possible partitions of a string
 
-  \noindent
-  where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. 
-  
+  \begin{equation}
+  @{thm Partitions_def}
+  \end{equation}
+
   Now assuming  @{term "x @ z \<in> A \<cdot> B"} there are only two possible ways of how to `split' 
   this string to be in @{term "A \<cdot> B"}:
   %
   \begin{center}
   \begin{tabular}{c}
-  \scalebox{0.9}{
+  \scalebox{1}{
   \begin{tikzpicture}
-    \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };
+    \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z\<^isub>p"}\hspace{0.6em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z\<^isub>s"}\hspace{2.6em}$  };
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           (x.north west) -- ($(za.north west)+(0em,0em)$)
+               node[midway, above=0.5em]{@{text x}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
+               node[midway, above=0.5em]{@{text z}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
+               node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "x @ z\<^isub>p \<in> A"}};
+
+    \draw[decoration={brace,transform={yscale=3}},decorate]
+           ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
+               node[midway, below=0.5em]{@{text "z\<^isub>s \<in> B"}};
+  \end{tikzpicture}}
+  \\[2mm]
+  \scalebox{1}{
+  \begin{tikzpicture}
+    \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x\<^isub>p"}\hspace{3em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x\<^isub>s"}\hspace{0.2em}$ };
     \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
@@ -1304,109 +1330,102 @@
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};
+               node[midway, below=0.5em]{@{term "x\<^isub>s @ z \<in> B"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{term "x' \<in> A"}};
-  \end{tikzpicture}}
-  \\
-  \scalebox{0.9}{
-  \begin{tikzpicture}
-    \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z - z'"}\hspace{2.6em}$  };
-
-    \draw[decoration={brace,transform={yscale=3}},decorate]
-           (x.north west) -- ($(za.north west)+(0em,0em)$)
-               node[midway, above=0.5em]{@{text x}};
-
-    \draw[decoration={brace,transform={yscale=3}},decorate]
-           ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
-               node[midway, above=0.5em]{@{text z}};
-
-    \draw[decoration={brace,transform={yscale=3}},decorate]
-           ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
-               node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
-
-    \draw[decoration={brace,transform={yscale=3}},decorate]
-           ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};
-
-    \draw[decoration={brace,transform={yscale=3}},decorate]
-           ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
+               node[midway, below=0.5em]{@{term "x\<^isub>p \<in> A"}};
   \end{tikzpicture}}
   \end{tabular}
   \end{center}
   %
   \noindent
-  Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),
-  or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
-  In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. For this we use the 
-  following tagging-function
-  %
+  Either @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} 
+  (first picture) or there is a prefix of @{text x} in @{text A} and the rest is in @{text B} 
+  (second picture). In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. The first case
+  we will only go through if we know that  @{term "x \<approx>A y"} holds @{text "(*)"}. Because then 
+  we can infer from @{term "x @ z\<^isub>p \<in> A"} that @{term "y @ z\<^isub>p \<in> A"} holds for all @{text "z\<^isub>p"}.
+  In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is a possible partition
+  of the string @{text x}. So we have to know that @{text "x\<^isub>p"} is `@{text A}-related' to the
+  corresponding partition @{text "y\<^isub>p"}, repsectively that @{text "x\<^isub>s"} is `@{text B}-related' 
+  to @{text "y\<^isub>s"} @{text "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
+  Taking the two requirements @{text "(*)"} and @{text "(**)"}, we define the
+  tagging-function:
+
   \begin{center}
-  @{thm tag_Times_def[where ?A="A" and ?B="B", THEN meta_eq_app]}
+  @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\<equiv>"}~
+  @{text ""}
   \end{center}
 
   \noindent
-  with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}
-  is in the language @{text B}.
+  With this definition in place, we can discharge the @{const "Times"}-case as follows.
+
 
   \begin{proof}[@{const TIMES}-Case]
   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_Times A B"} is a subset of this product set, and therefore finite.
-  We have to show injectivity of this tagging-function as
-  %
+  By Lemma \ref{refinement} we know
+
   \begin{center}
-  @{term "\<forall>z. tag_Times A B x = tag_Times A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
+   @{term "tag_Times A B x = tag_Times A B y"}
   \end{center}
-  %
+
   \noindent
-  There are two cases to be considered (see pictures above). First, there exists 
-  a @{text "x'"} such that
-  @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have
-  %
+  and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot> B"}. As shown
+  above, there are two cases to be considered (see pictures above). First, 
+  there exists a @{text "z\<^isub>p"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s \<in> B"}.
+  By the assumption about @{term "tag_Times A B"} we have
+  @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
+  relation that @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"}, we can conclude in this case
+  with @{term "y @ z \<in> A \<cdot> B"}.
+
+  Second there exists a @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{term "x\<^isub>p @ x\<^isub>s = x"},
+  @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have
+  
   \begin{center}
-  @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}
+  @{term "(\<approx>A `` {x\<^isub>p}, \<approx>B `` {x\<^isub>s}) \<in> ({(\<approx>A `` {x\<^isub>p}, \<approx>B `` {x\<^isub>s}) | x\<^isub>p x\<^isub>s. (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}
   \end{center}
-  %
+  
   \noindent
   and by the assumption about @{term "tag_Times A B"} also 
-  %
+  
   \begin{center}
-  @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
+  @{term "(\<approx>A `` {x\<^isub>p}, \<approx>B `` {x\<^isub>s}) \<in> ({(\<approx>A `` {y\<^isub>p}, \<approx>B `` {y\<^isub>s}) | y\<^isub>p y\<^isub>s. (y\<^isub>p, y\<^isub>s) \<in> Partitions y})"}
   \end{center}
-  %
-  \noindent
-  That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and 
-  @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
-  @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode
-  relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
-  have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore
-  @{term "y @ z \<in> A \<cdot> B"}, as needed in this case.
-
-  Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
-  By the assumption about @{term "tag_Times A B"} we have
-  @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
-  relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
-  with @{term "y @ z \<in> A \<cdot> B"}. We again can complete the @{const TIMES}-case
-  by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}. 
-  \end{proof}
   
   \noindent
-  The case for @{const Star} is similar to @{const TIMES}, but poses a few extra challenges. When
-  we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the 
-  empty string, we 
-  have the following picture:
-  %
+  That means there must be a @{text "y\<^isub>p"} and @{text "y\<^isub>s"}
+  such that @{text "y\<^isub>p @ y\<^isub>s = y"}. Moreover @{term "\<approx>A ``
+  {x\<^isub>p} = \<approx>A `` {y\<^isub>p}"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B ``
+  {y\<^isub>s}"}. Unfolding the Myhill-Nerode relation and together with the
+  facts that @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}, we
+  @{term "y\<^isub>p \<in> A"} and have @{text "y\<^isub>s @ z \<in> B"}, as needed in
+  this case.  We again can complete the @{const TIMES}-case by setting @{text
+  A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
+  \end{proof}
+
+  \noindent
+  The case for @{const Star} is similar to @{const TIMES}, but poses a few
+  extra challenges.  To deal with them we define first the notions of a \emph{string
+  prefix} and a \emph{strict string prefix}:
+
   \begin{center}
-  \scalebox{0.7}{
+  \begin{tabular}{l}
+  @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\
+  @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  When we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"}
+  and @{text x} is not the empty string, we have the following picture:
+
+  \begin{center}
+  \scalebox{1}{
   \begin{tikzpicture}
-    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ };
+    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x\<^bsub>pmax\<^esub>"}\hspace{4em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x\<^bsub>s\<^esub>"}\hspace{0.5em}$ };
     \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
     \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
 
@@ -1424,11 +1443,11 @@
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}};
+               node[midway, below=0.5em]{@{text "x\<^isub>s @ z\<^isub>a \<in> A"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{term "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
+               node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<star>"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
@@ -1436,26 +1455,28 @@
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
-               node[midway, below=0.5em]{@{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
+               node[midway, below=0.5em]{@{term "x\<^isub>s @ z \<in> A\<star>"}};
   \end{tikzpicture}}
   \end{center}
   %
   \noindent
-  We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},
-  @{text "x' < x"} and the rest @{term "(x - x') @ z \<in> A\<star>"}. For example the empty string 
+  We can find a strict prefix @{text "x\<^isub>p"} of @{text x} such that @{term "x\<^isub>p \<in> A\<star>"},
+  @{text "x\<^isub>p < x"} and the rest @{term "x\<^isub>s @ z \<in> A\<star>"}. For example the empty string 
   @{text "[]"} would do.
   There are potentially 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 
-  @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we
+  @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we
   know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, we can separate
   this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
-  and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},
-  otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a}
+  and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"},
+  otherwise @{text "x\<^bsub>pmax\<^esub>"} is not the longest prefix. That means @{text a}
   `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
-   @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and
+   @{text "z\<^isub>b"}. For this we know that @{text "x\<^isub>s @ z\<^isub>a \<in> A"} and
   @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
   such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
-  `border' of @{text x} and @{text z}. This string is @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a"}.
+  `border' of @{text x} and @{text z}. This string is @{text "x\<^isub>s @ z\<^isub>a"}.
+
+  HERE
 
   In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
   the following tagging-function:




