theory PSpace_C

lemma setObject_ccorres_helper:
  fixes ko :: "'a :: pspace_storable"
  assumes valid: "\<And>\<sigma> (ko' :: 'a).
        \<Gamma> \<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ko_at' ko' p \<sigma>}
              c {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKO ko)\<rparr>, s) \<in> rf_sr}"
  shows "\<lbrakk> \<And>ko :: 'a. updateObject ko = updateObject_default ko;
           \<And>ko :: 'a. (1 :: word32) < 2 ^ objBits ko \<rbrakk>
    \<Longrightarrow> ccorres dc xfdc P P' hs (setObject p ko) c" apply (rule ccorres_guard_imp2) apply (subst setObject_obj_at_pre) apply simp+ apply (rule ccorres_symb_exec_l[where Q'="\<lambda>_. P'"]) defer apply (rule stateAssert_inv) apply (rule stateAssert_sp[where P=P]) apply (rule empty_fail_stateAssert) apply simp apply (rule ccorres_from_vcg) apply (rule allI) apply (rule hoare_complete) apply (clarsimp simp: HoarePartialDef.valid_def) apply (simp add: typ_at_to_obj_at' koTypeOf_injectKO) apply (drule obj_at_ko_at', clarsimp) apply (cut_tac \<sigma>1=\<sigma> and ko'1=koa in valid) apply (drule hoare_sound,
         clarsimp simp: cvalid_def HoarePartialDef.valid_def) apply (elim allE, drule(1) mp) apply (drule mp, simp) apply clarsimp apply (rule imageI[OF CollectI]) apply (rule rev_bexI) apply (rule setObject_eq, simp+) apply (simp add: objBits_def) apply (simp only: objBitsT_koTypeOf[symmetric]
                      koTypeOf_injectKO) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc P P' hs (setObject p ko) c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q ?Q' hs (setObject p ko) c
 2. \<And>s s'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> updateObject ko = updateObject_default ko
 2. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits ko
 3. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q ?Q' hs (do _ <- stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [];
setObject p ko
od) c
 4. \<And>s s'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q ?Q' hs (do _ <- stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [];
setObject p ko
od) c
 2. \<And>s s'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (5 subgoals):
 1. \<And>uu_. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 uu_) P' hs (setObject p ko) c
 2. \<And>s. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [] \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [] \<lbrace>?Q6\<rbrace>
 4. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [])
 5. \<And>s s'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q6 rv s \<longrightarrow> s' \<in> P'} proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [] \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [] \<lbrace>?Q6\<rbrace>
 3. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [])
 4. \<And>s s'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q6 rv s \<longrightarrow> s' \<in> P'}
 5. \<And>uu_. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 uu_) P' hs (setObject p ko) c proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [] \<lbrace>?Q6\<rbrace>
 2. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [])
 3. \<And>s s'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q6 rv s \<longrightarrow> s' \<in> P'}
 4. \<And>uu_. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 uu_) P' hs (setObject p ko) c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> empty_fail (stateAssert (typ_at' (koTypeOf (injectKOS ko)) p) [])
 2. \<And>s s'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (P and typ_at' (koTypeOf (injectKOS ko)) p) s \<longrightarrow> s' \<in> P'}
 3. \<And>_. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc (P and typ_at' (koTypeOf (injectKOS ko)) p) P' hs (setObject p ko) c proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; (s, s') \<in> rf_sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> P s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (P and typ_at' (koTypeOf (injectKOS ko)) p) s \<longrightarrow> s' \<in> P'}
 2. \<And>_. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc (P and typ_at' (koTypeOf (injectKOS ko)) p) P' hs (setObject p ko) c proof (prove)
goal (1 subgoal):
 1. \<And>_. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> ccorres dc xfdc (P and typ_at' (koTypeOf (injectKOS ko)) p) P' hs (setObject p ko) c proof (prove)
goal (1 subgoal):
 1. \<And>_. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (P and typ_at' (koTypeOf (injectKOS ko)) p) \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (setObject p ko \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>_ \<sigma>. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (P and typ_at' (koTypeOf (injectKOS ko)) p) \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (setObject p ko \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>_ \<sigma>. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko\<rbrakk> \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> {s. (P and typ_at' (koTypeOf (injectKOS ko)) p) \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (setObject p ko \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)},{} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P \<sigma>; typ_at' (koTypeOf (injectKOS ko)) p \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x\<in>fst (setObject p ko \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P \<sigma>; obj_at' (\<lambda>_. True) p \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x\<in>fst (setObject p ko \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x koa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x\<in>fst (setObject p ko \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x koa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr \<and> P \<sigma> \<and> s \<in> P' \<and> ko_at' koa p \<sigma>} c {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, s) \<in> rf_sr}\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x\<in>fst (setObject p ko \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x koa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; \<forall>s t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` {s. (\<sigma>, s) \<in> rf_sr \<and> s \<in> P'} \<longrightarrow> t \<in> Normal ` {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, s) \<in> rf_sr}\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x\<in>fst (setObject p ko \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x koa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; Normal x \<in> Normal ` {s. (\<sigma>, s) \<in> rf_sr \<and> s \<in> P'} \<longrightarrow> t \<in> Normal ` {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, s) \<in> rf_sr}\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x\<in>fst (setObject p ko \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x koa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; t \<in> Normal ` {s. (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, s) \<in> rf_sr}\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. \<exists>x\<in>fst (setObject p ko \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> Normal xa \<in> Normal ` {s. \<exists>x\<in>fst (setObject p ko \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (setObject p ko \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', xa) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> ?x52 \<sigma> x koa xa \<in> fst (setObject p ko \<sigma>)
 2. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> case ?x52 \<sigma> x koa xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', xa) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x koa xa v v'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> objBits v = objBits v'
 2. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> obj_at' (?P55 \<sigma> x koa xa) p \<sigma>
 3. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> case ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', xa) \<in> rf_sr proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x koa xa v v'. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBitsKO (injectKOS ko); \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> objBitsKO (injectKOS v) = objBitsKO (injectKOS v')
 2. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> obj_at' (?P55 \<sigma> x koa xa) p \<sigma>
 3. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> case ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', xa) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> obj_at' (?P55 \<sigma> x koa xa) p \<sigma>
 2. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> case ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', xa) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x koa xa. \<lbrakk>\<And>ko. updateObject ko = updateObject_default ko; \<And>ko. 1 < 2 ^ objBits ko; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> Normal xa; P \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; ko_at' koa p \<sigma>; (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>, xa) \<in> rf_sr\<rbrakk> \<Longrightarrow> case ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(p \<mapsto> injectKOS ko)\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', xa) \<in> rf_sr proof (prove)
goal:
No subgoals!