diff -r 3ea82d8f0aa4 -r 0f00d440f484 thys3/BlexerSimp.thy
--- a/thys3/BlexerSimp.thy	Fri Jun 24 11:41:05 2022 +0100
+++ b/thys3/BlexerSimp.thy	Fri Jun 24 21:49:23 2022 +0100
@@ -266,10 +266,22 @@
   shows " \<lbrakk>erase a \<in> erase ` set rs1\<rbrakk> \<Longrightarrow> (rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)"
   apply(subgoal_tac "\<exists>rs1a rs1b x. rs1 = rs1a @ [x] @ rs1b \<and> erase x = erase a")
   prefer 2
+   apply (meson existing_preimage)
+  apply(erule exE)+
+  apply simp
+  apply(subgoal_tac "(rs1a @ [x] @ rs1b @ [a] @ rs2) s\<leadsto> (rs1a @ [x] @ rs1b @ rs2)")  
+  apply (simp add: rs_in_rstar)
+  apply(subgoal_tac "L (erase a) \<subseteq> L (erase x)")
+  using ss6 apply presburger
+  by simp
 
+lemma ss6_realistic:
+  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (concat (map turnIntoTerms (map erase rs2)))))"
+  
 
   sorry
 
+
 lemma ss6_stronger_aux:
   shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))"
   apply(induct rs2 arbitrary: rs1)
@@ -280,6 +292,9 @@
   apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)")
   using srewrites_trans apply blast
   using deletes_dB apply presburger
+  apply(case_tac "set (turnIntoTerms (erase a)) \<subseteq> erase ` set rs1")
+  
+  apply simp
 
   apply(auto)
   prefer 2