theory Ctac

lemma sequenceE_simpl_sequence_nth_corres':
  "\<lbrakk> length xs = length ys;
    \<And>zs. length zs < length xs \<Longrightarrow>
        ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (prev_xs @ zs @ [rv]) rv')) xf'
                            (inl_rrel arrel) axf
                            (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs
                            (xs ! length zs) (f (ys ! length zs));
    \<And>s \<sigma>. s \<in> Q \<Longrightarrow> P \<sigma> \<Longrightarrow>
        (\<sigma>, s) \<in> sr \<Longrightarrow> \<forall>y \<in> set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} (f y) Q,UNIV;
    \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -
    \<rbrakk>
    \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (prev_xs @ rv) rv')) xf'
                  (inl_rrel arrel) axf
                  (\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs
          (sequenceE xs)
          (simpl_sequence f ys)" proof (induct xs ys arbitrary: prev_xs rule: list_induct2) case Nil show ?case apply (simp add: sequenceE_def simpl_sequence_def) apply (rule ccorres_guard_imp2, rule ccorres_returnOk_skip) apply simp done next case (Cons x xs y ys) show ?case apply (simp add: simpl_sequence_Cons sequenceE_Cons) apply (rule ccorres_guard_imp2) apply (rule ccorres_splitE) apply simp apply (rule Cons.prems(1)[where zs=Nil, simplified]) apply (rule ceqv_refl) apply (simp add: liftME_def[symmetric] liftME_liftM) apply (rule ccorres_rel_imp2, rule Cons.hyps(2)[where prev_xs="prev_xs @ [rv]" for rv]) apply (rule ccorres_guard_imp2, rule ccorres_rel_imp2,
             rule Cons.prems(1)[where zs="z # zs" for z zs, simplified]) apply simp+ apply (blast dest: Cons.prems[simplified]) apply simp apply (cut_tac n="Suc n" in Cons.prems(3), simp, simp) apply (clarsimp elim!: inl_inrE) apply assumption apply (clarsimp elim!: inl_inrE) apply simp apply (rule hoare_vcg_const_imp_lift_R) apply (rule hoare_gen_asmE) apply (erule Cons.prems(3)[where n=0, simplified]) apply (rule_tac P="Q \<inter> {s. \<exists>\<sigma>. P \<sigma> \<and> (\<sigma>, s) \<in> sr}"
         in HoarePartial.conseq_exploit_pre) apply (clarsimp, rule conseqPost, rule Cons.prems(2)[simplified, THEN conjunct1],
       simp+) apply (clarsimp simp: ccHoarePost_def elim!: inl_inrE) apply simp apply auto done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; \<And>zs. length zs < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs (xs ! length zs) (f (ys ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE xs) (simpl_sequence f ys) proof (state)
goal (2 subgoals):
 1. \<And>prev_xs. \<lbrakk>\<And>zs. length zs < length [] \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs ([] ! length zs) (f ([] ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set []. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length [] \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> [] ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. [] \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE []) (simpl_sequence f [])
 2. \<And>x xs y ys prev_xs. \<lbrakk>length xs = length ys; \<And>prev_xs. \<lbrakk>\<And>zs. length zs < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs (xs ! length zs) (f (ys ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE xs) (simpl_sequence f ys); \<And>zs. length zs < length (x # xs) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs ((x # xs) ! length zs) (f ((y # ys) ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (y # ys). \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length (x # xs) \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> (x # xs) ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. x # xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE (x # xs)) (simpl_sequence f (y # ys)) proof (state)
this:
length ?zs < length [] \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ ?zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length ?zs)) (Q \<inter> {s. r' (prev_xs @ ?zs) (xf' s)}) hs ([] ! length ?zs) (f ([] ! length ?zs))
\<lbrakk>?s \<in> Q; P ?\<sigma>; (?\<sigma>, ?s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set []. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {?s} f y Q,UNIV
Suc ?n < length [] \<Longrightarrow> \<lbrace>P and F (length prev_xs + ?n)\<rbrace> [] ! ?n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc ?n)\<rbrace>, -

goal (2 subgoals):
 1. \<And>prev_xs. \<lbrakk>\<And>zs. length zs < length [] \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs ([] ! length zs) (f ([] ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set []. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length [] \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> [] ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. [] \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE []) (simpl_sequence f [])
 2. \<And>x xs y ys prev_xs. \<lbrakk>length xs = length ys; \<And>prev_xs. \<lbrakk>\<And>zs. length zs < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs (xs ! length zs) (f (ys ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE xs) (simpl_sequence f ys); \<And>zs. length zs < length (x # xs) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs ((x # xs) ! length zs) (f ((y # ys) ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (y # ys). \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length (x # xs) \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> (x # xs) ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. x # xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE (x # xs)) (simpl_sequence f (y # ys)) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. [] \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE []) (simpl_sequence f []) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. True) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (returnOk []) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; True; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. inr_rrel (\<lambda>rv. r' (prev_xs @ rv)) (Inr []) (xf' s)} proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. [] \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE []) (simpl_sequence f [])

goal (1 subgoal):
 1. \<And>x xs y ys prev_xs. \<lbrakk>length xs = length ys; \<And>prev_xs. \<lbrakk>\<And>zs. length zs < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs (xs ! length zs) (f (ys ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE xs) (simpl_sequence f ys); \<And>zs. length zs < length (x # xs) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs ((x # xs) ! length zs) (f ((y # ys) ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (y # ys). \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length (x # xs) \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> (x # xs) ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. x # xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE (x # xs)) (simpl_sequence f (y # ys)) proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys prev_xs. \<lbrakk>length xs = length ys; \<And>prev_xs. \<lbrakk>\<And>zs. length zs < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs (xs ! length zs) (f (ys ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE xs) (simpl_sequence f ys); \<And>zs. length zs < length (x # xs) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs ((x # xs) ! length zs) (f ((y # ys) ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (y # ys). \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length (x # xs) \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> (x # xs) ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. x # xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE (x # xs)) (simpl_sequence f (y # ys)) proof (state)
this:
length xs = length ys
\<lbrakk>\<And>zs. length zs < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (?prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length ?prev_xs + length zs)) (Q \<inter> {s. r' (?prev_xs @ zs) (xf' s)}) hs (xs ! length zs) (f (ys ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length ?prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length ?prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (?prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length ?prev_xs) s) (Q \<inter> {s. r' ?prev_xs (xf' s)}) hs (sequenceE xs) (simpl_sequence f ys)
length ?zs < length (x # xs) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ ?zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length ?zs)) (Q \<inter> {s. r' (prev_xs @ ?zs) (xf' s)}) hs ((x # xs) ! length ?zs) (f ((y # ys) ! length ?zs))
\<lbrakk>?s \<in> Q; P ?\<sigma>; (?\<sigma>, ?s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (y # ys). \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {?s} f y Q,UNIV
Suc ?n < length (x # xs) \<Longrightarrow> \<lbrace>P and F (length prev_xs + ?n)\<rbrace> (x # xs) ! ?n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc ?n)\<rbrace>, -

goal (1 subgoal):
 1. \<And>x xs y ys prev_xs. \<lbrakk>length xs = length ys; \<And>prev_xs. \<lbrakk>\<And>zs. length zs < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs (xs ! length zs) (f (ys ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE xs) (simpl_sequence f ys); \<And>zs. length zs < length (x # xs) \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ zs @ [rv]))) xf' (inl_rrel arrel) axf (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs ((x # xs) ! length zs) (f ((y # ys) ! length zs)); \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (y # ys). \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV; \<And>n. Suc n < length (x # xs) \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> (x # xs) ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, -\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. x # xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE (x # xs)) (simpl_sequence f (y # ys)) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. x # xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE (x # xs)) (simpl_sequence f (y # ys)) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (doE v <- x;
vs <- sequenceE xs;
returnOk (v # vs)
odE) (f y;;
simpl_sequence f ys) proof (prove)
goal (2 subgoals):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf ?Q9 ?Q'9 hs (doE v <- x;
vs <- sequenceE xs;
returnOk (v # vs)
odE) (f y;;
simpl_sequence f ys)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (6 subgoals):
 1. ccorres_underlying sr \<Gamma> (inr_rrel ?r'12) ?xf'12 (inl_rrel (inl_rrel arrel)) axf ?P12 ?P'12 hs x (f y)
 2. \<And>rv' t t'. ceqv \<Gamma> ?xf'12 rv' t t' (simpl_sequence f ys) (?d'12 rv')
 3. \<And>rv rv'. ?r'12 rv rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (?Q12 rv) (?Q'12 rv rv') hs (doE vs <- sequenceE xs;
returnOk (rv # vs)
odE) (?d'12 rv')
 4. \<lbrace>?R12\<rbrace> x \<lbrace>?Q12\<rbrace>, -
 5. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel ?r'12) ?xf'12 (\<lambda>v. ?Q'12 (theRight v))),UNIV
 6. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> (?P12 and ?R12) s \<and> s' \<in> ?P'12 \<inter> ?R'12 proof (prove)
goal (6 subgoals):
 1. ccorres_underlying sr \<Gamma> (inr_rrel ?r'12) ?xf'12 (inl_rrel arrel) axf ?P12 ?P'12 hs x (f y)
 2. \<And>rv' t t'. ceqv \<Gamma> ?xf'12 rv' t t' (simpl_sequence f ys) (?d'12 rv')
 3. \<And>rv rv'. ?r'12 rv rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (?Q12 rv) (?Q'12 rv rv') hs (doE vs <- sequenceE xs;
returnOk (rv # vs)
odE) (?d'12 rv')
 4. \<lbrace>?R12\<rbrace> x \<lbrace>?Q12\<rbrace>, -
 5. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel ?r'12) ?xf'12 (\<lambda>v. ?Q'12 (theRight v))),UNIV
 6. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> (?P12 and ?R12) s \<and> s' \<in> ?P'12 \<inter> ?R'12 proof (prove)
goal (5 subgoals):
 1. \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' (simpl_sequence f ys) (?d'12 rv')
 2. \<And>rv rv'. r' (prev_xs @ [] @ [rv]) rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (?Q12 rv) (?Q'12 rv rv') hs (doE vs <- sequenceE xs;
returnOk (rv # vs)
odE) (?d'12 rv')
 3. \<lbrace>?R12\<rbrace> x \<lbrace>?Q12\<rbrace>, -
 4. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v. ?Q'12 (theRight v))),UNIV
 5. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. r' (prev_xs @ [] @ [rv]) rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (?Q12 rv) (?Q'12 rv rv') hs (doE vs <- sequenceE xs;
returnOk (rv # vs)
odE) (simpl_sequence f ys)
 2. \<lbrace>?R12\<rbrace> x \<lbrace>?Q12\<rbrace>, -
 3. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v. ?Q'12 (theRight v))),UNIV
 4. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. r' (prev_xs @ [rv]) rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) xf' (inl_rrel arrel \<circ> case_sum Inl (Inr \<circ> (#) rv)) axf (?Q12 rv) (?Q'12 rv rv') hs (sequenceE xs) (simpl_sequence f ys)
 2. \<lbrace>?R12\<rbrace> x \<lbrace>?Q12\<rbrace>, -
 3. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v. ?Q'12 (theRight v))),UNIV
 4. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' zs. \<lbrakk>r' (prev_xs @ [rv]) rv'; length zs < length xs\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rva. r' ((prev_xs @ [?rv32 rv]) @ zs @ [rva]))) xf' (inl_rrel arrel) axf (P and F (length (prev_xs @ [?rv32 rv]) + length zs)) (Q \<inter> {s. r' ((prev_xs @ [?rv32 rv]) @ zs) (xf' s)}) hs (xs ! length zs) (f (ys ! length zs))
 2. \<And>rv rv' s \<sigma>. \<lbrakk>r' (prev_xs @ [rv]) rv'; s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV
 3. \<And>rv rv' n. \<lbrakk>r' (prev_xs @ [rv]) rv'; Suc n < length xs\<rbrakk> \<Longrightarrow> \<lbrace>P and F (length (prev_xs @ [?rv32 rv]) + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length (prev_xs @ [?rv32 rv]) + Suc n)\<rbrace>, -
 4. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [rv]) rv'; inr_rrel (\<lambda>rva. r' ((prev_xs @ [?rv32 rv]) @ rva)) rva (xf' s)\<rbrakk> \<Longrightarrow> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (xf' s)
 5. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [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)
 6. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length (prev_xs @ [?rv32 rv])) s\<rbrace>, -
 7. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [?rv32 (theRight v)]) (xf' s)})),UNIV
 8. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (11 subgoals):
 1. \<And>rv rv' zs. \<lbrakk>r' (prev_xs @ [rv]) rv'; length zs < length xs\<rbrakk> \<Longrightarrow> length zs < length xs
 2. \<And>rv rv' zs rva s. \<lbrakk>r' (prev_xs @ [rv]) rv'; length zs < length xs; inr_rrel (\<lambda>rva. r' (prev_xs @ (?z45 rv rv' zs # zs) @ [rva])) rva (xf' s)\<rbrakk> \<Longrightarrow> inr_rrel (\<lambda>rva. r' ((prev_xs @ [?rv32 rv]) @ zs @ [rva])) rva (xf' s)
 3. \<And>rv rv' zs rva s. \<lbrakk>r' (prev_xs @ [rv]) rv'; length zs < length xs; inl_rrel arrel rva (axf s); hs \<noteq> []\<rbrakk> \<Longrightarrow> inl_rrel arrel rva (axf s)
 4. \<And>rv rv' zs s s'. \<lbrakk>r' (prev_xs @ [rv]) rv'; length zs < length xs; (s, s') \<in> sr; (P and F (length (prev_xs @ [?rv32 rv]) + length zs)) s; s' \<in> Q \<inter> {s. r' ((prev_xs @ [?rv32 rv]) @ zs) (xf' s)}\<rbrakk> \<Longrightarrow> (P s \<and> F (Suc (length prev_xs + length zs)) s) \<and> s' \<in> Q \<inter> {s. r' (prev_xs @ ?z45 rv rv' zs # zs) (xf' s)}
 5. \<And>rv rv' s \<sigma>. \<lbrakk>r' (prev_xs @ [rv]) rv'; s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV
 6. \<And>rv rv' n. \<lbrakk>r' (prev_xs @ [rv]) rv'; Suc n < length xs\<rbrakk> \<Longrightarrow> \<lbrace>P and F (length (prev_xs @ [?rv32 rv]) + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length (prev_xs @ [?rv32 rv]) + Suc n)\<rbrace>, -
 7. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [rv]) rv'; inr_rrel (\<lambda>rva. r' ((prev_xs @ [?rv32 rv]) @ rva)) rva (xf' s)\<rbrakk> \<Longrightarrow> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (xf' s)
 8. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [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)
 9. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length (prev_xs @ [?rv32 rv])) s\<rbrace>, -
 10. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [?rv32 (theRight v)]) (xf' s)})),UNIV
A total of 11 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' s \<sigma>. \<lbrakk>r' (prev_xs @ [rv]) rv'; s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> \<forall>y\<in>set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} f y Q,UNIV
 2. \<And>rv rv' n. \<lbrakk>r' (prev_xs @ [rv]) rv'; Suc n < length xs\<rbrakk> \<Longrightarrow> \<lbrace>P and F (length (prev_xs @ [?rv32 rv]) + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length (prev_xs @ [?rv32 rv]) + Suc n)\<rbrace>, -
 3. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [rv]) rv'; inr_rrel (\<lambda>rva. r' ((prev_xs @ [?rv32 rv]) @ rva)) rva (xf' s)\<rbrakk> \<Longrightarrow> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (xf' s)
 4. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [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)
 5. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length (prev_xs @ [?rv32 rv])) s\<rbrace>, -
 6. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [?rv32 (theRight v)]) (xf' s)})),UNIV
 7. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' n. \<lbrakk>r' (prev_xs @ [rv]) rv'; Suc n < length xs\<rbrakk> \<Longrightarrow> \<lbrace>P and F (length (prev_xs @ [?rv32 rv]) + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length (prev_xs @ [?rv32 rv]) + Suc n)\<rbrace>, -
 2. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [rv]) rv'; inr_rrel (\<lambda>rva. r' ((prev_xs @ [?rv32 rv]) @ rva)) rva (xf' s)\<rbrakk> \<Longrightarrow> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (xf' s)
 3. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [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. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length (prev_xs @ [?rv32 rv])) s\<rbrace>, -
 5. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [?rv32 (theRight v)]) (xf' s)})),UNIV
 6. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' n. \<lbrakk>r' (prev_xs @ [rv]) rv'; Suc n < length xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. P a \<and> F (Suc (length prev_xs + n)) a\<rbrace> xs ! n \<lbrace>\<lambda>_ a. P a \<and> F (Suc (Suc (length prev_xs + n))) a\<rbrace>, -
 2. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [rv]) rv'; inr_rrel (\<lambda>rva. r' ((prev_xs @ [?rv32 rv]) @ rva)) rva (xf' s)\<rbrakk> \<Longrightarrow> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (xf' s)
 3. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [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. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length (prev_xs @ [?rv32 rv])) s\<rbrace>, -
 5. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [?rv32 (theRight v)]) (xf' s)})),UNIV
 6. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [rv]) rv'; inr_rrel (\<lambda>rva. r' ((prev_xs @ [?rv32 rv]) @ rva)) rva (xf' s)\<rbrakk> \<Longrightarrow> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv)) \<circ> case_sum Inl (Inr \<circ> (#) rv)) rva (xf' s)
 2. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [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. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length (prev_xs @ [?rv32 rv])) s\<rbrace>, -
 4. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [?rv32 (theRight v)]) (xf' s)})),UNIV
 5. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' s r. \<lbrakk>r' (prev_xs @ [rv]) rv'; r' (prev_xs @ ?rv32 rv # r) (xf' s)\<rbrakk> \<Longrightarrow> r' (prev_xs @ rv # r) (xf' s)
 2. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [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. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length (prev_xs @ [?rv32 rv])) s\<rbrace>, -
 4. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [?rv32 (theRight v)]) (xf' s)})),UNIV
 5. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' rva s. \<lbrakk>r' (prev_xs @ [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. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length (prev_xs @ [rv])) s\<rbrace>, -
 3. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [theRight v]) (xf' s)})),UNIV
 4. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length (prev_xs @ [rv])) s\<rbrace>, -
 2. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [theRight v]) (xf' s)})),UNIV
 3. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R12\<rbrace> x \<lbrace>\<lambda>rv s. xs \<noteq> [] \<longrightarrow> P s \<and> F (Suc (length prev_xs)) s\<rbrace>, -
 2. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [theRight v]) (xf' s)})),UNIV
 3. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and ?R12) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (3 subgoals):
 1. xs \<noteq> [] \<Longrightarrow> \<lbrace>?Q71\<rbrace> x \<lbrace>\<lambda>rv s. P s \<and> F (Suc (length prev_xs)) s\<rbrace>, -
 2. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [theRight v]) (xf' s)})),UNIV
 3. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and (\<lambda>s. xs \<noteq> [] \<longrightarrow> ?Q71 s)) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>xs \<noteq> []; ?P73\<rbrakk> \<Longrightarrow> \<lbrace>?P'73\<rbrace> x \<lbrace>\<lambda>rv s. P s \<and> F (Suc (length prev_xs)) s\<rbrace>, -
 2. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [theRight v]) (xf' s)})),UNIV
 3. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and (\<lambda>s. xs \<noteq> [] \<longrightarrow> (?P'73 and K ?P73) s)) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ?R'12 f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [theRight v]) (xf' s)})),UNIV
 2. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and (\<lambda>s. xs \<noteq> [] \<longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and K ?P73) s)) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> ?R'12 proof (prove)
goal (2 subgoals):
 1. \<forall>s\<in>Q \<inter> {s. \<exists>\<sigma>. P \<sigma> \<and> (\<sigma>, s) \<in> sr}. \<Gamma>\<turnstile>\<^bsub>/?F12\<^esub> ({s} \<inter> (Q \<inter> {s. \<exists>\<sigma>. P \<sigma> \<and> (\<sigma>, s) \<in> sr})) f y (ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [] @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [theRight v]) (xf' s)})),UNIV
 2. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and (\<lambda>s. xs \<noteq> [] \<longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and K ?P73) s)) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> (Q \<inter> {s. \<exists>\<sigma>. P \<sigma> \<and> (\<sigma>, s) \<in> sr}) proof (prove)
goal (3 subgoals):
 1. \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> Q \<subseteq> ccHoarePost (inr_rrel (\<lambda>rv. r' (prev_xs @ [rv]))) xf' (\<lambda>v rv'. Q \<inter> {s. r' (prev_xs @ [theRight v]) (xf' s)})
 2. \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> UNIV \<subseteq> UNIV
 3. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and (\<lambda>s. xs \<noteq> [] \<longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and K ?P73) s)) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> (Q \<inter> {s. \<exists>\<sigma>. P \<sigma> \<and> (\<sigma>, s) \<in> sr}) proof (prove)
goal (2 subgoals):
 1. \<And>s \<sigma>. \<lbrakk>s \<in> Q; P \<sigma>; (\<sigma>, s) \<in> sr\<rbrakk> \<Longrightarrow> UNIV \<subseteq> UNIV
 2. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and (\<lambda>s. xs \<noteq> [] \<longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and K ?P73) s)) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> (Q \<inter> {s. \<exists>\<sigma>. P \<sigma> \<and> (\<sigma>, s) \<in> sr}) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> F (length prev_xs) s; s' \<in> Q \<inter> {s. r' prev_xs (xf' s)}\<rbrakk> \<Longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and (\<lambda>s. xs \<noteq> [] \<longrightarrow> ((\<lambda>a. P a \<and> F (length prev_xs) a) and K ?P73) s)) s \<and> s' \<in> Q \<inter> {s. r' prev_xs (xf' s)} \<inter> (Q \<inter> {s. \<exists>\<sigma>. P \<sigma> \<and> (\<sigma>, s) \<in> sr}) proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (prev_xs @ rv))) xf' (inl_rrel arrel) axf (\<lambda>s. x # xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs (sequenceE (x # xs)) (simpl_sequence f (y # ys))

goal:
No subgoals!