diff -r 09ce1cdb70ab -r d9d4146325d9 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Wed May 15 11:51:52 2019 +0100
+++ b/thys/BitCoded.thy	Thu May 23 13:30:09 2019 +0100
@@ -129,7 +129,11 @@
 | "good (AONE cs) = True" 
 | "good (ACHAR cs c) = True"
 | "good (AALTs cs []) = False"
-| "good (AALTs cs (r#rs)) = (\<forall>r' \<in> set (r#rs). good r')"
+| "good (AALTs cs [r]) = False"
+| "good (AALTs cs (r1#r2#rs)) = (\<forall>r' \<in> set (r1#r2#rs). good r' \<and> nonalt r')"
+| "good (ASEQ _ AZERO _) = False"
+| "good (ASEQ _ (AONE _) _) = False"
+| "good (ASEQ _ _ AZERO) = False"
 | "good (ASEQ cs r1 r2) = (good r1 \<and> good r2)"
 | "good (ASTAR cs r) = True"
 
@@ -1079,13 +1083,40 @@
 
 lemma good_fuse:
   shows "good (fuse bs r) = good r"
-  apply(induct r)
+  apply(induct r arbitrary: bs)
        apply(auto)
-  apply (metis arexp.distinct(25) arexp.distinct(7) arexp.inject(4) good.elims(3) good.simps(4) good.simps(5))
-  by (metis good.simps(4) good.simps(5) neq_Nil_conv)
+     apply(case_tac r1)
+          apply(simp_all)
+  apply(case_tac r2)
+          apply(simp_all)
+  apply(case_tac r2)
+            apply(simp_all)
+  apply(case_tac r2)
+           apply(simp_all)
+  apply(case_tac r2)
+          apply(simp_all)
+  apply(case_tac r1)
+          apply(simp_all)
+  apply(case_tac r2)
+           apply(simp_all)
+  apply(case_tac r2)
+           apply(simp_all)
+  apply(case_tac r2)
+           apply(simp_all)
+  apply(case_tac r2)
+         apply(simp_all)
+  apply(case_tac x2a)
+    apply(simp_all)
+  apply(case_tac list)
+    apply(simp_all)
+  apply(case_tac x2a)
+    apply(simp_all)
+  apply(case_tac list)
+    apply(simp_all)
+  done
 
 lemma good0:
-  assumes "rs \<noteq> Nil" 
+  assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. nonalt r"
   shows "good (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. good r)"
   using  assms
   apply(induct bs rs rule: bsimp_AALTs.induct)
@@ -1093,12 +1124,17 @@
   done
 
 lemma good0a:
-  assumes "flts (map bsimp rs) \<noteq> Nil" 
+  assumes "flts (map bsimp rs) \<noteq> Nil" "\<forall>r \<in> set (flts (map bsimp rs)). nonalt r"
   shows "good (bsimp (AALTs bs rs)) \<longleftrightarrow> (\<forall>r \<in> set (flts (map bsimp rs)). good r)"
   using  assms
   apply(simp)
-  apply(rule good0)
+  apply(auto)
+  apply(subst (asm) good0)
    apply(simp)
+    apply(auto)
+   apply(subst good0)
+   apply(simp)
+    apply(auto)
   done
 
 lemma flts0:
@@ -1122,7 +1158,7 @@
 
 lemma flts2:
   assumes "good r" 
-  shows "\<forall>r' \<in> set (flts [r]). good r'"
+  shows "\<forall>r' \<in> set (flts [r]). good r' \<and> nonalt r'"
   using  assms
   apply(induct r)
        apply(simp)
@@ -1131,16 +1167,11 @@
     prefer 2
     apply(simp)
     apply(auto)[1]
-  apply (metis good.simps(5) good_fuse in_set_insert insert_Nil list.exhaust)
-   prefer 2
-   apply(simp)
-  by fastforce
-
-lemma flts3a:
-  assumes "good r" 
-  shows "good (AALTs bs (flts [r]))"
-  using  assms
-  by (metis flts1 flts2 good.simps(5) neq_Nil_conv)
+     apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) good_fuse)
+  apply (metis bsimp_AALTs.elims good.simps(4) good.simps(5) good.simps(6) nn11a)
+   apply fastforce
+  apply(simp)
+  done  
 
 
 lemma flts3:
@@ -1172,11 +1203,12 @@
   apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b nonalt.simps(1) nonalt.simps(2))
   apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(2) good0 k0b list.distinct(1) list.inject nonalt.simps(3))
   apply (metis arexp.distinct(3) arexp.distinct(7) bsimp_AALTs.elims fuse.simps(3) list.distinct(1) list.inject)
-  apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good.simps(6) good_fuse list.distinct(1) list.inject)
-  apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
-  apply (metis arexp.distinct(7) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) flts.simps(1) flts.simps(2) flts1 good.simps(7) good_fuse neq_Nil_conv)
+  apply (metis arexp.distinct(7) bsimp_AALTs.elims good.simps(1) good_fuse list.distinct(1) list.inject)
+    apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
+  apply (metis arexp.distinct(7) bsimp_AALTs.elims flts2 good.simps(1) good.simps(33) good0 k0b list.distinct(1) list.inject nonalt.simps(6))
   by (metis (no_types, lifting) Nil_is_append_conv append_Nil2 arexp.distinct(7) bsimp_AALTs.elims butlast.simps(2) butlast_append flts1 flts2 good.simps(1) good0 k0a)
 
+
 lemma flts_nil:
   assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
             good (bsimp y) \<or> bsimp y = AZERO"
@@ -1189,7 +1221,40 @@
   apply(subst k0)
   apply(simp)
   by force
