diff -r 0b5444f429da -r e29812ea4427 thys/BitCoded2.thy
--- a/thys/BitCoded2.thy	Sat Sep 07 14:47:06 2019 +0100
+++ b/thys/BitCoded2.thy	Mon Sep 09 09:37:33 2019 +0100
@@ -3593,10 +3593,7 @@
   by (metis append_Cons append_Nil contains50 f_cont2)
 
 
-(*
-lemma H00:
-  shows "((bder c) ` (AALTs_subs (AALTs bs rs))) =  AALTs_subs (map (bder c) rs)"
-*)
+
 
 lemma H1:
   assumes "r >> bs2" "r \<in> AALTs_subs a" 
@@ -3634,10 +3631,12 @@
   done
 
 lemma H6:
-  shows "AALTs_subs (AALTs bs (flts rs)) \<subseteq> AALTs_subs (AALTs bs rs)"
+  shows "AALTs_subs (AALTs bs (flts rs)) = AALTs_subs (AALTs bs rs)"
   apply(induct rs arbitrary: bs rule: flts.induct)
         apply(auto)
-  by (metis AALTs_subs_fuse2 H7 UnE fuse_map subset_iff)
+  apply (metis AALTs_subs_fuse2 H7 Un_iff fuse_map)
+  apply (metis AALTs_subs_fuse2 H7 UnCI fuse_map)
+  by (simp add: H7)
 
 
 lemma H2:
@@ -3649,7 +3648,12 @@
    apply (metis AALTs_subs_fuse2 H4 fuse_map in_mono)
   using H7 by blast
   
+lemma H00:
+  shows " (\<Union> (AALTs_subs ` (set (map (bder c o fuse bs) rs)))) \<subseteq> ((bder c) ` (AALTs_subs (AALTs bs rs)))"
+  apply(induct rs arbitrary: bs c)
+   apply(auto simp add: image_def)
   
+
   
 lemma contains61a_2:
   assumes "\<exists>r\<in>AALTs_subs (AALTs bs rs). r >> bs2" 
@@ -3757,6 +3761,7 @@
   apply(auto)
   
   
+  
 (* HERE HERE *)
 
 (* old *)