1115 |
1115 |
1116 \begin{proof}[@{const SEQ}-Case] |
1116 \begin{proof}[@{const SEQ}-Case] |
1117 If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"} |
1117 If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"} |
1118 then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of |
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. |
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 |
1120 We have to show injectivity of this tagging-function as |
1121 |
1121 |
1122 \begin{center} |
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"} |
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} |
1124 \end{center} |
1125 |
1125 |
1154 with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case |
1154 with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case |
1155 by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed |
1155 by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed |
1156 \end{proof} |
1156 \end{proof} |
1157 |
1157 |
1158 \noindent |
1158 \noindent |
1159 The case for @{const STAR} is similar, but poses a few extra challenges. When |
1159 The case for @{const STAR} is similar as @{const SEQ}, but poses a few extra challenges. When |
1160 we analyse the case that @{text "x @ z"} is element in @{text "A\<star>"}, we |
1160 we analyse the case that @{text "x @ z"} is element in @{text "A\<star>"} and @{text x} is not the |
|
1161 empty string, we |
1161 have the following picture: |
1162 have the following picture: |
1162 |
1163 |
1163 \begin{center} |
1164 \begin{center} |
1164 \scalebox{0.7}{ |
1165 \scalebox{0.7}{ |
1165 \begin{tikzpicture} |
1166 \begin{tikzpicture} |
1197 node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}}; |
1198 node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}}; |
1198 \end{tikzpicture}} |
1199 \end{tikzpicture}} |
1199 \end{center} |
1200 \end{center} |
1200 |
1201 |
1201 \noindent |
1202 \noindent |
1202 We can find a prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"} |
1203 We can find a strict prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"}, |
1203 and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string |
1204 @{text "x' < x"} and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string |
1204 @{text "[]"} would do. |
1205 @{text "[]"} would do. |
1205 There are many such prefixes, but there can only be finitely many of them (the |
1206 There are many such prefixes, but there can only be finitely many of them (the |
1206 string @{text x} is finite). Let us therefore choose the longest one and call it |
1207 string @{text x} is finite). Let us therefore choose the longest one and call it |
1207 @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we |
1208 @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we |
1208 know it is in @{text "A\<star>"}. By definition of @{text "A\<star>"}, we can separate |
1209 know it is in @{text "A\<star>"}. By definition of @{text "A\<star>"}, we can separate |
1221 \begin{center} |
1222 \begin{center} |
1222 @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]} |
1223 @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]} |
1223 \end{center} |
1224 \end{center} |
1224 |
1225 |
1225 \begin{proof}[@{const STAR}-Case] |
1226 \begin{proof}[@{const STAR}-Case] |
1226 |
1227 If @{term "finite (UNIV // \<approx>A)"} |
1227 |
1228 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of |
|
1229 @{term "tag_str_STAR A"} is a subset of this set, and therefore finite. |
|
1230 Again we have to show injectivity of this tagging-function as |
|
1231 |
|
1232 \begin{center} |
|
1233 @{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"} |
|
1234 \end{center} |
|
1235 |
|
1236 \noindent |
|
1237 We first need to consider the case that @{text x} is the empty string. |
|
1238 From the assumption we can infer @{text y} is the empty string and |
|
1239 clearly have @{text "y @ z \<in> A\<star>"}. In case @{text x} is not the empty |
|
1240 string, we can devide the string @{text "x @ z"} as shown in the picture |
|
1241 above. By the tagging function we have |
|
1242 |
|
1243 \begin{center} |
|
1244 @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"} |
|
1245 \end{center} |
|
1246 |
|
1247 \noindent |
|
1248 which by assumption is equal to |
|
1249 |
|
1250 \begin{center} |
|
1251 @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"} |
|
1252 \end{center} |
|
1253 |
|
1254 \noindent |
|
1255 and we know that we have a @{text "y'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"} and @{text "y'\<^isub>m\<^isub>a\<^isub>x < y"} |
|
1256 and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y'\<^isub>m\<^isub>a\<^isub>x)"}. Unfolding the Myhill-Nerode |
|
1257 relation we know @{term "(y - y'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}. We also know that @{text "z\<^isub>b \<in> A\<star>"}. |
|
1258 Therefore, finally, @{text "y'\<^isub>m\<^isub>a\<^isub>x @ ((y - y'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means |
|
1259 @{term "y @ z \<in> A\<star>"}. As a last step we have to set @{text "A"} to @{text "L r"} and |
|
1260 complete the proof. |
1228 \end{proof} |
1261 \end{proof} |
1229 *} |
1262 *} |
1230 |
1263 |
1231 |
1264 |
1232 |
1265 |