equal
deleted
inserted
replaced
318 \] |
318 \] |
319 |
319 |
320 \noindent |
320 \noindent |
321 which holds because @{term "(c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 "} implies @{term "s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) "} |
321 which holds because @{term "(c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 "} implies @{term "s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) "} |
322 |
322 |
323 \item[(2)] This case is similar except that in the last step we have to |
323 \item[(2)] This case is similar. |
324 instantiate the existential quantifier with @{term "Seq (projval r\<^sub>1 c v) v'"} |
|
325 \end{itemize} |
324 \end{itemize} |
326 |
325 |
327 \noindent |
326 \noindent |
328 The final case is that @{term " \<not> nullable r\<^sub>1"} holds. This case again similar |
327 The final case is that @{term " \<not> nullable r\<^sub>1"} holds. This case again similar |
329 to the cases above. |
328 to the cases above. |