theory Recycle_C

lemma ccorres_subst_basic_helper:
  "\<lbrakk> \<And>s s'. \<lbrakk> P s; s' \<in> P'; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> f s' = f' s';
     \<And>s s'. \<lbrakk> P s; s' \<in> P'; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr;
     \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv');
        ccorres rrel xf Q Q' hs a (c' v) \<rbrakk>
       \<Longrightarrow> ccorres rrel xf (P and Q) {s. s \<in> P' \<and> f' s \<in> Q'} hs a (Basic f ;; c)" apply (rule ccorres_guard_imp2) apply (rule ccorres_add_return) apply (rule ccorres_split_nothrow[where xf'=xf' and r'="\<lambda>rv rv'. rv' = v"]) apply (rule ccorres_from_vcg[where P=P and P'=P']) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def) apply assumption apply simp apply wp apply vcg apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> ccorres rrel xf (P and Q) {s \<in> P'. f' s \<in> Q'} hs a (Basic f;;
c) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> ccorres rrel xf ?Q ?Q' hs a (Basic f;;
c)
 2. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> ccorres rrel xf ?Q ?Q' hs (do _ <- return ();
a
od) (Basic f;;
c)
 2. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>_ rv'. rv' = v) xf' ?P5 ?P'5 hs (return ()) (Basic f)
 2. \<And>rv' t t'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' c (?d'5 rv')
 3. \<And>uu_ rv'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); rv' = v\<rbrakk> \<Longrightarrow> ccorres rrel xf (?Q5 uu_) (?Q'5 uu_ rv') hs a (?d'5 rv')
 4. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 5. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 Basic f {s. \<forall>uu_. xf' s = v \<longrightarrow> s \<in> ?Q'5 uu_ (xf' s)}
 6. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> (?P5 and ?R5) s \<and> s' \<in> ?P'5 \<inter> ?R'5 proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} Basic f {s. \<exists>(rv, \<sigma>')\<in>fst (return () \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> xf' s = v}
 2. \<And>rv' t t'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' c (?d'5 rv')
 3. \<And>uu_ rv'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); rv' = v\<rbrakk> \<Longrightarrow> ccorres rrel xf (?Q5 uu_) (?Q'5 uu_ rv') hs a (?d'5 rv')
 4. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 5. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 Basic f {s. \<forall>uu_. xf' s = v \<longrightarrow> s \<in> ?Q'5 uu_ (xf' s)}
 6. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> (P and ?R5) s \<and> s' \<in> P' \<inter> ?R'5 proof (prove)
goal (6 subgoals):
 1. \<And>\<sigma>. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return () \<sigma>). (\<sigma>', f s) \<in> rf_sr \<and> xf' (f s) = v}
 2. \<And>rv' t t'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' c (?d'5 rv')
 3. \<And>uu_ rv'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); rv' = v\<rbrakk> \<Longrightarrow> ccorres rrel xf (?Q5 uu_) (?Q'5 uu_ rv') hs a (?d'5 rv')
 4. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 5. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 Basic f {s. \<forall>uu_. xf' s = v \<longrightarrow> s \<in> ?Q'5 uu_ (xf' s)}
 6. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> (P and ?R5) s \<and> s' \<in> P' \<inter> ?R'5 proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' c (?d'5 rv')
 2. \<And>uu_ rv'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); rv' = v\<rbrakk> \<Longrightarrow> ccorres rrel xf (?Q5 uu_) (?Q'5 uu_ rv') hs a (?d'5 rv')
 3. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 4. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 Basic f {s. \<forall>uu_. xf' s = v \<longrightarrow> s \<in> ?Q'5 uu_ (xf' s)}
 5. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> (P and ?R5) s \<and> s' \<in> P' \<inter> ?R'5 proof (prove)
goal (4 subgoals):
 1. \<And>uu_ rv'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); rv' = v\<rbrakk> \<Longrightarrow> ccorres rrel xf (?Q5 uu_) (?Q'5 uu_ rv') hs a (c' rv')
 2. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>?Q5\<rbrace>
 3. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 Basic f {s. \<forall>uu_. xf' s = v \<longrightarrow> s \<in> ?Q'5 uu_ (xf' s)}
 4. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> (P and ?R5) s \<and> s' \<in> P' \<inter> ?R'5 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<lbrace>?R5\<rbrace> return () \<lbrace>\<lambda>a. Q\<rbrace>
 2. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 Basic f {s. \<forall>_. xf' s = v \<longrightarrow> s \<in> Q'}
 3. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> (P and ?R5) s \<and> s' \<in> P' \<inter> ?R'5 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F5\<^esub> ?R'5 Basic f {s. \<forall>_. xf' s = v \<longrightarrow> s \<in> Q'}
 2. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> (P and Q) s \<and> s' \<in> P' \<inter> ?R'5 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> f s' = f' s'; \<And>s s'. \<lbrakk>P s; s' \<in> P'; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s, f' s') \<in> rf_sr; \<And>s'. xf' (f' s') = v; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' c (c' rv'); ccorres rrel xf Q Q' hs a (c' v); (s, s') \<in> rf_sr; (P and Q) s; s' \<in> {s \<in> P'. f' s \<in> Q'}\<rbrakk> \<Longrightarrow> (P and Q) s \<and> s' \<in> P' \<inter> {s. \<forall>_. xf' (f s) = v \<longrightarrow> f s \<in> Q'} proof (prove)
goal:
No subgoals!