theory Corres_C

lemma ccorres_split_nothrow_novcg_case_sum:
  "\<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c;
    \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv');
    \<And>rv rv'. \<lbrakk> r' rv (vf' rv'); ef' rv' = scast EXCEPTION_NONE \<rbrakk>
             \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv');
    \<And>err rv' err'.
        \<lbrakk> ef' rv' \<noteq> scast EXCEPTION_NONE; f' err (ef' rv') err' \<rbrakk>
             \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv');
    \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf'
                               (\<lambda>rv rv'. {s. ef' rv' = scast EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'});
    \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es
             (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> scast EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk>
      \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>= case_sum e b) (c;;d)" apply (rule_tac R="case_sum QE Q" and R'="case_sum QE' QR'" for QE' QR'
              in ccorres_master_split_nohs_UNIV) apply assumption apply (case_tac rv, simp_all)[1] apply (erule ccorres_abstract) apply (rule ccorres_abstract[where xf'=es], rule ceqv_refl) apply (rule_tac P="ef' rv' \<noteq> scast EXCEPTION_NONE" in ccorres_gen_asm2) apply (rule_tac P="f' aa (ef' rv') rv'a" in ccorres_gen_asm2) apply assumption apply (erule ccorres_abstract) apply (rule_tac P="r' ba (vf' rv')" in ccorres_gen_asm2) apply (rule_tac P="ef' rv' = scast EXCEPTION_NONE" in ccorres_gen_asm2) apply assumption apply (simp add: validE_def) apply (erule hoare_strengthen_post, simp split: sum.split_asm) apply (clarsimp simp: guard_is_UNIV_def
                 split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>= case_sum e b) (c;;
d) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> ?r' ?xf' ?arrel' ?axf' P P' [] a c
 2. \<And>rv. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) (case rv of Inl x \<Rightarrow> ?QE'4 x | Inr x \<Rightarrow> ?QR'4 x) hs (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) d
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV ?r' ?xf' (\<lambda>a b. case a of Inl x \<Rightarrow> ?QE'4 x | Inr x \<Rightarrow> ?QR'4 x) proof (prove)
goal (3 subgoals):
 1. \<And>rv. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) (case rv of Inl x \<Rightarrow> ?QE'4 x | Inr x \<Rightarrow> ?QR'4 x) hs (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) d
 2. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl x \<Rightarrow> ?QE'4 x | Inr x \<Rightarrow> ?QR'4 x) proof (prove)
goal (4 subgoals):
 1. \<And>rv aa. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inl aa\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?QE'4 aa) hs (e aa) d
 2. \<And>rv ba. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl x \<Rightarrow> ?QE'4 x | Inr x \<Rightarrow> ?QR'4 x) proof (prove)
goal (4 subgoals):
 1. \<And>rv aa rv'. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inl aa\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?G'16 aa rv') hs (e aa) (d' rv')
 2. \<And>rv ba. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> ?G'16 a (xf' s)} | Inr x \<Rightarrow> ?QR'4 x) proof (prove)
goal (4 subgoals):
 1. \<And>rv aa rv' rv'a. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inl aa\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?G'20 aa rv' rv'a) hs (e aa) (d' rv')
 2. \<And>rv ba. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> ?G'20 a (xf' s) (es sa)}} | Inr x \<Rightarrow> ?QR'4 x) proof (prove)
goal (4 subgoals):
 1. \<And>rv aa rv' rv'a. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inl aa; ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?G'25 aa rv' rv'a) hs (e aa) (d' rv')
 2. \<And>rv ba. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> ?G'25 a (xf' s) (es sa) \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr x \<Rightarrow> ?QR'4 x) proof (prove)
goal (4 subgoals):
 1. \<And>rv aa rv' rv'a. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inl aa; ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' aa (ef' rv') rv'a\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?G'27 aa rv' rv'a) hs (e aa) (d' rv')
 2. \<And>rv ba. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> ?G'27 a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr x \<Rightarrow> ?QR'4 x) proof (prove)
goal (3 subgoals):
 1. \<And>rv ba. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 2. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr x \<Rightarrow> ?QR'4 x) proof (prove)
goal (3 subgoals):
 1. \<And>rv ba rv'. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'35 ba rv') hs (b ba) (d' rv')
 2. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> ?G'35 a (xf' s)}) proof (prove)
goal (3 subgoals):
 1. \<And>rv ba rv'. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inr ba; r' ba (vf' rv')\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'38 ba rv') hs (b ba) (d' rv')
 2. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> ?G'38 a (xf' s) \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>}) proof (prove)
goal (3 subgoals):
 1. \<And>rv ba rv'. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'}); rv = Inr ba; r' ba (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'40 ba rv') hs (b ba) (d' rv')
 2. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> ?G'40 a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 2. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> QE e s | Inr r \<Rightarrow> Q r s\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 2. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' [] a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; guard_is_UNIV (\<lambda>rv rv'. r' rv (vf' rv')) xf' (\<lambda>rv rv'. {s. ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q' rv rv'}); \<And>err. guard_is_UNIV (\<lambda>rv. f' err (ef' rv)) es (\<lambda>rv rv'. {s. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> Q'' err rv rv'})\<rbrakk> \<Longrightarrow> guard_is_UNIV (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>}) proof (prove)
goal:
No subgoals!