2300   After unfolding the definition of @{text "B"}, we need to establish that given @{term "i \<noteq> j"},

  2300   After unfolding the definition of @{text "B"}, we need to establish that given @{term "i \<noteq> j"},

  2301   the strings @{text "a\<^sup>i"} and @{text "a\<^sup>j"} are not Myhill-Nerode related by @{text "A"}.

  2301   the strings @{text "a\<^sup>i"} and @{text "a\<^sup>j"} are not Myhill-Nerode related by @{text "A"}.

  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 

  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   a contradiction. Let us take @{text "b\<^sup>i"} for @{text "z"}. Then we know @{text "a\<^sup>i @ b\<^sup>i \<in> A"}.

  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   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"}

  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"}

  2306   \end{proof}

  2306   \end{proof}

  2307 

  2307 

  2308   \noindent

  2308   \noindent

  2309   To conclude the proof of non-regularity for the language @{text A}, the

  2309   To conclude the proof of non-regularity for the language @{text A}, the

  2310   Continuation Lemma and the lemma above lead to a contradiction assuming

  2310   Continuation Lemma and the lemma above lead to a contradiction assuming