theory Corres_C

lemma ccorres_sequenceE_while_gen_either_way:
  fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word"
  assumes one: "\<And>n ys. \<lbrakk> n < length xs; n = length ys \<rbrakk> \<Longrightarrow>
                    ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (ys @ [rv]) rv')) xf'
                            (inl_rrel arrel) axf
                            (F n) (Q \<inter> {s. xf s = xfrel n \<and> r' ys (xf' s)}) hs
                            (xs ! n) body"
  and      pn: "\<And>n. (n < length xs \<longrightarrow> P (xfrel n)) \<and> \<not> P (xfrel (length xs))"
  and xfrel_u: "\<And>n. xfrel_upd (xfrel n) = xfrel (Suc n)"
  and   bodyi: "\<And>s. s \<in> Q \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> {t. xf t = xf s}), UNIV"
  and      hi: "\<And>n. n < length xs \<Longrightarrow> \<lbrace> F n \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n)\<rbrace>,-"
  and      xf: "\<forall>s f. xf (xf_update f s) = f (xf s)"
  and     xf': "\<forall>s f. xf' (xf_update f s) = (xf' s)
                               \<and> ((xf_update f s \<in> Q) = (s \<in> Q))
                               \<and> (\<forall>s'. ((s', xf_update f s) \<in> sr) = ((s', s) \<in> sr))"
  shows  "ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs)))
                  (\<lambda>s. (xf s, xf' s)) arrel axf
                  (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs
                  (sequenceE xs)
                  (While {s. P (xf s)}
                     (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))"
  (is "ccorres_underlying sr \<Gamma> (inr_rrel ?r') ?xf' arrel axf ?G ?G' hs (sequenceE xs) ?body") proof - define init_xs where "init_xs \<equiv> xs" have rl: "xs = drop (length init_xs - length xs) init_xs" unfolding init_xs_def by fastforce note pn' = pn [folded init_xs_def] note one' = one [folded init_xs_def] note hi'  = hi [folded init_xs_def] let ?Q  = "\<lambda>xs. F (length init_xs - length xs)" let ?Q' = "\<lambda>xs zs. Q \<inter> {s. (xf s) = xfrel (length init_xs - length xs)
                         \<and> r' zs (xf' s)}" let ?r'' = "\<lambda>zs rv (i', rv'). r' (zs @ rv) rv'
                   \<and> i' = xfrel (length init_xs)" have "\<forall>zs. length zs = length init_xs - length xs \<longrightarrow>
             ccorres_underlying sr \<Gamma> (inr_rrel (?r'' zs)) ?xf' (inl_rrel arrel) axf
             (?Q xs) (?Q' xs zs) hs
             (sequenceE xs) ?body" using rl proof (induct xs) case Nil thus ?case apply clarsimp apply (rule iffD1 [OF ccorres_expand_while_iff]) apply (simp add: sequenceE_def returnOk_def) apply (rule ccorres_guard_imp2) apply (rule ccorres_cond_false) apply (rule ccorres_return_Skip') apply (simp add: pn') done next case (Cons y ys) from Cons.prems have ly: "length (y # ys) \<le> length init_xs" by simp hence ln: "(length init_xs - length ys) = Suc (length init_xs - length (y # ys))" by simp hence yv: "y = init_xs ! (length init_xs - length (y # ys))" using Cons.prems by (fastforce simp add: drop_Suc_nth not_le) have lt0: "0 < length init_xs" using ly by clarsimp hence ly': "length init_xs - length (y # ys) < length init_xs" by simp note one'' = one'[OF ly', simplified yv[symmetric]] have ys_eq: "ys = drop (length init_xs - length ys) init_xs" using ln Cons.prems by (fastforce simp add: drop_Suc_nth not_le) note ih = Cons.hyps [OF ys_eq, rule_format] note hi'' = hi' [OF ly', folded yv] show ?case apply (clarsimp simp: sequenceE_Cons) apply (rule ccorres_guard_imp2) apply (rule iffD1 [OF ccorres_expand_while_iff]) apply (rule ccorres_cond_true) apply (rule ccorres_rhs_assoc)+ apply (rule ccorres_splitE) apply simp apply (rule_tac ys="zs" in one'') apply simp apply (rule ceqv_refl) apply (rule ccorres_symb_exec_r) apply (simp add: liftME_def[symmetric] liftME_liftM) apply (rule ccorres_rel_imp2, rule_tac zs="zs @ [rv]" in ih) apply (cut_tac ly, simp) apply (clarsimp elim!: inl_inrE) apply (clarsimp elim!: inl_inrE) apply vcg apply (rule conseqPre) apply vcg apply (clarsimp simp: xf xf') apply (subst ln) apply (rule hi'') apply (rule HoarePartialDef.Conseq [where P = "Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}"]) apply (intro ballI exI) apply (rule conjI) apply (rule_tac s=s in bodyi) apply simp apply (clarsimp simp: xf xf' ccHoarePost_def elim!: inl_inrE) apply (clarsimp simp: ln pn' xfrel_u diff_Suc_less[OF lt0]) done qed thus ?thesis by (clarsimp simp: init_xs_def dest!: spec[where x=Nil]
                elim!: ccorres_rel_imp2 inl_inrE
                 cong: ccorres_all_cong) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
init_xs \<equiv> xs

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
goal (1 subgoal):
 1. xs = drop (length init_xs - length xs) init_xs proof (prove)
goal (1 subgoal):
 1. xs = drop (length xs - length xs) xs proof (state)
this:
xs = drop (length init_xs - length xs) init_xs

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
(?n < length init_xs \<longrightarrow> P (xfrel ?n)) \<and> \<not> P (xfrel (length init_xs))

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
\<lbrakk>?n < length init_xs; ?n = length ?ys\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (?ys @ [rv]))) xf' (inl_rrel arrel) axf (F ?n) (Q \<inter> {s. xf s = xfrel ?n \<and> r' ?ys (xf' s)}) hs (init_xs ! ?n) body

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
?n < length init_xs \<Longrightarrow> \<lbrace>F ?n\<rbrace> init_xs ! ?n \<lbrace>\<lambda>_. F (Suc ?n)\<rbrace>, -

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
goal (1 subgoal):
 1. \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
using this:
xs = drop (length init_xs - length xs) init_xs

goal (1 subgoal):
 1. \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
goal (2 subgoals):
 1. [] = drop (length init_xs - length []) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length [] \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length [])) (Q \<inter> {s. xf s = xfrel (length init_xs - length []) \<and> r' zs (xf' s)}) hs (sequenceE []) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))
 2. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
