theory CCorresLemmas

lemma ccorres_sequence_while_genQ':
  fixes i :: "nat" and xf :: "('s, 't) state_scheme \<Rightarrow> ('c :: len) word"
  assumes one: "\<And>n ys. \<lbrakk> n < length xs \<rbrakk> \<Longrightarrow>
                    ccorresG rf_sr \<Gamma> (\<lambda>rv rv'. r' (ys @ [rv]) rv') xf'
                            (F (n * j)) ({s. xf s = of_nat (i + n * j) \<and> r' ys (xf' s)} \<inter> Q) hs
                            (xs ! n) body"
  and      pn: "\<And>n. P n = (n < of_nat (i + length xs * j))"
  and   bodyi: "\<forall>s. xf s < of_nat (i + length xs * j)
    \<longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>_. xf t + of_nat j) t \<in> Q}"
  and      hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace> F (n * j) \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>"
  and     lxs: "i + length xs * j < 2 ^ len_of TYPE('c)"
  and      xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s"
  and     xf': "\<forall>s f. xf' (xf_update f s) = (xf' s)"
  and rf_sr_xf: "\<And>s r f. (s, r) \<in> rf_sr \<Longrightarrow> (s, xf_update f r) \<in> rf_sr"
  and       j: " j > 0"
  shows  "ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = of_nat (i + length xs * of_nat j))
                  (\<lambda>s. (xf s, xf' s))
                  (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs
                  (sequence xs)
                  (While {s. P (xf s)}
                     (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))"
  (is "ccorresG rf_sr \<Gamma> ?r' ?xf' ?G (?G' \<inter> _) hs (sequence 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] note lxs' = lxs [folded init_xs_def] let ?Q  = "\<lambda>xs s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s" let ?Q' = "\<lambda>xs zs. {s. (xf s) = of_nat (i + (length init_xs - length xs) * j)
                         \<and> r' zs (xf' s)} \<inter> Q" let ?r'' = "\<lambda>zs rv (i', rv'). r' (zs @ rv) rv'
                   \<and> i' = of_nat (i + length init_xs * j)" have "\<forall>zs. ccorresG rf_sr \<Gamma> (?r'' zs) ?xf'
             (?Q xs) (?Q' xs zs) hs
             (sequence xs) ?body" using rl proof (induct xs) case Nil thus ?case apply clarsimp apply (rule iffD1 [OF ccorres_expand_while_iff]) apply (simp add: sequence_def ccorres_cond_iffs) 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' [where n="(length init_xs - length (y # ys))", folded yv] from Cons.prems have neq_Nil: "init_xs \<noteq> []" by clarsimp with ly have ys_xs: "length ys < length init_xs" by clarsimp hence hi''':
      "ys\<noteq>[] \<Longrightarrow>
      \<lbrace>F ((length init_xs - length (y # ys)) * j)\<rbrace> y \<lbrace>\<lambda>_. F (Suc (length init_xs - length (y # ys)) * j)\<rbrace>" apply - apply (rule hi'') apply simp apply (clarsimp simp: neq_Nil_conv) apply arith done show ?case using lxs' apply (clarsimp simp: sequence_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_split_nothrow) apply (rule_tac ys="zs" in one'') apply (rule ceqv_refl) apply (rule ccorres_symb_exec_r) apply (simp only: liftM_def[symmetric] ccorres_liftM_simp
                             o_def) apply (rule ccorres_rel_imp, rule_tac zs="zs @ [rv]" in ih) apply clarsimp apply vcg apply (rule conseqPre) apply vcg apply (clarsimp simp: xf rf_sr_xf) apply (subst ln) apply (rule hoare_impI) apply (rule hi''') apply simp apply (simp add: xf') apply (rule HoarePartialDef.Conseq [where P = "{s. P (xf s) \<and> xf s + of_nat j = of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q"]) apply (intro ballI exI) apply (rule conjI) apply (rule_tac s=s in bodyi[rule_format]) apply (clarsimp simp: pn) apply (clarsimp simp: xf) apply (clarsimp simp: ln pn') apply (subst of_nat_mult [symmetric])+ apply (subst of_nat_add [symmetric])+ apply (rule of_nat_mono_maybe) apply (simp add: word_bits_conv) apply (simp add: j) apply (rule diff_Suc_less [OF lt0]) done qed thus ?thesis using lxs j pn apply (auto simp: init_xs_def word_less_nat_alt neq_Nil_conv unat_word_ariths unat_of_nat push_mods
                elim!: ccorres_guard_imp2
                dest!: spec[where x=Nil]
                cong: ccorres_all_cong) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
this:
init_xs \<equiv> xs

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) 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. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
this:
P ?n = (?n < word_of_nat (i + length init_xs * j))

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
this:
?n < length init_xs \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv. r' (?ys @ [rv])) xf' (F (?n * j)) ({s. xf s = word_of_nat (i + ?n * j) \<and> r' ?ys (xf' s)} \<inter> Q) hs (init_xs ! ?n) body

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
this:
Suc ?n < length init_xs \<Longrightarrow> \<lbrace>F (?n * j)\<rbrace> init_xs ! ?n \<lbrace>\<lambda>_. F (Suc ?n * j)\<rbrace>

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
this:
i + length init_xs * j < 2 ^ LENGTH('c)

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (1 subgoal):
 1. \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
using this:
xs = drop (length init_xs - length xs) init_xs

goal (1 subgoal):
 1. \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
goal (2 subgoals):
 1. [] = drop (length init_xs - length []) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. [] \<noteq> [] \<longrightarrow> F ((length init_xs - length []) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length []) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence []) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) 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. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. [] \<noteq> [] \<longrightarrow> F ((length init_xs - length []) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length []) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence []) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
using this:
[] = drop (length init_xs - length []) init_xs

goal (1 subgoal):
 1. \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. [] \<noteq> [] \<longrightarrow> F ((length init_xs - length []) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length []) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence []) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (1 subgoal):
 1. \<And>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. True) ({s. xf s = word_of_nat i + word_of_nat (length init_xs) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence []) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (1 subgoal):
 1. \<And>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. True) ({s. xf s = word_of_nat i + word_of_nat (length init_xs) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence []) (IF P \<acute>xf THEN
  body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))
FI) proof (prove)
goal (1 subgoal):
 1. \<And>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. True) ({s. xf s = word_of_nat i + word_of_nat (length init_xs) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q) hs (return []) (IF P \<acute>xf THEN
  body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))
FI) proof (prove)
goal (2 subgoals):
 1. \<And>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q13 zs) (?Q'13 zs) hs (return []) (IF P \<acute>xf THEN
  body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))
FI)
 2. \<And>zs s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> ?Q13 zs s \<and> s' \<in> ?Q'13 zs proof (prove)
goal (2 subgoals):
 1. \<And>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q13 zs) (?R'16 zs) hs (return []) SKIP
 2. \<And>zs s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<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>(s, s') \<in> rf_sr; True; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> True \<and> s' \<in> UNIV \<inter> {s. case (xf s, xf' s) of (i', rv') \<Rightarrow> r' (zs @ []) rv' \<and> i' = word_of_nat (i + length init_xs * j)} \<inter> - {s. P (xf s)} proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. [] \<noteq> [] \<longrightarrow> F ((length init_xs - length []) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length []) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence []) (While {s. P (xf s)} (body;;
\<acute>xf :== \<acute>xf + word_of_nat j))

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
this:
ys = drop (length init_xs - length ys) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence ys) (While {s. P (xf s)} (body;;
\<acute>xf :== \<acute>xf + word_of_nat j))
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. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) 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. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) 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. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) 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. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) 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. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) 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. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
this:
ccorresG rf_sr \<Gamma> (\<lambda>rv. r' (?ys @ [rv])) xf' (F ((length init_xs - length (y # ys)) * j)) ({s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' ?ys (xf' s)} \<inter> Q) hs y body

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) 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. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
this:
ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (?zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' ?zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence ys) (While {s. P (xf s)} (body;;
\<acute>xf :== \<acute>xf + word_of_nat j))

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (state)
this:
Suc (length init_xs - length (y # ys)) < length init_xs \<Longrightarrow> \<lbrace>F ((length init_xs - length (y # ys)) * j)\<rbrace> y \<lbrace>\<lambda>_. F (Suc (length init_xs - length (y # ys)) * j)\<rbrace>

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) 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. init_xs \<noteq> [] proof (state)
this:
init_xs \<noteq> []

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (chain)
picking this:
length (y # ys) \<le> length init_xs
init_xs \<noteq> [] proof (prove)
using this:
length (y # ys) \<le> length init_xs
init_xs \<noteq> []

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

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
using this:
length ys < length init_xs

goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> \<lbrace>F ((length init_xs - length (y # ys)) * j)\<rbrace> y \<lbrace>\<lambda>_. F (Suc (length init_xs - length (y # ys)) * j)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys \<noteq> []; length ys < length init_xs\<rbrakk> \<Longrightarrow> \<lbrace>F ((length init_xs - length (y # ys)) * j)\<rbrace> y \<lbrace>\<lambda>_. F (Suc (length init_xs - length (y # ys)) * j)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys \<noteq> []; length ys < length init_xs\<rbrakk> \<Longrightarrow> Suc (length init_xs - length (y # ys)) < length init_xs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys \<noteq> []; length ys < length init_xs\<rbrakk> \<Longrightarrow> Suc (length init_xs - Suc (length ys)) < length init_xs proof (prove)
goal (1 subgoal):
 1. \<And>y ysa. \<lbrakk>Suc (length ysa) < length init_xs; ys = y # ysa\<rbrakk> \<Longrightarrow> Suc (length init_xs - Suc (Suc (length ysa))) < length init_xs proof (prove)
goal:
No subgoals! proof (state)
this:
ys \<noteq> [] \<Longrightarrow> \<lbrace>F ((length init_xs - length (y # ys)) * j)\<rbrace> y \<lbrace>\<lambda>_. F (Suc (length init_xs - length (y # ys)) * j)\<rbrace>

goal (1 subgoal):
 1. \<And>x1 xs. \<lbrakk>xs = drop (length init_xs - length xs) init_xs \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))); x1 # xs = drop (length init_xs - length (x1 # xs)) init_xs\<rbrakk> \<Longrightarrow> \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. x1 # xs \<noteq> [] \<longrightarrow> F ((length init_xs - length (x1 # xs)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (x1 # xs)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (x1 # xs)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (1 subgoal):
 1. \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. y # ys \<noteq> [] \<longrightarrow> F ((length init_xs - length (y # ys)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (y # ys)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
using this:
i + length init_xs * j < 2 ^ LENGTH('c)

goal (1 subgoal):
 1. \<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. y # ys \<noteq> [] \<longrightarrow> F ((length init_xs - length (y # ys)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (y # ys)) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (1 subgoal):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (F ((length init_xs - Suc (length ys)) * j)) ({s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q) hs (do v <- y;
vs <- Nondet_Monad.sequence ys;
return (v # vs)
od) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (2 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q10 zs) (?Q'10 zs) hs (do v <- y;
vs <- Nondet_Monad.sequence ys;
return (v # vs)
od) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> ?Q10 zs s \<and> s' \<in> ?Q'10 zs proof (prove)
goal (2 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q10 zs) (?Q'10 zs) hs (do v <- y;
vs <- Nondet_Monad.sequence ys;
return (v # vs)
od) (IF P \<acute>xf THEN
  body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))
FI)
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> ?Q10 zs s \<and> s' \<in> ?Q'10 zs proof (prove)
goal (2 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q10 zs) (?R'16 zs) hs (do v <- y;
vs <- Nondet_Monad.sequence ys;
return (v # vs)
od) (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> ?Q10 zs s \<and> s' \<in> ?R'16 zs \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q10 zs) (?R'16 zs) hs (do v <- y;
vs <- Nondet_Monad.sequence ys;
return (v # vs)
od) (body;;
(Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))))
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> ?Q10 zs s \<and> s' \<in> ?R'16 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> ccorresG rf_sr \<Gamma> (?r'20 zs) (?xf'20 zs) (?P20 zs) (?P'20 zs) hs y body
 2. \<And>zs rv' t t'. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> ceqv \<Gamma> (?xf'20 zs) rv' t t' (Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) (?d'20 zs rv')
 3. \<And>zs rv rv'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); ?r'20 zs rv rv'\<rbrakk> \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q20 zs rv) (?Q'20 zs rv rv') hs (do vs <- Nondet_Monad.sequence ys;
return (rv # vs)
od) (?d'20 zs rv')
 4. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>
 5. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. ?r'20 zs rv (?xf'20 zs s) \<longrightarrow> s \<in> ?Q'20 zs rv (?xf'20 zs s)}
 6. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<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 (5 subgoals):
 1. \<And>zs rv' t t'. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' (Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) (?d'20 zs rv')
 2. \<And>zs rv rv'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q20 zs rv) (?Q'20 zs rv rv') hs (do vs <- Nondet_Monad.sequence ys;
return (rv # vs)
od) (?d'20 zs rv')
 3. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>
 4. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> ?Q'20 zs rv (xf' s)}
 5. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (4 subgoals):
 1. \<And>zs rv rv'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q20 zs rv) (?Q'20 zs rv rv') hs (do vs <- Nondet_Monad.sequence ys;
return (rv # vs)
od) (Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s);;
While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>
 3. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> ?Q'20 zs rv (xf' s)}
 4. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs rv rv'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q20 zs rv) (?Q'27 zs rv rv') hs (do vs <- Nondet_Monad.sequence ys;
return (rv # vs)
od) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>zs rv rv'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) (?Q'27 zs rv rv')
 3. \<And>zs rv rv' s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'; ?Q20 zs rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) {s'. (s, s') \<in> rf_sr}
 4. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>
 5. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> ?Q'20 zs rv (xf' s)}
 6. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs rv rv'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> ccorresG rf_sr \<Gamma> (\<lambda>x (i', rv'). r' (zs @ rv # x) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (?Q20 zs rv) (?Q'27 zs rv rv') hs (Nondet_Monad.sequence ys) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s)))
 2. \<And>zs rv rv'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) (?Q'27 zs rv rv')
 3. \<And>zs rv rv' s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'; ?Q20 zs rv s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) {s'. (s, s') \<in> rf_sr}
 4. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>?Q20 zs\<rbrace>
 5. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> ?Q'20 zs rv (xf' s)}
 6. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (6 subgoals):
 1. \<And>zs rv rv' x y. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'; case (xf y, xf' y) of (i', rv') \<Rightarrow> r' ((zs @ [rv]) @ x) rv' \<and> i' = word_of_nat (i + length init_xs * j)\<rbrakk> \<Longrightarrow> case (xf y, xf' y) of (i', rv') \<Rightarrow> r' (zs @ rv # x) rv' \<and> i' = word_of_nat (i + length init_xs * j)
 2. \<And>zs rv rv'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) ({s. xf s = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' s)} \<inter> Q)
 3. \<And>zs rv rv' s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'; ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) {s'. (s, s') \<in> rf_sr}
 4. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv s. ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrace>
 5. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> ?Q'20 zs rv (xf' s)}
 6. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (5 subgoals):
 1. \<And>zs rv rv'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv') Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) ({s. xf s = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' s)} \<inter> Q)
 2. \<And>zs rv rv' s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'; ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q'20 zs rv rv' \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) {s'. (s, s') \<in> rf_sr}
 3. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv s. ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrace>
 4. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> ?Q'20 zs rv (xf' s)}
 5. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (4 subgoals):
 1. \<And>zs rv rv' s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'; ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ({s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q} \<inter> {s'. (s, s') \<in> rf_sr}) Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) {s'. (s, s') \<in> rf_sr}
 2. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv s. ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrace>
 3. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q}}
 4. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (5 subgoals):
 1. \<And>zs rv rv' s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'; ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'38 zs rv rv' s) Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s) {s'. (s, s') \<in> rf_sr}
 2. \<And>zs rv rv' s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'; ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrakk> \<Longrightarrow> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q} \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> ?P'38 zs rv rv' s
 3. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv s. ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrace>
 4. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q}}
 5. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (4 subgoals):
 1. \<And>zs rv rv' s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); r' (zs @ [rv]) rv'; ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrakk> \<Longrightarrow> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q} \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, xf_update (\<lambda>_. xf sa + word_of_nat j) sa) \<in> rf_sr}
 2. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv s. ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrace>
 3. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q}}
 4. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R20 zs\<rbrace> y \<lbrace>\<lambda>rv s. ys \<noteq> [] \<longrightarrow> F ((length init_xs - length ys) * j) s\<rbrace>
 2. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q}}
 3. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R20 zs) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<lbrace>?R55 zs (?zs55 zs)\<rbrace> y \<lbrace>\<lambda>rv s. ys \<noteq> [] \<longrightarrow> F (Suc (length init_xs - length (y # ys)) * j) s\<rbrace>
 2. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q}}
 3. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R55 zs (?zs55 zs)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); ys \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>?R55 zs (?zs55 zs)\<rbrace> y \<lbrace>\<lambda>rv. F (Suc (length init_xs - length (y # ys)) * j)\<rbrace>
 2. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q}}
 3. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and ?R55 zs (?zs55 zs)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); ys \<noteq> []\<rbrakk> \<Longrightarrow> ys \<noteq> []
 2. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q}}
 3. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and F ((length init_xs - length (y # ys)) * j)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. \<forall>rv. r' (zs @ [rv]) (xf' s) \<longrightarrow> s \<in> {s. xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat (i + (length init_xs - length ys) * j) \<and> r' (zs @ [rv]) (xf' (xf_update (\<lambda>_. xf s + word_of_nat j) s)) \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q}}
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and F ((length init_xs - length (y # ys)) * j)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?R'20 zs) body {s. (\<exists>rv. r' (zs @ [rv]) (xf' s)) \<longrightarrow> xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat i + word_of_nat (length init_xs - length ys) * word_of_nat j \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q}
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and F ((length init_xs - length (y # ys)) * j)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ?R'20 zs \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs. i + length init_xs * j < 2 ^ LENGTH('c) \<Longrightarrow> \<forall>s\<in>{s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q. \<exists>P' Q' A'. \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> P' body Q',A' \<and> s \<in> P' \<and> Q' \<subseteq> {s. (\<exists>rv. r' (zs @ [rv]) (xf' s)) \<longrightarrow> xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat i + word_of_nat (length init_xs - length ys) * word_of_nat j \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q} \<and> A' \<subseteq> {}
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and F ((length init_xs - length (y # ys)) * j)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ({s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q) \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); s \<in> {s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?P'63 zs s) body (?Q'64 zs s),(?A'65 zs s) \<and> s \<in> ?P'63 zs s \<and> ?Q'64 zs s \<subseteq> {s. (\<exists>rv. r' (zs @ [rv]) (xf' s)) \<longrightarrow> xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat i + word_of_nat (length init_xs - length ys) * word_of_nat j \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q} \<and> ?A'65 zs s \<subseteq> {}
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and F ((length init_xs - length (y # ys)) * j)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ({s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q) \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); s \<in> {s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/?F20 zs\<^esub> (?P'63 zs s) body (?Q'64 zs s),(?A'65 zs s)
 2. \<And>zs s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); s \<in> {s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q\<rbrakk> \<Longrightarrow> s \<in> ?P'63 zs s \<and> ?Q'64 zs s \<subseteq> {s. (\<exists>rv. r' (zs @ [rv]) (xf' s)) \<longrightarrow> xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat i + word_of_nat (length init_xs - length ys) * word_of_nat j \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q} \<and> ?A'65 zs s \<subseteq> {}
 3. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and F ((length init_xs - length (y # ys)) * j)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ({s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q) \<inter> {s. P (xf s)} proof (prove)
goal (3 subgoals):
 1. \<And>zs s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); s \<in> {s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q\<rbrakk> \<Longrightarrow> xf s < word_of_nat (i + length xs * j)
 2. \<And>zs s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); s \<in> {s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q\<rbrakk> \<Longrightarrow> s \<in> {s} \<inter> Q \<and> {t. xf t = xf s \<and> xf_update (\<lambda>_. xf t + word_of_nat j) t \<in> Q} \<subseteq> {s. (\<exists>rv. r' (zs @ [rv]) (xf' s)) \<longrightarrow> xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat i + word_of_nat (length init_xs - length ys) * word_of_nat j \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q} \<and> {} \<subseteq> {}
 3. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and F ((length init_xs - length (y # ys)) * j)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ({s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q) \<inter> {s. P (xf s)} proof (prove)
goal (2 subgoals):
 1. \<And>zs s. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); s \<in> {s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q\<rbrakk> \<Longrightarrow> s \<in> {s} \<inter> Q \<and> {t. xf t = xf s \<and> xf_update (\<lambda>_. xf t + word_of_nat j) t \<in> Q} \<subseteq> {s. (\<exists>rv. r' (zs @ [rv]) (xf' s)) \<longrightarrow> xf (xf_update (\<lambda>_. xf s + word_of_nat j) s) = word_of_nat i + word_of_nat (length init_xs - length ys) * word_of_nat j \<and> xf_update (\<lambda>_. xf s + word_of_nat j) s \<in> Q} \<and> {} \<subseteq> {}
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and F ((length init_xs - length (y # ys)) * j)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ({s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q) \<inter> {s. P (xf s)} proof (prove)
goal (1 subgoal):
 1. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; s' \<in> {s. xf s = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j \<and> r' zs (xf' s)} \<inter> Q\<rbrakk> \<Longrightarrow> (F ((length init_xs - length (y # ys)) * j) and F ((length init_xs - length (y # ys)) * j)) s \<and> s' \<in> {s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q \<inter> ({s. P (xf s) \<and> xf s + word_of_nat j = word_of_nat (i + (length init_xs - length ys) * of_nat j)} \<inter> Q) \<inter> {s. P (xf s)} proof (prove)
goal (1 subgoal):
 1. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; xf s' = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j; r' zs (xf' s'); s' \<in> Q\<rbrakk> \<Longrightarrow> word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j < word_of_nat i + word_of_nat (length init_xs) * word_of_nat j proof (prove)
goal (1 subgoal):
 1. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; xf s' = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j; r' zs (xf' s'); s' \<in> Q\<rbrakk> \<Longrightarrow> word_of_nat i + word_of_nat ((length init_xs - Suc (length ys)) * j) < word_of_nat i + word_of_nat (length init_xs * j) proof (prove)
goal (1 subgoal):
 1. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; xf s' = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j; r' zs (xf' s'); s' \<in> Q\<rbrakk> \<Longrightarrow> word_of_nat (i + (length init_xs - Suc (length ys)) * j) < word_of_nat (i + length init_xs * j) proof (prove)
goal (2 subgoals):
 1. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; xf s' = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j; r' zs (xf' s'); s' \<in> Q\<rbrakk> \<Longrightarrow> i + length init_xs * j < 2 ^ LENGTH('c)
 2. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; xf s' = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j; r' zs (xf' s'); s' \<in> Q\<rbrakk> \<Longrightarrow> i + (length init_xs - Suc (length ys)) * j < i + length init_xs * j proof (prove)
goal (1 subgoal):
 1. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; xf s' = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j; r' zs (xf' s'); s' \<in> Q\<rbrakk> \<Longrightarrow> i + (length init_xs - Suc (length ys)) * j < i + length init_xs * j proof (prove)
goal (1 subgoal):
 1. \<And>zs s s'. \<lbrakk>i + length init_xs * j < 2 ^ LENGTH('c); (s, s') \<in> rf_sr; F ((length init_xs - Suc (length ys)) * j) s; xf s' = word_of_nat i + word_of_nat (length init_xs - Suc (length ys)) * word_of_nat j; r' zs (xf' s'); s' \<in> Q\<rbrakk> \<Longrightarrow> length init_xs - Suc (length ys) < length init_xs proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv a. case a of (i', rv') \<Rightarrow> r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. y # ys \<noteq> [] \<longrightarrow> F ((length init_xs - length (y # ys)) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length (y # ys)) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence (y # ys)) (While {s. P (xf s)} (body;;
\<acute>xf :== \<acute>xf + word_of_nat j))

goal:
No subgoals! proof (state)
this:
\<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
\<acute>xf :== \<acute>xf + word_of_nat j))

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
using this:
\<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
\<acute>xf :== \<acute>xf + word_of_nat j))

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
using this:
\<forall>zs. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' (zs @ rv) rv' \<and> i' = word_of_nat (i + length init_xs * j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. xs \<noteq> [] \<longrightarrow> F ((length init_xs - length xs) * j) s) ({s. xf s = word_of_nat (i + (length init_xs - length xs) * j) \<and> r' zs (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
\<acute>xf :== \<acute>xf + word_of_nat j))
i + length xs * j < 2 ^ LENGTH('c)
0 < j
P ?n = (?n < word_of_nat (i + length xs * j))

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal:
No subgoals! proof (state)
this:
ccorresG rf_sr \<Gamma> (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
\<acute>xf :== \<acute>xf + word_of_nat j))

goal:
No subgoals!