--- a/thys2/SizeBound4.thy	Wed Feb 02 22:30:41 2022 +0000
+++ b/thys2/SizeBound4.thy	Fri Feb 04 00:05:12 2022 +0000
@@ -1444,6 +1444,40 @@
   using bsimp_ASEQ_idem apply presburger
   oops
 
+lemma neg:
+  shows " \<not>(\<exists>r2. r1 \<leadsto> r2 \<and>  (r2 \<leadsto>* bsimp r1) )"
+  apply(rule notI)
+  apply(erule exE)
+  apply(erule conjE)
+  oops
+
+
+
+
+lemma reduction_always_in_bsimp:
+  shows " \<lbrakk> r1 \<leadsto> r2 ; \<not>(r2 \<leadsto>* bsimp r1)\<rbrakk> \<Longrightarrow> False"
+  apply(erule rrewrite.cases)
+         apply simp
+        apply auto
+
+  oops
+
+(*
+AALTs [] [AZERO, AALTs(bs1, [a, b]) ] 
+rewrite seq 1: \<leadsto> AALTs [] [ AALTs(bs1, [a, b]) ] \<leadsto>
+fuse [] (AALTs bs1, [a, b])
+rewrite seq 2: \<leadsto> AALTs [] [AZERO, (fuse bs1 a), (fuse bs1 b)]) ]
+
+*)
+
+lemma normal_bsimp: 
+  shows "\<nexists>r'. bsimp r \<leadsto> r'"
+  oops
+
+  (*r' size bsimp r > size r' 
+    r' \<leadsto>* bsimp bsimp r
+size bsimp r > size r' \<ge> size bsimp bsimp r*)
+
 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers