359 apply(auto simp add: Sequ_def Der_def)[1]

   359 apply(auto simp add: Sequ_def Der_def)[1]

   360 using Star_def apply auto[1]

   360 using Star_def apply auto[1]

   361 apply(case_tac "[] \<in> L r")

   361 apply(case_tac "[] \<in> L r")

   362 apply(auto)

   362 apply(auto)

   363 using Der_UNION Der_star Star_def by fastforce

   363 using Der_UNION Der_star Star_def by fastforce

   364 

   365 

   365 lemma ders_correctness:

   366 lemma ders_correctness:

   366   shows "L (ders s r) = Ders s (L r)"

   367   shows "L (ders s r) = Ders s (L r)"

   367 apply(induct s arbitrary: r)

   368 apply(induct s arbitrary: r)

   368 apply(simp_all add: Ders_def der_correctness Der_def)

   369 apply(simp_all add: Ders_def der_correctness Der_def)