+
+lemma flts_nil2:
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+            good (bsimp y) \<or> bsimp y = AZERO"
+  and "bsimp_AALTs bs (flts (map bsimp rs)) = AZERO"
+  shows "flts (map bsimp rs) = []"
+  using assms
+  apply(induct rs arbitrary: bs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(simp)
+  apply(subst (asm) k0)
+  apply(auto)
+  apply (metis flts.simps(1) flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+  by (metis flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
   
+  
+
+lemma good_SEQ:
+  assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
+  shows "good (ASEQ bs r1 r2) = (good r1 \<and> good r2)"
+  using assms
+  apply(case_tac r1)
+       apply(simp_all)
+  apply(case_tac r2)
+          apply(simp_all)
+  apply(case_tac r2)
+         apply(simp_all)
+  apply(case_tac r2)
+        apply(simp_all)
+  apply(case_tac r2)
+       apply(simp_all)
+  done
 
 lemma good1:
   shows "good (bsimp a) \<or> bsimp a = AZERO"
@@ -1211,7 +1276,7 @@
     apply(erule disjE)
      prefer 2
      apply(simp)
-   apply(frule_tac x="AALTs x51 list" in spec)
+   apply(drule_tac x="AALTs x51 list" in spec)
    apply(drule mp)
   apply(simp add: asize0)
     apply(auto)[1]
@@ -1222,22 +1287,42 @@
     apply(rule disjI1)
   apply(simp add: good0)
     apply(subst good0)
-     apply (metis Nil_is_append_conv flts1 k0)
+      apply (metis Nil_is_append_conv flts1 k0)
+  apply (metis ex_map_conv list.simps(9) nn1b nn1c)
   apply(simp)
     apply(subst k0)
     apply(simp)
     apply(auto)[1]
   using flts2 apply blast
-    apply (metis good0 in_set_member member_rec(2))
-   apply(simp) 
-   apply(rule disjI1)
-   apply(drule flts4)
-   apply(subst k0)
-   apply(subst good0)
-    apply (metis append_is_Nil_conv flts1 k0)
-   apply(auto)[1]
+    apply(subst  (asm) good0)
+      prefer 3
+      apply(auto)[1]
+     apply auto[1]
+    apply (metis ex_map_conv nn1b nn1c)
+   apply(simp)
+   apply(frule_tac x="a" in spec)
+   apply(drule mp)
+  apply(simp)
+   apply(erule disjE)
+    apply(rule disjI1)
+    apply(subst good0)
+  apply(subst k0)
+  using flts1 apply blast
+     apply(auto)[1]
+  apply (metis (no_types, hide_lams) ex_map_conv list.simps(9) nn1b nn1c)
+    apply(auto)[1]
+  apply(subst (asm) k0)
+  apply(auto)[1]
   using flts2 apply blast
-  apply (metis add.commute add_lessD1 flts_nil list.distinct(1) list.set_cases not_less_eq)
+  apply(frule_tac x="AALTs x51 list" in spec)
+   apply(drule mp)
+     apply(simp add: asize0)
+    apply(erule disjE)
+     apply(simp)
+    apply(simp)
+  apply (metis add.left_commute flts_nil2 less_add_Suc1 less_imp_Suc_add list.distinct(1) list.set_cases nat.inject)
+   apply(subst (2) k0)
+  apply(simp)
   (* SEQ case *)
   apply(simp)
   apply(case_tac "bsimp x42 = AZERO")
@@ -1252,8 +1337,19 @@
   using good_fuse apply force
    apply(subst bsimp_ASEQ1)
      apply(auto)
-  using less_add_Suc1 apply blast
-  using less_add_Suc2 by blast
+  apply(subst  good_SEQ)
+  apply(simp)
+    apply(simp)
+   apply(simp)
+  using less_add_Suc1 less_add_Suc2 by blast
+
+lemma good1a:
+  assumes "L(erase a) \<noteq> {}"
+  shows "good (bsimp a)"
+  using good1 assms
+  using L_bsimp_erase by force
+  
+
 
 lemma flts_append:
   "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
@@ -1280,7 +1376,6 @@
   apply(simp)
   by simp
 
-
 lemma flts_0:
   assumes "nonnested (AALTs bs  rs)"
   shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
@@ -1306,66 +1401,8 @@
 lemma qqq1:
   shows "AZERO \<notin> set (flts (map bsimp rs))"
   by (metis ex_map_conv flts3 good.simps(1) good1)
-  
-lemma cc:
-  assumes "bsimp (fuse bs' r) = (AALTs bs rs)" 
-  shows "\<forall>r \<in> set  rs. r \<noteq> AZERO"
-  using assms
- apply(induct r arbitrary: rs bs bs' rule: bsimp.induct)
-       apply(simp)
-  apply(case_tac "bsimp r1 = AZERO")
-    apply simp
-   apply(case_tac "bsimp r2 = AZERO")
-    apply(simp)
-    apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
-     apply(auto)[1]
-  apply (simp add: bsimp_ASEQ0)
-  apply(case_tac "\<exists>bs'. bsimp r1 = AONE bs'")
-    apply(auto)[2]
-    apply (simp add: bsimp_ASEQ2)
-  using bsimp_fuse apply fastforce
-    apply (simp add: bsimp_ASEQ1)
-   prefer 2
-      apply(simp)
-     defer
-     apply(simp)
-    apply(simp)
-   apply(simp)
-  (* AALT case *)
-  apply(simp only: fuse.simps)
-  apply(simp)
-  apply(case_tac "flts (map bsimp rs)")
-   apply(simp)
-  apply(simp)
-  apply(case_tac list)
-   apply(simp)
-   apply(case_tac a)
-        apply(simp_all)
-   apply(auto)
-   apply (metis ex_map_conv list.set_intros(1) nn1b nn1c nonalt.simps(1))
-  apply(case_tac rs)
-   apply(simp)
-  apply(simp)
-  apply(case_tac list)
-   apply(simp)  
-  oops  
 
 
-lemma ww1:
-  assumes "flts [r1] = [r2]" "r1 \<noteq> AZERO"
-  shows  "r1 = r2"
-  using assms
-  apply(case_tac r1)
-       apply(simp)
-      apply(simp)
-     apply(simp)
-    apply(simp)
-   prefer 2
-   apply(simp)
-  apply(simp)
-  apply(auto)
-  oops
-
 fun nonazero :: "arexp \<Rightarrow> bool"
   where
   "nonazero AZERO = False"
@@ -1387,213 +1424,119 @@
   apply(auto)
   done
 
+lemma flts_qq:
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y" 
+          "\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
+  shows "flts (map bsimp rs) = rs"
+  using assms
+  apply(induct rs)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(subgoal_tac "flts [bsimp a] =  [a]")
+   prefer 2
+   apply(drule_tac x="a" in spec)
+   apply(drule mp)
+    apply(simp)
+   apply(auto)[1]
+  using good.simps(1) k0b apply blast
+  apply(auto)[1]  
+  done
+  
 lemma test:
-  assumes "good  r"
-  shows "bsimp (r) = r"
+  assumes "good r"
+  shows "bsimp r = r"
+  using assms
+  apply(induct r taking: "asize" rule: measure_induct)
+  apply(erule good.elims)
+  apply(simp_all)
+  apply(subst k0)
+  apply(subst (2) k0)
+                apply(subst flts_qq)
+                  apply(auto)[1]
+                 apply(auto)[1]
+                apply (metis append_Cons append_Nil bsimp_AALTs.simps(3) good.simps(1) k0b)
+               apply force+
+  apply (metis (no_types, lifting) add_Suc add_Suc_right asize.simps(5) bsimp.simps(1) bsimp_ASEQ.simps(19) less_add_Suc1 less_add_Suc2)
+  apply (metis add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(21) good.simps(8) less_add_Suc1 less_add_Suc2)
+         apply force+
+  apply (metis (no_types, lifting) add_Suc add_Suc_right arexp.distinct(5) arexp.distinct(7) asize.simps(4) asize.simps(5) bsimp.simps(1) bsimp.simps(2) bsimp_ASEQ1 good.simps(25) good.simps(8) less_add_Suc1 less_add_Suc2)
+  apply (metis add_Suc add_Suc_right arexp.distinct(7) asize.simps(4) bsimp.simps(2) bsimp_ASEQ1 good.simps(26) good.simps(8) less_add_Suc1 less_add_Suc2)
+    apply force+
+  done
+
+lemma test2:
+  assumes "good r"
+  shows "bsimp r = r"
   using assms
-  apply(induct r)
-  apply(simp_all)
+  apply(induct r taking: "asize" rule: measure_induct)
+  apply(case_tac x)
+       apply(simp_all)
+   defer  
+  (* AALT case *)
+   apply(subgoal_tac "1 < length x52")
+    prefer 2
+    apply(case_tac x52)
+     apply(simp)
+    apply(simp)
+    apply(case_tac list)
+     apply(simp)
+  apply(simp)
+    apply(subst bsimp_AALTs_qq)
+    prefer 2
+    apply(subst flts_qq)
+      apply(auto)[1]
+     apply(auto)[1]
+   apply(case_tac x52)
+     apply(simp)
+    apply(simp)
+    apply(case_tac list)
+     apply(simp)
+      apply(simp)
+      apply(auto)[1]
+  apply (metis (no_types, lifting) bsimp_AALTs.elims good.simps(6) length_Cons length_pos_if_in_set list.size(3) nat_neq_iff)
+  apply(simp)  
+  apply(case_tac x52)
+     apply(simp)
+    apply(simp)
+    apply(case_tac list)
+     apply(simp)
+   apply(simp)
+   apply(subst k0)
+   apply(simp)
+   apply(subst (2) k0)
+   apply(simp)
+  apply (simp add: Suc_lessI flts1 one_is_add)
+  (* SEQ case *)
+  apply(case_tac "bsimp x42 = AZERO")
+   apply simp
+  apply (metis asize.elims good.simps(10) good.simps(11) good.simps(12) good.simps(2) good.simps(7) good.simps(9) good_SEQ less_add_Suc1)  
+   apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'")
+   apply(auto)[1]
+  defer
+  apply(case_tac "bsimp x43 = AZERO")
+    apply(simp)
+  apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(12) good.simps(8) good.simps(9) good_SEQ less_add_Suc2)
+  apply(auto)  
+   apply (subst bsimp_ASEQ1)
+      apply(auto)[3]
+   apply(auto)[1]
+    apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1)
+   apply (metis bsimp.simps(3) good.simps(2) good_SEQ less_add_Suc1 less_add_Suc2)
+  apply (subst bsimp_ASEQ2)
+  apply(drule_tac x="x42" in spec)
+  apply(drule mp)
+   apply(simp)
+  apply(drule mp)
+   apply (metis bsimp.elims bsimp.simps(3) good.simps(10) good.simps(11) good.simps(2) good_SEQ)
+  apply(simp)
+  done
 
 
 lemma bsimp_idem:
   shows "bsimp (bsimp r) = bsimp r"
-apply(induct r taking: "asize" rule: measure_induct)
-  apply(case_tac x)
-  apply(simp)
-      apply(simp)
-     apply(simp)
-    prefer 3
-    apply(simp)
-   apply(simp)
-   apply (simp add: bsimp_ASEQ_idem)
-  apply(clarify)
-  apply(case_tac x52)
-   apply(simp)
-  (* AALT case where rs is of the form _ # _ *)
-  apply(clarify)
-  apply(simp)
-  apply(case_tac "length (flts (bsimp a # map bsimp list)) \<le> 1")
-   prefer 2
-   apply(subst bsimp_AALTs_qq)
-    apply(auto)[1]
-   apply(simp)
-   apply(subst k0)
-   apply(simp)
-   apply(simp add: flts_append)
-   apply(subst (2) k0)
-   apply(subst (asm) k0)
-   apply(simp)
-   apply(subgoal_tac "good (bsimp a) \<or> bsimp a = AZERO")
-    prefer 2
-  using good1 apply blast
-   apply(erule disjE)
-    prefer 2
-    apply(simp)
-    apply(drule_tac x="AALTs x51 list" in spec)
-    apply(drule mp)
-  apply(simp add: asize0)
-    apply(simp)
-    apply (simp add: bsimp_AALTs_qq)
-   apply(case_tac "nonalt (bsimp a)")
-  apply(subst flts_single1)
-      apply(simp)
-  using nonazero.elims(3) apply force
-    apply(simp)
-  apply(subst k0b)
-      apply(simp)
-     apply(auto)[1]
-  apply(subst k0b)
-      apply(simp)
-     apply(auto)[1]
-    apply(simp)
-  (* HERE *)
-    apply(subst (asm) flts_single1)
-      apply(simp)
-     apply(simp)
-  using nonazero.elims(3) apply force
-    apply(simp)
-  apply(subst (2) bsimp_AALTs_qq)
-     apply(auto)[1]
-  apply(subst bsimp_AALTs_qq)
-     apply(auto)[1]
-     apply(case_tac list)
-      apply(simp)
-  apply(simp)
-
-   prefer 2
-  apply(subgoal_tac "length (flts (bsimp a # map bsimp list)) = 0 \<or> 
-                     length (flts (bsimp a # map bsimp list)) = 1")
-    prefer 2
-    apply(auto)[1]
-  using le_SucE apply blast
-  apply(erule disjE)
-    apply(simp)
-   apply(simp)
-   apply(subst k0)
-   apply(subst (2)  k0)
-   apply(subst (asm) k0)
-   apply(simp)
-  apply(subgoal_tac "length (flts [bsimp a]) = 1 \<or> 
-                     length (flts (map bsimp list)) = 1")
-    prefer 2
-  apply linarith
-    apply(erule disjE)
-    apply(simp)
-    prefer 2
-    apply(simp)
-    apply(drule_tac x="AALTs x51 list" in  spec)
-    apply(drule mp)
-     apply(simp)
-  using asize0 apply blast
-    apply(simp)
-   apply(frule_tac x="a" in spec)
-  apply(drule mp)
-    apply(simp)
-   apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]")
-    prefer 2
-  apply (simp add: length_Suc_conv)
-   apply(clarify)
-   apply(simp only: )
-  apply(case_tac "bsimp a = AZERO")
-    apply simp
-  apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs")
-    apply(clarify)
-    apply(simp)
-  apply(drule_tac x="AALTs bs rs" in spec)
-  apply(drule mp)
-     apply(simp)
-  apply (metis asize.simps(4) bsimp_size lessI less_le_trans trans_less_add1)
-    apply(simp)
-  
-    apply(subst ww)
-   apply(subst ww)
-   apply(frule_tac x="fuse x51 r" in spec)
-  apply(drule mp)
-    apply(simp)
-  apply (smt add.commute add_le_cancel_right fuse_size le_add2 le_trans list.map(1) list.simps(9) not_less not_less_eq rt sum_list.Cons)
-   apply(case_tac "bsimp a = AZERO")
-    apply simp
-  apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs")
-    apply(clarify)
-  
-   defer
-  
-  apply(
-   apply(case_tac a)
-  apply(simp_all)
-   apply(subgoal_tac "\<exists>r. flts [bsimp a] = [r]")
-    prefer 2
-  apply (simp add: length_Suc_conv)
-   apply auto[1]
-  apply(case_tac 
-  apply(clarify)
-  
-  defer
-    apply(auto)[1]
-
-
-  apply(subst k0)
-  apply(subst (2) k0)
-  apply(case_tac "bsimp a = AZERO")
-   apply(simp)
-   apply(frule_tac x="AALTs x51 (flts (map bsimp list))" in spec)
-   apply(drule mp)
-    apply(simp)
-  apply (meson add_le_cancel_right asize0 le_trans not_le rt trans_le_add2)
-  apply(simp)
-    apply(subst (asm) flts_idem)
-     apply(auto)[1]
-     apply(drule_tac  x="r" in spec)
-  apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
-  apply(simp)
-  apply(subst flts_idem)
-   apply(auto)[1]
-     apply(drule_tac  x="r" in spec)
-  apply (metis add.commute add_lessD1 not_add_less1 not_less_eq sum_list_map_remove1)
-   apply(simp)
-  apply(case_tac "nonalt (bsimp a)")
-  apply(subst k0b)
-     apply(simp)
-    apply(simp)
-  apply(subst k0b)
-     apply(simp)
-    apply(simp)
-   apply(auto)[1]
-  apply(frule_tac x="AALTs x51 (bsimp a # flts (map bsimp list))" in spec)
-   apply(drule mp)
-    apply(simp)
-    prefer 2
-    apply(simp)
-  apply(subst (asm) k0)
-  apply(subst (asm) flts_idem)
-     apply(auto)[1]
-  apply (simp add: sum_list_map_remove1)
-  apply(subst (asm) k0b)
-     apply(simp)
-    apply(simp)
-    apply(simp)
-   apply(subst k0)
-  apply(subst flts_idem)
-     apply(auto)[1]
-     apply (simp add: sum_list_map_remove1)
-  apply(subst k0b)
-     apply(simp)
-    apply(simp)
-  apply(simp)
-lemma XX_bder:
-  shows "bsimp (bder c (bsimp r)) = (bsimp \<circ> bder c) r"
-  apply(induct r)
-       apply(simp)
-      apply(simp)
-     apply(simp)
-    prefer 3
-    apply(simp)
-  prefer 2
-   apply(simp)
-   apply(case_tac x2a)
-    apply(simp)
-  apply(simp)
-  apply(auto)[1]
+  using test good1
+  by force
 
 
 lemma q3a:
@@ -1760,360 +1703,6 @@
    apply(simp_all)
   done
 
-
-fun extr :: "arexp  \<Rightarrow> (bit list) set" where
-  "extr (AONE bs) = {bs}"
-| "extr (ACHAR bs c) = {bs}"
-| "extr (AALTs bs (r#rs)) = 
-     {bs @ bs' | bs'.  bs' \<in> extr r} \<union>
-     {bs @ bs' | bs'.  bs' \<in> extr (AALTs [] rs)}"
-| "extr (ASEQ bs r1 r2) = 
-     {bs @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r1 \<and> bs2 \<in> extr r2}"
-| "extr (ASTAR bs r) = {bs @ [S]} \<union>
-     {bs @ [Z] @ bs1 @ bs2 | bs1 bs2. bs1 \<in> extr r \<and> bs2 \<in> extr (ASTAR  [] r)}"
-
-
-lemma MAIN_decode:
-  assumes "\<Turnstile> v : ders s r"
-  shows "Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r"
-  using assms
-proof (induct s arbitrary: v rule: rev_induct)
-  case Nil
-  have "\<Turnstile> v : ders [] r" by fact
-  then have "\<Turnstile> v : r" by simp
-  then have "Some v = decode (retrieve (intern r) v) r"
-    using decode_code retrieve_code by auto
-  then show "Some (flex r id [] v) = decode (retrieve (bders_simp (intern r) []) v) r"
-    by simp
-next
-  case (snoc c s v)
-  have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> 
-     Some (flex r id s v) = decode (retrieve (bders_simp (intern r) s) v) r" by fact
-  have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact
-  then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" 
-    by(simp add: Prf_injval ders_append)
-  have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))"
-    by (simp add: flex_append)
-  also have "... = decode (retrieve (bders_simp (intern r) s) (injval (ders s r) c v)) r"
-    using asm2 IH by simp
-  also have "... = decode (retrieve (bder c (bders_simp (intern r) s)) v) r"
-    using asm bder_retrieve ders_append 
-    apply -
-    apply(drule_tac x="v" in meta_spec)
-    apply(drule_tac x="c" in meta_spec)
-    apply(drule_tac x="bders_simp (intern r) s" in meta_spec)
-    apply(drule_tac  meta_mp)
-     apply(simp add: ders_append)
-     defer
-    apply(simp)
-    oops
-
-fun vsimp :: "arexp \<Rightarrow> val \<Rightarrow> val"
-  where
-  "vsimp (ASEQ _ (AONE _) r) (Seq v1 v2) = vsimp r v1"
-| "vsimp _ v = v" 
-
-lemma fuse_vsimp:
-  assumes "\<Turnstile> v : (erase r)"
-  shows "vsimp (fuse bs r) v = vsimp r v"
-  using assms
-  apply(induct r arbitrary: v bs)
-       apply(simp_all)
-  apply(case_tac "\<exists>bs. r1 = AONE bs")
-   apply(auto)
-   apply (metis Prf_elims(2) vsimp.simps(1))
-  apply(erule Prf_elims)
-  apply(auto)
-  apply(case_tac r1)
-       apply(auto)
-  done  
-  
-
-lemma retrieve_XXX0:
-  assumes "\<And>r v. \<lbrakk>r \<in> set rs; \<Turnstile> v : erase r\<rbrakk> \<Longrightarrow> 
-              \<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v"
-          "\<Turnstile> v : erase (AALTs bs rs)"
-        shows "\<exists>v'. \<Turnstile> v' : erase (bsimp_AALTs bs (flts (map bsimp rs))) \<and>
-                retrieve (bsimp_AALTs bs (flts (map bsimp rs))) v' = retrieve (AALTs bs rs) v"
-  using assms
-apply(induct rs arbitrary: bs v taking: size rule: measure_induct)
-  apply(case_tac x)
-   apply(simp)
-  using Prf_elims(1) apply blast
-  apply(simp)
-  apply(case_tac list)
-   apply(simp_all)
-   apply(case_tac a)
-  apply(simp_all)
-  using Prf_elims(1) apply blast
-       apply (metis erase.simps(2) fuse.simps(2) retrieve_fuse2)
-  using Prf_elims(5) apply force
-     apply(erule Prf_elims)
-     apply(auto)[1]
-  
-  
-  
-
-  apply(simp)
-       apply(erule Prf_elims)
-  using Prf_elims(1) apply b last
-       apply(auto)
-       apply (metis append_Ni l2 erase_fuse fuse.simps(4) retrieve_fuse2)
-  apply(case_tac rs)
-       apply(auto)
-
-  
-  oops
-
-fun get where
-  "get (Some v) = v"
-
-  
-lemma retrieve_XXX:
-  assumes "\<Turnstile> v : erase r" 
-  shows "\<Turnstile> get (decode (code v) (erase (bsimp r))) : erase (bsimp r)"
-  using assms
-apply(induct r arbitrary: v)
-       apply(simp)
-  using Prf_elims(1) apply auto[1]  
-      apply(simp)
-  apply (simp add: decode_code)
-     apply(simp)
-  apply (simp add: decode_code)
-    apply(simp)
-    apply(erule Prf_elims)
-  apply(simp)
-   apply(case_tac  "r1 = AZERO")
-     apply(simp)
-  apply (meson Prf_elims(1) Prf_elims(2))
-  apply(case_tac  "r2 = AZERO")
-     apply(simp)
-     apply (meson Prf_elims(1) Prf_elims(2))
-   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
-     apply(clarify)
-     apply(simp)
-     apply(subst bsimp_ASEQ2)
-     apply(subst bsimp_ASEQ2)
-     apply(simp add: erase_fuse)
-     apply(case_tac r1)
-          apply(simp_all)
-  using Prf_elims(4) apply fastforce
-      apply(erule Prf_elims)
-      apply(simp)
-  
-      apply(simp)
-  
-  
-     defer
-     apply(subst bsimp_ASEQ1)
-  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fast force
-  using L_bsimp_erase L_
-
-lemma retrieve_XXX:
-  assumes "\<Turnstile> v : erase r" 
-  shows "\<Turnstile> (vsimp (bsimp r) v : erase (bsimp r)  \<and> retrieve (bsimp r) (vsimp (bsimp r) v) = retrieve r v"
-  using assms
-  apply(induct r arbitrary: v)
-       apply(simp)
-  using Prf_elims(1) apply blast
-      apply(simp)
-  using Prf_elims(4) apply fastforce
-    apply(simp)
-  apply blast
-  apply simp
-   apply(case_tac  "r1 = AZERO")
-     apply(simp)
-  apply (meson Prf_elims(1) Prf_elims(2))
-  apply(case_tac  "r2 = AZERO")
-     apply(simp)
-     apply (meson Prf_elims(1) Prf_elims(2))
-  apply(erule Prf_elims)
-  apply(simp)
-   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
-     apply(clarify)
-     apply(simp)
-    apply(subst bsimp_ASEQ2)
-     defer
-     apply(subst bsimp_ASEQ1)
-  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
-  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
-      apply(simp)
-    apply(simp)
-  apply(drule_tac  x="v1" in meta_spec)
-  apply(drule_tac  x="v2" in meta_spec)
-     apply(simp)
-  apply(clarify)
-     apply(rule_tac x="Seq v' v'a" in exI)
-     apply(simp)
-  apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6))
-    prefer 3
-  apply(drule_tac  x="v1" in meta_spec)
-  apply(drule_tac  x="v2" in meta_spec)
-     apply(simp)
-    apply(clarify)
-    apply(rule_tac x="v'a" in exI)
-    apply(subst bsimp_ASEQ2)
-    apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2)
-   prefer 2  
-   apply(auto)
-  apply(case_tac "x2a")
-   apply(simp)
-  using Prf_elims(1) apply blast
-  apply(simp)
-  apply(case_tac "list")
-   apply(simp)
-  sorry  
-
-
-lemma retrieve_XXX:
-  assumes "\<Turnstile> v : erase r" 
-  shows "\<exists>v'. \<Turnstile> v' : erase (bsimp r)  \<and> retrieve (bsimp r) v' = retrieve r v"
-  using assms
-  apply(induct r arbitrary: v)
-       apply(simp)
-  using Prf_elims(1) apply blast
-      apply(simp)
-  using Prf_elims(4) apply fastforce
-    apply(simp)
-  apply blast
-  apply simp
-   apply(case_tac  "r1 = AZERO")
-     apply(simp)
-  apply (meson Prf_elims(1) Prf_elims(2))
-  apply(case_tac  "r2 = AZERO")
-     apply(simp)
-     apply (meson Prf_elims(1) Prf_elims(2))
-  apply(erule Prf_elims)
-  apply(simp)
-   apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
-     apply(clarify)
-     apply(simp)
-    apply(subst bsimp_ASEQ2)
-     defer
-     apply(subst bsimp_ASEQ1)
-  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
-  using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce
-      apply(simp)
-    apply(simp)
-  apply(drule_tac  x="v1" in meta_spec)
-  apply(drule_tac  x="v2" in meta_spec)
-     apply(simp)
-  apply(clarify)
-     apply(rule_tac x="Seq v' v'a" in exI)
-     apply(simp)
-  apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6))
-    prefer 3
-  apply(drule_tac  x="v1" in meta_spec)
-  apply(drule_tac  x="v2" in meta_spec)
-     apply(simp)
-    apply(clarify)
-    apply(rule_tac x="v'a" in exI)
-    apply(subst bsimp_ASEQ2)
-    apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2)
-   prefer 2  
-   apply(auto)
-  apply(case_tac "x2a")
-   apply(simp)
-  using Prf_elims(1) apply blast
-  apply(simp)
-  apply(case_tac "list")
-   apply(simp)
-  sorry
-
-
-lemma TEST:
-  assumes "\<Turnstile> v : ders s r"
-  shows "\<exists>v'. retrieve (bders (intern r) s) v' = retrieve (bsimp (bders (intern r) s)) v"
-  using assms
-  apply(induct s arbitrary: r v rule: rev_induct)
-   apply(simp)
-  
-   defer
-   apply(simp add: ders_append)
-   apply(frule Prf_injval)
-  apply(drule_tac x="r" in meta_spec)
-   apply(drule_tac x="injval (ders xs r) x v" in meta_spec)
-   apply(simp)
-   apply(simp add: bders_append)
-   apply(subst bder_retrieve)
-    apply(simp)
-   apply(simp)
-  thm bder_retrieve
-  thm bmkeps_retrieve
-
-
-lemma bmkeps_simp2:
-  assumes "bnullable (bder c r)"
-  shows "bmkeps (bder c (bsimp r)) = bmkeps (bder c r)"
-  using  assms
-  apply(induct r)
-       apply(simp)
-      apply(simp)
-     apply(simp)
-  prefer 3
-    apply(simp)
-   apply(simp)
-   apply(auto)[1]
-     prefer 2
-     apply(case_tac "r1 = AZERO")
-      apply(simp)
-   apply(case_tac "r2 = AZERO")
-      apply(simp)
-     apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs")
-      apply(clarify)
-      apply(simp)
-      apply(subst bsimp_ASEQ2)
-  
-   apply(simp add: bmkeps_simp)
-  apply(simp add: bders_append)
-  apply(drule_tac x="bder a r" in meta_spec)
-       apply(simp)
-      apply(simp)
-     apply(simp)
-    prefer 3
-    apply(simp)
-   prefer 2
-   apply(simp)
-   apply(case_tac x2a)
-    apply(simp)
-  apply(simp add: )
-  apply(subst k0)
-   apply(auto)[1]
-    apply(case_tac list)
-     apply(simp)
-  
-
-   apply(case_tac  "r1=AZERO")
-    apply(simp)
-   apply(case_tac  "r2=AZERO")
-    apply(simp)
-    apply(auto)[1]
-   apply(case_tac  "\<exists>bs. r1=AONE bs")
-  apply(simp)
-    apply(auto)[1]
-     apply(subst bsimp_ASEQ2)
-
-  
-   prefer 2
-   apply(simp)
-  apply(subst  bmkeps_bder_AALTs)
-   apply(case_tac x2a)
-    apply(simp)
-   apply(simp)
-   apply(auto)[1]
-    apply(subst  bmkeps_bder_AALTs)
-  
-   apply(case_tac a)
-  apply(simp_all)
-   apply(auto)[1]
-    apply(case_tac list)
-         apply(simp)
-        apply(simp)
-  
-     prefer 2
-  apply(simp)
-
-
 lemma bbs0:
   shows "blexer_simp r [] = blexer r []"
   apply(simp add: blexer_def blexer_simp_def)
@@ -2130,341 +1719,12 @@
    apply(simp)
   apply(simp)
   done
-  
-lemma bbs1:
-  shows "blexer_simp r [c1, c2] = blexer r [c1, c2]"
-  apply(simp add: blexer_def blexer_simp_def)
-  apply(auto)
-    defer
-  apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))
-  apply (metis L_bsimp_erase bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))
-  apply(subst bmkeps_simp[symmetric])
-  using b3 apply auto[1]
-  apply(subst bmkeps_retrieve)
-  using b3 bnullable_correctness apply blast
-  apply(subst bder_retrieve)
-  using b3 bnullable_correctness mkeps_nullable apply fastforce
-  apply(subst bmkeps_retrieve)
-  using bnullable_correctness apply blast
-  apply(subst bder_retrieve)
-  using bnullable_correctness mkeps_nullable apply force
-  
-  using bder_retrieve bmkeps_simp bmkeps_retrieve
-
-  
-
-lemma bsimp_retrieve_bder:
-  assumes "\<Turnstile> v : der c (erase r)"
-  shows "retrieve (bder c r) v = retrieve (bsimp (bder c r)) v"
-  thm bder_retrieve bmkeps_simp
-  apply(induct  r arbitrary: c v)
-       apply(simp)
-      apply(simp)
-     apply(simp)
-    apply(auto)[1]
-     apply(case_tac "bsimp (bder c r1) = AZERO")
-      apply(simp)
-  
-    prefer 3
-    apply(simp)
-  apply(auto elim!: Prf_elims)[1]
-    apply(case_tac "(bsimp (fuse [Z] (bder c r))) = AZERO")
-     apply(simp)
-     apply (met is L_bsimp_erase L_flat_Prf1 L_flat_Prf2 Prf_elims(1) erase.simps(1) erase_bder erase_fuse)
-    apply(case_tac "\<exists>bs. bsimp (fuse [Z] (bder c r)) = AONE bs")
-     apply(clarify)
-     apply(subgoal_tac "L (der c (erase r)) = {[]}")
-      prefer 2
-      apply (metis L.simps(2) L_bsimp_erase erase.simps(2) erase_bder erase_fuse)
-     apply(simp)
-  
-  
-  
-    apply(subst bsimp_ASEQ1)
-       apply(simp)
-      apply(simp)
-  apply(auto)[1]
-  
-     prefer 2
-  
 
 lemma oo:
   shows "(case (blexer (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer r (c # s)"
   apply(simp add: blexer_correctness)
   done
 
-lemma oo2a:
-  assumes "\<forall>r. bmkeps (bders_simp r s) = bmkeps (bders r s)" "c # s \<in> L r"
-          "bnullable (bders_simp (bsimp (bder c (intern r))) s)"
-  shows "(case (blexer_simp (der c r) s) of None \<Rightarrow> None | Some v \<Rightarrow> Some (injval r c v)) = blexer_simp r (c # s)"
-  using assms
-  apply(simp add: blexer_simp_def)
-  apply(auto  split: option.split)
-    apply (metis blexer_correctness blexer_def lexer.simps(2) lexer_correct_None option.simps(4))
-   prefer 2
-  apply (metis L_bders_simp L_bsimp_erase Posix1(1) Posix_mkeps bnullable_correctness ders_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None)
-  apply(subst bmkeps_retrieve)
-  using L_bders_simp bnullable_correctness nullable_correctness apply blast
-  
-  thm bder_retrieve
-  
-  
-  apply(subst bder_retrieve[symmetric])
-  
-  
-
-  apply(drule_tac x="bsimp (bder c (intern r))" in  spec)
-  apply(drule sym)
-   apply(simp)
-   apply(subst blexer_simp_def)
-  apply(case_tac "bnullable (bders_simp (intern (der c r)) s)")
-   apply(simp)
-  apply(auto split: option.split)
-  apply(subst oo)
-  apply(simp)
-  done
-
-
-
-lemma oo3:
-  assumes "\<forall>r. bders r s = bders_simp r s"
-  shows "blexer_simp r (s @ [c]) = blexer r (s @ [c])"
-  using assms
-  apply(simp (no_asm) add: blexer_simp_def)
-  apply(auto)
-   prefer 2
-  apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
-  apply(simp add: bders_simp_append)
-  apply(subst bmkeps_simp[symmetric])
-  using b3 apply auto[1]
-  apply(simp add: blexer_def)
-  apply(auto)[1]
-   prefer 2
-  apply (metis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1))
-  apply(simp add: bders_append)     
-  done
-
-lemma oo4:
-  assumes "\<forall>r. bmkeps (bders r s) = bmkeps (bders_simp r s)" "bnullable (bder c (bders r s))"
-  shows "bmkeps (bders_simp r (s @ [c])) = bmkeps (bders r (s @ [c]))"
-  using assms
-  apply(simp add: bders_simp_append)
-  apply(subst bmkeps_simp[symmetric])
-  apply (metis L_bders_simp bnullable_correctness der_correctness erase_bder lexer.simps(1) lexer_correct_None option.distinct(1))
-  apply(simp add: bders_append)
-  done
-
-lemma oo4:
-  shows "blexer_simp r s = blexer r s"
-  apply(induct s arbitrary: r rule: rev_induct)
-   apply(simp only: blexer_simp_def blexer_def)
-   apply(simp)
-  apply(simp only: blexer_simp_def blexer_def)
-  apply(subgoal_tac "bnullable (bders_simp (intern r) (xs @ [x])) = bnullable (bders (intern r) (xs @ [x]))")
-   prefer 2
-   apply (simp add: b4)
-  apply(simp)
-  apply(rule impI)
-  apply(simp add: bders_simp_append)
-  apply(subst bmkeps_simp[symmetric])
-  using b3 apply auto[1]
-  apply(subst bmkeps_retrieve)
-  using b3 bnullable_correctness apply blast
-  apply(subst bder_retrieve)
-  using b3 bnullable_correctness mkeps_nullable apply fastforce
-  apply(simp add: bders_append)
-  apply(subst bmkeps_retrieve)
-  using bnullable_correctness apply blast
-  apply(subst bder_retrieve)
-  using bnullable_correctness mkeps_nullable apply fastforce
-  apply(subst erase_bder)
-  apply(case_tac "xs \<in> L")
-  apply(subst (asm) (2) bmkeps_retrieve)
-  
-  
-  thm bmkeps_retrieve bmkeps_retrieve
-  apply(subst bmkeps_retrieve[symmetric])
-  
-   apply (simp add: bnullable_correctness)
-  apply(simp add: bders_simp_append)
-   
-  
-  apply(induct s arbitrary: r rule: rev_induct) 
-   apply(simp add: blexer_def blexer_simp_def)
-  apply(rule oo3)
-  apply(simp (no_asm) add: blexer_simp_def)
-  apply(auto)
-   prefer 2
-  apply (metis L_bders_simp blexer_def bnullable_correctness lexer.simps(1) lexer_correct_None option.distinct(1))
-  apply(simp add: bders_simp_append)
-  apply(subst bmkeps_simp[symmetric])
-  using b3 apply auto[1]
-  apply(simp add: blexer_def)
-  apply(auto)[1]
-   prefer 2
-  apply (m etis (mono_tags, lifting) L_bders_simp Posix_mkeps append.right_neutral bders_simp.simps(1) bders_simp.simps(2) bders_simp_append bnullable_correctness lexer.simps(1) lexer_correct_None lexer_correctness(1) option.distinct(1))
-  apply(simp add: bders_append)     
-  oops
-
-
-lemma bnullable_simp:
-  assumes "s \<in> L (erase r)"
-  shows "bmkeps (bders r s) = bmkeps (bders_simp r s)"
-  using assms
-  apply(induct s arbitrary: r rule: rev_induct)
-   apply(simp)
-  apply(simp add: bders_append bders_simp_append)
-  apply(subst bmkeps_simp[symmetric])
-  apply (metis L_bders_simp b3 bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correct_Some lexer_correctness(1))
-  apply(subst bmkeps_retrieve)
-  apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer_correct_Some option.distinct(1))
-  apply(subst bmkeps_retrieve)
-  apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2))
-  apply(subst bder_retrieve)
-  apply (metis bders.simps(1) bders.simps(2) bders_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer_correct_Some mkeps_nullable option.distinct(1))
-  apply(subst bder_retrieve)
-  apply (metis L_bders_simp L_bsimp_erase Posix_mkeps bders_simp.simps(1) bders_simp.simps(2) bders_simp_append blexer_correctness blexer_def bnullable_correctness erase_bder erase_bders erase_intern lexer.simps(1) lexer_correct_None lexer_correctness(2) mkeps_nullable)
-    
-  apply(drule_tac x="bder a r" in meta_spec)
-  apply(drule_tac  meta_mp)
-  apply (me tis erase_bder lexer.simps(2) lexer_correct_None option.simps(4))
-  apply(simp)
-  oops
-
-
-lemma
-  shows "blexer r s = blexer_simp r s"
-  apply(induct s arbitrary: r rule: rev_induct)
-   apply(simp add: blexer_def blexer_simp_def)
-  apply(case_tac "xs @ [x] \<in> L r")
-   defer
-   apply(subgoal_tac "blexer (ders xs r) [x] = None")
-    prefer 2
-    apply(subst blexer_correctness)
-    apply(simp (no_asm) add: lexer_correct_None)
-    apply(simp add: nullable_correctness)
-    apply(simp add: der_correctness ders_correctness)
-  apply(simp add: Der_def Ders_def)
-apply(subgoal_tac "blexer r (xs @ [x]) = None")
-    prefer 2
-    apply (simp add: blexer_correctness)
-  using lexer_correct_None apply auto[1]
-  apply(simp)
-   apply(subgoal_tac "blexer_simp (ders xs r) [x] = None")
-    prefer 2
-  apply (metis L_bders_simp Posix_injval Posix_mkeps bders.simps(2) blexer_correctness blexer_simp_def bnullable_correctness ders.simps(1) erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2))
-   apply(subgoal_tac "[] \<notin> L (erase (bders_simp (intern r) (xs @ [x])))")
-  prefer 2
-  apply(metis L_bders_simp Posix_injval bders.simps(2) blexer_correctness ders.simps(1) ders_append erase_bder erase_bders erase_intern lexer_correct_None lexer_correctness(2))
-  using blexer_simp_def bnullable_correctness lexer_correct_None apply auto[1]
-(* case xs @ [x] \<in> L r *)
-  apply(subgoal_tac "\<exists>v. blexer (ders xs r) [x] = Some v \<and> [x] \<in> (ders xs r) \<rightarrow> v")
-   prefer 2  
-  using blexer_correctness lexer_correct_Some apply auto[1]
-    apply (simp add: Posix_injval Posix_mkeps)
-  apply (metis ders.simps(1) ders.simps(2) ders_append lexer_correct_None lexer_flex)    
-  apply(clarify)
-  apply(subgoal_tac "blexer_simp (ders xs r) [x] = Some v")
-   prefer 2
-   apply(simp add: blexer_simp_def)
-   apply(auto)[1]
-    apply (metis bders.simps(1) bders.simps(2) blexer_def bmkeps_simp option.simps(3))
-  using b3 blexer_def apply fastforce
-  apply(subgoal_tac "blexer_simp (ders xs r) [x] = blexer_simp r (xs @ [x])")
-   prefer 2
-   apply(simp add: blexer_simp_def)
-  
-   apply(simp)
-  
-  
-  
-   apply(simp)
-  apply(subst blexer_simp_def)
-  apply(simp)
-  apply(auto)
-  apply(drule_tac x="der a r" in meta_spec)
-  apply(subst blexer_def)
-   apply(subgoal_tac "bnullable (bders (intern r) (a # s))")
-    prefer 2
-    apply (me tis Posix_injval blexer_correctness blexer_def lexer_correctness(2))
-  apply(simp)
-  
-
-
-lemma
-  shows "blexer r s = blexer_simp r s"
-  apply(induct s arbitrary: r)
-   apply(simp add: blexer_def blexer_simp_def)
-  apply(case_tac "s \<in> L (der a r)")
-   defer
-   apply(subgoal_tac "blexer (der a r) s = None")
-    prefer 2
-    apply (simp add: blexer_correctness lexer_correct_None)
-apply(subgoal_tac "blexer r (a # s) = None")
-    prefer 2
-    apply (simp add: blexer_correctness)
-   apply(simp)
-  
-   apply(subst blexer_simp_def)
-   apply(simp)
-  apply(drule_tac  x="der a r" in  meta_spec)
-   apply(subgoal_tac "s \<notin> L(erase (bder a (intern  r)))")
-  prefer 2
-    apply simp
-   
-   apply(simp only:)
-   apply(subst blexer_simp_def)
-   apply(subgoal_tac "\<not> bnullable (bders_simp (intern r) (a # s))")
-    apply(simp)
-   apply(subst bnullable_correctness[symmetric])
-  apply(simp)
-  oops
-
-
-lemma flts_bsimp:
-  "flts (map bsimp rs) = map bsimp (flts rs)"
-apply(induct rs taking: size rule: measure_induct)
-  apply(case_tac x)
-   apply(simp)
-  apply(simp)
-  apply(induct rs rule: flts.induct)
-        apply(simp)
-       apply(simp)
-      defer
-      apply(simp)
-     apply(simp)
-    defer
-    apply(simp)
-  apply(subst List.list.map(2))
-   apply(simp only: flts.simps)
-   apply(subst k0)
-   apply(subst map_append)
-   apply(simp only:)
-   apply(simp del: bsimp.simps)
-   apply(case_tac rs1)
-    apply(simp)
-   apply(simp)
-  apply(case_tac list)
-    apply(simp_all)
-  thm map
-  apply(subst map.simps)
-        apply(auto)
-   defer
-  apply(case_tac "(bsimp va) = AZERO")
-    apply(simp)
-  
-  using b3 apply for ce
-   apply(case_tac "(bsimp a2) = AZERO")
-     apply(simp)
-  apply (me tis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1))
-    apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs")
-     apply(clarify)
-     apply(simp)
-  
-
-lemma XXX:
-  shows "bsimp (bsimp a) = bsimp a"
-  sorry
 
 lemma bder_fuse:
   shows "bder c (fuse bs a) = fuse bs  (bder c a)"
@@ -2472,134 +1732,428 @@
        apply(simp_all)
   done
 
-lemma XXX2:
+lemma XXX2_helper:
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y" 
+          "\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
+  shows "flts (map (bsimp \<circ> bder c) (flts (map bsimp rs))) = flts (map (bsimp \<circ> bder c) rs)"
+  using assms
+  apply(induct rs arbitrary: c)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(simp add: flts_append)
+  apply(subst (2) k0)
+  apply(simp add: flts_append)
+  apply(subgoal_tac "flts [a] =  [a]")
+   prefer 2
+  using good.simps(1) k0b apply blast
+  apply(simp)
+  done
+
+lemma bmkeps_good:
+  assumes "good a"
+  shows "bmkeps (bsimp a) = bmkeps a"
+  using assms
+  using test2 by auto
+
+
+lemma xxx_bder:
+  assumes "good r"
+  shows "L (erase r) \<noteq> {}"
+  using assms
+  apply(induct r rule: good.induct)
+  apply(auto simp add: Sequ_def)
+  done
+
+lemma xxx_bder2:
+  assumes "L (erase (bsimp r)) = {}"
+  shows "bsimp r = AZERO"
+  using assms xxx_bder test2 good1
+  by blast
+
+lemma XXX2aa:
+  assumes "good a"
   shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
-  apply(induct a arbitrary: c)
+  using  assms
+  by (simp add: test2)
+
+lemma XXX2aa_ders:
+  assumes "good a"
+  shows "bsimp (bders (bsimp a) s) = bsimp (bders a s)"
+  using  assms
+  by (simp add: test2)
+
+lemma XXX4a:
+  shows "good (bders_simp (bsimp r) s)  \<or> bders_simp (bsimp r) s = AZERO"
+  apply(induct s arbitrary: r rule:  rev_induct)
+   apply(simp)
+  apply (simp add: good1)
+  apply(simp add: bders_simp_append)
+  apply (simp add: good1)
+  done
+
+lemma XXX4a_good:
+  assumes "good a"
+  shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
+  using assms
+  apply(induct s arbitrary: a rule:  rev_induct)
+   apply(simp)
+  apply(simp add: bders_simp_append)
+  apply (simp add: good1)
+  done
+
+lemma XXX4a_good_cons:
+  assumes "s \<noteq> []"
+  shows "good (bders_simp a s) \<or> bders_simp a s = AZERO"
+  using assms
+  apply(case_tac s)
+   apply(auto)
+  using XXX4a by blast
+
+lemma XXX4b:
+  assumes "good a" "L (erase (bders_simp a s)) \<noteq> {}"
+  shows "good (bders_simp a s)"
+  using assms
+  apply(induct s arbitrary: a)
+   apply(simp)
+  apply(simp)
+  apply(subgoal_tac "L (erase (bder a aa)) = {} \<or> L (erase (bder a aa)) \<noteq> {}")
+   prefer 2
+   apply(auto)[1]
+  apply(erule disjE)
+   apply(subgoal_tac "bsimp (bder a aa) = AZERO")
+    prefer 2
+  using L_bsimp_erase xxx_bder2 apply auto[1]
+   apply(simp)
+  apply (metis L.simps(1) XXX4a erase.simps(1))  
+  apply(drule_tac x="bsimp (bder a aa)" in meta_spec)
+  apply(drule meta_mp)
+  apply simp
+  apply(rule good1a)
+  apply(auto)
+  done
+
+lemma bders_AZERO:
+  shows "bders AZERO s = AZERO"
+  and   "bders_simp AZERO s = AZERO"
+   apply (induct s)
+     apply(auto)
+  done
+
+lemma ZZ0:
+  assumes "bsimp a = AALTs bs rs"
+  shows "bsimp (bder c a) = AALTs bs (map (bder c) rs)"
+  using assms
+  apply(induct a arbitrary: rs bs c)
+       apply(simp_all)
+   apply(auto)[1]
+    prefer 2
+    apply (metis arexp.distinct(25) arexp.distinct(7) b3 bnullable.simps(2) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1)
+   prefer 2
+  oops
+  
+
+lemma ZZZ:
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> bsimp (bder c (bsimp y)) = bsimp (bder c y)"
+  shows "bsimp (bder c (bsimp_AALTs x51 (flts (map bsimp x52)))) = bsimp_AALTs x51 (flts (map (bsimp \<circ> bder c) x52))"
+  using assms
+  apply(induct x52)
+   apply(simp)
+  apply(simp)
+  apply(case_tac "bsimp a = AZERO")
+   apply(simp)
+   apply(subgoal_tac "bsimp (bder c a) = AZERO")
+    prefer 2
+  using less_add_Suc1 apply fastforce
+   apply(simp)
+  apply(case_tac "\<exists>bs rs. bsimp a = AALTs bs rs")
+   apply(clarify)
+   apply(simp)
+   apply(subst k0)
+   apply(case_tac "rs = []")
+  apply(simp)
+   apply(subgoal_tac "bsimp (bder c a) = AALTs bs []")
+     apply(simp)
+  apply (metis arexp.distinct(7) good.simps(4) good1)
+  oops
+  
+
+
+
+lemma bders_snoc:
+  "bder c (bders a s) = bders a (s @ [c])"
+  apply(simp add: bders_append)
+  done
+
+lemma
+  assumes "bnullable (bders a s)" "good a"
+  shows "bmkeps (bders_simp a s) = bmkeps (bders a s)"
+  using assms
+  apply(induct s arbitrary: a)
+   apply(simp)
+  apply(simp add: bders_append bders_simp_append)
+  apply(drule_tac x="bsimp (bsimp (bder a aa))" in meta_spec)
+  apply(drule meta_mp)
+  apply (metis b4 bders.simps(2) bders_simp.simps(2) bsimp_idem)
+  apply(subgoal_tac "good (bsimp (bder a aa)) \<or> bsimp (bder a aa) = AZERO")
+   apply(auto simp add: bders_AZERO)
+    prefer 2
+    apply (metis b4 bders.simps(2) bders_AZERO(2) bders_simp.simps(2) bnullable.simps(1))
+   prefer 2
+  using good1 apply auto[1]
+  apply(drule meta_mp)
+   apply (simp add: bsimp_idem)
+  apply (subst (asm) (1) bsimp_idem)
+  apply(simp)
+  apply(subst (asm) (2) bmkeps_simp)
+   apply (metis b4 bders.simps(2) bders_simp.simps(2) bsimp_idem)
+  apply (subst (asm) (1) bsimp_idem)
+  apply(simp) 
+   defer
+  oops
+
+
+lemma
+  shows "bmkeps (bders (bders_simp a s2) s1) = bmkeps (bders_simp a (s2 @ s1))"
+  apply(induct s2 arbitrary: a s1)
+   apply(simp)
+  defer
+  apply(simp add: bders_append bders_simp_append)
+  oops
+
+lemma QQ1:
+  shows "bsimp (bders (bsimp a) []) = bders_simp (bsimp a) []"
+  apply(simp)
+  apply(simp add: bsimp_idem)
+  done
+
+lemma QQ2:
+  shows "bsimp (bders (bsimp a) [c]) = bders_simp (bsimp a) [c]"
+  apply(simp)
+  done
+
+lemma QQ3:
+  assumes "good a"
+  shows "bmkeps (bsimp (bders (bsimp a) [c1, c2])) = bmkeps (bders_simp (bsimp a) [c1, c2])"
+  using assms
+  apply(simp)
+  
+  oops
+
+lemma QQ4:
+  shows "bmkeps (bsimp (bders (bsimp a) [c1, c2, c3])) = bmkeps (bders_simp (bsimp a) [c1, c2, c3])"
+  apply(simp)
+  oops
+
+lemma QQ3:
+  assumes "good a"
+  shows "bsimp (bders (bders_simp a s2) s1)= bders_simp a (s1 @ s2)"
+  using assms
+  apply(induct s2 arbitrary: a s1)
+   apply(simp)
+  oops
+
+lemma XXX2a_long:
+  assumes "good a"
+  shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+  using  assms
+  apply(induct a arbitrary: c taking: asize rule: measure_induct)
+  apply(case_tac x)
        apply(simp)
       apply(simp)
      apply(simp)
   prefer 3
     apply(simp)
+   apply(simp)
    apply(auto)[1]
-   apply(case_tac "(bsimp a1) = AZERO")
+apply(case_tac "x42 = AZERO")
+     apply(simp)
+   apply(case_tac "x43 = AZERO")
      apply(simp)
+  using test2 apply force  
+  apply(case_tac "\<exists>bs. x42 = AONE bs")
+     apply(clarify)
+     apply(simp)
+    apply(subst bsimp_ASEQ1)
+       apply(simp)
   using b3 apply force
-   apply(case_tac "(bsimp a2) = AZERO")
+  using bsimp_ASEQ0 test2 apply force
+  thm good_SEQ test2
+     apply (simp add: good_SEQ test2)
+    apply (simp add: good_SEQ test2)
+  apply(case_tac "x42 = AZERO")
      apply(simp)
-  apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_ASEQ0 bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1))
-    apply(case_tac "\<exists>bs. (bsimp a1) = AONE bs")
+   apply(case_tac "x43 = AZERO")
+    apply(simp)
+  apply (simp add: bsimp_ASEQ0)
+  apply(case_tac "\<exists>bs. x42 = AONE bs")
      apply(clarify)
      apply(simp)
-  apply(subst bsimp_ASEQ2)  
-     apply(subgoal_tac "bmkeps a1 = bs")
+    apply(subst bsimp_ASEQ1)
+      apply(simp)
+  using bsimp_ASEQ0 test2 apply force
+     apply (simp add: good_SEQ test2)
+    apply (simp add: good_SEQ test2)
+  apply (simp add: good_SEQ test2)
+  (* AALTs case *)
+  apply(simp)
+  using test2 by fastforce
+
+lemma XXX2a_long_without_good:
+  shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+  apply(induct a arbitrary: c taking: asize rule: measure_induct)
+  apply(case_tac x)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+  prefer 3
+    apply(simp)
+   apply(simp)
+   apply(auto)[1]
+apply(case_tac "x42 = AZERO")
+     apply(simp)
+   apply(case_tac "bsimp x43 = AZERO")
+     apply(simp)
+     apply (simp add: bsimp_ASEQ0)
+     apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO")
+      apply(simp)
+  apply (metis bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2)
+  apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
+     apply(clarify)
+     apply(simp)
+     apply(subst bsimp_ASEQ2)
+     apply(subgoal_tac "bsimp (bder c x42) = AZERO")
+      apply(simp)
+  prefer 2
+  using less_add_Suc1 apply fastforce
+     apply(subgoal_tac "bmkeps x42 = bs")
       prefer 2
       apply (simp add: bmkeps_simp)
      apply(simp)
-  apply(subst (1) bsimp_fuse[symmetric])
-     defer
-  apply(subst bsimp_ASEQ1)  
+     apply(case_tac "nonalt (bsimp (bder c x43))")
+  apply (metis bder_fuse bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) fuse_append k0b less_add_Suc2 nn11a)
+     apply(subgoal_tac "nonnested (bsimp (bder c x43))")
+      prefer 2
+  using nn1b apply blast
+     apply(case_tac x43)
+          apply(simp)
+         apply(simp)
+        apply(simp)
+       prefer 3
+       apply(simp)
+       apply (metis arexp.distinct(25) arexp.distinct(7) arexp.distinct(9) bsimp_ASEQ.simps(1) bsimp_ASEQ.simps(11) bsimp_ASEQ1 nn11a nonalt.elims(3) nonalt.simps(6)) 
+      apply(simp)
+      apply(auto)[1]
+       apply(case_tac "(bsimp (bder c x42a)) = AZERO")
         apply(simp)
+  
        apply(simp)
+  
+  
+  
+     apply(subgoal_tac "(\<exists>bs1 rs1. 1 < length rs1 \<and> bsimp (bder c x43) =  AALTs bs1 rs1 ) \<or>
+                        (\<exists>bs1 r. bsimp (bder c x43) =  fuse bs1 r)")
+      prefer 2
+  apply (metis fuse_empty)
+     apply(erule disjE)
+  prefer 2
+     apply(clarify)
+     apply(simp only:)
+     apply(simp)
+     apply(simp add: fuse_append)
+     apply(subst bder_fuse)
+     apply(subst bsimp_fuse[symmetric])
+     apply(subst bder_fuse)
+     apply(subst bsimp_fuse[symmetric])
+     apply(subgoal_tac "bsimp (bder c (bsimp x43)) = bsimp (bder c x43)")
+      prefer 2
+  using less_add_Suc2 apply blast
+     apply(simp only: )
+     apply(subst bsimp_fuse[symmetric])
+      apply(simp only: )
+  
+     apply(simp only: fuse.simps)
   apply(simp)
+      apply(case_tac rs1)
+      apply(simp)
+      apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(4) good1 good_fuse)
+  apply(simp)
+  apply(case_tac list)
+      apply(simp)
+      apply (metis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse)
+     apply(simp only: bsimp_AALTs.simps map_cons.simps)
      apply(auto)[1]
-      apply (metis XXX bmkeps_simp bsimp_fuse)
-  using b3 apply blast
-  apply (smt XXX b3 bder.simps(1) bder.simps(5) bnullable.simps(2) bsimp.simps(1) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1)
-   apply(simp)
-   prefer 2
-   apply(subst bder_fuse)
-  apply(subst bsimp_fuse[symmetric])
-   apply(simp)
-  sorry
+  
+  
+      
+      apply(subst bsimp_fuse[symmetric])
+  apply(subgoal_tac "bmkeps x42 = bs")
+      prefer 2
+      apply (simp add: bmkeps_simp)
+  
+  
+        apply(simp)
+  
+  using b3 apply force
+  using bsimp_ASEQ0 test2 apply force
+  thm good_SEQ test2
+     apply (simp add: good_SEQ test2)
+    apply (simp add: good_SEQ test2)
+  apply(case_tac "x42 = AZERO")
+     apply(simp)
+   apply(case_tac "x43 = AZERO")
+    apply(simp)
+  apply (simp add: bsimp_ASEQ0)
+  apply(case_tac "\<exists>bs. x42 = AONE bs")
+     apply(clarify)
+     apply(simp)
+    apply(subst bsimp_ASEQ1)
+      apply(simp)
+  using bsimp_ASEQ0 test2 apply force
+     apply (simp add: good_SEQ test2)
+    apply (simp add: good_SEQ test2)
+  apply (simp add: good_SEQ test2)
+  (* AALTs case *)
+  apply(simp)
+  using test2 by fastforce
 
 
-thm bsimp_AALTs.simps
-thm bsimp.simps
-thm flts.simps
-
-lemma XXX3:
-  "bsimp (bders (bsimp r) s) = bsimp (bders r s)"
+lemma XXX4ab:
+  shows "good (bders_simp (bsimp r) s)  \<or> bders_simp (bsimp r) s = AZERO"
   apply(induct s arbitrary: r rule:  rev_induct)
    apply(simp)
-   apply (simp add: XXX)
-  apply(simp add: bders_append)
-  apply(subst (2) XXX2[symmetric])
-  apply(subst XXX2[symmetric])
-  apply(drule_tac x="r" in meta_spec)
-  apply(simp)
+  apply (simp add: good1)
+  apply(simp add: bders_simp_append)
+  apply (simp add: good1)
   done
 
 lemma XXX4:
- "bders_simp (bsimp r) s = bsimp (bders r s)"
-  apply(induct s arbitrary: r)
-   apply(simp)
-  apply(simp)
-  by (metis XXX2)
-  
-  
-lemma
-  assumes "bnullable (bder c r)"  "bnullable (bder c (bsimp r))"
-  shows "bmkeps (bder c r) = bmkeps (bder c (bsimp r))"
- using  assms
-  apply(induct r arbitrary: c)
-      apply(simp)
-     apply(simp)
-    apply(simp)
-  prefer 3
+  assumes "good a"
+  shows "bders_simp a s = bsimp (bders a s)"
+  using  assms
+  apply(induct s arbitrary: a rule: rev_induct)
    apply(simp)
-  apply(auto)[1]
-    apply(case_tac "(bsimp r1) = AZERO")
-     apply(simp)
-   apply(case_tac "(bsimp r2) = AZERO")
-     apply(simp)
-  apply (simp add: bsimp_ASEQ0)
-    apply(case_tac "\<exists>bs. (bsimp r1) = AONE bs")
-     apply(clarify)
-     apply(simp)
-     apply(subgoal_tac "bnullable r1")
-      prefer 2
-  using b3 apply force
-      apply(simp)
-  apply(simp add: bsimp_ASEQ2) 
-      prefer 2
-  
-  
-  
-  apply(subst bsimp_ASEQ2)
-  
-  
-  
-  
+   apply (simp add: test2)
+  apply(simp add: bders_append bders_simp_append)
+  oops
 
 
-lemma
-  assumes  "bnullable (bders a (s1 @ s2))" "bnullable (bders (bsimp (bders a s1)) s2)"
-  shows "bmkeps (bders a (s1 @ s2)) = bmkeps (bders (bsimp (bders a s1)) s2)"
-  using  assms
-  apply(induct s2 arbitrary: a s1)
+lemma MAINMAIN:
+  "blexer r s = blexer_simp r s"
+  apply(induct s arbitrary: r)
+  apply(simp add: blexer_def blexer_simp_def)
+  apply(simp add: blexer_def blexer_simp_def del: bders.simps bders_simp.simps)
+  apply(auto simp del: bders.simps bders_simp.simps)
+    prefer 2
+  apply (metis b4 bders.simps(2) bders_simp.simps(2))
+   prefer 2
+  apply (metis b4 bders.simps(2))
+  apply(subst bmkeps_simp)
    apply(simp)
-  using bmkeps_simp apply blast
-  apply(simp add: bders_append)
-  apply(drule_tac x="aa" in meta_spec)
-  apply(drule_tac x="s1 @ [a]" in meta_spec)
-  apply(drule meta_mp)
-   apply(simp add: bders_append)
-  apply(simp add: bders_append)
-  apply(drule meta_mp)
-   apply (metis b4 bders.simps(2) bders_simp.simps(2))
+  apply(case_tac s)
+   apply(simp only: bders.simps)
+   apply(subst bders_simp.simps)
   apply(simp)
-  
-   apply (met is b4 bders.simps(2) bders_simp.simps(2))
-  
-  
-  
-  using b3 apply blast
-  using b3 apply auto[1]
-  apply(auto simp add: blex_def)
-    prefer 3
-  
-  
-  
-
+    
 
 end
\ No newline at end of file