diff -r 649ff0b8766d -r b69d4e04e64a Myhill.thy
--- a/Myhill.thy	Thu Feb 03 12:44:46 2011 +0000
+++ b/Myhill.thy	Fri Feb 04 13:02:00 2011 +0000
@@ -5,7 +5,88 @@
 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
 
 text {*
-  It is now the time for use to discuss further about the way.
+
+The intuition behind our treatment is still automata. Taking the automaton in 
+Fig.\ref{fig_origin_auto} as an example, like any automaton, it
+represents the vehicle used to recognize a certain regular language.
+For any given string, the process starts from the left most and proceed 
+character by character to the right, driving the state transtion of automaton 
+starting from the initial state (the one marked by an short arrow). There could
+be three outcomes:
+  \begin{enumerate}
+   \item The process finally reaches the end of the string and the automaton is at an accepting
+        state, in which case the string is considered a member of the language.
+         For the automaton in Fig.\ref{fig_origin_auto}, @{text "a, ab, abb, abc, abbcc, b, baa"}
+         are such kind of strings.
+   \item The process finally reaches the end of the string but the automaton is at an non-accepting
+         state, in which case, the string is considered a non-member of the language. For the automaton 
+         in Fig.\ref{fig_origin_auto}, @{text "ad, abbd, adbd, bdabbccd"}
+         are such kind of strings. \label{case_end_reject}
+   \item \label{case_stuck}
+     The process get stuck at the middle of the string, in which case, the string is considered
+           a non-member of the lauguage.  For the automaton in Fig.\ref{fig_origin_auto}, 
+           @{text "c, acb, bbacd, aaccd"} 
+           are such kind of strings.
+  \end{enumerate}
+To avoid the situation \ref{case_stuck} above, we can augment a normal automaton with a ``absorbing state'',
+as the state $X_3$ in Fig.\ref{fig_extended_auto}. In an auguments automaton, the process of strings never
+get stuck: whenever a string is recognized as not belonging to the language, the augmented automaton
+is transfered into the ``absorbing state'' and kept there until the process reaches the end of the string, 
+in which case, the string is rejected by situation \ref{case_end_reject} above.
+
+Given a language @{text "Lang"} and a string @{text "x"}, the equivalent class @{text "\<approx>Lang `` {x}"}
+corresponds to the state reached by processing @{text "x"} with the augmented automaton. 
+
+\begin{figure}[h!]
+\centering
+\subfigure[Original automaton]{\label{fig_origin_auto}
+\begin{minipage}{0.4\textwidth}
+\scalebox{0.8}{
+\begin{tikzpicture}[ultra thick,>=latex]
+  \node[draw,circle,initial] (start) {$X_0$};
+  \node[draw,circle,accepting] at ($(start) + (3.5cm,2cm)$) (ac1) {$X_1$};
+  \node[draw,circle,accepting] at ($(start) + (3.5cm,-2cm)$) (ac2) {$X_2$};
+
+  \path[->] (start) edge [bend left] node [midway, above] {$a$} (ac1);
+  \path[->] (start) edge [bend right] node [midway, below] {$b$} (ac2);
+  \path[->] (ac1) edge [loop above] node [midway, above] {$b$} (ac1);
+  \path[->] (ac2) edge [loop below] node [midway, below] {$a$} (ac2);
+  \path[->] (ac1) edge [bend right] node [midway, left] {$c$} (ac2);
+  \path[->] (ac2) edge [bend right] node [midway, right] {$c$} (ac1);
+  \path[->] (ac1) edge node [midway, sloped, above] {$d$} (start);
+  \path[->] (ac2) edge node [midway, sloped, above] {$d$} (start);
+\end{tikzpicture}}
+\end{minipage}
+}
+\subfigure[Extended automaton]{\label{fig_extended_auto}
+\begin{minipage}{0.5\textwidth}
+\scalebox{0.8}{
+\begin{tikzpicture}[ultra thick,>=latex]
+  \node[draw,circle,initial] (start) {$X_0$};
+  \node[draw,circle,accepting] at ($(start) + (3.5cm,2cm)$) (ac1) {$X_1$};
+  \node[draw,circle,accepting] at ($(start) + (3.5cm,-2cm)$) (ac2) {$X_2$};
+  \node[draw,circle] at ($(start) + (6.5cm,0cm)$) (ab) {$X_3$};
+
+  \path[->] (start) edge [bend left] node [midway, above] {$a$} (ac1);
+  \path[->] (start) edge [bend right] node [midway, below] {$b$} (ac2);
+  \path[->] (ac1) edge [loop above] node [midway, above] {$b$} (ac1);
+  \path[->] (ac2) edge [loop below] node [midway, below] {$a$} (ac2);
+  \path[->] (ac1) edge [bend right] node [midway, left] {$c$} (ac2);
+  \path[->] (ac2) edge [bend right] node [midway, right] {$c$} (ac1);
+  \path[->] (ac1) edge node [midway, sloped, above] {$d$} (start);
+  \path[->] (ac2) edge node [midway, sloped, above] {$d$} (start);
+
+  \path [draw, rounded corners,->,dashed] (start) -- ($(start) + (0cm, 3.7cm)$)
+         -- ($(ab) + (0cm, 3.7cm)$)  node[midway,above,sloped]{$\Sigma - \{a, b\}$} -- (ab);
+  \path[->,dashed] (ac1) edge node [midway, above, sloped] {$\Sigma - \{b,c,d\}$} (ab);
+  \path[->,dashed] (ac2) edge node [midway, below, sloped] {$\Sigma - \{a,c,d\}$} (ab);
+  \path[->,dashed] (ab) edge [loop right] node [midway, right] {$\Sigma$} (ab);
+\end{tikzpicture}}
+\end{minipage}
+}
+\caption{The relationship between automata and finite partition}\label{fig_auto_part_rel}
+\end{figure}
+
   *}
 
 end