diff -r 60bcf13adb77 -r e5e32faa2446 Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Jul 11 16:46:05 2013 +0100
+++ b/Journal/Paper.thy	Thu Sep 12 10:34:11 2013 +0200
@@ -96,7 +96,7 @@
   ONE ("ONE" 999) and
   ZERO ("ZERO" 999) and
   pderivs_lang ("pdersl") and
-  UNIV1 ("UNIV\<^isup>+") and
+  UNIV1 ("UNIV\<^sup>+") and
   Deriv_lang ("Dersl") and
   Derivss ("Derss") and
   deriv ("der") and
@@ -132,7 +132,7 @@
 unfolding str_eq_def by simp
 
 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 conc_Union_left: 
@@ -327,7 +327,7 @@
   union, namely 
   %
   \begin{equation}\label{disjointunion}
-  @{text "A\<^isub>1 \<uplus> A\<^isub>2 \<equiv> {(1, x) | x \<in> A\<^isub>1} \<union> {(2, y) | y \<in> A\<^isub>2}"}
+  @{text "A\<^sub>1 \<uplus> A\<^sub>2 \<equiv> {(1, x) | x \<in> A\<^sub>1} \<union> {(2, y) | y \<in> A\<^sub>2}"}
   \end{equation}
 
   \noindent
@@ -484,7 +484,7 @@
   establish the usual closure properties, including complementation, for
   regular languages. We use the Continuation Lemma, which is also a corollary 
   of the Myhill-Nerode Theorem, for establishing 
-  the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\medskip 
+  the non-regularity of the language @{text "a\<^sup>nb\<^sup>n"}.\medskip 
   
   \noindent 
   {\bf Contributions:} There is an extensive literature on regular languages.
@@ -541,8 +541,8 @@
   (ii)  & @{thm[mode=IfThen] pow_length}\\
   (iii) & @{thm conc_Union_left} \\ 
   (iv)  & If @{thm (prem 1) star_decom} and @{thm (prem 2) star_decom} then
-          there exists an @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{text "x = x\<^isub>p @ x\<^isub>s"} 
-          and \mbox{@{term "x\<^isub>p \<noteq> []"}} such that @{term "x\<^isub>p \<in> A"} and @{term "x\<^isub>s \<in> A\<star>"}.
+          there exists an @{text "x\<^sub>p"} and @{text "x\<^sub>s"} with @{text "x = x\<^sub>p @ x\<^sub>s"} 
+          and \mbox{@{term "x\<^sub>p \<noteq> []"}} such that @{term "x\<^sub>p \<in> A"} and @{term "x\<^sub>s \<in> A\<star>"}.
   \end{tabular}
   \end{proposition}
 
@@ -559,9 +559,9 @@
 
   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 as
+  will write @{text "\<lbrakk>x\<rbrakk>\<^sub>\<approx>"} for the equivalence class defined as
   \mbox{@{text "{y | y \<approx> x}"}}, and have @{text "x \<approx> y"} if and only if @{text
-  "\<lbrakk>x\<rbrakk>\<^isub>\<approx> = \<lbrakk>y\<rbrakk>\<^isub>\<approx>"}.
+  "\<lbrakk>x\<rbrakk>\<^sub>\<approx> = \<lbrakk>y\<rbrakk>\<^sub>\<approx>"}.
 
 
   Central to our proof will be the solution of equational systems
@@ -604,10 +604,10 @@
   @{thm (lhs) lang.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(1)}\\
   @{thm (lhs) lang.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(2)}\\
   @{thm (lhs) lang.simps(3)[where a="c"]} & @{text "\<equiv>"} & @{thm (rhs) lang.simps(3)[where a="c"]}\\
-  @{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}
@@ -665,15 +665,15 @@
   example: consider the regular language built up over the alphabet @{term "{a, b}"} and 
   containing just the string two strings @{text "[a]"} and @{text "[a, b]"}. The 
   relation @{term "\<approx>({[a], [a, b]})"} partitions @{text UNIV}
-  into four equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"}, @{text "X\<^isub>3"} and @{text "X\<^isub>4"}
+  into four equivalence classes @{text "X\<^sub>1"}, @{text "X\<^sub>2"}, @{text "X\<^sub>3"} and @{text "X\<^sub>4"}
   as follows
   
   \begin{center}
   \begin{tabular}{l}
-  @{text "X\<^isub>1 = {[]}"}\\
-  @{text "X\<^isub>2 = {[a]}"}\\
-  @{text "X\<^isub>3 = {[a, b]}"}\\
-  @{text "X\<^isub>4 = UNIV - {[], [a], [a, b]}"}
+  @{text "X\<^sub>1 = {[]}"}\\
+  @{text "X\<^sub>2 = {[a]}"}\\
+  @{text "X\<^sub>3 = {[a, b]}"}\\
+  @{text "X\<^sub>4 = UNIV - {[], [a], [a, b]}"}
   \end{tabular}
   \end{center}
 
@@ -694,7 +694,7 @@
   \end{equation}
 
   \noindent
-  In our running example, @{text "X\<^isub>2"} and @{text "X\<^isub>3"} are the only 
+  In our running example, @{text "X\<^sub>2"} and @{text "X\<^sub>3"} are the only 
   equivalence classes in @{term "finals {[a], [a, b]}"}.
   It is straightforward to show that in general 
   %
@@ -732,41 +732,41 @@
 
   \begin{center} 
   \begin{tabular}{l}
-  @{term "X\<^isub>1 \<Turnstile>a\<Rightarrow> X\<^isub>2"},\; @{term "X\<^isub>1 \<Turnstile>b\<Rightarrow> X\<^isub>4"};\\ 
-  @{term "X\<^isub>2 \<Turnstile>b\<Rightarrow> X\<^isub>3"},\; @{term "X\<^isub>2 \<Turnstile>a\<Rightarrow> X\<^isub>4"};\\
-  @{term "X\<^isub>3 \<Turnstile>a\<Rightarrow> X\<^isub>4"},\; @{term "X\<^isub>3 \<Turnstile>b\<Rightarrow> X\<^isub>4"} and\\ 
-  @{term "X\<^isub>4 \<Turnstile>a\<Rightarrow> X\<^isub>4"},\; @{term "X\<^isub>4 \<Turnstile>b\<Rightarrow> X\<^isub>4"}.
+  @{term "X\<^sub>1 \<Turnstile>a\<Rightarrow> X\<^sub>2"},\; @{term "X\<^sub>1 \<Turnstile>b\<Rightarrow> X\<^sub>4"};\\ 
+  @{term "X\<^sub>2 \<Turnstile>b\<Rightarrow> X\<^sub>3"},\; @{term "X\<^sub>2 \<Turnstile>a\<Rightarrow> X\<^sub>4"};\\
+  @{term "X\<^sub>3 \<Turnstile>a\<Rightarrow> X\<^sub>4"},\; @{term "X\<^sub>3 \<Turnstile>b\<Rightarrow> X\<^sub>4"} and\\ 
+  @{term "X\<^sub>4 \<Turnstile>a\<Rightarrow> X\<^sub>4"},\; @{term "X\<^sub>4 \<Turnstile>b\<Rightarrow> X\<^sub>4"}.
   \end{tabular}
   \end{center}
   
   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 initial equational system
+  Let us assume @{text "[] \<in> X\<^sub>1"}. We build the following initial equational system
   
   \begin{center}
   \begin{tabular}{rcl}
-  @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, ATOM c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, ATOM c\<^isub>1\<^isub>p) + \<lambda>(ONE)"} \\
-  @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, ATOM c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, ATOM c\<^isub>2\<^isub>o)"} \\
+  @{text "X\<^sub>1"} & @{text "="} & @{text "(Y\<^sub>1\<^sub>1, ATOM c\<^sub>1\<^sub>1) + \<dots> + (Y\<^sub>1\<^sub>p, ATOM c\<^sub>1\<^sub>p) + \<lambda>(ONE)"} \\
+  @{text "X\<^sub>2"} & @{text "="} & @{text "(Y\<^sub>2\<^sub>1, ATOM c\<^sub>2\<^sub>1) + \<dots> + (Y\<^sub>2\<^sub>o, ATOM c\<^sub>2\<^sub>o)"} \\
   & $\vdots$ \\
-  @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, ATOM c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, ATOM c\<^isub>n\<^isub>q)"}\\
+  @{text "X\<^sub>n"} & @{text "="} & @{text "(Y\<^sub>n\<^sub>1, ATOM c\<^sub>n\<^sub>1) + \<dots> + (Y\<^sub>n\<^sub>q, ATOM c\<^sub>n\<^sub>q)"}\\
   \end{tabular}
   \end{center}
 
   \noindent
-  where the terms @{text "(Y\<^isub>i\<^isub>j, ATOM c\<^isub>i\<^isub>j)"} are pairs consisting of an equivalence class and
+  where the terms @{text "(Y\<^sub>i\<^sub>j, ATOM c\<^sub>i\<^sub>j)"} are pairs consisting of an equivalence class and
   a regular expression. In the initial equational system, they
-  stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
-  X\<^isub>i"}. 
+  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, ATOM c\<^isub>i\<^isub>j)"} in a right-hand side 
+  finitely many terms of the form @{text "(Y\<^sub>i\<^sub>j, ATOM 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>(ONE)"} in the first equation acts as a marker for the initial state, that
@@ -783,11 +783,11 @@
   %
   \begin{equation}\label{exmpcs}
   \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{term "X\<^isub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
-  @{term "X\<^isub>2"} & @{text "="} & @{text "(X\<^isub>1, ATOM a)"}\\
-  @{term "X\<^isub>3"} & @{text "="} & @{text "(X\<^isub>2, ATOM b)"}\\
-  @{term "X\<^isub>4"} & @{text "="} & @{text "(X\<^isub>1, ATOM b) + (X\<^isub>2, ATOM a) + (X\<^isub>3, ATOM a)"}\\
-          & & \mbox{}\hspace{0mm}@{text "+ (X\<^isub>3, ATOM b) + (X\<^isub>4, ATOM a) + (X\<^isub>4, ATOM b)"}\\
+  @{term "X\<^sub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
+  @{term "X\<^sub>2"} & @{text "="} & @{text "(X\<^sub>1, ATOM a)"}\\
+  @{term "X\<^sub>3"} & @{text "="} & @{text "(X\<^sub>2, ATOM b)"}\\
+  @{term "X\<^sub>4"} & @{text "="} & @{text "(X\<^sub>1, ATOM b) + (X\<^sub>2, ATOM a) + (X\<^sub>3, ATOM a)"}\\
+          & & \mbox{}\hspace{0mm}@{text "+ (X\<^sub>3, ATOM b) + (X\<^sub>4, ATOM a) + (X\<^sub>4, ATOM b)"}\\
   \end{tabular}}
   \end{equation}
 
@@ -802,17 +802,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, ATOM c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, ATOM c\<^isub>i\<^isub>q)"}.
+  @{text "X\<^sub>i = \<calL>(Y\<^sub>i\<^sub>1, ATOM c\<^sub>i\<^sub>1) \<union> \<dots> \<union> \<calL>(Y\<^sub>i\<^sub>q, ATOM 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, ATOM c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, ATOM c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(ONE))"}.
+  @{text "X\<^sub>1 = \<calL>(Y\<^sub>1\<^sub>1, ATOM c\<^sub>1\<^sub>1) \<union> \<dots> \<union> \<calL>(Y\<^sub>1\<^sub>p, ATOM c\<^sub>1\<^sub>p) \<union> \<calL>(\<lambda>(ONE))"}.
   \end{equation}
 
   \noindent
@@ -863,12 +863,12 @@
 
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{thm (lhs) Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+  @{thm (lhs) Append_rexp.simps(2)[where X="Y" and r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}
   & @{text "\<equiv>"} & 
-  @{thm (rhs) Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\\
-  @{thm (lhs) Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+  @{thm (rhs) Append_rexp.simps(2)[where X="Y" and r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}\\
+  @{thm (lhs) Append_rexp.simps(1)[where r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}
   & @{text "\<equiv>"} & 
-  @{thm (rhs) Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+  @{thm (rhs) Append_rexp.simps(1)[where r="r\<^sub>1" and rexp="r\<^sub>2", THEN eq_reflection]}
   \end{tabular}
   \end{center}
 
@@ -891,22 +891,22 @@
   then we calculate the combined regular expressions for all @{text r} coming 
   from the deleted @{text "(X, r)"}, and take the @{const Star} of it;
   finally we append this regular expression to @{text rhs'}. If we apply this
-  operation to the right-hand side of @{text "X\<^isub>4"} in \eqref{exmpcs}, we obtain
+  operation to the right-hand side of @{text "X\<^sub>4"} in \eqref{exmpcs}, we obtain
   the equation:
 
   \begin{center}
   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{term "X\<^isub>4"} & @{text "="} & 
-    @{text "(X\<^isub>1, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
-  & & @{text "(X\<^isub>2, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
-  & & @{text "(X\<^isub>3, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
-  & & @{text "(X\<^isub>3, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b}))"}
+  @{term "X\<^sub>4"} & @{text "="} & 
+    @{text "(X\<^sub>1, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+  & & @{text "(X\<^sub>2, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+  & & @{text "(X\<^sub>3, TIMES (ATOM a) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+  & & @{text "(X\<^sub>3, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b}))"}
   \end{tabular}
   \end{center}
 
 
   \noindent
-  That means we eliminated the recursive occurrence of @{text "X\<^isub>4"} on the
+  That means we eliminated the recursive occurrence of @{text "X\<^sub>4"} on the
   right-hand side. 
 
   It can be easily seen that the @{text "Arden"}-operation mimics Arden's
@@ -952,11 +952,11 @@
   the substitution operation we will arrange it so that @{text "xrhs"} does not contain
   any occurrence of @{text X}. For example substituting the first equation in
   \eqref{exmpcs} into the right-hand side of the second, thus eliminating the equivalence 
-  class @{text "X\<^isub>1"}, gives us the equation
+  class @{text "X\<^sub>1"}, gives us the equation
   %
   \begin{equation}\label{exmpresult}
   \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{term "X\<^isub>2"} & @{text "="} & @{text "\<lambda>(TIMES ONE (ATOM a))"}
+  @{term "X\<^sub>2"} & @{text "="} & @{text "\<lambda>(TIMES ONE (ATOM a))"}
   \end{tabular}}
   \end{equation}
 
@@ -1223,8 +1223,8 @@
 
   \begin{center}
   \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{text "X\<^isub>2"} & @{text "="} & @{text "TIMES ONE (ATOM a)"}\\
-  @{text "X\<^isub>3"} & @{text "="} & @{text "TIMES (TIMES ONE (ATOM a)) (ATOM b)"}
+  @{text "X\<^sub>2"} & @{text "="} & @{text "TIMES ONE (ATOM a)"}\\
+  @{text "X\<^sub>3"} & @{text "="} & @{text "TIMES (TIMES ONE (ATOM a)) (ATOM b)"}
   \end{tabular}
   \end{center}
 
@@ -1235,7 +1235,7 @@
   calculating a regular expression for the complement of a regular language:
   if we combine all regular
   expressions corresponding to equivalence classes not in @{term "finals A"} 
-  (in the running example @{text "X\<^isub>1"} and @{text "X\<^isub>4"}),
+  (in the running example @{text "X\<^sub>1"} and @{text "X\<^sub>4"}),
   then we obtain a regular expression for the complement language @{term "- A"}.
   This is similar to the usual construction of a `complement automaton'.
 
@@ -1318,8 +1318,8 @@
   R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}. 
 
   \begin{definition}
-  A relation @{text "R\<^isub>1"} \emph{refines} @{text "R\<^isub>2"}
-  provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. 
+  A relation @{text "R\<^sub>1"} \emph{refines} @{text "R\<^sub>2"}
+  provided @{text "R\<^sub>1 \<subseteq> R\<^sub>2"}. 
   \end{definition}
 
   \noindent
@@ -1373,9 +1373,9 @@
   @{text "\<equiv>"} &
   @{thm (rhs) tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]} \\
   @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}\;@{text "x"} & @{text "\<equiv>"} &
-  @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}\\
+  @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^sub>p \<in> A \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x})"}\\
   @{thm (lhs) tag_Star_def[where ?A="A", THEN meta_eq_app]} & @{text "\<equiv>"} &
-  @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
+  @{text "{\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^sub>p < x \<and> x\<^sub>p \<in> A\<^sup>\<star> \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x}"}
   \end{tabular}
   \caption{Three tagging functions used the cases for @{term "PLUS"}, @{term "TIMES"} and @{term "STAR"} 
   regular expressions. The sets @{text A} and @{text B} are arbitrary languages instantiated
@@ -1402,27 +1402,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 must be 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
@@ -1450,7 +1450,7 @@
   "(\<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"}, 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"}.\qed
+  "lang r\<^sub>1"} and @{text B} to @{term "lang r\<^sub>2"}.\qed
   \end{proof}
 
   \noindent
@@ -1475,9 +1475,9 @@
   \end{equation}
 
   \noindent
-  If we know that @{text "(x\<^isub>p, x\<^isub>s) \<in> Partitions x"}, we will
-  refer to @{text "x\<^isub>p"} as the \emph{prefix} of the string @{text x},
-  and respectively to @{text "x\<^isub>s"} as the \emph{suffix}.
+  If we know that @{text "(x\<^sub>p, x\<^sub>s) \<in> Partitions x"}, we will
+  refer to @{text "x\<^sub>p"} as the \emph{prefix} of the string @{text x},
+  and respectively to @{text "x\<^sub>s"} as the \emph{suffix}.
 
 *}
 
@@ -1490,8 +1490,8 @@
   \scalebox{1}{
   \begin{tikzpicture}[scale=0.8,fill=gray!20]
     \node[draw,minimum height=3.8ex, fill] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of x, fill] (za) { $\hspace{0.6em}@{text "z\<^isub>p"}\hspace{0.6em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zza) { $\hspace{2.6em}@{text "z\<^isub>s"}\hspace{2.6em}$  };
+    \node[draw,minimum height=3.8ex, right=-0.03em of x, fill] (za) { $\hspace{0.6em}@{text "z\<^sub>p"}\hspace{0.6em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zza) { $\hspace{2.6em}@{text "z\<^sub>s"}\hspace{2.6em}$  };
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            (x.north west) -- ($(za.north west)+(0em,0em)$)
@@ -1507,17 +1507,17 @@
 
     \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"}};
+               node[midway, below=0.5em]{@{text "x @ z\<^sub>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"}};
+               node[midway, below=0.5em]{@{text "z\<^sub>s \<in> B"}};
   \end{tikzpicture}}
   \\[2mm]
   \scalebox{1}{
   \begin{tikzpicture}[scale=0.8,fill=gray!20]
-    \node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{3em}@{text "x\<^isub>p"}\hspace{3em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.2em}@{text "x\<^isub>s"}\hspace{0.2em}$ };
+    \node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{3em}@{text "x\<^sub>p"}\hspace{3em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.2em}@{text "x\<^sub>s"}\hspace{0.2em}$ };
     \node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
@@ -1534,11 +1534,11 @@
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{term "x\<^isub>s @ z \<in> B"}};
+               node[midway, below=0.5em]{@{term "x\<^sub>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\<^isub>p \<in> A"}};
+               node[midway, below=0.5em]{@{term "x\<^sub>p \<in> A"}};
   \end{tikzpicture}}
   \end{tabular}
   \end{center}
@@ -1550,22 +1550,22 @@
   (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 "("}@{text "*"}@{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 one possible partition
-  of the string @{text x}. We have to know that both @{text "x\<^isub>p"} and the
-  corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related' 
-  to @{text "y\<^isub>s"} @{text "("}@{text "**"}@{text ")"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.
+  we can infer from @{term "x @ z\<^sub>p \<in> A"} that @{term "y @ z\<^sub>p \<in> A"} holds for all @{text "z\<^sub>p"}.
+  In the second case we only know that @{text "x\<^sub>p"} and @{text "x\<^sub>s"} is one possible partition
+  of the string @{text x}. We have to know that both @{text "x\<^sub>p"} and the
+  corresponding partition @{text "y\<^sub>p"} are in @{text "A"}, and that @{text "x\<^sub>s"} is `@{text B}-related' 
+  to @{text "y\<^sub>s"} @{text "("}@{text "**"}@{text ")"}. From the latter fact we can infer that @{text "y\<^sub>s @ z \<in> B"}.
   This will solve the second case.
   Taking the two requirements, @{text "("}@{text "*"}@{text ")"} and @{text "(**)"}, together we define the
   tagging-function in the @{const Times}-case as (see Fig.~\ref{tagfig}):
 
   \begin{center}
   @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}\;@{text "x"}~@{text "\<equiv>"}~
-  @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}
+  @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^sub>p \<in> A \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x})"}
   \end{center}
 
   \noindent
-  Note that we have to make the assumption for all suffixes @{text "x\<^isub>s"}, since we do 
+  Note that we have to make the assumption for all suffixes @{text "x\<^sub>s"}, since we do 
   not know anything about how the string @{term x} is partitioned.
   With this definition in place, let us prove the @{const "Times"}-case.
 
@@ -1583,36 +1583,36 @@
   \noindent
   and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot>
   B"}. As shown in the pictures above, there are two cases to be
-  considered. First, there exists a @{text "z\<^isub>p"} and @{text
-  "z\<^isub>s"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s
+  considered. First, there exists a @{text "z\<^sub>p"} and @{text
+  "z\<^sub>s"} such that @{term "x @ z\<^sub>p \<in> A"} and @{text "z\<^sub>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"}. Hence by the Myhill-Nerode
-  Relation @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"},
+  Relation @{term "y @ z\<^sub>p \<in> A"} holds. Using @{text "z\<^sub>s \<in> B"},
   we can conclude in this case with @{term "y @ z \<in> A \<cdot> B"} (recall @{text
-  "z\<^isub>p @ z\<^isub>s = z"}).
+  "z\<^sub>p @ z\<^sub>s = z"}).
 
-  Second there exists a partition @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with 
-  @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have
+  Second there exists a partition @{text "x\<^sub>p"} and @{text "x\<^sub>s"} with 
+  @{text "x\<^sub>p \<in> A"} and @{text "x\<^sub>s @ z \<in> B"}. We therefore have
   
   \begin{center}
-  @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
+  @{text "\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^sub>p \<in> A \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x}"}
   \end{center}
   
   \noindent
   and by the assumption about @{term "tag_Times A B"} also 
   
   \begin{center}
-  @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | y\<^isub>p \<in> A \<and> (y\<^isub>p, y\<^isub>s) \<in> Partitions y}"}
+  @{text "\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>y\<^sub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | y\<^sub>p \<in> A \<and> (y\<^sub>p, y\<^sub>s) \<in> Partitions y}"}
   \end{center}
   
   \noindent
-  This means there must be a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"}
-  such that @{term "y\<^isub>p \<in> A"} 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 \mbox{@{text "x\<^isub>s @ z \<in> B"}}, we
-  obtain @{term "y\<^isub>p \<in> A"} and @{text "y\<^isub>s @ z \<in> B"}, as needed in
+  This means there must be a partition @{text "y\<^sub>p"} and @{text "y\<^sub>s"}
+  such that @{term "y\<^sub>p \<in> A"} and @{term "\<approx>B `` {x\<^sub>s} = \<approx>B ``
+  {y\<^sub>s}"}. Unfolding the Myhill-Nerode Relation and together with the
+  facts that @{text "x\<^sub>p \<in> A"} and \mbox{@{text "x\<^sub>s @ z \<in> B"}}, we
+  obtain @{term "y\<^sub>p \<in> A"} and @{text "y\<^sub>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"}.\qed
+  A} to @{term "lang r\<^sub>1"} and @{text B} to @{term "lang r\<^sub>2"}.\qed
   \end{proof}
 
   \noindent
@@ -1635,8 +1635,8 @@
   \begin{tikzpicture}[scale=0.8,fill=gray!20]
     \node[draw,minimum height=3.8ex, fill] (xa) { $\hspace{4em}@{text "x\<^bsub>pmax\<^esub>"}\hspace{4em}$ };
     \node[draw,minimum height=3.8ex, right=-0.03em of xa, fill] (xxa) { $\hspace{0.5em}@{text "x\<^bsub>s\<^esub>"}\hspace{0.5em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
-    \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of xxa, fill] (za) { $\hspace{2em}@{text "z\<^sub>a"}\hspace{2em}$ };
+    \node[draw,minimum height=3.8ex, right=-0.03em of za, fill] (zb) { $\hspace{7em}@{text "z\<^sub>b"}\hspace{7em}$ };
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
@@ -1652,46 +1652,46 @@
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{term "x\<^isub>s @ z\<^isub>a \<in> A"}};
+               node[midway, below=0.5em]{@{term "x\<^sub>s @ 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]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"}};
+               node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<^sup>\<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\<^isub>s @ z \<in> A\<star>"}};
+               node[midway, below=0.5em]{@{term "x\<^sub>s @ z \<in> A\<star>"}};
   \end{tikzpicture}}
   \end{center}
   %
   \noindent
-  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 
+  We can find a strict prefix @{text "x\<^sub>p"} of @{text x} such that @{term "x\<^sub>p \<in> A\<star>"},
+  @{text "x\<^sub>p < x"} and the rest @{term "x\<^sub>s @ z \<in> A\<star>"}. For example the empty string 
   @{text "[]"} would do (recall @{term "x \<noteq> []"}).
   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\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we
+  @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^sub>s @ z"} we
   know it is in @{term "A\<star>"} and cannot be the empty string. By Property~\ref{langprops}@{text "(iv)"}, 
   we can separate
   this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<noteq> []"}, @{text "a \<in> A"}
-  and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"},
+  and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^sub>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\<^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>"}
+  `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\<^sub>s @ 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\<^isub>s @ z\<^isub>a"}.
+  `border' of @{text x} and @{text z}. This string is @{text "x\<^sub>s @ 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:
   %
   \begin{center}
   @{thm (lhs) tag_Star_def[where ?A="A", THEN meta_eq_app]}~@{text "\<equiv>"}~
-  @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"}
+  @{text "{\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^sub>p < x \<and> x\<^sub>p \<in> A\<^sup>\<star> \<and> (x\<^sub>p, x\<^sub>s) \<in> Partitions x}"}
   \end{center}
 
   \begin{proof}[@{const Star}-Case]
@@ -1706,26 +1706,26 @@
   can infer @{text y} is the empty string and
   then clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
   string, we can divide the string @{text "x @ z"} as shown in the picture 
-  above. By the tagging-function and the facts @{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"} and @{text "x\<^bsub>pmax\<^esub> < x"}, 
+  above. By the tagging-function and the facts @{text "x\<^bsub>pmax\<^esub> \<in> A\<^sup>\<star>"} and @{text "x\<^bsub>pmax\<^esub> < x"}, 
   we have
 
   \begin{center}
-  @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^bsub>pmax\<^esub> < x \<and> x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star> \<and> (x\<^bsub>pmax\<^esub>, x\<^isub>s) \<in> Partitions x}"}
+  @{text "\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^bsub>pmax\<^esub> < x \<and> x\<^bsub>pmax\<^esub> \<in> A\<^sup>\<star> \<and> (x\<^bsub>pmax\<^esub>, x\<^sub>s) \<in> Partitions x}"}
   \end{center}
   
   \noindent
   which by assumption is equal to
   
   \begin{center}
-  @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | y\<^bsub>p\<^esub> < y \<and> y\<^bsub>p\<^esub> \<in> A\<^isup>\<star> \<and> (y\<^bsub>p\<^esub>, y\<^isub>s) \<in> Partitions y}"}
+  @{text "\<lbrakk>x\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>y\<^sub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | y\<^bsub>p\<^esub> < y \<and> y\<^bsub>p\<^esub> \<in> A\<^sup>\<star> \<and> (y\<^bsub>p\<^esub>, y\<^sub>s) \<in> Partitions y}"}
   \end{center}
   
   \noindent 
-  From this we know there exist a partition @{text "y\<^isub>p"} and @{text
-  "y\<^isub>s"} with @{term "y\<^isub>p \<in> A\<star>"} and also @{term "x\<^isub>s \<approx>A
-  y\<^isub>s"}. Unfolding the Myhill-Nerode Relation we know @{term
-  "y\<^isub>s @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
-  Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \<in>
+  From this we know there exist a partition @{text "y\<^sub>p"} and @{text
+  "y\<^sub>s"} with @{term "y\<^sub>p \<in> A\<star>"} and also @{term "x\<^sub>s \<approx>A
+  y\<^sub>s"}. Unfolding the Myhill-Nerode Relation we know @{term
+  "y\<^sub>s @ z\<^sub>a \<in> A"}. We also know that @{term "z\<^sub>b \<in> A\<star>"}.
+  Therefore @{term "y\<^sub>p @ (y\<^sub>s @ z\<^sub>a) @ z\<^sub>b \<in>
   A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. The last step is to set
   @{text "A"} to @{term "lang r"} and thus complete the proof.\qed
   \end{proof}
@@ -1775,7 +1775,7 @@
   component is accepting and at least one state in the set is also accepting.
 
   The idea behind the @{text "STAR"}-case is similar to the @{text "TIMES"}-case.
-  We assume some automaton has consumed some strictly smaller part of the input in @{text "A\<^isup>\<star>"};
+  We assume some automaton has consumed some strictly smaller part of the input in @{text "A\<^sup>\<star>"};
   we need to check that from the state we ended up in a terminal state in the 
   automaton @{text "\<lbrakk>_\<rbrakk>\<^bsub>\<approx>A\<^esub>"} can be reached. Since we do not know from which state this will 
   succeed, we need to run the automaton from all possible states we could have 
@@ -1840,8 +1840,8 @@
   @{thm (lhs) Deriv_star}  & $=$ & @{thm (rhs) Deriv_star}\\
   @{thm (lhs) Derivs_simps(1)} & $=$ & @{thm (rhs) Derivs_simps(1)}\\
   @{thm (lhs) Derivs_simps(2)} & $=$ & @{thm (rhs) Derivs_simps(2)}\\
-  %@{thm (lhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}  & $=$ 
-  %   & @{thm (rhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
+  %@{thm (lhs) Derivs_simps(3)[where ?s1.0="s\<^sub>1" and ?s2.0="s\<^sub>2"]}  & $=$ 
+  %   & @{thm (rhs) Derivs_simps(3)[where ?s1.0="s\<^sub>1" and ?s2.0="s\<^sub>2"]}\\
   \end{tabular}}
   \end{equation}
 
@@ -1863,13 +1863,13 @@
   @{thm (lhs) deriv.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(1)}\\
   @{thm (lhs) deriv.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(2)}\\
   @{thm (lhs) deriv.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(3)[where c'="d"]}\\
-  @{thm (lhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
-     & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm (lhs) deriv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
-     & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
-       @{term "Plus (Times (deriv c r\<^isub>1) r\<^isub>2) (deriv c r\<^isub>2)"}\\
-     &             & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%  
-                    @{term "Times (deriv c r\<^isub>1) r\<^isub>2"}\\ 
+  @{thm (lhs) deriv.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}  
+     & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+  @{thm (lhs) deriv.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}  
+     & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^sub>1"}~@{text "then"}~%
+       @{term "Plus (Times (deriv c r\<^sub>1) r\<^sub>2) (deriv c r\<^sub>2)"}\\
+     &             & \phantom{@{text "if"}~@{term "nullable r\<^sub>1"}~}@{text "else"}~%  
+                    @{term "Times (deriv c r\<^sub>1) r\<^sub>2"}\\ 
   @{thm (lhs) deriv.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(6)}\smallskip\\
   @{thm (lhs) derivs.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(1)}\\
   @{thm (lhs) derivs.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(2)}
@@ -1887,10 +1887,10 @@
   @{thm (lhs) nullable.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(1)}\\
   @{thm (lhs) nullable.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(2)}\\
   @{thm (lhs) nullable.simps(3)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(3)}\\
-  @{thm (lhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
-     & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm (lhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
-     & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) nullable.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}  
+     & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+  @{thm (lhs) nullable.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}  
+     & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
   @{thm (lhs) nullable.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) nullable.simps(6)}
   \end{longtable}
   \end{center}
@@ -1935,8 +1935,8 @@
   ensuring that there are only finitely many equivalence
   classes. Unfortunately, this is not true in general. Sakarovitch gives an
   example where a regular expression has infinitely many derivatives
-  w.r.t.~the language @{text "(ab)\<^isup>\<star> \<union> (ab)\<^isup>\<star>a"}, which is formally 
-  written in our notation as \mbox{@{text "{[a,b]}\<^isup>\<star> \<union> ({[a,b]}\<^isup>\<star> \<cdot> {[a]})"}}
+  w.r.t.~the language @{text "(ab)\<^sup>\<star> \<union> (ab)\<^sup>\<star>a"}, which is formally 
+  written in our notation as \mbox{@{text "{[a,b]}\<^sup>\<star> \<union> ({[a,b]}\<^sup>\<star> \<cdot> {[a]})"}}
   (see \cite[Page~141]{Sakarovitch09}).
 
 
@@ -1947,8 +1947,8 @@
   %
   \begin{equation}\label{ACI}
   \mbox{\begin{tabular}{cl}
-  (@{text A}) & @{term "Plus (Plus r\<^isub>1 r\<^isub>2) r\<^isub>3"} $\equiv$ @{term "Plus r\<^isub>1 (Plus r\<^isub>2 r\<^isub>3)"}\\
-  (@{text C}) & @{term "Plus r\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
+  (@{text A}) & @{term "Plus (Plus r\<^sub>1 r\<^sub>2) r\<^sub>3"} $\equiv$ @{term "Plus r\<^sub>1 (Plus r\<^sub>2 r\<^sub>3)"}\\
+  (@{text C}) & @{term "Plus r\<^sub>1 r\<^sub>2"} $\equiv$ @{term "Plus r\<^sub>2 r\<^sub>1"}\\
   (@{text I}) & @{term "Plus r r"} $\equiv$ @{term "r"}\\
   \end{tabular}}
   \end{equation}
@@ -1969,13 +1969,13 @@
   @{thm (lhs) pderiv.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(1)}\\
   @{thm (lhs) pderiv.simps(2)}  & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(2)}\\
   @{thm (lhs) pderiv.simps(3)[where c'="d"]}  & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(3)[where c'="d"]}\\
-  @{thm (lhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
-     & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm (lhs) pderiv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}  
-     & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
-       @{term "(Timess (pderiv c r\<^isub>1) r\<^isub>2) \<union> (pderiv c r\<^isub>2)"}\\
-     & & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%  
-                    @{term "Timess (pderiv c r\<^isub>1) r\<^isub>2"}\\ 
+  @{thm (lhs) pderiv.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}  
+     & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+  @{thm (lhs) pderiv.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}  
+     & @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^sub>1"}~@{text "then"}~%
+       @{term "(Timess (pderiv c r\<^sub>1) r\<^sub>2) \<union> (pderiv c r\<^sub>2)"}\\
+     & & \phantom{@{text "if"}~@{term "nullable r\<^sub>1"}~}@{text "else"}~%  
+                    @{term "Timess (pderiv c r\<^sub>1) r\<^sub>2"}\\ 
   @{thm (lhs) pderiv.simps(6)}  & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(6)}\smallskip\\
   @{thm (lhs) pderivs.simps(1)}  & @{text "\<equiv>"} & @{thm (rhs) pderivs.simps(1)}\\
   @{thm (lhs) pderivs.simps(2)}  & @{text "\<equiv>"} & @{text "\<Union> (pders s) ` (pder c r)"}
@@ -2093,8 +2093,8 @@
   @{thm pderivs_lang_Zero}\\
   @{thm pderivs_lang_One}\\
   @{thm pderivs_lang_Atom}\\
-  @{thm pderivs_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm pderivs_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm pderivs_lang_Plus[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+  @{thm pderivs_lang_Times[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
   @{thm pderivs_lang_Star}\\
   \end{tabular}}
   \end{equation}
@@ -2168,12 +2168,12 @@
   proved using both parts of 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"}
+  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. So if one is finite, the other is too, and
   vice versa. As noted earlier, our algorithm for solving equational systems
   actually calculates a regular expression for the complement language. 
@@ -2213,10 +2213,10 @@
   %@{thm (lhs) Rev.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(1)}\\
   %@{thm (lhs) Rev.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(2)}\\
   %@{thm (lhs) Rev.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(3)}\\
-  %@{thm (lhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} & 
-  %    @{thm (rhs) Rev.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  %@{thm (lhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} & 
-  %    @{thm (rhs) Rev.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  %@{thm (lhs) Rev.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]} & @{text "\<equiv>"} & 
+  %    @{thm (rhs) Rev.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+  %@{thm (lhs) Rev.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]} & @{text "\<equiv>"} & 
+  %    @{thm (rhs) Rev.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
   %@{thm (lhs) Rev.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) Rev.simps(6)}\\
   %\end{tabular}
   %\end{center}
@@ -2344,10 +2344,10 @@
   @{thm (lhs) UP.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(1)}\\  
   @{thm (lhs) UP.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(2)}\\ 
   @{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(3)}\\ 
-  @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & 
-     @{text "\<equiv>"} & @{thm (rhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
-  @{thm (lhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & 
-     @{text "\<equiv>"} & @{thm (rhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+  @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]} & 
+     @{text "\<equiv>"} & @{thm (rhs) UP.simps(4)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
+  @{thm (lhs) UP.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]} & 
+     @{text "\<equiv>"} & @{thm (rhs) UP.simps(5)[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
   @{thm (lhs) UP.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(6)}
   \end{tabular}
   \end{center}
@@ -2437,9 +2437,9 @@
   they need to be related by the Myhill-Nerode Relation.
 
   Using this lemma, it is straightforward to establish that the language 
-  \mbox{@{text "A \<equiv> \<Union>\<^isub>n a\<^sup>n @ b\<^sup>n"}} is not regular (@{text "a\<^sup>n"} stands
+  \mbox{@{text "A \<equiv> \<Union>\<^sub>n a\<^sup>n @ b\<^sup>n"}} is not regular (@{text "a\<^sup>n"} stands
   for the strings consisting of @{text n} times the character a; similarly for
-  @{text "b\<^isup>n"}). For this consider the infinite set @{text "B \<equiv> \<Union>\<^isub>n a\<^sup>n"}.
+  @{text "b\<^sup>n"}). For this consider the infinite set @{text "B \<equiv> \<Union>\<^sub>n a\<^sup>n"}.
 
   \begin{lemma}
   No two distinct strings in set @{text "B"} are Myhill-Nerode related by language @{text A}.