--- a/thys2/SizeBound4CT.thy	Fri Feb 04 00:35:34 2022 +0000
+++ b/thys2/SizeBound4CT.thy	Fri Feb 04 11:12:24 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