equal
deleted
inserted
replaced
1149 |
1149 |
1150 Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}. |
1150 Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}. |
1151 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 |
1152 @{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 |
1153 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 |
1154 with @{term "y @ z \<in> A ;; B"}. That completes the @{const SEQ}-case.\qed |
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 \end{proof} |
1156 \end{proof} |
1156 |
1157 |
1157 \noindent |
1158 \noindent |
1158 The case for @{const STAR} is similar, but poses a few extra challenges. When |
1159 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 we analyse the case that @{text "x @ z"} is element in @{text "A\<star>"}, we |