343 (* tests *)

   344 

   345 lemma b: 

   346   assumes "rd \<in> pder c r"

   347   shows "size rd \<le> (Suc (size r)) * (Suc (size r))"

   348   using assms

   349   apply(induct r arbitrary: rd)

   350   apply(auto)[3]

   351   apply(case_tac "c = x")

   352       apply(auto)[2]

   353   prefer 2

   354     apply(auto)[1]

   355   oops

   356   

   357   

   358 

   359 lemma a: 

   360   assumes "rd \<in> pders s (SEQ r1 r2)"

   361   shows "size  rd \<le> Suc (size r1 + size r2)"

   362   using assms

   363   apply(induct s arbitrary: r1 r2 rd)

   364    apply(simp)

   365   apply(auto)

   366   apply(case_tac "nullable r1")

   367    apply(auto)

   368   oops

   369   

   370 

   371 lemma

   372   shows "\<forall>rd \<in> (pders_Set UNIV r). size rd \<le> size r"

   373   apply(induct r)

   374        apply(auto)[1]

   375        apply(simp add: pders_Set_def)

   376       apply(simp add: pders_Set_def)

   377      apply(simp add: pders_Set_def pders_CHAR)

   378   using pders_CHAR apply fastforce

   379     prefer 2

   380     apply(simp add: pders_Set_def)

   381     apply (meson Un_iff le_SucI trans_le_add1 trans_le_add2)

   382   apply(simp add: pders_Set_def)

   383    apply(auto)[1]

   384   apply(case_tac y)

   385   apply(simp)

   386    apply(simp)

   387    apply(auto)[1]

   388    apply(case_tac "nullable r1")

   389     apply(simp)

   390     apply(auto)[1]

   391      prefer 3

   392      apply(simp)

   393      apply(auto)[1]

   394      apply(subgoal_tac "size xa \<le> size r1")

   395       prefer 2

   396       apply (metis UN_I pders.simps(1) pders_snoc singletonI)

   397   oops

   398   

   399   

   400   

   401