theory Recycle_C

lemma mapM_x_store_memset_ccorres_assist:
  fixes val :: "'a :: pspace_storable"
  assumes nofail: "\<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>)"
  assumes slots1: "\<forall>n < length slots. slots ! n = hd slots + (of_nat n << objBits val)"
  assumes slots2: "n = length slots * (2 ^ objBits val)"
  assumes ptr: "ptr = hd slots"
  assumes ko: "\<And>ko :: 'a. updateObject ko = updateObject_default ko"
              "\<And>ko :: 'a. (1 :: word32) < 2 ^ objBits ko"
  assumes restr: "set slots \<subseteq> S"
  assumes worker: "\<And>ptr s s' (ko :: 'a). \<lbrakk> (s, s') \<in> rf_sr; ko_at' ko ptr s; ptr \<in> S \<rbrakk>
                                \<Longrightarrow> (s \<lparr> ksPSpace := (ksPSpace s)(ptr \<mapsto> injectKO val)\<rparr>,
                                     globals_update (t_hrs_'_update (hrs_mem_update
                                                    (heap_update_list ptr
                                                    (replicateHider (2 ^ objBits val) (ucast c))))) s') \<in> rf_sr"
  assumes rf_sr: "(\<sigma>, s) \<in> rf_sr"
  shows
  "\<exists>(rv, \<sigma>') \<in> fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>).
      (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update
                          (heap_update_list ptr (replicateHider n c)))) s) \<in> rf_sr" unfolding slots2 ptr using rf_sr slots1 nofail restr proof (induct slots arbitrary: s \<sigma>) case Nil show ?case using Nil.prems apply (simp add: mapM_x_def sequence_x_def return_def replicateHider_def) apply (simp add: rf_sr_def hrs_mem_update_def cstate_relation_def Let_def
                     carch_state_relation_def cmachine_state_relation_def
                     h_t_valid_clift_Some_iff) done next case (Cons x xs tPre sPre) note nofail_bind = Cons.prems(3)[unfolded mapM_x_Cons K_bind_def] have obj_at: "obj_at' (\<lambda>x :: 'a. True) x sPre" using not_snd_bindI1[OF nofail_bind] apply (subst(asm) setObject_obj_at_pre, simp_all add: ko snd_bind) apply (clarsimp simp: stateAssert_def exec_get return_def) apply (simp add: koTypeOf_injectKO typ_at_to_obj_at') done note in_setObject = setObject_eq[OF _ _ objBits_eq_by_type obj_at,
                                   where ko=val, simplified ko, simplified] note nofail_mapM = not_snd_bindI2[OF nofail_bind, OF in_setObject] have hd_xs: "xs \<noteq> [] \<Longrightarrow> hd xs = x + (2 ^ objBits val)" using Cons.prems(2)[rule_format, where n=1] by (simp add: hd_conv_nth) show ?case using obj_at_ko_at'[OF obj_at] Cons.prems(4) apply (clarsimp simp add: mapM_x_Cons bind_def split_def) apply (rule rev_bexI, rule in_setObject) apply (cut_tac Cons.hyps[OF _ _ nofail_mapM]) defer apply (rule worker, rule Cons.prems, assumption+) apply clarsimp apply (case_tac "xs = []", simp_all)[1] apply (insert Cons.prems, simp)[1] apply (frule_tac x="Suc n" in spec) apply (simp add: hd_xs shiftl_t2n field_simps) apply assumption apply clarsimp apply (rule rev_bexI, assumption) apply (simp add: o_def) apply (case_tac "xs = []") apply (simp add: hrs_mem_update_def split_def replicateHider_def) apply (subst(asm) heap_update_list_concat_fold_hrs_mem) apply (simp add: hd_xs replicateHider_def) apply (simp add: replicateHider_def replicate_add) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptr (replicateHider n c)))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (prove)
using this:
(\<sigma>, s) \<in> rf_sr
\<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val)
\<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>)
set slots \<subseteq> S

goal (1 subgoal):
 1. \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (state)
goal (2 subgoals):
 1. \<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length []. [] ! n = hd [] + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) [] \<sigma>); set [] \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) [] \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd []) (replicateHider (length [] * 2 ^ objBits val) c)))) s) \<in> rf_sr
 2. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (state)
this:
(\<sigma>, s) \<in> rf_sr
\<forall>n<length []. [] ! n = hd [] + (word_of_nat n << objBits val)
\<not> snd (mapM_x (\<lambda>slot. setObject slot val) [] \<sigma>)
set [] \<subseteq> S

