450          "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"

   450          "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))"  

   451     (* here *)    

   530     case (NMTIMES x1 x2 m s v)

   529     case (NMTIMES r n m s v)

   531     then show ?case sorry      

   530       have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact

   531   have "s \<in> der c (NMTIMES r n m) \<rightarrow> v" by fact

   532   then consider

   533       (cons) v1 vs s1 s2 where 

   534         "v = Seq v1 (Stars vs)" "s = s1 @ s2" 

   535         "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> (Stars vs)" "0 < n" "n \<le> m"

   536         "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))"

   537      | (null) v1 vs s1 s2 where 

   538         "v = Seq v1 (Stars vs)" "s = s1 @ s2"  "s2 \<in> (UPNTIMES r (m - 1)) \<rightarrow> (Stars vs)" 

   539         "s1 \<in> der c r \<rightarrow> v1" "n = 0" "0 < m"

   540          "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))"  

   541     apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)

   542     prefer 2

   543     apply(erule Posix_elims)

   544     apply(simp)

   545     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")

   546     apply(clarify)

   547     apply(drule_tac x="v1" in meta_spec)

   548     apply(drule_tac x="vss" in meta_spec)

   549     apply(drule_tac x="s1" in meta_spec)

   550     apply(drule_tac x="s2" in meta_spec)

   551      apply(simp add: der_correctness Der_def)

   552       apply(rotate_tac 5)

   553     apply(erule Posix_elims)

   554       apply(auto)[2]

   555     apply(erule Posix_elims)

   556       apply(simp)

   557      apply blast

   558       

   559     apply(erule Posix_elims)

   560     apply(auto)

   561       apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits)      

   562     apply(subgoal_tac "\<exists>vss. v2 = Stars vss")

   563      apply(clarify)

   564     apply simp

   565       apply(rotate_tac 6)

   566     apply(erule Posix_elims)

   567       apply(auto)[2]

   568     done

   569     then show "(c # s) \<in> (NMTIMES r n m) \<rightarrow> injval (NMTIMES r n m) c v" 

   570     proof (cases)

   571       case cons

   572           have "s1 \<in> der c r \<rightarrow> v1" by fact

   573           then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp

   574         moreover

   575           have "s2 \<in> (NMTIMES r (n - 1) (m - 1)) \<rightarrow> Stars vs" by fact

   576         moreover 

   577           have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 

   578           then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)

   579           then have "flat (injval r c v1) \<noteq> []" by simp

   580         moreover 

   581           have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))" by fact

   582           then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r (n - 1) (m - 1)))" 

   583             by (simp add: der_correctness Der_def)

   584         ultimately 

   585         have "((c # s1) @ s2) \<in> NMTIMES r n m \<rightarrow> Stars (injval r c v1 # vs)" 

   586            apply (rule_tac Posix.intros)

   587                apply(simp_all)

   588               apply(case_tac n)

   589             apply(simp)

   590           using Posix_elims(1) NMTIMES.prems apply auto[1]

   591           using cons(5) apply blast

   592            apply(simp)

   593             apply(rule cons)

   594              done

   595         then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using cons by(simp)

   596       next 

   597        case null

   598           have "s1 \<in> der c r \<rightarrow> v1" by fact

   599           then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp

   600           moreover 

   601             have "s2 \<in> UPNTIMES r (m - 1) \<rightarrow> Stars vs" by fact

   602           moreover 

   603           have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact 

   604           then have "flat (injval r c v1) = (c # s1)" by (rule Posix1)

   605           then have "flat (injval r c v1) \<noteq> []" by simp

   606           moreover

   607              moreover 

   608           have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))" by fact

   609           then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r (m - 1)))" 

   610             by (simp add: der_correctness Der_def)

   611         ultimately 

   612         have "((c # s1) @ s2) \<in> NMTIMES r 0 m \<rightarrow> Stars (injval r c v1 # vs)" 

   613            apply (rule_tac Posix.intros) back

   614               apply(simp_all)

   615               apply(rule null)

   616            done

   617         then show "(c # s) \<in> NMTIMES r n m \<rightarrow> injval (NMTIMES r n m) c v" using null 

   618           apply(simp)

   619           done  

   620       qed