984   @{term "tag_str_ALT A B"} is a subset of this product set, so finite. It remains to be shown

   984   @{term "tag_str_ALT A B"} is a subset of this product set---so finite. It remains to be shown

  1043   Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways how this string

  1043   Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split' 

  1044   can be `distributed'  over @{term "A ;; B"}:

  1044   this string to be in @{term "A ;; B"}:

  1113   with the idea ???

  1113   with the idea that in the first split we have to make sure that @{text "x - x'"}

  1114   is in the language @{text B}.

  1116 

  1117   If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}

  1117 

  1118   then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of

  1119   @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.

  1120   We have to show injectivity of this tagging function as

  1121 

  1122   \begin{center}

  1123   @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}

  1124   \end{center}

  1125 

  1126   \noindent

  1127   There are two cases to be considered. First, there exists a @{text "x'"} such that

  1128   @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have

  1129   

  1130   \begin{center}

  1131   @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}

  1132   \end{center}

  1133 

  1134   \noindent

  1135   and by the assumption about @{term "tag_str_SEQ A B"} also 

  1136 

  1137   \begin{center}

  1138   @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}

  1139   \end{center}

  1140 

  1141   \noindent

  1142   That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and 

  1143   @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that

  1144   @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode

  1145   relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we

  1146   have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore

  1147   @{term "y @ z \<in> A ;; B"}, as needed in this case.

  1148 

  1149   Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.

  1150   By the assumption about @{term "tag_str_SEQ A B"} we have

  1151   @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode

  1152   relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude aslo in this case

  1153   with @{term "y @ z \<in> A ;; B"}. That completes the @{const SEQ}-case.\qed