--- a/thys3/BlexerSimp.thy	Thu Jun 23 16:59:58 2022 +0100
+++ b/thys3/BlexerSimp.thy	Thu Jun 23 18:32:14 2022 +0100
@@ -572,6 +572,7 @@
 done
 
 
+
 lemma central:  
   shows "bders r s \<leadsto>* bders_simp r s"
 proof(induct s arbitrary: r rule: rev_induct)
@@ -757,6 +758,57 @@
 *)
 
 
+lemma rewrites_to_bsimpStrong: 
+  shows "r \<leadsto>* bsimpStrong6 r"
+proof (induction r rule: bsimpStrong6.induct)
+  case (1 bs1 r1 r2)
+  have IH1: "r1 \<leadsto>* bsimpStrong6 r1" by fact
+  have IH2: "r2 \<leadsto>* bsimpStrong6 r2" by fact
+  { assume as: "bsimpStrong6 r1 = AZERO \<or> bsimpStrong6 r2 = AZERO"
+    with IH1 IH2 have "r1 \<leadsto>* AZERO \<or> r2 \<leadsto>* AZERO" by auto
+    then have "ASEQ bs1 r1 r2 \<leadsto>* AZERO"
+      by (metis bs2 continuous_rewrite rrewrites.simps star_seq2)  
+    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" using as by auto
+  }
+  moreover
+  { assume "\<exists>bs. bsimpStrong6 r1 = AONE bs"
+    then obtain bs where as: "bsimpStrong6 r1 = AONE bs" by blast
+    with IH1 have "r1 \<leadsto>* AONE bs" by simp
+    then have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) r2" using bs3 star_seq by blast
+    with IH2 have "ASEQ bs1 r1 r2 \<leadsto>* fuse (bs1 @ bs) (bsimpStrong6 r2)"
+      using rewrites_fuse by (meson rrewrites_trans) 
+    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 (AONE bs) r2)" by simp
+    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by (simp add: as) 
+  } 
+  moreover
+  { assume as1: "bsimpStrong6 r1 \<noteq> AZERO" "bsimpStrong6 r2 \<noteq> AZERO" and as2: "(\<nexists>bs. bsimpStrong6 r1 = AONE bs)" 
+    then have "bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2) = ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" 
+      by (simp add: bsimp_ASEQ1) 
+    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" using as1 as2 IH1 IH2
+      by (metis rrewrites_trans star_seq star_seq2) 
+    then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp
+  } 
+  ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" sorry
+next
+  case (2 bs1 rs)
+  have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact
+  then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites)
+  also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites) 
+  also have "... s\<leadsto>* distinctWith (flts (map bsimpStrong6 rs)) eq1 {}" by (simp add: ss6_stronger)
+  finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
+    using contextrewrites0 by auto
+  also have "... \<leadsto>* bsimp_AALTs  bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})"
+    by (simp add: bsimp_AALTs_rewrites)     
+  finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry
+qed (simp_all)
+
+lemma bders_simp_appendStrong :
+  shows "bdersStrong6 r (s1 @ s2) = bdersStrong6 (bdersStrong6 r s1) s2"
+  apply(induct s1 arbitrary: s2 rule: rev_induct)
+   apply simp
+  apply auto
+  done
+
 
 lemma centralStrong:  
   shows "bders r s \<leadsto>* bdersStrong6 r s"
@@ -770,9 +822,9 @@
   also have "... \<leadsto>* bders (bdersStrong6 r xs) [x]" using IH
     by (simp add: rewrites_preserves_bder)
   also have "... \<leadsto>* bdersStrong6 (bdersStrong6 r xs) [x]" using IH
-    by (simp add: rewrites_to_bsimp)
-  finally show "bders r (xs @ [x]) \<leadsto>* bders_simp r (xs @ [x])" 
-    by (simp add: bders_simp_append)
+    by (simp add: rewrites_to_bsimpStrong)
+  finally show "bders r (xs @ [x]) \<leadsto>* bdersStrong6 r (xs @ [x])" 
+    by (simp add: bders_simp_appendStrong)
 qed
 
 lemma mainStrong: