# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1560209202 -3600
# Node ID 2a128087215fb72f318fc1297fae2ef6c3416609
# Parent  d9d4146325d96f7f97ee364eacff3116ae3a1ce1
updated

diff -r d9d4146325d9 -r 2a128087215f Literature/evil-regs-study-javascript.pdf
Binary file Literature/evil-regs-study-javascript.pdf has changed
diff -r d9d4146325d9 -r 2a128087215f exps/bit-test.scala
--- a/exps/bit-test.scala	Thu May 23 13:30:09 2019 +0100
+++ b/exps/bit-test.scala	Tue Jun 11 00:26:42 2019 +0100
@@ -674,7 +674,7 @@
 //tests derivatives and bsimp
 
 def tests_ders_bsimp(ss: Set[String])(r: Rexp) = {
-  val a = internalise(r)
+  val a = fuse(List(Z,Z,S), internalise(r))
   for (s <- ss.par) yield {  
     val d1 = bsimp(bders(s.toList, bsimp(a)))
     val d2 = bsimp(bders(s.toList, a))
@@ -688,7 +688,7 @@
 
 println("Partial searching: ")
 enum(2, "abc").map(tests_ders_bsimp(strs(1, "abc"))).
-  flatten.toSet.flatten.minBy(a => asize(a._1))
+  flatten.toSet.flatten
 
 // tests about good
 def good(a: ARexp) : Boolean = a match {
diff -r d9d4146325d9 -r 2a128087215f thys/BitCoded.thy
--- a/thys/BitCoded.thy	Thu May 23 13:30:09 2019 +0100
+++ b/thys/BitCoded.thy	Tue Jun 11 00:26:42 2019 +0100
@@ -623,7 +623,7 @@
   shows "sum_list (map asize (flts rs)) \<le> sum_list (map asize rs)"
   apply(induct rs rule: flts.induct)
         apply(simp_all)
-  by (metis (mono_tags, lifting) add_mono_thms_linordered_semiring(1) comp_apply fuse_size le_SucI order_refl sum_list_cong)
+  by (metis (mono_tags, lifting) add_mono comp_apply eq_imp_le fuse_size le_SucI map_eq_conv)
   
 
 lemma bsimp_AALTs_size:
@@ -650,11 +650,6 @@
   apply(induct rs)
    apply(auto)
   by (simp add: add_mono bsimp_size)
-  
-
-
-
-
 
 lemma bsimp_AALTs_size2:
   assumes "\<forall>r \<in> set  rs. nonalt r"
@@ -664,6 +659,7 @@
     apply(simp_all add: fuse_size)
   done
 
+
 lemma qq:
   shows "map (asize \<circ> fuse bs) rs = map asize rs"
   apply(induct rs)
@@ -682,7 +678,26 @@
    prefer 2
    apply (simp add: flts_size le_imp_less_Suc)
   using less_Suc_eq by auto
-  
+
+lemma bsimp_AALTs_size3:
+  assumes "\<exists>r \<in> set  (map bsimp rs). \<not>nonalt r"
+  shows "asize (bsimp (AALTs bs rs)) < asize (AALTs bs rs)"
+  using assms flts_size2
+  apply  -
+  apply(clarify)
+  apply(simp)
+  apply(drule_tac x="map bsimp rs" in meta_spec)
+  apply(drule meta_mp)
+  apply (metis list.set_map nonalt.elims(3))
+  apply(simp)
+  apply(rule order_class.order.strict_trans1)
+   apply(rule bsimp_AALTs_size)
+  apply(simp)
+  by (smt Suc_leI bsimp_asize0 comp_def le_imp_less_Suc le_trans map_eq_conv not_less_eq)
+
+
+
+
 lemma L_bsimp_ASEQ:
   "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))"
   apply(induct bs r1 r2 rule: bsimp_ASEQ.induct)
@@ -929,16 +944,6 @@
   apply(simp)
   done
 
-fun spill where
- "spill (AALTs bs rs) =  map (fuse bs) rs"
-
-lemma  k0a2:
-  assumes "\<not> nonalt r"  
-  shows "flts [r] = spill r"
-  using  assms
-  apply(case_tac r)
-  apply(simp_all)
-  done
 
 lemma  k0b:
   assumes "nonalt r" "r \<noteq> AZERO"
@@ -1081,6 +1086,26 @@
    apply(simp_all)
   done
 
+
+lemma bsimp_AALTs1:
+  assumes "nonalt r"
+  shows "bsimp_AALTs bs (flts [r]) = fuse bs r"
+  using  assms
+  apply(case_tac r)
+   apply(simp_all)
+  done
+
+lemma bbbbs:
+  assumes "good r" "r = AALTs bs1 rs"
+  shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"
+  using  assms
+  by (metis (no_types, lifting) Nil_is_map_conv append.left_neutral append_butlast_last_id bsimp_AALTs.elims butlast.simps(2) good.simps(4) good.simps(5) k0a map_butlast)
+
+lemma bbbbs1:
+  shows "nonalt r \<or> (\<exists>bs rs. r  = AALTs bs rs)"
+  using nonalt.elims(3) by auto
+  
+
 lemma good_fuse:
   shows "good (fuse bs r) = good r"
   apply(induct r arbitrary: bs)
@@ -1678,6 +1703,7 @@
   apply (smt b3 bnullable.elims(2) bsimp_ASEQ.simps(17) bsimp_ASEQ.simps(19) bsimp_ASEQ.simps(20) bsimp_ASEQ.simps(21) bsimp_ASEQ.simps(22) bsimp_ASEQ.simps(24) bsimp_ASEQ.simps(25) bsimp_ASEQ.simps(26) bsimp_ASEQ.simps(27) bsimp_ASEQ.simps(29) bsimp_ASEQ.simps(30) bsimp_ASEQ.simps(31))
    apply(simp)
   apply(simp)
+  thm q3
   apply(subst q3[symmetric])
    apply simp
   using b3 qq4 apply auto[1]
@@ -1840,18 +1866,6 @@
      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)"
@@ -1908,8 +1922,6 @@
   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
 
 
@@ -1932,27 +1944,6 @@
   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)"
@@ -2000,16 +1991,452 @@
   using test2 by fastforce
 
 lemma XXX2a_long_without_good:
+  assumes "a = AALTs bs0  [AALTs bs1 [AALTs bs2 [ASTAR [] (AONE bs7), AONE bs6, ASEQ bs3 (ACHAR bs4 d) (AONE bs5)]]]" 
   shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
-  apply(induct a arbitrary: c taking: asize rule: measure_induct)
+        "bsimp (bder c (bsimp a)) = XXX"
+        "bsimp (bder c a) = YYY"
+  using  assms
+    apply(simp)
+  using  assms
+   apply(simp)
+   prefer 2
+  using  assms
+   apply(simp)
+  oops
+
+lemma bder_bsimp_AALTs:
+  shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
+  apply(induct bs rs rule: bsimp_AALTs.induct)
+    apply(simp)
+   apply(simp)
+   apply (simp add: bder_fuse)
+  apply(simp)
+  done
+
+lemma flts_nothing:
+  assumes "\<forall>r \<in> set rs. r \<noteq> AZERO" "\<forall>r \<in> set rs. nonalt r"
+  shows "flts rs = rs"
+  using assms
+  apply(induct rs rule: flts.induct)
+        apply(auto)
+  done
+
+lemma flts_flts:
+  assumes "\<forall>r \<in> set rs. good r"
+  shows "flts (flts rs) = flts rs"
+  using assms
+  apply(induct rs taking: "\<lambda>rs. sum_list  (map asize rs)" rule: measure_induct)
+  apply(case_tac x)
+   apply(simp)
+  apply(simp)
+  apply(case_tac a)
+       apply(simp_all  add: bder_fuse flts_append)
+  apply(subgoal_tac "\<forall>r \<in> set x52. r \<noteq> AZERO")
+   prefer 2
+  apply (metis Nil_is_append_conv bsimp_AALTs.elims good.simps(1) good.simps(5) good0 list.distinct(1) n0 nn1b split_list_last test2)
+  apply(subgoal_tac "\<forall>r \<in> set x52. nonalt r")
+   prefer 2
+   apply (metis n0 nn1b test2)
+  by (metis flts_fuse flts_nothing)
+
+lemma "good (bsimp a) \<or> bsimp a = AZERO"
+  by (simp add: good1)
+
+
+lemma 
+  assumes "bnullable (bders r s)" "good r"
+  shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)"
+  using assms
+  apply(induct s arbitrary: r)
+   apply(simp)
+  using bmkeps_simp apply auto[1]
+  apply(simp)
+  by (simp add: test2)
+
+lemma PP:
+  assumes "bnullable (bders r s)" 
+  shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)"
+  using assms
+  apply(induct s arbitrary: r)
+   apply(simp)
+  using bmkeps_simp apply auto[1]
+  apply(simp add: bders_append bders_simp_append)
+  oops
+
+lemma PP:
+  assumes "bnullable (bders r s)"
+  shows "bmkeps (bders_simp (bsimp r) s) = bmkeps (bders r s)"
+  using assms
+  apply(induct s arbitrary: r rule: rev_induct)
+   apply(simp)
+  using bmkeps_simp apply auto[1]
+  apply(simp add: bders_append bders_simp_append)
+  apply(drule_tac x="bder a (bsimp r)" in meta_spec)
+  apply(drule_tac meta_mp)
+   defer
+  oops
+
+
+lemma
+  assumes "asize (bsimp a) = asize a"  "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]"
+  shows "bsimp a = a"
+  using assms
+  apply(simp)
+  oops
+
+
+lemma iii:
+  assumes "bsimp_AALTs bs rs \<noteq> AZERO"
+  shows "rs \<noteq> []"
+  using assms
+  apply(induct bs  rs rule: bsimp_AALTs.induct)
+    apply(auto)
+  done
+
+lemma
+  assumes "\<forall>y. asize y < Suc (sum_list (map asize x52)) \<longrightarrow> asize (bsimp y) = asize y \<longrightarrow> bsimp y \<noteq> AZERO \<longrightarrow> bsimp y = y"
+   "asize (bsimp_AALTs x51 (flts (map bsimp x52))) = Suc (sum_list (map asize x52))" 
+          "bsimp_AALTs x51 (flts (map bsimp x52)) \<noteq> AZERO"
+   shows "bsimp_AALTs x51 (flts (map bsimp x52)) = AALTs x51 x52"
+  using assms
+  apply(induct x52 arbitrary: x51)
+   apply(simp)
+  
+  
+
+lemma
+  assumes "asize (bsimp a) = asize a" "bsimp a \<noteq> AZERO"
+  shows "bsimp a = a"
+  using assms
+  apply(induct a taking: asize rule: measure_induct)
+  apply(case_tac x)
+       apply(simp_all)
+   apply(case_tac "(bsimp x42) = AZERO")
+    apply(simp add: asize0)
+  apply(case_tac "(bsimp x43) = AZERO")
+    apply(simp add: asize0)
+    apply (metis bsimp_ASEQ0)
+   apply(case_tac "\<exists>bs. (bsimp x42) = AONE bs")
+    apply(auto)[1]
+    apply (metis b1 bsimp_size fuse_size less_add_Suc2 not_less)
+  apply (metis Suc_inject add.commute asize.simps(5) bsimp_ASEQ1 bsimp_size leD le_neq_implies_less less_add_Suc2 less_add_eq_less)
+  (* ALT case *)
+  apply(frule iii)
+  apply(case_tac x52)
+   apply(simp)
+  apply(simp)
+  apply(subst k0)
+  apply(subst (asm) k0)
+  apply(subst (asm) (2) k0)
+  apply(subst (asm) (3) k0)
+  apply(case_tac "(bsimp a) = AZERO")
+   apply(simp)
+  apply (metis (no_types, lifting) Suc_le_lessD asize0 bsimp_AALTs_size le_less_trans less_add_same_cancel2 not_less_eq rt)
+  apply(simp)
+  apply(case_tac "nonalt  (bsimp a)")
+   prefer 2
+  apply(drule_tac  x="AALTs x51 (bsimp a # list)" in  spec)
+   apply(drule mp)
+  apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
+   apply(drule mp)  
+    apply(simp)
+  apply (metis asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k0 lessI list.set_intros(1) list.simps(9) not_less_eq sum_list.Cons)
+   apply(drule mp)
+  apply(simp)
+  using bsimp_idem apply auto[1]
+    apply(simp add: bsimp_idem)
+  apply (metis append.left_neutral append_Cons asize.simps(4) bsimp.simps(2) bsimp_AALTs_size3 k00 less_not_refl list.set_intros(1) list.simps(9) sum_list.Cons)
+  apply (metis bsimp.simps(2) bsimp_idem k0 list.simps(9) nn1b nonalt.elims(3) nonnested.simps(2))
+  apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
+  prefer 2
+  using k0b apply blast
+  apply(clarify)
+  apply(simp only:)
+  apply(simp)
+  apply(case_tac "flts (map bsimp list) = Nil")
+   apply (metis bsimp_AALTs1 bsimp_size fuse_size less_add_Suc1 not_less) 
+  apply (subgoal_tac "bsimp_AALTs x51 (bsimp a # flts (map bsimp list)) =  AALTs x51 (bsimp a # flts (map bsimp list))")
+   prefer 2
+   apply (metis bsimp_AALTs.simps(3) neq_Nil_conv)
+  apply(auto)
+   apply (metis add.commute bsimp_size leD le_neq_implies_less less_add_Suc1 less_add_eq_less rt)
+   
+  apply(drule_tac x="AALTs x51 list" in spec)
+  apply(drule mp)
+   apply(auto simp add: asize0)[1]
+ 
+
+
+(* HERE*)
+
+
+
+
+
+lemma OOO:
+  shows "bsimp (bsimp_AALTs bs rs) = bsimp_AALTs bs (flts (map bsimp rs))"
+  apply(induct rs arbitrary: bs taking: "\<lambda>rs. sum_list (map asize rs)" rule: measure_induct)
+  apply(case_tac x)
+   apply(simp)
+  apply(simp)
+  apply(case_tac "a = AZERO")
+   apply(simp)
+  apply(case_tac "list")
+    apply(simp)
+  apply(simp)
+  apply(case_tac "bsimp a = AZERO")
+   apply(simp)
+  apply(case_tac "list")
+    apply(simp)
+    apply(simp add: bsimp_fuse[symmetric])
+  apply(simp)
+  apply(case_tac "nonalt (bsimp a)")
+  apply(case_tac list)
+  apply(simp)
+    apply(subst k0b)
+      apply(simp)
+     apply(simp)
+    apply(simp add: bsimp_fuse)
+   apply(simp)
+  apply(subgoal_tac "asize (bsimp a) < asize a \<or> asize (bsimp a) = asize a")
+   prefer 2
+  using bsimp_size le_neq_implies_less apply blast
+   apply(erule disjE)
+  apply(drule_tac x="(bsimp a) # list" in spec)
+  apply(drule mp)
+    apply(simp)
+   apply(simp)
+  apply (metis bsimp.simps(2) bsimp_AALTs.elims bsimp_AALTs.simps(2) bsimp_fuse bsimp_idem list.distinct(1) list.inject list.simps(9))
+    apply(subgoal_tac "\<exists>bs rs. bsimp a = AALTs bs rs  \<and> rs \<noteq> Nil \<and> length rs > 1")
+   prefer 2
+  apply (metis bbbbs1 bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) good.simps(5) good1 length_0_conv length_Suc_conv less_one list.simps(8) nat_neq_iff not_less_eq)
+  apply(auto)
+  sledgehammer [timeout=6000]  
+
+
+
+
+  defer
+  apply(case_tac  list)
+    apply(simp)
+    prefer 2
+    apply(simp)
+   apply (simp add: bsimp_fuse bsimp_idem)
+  apply(case_tac a)
+       apply(simp_all)
+  
+  
+  apply(subst k0b)
+      apply(simp)
+    apply(subst (asm) k0)
+  apply(subst (asm) (2) k0)
+
+
+  find_theorems "asize _ < asize _"
+  using bsimp_AALTs_size3
+  apply -
+  apply(drule_tac x="a # list" in meta_spec)
+  apply(drule_tac x="bs" in meta_spec)
+  apply(drule meta_mp)
+   apply(simp)
+  apply(simp)
+  apply(drule_tac x="(bsimp a) # list" in spec)
+  apply(drule mp)
+   apply(simp)
+  apply(case_tac  list)
+    apply(simp)
+    prefer 2
+    apply(simp)
+    apply(subst (asm) k0)
+  apply(subst (asm) (2) k0)
+  thm k0
+  apply(subst (asm) k0b)
+      apply(simp)
+     apply(simp)
+  
+   defer
+   apply(simp)
+   apply(case_tac  list)
+    apply(simp)
+    defer
+    apply(simp)
+  find_theorems "asize _ < asize _"
+  find_theorems "asize _ < asize _"
+apply(subst k0b)
+      apply(simp)
+     apply(simp)
+
+
+      apply(rule nn11a)
+      apply(simp)
+     apply (metis good.simps(1) good1 good_fuse)
+    apply(simp)
+  using fuse_append apply blast
+   apply(subgoal_tac "\<exists>bs rs. bsimp x43 = AALTs bs rs")
+    prefer 2
+  using nonalt.elims(3) apply blast
+   apply(clarify)
+   apply(simp)
+   apply(case_tac rs)
+    apply(simp)
+    apply (metis arexp.distinct(7) good.simps(4) good1)
+   apply(simp)
+  apply(case_tac list)
+    apply(simp)
+    apply (metis arexp.distinct(7) good.simps(5) good1)
+  apply(simp)
+  
+  
+  
+  
+  
+  
+  find_theorems "flts [_] = [_]"
+   apply(case_tac x52)
+  apply(simp)
+   apply(simp)
+  apply(case_tac list)
+    apply(simp)
+    apply(case_tac a)
+  apply(simp_all)
+  
+
+lemma XXX2a_long_without_good:
+  shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
+  apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
   apply(case_tac x)
        apply(simp)
       apply(simp)
      apply(simp)
   prefer 3
     apply(simp)
+  (* AALT case *)
+  prefer 2
+   apply(simp only:)
    apply(simp)
-   apply(auto)[1]
+   apply(subst bder_bsimp_AALTs)
+   apply(case_tac x52)
+    apply(simp)
+   apply(simp)
+   apply(case_tac list)
+  apply(simp)
+
+   apply(case_tac "\<exists>r \<in> set (map bsimp x52). \<not>nonalt r")
+    apply(drule_tac x="bsimp (AALTs x51 x52)" in spec)
+    apply(drule mp)
+  using bsimp_AALTs_size3 apply blast
+    apply(drule_tac x="c" in spec)
+  apply(subst (asm) (2) test)
+  
+   apply(case_tac x52)
+    apply(simp)
+   apply(simp)
+  apply(case_tac "bsimp a = AZERO")
+     apply(simp)
+     apply(subgoal_tac "bsimp (bder c a) = AZERO")
+      prefer 2
+     apply auto[1]
+  apply (metis L.simps(1) L_bsimp_erase der.simps(1) der_correctness erase.simps(1) erase_bder xxx_bder2)
+    apply(simp)
+    apply(drule_tac x="AALTs x51 list" in spec)
+    apply(drule mp)
+     apply(simp add: asize0)
+  apply(simp)
+   apply(case_tac list)
+    prefer 2
+    apply(simp)
+  apply(case_tac "bsimp aa = AZERO")
+     apply(simp)
+     apply(subgoal_tac "bsimp (bder c aa) = AZERO")
+      prefer 2
+      apply auto[1]
+      apply (metis add.left_commute bder.simps(1) bsimp.simps(3) less_add_Suc1)
+     apply(simp)
+  apply(drule_tac x="AALTs x51 (a#lista)" in spec)
+    apply(drule mp)
+     apply(simp  add: asize0)
+     apply(simp)
+     apply (metis flts.simps(2) k0)
+    apply(subst k0)
+  apply(subst (2) k0)
+  
+  
+  using less_add_Suc1 apply fastforce
+    apply(subst k0)
+  
+
+    apply(simp)
+    apply(case_tac "bsimp a = AZERO")
+     apply(simp)
+     apply(subgoal_tac "bsimp (bder c a) = AZERO")
+      prefer 2
+  apply auto[1]
+     apply(simp)
+  apply(case_tac "nonalt (bsimp a)")
+     apply(subst bsimp_AALTs1)
+      apply(simp)
+  using less_add_Suc1 apply fastforce
+  
+     apply(subst bsimp_AALTs1)
+  
+  using nn11a apply b last
+
+  (* SEQ case *)
+   apply(clarify)
+  apply(subst  bsimp.simps)
+   apply(simp del: bsimp.simps)
+   apply(auto simp del: bsimp.simps)[1]
+    apply(subgoal_tac "bsimp x42 \<noteq> AZERO")
+  prefer 2
+  using b3 apply force
+  apply(case_tac "bsimp x43 = AZERO")
+     apply(simp)
+     apply (simp add: bsimp_ASEQ0)
+  apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_fuse flts.simps(1) flts.simps(2) 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")
+      prefer 2
+  using less_add_Suc1 apply fastforce
+     apply(simp)
+     apply(frule_tac x="x43" in spec)
+  apply(drule mp)
+     apply(simp)
+  apply(drule_tac x="c" in spec)
+     apply(subst bder_fuse)
+  apply(subst bsimp_fuse[symmetric])
+     apply(simp)
+  apply(subgoal_tac "bmkeps x42 = bs")
+      prefer 2
+      apply (simp add: bmkeps_simp)
+     apply(simp)
+     apply(subst bsimp_fuse[symmetric])
+  apply(case_tac "nonalt (bsimp (bder c x43))")
+      apply(subst bsimp_AALTs1)
+  using nn11a apply blast
+  using fuse_append apply blast
+     apply(subgoal_tac "\<exists>bs rs. bsimp (bder c x43) = AALTs bs rs")
+      prefer 2
+  using bbbbs1 apply blast
+  apply(clarify)
+     apply(simp)
+     apply(case_tac rs)
+      apply(simp)
+      apply (metis arexp.distinct(7) good.simps(4) good1)
+     apply(simp)
+     apply(case_tac list)
+      apply(simp)
+      apply (metis arexp.distinct(7) good.simps(5) good1)
+  apply(simp del: bsimp_AALTs.simps)
+  apply(simp only: bsimp_AALTs.simps)
+     apply(simp)
+  
+  
+
+
+(* HERE *)
 apply(case_tac "x42 = AZERO")
      apply(simp)
    apply(case_tac "bsimp x43 = AZERO")
@@ -2017,7 +2444,7 @@
      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 (met is 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)
@@ -2067,7 +2494,7 @@
      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
+  using less_add_Suc2 apply bl ast
      apply(simp only: )
      apply(subst bsimp_fuse[symmetric])
       apply(simp only: )
@@ -2080,7 +2507,7 @@
   apply(simp)
   apply(case_tac list)
       apply(simp)
-      apply (metis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse)
+      apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse)
      apply(simp only: bsimp_AALTs.simps map_cons.simps)
      apply(auto)[1]
   
@@ -2095,7 +2522,7 @@
         apply(simp)
   
   using b3 apply force
-  using bsimp_ASEQ0 test2 apply force
+  using bsimp_ASEQ0 test2 apply fo rce
   thm good_SEQ test2
      apply (simp add: good_SEQ test2)
     apply (simp add: good_SEQ test2)
@@ -2109,13 +2536,13 @@
      apply(simp)
     apply(subst bsimp_ASEQ1)
       apply(simp)
-  using bsimp_ASEQ0 test2 apply force
+  using bsimp_ASEQ0 test2 apply fo rce
      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
+  using test2 by fa st force
 
 
 lemma XXX4ab: