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