author | Christian Urban <urbanc@in.tum.de> |
Fri, 12 Jan 2018 02:33:35 +0000 | |
changeset 282 | bfab5aded21d |
parent 281 | 281ce101cda6 |
child 283 | c4d821c6309d |
Literature/aho1990.pdf | file | annotate | diff | comparison | revisions | |
thys/Exercises.thy | file | annotate | diff | comparison | revisions |
--- a/thys/Exercises.thy Thu Dec 07 12:45:22 2017 +0000 +++ b/thys/Exercises.thy Fri Jan 12 02:33:35 2018 +0000 @@ -75,6 +75,10 @@ (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)" | "infinitestrings (STAR r) = (\<not> atmostempty r)" + + + + lemma Star_atmostempty: assumes "A \<subseteq> {[]}" shows "A\<star> \<subseteq> {[]}"