# HG changeset patch
# User zhang
# Date 1296914210 0
# Node ID dceb84acdee83eed0a506aa6d6871ed17d68bbad
# Parent  7478be786f87b98bfaac2223dbb5e3a7eb92b42e
Check in Myhill.thy before trying another way to explain DFA

diff -r 7478be786f87 -r dceb84acdee8 Myhill.thy
--- a/Myhill.thy	Sat Feb 05 09:54:52 2011 +0000
+++ b/Myhill.thy	Sat Feb 05 13:56:50 2011 +0000
@@ -35,7 +35,15 @@
 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. 
+corresponds to the state reached by processing @{text "x"} with the augmented automaton. Since  
+@{text "\<approx>Lang `` {x}"} is defined for every @{text "x"}, it corresponds to the fact that 
+the processing of @{text "x"} will never get stuck.
+
+The most acquainted way to define a regular language @{text "Lang"} is by giving an automaton which
+recorgizes every string in @{text "Lang"}. Fig.\ref{fig_origin_auto} gives such a automaton, which 
+can be viewed as a way of assigning status to strings: for any given string @{text "x"}:
+
+
 
 \begin{figure}[h!]
 \centering
diff -r 7478be786f87 -r dceb84acdee8 tphols-2011/myhill.pdf
Binary file tphols-2011/myhill.pdf has changed