--- a/thys2/BasicIdentities.thy	Tue Apr 12 15:51:35 2022 +0100
+++ b/thys2/BasicIdentities.thy	Wed Apr 13 09:18:29 2022 +0100
@@ -768,15 +768,23 @@
 
 fun star_update :: "char \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list" where
 "star_update c r [] = []"
-|"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) 
+|"star_update c r (s # Ss) = (if (rnullable (rders r s)) 
                                 then (s@[c]) # [c] # (star_update c r Ss) 
                                else   (s@[c]) # (star_update c r Ss) )"
 
+
 fun star_updates :: "char list \<Rightarrow> rrexp \<Rightarrow> char list list \<Rightarrow> char list list"
   where
 "star_updates [] r Ss = Ss"
 | "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)"
 
+lemma stupdates_append: shows 
+"star_updates (s @ [c]) r Ss = star_update c r (star_updates s r Ss)"
+  apply(induct s arbitrary: Ss)
+   apply simp
+  apply simp
+  done
+
 
 lemma distinct_flts_no0:
   shows "  rflts (map rsimp (rdistinct rs (insert RZERO rset)))  =