979   @{term "tag_str_ALT A B"} is a subset of this. It remains to be shown

   979   @{term "tag_str_ALT A B"} is a subset of this product set. It remains to show

   980   that @{text "=tag\<^isub>A\<^isub>L\<^isub>T="} refines @{text "\<approx>(A \<union> B)"}.

   980   that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to 

   981 

   981   showing

   982   %

   983   \begin{center}

   984   @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}

   985   \end{center}

   986 

   987   \noindent

   988   which by unfolding the Myhill-Nerode relation is identical to

   989   %

   990   \begin{equation}\label{pattern}

   991   @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}

   992   \end{equation}

   993 

   994   \noindent

   995   since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve

   996   \eqref{pattern} we just have to unfold the tagging-relation and analyse 

   997   in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. Fianlly we

   998   can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed