equal
deleted
inserted
replaced
1159 by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed |
1159 by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed |
1160 \end{proof} |
1160 \end{proof} |
1161 |
1161 |
1162 \noindent |
1162 \noindent |
1163 The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When |
1163 The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When |
1164 we analyse the case that @{text "x @ z"} is an element in @{text "A\<star>"} and @{text x} is not the |
1164 we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the |
1165 empty string, we |
1165 empty string, we |
1166 have the following picture: |
1166 have the following picture: |
1167 % |
1167 % |
1168 \begin{center} |
1168 \begin{center} |
1169 \scalebox{0.7}{ |
1169 \scalebox{0.7}{ |