[STATEMENT]
lemma seq_cont_Sup_distl:
    assumes "P is \<H>" "A \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H" "A \<noteq> {}"
    shows "P ;; (\<^bold>\<Sqinter> A) = \<^bold>\<Sqinter> {P ;; Q | Q. Q \<in> A }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}
[PROOF STEP]
have "{P ;; Q | Q. Q \<in> A } \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A} \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H
[PROOF STEP]
using Healthy_Sequence assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?P is \<H>; ?Q is \<H>\<rbrakk> \<Longrightarrow> ?P ;; ?Q is \<H>
P is \<H>
A \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H

goal (1 subgoal):
 1. {uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A} \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A} \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H

goal (1 subgoal):
 1. P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A} \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H

goal (1 subgoal):
 1. P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}
[PROOF STEP]
by (simp add: healthy_inf_cont seq_Sup_distl setcompr_eq_image assms)
[PROOF STATE]
proof (state)
this:
P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}

goal:
No subgoals!
[PROOF STEP]
qed