[] = drop (length init_xs - length []) init_xs

goal (2 subgoals):
 1. [] = drop (length init_xs - length []) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length [] \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length [])) (Q \<inter> {s. xf s = xfrel (length init_xs - length []) \<and> r' zs (xf' s)}) hs (sequenceE []) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))
 2. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
using this:
[] = drop (length init_xs - length []) init_xs

goal (1 subgoal):
 1. \<forall>zs. length zs = length init_xs - length [] \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length [])) (Q \<inter> {s. xf s = xfrel (length init_xs - length []) \<and> r' zs (xf' s)}) hs (sequenceE []) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
goal (1 subgoal):
 1. \<And>zs. length zs = length init_xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs)) (Q \<inter> {s. xf s = xfrel (length init_xs) \<and> r' zs (xf' s)}) hs (sequenceE []) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
goal (1 subgoal):
 1. \<And>zs. length zs = length init_xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs)) (Q \<inter> {s. xf s = xfrel (length init_xs) \<and> r' zs (xf' s)}) hs (sequenceE []) (IF P \<acute>xf THEN
  body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))
FI) proof (prove)
goal (1 subgoal):
 1. \<And>zs. length zs = length init_xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs)) (Q \<inter> {s. xf s = xfrel (length init_xs) \<and> r' zs (xf' s)}) hs (return (Inr [])) (IF P \<acute>xf THEN
  body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))
FI) proof (prove)
goal (2 subgoals):
 1. \<And>zs. length zs = length init_xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q13 zs) (?Q'13 zs) hs (return (Inr [])) (IF P \<acute>xf THEN
  body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))
FI)
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs; (s, s') \<in> sr; F (length init_xs) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> ?Q13 zs s \<and> s' \<in> ?Q'13 zs proof (prove)
goal (2 subgoals):
 1. \<And>zs. length zs = length init_xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q13 zs) (?R'16 zs) hs (return (Inr [])) SKIP
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs; (s, s') \<in> sr; F (length init_xs) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> ?Q13 zs s \<and> s' \<in> ?R'16 zs \<inter> - {s. P (xf s)} proof (prove)
goal (1 subgoal):
 1. \<And>zs s s'. \<lbrakk>length zs = length init_xs; (s, s') \<in> sr; F (length init_xs) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> UNIV \<inter> {s. inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs)) (Inr []) (xf s, xf' s)} \<inter> - {s. P (xf s)} proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>zs. length zs = length init_xs - length [] \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length [])) (Q \<inter> {s. xf s = xfrel (length init_xs - length []) \<and> r' zs (xf' s)}) hs (sequenceE []) (While {s. P (xf s)} (body;;
\<acute>xf :== xfrel_upd \<acute>xf))

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
ys = drop (length init_xs - length ys) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length ys \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length ys)) (Q \<inter> {s. xf s = xfrel (length init_xs - length ys) \<and> r' zs (xf' s)}) hs (sequenceE ys) (While {s. P (xf s)} (body;;
\<acute>xf :== xfrel_upd \<acute>xf))
y # ys = drop (length init_xs - length (y # ys)) init_xs

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (chain)
picking this:
y # ys = drop (length init_xs - length (y # ys)) init_xs proof (prove)
using this:
y # ys = drop (length init_xs - length (y # ys)) init_xs

goal (1 subgoal):
 1. length (y # ys) \<le> length init_xs proof (state)
this:
length (y # ys) \<le> length init_xs

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
using this:
length (y # ys) \<le> length init_xs

goal (1 subgoal):
 1. length init_xs - length ys = Suc (length init_xs - length (y # ys)) proof (state)
this:
length init_xs - length ys = Suc (length init_xs - length (y # ys))

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
using this:
length init_xs - length ys = Suc (length init_xs - length (y # ys))

goal (1 subgoal):
 1. y = init_xs ! (length init_xs - length (y # ys)) proof (prove)
using this:
length init_xs - length ys = Suc (length init_xs - length (y # ys))
y # ys = drop (length init_xs - length (y # ys)) init_xs

goal (1 subgoal):
 1. y = init_xs ! (length init_xs - length (y # ys)) proof (state)
this:
y = init_xs ! (length init_xs - length (y # ys))

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
goal (1 subgoal):
 1. 0 < length init_xs proof (prove)
using this:
length (y # ys) \<le> length init_xs

goal (1 subgoal):
 1. 0 < length init_xs proof (state)
this:
0 < length init_xs

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
using this:
0 < length init_xs

goal (1 subgoal):
 1. length init_xs - length (y # ys) < length init_xs proof (state)
this:
length init_xs - length (y # ys) < length init_xs

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
length init_xs - length (y # ys) = length ?ys \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (?ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length init_xs - length (y # ys))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' ?ys (xf' s)}) hs y body

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
goal (1 subgoal):
 1. ys = drop (length init_xs - length ys) init_xs proof (prove)
using this:
length init_xs - length ys = Suc (length init_xs - length (y # ys))
y # ys = drop (length init_xs - length (y # ys)) init_xs

goal (1 subgoal):
 1. ys = drop (length init_xs - length ys) init_xs proof (state)
this:
ys = drop (length init_xs - length ys) init_xs

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
length ?zs = length init_xs - length ys \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (?zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length ys)) (Q \<inter> {s. xf s = xfrel (length init_xs - length ys) \<and> r' ?zs (xf' s)}) hs (sequenceE ys) (While {s. P (xf s)} (body;;
\<acute>xf :== xfrel_upd \<acute>xf))

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
\<lbrace>F (length init_xs - length (y # ys))\<rbrace> y \<lbrace>\<lambda>_. F (Suc (length init_xs - length (y # ys)))\<rbrace>, -

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. length zs = length init_xs - length (x1 # xs) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (x1 # xs))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (x1 # xs)) \<and> r' zs (xf' s)}) hs (sequenceE (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
goal (1 subgoal):
 1. \<forall>zs. length zs = length init_xs - length (y # ys) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (y # ys))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)}) hs (sequenceE (y # ys)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
goal (1 subgoal):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - Suc (length ys))) (Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}) hs (doE v <- y;
vs <- sequenceE ys;
returnOk (v # vs)
odE) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
goal (2 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q10 zs) (?Q'10 zs) hs (doE v <- y;
vs <- sequenceE ys;
returnOk (v # vs)
odE) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> ?Q10 zs s \<and> s' \<in> ?Q'10 zs proof (prove)
goal (2 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q10 zs) (?Q'10 zs) hs (doE v <- y;
vs <- sequenceE ys;
returnOk (v # vs)
odE) (IF P \<acute>xf THEN
  body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))
FI)
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> ?Q10 zs s \<and> s' \<in> ?Q'10 zs proof (prove)
goal (2 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q10 zs) (?R'16 zs) hs (doE v <- y;
vs <- sequenceE ys;
returnOk (v # vs)
odE) (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> ?Q10 zs s \<and> s' \<in> ?R'16 zs \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q10 zs) (?R'16 zs) hs (doE v <- y;
vs <- sequenceE ys;
returnOk (v # vs)
odE) (body;;
(Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))))
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> ?Q10 zs s \<and> s' \<in> ?R'16 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (?r'20 zs)) (?xf'20 zs) (inl_rrel (inl_rrel arrel)) axf (?P20 zs) (?P'20 zs) hs y body
 2. \<And>zs rv' t t'. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ceqv \<Gamma> (?xf'20 zs) rv' t t' (Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) (?d'20 zs rv')
 3. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); ?r'20 zs rv rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q20 zs rv) (?Q'20 zs rv rv') hs (doE vs <- sequenceE ys;
returnOk (rv # vs)
odE) (?d'20 zs rv')
 4. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>, -
 5. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (?r'20 zs)) (?xf'20 zs) (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 6. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (?P20 zs and ?R20 zs) s \<and> s' \<in> ?P'20 zs \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (?r'20 zs)) (?xf'20 zs) (inl_rrel arrel) axf (?P20 zs) (?P'20 zs) hs y body
 2. \<And>zs rv' t t'. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ceqv \<Gamma> (?xf'20 zs) rv' t t' (Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) (?d'20 zs rv')
 3. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); ?r'20 zs rv rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q20 zs rv) (?Q'20 zs rv rv') hs (doE vs <- sequenceE ys;
returnOk (rv # vs)
odE) (?d'20 zs rv')
 4. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>, -
 5. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (?r'20 zs)) (?xf'20 zs) (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 6. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (?P20 zs and ?R20 zs) s \<and> s' \<in> ?P'20 zs \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> length init_xs - length (y # ys) = length zs
 2. \<And>zs rv' t t'. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' (Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) (?d'20 zs rv')
 3. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q20 zs rv) (?Q'20 zs rv rv') hs (doE vs <- sequenceE ys;
returnOk (rv # vs)
odE) (?d'20 zs rv')
 4. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>, -
 5. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 6. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (5 subgoals):
 1. \<And>zs rv' t t'. length zs = length init_xs - Suc (length ys) \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' (Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) (?d'20 zs rv')
 2. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q20 zs rv) (?Q'20 zs rv rv') hs (doE vs <- sequenceE ys;
returnOk (rv # vs)
odE) (?d'20 zs rv')
 3. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>, -
 4. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 5. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (4 subgoals):
 1. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q20 zs rv) (?Q'20 zs rv rv') hs (doE vs <- sequenceE ys;
returnOk (rv # vs)
odE) (Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))
 2. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>, -
 3. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 4. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (?Q20 zs rv) (?Q'33 zs rv rv') hs (doE vs <- sequenceE ys;
returnOk (rv # vs)
odE) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))
 2. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) (?Q'33 zs rv rv')
 3. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; ?Q20 zs rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) {s'. (s, s') \<in> sr}
 4. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>, -
 5. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 6. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel \<circ> case_sum Inl (Inr \<circ> (#) rv)) axf (?Q20 zs rv) (?Q'33 zs rv rv') hs (sequenceE ys) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))
 2. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) (?Q'33 zs rv rv')
 3. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; ?Q20 zs rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) {s'. (s, s') \<in> sr}
 4. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>, -
 5. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 6. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (8 subgoals):
 1. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> length (zs @ [rv]) = length init_xs - length ys
 2. \<And>zs rv rv' rva s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; inr_rrel (\<lambda>rva (i', rv'). r' ((zs @ [rv]) @ rva) rv' \<and> i' = xfrel (length init_xs)) rva (xf s, xf' s)\<rbrakk> \<Longrightarrow> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (xf s, xf' s)
 3. \<And>zs rv rv' rva s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; inl_rrel arrel rva (axf s); hs \<noteq> []\<rbrakk> \<Longrightarrow> (inl_rrel arrel \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (axf s)
 4. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) (Q \<inter> {s. xf s = xfrel (length init_xs - length ys) \<and> r' (zs @ [rv]) (xf' s)})
 5. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; F (length init_xs - length ys) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) {s'. (s, s') \<in> sr}
 6. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv. F (length init_xs - length ys)\<rbrace>, -
 7. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 8. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (7 subgoals):
 1. \<And>zs rv rv' rva s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; inr_rrel (\<lambda>rva (i', rv'). r' ((zs @ [rv]) @ rva) rv' \<and> i' = xfrel (length init_xs)) rva (xf s, xf' s)\<rbrakk> \<Longrightarrow> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (xf s, xf' s)
 2. \<And>zs rv rv' rva s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; inl_rrel arrel rva (axf s); hs \<noteq> []\<rbrakk> \<Longrightarrow> (inl_rrel arrel \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (axf s)
 3. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) (Q \<inter> {s. xf s = xfrel (length init_xs - length ys) \<and> r' (zs @ [rv]) (xf' s)})
 4. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; F (length init_xs - length ys) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) {s'. (s, s') \<in> sr}
 5. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv. F (length init_xs - length ys)\<rbrace>, -
 6. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 7. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs rv rv' rva s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; inl_rrel arrel rva (axf s); hs \<noteq> []\<rbrakk> \<Longrightarrow> (inl_rrel arrel \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (axf s)
 2. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) (Q \<inter> {s. xf s = xfrel (length init_xs - length ys) \<and> r' (zs @ [rv]) (xf' s)})
 3. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; F (length init_xs - length ys) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) {s'. (s, s') \<in> sr}
 4. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv. F (length init_xs - length ys)\<rbrace>, -
 5. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 6. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (5 subgoals):
 1. \<And>zs rv rv'. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) (Q \<inter> {s. xf s = xfrel (length init_xs - length ys) \<and> r' (zs @ [rv]) (xf' s)})
 2. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; F (length init_xs - length ys) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) {s'. (s, s') \<in> sr}
 3. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv. F (length init_xs - length ys)\<rbrace>, -
 4. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v. ?Q'20 zs (theRight v))),UNIV
 5. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (4 subgoals):
 1. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; F (length init_xs - length ys) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))} \<inter> {s'. (s, s') \<in> sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) {s'. (s, s') \<in> sr}
 2. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv. F (length init_xs - length ys)\<rbrace>, -
 3. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))})),UNIV
 4. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (5 subgoals):
 1. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; F (length init_xs - length ys) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'135 zs rv rv' s) Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s) {s'. (s, s') \<in> sr}
 2. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; F (length init_xs - length ys) s\<rbrakk> \<Longrightarrow> {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))} \<inter> {s'. (s, s') \<in> sr} \<subseteq> ?P'135 zs rv rv' s
 3. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv. F (length init_xs - length ys)\<rbrace>, -
 4. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))})),UNIV
 5. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (4 subgoals):
 1. \<And>zs rv rv' s. \<lbrakk>length zs = length init_xs - Suc (length ys); r' (zs @ [rv]) rv'; F (length init_xs - length ys) s\<rbrakk> \<Longrightarrow> {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))} \<inter> {s'. (s, s') \<in> sr} \<subseteq> {sa. (s, xf_update (\<lambda>_. xfrel_upd (xf sa)) sa) \<in> sr}
 2. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv. F (length init_xs - length ys)\<rbrace>, -
 3. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))})),UNIV
 4. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv. F (length init_xs - length ys)\<rbrace>, -
 2. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))})),UNIV
 3. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R20 zs) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<lbrace>?R143 zs (?zs143 zs)\<rbrace> y \<lbrace>\<lambda>rv. F (Suc (length init_xs - length (y # ys)))\<rbrace>, -
 2. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))})),UNIV
 3. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and ?R143 zs (?zs143 zs)) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body (ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))})),UNIV
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and F (length init_xs - length (y # ys))) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs. length zs = length init_xs - Suc (length ys) \<Longrightarrow> \<forall>s\<in>Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}. \<exists>P' Q' A'. \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> P' body Q',A' \<and> s \<in> P' \<and> Q' \<subseteq> ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))}) \<and> A' \<subseteq> UNIV
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and F (length init_xs - length (y # ys))) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> (Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}) \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs s. \<lbrakk>length zs = length init_xs - Suc (length ys); s \<in> Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?P'149 zs s) body (?Q'150 zs s),(?A'151 zs s) \<and> s \<in> ?P'149 zs s \<and> ?Q'150 zs s \<subseteq> ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))}) \<and> ?A'151 zs s \<subseteq> UNIV
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and F (length init_xs - length (y # ys))) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> (Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}) \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs s. \<lbrakk>length zs = length init_xs - Suc (length ys); s \<in> Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?P'149 zs s) body (?Q'150 zs s),(?A'151 zs s)
 2. \<And>zs s. \<lbrakk>length zs = length init_xs - Suc (length ys); s \<in> Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}\<rbrakk> \<Longrightarrow> s \<in> ?P'149 zs s \<and> ?Q'150 zs s \<subseteq> ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))}) \<and> ?A'151 zs s \<subseteq> UNIV
 3. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and F (length init_xs - length (y # ys))) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> (Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}) \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs s. \<lbrakk>length zs = length init_xs - Suc (length ys); s \<in> Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}\<rbrakk> \<Longrightarrow> s \<in> Q
 2. \<And>zs s. \<lbrakk>length zs = length init_xs - Suc (length ys); s \<in> Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}\<rbrakk> \<Longrightarrow> s \<in> {s} \<and> Q \<inter> {t. xf t = xf s} \<subseteq> ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))}) \<and> UNIV \<subseteq> UNIV
 3. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and F (length init_xs - length (y # ys))) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> (Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}) \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs s. \<lbrakk>length zs = length init_xs - Suc (length ys); s \<in> Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}\<rbrakk> \<Longrightarrow> s \<in> {s} \<and> Q \<inter> {t. xf t = xf s} \<subseteq> ccHoarePost (inr_rrel (\<lambda>rv. r' (zs @ [rv]))) xf' (\<lambda>v rv'. {s. xf_update (\<lambda>_. xfrel_upd (xf s)) s \<in> Q \<and> xf (xf_update (\<lambda>_. xfrel_upd (xf s)) s) = xfrel (length init_xs - length ys) \<and> r' (zs @ [theRight v]) (xf' (xf_update (\<lambda>_. xfrel_upd (xf s)) s))}) \<and> UNIV \<subseteq> UNIV
 2. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and F (length init_xs - length (y # ys))) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> (Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}) \<inter> {s. P (xf s)} proof (prove)
goal (1 subgoal):
 1. \<And>zs s s'. \<lbrakk>length zs = length init_xs - Suc (length ys); (s, s') \<in> sr; F (length init_xs - Suc (length ys)) s; s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - Suc (length ys)) \<and> r' zs (xf' s)}\<rbrakk> \<Longrightarrow> (F (length init_xs - length (y # ys)) and F (length init_xs - length (y # ys))) s \<and> s' \<in> Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)} \<inter> (Q \<inter> {s. xfrel_upd (xf s) = xfrel (length init_xs - length ys)}) \<inter> {s. P (xf s)} proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>zs. length zs = length init_xs - length (y # ys) \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length (y # ys))) (Q \<inter> {s. xf s = xfrel (length init_xs - length (y # ys)) \<and> r' zs (xf' s)}) hs (sequenceE (y # ys)) (While {s. P (xf s)} (body;;
\<acute>xf :== xfrel_upd \<acute>xf))

goal:
No subgoals! proof (state)
this:
\<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
\<acute>xf :== xfrel_upd \<acute>xf))

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (prove)
using this:
\<forall>zs. length zs = length init_xs - length xs \<longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = xfrel (length init_xs))) (\<lambda>s. (xf s, xf' s)) (inl_rrel arrel) axf (F (length init_xs - length xs)) (Q \<inter> {s. xf s = xfrel (length init_xs - length xs) \<and> r' zs (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
\<acute>xf :== xfrel_upd \<acute>xf))

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s))) proof (state)
this:
ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = xfrel (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = xfrel 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
\<acute>xf :== xfrel_upd \<acute>xf))

goal:
No subgoals!