theory Corres_UL_C

lemma ccorres_symb_exec_r_rv_abstract:
  "\<lbrakk>  \<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)});
        \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv');
        \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv');
        \<Gamma> \<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)} \<rbrakk>
       \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs a (c;;y)" apply (rule ccorres_guard_imp2) apply (rule ccorres_add_return,
          rule_tac r'="\<lambda>rv rv'. F rv'" and xf'=xf'
                in ccorres_split_nothrow) apply (rule_tac P'=R' in ccorres_from_vcg[where P=R]) apply (clarsimp simp add: return_def Int_def conj_comms) apply assumption apply fastforce apply wp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs a (c;;
y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs a (c;;
y)
 2. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; (s, s') \<in> sr; (P and R) s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> (\<lambda>rv. F) xf' ?P5 ?P'5 hs (return ()) c
 2. \<And>rv' t t'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' y (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; F rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q5 rv) (?Q'5 rv rv') hs a (?d'5 rv')
 4. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 5. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> ?Q'5 rv (xf' s)}
 6. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; (s, s') \<in> sr; (P and R) s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> (?P5 and ?R5) s \<and> s' \<in> ?P'5 \<inter> ?R'5 proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. R \<sigma> \<and> s \<in> R' \<and> (\<sigma>, s) \<in> sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (return () \<sigma>). (\<sigma>', s) \<in> sr \<and> F (xf' s)}
 2. \<And>rv' t t'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' y (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; F rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q5 rv) (?Q'5 rv rv') hs a (?d'5 rv')
 4. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 5. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> ?Q'5 rv (xf' s)}
 6. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; (s, s') \<in> sr; (P and R) s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> (R and ?R5) s \<and> s' \<in> R' \<inter> ?R'5 proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' y (?d'5 rv')
 2. \<And>rv rv'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; F rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q5 rv) (?Q'5 rv rv') hs a (?d'5 rv')
 3. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 4. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> ?Q'5 rv (xf' s)}
 5. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; (s, s') \<in> sr; (P and R) s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> (R and ?R5) s \<and> s' \<in> R' \<inter> ?R'5 proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; F rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?Q5 rv) (?Q'5 rv rv') hs a (y' rv')
 2. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 3. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> ?Q'5 rv (xf' s)}
 4. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; (s, s') \<in> sr; (P and R) s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> (R and ?R5) s \<and> s' \<in> R' \<inter> ?R'5 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>\<lambda>a. P\<rbrace>
 2. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}
 3. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; (s, s') \<in> sr; (P and R) s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> (R and ?R5) s \<and> s' \<in> R' \<inter> ?R'5 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}
 2. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; (s, s') \<in> sr; (P and R) s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> (R and P) s \<and> s' \<in> R' \<inter> ?R'5 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. F (xf' s)}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); \<And>rv'. F rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (Q rv') hs a (y' rv'); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. F (xf' s) \<longrightarrow> s \<in> Q (xf' s)}; (s, s') \<in> sr; (P and R) s; s' \<in> P' \<inter> R'\<rbrakk> \<Longrightarrow> (R and P) s \<and> s' \<in> R' \<inter> P' proof (prove)
goal:
No subgoals!