207 

   207 

   208 text {* 

   208 text {* 

   209   Arden's lemma expressed at the level of languages, rather 

   209   Arden's lemma expressed at the level of languages, rather 

   210   than the level of regular expression. 

   210   than the level of regular expression. 

   211 *}

   211 *}

   213 

   212 

   214 lemma ardens_helper:

   213 lemma ardens_helper:

   215   assumes eq: "X = X ;; A \<union> B"

   214   assumes eq: "X = X ;; A \<union> B"

   216   shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"

   215   shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"

   217 proof (induct n)

   216 proof (induct n)