goal (2 subgoals):
 1. \<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length []. [] ! n = hd [] + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) [] \<sigma>); set [] \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) [] \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd []) (replicateHider (length [] * 2 ^ objBits val) c)))) s) \<in> rf_sr
 2. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) [] \<sigma>). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd []) (replicateHider (length [] * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (prove)
using this:
(\<sigma>, s) \<in> rf_sr
\<forall>n<length []. [] ! n = hd [] + (word_of_nat n << objBits val)
\<not> snd (mapM_x (\<lambda>slot. setObject slot val) [] \<sigma>)
set [] \<subseteq> S

goal (1 subgoal):
 1. \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) [] \<sigma>). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd []) (replicateHider (length [] * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. (\<sigma>, s) \<in> rf_sr \<Longrightarrow> (\<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (\<lambda>a. a))) s) \<in> rf_sr proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) [] \<sigma>). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd []) (replicateHider (length [] * 2 ^ objBits val) c)))) s) \<in> rf_sr

goal (1 subgoal):
 1. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (state)
goal (1 subgoal):
 1. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (state)
this:
\<lbrakk>(?\<sigma>2, ?s2) \<in> rf_sr; \<forall>n<length xs. xs ! n = hd xs + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) xs ?\<sigma>2); set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs ?\<sigma>2). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) ?s2) \<in> rf_sr
(sPre, tPre) \<in> rf_sr
\<forall>n<length (x # xs). (x # xs) ! n = hd (x # xs) + (word_of_nat n << objBits val)
\<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x # xs) sPre)
set (x # xs) \<subseteq> S

goal (1 subgoal):
 1. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (state)
this:
\<not> snd ((do y <- setObject x val;
mapM_x (\<lambda>slot. setObject slot val) xs
od) sPre)

goal (1 subgoal):
 1. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. obj_at' (\<lambda>x. True) x sPre proof (prove)
using this:
\<not> snd (setObject x val sPre)

goal (1 subgoal):
 1. obj_at' (\<lambda>x. True) x sPre proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (stateAssert (typ_at' (koTypeOf (injectKOS val)) x) [] sPre) \<and> (\<forall>xa\<in>fst (stateAssert (typ_at' (koTypeOf (injectKOS val)) x) [] sPre). \<not> (case xa of (r, s') \<Rightarrow> snd (setObject x val s'))); \<not> snd (setObject x val sPre)\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) x sPre proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (setObject x val sPre); typ_at' (koTypeOf (injectKOS val)) x sPre\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) x sPre proof (prove)
goal:
No subgoals! proof (state)
this:
obj_at' (\<lambda>x. True) x sPre

goal (1 subgoal):
 1. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (state)
this:
((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>) \<in> fst (setObject x val sPre)

goal (1 subgoal):
 1. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (state)
this:
\<not> snd (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))

goal (1 subgoal):
 1. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> hd xs = x + 2 ^ objBits val proof (prove)
using this:
1 < length (x # xs) \<Longrightarrow> (x # xs) ! 1 = hd (x # xs) + (word_of_nat 1 << objBits val)

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> hd xs = x + 2 ^ objBits val proof (state)
this:
xs \<noteq> [] \<Longrightarrow> hd xs = x + 2 ^ objBits val

goal (1 subgoal):
 1. \<And>x1 slots s \<sigma>. \<lbrakk>\<And>s \<sigma>. \<lbrakk>(\<sigma>, s) \<in> rf_sr; \<forall>n<length slots. slots ! n = hd slots + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>); set slots \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) slots \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd slots) (replicateHider (length slots * 2 ^ objBits val) c)))) s) \<in> rf_sr; (\<sigma>, s) \<in> rf_sr; \<forall>n<length (x1 # slots). (x1 # slots) ! n = hd (x1 # slots) + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>); set (x1 # slots) \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>(rv, \<sigma>')\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x1 # slots) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x1 # slots)) (replicateHider (length (x1 # slots) * 2 ^ objBits val) c)))) s) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x # xs) sPre). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x # xs)) (replicateHider (length (x # xs) * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
using this:
\<exists>ko. ko_at' ko x sPre \<and> True
set (x # xs) \<subseteq> S

goal (1 subgoal):
 1. \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x # xs) sPre). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x # xs)) (replicateHider (length (x # xs) * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (setObject x val sPre). \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd y)). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (4 subgoals):
 1. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) (?s34 ko)) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr
 2. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>, ?s34 ko) \<in> rf_sr
 3. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<forall>n<length xs. xs ! n = hd xs + (word_of_nat n << objBits val)
 4. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> set xs \<subseteq> S proof (prove)
goal (4 subgoals):
 1. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>, ?s34 ko) \<in> rf_sr
 2. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<forall>n<length xs. xs ! n = hd xs + (word_of_nat n << objBits val)
 3. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> set xs \<subseteq> S
 4. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) (?s34 ko)) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<forall>n<length xs. xs ! n = hd xs + (word_of_nat n << objBits val)
 2. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> set xs \<subseteq> S
 3. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) (globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) (UCAST(8 \<rightarrow> 8) c))))) tPre)) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>ko n. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; n < length xs\<rbrakk> \<Longrightarrow> xs ! n = hd xs + (word_of_nat n << objBits val)
 2. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> set xs \<subseteq> S
 3. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) (globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) (UCAST(8 \<rightarrow> 8) c))))) tPre)) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>ko n. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; n < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs ! n = hd xs + (word_of_nat n << objBits val)
 2. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> set xs \<subseteq> S
 3. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) (globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) (UCAST(8 \<rightarrow> 8) c))))) tPre)) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>ko n. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; n < length xs; xs \<noteq> []; (sPre, tPre) \<in> rf_sr; \<forall>n<Suc (length xs). (x # xs) ! n = x + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x # xs) sPre)\<rbrakk> \<Longrightarrow> xs ! n = hd xs + (word_of_nat n << objBits val)
 2. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> set xs \<subseteq> S
 3. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) (globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) (UCAST(8 \<rightarrow> 8) c))))) tPre)) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>ko n. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; n < length xs; xs \<noteq> []; (sPre, tPre) \<in> rf_sr; \<forall>n<Suc (length xs). (x # xs) ! n = x + (word_of_nat n << objBits val); \<not> snd (mapM_x (\<lambda>slot. setObject slot val) (x # xs) sPre); Suc n < Suc (length xs) \<longrightarrow> (x # xs) ! Suc n = x + (word_of_nat (Suc n) << objBits val)\<rbrakk> \<Longrightarrow> xs ! n = hd xs + (word_of_nat n << objBits val)
 2. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> set xs \<subseteq> S
 3. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) (globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) (UCAST(8 \<rightarrow> 8) c))))) tPre)) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S\<rbrakk> \<Longrightarrow> set xs \<subseteq> S
 2. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) (globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) (UCAST(8 \<rightarrow> 8) c))))) tPre)) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; \<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)))) (globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) (UCAST(8 \<rightarrow> 8) c))))) tPre)) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (snd ((), sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>ko b. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; ((), b) \<in> fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)); (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c))) \<circ> t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) c)))) tPre) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>ko b. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; ((), b) \<in> fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)); (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c))) \<circ> t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) c)))) tPre) \<in> rf_sr\<rbrakk> \<Longrightarrow> (snd ((), b), globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>ko b. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; ((), b) \<in> fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)); (b, globals_update (t_hrs_'_update (\<lambda>xa. hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)) (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) c)) xa))) tPre) \<in> rf_sr\<rbrakk> \<Longrightarrow> (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>ko b. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; ((), b) \<in> fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)); (b, globals_update (t_hrs_'_update (\<lambda>xa. hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)) (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) c)) xa))) tPre) \<in> rf_sr; xs = []\<rbrakk> \<Longrightarrow> (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr
 2. \<And>ko b. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; ((), b) \<in> fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)); (b, globals_update (t_hrs_'_update (\<lambda>xa. hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)) (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) c)) xa))) tPre) \<in> rf_sr; xs \<noteq> []\<rbrakk> \<Longrightarrow> (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>ko b. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; ((), b) \<in> fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)); (b, globals_update (t_hrs_'_update (\<lambda>xa. hrs_mem_update (heap_update_list (hd xs) (replicateHider (length xs * 2 ^ objBits val) c)) (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) c)) xa))) tPre) \<in> rf_sr; xs \<noteq> []\<rbrakk> \<Longrightarrow> (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>ko b. \<lbrakk>xs \<noteq> []; ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; ((), b) \<in> fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>))\<rbrakk> \<Longrightarrow> hd xs = x + word_of_nat (length (replicateHider (2 ^ objBits val) c))
 2. \<And>ko b. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; ((), b) \<in> fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)); (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) c @ replicateHider (length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr; xs \<noteq> []\<rbrakk> \<Longrightarrow> (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>ko b. \<lbrakk>ko_at' ko x sPre; x \<in> S; set xs \<subseteq> S; ((), b) \<in> fst (mapM_x (\<lambda>slot. setObject slot val) xs (sPre\<lparr>ksPSpace := (ksPSpace sPre)(x \<mapsto> injectKOS val)\<rparr>)); (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val) c @ replicateHider (length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr; xs \<noteq> []\<rbrakk> \<Longrightarrow> (b, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list x (replicateHider (2 ^ objBits val + length xs * 2 ^ objBits val) c)))) tPre) \<in> rf_sr proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>a\<in>fst (mapM_x (\<lambda>slot. setObject slot val) (x # xs) sPre). case a of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list (hd (x # xs)) (replicateHider (length (x # xs) * 2 ^ objBits val) c)))) tPre) \<in> rf_sr

goal:
No subgoals!