54   all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using Lemma ???.

    54   all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using Lemma ???.

    55   For the inclusion in the other direction we assume a string @{text s}

    55   For the inclusion in the other direction we assume a string @{text s}

    56   with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised}

    56   with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised}

    57   we know that @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}

    57   we know that @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}

    58   (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). 

    58   (the strings in @{term "X ;; (A \<up> Suc k)"} are all longer). 

    60   @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn

    60   @{term s} must be element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn

    61   implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this

    61   implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Lemma ??? this

    62   is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed

    62   is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed

    63   \end{proof}

    63   \end{proof}

    64 *}

    64 *}