1044 this string to be in @{term "A ;; B"}: |
1044 this string to be in @{term "A ;; B"}: |
1045 |
1045 |
1046 \begin{center} |
1046 \begin{center} |
1047 \scalebox{0.7}{ |
1047 \scalebox{0.7}{ |
1048 \begin{tikzpicture} |
1048 \begin{tikzpicture} |
1049 \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}x'\hspace{4em}$ }; |
1049 \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'"}\hspace{4em}$ }; |
1050 \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}x - x'\hspace{0.5em}$ }; |
1050 \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'"}\hspace{0.5em}$ }; |
1051 \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}z\hspace{10.1em}$ }; |
1051 \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{10.1em}@{text z}\hspace{10.1em}$ }; |
1052 |
1052 |
1053 \draw[decoration={brace,transform={yscale=3}},decorate] |
1053 \draw[decoration={brace,transform={yscale=3}},decorate] |
1054 (xa.north west) -- ($(xxa.north east)+(0em,0em)$) |
1054 (xa.north west) -- ($(xxa.north east)+(0em,0em)$) |
1055 node[midway, above=0.5em]{$x$}; |
1055 node[midway, above=0.5em]{@{text x}}; |
1056 |
1056 |
1057 \draw[decoration={brace,transform={yscale=3}},decorate] |
1057 \draw[decoration={brace,transform={yscale=3}},decorate] |
1058 (z.north west) -- ($(z.north east)+(0em,0em)$) |
1058 (z.north west) -- ($(z.north east)+(0em,0em)$) |
1059 node[midway, above=0.5em]{$z$}; |
1059 node[midway, above=0.5em]{@{text z}}; |
1060 |
1060 |
1061 \draw[decoration={brace,transform={yscale=3}},decorate] |
1061 \draw[decoration={brace,transform={yscale=3}},decorate] |
1062 ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$) |
1062 ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$) |
1063 node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}}; |
1063 node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}}; |
1064 |
1064 |
1071 node[midway, below=0.5em]{@{term "x' \<in> A"}}; |
1071 node[midway, below=0.5em]{@{term "x' \<in> A"}}; |
1072 \end{tikzpicture}} |
1072 \end{tikzpicture}} |
1073 |
1073 |
1074 \scalebox{0.7}{ |
1074 \scalebox{0.7}{ |
1075 \begin{tikzpicture} |
1075 \begin{tikzpicture} |
1076 \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}x\hspace{6.5em}$ }; |
1076 \node[draw,minimum height=3.8ex] (x) { $\hspace{6.5em}@{text x}\hspace{6.5em}$ }; |
1077 \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}z'\hspace{2em}$ }; |
1077 \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{2em}@{text "z'"}\hspace{2em}$ }; |
1078 \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}z - z'\hspace{6.1em}$ }; |
1078 \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{6.1em}@{text "z - z'"}\hspace{6.1em}$ }; |
1079 |
1079 |
1080 \draw[decoration={brace,transform={yscale=3}},decorate] |
1080 \draw[decoration={brace,transform={yscale=3}},decorate] |
1081 (x.north west) -- ($(za.north west)+(0em,0em)$) |
1081 (x.north west) -- ($(za.north west)+(0em,0em)$) |
1082 node[midway, above=0.5em]{$x$}; |
1082 node[midway, above=0.5em]{@{text x}}; |
1083 |
1083 |
1084 \draw[decoration={brace,transform={yscale=3}},decorate] |
1084 \draw[decoration={brace,transform={yscale=3}},decorate] |
1085 ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$) |
1085 ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$) |
1086 node[midway, above=0.8em]{$z$}; |
1086 node[midway, above=0.5em]{@{text z}}; |
1087 |
1087 |
1088 \draw[decoration={brace,transform={yscale=3}},decorate] |
1088 \draw[decoration={brace,transform={yscale=3}},decorate] |
1089 ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$) |
1089 ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$) |
1090 node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}}; |
1090 node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}}; |
1091 |
1091 |
1150 By the assumption about @{term "tag_str_SEQ A B"} we have |
1151 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 @{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 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 |
1154 with @{term "y @ z \<in> A ;; B"}. That completes the @{const SEQ}-case.\qed |
1154 \end{proof} |
1155 \end{proof} |
|
1156 |
|
1157 \noindent |
|
1158 The case for @{const STAR} is similar, but poses a few extra challenges. When |
|
1159 we analyse the case that @{text "x @ z"} is element in @{text "A\<star>"}, we |
|
1160 have the following picture: |
|
1161 |
|
1162 \begin{center} |
|
1163 \scalebox{0.7}{ |
|
1164 \begin{tikzpicture} |
|
1165 \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ }; |
|
1166 \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ }; |
|
1167 \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ }; |
|
1168 \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ }; |
|
1169 |
|
1170 \draw[decoration={brace,transform={yscale=3}},decorate] |
|
1171 (xa.north west) -- ($(xxa.north east)+(0em,0em)$) |
|
1172 node[midway, above=0.5em]{@{text x}}; |
|
1173 |
|
1174 \draw[decoration={brace,transform={yscale=3}},decorate] |
|
1175 (za.north west) -- ($(zb.north east)+(0em,0em)$) |
|
1176 node[midway, above=0.5em]{@{text z}}; |
|
1177 |
|
1178 \draw[decoration={brace,transform={yscale=3}},decorate] |
|
1179 ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$) |
|
1180 node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}}; |
|
1181 |
|
1182 \draw[decoration={brace,transform={yscale=3}},decorate] |
|
1183 ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$) |
|
1184 node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}}; |
|
1185 |
|
1186 \draw[decoration={brace,transform={yscale=3}},decorate] |
|
1187 ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$) |
|
1188 node[midway, below=0.5em]{@{text "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}}; |
|
1189 |
|
1190 \draw[decoration={brace,transform={yscale=3}},decorate] |
|
1191 ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$) |
|
1192 node[midway, below=0.5em]{@{text "z\<^isub>b \<in> A\<star>"}}; |
|
1193 |
|
1194 \draw[decoration={brace,transform={yscale=3}},decorate] |
|
1195 ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$) |
|
1196 node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}}; |
|
1197 \end{tikzpicture}} |
|
1198 \end{center} |
|
1199 |
|
1200 \noindent |
|
1201 We can find a prefix @{text "x'"} of @{text x} such that @{text "x' \<in> A\<star>"} |
|
1202 and the rest @{text "(x - x') @ z \<in> A\<star>"}. For example the empty string |
|
1203 @{text "[]"} would do. |
|
1204 There are many such prefixes, but there can only be finitely many of them (the |
|
1205 string @{text x} is finite). Let us therefore choose the longest one and call it |
|
1206 @{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 |
|
1207 know it is in @{text "A\<star>"}. By definition of @{text "A\<star>"}, we can separate |
|
1208 this string into two parts, say @{text "a"} and @{text "b"}, such @{text "a \<in> A"} |
|
1209 and @{text "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}, |
|
1210 otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a} |
|
1211 `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and |
|
1212 @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and |
|
1213 @{text "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{text "x @ z \<in> A\<star>"} |
|
1214 such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the |
|
1215 `border' of @{text x} and @{text z}. This string is @{text "(x - x') @ z\<^isub>a"}. |
|
1216 |
|
1217 In order to show that @{text "x @ z \<in> A\<star>"} implies @{text "y @ z \<in> A\<star>"}, we use |
|
1218 the following tagging-function: |
|
1219 |
|
1220 \begin{center} |
|
1221 @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]} |
|
1222 \end{center} |
1155 |
1223 |
1156 \begin{proof}[@{const STAR}-Case] |
1224 \begin{proof}[@{const STAR}-Case] |
1157 |
1225 |
1158 \begin{center} |
1226 |
1159 @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]} |
|
1160 \end{center} |
|
1161 \end{proof} |
1227 \end{proof} |
1162 *} |
1228 *} |
1163 |
1229 |
1164 |
1230 |
1165 |
1231 |