--- a/thys3/BlexerSimp.thy	Thu Jun 23 19:11:02 2022 +0100
+++ b/thys3/BlexerSimp.thy	Thu Jun 23 21:04:43 2022 +0100
@@ -148,6 +148,7 @@
 | ss4:  "(AZERO # rs) s\<leadsto> rs"
 | ss5:  "(AALTs bs1 rs1 # rsb) s\<leadsto> ((map (fuse bs1) rs1) @ rsb)"
 | ss6:  "L (erase a2) \<subseteq> L (erase a1) \<Longrightarrow> (rsa@[a1]@rsb@[a2]@rsc) s\<leadsto> (rsa@[a1]@rsb@rsc)"
+| ss7:  " (as @ [a] @ as1) s\<leadsto> (as @ [prune6 (set (concat (map (\<lambda>r. turnIntoTerms (erase r)) as))) a Nil] @ as1)"
 
 
 inductive 
@@ -187,8 +188,6 @@
    apply(auto)
   done
 
-
-
 lemma contextrewrites0: 
   "rs1 s\<leadsto>* rs2 \<Longrightarrow> AALTs bs rs1 \<leadsto>* AALTs bs rs2"
   apply(induct rs1 rs2 rule: srewrites.inducts)
@@ -213,17 +212,24 @@
    apply(auto)
   using srewrite1 by blast
 
+lemma srewrites_prepend:
+  shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (r # rs1) s\<leadsto>* (r # rs2)"
+  by (metis append_Cons append_Nil srewrites1)  
+
 lemma srewrite2: 
   shows  "r1 \<leadsto> r2 \<Longrightarrow> True"
   and "rs1 s\<leadsto> rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
-  apply(induct rule: rrewrite_srewrite.inducts)
-  apply(auto)
-  apply (metis append_Cons append_Nil srewrites1)
-  apply(meson srewrites.simps ss3)
-  apply (meson srewrites.simps ss4)
-  apply (meson srewrites.simps ss5)
-  by (metis append_Cons append_Nil srewrites.simps ss6)
-  
+  apply(induct arbitrary: rs rule: rrewrite_srewrite.inducts)
+                apply simp+
+  using srewrites_prepend apply force
+      apply (simp add: rs_in_rstar ss3)
+  using ss4 apply force 
+  using rs_in_rstar ss5 apply auto[1]
+  using rs_in_rstar ss6 apply auto[1]
+  using rs_in_rstar ss7 by force
+
+
+
 
 lemma srewrites3: 
   shows "rs1 s\<leadsto>* rs2 \<Longrightarrow> (rs1 @ rs) s\<leadsto>* (rs2 @ rs)"
@@ -231,15 +237,6 @@
    apply(auto)
   by (meson srewrite2(2) srewrites_trans)
 
-(*
-lemma srewrites4:
-  assumes "rs3 s\<leadsto>* rs4" "rs1 s\<leadsto>* rs2" 
-  shows "(rs1 @ rs3) s\<leadsto>* (rs2 @ rs4)"
-  using assms
-  apply(induct rs3 rs4 arbitrary: rs1 rs2 rule: srewrites.induct)
-  apply (simp add: srewrites3)
-  using srewrite1 by blast
-*)
 
 lemma srewrites6:
   assumes "r1 \<leadsto>* r2" 
@@ -256,7 +253,7 @@
   by (smt (verit, best) append_Cons append_Nil srewrites1 srewrites3 srewrites6 srewrites_trans)
 
 lemma ss6_stronger_aux:
-  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ distinctWith rs2 eq1 (set rs1))"
+  shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))"
   apply(induct rs2 arbitrary: rs1)
   apply(auto)
   prefer 2
@@ -270,11 +267,13 @@
   apply (simp add: split_list)
   apply(erule exE)+
   apply(simp)
-  using eq1_L rs_in_rstar ss6 by force
+  using eq1_L rs_in_rstar ss
+  sorry
+
 
 lemma ss6_stronger:
-  shows "rs1 s\<leadsto>* distinctWith rs1 eq1 {}"
-  by (metis append_Nil list.set(1) ss6_stronger_aux)
+  shows "rs1 s\<leadsto>* dB6 rs1 {}"
+  sorry
 
 
 lemma rewrite_preserves_fuse: 
@@ -338,17 +337,12 @@
   shows "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
 using assms bs1 star_seq by blast
 
-(*
-lemma continuous_rewrite2: 
-  assumes "r1 \<leadsto>* AONE bs"
-  shows "ASEQ bs1 r1 r2 \<leadsto>* (fuse (bs1 @ bs) r2)"
-  using assms  by (meson bs3 rrewrites.simps star_seq)
-*)
+
 
 lemma bsimp_aalts_simpcases: 
-  shows "AONE bs \<leadsto>* bsimp (AONE bs)"  
-  and   "AZERO \<leadsto>* bsimp AZERO" 
-  and   "ACHAR bs c \<leadsto>* bsimp (ACHAR bs c)"
+  shows "AONE bs \<leadsto>* bsimpStrong6 (AONE bs)"  
+  and   "AZERO \<leadsto>* bsimpStrong6 AZERO" 
+  and   "ACHAR bs c \<leadsto>* bsimpStrong6 (ACHAR bs c)"
   by (simp_all)
 
 lemma bsimp_AALTs_rewrites: