diff -r c27f04bb2262 -r 812e5d112f49 thys3/BlexerSimp.thy
--- a/thys3/BlexerSimp.thy	Wed Jun 29 12:38:05 2022 +0100
+++ b/thys3/BlexerSimp.thy	Fri Jul 01 13:02:15 2022 +0100
@@ -276,9 +276,12 @@
   by simp
 
 lemma ss6_realistic:
-  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (concat (map turnIntoTerms (map erase rs2)))))"
-  
-
+  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (concat (map turnIntoTerms (map erase rs1)))))"
+  apply(induct rs2 arbitrary: rs1)
+   apply simp
+  apply(rename_tac cc cc')
+ 
+ 
   sorry