equal
deleted
inserted
replaced
999 @{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"} |
999 @{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"} |
1000 \end{equation} |
1000 \end{equation} |
1001 % |
1001 % |
1002 \noindent |
1002 \noindent |
1003 since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve |
1003 since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve |
1004 \eqref{pattern} we just have to unfold the definition of the tagging-relation and analyse |
1004 \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse |
1005 in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. |
1005 in which set, @{text A} or @{text B}, the string @{term "x @ z"} is. |
1006 The definition of the tagging-function will give us in each case the |
1006 The definition of the tagging-function will give us in each case the |
1007 information to infer that @{text "y @ z \<in> A \<union> B"}. |
1007 information to infer that @{text "y @ z \<in> A \<union> B"}. |
1008 Finally we |
1008 Finally we |
1009 can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed |
1009 can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed |
1040 @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\ |
1040 @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\ |
1041 \end{tabular} |
1041 \end{tabular} |
1042 \end{center} |
1042 \end{center} |
1043 % |
1043 % |
1044 \noindent |
1044 \noindent |
1045 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. |
1045 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. |
1046 |
1046 |
1047 Now assuming @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split' |
1047 Now assuming @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split' |
1048 this string to be in @{term "A ;; B"}: |
1048 this string to be in @{term "A ;; B"}: |
1049 % |
1049 % |
1050 \begin{center} |
1050 \begin{center} |
1102 node[midway, below=0.5em]{@{text "(z - z') \<in> B"}}; |
1102 node[midway, below=0.5em]{@{text "(z - z') \<in> B"}}; |
1103 \end{tikzpicture}} |
1103 \end{tikzpicture}} |
1104 \end{center} |
1104 \end{center} |
1105 % |
1105 % |
1106 \noindent |
1106 \noindent |
1107 Either there is a prefix of @{text x} in @{text A} and the rest in @{text B}, |
1107 Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B}, |
1108 or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}. |
1108 or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}. |
1109 In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the |
1109 In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the |
1110 following tagging-function |
1110 following tagging-function |
1111 % |
1111 % |
1112 \begin{center} |
1112 \begin{center} |