diff -r 01d1285b08ed -r f71df68776bb thys2/SizeBound4CT.thy
--- a/thys2/SizeBound4CT.thy	Wed Feb 02 22:30:41 2022 +0000
+++ b/thys2/SizeBound4CT.thy	Fri Feb 04 00:05:12 2022 +0000
@@ -1156,6 +1156,16 @@
   using bsimp_ASEQ_idem apply presburger
   oops
 
+
+lemma normal_form: 
+  shows "\<forall>r. \<nexists> r'. bsimp r \<leadsto> r'"
+
+  oops
+
+lemma another_normal:
+  shows "\<nexists>r'. bsimp r \<leadsto> r'"
+  oops
+
 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers