--- a/thys/BitCoded.thy	Mon Jul 29 14:27:17 2019 +0100
+++ b/thys/BitCoded.thy	Mon Jul 29 16:54:56 2019 +0100
@@ -2630,6 +2630,16 @@
   by (metis bsimp_fuse flts_fuse k0 list.simps(9))
   
 
+lemma flts_nonalt:
+  assumes "flts (map bsimp xs) = ys"
+  shows "\<forall>y \<in> set ys. nonalt y"
+  using assms
+  apply(induct xs arbitrary: ys)
+   apply(auto)
+  apply(case_tac xs)
+   apply(auto)
+  using flts2 good1 apply fastforce
+  by (smt ex_map_conv list.simps(9) nn1b nn1c)
 
 lemma big0:
   assumes as1p: "\<exists>as1'. map (fuse bs1) as1 = as1'" 
@@ -2664,7 +2674,26 @@
     apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2) [a]")
      prefer 2
   using YY apply blast
-     apply(simp)
+    apply(simp)
+    apply(subgoal_tac "nonalt a")
+     prefer 2
+     apply (simp add: flts_nonalt)
+    apply(subgoal_tac "nonalt (fuse bs2 a)")
+     prefer 2
+  using nn11a apply blast
+    apply (metis bsimp.simps(2) bsimp_AALTs.simps(2) bsimp_AALTs1 bsimp_idem)
+   apply(simp only:)
+   apply(subgoal_tac "bsimp_AALTs bs2 (a # aa # lista) = AALTs bs2 (a # aa # lista)")
+    prefer 2
+  using bsimp_AALTs.simps(3) apply blast
+   apply(simp only:)
+  apply(subgoal_tac "flts (map bsimp as2') = map (fuse bs2)(a # aa # lista) ")
+  prefer 2
+  using YY apply blast
+   apply(simp only:)
+    apply(subst (1) bsimp_idem[symmetric])
+   apply(simp)
+  apply (metis arexp.distinct(7) bbbbs bsimp.simps(2) bsimp_AALTs.simps(3) bsimp_idem good1 list.simps(9) map_map)
   (* HERE TODAY *)