equal
deleted
inserted
replaced
1039 \end{center} |
1039 \end{center} |
1040 |
1040 |
1041 \noindent |
1041 \noindent |
1042 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. |
1042 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. |
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 how this string |
1044 is `split' over @{term "A ;; B"}: |
1044 can be `distributed' over @{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}x'\hspace{4em}$ }; |
1100 \end{center} |
1100 \end{center} |
1101 |
1101 |
1102 \noindent |
1102 \noindent |
1103 Either there is a prefix of @{text x} in @{text A} and the rest in @{text B}, |
1103 Either there is a prefix of @{text x} in @{text A} and the rest in @{text B}, |
1104 or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}. |
1104 or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B}. |
1105 In bot cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the |
1105 In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the |
1106 following tagging-function |
1106 following tagging-function |
1107 |
1107 |
1108 \begin{center} |
1108 \begin{center} |
1109 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]} |
1109 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]} |
1110 \end{center} |
1110 \end{center} |