72 | "infinitestrings (CHAR c) = False"

    72 | "infinitestrings (CHAR c) = False"

    73 | "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)"

    73 | "infinitestrings (ALT r1 r2) = (infinitestrings r1 \<or> infinitestrings r2)"

    74 | "infinitestrings (SEQ r1 r2) \<longleftrightarrow> 

    74 | "infinitestrings (SEQ r1 r2) \<longleftrightarrow> 

    75       (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)"

    75       (\<not> zeroable r1 \<and> infinitestrings r2) \<or> (\<not> zeroable r2 \<and> infinitestrings r1)"

    76 | "infinitestrings (STAR r) = (\<not> atmostempty r)"

    76 | "infinitestrings (STAR r) = (\<not> atmostempty r)"

    77 

    81 

    78 lemma Star_atmostempty:

    82 lemma Star_atmostempty:

    79   assumes "A \<subseteq> {[]}"

    83   assumes "A \<subseteq> {[]}"

    80   shows "A\<star> \<subseteq> {[]}"

    84   shows "A\<star> \<subseteq> {[]}"

    81 using assms

    85 using assms