regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:60bcf13adb77
+:e5e32faa2446
 Deriv ("Der _ _" [1000, 1000] 100) and
 Derivs ("Ders") and
 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
 derivs ("ders") and
 pderiv ("pder") and
 lemma str_eq_def':
 shows "x \<approx>A y \<equiv> (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)"
 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:
 shows "B \<cdot> (\<Union>n. A \<up> n) = (\<Union>n. B \<cdot> (A \<up> n))"
 unfolding conc_def by auto
 graph in terms of the disjoint
 union of the state nodes. Unfortunately in HOL, the standard definition for disjoint
 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
 changes the type---the disjoint union is not a set, but a set of
 pairs. Using this definition for disjoint union means we do not have a
 regular expressions. This theorem gives necessary and sufficient conditions
 for when a language is regular. As a corollary of this theorem we can easily
 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.
 To our best knowledge, our proof of the Myhill-Nerode Theorem is the first
 that is based on regular expressions, only. The part of this theorem stating
 \begin{tabular}{@ {}lp{10cm}}
 (i)   & @{thm star_unfold_left}     \\
 (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"}
+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\<^isub>p \<noteq> []"}} such that @{term "x\<^isub>p \<in> A"} and @{term "x\<^isub>s \<in> A\<star>"}.
+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}
 \noindent
 In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
 formalisation.\footnote{Available under \citeN{myhillnerodeafp11} in the Archive of Formal Proofs at\\
 \url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}.}
 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
 involving equivalence classes of languages. For this we will use Arden's Lemma
 (see for example \citet[Page 100]{Sakarovitch09}),
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 @{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 (lhs) lang.simps(4)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]} & @{text "\<equiv>"} &
-@{thm (rhs) lang.simps(4)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]}\\
+@{thm (rhs) lang.simps(4)[where ?r="r\<^sub>1" and ?s="r\<^sub>2"]}\\
-@{thm (lhs) lang.simps(5)[where ?r="r\<^isub>1" and ?s="r\<^isub>2"]} & @{text "\<equiv>"} &
+@{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\<^isub>1" and ?s="r\<^isub>2"]}\\
+@{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}
 \end{center}
 partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
 equivalence classes. To illustrate this quotient construction, let us give a simple
 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\<^sub>1 = {[]}"}\\
-@{text "X\<^isub>2 = {[a]}"}\\
+@{text "X\<^sub>2 = {[a]}"}\\
-@{text "X\<^isub>3 = {[a, b]}"}\\
+@{text "X\<^sub>3 = {[a, b]}"}\\
-@{text "X\<^isub>4 = UNIV - {[], [a], [a, b]}"}
+@{text "X\<^sub>4 = UNIV - {[], [a], [a, b]}"}
 \end{tabular}
 \end{center}
 One direction of the Myhill-Nerode Theorem establishes
 that if there are finitely many equivalence classes, like in the example above, then
 \begin{equation}
 @{thm finals_def}
 \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
 %
 \begin{equation}\label{finalprops}
 @{thm lang_is_union_of_finals}\hspace{15mm}
 %(with the help of a character).
 In our concrete example we have
 \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\<^sub>1 \<Turnstile>a\<Rightarrow> X\<^sub>2"},\; @{term "X\<^sub>1 \<Turnstile>b\<Rightarrow> X\<^sub>4"};\\
-@{term "X\<^isub>2 \<Turnstile>b\<Rightarrow> X\<^isub>3"},\; @{term "X\<^isub>2 \<Turnstile>a\<Rightarrow> X\<^isub>4"};\\
+@{term "X\<^sub>2 \<Turnstile>b\<Rightarrow> X\<^sub>3"},\; @{term "X\<^sub>2 \<Turnstile>a\<Rightarrow> X\<^sub>4"};\\
-@{term "X\<^isub>3 \<Turnstile>a\<Rightarrow> X\<^isub>4"},\; @{term "X\<^isub>3 \<Turnstile>b\<Rightarrow> X\<^isub>4"} and\\
+@{term "X\<^sub>3 \<Turnstile>a\<Rightarrow> X\<^sub>4"},\; @{term "X\<^sub>3 \<Turnstile>b\<Rightarrow> X\<^sub>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>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\<^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\<^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>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>
+stand for all transitions @{term "Y\<^sub>i\<^sub>j \<Turnstile>c\<^sub>i\<^sub>j\<Rightarrow>
-X\<^isub>i"}.
+X\<^sub>i"}.
 %The intuition behind the equational system is that every
-%equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
+%equation @{text "X\<^sub>i = rhs\<^sub>i"} in this system
-%corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states
+%corresponds roughly to a state of an automaton whose name is @{text X\<^sub>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
+%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\<^isub>i}.
+%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
 is the equivalence class
 containing the empty string @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
 reason why we have to use our reversed version of Arden's Lemma.}
 In our running example we have the initial equational system
 %
 \begin{equation}\label{exmpcs}
 \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-@{term "X\<^isub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
+@{term "X\<^sub>1"} & @{text "="} & @{text "\<lambda>(ONE)"}\\
-@{term "X\<^isub>2"} & @{text "="} & @{text "(X\<^isub>1, ATOM a)"}\\
+@{term "X\<^sub>2"} & @{text "="} & @{text "(X\<^sub>1, ATOM a)"}\\
-@{term "X\<^isub>3"} & @{text "="} & @{text "(X\<^isub>2, ATOM b)"}\\
+@{term "X\<^sub>3"} & @{text "="} & @{text "(X\<^sub>2, ATOM b)"}\\
-@{term "X\<^isub>4"} & @{text "="} & @{text "(X\<^isub>1, ATOM b) + (X\<^isub>2, ATOM a) + (X\<^isub>3, ATOM a)"}\\
+@{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\<^isub>3, ATOM b) + (X\<^isub>4, ATOM a) + (X\<^isub>4, ATOM b)"}\\
+& & \mbox{}\hspace{0mm}@{text "+ (X\<^sub>3, ATOM b) + (X\<^sub>4, ATOM a) + (X\<^sub>4, ATOM b)"}\\
 \end{tabular}}
 \end{equation}
 \noindent
 Overloading the function @{text \<calL>} for the two kinds of terms in the
 @{thm (rhs) lang_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
 @{thm lang_trm.simps(1)[where r="r", THEN eq_reflection]}
 \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
 holds. The reason for adding the @{text \<lambda>}-marker to our initial equational system is
 to obtain this equation: it only holds with the marker, since none of
 adjusting the remaining regular expressions appropriately. To define this adjustment
 we define the \emph{append-operation} taking a term and a regular expression as argument
 \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 (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\<^isub>1" and rexp="r\<^isub>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}
 \noindent
 We lift this operation to entire right-hand sides of equations, written as
 \noindent
 In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
 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 "="} &
+@{term "X\<^sub>4"} & @{text "="} &
-@{text "(X\<^isub>1, TIMES (ATOM b) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM a, ATOM b})) +"}\\
+@{text "(X\<^sub>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\<^sub>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\<^sub>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}))"}
+& & @{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
 Lemma on the level of equations. To ensure the non-emptiness condition of
 Arden's Lemma we say that a right-hand side is @{text ardenable} provided
 the regular expression corresponding to the deleted terms; finally we append this
 regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
 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}
 With these two operations in place, we can define the operation that removes one equation
 from an equational systems @{text ES}. The operation @{const Subst_all}
 Solving the equational system of our running example gives as solution for the
 two final equivalence classes:
 \begin{center}
 \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-@{text "X\<^isub>2"} & @{text "="} & @{text "TIMES ONE (ATOM a)"}\\
+@{text "X\<^sub>2"} & @{text "="} & @{text "TIMES ONE (ATOM a)"}\\
-@{text "X\<^isub>3"} & @{text "="} & @{text "TIMES (TIMES ONE (ATOM a)) (ATOM b)"}
+@{text "X\<^sub>3"} & @{text "="} & @{text "TIMES (TIMES ONE (ATOM a)) (ATOM b)"}
 \end{tabular}
 \end{center}
 \noindent
 Combining them with $\bigplus$ gives us a regular expression for the language @{text "{[a], [a, b]}"}.
 Note that our algorithm for solving equational systems provides also a method for
 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'.
 *}
 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)"}.
 \begin{definition}
-A relation @{text "R\<^isub>1"} \emph{refines} @{text "R\<^isub>2"}
+A relation @{text "R\<^sub>1"} \emph{refines} @{text "R\<^sub>2"}
-provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}.
+provided @{text "R\<^sub>1 \<subseteq> R\<^sub>2"}.
 \end{definition}
 \noindent
 For constructing @{text R}, we will rely on some \emph{tagging-functions}
 defined over strings, see Fig.~\ref{tagfig}. These functions are parameterised by sets
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{thm (lhs) tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]} &
 @{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
 in the proof with the induction hypotheses. \emph{Partitions} is a function
 that generates all possible partitions of a string.\label{tagfig}}
 and @{text Y} must be equal. Therefore \eqref{finiteimageD} allows us to conclude
 with @{thm (concl) finite_eq_tag_rel}.\qed
 \end{proof}
 \begin{lemma}\label{fintwo}
-Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
+Given two equivalence relations @{text "R\<^sub>1"} and @{text "R\<^sub>2"}, whereby
-@{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
+@{text "R\<^sub>1"} refines @{text "R\<^sub>2"}.
-If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>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\<^isub>1" and ?R2.0="R\<^isub>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
+be @{text "X \<mapsto>"}~@{term "{R\<^sub>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)"},
+@{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
+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\<^isub>2"} are equal, provided
+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.
+@{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\<^isub>2 `` {x}"}}.
+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\<^isub>1 ``{x} \<in> f X"}
+From the latter fact we can infer that @{term "R\<^sub>1 ``{x} \<in> f X"}
-and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
+and further @{term "R\<^sub>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}
+such that @{term "R\<^sub>1 `` {x} = R\<^sub>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"},
+are @{text "R\<^sub>1"}-related. Since by assumption @{text "R\<^sub>1"} refines @{text "R\<^sub>2"},
-they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
+they must also be @{text "R\<^sub>2"}-related, as we need to show.\qed
 \end{proof}
 \noindent
 Chaining Lemma~\ref{finone} and \ref{fintwo} together, means in order to show
 that @{term "UNIV // \<approx>(lang r)"} is finite, we have to construct a tagging-function whose
 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"}, 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
 The @{const TIMES}-case is slightly more complicated. We first prove the
 following lemma, which will aid the proof about refinement.
 \begin{equation}
 @{thm Partitions_def}
 \end{equation}
 \noindent
-If we know that @{text "(x\<^isub>p, x\<^isub>s) \<in> Partitions x"}, we will
+If we know that @{text "(x\<^sub>p, x\<^sub>s) \<in> Partitions x"}, we will
-refer to @{text "x\<^isub>p"} as the \emph{prefix} of the string @{text x},
+refer to @{text "x\<^sub>p"} as the \emph{prefix} of the string @{text x},
-and respectively to @{text "x\<^isub>s"} as the \emph{suffix}.
+and respectively to @{text "x\<^sub>s"} as the \emph{suffix}.
 *}
 text {*
 Now assuming  @{term "x @ z \<in> A \<cdot> B"}, there are only two possible ways of how to `split'
 \begin{center}
 \begin{tabular}{c}
 \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 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\<^isub>s"}\hspace{2.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)$)
 node[midway, above=0.5em]{@{text x}};
 ($(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"}};
+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, 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\<^isub>s"}\hspace{0.2em}$ };
+\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]
 (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
 node[midway, above=0.5em]{@{text x}};
 ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
 node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
 \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}
 %
 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 "("}@{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"}.
+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\<^isub>p"} and @{text "x\<^isub>s"} is one possible partition
+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\<^isub>p"} and the
+of the string @{text x}. We have to know that both @{text "x\<^sub>p"} and the
-corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related'
+corresponding partition @{text "y\<^sub>p"} are in @{text "A"}, and that @{text "x\<^sub>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"}.
+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.
 \begin{proof}[@{const TIMES}-Case]
 If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
 \end{center}
 \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
+considered. First, there exists a @{text "z\<^sub>p"} and @{text
-"z\<^isub>s"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s
+"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
+Second there exists a partition @{text "x\<^sub>p"} and @{text "x\<^sub>s"} with
-@{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have
+@{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"}
+This means there must be a partition @{text "y\<^sub>p"} and @{text "y\<^sub>s"}
-such that @{term "y\<^isub>p \<in> A"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B ``
+such that @{term "y\<^sub>p \<in> A"} and @{term "\<approx>B `` {x\<^sub>s} = \<approx>B ``
-{y\<^isub>s}"}. Unfolding the Myhill-Nerode Relation and together with the
+{y\<^sub>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
+facts that @{text "x\<^sub>p \<in> A"} and \mbox{@{text "x\<^sub>s @ z \<in> B"}}, we
-obtain @{term "y\<^isub>p \<in> A"} and @{text "y\<^isub>s @ z \<in> B"}, as needed in
+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
 The case for @{const Star} is similar to @{const TIMES}, but poses a few
 extra challenges.  To deal with them, we define first the notion of a \emph{string
 \begin{center}
 \scalebox{1}{
 \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 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\<^isub>b"}\hspace{7em}$ };
+\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)$)
 node[midway, above=0.5em]{@{text x}};
 ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
 node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}};
 \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>"},
+We can find a strict prefix @{text "x\<^sub>p"} of @{text x} such that @{term "x\<^sub>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 "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
+`overlaps' with @{text z}, splitting it into two components @{text "z\<^sub>a"} and
-@{text "z\<^isub>b"}. For this we know that @{text "x\<^isub>s @ z\<^isub>a \<in> A"} and
+@{text "z\<^sub>b"}. For this we know that @{text "x\<^sub>s @ z\<^sub>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>"}
+@{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]
 If @{term "finite (UNIV // \<approx>A)"}
 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
 We first need to consider the case that @{text x} is the empty string.
 From the assumption about strict prefixes in @{text "\<^raw:$\threesim$>\<^bsub>\<star>tag A\<^esub>"}, we
 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
+From this we know there exist a partition @{text "y\<^sub>p"} and @{text
-"y\<^isub>s"} with @{term "y\<^isub>p \<in> A\<star>"} and also @{term "x\<^isub>s \<approx>A
+"y\<^sub>s"} with @{term "y\<^sub>p \<in> A\<star>"} and also @{term "x\<^sub>s \<approx>A
-y\<^isub>s"}. Unfolding the Myhill-Nerode Relation we know @{term
+y\<^sub>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>"}.
+"y\<^sub>s @ z\<^sub>a \<in> A"}. We also know that @{term "z\<^sub>b \<in> A\<star>"}.
-Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \<in>
+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}
 \begin{rmk}
 @{text "\<times>tag"} function (see second clause in Fig.~\ref{tagfig}).
 A state of this sequentially composed automaton is accepting, if the first
 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
 ended up in. Therefore the @{text "\<star>tag"} function generates again a set of states.
 @{thm (lhs) Deriv_simps(4)} & $=$ & @{thm (rhs) Deriv_simps(4)}\\
 @{thm (lhs) Der_conc}  & $=$ & @{thm (rhs) Der_conc}\\
 @{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 (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\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
+%   & @{thm (rhs) Derivs_simps(3)[where ?s1.0="s\<^sub>1" and ?s2.0="s\<^sub>2"]}\\
 \end{tabular}}
 \end{equation}
 \noindent
 Note that in the last equation we use the list-cons operator written
 \begin{center}
 \begin{longtable}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
 @{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"]}
+@{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\<^isub>1" and ?r2.0="r\<^isub>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\<^isub>1" and ?r2.0="r\<^isub>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\<^isub>1"}~@{text "then"}~%
+& @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^sub>1"}~@{text "then"}~%
-@{term "Plus (Times (deriv c r\<^isub>1) r\<^isub>2) (deriv c r\<^isub>2)"}\\
+@{term "Plus (Times (deriv c r\<^sub>1) r\<^sub>2) (deriv c r\<^sub>2)"}\\
-&             & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
+&             & \phantom{@{text "if"}~@{term "nullable r\<^sub>1"}~}@{text "else"}~%
-@{term "Times (deriv c r\<^isub>1) r\<^isub>2"}\\
+@{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)}
 \end{longtable}
 \end{center}
 \begin{center}
 \begin{longtable}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
 @{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"]}
+@{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\<^isub>1" and ?r2.0="r\<^isub>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\<^isub>1" and ?r2.0="r\<^isub>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\<^isub>1" and ?r2.0="r\<^isub>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}
 \noindent
 Myhill-Nerode Theorem, we have to be able to establish that for the
 corresponding language there are only finitely many derivatives---thus
 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
+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]}\<^isup>\<star> \<union> ({[a,b]}\<^isup>\<star> \<cdot> {[a]})"}}
+written in our notation as \mbox{@{text "{[a,b]}\<^sup>\<star> \<union> ({[a,b]}\<^sup>\<star> \<cdot> {[a]})"}}
 (see \cite[Page~141]{Sakarovitch09}).
 What \citeN{Brzozowski64} established is that for every language there
 \emph{are} only finitely `dissimilar' derivatives for a regular
 expression. Two regular expressions are said to be \emph{similar} provided
 they can be identified using the using the @{text "ACI"}-identities:
 %
 \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 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\<^isub>1 r\<^isub>2"} $\equiv$ @{term "Plus r\<^isub>2 r\<^isub>1"}\\
+(@{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}
 \noindent
 \begin{center}
 \begin{longtable}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
 @{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"]}
+@{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\<^isub>1" and ?r2.0="r\<^isub>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\<^isub>1" and ?r2.0="r\<^isub>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\<^isub>1"}~@{text "then"}~%
+& @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^sub>1"}~@{text "then"}~%
-@{term "(Timess (pderiv c r\<^isub>1) r\<^isub>2) \<union> (pderiv c r\<^isub>2)"}\\
+@{term "(Timess (pderiv c r\<^sub>1) r\<^sub>2) \<union> (pderiv c r\<^sub>2)"}\\
-& & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
+& & \phantom{@{text "if"}~@{term "nullable r\<^sub>1"}~}@{text "else"}~%
-@{term "Timess (pderiv c r\<^isub>1) r\<^isub>2"}\\
+@{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)"}
 \end{longtable}
 \end{center}
 \begin{equation}\label{pdersunivone}
 \mbox{\begin{tabular}{l}
 @{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_Plus[where ?r1.0="r\<^sub>1" and ?r2.0="r\<^sub>2"]}\\
-@{thm pderivs_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>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}
 \noindent
 to construct a regular expression for the complement language by direct
 means. However the existence of such a regular expression can now be easily
 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
+holds for any strings @{text "s\<^sub>1"} and @{text
-"s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"}
+"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.
 Calculating such a regular expression via
 automata using the standard method would be quite involved. It includes the
 %\begin{center}
 %\begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 %@{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 (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\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+%    @{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\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+%@{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\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+%    @{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}
 %
 %\noindent
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{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"]} &
+@{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\<^isub>1" and ?r2.0="r\<^isub>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\<^isub>1" and ?r2.0="r\<^isub>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\<^isub>1" and ?r2.0="r\<^isub>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}
 \noindent
 equivalence classes. Hence an infinite set must contain
 at least two strings that are in the same equivalence class, that is
 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}.
 \end{lemma}

changeset 385	e5e32faa2446
parent 384	60bcf13adb77
child 386	92ca56c1a199