Journal/Paper.thy
changeset 257 f512026d5d6e
parent 256 acbae3a11fb5
child 258 1abf8586ee6b
equal deleted inserted replaced
256:acbae3a11fb5 257:f512026d5d6e
  2273   Finally we like to show that the Myhill-Nerode Theorem is also convenient for establishing 
  2273   Finally we like to show that the Myhill-Nerode Theorem is also convenient for establishing 
  2274   the non-regularity of languages. For this we use the following version of the Continuation
  2274   the non-regularity of languages. For this we use the following version of the Continuation
  2275   Lemma (see for example~\cite{Rosenberg06}).
  2275   Lemma (see for example~\cite{Rosenberg06}).
  2276 
  2276 
  2277   \begin{lmm}[Continuation Lemma]
  2277   \begin{lmm}[Continuation Lemma]
  2278   If a language @{text A} is regular and a set @{text B} is infinite,
  2278   If a language @{text A} is regular and a set of strings @{text B} is infinite,
  2279   then there exist two distinct strings @{text x} and @{text y} in @{text B} 
  2279   then there exist two distinct strings @{text x} and @{text y} in @{text B} 
  2280   such that @{term "x \<approx>A y"}.
  2280   such that @{term "x \<approx>A y"}.
  2281   \end{lmm}
  2281   \end{lmm}
  2282 
  2282 
  2283   \noindent
  2283   \noindent