--- a/thys/Exercises.thy	Fri Dec 30 23:41:44 2022 +0000
+++ b/thys/Exercises.thy	Wed Feb 15 11:52:22 2023 +0000
@@ -30,7 +30,10 @@
      zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)"
 | "atmostempty (STAR r) = atmostempty r"
 
-
+lemma "atmostempty r \<longrightarrow> (zeroable r \<or> nullable r)"
+  apply(induct r)
+  apply(auto)
+  done
 
 fun
  somechars :: "rexp \<Rightarrow> bool"
@@ -40,8 +43,7 @@
 | "somechars (CH c) \<longleftrightarrow> True"
 | "somechars (ALT r1 r2) \<longleftrightarrow> somechars r1 \<or> somechars r2"
 | "somechars (SEQ r1 r2) \<longleftrightarrow> 
-      (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1) \<or> 
-      (somechars r1 \<and> nullable r2) \<or> (somechars r2 \<and> nullable r1)"
+      (\<not> zeroable r1 \<and> somechars r2) \<or> (\<not> zeroable r2 \<and> somechars r1)"
 | "somechars (STAR r) \<longleftrightarrow> somechars r"
 
 lemma somechars_correctness: