18   projval ("proj _ _ _" [1000,77,1000] 77) and 

   261   

   262   \noindent {\bf Proof} The proof is by induction on the definition of

   263   @{const der}. Other inductions would go through as well. The

   264   interesting case is for @{term "SEQ r\<^sub>1 r\<^sub>2"}. First we analyse the

   265   case where @{term "nullable r\<^sub>1"}. We have by induction hypothesis

   266 

   267   \[

   268   \begin{array}{l}

   269   (IH1)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>1 \<rightarrow> v"} 

   270   \text{\;then\;} @{term "(c # s) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v"}\\

   271   (IH2)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>2 \<rightarrow> v"} 

   272   \text{\;then\;} @{term "(c # s) \<in> r\<^sub>2 \<rightarrow> injval r\<^sub>2 c v"}

   273   \end{array}

   274   \]

   275   

   276   \noindent

   277   and have 

   278 

   279   \[

   280   @{term "s \<in> ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2) \<rightarrow> v"}

   281   \]

   282   

   283   \noindent

   284   There are two cases what @{term v} can be: (1) @{term "Left v'"} and (2) @{term "Right v'"}.

   285 

   286   \begin{itemize}

   287   \item[(1)] We know @{term "s \<in> SEQ (der c r\<^sub>1) r\<^sub>2 \<rightarrow> v'"} holds, from which we

   288   can infer that there are @{text "s\<^sub>1"}, @{term "s\<^sub>2"}, @{text "v\<^sub>1"}, @{term "v\<^sub>2"}

   289   with

   290 

   291   \[

   292   @{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} \qquad\text{and}\qquad @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"}

   293   \]

   294 

   295   and also

   296 

   297   \[

   298   @{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) \<and> s\<^sub>4 \<in> L r\<^sub>2)"}

   299   \]

   300 

   301   \noindent

   302   and have to prove

   303   

   304   \[

   305   @{term "((c # s\<^sub>1) @ s\<^sub>2) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (injval r\<^sub>1 c v\<^sub>1) v\<^sub>2"}

   306   \]

   307 

   308   \noindent

   309   The two requirements @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"} and 

   310   @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} can be proved by the induction hypothese (IH1) and the

   311   fact above.

   312 

   313   \noindent

   314   This leaves to prove

   315   

   316   \[

   317   @{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> (c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}

   318   \]

   319   

   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) "}

   322 

   323   \item[(2)] This case is similar except that in the last step we have to

   324   instantiate the existential quantifier with @{term "Seq (projval r\<^sub>1 c v) v'"}

   325   \end{itemize}

   326 

   327   \noindent 

   328   The final case is that @{term " \<not> nullable r\<^sub>1"} holds. This case again similar

   329   to the cases above.