791 proof -

   791 proof -

   792   def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"

   792   def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"

   793   def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"

   793   def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"

   794   def B \<equiv> "L b" 

   794   def B \<equiv> "L b" 

   795   have "X = B ;; A\<star>"

   795   have "X = B ;; A\<star>"

   797     have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)

   797     have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)

   798     also have "\<dots> = X ;; A \<union> B"

   798     also have "\<dots> = X ;; A \<union> B"

   799       unfolding L_rhs_union_distrib[symmetric]

   799       unfolding L_rhs_union_distrib[symmetric]

   800       by (simp only: lang_of_rexp_of finite B_def A_def)

   800       by (simp only: lang_of_rexp_of finite B_def A_def)

   801     finally show ?thesis

   801     finally show ?thesis