diff -r 60bcf13adb77 -r e5e32faa2446 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Jul 11 16:46:05 2013 +0100
+++ b/Paper/Paper.thy	Thu Sep 12 10:34:11 2013 +0200
@@ -51,19 +51,19 @@
   Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
   
   uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
-  tag_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
-  tag_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [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)
+  tag_Plus ("tag\<^sub>A\<^sub>L\<^sub>T _ _" [100, 100] 100) and
+  tag_Plus ("tag\<^sub>A\<^sub>L\<^sub>T _ _ _" [100, 100, 100] 100) and
+  tag_Times ("tag\<^sub>S\<^sub>E\<^sub>Q _ _" [100, 100] 100) and
+  tag_Times ("tag\<^sub>S\<^sub>E\<^sub>Q _ _ _" [100, 100, 100] 100) and
+  tag_Star ("tag\<^sub>S\<^sub>T\<^sub>A\<^sub>R _" [100] 100) and
+  tag_Star ("tag\<^sub>S\<^sub>T\<^sub>A\<^sub>R _ _" [100, 100] 100)
 
 lemma meta_eq_app:
   shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
   by auto
 
 lemma conc_def':
-  "A \<cdot> B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
+  "A \<cdot> B = {s\<^sub>1 @ s\<^sub>2 | s\<^sub>1 s\<^sub>2. s\<^sub>1 \<in> A \<and> s\<^sub>2 \<in> B}"
 unfolding conc_def by simp
 
 lemma str_eq_def':
@@ -222,7 +222,7 @@
   union, namely 
   %
   \begin{equation}\label{disjointunion}
-  @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"}
+  @{term "UPLUS A\<^sub>1 A\<^sub>2 \<equiv> {(1, x) | x. x \<in> A\<^sub>1} \<union> {(2, y) | y. y \<in> A\<^sub>2}"}
   \end{equation}
 
   \noindent
@@ -356,7 +356,7 @@
 
   The notation in Isabelle/HOL for the quotient of a language @{text A} according to an 
   equivalence relation @{term REL} is @{term "A // REL"}. We will write 
-  @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined 
+  @{text "\<lbrakk>x\<rbrakk>\<^sub>\<approx>"} for the equivalence class defined 
   as \mbox{@{text "{y | y \<approx> x}"}}.
 
 
@@ -428,10 +428,10 @@
   \end{tabular}
   &
   \begin{tabular}{rcl}
-  @{thm (lhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
-       @{thm (rhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
-  @{thm (lhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
-       @{thm (rhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
+  @{thm (lhs) lang.simps(4)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]} & @{text "\<equiv>"} &
+       @{thm (rhs) lang.simps(4)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]}\\
+  @{thm (lhs) lang.simps(5)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]} & @{text "\<equiv>"} &
+       @{thm (rhs) lang.simps(5)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]}\\
   @{thm (lhs) lang.simps(6)[where r="r"]} & @{text "\<equiv>"} &
       @{thm (rhs) lang.simps(6)[where r="r"]}\\
   \end{tabular}
@@ -476,13 +476,13 @@
   equivalence classes. To illustrate this quotient construction, let us give a simple 
   example: consider the regular language containing just
   the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
-  into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and  @{text "X\<^isub>3"}
+  into three equivalence classes @{text "X\<^sub>1"}, @{text "X\<^sub>2"} and  @{text "X\<^sub>3"}
   as follows
   
   \begin{center}
-  @{text "X\<^isub>1 = {[]}"}\hspace{5mm}
-  @{text "X\<^isub>2 = {[c]}"}\hspace{5mm}
-  @{text "X\<^isub>3 = UNIV - {[], [c]}"}
+  @{text "X\<^sub>1 = {[]}"}\hspace{5mm}
+  @{text "X\<^sub>2 = {[c]}"}\hspace{5mm}
+  @{text "X\<^sub>3 = UNIV - {[], [c]}"}
   \end{center}
 
   One direction of the Myhill-Nerode theorem establishes 
@@ -502,7 +502,7 @@
   \end{equation}
 
   \noindent
-  In our running example, @{text "X\<^isub>2"} is the only 
+  In our running example, @{text "X\<^sub>2"} is the only 
   equivalence class in @{term "finals {[c]}"}.
   It is straightforward to show that in general @{thm lang_is_union_of_finals} and 
   @{thm finals_in_partitions} hold. 
@@ -527,36 +527,36 @@
   strings in the equivalence class @{text Y}, we obtain a subset of 
   @{text X}. Note that we do not define an automaton here, we merely relate two sets
   (with the help of a character). In our concrete example we have 
-  @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any 
-  other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
+  @{term "X\<^sub>1 \<Turnstile>c\<Rightarrow> X\<^sub>2"}, @{term "X\<^sub>1 \<Turnstile>d\<Rightarrow> X\<^sub>3"} with @{text d} being any 
+  other character than @{text c}, and @{term "X\<^sub>3 \<Turnstile>d\<Rightarrow> X\<^sub>3"} for any @{text d}.
   
   Next we construct an \emph{initial equational system} that
   contains an equation for each equivalence class. We first give
   an informal description of this construction. Suppose we have 
-  the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
+  the equivalence classes @{text "X\<^sub>1,\<dots>,X\<^sub>n"}, there must be one and only one that
   contains the empty string @{text "[]"} (since equivalence classes are disjoint).
-  Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
+  Let us assume @{text "[] \<in> X\<^sub>1"}. We build the following equational system
   
   \begin{center}
   \begin{tabular}{rcl}
-  @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\
-  @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\
+  @{text "X\<^sub>1"} & @{text "="} & @{text "(Y\<^sub>1\<^sub>1, CHAR c\<^sub>1\<^sub>1) + \<dots> + (Y\<^sub>1\<^sub>p, CHAR c\<^sub>1\<^sub>p) + \<lambda>(EMPTY)"} \\
+  @{text "X\<^sub>2"} & @{text "="} & @{text "(Y\<^sub>2\<^sub>1, CHAR c\<^sub>2\<^sub>1) + \<dots> + (Y\<^sub>2\<^sub>o, CHAR c\<^sub>2\<^sub>o)"} \\
   & $\vdots$ \\
-  @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\
+  @{text "X\<^sub>n"} & @{text "="} & @{text "(Y\<^sub>n\<^sub>1, CHAR c\<^sub>n\<^sub>1) + \<dots> + (Y\<^sub>n\<^sub>q, CHAR c\<^sub>n\<^sub>q)"}\\
   \end{tabular}
   \end{center}
 
   \noindent
-  where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
-  stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
-  X\<^isub>i"}. 
+  where the terms @{text "(Y\<^sub>i\<^sub>j, CHAR c\<^sub>i\<^sub>j)"}
+  stand for all transitions @{term "Y\<^sub>i\<^sub>j \<Turnstile>c\<^sub>i\<^sub>j\<Rightarrow>
+  X\<^sub>i"}. 
   %The intuition behind the equational system is that every 
-  %equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
-  %corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states 
-  %are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these 
-  %predecessor states to @{text X\<^isub>i}. 
+  %equation @{text "X\<^sub>i = rhs\<^sub>i"} in this system
+  %corresponds roughly to a state of an automaton whose name is @{text X\<^sub>i} and its predecessor states 
+  %are the @{text "Y\<^sub>i\<^sub>j"}; the @{text "c\<^sub>i\<^sub>j"} are the labels of the transitions from these 
+  %predecessor states to @{text X\<^sub>i}. 
   There can only be
-  finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side 
+  finitely many terms of the form @{text "(Y\<^sub>i\<^sub>j, CHAR c\<^sub>i\<^sub>j)"} in a right-hand side 
   since by assumption there are only finitely many
   equivalence classes and only finitely many characters.
   The term @{text "\<lambda>(EMPTY)"} in the first equation acts as a marker for the initial state, that
@@ -570,7 +570,7 @@
   be reached by adding a character to the end of @{text Y}. This is also the
   reason why we have to use our reverse version of Arden's Lemma.}
   %In our initial equation system there can only be
-  %finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side 
+  %finitely many terms of the form @{text "(Y\<^sub>i\<^sub>j, CHAR c\<^sub>i\<^sub>j)"} in a right-hand side 
   %since by assumption there are only finitely many
   %equivalence classes and only finitely many characters. 
   Overloading the function @{text \<calL>} for the two kinds of terms in the
@@ -583,17 +583,17 @@
   \end{center}
 
   \noindent
-  and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
+  and we can prove for @{text "X\<^sub>2\<^sub>.\<^sub>.\<^sub>n"} that the following equations
   %
   \begin{equation}\label{inv1}
-  @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
+  @{text "X\<^sub>i = \<calL>(Y\<^sub>i\<^sub>1, CHAR c\<^sub>i\<^sub>1) \<union> \<dots> \<union> \<calL>(Y\<^sub>i\<^sub>q, CHAR c\<^sub>i\<^sub>q)"}.
   \end{equation}
 
   \noindent
-  hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+  hold. Similarly for @{text "X\<^sub>1"} we can show the following equation
   %
   \begin{equation}\label{inv2}
-  @{text "X\<^isub>1 = \<calL>(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
+  @{text "X\<^sub>1 = \<calL>(Y\<^sub>1\<^sub>1, CHAR c\<^sub>1\<^sub>1) \<union> \<dots> \<union> \<calL>(Y\<^sub>1\<^sub>p, CHAR c\<^sub>1\<^sub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
   \end{equation}
 
   \noindent
@@ -650,8 +650,8 @@
   we define the \emph{append-operation} taking a term and a regular expression as argument
 
   \begin{center}
-  @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
-  @{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+  @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}\hspace{10mm}
+  @{thm Append_rexp.simps(1)[where r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}
   \end{center}
 
   \noindent
@@ -1002,8 +1002,8 @@
   With this we will be able to infer that the tagging-functions, seen as relations,
   give rise to finitely many equivalence classes of @{const UNIV}. Finally we 
   will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which
-  implies that @{term "UNIV // \<approx>(L r)"} must also be finite (a relation @{text "R\<^isub>1"} 
-  is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}).
+  implies that @{term "UNIV // \<approx>(L r)"} must also be finite (a relation @{text "R\<^sub>1"} 
+  is said to \emph{refine} @{text "R\<^sub>2"} provided @{text "R\<^sub>1 \<subseteq> R\<^sub>2"}).
   We formally define the notion of a \emph{tagging-relation} as follows.
 
   \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
@@ -1043,27 +1043,27 @@
   \end{proof}
 
   \begin{lemma}\label{fintwo} 
-  Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
-  @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
-  If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
-  then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
+  Given two equivalence relations @{text "R\<^sub>1"} and @{text "R\<^sub>2"}, whereby
+  @{text "R\<^sub>1"} refines @{text "R\<^sub>2"}.
+  If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^sub>1" and ?R2.0="R\<^sub>2"]}
+  then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^sub>1" and ?R2.0="R\<^sub>2"]}.
   \end{lemma}
 
   \begin{proof}
   We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
-  be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that 
-  @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"},
+  be @{text "X \<mapsto>"}~@{term "{R\<^sub>1 `` {x} | x. x \<in> X}"}. It is easy to see that 
+  @{term "finite (f ` (UNIV // R\<^sub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^sub>1)"},
   which is finite by assumption. What remains to be shown is that @{text f} is injective
-  on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence 
-  classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
+  on @{term "UNIV // R\<^sub>2"}. This is equivalent to showing that two equivalence 
+  classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^sub>2"} are equal, provided
   @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
-  @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
-  We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}. 
-  From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
-  and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
-  such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
-  are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
-  they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
+  @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^sub>2} related.
+  We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^sub>2 `` {x}"}}. 
+  From the latter fact we can infer that @{term "R\<^sub>1 ``{x} \<in> f X"}
+  and further @{term "R\<^sub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
+  such that @{term "R\<^sub>1 `` {x} = R\<^sub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
+  are @{text "R\<^sub>1"}-related. Since by assumption @{text "R\<^sub>1"} refines @{text "R\<^sub>2"},
+  they must also be @{text "R\<^sub>2"}-related, as we need to show.\qed
   \end{proof}
 
   \noindent
@@ -1084,28 +1084,28 @@
   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 product set---so finite. It remains to be shown
-  that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to 
+  that @{text "=tag\<^sub>A\<^sub>L\<^sub>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"}
+  @{term "tag\<^sub>A\<^sub>L\<^sub>T A B x = tag\<^sub>A\<^sub>L\<^sub>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"}
+  @{text "\<forall>z. tag\<^sub>A\<^sub>L\<^sub>T A B x = tag\<^sub>A\<^sub>L\<^sub>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
+  since both @{text "=tag\<^sub>A\<^sub>L\<^sub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
   \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse 
   in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. 
   The definition of the tagging-function will give us in each case the
   information to infer that @{text "y @ z \<in> A \<union> B"}.
   Finally 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
+  can discharge this case by setting @{text A} to @{term "L r\<^sub>1"} and @{text B} to @{term "L r\<^sub>2"}.\qed
   \end{proof}
 
 
@@ -1255,7 +1255,7 @@
   @{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 SEQ}-case
-  by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed 
+  by setting @{text A} to @{term "L r\<^sub>1"} and @{text B} to @{term "L r\<^sub>2"}.\qed 
   \end{proof}
   
   \noindent
@@ -1267,10 +1267,10 @@
   \begin{center}
   \scalebox{0.7}{
   \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, 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}$ };
+    \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^sub>m\<^sub>a\<^sub>x"}\hspace{4em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^sub>m\<^sub>a\<^sub>x"}\hspace{0.5em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}@{text "z\<^sub>a"}\hspace{2em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}@{text "z\<^sub>b"}\hspace{7em}$ };
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
@@ -1286,19 +1286,19 @@
 
     \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 - x'\<^sub>m\<^sub>a\<^sub>x) @ z\<^sub>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]{@{term "x'\<^sub>m\<^sub>a\<^sub>x \<in> A\<star>"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}};
+               node[midway, below=0.5em]{@{term "z\<^sub>b \<in> A\<star>"}};
 
     \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 - x'\<^sub>m\<^sub>a\<^sub>x) @ z \<in> A\<star>"}};
   \end{tikzpicture}}
   \end{center}
   %
@@ -1308,16 +1308,16 @@
   @{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'\<^sub>m\<^sub>a\<^sub>x"}. Now for the rest of the string @{text "(x - x'\<^sub>m\<^sub>a\<^sub>x) @ 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}
-  `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
-  @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
+  and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^sub>m\<^sub>a\<^sub>x"},
+  otherwise @{text "x'\<^sub>m\<^sub>a\<^sub>x"} is not the longest prefix. That means @{text a}
+  `overlaps' with @{text z}, splitting it into two components @{text "z\<^sub>a"} and
+   @{text "z\<^sub>b"}. For this we know that @{text "(x - x'\<^sub>m\<^sub>a\<^sub>x) @ z\<^sub>a \<in> A"} and
+  @{term "z\<^sub>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 - x'\<^sub>m\<^sub>a\<^sub>x) @ z\<^sub>a"}.
 
   In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
   the following tagging-function:
@@ -1344,21 +1344,21 @@
   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>})"}
+  @{term "\<approx>A `` {(x - x'\<^sub>m\<^sub>a\<^sub>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>})"}
+  @{term "\<approx>A `` {(x - x'\<^sub>m\<^sub>a\<^sub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
   \end{center}
   %
   \noindent 
   and we know that we have a @{term "y' \<in> A\<star>"} and @{text "y' < y"}
-  and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode
-  relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
-  Therefore @{term "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
+  and also know @{term "(x - x'\<^sub>m\<^sub>a\<^sub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode
+  relation we know @{term "(y - y') @ z\<^sub>a \<in> A"}. We also know that @{term "z\<^sub>b \<in> A\<star>"}.
+  Therefore @{term "y' @ ((y - y') @ z\<^sub>a) @ z\<^sub>b \<in> A\<star>"}, which means
   @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "L r"} and
   complete the proof.\qed
   \end{proof}
@@ -1393,12 +1393,12 @@
   can be easily proved using the Myhill-Nerode theorem since 
   %
   \begin{center}
-  @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
+  @{term "s\<^sub>1 \<approx>A s\<^sub>2"} if and only if @{term "s\<^sub>1 \<approx>(-A) s\<^sub>2"}
   \end{center}
   %
   \noindent
-  holds for any strings @{text "s\<^isub>1"} and @{text
-  "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
+  holds for any strings @{text "s\<^sub>1"} and @{text
+  "s\<^sub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
   partitions.  Proving the existence of such a regular expression via automata 
   using the standard method would 
   be quite involved. It includes the