
diff -r 5dcecc92608e -r afd8eff20402 thys2/SizeBound4.thy
--- a/thys2/SizeBound4.thy	Wed Feb 09 18:21:01 2022 +0000
+++ b/thys2/SizeBound4.thy	Wed Feb 09 18:21:15 2022 +0000
@@ -467,7 +467,6 @@
 | "flts (r1 # rs) = r1 # flts rs"
 
 
-
 fun bsimp_ASEQ :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp \<Rightarrow> arexp"
   where
   "bsimp_ASEQ _ AZERO _ = AZERO"
@@ -695,7 +694,7 @@
   using rs_in_rstar by force
 
 lemma ss6_stronger:
-  shows "rs1 s\<leadsto>* distinctBy rs1 erase {}"
+  shows "rs s\<leadsto>* distinctBy rs erase {}"
   using ss6_stronger_aux[of "[]" _] by auto
 
 lemma rewrite_preserves_fuse: 




