--- a/thys2/SizeBound4.thy	Wed Feb 09 00:29:04 2022 +0000
+++ b/thys2/SizeBound4.thy	Wed Feb 09 11:21:28 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: