theory CCorresLemmas

lemma ccorres_if_cond_throws:
  fixes e :: 'e
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> Q' s' \<longrightarrow> P = (s' \<in> P')"
  and     ac: "P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R R' (SKIP # hs) a c"
  and     bd: "\<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf U U' (SKIP # hs) b d"
  and cthrows: "\<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> PT' c {}, UNIV" \<comment> \<open>c always throws\<close>
  shows  "ccorres_underlying sr \<Gamma> r xf arrel axf
          (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s))
          (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')})
          (SKIP # hs)
          (if P then a else b) (Cond P' c SKIP ;; d)"
  (is "ccorres_underlying sr \<Gamma> r xf arrel axf ?G ?G' ?hs ?a ?c") proof (cases P) case True thus ?thesis apply simp apply (rule ccorres_guard_imp2) apply (rule ccorres_split_throws) apply (rule ccorres_cond_true [OF ac [OF True]]) apply (rule HoarePartial.Cond [where P = "P' \<inter> PT'", OF _ cthrows]) apply clarsimp apply (rule HoarePartial.Skip) apply (rule subset_refl) apply (clarsimp simp: abs [rule_format, OF conjI]) done next case False thus ?thesis apply simp apply (rule ccorres_guard_imp2) apply (rule ccorres_add_return) apply (rule ccorres_split_nothrow) apply (rule ccorres_cond_false) apply (rule ccorres_return_Skip) apply (rule ceqv_refl) apply (rule bd [OF False]) apply wp apply simp apply (rule Cond_false) apply (rule HoarePartial.Skip [OF subset_refl]) apply (clarsimp simp: abs [rule_format, OF conjI]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d) proof (state)
goal (2 subgoals):
 1. P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d)
 2. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d) proof (state)
this:
P

goal (2 subgoals):
 1. P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d)
 2. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d) proof (prove)
using this:
P

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d) proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q and R) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) a (Cond P' c SKIP;;
d) proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q9 ?Q'9 (SKIP # hs) a (Cond P' c SKIP;;
d)
 2. \<And>s s'. \<lbrakk>P; (s, s') \<in> sr; (Q and R) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (3 subgoals):
 1. P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q9 ?P'12 (SKIP # hs) a (Cond P' c SKIP)
 2. P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'12 Cond P' c SKIP {},UNIV
 3. \<And>s s'. \<lbrakk>P; (s, s') \<in> sr; (Q and R) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?P'12 \<inter> ?R'12 proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'12 Cond P' c SKIP {},UNIV
 2. \<And>s s'. \<lbrakk>P; (s, s') \<in> sr; (Q and R) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> R s \<and> s' \<in> R' \<inter> P' \<inter> ?R'12 proof (prove)
goal (3 subgoals):
 1. P \<Longrightarrow> P' \<inter> PT' \<subseteq> {s. (s \<in> P' \<longrightarrow> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> ?P\<^sub>216)}
 2. P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?P\<^sub>216 SKIP {},UNIV
 3. \<And>s s'. \<lbrakk>P; (s, s') \<in> sr; (Q and R) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> R s \<and> s' \<in> R' \<inter> P' \<inter> (P' \<inter> PT') proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?P\<^sub>216 SKIP {},UNIV
 2. \<And>s s'. \<lbrakk>P; (s, s') \<in> sr; (Q and R) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> R s \<and> s' \<in> R' \<inter> P' \<inter> (P' \<inter> PT') proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> ?P\<^sub>216 \<subseteq> {}
 2. \<And>s s'. \<lbrakk>P; (s, s') \<in> sr; (Q and R) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> R s \<and> s' \<in> R' \<inter> P' \<inter> (P' \<inter> PT') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>P; (s, s') \<in> sr; (Q and R) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> R s \<and> s' \<in> R' \<inter> P' \<inter> (P' \<inter> PT') proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d)

goal (1 subgoal):
 1. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d) proof (state)
goal (1 subgoal):
 1. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d) proof (state)
this:
\<not> P

goal (1 subgoal):
 1. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d) proof (prove)
using this:
\<not> P

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d) proof (prove)
goal (1 subgoal):
 1. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q and U) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) b (Cond P' c SKIP;;
d) proof (prove)
goal (2 subgoals):
 1. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q9 ?Q'9 (SKIP # hs) b (Cond P' c SKIP;;
d)
 2. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (2 subgoals):
 1. \<not> P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q9 ?Q'9 (SKIP # hs) (do _ <- return ();
b
od) (Cond P' c SKIP;;
d)
 2. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (6 subgoals):
 1. \<not> P \<Longrightarrow> ccorresG sr \<Gamma> ?r'14 ?xf'14 ?P14 ?P'14 (SKIP # hs) (return ()) (Cond P' c SKIP)
 2. \<And>rv' t t'. \<not> P \<Longrightarrow> ceqv \<Gamma> ?xf'14 rv' t t' d (?d'14 rv')
 3. \<And>uu_ rv'. \<lbrakk>\<not> P; ?r'14 uu_ rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q14 uu_) (?Q'14 uu_ rv') (SKIP # hs) b (?d'14 rv')
 4. \<not> P \<Longrightarrow> \<lbrace>?R14\<rbrace> return () \<lbrace>?Q14\<rbrace>
 5. \<not> P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F14\<^esub> ?R'14 Cond P' c SKIP {s. \<forall>uu_. ?r'14 uu_ (?xf'14 s) \<longrightarrow> s \<in> ?Q'14 uu_ (?xf'14 s)}
 6. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> (?P14 and ?R14) s \<and> s' \<in> ?P'14 \<inter> ?R'14 proof (prove)
goal (6 subgoals):
 1. \<not> P \<Longrightarrow> ccorresG sr \<Gamma> ?r'14 ?xf'14 ?P14 ?R'20 (SKIP # hs) (return ()) SKIP
 2. \<And>rv' t t'. \<not> P \<Longrightarrow> ceqv \<Gamma> ?xf'14 rv' t t' d (?d'14 rv')
 3. \<And>uu_ rv'. \<lbrakk>\<not> P; ?r'14 uu_ rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q14 uu_) (?Q'14 uu_ rv') (SKIP # hs) b (?d'14 rv')
 4. \<not> P \<Longrightarrow> \<lbrace>?R14\<rbrace> return () \<lbrace>?Q14\<rbrace>
 5. \<not> P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F14\<^esub> ?R'14 Cond P' c SKIP {s. \<forall>uu_. ?r'14 uu_ (?xf'14 s) \<longrightarrow> s \<in> ?Q'14 uu_ (?xf'14 s)}
 6. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> (?P14 and ?R14) s \<and> s' \<in> ?R'20 \<inter> - P' \<inter> ?R'14 proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. \<not> P \<Longrightarrow> ceqv \<Gamma> ?xf'14 rv' t t' d (?d'14 rv')
 2. \<And>uu_ rv'. \<lbrakk>\<not> P; dc uu_ rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q14 uu_) (?Q'14 uu_ rv') (SKIP # hs) b (?d'14 rv')
 3. \<not> P \<Longrightarrow> \<lbrace>?R14\<rbrace> return () \<lbrace>?Q14\<rbrace>
 4. \<not> P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F14\<^esub> ?R'14 Cond P' c SKIP {s. \<forall>uu_. dc uu_ (?xf'14 s) \<longrightarrow> s \<in> ?Q'14 uu_ (?xf'14 s)}
 5. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R14) s \<and> s' \<in> UNIV \<inter> - P' \<inter> ?R'14 proof (prove)
goal (4 subgoals):
 1. \<And>uu_ rv'. \<lbrakk>\<not> P; dc uu_ rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q14 uu_) (?Q'14 uu_ rv') (SKIP # hs) b d
 2. \<not> P \<Longrightarrow> \<lbrace>?R14\<rbrace> return () \<lbrace>?Q14\<rbrace>
 3. \<not> P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F14\<^esub> ?R'14 Cond P' c SKIP {s. \<forall>uu_. dc uu_ (?xf'14 s) \<longrightarrow> s \<in> ?Q'14 uu_ (?xf'14 s)}
 4. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R14) s \<and> s' \<in> UNIV \<inter> - P' \<inter> ?R'14 proof (prove)
goal (3 subgoals):
 1. \<not> P \<Longrightarrow> \<lbrace>?R14\<rbrace> return () \<lbrace>\<lambda>_. U\<rbrace>
 2. \<not> P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F14\<^esub> ?R'14 Cond P' c SKIP {s. \<forall>uu_. dc uu_ (?xf'14 s) \<longrightarrow> s \<in> U'}
 3. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R14) s \<and> s' \<in> UNIV \<inter> - P' \<inter> ?R'14 proof (prove)
goal (2 subgoals):
 1. \<not> P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F14\<^esub> ?R'14 Cond P' c SKIP {s. \<forall>uu_. dc uu_ (?xf'14 s) \<longrightarrow> s \<in> U'}
 2. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and U) s \<and> s' \<in> UNIV \<inter> - P' \<inter> ?R'14 proof (prove)
goal (2 subgoals):
 1. \<not> P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F14\<^esub> ?R'14 Cond P' c SKIP U'
 2. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and U) s \<and> s' \<in> UNIV \<inter> - P' \<inter> ?R'14 proof (prove)
goal (2 subgoals):
 1. \<not> P \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F14\<^esub> ?P27 SKIP U'
 2. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and U) s \<and> s' \<in> UNIV \<inter> - P' \<inter> (?P27 \<inter> - P') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<not> P; (s, s') \<in> sr; (Q and U) s; s' \<in> Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<and> s \<in> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and U) s \<and> s' \<in> UNIV \<inter> - P' \<inter> (U' \<inter> - P') proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres_underlying sr \<Gamma> r xf arrel axf (Q and (\<lambda>s. P \<longrightarrow> R s) and (\<lambda>s. \<not> P \<longrightarrow> U s)) (Collect Q' \<inter> {s. (s \<in> P' \<longrightarrow> s \<in> R' \<inter> PT') \<and> (s \<notin> P' \<longrightarrow> s \<in> U')}) (SKIP # hs) (if P then a else b) (Cond P' c SKIP;;
d)

goal:
No subgoals!