2295 \begin{lmm} |
2295 \begin{lmm} |
2296 No two distinct strings in set @{text "B"} are Myhill-Nerode related by language @{text A}. |
2296 No two distinct strings in set @{text "B"} are Myhill-Nerode related by language @{text A}. |
2297 \end{lmm} |
2297 \end{lmm} |
2298 |
2298 |
2299 \begin{proof} |
2299 \begin{proof} |
2300 After unfolding the definitions, we need to establish that for @{term "i \<noteq> j"}, |
2300 After unfolding the definition of @{text "B"}, we need to establish that given @{term "i \<noteq> j"}, |
2301 the equality \mbox{@{text "a\<^sup>i @ b\<^sup>j = a\<^sup>n @ b\<^sup>n"}} leads to a contradiction. This is clearly the case |
2301 the strings @{text "a\<^sup>i"} and @{text "a\<^sup>j"} are not Myhill-Nerode related by @{text "A"}. |
2302 if we test that the two strings have the same amount of @{text a}'s and @{text b}'s; |
2302 That means we have to show that \mbox{@{text "\<forall>z. a\<^sup>i @ z \<in> A = a\<^sup>j @ z \<in> A"}} leads to |
2303 the string on the right-hand side satisfies this property, but not the one on |
2303 a contradiction. Let us take @{text "b\<^sup>i"} for @{text "z"}. Then we know @{text "a\<^sup>i @ b\<^sup>i \<in> A"}. |
2304 the left-hand side. Therefore the strings cannot be equal and we have a contradiction. |
2304 But since @{term "i \<noteq> j"}, @{text "a\<^sup>j @ b\<^sup>i \<notin> A"}. Therefore @{text "a\<^sup>i"} and @{text "a\<^sup>j"} |
|
2305 cannot be Myhill-Nerode related by @{text "A"} and we are done. |
2305 \end{proof} |
2306 \end{proof} |
2306 |
2307 |
2307 \noindent |
2308 \noindent |
2308 To conclude the proof on non-regularity of language @{text A}, the |
2309 To conclude the proof of non-regularity for the language @{text A}, the |
2309 Continuation Lemma and the lemma above lead to a contradiction assuming |
2310 Continuation Lemma and the lemma above lead to a contradiction assuming |
2310 @{text A} is regular. Therefore the language @{text A} is not regular, as we |
2311 @{text A} is regular. Therefore the language @{text A} is not regular, as we |
2311 wanted to show. |
2312 wanted to show. |
2312 *} |
2313 *} |
2313 |
2314 |