diff -r 28cb8089ec36 -r 7a579f5533f8 thys3/BlexerSimp.thy
--- a/thys3/BlexerSimp.thy	Thu Jul 14 14:57:32 2022 +0100
+++ b/thys3/BlexerSimp.thy	Sat Jul 16 18:34:46 2022 +0100
@@ -359,11 +359,38 @@
 done
 
 
-lemma "set (tint (seqFold (erase x42) [erase x43])) = 
+lemma tint_seqFold_eq: shows"set (tint (seqFold (erase x42) [erase x43])) = 
            set (tint (SEQ (erase x42) (erase x43)))"
   apply(case_tac "erase x42 = ONE")
    apply simp
+  using seqFold_concats
   apply simp
+  done
+
+fun top :: "arexp \<Rightarrow> bit list" where
+  "top AZERO = []"
+| "top (AONE bs) = bs"
+| "top (ASEQ bs r1 r2) = bs"
+| "top (ACHAR v va) = v"
+| "top (AALTs v va) = v"
+| "top (ASTAR v va) = v "
+
+
+
+lemma top_bitcodes_preserved_p6:
+  shows "\<lbrakk> r = ASEQ bs a1 a2 \<rbrakk> \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>bs3. top (p6 as r) = bs @ bs3)"
+  apply(induct r arbitrary: as)
+       apply simp
+  apply simp
+     apply simp
+
+  apply(case_tac "a1")
+         apply simp
+
+
+  sorry
+
+
 
 lemma prune6_preserves_fuse:
   shows "fuse bs (p6 as a) = p6 as (fuse bs a)"
@@ -377,7 +404,7 @@
   using fused_bits_at_head
 
     apply simp
-  apply(case_tac "erase x42 = ONE")
+  using tint_seqFold_eq
   apply simp
 
   sorry