theory Ipc_C

lemma ccorres_sequenceE_while':
  fixes axf :: "globals myvars \<Rightarrow> 'e" shows
  "\<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow>
        ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (ys @ [rv]) rv')) xf'
                            (inl_rrel arrel) axf
                            (F (length ys)) (Q \<inter> {s. i_' s = of_nat (length ys) \<and> r' ys (xf' s)}) hs
                            (xs ! length ys) body;
    \<And>n. P n = (n < of_nat (length xs));
    \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> {t. i_' t = i_' s}),UNIV;
    \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -;
     length xs < 2 ^ word_bits;
     \<forall>s f. xf' (i_'_update f s) = xf' s
                 \<and> ((i_'_update f s \<in> Q) = (s \<in> Q))
                 \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)) \<rbrakk>
    \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = of_nat (length xs)))
                  (\<lambda>s. (i_' s, xf' s)) arrel axf
                  (F 0) (Q \<inter> {s. r' [] (xf' s)}) hs
          (sequenceE xs)
          (Basic (\<lambda>s. i_'_update (\<lambda>_. 0) s) ;;
           While {s. P (i_' s)} (body;;
             Basic (\<lambda>s. i_'_update (\<lambda>_. i_' s + 1) s)))" apply (rule ccorres_guard_imp2) apply (rule ccorres_symb_exec_r) apply (rule ccorres_rel_imp2) apply (rule ccorres_sequenceE_while_gen'[where i=0, simplified, where xf_update=i_'_update],
              (assumption | simp)+) apply (simp add: word_bits_def) apply simp+ apply vcg apply (rule conseqPre, vcg) apply clarsimp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (length xs))) (\<lambda>s. (i_' s, xf' s)) arrel axf (F 0) (Q \<inter> {s. r' [] (xf' s)}) hs (sequenceE xs) (\<acute>i :== 0;;
While \<lbrace>P \<acute>i\<rbrace> (body;;
\<acute>i :== \<acute>i + 1)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (length xs))) (\<lambda>s. (i_' s, xf' s)) arrel axf ?Q ?Q' hs (sequenceE xs) (\<acute>i :== 0;;
While \<lbrace>P \<acute>i\<rbrace> (body;;
\<acute>i :== \<acute>i + 1))
 2. \<And>s s'. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); (s, s') \<in> sr; F 0 s; s' \<in> Q \<inter> {s. r' [] (xf' s)}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (length xs))) (\<lambda>s. (i_' s, xf' s)) arrel axf ?Q ?Q'3 hs (sequenceE xs) (While \<lbrace>P \<acute>i\<rbrace> (body;;
\<acute>i :== \<acute>i + 1))
 2. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q' \<acute>i :== 0 ?Q'3
 3. \<And>s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); ?Q s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q' \<inter> {s'. (s, s') \<in> sr}) \<acute>i :== 0 {s'. (s, s') \<in> sr}
 4. \<And>s s'. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); (s, s') \<in> sr; F 0 s; s' \<in> Q \<inter> {s. r' [] (xf' s)}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> ?r'7 ?xf'7 ?arrel'7 ?axf'7 ?Q ?Q'3 hs (sequenceE xs) (While \<lbrace>P \<acute>i\<rbrace> (body;;
\<acute>i :== \<acute>i + 1))
 2. \<And>rv s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); ?r'7 rv (?xf'7 s)\<rbrakk> \<Longrightarrow> inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (length xs)) rv (i_' s, xf' s)
 3. \<And>rv s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); ?arrel'7 rv (?axf'7 s); hs \<noteq> []\<rbrakk> \<Longrightarrow> arrel rv (axf s)
 4. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q' \<acute>i :== 0 ?Q'3
 5. \<And>s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); ?Q s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q' \<inter> {s'. (s, s') \<in> sr}) \<acute>i :== 0 {s'. (s, s') \<in> sr}
 6. \<And>s s'. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); (s, s') \<in> sr; F 0 s; s' \<in> Q \<inter> {s. r' [] (xf' s)}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (8 subgoals):
 1. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> length xs < 4294967296
 2. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> \<forall>s f. i_' (i_'_update f s) = f (i_' s)
 3. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))
 4. \<And>rv s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (0 + length xs)) rv (i_' s, xf' s)\<rbrakk> \<Longrightarrow> inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (length xs)) rv (i_' s, xf' s)
 5. \<And>rv s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); arrel rv (axf s); hs \<noteq> []\<rbrakk> \<Longrightarrow> arrel rv (axf s)
 6. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q' \<acute>i :== 0 (Q \<inter> {s. i_' s = 0 \<and> r' [] (xf' s)})
 7. \<And>s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); F 0 s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q' \<inter> {s'. (s, s') \<in> sr}) \<acute>i :== 0 {s'. (s, s') \<in> sr}
 8. \<And>s s'. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); (s, s') \<in> sr; F 0 s; s' \<in> Q \<inter> {s. r' [] (xf' s)}\<rbrakk> \<Longrightarrow> F 0 s \<and> s' \<in> ?Q' proof (prove)
goal (7 subgoals):
 1. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> \<forall>s f. i_' (i_'_update f s) = f (i_' s)
 2. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))
 3. \<And>rv s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (0 + length xs)) rv (i_' s, xf' s)\<rbrakk> \<Longrightarrow> inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (length xs)) rv (i_' s, xf' s)
 4. \<And>rv s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); arrel rv (axf s); hs \<noteq> []\<rbrakk> \<Longrightarrow> arrel rv (axf s)
 5. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q' \<acute>i :== 0 (Q \<inter> {s. i_' s = 0 \<and> r' [] (xf' s)})
 6. \<And>s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); F 0 s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q' \<inter> {s'. (s, s') \<in> sr}) \<acute>i :== 0 {s'. (s, s') \<in> sr}
 7. \<And>s s'. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); (s, s') \<in> sr; F 0 s; s' \<in> Q \<inter> {s. r' [] (xf' s)}\<rbrakk> \<Longrightarrow> F 0 s \<and> s' \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ?Q' \<acute>i :== 0 (Q \<inter> {s. i_' s = 0 \<and> r' [] (xf' s)})
 2. \<And>s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); F 0 s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q' \<inter> {s'. (s, s') \<in> sr}) \<acute>i :== 0 {s'. (s, s') \<in> sr}
 3. \<And>s s'. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); (s, s') \<in> sr; F 0 s; s' \<in> Q \<inter> {s. r' [] (xf' s)}\<rbrakk> \<Longrightarrow> F 0 s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); F 0 s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({s. i_'_update (\<lambda>_. 0) s \<in> Q \<and> 0 = 0 \<and> r' [] (xf' (i_'_update (\<lambda>_. 0) s))} \<inter> {s'. (s, s') \<in> sr}) \<acute>i :== 0 {s'. (s, s') \<in> sr}
 2. \<And>s s'. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); (s, s') \<in> sr; F 0 s; s' \<in> Q \<inter> {s. r' [] (xf' s)}\<rbrakk> \<Longrightarrow> F 0 s \<and> s' \<in> {s. i_'_update (\<lambda>_. 0) s \<in> Q \<and> 0 = 0 \<and> r' [] (xf' (i_'_update (\<lambda>_. 0) s))} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); F 0 s\<rbrakk> \<Longrightarrow> {s. i_'_update (\<lambda>_. 0) s \<in> Q \<and> 0 = 0 \<and> r' [] (xf' (i_'_update (\<lambda>_. 0) s))} \<inter> {s'. (s, s') \<in> sr} \<subseteq> {sa. (s, i_'_update (\<lambda>_. 0) sa) \<in> sr}
 2. \<And>s s'. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); (s, s') \<in> sr; F 0 s; s' \<in> Q \<inter> {s. r' [] (xf' s)}\<rbrakk> \<Longrightarrow> F 0 s \<and> s' \<in> {s. i_'_update (\<lambda>_. 0) s \<in> Q \<and> 0 = 0 \<and> r' [] (xf' (i_'_update (\<lambda>_. 0) s))} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>ys. length ys < length xs \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv. r' (ys @ [rv]))) xf' (inl_rrel arrel) axf (F (length ys)) (Q \<inter> {s. i_' s = word_of_nat (length ys) \<and> r' ys (xf' s)}) hs (xs ! length ys) body; \<And>n. P n = (n < word_of_nat (length xs)); \<And>s. s \<in> Q \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> \<lbrace>\<acute>i = \<^bsup>s\<^esup>i\<rbrace>),UNIV; \<And>n. n < length xs \<Longrightarrow> \<lbrace>F n\<rbrace> xs ! n \<lbrace>\<lambda>_. F (Suc n)\<rbrace>, -; length xs < 2 ^ word_bits; \<forall>s f. xf' (i_'_update f s) = xf' s \<and> (i_'_update f s \<in> Q) = (s \<in> Q) \<and> (\<forall>s'. ((s', i_'_update f s) \<in> sr) = ((s', s) \<in> sr)); (s, s') \<in> sr; F 0 s; s' \<in> Q \<inter> {s. r' [] (xf' s)}\<rbrakk> \<Longrightarrow> F 0 s \<and> s' \<in> {s. i_'_update (\<lambda>_. 0) s \<in> Q \<and> 0 = 0 \<and> r' [] (xf' (i_'_update (\<lambda>_. 0) s))} proof (prove)
goal:
No subgoals!